From 4490dfcb94057dd6518963a904565e3a4a354bac Mon Sep 17 00:00:00 2001 From: ppedrot Date: Mon, 29 Apr 2013 16:02:05 +0000 Subject: Splitting Term into five unrelated interfaces: 1. sorts.ml: A small file utility for sorts; 2. constr.ml: Really low-level terms, essentially kind_of_constr, smart constructor and basic operators; 3. vars.ml: Everything related to term variables, that is, occurences and substitution; 4. context.ml: Rel/Named context and all that; 5. term.ml: derived utility operations on terms; also includes constr.ml up to some renaming, and acts as a compatibility layer, to be deprecated. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16462 85f007b7-540e-0410-9357-904b9bb8a0f7 --- dev/printers.mllib | 4 + interp/constrextern.mli | 1 + interp/constrintern.mli | 1 + kernel/closure.ml | 3 +- kernel/constr.ml | 660 +++++++++++++++ kernel/constr.mli | 246 ++++++ kernel/context.ml | 64 ++ kernel/context.mli | 60 ++ kernel/cooking.ml | 1 + kernel/csymtable.ml | 1 + kernel/declarations.mli | 1 + kernel/environ.ml | 4 +- kernel/environ.mli | 1 + kernel/indtypes.ml | 2 + kernel/inductive.ml | 2 + kernel/inductive.mli | 1 + kernel/kernel.mllib | 4 + kernel/nativecode.ml | 3 +- kernel/pre_env.ml | 1 + kernel/pre_env.mli | 1 + kernel/reduction.ml | 2 + kernel/reduction.mli | 1 + kernel/sign.ml | 5 +- kernel/sign.mli | 5 +- kernel/sorts.ml | 64 ++ kernel/sorts.mli | 29 + kernel/term.ml | 1023 +++--------------------- kernel/term.mli | 423 +++------- kernel/term_typing.ml | 1 + kernel/typeops.ml | 2 + kernel/typeops.mli | 1 + kernel/vars.ml | 186 +++++ kernel/vars.mli | 69 ++ library/global.mli | 1 + library/heads.ml | 1 + plugins/cc/ccalgo.ml | 1 + plugins/cc/cctac.ml | 3 +- plugins/decl_mode/decl_interp.ml | 1 + plugins/decl_mode/decl_proof_instr.ml | 9 +- plugins/extraction/extraction.ml | 2 + plugins/firstorder/formula.ml | 8 +- plugins/firstorder/formula.mli | 3 +- plugins/firstorder/ground.ml | 1 + plugins/firstorder/instances.ml | 1 + plugins/firstorder/rules.ml | 1 + plugins/firstorder/unify.ml | 1 + plugins/funind/functional_principles_proofs.ml | 2 + plugins/funind/functional_principles_types.ml | 2 + plugins/funind/g_indfun.ml4 | 1 + plugins/funind/glob_term_to_relation.ml | 1 + plugins/funind/invfun.ml | 1 + plugins/funind/merge.ml | 2 + plugins/funind/recdef.ml | 1 + plugins/rtauto/refl_tauto.ml | 2 +- plugins/setoid_ring/newring.ml4 | 1 + plugins/xml/cic2acic.ml | 12 +- plugins/xml/doubleTypeInference.ml | 7 +- pretyping/cases.ml | 2 + pretyping/cases.mli | 5 +- pretyping/cbv.ml | 3 +- pretyping/coercion.ml | 9 +- pretyping/detyping.ml | 2 + pretyping/detyping.mli | 1 + pretyping/evarconv.ml | 1 + pretyping/evarsolve.ml | 2 + pretyping/evarutil.ml | 2 + pretyping/evarutil.mli | 1 + pretyping/evd.ml | 1 + pretyping/indrec.ml | 2 + pretyping/inductiveops.ml | 2 + pretyping/inductiveops.mli | 1 + pretyping/matching.ml | 2 + pretyping/namegen.ml | 1 + pretyping/namegen.mli | 1 + pretyping/nativenorm.ml | 1 + pretyping/patternops.ml | 1 + pretyping/pretype_errors.ml | 1 + pretyping/pretyping.ml | 2 + pretyping/reductionops.ml | 8 +- pretyping/reductionops.mli | 1 + pretyping/retyping.ml | 1 + pretyping/tacred.ml | 1 + pretyping/termops.ml | 2 + pretyping/termops.mli | 3 + pretyping/typeclasses.ml | 4 +- pretyping/typeclasses.mli | 1 + pretyping/typeclasses_errors.ml | 1 + pretyping/typeclasses_errors.mli | 1 + pretyping/typing.ml | 1 + pretyping/unification.ml | 1 + pretyping/vnorm.ml | 1 + printing/printer.ml | 2 + printing/printer.mli | 1 + proofs/clenv.ml | 1 + proofs/goal.ml | 18 +- proofs/goal.mli | 2 +- proofs/logic.ml | 10 +- proofs/proof_type.ml | 1 + proofs/proof_type.mli | 1 + proofs/tacmach.mli | 1 + tactics/auto.ml | 1 + tactics/auto.mli | 1 + tactics/eqschemes.ml | 2 + tactics/equality.ml | 1 + tactics/equality.mli | 1 + tactics/extratactics.ml4 | 1 + tactics/inv.ml | 2 + tactics/leminv.ml | 1 + tactics/refine.ml | 1 + tactics/rewrite.ml4 | 1 + tactics/tacticals.mli | 1 + tactics/tactics.ml | 2 + tactics/tactics.mli | 1 + toplevel/auto_ind_decl.ml | 3 +- toplevel/autoinstance.ml | 2 + toplevel/autoinstance.mli | 1 + toplevel/class.ml | 1 + toplevel/classes.ml | 2 + toplevel/classes.mli | 1 + toplevel/command.ml | 2 + toplevel/discharge.ml | 1 + toplevel/ide_slave.ml | 2 +- toplevel/obligations.ml | 9 +- toplevel/record.ml | 1 + toplevel/record.mli | 1 + toplevel/vernacentries.ml | 4 +- 126 files changed, 1810 insertions(+), 1279 deletions(-) create mode 100644 kernel/constr.ml create mode 100644 kernel/constr.mli create mode 100644 kernel/context.ml create mode 100644 kernel/context.mli create mode 100644 kernel/sorts.ml create mode 100644 kernel/sorts.mli create mode 100644 kernel/vars.ml create mode 100644 kernel/vars.mli diff --git a/dev/printers.mllib b/dev/printers.mllib index 73bda713a..b09c8e97e 100644 --- a/dev/printers.mllib +++ b/dev/printers.mllib @@ -40,6 +40,10 @@ Dnet Names Univ Esubst +Sorts +Constr +Context +Vars Term Mod_subst Sign diff --git a/interp/constrextern.mli b/interp/constrextern.mli index 0a4192c3e..4cf79337c 100644 --- a/interp/constrextern.mli +++ b/interp/constrextern.mli @@ -9,6 +9,7 @@ open Pp open Names open Term +open Context open Termops open Sign open Environ diff --git a/interp/constrintern.mli b/interp/constrintern.mli index 99c2a338e..1fa0db911 100644 --- a/interp/constrintern.mli +++ b/interp/constrintern.mli @@ -8,6 +8,7 @@ open Names open Term +open Context open Sign open Evd open Environ diff --git a/kernel/closure.ml b/kernel/closure.ml index b22dd42e7..2628895eb 100644 --- a/kernel/closure.ml +++ b/kernel/closure.ml @@ -22,8 +22,9 @@ open Errors open Util open Pp -open Term open Names +open Term +open Vars open Environ open Esubst diff --git a/kernel/constr.ml b/kernel/constr.ml new file mode 100644 index 000000000..d09222ead --- /dev/null +++ b/kernel/constr.ml @@ -0,0 +1,660 @@ +(************************************************************************) +(* v * The Coq Proof Assistant / The Coq Development Team *) +(* mkProp (* Easy sharing *) + | Sorts.Prop Sorts.Pos -> mkSet + | s -> Sort s + +(* Constructs the term t1::t2, i.e. the term t1 casted with the type t2 *) +(* (that means t2 is declared as the type of t1) *) +let mkCast (t1,k2,t2) = + match t1 with + | Cast (c,k1, _) when (k1 == VMcast || k1 == NATIVEcast) && k1 == k2 -> Cast (c,k1,t2) + | _ -> Cast (t1,k2,t2) + +(* Constructs the product (x:t1)t2 *) +let mkProd (x,t1,t2) = Prod (x,t1,t2) + +(* Constructs the abstraction [x:t1]t2 *) +let mkLambda (x,t1,t2) = Lambda (x,t1,t2) + +(* Constructs [x=c_1:t]c_2 *) +let mkLetIn (x,c1,t,c2) = LetIn (x,c1,t,c2) + +(* If lt = [t1; ...; tn], constructs the application (t1 ... tn) *) +(* We ensure applicative terms have at least one argument and the + function is not itself an applicative term *) +let mkApp (f, a) = + if Int.equal (Array.length a) 0 then f else + match f with + | App (g, cl) -> App (g, Array.append cl a) + | _ -> App (f, a) + +(* Constructs a constant *) +let mkConst c = Const 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 + +(* 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 + +(* Constructs the term

Case c of c1 | c2 .. | cn end *) +let mkCase (ci, p, c, ac) = Case (ci, p, c, ac) + +(* If recindxs = [|i1,...in|] + funnames = [|f1,...fn|] + typarray = [|t1,...tn|] + bodies = [|b1,...bn|] + then + + mkFix ((recindxs,i),(funnames,typarray,bodies)) + + constructs the ith function of the block + + Fixpoint f1 [ctx1] : t1 := b1 + with f2 [ctx2] : t2 := b2 + ... + with fn [ctxn] : tn := bn. + + where the length of the jth context is ij. +*) + +let mkFix fix = Fix fix + +(* If funnames = [|f1,...fn|] + typarray = [|t1,...tn|] + bodies = [|b1,...bn|] + then + + mkCoFix (i,(funnames,typsarray,bodies)) + + constructs the ith function of the block + + CoFixpoint f1 : t1 := b1 + with f2 : t2 := b2 + ... + with fn : tn := bn. +*) +let mkCoFix cofix= CoFix cofix + +(* Constructs an existential variable named "?n" *) +let mkMeta n = Meta n + +(* Constructs a Variable named id *) +let mkVar id = Var id + + +(************************************************************************) +(* kind_of_term = constructions as seen by the user *) +(************************************************************************) + +(* User view of [constr]. For [App], it is ensured there is at + least one argument and the function is not itself an applicative + term *) + +let kind c = c + +(****************************************************************************) +(* Functions to recur through subterms *) +(****************************************************************************) + +(* [fold f acc c] folds [f] on the immediate subterms of [c] + starting from [acc] and proceeding from left to right according to + the usual representation of the constructions; it is not recursive *) + +let fold f acc c = match kind c with + | (Rel _ | Meta _ | Var _ | Sort _ | Const _ | Ind _ + | Construct _) -> acc + | Cast (c,_,t) -> f (f acc c) t + | Prod (_,t,c) -> f (f acc t) c + | 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 + | 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)) -> + let fd = Array.map3 (fun na t b -> (na,t,b)) lna tl bl in + Array.fold_left (fun acc (na,t,b) -> f (f acc t) b) acc fd + | CoFix (_,(lna,tl,bl)) -> + let fd = Array.map3 (fun na t b -> (na,t,b)) lna tl bl in + Array.fold_left (fun acc (na,t,b) -> f (f acc t) b) acc fd + +(* [iter f c] iters [f] on the immediate subterms of [c]; it is + not recursive and the order with which subterms are processed is + not specified *) + +let iter f c = match kind c with + | (Rel _ | Meta _ | Var _ | Sort _ | Const _ | Ind _ + | Construct _) -> () + | Cast (c,_,t) -> f c; f t + | Prod (_,t,c) -> f t; f c + | 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 + | 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 + | CoFix (_,(_,tl,bl)) -> Array.iter f tl; Array.iter f bl + +(* [iter_with_binders g f n c] iters [f n] on the immediate + subterms of [c]; 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 and the order with which + subterms are processed is not specified *) + +let iter_with_binders g f n c = match kind c with + | (Rel _ | Meta _ | Var _ | Sort _ | Const _ | Ind _ + | Construct _) -> () + | Cast (c,_,t) -> f n c; f n t + | Prod (_,t,c) -> f n t; f (g n) c + | Lambda (_,t,c) -> f n t; f (g n) c + | LetIn (_,b,t,c) -> f n b; f n t; f (g n) c + | App (c,l) -> f n c; Array.iter (f n) l + | Evar (_,l) -> Array.iter (f n) l + | Case (_,p,c,bl) -> f n p; f n c; Array.iter (f n) bl + | Fix (_,(_,tl,bl)) -> + Array.iter (f n) tl; + Array.iter (f (iterate g (Array.length tl) n)) bl + | CoFix (_,(_,tl,bl)) -> + Array.iter (f n) tl; + Array.iter (f (iterate g (Array.length tl) n)) bl + +(* [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 *) + +let map f c = match kind c with + | (Rel _ | Meta _ | Var _ | Sort _ | Const _ | Ind _ + | Construct _) -> c + | Cast (c,k,t) -> mkCast (f c, k, f t) + | Prod (na,t,c) -> mkProd (na, f t, f c) + | Lambda (na,t,c) -> mkLambda (na, f t, f c) + | LetIn (na,b,t,c) -> mkLetIn (na, f b, f t, f c) + | App (c,l) -> mkApp (f c, Array.map f l) + | Evar (e,l) -> mkEvar (e, Array.map f l) + | Case (ci,p,c,bl) -> mkCase (ci, f p, f c, Array.map f bl) + | Fix (ln,(lna,tl,bl)) -> + mkFix (ln,(lna,Array.map f tl,Array.map f bl)) + | CoFix(ln,(lna,tl,bl)) -> + mkCoFix (ln,(lna,Array.map f tl,Array.map f bl)) + +(* [map_with_binders g f n c] maps [f n] on the immediate + subterms of [c]; 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 and the order with which + subterms are processed is not specified *) + +let map_with_binders g f l c = match kind c with + | (Rel _ | Meta _ | Var _ | Sort _ | Const _ | Ind _ + | Construct _) -> c + | Cast (c,k,t) -> mkCast (f l c, k, f l t) + | Prod (na,t,c) -> mkProd (na, f l t, f (g l) c) + | Lambda (na,t,c) -> mkLambda (na, f l t, f (g l) c) + | LetIn (na,b,t,c) -> mkLetIn (na, f l b, f l t, f (g l) c) + | App (c,al) -> mkApp (f l c, Array.map (f l) al) + | Evar (e,al) -> mkEvar (e, Array.map (f l) al) + | Case (ci,p,c,bl) -> mkCase (ci, f l p, f l c, Array.map (f l) bl) + | Fix (ln,(lna,tl,bl)) -> + let l' = iterate g (Array.length tl) l in + mkFix (ln,(lna,Array.map (f l) tl,Array.map (f l') bl)) + | CoFix(ln,(lna,tl,bl)) -> + let l' = iterate g (Array.length tl) l in + mkCoFix (ln,(lna,Array.map (f l) tl,Array.map (f l') bl)) + +(* [compare f c1 c2] compare [c1] and [c2] using [f] to compare + the immediate subterms of [c1] of [c2] if needed; Cast's, + application associativity, binders name and Cases annotations are + not taken into account *) + + +let compare_head 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 + | Var id1, Var id2 -> Id.equal id1 id2 + | Sort s1, Sort s2 -> Int.equal (Sorts.compare s1 s2) 0 + | 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) -> Int.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 + | 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 + +(*******************************) +(* alpha conversion functions *) +(*******************************) + +(* alpha conversion : ignore print names and casts *) + +let rec eq_constr m n = + (m == n) || compare_head eq_constr m n + +let equal m n = eq_constr m n (* to avoid tracing a recursive fun *) + +let constr_ord_int f t1 t2 = + let (=?) f g i1 i2 j1 j2= + let c = f i1 i2 in + if Int.equal c 0 then g j1 j2 else c in + let (==?) fg h i1 i2 j1 j2 k1 k2= + let c=fg i1 i2 j1 j2 in + if Int.equal c 0 then h k1 k2 else c in + let fix_cmp (a1, i1) (a2, i2) = + ((Array.compare Int.compare) =? Int.compare) a1 a2 i1 i2 + in + match kind t1, kind t2 with + | Rel n1, Rel n2 -> Int.compare n1 n2 + | Meta m1, Meta m2 -> Int.compare m1 m2 + | Var id1, Var id2 -> Id.compare id1 id2 + | Sort s1, Sort s2 -> Sorts.compare s1 s2 + | Cast (c1,_,_), _ -> f c1 t2 + | _, Cast (c2,_,_) -> f t1 c2 + | Prod (_,t1,c1), Prod (_,t2,c2) + | Lambda (_,t1,c1), Lambda (_,t2,c2) -> + (f =? f) t1 t2 c1 c2 + | 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)) + | 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 -> 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)) -> + ((fix_cmp =? (Array.compare f)) ==? (Array.compare f)) + ln1 ln2 tl1 tl2 bl1 bl2 + | CoFix(ln1,(_,tl1,bl1)), CoFix(ln2,(_,tl2,bl2)) -> + ((Int.compare =? (Array.compare f)) ==? (Array.compare f)) + ln1 ln2 tl1 tl2 bl1 bl2 + | t1, t2 -> Pervasives.compare t1 t2 + +let rec compare m n= + constr_ord_int compare m n + +(*******************) +(* hash-consing *) +(*******************) + +(* Hash-consing of [constr] does not use the module [Hashcons] because + [Hashcons] is not efficient on deep tree-like data + structures. Indeed, [Hashcons] is based the (very efficient) + generic hash function [Hashtbl.hash], which computes the hash key + through a depth bounded traversal of the data structure to be + hashed. As a consequence, for a deep [constr] like the natural + number 1000 (S (S (... (S O)))), the same hash is assigned to all + the sub [constr]s greater than the maximal depth handled by + [Hashtbl.hash]. This entails a huge number of collisions in the + hash table and leads to cubic hash-consing in this worst-case. + + In order to compute a hash key that is independent of the data + structure depth while being constant-time, an incremental hashing + function must be devised. A standard implementation creates a cache + of the hashing function by decorating each node of the hash-consed + data structure with its hash key. In that case, the hash function + can deduce the hash key of a toplevel data structure by a local + computation based on the cache held on its substructures. + Unfortunately, this simple implementation introduces a space + overhead that is damageable for the hash-consing of small [constr]s + (the most common case). One can think of an heterogeneous + distribution of caches on smartly chosen nodes, but this is forbidden + by the use of generic equality in Coq source code. (Indeed, this forces + each [constr] to have a unique canonical representation.) + + Given that hash-consing proceeds inductively, we can nonetheless + computes the hash key incrementally during hash-consing by changing + a little the signature of the hash-consing function: it now returns + both the hash-consed term and its hash key. This simple solution is + implemented in the following code: it does not introduce a space + overhead in [constr], that's why the efficiency is unchanged for + small [constr]s. Besides, it does handle deep [constr]s without + introducing an unreasonable number of collisions in the hash table. + Some benchmarks make us think that this implementation of + hash-consing is linear in the size of the hash-consed data + structure for our daily use of Coq. +*) + +let array_eqeq t1 t2 = + t1 == t2 || + (Int.equal (Array.length t1) (Array.length t2) && + let rec aux i = + (Int.equal i (Array.length t1)) || (t1.(i) == t2.(i) && aux (i + 1)) + in aux 0) + +let hasheq t1 t2 = + match t1, t2 with + | Rel n1, Rel n2 -> n1 == n2 + | Meta m1, Meta m2 -> m1 == m2 + | Var id1, Var id2 -> id1 == id2 + | Sort s1, Sort s2 -> s1 == s2 + | Cast (c1,k1,t1), Cast (c2,k2,t2) -> c1 == c2 & k1 == k2 & t1 == t2 + | Prod (n1,t1,c1), Prod (n2,t2,c2) -> n1 == n2 & t1 == t2 & c1 == c2 + | 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 + | 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 + | 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 + | 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)) -> + Int.equal i1 i2 + && Array.equal Int.equal ln1 ln2 + && array_eqeq lna1 lna2 + && array_eqeq tl1 tl2 + && array_eqeq bl1 bl2 + | CoFix(ln1,(lna1,tl1,bl1)), CoFix(ln2,(lna2,tl2,bl2)) -> + Int.equal ln1 ln2 + & array_eqeq lna1 lna2 + & array_eqeq tl1 tl2 + & array_eqeq bl1 bl2 + | _ -> 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 *) + +module HashsetTerm = Hashset.Make(struct type t = constr let equal = hasheq end) + +let term_table = HashsetTerm.create 19991 +(* The associative table to hashcons terms. *) + +open Hashset.Combine + +(* [hashcons hash_consing_functions constr] computes an hash-consed + representation for [constr] using [hash_consing_functions] on + leaves. *) +let hashcons (sh_sort,sh_ci,sh_construct,sh_ind,sh_con,sh_na,sh_id) = + + (* Note : we hash-cons constr arrays *in place* *) + + let rec hash_term_array t = + let accu = ref 0 in + for i = 0 to Array.length t - 1 do + let x, h = sh_rec t.(i) in + accu := combine !accu h; + t.(i) <- x + done; + !accu + + and hash_term t = + match t with + | Var i -> + (Var (sh_id i), combinesmall 1 (Hashtbl.hash i)) + | Sort s -> + (Sort (sh_sort s), combinesmall 2 (Hashtbl.hash s)) + | Cast (c, k, t) -> + let c, hc = sh_rec c in + let t, ht = sh_rec t in + (Cast (c, k, t), combinesmall 3 (combine3 hc (Hashtbl.hash k) ht)) + | Prod (na,t,c) -> + let t, ht = sh_rec t + and c, hc = sh_rec c in + (Prod (sh_na na, t, c), combinesmall 4 (combine3 (Hashtbl.hash na) ht hc)) + | Lambda (na,t,c) -> + let t, ht = sh_rec t + and c, hc = sh_rec c in + (Lambda (sh_na na, t, c), combinesmall 5 (combine3 (Hashtbl.hash na) ht hc)) + | LetIn (na,b,t,c) -> + let b, hb = sh_rec b in + let t, ht = sh_rec t in + let c, hc = sh_rec c in + (LetIn (sh_na na, b, t, c), combinesmall 6 (combine4 (Hashtbl.hash na) hb ht hc)) + | App (c,l) -> + let c, hc = sh_rec c in + let hl = hash_term_array l in + (App (c, l), combinesmall 7 (combine hl hc)) + | Evar (e,l) -> + let hl = hash_term_array l in + (* since the array have been hashed in place : *) + (t, combinesmall 8 (combine (Hashtbl.hash e) hl)) + | Const c -> + (Const (sh_con c), combinesmall 9 (Hashtbl.hash c)) + | Ind ((kn,i) as ind) -> + (Ind (sh_ind ind), combinesmall 10 (combine (Hashtbl.hash kn) i)) + | Construct (((kn,i),j) as c)-> + (Construct (sh_construct c), combinesmall 11 (combine3 (Hashtbl.hash kn) i j)) + | Case (ci,p,c,bl) -> + let p, hp = sh_rec p + and c, hc = sh_rec c in + let hbl = hash_term_array bl in + let hbl = combine (combine hc hp) hbl in + (Case (sh_ci ci, p, c, bl), combinesmall 12 hbl) + | Fix (ln,(lna,tl,bl)) -> + let hbl = hash_term_array bl in + let htl = hash_term_array tl in + Array.iteri (fun i x -> lna.(i) <- sh_na x) lna; + (* since the three arrays have been hashed in place : *) + (t, combinesmall 13 (combine (Hashtbl.hash lna) (combine hbl htl))) + | CoFix(ln,(lna,tl,bl)) -> + let hbl = hash_term_array bl in + let htl = hash_term_array tl in + Array.iteri (fun i x -> lna.(i) <- sh_na x) lna; + (* since the three arrays have been hashed in place : *) + (t, combinesmall 14 (combine (Hashtbl.hash lna) (combine hbl htl))) + | Meta n -> + (t, combinesmall 15 n) + | Rel n -> + (t, combinesmall 16 n) + + and sh_rec t = + let (y, h) = hash_term t in + (* [h] must be positive. *) + let h = h land 0x3FFFFFFF in + (HashsetTerm.repr h y term_table, h) + + in + (* Make sure our statically allocated Rels (1 to 16) are considered + as canonical, and hence hash-consed to themselves *) + ignore (hash_term_array rels); + + fun t -> fst (sh_rec t) + +(* Exported hashing fonction on constr, used mainly in plugins. + Appears to have slight differences from [snd (hash_term t)] above ? *) + +let rec hash t = + match kind t with + | Var i -> combinesmall 1 (Hashtbl.hash i) + | Sort s -> combinesmall 2 (Hashtbl.hash s) + | Cast (c, _, _) -> hash c + | Prod (_, t, c) -> combinesmall 4 (combine (hash t) (hash c)) + | Lambda (_, t, c) -> combinesmall 5 (combine (hash t) (hash c)) + | LetIn (_, b, t, c) -> + combinesmall 6 (combine3 (hash b) (hash t) (hash c)) + | App (Cast(c, _, _),l) -> hash (mkApp (c,l)) + | App (c,l) -> + combinesmall 7 (combine (hash_term_array l) (hash c)) + | Evar (e,l) -> + combinesmall 8 (combine (Hashtbl.hash e) (hash_term_array l)) + | Const c -> + combinesmall 9 (Hashtbl.hash c) (* TODO: proper hash function for constants *) + | Ind (kn,i) -> + combinesmall 10 (combine (Hashtbl.hash kn) i) + | Construct ((kn,i),j) -> + combinesmall 11 (combine3 (Hashtbl.hash kn) i j) + | Case (_ , p, c, bl) -> + combinesmall 12 (combine3 (hash c) (hash p) (hash_term_array bl)) + | Fix (ln ,(_, tl, bl)) -> + combinesmall 13 (combine (hash_term_array bl) (hash_term_array tl)) + | CoFix(ln, (_, tl, bl)) -> + combinesmall 14 (combine (hash_term_array bl) (hash_term_array tl)) + | Meta n -> combinesmall 15 n + | Rel n -> combinesmall 16 n + +and hash_term_array t = + Array.fold_left (fun acc t -> combine (hash t) acc) 0 t + +module Hcaseinfo = + Hashcons.Make( + struct + type t = case_info + type u = inductive -> inductive + let hashcons hind ci = { ci with ci_ind = hind ci.ci_ind } + let pp_info_equal info1 info2 = + Int.equal info1.ind_nargs info2.ind_nargs && + info1.style == info2.style + let equal ci ci' = + ci.ci_ind == ci'.ci_ind && + Int.equal ci.ci_npar ci'.ci_npar && + Array.equal Int.equal ci.ci_cstr_ndecls ci'.ci_cstr_ndecls && (* we use [Array.equal] on purpose *) + pp_info_equal ci.ci_pp_info ci'.ci_pp_info (* we use (=) on purpose *) + let hash = Hashtbl.hash + end) + +let hcons_caseinfo = Hashcons.simple_hcons Hcaseinfo.generate hcons_ind + +let hcons = + hashcons + (Sorts.hcons, + hcons_caseinfo, + hcons_construct, + hcons_ind, + hcons_con, + Name.hcons, + Id.hcons) + +(* let hcons_types = hcons_constr *) + +(*******) +(* Type of abstract machine values *) +(** FIXME: nothing to do there *) +type values diff --git a/kernel/constr.mli b/kernel/constr.mli new file mode 100644 index 000000000..59430125f --- /dev/null +++ b/kernel/constr.mli @@ -0,0 +1,246 @@ +(************************************************************************) +(* v * The Coq Proof Assistant / The Coq Development Team *) +(* constr + +(** Constructs a Variable *) +val mkVar : Id.t -> constr + +(** Constructs an patvar named "?n" *) +val mkMeta : metavariable -> constr + +(** Constructs an existential variable *) +type existential = existential_key * constr array +val mkEvar : existential -> constr + +(** Construct a sort *) +val mkSort : Sorts.t -> types +val mkProp : types +val mkSet : types +val mkType : Univ.universe -> types + + +(** This defines the strategy to use for verifiying a Cast *) +type cast_kind = VMcast | NATIVEcast | DEFAULTcast | REVERTcast + +(** Constructs the term [t1::t2], i.e. the term t{_ 1} casted with the + type t{_ 2} (that means t2 is declared as the type of t1). *) +val mkCast : constr * cast_kind * constr -> constr + +(** Constructs the product [(x:t1)t2] *) +val mkProd : Name.t * types * types -> types + +(** Constructs the abstraction \[x:t{_ 1}\]t{_ 2} *) +val mkLambda : Name.t * types * constr -> constr + +(** Constructs the product [let x = t1 : t2 in t3] *) +val mkLetIn : Name.t * constr * types * constr -> constr + +(** [mkApp (f,[| t_1; ...; t_n |]] constructs the application + {% $(f~t_1~\dots~t_n)$ %}. *) +val mkApp : constr * constr array -> constr + +(** Constructs a constant + The array of terms correspond to the variables introduced in the section *) +val mkConst : constant -> constr + +(** Inductive types *) + +(** Constructs the ith (co)inductive type of the block named kn + The array of terms correspond to the variables introduced in the section *) +val mkInd : inductive -> constr + +(** 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 *) +val mkConstruct : constructor -> constr + +(** Constructs a destructor of inductive type. + + [mkCase ci p c ac] stand for match [c] as [x] in [I args] return [p] with [ac] + presented as describe in [ci]. + + [p] stucture is [fun args x -> "return clause"] + + [ac]{^ ith} element is ith constructor case presented as + {e lambda construct_args (without params). case_term } *) +val mkCase : case_info * constr * constr * constr array -> constr + +(** If [recindxs = [|i1,...in|]] + [funnames = [|f1,.....fn|]] + [typarray = [|t1,...tn|]] + [bodies = [|b1,.....bn|]] + then [mkFix ((recindxs,i), funnames, typarray, bodies) ] + constructs the {% $ %}i{% $ %}th function of the block (counting from 0) + + [Fixpoint f1 [ctx1] = b1 + with f2 [ctx2] = b2 + ... + with fn [ctxn] = bn.] + + where the length of the {% $ %}j{% $ %}th context is {% $ %}ij{% $ %}. +*) +type rec_declaration = Name.t array * types array * constr array +type fixpoint = (int array * int) * rec_declaration +val mkFix : fixpoint -> constr + +(** If [funnames = [|f1,.....fn|]] + [typarray = [|t1,...tn|]] + [bodies = [b1,.....bn]] + then [mkCoFix (i, (funnames, typarray, bodies))] + constructs the ith function of the block + + [CoFixpoint f1 = b1 + with f2 = b2 + ... + with fn = bn.] + *) +type cofixpoint = int * rec_declaration +val mkCoFix : cofixpoint -> constr + + +(** {6 Concrete type for making pattern-matching. } *) + +(** [constr array] is an instance matching definitional [named_context] in + the same order (i.e. last argument first) *) +type 'constr pexistential = existential_key * 'constr array +type ('constr, 'types) prec_declaration = + Name.t array * 'types array * 'constr array +type ('constr, 'types) pfixpoint = + (int array * int) * ('constr, 'types) prec_declaration +type ('constr, 'types) pcofixpoint = + int * ('constr, 'types) prec_declaration + +type ('constr, 'types) kind_of_term = + | Rel of int + | Var of Id.t + | Meta of metavariable + | Evar of 'constr pexistential + | Sort of Sorts.t + | 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 constant + | Ind of inductive + | Construct of constructor + | Case of case_info * 'constr * 'constr * 'constr array + | Fix of ('constr, 'types) pfixpoint + | CoFix of ('constr, 'types) pcofixpoint + +(** User view of [constr]. For [App], it is ensured there is at + least one argument and the function is not itself an applicative + term *) + +val kind : constr -> (constr, types) kind_of_term + +(** [equal a b] is true if [a] equals [b] modulo alpha, casts, + and application grouping *) +val equal : constr -> constr -> bool + +(** Total ordering compatible with [equal] *) +val compare : constr -> constr -> int + +(** {6 Functionals working on the immediate subterm of a construction } *) + +(** [fold f acc c] folds [f] on the immediate subterms of [c] + starting from [acc] and proceeding from left to right according to + the usual representation of the constructions; it is not recursive *) + +val fold : ('a -> constr -> 'a) -> 'a -> constr -> 'a + +(** [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 *) + +val map : (constr -> constr) -> constr -> constr + +(** [map_with_binders g f n c] maps [f n] on the immediate + subterms of [c]; 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 and the order with which + subterms are processed is not specified *) + +val map_with_binders : + ('a -> 'a) -> ('a -> constr -> constr) -> 'a -> constr -> constr + +(** [iter f c] iters [f] on the immediate subterms of [c]; it is + not recursive and the order with which subterms are processed is + not specified *) + +val iter : (constr -> unit) -> constr -> unit + +(** [iter_with_binders g f n c] iters [f n] on the immediate + subterms of [c]; 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 and the order with which + subterms are processed is not specified *) + +val iter_with_binders : + ('a -> 'a) -> ('a -> constr -> unit) -> 'a -> constr -> unit + +(** [compare_head f c1 c2] compare [c1] and [c2] using [f] to compare + the immediate subterms of [c1] of [c2] if needed; Cast's, binders + name and Cases annotations are not taken into account *) + +val compare_head : (constr -> constr -> bool) -> constr -> constr -> bool + +(** {6 Hashconsing} *) + +val hash : constr -> int + +(*********************************************************************) + +val hcons : constr -> constr + +(**************************************) + +type values diff --git a/kernel/context.ml b/kernel/context.ml new file mode 100644 index 000000000..4bc268da1 --- /dev/null +++ b/kernel/context.ml @@ -0,0 +1,64 @@ +(************************************************************************) +(* v * The Coq Proof Assistant / The Coq Development Team *) +(* decl + | n, _ :: sign -> lookup_rel (n-1) sign + | _, [] -> raise Not_found + +let rel_context_length = List.length + +let rel_context_nhyps hyps = + let rec nhyps acc = function + | [] -> acc + | (_,None,_)::hyps -> nhyps (1+acc) hyps + | (_,Some _,_)::hyps -> nhyps acc hyps in + nhyps 0 hyps diff --git a/kernel/context.mli b/kernel/context.mli new file mode 100644 index 000000000..32efb743a --- /dev/null +++ b/kernel/context.mli @@ -0,0 +1,60 @@ +(************************************************************************) +(* v * The Coq Proof Assistant / The Coq Development Team *) +(* Constr.t) -> named_declaration -> named_declaration +val map_rel_declaration : + (Constr.t -> Constr.t) -> rel_declaration -> rel_declaration + +val fold_named_declaration : + (Constr.t -> 'a -> 'a) -> named_declaration -> 'a -> 'a +val fold_rel_declaration : + (Constr.t -> 'a -> 'a) -> rel_declaration -> 'a -> 'a + +val exists_named_declaration : + (Constr.t -> bool) -> named_declaration -> bool +val exists_rel_declaration : + (Constr.t -> bool) -> rel_declaration -> bool + +val for_all_named_declaration : + (Constr.t -> bool) -> named_declaration -> bool +val for_all_rel_declaration : + (Constr.t -> bool) -> rel_declaration -> bool + +val eq_named_declaration : + named_declaration -> named_declaration -> bool + +val eq_rel_declaration : + rel_declaration -> rel_declaration -> bool + +(** {6 Contexts of declarations referred to by de Bruijn indices } *) + +(** In [rel_context], more recent declaration is on top *) +type rel_context = rel_declaration list + +val empty_rel_context : rel_context +val add_rel_decl : rel_declaration -> rel_context -> rel_context + +val lookup_rel : int -> rel_context -> rel_declaration +(** Size of the [rel_context] including LetIns *) +val rel_context_length : rel_context -> int +(** Size of the [rel_context] without LetIns *) +val rel_context_nhyps : rel_context -> int diff --git a/kernel/cooking.ml b/kernel/cooking.ml index 0ff7d64f0..0851f682d 100644 --- a/kernel/cooking.ml +++ b/kernel/cooking.ml @@ -17,6 +17,7 @@ open Errors open Util open Names open Term +open Context open Sign open Declarations open Environ diff --git a/kernel/csymtable.ml b/kernel/csymtable.ml index 5dd4cb570..d00a20a80 100644 --- a/kernel/csymtable.ml +++ b/kernel/csymtable.ml @@ -14,6 +14,7 @@ open Names open Term +open Context open Vm open Cemitcodes open Cbytecodes diff --git a/kernel/declarations.mli b/kernel/declarations.mli index 3a05f9309..5d9eaa928 100644 --- a/kernel/declarations.mli +++ b/kernel/declarations.mli @@ -8,6 +8,7 @@ open Names open Term +open Context (** This module defines the internal representation of global declarations. This includes global constants/axioms, mutual diff --git a/kernel/environ.ml b/kernel/environ.ml index 0063aa6f2..d3b223505 100644 --- a/kernel/environ.ml +++ b/kernel/environ.ml @@ -23,9 +23,11 @@ open Errors open Util open Names +open Term +open Context open Sign +open Vars open Univ -open Term open Declarations open Pre_env diff --git a/kernel/environ.mli b/kernel/environ.mli index d2ca7b3da..ffe28ddc4 100644 --- a/kernel/environ.mli +++ b/kernel/environ.mli @@ -8,6 +8,7 @@ open Names open Term +open Context open Declarations open Sign diff --git a/kernel/indtypes.ml b/kernel/indtypes.ml index 57e638982..77675bd58 100644 --- a/kernel/indtypes.ml +++ b/kernel/indtypes.ml @@ -11,6 +11,8 @@ open Util open Names open Univ open Term +open Vars +open Context open Declarations open Declareops open Inductive diff --git a/kernel/inductive.ml b/kernel/inductive.ml index b93237679..ef4416061 100644 --- a/kernel/inductive.ml +++ b/kernel/inductive.ml @@ -11,6 +11,8 @@ open Util open Names open Univ open Term +open Vars +open Context open Declarations open Declareops open Environ diff --git a/kernel/inductive.mli b/kernel/inductive.mli index abf5e6c2c..9a458f02a 100644 --- a/kernel/inductive.mli +++ b/kernel/inductive.mli @@ -9,6 +9,7 @@ open Names open Univ open Term +open Context open Declarations open Environ diff --git a/kernel/kernel.mllib b/kernel/kernel.mllib index ef3ef6d94..421003560 100644 --- a/kernel/kernel.mllib +++ b/kernel/kernel.mllib @@ -1,6 +1,10 @@ Names Univ Esubst +Sorts +Constr +Context +Vars Term Mod_subst Sign diff --git a/kernel/nativecode.ml b/kernel/nativecode.ml index dcf56a23c..f112393cd 100644 --- a/kernel/nativecode.ml +++ b/kernel/nativecode.ml @@ -6,8 +6,9 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) open Errors -open Term open Names +open Term +open Context open Declarations open Util open Nativevalues diff --git a/kernel/pre_env.ml b/kernel/pre_env.ml index f365d19c3..922fbae92 100644 --- a/kernel/pre_env.ml +++ b/kernel/pre_env.ml @@ -15,6 +15,7 @@ open Util open Names +open Context open Sign open Univ open Term diff --git a/kernel/pre_env.mli b/kernel/pre_env.mli index 569e8830a..d3d500b2c 100644 --- a/kernel/pre_env.mli +++ b/kernel/pre_env.mli @@ -10,6 +10,7 @@ open Names open Sign open Univ open Term +open Context open Declarations (** The type of environments. *) diff --git a/kernel/reduction.ml b/kernel/reduction.ml index 7a14e57cc..1f5a6a6a0 100644 --- a/kernel/reduction.ml +++ b/kernel/reduction.ml @@ -19,6 +19,8 @@ open Errors open Util open Names open Term +open Vars +open Context open Univ open Environ open Closure diff --git a/kernel/reduction.mli b/kernel/reduction.mli index 9d1d12573..3f958dc9d 100644 --- a/kernel/reduction.mli +++ b/kernel/reduction.mli @@ -7,6 +7,7 @@ (************************************************************************) open Term +open Context open Environ open Closure diff --git a/kernel/sign.ml b/kernel/sign.ml index 3fced7119..66c872f12 100644 --- a/kernel/sign.ml +++ b/kernel/sign.ml @@ -18,6 +18,7 @@ open Names open Util open Term +open Context (*s Signatures of named hypotheses. Used for section variables and goal assumptions. *) @@ -71,7 +72,7 @@ let iter_named_context f = List.iter (fun (_,b,t) -> f t; Option.iter f b) (* Push named declarations on top of a rel context *) (* Bizarre. Should be avoided. *) -let push_named_to_rel_context hyps ctxt = +(*let push_named_to_rel_context hyps ctxt = let rec push = function | (id,b,t) :: l -> let s, hyps = push l in @@ -84,4 +85,4 @@ let push_named_to_rel_context hyps ctxt = let n, ctxt = subst l in (n+1), (map_rel_declaration (substn_vars n s) d)::ctxt | [] -> 1, hyps in - snd (subst ctxt) + snd (subst ctxt)*) diff --git a/kernel/sign.mli b/kernel/sign.mli index 6239ab5dc..6e581df34 100644 --- a/kernel/sign.mli +++ b/kernel/sign.mli @@ -8,6 +8,9 @@ open Names open Term +open Context + +(** TODO: Merge this with Context *) (** {6 Signatures of ordered named declarations } *) @@ -41,7 +44,7 @@ val instance_from_named_context : named_context -> constr array (** Signatures of ordered optionally named variables, intended to be accessed by de Bruijn indices *) -val push_named_to_rel_context : named_context -> rel_context -> rel_context +(* val push_named_to_rel_context : named_context -> rel_context -> rel_context *) (** {6 Recurrence on [rel_context]: older declarations processed first } *) val fold_rel_context : diff --git a/kernel/sorts.ml b/kernel/sorts.ml new file mode 100644 index 000000000..7ab6b553a --- /dev/null +++ b/kernel/sorts.ml @@ -0,0 +1,64 @@ +(************************************************************************) +(* v * The Coq Proof Assistant / The Coq Development Team *) +(* + begin match c1, c2 with + | Pos, Pos | Null, Null -> 0 + | Pos, Null -> -1 + | Null, Pos -> 1 + end + | Type u1, Type u2 -> Universe.compare u1 u2 + | Prop _, Type _ -> -1 + | Type _, Prop _ -> 1 + +let equal s1 s2 = Int.equal (compare s1 s2) 0 + +let is_prop = function +| Prop Null -> true +| _ -> false + +let family = function + | Prop Null -> InProp + | Prop Pos -> InSet + | Type _ -> InType + +module Hsorts = + Hashcons.Make( + struct + type _t = t + type t = _t + type u = universe -> universe + let hashcons huniv = function + Prop c -> Prop c + | Type u -> Type (huniv u) + let equal 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 = Hashcons.simple_hcons Hsorts.generate hcons_univ diff --git a/kernel/sorts.mli b/kernel/sorts.mli new file mode 100644 index 000000000..f15b7cba4 --- /dev/null +++ b/kernel/sorts.mli @@ -0,0 +1,29 @@ +(************************************************************************) +(* v * The Coq Proof Assistant / The Coq Development Team *) +(* t -> bool +val compare : t -> t -> int + +val is_prop : t -> bool +val family : t -> family + +val hcons : t -> t diff --git a/kernel/term.ml b/kernel/term.ml index 82d534a33..258f8423c 100644 --- a/kernel/term.ml +++ b/kernel/term.ml @@ -6,106 +6,63 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(* File initially created by Gérard Huet and Thierry Coquand in 1984 *) -(* Extension to inductive constructions by Christine Paulin for Coq V5.6 *) -(* Extension to mutual inductive constructions by Christine Paulin for - Coq V5.10.2 *) -(* Extension to co-inductive constructions by Eduardo Gimenez *) -(* Optimization of substitution functions by Chet Murthy *) -(* Optimization of lifting functions by Bruno Barras, Mar 1997 *) -(* Hash-consing by Bruno Barras in Feb 1998 *) -(* Restructuration of Coq of the type-checking kernel by Jean-Christophe - Filliâtre, 1999 *) -(* Abstraction of the syntax of terms and iterators by Hugo Herbelin, 2000 *) -(* Cleaning and lightening of the kernel by Bruno Barras, Nov 2001 *) - -(* This file defines the internal syntax of the Calculus of - Inductive Constructions (CIC) terms together with constructors, - destructors, iterators and basic functions *) - -open Errors open Util open Pp +open Errors open Names -open Univ -open Esubst - +open Context +open Vars -type existential_key = int -type metavariable = int +(**********************************************************************) +(** Redeclaration of types from module Constr *) +(**********************************************************************) -(* This defines the strategy to use for verifiying a Cast *) -(* Warning: REVERTcast is not exported to vo-files; as of r14492, it has to *) -(* come after the vo-exported cast_kind so as to be compatible with coqchk *) -type cast_kind = VMcast | NATIVEcast | DEFAULTcast | REVERTcast +type contents = Sorts.contents = Pos | Null -(* This defines Cases annotations *) -type case_style = LetStyle | IfStyle | LetPatternStyle | MatchStyle | RegularStyle -type case_printing = - { ind_nargs : int; (* length of the arity of the inductive type *) - style : case_style } -type case_info = - { ci_ind : inductive; - ci_npar : int; - ci_cstr_ndecls : int array; (* number of pattern vars of each constructor *) - ci_pp_info : case_printing (* not interpreted by the kernel *) - } +type sorts = Sorts.t = + | Prop of contents (** Prop and Set *) + | Type of Univ.universe (** Type *) -(* Sorts. *) +type sorts_family = Sorts.family = InProp | InSet | InType -type contents = Pos | Null +type constr = Constr.t +(** Alias types, for compatibility. *) -type sorts = - | Prop of contents (* proposition types *) - | Type of universe +type types = Constr.t +(** Same as [constr], for documentation purposes. *) -let prop_sort = Prop Null -let set_sort = Prop Pos -let type1_sort = Type type1_univ +type existential_key = Constr.existential_key -let sorts_ord s1 s2 = - if s1 == s2 then 0 else - match s1, s2 with - | Prop c1, Prop c2 -> - begin match c1, c2 with - | Pos, Pos | Null, Null -> 0 - | Pos, Null -> -1 - | Null, Pos -> 1 - end - | Type u1, Type u2 -> Universe.compare u1 u2 - | Prop _, Type _ -> -1 - | Type _, Prop _ -> 1 +type existential = Constr.existential -let sorts_eq s1 s2 = Int.equal (sorts_ord s1 s2) 0 +type metavariable = Constr.metavariable -let is_prop_sort = function -| Prop Null -> true -| _ -> false +type case_style = Constr.case_style = + LetStyle | IfStyle | LetPatternStyle | MatchStyle | RegularStyle -type sorts_family = InProp | InSet | InType +type case_printing = Constr.case_printing = + { ind_nargs : int; style : case_style } -let family_of_sort = function - | Prop Null -> InProp - | Prop Pos -> InSet - | Type _ -> InType +type case_info = Constr.case_info = + { ci_ind : inductive; + ci_npar : int; + ci_cstr_ndecls : int array; + ci_pp_info : case_printing + } -(********************************************************************) -(* Constructions as implemented *) -(********************************************************************) +type cast_kind = Constr.cast_kind = + VMcast | NATIVEcast | DEFAULTcast | REVERTcast -(* [constr array] is an instance matching definitional [named_context] in - the same order (i.e. last argument first) *) -type 'constr pexistential = existential_key * 'constr array +type rec_declaration = Constr.rec_declaration +type fixpoint = Constr.fixpoint +type cofixpoint = Constr.cofixpoint +type 'constr pexistential = 'constr Constr.pexistential type ('constr, 'types) prec_declaration = - Name.t array * 'types array * 'constr array -type ('constr, 'types) pfixpoint = - (int array * int) * ('constr, 'types) prec_declaration -type ('constr, 'types) pcofixpoint = - int * ('constr, 'types) prec_declaration - -(* [Var] is used for named variables and [Rel] for variables as - de Bruijn indices. *) -type ('constr, 'types) kind_of_term = + ('constr, 'types) Constr.prec_declaration +type ('constr, 'types) pfixpoint = ('constr, 'types) Constr.pfixpoint +type ('constr, 'types) pcofixpoint = ('constr, 'types) Constr.pcofixpoint + +type ('constr, 'types) kind_of_term = ('constr, 'types) Constr.kind_of_term = | Rel of int | Var of Id.t | Meta of metavariable @@ -123,148 +80,62 @@ type ('constr, 'types) kind_of_term = | Fix of ('constr, 'types) pfixpoint | CoFix of ('constr, 'types) pcofixpoint -(* constr is the fixpoint of the previous type. Requires option - -rectypes of the Caml compiler to be set *) -type constr = (constr,constr) kind_of_term - -type existential = existential_key * constr array -type rec_declaration = Name.t array * constr array * constr array -type fixpoint = (int array * int) * rec_declaration -type cofixpoint = int * rec_declaration - - -(*********************) -(* Term constructors *) -(*********************) - -(* Constructs a DeBrujin 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|] - -let mkRel n = if 0 mkProp (* Easy sharing *) - | Prop Pos -> mkSet - | s -> Sort s - -(* Constructs the term t1::t2, i.e. the term t1 casted with the type t2 *) -(* (that means t2 is declared as the type of t1) *) -let mkCast (t1,k2,t2) = - match t1 with - | Cast (c,k1, _) when (k1 == VMcast || k1 == NATIVEcast) && k1 == k2 -> Cast (c,k1,t2) - | _ -> Cast (t1,k2,t2) - -(* Constructs the product (x:t1)t2 *) -let mkProd (x,t1,t2) = Prod (x,t1,t2) - -(* Constructs the abstraction [x:t1]t2 *) -let mkLambda (x,t1,t2) = Lambda (x,t1,t2) - -(* Constructs [x=c_1:t]c_2 *) -let mkLetIn (x,c1,t,c2) = LetIn (x,c1,t,c2) - -(* If lt = [t1; ...; tn], constructs the application (t1 ... tn) *) -(* We ensure applicative terms have at least one argument and the - function is not itself an applicative term *) -let mkApp (f, a) = - if Int.equal (Array.length a) 0 then f else - match f with - | App (g, cl) -> App (g, Array.append cl a) - | _ -> App (f, a) - -(* Constructs a constant *) -let mkConst c = Const 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 - -(* 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 - -(* Constructs the term

Case c of c1 | c2 .. | cn end *) -let mkCase (ci, p, c, ac) = Case (ci, p, c, ac) - -(* If recindxs = [|i1,...in|] - funnames = [|f1,...fn|] - typarray = [|t1,...tn|] - bodies = [|b1,...bn|] - then - - mkFix ((recindxs,i),(funnames,typarray,bodies)) +type values = Constr.values - constructs the ith function of the block - - Fixpoint f1 [ctx1] : t1 := b1 - with f2 [ctx2] : t2 := b2 - ... - with fn [ctxn] : tn := bn. - - where the length of the jth context is ij. -*) - -let mkFix fix = Fix fix - -(* If funnames = [|f1,...fn|] - typarray = [|t1,...tn|] - bodies = [|b1,...bn|] - then - - mkCoFix (i,(funnames,typsarray,bodies)) - - constructs the ith function of the block - - CoFixpoint f1 : t1 := b1 - with f2 : t2 := b2 - ... - with fn : tn := bn. -*) -let mkCoFix cofix= CoFix cofix - -(* Constructs an existential variable named "?n" *) -let mkMeta n = Meta n - -(* Constructs a Variable named id *) -let mkVar id = Var id - - -(************************************************************************) -(* kind_of_term = constructions as seen by the user *) -(************************************************************************) +(**********************************************************************) +(** Redeclaration of functions from module Constr *) +(**********************************************************************) -(* User view of [constr]. For [App], it is ensured there is at - least one argument and the function is not itself an applicative - term *) +let set_sort = Sorts.set +let prop_sort = Sorts.prop +let type1_sort = Sorts.type1 +let sorts_ord = Sorts.compare +let is_prop_sort = Sorts.is_prop +let family_of_sort = Sorts.family + +(** {6 Term constructors. } *) + +let mkRel = Constr.mkRel +let mkVar = Constr.mkVar +let mkMeta = Constr.mkMeta +let mkEvar = Constr.mkEvar +let mkSort = Constr.mkSort +let mkProp = Constr.mkProp +let mkSet = Constr.mkSet +let mkType = Constr.mkType +let mkCast = Constr.mkCast +let mkProd = Constr.mkProd +let mkLambda = Constr.mkLambda +let mkLetIn = Constr.mkLetIn +let mkApp = Constr.mkApp +let mkConst = Constr.mkConst +let mkInd = Constr.mkInd +let mkConstruct = Constr.mkConstruct +let mkCase = Constr.mkCase +let mkFix = Constr.mkFix +let mkCoFix = Constr.mkCoFix -let kind_of_term c = c +(**********************************************************************) +(** Aliases of functions from module Constr *) +(**********************************************************************) -(* Experimental, used in Presburger contrib *) -type ('constr, 'types) kind_of_type = - | SortType of sorts - | CastType of 'types * 'types - | ProdType of Name.t * 'types * 'types - | LetInType of Name.t * 'constr * 'types * 'types - | AtomicType of 'constr * 'constr array +let eq_constr = Constr.equal +let kind_of_term = Constr.kind +let constr_ord = Constr.compare +let fold_constr = Constr.fold +let map_constr = Constr.map +let map_constr_with_binders = Constr.map_with_binders +let iter_constr = Constr.iter +let iter_constr_with_binders = Constr.iter_with_binders +let compare_constr = Constr.compare_head +let hash_constr = Constr.hash +let hcons_sorts = Sorts.hcons +let hcons_constr = Constr.hcons +let hcons_types = Constr.hcons -let kind_of_type = function - | Sort s -> SortType s - | Cast (c,_,t) -> CastType (c, t) - | Prod (na,t,c) -> ProdType (na, t, c) - | LetIn (na,b,t,c) -> LetInType (na, b, t, c) - | App (c,l) -> AtomicType (c, l) - | (Rel _ | Meta _ | Var _ | Evar _ | Const _ | Case _ | Fix _ | CoFix _ | Ind _ as c) - -> AtomicType (c,[||]) - | (Lambda _ | Construct _) -> failwith "Not a type" +(**********************************************************************) +(** HERE BEGINS THE INTERESTING STUFF *) +(**********************************************************************) (**********************************************************************) (* Non primitive term destructors *) @@ -438,7 +309,7 @@ let rec strip_outer_cast c = match kind_of_term c with | Cast (c,_,_) -> strip_outer_cast c | _ -> c -(* Fonction spéciale qui laisse les cast clés sous les Fix ou les Case *) +(* Fonction spéciale qui laisse les cast clés sous les Fix ou les Case *) let under_outer_cast f c = match kind_of_term c with | Cast (b,k,t) -> mkCast (f b, k, f t) @@ -457,8 +328,8 @@ let collapse_appl c = match kind_of_term c with | App (f,cl) -> let rec collapse_rec f cl2 = match kind_of_term (strip_outer_cast f) with - | App (g,cl1) -> collapse_rec g (Array.append cl1 cl2) - | _ -> mkApp (f,cl2) + | App (g,cl1) -> collapse_rec g (Array.append cl1 cl2) + | _ -> mkApp (f,cl2) in collapse_rec f cl | _ -> c @@ -468,431 +339,10 @@ let decompose_app c = | App (f,cl) -> (f, Array.to_list cl) | _ -> (c,[]) -(****************************************************************************) -(* Functions to recur through subterms *) -(****************************************************************************) - -(* [fold_constr f acc c] folds [f] on the immediate subterms of [c] - starting from [acc] and proceeding from left to right according to - the usual representation of the constructions; it is not recursive *) - -let fold_constr f acc c = match kind_of_term c with - | (Rel _ | Meta _ | Var _ | Sort _ | Const _ | Ind _ - | Construct _) -> acc - | Cast (c,_,t) -> f (f acc c) t - | Prod (_,t,c) -> f (f acc t) c - | 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 - | 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)) -> - let fd = Array.map3 (fun na t b -> (na,t,b)) lna tl bl in - Array.fold_left (fun acc (na,t,b) -> f (f acc t) b) acc fd - | CoFix (_,(lna,tl,bl)) -> - let fd = Array.map3 (fun na t b -> (na,t,b)) lna tl bl in - Array.fold_left (fun acc (na,t,b) -> f (f acc t) b) acc fd - -(* [iter_constr f c] iters [f] on the immediate subterms of [c]; it is - not recursive and the order with which subterms are processed is - not specified *) - -let iter_constr f c = match kind_of_term c with - | (Rel _ | Meta _ | Var _ | Sort _ | Const _ | Ind _ - | Construct _) -> () - | Cast (c,_,t) -> f c; f t - | Prod (_,t,c) -> f t; f c - | 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 - | 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 - | CoFix (_,(_,tl,bl)) -> Array.iter f tl; Array.iter f bl - -(* [iter_constr_with_binders g f n c] iters [f n] on the immediate - subterms of [c]; 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 and the order with which - subterms are processed is not specified *) - -let iter_constr_with_binders g f n c = match kind_of_term c with - | (Rel _ | Meta _ | Var _ | Sort _ | Const _ | Ind _ - | Construct _) -> () - | Cast (c,_,t) -> f n c; f n t - | Prod (_,t,c) -> f n t; f (g n) c - | Lambda (_,t,c) -> f n t; f (g n) c - | LetIn (_,b,t,c) -> f n b; f n t; f (g n) c - | App (c,l) -> f n c; Array.iter (f n) l - | Evar (_,l) -> Array.iter (f n) l - | Case (_,p,c,bl) -> f n p; f n c; Array.iter (f n) bl - | Fix (_,(_,tl,bl)) -> - Array.iter (f n) tl; - Array.iter (f (iterate g (Array.length tl) n)) bl - | CoFix (_,(_,tl,bl)) -> - Array.iter (f n) tl; - Array.iter (f (iterate g (Array.length tl) n)) bl - -(* [map_constr 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 *) - -let map_constr f c = match kind_of_term c with - | (Rel _ | Meta _ | Var _ | Sort _ | Const _ | Ind _ - | Construct _) -> c - | Cast (c,k,t) -> mkCast (f c, k, f t) - | Prod (na,t,c) -> mkProd (na, f t, f c) - | Lambda (na,t,c) -> mkLambda (na, f t, f c) - | LetIn (na,b,t,c) -> mkLetIn (na, f b, f t, f c) - | App (c,l) -> mkApp (f c, Array.map f l) - | Evar (e,l) -> mkEvar (e, Array.map f l) - | Case (ci,p,c,bl) -> mkCase (ci, f p, f c, Array.map f bl) - | Fix (ln,(lna,tl,bl)) -> - mkFix (ln,(lna,Array.map f tl,Array.map f bl)) - | CoFix(ln,(lna,tl,bl)) -> - mkCoFix (ln,(lna,Array.map f tl,Array.map f bl)) - -(* [map_constr_with_binders g f n c] maps [f n] on the immediate - subterms of [c]; 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 and the order with which - subterms are processed is not specified *) - -let map_constr_with_binders g f l c = match kind_of_term c with - | (Rel _ | Meta _ | Var _ | Sort _ | Const _ | Ind _ - | Construct _) -> c - | Cast (c,k,t) -> mkCast (f l c, k, f l t) - | Prod (na,t,c) -> mkProd (na, f l t, f (g l) c) - | Lambda (na,t,c) -> mkLambda (na, f l t, f (g l) c) - | LetIn (na,b,t,c) -> mkLetIn (na, f l b, f l t, f (g l) c) - | App (c,al) -> mkApp (f l c, Array.map (f l) al) - | Evar (e,al) -> mkEvar (e, Array.map (f l) al) - | Case (ci,p,c,bl) -> mkCase (ci, f l p, f l c, Array.map (f l) bl) - | Fix (ln,(lna,tl,bl)) -> - let l' = iterate g (Array.length tl) l in - mkFix (ln,(lna,Array.map (f l) tl,Array.map (f l') bl)) - | CoFix(ln,(lna,tl,bl)) -> - let l' = iterate g (Array.length tl) l in - mkCoFix (ln,(lna,Array.map (f l) tl,Array.map (f l') bl)) - -(* [compare_constr f c1 c2] compare [c1] and [c2] using [f] to compare - the immediate subterms of [c1] of [c2] if needed; Cast's, - application associativity, binders name and Cases annotations are - not taken into account *) - - -let compare_constr f t1 t2 = - match kind_of_term t1, kind_of_term 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 -> Int.equal (sorts_ord s1 s2) 0 - | 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 (c1,l1), _ when isCast c1 -> f (mkApp (pi1 (destCast c1),l1)) t2 - | _, App (c2,l2) when isCast c2 -> f t1 (mkApp (pi1 (destCast 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) -> Int.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 - | 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 - -(*******************************) -(* alpha conversion functions *) -(*******************************) - -(* alpha conversion : ignore print names and casts *) - -let rec eq_constr m n = - (m == n) || compare_constr eq_constr m n - -let eq_constr m n = eq_constr m n (* to avoid tracing a recursive fun *) - -let constr_ord_int f t1 t2 = - let (=?) f g i1 i2 j1 j2= - let c = f i1 i2 in - if Int.equal c 0 then g j1 j2 else c in - let (==?) fg h i1 i2 j1 j2 k1 k2= - let c=fg i1 i2 j1 j2 in - if Int.equal c 0 then h k1 k2 else c in - let fix_cmp (a1, i1) (a2, i2) = - ((Array.compare Int.compare) =? Int.compare) a1 a2 i1 i2 - in - match kind_of_term t1, kind_of_term t2 with - | Rel n1, Rel n2 -> Int.compare n1 n2 - | Meta m1, Meta m2 -> Int.compare m1 m2 - | Var id1, Var id2 -> Id.compare id1 id2 - | Sort s1, Sort s2 -> sorts_ord s1 s2 - | Cast (c1,_,_), _ -> f c1 t2 - | _, Cast (c2,_,_) -> f t1 c2 - | Prod (_,t1,c1), Prod (_,t2,c2) - | Lambda (_,t1,c1), Lambda (_,t2,c2) -> - (f =? f) t1 t2 c1 c2 - | LetIn (_,b1,t1,c1), LetIn (_,b2,t2,c2) -> - ((f =? f) ==? f) b1 b2 t1 t2 c1 c2 - | App (c1,l1), _ when isCast c1 -> f (mkApp (pi1 (destCast c1),l1)) t2 - | _, App (c2,l2) when isCast c2 -> f t1 (mkApp (pi1 (destCast 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 - | 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)) -> - ((fix_cmp =? (Array.compare f)) ==? (Array.compare f)) - ln1 ln2 tl1 tl2 bl1 bl2 - | CoFix(ln1,(_,tl1,bl1)), CoFix(ln2,(_,tl2,bl2)) -> - ((Int.compare =? (Array.compare f)) ==? (Array.compare f)) - ln1 ln2 tl1 tl2 bl1 bl2 - | t1, t2 -> Pervasives.compare t1 t2 - -let rec constr_ord m n= - constr_ord_int constr_ord m n - -(***************************************************************************) -(* Type of assumptions *) -(***************************************************************************) - -type types = constr - -type strategy = types option - -type named_declaration = Id.t * constr option * types -type rel_declaration = Name.t * constr option * types - -let map_named_declaration f (id, (v : strategy), ty) = (id, Option.map f v, f ty) -let map_rel_declaration = map_named_declaration - -let fold_named_declaration f (_, v, ty) a = f ty (Option.fold_right f v a) -let fold_rel_declaration = fold_named_declaration - -let exists_named_declaration f (_, v, ty) = Option.cata f false v || f ty -let exists_rel_declaration f (_, v, ty) = Option.cata f false v || f ty - -let for_all_named_declaration f (_, v, ty) = Option.cata f true v && f ty -let for_all_rel_declaration f (_, v, ty) = Option.cata f true v && f ty - -let eq_named_declaration (i1, c1, t1) (i2, c2, t2) = - Id.equal i1 i2 && Option.equal eq_constr c1 c2 && eq_constr t1 t2 - -let eq_rel_declaration (n1, c1, t1) (n2, c2, t2) = - Name.equal n1 n2 && Option.equal eq_constr c1 c2 && eq_constr t1 t2 - -(***************************************************************************) -(* Type of local contexts (telescopes) *) -(***************************************************************************) - -(*s Signatures of ordered optionally named variables, intended to be - accessed by de Bruijn indices (to represent bound variables) *) - -type rel_context = rel_declaration list - -let empty_rel_context = [] - -let add_rel_decl d ctxt = d::ctxt - -let rec lookup_rel n sign = - match n, sign with - | 1, decl :: _ -> decl - | n, _ :: sign -> lookup_rel (n-1) sign - | _, [] -> raise Not_found - -let rel_context_length = List.length - -let rel_context_nhyps hyps = - let rec nhyps acc = function - | [] -> acc - | (_,None,_)::hyps -> nhyps (1+acc) hyps - | (_,Some _,_)::hyps -> nhyps acc hyps in - nhyps 0 hyps - (****************************************************************************) (* Functions for dealing with constr terms *) (****************************************************************************) -(*********************) -(* Occurring *) -(*********************) - -exception LocalOccur - -(* (closedn n M) raises FreeVar if a variable of height greater than n - occurs in M, returns () otherwise *) - -let closedn n c = - let rec closed_rec n c = match kind_of_term c with - | Rel m -> if m>n then raise LocalOccur - | _ -> iter_constr_with_binders succ closed_rec n c - in - try closed_rec n c; true with LocalOccur -> false - -(* [closed0 M] is true iff [M] is a (deBruijn) closed term *) - -let closed0 = closedn 0 - -(* (noccurn n M) returns true iff (Rel n) does NOT occur in term M *) - -let noccurn n term = - let rec occur_rec n c = match kind_of_term c with - | Rel m -> if Int.equal m n then raise LocalOccur - | _ -> iter_constr_with_binders succ occur_rec n c - in - try occur_rec n term; true with LocalOccur -> false - -(* (noccur_between n m M) returns true iff (Rel p) does NOT occur in term M - for n <= p < n+m *) - -let noccur_between n m term = - let rec occur_rec n c = match kind_of_term c with - | Rel(p) -> if n<=p && p iter_constr_with_binders succ occur_rec n c - in - try occur_rec n term; true with LocalOccur -> false - -(* Checking function for terms containing existential variables. - The function [noccur_with_meta] considers the fact that - each existential variable (as well as each isevar) - in the term appears applied to its local context, - which may contain the CoFix variables. These occurrences of CoFix variables - are not considered *) - -let noccur_with_meta n m term = - let rec occur_rec n c = match kind_of_term c with - | Rel p -> if n<=p & p - (match kind_of_term f with - | Cast (c,_,_) when isMeta c -> () - | Meta _ -> () - | _ -> iter_constr_with_binders succ occur_rec n c) - | Evar (_, _) -> () - | _ -> iter_constr_with_binders succ occur_rec n c - in - try (occur_rec n term; true) with LocalOccur -> false - - -(*********************) -(* Lifting *) -(*********************) - -(* The generic lifting function *) -let rec exliftn el c = match kind_of_term c with - | Rel i -> mkRel(reloc_rel i el) - | _ -> map_constr_with_binders el_lift exliftn el c - -(* Lifting the binding depth across k bindings *) - -let liftn n k = - match el_liftn (pred k) (el_shft n el_id) with - | ELID -> (fun c -> c) - | el -> exliftn el - -let lift n = liftn n 1 - -(*********************) -(* Substituting *) -(*********************) - -(* (subst1 M c) substitutes M for Rel(1) in c - we generalise it to (substl [M1,...,Mn] c) which substitutes in parallel - M1,...,Mn for respectively Rel(1),...,Rel(n) in c *) - -(* 1st : general case *) - -type info = Closed | Open | Unknown -type 'a substituend = { mutable sinfo: info; sit: 'a } - -let rec lift_substituend depth s = - match s.sinfo with - | Closed -> s.sit - | Open -> lift depth s.sit - | Unknown -> - s.sinfo <- if closed0 s.sit then Closed else Open; - lift_substituend depth s - -let make_substituend c = { sinfo=Unknown; sit=c } - -let substn_many lamv n c = - let lv = Array.length lamv in - if Int.equal lv 0 then c - else - let rec substrec depth c = match kind_of_term c with - | Rel k -> - if k<=depth then c - else if k-depth <= lv then lift_substituend depth lamv.(k-depth-1) - else mkRel (k-lv) - | _ -> map_constr_with_binders succ substrec depth c in - substrec n c - -(* -let substkey = Profile.declare_profile "substn_many";; -let substn_many lamv n c = Profile.profile3 substkey substn_many lamv n c;; -*) - -let substnl laml n = - substn_many (Array.map make_substituend (Array.of_list laml)) n -let substl laml = substnl laml 0 -let subst1 lam = substl [lam] - -let substnl_decl laml k = map_rel_declaration (substnl laml k) -let substl_decl laml = substnl_decl laml 0 -let subst1_decl lam = substl_decl [lam] -let substl_named_decl = substl_decl -let subst1_named_decl = subst1_decl - -(* (thin_val sigma) removes identity substitutions from sigma *) - -let rec thin_val = function - | [] -> [] - | (((id,{ sit = v }) as s)::tl) when isVar v -> - if Id.equal id (destVar v) then thin_val tl else s::(thin_val tl) - | h::tl -> h::(thin_val tl) - -(* (replace_vars sigma M) applies substitution sigma to term M *) -let replace_vars var_alist = - let var_alist = - List.map (fun (str,c) -> (str,make_substituend c)) var_alist in - let var_alist = thin_val var_alist in - let rec substrec n c = match kind_of_term c with - | Var x -> - (try lift_substituend n (List.assoc x var_alist) - with Not_found -> c) - | _ -> map_constr_with_binders succ substrec n c - in - match var_alist with - | [] -> (function x -> x) - | _ -> substrec 0 - -(* -let repvarkey = Profile.declare_profile "replace_vars";; -let replace_vars vl c = Profile.profile2 repvarkey replace_vars vl c ;; -*) - -(* (subst_var str t) substitute (VAR str) by (Rel 1) in t *) -let subst_var str = replace_vars [(str, mkRel 1)] - -(* (subst_vars [id1;...;idn] t) substitute (VAR idj) by (Rel j) in t *) -let substn_vars p vars = - let _,subst = - List.fold_left (fun (n,l) var -> ((n+1),(var,mkRel n)::l)) (p,[]) vars - in replace_vars (List.rev subst) - -let subst_vars = substn_vars 1 - (***************************) (* Other term constructors *) (***************************) @@ -997,8 +447,8 @@ let prod_app t n = match kind_of_term (strip_outer_cast t) with | Prod (_,_,b) -> subst1 n b | _ -> - errorlabstrm "prod_app" - (str"Needed a product, but didn't find one" ++ fnl ()) + errorlabstrm "prod_app" + (str"Needed a product, but didn't find one" ++ fnl ()) (* prod_appvect T [| a1 ; ... ; an |] -> (T a1 ... an) *) @@ -1177,269 +627,22 @@ let rec isArity c = | Sort _ -> true | _ -> false -(*******************) -(* hash-consing *) -(*******************) - -(* Hash-consing of [constr] does not use the module [Hashcons] because - [Hashcons] is not efficient on deep tree-like data - structures. Indeed, [Hashcons] is based the (very efficient) - generic hash function [Hashtbl.hash], which computes the hash key - through a depth bounded traversal of the data structure to be - hashed. As a consequence, for a deep [constr] like the natural - number 1000 (S (S (... (S O)))), the same hash is assigned to all - the sub [constr]s greater than the maximal depth handled by - [Hashtbl.hash]. This entails a huge number of collisions in the - hash table and leads to cubic hash-consing in this worst-case. - - In order to compute a hash key that is independent of the data - structure depth while being constant-time, an incremental hashing - function must be devised. A standard implementation creates a cache - of the hashing function by decorating each node of the hash-consed - data structure with its hash key. In that case, the hash function - can deduce the hash key of a toplevel data structure by a local - computation based on the cache held on its substructures. - Unfortunately, this simple implementation introduces a space - overhead that is damageable for the hash-consing of small [constr]s - (the most common case). One can think of an heterogeneous - distribution of caches on smartly chosen nodes, but this is forbidden - by the use of generic equality in Coq source code. (Indeed, this forces - each [constr] to have a unique canonical representation.) - - Given that hash-consing proceeds inductively, we can nonetheless - computes the hash key incrementally during hash-consing by changing - a little the signature of the hash-consing function: it now returns - both the hash-consed term and its hash key. This simple solution is - implemented in the following code: it does not introduce a space - overhead in [constr], that's why the efficiency is unchanged for - small [constr]s. Besides, it does handle deep [constr]s without - introducing an unreasonable number of collisions in the hash table. - Some benchmarks make us think that this implementation of - hash-consing is linear in the size of the hash-consed data - structure for our daily use of Coq. -*) - -let array_eqeq t1 t2 = - t1 == t2 || - (Int.equal (Array.length t1) (Array.length t2) && - let rec aux i = - (Int.equal i (Array.length t1)) || (t1.(i) == t2.(i) && aux (i + 1)) - in aux 0) - -let equals_constr t1 t2 = - match t1, t2 with - | Rel n1, Rel n2 -> n1 == n2 - | Meta m1, Meta m2 -> m1 == m2 - | Var id1, Var id2 -> id1 == id2 - | Sort s1, Sort s2 -> s1 == s2 - | Cast (c1,k1,t1), Cast (c2,k2,t2) -> c1 == c2 & k1 == k2 & t1 == t2 - | Prod (n1,t1,c1), Prod (n2,t2,c2) -> n1 == n2 & t1 == t2 & c1 == c2 - | 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 - | 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 - | 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 - | 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)) -> - Int.equal i1 i2 - && Array.equal Int.equal ln1 ln2 - && array_eqeq lna1 lna2 - && array_eqeq tl1 tl2 - && array_eqeq bl1 bl2 - | CoFix(ln1,(lna1,tl1,bl1)), CoFix(ln2,(lna2,tl2,bl2)) -> - Int.equal ln1 ln2 - & array_eqeq lna1 lna2 - & array_eqeq tl1 tl2 - & array_eqeq bl1 bl2 - | _ -> 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 *) - -module HashsetTerm = Hashset.Make(struct type t = constr let equal = equals_constr end) - -let term_table = HashsetTerm.create 19991 -(* The associative table to hashcons terms. *) - -open Hashset.Combine - -(* [hcons_term hash_consing_functions constr] computes an hash-consed - representation for [constr] using [hash_consing_functions] on - leaves. *) -let hcons_term (sh_sort,sh_ci,sh_construct,sh_ind,sh_con,sh_na,sh_id) = - - (* Note : we hash-cons constr arrays *in place* *) - - let rec hash_term_array t = - let accu = ref 0 in - for i = 0 to Array.length t - 1 do - let x, h = sh_rec t.(i) in - accu := combine !accu h; - t.(i) <- x - done; - !accu - - and hash_term t = - match t with - | Var i -> - (Var (sh_id i), combinesmall 1 (Hashtbl.hash i)) - | Sort s -> - (Sort (sh_sort s), combinesmall 2 (Hashtbl.hash s)) - | Cast (c, k, t) -> - let c, hc = sh_rec c in - let t, ht = sh_rec t in - (Cast (c, k, t), combinesmall 3 (combine3 hc (Hashtbl.hash k) ht)) - | Prod (na,t,c) -> - let t, ht = sh_rec t - and c, hc = sh_rec c in - (Prod (sh_na na, t, c), combinesmall 4 (combine3 (Hashtbl.hash na) ht hc)) - | Lambda (na,t,c) -> - let t, ht = sh_rec t - and c, hc = sh_rec c in - (Lambda (sh_na na, t, c), combinesmall 5 (combine3 (Hashtbl.hash na) ht hc)) - | LetIn (na,b,t,c) -> - let b, hb = sh_rec b in - let t, ht = sh_rec t in - let c, hc = sh_rec c in - (LetIn (sh_na na, b, t, c), combinesmall 6 (combine4 (Hashtbl.hash na) hb ht hc)) - | App (c,l) -> - let c, hc = sh_rec c in - let hl = hash_term_array l in - (App (c, l), combinesmall 7 (combine hl hc)) - | Evar (e,l) -> - let hl = hash_term_array l in - (* since the array have been hashed in place : *) - (t, combinesmall 8 (combine (Hashtbl.hash e) hl)) - | Const c -> - (Const (sh_con c), combinesmall 9 (Hashtbl.hash c)) - | Ind ((kn,i) as ind) -> - (Ind (sh_ind ind), combinesmall 10 (combine (Hashtbl.hash kn) i)) - | Construct (((kn,i),j) as c)-> - (Construct (sh_construct c), combinesmall 11 (combine3 (Hashtbl.hash kn) i j)) - | Case (ci,p,c,bl) -> - let p, hp = sh_rec p - and c, hc = sh_rec c in - let hbl = hash_term_array bl in - let hbl = combine (combine hc hp) hbl in - (Case (sh_ci ci, p, c, bl), combinesmall 12 hbl) - | Fix (ln,(lna,tl,bl)) -> - let hbl = hash_term_array bl in - let htl = hash_term_array tl in - Array.iteri (fun i x -> lna.(i) <- sh_na x) lna; - (* since the three arrays have been hashed in place : *) - (t, combinesmall 13 (combine (Hashtbl.hash lna) (combine hbl htl))) - | CoFix(ln,(lna,tl,bl)) -> - let hbl = hash_term_array bl in - let htl = hash_term_array tl in - Array.iteri (fun i x -> lna.(i) <- sh_na x) lna; - (* since the three arrays have been hashed in place : *) - (t, combinesmall 14 (combine (Hashtbl.hash lna) (combine hbl htl))) - | Meta n -> - (t, combinesmall 15 n) - | Rel n -> - (t, combinesmall 16 n) - - and sh_rec t = - let (y, h) = hash_term t in - (* [h] must be positive. *) - let h = h land 0x3FFFFFFF in - (HashsetTerm.repr h y term_table, h) +(** Kind of type *) - in - (* Make sure our statically allocated Rels (1 to 16) are considered - as canonical, and hence hash-consed to themselves *) - ignore (hash_term_array rels); - - fun t -> fst (sh_rec t) - -(* Exported hashing fonction on constr, used mainly in plugins. - Appears to have slight differences from [snd (hash_term t)] above ? *) - -let rec hash_constr t = - match kind_of_term t with - | Var i -> combinesmall 1 (Hashtbl.hash i) - | Sort s -> combinesmall 2 (Hashtbl.hash s) - | Cast (c, _, _) -> hash_constr c - | Prod (_, t, c) -> combinesmall 4 (combine (hash_constr t) (hash_constr c)) - | Lambda (_, t, c) -> combinesmall 5 (combine (hash_constr t) (hash_constr c)) - | LetIn (_, b, t, c) -> - combinesmall 6 (combine3 (hash_constr b) (hash_constr t) (hash_constr c)) - | App (c,l) when isCast c -> hash_constr (mkApp (pi1 (destCast c),l)) - | App (c,l) -> - combinesmall 7 (combine (hash_term_array l) (hash_constr c)) - | Evar (e,l) -> - combinesmall 8 (combine (Hashtbl.hash e) (hash_term_array l)) - | Const c -> - combinesmall 9 (Hashtbl.hash c) (* TODO: proper hash function for constants *) - | Ind (kn,i) -> - combinesmall 10 (combine (Hashtbl.hash kn) i) - | Construct ((kn,i),j) -> - combinesmall 11 (combine3 (Hashtbl.hash kn) i j) - | Case (_ , p, c, bl) -> - combinesmall 12 (combine3 (hash_constr c) (hash_constr p) (hash_term_array bl)) - | Fix (ln ,(_, tl, bl)) -> - combinesmall 13 (combine (hash_term_array bl) (hash_term_array tl)) - | CoFix(ln, (_, tl, bl)) -> - combinesmall 14 (combine (hash_term_array bl) (hash_term_array tl)) - | Meta n -> combinesmall 15 n - | Rel n -> combinesmall 16 n - -and hash_term_array t = - Array.fold_left (fun acc t -> combine (hash_constr t) acc) 0 t - -module Hsorts = - Hashcons.Make( - struct - type t = sorts - type u = universe -> universe - let hashcons huniv = function - Prop c -> Prop c - | Type u -> Type (huniv u) - let equal s1 s2 = - match (s1,s2) with - (Prop c1, Prop c2) -> c1 == c2 - | (Type u1, Type u2) -> u1 == u2 - |_ -> false - let hash = Hashtbl.hash - end) - -module Hcaseinfo = - Hashcons.Make( - struct - type t = case_info - type u = inductive -> inductive - let hashcons hind ci = { ci with ci_ind = hind ci.ci_ind } - let pp_info_equal info1 info2 = - Int.equal info1.ind_nargs info2.ind_nargs && - info1.style == info2.style - let equal ci ci' = - ci.ci_ind == ci'.ci_ind && - Int.equal ci.ci_npar ci'.ci_npar && - Array.equal Int.equal ci.ci_cstr_ndecls ci'.ci_cstr_ndecls && (* we use [Array.equal] on purpose *) - pp_info_equal ci.ci_pp_info ci'.ci_pp_info (* we use (=) on purpose *) - 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_constr = - hcons_term - (hcons_sorts, - hcons_caseinfo, - hcons_construct, - hcons_ind, - hcons_con, - Name.hcons, - Id.hcons) - -let hcons_types = hcons_constr - -(*******) -(* Type of abstract machine values *) -type values +(* Experimental, used in Presburger contrib *) +type ('constr, 'types) kind_of_type = + | SortType of sorts + | CastType of 'types * 'types + | ProdType of Name.t * 'types * 'types + | LetInType of Name.t * 'constr * 'types * 'types + | AtomicType of 'constr * 'constr array + +let kind_of_type t = match kind_of_term t with + | Sort s -> SortType s + | Cast (c,_,t) -> CastType (c, t) + | Prod (na,t,c) -> ProdType (na, t, c) + | LetIn (na,b,t,c) -> LetInType (na, b, t, c) + | App (c,l) -> AtomicType (c, l) + | (Rel _ | Meta _ | Var _ | Evar _ | Const _ | Case _ | Fix _ | CoFix _ | Ind _) + -> AtomicType (t,[||]) + | (Lambda _ | Construct _) -> failwith "Not a type" diff --git a/kernel/term.mli b/kernel/term.mli index e585e66b7..a3745d5e3 100644 --- a/kernel/term.mli +++ b/kernel/term.mli @@ -7,195 +7,61 @@ (************************************************************************) open Names +open Context +(** {5 Redeclaration of types from module Constr and Sorts} -(** {6 The sorts of CCI. } *) + This reexports constructors of inductive types defined in module [Constr], + for compatibility purposes. Refer to this module for further info. -type contents = Pos | Null +*) + +type contents = Sorts.contents = Pos | Null -type sorts = +type sorts = Sorts.t = | Prop of contents (** Prop and Set *) | Type of Univ.universe (** Type *) -val set_sort : sorts -val prop_sort : sorts -val type1_sort : sorts - -val sorts_ord : sorts -> sorts -> int -val is_prop_sort : sorts -> bool +type sorts_family = Sorts.family = InProp | InSet | InType -(** {6 The sorts family of CCI. } *) +type constr = Constr.constr +(** Alias types, for compatibility. *) -type sorts_family = InProp | InSet | InType +type types = Constr.types +(** Same as [constr], for documentation purposes. *) -val family_of_sort : sorts -> sorts_family +type existential_key = Constr.existential_key -(** {6 Useful types } *) +type existential = Constr.existential -(** {6 Existential variables } *) -type existential_key = int +type metavariable = Constr.metavariable -(** {6 Existential variables } *) -type metavariable = int +type case_style = Constr.case_style = + LetStyle | IfStyle | LetPatternStyle | MatchStyle | RegularStyle -(** {6 Case annotation } *) -type case_style = LetStyle | IfStyle | LetPatternStyle | MatchStyle - | RegularStyle (** infer printing form from number of constructor *) -type case_printing = - { ind_nargs : int; (** length of the arity of the inductive type *) - style : case_style } +type case_printing = Constr.case_printing = + { ind_nargs : int; style : case_style } -(** the integer is the number of real args, needed for reduction *) -type case_info = +type case_info = Constr.case_info = { ci_ind : inductive; ci_npar : int; - ci_cstr_ndecls : int array; (** number of real args of each constructor *) - ci_pp_info : case_printing (** not interpreted by the kernel *) + ci_cstr_ndecls : int array; + ci_pp_info : case_printing } -(** {6 The type of constructions } *) - -type constr - -(** [eq_constr a b] is true if [a] equals [b] modulo alpha, casts, - and application grouping *) -val eq_constr : constr -> constr -> bool - -(** [types] is the same as [constr] but is intended to be used for - documentation to indicate that such or such function specifically works - with {e types} (i.e. terms of type a sort). - (Rem:plurial form since [type] is a reserved ML keyword) *) - -type types = constr - -(** {5 Functions for dealing with constr terms. } - The following functions are intended to simplify and to uniform the - manipulation of terms. Some of these functions may be overlapped with - previous ones. *) - -(** {6 Term constructors. } *) - -(** Constructs a DeBrujin index (DB indices begin at 1) *) -val mkRel : int -> constr - -(** Constructs a Variable *) -val mkVar : Id.t -> constr - -(** Constructs an patvar named "?n" *) -val mkMeta : metavariable -> constr - -(** Constructs an existential variable *) -type existential = existential_key * constr array -val mkEvar : existential -> constr - -(** Construct a sort *) -val mkSort : sorts -> types -val mkProp : types -val mkSet : types -val mkType : Univ.universe -> types - - -(** This defines the strategy to use for verifiying a Cast *) -type cast_kind = VMcast | NATIVEcast | DEFAULTcast | REVERTcast - -(** Constructs the term [t1::t2], i.e. the term t{_ 1} casted with the - type t{_ 2} (that means t2 is declared as the type of t1). *) -val mkCast : constr * cast_kind * constr -> constr - -(** Constructs the product [(x:t1)t2] *) -val mkProd : Name.t * types * types -> types -val mkNamedProd : Id.t -> types -> types -> types - -(** non-dependent product [t1 -> t2], an alias for - [forall (_:t1), t2]. Beware [t_2] is NOT lifted. - Eg: in context [A:Prop], [A->A] is built by [(mkArrow (mkRel 0) (mkRel 1))] -*) -val mkArrow : types -> types -> constr - -(** Constructs the abstraction \[x:t{_ 1}\]t{_ 2} *) -val mkLambda : Name.t * types * constr -> constr -val mkNamedLambda : Id.t -> types -> constr -> constr - -(** Constructs the product [let x = t1 : t2 in t3] *) -val mkLetIn : Name.t * constr * types * constr -> constr -val mkNamedLetIn : Id.t -> constr -> types -> constr -> constr - -(** [mkApp (f,[| t_1; ...; t_n |]] constructs the application - {% $(f~t_1~\dots~t_n)$ %}. *) -val mkApp : constr * constr array -> constr - -(** Constructs a constant - The array of terms correspond to the variables introduced in the section *) -val mkConst : constant -> constr - -(** Inductive types *) - -(** Constructs the ith (co)inductive type of the block named kn - The array of terms correspond to the variables introduced in the section *) -val mkInd : inductive -> constr +type cast_kind = Constr.cast_kind = + VMcast | NATIVEcast | DEFAULTcast | REVERTcast -(** 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 *) -val mkConstruct : constructor -> constr - -(** Constructs a destructor of inductive type. - - [mkCase ci p c ac] stand for match [c] as [x] in [I args] return [p] with [ac] - presented as describe in [ci]. - - [p] stucture is [fun args x -> "return clause"] - - [ac]{^ ith} element is ith constructor case presented as - {e lambda construct_args (without params). case_term } *) -val mkCase : case_info * constr * constr * constr array -> constr - -(** If [recindxs = [|i1,...in|]] - [funnames = [|f1,.....fn|]] - [typarray = [|t1,...tn|]] - [bodies = [|b1,.....bn|]] - then [mkFix ((recindxs,i), funnames, typarray, bodies) ] - constructs the {% $ %}i{% $ %}th function of the block (counting from 0) - - [Fixpoint f1 [ctx1] = b1 - with f2 [ctx2] = b2 - ... - with fn [ctxn] = bn.] - - where the length of the {% $ %}j{% $ %}th context is {% $ %}ij{% $ %}. -*) -type rec_declaration = Name.t array * types array * constr array -type fixpoint = (int array * int) * rec_declaration -val mkFix : fixpoint -> constr - -(** If [funnames = [|f1,.....fn|]] - [typarray = [|t1,...tn|]] - [bodies = [b1,.....bn]] - then [mkCoFix (i, (funnames, typarray, bodies))] - constructs the ith function of the block - - [CoFixpoint f1 = b1 - with f2 = b2 - ... - with fn = bn.] - *) -type cofixpoint = int * rec_declaration -val mkCoFix : cofixpoint -> constr - - -(** {6 Concrete type for making pattern-matching. } *) - -(** [constr array] is an instance matching definitional [named_context] in - the same order (i.e. last argument first) *) -type 'constr pexistential = existential_key * 'constr array +type rec_declaration = Constr.rec_declaration +type fixpoint = Constr.fixpoint +type cofixpoint = Constr.cofixpoint +type 'constr pexistential = 'constr Constr.pexistential type ('constr, 'types) prec_declaration = - Name.t array * 'types array * 'constr array -type ('constr, 'types) pfixpoint = - (int array * int) * ('constr, 'types) prec_declaration -type ('constr, 'types) pcofixpoint = - int * ('constr, 'types) prec_declaration + ('constr, 'types) Constr.prec_declaration +type ('constr, 'types) pfixpoint = ('constr, 'types) Constr.pfixpoint +type ('constr, 'types) pcofixpoint = ('constr, 'types) Constr.pcofixpoint -type ('constr, 'types) kind_of_term = +type ('constr, 'types) kind_of_term = ('constr, 'types) Constr.kind_of_term = | Rel of int | Var of Id.t | Meta of metavariable @@ -213,23 +79,9 @@ type ('constr, 'types) kind_of_term = | Fix of ('constr, 'types) pfixpoint | CoFix of ('constr, 'types) pcofixpoint -(** User view of [constr]. For [App], it is ensured there is at - least one argument and the function is not itself an applicative - term *) - -val kind_of_term : constr -> (constr, types) kind_of_term - -(** Experimental, used in Presburger contrib *) -type ('constr, 'types) kind_of_type = - | SortType of sorts - | CastType of 'types * 'types - | ProdType of Name.t * 'types * 'types - | LetInType of Name.t * 'constr * 'types * 'types - | AtomicType of 'constr * 'constr array - -val kind_of_type : types -> (constr, types) kind_of_type +type values = Constr.values -(** {6 Simple term case analysis. } *) +(** {5 Simple term case analysis. } *) val isRel : constr -> bool val isRelN : int -> constr -> bool @@ -260,7 +112,7 @@ val iskind : constr -> bool val is_small : sorts -> bool -(** {6 Term destructors } *) +(** {5 Term destructors } *) (** Destructor operations are partial functions and @raise DestKO if the term has not the expected form. *) @@ -331,56 +183,18 @@ val destFix : constr -> fixpoint val destCoFix : constr -> cofixpoint -(** {6 Local context} *) -(** A {e declaration} has the form [(name,body,type)]. It is either an - {e assumption} if [body=None] or a {e definition} if - [body=Some actualbody]. It is referred by {e name} if [na] is an - identifier or by {e relative index} if [na] is not an identifier - (in the latter case, [na] is of type [name] but just for printing - purpose) *) - -type named_declaration = Id.t * constr option * types -type rel_declaration = Name.t * constr option * types +(** {5 Derived constructors} *) -val map_named_declaration : - (constr -> constr) -> named_declaration -> named_declaration -val map_rel_declaration : - (constr -> constr) -> rel_declaration -> rel_declaration - -val fold_named_declaration : - (constr -> 'a -> 'a) -> named_declaration -> 'a -> 'a -val fold_rel_declaration : - (constr -> 'a -> 'a) -> rel_declaration -> 'a -> 'a - -val exists_named_declaration : - (constr -> bool) -> named_declaration -> bool -val exists_rel_declaration : - (constr -> bool) -> rel_declaration -> bool - -val for_all_named_declaration : - (constr -> bool) -> named_declaration -> bool -val for_all_rel_declaration : - (constr -> bool) -> rel_declaration -> bool - -val eq_named_declaration : - named_declaration -> named_declaration -> bool - -val eq_rel_declaration : - rel_declaration -> rel_declaration -> bool - -(** {6 Contexts of declarations referred to by de Bruijn indices } *) - -(** In [rel_context], more recent declaration is on top *) -type rel_context = rel_declaration list - -val empty_rel_context : rel_context -val add_rel_decl : rel_declaration -> rel_context -> rel_context +(** non-dependent product [t1 -> t2], an alias for + [forall (_:t1), t2]. Beware [t_2] is NOT lifted. + Eg: in context [A:Prop], [A->A] is built by [(mkArrow (mkRel 0) (mkRel 1))] +*) +val mkArrow : types -> types -> constr -val lookup_rel : int -> rel_context -> rel_declaration -(** Size of the [rel_context] including LetIns *) -val rel_context_length : rel_context -> int -(** Size of the [rel_context] without LetIns *) -val rel_context_nhyps : rel_context -> int +(** Named version of the functions from [Term]. *) +val mkNamedLambda : Id.t -> types -> constr -> constr +val mkNamedLetIn : Id.t -> constr -> types -> constr -> constr +val mkNamedProd : Id.t -> types -> types -> types (** Constructs either [(x:t)c] or [[x=b:t]c] *) val mkProd_or_LetIn : rel_declaration -> types -> types @@ -392,7 +206,7 @@ val mkNamedProd_wo_LetIn : named_declaration -> types -> types val mkLambda_or_LetIn : rel_declaration -> constr -> constr val mkNamedLambda_or_LetIn : named_declaration -> constr -> constr -(** {6 Other term constructors. } *) +(** {5 Other term constructors. } *) (** [applist (f,args)] and its variants work as [mkApp] *) @@ -441,7 +255,7 @@ val prod_applist : constr -> constr list -> constr val it_mkLambda_or_LetIn : constr -> rel_context -> constr val it_mkProd_or_LetIn : types -> rel_context -> types -(** {6 Other term destructors. } *) +(** {5 Other term destructors. } *) (** Transforms a product term {% $ %}(x_1:T_1)..(x_n:T_n)T{% $ %} into the pair {% $ %}([(x_n,T_n);...;(x_1,T_1)],T){% $ %}, where {% $ %}T{% $ %} is not a product. *) @@ -512,7 +326,7 @@ val under_casts : (constr -> constr) -> constr -> constr (** Apply a function under components of Cast if any *) val under_outer_cast : (constr -> constr) -> constr -> constr -(** {6 ... } *) +(** {5 ... } *) (** An "arity" is a term of the form [[x1:T1]...[xn:Tn]s] with [s] a sort. Such a term can canonically be seen as the pair of a context of types and of a sort *) @@ -528,117 +342,102 @@ val destArity : types -> arity (** Tells if a term has the form of an arity *) val isArity : types -> bool -(** {6 Occur checks } *) +(** {5 Kind of type} *) -(** [closedn n M] is true iff [M] is a (deBruijn) closed term under n binders *) -val closedn : int -> constr -> bool - -(** [closed0 M] is true iff [M] is a (deBruijn) closed term *) -val closed0 : constr -> bool +type ('constr, 'types) kind_of_type = + | SortType of sorts + | CastType of 'types * 'types + | ProdType of Name.t * 'types * 'types + | LetInType of Name.t * 'constr * 'types * 'types + | AtomicType of 'constr * 'constr array -(** [noccurn n M] returns true iff [Rel n] does NOT occur in term [M] *) -val noccurn : int -> constr -> bool +val kind_of_type : types -> (constr, types) kind_of_type -(** [noccur_between n m M] returns true iff [Rel p] does NOT occur in term [M] - for n <= p < n+m *) -val noccur_between : int -> int -> constr -> bool +(** {5 Redeclaration of stuff from module [Sorts]} *) -(** Checking function for terms containing existential- or - meta-variables. The function [noccur_with_meta] does not consider - meta-variables applied to some terms (intended to be its local - context) (for existential variables, it is necessarily the case) *) -val noccur_with_meta : int -> int -> constr -> bool +val set_sort : sorts +(** Alias for Sorts.set *) -(** {6 Relocation and substitution } *) +val prop_sort : sorts +(** Alias for Sorts.prop *) -(** [exliftn el c] lifts [c] with lifting [el] *) -val exliftn : Esubst.lift -> constr -> constr +val type1_sort : sorts +(** Alias for Sorts.type1 *) -(** [liftn n k c] lifts by [n] indexes above or equal to [k] in [c] *) -val liftn : int -> int -> constr -> constr +val sorts_ord : sorts -> sorts -> int +(** Alias for Sorts.compare *) -(** [lift n c] lifts by [n] the positive indexes in [c] *) -val lift : int -> constr -> constr +val is_prop_sort : sorts -> bool +(** Alias for Sorts.is_prop *) -(** [substnl [a1;...;an] k c] substitutes in parallel [a1],...,[an] - for respectively [Rel(k+1)],...,[Rel(k+n)] in [c]; it relocates - accordingly indexes in [a1],...,[an] *) -val substnl : constr list -> int -> constr -> constr -val substl : constr list -> constr -> constr -val subst1 : constr -> constr -> constr +val family_of_sort : sorts -> sorts_family +(** Alias for Sorts.family *) -val substnl_decl : constr list -> int -> rel_declaration -> rel_declaration -val substl_decl : constr list -> rel_declaration -> rel_declaration -val subst1_decl : constr -> rel_declaration -> rel_declaration +(** {5 Redeclaration of stuff from module [Constr]} -val subst1_named_decl : constr -> named_declaration -> named_declaration -val substl_named_decl : constr list -> named_declaration -> named_declaration + See module [Constr] for further info. *) -val replace_vars : (Id.t * constr) list -> constr -> constr -val subst_var : Id.t -> constr -> constr +(** {6 Term constructors. } *) -(** [subst_vars [id1;...;idn] t] substitute [VAR idj] by [Rel j] in [t] - if two names are identical, the one of least indice is kept *) -val subst_vars : Id.t list -> constr -> constr +val mkRel : int -> constr +val mkVar : Id.t -> constr +val mkMeta : metavariable -> constr +val mkEvar : existential -> constr +val mkSort : sorts -> types +val mkProp : types +val mkSet : types +val mkType : Univ.universe -> types +val mkCast : constr * cast_kind * constr -> constr +val mkProd : Name.t * types * types -> types +val mkLambda : Name.t * types * constr -> constr +val mkLetIn : Name.t * constr * types * constr -> constr +val mkApp : constr * constr array -> constr +val mkConst : constant -> constr +val mkInd : inductive -> constr +val mkConstruct : constructor -> constr +val mkCase : case_info * constr * constr * constr array -> constr +val mkFix : fixpoint -> constr +val mkCoFix : cofixpoint -> constr -(** [substn_vars n [id1;...;idn] t] substitute [VAR idj] by [Rel j+n-1] in [t] - if two names are identical, the one of least indice is kept *) -val substn_vars : int -> Id.t list -> constr -> constr +(** {6 Aliases} *) +val eq_constr : constr -> constr -> bool +(** Alias for [Constr.eq] *) -(** {6 Functionals working on the immediate subterm of a construction } *) +val kind_of_term : constr -> (constr, types) kind_of_term +(** Alias for [Constr.kind] *) -(** [fold_constr f acc c] folds [f] on the immediate subterms of [c] - starting from [acc] and proceeding from left to right according to - the usual representation of the constructions; it is not recursive *) +val constr_ord : constr -> constr -> int +(** Alias for [Constr.compare] *) val fold_constr : ('a -> constr -> 'a) -> 'a -> constr -> 'a - -(** [map_constr 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 *) +(** Alias for [Constr.fold] *) val map_constr : (constr -> constr) -> constr -> constr - -(** [map_constr_with_binders g f n c] maps [f n] on the immediate - subterms of [c]; 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 and the order with which - subterms are processed is not specified *) +(** Alias for [Constr.map] *) val map_constr_with_binders : ('a -> 'a) -> ('a -> constr -> constr) -> 'a -> constr -> constr - -(** [iter_constr f c] iters [f] on the immediate subterms of [c]; it is - not recursive and the order with which subterms are processed is - not specified *) +(** Alias for [Constr.map_with_binders] *) val iter_constr : (constr -> unit) -> constr -> unit - -(** [iter_constr_with_binders g f n c] iters [f n] on the immediate - subterms of [c]; 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 and the order with which - subterms are processed is not specified *) +(** Alias for [Constr.iter] *) val iter_constr_with_binders : ('a -> 'a) -> ('a -> constr -> unit) -> 'a -> constr -> unit - -(** [compare_constr f c1 c2] compare [c1] and [c2] using [f] to compare - the immediate subterms of [c1] of [c2] if needed; Cast's, binders - name and Cases annotations are not taken into account *) +(** Alias for [Constr.iter_with_binders] *) val compare_constr : (constr -> constr -> bool) -> constr -> constr -> bool +(** Alias for [Constr.compare_head] *) -val constr_ord : constr -> constr -> int val hash_constr : constr -> int - -(*********************************************************************) +(** Alias for [Constr.hash] *) val hcons_sorts : sorts -> sorts -val hcons_constr : constr -> constr -val hcons_types : types -> types +(** Alias for [Constr.hashcons_sorts] *) -(**************************************) +val hcons_constr : constr -> constr +(** Alias for [Constr.hashcons] *) -type values +val hcons_types : types -> types +(** Alias for [Constr.hashcons] *) diff --git a/kernel/term_typing.ml b/kernel/term_typing.ml index 67d80fa50..3653e1954 100644 --- a/kernel/term_typing.ml +++ b/kernel/term_typing.ml @@ -17,6 +17,7 @@ open Util open Names open Univ open Term +open Context open Declarations open Environ open Entries diff --git a/kernel/typeops.ml b/kernel/typeops.ml index 18e6fec79..a27ce1c47 100644 --- a/kernel/typeops.ml +++ b/kernel/typeops.ml @@ -11,6 +11,8 @@ open Util open Names open Univ open Term +open Vars +open Context open Declarations open Environ open Entries diff --git a/kernel/typeops.mli b/kernel/typeops.mli index 7617e8219..14ba95ec6 100644 --- a/kernel/typeops.mli +++ b/kernel/typeops.mli @@ -9,6 +9,7 @@ open Names open Univ open Term +open Context open Environ open Entries open Declarations diff --git a/kernel/vars.ml b/kernel/vars.ml new file mode 100644 index 000000000..1469192b1 --- /dev/null +++ b/kernel/vars.ml @@ -0,0 +1,186 @@ +(************************************************************************) +(* v * The Coq Proof Assistant / The Coq Development Team *) +(* if m>n then raise LocalOccur + | _ -> Constr.iter_with_binders succ closed_rec n c + in + try closed_rec n c; true with LocalOccur -> false + +(* [closed0 M] is true iff [M] is a (deBruijn) closed term *) + +let closed0 = closedn 0 + +(* (noccurn n M) returns true iff (Rel n) does NOT occur in term M *) + +let noccurn n term = + let rec occur_rec n c = match Constr.kind c with + | Constr.Rel m -> if Int.equal m n then raise LocalOccur + | _ -> Constr.iter_with_binders succ occur_rec n c + in + try occur_rec n term; true with LocalOccur -> false + +(* (noccur_between n m M) returns true iff (Rel p) does NOT occur in term M + for n <= p < n+m *) + +let noccur_between n m term = + let rec occur_rec n c = match Constr.kind c with + | Constr.Rel p -> if n<=p && p Constr.iter_with_binders succ occur_rec n c + in + try occur_rec n term; true with LocalOccur -> false + +(* Checking function for terms containing existential variables. + The function [noccur_with_meta] considers the fact that + each existential variable (as well as each isevar) + in the term appears applied to its local context, + which may contain the CoFix variables. These occurrences of CoFix variables + are not considered *) + +let isMeta c = match Constr.kind c with +| Constr.Meta _ -> true +| _ -> false + +let noccur_with_meta n m term = + let rec occur_rec n c = match Constr.kind c with + | Constr.Rel p -> if n<=p & p + (match Constr.kind f with + | Constr.Cast (c,_,_) when isMeta c -> () + | Constr.Meta _ -> () + | _ -> Constr.iter_with_binders succ occur_rec n c) + | Constr.Evar (_, _) -> () + | _ -> Constr.iter_with_binders succ occur_rec n c + in + try (occur_rec n term; true) with LocalOccur -> false + +(*********************) +(* Lifting *) +(*********************) + +(* The generic lifting function *) +let rec exliftn el c = match Constr.kind c with + | Constr.Rel i -> Constr.mkRel(reloc_rel i el) + | _ -> Constr.map_with_binders el_lift exliftn el c + +(* Lifting the binding depth across k bindings *) + +let liftn n k = + match el_liftn (pred k) (el_shft n el_id) with + | ELID -> (fun c -> c) + | el -> exliftn el + +let lift n = liftn n 1 + +(*********************) +(* Substituting *) +(*********************) + +(* (subst1 M c) substitutes M for Rel(1) in c + we generalise it to (substl [M1,...,Mn] c) which substitutes in parallel + M1,...,Mn for respectively Rel(1),...,Rel(n) in c *) + +(* 1st : general case *) + +type info = Closed | Open | Unknown +type 'a substituend = { mutable sinfo: info; sit: 'a } + +let rec lift_substituend depth s = + match s.sinfo with + | Closed -> s.sit + | Open -> lift depth s.sit + | Unknown -> + s.sinfo <- if closed0 s.sit then Closed else Open; + lift_substituend depth s + +let make_substituend c = { sinfo=Unknown; sit=c } + +let substn_many lamv n c = + let lv = Array.length lamv in + if Int.equal lv 0 then c + else + let rec substrec depth c = match Constr.kind c with + | Constr.Rel k -> + if k<=depth then c + else if k-depth <= lv then lift_substituend depth lamv.(k-depth-1) + else Constr.mkRel (k-lv) + | _ -> Constr.map_with_binders succ substrec depth c in + substrec n c + +(* +let substkey = Profile.declare_profile "substn_many";; +let substn_many lamv n c = Profile.profile3 substkey substn_many lamv n c;; +*) + +let substnl laml n = + substn_many (Array.map make_substituend (Array.of_list laml)) n +let substl laml = substnl laml 0 +let subst1 lam = substl [lam] + +let substnl_decl laml k = map_rel_declaration (substnl laml k) +let substl_decl laml = substnl_decl laml 0 +let subst1_decl lam = substl_decl [lam] + +let substnl_named_decl laml k = map_named_declaration (substnl laml k) +let substl_named_decl laml = substnl_named_decl laml 0 +let subst1_named_decl lam = substl_named_decl [lam] + +(* (thin_val sigma) removes identity substitutions from sigma *) + +let rec thin_val = function + | [] -> [] + | s :: tl -> + let id, { sit = c } = s in + match Constr.kind c with + | Constr.Var v -> if Id.equal id v then thin_val tl else s::(thin_val tl) + | _ -> s :: (thin_val tl) + +(* (replace_vars sigma M) applies substitution sigma to term M *) +let replace_vars var_alist = + let var_alist = + List.map (fun (str,c) -> (str,make_substituend c)) var_alist in + let var_alist = thin_val var_alist in + let rec substrec n c = match Constr.kind c with + | Constr.Var x -> + (try lift_substituend n (List.assoc x var_alist) + with Not_found -> c) + | _ -> Constr.map_with_binders succ substrec n c + in + match var_alist with + | [] -> (function x -> x) + | _ -> substrec 0 + +(* +let repvarkey = Profile.declare_profile "replace_vars";; +let replace_vars vl c = Profile.profile2 repvarkey replace_vars vl c ;; +*) + +(* (subst_var str t) substitute (VAR str) by (Rel 1) in t *) +let subst_var str = replace_vars [(str, Constr.mkRel 1)] + +(* (subst_vars [id1;...;idn] t) substitute (VAR idj) by (Rel j) in t *) +let substn_vars p vars = + let _,subst = + List.fold_left (fun (n,l) var -> ((n+1),(var,Constr.mkRel n)::l)) (p,[]) vars + in replace_vars (List.rev subst) + +let subst_vars = substn_vars 1 diff --git a/kernel/vars.mli b/kernel/vars.mli new file mode 100644 index 000000000..240d4d413 --- /dev/null +++ b/kernel/vars.mli @@ -0,0 +1,69 @@ +(************************************************************************) +(* v * The Coq Proof Assistant / The Coq Development Team *) +(* constr -> bool + +(** [closed0 M] is true iff [M] is a (deBruijn) closed term *) +val closed0 : constr -> bool + +(** [noccurn n M] returns true iff [Rel n] does NOT occur in term [M] *) +val noccurn : int -> constr -> bool + +(** [noccur_between n m M] returns true iff [Rel p] does NOT occur in term [M] + for n <= p < n+m *) +val noccur_between : int -> int -> constr -> bool + +(** Checking function for terms containing existential- or + meta-variables. The function [noccur_with_meta] does not consider + meta-variables applied to some terms (intended to be its local + context) (for existential variables, it is necessarily the case) *) +val noccur_with_meta : int -> int -> constr -> bool + +(** {6 Relocation and substitution } *) + +(** [exliftn el c] lifts [c] with lifting [el] *) +val exliftn : Esubst.lift -> constr -> constr + +(** [liftn n k c] lifts by [n] indexes above or equal to [k] in [c] *) +val liftn : int -> int -> constr -> constr + +(** [lift n c] lifts by [n] the positive indexes in [c] *) +val lift : int -> constr -> constr + +(** [substnl [a1;...;an] k c] substitutes in parallel [a1],...,[an] + for respectively [Rel(k+1)],...,[Rel(k+n)] in [c]; it relocates + accordingly indexes in [a1],...,[an] *) +val substnl : constr list -> int -> constr -> constr +val substl : constr list -> constr -> constr +val subst1 : constr -> constr -> constr + +val substnl_decl : constr list -> int -> rel_declaration -> rel_declaration +val substl_decl : constr list -> rel_declaration -> rel_declaration +val subst1_decl : constr -> rel_declaration -> rel_declaration + +val subst1_named_decl : constr -> named_declaration -> named_declaration +val substl_named_decl : constr list -> named_declaration -> named_declaration + +val replace_vars : (Id.t * constr) list -> constr -> constr +val subst_var : Id.t -> constr -> constr + +(** [subst_vars [id1;...;idn] t] substitute [VAR idj] by [Rel j] in [t] + if two names are identical, the one of least indice is kept *) +val subst_vars : Id.t list -> constr -> constr + +(** [substn_vars n [id1;...;idn] t] substitute [VAR idj] by [Rel j+n-1] in [t] + if two names are identical, the one of least indice is kept *) +val substn_vars : int -> Id.t list -> constr -> constr diff --git a/library/global.mli b/library/global.mli index b1184da11..a06d4640e 100644 --- a/library/global.mli +++ b/library/global.mli @@ -9,6 +9,7 @@ open Names open Univ open Term +open Context open Declarations open Entries open Indtypes diff --git a/library/heads.ml b/library/heads.ml index 022e61156..2a42888d5 100644 --- a/library/heads.ml +++ b/library/heads.ml @@ -10,6 +10,7 @@ open Pp open Util open Names open Term +open Vars open Mod_subst open Environ open Globnames diff --git a/plugins/cc/ccalgo.ml b/plugins/cc/ccalgo.ml index 473199cb2..aba908d48 100644 --- a/plugins/cc/ccalgo.ml +++ b/plugins/cc/ccalgo.ml @@ -15,6 +15,7 @@ open Pp open Goptions open Names open Term +open Vars open Tacmach open Evd diff --git a/plugins/cc/cctac.ml b/plugins/cc/cctac.ml index a5baa00f9..a7800667f 100644 --- a/plugins/cc/cctac.ml +++ b/plugins/cc/cctac.ml @@ -13,6 +13,7 @@ open Names open Inductiveops open Declarations open Term +open Vars open Tacmach open Tactics open Tacticals @@ -226,7 +227,7 @@ let build_projection intype outtype (cstr:constructor) special default gls= let lp=Array.length types in let ci=pred (snd cstr) in let branch i= - let ti=Term.prod_appvect types.(i) argv in + let ti= prod_appvect types.(i) argv in let rc=fst (decompose_prod_assum ti) in let head= if i=ci then special else default in diff --git a/plugins/decl_mode/decl_interp.ml b/plugins/decl_mode/decl_interp.ml index 9d34dc99a..b9334801c 100644 --- a/plugins/decl_mode/decl_interp.ml +++ b/plugins/decl_mode/decl_interp.ml @@ -17,6 +17,7 @@ open Decl_mode open Pretyping open Glob_term open Term +open Vars open Pp open Decl_kinds open Misctypes diff --git a/plugins/decl_mode/decl_proof_instr.ml b/plugins/decl_mode/decl_proof_instr.ml index 2ef2c9756..5e55bcfb2 100644 --- a/plugins/decl_mode/decl_proof_instr.ml +++ b/plugins/decl_mode/decl_proof_instr.ml @@ -25,6 +25,7 @@ open Declarations open Tactics open Tacticals open Term +open Vars open Termops open Namegen open Reductionops @@ -301,7 +302,7 @@ let enstack_subsubgoals env se stack gls= let constructor = mkConstruct(ind,succ i) (* constructors numbering*) in let appterm = applist (constructor,params) in - let apptype = Term.prod_applist gentyp params in + let apptype = prod_applist gentyp params in let rc,_ = Reduction.dest_prod env apptype in let rec meta_aux last lenv = function [] -> (last,lenv,[]) @@ -638,7 +639,7 @@ let rec build_applist prod = function [] -> [],prod | n::q -> let (_,typ,_) = destProd prod in - let ctx,head = build_applist (Term.prod_applist prod [mkMeta n]) q in + let ctx,head = build_applist (prod_applist prod [mkMeta n]) q in (n,typ)::ctx,head let instr_suffices _then cut gls0 = @@ -671,7 +672,7 @@ let conjunction_arity id gls = let gentypes= Inductive.arities_of_constructors ind (mib,oib) in let _ = if Array.length gentypes <> 1 then raise Not_found in - let apptype = Term.prod_applist gentypes.(0) params in + let apptype = prod_applist gentypes.(0) params in let rc,_ = Reduction.dest_prod env apptype in List.length rc | _ -> raise Not_found @@ -1218,7 +1219,7 @@ let rec execute_cases fix_name per_info tacnext args objs nhrec tree gls = let gen_arities = Inductive.arities_of_constructors ind spec in let f_ids typ = let sign = - (prod_assum (Term.prod_applist typ params)) in + (prod_assum (prod_applist typ params)) in find_intro_names sign gls in let constr_args_ids = Array.map f_ids gen_arities in let case_term = diff --git a/plugins/extraction/extraction.ml b/plugins/extraction/extraction.ml index 903a647fc..a6a9838ae 100644 --- a/plugins/extraction/extraction.ml +++ b/plugins/extraction/extraction.ml @@ -10,6 +10,8 @@ open Util open Names open Term +open Vars +open Context open Declarations open Declareops open Environ diff --git a/plugins/firstorder/formula.ml b/plugins/firstorder/formula.ml index 557e9c25d..89ba7b259 100644 --- a/plugins/firstorder/formula.ml +++ b/plugins/firstorder/formula.ml @@ -9,6 +9,7 @@ open Hipattern open Names open Term +open Vars open Termops open Tacmach open Util @@ -50,12 +51,11 @@ let construct_nhyps ind gls = (* indhyps builds the array of arrays of constructor hyps for (ind largs)*) let ind_hyps nevar ind largs gls= let types= Inductiveops.arities_of_constructors (pf_env gls) ind in - let lp=Array.length types in - let myhyps i= - let t1=Term.prod_applist types.(i) largs in + let myhyps t = + let t1=prod_applist t largs in let t2=snd (decompose_prod_n_assum nevar t1) in fst (decompose_prod_assum t2) in - Array.init lp myhyps + Array.map myhyps types let special_nf gl= let infos=Closure.create_clos_infos !red_flags (pf_env gl) in diff --git a/plugins/firstorder/formula.mli b/plugins/firstorder/formula.mli index f1f04fdb5..59b363393 100644 --- a/plugins/firstorder/formula.mli +++ b/plugins/firstorder/formula.mli @@ -6,8 +6,9 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -open Term open Names +open Term +open Context open Globnames val qflag : bool ref diff --git a/plugins/firstorder/ground.ml b/plugins/firstorder/ground.ml index 6c1709140..5133801ee 100644 --- a/plugins/firstorder/ground.ml +++ b/plugins/firstorder/ground.ml @@ -11,6 +11,7 @@ open Sequent open Rules open Instances open Term +open Vars open Tacmach open Tacticals diff --git a/plugins/firstorder/instances.ml b/plugins/firstorder/instances.ml index 12b2304ac..4b15dcae5 100644 --- a/plugins/firstorder/instances.ml +++ b/plugins/firstorder/instances.ml @@ -11,6 +11,7 @@ open Rules open Errors open Util open Term +open Vars open Glob_term open Tacmach open Tactics diff --git a/plugins/firstorder/rules.ml b/plugins/firstorder/rules.ml index 8abf9d7e2..02a0dd20d 100644 --- a/plugins/firstorder/rules.ml +++ b/plugins/firstorder/rules.ml @@ -10,6 +10,7 @@ open Errors open Util open Names open Term +open Vars open Tacmach open Tactics open Tacticals diff --git a/plugins/firstorder/unify.ml b/plugins/firstorder/unify.ml index 75fd0261a..e59f0419e 100644 --- a/plugins/firstorder/unify.ml +++ b/plugins/firstorder/unify.ml @@ -8,6 +8,7 @@ open Util open Term +open Vars open Termops open Reductionops diff --git a/plugins/funind/functional_principles_proofs.ml b/plugins/funind/functional_principles_proofs.ml index 74d719438..6913b40ea 100644 --- a/plugins/funind/functional_principles_proofs.ml +++ b/plugins/funind/functional_principles_proofs.ml @@ -2,6 +2,8 @@ open Printer open Errors open Util open Term +open Vars +open Context open Namegen open Names open Declarations diff --git a/plugins/funind/functional_principles_types.ml b/plugins/funind/functional_principles_types.ml index 50a4703f6..f70ce0092 100644 --- a/plugins/funind/functional_principles_types.ml +++ b/plugins/funind/functional_principles_types.ml @@ -2,6 +2,8 @@ open Printer open Errors open Util open Term +open Vars +open Context open Namegen open Names open Declarations diff --git a/plugins/funind/g_indfun.ml4 b/plugins/funind/g_indfun.ml4 index 1ccfe3c31..088b4a0cd 100644 --- a/plugins/funind/g_indfun.ml4 +++ b/plugins/funind/g_indfun.ml4 @@ -9,6 +9,7 @@ open Compat open Util open Term +open Vars open Names open Pp open Constrexpr diff --git a/plugins/funind/glob_term_to_relation.ml b/plugins/funind/glob_term_to_relation.ml index fe48cbd88..2b4b6245a 100644 --- a/plugins/funind/glob_term_to_relation.ml +++ b/plugins/funind/glob_term_to_relation.ml @@ -2,6 +2,7 @@ open Printer open Pp open Names open Term +open Vars open Glob_term open Glob_ops open Globnames diff --git a/plugins/funind/invfun.ml b/plugins/funind/invfun.ml index 16b1881f4..e46c1a15a 100644 --- a/plugins/funind/invfun.ml +++ b/plugins/funind/invfun.ml @@ -11,6 +11,7 @@ open Errors open Util open Names open Term +open Vars open Pp open Globnames open Tacticals diff --git a/plugins/funind/merge.ml b/plugins/funind/merge.ml index bf5eba63a..65b4101a0 100644 --- a/plugins/funind/merge.ml +++ b/plugins/funind/merge.ml @@ -18,6 +18,8 @@ open Vernacexpr open Pp open Names open Term +open Vars +open Context open Termops open Declarations open Glob_term diff --git a/plugins/funind/recdef.ml b/plugins/funind/recdef.ml index a8ffd51ef..34085dca2 100644 --- a/plugins/funind/recdef.ml +++ b/plugins/funind/recdef.ml @@ -7,6 +7,7 @@ (************************************************************************) open Term +open Vars open Namegen open Environ open Declarations diff --git a/plugins/rtauto/refl_tauto.ml b/plugins/rtauto/refl_tauto.ml index 597b6afb6..5a77bf967 100644 --- a/plugins/rtauto/refl_tauto.ml +++ b/plugins/rtauto/refl_tauto.ml @@ -298,7 +298,7 @@ let rtauto_tac gls= build_form formula; build_proof [] 0 prf|]) in let term= - Term.applist (main,List.rev_map (fun (id,_) -> mkVar id) hyps) in + applist (main,List.rev_map (fun (id,_) -> mkVar id) hyps) in let build_end_time=System.get_time () in let _ = if !verbose then begin diff --git a/plugins/setoid_ring/newring.ml4 b/plugins/setoid_ring/newring.ml4 index 48741525d..670cd2c47 100644 --- a/plugins/setoid_ring/newring.ml4 +++ b/plugins/setoid_ring/newring.ml4 @@ -13,6 +13,7 @@ open Errors open Util open Names open Term +open Vars open Closure open Environ open Libnames diff --git a/plugins/xml/cic2acic.ml b/plugins/xml/cic2acic.ml index 98c485dba..a7a181aa6 100644 --- a/plugins/xml/cic2acic.ml +++ b/plugins/xml/cic2acic.ml @@ -170,6 +170,7 @@ let family_of_term ty = module CPropRetyping = struct module T = Term + module V = Vars let outsort env sigma t = family_of_term (DoubleTypeInference.whd_betadeltaiotacprop env sigma t) @@ -178,7 +179,7 @@ module CPropRetyping = | [] -> typ | h::rest -> match T.kind_of_term (DoubleTypeInference.whd_betadeltaiotacprop env sigma typ) with - | T.Prod (na,c1,c2) -> subst_type env sigma (T.subst1 h c2) rest + | T.Prod (na,c1,c2) -> subst_type env sigma (V.subst1 h c2) rest | _ -> Errors.anomaly (Pp.str "Non-functional construction") @@ -198,7 +199,7 @@ let typeur sigma metamap = with Not_found -> Errors.anomaly ~label:"type_of" (Pp.str "this is not a well-typed term")) | T.Rel n -> let (_,_,ty) = Environ.lookup_rel n env in - T.lift n ty + V.lift n ty | T.Var id -> (try let (_,_,ty) = Environ.lookup_named id env in @@ -222,7 +223,7 @@ let typeur sigma metamap = | T.Lambda (name,c1,c2) -> T.mkProd (name, c1, type_of (Environ.push_rel (name,None,c1) env) c2) | T.LetIn (name,b,c1,c2) -> - T.subst1 b (type_of (Environ.push_rel (name,Some b,c1) env) c2) + V.subst1 b (type_of (Environ.push_rel (name,Some b,c1) env) c2) | T.Fix ((_,i),(_,tys,_)) -> tys.(i) | T.CoFix (i,(_,tys,_)) -> tys.(i) | T.App(f,args)-> @@ -326,6 +327,7 @@ let acic_of_cic_context' computeinnertypes seed ids_to_terms constr_to_ids let module N = Names in let module A = Acic in let module T = Term in + let module V = Vars in let fresh_id' = fresh_id seed ids_to_terms constr_to_ids ids_to_father_ids in (* CSC: do you have any reasonable substitute for 503? *) let terms_to_types = Acic.CicHash.create 503 in @@ -473,7 +475,7 @@ print_endline "PASSATO" ; flush stdout ; in let eta_expanded = let arguments = - List.map (T.lift uninst_vars_length) t @ + List.map (V.lift uninst_vars_length) t @ Termops.rel_list 0 uninst_vars_length in Unshare.unshare @@ -528,7 +530,7 @@ print_endline "PASSATO" ; flush stdout ; match n with N.Anonymous -> N.Anonymous | _ -> - if not fake_dependent_products && T.noccurn 1 t then + if not fake_dependent_products && V.noccurn 1 t then N.Anonymous else N.Name diff --git a/plugins/xml/doubleTypeInference.ml b/plugins/xml/doubleTypeInference.ml index c95cf94b6..5a3880b01 100644 --- a/plugins/xml/doubleTypeInference.ml +++ b/plugins/xml/doubleTypeInference.ml @@ -59,6 +59,7 @@ let double_type_of env sigma cstr expectedty subterms_to_types = (*CSC: functions used do checks that we do not need *) let rec execute env sigma cstr expectedty = let module T = Term in + let module V = Vars in let module E = Environ in (* the type part is the synthesized type *) let judgement = @@ -84,7 +85,7 @@ let double_type_of env sigma cstr expectedty subterms_to_types = (function (m,bo,ty) -> (* Warning: the substitution should be performed also on bo *) (* This is not done since bo is not used later yet *) - (m,bo,Unshare.unshare (T.replace_vars [n,he1] ty)) + (m,bo,Unshare.unshare (V.replace_vars [n,he1] ty)) ) tl2 in iter tl1 tl2' @@ -161,7 +162,7 @@ let double_type_of env sigma cstr expectedty subterms_to_types = match T.kind_of_term (Reduction.whd_betadeltaiota env typ) with T.Prod (_,c1,c2) -> (Some (Reductionops.nf_beta sigma c1)) :: - (aux (T.subst1 hj c2) restjl) + (aux (V.subst1 hj c2) restjl) | _ -> assert false in Array.of_list (aux j.Environ.uj_type (Array.to_list args)) @@ -249,7 +250,7 @@ if Acic.CicHash.mem subterms_to_types cstr then let lara = Array.map (assumption_of_judgment env sigma) larj in let env1 = Environ.push_rec_types (names,lara,vdef) env in let expectedtypes = - Array.map (function i -> Some (Term.lift length i)) lar + Array.map (function i -> Some (Vars.lift length i)) lar in let vdefj = execute_array env1 sigma vdef expectedtypes in let vdefv = Array.map Environ.j_val vdefj in diff --git a/pretyping/cases.ml b/pretyping/cases.ml index e16e8e1cc..5d11dbc81 100644 --- a/pretyping/cases.ml +++ b/pretyping/cases.ml @@ -12,6 +12,8 @@ open Util open Names open Nameops open Term +open Vars +open Context open Termops open Namegen open Declarations diff --git a/pretyping/cases.mli b/pretyping/cases.mli index d9f9b9d76..3e4b09148 100644 --- a/pretyping/cases.mli +++ b/pretyping/cases.mli @@ -9,6 +9,7 @@ open Pp open Names open Term +open Context open Evd open Environ open Inductiveops @@ -57,11 +58,11 @@ val compile_cases : val constr_of_pat : Environ.env -> Evd.evar_map ref -> - Term.rel_declaration list -> + rel_declaration list -> Glob_term.cases_pattern -> Names.Id.t list -> Glob_term.cases_pattern * - (Term.rel_declaration list * Term.constr * + (rel_declaration list * Term.constr * (Term.types * Term.constr list) * Glob_term.cases_pattern) * Names.Id.t list diff --git a/pretyping/cbv.ml b/pretyping/cbv.ml index a84bbcc54..1334fb285 100644 --- a/pretyping/cbv.ml +++ b/pretyping/cbv.ml @@ -7,8 +7,9 @@ (************************************************************************) open Util -open Term open Names +open Term +open Vars open Closure open Esubst diff --git a/pretyping/coercion.ml b/pretyping/coercion.ml index 7d2ad487c..e97e45580 100644 --- a/pretyping/coercion.ml +++ b/pretyping/coercion.ml @@ -18,6 +18,7 @@ open Errors open Util open Names open Term +open Vars open Reductionops open Environ open Typeops @@ -80,7 +81,7 @@ let disc_subset x = Ind i -> let len = Array.length l in let sigty = delayed_force sig_typ in - if Int.equal len 2 && eq_ind i (Term.destInd sigty) + if Int.equal len 2 && eq_ind i (destInd sigty) then let (a, b) = pair_of_array l in Some (a, b) @@ -190,7 +191,7 @@ and coerce loc env isevars (x : Term.constr) (y : Term.constr) (fun f -> mkLambda (name', a', app_opt env' isevars c2 - (mkApp (Term.lift 1 f, [| coec1 |]))))) + (mkApp (lift 1 f, [| coec1 |]))))) | App (c, l), App (c', l') -> (match kind_of_term c, kind_of_term c' with @@ -200,9 +201,9 @@ and coerce loc env isevars (x : Term.constr) (y : Term.constr) let prod = delayed_force prod_typ in (* Sigma types *) if Int.equal len (Array.length l') && Int.equal len 2 && eq_ind i i' - && (eq_ind i (Term.destInd sigT) || eq_ind i (Term.destInd prod)) + && (eq_ind i (destInd sigT) || eq_ind i (destInd prod)) then - if eq_ind i (Term.destInd sigT) + if eq_ind i (destInd sigT) then begin let (a, pb), (a', pb') = diff --git a/pretyping/detyping.ml b/pretyping/detyping.ml index cc900adb4..9483f0220 100644 --- a/pretyping/detyping.ml +++ b/pretyping/detyping.ml @@ -11,6 +11,8 @@ open Errors open Util open Names open Term +open Vars +open Context open Inductiveops open Environ open Glob_term diff --git a/pretyping/detyping.mli b/pretyping/detyping.mli index 3a8f54904..f2f5c9eff 100644 --- a/pretyping/detyping.mli +++ b/pretyping/detyping.mli @@ -10,6 +10,7 @@ open Errors open Pp open Names open Term +open Context open Sign open Environ open Glob_term diff --git a/pretyping/evarconv.ml b/pretyping/evarconv.ml index 19bced344..39e262a3c 100644 --- a/pretyping/evarconv.ml +++ b/pretyping/evarconv.ml @@ -10,6 +10,7 @@ open Errors open Util open Names open Term +open Vars open Closure open Reduction open Reductionops diff --git a/pretyping/evarsolve.ml b/pretyping/evarsolve.ml index b3a2e2a39..1d5dda69f 100644 --- a/pretyping/evarsolve.ml +++ b/pretyping/evarsolve.ml @@ -11,6 +11,8 @@ open Util open Errors open Names open Term +open Vars +open Context open Environ open Termops open Evd diff --git a/pretyping/evarutil.ml b/pretyping/evarutil.ml index 82dda8e0f..5719d750e 100644 --- a/pretyping/evarutil.ml +++ b/pretyping/evarutil.ml @@ -11,6 +11,8 @@ open Util open Pp open Names open Term +open Vars +open Context open Termops open Namegen open Pre_env diff --git a/pretyping/evarutil.mli b/pretyping/evarutil.mli index 4db6fdd3e..26d85ac94 100644 --- a/pretyping/evarutil.mli +++ b/pretyping/evarutil.mli @@ -11,6 +11,7 @@ open Util open Names open Glob_term open Term +open Context open Sign open Evd open Environ diff --git a/pretyping/evd.ml b/pretyping/evd.ml index 6efdf0455..28b6ac93b 100644 --- a/pretyping/evd.ml +++ b/pretyping/evd.ml @@ -12,6 +12,7 @@ open Util open Names open Nameops open Term +open Vars open Termops open Environ open Globnames diff --git a/pretyping/indrec.ml b/pretyping/indrec.ml index 8904e2b7b..c0c20a1e3 100644 --- a/pretyping/indrec.ml +++ b/pretyping/indrec.ml @@ -18,6 +18,8 @@ open Libnames open Globnames open Nameops open Term +open Vars +open Context open Namegen open Declarations open Declareops diff --git a/pretyping/inductiveops.ml b/pretyping/inductiveops.ml index 610bde687..b0637a972 100644 --- a/pretyping/inductiveops.ml +++ b/pretyping/inductiveops.ml @@ -11,6 +11,8 @@ open Util open Names open Univ open Term +open Vars +open Context open Termops open Namegen open Declarations diff --git a/pretyping/inductiveops.mli b/pretyping/inductiveops.mli index 4fcc6c6bd..038bf465a 100644 --- a/pretyping/inductiveops.mli +++ b/pretyping/inductiveops.mli @@ -8,6 +8,7 @@ open Names open Term +open Context open Declarations open Environ open Evd diff --git a/pretyping/matching.ml b/pretyping/matching.ml index 5460d8ba1..ab90b5601 100644 --- a/pretyping/matching.ml +++ b/pretyping/matching.ml @@ -16,6 +16,8 @@ open Nameops open Termops open Reductionops open Term +open Vars +open Context open Pattern open Patternops open Misctypes diff --git a/pretyping/namegen.ml b/pretyping/namegen.ml index bf1adb3cf..a2fa81750 100644 --- a/pretyping/namegen.ml +++ b/pretyping/namegen.ml @@ -15,6 +15,7 @@ open Util open Names open Term +open Vars open Nametab open Nameops open Libnames diff --git a/pretyping/namegen.mli b/pretyping/namegen.mli index 6c982451a..095c7a59f 100644 --- a/pretyping/namegen.mli +++ b/pretyping/namegen.mli @@ -8,6 +8,7 @@ open Names open Term +open Context open Environ (********************************************************************* diff --git a/pretyping/nativenorm.ml b/pretyping/nativenorm.ml index 9a2a8dce7..ed52f574f 100644 --- a/pretyping/nativenorm.ml +++ b/pretyping/nativenorm.ml @@ -8,6 +8,7 @@ open Pp open Errors open Term +open Vars open Environ open Reduction open Univ diff --git a/pretyping/patternops.ml b/pretyping/patternops.ml index ef0869fe6..d227e1f2a 100644 --- a/pretyping/patternops.ml +++ b/pretyping/patternops.ml @@ -12,6 +12,7 @@ open Names open Globnames open Nameops open Term +open Vars open Glob_term open Glob_ops open Pp diff --git a/pretyping/pretype_errors.ml b/pretyping/pretype_errors.ml index 72cc6502a..d1a0aaf8d 100644 --- a/pretyping/pretype_errors.ml +++ b/pretyping/pretype_errors.ml @@ -9,6 +9,7 @@ open Util open Names open Term +open Vars open Termops open Namegen open Environ diff --git a/pretyping/pretyping.ml b/pretyping/pretyping.ml index d4afb3a5f..26325872f 100644 --- a/pretyping/pretyping.ml +++ b/pretyping/pretyping.ml @@ -28,6 +28,8 @@ open Names open Sign open Evd open Term +open Vars +open Context open Termops open Reductionops open Environ diff --git a/pretyping/reductionops.ml b/pretyping/reductionops.ml index 6a94fa109..b2a9bdcc5 100644 --- a/pretyping/reductionops.ml +++ b/pretyping/reductionops.ml @@ -10,6 +10,8 @@ open Errors open Util open Names open Term +open Vars +open Context open Termops open Univ open Evd @@ -54,7 +56,7 @@ let compare_stack_shape stk1 stk2 = let fold_stack2 f o sk1 sk2 = let rec aux o lft1 sk1 lft2 sk2 = let fold_array = - Array.fold_left2 (fun a x y -> f a (Term.lift lft1 x) (Term.lift lft2 y)) + Array.fold_left2 (fun a x y -> f a (Vars.lift lft1 x) (Vars.lift lft2 y)) in match sk1,sk2 with | [], [] -> o,lft1,lft2 @@ -63,11 +65,11 @@ let fold_stack2 f o sk1 sk2 = | Zapp [] :: q1, _ -> aux o lft1 q1 lft2 sk2 | _, Zapp [] :: q2 -> aux o lft1 sk1 lft2 q2 | Zapp (t1::l1) :: q1, Zapp (t2::l2) :: q2 -> - aux (f o (Term.lift lft1 t1) (Term.lift lft2 t2)) + aux (f o (Vars.lift lft1 t1) (Vars.lift lft2 t2)) lft1 (Zapp l1 :: q1) lft2 (Zapp l2 :: q2) | Zcase (_,t1,a1,_) :: q1, Zcase (_,t2,a2,_) :: q2 -> aux (fold_array - (f o (Term.lift lft1 t1) (Term.lift lft2 t2)) + (f o (Vars.lift lft1 t1) (Vars.lift lft2 t2)) a1 a2) lft1 q1 lft2 q2 | Zfix ((_,(_,a1,b1)),s1,_) :: q1, Zfix ((_,(_,a2,b2)),s2,_) :: q2 -> let (o',_,_) = aux (fold_array (fold_array o b1 b2) a1 a2) diff --git a/pretyping/reductionops.mli b/pretyping/reductionops.mli index 1914b3b1e..e95fc41c0 100644 --- a/pretyping/reductionops.mli +++ b/pretyping/reductionops.mli @@ -8,6 +8,7 @@ open Names open Term +open Context open Univ open Evd open Environ diff --git a/pretyping/retyping.ml b/pretyping/retyping.ml index d290d0a47..a49e2026a 100644 --- a/pretyping/retyping.ml +++ b/pretyping/retyping.ml @@ -10,6 +10,7 @@ open Pp open Errors open Util open Term +open Vars open Inductive open Inductiveops open Names diff --git a/pretyping/tacred.ml b/pretyping/tacred.ml index efc2a7467..08d2c7cdf 100644 --- a/pretyping/tacred.ml +++ b/pretyping/tacred.ml @@ -11,6 +11,7 @@ open Errors open Util open Names open Term +open Vars open Libnames open Globnames open Termops diff --git a/pretyping/termops.ml b/pretyping/termops.ml index 5056c3123..0128f8bde 100644 --- a/pretyping/termops.ml +++ b/pretyping/termops.ml @@ -12,6 +12,8 @@ open Util open Names open Nameops open Term +open Vars +open Context open Environ open Locus diff --git a/pretyping/termops.mli b/pretyping/termops.mli index 97ac88183..9547231af 100644 --- a/pretyping/termops.mli +++ b/pretyping/termops.mli @@ -10,10 +10,13 @@ open Util open Pp open Names open Term +open Context open Sign open Environ open Locus +(** TODO: merge this with Term *) + (** Universes *) val new_univ_level : unit -> Univ.universe_level val new_univ : unit -> Univ.universe diff --git a/pretyping/typeclasses.ml b/pretyping/typeclasses.ml index 86ff2a28f..53171d02c 100644 --- a/pretyping/typeclasses.ml +++ b/pretyping/typeclasses.ml @@ -11,6 +11,8 @@ open Names open Globnames open Decl_kinds open Term +open Vars +open Context open Sign open Evd open Environ @@ -109,7 +111,7 @@ let dest_class_app env c = global_class_of_constr env cl, args let dest_class_arity env c = - let rels, c = Term.decompose_prod_assum c in + let rels, c = decompose_prod_assum c in rels, dest_class_app env c let class_of_constr c = diff --git a/pretyping/typeclasses.mli b/pretyping/typeclasses.mli index 3f10200c0..af6824924 100644 --- a/pretyping/typeclasses.mli +++ b/pretyping/typeclasses.mli @@ -10,6 +10,7 @@ open Names open Globnames open Decl_kinds open Term +open Context open Sign open Evd open Environ diff --git a/pretyping/typeclasses_errors.ml b/pretyping/typeclasses_errors.ml index d0d90017f..89eb217d2 100644 --- a/pretyping/typeclasses_errors.ml +++ b/pretyping/typeclasses_errors.ml @@ -9,6 +9,7 @@ (*i*) open Names open Term +open Context open Evd open Environ open Constrexpr diff --git a/pretyping/typeclasses_errors.mli b/pretyping/typeclasses_errors.mli index 5155b7163..f80ff00fc 100644 --- a/pretyping/typeclasses_errors.mli +++ b/pretyping/typeclasses_errors.mli @@ -10,6 +10,7 @@ open Loc open Names open Decl_kinds open Term +open Context open Sign open Evd open Environ diff --git a/pretyping/typing.ml b/pretyping/typing.ml index 7cf7e5889..008b8b9a3 100644 --- a/pretyping/typing.ml +++ b/pretyping/typing.ml @@ -10,6 +10,7 @@ open Pp open Errors open Util open Term +open Vars open Environ open Reductionops open Type_errors diff --git a/pretyping/unification.ml b/pretyping/unification.ml index 31148ee39..f3014424c 100644 --- a/pretyping/unification.ml +++ b/pretyping/unification.ml @@ -10,6 +10,7 @@ open Errors open Util open Names open Term +open Vars open Termops open Namegen open Environ diff --git a/pretyping/vnorm.ml b/pretyping/vnorm.ml index fb8a05a97..4b08f7517 100644 --- a/pretyping/vnorm.ml +++ b/pretyping/vnorm.ml @@ -9,6 +9,7 @@ open Names open Declarations open Term +open Vars open Environ open Inductive open Reduction diff --git a/printing/printer.ml b/printing/printer.ml index 531614e50..27266cfe1 100644 --- a/printing/printer.ml +++ b/printing/printer.ml @@ -11,7 +11,9 @@ open Errors open Util open Names open Term +open Vars open Sign +open Context open Environ open Globnames open Nametab diff --git a/printing/printer.mli b/printing/printer.mli index b99a9f9ab..55058ae16 100644 --- a/printing/printer.mli +++ b/printing/printer.mli @@ -11,6 +11,7 @@ open Names open Libnames open Globnames open Term +open Context open Sign open Environ open Glob_term diff --git a/proofs/clenv.ml b/proofs/clenv.ml index 6177040cc..156629c19 100644 --- a/proofs/clenv.ml +++ b/proofs/clenv.ml @@ -12,6 +12,7 @@ open Util open Names open Nameops open Term +open Vars open Termops open Namegen open Environ diff --git a/proofs/goal.ml b/proofs/goal.ml index 7948020a9..6b794c147 100644 --- a/proofs/goal.ml +++ b/proofs/goal.ml @@ -9,6 +9,8 @@ open Util open Pp open Term +open Vars +open Context (* This module implements the abstract interface to goals *) (* A general invariant of the module, is that a goal whose associated @@ -64,7 +66,7 @@ let rec advance sigma g = | Evd.Evar_defined c -> c | _ -> Errors.anomaly (Pp.str "Some goal is marked as 'cleared' but is uninstantiated") in - let (e,_) = Term.destEvar v in + let (e,_) = destEvar v in let g' = { g with content = e } in advance sigma g' else @@ -141,7 +143,7 @@ module Refinable = struct let mkEvar handle env typ _ rdefs _ _ = let ev = Evarutil.e_new_evar rdefs env typ in - let (e,_) = Term.destEvar ev in + let (e,_) = destEvar ev in handle := e::!handle; ev @@ -260,7 +262,7 @@ let clear ids env rdefs gl info = let (hyps,concl) = Evarutil.clear_hyps_in_evi rdefs hyps concl ids in let cleared_env = Environ.reset_with_named_context hyps env in let cleared_concl = Evarutil.e_new_evar rdefs cleared_env concl in - let (cleared_evar,_) = Term.destEvar cleared_concl in + let (cleared_evar,_) = destEvar cleared_concl in let cleared_goal = descendent gl cleared_evar in rdefs := Evd.define gl.content cleared_concl !rdefs; { subgoals = [cleared_goal] } @@ -396,7 +398,7 @@ let convert_hyp check (id,b,bt as d) env rdefs gl info = let new_constr = Evarutil.e_new_evar rdefs new_env (concl env rdefs gl info) in - let (new_evar,_) = Term.destEvar new_constr in + let (new_evar,_) = destEvar new_constr in let new_goal = descendent gl new_evar in rdefs := Evd.define gl.content new_constr !rdefs; { subgoals = [new_goal] } @@ -409,7 +411,7 @@ let convert_concl check cl' env rdefs gl info = let new_constr = Evarutil.e_new_evar rdefs env cl' in - let (new_evar,_) = Term.destEvar new_constr in + let (new_evar,_) = destEvar new_constr in let new_goal = descendent gl new_evar in rdefs := Evd.define gl.content new_constr !rdefs; { subgoals = [new_goal] } @@ -431,10 +433,10 @@ let rename_hyp id1 id2 env rdefs gl info = Errors.error ((Names.Id.to_string id2)^" is already used."); let new_hyps = rename_hyp_sign id1 id2 hyps in let new_env = Environ.reset_with_named_context new_hyps env in - let new_concl = Term.replace_vars [id1,mkVar id2] (concl env rdefs gl info) in + let new_concl = Vars.replace_vars [id1,mkVar id2] (concl env rdefs gl info) in let new_subproof = Evarutil.e_new_evar rdefs new_env new_concl in - let new_subproof = Term.replace_vars [id2,mkVar id1] new_subproof in - let (new_evar,_) = Term.destEvar new_subproof in + let new_subproof = Vars.replace_vars [id2,mkVar id1] new_subproof in + let (new_evar,_) = destEvar new_subproof in let new_goal = descendent gl new_evar in rdefs := Evd.define gl.content new_subproof !rdefs; { subgoals = [new_goal] } diff --git a/proofs/goal.mli b/proofs/goal.mli index 6b587959a..4cd3e4746 100644 --- a/proofs/goal.mli +++ b/proofs/goal.mli @@ -111,7 +111,7 @@ val clear_body : Names.Id.t list -> subgoals sensitive (* Changes an hypothesis of the goal with a convertible type and body. Checks convertibility if the boolean argument is true. *) -val convert_hyp : bool -> Term.named_declaration -> subgoals sensitive +val convert_hyp : bool -> Context.named_declaration -> subgoals sensitive (* Changes the conclusion of the goal with a convertible type and body. Checks convertibility if the boolean argument is true. *) diff --git a/proofs/logic.ml b/proofs/logic.ml index 7ec1b684b..a0781ae6a 100644 --- a/proofs/logic.ml +++ b/proofs/logic.ml @@ -12,6 +12,8 @@ open Util open Names open Nameops open Term +open Vars +open Context open Termops open Environ open Reductionops @@ -538,7 +540,7 @@ let prim_refiner r sigma goal = push_named_context_val (id,None,t) sign,cl,sigma) in let (sg2,ev2,sigma) = Goal.V82.mk_goal sigma sign cl (Goal.V82.extra sigma goal) in - let oterm = Term.mkApp (Term.mkNamedLambda id t ev2 , [| ev1 |]) in + let oterm = Term.mkApp (mkNamedLambda id t ev2 , [| ev1 |]) in let sigma = Goal.V82.partial_solution sigma goal oterm in if b then ([sg1;sg2],sigma) else ([sg2;sg1],sigma) @@ -579,7 +581,7 @@ let prim_refiner r sigma goal = let (gls_evs,sigma) = mk_sign sign all in let (gls,evs) = List.split gls_evs in let ids = List.map pi1 all in - let evs = List.map (Term.subst_vars (List.rev ids)) evs in + let evs = List.map (Vars.subst_vars (List.rev ids)) evs in let indxs = Array.of_list (List.map (fun n -> n-1) (List.map pi2 all)) in let funnames = Array.of_list (List.map (fun i -> Name i) ids) in let typarray = Array.of_list (List.map pi3 all) in @@ -622,7 +624,7 @@ let prim_refiner r sigma goal = let (gls_evs,sigma) = mk_sign sign all in let (gls,evs) = List.split gls_evs in let (ids,types) = List.split all in - let evs = List.map (Term.subst_vars (List.rev ids)) evs in + let evs = List.map (Vars.subst_vars (List.rev ids)) evs in let funnames = Array.of_list (List.map (fun i -> Name i) ids) in let typarray = Array.of_list types in let bodies = Array.of_list evs in @@ -695,7 +697,7 @@ let prim_refiner r sigma goal = let sign' = rename_hyp id1 id2 sign in let cl' = replace_vars [id1,mkVar id2] cl in let (gl,ev,sigma) = mk_goal sign' cl' in - let ev = Term.replace_vars [(id2,mkVar id1)] ev in + let ev = Vars.replace_vars [(id2,mkVar id1)] ev in let sigma = Goal.V82.partial_solution sigma goal ev in ([gl], sigma) diff --git a/proofs/proof_type.ml b/proofs/proof_type.ml index af50059b8..954e2fdb7 100644 --- a/proofs/proof_type.ml +++ b/proofs/proof_type.ml @@ -10,6 +10,7 @@ open Evd open Names open Term +open Context open Tacexpr open Glob_term open Nametab diff --git a/proofs/proof_type.mli b/proofs/proof_type.mli index 063599535..33945052f 100644 --- a/proofs/proof_type.mli +++ b/proofs/proof_type.mli @@ -11,6 +11,7 @@ open Evd open Names open Libnames open Term +open Context open Pp open Tacexpr open Glob_term diff --git a/proofs/tacmach.mli b/proofs/tacmach.mli index 328a3d65b..5b502f2c9 100644 --- a/proofs/tacmach.mli +++ b/proofs/tacmach.mli @@ -8,6 +8,7 @@ open Names open Term +open Context open Sign open Environ open Evd diff --git a/tactics/auto.ml b/tactics/auto.ml index e05c5384a..470d2e6cf 100644 --- a/tactics/auto.ml +++ b/tactics/auto.ml @@ -13,6 +13,7 @@ open Names open Nameops open Namegen open Term +open Vars open Termops open Inductiveops open Environ diff --git a/tactics/auto.mli b/tactics/auto.mli index 2ec0c877d..a93f9be26 100644 --- a/tactics/auto.mli +++ b/tactics/auto.mli @@ -8,6 +8,7 @@ open Names open Term +open Context open Sign open Proof_type open Tacmach diff --git a/tactics/eqschemes.ml b/tactics/eqschemes.ml index f86c22bcf..cc1162168 100644 --- a/tactics/eqschemes.ml +++ b/tactics/eqschemes.ml @@ -48,6 +48,8 @@ open Errors open Util open Names open Term +open Vars +open Context open Declarations open Environ open Inductive diff --git a/tactics/equality.ml b/tactics/equality.ml index 0e4415344..18e582b31 100644 --- a/tactics/equality.ml +++ b/tactics/equality.ml @@ -12,6 +12,7 @@ open Util open Names open Nameops open Term +open Vars open Termops open Namegen open Inductive diff --git a/tactics/equality.mli b/tactics/equality.mli index ddef64502..d341db4f4 100644 --- a/tactics/equality.mli +++ b/tactics/equality.mli @@ -10,6 +10,7 @@ open Pp open Names open Term +open Context open Sign open Evd open Environ diff --git a/tactics/extratactics.ml4 b/tactics/extratactics.ml4 index 0ec167873..af04dcacb 100644 --- a/tactics/extratactics.ml4 +++ b/tactics/extratactics.ml4 @@ -271,6 +271,7 @@ END (* Hint Resolve *) open Term +open Vars open Coqlib let project_hint pri l2r r = diff --git a/tactics/inv.ml b/tactics/inv.ml index 7308b7091..b508fb83b 100644 --- a/tactics/inv.ml +++ b/tactics/inv.ml @@ -12,6 +12,8 @@ open Util open Names open Nameops open Term +open Vars +open Context open Termops open Namegen open Environ diff --git a/tactics/leminv.ml b/tactics/leminv.ml index c8a3ffd55..86651e76c 100644 --- a/tactics/leminv.ml +++ b/tactics/leminv.ml @@ -11,6 +11,7 @@ open Errors open Util open Names open Term +open Vars open Termops open Namegen open Sign diff --git a/tactics/refine.ml b/tactics/refine.ml index 160bcfc70..03b697e8f 100644 --- a/tactics/refine.ml +++ b/tactics/refine.ml @@ -51,6 +51,7 @@ open Errors open Util open Names open Term +open Vars open Termops open Namegen open Tacmach diff --git a/tactics/rewrite.ml4 b/tactics/rewrite.ml4 index 19a2f390b..30daa03ea 100644 --- a/tactics/rewrite.ml4 +++ b/tactics/rewrite.ml4 @@ -15,6 +15,7 @@ open Names open Nameops open Namegen open Term +open Vars open Termops open Reduction open Tacticals diff --git a/tactics/tacticals.mli b/tactics/tacticals.mli index 1d97e2b94..3ab04dcbd 100644 --- a/tactics/tacticals.mli +++ b/tactics/tacticals.mli @@ -10,6 +10,7 @@ open Loc open Pp open Names open Term +open Context open Sign open Tacmach open Proof_type diff --git a/tactics/tactics.ml b/tactics/tactics.ml index c531a34fa..a4b89f865 100644 --- a/tactics/tactics.ml +++ b/tactics/tactics.ml @@ -13,6 +13,8 @@ open Names open Nameops open Sign open Term +open Vars +open Context open Termops open Namegen open Declarations diff --git a/tactics/tactics.mli b/tactics/tactics.mli index 84040722e..f39ed97f8 100644 --- a/tactics/tactics.mli +++ b/tactics/tactics.mli @@ -10,6 +10,7 @@ open Loc open Pp open Names open Term +open Context open Environ open Sign open Tacmach diff --git a/toplevel/auto_ind_decl.ml b/toplevel/auto_ind_decl.ml index 3ba32da3c..56bdc810d 100644 --- a/toplevel/auto_ind_decl.ml +++ b/toplevel/auto_ind_decl.ml @@ -13,9 +13,10 @@ open Tacmach open Errors open Util open Pp +open Term +open Vars open Termops open Declarations -open Term open Names open Globnames open Inductiveops diff --git a/toplevel/autoinstance.ml b/toplevel/autoinstance.ml index b2a9aebdc..f8a76f874 100644 --- a/toplevel/autoinstance.ml +++ b/toplevel/autoinstance.ml @@ -12,6 +12,8 @@ open Pp open Printer open Names open Term +open Vars +open Context open Evd open Globnames (*i*) diff --git a/toplevel/autoinstance.mli b/toplevel/autoinstance.mli index 0be19e4e0..fcd46c3e8 100644 --- a/toplevel/autoinstance.mli +++ b/toplevel/autoinstance.mli @@ -11,6 +11,7 @@ open Globnames open Typeclasses open Names open Evd +open Context open Sign (** {6 Automatic detection of (some) record instances } *) diff --git a/toplevel/class.ml b/toplevel/class.ml index 8f8f70816..14473e46f 100644 --- a/toplevel/class.ml +++ b/toplevel/class.ml @@ -11,6 +11,7 @@ open Util open Pp open Names open Term +open Vars open Termops open Entries open Environ diff --git a/toplevel/classes.ml b/toplevel/classes.ml index 640bd0b08..78848f1c2 100644 --- a/toplevel/classes.ml +++ b/toplevel/classes.ml @@ -9,6 +9,8 @@ (*i*) open Names open Term +open Vars +open Context open Evd open Environ open Nametab diff --git a/toplevel/classes.mli b/toplevel/classes.mli index 736ba62a9..d05eff126 100644 --- a/toplevel/classes.mli +++ b/toplevel/classes.mli @@ -9,6 +9,7 @@ open Names open Decl_kinds open Term +open Context open Sign open Evd open Environ diff --git a/toplevel/command.ml b/toplevel/command.ml index 420de5d20..6a3d9a11a 100644 --- a/toplevel/command.ml +++ b/toplevel/command.ml @@ -11,6 +11,8 @@ open Errors open Util open Flags open Term +open Vars +open Context open Termops open Entries open Environ diff --git a/toplevel/discharge.ml b/toplevel/discharge.ml index 4dd00301f..aeb63c348 100644 --- a/toplevel/discharge.ml +++ b/toplevel/discharge.ml @@ -11,6 +11,7 @@ open Errors open Util open Sign open Term +open Vars open Entries open Declarations open Cooking diff --git a/toplevel/ide_slave.ml b/toplevel/ide_slave.ml index 2aa2cc36f..7a826c1da 100644 --- a/toplevel/ide_slave.ml +++ b/toplevel/ide_slave.ml @@ -182,7 +182,7 @@ let process_goal sigma g = let norm_constr = Reductionops.nf_evar sigma (Goal.V82.concl sigma g) in string_of_ppcmds (pr_goal_concl_style_env env norm_constr) in let process_hyp h_env d acc = - let d = Term.map_named_declaration (Reductionops.nf_evar sigma) d in + let d = Context.map_named_declaration (Reductionops.nf_evar sigma) d in (string_of_ppcmds (pr_var_decl h_env d)) :: acc in let hyps = List.rev (Environ.fold_named_context process_hyp env ~init: []) in diff --git a/toplevel/obligations.ml b/toplevel/obligations.ml index 8c7c377bf..53ee27f3b 100644 --- a/toplevel/obligations.ml +++ b/toplevel/obligations.ml @@ -14,6 +14,7 @@ open Declare open Term open Sign +open Vars open Names open Evd open Pp @@ -386,7 +387,7 @@ let obl_substitution expand obls deps = let subst_deps expand obls deps t = let subst = obl_substitution expand obls deps in - Term.replace_vars (List.map (fun (n, (_, b)) -> n, b) subst) t + Vars.replace_vars (List.map (fun (n, (_, b)) -> n, b) subst) t let rec prod_app t n = match kind_of_term (strip_outer_cast t) with @@ -420,8 +421,8 @@ let subst_prog expand obls ints prg = replace_appvars subst (Termops.refresh_universes prg.prg_type)) else let subst' = List.map (fun (n, (_, b)) -> n, b) subst in - (Term.replace_vars subst' prg.prg_body, - Term.replace_vars subst' (Termops.refresh_universes prg.prg_type)) + (Vars.replace_vars subst' prg.prg_body, + Vars.replace_vars subst' (Termops.refresh_universes prg.prg_type)) let subst_deps_obl obls obl = let t' = subst_deps true obls obl.obl_deps obl.obl_type in @@ -518,7 +519,7 @@ let compute_possible_guardness_evidences (n,_) fixbody fixtype = but doing it properly involves delta-reduction, and it finally doesn't seem to worth the effort (except for huge mutual fixpoints ?) *) - let m = Term.nb_prod fixtype in + let m = nb_prod fixtype in let ctx = fst (decompose_prod_n_assum m fixtype) in List.map_i (fun i _ -> i) 0 ctx diff --git a/toplevel/record.ml b/toplevel/record.ml index b6181590e..c5ec2d7e9 100644 --- a/toplevel/record.ml +++ b/toplevel/record.ml @@ -13,6 +13,7 @@ open Names open Globnames open Nameops open Term +open Vars open Environ open Declarations open Entries diff --git a/toplevel/record.mli b/toplevel/record.mli index 9e3781fd5..331bf9ed5 100644 --- a/toplevel/record.mli +++ b/toplevel/record.mli @@ -8,6 +8,7 @@ open Names open Term +open Context open Sign open Vernacexpr open Constrexpr diff --git a/toplevel/vernacentries.ml b/toplevel/vernacentries.ml index b1afb3b3e..8cf3767cb 100644 --- a/toplevel/vernacentries.ml +++ b/toplevel/vernacentries.ml @@ -170,7 +170,7 @@ let make_cases s = = Global.lookup_inductive i in Util.Array.fold_right2 (fun consname typ l -> - let al = List.rev (fst (Term.decompose_prod typ)) in + let al = List.rev (fst (decompose_prod typ)) in let al = Util.List.skipn np al in let rec rename avoid = function | [] -> [] @@ -303,7 +303,7 @@ let print_namespace ns = let print_constant k body = let t = match body.Declarations.const_type with - | Declarations.PolymorphicArity (ctx,a) -> Term.mkArity (ctx, Term.Type a.Declarations.poly_level) + | Declarations.PolymorphicArity (ctx,a) -> mkArity (ctx, Term.Type a.Declarations.poly_level) | Declarations.NonPolymorphicType t -> t in print_kn k ++ str":" ++ spc() ++ Printer.pr_type t -- cgit v1.2.3