From 2e43b03b0bb88bd3b4cb7695d5079c51ca41b0a7 Mon Sep 17 00:00:00 2001 From: ppedrot Date: Thu, 22 Nov 2012 18:09:38 +0000 Subject: Monomorphization (library) git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15993 85f007b7-540e-0410-9357-904b9bb8a0f7 --- library/nametab.ml | 179 ++++++++++++++++++++++++++++++++--------------------- 1 file changed, 110 insertions(+), 69 deletions(-) (limited to 'library/nametab.ml') diff --git a/library/nametab.ml b/library/nametab.ml index 871381530..7c1100165 100644 --- a/library/nametab.ml +++ b/library/nametab.ml @@ -46,10 +46,16 @@ type visibility = Until of int | Exactly of int (* The [repr] function is assumed to return the reversed list of idents. *) module type UserName = sig type t + val equal : t -> t -> bool val to_string : t -> string val repr : t -> identifier * module_ident list end +module type EqualityType = +sig + type t + val equal : t -> t -> bool +end (* A ['a t] is a map from [user_name] to ['a], with possible lookup by partially qualified names of type [qualid]. The mapping of @@ -61,39 +67,41 @@ end the same object. *) module type NAMETREE = sig - type 'a t + type elt + type t type user_name - val empty : 'a t - val push : visibility -> user_name -> 'a -> 'a t -> 'a t - val locate : qualid -> 'a t -> 'a - val find : user_name -> 'a t -> 'a - val exists : user_name -> 'a t -> bool - val user_name : qualid -> 'a t -> user_name - val shortest_qualid : Idset.t -> user_name -> 'a t -> qualid - val find_prefixes : qualid -> 'a t -> 'a list + val empty : t + val push : visibility -> user_name -> elt -> t -> t + val locate : qualid -> t -> elt + val find : user_name -> t -> elt + val exists : user_name -> t -> bool + val user_name : qualid -> t -> user_name + val shortest_qualid : Idset.t -> user_name -> t -> qualid + val find_prefixes : qualid -> t -> elt list end -module Make(U:UserName) : NAMETREE with type user_name = U.t - = +module Make (U : UserName) (E : EqualityType) : NAMETREE + with type user_name = U.t and type elt = E.t = struct + type elt = E.t type user_name = U.t - type 'a path_status = + type path_status = Nothing - | Relative of user_name * 'a - | Absolute of user_name * 'a + | Relative of user_name * elt + | Absolute of user_name * elt (* Dictionaries of short names *) - type 'a nametree = - { path : 'a path_status; - map : 'a nametree ModIdmap.t } + type nametree = + { path : path_status; + map : nametree ModIdmap.t } let mktree p m = { path=p; map=m } let empty_tree = mktree Nothing ModIdmap.empty - type 'a t = 'a nametree Idmap.t + type t = nametree Idmap.t let empty = Idmap.empty @@ -125,8 +133,8 @@ struct | [] -> match tree.path with | Absolute (uname',o') -> - if o'=o then begin - assert (uname=uname'); + if E.equal o' o then begin + assert (U.equal uname uname'); tree (* we are putting the same thing for the second time :) *) end @@ -146,7 +154,7 @@ let rec push_exactly uname o level tree = function try ModIdmap.find modid tree.map with Not_found -> empty_tree in - if level = 0 then + if Int.equal level 0 then let this = match tree.path with | Absolute (n,_) -> @@ -219,9 +227,10 @@ let shortest_qualid ctx uname tab = let id,dir = U.repr uname in let hidden = Idset.mem id ctx in let rec find_uname pos dir tree = + let is_empty = match pos with [] -> true | _ -> false in match tree.path with | Absolute (u,_) | Relative (u,_) - when u=uname && not(pos=[] && hidden) -> List.rev pos + when U.equal u uname && not (is_empty && hidden) -> List.rev pos | _ -> match dir with [] -> raise Not_found @@ -256,36 +265,68 @@ end (* Global name tables *************************************************) -module SpTab = Make (struct - type t = full_path - let to_string = string_of_path - let repr sp = - let dir,id = repr_path sp in - id, (repr_dirpath dir) - end) +module FullPath = +struct + type t = full_path + let equal = eq_full_path + let to_string = string_of_path + let repr sp = + let dir,id = repr_path sp in + id, (repr_dirpath dir) +end +module ExtRefEqual = +struct + type t = extended_global_reference + let equal e1 e2 = Int.equal (ExtRefOrdered.compare e1 e2) 0 +end -type ccitab = extended_global_reference SpTab.t -let the_ccitab = ref (SpTab.empty : ccitab) +module KnEqual = +struct + type t = kernel_name + let equal kn1 kn2 = Int.equal (kn_ord kn1 kn2) 0 +end -type kntab = kernel_name SpTab.t -let the_tactictab = ref (SpTab.empty : kntab) +module MPEqual = +struct + type t = module_path + let equal = mp_eq +end + +module ExtRefTab = Make(FullPath)(ExtRefEqual) +module KnTab = Make(FullPath)(KnEqual) +module MPTab = Make(FullPath)(MPEqual) + +type ccitab = ExtRefTab.t +let the_ccitab = ref (ExtRefTab.empty : ccitab) -type mptab = module_path SpTab.t -let the_modtypetab = ref (SpTab.empty : mptab) +type kntab = KnTab.t +let the_tactictab = ref (KnTab.empty : kntab) +type mptab = MPTab.t +let the_modtypetab = ref (MPTab.empty : mptab) + +module DirPath = +struct + type t = dir_path + let equal d1 d2 = Int.equal (dir_path_ord d1 d2) 0 + let to_string = string_of_dirpath + let repr dir = match repr_dirpath dir with + | [] -> anomaly "Empty dirpath" + | id :: l -> (id, l) +end + +module GlobDir = +struct + type t = global_dir_reference + let equal = eq_global_dir_reference +end -module DirTab = Make(struct - type t = dir_path - let to_string = string_of_dirpath - let repr dir = match repr_dirpath dir with - | [] -> anomaly "Empty dirpath" - | id::l -> (id,l) - end) +module DirTab = Make(DirPath)(GlobDir) (* If we have a (closed) module M having a submodule N, than N does not have the entry in [the_dirtab]. *) -type dirtab = global_dir_reference DirTab.t +type dirtab = DirTab.t let the_dirtab = ref (DirTab.empty : dirtab) @@ -317,19 +358,19 @@ let the_tacticrevtab = ref (KNmap.empty : knrevtab) let push_xref visibility sp xref = match visibility with | Until _ -> - the_ccitab := SpTab.push visibility sp xref !the_ccitab; + the_ccitab := ExtRefTab.push visibility sp xref !the_ccitab; the_globrevtab := Globrevtab.add xref sp !the_globrevtab | _ -> begin - if SpTab.exists sp !the_ccitab then - match SpTab.find sp !the_ccitab with + if ExtRefTab.exists sp !the_ccitab then + match ExtRefTab.find sp !the_ccitab with | TrueGlobal( ConstRef _) | TrueGlobal( IndRef _) | TrueGlobal( ConstructRef _) as xref -> - the_ccitab := SpTab.push visibility sp xref !the_ccitab; + the_ccitab := ExtRefTab.push visibility sp xref !the_ccitab; | _ -> - the_ccitab := SpTab.push visibility sp xref !the_ccitab; + the_ccitab := ExtRefTab.push visibility sp xref !the_ccitab; else - the_ccitab := SpTab.push visibility sp xref !the_ccitab; + the_ccitab := ExtRefTab.push visibility sp xref !the_ccitab; end let push_cci visibility sp ref = @@ -342,13 +383,13 @@ let push_syndef visibility sp kn = let push = push_cci let push_modtype vis sp kn = - the_modtypetab := SpTab.push vis sp kn !the_modtypetab; + the_modtypetab := MPTab.push vis sp kn !the_modtypetab; the_modtyperevtab := MPmap.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_tactictab := KnTab.push vis sp kn !the_tactictab; the_tacticrevtab := KNmap.add kn sp !the_tacticrevtab @@ -364,22 +405,22 @@ let push_dir vis dir dir_ref = (* This should be used when syntactic definitions are allowed *) -let locate_extended qid = SpTab.locate qid !the_ccitab +let locate_extended qid = ExtRefTab.locate qid !the_ccitab (* This should be used when no syntactic definitions is expected *) let locate qid = match locate_extended qid with | TrueGlobal ref -> ref | SynDef _ -> raise Not_found -let full_name_cci qid = SpTab.user_name qid !the_ccitab +let full_name_cci qid = ExtRefTab.user_name qid !the_ccitab let locate_syndef qid = match locate_extended qid with | TrueGlobal _ -> raise Not_found | SynDef kn -> kn -let locate_modtype qid = SpTab.locate qid !the_modtypetab -let full_name_modtype qid = SpTab.user_name qid !the_modtypetab +let locate_modtype qid = MPTab.locate qid !the_modtypetab +let full_name_modtype qid = MPTab.user_name qid !the_modtypetab -let locate_tactic qid = SpTab.locate qid !the_tactictab +let locate_tactic qid = KnTab.locate qid !the_tactictab let locate_dir qid = DirTab.locate qid !the_dirtab @@ -401,9 +442,9 @@ let locate_section qid = let locate_all qid = List.fold_right (fun a l -> match a with TrueGlobal a -> a::l | _ -> l) - (SpTab.find_prefixes qid !the_ccitab) [] + (ExtRefTab.find_prefixes qid !the_ccitab) [] -let locate_extended_all qid = SpTab.find_prefixes qid !the_ccitab +let locate_extended_all qid = ExtRefTab.find_prefixes qid !the_ccitab (* Derived functions *) @@ -413,11 +454,11 @@ let locate_constant qid = | _ -> raise Not_found let global_of_path sp = - match SpTab.find sp !the_ccitab with + match ExtRefTab.find sp !the_ccitab with | TrueGlobal ref -> ref | _ -> raise Not_found -let extended_global_of_path sp = SpTab.find sp !the_ccitab +let extended_global_of_path sp = ExtRefTab.find sp !the_ccitab let global r = let (loc,qid) = qualid_of_reference r in @@ -432,7 +473,7 @@ let global r = (* Exists functions ********************************************************) -let exists_cci sp = SpTab.exists sp !the_ccitab +let exists_cci sp = ExtRefTab.exists sp !the_ccitab let exists_dir dir = DirTab.exists dir !the_dirtab @@ -440,7 +481,7 @@ let exists_section = exists_dir let exists_module = exists_dir -let exists_modtype sp = SpTab.exists sp !the_modtypetab +let exists_modtype sp = MPTab.exists sp !the_modtypetab (* Reverse locate functions ***********************************************) @@ -471,11 +512,11 @@ let shortest_qualid_of_global ctx ref = | VarRef id -> make_qualid empty_dirpath id | _ -> let sp = Globrevtab.find (TrueGlobal ref) !the_globrevtab in - SpTab.shortest_qualid ctx sp !the_ccitab + ExtRefTab.shortest_qualid ctx sp !the_ccitab let shortest_qualid_of_syndef ctx kn = let sp = path_of_syndef kn in - SpTab.shortest_qualid ctx sp !the_ccitab + ExtRefTab.shortest_qualid ctx sp !the_ccitab let shortest_qualid_of_module mp = let dir = MPmap.find mp !the_modrevtab in @@ -483,11 +524,11 @@ let shortest_qualid_of_module mp = let shortest_qualid_of_modtype kn = let sp = MPmap.find kn !the_modtyperevtab in - SpTab.shortest_qualid Idset.empty sp !the_modtypetab + MPTab.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 + KnTab.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 @@ -513,10 +554,10 @@ type frozen = ccitab * dirtab * mptab * kntab * globrevtab * mprevtab * mptrevtab * knrevtab let init () = - the_ccitab := SpTab.empty; + the_ccitab := ExtRefTab.empty; the_dirtab := DirTab.empty; - the_modtypetab := SpTab.empty; - the_tactictab := SpTab.empty; + the_modtypetab := MPTab.empty; + the_tactictab := KnTab.empty; the_globrevtab := Globrevtab.empty; the_modrevtab := MPmap.empty; the_modtyperevtab := MPmap.empty; -- cgit v1.2.3