diff options
Diffstat (limited to 'kernel/constr.ml')
| -rw-r--r-- | kernel/constr.ml | 238 |
1 files changed, 204 insertions, 34 deletions
diff --git a/kernel/constr.ml b/kernel/constr.ml index e9e21d30d9..89c138a085 100644 --- a/kernel/constr.ml +++ b/kernel/constr.ml @@ -25,7 +25,7 @@ open Util open Names - +open Univ type existential_key = Evar.t type metavariable = int @@ -61,6 +61,10 @@ type ('constr, 'types) pfixpoint = (int array * int) * ('constr, 'types) prec_declaration type ('constr, 'types) pcofixpoint = int * ('constr, 'types) prec_declaration +type 'a puniverses = 'a Univ.puniverses +type pconstant = constant puniverses +type pinductive = inductive puniverses +type pconstructor = constructor puniverses (* [Var] is used for named variables and [Rel] for variables as de Bruijn indices. *) @@ -75,13 +79,13 @@ type ('constr, 'types) kind_of_term = | Lambda of Name.t * 'types * 'constr | LetIn of Name.t * 'constr * 'types * 'constr | App of 'constr * 'constr array - | Const of constant - | Ind of inductive - | Construct of constructor + | Const of pconstant + | Ind of pinductive + | Construct of pconstructor | Case of case_info * 'constr * 'constr * 'constr array | Fix of ('constr, 'types) pfixpoint | CoFix of ('constr, 'types) pcofixpoint - + | Proj of constant * 'constr (* constr is the fixpoint of the previous type. Requires option -rectypes of the Caml compiler to be set *) type t = (t,t) kind_of_term @@ -139,19 +143,29 @@ let mkApp (f, a) = | App (g, cl) -> App (g, Array.append cl a) | _ -> App (f, a) +let out_punivs (a, _) = a +let map_puniverses f (x,u) = (f x, u) +let in_punivs a = (a, Univ.Instance.empty) + (* Constructs a constant *) -let mkConst c = Const c +let mkConst c = Const (in_punivs c) +let mkConstU c = Const c + +(* Constructs an applied projection *) +let mkProj (p,c) = Proj (p,c) (* Constructs an existential variable *) let mkEvar e = Evar e (* Constructs the ith (co)inductive type of the block named kn *) -let mkInd m = Ind m +let mkInd m = Ind (in_punivs m) +let mkIndU m = Ind m (* Constructs the jth constructor of the ith (co)inductive type of the - block named kn. The array of terms correspond to the variables - introduced in the section *) -let mkConstruct c = Construct c + block named kn. *) +let mkConstruct c = Construct (in_punivs c) +let mkConstructU c = Construct c +let mkConstructUi ((ind,u),i) = Construct ((ind,i),u) (* Constructs the term <p>Case c of c1 | c2 .. | cn end *) let mkCase (ci, p, c, ac) = Case (ci, p, c, ac) @@ -225,6 +239,7 @@ let fold f acc c = match kind c with | Lambda (_,t,c) -> f (f acc t) c | LetIn (_,b,t,c) -> f (f (f acc b) t) c | App (c,l) -> Array.fold_left f (f acc c) l + | Proj (p,c) -> f acc c | Evar (_,l) -> Array.fold_left f acc l | Case (_,p,c,bl) -> Array.fold_left f (f (f acc p) c) bl | Fix (_,(lna,tl,bl)) -> @@ -244,6 +259,7 @@ let iter f c = match kind c with | Lambda (_,t,c) -> f t; f c | LetIn (_,b,t,c) -> f b; f t; f c | App (c,l) -> f c; Array.iter f l + | Proj (p,c) -> f c | Evar (_,l) -> Array.iter f l | Case (_,p,c,bl) -> f p; f c; Array.iter f bl | Fix (_,(_,tl,bl)) -> Array.iter f tl; Array.iter f bl @@ -265,6 +281,7 @@ let iter_with_binders g f n c = match kind c with | App (c,l) -> f n c; CArray.Fun1.iter f n l | Evar (_,l) -> CArray.Fun1.iter f n l | Case (_,p,c,bl) -> f n p; f n c; CArray.Fun1.iter f n bl + | Proj (p,c) -> f n c | Fix (_,(_,tl,bl)) -> CArray.Fun1.iter f n tl; CArray.Fun1.iter f (iterate g (Array.length tl) n) bl @@ -305,6 +322,10 @@ let map f c = match kind c with let l' = Array.smartmap f l in if b'==b && l'==l then c else mkApp (b', l') + | Proj (p,t) -> + let t' = f t in + if t' == t then c + else mkProj (p, t') | Evar (e,l) -> let l' = Array.smartmap f l in if l'==l then c @@ -413,6 +434,10 @@ let map_with_binders g f l c0 = match kind c0 with let al' = CArray.Fun1.smartmap f l al in if c' == c && al' == al then c0 else mkApp (c', al') + | Proj (p, t) -> + let t' = f l t in + if t' == t then c0 + else mkProj (p, t') | Evar (e, al) -> let al' = CArray.Fun1.smartmap f l al in if al' == al then c0 @@ -435,13 +460,13 @@ let map_with_binders g f l c0 = match kind c0 with let bl' = CArray.Fun1.smartmap f l' bl in mkCoFix (ln,(lna,tl',bl')) -(* [compare f c1 c2] compare [c1] and [c2] using [f] to compare - the immediate subterms of [c1] of [c2] if needed; Cast's, +(* [compare_head_gen u s f c1 c2] compare [c1] and [c2] using [f] to compare + the immediate subterms of [c1] of [c2] if needed, [u] to compare universe + instances and [s] to compare sorts; Cast's, application associativity, binders name and Cases annotations are not taken into account *) - -let compare_head f t1 t2 = +let compare_head_gen eq_universes eq_sorts f t1 t2 = match kind t1, kind t2 with | Rel n1, Rel n2 -> Int.equal n1 n2 | Meta m1, Meta m2 -> Int.equal m1 m2 @@ -458,9 +483,10 @@ let compare_head f t1 t2 = Int.equal (Array.length l1) (Array.length l2) && f c1 c2 && Array.equal f l1 l2 | Evar (e1,l1), Evar (e2,l2) -> Evar.equal e1 e2 && Array.equal f l1 l2 - | Const c1, Const c2 -> eq_constant c1 c2 - | Ind c1, Ind c2 -> eq_ind c1 c2 - | Construct c1, Construct c2 -> eq_constructor c1 c2 + | Proj (p1,c1), Proj (p2,c2) -> eq_constant p1 p2 && f c1 c2 + | Const (c1,u1), Const (c2,u2) -> eq_constant c1 c2 && eq_universes true u1 u2 + | Ind (c1,u1), Ind (c2,u2) -> eq_ind c1 c2 && eq_universes false u1 u2 + | Construct (c1,u1), Construct (c2,u2) -> eq_constructor c1 c2 && eq_universes false u1 u2 | Case (_,p1,c1,bl1), Case (_,p2,c2,bl2) -> f p1 p2 && f c1 c2 && Array.equal f bl1 bl2 | Fix ((ln1, i1),(_,tl1,bl1)), Fix ((ln2, i2),(_,tl2,bl2)) -> @@ -470,6 +496,44 @@ let compare_head f t1 t2 = Int.equal ln1 ln2 && Array.equal f tl1 tl2 && Array.equal f bl1 bl2 | _ -> false +let compare_head = compare_head_gen (fun _ -> Univ.Instance.eq) Sorts.equal + +(* [compare_head_gen_leq u s sl eq leq c1 c2] compare [c1] and [c2] using [eq] to compare + the immediate subterms of [c1] of [c2] for conversion if needed, [leq] for cumulativity, + [u] to compare universe instances and [s] to compare sorts; Cast's, + application associativity, binders name and Cases annotations are + not taken into account *) + +let compare_head_gen_leq eq_universes eq_sorts leq_sorts eq leq t1 t2 = + match kind t1, kind t2 with + | Rel n1, Rel n2 -> Int.equal n1 n2 + | Meta m1, Meta m2 -> Int.equal m1 m2 + | Var id1, Var id2 -> Int.equal (id_ord id1 id2) 0 + | Sort s1, Sort s2 -> leq_sorts s1 s2 + | Cast (c1,_,_), _ -> leq c1 t2 + | _, Cast (c2,_,_) -> leq t1 c2 + | Prod (_,t1,c1), Prod (_,t2,c2) -> eq t1 t2 && leq c1 c2 + | Lambda (_,t1,c1), Lambda (_,t2,c2) -> eq t1 t2 && eq c1 c2 + | LetIn (_,b1,t1,c1), LetIn (_,b2,t2,c2) -> eq b1 b2 && eq t1 t2 && leq c1 c2 + | App (Cast(c1, _, _),l1), _ -> leq (mkApp (c1,l1)) t2 + | _, App (Cast (c2, _, _),l2) -> leq t1 (mkApp (c2,l2)) + | App (c1,l1), App (c2,l2) -> + Int.equal (Array.length l1) (Array.length l2) && + eq c1 c2 && Array.equal eq l1 l2 + | Proj (p1,c1), Proj (p2,c2) -> eq_constant p1 p2 && eq c1 c2 + | Evar (e1,l1), Evar (e2,l2) -> Evar.equal e1 e2 && Array.equal eq l1 l2 + | Const (c1,u1), Const (c2,u2) -> eq_constant c1 c2 && eq_universes true u1 u2 + | Ind (c1,u1), Ind (c2,u2) -> eq_ind c1 c2 && eq_universes false u1 u2 + | Construct (c1,u1), Construct (c2,u2) -> eq_constructor c1 c2 && eq_universes false u1 u2 + | Case (_,p1,c1,bl1), Case (_,p2,c2,bl2) -> + eq p1 p2 && eq c1 c2 && Array.equal eq bl1 bl2 + | Fix ((ln1, i1),(_,tl1,bl1)), Fix ((ln2, i2),(_,tl2,bl2)) -> + Int.equal i1 i2 && Array.equal Int.equal ln1 ln2 + && Array.equal eq tl1 tl2 && Array.equal eq bl1 bl2 + | CoFix(ln1,(_,tl1,bl1)), CoFix(ln2,(_,tl2,bl2)) -> + Int.equal ln1 ln2 && Array.equal eq tl1 tl2 && Array.equal eq bl1 bl2 + | _ -> false + (*******************************) (* alpha conversion functions *) (*******************************) @@ -477,10 +541,81 @@ let compare_head f t1 t2 = (* alpha conversion : ignore print names and casts *) let rec eq_constr m n = - (m == n) || compare_head eq_constr m n + (m == n) || compare_head_gen (fun _ -> Univ.Instance.eq) Sorts.equal eq_constr m n + +(** Strict equality of universe instances. *) +let compare_constr = compare_head_gen (fun _ -> Univ.Instance.eq) Sorts.equal let equal m n = eq_constr m n (* to avoid tracing a recursive fun *) +let eq_constr_univs univs m n = + if m == n then true + else + let eq_universes _ = Univ.Instance.check_eq univs in + let eq_sorts s1 s2 = Univ.check_eq univs (Sorts.univ_of_sort s1) (Sorts.univ_of_sort s2) in + let rec eq_constr' m n = + m == n || compare_head_gen eq_universes eq_sorts eq_constr' m n + in compare_head_gen eq_universes eq_sorts eq_constr' m n + +let leq_constr_univs univs m n = + if m == n then true + else + let eq_universes _ = Univ.Instance.check_eq univs in + let eq_sorts s1 s2 = Univ.check_eq univs (Sorts.univ_of_sort s1) (Sorts.univ_of_sort s2) in + let leq_sorts s1 s2 = Univ.check_leq univs (Sorts.univ_of_sort s1) (Sorts.univ_of_sort s2) in + let rec eq_constr' m n = + m == n || compare_head_gen eq_universes eq_sorts eq_constr' m n + in + let rec compare_leq m n = + compare_head_gen_leq eq_universes eq_sorts leq_sorts eq_constr' leq_constr' m n + and leq_constr' m n = m == n || compare_leq m n in + compare_leq m n + +let eq_constr_universes m n = + if m == n then true, UniverseConstraints.empty + else + let cstrs = ref UniverseConstraints.empty in + let eq_universes strict l l' = + cstrs := Univ.enforce_eq_instances_univs strict l l' !cstrs; true in + let eq_sorts s1 s2 = + cstrs := Univ.UniverseConstraints.add + (Sorts.univ_of_sort s1, Univ.UEq, Sorts.univ_of_sort s2) !cstrs; + true + in + let rec eq_constr' m n = + m == n || compare_head_gen eq_universes eq_sorts eq_constr' m n + in + let res = compare_head_gen eq_universes eq_sorts eq_constr' m n in + res, !cstrs + +let leq_constr_universes m n = + if m == n then true, UniverseConstraints.empty + else + let cstrs = ref UniverseConstraints.empty in + let eq_universes strict l l' = + cstrs := Univ.enforce_eq_instances_univs strict l l' !cstrs; true in + let eq_sorts s1 s2 = + cstrs := Univ.UniverseConstraints.add + (Sorts.univ_of_sort s1,Univ.UEq,Sorts.univ_of_sort s2) !cstrs; true + in + let leq_sorts s1 s2 = + cstrs := Univ.UniverseConstraints.add + (Sorts.univ_of_sort s1,Univ.ULe,Sorts.univ_of_sort s2) !cstrs; true + in + let rec eq_constr' m n = + m == n || compare_head_gen eq_universes eq_sorts eq_constr' m n + in + let rec compare_leq m n = + compare_head_gen_leq eq_universes eq_sorts leq_sorts eq_constr' leq_constr' m n + and leq_constr' m n = m == n || compare_leq m n in + let res = compare_leq m n in + res, !cstrs + +let always_true _ _ = true + +let rec eq_constr_nounivs m n = + (m == n) || compare_head_gen (fun _ -> always_true) always_true eq_constr_nounivs m n + (** We only use this function over blocks! *) let tag t = Obj.tag (Obj.repr t) @@ -509,11 +644,12 @@ let constr_ord_int f t1 t2 = | App (Cast(c1,_,_),l1), _ -> f (mkApp (c1,l1)) t2 | _, App (Cast(c2, _,_),l2) -> f t1 (mkApp (c2,l2)) | App (c1,l1), App (c2,l2) -> (f =? (Array.compare f)) c1 c2 l1 l2 + | Proj (p1,c1), Proj (p2,c2) -> (con_ord =? f) p1 p2 c1 c2 | Evar (e1,l1), Evar (e2,l2) -> (Evar.compare =? (Array.compare f)) e1 e2 l1 l2 - | Const c1, Const c2 -> con_ord c1 c2 - | Ind ind1, Ind ind2 -> ind_ord ind1 ind2 - | Construct ct1, Construct ct2 -> constructor_ord ct1 ct2 + | Const (c1,u1), Const (c2,u2) -> con_ord c1 c2 + | Ind (ind1, u1), Ind (ind2, u2) -> ind_ord ind1 ind2 + | Construct (ct1,u1), Construct (ct2,u2) -> 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)) -> @@ -587,12 +723,14 @@ let hasheq t1 t2 = | Lambda (n1,t1,c1), Lambda (n2,t2,c2) -> n1 == n2 && t1 == t2 && c1 == c2 | LetIn (n1,b1,t1,c1), LetIn (n2,b2,t2,c2) -> n1 == n2 && b1 == b2 && t1 == t2 && c1 == c2 + | Proj (c1,t1), Proj (c2,t2) -> c1 == c2 && t1 == t2 | App (c1,l1), App (c2,l2) -> c1 == c2 && array_eqeq l1 l2 | Evar (e1,l1), Evar (e2,l2) -> Evar.equal e1 e2 && array_eqeq l1 l2 - | Const c1, Const c2 -> c1 == c2 - | Ind (sp1,i1), Ind (sp2,i2) -> sp1 == sp2 && Int.equal i1 i2 - | Construct ((sp1,i1),j1), Construct ((sp2,i2),j2) -> - sp1 == sp2 && Int.equal i1 i2 && Int.equal j1 j2 + | Const (c1,u1), Const (c2,u2) -> c1 == c2 && Univ.Instance.eqeq u1 u2 + | Ind ((sp1,i1),u1), Ind ((sp2,i2),u2) -> + sp1 == sp2 && Int.equal i1 i2 && Univ.Instance.eqeq u1 u2 + | Construct (((sp1,i1),j1),u1), Construct (((sp2,i2),j2),u2) -> + sp1 == sp2 && Int.equal i1 i2 && Int.equal j1 j2 && Univ.Instance.eqeq u1 u2 | Case (ci1,p1,c1,bl1), Case (ci2,p2,c2,bl2) -> ci1 == ci2 && p1 == p2 && c1 == c2 && array_eqeq bl1 bl2 | Fix ((ln1, i1),(lna1,tl1,bl1)), Fix ((ln2, i2),(lna2,tl2,bl2)) -> @@ -631,6 +769,8 @@ let hash_cast_kind = function | DEFAULTcast -> 2 | REVERTcast -> 3 +let hash_instance = Univ.Instance.hcons + (* [hashcons hash_consing_functions constr] computes an hash-consed representation for [constr] using [hash_consing_functions] on leaves. *) @@ -665,12 +805,16 @@ let hashcons (sh_sort,sh_ci,sh_construct,sh_ind,sh_con,sh_na,sh_id) = | Evar (e,l) -> let l, hl = hash_term_array l in (Evar (e,l), combinesmall 8 (combine (Evar.hash e) hl)) - | Const c -> - (Const (sh_con c), combinesmall 9 (Constant.hash c)) - | Ind ind -> - (Ind (sh_ind ind), combinesmall 10 (ind_hash ind)) - | Construct c -> - (Construct (sh_construct c), combinesmall 11 (constructor_hash c)) + | Proj (p,c) -> + let c, hc = sh_rec c in + let p' = sh_con p in + (Proj (p', c), combinesmall 17 (Hashtbl.hash p')) (** FIXME *) + | Const (c,u) -> + (Const (sh_con c, hash_instance u), combinesmall 9 (Constant.hash c)) + | Ind (ind, u) -> + (Ind (sh_ind ind, hash_instance u), combinesmall 10 (ind_hash ind)) + | Construct (c, u) -> + (Construct (sh_construct c, hash_instance u), combinesmall 11 (constructor_hash c)) | Case (ci,p,c,bl) -> let p, hp = sh_rec p and c, hc = sh_rec c in @@ -742,13 +886,15 @@ let rec hash t = | App (Cast(c, _, _),l) -> hash (mkApp (c,l)) | App (c,l) -> combinesmall 7 (combine (hash_term_array l) (hash c)) + | Proj (p,c) -> + combinesmall 17 (combine (Hashtbl.hash p) (hash c)) | Evar (e,l) -> combinesmall 8 (combine (Evar.hash e) (hash_term_array l)) - | Const c -> + | Const (c, _) -> combinesmall 9 (Constant.hash c) - | Ind ind -> + | Ind (ind, _) -> combinesmall 10 (ind_hash ind) - | Construct c -> + | Construct (c, _) -> combinesmall 11 (constructor_hash c) | Case (_ , p, c, bl) -> combinesmall 12 (combine3 (hash c) (hash p) (hash_term_array bl)) @@ -799,8 +945,32 @@ module Hcaseinfo = Hashcons.Make(CaseinfoHash) let case_info_hash = CaseinfoHash.hash +module Hsorts = + Hashcons.Make( + struct + open Sorts + + type t = Sorts.t + type u = universe -> universe + let hashcons huniv = function + Prop c -> Prop c + | Type u -> Type (huniv u) + let equal s1 s2 = + s1 == s2 || + match (s1,s2) with + (Prop c1, Prop c2) -> c1 == c2 + | (Type u1, Type u2) -> u1 == u2 + |_ -> false + let hash = Hashtbl.hash + end) + +let hcons_sorts = Hashcons.simple_hcons Hsorts.generate hcons_univ let hcons_caseinfo = Hashcons.simple_hcons Hcaseinfo.generate hcons_ind +let hcons_pconstruct (c,u) = (hcons_construct c, Univ.Instance.hcons u) +let hcons_pind (i,u) = (hcons_ind i, Univ.Instance.hcons u) +let hcons_pcon (c,u) = (hcons_con c, Univ.Instance.hcons u) + let hcons = hashcons (Sorts.hcons, |