From ef64634b31a4cd999cd08636adbf117f81889fb1 Mon Sep 17 00:00:00 2001 From: letouzey Date: Tue, 19 Feb 2013 16:55:18 +0000 Subject: Names: revised representation of constants and mutual_inductive - a module KernelPair for improving sharing between constant and mind - shorter representation than a pair when possible - exports comparisions on constant and mind and ... - a kn_equal function instead of Int.equal (kn_ord ...) 0 git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16217 85f007b7-540e-0410-9357-904b9bb8a0f7 --- checker/validate.ml | 3 +- kernel/names.ml | 267 +++++++++++++++++++++++++++++-------------------- kernel/names.mli | 9 ++ kernel/term.ml | 13 +-- library/assumptions.ml | 8 +- library/globnames.ml | 31 +++--- library/lib.ml | 2 +- library/nametab.ml | 2 +- toplevel/search.ml | 5 +- 9 files changed, 195 insertions(+), 145 deletions(-) diff --git a/checker/validate.ml b/checker/validate.ml index eeff9d1cd..649b2cdd6 100644 --- a/checker/validate.ml +++ b/checker/validate.ml @@ -188,8 +188,7 @@ let val_mp = let val_kn = val_tuple ~name:"kernel_name" [|val_mp;val_dp;val_id|] -let val_con = - val_tuple ~name:"constant/mutind" [|val_kn;val_kn|] +let val_con = val_sum "constant/mutind" 0 [|[|val_kn|];[|val_kn;val_kn|]|] let val_ind = val_tuple ~name:"inductive"[|val_con;val_int|] let val_cstr = val_tuple ~name:"constructor"[|val_ind;val_int|] diff --git a/kernel/names.ml b/kernel/names.ml index 12df0a3c8..f64566f5a 100644 --- a/kernel/names.ml +++ b/kernel/names.ml @@ -323,6 +323,8 @@ let kn_ord (kn1 : kernel_name) (kn2 : kernel_name) = if not (Int.equal c 0) then c else MPord.compare mp1 mp2 +let kn_equal kn1 kn2 = Int.equal (kn_ord kn1 kn2) 0 + module KNord = struct type t = kernel_name let compare = kn_ord @@ -332,58 +334,121 @@ module KNmap = Map.Make(KNord) module KNpred = Predicate.Make(KNord) module KNset = Set.Make(KNord) -(** {6 Constant names } *) +(** {6 Kernel pairs } *) -(** a constant name is a kernel name couple (kn1,kn2) - where kn1 corresponds to the name used at toplevel - (i.e. what the user see) - and kn2 corresponds to the canonical kernel name - i.e. in the environment we have - {% kn1 \rhd_{\delta}^* kn2 \rhd_{\delta} t %} *) -type constant = kernel_name*kernel_name - -let constant_of_kn kn = (kn,kn) -let constant_of_kn_equiv kn1 kn2 = (kn1,kn2) -let make_con mp dir l = constant_of_kn (mp,dir,l) -let make_con_equiv mp1 mp2 dir l = ((mp1,dir,l),(mp2,dir,l)) -let canonical_con con = snd con -let user_con con = fst con -let repr_con con = fst con - -let eq_constant (_, kn1) (_, kn2) = Int.equal (kn_ord kn1 kn2) 0 - -let con_label con = label (fst con) -let con_modpath con = modpath (fst con) - -let string_of_con con = string_of_kn (fst con) -let pr_con con = str (string_of_con con) -let debug_string_of_con con = - "(" ^ string_of_kn (fst con) ^ "," ^ string_of_kn (snd con) ^ ")" -let debug_pr_con con = str (debug_string_of_con con) - -let con_with_label ((mp1,dp1,l1),(mp2,dp2,l2) as con) lbl = - if String.equal lbl l1 && String.equal lbl l2 - then con - else ((mp1, dp1, lbl), (mp2, dp2, lbl)) - -(** For the environment we distinguish constants by their user part*) -module User_ord = struct - type t = kernel_name*kernel_name - let compare x y= kn_ord (fst x) (fst y) -end +(** For constant and inductive names, we use a kernel name couple (kn1,kn2) + where kn1 corresponds to the name used at toplevel (i.e. what the user see) + and kn2 corresponds to the canonical kernel name i.e. in the environment + we have {% kn1 \rhd_{\delta}^* kn2 \rhd_{\delta} t %} + + Invariants : + - the user and canonical kn may differ only on their [module_path], + the dirpaths and labels should be the same + - when user and canonical parts differ, we cannot be in a section + anymore, hence the dirpath must be empty + - two pairs with the same user part should have the same canonical part + + Note: since most of the time the canonical and user parts are equal, + we handle this case with a particular constructor to spare some memory *) + +module KernelPair = struct + + type kernel_pair = + | Same of kernel_name (** user = canonical *) + | Dual of kernel_name * kernel_name (** user then canonical *) + + type t = kernel_pair + + let canonical = function + | Same kn -> kn + | Dual (_,kn) -> kn + + let user = function + | Same kn -> kn + | Dual (kn,_) -> kn + + let same kn = Same kn + let dual knu knc = Dual (knu,knc) + let make knu knc = if knu == knc then Same knc else Dual (knu,knc) + + let debug_to_string = function + | Same kn -> "(" ^ string_of_kn kn ^ ")" + | Dual (knu,knc) -> "(" ^ string_of_kn knu ^ "," ^ string_of_kn knc ^ ")" + + (** Default comparison is on the canonical part *) + let equal x y = x == y || kn_equal (canonical x) (canonical y) + + (** For ordering kernel pairs, both user or canonical parts may make + sense, according to your needs : user for the environments, canonical + for other uses (ex: non-logical things). *) + + module UserOrd = struct + type t = kernel_pair + let compare x y = kn_ord (user x) (user y) + end + + module CanOrd = struct + type t = kernel_pair + let compare x y = kn_ord (canonical x) (canonical y) + end + + (** Hash-consing : we discriminate only on the user part, since having + the same user part implies having the same canonical part + (invariant of the system). *) + + module Self_Hashcons = + struct + type t = kernel_pair + type u = kernel_name -> kernel_name + let hashcons hkn = function + | Same kn -> Same (hkn kn) + | Dual (knu,knc) -> make (hkn knu) (hkn knc) + let equal x y = (user x) == (user y) + let hash = Hashtbl.hash + end + + module HashKP = Hashcons.Make(Self_Hashcons) -(** For other uses (ex: non-logical things) it is enough - to deal with the canonical part *) -module Canonical_ord = struct - type t = kernel_name*kernel_name - let compare x y= kn_ord (snd x) (snd y) end -module Cmap = Map.Make(Canonical_ord) -module Cmap_env = Map.Make(User_ord) -module Cpred = Predicate.Make(Canonical_ord) -module Cset = Set.Make(Canonical_ord) -module Cset_env = Set.Make(User_ord) +(** {6 Constant names } *) + +type constant = KernelPair.t + +let canonical_con = KernelPair.canonical +let user_con = KernelPair.user +let constant_of_kn = KernelPair.same +let constant_of_kn_equiv = KernelPair.make +let make_con mp dir l = KernelPair.same (mp,dir,l) +let make_con_dual mpu mpc dir l = KernelPair.dual (mpu,dir,l) (mpc,dir,l) +let make_con_equiv mpu mpc dir l = + if mpu == mpc then make_con mpc dir l else make_con_dual mpu mpc dir l +let repr_con = user_con + +let eq_constant = KernelPair.equal +let con_ord = KernelPair.CanOrd.compare +let con_user_ord = KernelPair.UserOrd.compare + +let con_label cst = label (canonical_con cst) +let con_modpath cst = modpath (canonical_con cst) + +let string_of_con cst = string_of_kn (canonical_con cst) +let pr_con cst = str (string_of_con cst) +let debug_string_of_con = KernelPair.debug_to_string +let debug_pr_con cst = str (debug_string_of_con cst) + +let con_with_label cst lbl = + let (mp1,dp1,l1) = user_con cst and (mp2,dp2,l2) = canonical_con cst in + assert (String.equal l1 l2 && Dir_path.equal dp1 dp2); + if String.equal lbl l1 + then cst + else make_con_equiv mp1 mp2 dp1 lbl + +module Cmap = Map.Make(KernelPair.CanOrd) +module Cmap_env = Map.Make(KernelPair.UserOrd) +module Cpred = Predicate.Make(KernelPair.CanOrd) +module Cset = Set.Make(KernelPair.CanOrd) +module Cset_env = Set.Make(KernelPair.UserOrd) (** {6 Names of mutual inductive types } *) @@ -394,29 +459,32 @@ module Cset_env = Set.Make(User_ord) (** Beware: first inductive has index 0 *) (** Beware: first constructor has index 1 *) -type mutual_inductive = kernel_name*kernel_name +type mutual_inductive = KernelPair.t type inductive = mutual_inductive * int type constructor = inductive * int -let mind_modpath mind = modpath (fst mind) +let mind_modpath mind = modpath (KernelPair.user mind) let ind_modpath ind = mind_modpath (fst ind) let constr_modpath c = ind_modpath (fst c) -let mind_of_kn kn = (kn,kn) -let mind_of_kn_equiv kn1 kn2 = (kn1,kn2) -let make_mind mp dir l = ((mp,dir,l),(mp,dir,l)) -let make_mind_equiv mp1 mp2 dir l = ((mp1,dir,l),(mp2,dir,l)) -let canonical_mind mind = snd mind -let user_mind mind = fst mind -let repr_mind mind = fst mind -let mind_label mind = label (fst mind) - -let eq_mind (_, kn1) (_, kn2) = Int.equal (kn_ord kn1 kn2) 0 - -let string_of_mind mind = string_of_kn (fst mind) +let mind_of_kn = KernelPair.same +let mind_of_kn_equiv = KernelPair.make +let make_mind mp dir l = KernelPair.same (mp,dir,l) +let make_mind_dual mpu mpc dir l = KernelPair.dual (mpu,dir,l) (mpc,dir,l) +let make_mind_equiv mpu mpc dir l = + if mpu == mpc then make_mind mpu dir l else make_mind_dual mpu mpc dir l +let canonical_mind = KernelPair.canonical +let user_mind = KernelPair.user +let repr_mind = user_mind +let mind_label mind = label (user_mind mind) + +let eq_mind = KernelPair.equal +let mind_ord = KernelPair.CanOrd.compare +let mind_user_ord = KernelPair.UserOrd.compare + +let string_of_mind mind = string_of_kn (user_mind mind) let pr_mind mind = str (string_of_mind mind) -let debug_string_of_mind mind = - "(" ^ string_of_kn (fst mind) ^ "," ^ string_of_kn (snd mind) ^ ")" +let debug_string_of_mind = KernelPair.debug_to_string let debug_pr_mind con = str (debug_string_of_mind con) let ith_mutual_inductive (kn, _) i = (kn, i) @@ -424,26 +492,34 @@ let ith_constructor_of_inductive ind i = (ind, i) let inductive_of_constructor (ind, i) = ind let index_of_constructor (ind, i) = i -let eq_ind (kn1, i1) (kn2, i2) = Int.equal i1 i2 && eq_mind kn1 kn2 - -let eq_constructor (kn1, i1) (kn2, i2) = Int.equal i1 i2 && eq_ind kn1 kn2 - -module Mindmap = Map.Make(Canonical_ord) -module Mindset = Set.Make(Canonical_ord) -module Mindmap_env = Map.Make(User_ord) +let eq_ind (m1, i1) (m2, i2) = Int.equal i1 i2 && eq_mind m1 m2 +let ind_ord (m1, i1) (m2, i2) = + let c = Int.compare i1 i2 in + if Int.equal c 0 then mind_ord m1 m2 else c +let ind_user_ord (m1, i1) (m2, i2) = + let c = Int.compare i1 i2 in + if Int.equal c 0 then mind_user_ord m1 m2 else c + +let eq_constructor (ind1, j1) (ind2, j2) = Int.equal j1 j2 && eq_ind ind1 ind2 +let constructor_ord (ind1, j1) (ind2, j2) = + let c = Int.compare j1 j2 in + if Int.equal c 0 then ind_ord ind1 ind2 else c +let constructor_user_ord (ind1, j1) (ind2, j2) = + let c = Int.compare j1 j2 in + if Int.equal c 0 then ind_user_ord ind1 ind2 else c + +module Mindmap = Map.Make(KernelPair.CanOrd) +module Mindset = Set.Make(KernelPair.CanOrd) +module Mindmap_env = Map.Make(KernelPair.UserOrd) module InductiveOrdered = struct type t = inductive - let compare (spx,ix) (spy,iy) = - let c = Int.compare ix iy in - if Int.equal c 0 then Canonical_ord.compare spx spy else c + let compare = ind_ord end module InductiveOrdered_env = struct type t = inductive - let compare (spx,ix) (spy,iy) = - let c = Int.compare ix iy in - if Int.equal c 0 then User_ord.compare spx spy else c + let compare = ind_user_ord end module Indmap = Map.Make(InductiveOrdered) @@ -451,16 +527,12 @@ module Indmap_env = Map.Make(InductiveOrdered_env) module ConstructorOrdered = struct type t = constructor - let compare (indx,ix) (indy,iy) = - let c = Int.compare ix iy in - if Int.equal c 0 then InductiveOrdered.compare indx indy else c + let compare = constructor_ord end module ConstructorOrdered_env = struct type t = constructor - let compare (indx,ix) (indy,iy) = - let c = Int.compare ix iy in - if Int.equal c 0 then InductiveOrdered_env.compare indx indy else c + let compare = constructor_user_ord end module Constrmap = Map.Make(ConstructorOrdered) @@ -509,19 +581,6 @@ module Hkn = Hashcons.Make( let hash = Hashtbl.hash end) -(** For [constant] and [mutual_inductive], we discriminate only on - the user part : having the same user part implies having the - same canonical part (invariant of the system). *) - -module Hcn = Hashcons.Make( - struct - type t = kernel_name*kernel_name - type u = kernel_name -> kernel_name - let hashcons hkn (user,can) = (hkn user, hkn can) - let equal (user1,_) (user2,_) = user1 == user2 - let hash (user,_) = Hashtbl.hash user - end) - module Hind = Hashcons.Make( struct type t = inductive @@ -543,8 +602,8 @@ module Hconstruct = Hashcons.Make( let hcons_mp = Hashcons.simple_hcons Hmod.generate (Dir_path.hcons,MBId.hcons,String.hcons) let hcons_kn = Hashcons.simple_hcons Hkn.generate (hcons_mp,Dir_path.hcons,String.hcons) -let hcons_con = Hashcons.simple_hcons Hcn.generate hcons_kn -let hcons_mind = Hashcons.simple_hcons Hcn.generate hcons_kn +let hcons_con = Hashcons.simple_hcons KernelPair.HashKP.generate hcons_kn +let hcons_mind = Hashcons.simple_hcons KernelPair.HashKP.generate hcons_kn let hcons_ind = Hashcons.simple_hcons Hind.generate hcons_mind let hcons_construct = Hashcons.simple_hcons Hconstruct.generate hcons_ind @@ -573,17 +632,13 @@ type id_key = inv_rel_key tableKey let eq_id_key ik1 ik2 = if ik1 == ik2 then true else match ik1,ik2 with - | ConstKey (u1, kn1), ConstKey (u2, kn2) -> - let ans = Int.equal (kn_ord u1 u2) 0 in - if ans then Int.equal (kn_ord kn1 kn2) 0 - else ans - | VarKey id1, VarKey id2 -> - Int.equal (Id.compare id1 id2) 0 + | ConstKey cst1, ConstKey cst2 -> kn_equal (user_con cst1) (user_con cst2) + | VarKey id1, VarKey id2 -> Id.equal id1 id2 | RelKey k1, RelKey k2 -> Int.equal k1 k2 | _ -> false -let eq_con_chk (kn1,_) (kn2,_) = Int.equal (kn_ord kn1 kn2) 0 -let eq_mind_chk (kn1,_) (kn2,_) = Int.equal (kn_ord kn1 kn2) 0 +let eq_con_chk cst1 cst2 = kn_equal (user_con cst1) (user_con cst2) +let eq_mind_chk mind1 mind2 = kn_equal (user_mind mind1) (user_mind mind2) let eq_ind_chk (kn1,i1) (kn2,i2) = Int.equal i1 i2 && eq_mind_chk kn1 kn2 (** Compatibility layers *) diff --git a/kernel/names.mli b/kernel/names.mli index a51ac0ad8..f704b91ba 100644 --- a/kernel/names.mli +++ b/kernel/names.mli @@ -210,6 +210,7 @@ val string_of_kn : kernel_name -> string val pr_kn : kernel_name -> Pp.std_ppcmds val kn_ord : kernel_name -> kernel_name -> int +val kn_equal : kernel_name -> kernel_name -> bool module KNset : Set.S with type elt = kernel_name module KNpred : Predicate.S with type elt = kernel_name @@ -251,6 +252,8 @@ val user_con : constant -> kernel_name val canonical_con : constant -> kernel_name val repr_con : constant -> module_path * Dir_path.t * Label.t val eq_constant : constant -> constant -> bool +val con_ord : constant -> constant -> int +val con_user_ord : constant -> constant -> int val con_with_label : constant -> Label.t -> constant val string_of_con : constant -> string @@ -271,6 +274,8 @@ val user_mind : mutual_inductive -> kernel_name val canonical_mind : mutual_inductive -> kernel_name val repr_mind : mutual_inductive -> module_path * Dir_path.t * Label.t val eq_mind : mutual_inductive -> mutual_inductive -> bool +val mind_ord : mutual_inductive -> mutual_inductive -> int +val mind_user_ord : mutual_inductive -> mutual_inductive -> int val string_of_mind : mutual_inductive -> string val mind_label : mutual_inductive -> Label.t @@ -289,7 +294,11 @@ val ith_constructor_of_inductive : inductive -> int -> constructor val inductive_of_constructor : constructor -> inductive val index_of_constructor : constructor -> int val eq_ind : inductive -> inductive -> bool +val ind_ord : inductive -> inductive -> int +val ind_user_ord : inductive -> inductive -> int val eq_constructor : constructor -> constructor -> bool +val constructor_ord : constructor -> constructor -> int +val constructor_user_ord : constructor -> constructor -> int (** Better to have it here that in Closure, since required in grammar.cma *) type evaluable_global_reference = diff --git a/kernel/term.ml b/kernel/term.ml index 93e870015..de7bdbb88 100644 --- a/kernel/term.ml +++ b/kernel/term.ml @@ -638,16 +638,9 @@ let constr_ord_int f t1 t2 = | App (c1,l1), App (c2,l2) -> (f =? (Array.compare f)) c1 c2 l1 l2 | Evar (e1,l1), Evar (e2,l2) -> ((-) =? (Array.compare f)) e1 e2 l1 l2 - | Const c1, Const c2 -> kn_ord (canonical_con c1) (canonical_con c2) - | Ind (spx, ix), Ind (spy, iy) -> - let c = Int.compare ix iy in - if Int.equal c 0 then kn_ord (canonical_mind spx) (canonical_mind spy) else c - | Construct ((spx, ix), jx), Construct ((spy, iy), jy) -> - let c = Int.compare jx jy in - if Int.equal c 0 then - (let c = Int.compare ix iy in - if Int.equal c 0 then kn_ord (canonical_mind spx) (canonical_mind spy) else c) - else c + | Const c1, Const c2 -> con_ord c1 c2 + | Ind ind1, Ind ind2 -> ind_ord ind1 ind2 + | Construct ct1, Construct ct2 -> constructor_ord ct1 ct2 | Case (_,p1,c1,bl1), Case (_,p2,c2,bl2) -> ((f =? f) ==? (Array.compare f)) p1 p2 c1 c2 bl1 bl2 | Fix (ln1,(_,tl1,bl1)), Fix (ln2,(_,tl2,bl2)) -> diff --git a/library/assumptions.ml b/library/assumptions.ml index cb0c99e5a..ee916c237 100644 --- a/library/assumptions.ml +++ b/library/assumptions.ml @@ -22,8 +22,6 @@ open Term open Declarations open Mod_subst -let cst_ord k1 k2 = kn_ord (canonical_con k1) (canonical_con k2) - type context_object = | Variable of Id.t (* A section variable or a Let definition *) | Axiom of constant (* An axiom or a constant. *) @@ -37,9 +35,9 @@ struct let compare x y = match x , y with | Variable i1 , Variable i2 -> Id.compare i1 i2 - | Axiom k1 , Axiom k2 -> cst_ord k1 k2 - | Opaque k1 , Opaque k2 -> cst_ord k1 k2 - | Transparent k1 , Transparent k2 -> cst_ord k1 k2 + | Axiom k1 , Axiom k2 -> con_ord k1 k2 + | Opaque k1 , Opaque k2 -> con_ord k1 k2 + | Transparent k1 , Transparent k2 -> con_ord k1 k2 | Axiom _ , Variable _ -> 1 | Opaque _ , Variable _ | Opaque _ , Axiom _ -> 1 diff --git a/library/globnames.ml b/library/globnames.ml index e63fa64d5..0ee82f0f7 100644 --- a/library/globnames.ml +++ b/library/globnames.ml @@ -76,22 +76,17 @@ let constr_of_global = function let constr_of_reference = constr_of_global let reference_of_constr = global_of_constr -let global_ord_gen fc fmi x y = - let ind_ord (indx,ix) (indy,iy) = - let c = Int.compare ix iy in - if Int.equal c 0 then kn_ord (fmi indx) (fmi indy) else c - in - match x, y with - | ConstRef cx, ConstRef cy -> kn_ord (fc cx) (fc cy) - | IndRef indx, IndRef indy -> ind_ord indx indy - | ConstructRef (indx,jx), ConstructRef (indy,jy) -> - let c = Int.compare jx jy in - if Int.equal c 0 then ind_ord indx indy else c - | VarRef v1, VarRef v2 -> Id.compare v1 v2 - | _, _ -> Pervasives.compare x y - -let global_ord_can = global_ord_gen canonical_con canonical_mind -let global_ord_user = global_ord_gen user_con user_mind +let global_ord_gen ord_cst ord_ind ord_cons x y = match x, y with + | ConstRef cx, ConstRef cy -> ord_cst cx cy + | IndRef indx, IndRef indy -> ord_ind indx indy + | ConstructRef consx, ConstructRef consy -> ord_cons consx consy + | VarRef v1, VarRef v2 -> Id.compare v1 v2 + | _, _ -> Pervasives.compare x y + +let global_ord_can = + global_ord_gen con_ord ind_ord constructor_ord +let global_ord_user = + global_ord_gen con_user_ord ind_user_ord constructor_user_ord (* By default, [global_reference] are ordered on their canonical part *) @@ -166,7 +161,9 @@ let decode_con kn = | MPfile dir -> (dir,Label.to_id l) | _ -> anomaly (Pp.str "MPfile expected!") -(* popping one level of section in global names *) +(** Popping one level of section in global names. + These functions are meant to be used during discharge: + user and canonical kernel names must be equal. *) let pop_con con = let (mp,dir,l) = repr_con con in diff --git a/library/lib.ml b/library/lib.ml index 191b00ea9..53ffce1d7 100644 --- a/library/lib.ml +++ b/library/lib.ml @@ -190,7 +190,7 @@ let split_lib_gen test = | Some r -> r let eq_object_name (fp1, kn1) (fp2, kn2) = - eq_full_path fp1 fp2 && Int.equal (Names.kn_ord kn1 kn2) 0 + eq_full_path fp1 fp2 && Names.kn_equal kn1 kn2 let split_lib sp = let is_sp (nsp, _) = eq_object_name sp nsp in diff --git a/library/nametab.ml b/library/nametab.ml index 9e0e38745..0d326a49c 100644 --- a/library/nametab.ml +++ b/library/nametab.ml @@ -284,7 +284,7 @@ end module KnEqual = struct type t = kernel_name - let equal kn1 kn2 = Int.equal (kn_ord kn1 kn2) 0 + let equal = Names.kn_equal end module MPEqual = diff --git a/toplevel/search.ml b/toplevel/search.ml index afc961596..30e7dca8b 100644 --- a/toplevel/search.ml +++ b/toplevel/search.ml @@ -128,9 +128,8 @@ let filter_by_module (module_list:Dir_path.t list) (accept:bool) in xor accept (filter_aux module_list) -let ref_eq = Globnames.encode_mind Coqlib.logic_module (Id.of_string "eq"), 0 -let c_eq = mkInd ref_eq -let gref_eq = IndRef ref_eq +let gref_eq = Coqlib.glob_eq +let c_eq = mkInd (Globnames.destIndRef gref_eq) let mk_rewrite_pattern1 eq pattern = PApp (PRef eq, [| PMeta None; pattern; PMeta None |]) -- cgit v1.2.3