From 7d515acbc5d83aa2300b71a9b7712b3da1d3d2e3 Mon Sep 17 00:00:00 2001 From: herbelin Date: Mon, 4 Aug 2008 18:10:48 +0000 Subject: Évolutions diverses et variées. - Correction divers messages d'erreur - lorsque rien à réécrire dans une hyp, - lorsqu'une variable ltac n'est pas liée, - correction anomalie en présence de ?id dans le "as" de induction, - correction mauvais env dans message d'erreur de unify_0. - Diverses extensions et améliorations - "specialize" : - extension au cas (fun x1 ... xn => H u1 ... un), - renommage au même endroit. - "assert" et "pose proof" peuvent réutiliser la même hyp comme "specialize". - "induction" - intro des IH toujours au sommet même si induction sur var quantifiée, - ajout d'un hack pour la reconnaissance de schémas inductifs comme N_ind_double mais il reste du boulot pour reconnaître (et/ou réordonner) les composantes d'un schéma dont les hypothèses ne sont pas dans l'ordre standard, - vérification de longueur et éventuelle complétion des intropatterns dans le cas de sous-patterns destructifs dans induction (par exemple "destruct n as [|[|]]" sur "forall n, n=0" ne mettait pas le n dans le contexte), - localisation des erreurs d'intropattern, - ajout d'un pattern optionnel après "as" pour forcer une égalité et la nommer (*). - "apply" accepte plusieurs arguments séparés par des virgules (*). - Plus de robustesse pour clear en présence d'evars. - Amélioration affichage TacFun dans Print Ltac. - Vieux pb espace en trop en tête d'affichage des tactiques EXTEND résolu (incidemment, ça remodifie une nouvelle fois le test output Fixpoint.v !). - Fusion VTactic/VFun dans l'espoir. - Mise en place d'un système de trace de la pile des appels Ltac (tout en préservant certains aspects de la récursivité terminale - cf bug #468). - Tactiques primitives - ajout de "move before" dans les tactiques primitives et ajout des syntaxes move before et move dependent au niveau utilisateur (*), - internal_cut peuvent faire du remplacement de nom d'hypothèse existant, - suppression de Intro_replacing et du code sous-traitant - Nettoyage - Suppression cible et fichiers minicoq non portés depuis longtemps. (*) Extensions de syntaxe qu'il pourrait être opportun de discuter git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11300 85f007b7-540e-0410-9357-904b9bb8a0f7 --- lib/flags.ml | 4 ++-- lib/util.ml | 33 +++++++++++++++++++++++++++++++++ lib/util.mli | 3 +++ 3 files changed, 38 insertions(+), 2 deletions(-) (limited to 'lib') diff --git a/lib/flags.ml b/lib/flags.ml index 0378e11fb4..76ab9fe64b 100644 --- a/lib/flags.ml +++ b/lib/flags.ml @@ -8,8 +8,6 @@ (*i $Id$ i*) -open Util - let with_option o f x = let old = !o in o:=true; try let r = f x in o := old; r @@ -78,6 +76,8 @@ let print_hyps_limit () = !print_hyps_limit (* A list of the areas of the system where "unsafe" operation * has been requested *) +module Stringset = Set.Make(struct type t = string let compare = compare end) + let unsafe_set = ref Stringset.empty let add_unsafe s = unsafe_set := Stringset.add s !unsafe_set let is_unsafe s = Stringset.mem s !unsafe_set diff --git a/lib/util.ml b/lib/util.ml index 549b79e786..94e812ff65 100644 --- a/lib/util.ml +++ b/lib/util.ml @@ -1210,6 +1210,8 @@ let pr_opt_no_spc pr = function None -> mt () | Some x -> pr x let nth n = str (ordinal n) +(* [prlist pr [a ; ... ; c]] outputs [pr a ++ ... ++ pr c] *) + let rec prlist elem l = match l with | [] -> mt () | h::t -> Stream.lapp (fun () -> elem h) (prlist elem t) @@ -1221,6 +1223,9 @@ let rec prlist_strict elem l = match l with | [] -> mt () | h::t -> (elem h)++(prlist_strict elem t) +(* [prlist_with_sep sep pr [a ; ... ; c]] outputs + [pr a ++ sep() ++ ... ++ sep() ++ pr c] *) + let rec prlist_with_sep sep elem l = match l with | [] -> mt () | [h] -> elem h @@ -1228,6 +1233,23 @@ let rec prlist_with_sep sep elem l = match l with let e = elem h and s = sep() and r = prlist_with_sep sep elem t in e ++ s ++ r +(* Print sequence of objects separated by space (unless an element is empty) *) + +let rec pr_sequence elem = function + | [] -> mt () + | [h] -> elem h + | h::t -> + let e = elem h and r = pr_sequence elem t in + if e = mt () then r else e ++ spc () ++ r + +(* [pr_enum pr [a ; b ; ... ; c]] outputs + [pr a ++ str "," ++ pr b ++ str "," ++ ... ++ str "and" ++ pr c] *) + +let pr_enum pr l = + let c,l' = list_sep_last l in + prlist_with_sep pr_coma pr l' ++ + (if l'<>[] then str " and" ++ spc () else mt()) ++ pr c + let pr_vertical_list pr = function | [] -> str "none" ++ fnl () | l -> fnl () ++ str " " ++ hov 0 (prlist_with_sep pr_fnl pr l) ++ fnl () @@ -1242,6 +1264,9 @@ let prvecti elem v = in if n = 0 then mt () else pr (n - 1) +(* [prvect_with_sep sep pr [|a ; ... ; c|]] outputs + [pr a ++ sep() ++ ... ++ sep() ++ pr c] *) + let prvect_with_sep sep elem v = let rec pr n = if n = 0 then @@ -1253,8 +1278,16 @@ let prvect_with_sep sep elem v = let n = Array.length v in if n = 0 then mt () else pr (n - 1) +(* [prvect pr [|a ; ... ; c|]] outputs [pr a ++ ... ++ pr c] *) + let prvect elem v = prvect_with_sep mt elem v +let pr_located pr (loc,x) = + if Flags.do_translate() && loc<>dummy_loc then + let (b,e) = unloc loc in + comment b ++ pr x ++ comment e + else pr x + let surround p = hov 1 (str"(" ++ p ++ str")") (*s Size of ocaml values. *) diff --git a/lib/util.mli b/lib/util.mli index d845dd2ebf..40d6046d7d 100644 --- a/lib/util.mli +++ b/lib/util.mli @@ -282,6 +282,9 @@ val prvecti : (int -> 'a -> std_ppcmds) -> 'a array -> std_ppcmds val prvect_with_sep : (unit -> std_ppcmds) -> ('b -> std_ppcmds) -> 'b array -> std_ppcmds val pr_vertical_list : ('b -> std_ppcmds) -> 'b list -> std_ppcmds +val pr_enum : ('a -> std_ppcmds) -> 'a list -> std_ppcmds +val pr_located : ('a -> std_ppcmds) -> 'a located -> std_ppcmds +val pr_sequence : ('a -> std_ppcmds) -> 'a list -> std_ppcmds val surround : std_ppcmds -> std_ppcmds -- cgit v1.2.3