diff options
| -rw-r--r-- | CHANGES | 2 | ||||
| -rw-r--r-- | TODO | 19 | ||||
| -rw-r--r-- | kernel/reduction.ml | 34 | ||||
| -rw-r--r-- | kernel/reduction.mli | 2 | ||||
| -rw-r--r-- | library/impargs.ml | 35 | ||||
| -rw-r--r-- | library/library.ml | 25 | ||||
| -rw-r--r-- | library/library.mli | 14 | ||||
| -rw-r--r-- | parsing/g_basevernac.ml4 | 2 | ||||
| -rw-r--r-- | parsing/pretty.mli | 3 | ||||
| -rw-r--r-- | toplevel/vernacentries.ml | 3 |
10 files changed, 90 insertions, 49 deletions
@@ -87,6 +87,8 @@ Tactiques - Intro échoue si le nom d'hypothèse existe au lieu de mettre un avertissement +- Plus de "Require Prolog" (intégré par défaut) + Outils - deux binaires maximum : coqtop.byte et coqtop.opt si plateforme native; @@ -1,19 +1,14 @@ Distribution: -- Faire fonctionner coqc/coqtop en non local FAIT -- "System Error (Failure): "input_value: code mismatch" quand on - charge en bytecode certains .vo compilés en natif (exemple typique: - Ring_abstract.v) COMPRIS, FAIT -- où va RELATIONS/WELLFOUNDED ? +- faire une passe sur les options de coqtop et coqc +- option -byte à coqtop +- coqc utilise coqtop.opt par défaut, sauf si -byte indiqué Environnement: - Faire fonctionner Search - Porter SearchIsos -- Faire fonctionner Abstract FAIT -- Faire fonctionner Reset FAIT -- Décider s'il faut garder Transparent/Opaque et si oui, l'implanter FAIT -- Ajouter "parsing" aux chemins par défaut (pour g_{nat,z}syntax.cmo) FAIT +- Require synchronisé Tactiques: @@ -23,6 +18,12 @@ Tactiques: Noyau: - Intégrer Let dans whd_* et les fonctions de tacred +- Gérer les alias avec un let in dans les cases + +Vernac: + +- Imprimer les paths avec "." +- Pb noms cachés (utilisation de noms absolus ?) Grammaires: diff --git a/kernel/reduction.ml b/kernel/reduction.ml index dd2adf2f5..d496a9e49 100644 --- a/kernel/reduction.ml +++ b/kernel/reduction.ml @@ -1104,40 +1104,6 @@ let is_info_type env sigma t = (s <> Prop Null && try info_arity env sigma t.utj_val with IsType -> true) -(* calcul des arguments implicites *) - -(* la seconde liste est ordonne'e *) - -let ord_add x l = - let rec aux l = match l with - | [] -> [x] - | y::l' -> if y > x then x::l else if x = y then l else y::(aux l') - in - aux l - -let add_free_rels_until bound m acc = - let rec frec depth acc c = match kind_of_term c with - | IsRel n when (n < bound+depth) & (n >= depth) -> - Intset.add (bound+depth-n) acc - | _ -> fold_constr_with_binders succ frec depth acc c - in - frec 1 acc m - -(* calcule la liste des arguments implicites *) - -let poly_args env sigma t = - let rec aux env n t = - match kind_of_term (whd_betadeltaiota env sigma t) with - | IsProd (x,a,b) -> - add_free_rels_until n a - (aux (push_rel_assum (x,a) env) (n+1) b) - | _ -> Intset.empty - in - match kind_of_term (whd_betadeltaiota env sigma t) with - | IsProd (x,a,b) -> - Intset.elements (aux (push_rel_assum (x,a) env) 1 b) - | _ -> [] - (* Expanding existential variables (pretyping.ml) *) (* 1- whd_ise fails if an existential is undefined *) diff --git a/kernel/reduction.mli b/kernel/reduction.mli index 7908c26f2..10b4edc43 100644 --- a/kernel/reduction.mli +++ b/kernel/reduction.mli @@ -142,8 +142,6 @@ val is_info_cast_type : env -> 'a evar_map -> constr -> bool val contents_of_cast_type : env -> 'a evar_map -> constr -> contents i*) -val poly_args : env -> 'a evar_map -> constr -> int list - val whd_programs : 'a reduction_function (* [reduce_fix] contracts a fix redex if it is actually reducible *) diff --git a/library/impargs.ml b/library/impargs.ml index cf2d09d61..6ef403f59 100644 --- a/library/impargs.ml +++ b/library/impargs.ml @@ -1,6 +1,7 @@ (* $Id$ *) +open Util open Names open Term open Reduction @@ -10,6 +11,40 @@ open Inductive open Libobject open Lib +(* calcul des arguments implicites *) + +(* la seconde liste est ordonne'e *) + +let ord_add x l = + let rec aux l = match l with + | [] -> [x] + | y::l' -> if y > x then x::l else if x = y then l else y::(aux l') + in + aux l + +let add_free_rels_until bound m acc = + let rec frec depth acc c = match kind_of_term c with + | IsRel n when (n < bound+depth) & (n >= depth) -> + Intset.add (bound+depth-n) acc + | _ -> fold_constr_with_binders succ frec depth acc c + in + frec 1 acc m + +(* calcule la liste des arguments implicites *) + +let poly_args env sigma t = + let rec aux env n t = + match kind_of_term (whd_betadeltaiota env sigma t) with + | IsProd (x,a,b) -> + add_free_rels_until n a + (aux (push_rel_assum (x,a) env) (n+1) b) + | _ -> Intset.empty + in + match kind_of_term (whd_betadeltaiota env sigma t) with + | IsProd (x,a,b) -> + Intset.elements (aux (push_rel_assum (x,a) env) 1 b) + | _ -> [] + type implicits = | Impl_auto of int list | Impl_manual of int list diff --git a/library/library.ml b/library/library.ml index 55c8aca0f..558052a11 100644 --- a/library/library.ml +++ b/library/library.ml @@ -204,6 +204,31 @@ let save_module_to process s f = System.marshal_out ch di; close_out ch +(*s Iterators. *) + +let fold_all_segments insec f x = + let rec apply acc = function + | sp, Leaf o -> f acc sp o + | _, ClosedSection (_,_,seg,_) -> + if insec then List.fold_left apply acc seg else acc + | _ -> acc + in + let acc' = + Stringmap.fold + (fun _ m acc -> List.fold_left apply acc (fst m.module_declarations)) + !modules_table x + in + List.fold_left apply acc' (Lib.contents_after None) + +let iter_all_segments insec f = + let rec apply = function + | sp, Leaf o -> f sp o + | _, ClosedSection (_,_,seg,_) -> if insec then List.iter apply seg + | _ -> () + in + Stringmap.iter + (fun _ m -> List.iter apply (fst m.module_declarations)) !modules_table; + List.iter apply (Lib.contents_after None) (*s Pretty-printing of modules state. *) diff --git a/library/library.mli b/library/library.mli index 6d4bb1ed5..4ff27b4cd 100644 --- a/library/library.mli +++ b/library/library.mli @@ -1,6 +1,11 @@ (* $Id$ *) +(*i*) +open Names +open Libobject +(*i*) + (*s This module is the heart of the library. It provides low level functions to load, open and save modules. Modules are saved onto the disk with checksums (obtained with the [Digest] module), which are checked at loading time to @@ -41,6 +46,15 @@ val save_module_to : (Lib.library_segment -> Nametab.module_contents) -> val module_segment : string option -> Lib.library_segment val module_filename : string -> System.load_path_entry * string +(*s [fold_all_segments] and [iter_all_segments] iterate over all + segments, the modules' segments first and then the current + segment. Modules are presented in an arbitrary order. The given + function is applied to all leaves (together with their section + path). The boolean indicates if we must enter closed sections. *) + +val fold_all_segments : bool -> ('a -> section_path -> obj -> 'a) -> 'a -> 'a +val iter_all_segments : bool -> (section_path -> obj -> unit) -> unit + (*s Global load path *) val get_load_path : unit -> System.load_path val add_load_path_entry : System.load_path_entry -> unit diff --git a/parsing/g_basevernac.ml4 b/parsing/g_basevernac.ml4 index efe9d77cd..d9eaf2a0a 100644 --- a/parsing/g_basevernac.ml4 +++ b/parsing/g_basevernac.ml4 @@ -95,7 +95,7 @@ GEXTEND Gram <:ast< (PrintOpaqueId $id) >> (* Pris en compte dans PrintOption ci-dessous (CADUC) *) | IDENT "Print"; id = identarg; "." -> <:ast< (PrintId $id) >> - | IDENT "Search"; id = identarg; "." -> <:ast< (SEARCH $id) >> + | IDENT "Search"; id = Tactic.qualidarg; "." -> <:ast< (SEARCH $id) >> | IDENT "Inspect"; n = numarg; "." -> <:ast< (INSPECT $n) >> (* TODO: rapprocher Eval et Check *) | IDENT "Eval"; r = Tactic.red_tactic; "in"; c = constrarg; "." -> diff --git a/parsing/pretty.mli b/parsing/pretty.mli index 946965c6d..64e2cb109 100644 --- a/parsing/pretty.mli +++ b/parsing/pretty.mli @@ -48,7 +48,6 @@ val print_path_between : identifier -> identifier -> std_ppcmds val search_by_head : global_reference -> unit -val crible : (string -> env -> constr -> unit) -> global_reference -> - unit +val crible : (string -> env -> constr -> unit) -> global_reference -> unit val inspect : int -> std_ppcmds diff --git a/toplevel/vernacentries.ml b/toplevel/vernacentries.ml index 53d0c7b51..118ba6616 100644 --- a/toplevel/vernacentries.ml +++ b/toplevel/vernacentries.ml @@ -891,7 +891,8 @@ let _ = try Nametab.locate q with Not_found -> Pretype_errors.error_global_not_found_loc loc q - in search_by_head ref) + in + search_by_head ref) | _ -> bad_vernac_args "SEARCH") let _ = |