diff options
Diffstat (limited to 'kernel/names.ml')
| -rw-r--r-- | kernel/names.ml | 305 |
1 files changed, 168 insertions, 137 deletions
diff --git a/kernel/names.ml b/kernel/names.ml index a3aa71f2..e1d70e81 100644 --- a/kernel/names.ml +++ b/kernel/names.ml @@ -17,7 +17,7 @@ the module system, Aug 2002 *) (* Abstraction over the type of constant for module inlining by Claudio Sacerdoti, Nov 2004 *) -(* Miscellaneous features or improvements by Hugo Herbelin, +(* Miscellaneous features or improvements by Hugo Herbelin, Élie Soubiran, ... *) open Pp @@ -364,7 +364,6 @@ module MPmap = CMap.Make(ModPath) module KerName = struct type t = { - canary : Canary.t; modpath : ModPath.t; dirpath : DirPath.t; knlabel : Label.t; @@ -372,16 +371,14 @@ module KerName = struct (** Lazily computed hash. If unset, it is set to negative values. *) } - let canary = Canary.obj - type kernel_name = t let make modpath dirpath knlabel = - { modpath; dirpath; knlabel; refhash = -1; canary; } + { modpath; dirpath; knlabel; refhash = -1; } let repr kn = (kn.modpath, kn.dirpath, kn.knlabel) let make2 modpath knlabel = - { modpath; dirpath = DirPath.empty; knlabel; refhash = -1; canary; } + { modpath; dirpath = DirPath.empty; knlabel; refhash = -1; } let modpath kn = kn.modpath let label kn = kn.knlabel @@ -437,7 +434,7 @@ module KerName = struct * (string -> string) let hashcons (hmod,hdir,hstr) kn = let { modpath = mp; dirpath = dp; knlabel = l; refhash; } = kn in - { modpath = hmod mp; dirpath = hdir dp; knlabel = hstr l; refhash; canary; } + { modpath = hmod mp; dirpath = hdir dp; knlabel = hstr l; refhash; } let eq kn1 kn2 = kn1.modpath == kn2.modpath && kn1.dirpath == kn2.dirpath && kn1.knlabel == kn2.knlabel @@ -701,22 +698,6 @@ end module Constrmap = Map.Make(ConstructorOrdered) module Constrmap_env = Map.Make(ConstructorOrdered_env) -type global_reference = - | VarRef of variable (** A reference to the section-context. *) - | ConstRef of Constant.t (** A reference to the environment. *) - | IndRef of inductive (** A reference to an inductive type. *) - | ConstructRef of constructor (** A reference to a constructor of an inductive type. *) - -(* Better to have it here that in closure, since used in grammar.cma *) -type evaluable_global_reference = - | EvalVarRef of Id.t - | EvalConstRef of Constant.t - -let eq_egr e1 e2 = match e1, e2 with - EvalConstRef con1, EvalConstRef con2 -> Constant.equal con1 con2 - | EvalVarRef id1, EvalVarRef id2 -> Id.equal id1 id2 - | _, _ -> false - (** {6 Hash-consing of name objects } *) module Hind = Hashcons.Make( @@ -776,109 +757,155 @@ let eq_ind_chk (kn1,i1) (kn2,i2) = Int.equal i1 i2 && eq_mind_chk kn1 kn2 (*******************************************************************) (** Compatibility layers *) -(** Backward compatibility for [Id] *) +type mod_bound_id = MBId.t +let eq_constant_key = Constant.UserOrd.equal + +(** Compatibility layer for [ModPath] *) + +type module_path = ModPath.t = + | MPfile of DirPath.t + | MPbound of MBId.t + | MPdot of module_path * Label.t + +(** Compatibility layer for [Constant] *) -type identifier = Id.t +module Projection = +struct + module Repr = struct + type t = + { proj_ind : inductive; + proj_npars : int; + proj_arg : int; + proj_name : Label.t; } -let id_eq = Id.equal -let id_ord = Id.compare -let string_of_id = Id.to_string -let id_of_string = Id.of_string + let make proj_ind ~proj_npars ~proj_arg proj_name = + {proj_ind;proj_npars;proj_arg;proj_name} -module Idset = Id.Set -module Idmap = Id.Map -module Idpred = Id.Pred + let inductive c = c.proj_ind -(** Compatibility layer for [Name] *) + let mind c = fst c.proj_ind -let name_eq = Name.equal + let constant c = KerPair.change_label (mind c) c.proj_name -(** Compatibility layer for [DirPath] *) + let label c = c.proj_name -type dir_path = DirPath.t -let dir_path_ord = DirPath.compare -let dir_path_eq = DirPath.equal -let make_dirpath = DirPath.make -let repr_dirpath = DirPath.repr -let empty_dirpath = DirPath.empty -let is_empty_dirpath = DirPath.is_empty -let string_of_dirpath = DirPath.to_string -let initial_dir = DirPath.initial + let npars c = c.proj_npars -(** Compatibility layer for [MBId] *) + let arg c = c.proj_arg -type mod_bound_id = MBId.t -let mod_bound_id_ord = MBId.compare -let mod_bound_id_eq = MBId.equal -let make_mbid = MBId.make -let repr_mbid = MBId.repr -let debug_string_of_mbid = MBId.debug_to_string -let string_of_mbid = MBId.to_string -let id_of_mbid = MBId.to_id - -(** Compatibility layer for [Label] *) - -type label = Id.t -let mk_label = Label.make -let string_of_label = Label.to_string -let pr_label = Label.print -let id_of_label = Label.to_id -let label_of_id = Label.of_id -let eq_label = Label.equal + let equal a b = + eq_ind a.proj_ind b.proj_ind && Int.equal a.proj_arg b.proj_arg -(** Compatibility layer for [ModPath] *) + let hash p = + Hashset.Combine.combinesmall p.proj_arg (ind_hash p.proj_ind) -type module_path = ModPath.t = - | MPfile of DirPath.t - | MPbound of MBId.t - | MPdot of module_path * Label.t -let check_bound_mp = ModPath.is_bound -let string_of_mp = ModPath.to_string -let mp_ord = ModPath.compare -let mp_eq = ModPath.equal -let initial_path = ModPath.initial - -(** Compatibility layer for [KerName] *) - -type kernel_name = KerName.t -let make_kn = KerName.make -let repr_kn = KerName.repr -let modpath = KerName.modpath -let label = KerName.label -let string_of_kn = KerName.to_string -let pr_kn = KerName.print -let kn_ord = KerName.compare + module SyntacticOrd = struct + let compare a b = + let c = ind_syntactic_ord a.proj_ind b.proj_ind in + if c == 0 then Int.compare a.proj_arg b.proj_arg + else c -(** Compatibility layer for [Constant] *) + let equal a b = + a.proj_arg == b.proj_arg && eq_syntactic_ind a.proj_ind b.proj_ind -type constant = Constant.t + let hash p = + Hashset.Combine.combinesmall p.proj_arg (ind_hash p.proj_ind) + end + module CanOrd = struct + let compare a b = + let c = ind_ord a.proj_ind b.proj_ind in + if c == 0 then Int.compare a.proj_arg b.proj_arg + else c + let equal a b = + a.proj_arg == b.proj_arg && eq_ind a.proj_ind b.proj_ind + + let hash p = + Hashset.Combine.combinesmall p.proj_arg (ind_hash p.proj_ind) + end + module UserOrd = struct + let compare a b = + let c = ind_user_ord a.proj_ind b.proj_ind in + if c == 0 then Int.compare a.proj_arg b.proj_arg + else c + + let equal a b = + a.proj_arg == b.proj_arg && eq_user_ind a.proj_ind b.proj_ind + + let hash p = + Hashset.Combine.combinesmall p.proj_arg (ind_user_hash p.proj_ind) + end + + let compare a b = + let c = ind_ord a.proj_ind b.proj_ind in + if c == 0 then Int.compare a.proj_arg b.proj_arg + else c + + module Self_Hashcons = struct + type nonrec t = t + type u = (inductive -> inductive) * (Id.t -> Id.t) + let hashcons (hind,hid) p = + { proj_ind = hind p.proj_ind; + proj_npars = p.proj_npars; + proj_arg = p.proj_arg; + proj_name = hid p.proj_name } + let eq p p' = + p == p' || (p.proj_ind == p'.proj_ind && p.proj_npars == p'.proj_npars && p.proj_arg == p'.proj_arg && p.proj_name == p'.proj_name) + let hash = hash + end + module HashRepr = Hashcons.Make(Self_Hashcons) + let hcons = Hashcons.simple_hcons HashRepr.generate HashRepr.hcons (hcons_ind,Id.hcons) + + let map_npars f p = + let ind = fst p.proj_ind in + let npars = p.proj_npars in + let ind', npars' = f ind npars in + if ind == ind' && npars == npars' then p + else {p with proj_ind = (ind',snd p.proj_ind); proj_npars = npars'} + + let map f p = map_npars (fun mind n -> f mind, n) p + + let to_string p = Constant.to_string (constant p) + let print p = Constant.print (constant p) + end + + type t = Repr.t * bool -module Projection = -struct - type t = constant * bool - let make c b = (c, b) - let constant = fst + let mind (c,_) = Repr.mind c + let inductive (c,_) = Repr.inductive c + let npars (c,_) = Repr.npars c + let arg (c,_) = Repr.arg c + let constant (c,_) = Repr.constant c + let label (c,_) = Repr.label c + let repr = fst let unfolded = snd let unfold (c, b as p) = if b then p else (c, true) - let equal (c, b) (c', b') = Constant.equal c c' && b == b' - let hash (c, b) = (if b then 0 else 1) + Constant.hash c + let equal (c, b) (c', b') = Repr.equal c c' && b == b' + + let hash (c, b) = (if b then 0 else 1) + Repr.hash c module SyntacticOrd = struct let compare (c, b) (c', b') = - if b = b' then Constant.SyntacticOrd.compare c c' else -1 + if b = b' then Repr.SyntacticOrd.compare c c' else -1 let equal (c, b as x) (c', b' as x') = - x == x' || b = b' && Constant.SyntacticOrd.equal c c' - let hash (c, b) = (if b then 0 else 1) + Constant.SyntacticOrd.hash c + x == x' || b = b' && Repr.SyntacticOrd.equal c c' + let hash (c, b) = (if b then 0 else 1) + Repr.SyntacticOrd.hash c + end + module CanOrd = struct + let compare (c, b) (c', b') = + if b = b' then Repr.CanOrd.compare c c' else -1 + let equal (c, b as x) (c', b' as x') = + x == x' || b = b' && Repr.CanOrd.equal c c' + let hash (c, b) = (if b then 0 else 1) + Repr.CanOrd.hash c end module Self_Hashcons = struct type nonrec t = t - type u = Constant.t -> Constant.t + type u = Repr.t -> Repr.t let hashcons hc (c,b) = (hc c,b) let eq ((c,b) as x) ((c',b') as y) = x == y || (c == c' && b == b') @@ -887,15 +914,19 @@ struct module HashProjection = Hashcons.Make(Self_Hashcons) - let hcons = Hashcons.simple_hcons HashProjection.generate HashProjection.hcons hcons_con + let hcons = Hashcons.simple_hcons HashProjection.generate HashProjection.hcons Repr.hcons let compare (c, b) (c', b') = - if b == b' then Constant.CanOrd.compare c c' + if b == b' then Repr.compare c c' else if b then 1 else -1 let map f (c, b as x) = - let c' = f c in - if c' == c then x else (c', b) + let c' = Repr.map f c in + if c' == c then x else (c', b) + + let map_npars f (c, b as x) = + let c' = Repr.map_npars f c in + if c' == c then x else (c', b) let to_string p = Constant.to_string (constant p) let print p = Constant.print (constant p) @@ -904,39 +935,39 @@ end type projection = Projection.t -let constant_of_kn = Constant.make1 -let constant_of_kn_equiv = Constant.make -let make_con = Constant.make3 -let repr_con = Constant.repr3 -let canonical_con = Constant.canonical -let user_con = Constant.user -let con_label = Constant.label -let con_modpath = Constant.modpath -let eq_constant = Constant.equal -let eq_constant_key = Constant.UserOrd.equal -let con_ord = Constant.CanOrd.compare -let con_user_ord = Constant.UserOrd.compare -let string_of_con = Constant.to_string -let pr_con = Constant.print -let debug_string_of_con = Constant.debug_to_string -let debug_pr_con = Constant.debug_print -let con_with_label = Constant.change_label - -(** Compatibility layer for [MutInd] *) - -type mutual_inductive = MutInd.t -let mind_of_kn = MutInd.make1 -let mind_of_kn_equiv = MutInd.make -let make_mind = MutInd.make3 -let canonical_mind = MutInd.canonical -let user_mind = MutInd.user -let repr_mind = MutInd.repr3 -let mind_label = MutInd.label -let mind_modpath = MutInd.modpath -let eq_mind = MutInd.equal -let mind_ord = MutInd.CanOrd.compare -let mind_user_ord = MutInd.UserOrd.compare -let string_of_mind = MutInd.to_string -let pr_mind = MutInd.print -let debug_string_of_mind = MutInd.debug_to_string -let debug_pr_mind = MutInd.debug_print +module GlobRef = struct + + type t = + | VarRef of variable (** A reference to the section-context. *) + | ConstRef of Constant.t (** A reference to the environment. *) + | IndRef of inductive (** A reference to an inductive type. *) + | ConstructRef of constructor (** A reference to a constructor of an inductive type. *) + + let equal gr1 gr2 = + gr1 == gr2 || match gr1,gr2 with + | ConstRef con1, ConstRef con2 -> Constant.equal con1 con2 + | IndRef kn1, IndRef kn2 -> eq_ind kn1 kn2 + | ConstructRef kn1, ConstructRef kn2 -> eq_constructor kn1 kn2 + | VarRef v1, VarRef v2 -> Id.equal v1 v2 + | (ConstRef _ | IndRef _ | ConstructRef _ | VarRef _), _ -> false + +end + +type global_reference = GlobRef.t +[@@ocaml.deprecated "Alias for [GlobRef.t]"] + +type evaluable_global_reference = + | EvalVarRef of Id.t + | EvalConstRef of Constant.t + +(* Better to have it here that in closure, since used in grammar.cma *) +let eq_egr e1 e2 = match e1, e2 with + EvalConstRef con1, EvalConstRef con2 -> Constant.equal con1 con2 + | EvalVarRef id1, EvalVarRef id2 -> Id.equal id1 id2 + | _, _ -> false + +(** Located identifiers and objects with syntax. *) + +type lident = Id.t CAst.t +type lname = Name.t CAst.t +type lstring = string CAst.t |