diff options
Diffstat (limited to 'parsing')
| -rw-r--r-- | parsing/g_rsyntax.ml | 2 | ||||
| -rw-r--r-- | parsing/g_string_syntax.ml | 2 | ||||
| -rw-r--r-- | parsing/g_vernac.ml4 | 13 | ||||
| -rw-r--r-- | parsing/ppdecl_proof.ml | 2 | ||||
| -rw-r--r-- | parsing/ppvernac.ml | 5 | ||||
| -rw-r--r-- | parsing/search.ml | 214 | ||||
| -rw-r--r-- | parsing/search.mli | 50 |
7 files changed, 14 insertions, 274 deletions
diff --git a/parsing/g_rsyntax.ml b/parsing/g_rsyntax.ml index 3218781d12..4a5972cc71 100644 --- a/parsing/g_rsyntax.ml +++ b/parsing/g_rsyntax.ml @@ -6,7 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(*i $Id:$ i*) +(*i $Id$ i*) open Pp open Util diff --git a/parsing/g_string_syntax.ml b/parsing/g_string_syntax.ml index 6b1faa76ce..a936485d9b 100644 --- a/parsing/g_string_syntax.ml +++ b/parsing/g_string_syntax.ml @@ -6,7 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (***********************************************************************) -(*i $Id:$ i*) +(*i $Id$ i*) open Pp open Util diff --git a/parsing/g_vernac.ml4 b/parsing/g_vernac.ml4 index 4b79113f3f..3a88a09f81 100644 --- a/parsing/g_vernac.ml4 +++ b/parsing/g_vernac.ml4 @@ -151,7 +151,7 @@ GEXTEND Gram (* Gallina inductive declarations *) | f = finite_token; indl = LIST1 inductive_definition SEP "with" -> - VernacInductive (f,indl) + VernacInductive (f,false,indl) | IDENT "Boxed";"Fixpoint"; recs = LIST1 rec_definition SEP "with" -> VernacFixpoint (recs,true) | IDENT "Unboxed";"Fixpoint"; recs = LIST1 rec_definition SEP "with" -> @@ -165,13 +165,13 @@ GEXTEND Gram l = LIST1 identref SEP "," -> VernacCombinedScheme (id, l) ] ] ; gallina_ext: - [ [ b = record_token; oc = opt_coercion; name = identref; + [ [ b = record_token; infer = infer_token; oc = opt_coercion; name = identref; ps = binders_let; s = OPT [ ":"; s = lconstr -> s ]; cfs = [ ":="; l = constructor_list_or_record_decl -> l | -> RecordDecl (None, []) ] -> let (recf,indf) = b in - VernacInductive (indf,[((oc,name),ps,s,Some recf,cfs),None]) + VernacInductive (indf,infer,[((oc,name),ps,s,Some recf,cfs),None]) ] ] ; typeclass_context: @@ -217,6 +217,9 @@ GEXTEND Gram [ [ "Inductive" -> true | "CoInductive" -> false ] ] ; + infer_token: + [ [ "Infer" -> true | -> false ] ] + ; record_token: [ [ IDENT "Record" -> (Record,true) | IDENT "Structure" -> (Structure,true) @@ -597,8 +600,8 @@ GEXTEND Gram | IDENT "About"; qid = global -> VernacPrint (PrintAbout qid) (* Searching the environment *) - | IDENT "Search"; qid = global; l = in_or_out_modules -> - VernacSearch (SearchHead qid, l) + | IDENT "Search"; c = constr_pattern; l = in_or_out_modules -> + VernacSearch (SearchHead c, l) | IDENT "SearchPattern"; c = constr_pattern; l = in_or_out_modules -> VernacSearch (SearchPattern c, l) | IDENT "SearchRewrite"; c = constr_pattern; l = in_or_out_modules -> diff --git a/parsing/ppdecl_proof.ml b/parsing/ppdecl_proof.ml index 790b5c363f..31fd4561e6 100644 --- a/parsing/ppdecl_proof.ml +++ b/parsing/ppdecl_proof.ml @@ -6,7 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(* $Id:$ *) +(* $Id$ *) open Util open Pp diff --git a/parsing/ppvernac.ml b/parsing/ppvernac.ml index df4eee8aa0..113b2f0402 100644 --- a/parsing/ppvernac.ml +++ b/parsing/ppvernac.ml @@ -140,7 +140,7 @@ let pr_search_about (b,c) = | SearchString (s,sc) -> qs s ++ pr_opt (fun sc -> str "%" ++ str sc) sc let pr_search a b pr_p = match a with - | SearchHead qid -> str"Search" ++ spc() ++ pr_reference qid ++ pr_in_out_modules b + | SearchHead c -> str"Search" ++ spc() ++ pr_p c ++ pr_in_out_modules b | SearchPattern c -> str"SearchPattern" ++ spc() ++ pr_p c ++ pr_in_out_modules b | SearchRewrite c -> str"SearchRewrite" ++ spc() ++ pr_p c ++ pr_in_out_modules b | SearchAbout sl -> str"SearchAbout" ++ spc() ++ str "[" ++ prlist_with_sep spc pr_search_about sl ++ str "]" ++ pr_in_out_modules b @@ -576,7 +576,7 @@ let rec pr_vernac = function hov 2 (pr_assumption_token (n > 1) stre ++ spc() ++ pr_ne_params_list pr_lconstr_expr l) - | VernacInductive (f,l) -> + | VernacInductive (f,i,l) -> let pr_constructor (coe,(id,c)) = hov 2 (pr_lident id ++ str" " ++ @@ -601,6 +601,7 @@ let rec pr_vernac = function in hov 0 ( kw ++ spc() ++ + (if i then str"Infer" else str"") ++ (if coe then str" > " else str" ") ++ pr_lident id ++ pr_and_type_binders_arg indpar ++ spc() ++ Option.cata (fun s -> str":" ++ spc() ++ pr_lconstr_expr s) (mt()) s ++ diff --git a/parsing/search.ml b/parsing/search.ml deleted file mode 100644 index 94270ee135..0000000000 --- a/parsing/search.ml +++ /dev/null @@ -1,214 +0,0 @@ -(************************************************************************) -(* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud *) -(* \VV/ **************************************************************) -(* // * This file is distributed under the terms of the *) -(* * GNU Lesser General Public License Version 2.1 *) -(************************************************************************) - -(* $Id$ *) - -open Pp -open Util -open Names -open Nameops -open Term -open Rawterm -open Declarations -open Libobject -open Declare -open Environ -open Pattern -open Matching -open Printer -open Libnames -open Nametab - -(* The functions print_constructors and crible implement the behavior needed - for the Coq searching commands. - These functions take as first argument the procedure - that will be called to treat each entry. This procedure receives the name - of the object, the assumptions that will make it possible to print its type, - and the constr term that represent its type. *) - -let print_constructors indsp fn env nconstr = - for i = 1 to nconstr do - fn (ConstructRef (indsp,i)) env (Inductiveops.type_of_constructor env (indsp,i)) - done - -let rec head_const c = match kind_of_term c with - | Prod (_,_,d) -> head_const d - | LetIn (_,_,_,d) -> head_const d - | App (f,_) -> head_const f - | Cast (d,_,_) -> head_const d - | _ -> c - -(* General search, restricted to head constant if [only_head] *) - -let gen_crible refopt (fn : global_reference -> env -> constr -> unit) = - let env = Global.env () in - let crible_rec (sp,_) lobj = match object_tag lobj with - | "VARIABLE" -> - (try - let (id,_,typ) = Global.lookup_named (basename sp) in - if refopt = None - || head_const typ = constr_of_global (Option.get refopt) - then - fn (VarRef id) env typ - with Not_found -> (* we are in a section *) ()) - | "CONSTANT" -> - let cst = locate_constant (qualid_of_sp sp) in - let typ = Typeops.type_of_constant env cst in - if refopt = None - || head_const typ = constr_of_global (Option.get refopt) - then - fn (ConstRef cst) env typ - | "INDUCTIVE" -> - let kn = locate_mind (qualid_of_sp sp) in - let mib = Global.lookup_mind kn in - (match refopt with - | Some (IndRef ((kn',tyi) as ind)) when kn=kn' -> - print_constructors ind fn env - (Array.length (mib.mind_packets.(tyi).mind_user_lc)) - | Some _ -> () - | _ -> - Array.iteri - (fun i mip -> print_constructors (kn,i) fn env - (Array.length mip.mind_user_lc)) mib.mind_packets) - | _ -> () - in - try - Declaremods.iter_all_segments crible_rec - with Not_found -> - () - -let crible ref = gen_crible (Some ref) - -(* Fine Search. By Yves Bertot. *) - -exception No_section_path - -let rec head c = - let c = strip_outer_cast c in - match kind_of_term c with - | Prod (_,_,c) -> head c - | LetIn (_,_,_,c) -> head c - | _ -> c - -let constr_to_section_path c = match kind_of_term c with - | Const sp -> sp - | _ -> raise No_section_path - -let xor a b = (a or b) & (not (a & b)) - -let plain_display ref a c = - let pc = pr_lconstr_env a c in - let pr = pr_global ref in - msg (hov 2 (pr ++ str":" ++ spc () ++ pc) ++ fnl ()) - -let filter_by_module (module_list:dir_path list) (accept:bool) - (ref:global_reference) _ _ = - try - let sp = sp_of_global ref in - let sl = dirpath sp in - let rec filter_aux = function - | m :: tl -> (not (is_dirpath_prefix_of m sl)) && (filter_aux tl) - | [] -> true - in - xor accept (filter_aux module_list) - with No_section_path -> - false - -let gref_eq = - IndRef (Libnames.encode_kn Coqlib.logic_module (id_of_string "eq"), 0) -let gref_eqT = - IndRef (Libnames.encode_kn Coqlib.logic_type_module (id_of_string "eqT"), 0) - -let mk_rewrite_pattern1 eq pattern = - PApp (PRef eq, [| PMeta None; pattern; PMeta None |]) - -let mk_rewrite_pattern2 eq pattern = - PApp (PRef eq, [| PMeta None; PMeta None; pattern |]) - -let pattern_filter pat _ a c = - try - try - is_matching pat (head c) - with _ -> - is_matching - pat (head (Typing.type_of (Global.env()) Evd.empty c)) - with UserError _ -> - false - -let filtered_search filter_function display_function ref = - crible ref - (fun s a c -> if filter_function s a c then display_function s a c) - -let rec id_from_pattern = function - | PRef gr -> gr -(* should be appear as a PRef (VarRef sp) !! - | PVar id -> Nametab.locate (make_qualid [] (string_of_id id)) - *) - | PApp (p,_) -> id_from_pattern p - | _ -> error "The pattern is not simple enough." - -let raw_pattern_search extra_filter display_function pat = - let name = id_from_pattern pat in - filtered_search - (fun s a c -> (pattern_filter pat s a c) & extra_filter s a c) - display_function name - -let raw_search_rewrite extra_filter display_function pattern = - filtered_search - (fun s a c -> - ((pattern_filter (mk_rewrite_pattern1 gref_eq pattern) s a c) || - (pattern_filter (mk_rewrite_pattern2 gref_eq pattern) s a c)) - && extra_filter s a c) - display_function gref_eq - -let text_pattern_search extra_filter = - raw_pattern_search extra_filter plain_display - -let text_search_rewrite extra_filter = - raw_search_rewrite extra_filter plain_display - -let filter_by_module_from_list = function - | [], _ -> (fun _ _ _ -> true) - | l, outside -> filter_by_module l (not outside) - -let search_by_head ref inout = - filtered_search (filter_by_module_from_list inout) plain_display ref - -let search_rewrite pat inout = - text_search_rewrite (filter_by_module_from_list inout) pat - -let search_pattern pat inout = - text_pattern_search (filter_by_module_from_list inout) pat - - -let gen_filtered_search filter_function display_function = - gen_crible None - (fun s a c -> if filter_function s a c then display_function s a c) - -(** SearchAbout *) - -let name_of_reference ref = string_of_id (id_of_global ref) - -type glob_search_about_item = - | GlobSearchSubPattern of constr_pattern - | GlobSearchString of string - -let search_about_item (itemref,typ) = function - | GlobSearchSubPattern pat -> is_matching_appsubterm ~closed:false pat typ - | GlobSearchString s -> string_string_contains (name_of_reference itemref) s - -let raw_search_about filter_modules display_function l = - let filter ref' env typ = - filter_modules ref' env typ && - List.for_all (fun (b,i) -> b = search_about_item (ref',typ) i) l && - not (string_string_contains (name_of_reference ref') "_subproof") - in - gen_filtered_search filter display_function - -let search_about ref inout = - raw_search_about (filter_by_module_from_list inout) plain_display ref diff --git a/parsing/search.mli b/parsing/search.mli deleted file mode 100644 index fc2ea925fe..0000000000 --- a/parsing/search.mli +++ /dev/null @@ -1,50 +0,0 @@ -(************************************************************************) -(* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud *) -(* \VV/ **************************************************************) -(* // * This file is distributed under the terms of the *) -(* * GNU Lesser General Public License Version 2.1 *) -(************************************************************************) - -(*i $Id$ i*) - -open Pp -open Names -open Term -open Environ -open Pattern -open Libnames -open Nametab - -(*s Search facilities. *) - -type glob_search_about_item = - | GlobSearchSubPattern of constr_pattern - | GlobSearchString of string - -val search_by_head : global_reference -> dir_path list * bool -> unit -val search_rewrite : constr_pattern -> dir_path list * bool -> unit -val search_pattern : constr_pattern -> dir_path list * bool -> unit -val search_about : - (bool * glob_search_about_item) list -> dir_path list * bool -> unit - -(* The filtering function that is by standard search facilities. - It can be passed as argument to the raw search functions. - It is used in pcoq. *) - -val filter_by_module_from_list : - dir_path list * bool -> global_reference -> env -> 'a -> bool - -(* raw search functions can be used for various extensions. - They are also used for pcoq. *) -val gen_filtered_search : (global_reference -> env -> constr -> bool) -> - (global_reference -> env -> constr -> unit) -> unit -val filtered_search : (global_reference -> env -> constr -> bool) -> - (global_reference -> env -> constr -> unit) -> global_reference -> unit -val raw_pattern_search : (global_reference -> env -> constr -> bool) -> - (global_reference -> env -> constr -> unit) -> constr_pattern -> unit -val raw_search_rewrite : (global_reference -> env -> constr -> bool) -> - (global_reference -> env -> constr -> unit) -> constr_pattern -> unit -val raw_search_about : (global_reference -> env -> constr -> bool) -> - (global_reference -> env -> constr -> unit) -> - (bool * glob_search_about_item) list -> unit |