aboutsummaryrefslogtreecommitdiffhomepage
path: root/interp
diff options
context:
space:
mode:
authorGravatar notin <notin@85f007b7-540e-0410-9357-904b9bb8a0f7>2008-06-25 18:19:21 +0000
committerGravatar notin <notin@85f007b7-540e-0410-9357-904b9bb8a0f7>2008-06-25 18:19:21 +0000
commit693d398b5e4e55a916bbdaa8e4c23c83d9dbcef7 (patch)
treee015dc24293114d03433c2cf4412b4fa5df9b87c /interp
parent217bbf499dc09f11a137fdc9aead1e0a78c760c2 (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.ml164
-rw-r--r--interp/constrintern.mli7
-rw-r--r--interp/dumpglob.ml220
-rw-r--r--interp/modintern.ml32
-rw-r--r--interp/modintern.mli3
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