diff options
| -rw-r--r-- | library/libnames.ml | 23 | ||||
| -rw-r--r-- | library/libnames.mli | 4 | ||||
| -rwxr-xr-x | library/nametab.ml | 59 | ||||
| -rwxr-xr-x | library/nametab.mli | 15 |
4 files changed, 66 insertions, 35 deletions
diff --git a/library/libnames.ml b/library/libnames.ml index 9a8439804..03d16f417 100644 --- a/library/libnames.ml +++ b/library/libnames.ml @@ -54,6 +54,24 @@ module RefOrdered = module Refset = Set.Make(RefOrdered) module Refmap = Map.Make(RefOrdered) +module InductiveOrdered = struct + type t = inductive + let compare (spx,ix) (spy,iy) = + let c = ix - iy in if c = 0 then compare spx spy else c +end + +module Indmap = Map.Make(InductiveOrdered) + +let inductives_table = ref Indmap.empty + +module ConstructorOrdered = struct + type t = constructor + let compare (indx,ix) (indy,iy) = + let c = ix - iy in if c = 0 then InductiveOrdered.compare indx indy else c +end + +module Constrmap = Map.Make(ConstructorOrdered) + (**********************************************) let pr_dirpath sl = (str (string_of_dirpath sl)) @@ -130,8 +148,8 @@ let repr_path { dirpath = pa; basename = id } = (pa,id) (* parsing and printing of section paths *) let string_of_path sp = let (sl,id) = repr_path sp in - if repr_dirpath sl = [] then string_of_v7_id id - else (string_of_dirpath sl) ^ "." ^ (string_of_v7_id id) + if repr_dirpath sl = [] then string_of_id id + else (string_of_dirpath sl) ^ "." ^ (string_of_id id) let sp_ord sp1 sp2 = let (p1,id1) = repr_path sp1 @@ -249,3 +267,4 @@ let pr_reference = function let loc_of_reference = function | Qualid (loc,qid) -> loc | Ident (loc,id) -> loc + diff --git a/library/libnames.mli b/library/libnames.mli index e902cec9b..95b47c52b 100644 --- a/library/libnames.mli +++ b/library/libnames.mli @@ -34,6 +34,9 @@ val reference_of_constr : constr -> global_reference module Refset : Set.S with type elt = global_reference module Refmap : Map.S with type key = global_reference +module Indmap : Map.S with type key = inductive +module Constrmap : Map.S with type key = constructor + (*s Dirpaths *) val pr_dirpath : dir_path -> Pp.std_ppcmds @@ -135,4 +138,3 @@ val qualid_of_reference : reference -> qualid located val string_of_reference : reference -> string val pr_reference : reference -> std_ppcmds val loc_of_reference : reference -> loc - diff --git a/library/nametab.ml b/library/nametab.ml index ba3e7ff9f..27f56e7b4 100755 --- a/library/nametab.ml +++ b/library/nametab.ml @@ -243,6 +243,7 @@ let the_ccitab = ref (SpTab.empty : ccitab) type kntab = kernel_name SpTab.t let the_modtypetab = ref (SpTab.empty : kntab) +let the_tactictab = ref (SpTab.empty : kntab) type objtab = unit SpTab.t let the_objtab = ref (SpTab.empty : objtab) @@ -277,9 +278,9 @@ let the_globrevtab = ref (Globrevtab.empty : globrevtab) type mprevtab = dir_path MPmap.t let the_modrevtab = ref (MPmap.empty : mprevtab) - type knrevtab = section_path KNmap.t let the_modtyperevtab = ref (KNmap.empty : knrevtab) +let the_tacticrevtab = ref (KNmap.empty : knrevtab) (* Push functions *********************************************************) @@ -308,6 +309,12 @@ let push_modtype vis sp kn = the_modtypetab := SpTab.push vis sp kn !the_modtypetab; the_modtyperevtab := KNmap.add kn sp !the_modtyperevtab +(* This is for tactic definition names *) + +let push_tactic vis sp kn = + the_tactictab := SpTab.push vis sp kn !the_tactictab; + the_tacticrevtab := KNmap.add kn sp !the_tacticrevtab + (* This is for dischargeable non-cci objects (removed at the end of the section -- i.e. Hints, Grammar ...) *) (* --> Unused *) @@ -315,10 +322,6 @@ let push_modtype vis sp kn = let push_object visibility sp = the_objtab := SpTab.push visibility sp () !the_objtab -(* This is for tactic definition names *) - -let push_tactic = push_object - (* This is to remember absolute Section/Module names and to avoid redundancy *) let push_dir vis dir dir_ref = the_dirtab := DirTab.push vis dir dir_ref !the_dirtab; @@ -348,11 +351,9 @@ let full_name_modtype qid = SpTab.user_name qid !the_modtypetab let locate_obj qid = SpTab.user_name qid !the_objtab -type ltac_constant = section_path -let locate_tactic = locate_obj - -let shortest_qualid_of_tactic sp = - SpTab.shortest_qualid Idset.empty sp !the_objtab +type ltac_constant = kernel_name +let locate_tactic qid = SpTab.locate qid !the_tactictab +let full_name_tactic qid = SpTab.user_name qid !the_tactictab let locate_dir qid = DirTab.locate qid !the_dirtab @@ -416,6 +417,7 @@ let exists_module = exists_dir let exists_modtype sp = SpTab.exists sp !the_modtypetab +let exists_tactic sp = SpTab.exists sp !the_tactictab (* Reverse locate functions ***********************************************) @@ -457,6 +459,10 @@ let shortest_qualid_of_modtype kn = let sp = KNmap.find kn !the_modtyperevtab in SpTab.shortest_qualid Idset.empty sp !the_modtypetab +let shortest_qualid_of_tactic kn = + let sp = KNmap.find kn !the_tacticrevtab in + SpTab.shortest_qualid Idset.empty sp !the_tactictab + let pr_global_env env ref = (* Il est important de laisser le let-in, car les streams s'évaluent paresseusement : il faut forcer l'évaluation pour capturer @@ -476,35 +482,42 @@ let global_inductive r = (********************************************************************) (* Registration of tables as a global table and rollback *) -type frozen = ccitab * dirtab * objtab * kntab - * globrevtab * mprevtab * knrevtab +type frozen = ccitab * dirtab * objtab * kntab * kntab + * globrevtab * mprevtab * knrevtab * knrevtab let init () = the_ccitab := SpTab.empty; the_dirtab := DirTab.empty; the_objtab := SpTab.empty; the_modtypetab := SpTab.empty; + the_tactictab := SpTab.empty; the_globrevtab := Globrevtab.empty; the_modrevtab := MPmap.empty; - the_modtyperevtab := KNmap.empty + the_modtyperevtab := KNmap.empty; + the_tacticrevtab := KNmap.empty + let freeze () = !the_ccitab, !the_dirtab, !the_objtab, !the_modtypetab, + !the_tactictab, !the_globrevtab, !the_modrevtab, - !the_modtyperevtab - -let unfreeze (mc,md,mo,mt,gt,mrt,mtrt) = - the_ccitab := mc; - the_dirtab := md; - the_objtab := mo; - the_modtypetab := mt; - the_globrevtab := gt; - the_modrevtab := mrt; - the_modtyperevtab := mtrt + !the_modtyperevtab, + !the_tacticrevtab + +let unfreeze (ccit,dirt,objt,mtyt,tact,globr,modr,mtyr,tacr) = + the_ccitab := ccit; + the_dirtab := dirt; + the_objtab := objt; + the_modtypetab := mtyt; + the_tactictab := tact; + the_globrevtab := globr; + the_modrevtab := modr; + the_modtyperevtab := mtyr; + the_tacticrevtab := tacr let _ = Summary.declare_summary "names" diff --git a/library/nametab.mli b/library/nametab.mli index df433d145..f1af6c171 100755 --- a/library/nametab.mli +++ b/library/nametab.mli @@ -75,7 +75,7 @@ val push_syntactic_definition : val push_modtype : visibility -> section_path -> kernel_name -> unit val push_dir : visibility -> dir_path -> global_dir_reference -> unit val push_object : visibility -> section_path -> unit -val push_tactic : visibility -> section_path -> unit +val push_tactic : visibility -> section_path -> kernel_name -> unit (*s The following functions perform globalization of qualified names *) @@ -101,9 +101,8 @@ val locate_section : qualid -> dir_path val locate_modtype : qualid -> kernel_name val locate_syntactic_definition : qualid -> kernel_name -type ltac_constant = section_path +type ltac_constant = kernel_name val locate_tactic : qualid -> ltac_constant -val shortest_qualid_of_tactic : ltac_constant -> qualid val locate_dir : qualid -> global_dir_reference val locate_module : qualid -> module_path @@ -136,13 +135,11 @@ val full_name_module : qualid -> dir_path internal name *) val sp_of_syntactic_definition : kernel_name -> section_path -val shortest_qualid_of_global : - Idset.t -> global_reference -> qualid -val shortest_qualid_of_syndef : - kernel_name -> qualid +val shortest_qualid_of_global : Idset.t -> global_reference -> qualid +val shortest_qualid_of_syndef : kernel_name -> qualid +val shortest_qualid_of_tactic : ltac_constant -> qualid -val dir_of_mp : - module_path -> dir_path +val dir_of_mp : module_path -> dir_path val sp_of_global : global_reference -> section_path val id_of_global : global_reference -> identifier |