diff options
Diffstat (limited to 'kernel/constr.ml')
| -rw-r--r-- | kernel/constr.ml | 95 |
1 files changed, 45 insertions, 50 deletions
diff --git a/kernel/constr.ml b/kernel/constr.ml index 49f74841..e823c01b 100644 --- a/kernel/constr.ml +++ b/kernel/constr.ml @@ -464,55 +464,22 @@ 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_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, +(* [compare_head_gen_evar k1 k2 u s e eq leq c1 c2] compare [c1] and + [c2] (using [k1] to expose the structure of [c1] and [k2] to expose + the structure [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 *) + not taken into account. Note that as [kind1] and [kind2] are + potentially different, we cannot use, in recursive case, the + optimisation that physically equal arrays are equals (hence the + calls to {!Array.equal_norefl}). *) -let compare_head_gen eq_universes eq_sorts f t1 t2 = - match kind t1, kind t2 with +let compare_head_gen_with kind1 kind2 eq_universes leq_sorts eq leq t1 t2 = + match kind1 t1, kind2 t2 with | Rel n1, Rel n2 -> Int.equal n1 n2 | Meta m1, Meta m2 -> Int.equal m1 m2 | Var id1, Var id2 -> Id.equal id1 id2 - | Sort s1, Sort s2 -> eq_sorts s1 s2 - | Cast (c1,_,_), _ -> f c1 t2 - | _, Cast (c2,_,_) -> f t1 c2 - | Prod (_,t1,c1), Prod (_,t2,c2) -> f t1 t2 && f c1 c2 - | Lambda (_,t1,c1), Lambda (_,t2,c2) -> f t1 t2 && f c1 c2 - | LetIn (_,b1,t1,c1), LetIn (_,b2,t2,c2) -> f b1 b2 && f t1 t2 && f c1 c2 - | App (Cast(c1, _, _),l1), _ -> f (mkApp (c1,l1)) t2 - | _, App (Cast (c2, _, _),l2) -> f t1 (mkApp (c2,l2)) - | App (c1,l1), App (c2,l2) -> - 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 - | Proj (p1,c1), Proj (p2,c2) -> Projection.equal 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)) -> - Int.equal i1 i2 && Array.equal Int.equal ln1 ln2 - && Array.equal f tl1 tl2 && Array.equal f bl1 bl2 - | CoFix(ln1,(_,tl1,bl1)), CoFix(ln2,(_,tl2,bl2)) -> - Int.equal ln1 ln2 && Array.equal f tl1 tl2 && Array.equal f bl1 bl2 - | _ -> false - -let compare_head = compare_head_gen (fun _ -> Univ.Instance.equal) 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 @@ -522,8 +489,8 @@ let compare_head_gen_leq eq_universes eq_sorts leq_sorts eq leq t1 t2 = | 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 + Int.equal (Array.length l1) (Array.length l2) && + eq c1 c2 && Array.equal_norefl eq l1 l2 | Proj (p1,c1), Proj (p2,c2) -> Projection.equal 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 @@ -533,11 +500,31 @@ let compare_head_gen_leq eq_universes eq_sorts leq_sorts eq leq t1 t2 = 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 + && Array.equal_norefl eq tl1 tl2 && Array.equal_norefl 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 + Int.equal ln1 ln2 && Array.equal_norefl eq tl1 tl2 && Array.equal_norefl eq bl1 bl2 | _ -> false +(* [compare_head_gen_leq u s 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 leq_sorts eq leq t1 t2 = + compare_head_gen_with kind kind eq_universes leq_sorts eq leq t1 t2 + +(* [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_gen eq_universes eq_sorts eq t1 t2 = + compare_head_gen_leq eq_universes eq_sorts eq eq t1 t2 + +let compare_head = compare_head_gen (fun _ -> Univ.Instance.equal) Sorts.equal + (*******************************) (* alpha conversion functions *) (*******************************) @@ -549,6 +536,14 @@ let rec eq_constr m n = let equal m n = eq_constr m n (* to avoid tracing a recursive fun *) +let rec equal_with kind1 kind2 m n = + (* note that pointer equality is not sufficient to ensure equality + up to [eq_evars], because we may evaluates evars of [m] and [n] + in different evar contexts. *) + let req_constr m n = equal_with kind1 kind2 m n in + compare_head_gen_with kind1 kind2 + (fun _ -> Instance.equal) Sorts.equal req_constr req_constr m n + let eq_constr_univs univs m n = if m == n then true else @@ -570,7 +565,7 @@ let leq_constr_univs univs 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 + compare_head_gen_leq eq_universes leq_sorts eq_constr' leq_constr' m n and leq_constr' m n = m == n || compare_leq m n in compare_leq m n @@ -620,7 +615,7 @@ let leq_constr_univs_infer univs 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 + compare_head_gen_leq eq_universes 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 |