diff options
Diffstat (limited to 'kernel')
| -rw-r--r-- | kernel/constr.ml | 8 | ||||
| -rw-r--r-- | kernel/constr.mli | 2 | ||||
| -rw-r--r-- | kernel/evar.ml | 24 | ||||
| -rw-r--r-- | kernel/evar.mli | 31 | ||||
| -rw-r--r-- | kernel/kernel.mllib | 1 | ||||
| -rw-r--r-- | kernel/reduction.ml | 2 |
6 files changed, 62 insertions, 6 deletions
diff --git a/kernel/constr.ml b/kernel/constr.ml index eba490dbd..8b7505aeb 100644 --- a/kernel/constr.ml +++ b/kernel/constr.ml @@ -31,7 +31,7 @@ open Univ open Esubst -type existential_key = int +type existential_key = Evar.t type metavariable = int (* This defines the strategy to use for verifiying a Cast *) @@ -341,7 +341,7 @@ let compare_head f t1 t2 = | 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) -> Int.equal e1 e2 && 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 @@ -391,7 +391,7 @@ let constr_ord_int f t1 t2 = | _, App (Cast(c2, _,_),l2) -> f t1 (mkApp (c2,l2)) | 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 + (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 @@ -469,7 +469,7 @@ let hasheq t1 t2 = | LetIn (n1,b1,t1,c1), LetIn (n2,b2,t2,c2) -> n1 == n2 & b1 == b2 & t1 == t2 & c1 == c2 | App (c1,l1), App (c2,l2) -> c1 == c2 & array_eqeq l1 l2 - | Evar (e1,l1), Evar (e2,l2) -> Int.equal e1 e2 & 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) -> diff --git a/kernel/constr.mli b/kernel/constr.mli index 59430125f..261b6bfb4 100644 --- a/kernel/constr.mli +++ b/kernel/constr.mli @@ -9,7 +9,7 @@ open Names (** {6 Existential variables } *) -type existential_key = int +type existential_key = Evar.t (** {6 Existential variables } *) type metavariable = int diff --git a/kernel/evar.ml b/kernel/evar.ml new file mode 100644 index 000000000..d7e32626f --- /dev/null +++ b/kernel/evar.ml @@ -0,0 +1,24 @@ +(************************************************************************) +(* v * The Coq Proof Assistant / The Coq Development Team *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2012 *) +(* \VV/ **************************************************************) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(************************************************************************) + +type t = int + +let repr x = x +let unsafe_of_int x = x +let compare = Int.compare +let equal = Int.equal + +module Self = +struct + type _t = t + type t = _t + let compare = compare +end + +module Set = Set.Make(Self) +module Map = CMap.Make(Self) diff --git a/kernel/evar.mli b/kernel/evar.mli new file mode 100644 index 000000000..8e8b88d94 --- /dev/null +++ b/kernel/evar.mli @@ -0,0 +1,31 @@ +(************************************************************************) +(* v * The Coq Proof Assistant / The Coq Development Team *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2012 *) +(* \VV/ **************************************************************) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(************************************************************************) + +(** This module defines existential variables, which are isomorphic to [int]. + Nonetheless, casting from an [int] to a variable is deemed unsafe, so that + to keep track of such casts, one has to use the provided {!unsafe_of_int} + function. *) + +type t +(** Type of existential variables. *) + +val repr : t -> int +(** Recover the underlying integer. *) + +val unsafe_of_int : int -> t +(** This is not for dummies. Do not use this function if you don't know what you + are doing. *) + +val equal : t -> t -> bool +(** Equality over existential variables. *) + +val compare : t -> t -> int +(** Comparison over existential variables. *) + +module Set : Set.S with type elt = t +module Map : CMap.ExtS with type key = t and module Set := Set diff --git a/kernel/kernel.mllib b/kernel/kernel.mllib index 36b3d8323..cbc147e9e 100644 --- a/kernel/kernel.mllib +++ b/kernel/kernel.mllib @@ -2,6 +2,7 @@ Names Univ Esubst Sorts +Evar Constr Context Vars diff --git a/kernel/reduction.ml b/kernel/reduction.ml index 1f5a6a6a0..48c63ac96 100644 --- a/kernel/reduction.ml +++ b/kernel/reduction.ml @@ -277,7 +277,7 @@ and eqappr cv_pb l2r infos (lft1,st1) (lft2,st2) cuniv = else raise NotConvertible | _ -> raise NotConvertible) | (FEvar ((ev1,args1),env1), FEvar ((ev2,args2),env2)) -> - if Int.equal ev1 ev2 then + if Evar.equal ev1 ev2 then let u1 = convert_stacks l2r infos lft1 lft2 v1 v2 cuniv in convert_vect l2r infos el1 el2 (Array.map (mk_clos env1) args1) |