diff options
author | 2008-06-25 18:19:21 +0000 | |
---|---|---|
committer | 2008-06-25 18:19:21 +0000 | |
commit | 693d398b5e4e55a916bbdaa8e4c23c83d9dbcef7 (patch) | |
tree | e015dc24293114d03433c2cf4412b4fa5df9b87c /interp | |
parent | 217bbf499dc09f11a137fdc9aead1e0a78c760c2 (diff) |
Création du fichier dumpglob.ml, qui rassemble les fonctions de globalisation (add_glob* et dump_*)
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11177 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'interp')
-rw-r--r-- | interp/constrintern.ml | 164 | ||||
-rw-r--r-- | interp/constrintern.mli | 7 | ||||
-rw-r--r-- | interp/dumpglob.ml | 220 | ||||
-rw-r--r-- | interp/modintern.ml | 32 | ||||
-rw-r--r-- | interp/modintern.mli | 3 |
5 files changed, 232 insertions, 194 deletions
diff --git a/interp/constrintern.ml b/interp/constrintern.ml index 1ddcac276..54abacaf6 100644 --- a/interp/constrintern.ml +++ b/interp/constrintern.ml @@ -124,150 +124,6 @@ let error_inductive_parameter_not_implicit loc = "the 'return' clauses; they must be replaced by '_' in the 'in' clauses.")) (**********************************************************************) -(* Dump of globalization (to be used by coqdoc) *) -let token_number = ref 0 -let last_pos = ref 0 - -type coqdoc_state = Lexer.location_table * int * int - -let coqdoc_freeze () = - let lt = Lexer.location_table() in - let state = (lt,!token_number,!last_pos) in - token_number := 0; - last_pos := 0; - state - -let coqdoc_unfreeze (lt,tn,lp) = - Lexer.restore_location_table lt; - token_number := tn; - last_pos := lp - -open Decl_kinds - -let type_of_logical_kind = function - | IsDefinition def -> - (match def with - | Definition -> "def" - | Coercion -> "coe" - | SubClass -> "subclass" - | CanonicalStructure -> "canonstruc" - | Example -> "ex" - | Fixpoint -> "def" - | CoFixpoint -> "def" - | Scheme -> "scheme" - | StructureComponent -> "proj" - | IdentityCoercion -> "coe" - | Instance -> "inst" - | Method -> "meth") - | IsAssumption a -> - (match a with - | Definitional -> "defax" - | Logical -> "prfax" - | Conjectural -> "prfax") - | IsProof th -> - (match th with - | Theorem - | Lemma - | Fact - | Remark - | Property - | Proposition - | Corollary -> "thm") - -let type_of_global_ref gr = - if Typeclasses.is_class gr then - "class" - else - match gr with - | ConstRef cst -> - type_of_logical_kind (Decls.constant_kind cst) - | VarRef v -> - "var" ^ type_of_logical_kind (Decls.variable_kind v) - | IndRef ind -> - let (mib,oib) = Inductive.lookup_mind_specif (Global.env ()) ind in - if mib.Declarations.mind_record then - if mib.Declarations.mind_finite then "rec" - else "corec" - else if mib.Declarations.mind_finite then "ind" - else "coind" - | ConstructRef _ -> "constr" - -let remove_sections dir = - if is_dirpath_prefix_of dir (Lib.cwd ()) then - (* Not yet (fully) discharged *) - extract_dirpath_prefix (Lib.sections_depth ()) (Lib.cwd ()) - else - (* Theorem/Lemma outside its outer section of definition *) - dir - -let dump_reference loc filepath modpath ident ty = - dump_string (Printf.sprintf "R%d %s %s %s %s\n" - (fst (unloc loc)) filepath modpath ident ty) - -let add_glob_gen loc sp lib_dp ty = - let mod_dp,id = repr_path sp in - let mod_dp = remove_sections mod_dp in - let mod_dp_trunc = drop_dirpath_prefix lib_dp mod_dp in - let filepath = string_of_dirpath lib_dp in - let modpath = string_of_dirpath mod_dp_trunc in - let ident = string_of_id id in - dump_reference loc filepath modpath ident ty - -let add_glob loc ref = - let sp = Nametab.sp_of_global ref in - let lib_dp = Lib.library_part ref in - let ty = type_of_global_ref ref in - add_glob_gen loc sp lib_dp ty - -let add_glob loc ref = - if !Flags.dump && loc <> dummy_loc then add_glob loc ref - -let mp_of_kn kn = - let mp,sec,l = repr_kn kn in - MPdot (mp,l) - -let add_glob_kn loc kn = - let sp = Nametab.sp_of_syntactic_definition kn in - let lib_dp = Lib.dp_of_mp (mp_of_kn kn) in - add_glob_gen loc sp lib_dp "syndef" - -let add_glob_kn loc ref = - if !Flags.dump && loc <> dummy_loc then add_glob_kn loc ref - -let add_local loc id = () -(* let mod_dp,id = repr_path sp in *) -(* let mod_dp = remove_sections mod_dp in *) -(* let mod_dp_trunc = drop_dirpath_prefix lib_dp mod_dp in *) -(* let filepath = string_of_dirpath lib_dp in *) -(* let modpath = string_of_dirpath mod_dp_trunc in *) -(* let ident = string_of_id id in *) -(* dump_string (Printf.sprintf "R%d %s %s %s %s\n" *) -(* (fst (unloc loc)) filepath modpath ident ty) *) - -let dump_binding loc id = () - -let loc_of_notation f loc args ntn = - if args=[] or ntn.[0] <> '_' then fst (unloc loc) - else snd (unloc (f (List.hd args))) - -let ntn_loc = loc_of_notation constr_loc -let patntn_loc = loc_of_notation cases_pattern_expr_loc - -let dump_notation_location pos ((path,df),sc) = - let rec next growing = - let loc = Lexer.location_function !token_number in - let (bp,_) = unloc loc in - if growing then if bp >= pos then loc else (incr token_number;next true) - else if bp = pos then loc - else if bp > pos then (decr token_number;next false) - else (incr token_number;next true) in - let loc = next (pos >= !last_pos) in - last_pos := pos; - let path = string_of_dirpath path in - let _sc = match sc with Some sc -> " "^sc | None -> "" in - dump_string (Printf.sprintf "R%d %s \"%s\" not\n" (fst (unloc loc)) path df) - -(**********************************************************************) (* Contracting "{ _ }" in notations *) let rec wildcards ntn n = @@ -394,9 +250,9 @@ let rec subst_aconstr_in_rawconstr loc interp subst (renaming,(ids,_,scopes)) = let intern_notation intern (_,tmp_scope,scopes as env) loc ntn args = let ntn,args = contract_notation ntn args in let ((ids,c),df) = Notation.interp_notation loc ntn (tmp_scope,scopes) in - if !dump then dump_notation_location (ntn_loc loc args ntn) df; - let subst = List.map2 (fun (id,scl) a -> (id,(a,scl))) ids args in - subst_aconstr_in_rawconstr loc intern subst ([],env) c + if !Flags.dump then Dumpglob.dump_notation_location (Dumpglob.ntn_loc loc args ntn) df; + let subst = List.map2 (fun (id,scl) a -> (id,(a,scl))) ids args in + subst_aconstr_in_rawconstr loc intern subst ([],env) c let set_type_scope (ids,tmp_scope,scopes) = (ids,Some Notation.type_scope,scopes) @@ -476,10 +332,10 @@ let check_no_explicitation l = let intern_qualid loc qid intern env args = try match Nametab.extended_locate qid with | TrueGlobal ref -> - add_glob loc ref; + Dumpglob.add_glob loc ref; RRef (loc, ref), args | SyntacticDef sp -> - add_glob_kn loc sp; + Dumpglob.add_glob_kn loc sp; let (ids,c) = Syntax_def.search_syntactic_definition loc sp in let nids = List.length ids in if List.length args < nids then error_not_enough_arguments loc; @@ -709,7 +565,7 @@ let find_constructor ref f aliases pats scopes = let v = Environ.constant_value (Global.env()) cst in unf (global_of_constr v) | ConstructRef cstr -> - add_glob loc r; + Dumpglob.add_glob loc r; cstr, [], pats | _ -> raise Not_found in unf r @@ -760,7 +616,7 @@ let rec intern_cases_pattern genv scopes (ids,subst as aliases) tmp_scope pat = | CPatNotation (loc, ntn, args) -> let ntn,args = contract_pat_notation ntn args in let ((ids',c),df) = Notation.interp_notation loc ntn (tmp_scope,scopes) in - if !dump then dump_notation_location (patntn_loc loc args ntn) df; + if !Flags.dump then Dumpglob.dump_notation_location (Dumpglob.patntn_loc loc args ntn) df; let subst = List.map2 (fun (id,scl) a -> (id,(a,scl))) ids' args in let ids'',pl = subst_cases_pattern loc (alias_of aliases) intern_pat subst scopes c @@ -769,7 +625,7 @@ let rec intern_cases_pattern genv scopes (ids,subst as aliases) tmp_scope pat = let a = alias_of aliases in let (c,df) = Notation.interp_prim_token_cases_pattern loc p a (tmp_scope,scopes) in - if !dump then dump_notation_location (fst (unloc loc)) df; + if !Flags.dump then Dumpglob.dump_notation_location (fst (unloc loc)) df; (ids,[subst,c]) | CPatDelimiters (loc, key, e) -> intern_pat (find_delimiters_scope loc key::scopes) aliases None e @@ -829,7 +685,7 @@ let push_loc_name_env lvar (ids,tmpsc,scopes as env) loc = function | Anonymous -> env | Name id -> check_hidden_implicit_parameters id lvar; - dump_binding loc id; + Dumpglob.dump_binding loc id; (Idset.add id ids,tmpsc,scopes) let intern_typeclass_binders intern_type lvar env bl = @@ -1029,7 +885,7 @@ let internalise sigma globalenv env allow_patvar lvar c = intern_notation intern env loc ntn args | CPrim (loc, p) -> let c,df = Notation.interp_prim_token loc p (tmp_scope,scopes) in - if !dump then dump_notation_location (fst (unloc loc)) df; + if !Flags.dump then Dumpglob.dump_notation_location (fst (unloc loc)) df; c | CDelimiters (loc, key, e) -> intern (ids,None,find_delimiters_scope loc key::scopes) e diff --git a/interp/constrintern.mli b/interp/constrintern.mli index d3b8da8f9..27a46daf1 100644 --- a/interp/constrintern.mli +++ b/interp/constrintern.mli @@ -144,10 +144,3 @@ val interp_aconstr : implicits_env -> identifier list -> constr_expr -> (* Globalization leak for Grammar *) val for_grammar : ('a -> 'b) -> 'a -> 'b - -(* Coqdoc utility functions *) -type coqdoc_state -val coqdoc_freeze : unit -> coqdoc_state -val coqdoc_unfreeze : coqdoc_state -> unit - -val add_glob : Util.loc -> global_reference -> unit diff --git a/interp/dumpglob.ml b/interp/dumpglob.ml new file mode 100644 index 000000000..8cc6371f5 --- /dev/null +++ b/interp/dumpglob.ml @@ -0,0 +1,220 @@ +(************************************************************************) +(* 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$ *) + + +let rec drop_last = function [] -> assert false | hd :: [] -> [] | hd :: tl -> hd :: drop_last tl + +(* Dump of globalization (to be used by coqdoc) *) + +let glob_file = ref Pervasives.stdout + +let open_glob_file f = + glob_file := Pervasives.open_out(f ^ ".glob") + +let close_glob_file () = + Pervasives.close_out !glob_file + +let dump_string s = + Pervasives.output_string !glob_file s + + + +(**********************************************************************) +(* Dump of globalization (to be used by coqdoc) *) +let token_number = ref 0 +let last_pos = ref 0 + +type coqdoc_state = Lexer.location_table * int * int + +let coqdoc_freeze () = + let lt = Lexer.location_table() in + let state = (lt,!token_number,!last_pos) in + token_number := 0; + last_pos := 0; + state + +let coqdoc_unfreeze (lt,tn,lp) = + Lexer.restore_location_table lt; + token_number := tn; + last_pos := lp + +open Decl_kinds + +let type_of_logical_kind = function + | IsDefinition def -> + (match def with + | Definition -> "def" + | Coercion -> "coe" + | SubClass -> "subclass" + | CanonicalStructure -> "canonstruc" + | Example -> "ex" + | Fixpoint -> "def" + | CoFixpoint -> "def" + | Scheme -> "scheme" + | StructureComponent -> "proj" + | IdentityCoercion -> "coe" + | Instance -> "inst" + | Method -> "meth") + | IsAssumption a -> + (match a with + | Definitional -> "defax" + | Logical -> "prfax" + | Conjectural -> "prfax") + | IsProof th -> + (match th with + | Theorem + | Lemma + | Fact + | Remark + | Property + | Proposition + | Corollary -> "thm") + +let type_of_global_ref gr = + if Typeclasses.is_class gr then + "class" + else + match gr with + | Libnames.ConstRef cst -> + type_of_logical_kind (Decls.constant_kind cst) + | Libnames.VarRef v -> + "var" ^ type_of_logical_kind (Decls.variable_kind v) + | Libnames.IndRef ind -> + let (mib,oib) = Inductive.lookup_mind_specif (Global.env ()) ind in + if mib.Declarations.mind_record then + if mib.Declarations.mind_finite then "rec" + else "corec" + else if mib.Declarations.mind_finite then "ind" + else "coind" + | Libnames.ConstructRef _ -> "constr" + +let remove_sections dir = + if Libnames.is_dirpath_prefix_of dir (Lib.cwd ()) then + (* Not yet (fully) discharged *) + Libnames.extract_dirpath_prefix (Lib.sections_depth ()) (Lib.cwd ()) + else + (* Theorem/Lemma outside its outer section of definition *) + dir + +let dump_ref loc filepath modpath ident ty = + dump_string (Printf.sprintf "R%d %s %s %s %s\n" + (fst (Util.unloc loc)) filepath modpath ident ty) + +let add_glob_gen loc sp lib_dp ty = + let mod_dp,id = Libnames.repr_path sp in + let mod_dp = remove_sections mod_dp in + let mod_dp_trunc = Libnames.drop_dirpath_prefix lib_dp mod_dp in + let filepath = Names.string_of_dirpath lib_dp in + let modpath = Names.string_of_dirpath mod_dp_trunc in + let ident = Names.string_of_id id in + dump_ref loc filepath modpath ident ty + +let add_glob loc ref = + let sp = Nametab.sp_of_global ref in + let lib_dp = Lib.library_part ref in + let ty = type_of_global_ref ref in + add_glob_gen loc sp lib_dp ty + +let add_glob loc ref = + if !Flags.dump && loc <> Util.dummy_loc then add_glob loc ref + +let mp_of_kn kn = + let mp,sec,l = Names.repr_kn kn in + Names.MPdot (mp,l) + +let add_glob_kn loc kn = + let sp = Nametab.sp_of_syntactic_definition kn in + let lib_dp = Lib.dp_of_mp (mp_of_kn kn) in + add_glob_gen loc sp lib_dp "syndef" + +let add_glob_kn loc ref = + if !Flags.dump && loc <> Util.dummy_loc then add_glob_kn loc ref + +let add_local loc id = () +(* let mod_dp,id = repr_path sp in *) +(* let mod_dp = remove_sections mod_dp in *) +(* let mod_dp_trunc = drop_dirpath_prefix lib_dp mod_dp in *) +(* let filepath = string_of_dirpath lib_dp in *) +(* let modpath = string_of_dirpath mod_dp_trunc in *) +(* let ident = string_of_id id in *) +(* dump_string (Printf.sprintf "R%d %s %s %s %s\n" *) +(* (fst (unloc loc)) filepath modpath ident ty) *) + +let dump_binding loc id = () + +(* BEGIN obsolete *) + +let dump_modref qid = Pp.warning ("Dumpglob.modref: not yet implemented") + +let dump_def loc ref = + let curr_mp, _ = Lib.current_prefix() in + let lib_dp, curr_dp = Lib.split_mp curr_mp in + let mod_dp_trunc = Libnames.drop_dirpath_prefix lib_dp curr_dp in + + let fullname = Libnames.string_of_qualid (Libnames.make_qualid mod_dp_trunc ref) in + let filepath = Names.string_of_dirpath lib_dp in + dump_string (Printf.sprintf "D%d %s %s\n" (fst (Util.unloc loc)) filepath fullname) + +(* END obsolete *) + +let dump_definition (loc, id) sec s = + dump_string (Printf.sprintf "%s %d %s %s\n" s (fst (Util.unloc loc)) + (Names.string_of_dirpath (Lib.current_dirpath sec)) (Names.string_of_id id)) + +let dump_reference loc modpath ident ty = + dump_string (Printf.sprintf "R%d %s %s %s %s\n" + (fst (Util.unloc loc)) (Names.string_of_dirpath (Lib.library_dp ())) modpath ident ty) + +let dump_constraint ((loc, n), _, _) sec ty = + match n with + | Names.Name id -> dump_definition (loc, id) sec ty + | Names.Anonymous -> () + +let dump_modref loc mp ty = + if !Flags.dump then + let (dp, l) = Lib.split_modpath mp in + let fp = Names.string_of_dirpath dp in + let mp = Names.string_of_dirpath (Names.make_dirpath (drop_last l)) in + dump_string (Printf.sprintf "R%d %s %s %s %s\n" + (fst (Util.unloc loc)) fp mp "<>" ty) + +let dump_moddef loc mp ty = + if !Flags.dump then + let (dp, l) = Lib.split_modpath mp in + let mp = Names.string_of_dirpath (Names.make_dirpath l) in + dump_string (Printf.sprintf "%s %d %s %s\n" ty (fst (Util.unloc loc)) "<>" mp) + +let dump_libref loc dp ty = + if !Flags.dump then + dump_string (Printf.sprintf "R%d %s <> <> %s\n" + (fst (Util.unloc loc)) (Names.string_of_dirpath dp) ty) + +let loc_of_notation f loc args ntn = + if args=[] or ntn.[0] <> '_' then fst (Util.unloc loc) + else snd (Util.unloc (f (List.hd args))) + +let ntn_loc = loc_of_notation Topconstr.constr_loc +let patntn_loc = loc_of_notation Topconstr.cases_pattern_expr_loc + +let dump_notation_location pos ((path,df),sc) = + let rec next growing = + let loc = Lexer.location_function !token_number in + let (bp,_) = Util.unloc loc in + if growing then if bp >= pos then loc else (incr token_number; next true) + else if bp = pos then loc + else if bp > pos then (decr token_number;next false) + else (incr token_number;next true) in + let loc = next (pos >= !last_pos) in + last_pos := pos; + let path = Names.string_of_dirpath path in + let _sc = match sc with Some sc -> " "^sc | None -> "" in + dump_string (Printf.sprintf "R%d %s \"%s\" not\n" (fst (Util.unloc loc)) path df) + + diff --git a/interp/modintern.ml b/interp/modintern.ml index 0af11bad9..3482dd3a0 100644 --- a/interp/modintern.ml +++ b/interp/modintern.ml @@ -61,34 +61,6 @@ let lookup_qualid (modtype:bool) qid = *) -let split_modpath mp = - let rec aux = function - | MPfile dp -> dp, [] - | MPbound mbid -> - Lib.library_dp (), [id_of_mbid mbid] - | MPself msid -> Lib.library_dp (), [id_of_msid msid] - | MPdot (mp,l) -> let (mp', lab) = aux mp in - (mp', id_of_label l :: lab) - in - let (mp, l) = aux mp in - mp, l - -let dump_moddef loc mp ty = - if !Flags.dump then - let (dp, l) = split_modpath mp in - let mp = string_of_dirpath (make_dirpath l) in - Flags.dump_string (Printf.sprintf "%s %d %s %s\n" ty (fst (unloc loc)) "<>" mp) - -let rec drop_last = function [] -> assert false | hd :: [] -> [] | hd :: tl -> hd :: drop_last tl - -let dump_modref loc mp ty = - if !Flags.dump then - let (dp, l) = split_modpath mp in - let fp = string_of_dirpath dp in - let mp = string_of_dirpath (make_dirpath (drop_last l)) in - Flags.dump_string (Printf.sprintf "R%d %s %s %s %s\n" - (fst (unloc loc)) fp mp "<>" ty) - (* Search for the head of [qid] in [binders]. If found, returns the module_path/kernel_name created from the dirpath and the basename. Searches Nametab otherwise. @@ -96,14 +68,14 @@ let dump_modref loc mp ty = let lookup_module (loc,qid) = try let mp = Nametab.locate_module qid in - dump_modref loc mp "modtype"; mp + Dumpglob.dump_modref loc mp "modtype"; mp with | Not_found -> Modops.error_not_a_module_loc loc (string_of_qualid qid) let lookup_modtype (loc,qid) = try let mp = Nametab.locate_modtype qid in - dump_modref loc mp "mod"; mp + Dumpglob.dump_modref loc mp "mod"; mp with | Not_found -> Modops.error_not_a_modtype_loc loc (string_of_qualid qid) diff --git a/interp/modintern.mli b/interp/modintern.mli index c14b6481e..1f27e3c18 100644 --- a/interp/modintern.mli +++ b/interp/modintern.mli @@ -26,6 +26,3 @@ val interp_modtype : env -> module_type_ast -> module_struct_entry val interp_modexpr : env -> module_ast -> module_struct_entry val lookup_module : qualid located -> module_path - -val dump_moddef : loc -> module_path -> string -> unit -val dump_modref : loc -> module_path -> string -> unit |