diff options
author | Benjamin Barenblat <bbaren@debian.org> | 2018-12-29 14:31:27 -0500 |
---|---|---|
committer | Benjamin Barenblat <bbaren@debian.org> | 2018-12-29 14:31:27 -0500 |
commit | 9043add656177eeac1491a73d2f3ab92bec0013c (patch) | |
tree | 2b0092c84bfbf718eca10c81f60b2640dc8cab05 /kernel/constr.ml | |
parent | a4c7f8bd98be2a200489325ff7c5061cf80ab4f3 (diff) |
Imported Upstream version 8.8.2upstream/8.8.2
Diffstat (limited to 'kernel/constr.ml')
-rw-r--r-- | kernel/constr.ml | 423 |
1 files changed, 314 insertions, 109 deletions
diff --git a/kernel/constr.ml b/kernel/constr.ml index ce20751a..de4e7c18 100644 --- a/kernel/constr.ml +++ b/kernel/constr.ml @@ -1,9 +1,11 @@ (************************************************************************) -(* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016 *) +(* * The Coq Proof Assistant / The Coq Development Team *) +(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *) +(* <O___,, * (see CREDITS file for the list of authors) *) (* \VV/ **************************************************************) -(* // * This file is distributed under the terms of the *) -(* * GNU Lesser General Public License Version 2.1 *) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(* * (see LICENSE file for the text of the license) *) (************************************************************************) (* File initially created by GĂ©rard Huet and Thierry Coquand in 1984 *) @@ -75,39 +77,48 @@ type ('constr, 'types) pfixpoint = type ('constr, 'types) pcofixpoint = int * ('constr, 'types) prec_declaration type 'a puniverses = 'a Univ.puniverses -type pconstant = constant puniverses +type pconstant = Constant.t puniverses type pinductive = inductive puniverses type pconstructor = constructor puniverses (* [Var] is used for named variables and [Rel] for variables as de Bruijn indices. *) -type ('constr, 'types) kind_of_term = +type ('constr, 'types, 'sort, 'univs) kind_of_term = | Rel of int | Var of Id.t | Meta of metavariable | Evar of 'constr pexistential - | Sort of Sorts.t + | Sort of 'sort | Cast of 'constr * cast_kind * 'types | Prod of Name.t * 'types * 'types | Lambda of Name.t * 'types * 'constr | LetIn of Name.t * 'constr * 'types * 'constr | App of 'constr * 'constr array - | Const of pconstant - | Ind of pinductive - | Construct of pconstructor + | Const of (Constant.t * 'univs) + | Ind of (inductive * 'univs) + | Construct of (constructor * 'univs) | Case of case_info * 'constr * 'constr * 'constr array | Fix of ('constr, 'types) pfixpoint | CoFix of ('constr, 'types) pcofixpoint - | Proj of projection * 'constr + | Proj of Projection.t * '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 +type t = (t, t, Sorts.t, Instance.t) kind_of_term type constr = t type existential = existential_key * constr array type rec_declaration = Name.t array * constr array * constr array type fixpoint = (int array * int) * rec_declaration + (* The array of [int]'s tells for each component of the array of + mutual fixpoints the number of lambdas to skip before finding the + recursive argument (e.g., value is 2 in "fix f (x:A) (y:=t) (z:B) + (v:=u) (w:I) {struct w}"), telling to skip x and z and that w is + the recursive argument); + The second component [int] tells which component of the block is + returned *) type cofixpoint = int * rec_declaration + (* The component [int] tells which component of the block of + cofixpoint is returned *) type types = constr @@ -115,7 +126,7 @@ type types = constr (* Term constructors *) (*********************) -(* Constructs a DeBrujin index with number n *) +(* Constructs a de Bruijn index with number n *) let rels = [|Rel 1;Rel 2;Rel 3;Rel 4;Rel 5;Rel 6;Rel 7; Rel 8; Rel 9;Rel 10;Rel 11;Rel 12;Rel 13;Rel 14;Rel 15; Rel 16|] @@ -224,7 +235,6 @@ let mkMeta n = Meta n (* Constructs a Variable named id *) let mkVar id = Var id - (************************************************************************) (* kind_of_term = constructions as seen by the user *) (************************************************************************) @@ -235,6 +245,174 @@ let mkVar id = Var id let kind c = c +(* The other way around. We treat specifically smart constructors *) +let of_kind = function +| App (f, a) -> mkApp (f, a) +| Cast (c, knd, t) -> mkCast (c, knd, t) +| k -> k + +(**********************************************************************) +(* Non primitive term destructors *) +(**********************************************************************) + +(* Destructor operations : partial functions + Raise [DestKO] if the const has not the expected form *) + +exception DestKO + +let isMeta c = match kind c with Meta _ -> true | _ -> false + +(* Destructs a type *) +let isSort c = match kind c with + | Sort _ -> true + | _ -> false + +let rec isprop c = match kind c with + | Sort (Sorts.Prop _) -> true + | Cast (c,_,_) -> isprop c + | _ -> false + +let rec is_Prop c = match kind c with + | Sort (Sorts.Prop Sorts.Null) -> true + | Cast (c,_,_) -> is_Prop c + | _ -> false + +let rec is_Set c = match kind c with + | Sort (Sorts.Prop Sorts.Pos) -> true + | Cast (c,_,_) -> is_Set c + | _ -> false + +let rec is_Type c = match kind c with + | Sort (Sorts.Type _) -> true + | Cast (c,_,_) -> is_Type c + | _ -> false + +let is_small = Sorts.is_small +let iskind c = isprop c || is_Type c + +(* Tests if an evar *) +let isEvar c = match kind c with Evar _ -> true | _ -> false +let isEvar_or_Meta c = match kind c with + | Evar _ | Meta _ -> true + | _ -> false + +let isCast c = match kind c with Cast _ -> true | _ -> false +(* Tests if a de Bruijn index *) +let isRel c = match kind c with Rel _ -> true | _ -> false +let isRelN n c = + match kind c with Rel n' -> Int.equal n n' | _ -> false +(* Tests if a variable *) +let isVar c = match kind c with Var _ -> true | _ -> false +let isVarId id c = match kind c with Var id' -> Id.equal id id' | _ -> false +(* Tests if an inductive *) +let isInd c = match kind c with Ind _ -> true | _ -> false +let isProd c = match kind c with | Prod _ -> true | _ -> false +let isLambda c = match kind c with | Lambda _ -> true | _ -> false +let isLetIn c = match kind c with LetIn _ -> true | _ -> false +let isApp c = match kind c with App _ -> true | _ -> false +let isConst c = match kind c with Const _ -> true | _ -> false +let isConstruct c = match kind c with Construct _ -> true | _ -> false +let isCase c = match kind c with Case _ -> true | _ -> false +let isProj c = match kind c with Proj _ -> true | _ -> false +let isFix c = match kind c with Fix _ -> true | _ -> false +let isCoFix c = match kind c with CoFix _ -> true | _ -> false + +(* Destructs a de Bruijn index *) +let destRel c = match kind c with + | Rel n -> n + | _ -> raise DestKO + +(* Destructs an existential variable *) +let destMeta c = match kind c with + | Meta n -> n + | _ -> raise DestKO + +(* Destructs a variable *) +let destVar c = match kind c with + | Var id -> id + | _ -> raise DestKO + +let destSort c = match kind c with + | Sort s -> s + | _ -> raise DestKO + +(* Destructs a casted term *) +let destCast c = match kind c with + | Cast (t1,k,t2) -> (t1,k,t2) + | _ -> raise DestKO + +(* Destructs the product (x:t1)t2 *) +let destProd c = match kind c with + | Prod (x,t1,t2) -> (x,t1,t2) + | _ -> raise DestKO + +(* Destructs the abstraction [x:t1]t2 *) +let destLambda c = match kind c with + | Lambda (x,t1,t2) -> (x,t1,t2) + | _ -> raise DestKO + +(* Destructs the let [x:=b:t1]t2 *) +let destLetIn c = match kind c with + | LetIn (x,b,t1,t2) -> (x,b,t1,t2) + | _ -> raise DestKO + +(* Destructs an application *) +let destApp c = match kind c with + | App (f,a) -> (f, a) + | _ -> raise DestKO + +(* Destructs a constant *) +let destConst c = match kind c with + | Const kn -> kn + | _ -> raise DestKO + +(* Destructs an existential variable *) +let destEvar c = match kind c with + | Evar (kn, a as r) -> r + | _ -> raise DestKO + +(* Destructs a (co)inductive type named kn *) +let destInd c = match kind c with + | Ind (kn, a as r) -> r + | _ -> raise DestKO + +(* Destructs a constructor *) +let destConstruct c = match kind c with + | Construct (kn, a as r) -> r + | _ -> raise DestKO + +(* Destructs a term <p>Case c of lc1 | lc2 .. | lcn end *) +let destCase c = match kind c with + | Case (ci,p,c,v) -> (ci,p,c,v) + | _ -> raise DestKO + +let destProj c = match kind c with + | Proj (p, c) -> (p, c) + | _ -> raise DestKO + +let destFix c = match kind c with + | Fix fix -> fix + | _ -> raise DestKO + +let destCoFix c = match kind c with + | CoFix cofix -> cofix + | _ -> raise DestKO + + +(******************************************************************) +(* Flattening and unflattening of embedded applications and casts *) +(******************************************************************) + +let decompose_app c = + match kind c with + | App (f,cl) -> (f, Array.to_list cl) + | _ -> (c,[]) + +let decompose_appvect c = + match kind c with + | App (f,cl) -> (f, cl) + | _ -> (c,[||]) + (****************************************************************************) (* Functions to recur through subterms *) (****************************************************************************) @@ -301,6 +479,34 @@ let iter_with_binders g f n c = match kind c with CArray.Fun1.iter f n tl; CArray.Fun1.iter f (iterate g (Array.length tl) n) bl +(* [fold_constr_with_binders g f n acc c] folds [f n] on the immediate + subterms of [c] starting from [acc] and proceeding from left to + right according to the usual representation of the constructions as + [fold_constr] but it carries an extra data [n] (typically a lift + index) which is processed by [g] (which typically add 1 to [n]) at + each binder traversal; it is not recursive *) + +let fold_constr_with_binders g f n acc c = + match kind c with + | (Rel _ | Meta _ | Var _ | Sort _ | Const _ | Ind _ + | Construct _) -> acc + | Cast (c,_, t) -> f n (f n acc c) t + | Prod (na,t,c) -> f (g n) (f n acc t) c + | Lambda (na,t,c) -> f (g n) (f n acc t) c + | LetIn (na,b,t,c) -> f (g n) (f n (f n acc b) t) c + | App (c,l) -> Array.fold_left (f n) (f n acc c) l + | Proj (p,c) -> f n acc c + | Evar (_,l) -> Array.fold_left (f n) acc l + | Case (_,p,c,bl) -> Array.fold_left (f n) (f n (f n acc p) c) bl + | Fix (_,(lna,tl,bl)) -> + let n' = CArray.fold_left2 (fun c n t -> g c) n lna tl in + let fd = Array.map2 (fun t b -> (t,b)) tl bl in + Array.fold_left (fun acc (t,b) -> f n' (f n acc t) b) acc fd + | CoFix (_,(lna,tl,bl)) -> + let n' = CArray.fold_left2 (fun c n t -> g c) n lna tl in + let fd = Array.map2 (fun t b -> (t,b)) tl bl in + Array.fold_left (fun acc (t,b) -> f n' (f n acc t) b) acc fd + (* [map f c] maps [f] on the immediate subterms of [c]; it is not recursive and the order with which subterms are processed is not specified *) @@ -476,6 +682,11 @@ 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')) +type instance_compare_fn = global_reference -> int -> + Univ.Instance.t -> Univ.Instance.t -> bool + +type constr_compare_fn = int -> constr -> constr -> bool + (* [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 @@ -487,35 +698,42 @@ let map_with_binders g f l c0 = match kind c0 with optimisation that physically equal arrays are equals (hence the calls to {!Array.equal_norefl}). *) -let compare_head_gen_leq_with kind1 kind2 eq_universes leq_sorts eq leq t1 t2 = +let compare_head_gen_leq_with kind1 kind2 leq_universes leq_sorts eq leq nargs 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 -> 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_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 - | 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 + | Cast (c1, _, _), _ -> leq nargs c1 t2 + | _, Cast (c2, _, _) -> leq nargs t1 c2 + | Prod (_,t1,c1), Prod (_,t2,c2) -> eq 0 t1 t2 && leq 0 c1 c2 + | Lambda (_,t1,c1), Lambda (_,t2,c2) -> eq 0 t1 t2 && eq 0 c1 c2 + | LetIn (_,b1,t1,c1), LetIn (_,b2,t2,c2) -> eq 0 b1 b2 && eq 0 t1 t2 && leq nargs c1 c2 + (* Why do we suddenly make a special case for Cast here? *) + | App (Cast (c1, _, _), l1), _ -> leq nargs (mkApp (c1, l1)) t2 + | _, App (Cast (c2, _, _), l2) -> leq nargs t1 (mkApp (c2, l2)) + | App (c1, l1), App (c2, l2) -> + let len = Array.length l1 in + Int.equal len (Array.length l2) && + eq (nargs+len) c1 c2 && Array.equal_norefl (eq 0) l1 l2 + | Proj (p1,c1), Proj (p2,c2) -> Projection.equal p1 p2 && eq 0 c1 c2 + | Evar (e1,l1), Evar (e2,l2) -> Evar.equal e1 e2 && Array.equal (eq 0) l1 l2 + | Const (c1,u1), Const (c2,u2) -> + (* The args length currently isn't used but may as well pass it. *) + Constant.equal c1 c2 && leq_universes (ConstRef c1) nargs u1 u2 + | Ind (c1,u1), Ind (c2,u2) -> eq_ind c1 c2 && leq_universes (IndRef c1) nargs u1 u2 + | Construct (c1,u1), Construct (c2,u2) -> + eq_constructor c1 c2 && leq_universes (ConstructRef c1) nargs u1 u2 | Case (_,p1,c1,bl1), Case (_,p2,c2,bl2) -> - eq p1 p2 && eq c1 c2 && Array.equal eq bl1 bl2 + eq 0 p1 p2 && eq 0 c1 c2 && Array.equal (eq 0) bl1 bl2 | Fix ((ln1, i1),(_,tl1,bl1)), Fix ((ln2, i2),(_,tl2,bl2)) -> - Int.equal i1 i2 && Array.equal Int.equal ln1 ln2 - && Array.equal_norefl eq tl1 tl2 && Array.equal_norefl eq bl1 bl2 + Int.equal i1 i2 && Array.equal Int.equal ln1 ln2 + && Array.equal_norefl (eq 0) tl1 tl2 && Array.equal_norefl (eq 0) bl1 bl2 | CoFix(ln1,(_,tl1,bl1)), CoFix(ln2,(_,tl2,bl2)) -> - Int.equal ln1 ln2 && Array.equal_norefl eq tl1 tl2 && Array.equal_norefl eq bl1 bl2 - | _ -> false + Int.equal ln1 ln2 && Array.equal_norefl (eq 0) tl1 tl2 && Array.equal_norefl (eq 0) bl1 bl2 + | (Rel _ | Meta _ | Var _ | Sort _ | Prod _ | Lambda _ | LetIn _ | App _ + | Proj _ | Evar _ | Const _ | Ind _ | Construct _ | Case _ | Fix _ + | CoFix _), _ -> 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, @@ -523,8 +741,8 @@ let compare_head_gen_leq_with kind1 kind2 eq_universes leq_sorts eq leq t1 t2 = 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_leq_with kind kind eq_universes leq_sorts eq leq t1 t2 +let compare_head_gen_leq leq_universes leq_sorts eq leq t1 t2 = + compare_head_gen_leq_with kind kind leq_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 @@ -541,7 +759,7 @@ let compare_head_gen_with kind1 kind2 eq_universes eq_sorts eq t1 t2 = 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 +let compare_head = compare_head_gen (fun _ _ -> Univ.Instance.equal) Sorts.equal (*******************************) (* alpha conversion functions *) @@ -549,41 +767,41 @@ let compare_head = compare_head_gen (fun _ -> Univ.Instance.equal) Sorts.equal (* alpha conversion : ignore print names and casts *) -let rec eq_constr m n = - (m == n) || compare_head_gen (fun _ -> Instance.equal) Sorts.equal eq_constr m n +let rec eq_constr nargs m n = + (m == n) || compare_head_gen (fun _ _ -> Instance.equal) Sorts.equal eq_constr nargs m n -let equal m n = eq_constr m n (* to avoid tracing a recursive fun *) +let equal n m = eq_constr 0 m n (* to avoid tracing a recursive fun *) let eq_constr_univs univs m n = if m == n then true else - let eq_universes _ = UGraph.check_eq_instances univs in + let eq_universes _ _ = UGraph.check_eq_instances univs in let eq_sorts s1 s2 = s1 == s2 || UGraph.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 rec eq_constr' nargs m n = + m == n || compare_head_gen eq_universes eq_sorts eq_constr' nargs m n + in compare_head_gen eq_universes eq_sorts eq_constr' 0 m n let leq_constr_univs univs m n = if m == n then true else - let eq_universes _ = UGraph.check_eq_instances univs in + let eq_universes _ _ = UGraph.check_eq_instances univs in let eq_sorts s1 s2 = s1 == s2 || UGraph.check_eq univs (Sorts.univ_of_sort s1) (Sorts.univ_of_sort s2) in let leq_sorts s1 s2 = s1 == s2 || UGraph.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 + let rec eq_constr' nargs m n = + m == n || compare_head_gen eq_universes eq_sorts eq_constr' nargs m n in - let rec compare_leq 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 + let rec compare_leq nargs m n = + compare_head_gen_leq eq_universes leq_sorts eq_constr' leq_constr' nargs m n + and leq_constr' nargs m n = m == n || compare_leq nargs m n in + compare_leq 0 m n let eq_constr_univs_infer univs m n = if m == n then true, Constraint.empty else let cstrs = ref Constraint.empty in - let eq_universes strict = UGraph.check_eq_instances univs in + let eq_universes _ _ = UGraph.check_eq_instances univs in let eq_sorts s1 s2 = if Sorts.equal s1 s2 then true else @@ -593,17 +811,17 @@ let eq_constr_univs_infer univs m n = (cstrs := Univ.enforce_eq u1 u2 !cstrs; true) in - let rec eq_constr' m n = - m == n || compare_head_gen eq_universes eq_sorts eq_constr' m n + let rec eq_constr' nargs m n = + m == n || compare_head_gen eq_universes eq_sorts eq_constr' nargs m n in - let res = compare_head_gen eq_universes eq_sorts eq_constr' m n in + let res = compare_head_gen eq_universes eq_sorts eq_constr' 0 m n in res, !cstrs let leq_constr_univs_infer univs m n = if m == n then true, Constraint.empty else let cstrs = ref Constraint.empty in - let eq_universes strict l l' = UGraph.check_eq_instances univs l l' in + let eq_universes _ _ l l' = UGraph.check_eq_instances univs l l' in let eq_sorts s1 s2 = if Sorts.equal s1 s2 then true else @@ -618,25 +836,22 @@ let leq_constr_univs_infer univs m n = let u1 = Sorts.univ_of_sort s1 and u2 = Sorts.univ_of_sort s2 in if UGraph.check_leq univs u1 u2 then true else - (cstrs := Univ.enforce_leq u1 u2 !cstrs; - true) + (try let c, _ = UGraph.enforce_leq_alg u1 u2 univs in + cstrs := Univ.Constraint.union c !cstrs; + true + with Univ.UniverseInconsistency _ -> false) in - let rec eq_constr' m n = - m == n || compare_head_gen eq_universes eq_sorts eq_constr' m n + let rec eq_constr' nargs m n = + m == n || compare_head_gen eq_universes eq_sorts eq_constr' nargs m n in - let rec compare_leq 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 + let rec compare_leq nargs m n = + compare_head_gen_leq eq_universes leq_sorts eq_constr' leq_constr' nargs m n + and leq_constr' nargs m n = m == n || compare_leq nargs m n in + let res = compare_leq 0 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) + (m == n) || compare_head_gen (fun _ _ _ _ -> true) (fun _ _ -> true) (fun _ -> eq_constr_nounivs) 0 m n let constr_ord_int f t1 t2 = let (=?) f g i1 i2 j1 j2= @@ -649,35 +864,50 @@ let constr_ord_int f t1 t2 = ((Array.compare Int.compare) =? Int.compare) a1 a2 i1 i2 in match kind t1, kind t2 with + | Cast (c1,_,_), _ -> f c1 t2 + | _, Cast (c2,_,_) -> f t1 c2 + (* Why this special case? *) + | App (Cast(c1,_,_),l1), _ -> f (mkApp (c1,l1)) t2 + | _, App (Cast(c2, _,_),l2) -> f t1 (mkApp (c2,l2)) | Rel n1, Rel n2 -> Int.compare n1 n2 - | Meta m1, Meta m2 -> Int.compare m1 m2 + | Rel _, _ -> -1 | _, Rel _ -> 1 | Var id1, Var id2 -> Id.compare id1 id2 + | Var _, _ -> -1 | _, Var _ -> 1 + | Meta m1, Meta m2 -> Int.compare m1 m2 + | Meta _, _ -> -1 | _, Meta _ -> 1 + | Evar (e1,l1), Evar (e2,l2) -> + (Evar.compare =? (Array.compare f)) e1 e2 l1 l2 + | Evar _, _ -> -1 | _, Evar _ -> 1 | Sort s1, Sort s2 -> Sorts.compare s1 s2 - | Cast (c1,_,_), _ -> f c1 t2 - | _, Cast (c2,_,_) -> f t1 c2 + | Sort _, _ -> -1 | _, Sort _ -> 1 | Prod (_,t1,c1), Prod (_,t2,c2) | Lambda (_,t1,c1), Lambda (_,t2,c2) -> (f =? f) t1 t2 c1 c2 + | Prod _, _ -> -1 | _, Prod _ -> 1 + | Lambda _, _ -> -1 | _, Lambda _ -> 1 | LetIn (_,b1,t1,c1), LetIn (_,b2,t2,c2) -> ((f =? f) ==? f) b1 b2 t1 t2 c1 c2 - | App (Cast(c1,_,_),l1), _ -> f (mkApp (c1,l1)) t2 - | _, App (Cast(c2, _,_),l2) -> f t1 (mkApp (c2,l2)) + | LetIn _, _ -> -1 | _, LetIn _ -> 1 | App (c1,l1), App (c2,l2) -> (f =? (Array.compare f)) c1 c2 l1 l2 - | Proj (p1,c1), Proj (p2,c2) -> (Projection.compare =? f) p1 p2 c1 c2 - | Evar (e1,l1), Evar (e2,l2) -> - (Evar.compare =? (Array.compare f)) e1 e2 l1 l2 - | Const (c1,u1), Const (c2,u2) -> con_ord c1 c2 + | App _, _ -> -1 | _, App _ -> 1 + | Const (c1,u1), Const (c2,u2) -> Constant.CanOrd.compare c1 c2 + | Const _, _ -> -1 | _, Const _ -> 1 | Ind (ind1, u1), Ind (ind2, u2) -> ind_ord ind1 ind2 + | Ind _, _ -> -1 | _, Ind _ -> 1 | Construct (ct1,u1), Construct (ct2,u2) -> constructor_ord ct1 ct2 + | Construct _, _ -> -1 | _, Construct _ -> 1 | Case (_,p1,c1,bl1), Case (_,p2,c2,bl2) -> ((f =? f) ==? (Array.compare f)) p1 p2 c1 c2 bl1 bl2 + | Case _, _ -> -1 | _, Case _ -> 1 | Fix (ln1,(_,tl1,bl1)), Fix (ln2,(_,tl2,bl2)) -> ((fix_cmp =? (Array.compare f)) ==? (Array.compare f)) ln1 ln2 tl1 tl2 bl1 bl2 + | Fix _, _ -> -1 | _, Fix _ -> 1 | CoFix(ln1,(_,tl1,bl1)), CoFix(ln2,(_,tl2,bl2)) -> ((Int.compare =? (Array.compare f)) ==? (Array.compare f)) ln1 ln2 tl1 tl2 bl1 bl2 - | t1, t2 -> Int.compare (tag t1) (tag t2) + | CoFix _, _ -> -1 | _, CoFix _ -> 1 + | Proj (p1,c1), Proj (p2,c2) -> (Projection.compare =? f) p1 p2 c1 c2 let rec compare m n= constr_ord_int compare m n @@ -761,7 +991,9 @@ let hasheq t1 t2 = && array_eqeq lna1 lna2 && array_eqeq tl1 tl2 && array_eqeq bl1 bl2 - | _ -> false + | (Rel _ | Meta _ | Var _ | Sort _ | Cast _ | Prod _ | Lambda _ | LetIn _ + | App _ | Proj _ | Evar _ | Const _ | Ind _ | Construct _ | Case _ + | Fix _ | CoFix _), _ -> false (** Note that the following Make has the side effect of creating once and for all the table we'll use for hash-consing all constr *) @@ -972,28 +1204,6 @@ 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 eq s1 s2 = - s1 == s2 || - match (s1,s2) with - (Prop c1, Prop c2) -> c1 == c2 - | (Type u1, Type u2) -> u1 == u2 - |_ -> false - let hash = function - | Prop Null -> 0 | Prop Pos -> 1 - | Type u -> 2 + Universe.hash u - end) - -(* let hcons_sorts = Hashcons.simple_hcons Hsorts.generate hcons_univ *) let hcons_caseinfo = Hashcons.simple_hcons Hcaseinfo.generate Hcaseinfo.hcons hcons_ind let hcons = @@ -1007,8 +1217,3 @@ let hcons = Id.hcons) (* let hcons_types = hcons_constr *) - -(*******) -(* Type of abstract machine values *) -(** FIXME: nothing to do there *) -type values |