aboutsummaryrefslogtreecommitdiffhomepage
path: root/kernel
diff options
context:
space:
mode:
authorGravatar herbelin <herbelin@85f007b7-540e-0410-9357-904b9bb8a0f7>2000-09-10 07:19:28 +0000
committerGravatar herbelin <herbelin@85f007b7-540e-0410-9357-904b9bb8a0f7>2000-09-10 07:19:28 +0000
commit79dc33cbc403ebab0bd1fe815c13f740f0a1b850 (patch)
treee38e167003d7dd97d95a59ea7c026a1629b346f8 /kernel
parentc0ff579606f2eba24bc834316d8bb7bcc076000d (diff)
Ajout d'un LetIn primitif.
Abstraction de constr via kind_of_constr dans une bonne partie du code. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@591 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'kernel')
-rw-r--r--kernel/abstraction.ml2
-rw-r--r--kernel/closure.ml366
-rw-r--r--kernel/closure.mli78
-rw-r--r--kernel/declarations.ml2
-rw-r--r--kernel/environ.ml51
-rw-r--r--kernel/environ.mli1
-rw-r--r--kernel/indtypes.ml93
-rw-r--r--kernel/inductive.ml2
-rw-r--r--kernel/instantiate.ml2
-rw-r--r--kernel/reduction.ml716
-rw-r--r--kernel/reduction.mli20
-rw-r--r--kernel/safe_typing.ml12
-rw-r--r--kernel/sign.ml51
-rw-r--r--kernel/sign.mli2
-rw-r--r--kernel/sosub.ml34
-rw-r--r--kernel/sosub.mli2
-rw-r--r--kernel/term.ml1193
-rw-r--r--kernel/term.mli192
-rw-r--r--kernel/type_errors.ml24
-rw-r--r--kernel/type_errors.mli25
-rw-r--r--kernel/typeops.ml338
21 files changed, 1860 insertions, 1346 deletions
diff --git a/kernel/abstraction.ml b/kernel/abstraction.ml
index 9df751b46..a6e5937a4 100644
--- a/kernel/abstraction.ml
+++ b/kernel/abstraction.ml
@@ -3,7 +3,7 @@
open Util
open Names
-open Generic
+(*i open Generic i*)
open Term
type abstraction_body = {
diff --git a/kernel/closure.ml b/kernel/closure.ml
index f452a6dfc..948361690 100644
--- a/kernel/closure.ml
+++ b/kernel/closure.ml
@@ -4,7 +4,6 @@
open Util
open Pp
open Term
-open Generic
open Names
open Environ
open Instantiate
@@ -31,6 +30,9 @@ let stop() =
(* sets of reduction kinds *)
type red_kind = BETA | DELTA of sorts oper | IOTA
+(* Hack: we use oper (Const "$LOCAL VAR$") for local variables *)
+let local_const_oper = Const (make_path [] (id_of_string "$LOCAL VAR$") CCI)
+
type reds = {
r_beta : bool;
r_delta : sorts oper -> bool; (* this is unsafe: exceptions may pop out *)
@@ -157,6 +159,58 @@ let infos_under infos =
i_tab = infos.i_tab }
+(* explicit substitutions of type 'a *)
+type 'a subs =
+ | ESID (* ESID = identity *)
+ | CONS of 'a * 'a subs (* CONS(t,S) = (S.t) parallel substitution *)
+ | SHIFT of int * 'a subs (* SHIFT(n,S) = (^n o S) terms in S are relocated *)
+ (* with n vars *)
+ | LIFT of int * 'a subs (* LIFT(n,S) = (%n S) stands for ((^n o S).n...1) *)
+
+(* operations of subs: collapses constructors when possible.
+ * Needn't be recursive if we always use these functions
+ *)
+
+let subs_cons(x,s) = CONS(x,s)
+
+let subs_liftn n = function
+ | ESID -> ESID (* the identity lifted is still the identity *)
+ (* (because (^1.1) --> id) *)
+ | LIFT (p,lenv) -> LIFT (p+n, lenv)
+ | lenv -> LIFT (n,lenv)
+
+let subs_lift a = subs_liftn 1 a
+
+let subs_shft = function
+ | (0, s) -> s
+ | (n, SHIFT (k,s1)) -> SHIFT (k+n, s1)
+ | (n, s) -> SHIFT (n,s)
+
+(* Expands de Bruijn k in the explicit substitution subs
+ * lams accumulates de shifts to perform when retrieving the i-th value
+ * the rules used are the following:
+ *
+ * [id]k --> k
+ * [S.t]1 --> t
+ * [S.t]k --> [S](k-1) if k > 1
+ * [^n o S] k --> [^n]([S]k)
+ * [(%n S)] k --> k if k <= n
+ * [(%n S)] k --> [^n]([S](k-n))
+ *
+ * the result is (Inr k) when the variable is just relocated
+ *)
+let rec exp_rel lams k subs =
+ match (k,subs) with
+ | (1, CONS (def,_)) -> Inl(lams,def)
+ | (_, CONS (_,l)) -> exp_rel lams (pred k) l
+ | (_, LIFT (n,_)) when k<=n -> Inr(lams+k)
+ | (_, LIFT (n,l)) -> exp_rel (n+lams) (k-n) l
+ | (_, SHIFT (n,s)) -> exp_rel (n+lams) k s
+ | (_, ESID) -> Inr(lams+k)
+
+let expand_rel k subs = exp_rel 0 k subs
+
+
(**** Call by value reduction ****)
(* The type of terms with closure. The meaning of the constructors and
@@ -185,7 +239,8 @@ let infos_under infos =
type cbv_value =
| VAL of int * constr
| LAM of name * constr * constr * cbv_value subs
- | FIXP of sorts oper * constr array * cbv_value subs * cbv_value list
+ | FIXP of fixpoint * cbv_value subs * cbv_value list
+ | COFIXP of cofixpoint * cbv_value subs * cbv_value list
| CONSTR of int * (section_path * int) * cbv_value array * cbv_value list
(* les vars pourraient etre des constr,
@@ -197,8 +252,10 @@ type cbv_value =
let rec shift_value n = function
| VAL (k,v) -> VAL ((k+n),v)
| LAM (x,a,b,s) -> LAM (x,a,b,subs_shft (n,s))
- | FIXP (op,bv,s,args) ->
- FIXP (op,bv,subs_shft (n,s), List.map (shift_value n) args)
+ | FIXP (fix,s,args) ->
+ FIXP (fix,subs_shft (n,s), List.map (shift_value n) args)
+ | COFIXP (cofix,s,args) ->
+ COFIXP (cofix,subs_shft (n,s), List.map (shift_value n) args)
| CONSTR (i,spi,vars,args) ->
CONSTR (i, spi, Array.map (shift_value n) vars,
List.map (shift_value n) args)
@@ -210,20 +267,23 @@ let rec shift_value n = function
* (S, (fix Fi {F0 := T0 .. Fn-1 := Tn-1}))
* -> (S. [S]F0 . [S]F1 ... . [S]Fn-1, Ti)
*)
-let contract_fixp env fix =
- let (bnum, bodies, make_body) = match fix with
- | DOPN(Fix(reci,i),bvect) ->
- (i, array_last bvect, (fun j -> FIXP(Fix(reci,j), bvect, env, [])))
- | DOPN(CoFix i,bvect) ->
- (i, array_last bvect, (fun j -> FIXP(CoFix j, bvect, env, [])))
- | _ -> anomaly "Closure.contract_fixp: not a (co)fixpoint"
- in
- let rec subst_bodies_from_i i subs = function
- | DLAM(_,t) -> subst_bodies_from_i (i+1) (subs_cons (make_body i, subs)) t
- | DLAMV(_,bds) -> (subs_cons (make_body i, subs), bds.(bnum))
- | _ -> anomaly "Closure.contract_fixp: malformed (co)fixpoint"
+let contract_fixp env ((reci,i),(_,_,bds as bodies)) =
+ let make_body j = FIXP(((reci,j),bodies), env, []) in
+ let n = Array.length bds in
+ let rec subst_bodies_from_i i subs =
+ if i=n then subs
+ else subst_bodies_from_i (i+1) (subs_cons (make_body i, subs))
+ in
+ subst_bodies_from_i 0 env, bds.(i)
+
+let contract_cofixp env (i,(_,_,bds as bodies)) =
+ let make_body j = COFIXP((j,bodies), env, []) in
+ let n = Array.length bds in
+ let rec subst_bodies_from_i i subs =
+ if i=n then subs
+ else subst_bodies_from_i (i+1) (subs_cons (make_body i, subs))
in
- subst_bodies_from_i 0 env bodies
+ subst_bodies_from_i 0 env, bds.(i)
(* type of terms with a hole. This hole can appear only under AppL or Case.
@@ -274,12 +334,13 @@ let red_allowed flags stack rk =
*)
let strip_appl head stack =
match head with
- | FIXP (op,bv,env,app) -> (FIXP(op,bv,env,[]), stack_app app stack)
+ | FIXP (fix,env,app) -> (FIXP(fix,env,[]), stack_app app stack)
+ | COFIXP (cofix,env,app) -> (COFIXP(cofix,env,[]), stack_app app stack)
| CONSTR (i,spi,vars,app) -> (CONSTR(i,spi,vars,[]), stack_app app stack)
| _ -> (head, stack)
-(* Invariant: if the result of norm_head is CONSTR or FIXP, it last
+(* Invariant: if the result of norm_head is CONSTR or (CO)FIXP, it last
* argument is [].
* Because we must put all the applied terms in the stack.
*)
@@ -298,12 +359,18 @@ let rec check_app_constr redfun = function
| _ -> false)
| (_::l, n) -> check_app_constr redfun (l,(pred n))
-let fixp_reducible redfun flgs op stk =
+let fixp_reducible redfun flgs ((reci,i),_) stk =
+ if red_allowed flgs stk IOTA then
+ match stk with (* !!! for Acc_rec: reci.(i) = -2 *)
+ | APP(appl,_) -> reci.(i) >=0 & check_app_constr redfun (appl, reci.(i))
+ | _ -> false
+ else
+ false
+
+let cofixp_reducible redfun flgs _ stk =
if red_allowed flgs stk IOTA then
- match (op,stk) with (* !!! for Acc_rec: reci.(i) = -2 *)
- | (Fix (reci,i), APP(appl,_)) ->
- (reci.(i) >= 0 & check_app_constr redfun (appl, reci.(i)))
- | (CoFix i, (CASE _ | APP(_,CASE _))) -> true
+ match stk with
+ | (CASE _ | APP(_,CASE _)) -> true
| _ -> false
else
false
@@ -318,65 +385,72 @@ let mindsp_nparams env sp =
* constructor, a lambda or a fixp in the head. If not, it is a value
* and is completely computed here. The head redexes are NOT reduced:
* the function returns the pair of a cbv_value and its stack. *
- * Invariant: if the result of norm_head is CONSTR or FIXP, it last
+ * Invariant: if the result of norm_head is CONSTR or (CO)FIXP, it last
* argument is []. Because we must put all the applied terms in the
* stack. *)
let rec norm_head info env t stack =
(* no reduction under binders *)
- match t with
+ match kind_of_term t with
(* stack grows (remove casts) *)
- | DOPN (AppL,appl) -> (* Applied terms are normalized immediately;
+ | IsAppL (head,args) -> (* Applied terms are normalized immediately;
they could be computed when getting out of the stack *)
- (match Array.to_list appl with
- | head::args ->
- let nargs = List.map (cbv_stack_term info TOP env) args in
- norm_head info env head (stack_app nargs stack)
- | [] -> anomaly "norm_head : malformed constr AppL [||]")
- | DOPN (MutCase _,_) ->
- let (ci,p,c,v) = destCase t in
- norm_head info env c (CASE(p,v,ci,env,stack))
- | DOP2 (Cast,ct,c) -> norm_head info env ct stack
+ let nargs = List.map (cbv_stack_term info TOP env) args in
+ norm_head info env head (stack_app nargs stack)
+ | IsMutCase (ci,p,c,v) -> norm_head info env c (CASE(p,v,ci,env,stack))
+ | IsCast (ct,_) -> norm_head info env ct stack
(* constants, axioms
* the first pattern is CRUCIAL, n=0 happens very often:
* when reducing closed terms, n is always 0 *)
- | Rel i -> (match expand_rel i env with
+ | IsRel i -> (match expand_rel i env with
| Inl (0,v) ->
reduce_const_body (cbv_norm_more info) v stack
| Inl (n,v) ->
reduce_const_body
(cbv_norm_more info) (shift_value n v) stack
| Inr n -> (VAL(0, Rel n), stack))
- | DOPN ((Const _ | Evar _ | Abst _) as op, vars)
- when red_allowed info.i_flags stack (DELTA op) ->
- let normt = DOPN(op, Array.map (cbv_norm_term info env) vars) in
- (match const_value_cache info normt with
- | Some body -> reduce_const_body (cbv_norm_more info) body stack
- | None -> (VAL(0,normt), stack))
+ | IsConst (sp,vars) ->
+ let normt = mkConst (sp,Array.map (cbv_norm_term info env) vars) in
+ if red_allowed info.i_flags stack (DELTA (Const sp)) then
+ match const_value_cache info normt with
+ | Some body -> reduce_const_body (cbv_norm_more info) body stack
+ | None -> (VAL(0,normt), stack)
+ else (VAL(0,normt), stack)
+ | IsLetIn (x, b, t, c) ->
+ if red_allowed info.i_flags stack (DELTA local_const_oper) then
+ let b = cbv_stack_term info TOP env b in
+ norm_head info (subs_cons (b,env)) c stack
+ else
+ let normt =
+ mkLetIn (x, cbv_norm_term info env b,
+ cbv_norm_term info env t,
+ cbv_norm_term info (subs_lift env) c) in
+ (VAL(0,normt), stack) (* Considérer une coupure commutative ? *)
+ | IsEvar (n,vars) ->
+ let normt = mkEvar (n,Array.map (cbv_norm_term info env) vars) in
+ if red_allowed info.i_flags stack (DELTA (Evar n)) then
+ match const_value_cache info normt with
+ | Some body -> reduce_const_body (cbv_norm_more info) body stack
+ | None -> (VAL(0,normt), stack)
+ else (VAL(0,normt), stack)
(* non-neutral cases *)
- | DOP2 (Lambda,a,DLAM(x,b)) -> (LAM(x,a,b,env), stack)
- | DOPN ((Fix _ | CoFix _) as op, v) -> (FIXP(op,v,env,[]), stack)
- | DOPN (MutConstruct(spi,i),vars) ->
+ | IsLambda (x,a,b) -> (LAM(x,a,b,env), stack)
+ | IsFix fix -> (FIXP(fix,env,[]), stack)
+ | IsCoFix cofix -> (COFIXP(cofix,env,[]), stack)
+ | IsMutConstruct ((spi,i),vars) ->
(CONSTR(i,spi, Array.map (cbv_stack_term info TOP env) vars,[]), stack)
(* neutral cases *)
- | (VAR _ | DOP0 _) -> (VAL(0, t), stack)
- | DOP1 (op, nt) -> (VAL(0, DOP1(op, cbv_norm_term info env nt)), stack)
- | DOP2 (op,a,b) ->
- (VAL(0, DOP2(op, cbv_norm_term info env a, cbv_norm_term info env b)),
- stack)
- | DOPN (op,vars) ->
- (VAL(0, DOPN(op, Array.map (cbv_norm_term info env) vars)), stack)
- | DOPL (op,l) ->
- (VAL(0, DOPL(op, List.map (cbv_norm_term info env) l)), stack)
- | DLAM (x,t) ->
- (VAL(0, DLAM(x, cbv_norm_term info (subs_lift env) t)), stack)
- | DLAMV (x,ve) ->
- (VAL(0, DLAMV(x, Array.map(cbv_norm_term info (subs_lift env)) ve)),
- stack)
-
+ | (IsVar _ | IsSort _ | IsMeta _ | IsXtra _ ) -> (VAL(0, t), stack)
+ | IsMutInd (sp,vars) ->
+ (VAL(0, mkMutInd (sp, Array.map (cbv_norm_term info env) vars)), stack)
+ | IsProd (x,t,c) ->
+ (VAL(0, mkProd (x, cbv_norm_term info env t,
+ cbv_norm_term info (subs_lift env) c)),
+ stack)
+ | IsAbst (_,_) -> failwith "No longer implemented"
(* cbv_stack_term performs weak reduction on constr t under the subs
* env, with context stack, i.e. ([env]t stack). First computes weak
@@ -392,12 +466,17 @@ and cbv_stack_term info stack env t =
let subs = subs_cons (arg,env) in
cbv_stack_term info (stack_app args stk) subs b
- (* a Fix applied enough,
- constructor guard satisfied or Cofix in a Case -> IOTA *)
- | (FIXP(op,bv,env,_), stk)
- when fixp_reducible (cbv_norm_more info) info.i_flags op stk ->
- let (envf,redfix) = contract_fixp env (DOPN(op,bv)) in
- cbv_stack_term info stk envf redfix
+ (* a Fix applied enough -> IOTA *)
+ | (FIXP(fix,env,_), stk)
+ when fixp_reducible (cbv_norm_more info) info.i_flags fix stk ->
+ let (envf,redfix) = contract_fixp env fix in
+ cbv_stack_term info stk envf redfix
+
+ (* constructor guard satisfied or Cofix in a Case -> IOTA *)
+ | (COFIXP(cofix,env,_), stk)
+ when cofixp_reducible (cbv_norm_more info) info.i_flags cofix stk ->
+ let (envf,redfix) = contract_cofixp env cofix in
+ cbv_stack_term info stk envf redfix
(* constructor in a Case -> IOTA
(use red_under because we know there is a Case) *)
@@ -414,7 +493,8 @@ and cbv_stack_term info stack env t =
(* may be reduced later by application *)
| (head, TOP) -> head
- | (FIXP(op,bv,env,_), APP(appl,TOP)) -> FIXP(op,bv,env,appl)
+ | (FIXP(fix,env,_), APP(appl,TOP)) -> FIXP(fix,env,appl)
+ | (COFIXP(cofix,env,_), APP(appl,TOP)) -> COFIXP(cofix,env,appl)
| (CONSTR(n,spi,vars,_), APP(appl,TOP)) -> CONSTR(n,spi,vars,appl)
(* definitely a value *)
@@ -452,19 +532,28 @@ and cbv_norm_term info env t =
(* reduction of a cbv_value to a constr *)
and cbv_norm_value info = function (* reduction under binders *)
| VAL (n,v) -> lift n v
- | LAM (x,a,b,env) -> DOP2(Lambda, cbv_norm_term info env a,
- DLAM(x,cbv_norm_term info (subs_lift env) b))
- | FIXP (op,cl,env,args) ->
+ | LAM (x,a,b,env) ->
+ mkLambda (x, cbv_norm_term info env a,
+ cbv_norm_term info (subs_lift env) b)
+ | FIXP ((lij,(lty,lna,bds)),env,args) ->
+ applistc
+ (mkFix (lij,
+ (Array.map (cbv_norm_term info env) lty, lna,
+ Array.map (cbv_norm_term info
+ (subs_liftn (Array.length lty) env)) bds)))
+ (List.map (cbv_norm_value info) args)
+ | COFIXP ((j,(lty,lna,bds)),env,args) ->
applistc
- (DOPN(op, Array.map (cbv_norm_term info env) cl))
+ (mkCoFix (j,
+ (Array.map (cbv_norm_term info env) lty, lna,
+ Array.map (cbv_norm_term info
+ (subs_liftn (Array.length lty) env)) bds)))
(List.map (cbv_norm_value info) args)
| CONSTR (n,spi,vars,args) ->
applistc
- (DOPN (MutConstruct(spi,n), Array.map (cbv_norm_value info) vars))
+ (mkMutConstruct ((spi,n), Array.map (cbv_norm_value info) vars))
(List.map (cbv_norm_value info) args)
-
-
type 'a cbv_infos = (cbv_value, 'a) infos
(* constant bodies are normalized at the first expansion *)
@@ -499,22 +588,40 @@ let cbv_norm infos constr =
* substitution applied to a constr
*)
-type 'oper freeze = {
+type freeze = {
mutable norm: bool;
- mutable term: 'oper frterm }
+ mutable term: frterm }
-and 'oper frterm =
+and frterm =
| FRel of int
| FVAR of identifier
- | FOP0 of 'oper
- | FOP1 of 'oper * 'oper freeze
- | FOP2 of 'oper * 'oper freeze * 'oper freeze
- | FOPN of 'oper * 'oper freeze array
- | FOPL of 'oper * 'oper freeze list
- | FLAM of name * 'oper freeze * 'oper term * 'oper freeze subs
- | FLAMV of name * 'oper freeze array * 'oper term array * 'oper freeze subs
- | FLIFT of int * 'oper freeze
- | FFROZEN of 'oper term * 'oper freeze subs
+ | FOP0 of sorts oper
+ | FOP1 of sorts oper * freeze
+ | FOP2 of sorts oper * freeze * freeze
+ | FOPN of sorts oper * freeze array
+ | FLAM of name * freeze * constr * freeze subs
+ | FLAMV of name * freeze array * constr array * freeze subs
+ | FLam of name * type_freeze * freeze * constr * freeze subs
+ | FPrd of name * type_freeze * freeze * constr * freeze subs
+ | FLet of name * freeze * type_freeze * freeze * constr * freeze subs
+ | FLIFT of int * freeze
+ | FFROZEN of constr * freeze subs
+
+(* Cas où typed_type est casté en interne
+and type_freeze = freeze * sorts
+ *)
+(* Cas où typed_type n'est pas casté *)
+and type_freeze = freeze
+(**)
+
+(*
+let typed_map f t = f (body_of_type t), level_of_type t
+let typed_unmap f (t,s) = make_typed (f t) s
+*)
+(**)
+let typed_map f t = f (body_of_type t)
+let typed_unmap f t = make_typed_lazy (f t) (fun _ -> assert false)
+(**)
let frterm_of v = v.term
let is_val v = v.norm
@@ -579,8 +686,6 @@ let rec traverse_term env t =
term = FOP2 (op, traverse_term env a, traverse_term env b)}
| DOPN (op,v) ->
{ norm = false; term = FOPN (op, Array.map (traverse_term env) v) }
- | DOPL (op,l) ->
- { norm = false; term = FOPL (op, List.map (traverse_term env) l) }
| DLAM (x,a) ->
{ norm = false;
term = FLAM (x, traverse_term (subs_lift env) a, a, env) }
@@ -588,9 +693,24 @@ let rec traverse_term env t =
{ norm = (ve=[||]);
term = FLAMV (x, Array.map (traverse_term (subs_lift env)) ve,
ve, env) }
+ | CLam (n,t,c) ->
+ { norm = false;
+ term = FLam (n, traverse_type env t, traverse_term (subs_lift env) c,
+ c, env) }
+ | CPrd (n,t,c) ->
+ { norm = false;
+ term = FPrd (n, traverse_type env t, traverse_term (subs_lift env) c,
+ c, env) }
+ | CLet (n,b,t,c) ->
+ { norm = false;
+ term = FLet (n, traverse_term env b, traverse_type env t,
+ traverse_term (subs_lift env) c,
+ c, env) }
+
+and traverse_type env = typed_map (traverse_term env)
(* Back to regular terms: remove all FFROZEN, keep casts (since this
- * fun is not dedicated to the Calulus of Constructions).
+ * fun is not dedicated to the Calculus of Constructions).
*)
let rec lift_term_of_freeze lfts v =
match v.term with
@@ -601,10 +721,19 @@ let rec lift_term_of_freeze lfts v =
| FOP2 (op,a,b) ->
DOP2 (op, lift_term_of_freeze lfts a, lift_term_of_freeze lfts b)
| FOPN (op,ve) -> DOPN (op, Array.map (lift_term_of_freeze lfts) ve)
- | FOPL (op,l) -> DOPL (op, List.map (lift_term_of_freeze lfts) l)
| FLAM (x,a,_,_) -> DLAM (x, lift_term_of_freeze (el_lift lfts) a)
| FLAMV (x,ve,_,_) ->
DLAMV (x, Array.map (lift_term_of_freeze (el_lift lfts)) ve)
+ | FLam (n,t,c,_,_) ->
+ CLam (n, typed_unmap (lift_term_of_freeze lfts) t,
+ lift_term_of_freeze (el_lift lfts) c)
+ | FPrd (n,t,c,_,_) ->
+ CPrd (n, typed_unmap (lift_term_of_freeze lfts) t,
+ lift_term_of_freeze (el_lift lfts) c)
+ | FLet (n,b,t,c,_,_) ->
+ CLet (n, lift_term_of_freeze lfts b,
+ typed_unmap (lift_term_of_freeze lfts) t,
+ lift_term_of_freeze (el_lift lfts) c)
| FLIFT (k,a) -> lift_term_of_freeze (el_shft k lfts) a
| FFROZEN (t,env) ->
let unfv = freeze_assign v (traverse_term env t) in
@@ -629,30 +758,34 @@ let rec fstrong unfreeze_fun lfts v =
| FOP2 (op,a,b) ->
DOP2 (op, fstrong unfreeze_fun lfts a, fstrong unfreeze_fun lfts b)
| FOPN (op,ve) -> DOPN (op, Array.map (fstrong unfreeze_fun lfts) ve)
- | FOPL (op,l) -> DOPL (op, List.map (fstrong unfreeze_fun lfts) l)
| FLAM (x,a,_,_) -> DLAM (x, fstrong unfreeze_fun (el_lift lfts) a)
| FLAMV (x,ve,_,_) ->
DLAMV (x, Array.map (fstrong unfreeze_fun (el_lift lfts)) ve)
+ | FLam (n,t,c,_,_) ->
+ CLam (n, typed_unmap (fstrong unfreeze_fun lfts) t,
+ fstrong unfreeze_fun (el_lift lfts) c)
+ | FPrd (n,t,c,_,_) ->
+ CPrd (n, typed_unmap (fstrong unfreeze_fun lfts) t,
+ fstrong unfreeze_fun (el_lift lfts) c)
+ | FLet (n,b,t,c,_,_) ->
+ CLet (n, fstrong unfreeze_fun lfts b,
+ typed_unmap (fstrong unfreeze_fun lfts) t,
+ fstrong unfreeze_fun (el_lift lfts) c)
| FLIFT (k,a) -> fstrong unfreeze_fun (el_shft k lfts) a
| FFROZEN _ -> anomaly "Closure.fstrong"
-(* Build a freeze, which represents the substitution of arg in fun_body.
+(* Build a freeze, which represents the substitution of arg in t
* Used to constract a beta-redex:
- * [^depth](FLAM(S,t)) arg -> [(^depth o S).arg]t
- * We also deal with FLIFT that would have been inserted between the
- * Lambda and FLAM operators. This never happens in practice.
+ * [^depth](FLam(S,t)) arg -> [(^depth o S).arg]t
*)
-let rec contract_subst depth fun_body arg =
- match fun_body.term with
- FLAM(_,_,t,subs) -> freeze (subs_cons (arg, subs_shft (depth,subs))) t
- | FLIFT(k,fb) -> contract_subst (depth+k) fb arg
- | _ -> anomaly "Closure.contract_subst: malformed function"
+let rec contract_subst depth t subs arg =
+ freeze (subs_cons (arg, subs_shft (depth,subs))) t
(* Calculus of Constructions *)
-type fconstr = sorts oper freeze
+type fconstr = freeze
let inject constr = freeze ESID constr
@@ -760,6 +893,7 @@ and whnf_frterm info ft =
| None -> { norm = array_for_all is_val vars; term = ft.term })
else
ft
+
| FOPN (MutCase ci,cl) ->
if red_under info.i_flags IOTA then
let c = unfreeze (infos_under info) cl.(1) in
@@ -777,8 +911,11 @@ and whnf_frterm info ft =
else
ft
- | FRel _ | FVAR _ | FOP0 _ -> { norm = true; term = ft.term }
- | _ -> ft
+ | FLet (na,b,_,_,t,subs) -> warning "Should be catch in whnf_term";
+ contract_subst 0 t subs b
+
+ | FRel _ | FVAR _ | FOP0 _ -> { norm = true; term = ft.term }
+ | FOPN _ | FOP2 _ | FOP1 _ | FLam _ | FPrd _ | FLAM _ | FLAMV _ -> ft
(* Weak head reduction: case of the application (head appl) *)
and whnf_apply info head appl =
@@ -788,8 +925,8 @@ and whnf_apply info head appl =
else
let (lft_hd,whd,args) = strip_frterm 0 head [appl] in
match whd.term with
- | FOP2(Lambda,_,b) when red_under info.i_flags BETA ->
- let vbody = contract_subst lft_hd (unfreeze info b) args.(0) in
+ | FLam (_,_,_,t,subs) when red_under info.i_flags BETA ->
+ let vbody = contract_subst lft_hd t subs args.(0) in
whnf_apply info vbody (array_tl args)
| (FOPN(Fix(reci,bnum), tb) as fx)
when red_under info.i_flags IOTA
@@ -815,21 +952,30 @@ and whnf_term info env t =
| DOP0 op -> {norm = true; term = FOP0 op }
| DOP1 (op, nt) -> { norm = false; term = FOP1 (op, freeze env nt) }
| DOP2 (Cast,ct,c) -> whnf_term info env ct (* remove outer casts *)
- | DOP2 (op,a,b) -> (* Lambda Prod *)
- { norm = false; term = FOP2 (op, freeze env a, freeze env b) }
+ | DOP2 (_,_,_) -> assert false (* Lambda|Prod made explicit *)
| DOPN ((AppL | Const _ | Evar _ | Abst _ | MutCase _) as op, ve) ->
whnf_frterm info { norm = false; term = FOPN (op, freeze_vect env ve) }
| DOPN ((MutInd _ | MutConstruct _) as op,v) ->
{ norm = (v=[||]); term = FOPN (op, freeze_vect env v) }
| DOPN (op,v) ->
{ norm = false; term = FOPN (op, freeze_vect env v) } (* Fix CoFix *)
- | DOPL (op,l) -> { norm = false; term = FOPL (op, freeze_list env l) }
| DLAM (x,a) ->
{ norm = false; term = FLAM (x, freeze (subs_lift env) a, a, env) }
| DLAMV (x,ve) ->
{ norm = (ve=[||]);
term = FLAMV (x, freeze_vect (subs_lift env) ve, ve, env) }
-
+ | CLam (n,t,c) ->
+ { norm = false;
+ term = FLam (n, typed_map (freeze env) t, freeze (subs_lift env) c,
+ c, env) }
+ | CPrd (n,t,c) ->
+ { norm = false;
+ term = FPrd (n, typed_map (freeze env) t, freeze (subs_lift env) c,
+ c, env) }
+
+ (* WHNF removes LetIn (see Paula Severi) *)
+ | CLet (n,b,t,c) -> whnf_term info (subs_cons (freeze env b,env)) c
+
(* parameterized norm *)
let norm_val info v =
if !stats then begin
diff --git a/kernel/closure.mli b/kernel/closure.mli
index 0cba4cb87..940cd2664 100644
--- a/kernel/closure.mli
+++ b/kernel/closure.mli
@@ -4,7 +4,7 @@
(*i*)
open Pp
open Names
-open Generic
+(*i open Generic i*)
open Term
open Evd
open Environ
@@ -54,17 +54,29 @@ val betadeltaiota : flags
val hnf_flags : flags
+(*s Explicit substitutions of type ['a]. [ESID] = identity.
+ [CONS(t,S)] = $S.t$ i.e. parallel substitution. [SHIFT(n,S)] =
+ $(\uparrow n~o~S)$ i.e. terms in S are relocated with n vars.
+ [LIFT(n,S)] = $(\%n~S)$ stands for $((\uparrow n~o~S).n...1)$. *)
+type 'a subs =
+ | ESID
+ | CONS of 'a * 'a subs
+ | SHIFT of int * 'a subs
+ | LIFT of int * 'a subs
(*s Call by value functions *)
type cbv_value =
| VAL of int * constr
| LAM of name * constr * constr * cbv_value subs
- | FIXP of sorts oper * constr array * cbv_value subs * cbv_value list
+ | FIXP of fixpoint * cbv_value subs * cbv_value list
+ | COFIXP of cofixpoint * cbv_value subs * cbv_value list
| CONSTR of int * (section_path * int) * cbv_value array * cbv_value list
val shift_value : int -> cbv_value -> cbv_value
-val contract_fixp : cbv_value subs -> constr -> cbv_value subs * constr
+(*i Private ??
+val contract_fixp : cbv_value subs -> fixpoint -> cbv_value subs * constr
+i*)
type stack =
| TOP
@@ -78,8 +90,10 @@ val strip_appl : cbv_value -> stack -> cbv_value * stack
val red_allowed : flags -> stack -> red_kind -> bool
val reduce_const_body :
(cbv_value -> cbv_value) -> cbv_value -> stack -> cbv_value * stack
+(*i Private ??
val fixp_reducible :
- (cbv_value -> cbv_value) -> flags -> sorts oper -> stack -> bool
+ (cbv_value -> cbv_value) -> flags -> fixpoint -> stack -> bool
+i*)
(* normalization of a constr: the two functions to know... *)
type 'a cbv_infos
@@ -99,45 +113,49 @@ val cbv_norm_value : 'a cbv_infos -> cbv_value -> constr
(*s Lazy reduction. *)
-type 'a freeze
+type freeze
-type 'a frterm =
+type frterm =
| FRel of int
| FVAR of identifier
- | FOP0 of 'a
- | FOP1 of 'a * 'a freeze
- | FOP2 of 'a * 'a freeze * 'a freeze
- | FOPN of 'a * 'a freeze array
- | FOPL of 'a * 'a freeze list
- | FLAM of name * 'a freeze * 'a term * 'a freeze subs
- | FLAMV of name * 'a freeze array * 'a term array * 'a freeze subs
- | FLIFT of int * 'a freeze
- | FFROZEN of 'a term * 'a freeze subs
+ | FOP0 of sorts oper
+ | FOP1 of sorts oper * freeze
+ | FOP2 of sorts oper * freeze * freeze
+ | FOPN of sorts oper * freeze array
+ | FLAM of name * freeze * constr * freeze subs
+ | FLAMV of name * freeze array * constr array * freeze subs
+ | FLam of name * type_freeze * freeze * constr * freeze subs
+ | FPrd of name * type_freeze * freeze * constr * freeze subs
+ | FLet of name * freeze * type_freeze * freeze * constr * freeze subs
+ | FLIFT of int * freeze
+ | FFROZEN of constr * freeze subs
-val frterm_of : 'a freeze -> 'a frterm
-val is_val : 'a freeze -> bool
+and type_freeze = freeze
-val lift_frterm : int -> 'a freeze -> 'a freeze
-val lift_freeze : int -> 'a freeze -> 'a freeze
+val frterm_of : freeze -> frterm
+val is_val : freeze -> bool
-val freeze : 'a freeze subs -> 'a term -> 'a freeze
-val freeze_vect : 'a freeze subs -> 'a term array -> 'a freeze array
-val freeze_list : 'a freeze subs -> 'a term list -> 'a freeze list
+val lift_frterm : int -> freeze -> freeze
+val lift_freeze : int -> freeze -> freeze
-val traverse_term : 'a freeze subs -> 'a term -> 'a freeze
-val lift_term_of_freeze : lift_spec -> 'a freeze -> 'a term
+val freeze : freeze subs -> constr -> freeze
+val freeze_vect : freeze subs -> constr array -> freeze array
+val freeze_list : freeze subs -> constr list -> freeze list
+
+val traverse_term : freeze subs -> constr -> freeze
+val lift_term_of_freeze : lift_spec -> freeze -> constr
(* Back to constr *)
-val fstrong : ('a freeze -> 'a freeze) -> lift_spec -> 'a freeze -> 'a term
-val term_of_freeze : 'a freeze -> 'a term
-val applist_of_freeze : 'a freeze array -> 'a term list
+val fstrong : (freeze -> freeze) -> lift_spec -> freeze -> constr
+val term_of_freeze : freeze -> constr
+val applist_of_freeze : freeze array -> constr list
(* contract a substitution *)
-val contract_subst : int -> 'a freeze -> 'a freeze -> 'a freeze
+val contract_subst : int -> constr -> freeze subs -> freeze -> freeze
(* Calculus of Constructions *)
-type fconstr = sorts oper freeze
+type fconstr = freeze
val inject : constr -> fconstr
val strip_frterm :
@@ -146,7 +164,7 @@ val strip_freeze : fconstr -> int * fconstr * fconstr array
(* Auxiliary functions for (co)fixpoint reduction *)
-val contract_fix_vect : (fconstr -> fconstr) -> sorts oper frterm -> fconstr
+val contract_fix_vect : (fconstr -> fconstr) -> frterm -> fconstr
val copy_case : case_info -> fconstr array -> fconstr -> fconstr
diff --git a/kernel/declarations.ml b/kernel/declarations.ml
index e83e1e509..a5cb164d0 100644
--- a/kernel/declarations.ml
+++ b/kernel/declarations.ml
@@ -3,7 +3,7 @@
open Names
open Univ
-open Generic
+(*i open Generic i*)
open Term
open Sign
diff --git a/kernel/environ.ml b/kernel/environ.ml
index 217a7f989..4909e4444 100644
--- a/kernel/environ.ml
+++ b/kernel/environ.ml
@@ -6,7 +6,7 @@ open Util
open Names
open Sign
open Univ
-open Generic
+(*i open Generic i*)
open Term
open Declarations
open Abstraction
@@ -229,32 +229,40 @@ let id_of_global env = function
assert false
let hdchar env c =
- let rec hdrec k = function
- | DOP2((Prod|Lambda),_,DLAM(_,c)) -> hdrec (k+1) c
- | DOP2(Cast,c,_) -> hdrec k c
- | DOPN(AppL,cl) -> hdrec k (array_hd cl)
- | DOPN(Const _,_) as x ->
- let c = lowercase_first_char (basename (path_of_const x)) in
+ let rec hdrec k c =
+ match kind_of_term c with
+ | IsProd (_,_,c) -> hdrec (k+1) c
+ | IsLambda (_,_,c) -> hdrec (k+1) c
+ | IsLetIn (_,_,_,c) -> hdrec (k+1) c
+ | IsCast (c,_) -> hdrec k c
+ | IsAppL (f,l) -> hdrec k f
+ | IsConst (sp,_) ->
+ let c = lowercase_first_char (basename sp) in
if c = "?" then "y" else c
- | DOPN(Abst _,_) as x ->
- lowercase_first_char (basename (path_of_abst x))
- | DOPN(MutInd (sp,i) as x,_) ->
+ | IsMutInd ((sp,i) as x,_) ->
if i=0 then
lowercase_first_char (basename sp)
else
- let na = id_of_global env x in lowercase_first_char na
- | DOPN(MutConstruct(sp,i) as x,_) ->
- let na = id_of_global env x in String.lowercase(List.hd(explode_id na))
- | VAR id -> lowercase_first_char id
- | DOP0(Sort s) -> sort_hdchar s
- | Rel n ->
+ let na = id_of_global env (MutInd x) in lowercase_first_char na
+ | IsMutConstruct ((sp,i) as x,_) ->
+ let na = id_of_global env (MutConstruct x) in
+ String.lowercase(List.hd(explode_id na))
+ | IsVar id -> lowercase_first_char id
+ | IsSort s -> sort_hdchar s
+ | IsRel n ->
(if n<=k then "p" (* the initial term is flexible product/function *)
else
try match lookup_rel_type (n-k) env with
| Name id,_ -> lowercase_first_char id
| Anonymous,t -> hdrec 0 (lift (n-k) (body_of_type t))
with Not_found -> "y")
- | _ -> "y"
+ | IsFix ((_,i),(_,ln,_)) ->
+ let id = match List.nth ln i with Name id -> id | _ -> assert false in
+ lowercase_first_char id
+ | IsCoFix (i,(_,ln,_)) ->
+ let id = match List.nth ln i with Name id -> id | _ -> assert false in
+ lowercase_first_char id
+ | IsMeta _|IsXtra _|IsAbst (_, _)|IsEvar _|IsMutCase (_, _, _, _) -> "y"
in
hdrec 0 c
@@ -266,14 +274,14 @@ let named_hd env a = function
| Anonymous -> Name (id_of_string (hdchar env a))
| x -> x
-let prod_name env (n,a,b) = mkProd (named_hd env a n) a b
-let lambda_name env (n,a,b) = mkLambda (named_hd env a n) a b
+let prod_name env (n,a,b) = mkProd (named_hd env a n, a, b)
+let lambda_name env (n,a,b) = mkLambda (named_hd env a n, a, b)
let it_prod_name env = List.fold_left (fun c (n,t) ->prod_name env (n,t,c))
let it_lambda_name env = List.fold_left (fun c (n,t) ->lambda_name env (n,t,c))
-let prod_create env (a,b) = mkProd (named_hd env a Anonymous) a b
-let lambda_create env (a,b) = mkLambda (named_hd env a Anonymous) a b
+let prod_create env (a,b) = mkProd (named_hd env a Anonymous, a, b)
+let lambda_create env (a,b) = mkLambda (named_hd env a Anonymous, a, b)
let name_assumption env (na,c,t) =
match c with
@@ -286,6 +294,7 @@ let lambda_assum_name env b d = mkLambda_or_LetIn (name_assumption env d) b
let it_mkProd_or_LetIn_name env = List.fold_left (prod_assum_name env)
let it_mkLambda_or_LetIn_name env = List.fold_left (lambda_assum_name env)
+let it_mkProd_wo_LetIn = List.fold_left (fun c d -> mkProd_wo_LetIn d c)
let it_mkProd_or_LetIn = List.fold_left (fun c d -> mkProd_or_LetIn d c)
let it_mkLambda_or_LetIn = List.fold_left (fun c d -> mkLambda_or_LetIn d c)
diff --git a/kernel/environ.mli b/kernel/environ.mli
index 981be607f..b99410bd3 100644
--- a/kernel/environ.mli
+++ b/kernel/environ.mli
@@ -130,6 +130,7 @@ val it_prod_name : env -> constr -> (name * constr) list -> constr
val it_mkLambda_or_LetIn_name : env -> constr -> rel_context -> constr
val it_mkProd_or_LetIn_name : env -> constr -> rel_context -> constr
+val it_mkProd_wo_LetIn : constr -> rel_context -> constr
val it_mkLambda_or_LetIn : constr -> rel_context -> constr
val it_mkProd_or_LetIn : constr -> rel_context -> constr
diff --git a/kernel/indtypes.ml b/kernel/indtypes.ml
index 0536b1f2f..a37e469bd 100644
--- a/kernel/indtypes.ml
+++ b/kernel/indtypes.ml
@@ -3,7 +3,7 @@
open Util
open Names
-open Generic
+(*i open Generic i*)
open Term
open Declarations
open Inductive
@@ -92,14 +92,6 @@ let mind_extract_and_check_params mie =
List.iter (fun (_,c,_,_) -> check_params params (extract nparams c)) l;
params
-let decomp_all_DLAMV_name constr =
- let rec decomprec lna = function
- | DLAM(na,lc) -> decomprec (na::lna) lc
- | DLAMV(na,lc) -> (na::lna,lc)
- | _ -> assert false
- in
- decomprec [] constr
-
let mind_check_lc params mie =
let nparams = List.length params in
let check_lc (_,_,_,lc) =
@@ -156,6 +148,7 @@ let failwith_non_pos_vect n ntypes v =
anomaly "failwith_non_pos_vect: some k in [n;n+ntypes-1] should occur in v"
let check_correct_par env nparams ntypes n l largs =
+ let largs = Array.of_list largs in
if Array.length largs < nparams then
raise (IllFormedInd (LocalNotEnoughArgs l));
let (lpar,largs') = array_chop nparams largs in
@@ -182,40 +175,40 @@ let decomp_par n c = snd (mind_extract_params n c)
let listrec_mconstr env ntypes nparams i indlc =
(* check the inductive types occur positively in [c] *)
let rec check_pos n c =
- match whd_betadeltaiota env Evd.empty c with
- | DOP2(Prod,b,DLAM(na,d)) ->
- if not (noccur_between n ntypes b) then raise (IllFormedInd (LocalNonPos n));
+ let x,largs = whd_betadeltaiota_stack env Evd.empty c [] in
+ match kind_of_term x with
+ | IsProd (na,b,d) ->
+ assert (largs = []);
+ if not (noccur_between n ntypes b) then
+ raise (IllFormedInd (LocalNonPos n));
check_pos (n+1) d
- | x ->
- let hd,largs = destApplication (ensure_appl x) in
- match hd with
- | Rel k ->
- if k >= n && k<n+ntypes then begin
- check_correct_par env nparams ntypes n (k-n+1) largs;
- Mrec(n+ntypes-k-1)
- end else if noccur_between n ntypes x then
- if (n-nparams) <= k & k <= (n-1)
- then Param(n-1-k)
- else Norec
- else
- raise (IllFormedInd (LocalNonPos n))
- | DOPN(MutInd ind_sp,a) ->
- if (noccur_between n ntypes x) then Norec
- else Imbr(ind_sp,imbr_positive n (ind_sp,a) largs)
- | err ->
- if noccur_between n ntypes x then Norec
- else raise (IllFormedInd (LocalNonPos n))
+ | IsRel k ->
+ if k >= n && k<n+ntypes then begin
+ check_correct_par env nparams ntypes n (k-n+1) largs;
+ Mrec(n+ntypes-k-1)
+ end else if noccur_between n ntypes x then
+ if (n-nparams) <= k & k <= (n-1)
+ then Param(n-1-k)
+ else Norec
+ else
+ raise (IllFormedInd (LocalNonPos n))
+ | IsMutInd (ind_sp,a) ->
+ if (noccur_between n ntypes x) then Norec
+ else Imbr(ind_sp,imbr_positive n (ind_sp,a) largs)
+ | err ->
+ if noccur_between n ntypes x then Norec
+ else raise (IllFormedInd (LocalNonPos n))
and imbr_positive n mi largs =
let mispeci = lookup_mind_specif mi env in
let auxnpar = mis_nparams mispeci in
- let (lpar,auxlargs) = array_chop auxnpar largs in
- if not (array_for_all (noccur_between n ntypes) auxlargs) then
+ let (lpar,auxlargs) = list_chop auxnpar largs in
+ if not (List.for_all (noccur_between n ntypes) auxlargs) then
raise (IllFormedInd (LocalNonPos n));
let auxlc = mis_lc mispeci
and auxntyp = mis_ntypes mispeci in
if auxntyp <> 1 then raise (IllFormedInd (LocalNonPos n));
- let lrecargs = array_map_to_list (check_weak_pos n) lpar in
+ let lrecargs = List.map (check_weak_pos n) lpar in
(* The abstract imbricated inductive type with parameters substituted *)
let auxlcvect = abstract_mind_lc env auxntyp auxnpar auxlc in
let newidx = n + auxntyp in
@@ -224,8 +217,8 @@ let listrec_mconstr env ntypes nparams i indlc =
(* when substituted *)
Array.map
(function c ->
- let c' = hnf_prod_appvect env Evd.empty c
- (Array.map (lift auxntyp) lpar) in
+ let c' = hnf_prod_applist env Evd.empty c
+ (List.map (lift auxntyp) lpar) in
check_construct false newidx c')
auxlcvect
in
@@ -248,15 +241,16 @@ let listrec_mconstr env ntypes nparams i indlc =
(* Since Lambda can no longer occur after a product or a MutInd,
I have branched the remaining cases on check_pos. HH 28/1/00 *)
- and check_weak_pos n c =
- match whd_betadeltaiota env Evd.empty c with
+ and check_weak_pos n c =
+ let x = whd_betadeltaiota env Evd.empty c in
+ match kind_of_term x with
(* The extra case *)
- | DOP2(Lambda,b,DLAM(na,d)) ->
+ | IsLambda (na,b,d) ->
if noccur_between n ntypes b
then check_weak_pos (n+1) d
else raise (IllFormedInd (LocalNonPos n))
(******************)
- | x -> check_pos n x
+ | _ -> check_pos n x
(* check the inductive types occur positively in the products of C, if
check_head=true, also check the head corresponds to a constructor of
@@ -264,19 +258,20 @@ let listrec_mconstr env ntypes nparams i indlc =
and check_construct check_head =
let rec check_constr_rec lrec n c =
- match whd_betadeltaiota env Evd.empty c with
- | DOP2(Prod,b,DLAM(na,d)) ->
+ let x,largs = whd_betadeltaiota_stack env Evd.empty c [] in
+ match kind_of_term x with
+ | IsProd (na,b,d) ->
+ assert (largs = []);
let recarg = check_pos n b in
check_constr_rec (recarg::lrec) (n+1) d
- | x ->
- let hd,largs = destApplication (ensure_appl x) in
+ | hd ->
if check_head then
- match hd with
- | Rel k when k = n+ntypes-i ->
- check_correct_par env nparams ntypes n (k-n+1) largs
- | _ -> raise (IllFormedInd LocalNotConstructor)
+ if hd = IsRel (n+ntypes-i) then
+ check_correct_par env nparams ntypes n (ntypes-i+1) largs
+ else
+ raise (IllFormedInd LocalNotConstructor)
else
- if not (array_for_all (noccur_between n ntypes) largs)
+ if not (List.for_all (noccur_between n ntypes) largs)
then raise (IllFormedInd (LocalNonPos n));
List.rev lrec
in check_constr_rec []
diff --git a/kernel/inductive.ml b/kernel/inductive.ml
index 43b756651..db3329a1a 100644
--- a/kernel/inductive.ml
+++ b/kernel/inductive.ml
@@ -4,7 +4,7 @@
open Util
open Names
open Univ
-open Generic
+(*i open Generic i*)
open Term
open Sign
open Declarations
diff --git a/kernel/instantiate.ml b/kernel/instantiate.ml
index 9fb85961f..627f0d45c 100644
--- a/kernel/instantiate.ml
+++ b/kernel/instantiate.ml
@@ -4,7 +4,7 @@
open Pp
open Util
open Names
-open Generic
+(*i open Generic i*)
open Term
open Sign
open Evd
diff --git a/kernel/reduction.ml b/kernel/reduction.ml
index c4642b933..f0f7945d6 100644
--- a/kernel/reduction.ml
+++ b/kernel/reduction.ml
@@ -4,7 +4,7 @@
open Pp
open Util
open Names
-open Generic
+(*i open Generic i*)
open Term
open Univ
open Evd
@@ -26,6 +26,17 @@ type 'a stack_reduction_function = 'a contextual_stack_reduction_function
type local_stack_reduction_function =
constr -> constr list -> constr * constr list
+type stack =
+ | EmptyStack
+ | ConsStack of constr array * int * stack
+
+let decomp_stack = function
+ | EmptyStack -> None
+ | ConsStack (v, n, s) ->
+ Some (v.(n), (if n+1 = Array.length v then s else ConsStack (v, n+1, s)))
+
+let append_stack v s = if Array.length v = 0 then s else ConsStack (v,0,s)
+
(*************************************)
(*** Reduction Functions Operators ***)
(*************************************)
@@ -49,44 +60,66 @@ let stack_reduction_of_reduction red_fun env sigma x stack =
whd_stack t []
let strong whdfun env sigma =
- let rec strongrec t = match whdfun env sigma t with
+ let rec strongrec env t = match whdfun env sigma t with
| DOP0 _ as t -> t
+ | DOP1(oper,c) -> DOP1(oper,strongrec env c)
+ | DOP2(oper,c1,c2) -> DOP2(oper,strongrec env c1,strongrec env c2)
(* Cas ad hoc *)
- | DOP1(oper,c) -> DOP1(oper,strongrec c)
- (* Faut differencier sinon fait planter kind_of_term *)
- | DOP2(Prod|Lambda as oper,c1,DLAM(na,c2)) ->
- DOP2(oper,strongrec c1,DLAM(na,strongrec c2))
- | DOP2(oper,c1,c2) -> DOP2(oper,strongrec c1,strongrec c2)
- | DOPN(oper,cl) -> DOPN(oper,Array.map strongrec cl)
- | DOPL(oper,cl) -> DOPL(oper,List.map strongrec cl)
- | DLAM(na,c) -> DLAM(na,strongrec c)
- | DLAMV(na,c) -> DLAMV(na,Array.map strongrec c)
+ | DOPN(Fix _ as oper,cl) ->
+ let cl' = Array.copy cl in
+ let l = Array.length cl -1 in
+ for i=0 to l-1 do cl'.(i) <- strongrec env cl.(i) done;
+ cl'.(l) <- strongrec_lam env cl.(l);
+ DOPN(oper, cl')
+ | DOPN(oper,cl) -> DOPN(oper,Array.map (strongrec env) cl)
+ | CLam (n,t,c) ->
+ CLam (n, typed_app (strongrec env) t, strongrec (push_rel_decl (n,t) env) c)
+ | CPrd (n,t,c) ->
+ CPrd (n, typed_app (strongrec env) t, strongrec (push_rel_decl (n,t) env) c)
+ | CLet (n,b,t,c) ->
+ CLet (n, strongrec env b, typed_app (strongrec env) t,
+ strongrec (push_rel_def (n,b,t) env) c)
| VAR _ as t -> t
| Rel _ as t -> t
+ | DLAM _ | DLAMV _ -> assert false
+ and strongrec_lam env = function (* Gestion incorrecte de l'env des Fix *)
+ | DLAM(na,c) -> DLAM(na,strongrec_lam env c)
+ | DLAMV(na,c) -> DLAMV(na,Array.map (strongrec env) c)
+ | _ -> assert false
in
- strongrec
+ strongrec env
let local_strong whdfun =
let rec strongrec t = match whdfun t with
| DOP0 _ as t -> t
- (* Cas ad hoc *)
| DOP1(oper,c) -> DOP1(oper,strongrec c)
| DOP2(oper,c1,c2) -> DOP2(oper,strongrec c1,strongrec c2)
+ (* Cas ad hoc *)
+ | DOPN(Fix _ as oper,cl) ->
+ let cl' = Array.copy cl in
+ let l = Array.length cl -1 in
+ for i=0 to l-1 do cl'.(i) <- strongrec cl.(i) done;
+ cl'.(l) <- strongrec_lam cl.(l);
+ DOPN(oper, cl')
| DOPN(oper,cl) -> DOPN(oper,Array.map strongrec cl)
- | DOPL(oper,cl) -> DOPL(oper,List.map strongrec cl)
- | DLAM(na,c) -> DLAM(na,strongrec c)
- | DLAMV(na,c) -> DLAMV(na,Array.map strongrec c)
+ | CLam(n,t,c) -> CLam (n, typed_app strongrec t, strongrec c)
+ | CPrd(n,t,c) -> CPrd (n, typed_app strongrec t, strongrec c)
+ | CLet(n,b,t,c) -> CLet (n, strongrec b,typed_app strongrec t, strongrec c)
| VAR _ as t -> t
| Rel _ as t -> t
+ | DLAM _ | DLAMV _ -> assert false
+ and strongrec_lam = function
+ | DLAM(na,c) -> DLAM(na,strongrec_lam c)
+ | DLAMV(na,c) -> DLAMV(na,Array.map strongrec c)
+ | _ -> assert false
in
strongrec
-let rec strong_prodspine redfun env sigma c =
- match redfun env sigma c with
- | DOP2(Prod,a,DLAM(na,b)) ->
- DOP2(Prod,a,DLAM(na,strong_prodspine redfun env sigma b))
- | x -> x
-
+let rec strong_prodspine redfun c =
+ let x = redfun c in
+ match kind_of_term x with
+ | IsProd (na,a,b) -> mkProd (na,a,strong_prodspine redfun b)
+ | _ -> x
(****************************************************************************)
(* Reduction Functions *)
@@ -122,17 +155,14 @@ let whd_flags flgs env sigma t =
(* Red reduction tactic: reduction to a product *)
let red_product env sigma c =
let rec redrec x =
- match x with
- | DOPN(AppL,cl) ->
- DOPN(AppL,Array.append [|redrec (array_hd cl)|] (array_tl cl))
- | DOPN(Const _,_) when evaluable_constant env x ->
- constant_value env x
- | DOPN(Evar ev,args) when Evd.is_defined sigma ev ->
+ match kind_of_term x with
+ | IsAppL (f,l) -> applist (redrec f, l)
+ | IsConst (_,_) when evaluable_constant env x -> constant_value env x
+ | IsEvar (ev,args) when Evd.is_defined sigma ev ->
existential_value sigma (ev,args)
- | DOPN(Abst _,_) when evaluable_abst env x ->
- abst_value env x
- | DOP2(Cast,c,_) -> redrec c
- | DOP2(Prod,a,DLAM(x,b)) -> DOP2(Prod, a, DLAM(x, redrec b))
+ | IsAbst (_,_) when evaluable_abst env x -> abst_value env x
+ | IsCast (c,_) -> redrec c
+ | IsProd (x,a,b) -> mkProd (x, a, redrec b)
| _ -> error "Term not reducible"
in
nf_betaiota env sigma (redrec c)
@@ -141,33 +171,26 @@ let red_product env sigma c =
* n is the number of the next occurence of name.
* ol is the occurence list to find. *)
let rec substlin env name n ol c =
- match c with
- | DOPN(Const sp,_) ->
- if sp = name then
- if List.hd ol = n then
- if evaluable_constant env c then
- (n+1, List.tl ol, constant_value env c)
- else
- errorlabstrm "substlin"
- [< print_sp sp; 'sTR " is not a defined constant" >]
- else
- ((n+1),ol,c)
+ match kind_of_term c with
+ | IsConst (sp,_) when sp = name ->
+ if List.hd ol = n then
+ if evaluable_constant env c then
+ (n+1, List.tl ol, constant_value env c)
+ else
+ errorlabstrm "substlin"
+ [< print_sp sp; 'sTR " is not a defined constant" >]
else
- (n,ol,c)
+ ((n+1),ol,c)
- | DOPN(Abst _,_) ->
- if path_of_abst c = name then
- if List.hd ol = n then
- (n+1, List.tl ol, abst_value env c)
- else
- (n+1,ol,c)
+ | IsAbst (_,_) when path_of_abst c = name ->
+ if List.hd ol = n then
+ (n+1, List.tl ol, abst_value env c)
else
- (n,ol,c)
+ (n+1,ol,c)
(* INEFFICIENT: OPTIMIZE *)
- | DOPN(AppL,tl) ->
- let c1 = array_hd tl and cl = array_tl tl in
- Array.fold_left
+ | IsAppL (c1,cl) ->
+ List.fold_left
(fun (n1,ol1,c1') c2 ->
(match ol1 with
| [] -> (n1,[],applist(c1',[c2]))
@@ -176,24 +199,31 @@ let rec substlin env name n ol c =
(n2,ol2,applist(c1',[c2']))))
(substlin env name n ol c1) cl
- | DOP2(Lambda,c1,DLAM(na,c2)) ->
+ | IsLambda (na,c1,c2) ->
let (n1,ol1,c1') = substlin env name n ol c1 in
(match ol1 with
- | [] -> (n1,[],DOP2(Lambda,c1',DLAM(na,c2)))
+ | [] -> (n1,[],mkLambda (na,c1',c2))
| _ ->
let (n2,ol2,c2') = substlin env name n1 ol1 c2 in
- (n2,ol2,DOP2(Lambda,c1',DLAM(na,c2'))))
+ (n2,ol2,mkLambda (na,c1',c2')))
- | DOP2(Prod,c1,DLAM(na,c2)) ->
+ | IsLetIn (na,c1,t,c2) ->
let (n1,ol1,c1') = substlin env name n ol c1 in
(match ol1 with
- | [] -> (n1,[],DOP2(Prod,c1',DLAM(na,c2)))
+ | [] -> (n1,[],mkLambda (na,c1',c2))
| _ ->
let (n2,ol2,c2') = substlin env name n1 ol1 c2 in
- (n2,ol2,DOP2(Prod,c1',DLAM(na,c2'))))
+ (n2,ol2,mkLambda (na,c1',c2')))
+
+ | IsProd (na,c1,c2) ->
+ let (n1,ol1,c1') = substlin env name n ol c1 in
+ (match ol1 with
+ | [] -> (n1,[],mkProd (na,c1',c2))
+ | _ ->
+ let (n2,ol2,c2') = substlin env name n1 ol1 c2 in
+ (n2,ol2,mkProd (na,c1',c2')))
- | DOPN(MutCase _,_) ->
- let (ci,p,d,llf) = destCase c in
+ | IsMutCase (ci,p,d,llf) ->
let rec substlist nn oll = function
| [] -> (nn,oll,[])
| f::lfe ->
@@ -213,23 +243,26 @@ let rec substlin env name n ol c =
| [] -> (n2,[],mkMutCaseA ci p' d' llf)
| _ ->
let (n3,ol3,lf') = substlist n2 ol2 (Array.to_list llf)
- in (n3,ol3,mkMutCase ci p' d' lf')))
+ in (n3,ol3,mkMutCase (ci, p', d', lf'))))
- | DOP2(Cast,c1,c2) ->
+ | IsCast (c1,c2) ->
let (n1,ol1,c1') = substlin env name n ol c1 in
(match ol1 with
- | [] -> (n1,[],DOP2(Cast,c1',c2))
+ | [] -> (n1,[],mkCast (c1',c2))
| _ ->
let (n2,ol2,c2') = substlin env name n1 ol1 c2 in
- (n2,ol2,DOP2(Cast,c1',c2')))
+ (n2,ol2,mkCast (c1',c2')))
- | DOPN(Fix _,_) ->
+ | IsFix _ ->
(warning "do not consider occurrences inside fixpoints"; (n,ol,c))
- | DOPN(CoFix _,_) ->
+ | IsCoFix _ ->
(warning "do not consider occurrences inside cofixpoints"; (n,ol,c))
+
+ | (IsRel _|IsMeta _|IsVar _|IsXtra _|IsSort _
+ |IsAbst (_, _)|IsEvar _|IsConst _
+ |IsMutInd _|IsMutConstruct _) -> (n,ol,c)
- | _ -> (n,ol,c)
let unfold env sigma name =
let flag =
@@ -275,9 +308,9 @@ let abstract_scheme env (locc,a,ta) t =
let na = named_hd env ta Anonymous in
if occur_meta ta then error "cannot find a type for the generalisation";
if occur_meta a then
- DOP2(Lambda,ta,DLAM(na,t))
+ mkLambda (na,ta,t)
else
- DOP2(Lambda, ta, DLAM(na,subst_term_occ locc a t))
+ mkLambda (na, ta,subst_term_occ locc a t)
let pattern_occs loccs_trm_typ env sigma c =
@@ -293,26 +326,25 @@ let pattern_occs loccs_trm_typ env sigma c =
let rec stacklam recfun env t stack =
match (stack,t) with
- | (h::stacktl, DOP2(Lambda,_,DLAM(_,c))) ->
- stacklam recfun (h::env) c stacktl
- | _ -> recfun (substl env t) stack
+ | h::stacktl, CLam (_,_,c) -> stacklam recfun (h::env) c stacktl
+ | _ -> recfun (substl env t, stack)
-let beta_applist (c,l) = stacklam (fun c l -> applist(c,l)) [] c l
+let beta_applist (c,l) = stacklam applist [] c l
-let whd_beta_stack =
- let rec whrec x stack = match x with
- | DOP2(Lambda,c1,DLAM(name,c2)) ->
+let whd_beta_stack x stack =
+ let rec whrec (x, stack as s) = match x with
+ | CLam (name,c1,c2) ->
(match stack with
| [] -> (x,[])
| a1::rest -> stacklam whrec [a1] c2 rest)
- | DOPN(AppL,cl) -> whrec (array_hd cl) (array_app_tl cl stack)
- | DOP2(Cast,c,_) -> whrec c stack
- | x -> (x,stack)
+ | DOPN(AppL,cl) -> whrec (array_hd cl, array_app_tl cl stack)
+ | DOP2(Cast,c,_) -> whrec (c, stack)
+ | x -> s
in
- whrec
+ whrec (x, stack)
let whd_beta x = applist (whd_beta_stack x [])
@@ -375,103 +407,105 @@ let whd_delta_stack env sigma =
let whd_delta env sigma c = applist(whd_delta_stack env sigma c [])
-let whd_betadelta_stack env sigma =
- let rec whrec x l =
- match x with
- | DOPN(Const _,_) ->
+let whd_betadelta_stack env sigma x l =
+ let rec whrec (x, l as s) =
+ match kind_of_term x with
+ | IsConst _ ->
if evaluable_constant env x then
- whrec (constant_value env x) l
+ whrec (constant_value env x, l)
else
- (x,l)
- | DOPN(Evar ev,args) ->
+ s
+ | IsEvar (ev,args) ->
if Evd.is_defined sigma ev then
- whrec (existential_value sigma (ev,args)) l
+ whrec (existential_value sigma (ev,args), l)
else
- (x,l)
+ s
+(*
| DOPN(Abst _,_) ->
if evaluable_abst env x then
whrec (abst_value env x) l
else
(x,l)
- | DOP2(Cast,c,_) -> whrec c l
- | DOPN(AppL,cl) -> whrec (array_hd cl) (array_app_tl cl l)
- | DOP2(Lambda,_,DLAM(_,c)) ->
+*)
+ | IsCast (c,_) -> whrec (c, l)
+ | IsAppL (f,cl) -> whrec (f, cl@l)
+ | IsLambda (_,_,c) ->
(match l with
- | [] -> (x,l)
+ | [] -> s
| (a::m) -> stacklam whrec [a] c m)
- | x -> (x,l)
+ | x -> s
in
- whrec
+ whrec (x, l)
let whd_betadelta env sigma c = applist(whd_betadelta_stack env sigma c [])
-let whd_betaevar_stack env sigma =
- let rec whrec x l =
- match x with
- | DOPN(Evar ev,args) ->
+let whd_betaevar_stack env sigma x l =
+ let rec whrec (x, l as s) =
+ match kind_of_term x with
+ | IsEvar (ev,args) ->
if Evd.is_defined sigma ev then
- whrec (existential_value sigma (ev,args)) l
+ whrec (existential_value sigma (ev,args), l)
else
- (x,l)
+ s
+(*
| DOPN(Abst _,_) ->
if translucent_abst env x then
whrec (abst_value env x) l
else
(x,l)
- | DOP2(Cast,c,_) -> whrec c l
- | DOPN(AppL,cl) -> whrec (array_hd cl) (array_app_tl cl l)
- | DOP2(Lambda,_,DLAM(_,c)) ->
+*)
+ | IsCast (c,_) -> whrec (c, l)
+ | IsAppL (f,cl) -> whrec (f, cl@l)
+ | IsLambda (_,_,c) ->
(match l with
| [] -> (x,l)
| (a::m) -> stacklam whrec [a] c m)
- | DOPN(Const _,_) -> (x,l)
- | x -> (x,l)
+ | x -> s
in
- whrec
+ whrec (x, l)
let whd_betaevar env sigma c = applist(whd_betaevar_stack env sigma c [])
-let whd_betadeltaeta_stack env sigma =
- let rec whrec x stack =
- match x with
- | DOPN(Const _,_) ->
- if evaluable_constant env x then
- whrec (constant_value env x) stack
+let whd_betadeltaeta_stack env sigma x l =
+ let rec whrec (x, l as s) =
+ match kind_of_term x with
+ | IsConst _ ->
+ if evaluable_constant env x then
+ whrec (constant_value env x, l)
else
- (x,stack)
- | DOPN(Evar ev,args) ->
+ s
+ | IsEvar (ev,args) ->
if Evd.is_defined sigma ev then
- whrec (existential_value sigma (ev,args)) stack
+ whrec (existential_value sigma (ev,args), l)
else
- (x,stack)
+ s
+(*
| DOPN(Abst _,_) ->
- if evaluable_abst env x then
- whrec (abst_value env x) stack
+ if evaluable_abst env x then
+ whrec (abst_value env x) l
else
- (x,stack)
- | DOP2(Cast,c,_) -> whrec c stack
- | DOPN(AppL,cl) -> whrec (array_hd cl) (array_app_tl cl stack)
- | DOP2(Lambda,_,DLAM(_,c)) ->
- (match stack with
- | [] ->
- (match applist (whrec c []) with
- | DOPN(AppL,cl) ->
- (match whrec (array_last cl) [] with
- | (Rel 1,[]) ->
- let napp = (Array.length cl) -1 in
- if napp = 0 then (x,stack) else
- let lc = Array.sub cl 0 napp in
- let u =
- if napp = 1 then lc.(0) else DOPN(AppL,lc)
- in
- if noccurn 1 u then (pop u,[]) else (x,stack)
- | _ -> (x,stack))
- | _ -> (x,stack))
+ (x,l)
+*)
+ | IsCast (c,_) -> whrec (c, l)
+ | IsAppL (f,cl) -> whrec (f, cl@l)
+ | IsLambda (_,_,c) ->
+ (match l with
+ | [] ->
+ (match applist (whrec (c, [])) with
+ | DOPN(AppL,cl) ->
+ let napp = (Array.length cl) -1 in
+ (match whrec (array_last cl, []) with
+ | (Rel 1,[]) when napp > 0 ->
+ let lc = Array.sub cl 0 napp in
+ let u = if napp=1 then lc.(0) else DOPN(AppL,lc)
+ in if noccurn 1 u then (pop u,[]) else s
+ | _ -> s)
+ | _ -> s)
| (a::m) -> stacklam whrec [a] c m)
- | x -> (x,stack)
+ | x -> s
in
- whrec
+ whrec (x, l)
let whd_betadeltaeta env sigma x =
applist(whd_betadeltaeta_stack env sigma x [])
@@ -540,185 +574,185 @@ let fix_recarg ((recindices,bodynum),_) stack =
else
None
+type fix_reduction_result = NotReducible | Reduced of (constr * constr list)
+
let reduce_fix whfun fix stack =
- let dfix = destFix fix in
- match fix_recarg dfix stack with
- | None -> (false,(fix,stack))
+ match fix_recarg fix stack with
+ | None -> NotReducible
| Some (recargnum,recarg) ->
- let (recarg'hd,_ as recarg') = whfun recarg [] in
+ let (recarg'hd,_ as recarg') = whfun (recarg, []) in
let stack' = list_assign stack recargnum (applist recarg') in
(match recarg'hd with
- | DOPN(MutConstruct _,_) ->
- (true,(contract_fix dfix,stack'))
- | _ -> (false,(fix,stack')))
+ | DOPN(MutConstruct _,_) -> Reduced (contract_fix fix, stack')
+ | _ -> NotReducible)
(* NB : Cette fonction alloue peu c'est l'appel
``let (recarg'hd,_ as recarg') = whfun recarg [] in''
--------------------
qui coute cher dans whd_betadeltaiota *)
-let whd_betaiota_stack =
- let rec whrec x stack =
- match x with
- | DOP2(Cast,c,_) -> whrec c stack
- | DOPN(AppL,cl) -> whrec (array_hd cl) (array_app_tl cl stack)
- | DOP2(Lambda,_,DLAM(_,c)) ->
+let whd_betaiota_stack x l =
+ let rec whrec (x,stack as s) =
+ match kind_of_term x with
+ | IsCast (c,_) -> whrec (c, stack)
+ | IsAppL (f,cl) -> whrec (f, cl@stack)
+ | IsLambda (_,_,c) ->
(match stack with
- | [] -> (x,stack)
- | (a::m) -> stacklam whrec [a] c m)
- | DOPN(MutCase _,_) ->
- let (ci,p,d,lf) = destCase x in
- let (c,cargs) = whrec d [] in
+ | [] -> s
+ | a::m -> stacklam whrec [a] c m)
+ | IsMutCase (ci,p,d,lf) ->
+ let (c,cargs) = whrec (d, []) in
if reducible_mind_case c then
whrec (reduce_mind_case
- {mP=p; mconstr=c; mcargs=cargs; mci=ci; mlf=lf}) stack
+ {mP=p; mconstr=c; mcargs=cargs; mci=ci; mlf=lf}, stack)
else
(mkMutCaseA ci p (applist(c,cargs)) lf, stack)
- | DOPN(Fix _,_) ->
- let (reduced,(fix,stack)) = reduce_fix whrec x stack in
- if reduced then whrec fix stack else (fix,stack)
- | x -> (x,stack)
+ | IsFix fix ->
+ (match reduce_fix whrec fix stack with
+ | Reduced s' -> whrec s'
+ | NotReducible -> s)
+ | _ -> s
in
- whrec
+ whrec (x, l)
let whd_betaiota x = applist (whd_betaiota_stack x [])
-let whd_betaiotaevar_stack env sigma =
- let rec whrec x stack =
- match x with
- | DOPN(Evar ev,args) ->
+let whd_betaiotaevar_stack env sigma x l =
+ let rec whrec (x, stack as s) =
+ match kind_of_term x with
+ | IsEvar (ev,args) ->
if Evd.is_defined sigma ev then
- whrec (existential_value sigma (ev,args)) stack
+ whrec (existential_value sigma (ev,args), stack)
else
- (x,stack)
+ s
+(*
| DOPN(Abst _,_) ->
if translucent_abst env x then
whrec (abst_value env x) stack
else
(x,stack)
- | DOP2(Cast,c,_) -> whrec c stack
- | DOPN(AppL,cl) -> whrec (array_hd cl) (array_app_tl cl stack)
- | DOP2(Lambda,_,DLAM(_,c)) ->
+*)
+ | IsCast (c,_) -> whrec (c, stack)
+ | IsAppL (f,cl) -> whrec (f, cl@stack)
+ | IsLambda (_,_,c) ->
(match stack with
- | [] -> (x,stack)
+ | [] -> s
| (a::m) -> stacklam whrec [a] c m)
- | DOPN(MutCase _,_) ->
- let (ci,p,d,lf) = destCase x in
- let (c,cargs) = whrec d [] in
+ | IsMutCase (ci,p,d,lf) ->
+ let (c,cargs) = whrec (d, []) in
if reducible_mind_case c then
whrec (reduce_mind_case
- {mP=p; mconstr=c; mcargs=cargs; mci=ci; mlf=lf}) stack
+ {mP=p; mconstr=c; mcargs=cargs; mci=ci; mlf=lf}, stack)
else
- (mkMutCaseA ci p (applist(c,cargs)) lf,stack)
- | DOPN(Fix _,_) ->
- let (reduced,(fix,stack)) = reduce_fix whrec x stack in
- if reduced then whrec fix stack else (fix,stack)
- | DOPN(Const _,_) -> (x,stack)
- | x -> (x,stack)
+ (mkMutCaseA ci p (applist(c,cargs)) lf, stack)
+ | IsFix fix ->
+ (match reduce_fix whrec fix stack with
+ | Reduced s' -> whrec s'
+ | NotReducible -> s)
+ | _ -> s
in
- whrec
+ whrec (x, l)
let whd_betaiotaevar env sigma x =
applist(whd_betaiotaevar_stack env sigma x [])
-let whd_betadeltaiota_stack env sigma =
- let rec bdi_rec x stack =
- match x with
- | DOPN(Const _,_) ->
+let whd_betadeltaiota_stack env sigma x l =
+ let rec whrec (x, stack as s) =
+ match kind_of_term x with
+ | IsConst _ ->
if evaluable_constant env x then
- bdi_rec (constant_value env x) stack
+ whrec (constant_value env x, stack)
else
- (x,stack)
- | DOPN(Evar ev,args) ->
+ s
+ | IsEvar (ev,args) ->
if Evd.is_defined sigma ev then
- bdi_rec (existential_value sigma (ev,args)) stack
+ whrec (existential_value sigma (ev,args), stack)
else
- (x,stack)
+ s
+(*
| DOPN(Abst _,_) ->
if evaluable_abst env x then
- bdi_rec (abst_value env x) stack
+ whrec (abst_value env x) stack
else
(x,stack)
- | DOP2(Cast,c,_) -> bdi_rec c stack
- | DOPN(AppL,cl) -> bdi_rec (array_hd cl) (array_app_tl cl stack)
- | DOP2(Lambda,_,DLAM(_,c)) ->
+*)
+ | IsCast (c,_) -> whrec (c, stack)
+ | IsAppL (f,cl) -> whrec (f, cl@stack)
+ | IsLambda (_,_,c) ->
(match stack with
- | [] -> (x,[])
- | (a::m) -> stacklam bdi_rec [a] c m)
- | DOPN(MutCase _,_) ->
- let (ci,p,d,lf) = destCase x in
- let (c,cargs) = bdi_rec d [] in
+ | [] -> s
+ | (a::m) -> stacklam whrec [a] c m)
+ | IsMutCase (ci,p,d,lf) ->
+ let (c,cargs) = whrec (d, []) in
if reducible_mind_case c then
- bdi_rec (reduce_mind_case
- {mP=p; mconstr=c; mcargs=cargs; mci=ci; mlf=lf}) stack
+ whrec (reduce_mind_case
+ {mP=p; mconstr=c; mcargs=cargs; mci=ci; mlf=lf}, stack)
else
- (mkMutCaseA ci p (applist(c,cargs)) lf,stack)
- | DOPN(Fix _,_) ->
- let (reduced,(fix,stack)) = reduce_fix bdi_rec x stack in
- if reduced then bdi_rec fix stack else (fix,stack)
- | x -> (x,stack)
+ (mkMutCaseA ci p (applist(c,cargs)) lf, stack)
+ | IsFix fix ->
+ (match reduce_fix whrec fix stack with
+ | Reduced s' -> whrec s'
+ | NotReducible -> s)
+ | _ -> s
in
- bdi_rec
+ whrec (x, l)
let whd_betadeltaiota env sigma x =
applist(whd_betadeltaiota_stack env sigma x [])
-let whd_betadeltaiotaeta_stack env sigma =
- let rec whrec x stack =
- match x with
- | DOPN(Const _,_) ->
- if evaluable_constant env x then
- whrec (constant_value env x) stack
+let whd_betadeltaiotaeta_stack env sigma x l =
+ let rec whrec (x, stack as s) =
+ match kind_of_term x with
+ | IsConst _ ->
+ if evaluable_constant env x then
+ whrec (constant_value env x, stack)
else
- (x,stack)
- | DOPN(Evar ev,args) ->
+ s
+ | IsEvar (ev,args) ->
if Evd.is_defined sigma ev then
- whrec (existential_value sigma (ev,args)) stack
+ whrec (existential_value sigma (ev,args), stack)
else
- (x,stack)
+ s
+(*
| DOPN(Abst _,_) ->
- if evaluable_abst env x then
- whrec (abst_value env x) stack
- else
+ if evaluable_abst env x then
+ whrec (abst_value env x) stack
+ else
(x,stack)
- | DOP2(Cast,c,_) -> whrec c stack
- | DOPN(AppL,cl) -> whrec (array_hd cl) (array_app_tl cl stack)
- | DOP2(Lambda,_,DLAM(_,c)) ->
+*)
+ | IsCast (c,_) -> whrec (c, stack)
+ | IsAppL (f,cl) -> whrec (f, cl@stack)
+ | IsLambda (_,_,c) ->
(match stack with
| [] ->
- (match applist (whrec c []) with
- | DOPN(AppL,cl) ->
- (match whrec (array_last cl) [] with
- | (Rel 1,[]) ->
- let napp = (Array.length cl) -1 in
- if napp = 0 then
- (x,stack)
- else
- let lc = Array.sub cl 0 napp in
- let u =
- if napp = 1 then lc.(0) else DOPN(AppL,lc)
- in
- if noccurn 1 u then (pop u,[]) else (x,stack)
- | _ -> (x,stack))
- | _ -> (x,stack))
+ (match applist (whrec (c, [])) with
+ | DOPN(AppL,cl) ->
+ let napp = (Array.length cl) -1 in
+ (match whrec (array_last cl, []) with
+ | (Rel 1,[]) when napp > 0 ->
+ let lc = Array.sub cl 0 napp in
+ let u = if napp=1 then lc.(0) else DOPN(AppL,lc)
+ in if noccurn 1 u then (pop u,[]) else s
+ | _ -> s)
+ | _ -> s)
| (a::m) -> stacklam whrec [a] c m)
- | DOPN(MutCase _,_) ->
- let (ci,p,d,lf) = destCase x in
- let (c,cargs) = whrec d [] in
+ | IsMutCase (ci,p,d,lf) ->
+ let (c,cargs) = whrec (d, []) in
if reducible_mind_case c then
whrec (reduce_mind_case
- {mP=p; mconstr=c; mcargs=cargs; mci=ci; mlf=lf}) stack
+ {mP=p; mconstr=c; mcargs=cargs; mci=ci; mlf=lf}, stack)
else
- (mkMutCaseA ci p (applist(c,cargs)) lf,stack)
- | DOPN(Fix _,_) ->
- let (reduced,(fix,stack)) = reduce_fix whrec x stack in
- if reduced then whrec fix stack else (fix,stack)
- | x -> (x,stack)
+ (mkMutCaseA ci p (applist(c,cargs)) lf, stack)
+ | IsFix fix ->
+ (match reduce_fix whrec fix stack with
+ | Reduced s' -> whrec s'
+ | NotReducible -> s)
+ | _ -> s
in
- whrec
+ whrec (x, l)
let whd_betadeltaiotaeta env sigma x =
applist(whd_betadeltaiotaeta_stack env sigma x [])
@@ -879,19 +913,21 @@ and eqappr cv_pb infos appr1 appr2 =
| None -> fun _ -> raise NotConvertible)
(* other constructors *)
- | (FOP2(Lambda,c1,c2), FOP2(Lambda,c'1,c'2)) ->
+ | (FLam (_,c1,c2,_,_), FLam (_,c'1,c'2,_,_)) ->
bool_and_convert
(Array.length v1 = 0 && Array.length v2 = 0)
(convert_and
(ccnv (pb_equal cv_pb) infos el1 el2 c1 c'1)
- (ccnv (pb_equal cv_pb) infos el1 el2 c2 c'2))
+ (ccnv (pb_equal cv_pb) infos (el_lift el1) (el_lift el2) c2 c'2))
+
+ | (FLet _, _) | (_, FLet _) -> anomaly "Normally removed by fhnf"
- | (FOP2(Prod,c1,c2), FOP2(Prod,c'1,c'2)) ->
+ | (FPrd (_,c1,c2,_,_), FPrd (_,c'1,c'2,_,_)) ->
bool_and_convert
(Array.length v1 = 0 && Array.length v2 = 0)
(convert_and
(ccnv (pb_equal cv_pb) infos el1 el2 c1 c'1) (* Luo's system *)
- (ccnv cv_pb infos el1 el2 c2 c'2))
+ (ccnv cv_pb infos (el_lift el1) (el_lift el2) c2 c'2))
(* Inductive types: MutInd MutConstruct MutCase Fix Cofix *)
@@ -926,8 +962,8 @@ and eqappr cv_pb infos appr1 appr2 =
let fconv cv_pb env sigma t1 t2 =
- let t1 = strong (fun _ _ -> strip_outer_cast) env sigma t1
- and t2 = strong (fun _ _ -> strip_outer_cast) env sigma t2 in
+ let t1 = local_strong strip_outer_cast t1
+ and t2 = local_strong strip_outer_cast t2 in
if eq_constr t1 t2 then
Constraint.empty
else
@@ -972,9 +1008,11 @@ let plain_instance s c =
| DOP1(oper,c) -> DOP1(oper, irec c)
| DOP2(oper,c1,c2) -> DOP2(oper, irec c1, irec c2)
| DOPN(oper,cl) -> DOPN(oper, Array.map irec cl)
- | DOPL(oper,cl) -> DOPL(oper, List.map irec cl)
| DLAM(x,c) -> DLAM(x, irec c)
| DLAMV(x,v) -> DLAMV(x, Array.map irec v)
+ | CLam (n,t,c) -> CLam (n, typed_app irec t, irec c)
+ | CPrd (n,t,c) -> CPrd (n, typed_app irec t, irec c)
+ | CLet (n,b,t,c) -> CLet (n, irec b, typed_app irec t, irec c)
| u -> u
in
if s = [] then c else irec c
@@ -992,7 +1030,7 @@ let instance s c =
let hnf_prod_app env sigma t n =
match whd_betadeltaiota env sigma t with
- | DOP2(Prod,_,DLAM(_,b)) -> subst1 n b
+ | CPrd (_,_,b) -> subst1 n b
| _ -> anomaly "hnf_prod_app: Need a product"
let hnf_prod_appvect env sigma t nl =
@@ -1003,7 +1041,7 @@ let hnf_prod_applist env sigma t nl =
let hnf_lam_app env sigma t n =
match whd_betadeltaiota env sigma t with
- | DOP2(Lambda,_,DLAM(_,b)) -> subst1 n b
+ | CLam (_,_,b) -> subst1 n b
| _ -> anomaly "hnf_lam_app: Need an abstraction"
let hnf_lam_appvect env sigma t nl =
@@ -1015,7 +1053,7 @@ let hnf_lam_applist env sigma t nl =
let splay_prod env sigma =
let rec decrec m c =
match whd_betadeltaiota env sigma c with
- | DOP2(Prod,a,DLAM(n,c_0)) -> decrec ((n,a)::m) c_0
+ | CPrd (n,a,c0) -> decrec ((n,body_of_type a)::m) c0
| t -> m,t
in
decrec []
@@ -1030,8 +1068,8 @@ let sort_of_arity env c = snd (splay_arity env Evd.empty c)
let decomp_n_prod env sigma n =
let rec decrec m ln c = if m = 0 then (ln,c) else
match whd_betadeltaiota env sigma c with
- | DOP2(Prod,a,DLAM(n,c0)) ->
- decrec (m-1) (Sign.add_rel_decl (n,outcast_type a) ln) c0
+ | CPrd (n,a,c0) ->
+ decrec (m-1) (Sign.add_rel_decl (n,a) ln) c0
| _ -> error "decomp_n_prod: Not enough products"
in
decrec n Sign.empty_rel_context
@@ -1053,7 +1091,7 @@ with bj=aj if j<>ik and bj=(Rel c) and Bic=Aic[xn..xic-1 <- an..aic-1]
let compute_consteval env sigma c =
let rec srec n labs c =
match whd_betadeltaeta_stack env sigma c [] with
- | (DOP2(Lambda,t,DLAM(_,g)),[]) -> srec (n+1) (t::labs) g
+ | CLam (_,t,g), [] -> srec (n+1) (t::labs) g
| (DOPN(Fix((nv,i)),bodies),l) ->
if List.length l > n then
raise Elimconst
@@ -1083,22 +1121,23 @@ let compute_consteval env sigma c =
(* One step of approximation *)
let rec apprec env sigma c stack =
- let (t,stack) = whd_betaiota_stack c stack in
- match t with
- | DOPN(MutCase _,_) ->
- let (ci,p,d,lf) = destCase t in
+ let (t, stack as s) = whd_betaiota_stack c stack in
+ match kind_of_term t with
+ | IsMutCase (ci,p,d,lf) ->
let (cr,crargs) = whd_betadeltaiota_stack env sigma d [] in
let rslt = mkMutCaseA ci p (applist(cr,crargs)) lf in
if reducible_mind_case cr then
apprec env sigma rslt stack
else
- (t,stack)
- | DOPN(Fix _,_) ->
- let (reduced,(fix,stack)) =
- reduce_fix (whd_betadeltaiota_stack env sigma) t stack
- in
- if reduced then apprec env sigma fix stack else (fix,stack)
- | _ -> (t,stack)
+ s
+ | IsFix fix ->
+ (match reduce_fix
+ (fun (c,l) -> whd_betadeltaiota_stack env sigma c l)
+ fix stack
+ with
+ | Reduced (c,stack) -> apprec env sigma c stack
+ | NotReducible -> s)
+ | _ -> s
let hnf env sigma c = apprec env sigma c []
@@ -1108,36 +1147,31 @@ let hnf env sigma c = apprec env sigma c []
* Used in Programs.
* Added by JCF, 29/1/98. *)
-let whd_programs_stack env sigma =
- let rec whrec x stack =
- match x with
- | DOPN(AppL,cl) ->
- if occur_meta cl.(1) then
- (x,stack)
- else
- whrec (array_hd cl) (array_app_tl cl stack)
- | DOP2(Lambda,_,DLAM(_,c)) ->
+let whd_programs_stack env sigma x l =
+ let rec whrec (x, stack as s) =
+ match kind_of_term x with
+ | IsAppL (f,[c]) -> if occur_meta c then s else whrec (f, c::stack)
+ | IsLambda (_,_,c) ->
(match stack with
- | [] -> (x,stack)
+ | [] -> s
| (a::m) -> stacklam whrec [a] c m)
- | DOPN(MutCase _,_) ->
- let (ci,p,d,lf) = destCase x in
+ | IsMutCase (ci,p,d,lf) ->
if occur_meta d then
- (x,stack)
+ s
else
- let (c,cargs) = whrec d [] in
+ let (c,cargs) = whrec (d, []) in
if reducible_mind_case c then
whrec (reduce_mind_case
- {mP=p; mconstr=c; mcargs=cargs; mci=ci; mlf=lf})
- stack
+ {mP=p; mconstr=c; mcargs=cargs; mci=ci; mlf=lf}, stack)
else
(mkMutCaseA ci p (applist(c,cargs)) lf, stack)
- | DOPN(Fix _,_) ->
- let (reduced,(fix,stack)) = reduce_fix whrec x stack in
- if reduced then whrec fix stack else (fix,stack)
- | x -> (x,stack)
+ | IsFix fix ->
+ (match reduce_fix whrec fix stack with
+ | Reduced s' -> whrec s'
+ | NotReducible -> s)
+ | _ -> s
in
- whrec
+ whrec (x, l)
let whd_programs env sigma x = applist (whd_programs_stack env sigma x [])
@@ -1145,37 +1179,34 @@ exception IsType
let is_arity env sigma =
let rec srec c =
- match whd_betadeltaiota env sigma c with
- | DOP0(Sort _) -> true
- | DOP2(Prod,_,DLAM(_,c')) -> srec c'
- | DOP2(Lambda,_,DLAM(_,c')) -> srec c'
+ match kind_of_term (whd_betadeltaiota env sigma c) with
+ | IsSort _ -> true
+ | IsProd (_,_,c') -> srec c'
+ | IsLambda (_,_,c') -> srec c'
| _ -> false
in
srec
let info_arity env sigma =
let rec srec c =
- match whd_betadeltaiota env sigma c with
- | DOP0(Sort(Prop Null)) -> false
- | DOP0(Sort(Prop Pos)) -> true
- | DOP2(Prod,_,DLAM(_,c')) -> srec c'
- | DOP2(Lambda,_,DLAM(_,c')) -> srec c'
+ match kind_of_term (whd_betadeltaiota env sigma c) with
+ | IsSort (Prop Null) -> false
+ | IsSort (Prop Pos) -> true
+ | IsProd (_,_,c') -> srec c'
+ | IsLambda (_,_,c') -> srec c'
| _ -> raise IsType
in
srec
-let is_logic_arity env sigma c =
- try (not (info_arity env sigma c)) with IsType -> false
-
-let is_info_arity env sigma c =
+let is_info_arity env sigma c =
try (info_arity env sigma c) with IsType -> true
-
+
let is_type_arity env sigma =
let rec srec c =
- match whd_betadeltaiota env sigma c with
- | DOP0(Sort(Type _)) -> true
- | DOP2(Prod,_,DLAM(_,c')) -> srec c'
- | DOP2(Lambda,_,DLAM(_,c')) -> srec c'
+ match kind_of_term (whd_betadeltaiota env sigma c) with
+ | IsSort (Type _) -> true
+ | IsProd (_,_,c') -> srec c'
+ | IsLambda (_,_,c') -> srec c'
| _ -> false
in
srec
@@ -1186,20 +1217,6 @@ let is_info_type env sigma t =
(s <> Prop Null &&
try info_arity env sigma t.utj_val with IsType -> true)
-(* Pour l'extraction
-let is_info_cast_type env sigma c =
- match c with
- | DOP2(Cast,c,t) ->
- (try info_arity env sigma t
- with IsType -> try info_arity env sigma c with IsType -> true)
- | _ -> try info_arity env sigma c with IsType -> true
-
-let contents_of_cast_type env sigma c =
- if is_info_cast_type env sigma c then Pos else Null
-*)
-
-let is_info_sort = is_info_arity
-
(* calcul des arguments implicites *)
(* la seconde liste est ordonne'e *)
@@ -1211,31 +1228,36 @@ let ord_add x l =
in
aux l
-let add_free_rels_until depth m acc =
- let rec frec depth loc acc = function
+let add_free_rels_until bound m acc =
+ let rec frec depth acc = function
| Rel n ->
- if (n <= depth) & (n > loc) then (ord_add (depth-n+1) acc) else acc
- | DOPN(_,cl) -> Array.fold_left (frec depth loc) acc cl
- | DOPL(_,cl) -> List.fold_left (frec depth loc) acc cl
- | DOP2(_,c1,c2) -> frec depth loc (frec depth loc acc c1) c2
- | DOP1(_,c) -> frec depth loc acc c
- | DLAM(_,c) -> frec (depth+1) (loc+1) acc c
- | DLAMV(_,cl) -> Array.fold_left (frec (depth+1) (loc+1)) acc cl
+ if (n < bound+depth) & (n >= depth) then
+ Intset.add (bound+depth-n) acc
+ else
+ acc
+ | DOPN(_,cl) -> Array.fold_left (frec depth) acc cl
+ | DOP2(_,c1,c2) -> frec depth (frec depth acc c1) c2
+ | DOP1(_,c) -> frec depth acc c
+ | DLAM(_,c) -> frec (depth+1) acc c
+ | DLAMV(_,cl) -> Array.fold_left (frec (depth+1)) acc cl
+ | CLam (_,t,c) -> frec (depth+1) (frec depth acc (body_of_type t)) c
+ | CPrd (_,t,c) -> frec (depth+1) (frec depth acc (body_of_type t)) c
+ | CLet (_,b,t,c) -> frec (depth+1) (frec depth (frec depth acc b) (body_of_type t)) c
| VAR _ -> acc
| DOP0 _ -> acc
in
- frec depth 0 acc m
+ frec 1 acc m
(* calcule la liste des arguments implicites *)
let poly_args env sigma t =
- let rec aux n t = match (whd_betadeltaiota env sigma t) with
- | DOP2(Prod,a,DLAM(_,b)) -> add_free_rels_until n a (aux (n+1) b)
- | DOP2(Cast,t',_) -> aux n t'
- | _ -> []
+ let rec aux n t = match kind_of_term (whd_betadeltaiota env sigma t) with
+ | IsProd (_,a,b) -> add_free_rels_until n a (aux (n+1) b)
+ | IsCast (t',_) -> aux n t'
+ | _ -> Intset.empty
in
- match (strip_outer_cast (whd_betadeltaiota env sigma t)) with
- | DOP2(Prod,a,DLAM(_,b)) -> aux 1 b
+ match kind_of_term (strip_outer_cast (whd_betadeltaiota env sigma t)) with
+ | IsProd (_,a,b) -> Intset.elements (aux 1 b)
| _ -> []
diff --git a/kernel/reduction.mli b/kernel/reduction.mli
index bab5f446f..01d42fc07 100644
--- a/kernel/reduction.mli
+++ b/kernel/reduction.mli
@@ -3,7 +3,7 @@
(*i*)
open Names
-open Generic
+(*i open Generic i*)
open Term
open Univ
open Evd
@@ -35,10 +35,10 @@ val under_casts :
'a contextual_reduction_function -> 'a contextual_reduction_function
val strong : 'a reduction_function -> 'a reduction_function
val local_strong : local_reduction_function -> local_reduction_function
-val strong_prodspine : 'a reduction_function -> 'a reduction_function
+val strong_prodspine : local_reduction_function -> local_reduction_function
val stack_reduction_of_reduction :
'a reduction_function -> 'a stack_reduction_function
-val stacklam : (constr -> constr list -> 'a) -> constr list -> constr
+val stacklam : (constr * constr list -> 'a) -> constr list -> constr
-> constr list -> 'a
(*s Generic Optimized Reduction Functions using Closures *)
@@ -110,15 +110,14 @@ val reducible_mind_case : constr -> bool
val reduce_mind_case : constr miota_args -> constr
val is_arity : env -> 'a evar_map -> constr -> bool
-val is_info_arity : env -> 'a evar_map -> constr -> bool
-val is_info_sort : env -> 'a evar_map -> constr -> bool
-val is_logic_arity : env -> 'a evar_map -> constr -> bool
-val is_type_arity : env -> 'a evar_map -> constr -> bool
val is_info_type : env -> 'a evar_map -> unsafe_type_judgment -> bool
+val is_info_arity : env -> 'a evar_map -> constr -> bool
(*i Pour l'extraction
+val is_type_arity : env -> 'a evar_map -> constr -> bool
val is_info_cast_type : env -> 'a evar_map -> constr -> bool
val contents_of_cast_type : env -> 'a evar_map -> constr -> contents
i*)
+
val poly_args : env -> 'a evar_map -> constr -> int list
val whd_programs : 'a reduction_function
@@ -130,9 +129,12 @@ val fold_commands : constr list -> 'a reduction_function
val pattern_occs : (int list * constr * constr) list -> 'a reduction_function
val compute : 'a reduction_function
+(* [reduce_fix] contracts a fix redex if it is actually reducible *)
+type fix_reduction_result = NotReducible | Reduced of (constr * constr list)
+
val fix_recarg : fixpoint -> 'a list -> (int * 'a) option
-val reduce_fix : (constr -> 'a list -> constr * constr list) -> constr ->
- constr list -> bool * (constr * constr list)
+val reduce_fix : (constr * constr list -> constr * constr list) -> fixpoint ->
+ constr list -> fix_reduction_result
(*s Conversion Functions (uses closures, lazy strategy) *)
diff --git a/kernel/safe_typing.ml b/kernel/safe_typing.ml
index ca5d4a2ec..6b97c63ac 100644
--- a/kernel/safe_typing.ml
+++ b/kernel/safe_typing.ml
@@ -5,7 +5,7 @@ open Pp
open Util
open Names
open Univ
-open Generic
+(*i open Generic i*)
open Term
open Reduction
open Sign
@@ -122,6 +122,16 @@ let rec execute mf env cstr =
let (j,cst3) = gen_rel env1 Evd.empty name varj j' in
let cst = Constraint.union cst1 (Constraint.union cst2 cst3) in
(j, cst)
+
+ | IsLetIn (name,c1,c2,c3) ->
+ let (j1,cst1) = execute mf env c1 in
+ let (j2,cst2) = execute mf env c2 in
+ let { uj_val = b; uj_type = t } = cast_rel env Evd.empty j1 j2 in
+ let (j3,cst3) = execute mf (push_rel_def (name,b,t) env) c3 in
+ let cst = Constraint.union cst1 (Constraint.union cst2 cst3) in
+ ({ uj_val = mkLetIn (name, j1.uj_val, j2.uj_val, j3.uj_val) ;
+ uj_type = typed_app (subst1 j1.uj_val) j3.uj_type },
+ cst)
| IsCast (c,t) ->
let (cj,cst1) = execute mf env c in
diff --git a/kernel/sign.ml b/kernel/sign.ml
index edee43885..eac5c8cc9 100644
--- a/kernel/sign.ml
+++ b/kernel/sign.ml
@@ -3,7 +3,7 @@
open Names
open Util
-open Generic
+(*i open Generic i*)
open Term
(* Signatures *)
@@ -98,7 +98,7 @@ let map_rel_context = map
let instantiate_sign sign args =
let rec instrec = function
| ((id,None,_) :: sign, c::args) -> (id,c) :: (instrec (sign,args))
- | ((id,Some c,_) :: _, args) -> (id,c) :: (instrec (sign,args))
+ | ((id,Some c,_) :: sign, args) -> (id,c) :: (instrec (sign,args))
| ([],[]) -> []
| ([],_) | (_,[]) ->
anomaly "Signature and its instance do not match"
@@ -146,26 +146,24 @@ let empty_names_context = []
(* Transforms a product term (x1:T1)..(xn:Tn)T into the pair
([(xn,Tn);...;(x1,T1)],T), where T is not a product *)
let decompose_prod_assum =
- let rec prodec_rec l = function
- | DOP2(Prod,t,DLAM(x,c)) ->
- prodec_rec (add_rel_decl (x,outcast_type t) l) c
-(* | Letin,t,DLAM(x,c)) ->
- prodec_rec (add_rel_def (x,c,outcast_type t) l) c*)
- | DOP2(Cast,c,_) -> prodec_rec l c
- | c -> l,c
+ let rec prodec_rec l c =
+ match kind_of_term c with
+ | IsProd (x,t,c) -> prodec_rec (add_rel_decl (x,outcast_type t) l) c
+ | IsLetIn (x,b,t,c) -> prodec_rec (add_rel_def (x,b,outcast_type t) l) c
+ | IsCast (c,_) -> prodec_rec l c
+ | _ -> l,c
in
prodec_rec empty_rel_context
(* Transforms a lambda term [x1:T1]..[xn:Tn]T into the pair
([(xn,Tn);...;(x1,T1)],T), where T is not a lambda *)
let decompose_lam_assum =
- let rec lamdec_rec l = function
- | DOP2(Lambda,t,DLAM(x,c)) ->
- lamdec_rec (add_rel_decl (x,outcast_type t) l) c
-(* | Letin,t,DLAM(x,c)) ->
- lamdec_rec (add_rel_def (x,c,outcast_type t) l) c*)
- | DOP2(Cast,c,_) -> lamdec_rec l c
- | c -> l,c
+ let rec lamdec_rec l c =
+ match kind_of_term c with
+ | IsLambda (x,t,c) -> lamdec_rec (add_rel_decl (x,outcast_type t) l) c
+ | IsLetIn (x,b,t,c) -> lamdec_rec (add_rel_def (x,b,outcast_type t) l) c
+ | IsCast (c,_) -> lamdec_rec l c
+ | _ -> l,c
in
lamdec_rec empty_rel_context
@@ -175,10 +173,12 @@ let decompose_prod_n_assum n =
if n < 0 then error "decompose_prod_n: integer parameter must be positive";
let rec prodec_rec l n c =
if n=0 then l,c
- else match c with
- | DOP2(Prod,t,DLAM(x,c)) -> prodec_rec (add_rel_decl (x,outcast_type t) l) (n-1) c
- | DOP2(Cast,c,_) -> prodec_rec l n c
- | c -> error "decompose_prod_n: not enough products"
+ else match kind_of_term c with
+ | IsProd (x,t,c) -> prodec_rec (add_rel_decl(x,outcast_type t) l) (n-1) c
+ | IsLetIn (x,b,t,c) ->
+ prodec_rec (add_rel_def (x,b,outcast_type t) l) (n-1) c
+ | IsCast (c,_) -> prodec_rec l n c
+ | c -> error "decompose_prod_n: not enough products"
in
prodec_rec empty_rel_context n
@@ -188,10 +188,11 @@ let decompose_lam_n_assum n =
if n < 0 then error "decompose_lam_n: integer parameter must be positive";
let rec lamdec_rec l n c =
if n=0 then l,c
- else match c with
- | DOP2(Lambda,t,DLAM(x,c)) -> lamdec_rec (add_rel_decl (x,outcast_type t) l) (n-1) c
- | DOP2(Cast,c,_) -> lamdec_rec l n c
- | c -> error "decompose_lam_n: not enough abstractions"
+ else match kind_of_term c with
+ | IsLambda (x,t,c) -> lamdec_rec (add_rel_decl (x,outcast_type t) l) (n-1) c
+ | IsLetIn (x,b,t,c) ->
+ lamdec_rec (add_rel_def (x,b,outcast_type t) l) (n-1) c
+ | IsCast (c,_) -> lamdec_rec l n c
+ | c -> error "decompose_lam_n: not enough abstractions"
in
lamdec_rec empty_rel_context n
-
diff --git a/kernel/sign.mli b/kernel/sign.mli
index 17d9267d9..889c79b4e 100644
--- a/kernel/sign.mli
+++ b/kernel/sign.mli
@@ -3,7 +3,7 @@
(*i*)
open Names
-open Generic
+(*i open Generic i*)
open Term
(*i*)
diff --git a/kernel/sosub.ml b/kernel/sosub.ml
index 904d089d3..7212216ee 100644
--- a/kernel/sosub.ml
+++ b/kernel/sosub.ml
@@ -3,9 +3,9 @@
open Util
open Names
-open Generic
+(*i open Generic i*)
open Term
-
+(*
(* Given a term with variables in it, and second-order substitution,
this function will apply the substitution. The special
operator "XTRA[$SOAPP]" is used to represent the second-order
@@ -100,15 +100,6 @@ let propagate_names =
cllist (smap,[])
in
(smap',DOPN(op,Array.of_list cl'list))
- | DOPL(op,cl) ->
- let cllist = cl in
- let (smap',cl'list) =
- List.fold_right
- (fun c (smap,acc) ->
- let (smap',c') = proprec smap c in (smap',c'::acc))
- cllist (smap,[])
- in
- (smap',DOPL(op,cl'list))
| DLAM(na,c) ->
let (lna', c') = proprec (na::smap) c in
(List.tl lna', DLAM(List.hd lna', c'))
@@ -163,14 +154,6 @@ let rec soeval t=
socontract args lam
else
DOPN(op,cl')
- | DOPL(op,cl) ->
- let cl' = List.map soeval cl in
- if is_soapp_operator t then
- let lam = List.hd cl'
- and args = List.tl cl' in
- socontract args lam
- else
- DOPL(op,cl')
let rec try_soeval t =
match t with
@@ -197,15 +180,6 @@ let rec try_soeval t =
with (Failure _ | UserError _) -> DOPN(op,cl'))
else
DOPN(op,cl')
- | DOPL(op,cl) ->
- let cl' = List.map try_soeval cl in
- if is_soapp_operator t then
- let lam = List.hd cl'
- and args = List.tl cl' in
- (try socontract args lam
- with (Failure _ | UserError _) -> DOPL(op,cl'))
- else
- DOPL(op,cl')
let soexecute t =
let (_,t) = propagate_names [] t in
@@ -217,3 +191,7 @@ let try_soexecute t =
with (Failure _ | UserError _) -> ([],t)
in
try_soeval t
+*)
+
+let soexecute a = failwith "No longer implemented"
+
diff --git a/kernel/sosub.mli b/kernel/sosub.mli
index 531b7ee7e..123362527 100644
--- a/kernel/sosub.mli
+++ b/kernel/sosub.mli
@@ -8,5 +8,7 @@ open Term
(* Second-order substitutions. *)
val soexecute : constr -> constr
+(*
val try_soexecute : constr -> constr
+*)
diff --git a/kernel/term.ml b/kernel/term.ml
index f4c074471..40feeaab1 100644
--- a/kernel/term.ml
+++ b/kernel/term.ml
@@ -6,7 +6,6 @@
open Util
open Pp
open Names
-open Generic
open Univ
(* Coq abstract syntax with deBruijn variables; 'a is the type of sorts *)
@@ -64,14 +63,34 @@ let print_sort = function
| Prop Null -> [< 'sTR "Prop" >]
| Type _ -> [< 'sTR "Type" >]
-type constr = sorts oper term
+(********************************************************************)
+(* Generic syntax of terms with de Bruijn indexes *)
+(********************************************************************)
+
+type constr =
+ | DOP0 of sorts oper (* atomic terms *)
+ | DOP1 of sorts oper * constr (* operator of arity 1 *)
+ | DOP2 of sorts oper * constr * constr (* operator of arity 2 *)
+ | DOPN of sorts oper * constr array (* operator of variadic arity *)
+ | DLAM of name * constr (* deBruijn binder on one term *)
+ | DLAMV of name * constr array (* deBruijn binder on many terms *)
+ | CLam of name * constr * constr
+ | CPrd of name * constr * constr
+ | CLet of name * constr * constr * constr
+ | VAR of identifier (* named variable *)
+ | Rel of int (* variable as deBruijn index *)
+
+and
+ (*
+ typed_type = sorts judge
+ *)
+ typed_type = constr
type flat_arity = (name * constr) list * sorts
type 'a judge = { body : constr; typ : 'a }
(*
-type typed_type = sorts judge
type typed_term = typed_type judge
let make_typed t s = { body = t; typ = s }
@@ -91,7 +110,6 @@ let outcast_type = function
let typed_combine f g t u = { f t.body u.body ; g t.typ u.typ}
*)
-type typed_type = constr
type typed_term = typed_type judge
let make_typed t s = t
@@ -115,15 +133,281 @@ type rel_declaration = name * constr option * typed_type
(****************************************************************************)
(*********************)
+(* Occurring *)
+(*********************)
+
+exception FreeVar
+exception Occur
+
+(* (closedn n M) raises FreeVar if a variable of height greater than n
+ occurs in M, returns () otherwise *)
+
+let closedn =
+ let rec closed_rec n = function
+ | Rel(m) -> if m>n then raise FreeVar
+ | VAR _ -> ()
+ | DOPN(_,cl) -> Array.iter (closed_rec n) cl
+ | DOP2(_,c1,c2) -> closed_rec n c1; closed_rec n c2
+ | DOP1(_,c) -> closed_rec n c
+ | DLAM(_,c) -> closed_rec (n+1) c
+ | DLAMV(_,v) -> Array.iter (closed_rec (n+1)) v
+ | CLam (_,t,c) -> closed_rec n t; closed_rec (n+1) c
+ | CPrd (_,t,c) -> closed_rec n t; closed_rec (n+1) c
+ | CLet (_,b,t,c) -> closed_rec n b; closed_rec n t; closed_rec (n+1) c
+ | _ -> ()
+ in
+ closed_rec
+
+(* [closed0 M] is true iff [M] is a (deBruijn) closed term *)
+
+let closed0 term =
+ try closedn 0 term; true with FreeVar -> false
+
+(* returns the list of free debruijn indices in a term *)
+
+let free_rels m =
+ let rec frec depth acc = function
+ | Rel n -> if n >= depth then Intset.add (n-depth+1) acc else acc
+ | DOPN(_,cl) -> Array.fold_left (frec depth) acc cl
+ | DOP2(_,c1,c2) -> frec depth (frec depth acc c1) c2
+ | DOP1(_,c) -> frec depth acc c
+ | DLAM(_,c) -> frec (depth+1) acc c
+ | DLAMV(_,cl) -> Array.fold_left (frec (depth+1)) acc cl
+ | CLam (_,t,c) -> frec (depth+1) (frec depth acc t) c
+ | CPrd (_,t,c) -> frec (depth+1) (frec depth acc t) c
+ | CLet (_,b,t,c) -> frec (depth+1) (frec depth (frec depth acc b) t) c
+ | VAR _ -> acc
+ | DOP0 _ -> acc
+ in
+ frec 1 Intset.empty m
+
+(* (noccurn n M) returns true iff (Rel n) does NOT occur in term M *)
+
+let noccurn n term =
+ let rec occur_rec n = function
+ | Rel(m) -> if m = n then raise Occur
+ | VAR _ -> ()
+ | DOPN(_,cl) -> Array.iter (occur_rec n) cl
+ | DOP1(_,c) -> occur_rec n c
+ | DOP2(_,c1,c2) -> occur_rec n c1; occur_rec n c2
+ | DLAM(_,c) -> occur_rec (n+1) c
+ | DLAMV(_,v) -> Array.iter (occur_rec (n+1)) v
+ | CLam (_,t,c) -> occur_rec n t; occur_rec (n+1) c
+ | CPrd (_,t,c) -> occur_rec n t; occur_rec (n+1) c
+ | CLet (_,b,t,c) -> occur_rec n b; occur_rec n t; occur_rec (n+1) c
+ | _ -> ()
+ in
+ try occur_rec n term; true with Occur -> 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 = function
+ | Rel(p) -> if n<=p && p<n+m then raise Occur
+ | VAR _ -> ()
+ | DOPN(_,cl) -> Array.iter (occur_rec n) cl
+ | DOP1(_,c) -> occur_rec n c
+ | DOP2(_,c1,c2) -> occur_rec n c1; occur_rec n c2
+ | DLAM(_,c) -> occur_rec (n+1) c
+ | DLAMV(_,v) -> Array.iter (occur_rec (n+1)) v
+ | CLam (_,t,c) -> occur_rec n t; occur_rec (n+1) c
+ | CPrd (_,t,c) -> occur_rec n t; occur_rec (n+1) c
+ | CLet (_,b,t,c) -> occur_rec n b; occur_rec n t; occur_rec (n+1) c
+ | _ -> ()
+ in
+ try occur_rec n term; true with Occur -> 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 = function
+ | Rel p -> if n<=p & p<n+m then raise Occur
+ | VAR _ -> ()
+ | DOPN(AppL,cl) ->
+ (match cl.(0) with
+ | DOP2 (Cast,DOP0 (Meta _),_) -> ()
+ | DOP0 (Meta _) -> ()
+ | _ -> Array.iter (occur_rec n) cl)
+ | DOPN(Evar _, _) -> ()
+ | DOPN(op,cl) -> Array.iter (occur_rec n) cl
+ | DOP0(_) -> ()
+ | DOP1(_,c) -> occur_rec n c
+ | DOP2(_,c1,c2) -> occur_rec n c1; occur_rec n c2
+ | DLAM(_,c) -> occur_rec (n+1) c
+ | DLAMV(_,v) -> Array.iter (occur_rec (n+1)) v
+ | CLam (_,t,c) -> occur_rec n t; occur_rec (n+1) c
+ | CPrd (_,t,c) -> occur_rec n t; occur_rec (n+1) c
+ | CLet (_,b,t,c) -> occur_rec n b; occur_rec n t; occur_rec (n+1) c
+ in
+ try (occur_rec n term; true) with Occur -> false
+
+
+(*********************)
+(* Lifting *)
+(*********************)
+
+(* Explicit lifts and basic operations *)
+type lift_spec =
+ | ELID
+ | ELSHFT of lift_spec * int (* ELSHFT(l,n) == lift of n, then apply lift l *)
+ | ELLFT of int * lift_spec (* ELLFT(n,l) == apply l to de Bruijn > n *)
+ (* i.e under n binders *)
+
+(* compose a relocation of magnitude n *)
+let rec el_shft n = function
+ | ELSHFT(el,k) -> el_shft (k+n) el
+ | el -> if n = 0 then el else ELSHFT(el,n)
+
+
+(* cross n binders *)
+let rec el_liftn n = function
+ | ELID -> ELID
+ | ELLFT(k,el) -> el_liftn (n+k) el
+ | el -> if n=0 then el else ELLFT(n, el)
+
+let el_lift el = el_liftn 1 el
+
+(* relocation of de Bruijn n in an explicit lift *)
+let rec reloc_rel n = function
+ | ELID -> n
+ | ELLFT(k,el) ->
+ if n <= k then n else (reloc_rel (n-k) el) + k
+ | ELSHFT(el,k) -> (reloc_rel (n+k) el)
+
+
+(* The generic lifting function *)
+let rec exliftn el = function
+ | Rel i -> Rel(reloc_rel i el)
+ | DOPN(oper,cl) -> DOPN(oper, Array.map (exliftn el) cl)
+ | DOP1(oper,c) -> DOP1(oper, exliftn el c)
+ | DOP2(oper,c1,c2) -> DOP2(oper, exliftn el c1, exliftn el c2)
+ | DLAM(na,c) -> DLAM(na, exliftn (el_lift el) c)
+ | DLAMV(na,v) -> DLAMV(na, Array.map (exliftn (el_lift el)) v)
+ | CLam (n,t,c) -> CLam (n, exliftn el t, exliftn (el_lift el) c)
+ | CPrd (n,t,c) -> CPrd (n, exliftn el t, exliftn (el_lift el) c)
+ | CLet (n,b,t,c) -> CLet (n,exliftn el b,exliftn el t,exliftn (el_lift el) c)
+ | x -> x
+
+(* Lifting the binding depth across k bindings *)
+
+let liftn k n =
+ match el_liftn (pred n) (el_shft k ELID) with
+ | ELID -> (fun c -> c)
+ | el -> exliftn el
+
+let lift k = liftn k 1
+
+let pop t = lift (-1) t
+
+let lift_context n l =
+ let k = List.length l in
+ list_map_i (fun i (name,c) -> (name,liftn n (k-i) c)) 0 l
+
+(*********************)
+(* 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 =
+ let lv = Array.length lamv in
+ let rec substrec depth = function
+ | Rel k as x ->
+ if k<=depth then
+ x
+ else if k-depth <= lv then
+ lift_substituend depth lamv.(k-depth-1)
+ else
+ Rel (k-lv)
+ | VAR id -> VAR id
+ | DOPN(oper,cl) -> DOPN(oper,Array.map (substrec depth) cl)
+ | DOP1(oper,c) -> DOP1(oper,substrec depth c)
+ | DOP2(oper,c1,c2) -> DOP2(oper,substrec depth c1,substrec depth c2)
+ | DLAM(na,c) -> DLAM(na,substrec (depth+1) c)
+ | DLAMV(na,v) -> DLAMV(na,Array.map (substrec (depth+1)) v)
+ | CLam (n,t,c) -> CLam (n, substrec depth t, substrec (depth+1) c)
+ | CPrd (n,t,c) -> CPrd (n, substrec depth t, substrec (depth+1) c)
+ | CLet (n,b,t,c) -> CLet (n, substrec depth b, substrec depth t,
+ substrec (depth+1) c)
+ | x -> x
+ in
+ substrec n
+
+let substnl laml k =
+ substn_many (Array.map make_substituend (Array.of_list laml)) k
+let substl laml =
+ substn_many (Array.map make_substituend (Array.of_list laml)) 0
+let subst1 lam = substl [lam]
+
+(* (thin_val sigma) removes identity substitutions from sigma *)
+
+let rec thin_val = function
+ | [] -> []
+ | (((id,{sit=VAR id'}) as s)::tl) ->
+ if id = id' 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 = function
+ | (VAR(x) as c) ->
+ (try lift_substituend n (List.assoc x var_alist)
+ with Not_found -> c)
+
+ | DOPN(oper,cl) -> DOPN(oper,Array.map (substrec n) cl)
+ | DOP1(oper,c) -> DOP1(oper,substrec n c)
+ | DOP2(oper,c1,c2) -> DOP2(oper,substrec n c1,substrec n c2)
+ | DLAM(na,c) -> DLAM(na,substrec (n+1) c)
+ | DLAMV(na,v) -> DLAMV(na,Array.map (substrec (n+1)) v)
+ | CLam (na,t,c) -> CLam (na, substrec n t, substrec (n+1) c)
+ | CPrd (na,t,c) -> CPrd (na, substrec n t, substrec (n+1) c)
+ | CLet (na,b,t,c) -> CLet (na,substrec n b,substrec n t,substrec (n+1) c)
+ | x -> x
+ in
+ if var_alist = [] then (function x -> x) else substrec 0
+
+(* (subst_var str t) substitute (VAR str) by (Rel 1) in t *)
+let subst_var str = replace_vars [(str, Rel 1)]
+
+(* (subst_vars [id1;...;idn] t) substitute (VAR idj) by (Rel j) in t *)
+let subst_vars vars =
+ let _,subst =
+ List.fold_left (fun (n,l) var -> ((n+1),(var,Rel n)::l)) (1,[]) vars
+ in replace_vars (List.rev subst)
+
+(*********************)
(* Term constructors *)
(*********************)
(* Constructs a DeBrujin index with number n *)
let mkRel n = (Rel n)
-(* Constructs an existential variable named "?" *)
-let mkExistential = (DOP0 (XTRA "ISEVAR"))
-
(* Constructs an existential variable named "?n" *)
let mkMeta n = DOP0 (Meta n)
@@ -155,30 +439,30 @@ let mkImplicit = DOP0 (Sort implicit_sort)
(* 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 t2 =
+let mkCast (t1,t2) =
match t1 with
| DOP2(Cast,t,_) -> DOP2(Cast,t,t2)
| _ -> (DOP2 (Cast,t1,t2))
(* Constructs the product (x:t1)t2 *)
-let mkProd x t1 t2 = (DOP2 (Prod,t1,(DLAM (x,t2))))
-let mkNamedProd id typ c = mkProd (Name id) typ (subst_var id c)
-let mkProd_string s t c = mkProd (Name (id_of_string s)) t c
+let mkProd (x,t1,t2) = CPrd (x,t1,t2)
+let mkNamedProd id typ c = mkProd (Name id, typ, subst_var id c)
+let mkProd_string s t c = mkProd (Name (id_of_string s), t, c)
(* Constructs the abstraction [x:t1]t2 *)
-let mkLambda x t1 t2 = (DOP2 (Lambda,t1,(DLAM (x,t2))))
-let mkNamedLambda id typ c = mkLambda (Name id) typ (subst_var id c)
-let mkLambda_string s t c = mkLambda (Name (id_of_string s)) t c
+let mkLambda (x,t1,t2) = CLam (x,t1,t2)
+let mkNamedLambda id typ c = mkLambda (Name id, typ, subst_var id c)
+let mkLambda_string s t c = mkLambda (Name (id_of_string s), t, c)
(* Constructs [x=c_1:t]c_2 *)
-let mkLetIn x c1 t c2 = failwith "TODO"
-let mkNamedLetIn id c1 t c2 = mkLetIn (Name id) c1 t (subst_var id c2)
+let mkLetIn (x,c1,t,c2) = CLet (x,c1,t,c2)
+let mkNamedLetIn id c1 t c2 = mkLetIn (Name id, c1, t, subst_var id c2)
(* Constructs either [(x:t)c] or [[x=b:t]c] *)
let mkProd_or_LetIn (na,body,t) c =
match body with
- | None -> mkProd na t c
- | Some b -> mkLetIn na b t c
+ | None -> mkProd (na, t, c)
+ | Some b -> mkLetIn (na, b, t, c)
let mkNamedProd_or_LetIn (id,body,t) c =
match body with
@@ -188,8 +472,8 @@ let mkNamedProd_or_LetIn (id,body,t) c =
(* Constructs either [[x:t]c] or [[x=b:t]c] *)
let mkLambda_or_LetIn (na,body,t) c =
match body with
- | None -> mkLambda na t c
- | Some b -> mkLetIn na b t c
+ | None -> mkLambda (na, t, c)
+ | Some b -> mkLetIn (na, b, t, c)
let mkNamedLambda_or_LetIn (id,body,t) c =
match body with
@@ -199,7 +483,7 @@ let mkNamedLambda_or_LetIn (id,body,t) c =
(* Constructs either [(x:t)c] or [c] where [x] is replaced by [b] *)
let mkProd_wo_LetIn (na,body,t) c =
match body with
- | None -> mkProd na (body_of_type t) c
+ | None -> mkProd (na, body_of_type t, c)
| Some b -> subst1 b c
let mkNamedProd_wo_LetIn (id,body,t) c =
@@ -208,7 +492,7 @@ let mkNamedProd_wo_LetIn (id,body,t) c =
| Some b -> subst1 b (subst_var id c)
(* non-dependent product t1 -> t2 *)
-let mkArrow t1 t2 = mkProd Anonymous t1 t2
+let mkArrow t1 t2 = mkProd (Anonymous, t1, t2)
(* If lt = [t1; ...; tn], constructs the application (t1 ... tn) *)
let mkAppL a = DOPN (AppL, a)
@@ -234,7 +518,7 @@ let mkMutInd (ind_sp,l) = DOPN (MutInd ind_sp, l)
let mkMutConstruct (cstr_sp,l) = DOPN (MutConstruct cstr_sp,l)
(* Constructs the term <p>Case c of c1 | c2 .. | cn end *)
-let mkMutCase ci p c ac =
+let mkMutCase (ci, p, c, ac) =
DOPN (MutCase ci, Array.append [|p;c|] (Array.of_list ac))
let mkMutCaseA ci p c ac =
DOPN (MutCase ci, Array.append [|p;c|] ac)
@@ -316,7 +600,6 @@ let destMeta = function
| (DOP0 (Meta n)) -> n
| _ -> invalid_arg "destMeta"
-let isMETA = function DOP0(Meta _) -> true | _ -> false
(* Destructs a variable *)
let destVar = function
@@ -416,9 +699,12 @@ let rec strip_all_casts t =
| DOP1(oper,c) -> DOP1(oper,strip_all_casts c)
| DOP2(oper,c1,c2) -> DOP2(oper,strip_all_casts c1,strip_all_casts c2)
| DOPN(oper,cl) -> DOPN(oper,Array.map strip_all_casts cl)
- | DOPL(oper,cl) -> DOPL(oper,List.map strip_all_casts cl)
| DLAM(na,c) -> DLAM(na,strip_all_casts c)
| DLAMV(na,c) -> DLAMV(na,Array.map (under_outer_cast strip_all_casts) c)
+ | CLam (n,t,c) -> CLam (n, strip_all_casts t, strip_all_casts c)
+ | CPrd (n,t,c) -> CPrd (n, strip_all_casts t, strip_all_casts c)
+ | CLet (n,b,t,c) -> CLet (n, strip_all_casts b, strip_all_casts t,
+ strip_all_casts c)
| VAR _ as t -> t
| Rel _ as t -> t
@@ -430,13 +716,13 @@ let isVar = function VAR _ -> true | _ -> false
(* Destructs the product (x:t1)t2 *)
let destProd = function
- | DOP2 (Prod, t1, (DLAM (x,t2))) -> (x,t1,t2)
+ | CPrd (x,t1,t2) -> (x,t1,t2)
| _ -> invalid_arg "destProd"
let rec hd_of_prod prod =
match strip_outer_cast prod with
- | DOP2(Prod,c,DLAM(n,t')) -> hd_of_prod t'
- | t -> t
+ | CPrd (n,c,t') -> hd_of_prod t'
+ | t -> t
let hd_is_constructor t =
let is_constructor = function
@@ -449,9 +735,14 @@ let hd_is_constructor t =
(* Destructs the abstraction [x:t1]t2 *)
let destLambda = function
- | DOP2 (Lambda, t1, (DLAM (x,t2))) -> (x,t1,t2)
+ | CLam (x,t1,t2) -> (x,t1,t2)
| _ -> invalid_arg "destLambda"
+(* Destructs the let [x:=b:t1]t2 *)
+let destLetIn = function
+ | CLet (x,b,t1,t2) -> (x,b,t1,t2)
+ | _ -> invalid_arg "destProd"
+
(* Destructs an application *)
let destAppL = function
| (DOPN (AppL,a)) -> a
@@ -461,8 +752,6 @@ let destApplication = function
| (DOPN (AppL,a)) when Array.length a <> 0 -> (a.(0), array_tl a)
| _ -> invalid_arg "destApplication"
-let isAppL = function DOPN(AppL,_) -> true | _ -> false
-
let args_app = function
| DOPN(AppL,cl) -> if Array.length cl >1 then array_tl cl else [||]
| c -> [||]
@@ -573,9 +862,9 @@ let destCoFix = function
(**********************************************************************)
-type binder_kind = BProd | BLambda
+type binder_kind = BProd | BLambda | BLetIn
-type fix_kind = RFix of (int array * int) | RCofix of int
+type fix_kind = RFix of (int array * int) | RCoFix of int
type 'ctxt reference =
| RConst of section_path * 'ctxt
@@ -596,6 +885,12 @@ type cofixpoint = int * (constr array * name list * constr array)
(* Term analysis *)
(******************)
+type hnftype =
+ | HnfSort of sorts
+ | HnfProd of name * constr * constr
+ | HnfAtom of constr
+ | HnfMutInd of inductive * constr array
+
type kindOfTerm =
| IsRel of int
| IsMeta of int
@@ -605,6 +900,7 @@ type kindOfTerm =
| IsCast of constr * constr
| IsProd of name * constr * constr
| IsLambda of name * constr * constr
+ | IsLetIn of name * constr * constr * constr
| IsAppL of constr * constr list
| IsAbst of section_path * constr array
| IsEvar of existential
@@ -629,8 +925,9 @@ let kind_of_term c =
| DOP0 (Sort s) -> IsSort s
| DOP0 (XTRA s) -> IsXtra s
| DOP2 (Cast, t1, t2) -> IsCast (t1,t2)
- | DOP2 (Prod, t1, (DLAM (x,t2))) -> IsProd (x,t1,t2)
- | DOP2 (Lambda, t1, (DLAM (x,t2))) -> IsLambda (x,t1,t2)
+ | CPrd (x,t1,t2) -> IsProd (x,t1,t2)
+ | CLam (x,t1,t2) -> IsLambda (x,t1,t2)
+ | CLet (x,b,t1,t2) -> IsLetIn (x,b,t1,t2)
| DOPN (AppL,a) when Array.length a <> 0 ->
IsAppL (a.(0), List.tl (Array.to_list a))
| DOPN (Const sp, a) -> IsConst (sp,a)
@@ -648,26 +945,31 @@ let kind_of_term c =
IsCoFix (i,typedbodies)
| _ -> errorlabstrm "Term.kind_of_term" [< 'sTR "ill-formed constr" >]
+let isMeta = function DOP0(Meta _) -> true | _ -> false
+let isConst = function DOPN(Const _,_) -> true | _ -> false
+let isMutConstruct = function DOPN(MutCase _,_) -> true | _ -> false
+let isAppL = function DOPN(AppL,_) -> true | _ -> false
+
(***************************)
(* Other term constructors *)
(***************************)
-let abs_implicit c = mkLambda Anonymous mkImplicit c
-let lambda_implicit a = mkLambda (Name(id_of_string"y")) mkImplicit a
+let abs_implicit c = mkLambda (Anonymous, mkImplicit, c)
+let lambda_implicit a = mkLambda (Name(id_of_string"y"), mkImplicit, a)
let lambda_implicit_lift n a = iterate lambda_implicit n (lift n a)
(* prod_it b [xn:Tn;..;x1:T1] = (x1:T1)..(xn:Tn)b *)
-let prod_it = List.fold_left (fun c (n,t) -> mkProd n t c)
+let prod_it = List.fold_left (fun c (n,t) -> mkProd (n, t, c))
(* lam_it b [xn:Tn;..;x1:T1] = [x1:T1]..[xn:Tn]b *)
-let lam_it = List.fold_left (fun c (n,t) -> mkLambda n t c)
+let lam_it = List.fold_left (fun c (n,t) -> mkLambda (n, t, c))
(* prodn n [xn:Tn;..;x1:T1;Gamma] b = (x1:T1)..(xn:Tn)b *)
let prodn n env b =
let rec prodrec = function
| (0, env, b) -> b
- | (n, ((v,t)::l), b) -> prodrec (n-1, l, DOP2(Prod,t,DLAM(v,b)))
+ | (n, ((v,t)::l), b) -> prodrec (n-1, l, CPrd (v,t,b))
| _ -> assert false
in
prodrec (n,env,b)
@@ -676,7 +978,7 @@ let prodn n env b =
let lamn n env b =
let rec lamrec = function
| (0, env, b) -> b
- | (n, ((v,t)::l), b) -> lamrec (n-1, l, DOP2(Lambda,t,DLAM(v,b)))
+ | (n, ((v,t)::l), b) -> lamrec (n-1, l, CLam (v,t,b))
| _ -> assert false
in
lamrec (n,env,b)
@@ -712,8 +1014,7 @@ let rec to_lambda n prod =
prod
else
match prod with
- | DOP2(Prod,ty,DLAM(na,bd)) ->
- DOP2(Lambda,ty,DLAM(na, to_lambda (n-1) bd))
+ | CPrd(na,ty,bd) -> CLam(na,ty,to_lambda (n-1) bd)
| DOP2(Cast,c,_) -> to_lambda n c
| _ -> errorlabstrm "to_lambda" [<>]
@@ -722,8 +1023,7 @@ let rec to_prod n lam =
lam
else
match lam with
- | DOP2(Lambda,ty,DLAM(na,bd)) ->
- DOP2(Prod,ty,DLAM(na, to_prod (n-1) bd))
+ | CLam(na,ty,bd) -> CPrd(na,ty,to_prod (n-1) bd)
| DOP2(Cast,c,_) -> to_prod n c
| _ -> errorlabstrm "to_prod" [<>]
@@ -733,7 +1033,7 @@ let rec to_prod n lam =
let prod_app t n =
match strip_outer_cast t with
- | DOP2(Prod,_,DLAM(na,b)) -> subst1 n b
+ | CPrd (_,_,b) -> subst1 n b
| _ ->
errorlabstrm "prod_app"
[< 'sTR"Needed a product, but didn't find one" ; 'fNL >]
@@ -753,27 +1053,29 @@ let prod_applist t nL = List.fold_left prod_app t nL
(* Transforms a product term (x1:T1)..(xn:Tn)T into the pair
([(xn,Tn);...;(x1,T1)],T), where T is not a product *)
let destArity =
- let rec prodec_rec l = function
- | DOP2(Prod,t,DLAM(x,c)) -> prodec_rec ((x,t)::l) c
- | DOP2(Cast,c,_) -> prodec_rec l c
- | DOP0(Sort s) -> l,s
- | _ -> anomaly "decompose_arity: not an arity"
+ let rec prodec_rec l c =
+ match kind_of_term c with
+ | IsProd (x,t,c) -> prodec_rec ((x,t)::l) c
+ | IsCast (c,_) -> prodec_rec l c
+ | IsSort s -> l,s
+ | _ -> anomaly "decompose_arity: not an arity"
in
prodec_rec []
-let rec isArity = function
- | DOP2(Prod,_,DLAM(_,c)) -> isArity c
- | DOP2(Cast,c,_) -> isArity c
- | DOP0(Sort _) -> true
+let rec isArity c =
+ match kind_of_term c with
+ | IsProd (_,_,c) -> isArity c
+ | IsCast (c,_) -> isArity c
+ | IsSort _ -> true
| _ -> false
(* Transforms a product term (x1:T1)..(xn:Tn)T into the pair
([(xn,Tn);...;(x1,T1)],T), where T is not a product *)
let decompose_prod =
let rec prodec_rec l = function
- | DOP2(Prod,t,DLAM(x,c)) -> prodec_rec ((x,t)::l) c
- | DOP2(Cast,c,_) -> prodec_rec l c
- | c -> l,c
+ | CPrd(x,t,c) -> prodec_rec ((x,t)::l) c
+ | DOP2(Cast,c,_) -> prodec_rec l c
+ | c -> l,c
in
prodec_rec []
@@ -781,9 +1083,9 @@ let decompose_prod =
([(xn,Tn);...;(x1,T1)],T), where T is not a lambda *)
let decompose_lam =
let rec lamdec_rec l = function
- | DOP2(Lambda,t,DLAM(x,c)) -> lamdec_rec ((x,t)::l) c
- | DOP2(Cast,c,_) -> lamdec_rec l c
- | c -> l,c
+ | CLam (x,t,c) -> lamdec_rec ((x,t)::l) c
+ | DOP2 (Cast,c,_) -> lamdec_rec l c
+ | c -> l,c
in
lamdec_rec []
@@ -794,8 +1096,8 @@ let decompose_prod_n n =
let rec prodec_rec l n c =
if n=0 then l,c
else match c with
- | DOP2(Prod,t,DLAM(x,c)) -> prodec_rec ((x,t)::l) (n-1) c
- | DOP2(Cast,c,_) -> prodec_rec l n c
+ | CPrd (x,t,c) -> prodec_rec ((x,t)::l) (n-1) c
+ | DOP2 (Cast,c,_) -> prodec_rec l n c
| c -> error "decompose_prod_n: not enough products"
in
prodec_rec [] n
@@ -807,8 +1109,8 @@ let decompose_lam_n n =
let rec lamdec_rec l n c =
if n=0 then l,c
else match c with
- | DOP2(Lambda,t,DLAM(x,c)) -> lamdec_rec ((x,t)::l) (n-1) c
- | DOP2(Cast,c,_) -> lamdec_rec l n c
+ | CLam (x,t,c) -> lamdec_rec ((x,t)::l) (n-1) c
+ | DOP2 (Cast,c,_) -> lamdec_rec l n c
| c -> error "decompose_lam_n: not enough abstractions"
in
lamdec_rec [] n
@@ -817,7 +1119,7 @@ let decompose_lam_n n =
* gives n (casts are ignored) *)
let nb_lam =
let rec nbrec n = function
- | DOP2(Lambda,_,DLAM(_,c)) -> nbrec (n+1) c
+ | CLam (_,_,c) -> nbrec (n+1) c
| DOP2(Cast,c,_) -> nbrec n c
| _ -> n
in
@@ -826,145 +1128,13 @@ let nb_lam =
(* similar to nb_lam, but gives the number of products instead *)
let nb_prod =
let rec nbrec n = function
- | DOP2(Prod,_,DLAM(_,c)) -> nbrec (n+1) c
+ | CPrd (_,_,c) -> nbrec (n+1) c
| DOP2(Cast,c,_) -> nbrec n c
| _ -> n
in
nbrec 0
-(* Trop compliqué...
-(********************************************************************)
-(* various utility functions for implementing terms with bindings *)
-(********************************************************************)
-
-let extract_lifted (n,x) = lift n x
-let insert_lifted x = (0,x)
-
-(* l is a list of pairs (n:nat,x:constr), env is a stack of (na:name,T:constr)
- push_and_lift adds a component to env and lifts l one step *)
-let push_and_lift (na,t) env l =
- ((na,t)::env, List.map (fun (n,x) -> (n+1,x)) l)
-
-
-(* if T is not (x1:A1)(x2:A2)....(xn:An)T' then (push_and_liftl n env T l)
- raises an error else it gives ([x1,A1 ; x2,A2 ; ... ; xn,An]@env,T',l')
- where l' is l lifted n steps *)
-let push_and_liftl n env t l =
- let rec pushrec n t (env,l) =
- match (n,t) with
- | (0, _) -> (env,t,l)
- | (_, DOP2(Prod,t,DLAM(na,b))) ->
- pushrec (n-1) b (push_and_lift (na,t) env l)
- | (_, DOP2(Cast,t,_)) -> pushrec n t (env,l)
- | _ -> error "push_and_liftl"
- in
- pushrec n t (env,l)
-
-(* if T is not (x1:A1)(x2:A2)....(xn:An)T' then (push_and_liftl n env T l)
- raises an error else it gives ([x1,A1 ; x2,A2 ; ... ; xn,An]@env,T',l')
- where l' is l lifted n steps *)
-let push_lam_and_liftl n env t l =
- let rec pushrec n t (env,l) =
- match (n,t) with
- | (0, _) -> (env,t,l)
- | (_, DOP2(Lambda,t,DLAM(na,b))) ->
- pushrec (n-1) b (push_and_lift (na,t) env l)
- | (_, DOP2(Cast,t,_)) -> pushrec n t (env,l)
- | _ -> error "push_lam_and_liftl"
- in
- pushrec n t (env,l)
-
-(* l is a list of pairs (n:nat,x:constr), tlenv is a stack of
-(na:name,T:constr), B : constr, na : name
-(prod_and_pop ((na,T)::tlenv) B l) gives (tlenv, (na:T)B, l')
-where l' is l lifted down one step *)
-let prod_and_pop env b l =
- match env with
- | [] -> error "prod_and_pop"
- | (na,t)::tlenv ->
- (tlenv,DOP2(Prod,t,DLAM(na,b)),
- List.map (function
- (0,x) -> (0,lift (-1) x)
- | (n,x) -> (n-1,x)) l)
-
-(* recusively applies prod_and_pop :
-if env = [na1:T1 ; na2:T2 ; ... ; nan:Tn]@tlenv
-then
-(prod_and_popl n env T l) gives (tlenv,(nan:Tn)...(na1:Ta1)T,l') where
-l' is l lifted down n steps *)
-let prod_and_popl n env t l =
- let rec poprec = function
- | (0, (env,b,l)) -> (env,b,l)
- | (n, ([],_,_)) -> error "prod_and_popl"
- | (n, (env,b,l)) -> poprec (n-1, prod_and_pop env b l)
- in
- poprec (n,(env,t,l))
-
-(* similar to prod_and_pop, but gives [na:T]B intead of (na:T)B *)
-let lam_and_pop env b l =
- match env with
- | [] -> error "lam_and_pop"
- | (na,t)::tlenv ->
- (tlenv,DOP2(Lambda,t,DLAM(na,b)),
- List.map (function
- (0,x) -> (0,lift (-1) x)
- | (n,x) -> (n-1,x)) l)
-
-(* similar to lamn_and_pop but generates new names whenever the name is
- * Anonymous *)
-let lam_and_pop_named env body l acc_ids =
- match env with
- | [] -> error "lam_and_pop"
- | (na,t)::tlenv ->
- let id = match na with
- | Anonymous -> next_ident_away (id_of_string "a") acc_ids
- | Name id -> id
- in
- (tlenv,DOP2(Lambda,t,DLAM((Name id),body)),
- List.map (function
- | (0,x) -> (0,lift (-1) x)
- | (n,x) -> (n-1,x)) l,
- (id::acc_ids))
-
-(* similar to prod_and_popl but gives [nan:Tan]...[na1:Ta1]B instead of
- * (nan:Tan)...(na1:Ta1)B *)
-let lam_and_popl n env t l =
- let rec poprec = function
- | (0, (env,b,l)) -> (env,b,l)
- | (n, ([],_,_)) -> error "lam_and_popl"
- | (n, (env,b,l)) -> poprec (n-1, lam_and_pop env b l)
- in
- poprec (n,(env,t,l))
-
-(* similar to prod_and_popl but gives [nan:Tan]...[na1:Ta1]B instead of
- * but it generates names whenever nai=Anonymous *)
-
-let lam_and_popl_named n env t l =
- let rec poprec = function
- | (0, (env,b,l,_)) -> (env,b,l)
- | (n, ([],_,_,_)) -> error "lam_and_popl"
- | (n, (env,b,l,acc_ids)) -> poprec (n-1, lam_and_pop_named env b l acc_ids)
- in
- poprec (n,(env,t,l,[]))
-
-(* [lambda_ize n T endpt]
- * will pop off the first [n] products in [T], then stick in [endpt],
- * properly lifted, and then push back the products, but as lambda-
- * abstractions *)
-let lambda_ize n t endpt =
- let env = []
- and carry = [insert_lifted endpt] in
- let env, endpt =
- match push_and_liftl n env t carry with
- | (env,_,[endpt]) -> env, endpt
- | _ -> anomaly "bud in Term.lamda_ize"
- in
- let t = extract_lifted endpt in
- match lam_and_popl n env t [] with
- | (_,t,[]) -> t
- | _ -> anomaly "bud in Term.lamda_ize"
-*)
-
+(* Misc *)
let sort_hdchar = function
| Prop(_) -> "P"
| Type(_) -> "T"
@@ -1021,17 +1191,65 @@ let rec strip_head_cast = function
| DOP2(Cast,c,t) -> strip_head_cast c
| c -> c
+(* Returns the list of global variables in a term *)
+
+let global_varsl l constr =
+ let rec filtrec acc = function
+ | VAR id -> id::acc
+ | DOP1(oper,c) -> filtrec acc c
+ | DOP2(oper,c1,c2) -> filtrec (filtrec acc c1) c2
+ | DOPN(oper,cl) -> Array.fold_left filtrec acc cl
+ | DLAM(_,c) -> filtrec acc c
+ | DLAMV(_,v) -> Array.fold_left filtrec acc v
+ | CLam (_,t,c) -> filtrec (filtrec acc t) c
+ | CPrd (_,t,c) -> filtrec (filtrec acc t) c
+ | CLet (_,b,t,c) -> filtrec (filtrec (filtrec acc b) t) c
+ | _ -> acc
+ in
+ filtrec l constr
+
+let global_vars constr = global_varsl [] constr
+
+let global_vars_set constr =
+ let rec filtrec acc = function
+ | VAR id -> Idset.add id acc
+ | DOP1(oper,c) -> filtrec acc c
+ | DOP2(oper,c1,c2) -> filtrec (filtrec acc c1) c2
+ | DOPN(oper,cl) -> Array.fold_left filtrec acc cl
+ | DLAM(_,c) -> filtrec acc c
+ | DLAMV(_,v) -> Array.fold_left filtrec acc v
+ | CLam (_,t,c) -> filtrec (filtrec acc t) c
+ | CPrd (_,t,c) -> filtrec (filtrec acc t) c
+ | CLet (_,b,t,c) -> filtrec (filtrec (filtrec acc b) t) c
+ | _ -> acc
+ in
+ filtrec Idset.empty constr
+
+(* [Rel (n+m);...;Rel(n+1)] *)
+
+let rel_vect n m = Array.init m (fun i -> Rel(n+m-i))
+
+let rel_list n m =
+ let rec reln l p =
+ if p>m then l else reln (Rel(n+p)::l) (p+1)
+ in
+ reln [] 1
+
+(* Rem: end of import from old module Generic *)
+
(* Various occurs checks *)
let occur_opern s =
let rec occur_rec = function
| DOPN(oper,cl) -> s=oper or (array_exists occur_rec cl)
- | DOPL(oper,cl) -> s=oper or (List.exists occur_rec cl)
| VAR _ -> false
| DOP1(_,c) -> occur_rec c
| DOP2(_,c1,c2) -> (occur_rec c1) or (occur_rec c2)
| DLAM(_,c) -> occur_rec c
| DLAMV(_,v) -> array_exists occur_rec v
+ | CLam (_,t,c) -> occur_rec t or occur_rec c
+ | CPrd (_,t,c) -> occur_rec t or occur_rec c
+ | CLet (_,b,t,c) -> occur_rec b or occur_rec t or occur_rec c
| _ -> false
in
occur_rec
@@ -1044,12 +1262,14 @@ let occur_evar ev = occur_opern (Evar ev)
let occur_var s =
let rec occur_rec = function
| DOPN(_,cl) -> array_exists occur_rec cl
- | DOPL(_,cl) -> List.exists occur_rec cl
| VAR id -> s=id
| DOP1(_,c) -> occur_rec c
| DOP2(_,c1,c2) -> (occur_rec c1) or (occur_rec c2)
| DLAM(_,c) -> occur_rec c
| DLAMV(_,v) -> array_exists occur_rec v
+ | CLam (_,t,c) -> occur_rec t or occur_rec c
+ | CPrd (_,t,c) -> occur_rec t or occur_rec c
+ | CLet (_,b,t,c) -> occur_rec b or occur_rec t or occur_rec c
| _ -> false
in
occur_rec
@@ -1068,7 +1288,6 @@ let occur_var s =
- if no (sp,_) appears in sigma, then sp is not unfolded.
- NOTE : the case of DOPL is not handled...
*)
let replace_consts const_alist =
let rec substrec = function
@@ -1090,11 +1309,13 @@ let replace_consts const_alist =
| DOP2(oper,c1,c2) -> DOP2(oper,substrec c1,substrec c2)
| DLAM(na,c) -> DLAM(na,substrec c)
| DLAMV(na,v) -> DLAMV(na,Array.map substrec v)
+ | CLam (na,t,c) -> CLam (na, substrec t, substrec c)
+ | CPrd (na,t,c) -> CPrd (na, substrec t, substrec c)
+ | CLet (na,b,t,c) -> CLet (na, substrec b, substrec t, substrec c)
| x -> x
in
if const_alist = [] then function x -> x else substrec
-(* NOTE : the case of DOPL is not handled by whd_castapp_stack *)
let whd_castapp_stack =
let rec whrec x stack = match x with
| DOPN(AppL,cl) -> whrec (array_hd cl) (array_app_tl cl stack)
@@ -1129,41 +1350,31 @@ let rec eq_constr_rec m n =
| (DLAM(_,c1),DLAM(_,c2)) -> eq_constr_rec c1 c2
| (DLAMV(_,cl1),DLAMV(_,cl2)) ->
array_for_all2 eq_constr_rec cl1 cl2
+ | CLam(_,t1,c1), CLam(_,t2,c2) -> eq_constr_rec t1 t2 & eq_constr_rec c1 c2
+ | CPrd(_,t1,c1), CPrd(_,t2,c2) -> eq_constr_rec t1 t2 & eq_constr_rec c1 c2
+ | CLet(_,b1,t1,c1), CLet (_,b2,t2,c2) ->
+ eq_constr_rec b1 b2 & eq_constr_rec t1 t2 & eq_constr_rec c1 c2
| _ -> false
let eq_constr = eq_constr_rec
-let rec eq_constr_with_meta_rec m n=
- (m == n) or
- (m=n) or
- (match (strip_head_cast m,strip_head_cast n) with
- | (Rel p1,Rel p2) -> p1=p2
- | (DOPN(oper1,cl1),DOPN(oper2,cl2)) ->
- oper1=oper2 & array_for_all2 eq_constr_rec cl1 cl2
- | (DOP0 oper1,DOP0 oper2) -> oper1=oper2
- | (DOP1(i,c1),DOP1(j,c2)) -> (i=j) & eq_constr_rec c1 c2
- | (DOP2(i,c1,c1'),DOP2(j,c2,c2')) ->
- (i=j) & eq_constr_rec c1 c2 & eq_constr_rec c1' c2'
- | (DLAM(_,c1),DLAM(_,c2)) -> eq_constr_rec c1 c2
- | (DLAMV(_,cl1),DLAMV(_,cl2)) ->
- array_for_all2 eq_constr_rec cl1 cl2
- | _ -> false)
-
(* (dependent M N) is true iff M is eq_term with a subterm of N
M is appropriately lifted through abstractions of N *)
let dependent =
let rec deprec m t =
- (eq_constr m t)
- or (match t with
- | VAR _ -> false
- | DOP1(_,c) -> deprec m c
- | DOP2(_,c,t) -> deprec m c or deprec m t
- | DOPN(_,cl) -> array_exists (deprec m) cl
- | DOPL(_,cl) -> List.exists (deprec m) cl
- | DLAM(_,c) -> deprec (lift 1 m) c
- | DLAMV(_,v) -> array_exists (deprec (lift 1 m)) v
- | _ -> false)
+ (eq_constr m t) or
+ (match t with
+ | VAR _ -> false
+ | DOP1(_,c) -> deprec m c
+ | DOP2(_,c,t) -> deprec m c or deprec m t
+ | DOPN(_,cl) -> array_exists (deprec m) cl
+ | DLAM(_,c) -> deprec (lift 1 m) c
+ | DLAMV(_,v) -> array_exists (deprec (lift 1 m)) v
+ | CLam (_,t,c) -> deprec m t or deprec (lift 1 m) c
+ | CPrd (_,t,c) -> deprec m t or deprec (lift 1 m) c
+ | CLet (_,b,t,c) -> deprec m b or deprec m t or deprec (lift 1 m) c
+ | _ -> false)
in
deprec
@@ -1173,7 +1384,7 @@ let dependent =
let rec eta_reduce_head c =
match c with
- | DOP2(Lambda,c1,DLAM(_,c')) ->
+ | CLam (_,c1,c') ->
(match eta_reduce_head c' with
| DOPN(AppL,cl) ->
let lastn = (Array.length cl) - 1 in
@@ -1185,7 +1396,7 @@ let rec eta_reduce_head c =
if lastn = 1 then cl.(0)
else DOPN(AppL,Array.sub cl 0 lastn)
in
- if (not ((dependent (Rel 1) c')))
+ if (not ((dependent (mkRel 1) c')))
then lift (-1) c'
else c
| _ -> c)
@@ -1194,40 +1405,43 @@ let rec eta_reduce_head c =
(* alpha-eta conversion : ignore print names and casts *)
-let rec eta_eq_constr t1 t2 =
- let t1 = eta_reduce_head (strip_head_cast t1)
- and t2 = eta_reduce_head (strip_head_cast t2) in
- t1=t2 or match (t1,t2) with
- | (DOP2(Cast,c1,_),c2) -> eta_eq_constr c1 c2
- | (c1,DOP2(Cast,c2,_)) -> eta_eq_constr c1 c2
+let eta_eq_constr =
+ let rec aux t1 t2 =
+ let t1 = eta_reduce_head (strip_head_cast t1)
+ and t2 = eta_reduce_head (strip_head_cast t2) in
+ t1=t2 or match (t1,t2) with
+ | (DOP2(Cast,c1,_),c2) -> aux c1 c2
+ | (c1,DOP2(Cast,c2,_)) -> aux c1 c2
| (Rel p1,Rel p2) -> p1=p2
- | (DOPN(oper1,cl1),DOPN(oper2,cl2)) ->
- oper1=oper2 & array_for_all2 eta_eq_constr cl1 cl2
- | (DOP0 oper1,DOP0 oper2) -> oper1=oper2
- | (DOP1(i,c1),DOP1(j,c2)) -> (i=j) & eta_eq_constr c1 c2
- | (DOP2(i,c1,c1'),DOP2(j,c2,c2')) ->
- (i=j) & eta_eq_constr c1 c2 & eta_eq_constr c1' c2'
- | (DLAM(_,c1),DLAM(_,c2)) -> eta_eq_constr c1 c2
- | (DLAMV(_,cl1),DLAMV(_,cl2)) -> array_for_all2 eta_eq_constr cl1 cl2
+ | (DOPN(op1,cl1),DOPN(op2,cl2)) -> op1=op2 & array_for_all2 aux cl1 cl2
+ | (DOP0 oper1,DOP0 oper2) -> oper1=oper2
+ | (DOP1(i,c1),DOP1(j,c2)) -> (i=j) & aux c1 c2
+ | (DOP2(i,c1,c1'),DOP2(j,c2,c2')) -> (i=j) & aux c1 c2 & aux c1' c2'
+ | (DLAM(_,c1),DLAM(_,c2)) -> aux c1 c2
+ | (DLAMV(_,cl1),DLAMV(_,cl2)) -> array_for_all2 aux cl1 cl2
+ | CLam(_,t1,c1), CLam(_,t2,c2) -> aux t1 t2 & aux c1 c2
+ | CPrd(_,t1,c1), CPrd(_,t2,c2) -> aux t1 t2 & aux c1 c2
+ | CLet(_,b1,t1,c1), CLet (_,b2,t2,c2) -> aux b1 b2 & aux t1 t2 & aux c1 c2
| _ -> false
+ in aux
-(* This renames bound variablew with fresh and distinct names *)
+(* This renames bound variables with fresh and distinct names *)
(* in such a way that the printer doe not generate new names *)
(* and therefore that printed names are the intern names *)
(* In this way, tactics such as Induction works well *)
-let rec rename_bound_var l = function
- | DOP2(Prod,c1,DLAM(Name(s),c2)) ->
- if dependent (Rel 1) c2 then
+let rec rename_bound_var l c =
+ match kind_of_term c with
+ | IsProd (Name s,c1,c2) ->
+ if dependent (mkRel 1) c2 then
let s' = next_ident_away s (global_vars c2@l) in
- DOP2(Prod,c1,DLAM(Name(s'),rename_bound_var (s'::l) c2))
+ mkProd (Name s', c1, rename_bound_var (s'::l) c2)
else
- DOP2(Prod,c1,DLAM(Name(s),rename_bound_var l c2))
- | DOP2(Prod,c1,DLAM(Anonymous,c2)) ->
- DOP2(Prod,c1,DLAM(Anonymous,rename_bound_var l c2))
- | DOP2(Cast,c,t) -> DOP2(Cast,rename_bound_var l c,t)
- | x -> x
+ mkProd (Name s, c1, rename_bound_var l c2)
+ | IsProd (Anonymous,c1,c2) -> mkProd (Anonymous, c1, rename_bound_var l c2)
+ | IsCast (c,t) -> mkCast (rename_bound_var l c, t)
+ | x -> c
(***************************)
(* substitution functions *)
@@ -1269,47 +1483,38 @@ let sort_increasing_snd =
[subst_term c t] substitutes [(Rel 1)] for all occurrences of (closed)
term [c] in a term [t] *)
-let subst_term c t =
+let subst_term_gen eq_fun c t =
let rec substrec k c t =
match prefix_application k c t with
| Some x -> x
| None ->
- (if eq_constr t c then Rel(k) else match t with
- | DOPN(Const sp,cl) -> t
- | DOPN(MutInd (x_0,x_1),cl) -> t
- | DOPN(MutConstruct (x_0,x_1),cl) -> t
- | DOPN(oper,tl) -> DOPN(oper,Array.map (substrec k c) tl)
- | DOP1(i,t) -> DOP1(i,substrec k c t)
- | DOP2(oper,c1,c2) -> DOP2(oper,substrec k c c1,substrec k c c2)
- | DLAM(na,t) -> DLAM(na,substrec (k+1) (lift 1 c) t)
- | DLAMV(na,v) -> DLAMV(na,Array.map (substrec (k+1) (lift 1 c)) v)
- | _ -> t)
+ (if eq_fun t c then Rel(k) else match t with
+ | DOPN(Const sp,cl) -> t
+ | DOPN(MutInd (x_0,x_1),cl) -> t
+ | DOPN(MutConstruct (x_0,x_1),cl) -> t
+ | DOPN(oper,tl) -> DOPN(oper,Array.map (substrec k c) tl)
+ | DOP1(i,t) -> DOP1(i,substrec k c t)
+ | DOP2(oper,c1,c2) -> DOP2(oper,substrec k c c1,substrec k c c2)
+ | DLAM(na,t) -> DLAM(na,substrec (k+1) (lift 1 c) t)
+ | DLAMV(na,v) -> DLAMV(na,Array.map (substrec (k+1) (lift 1 c)) v)
+ | CLam(na,t,c2) -> CLam(na,substrec k c t,substrec (k+1) (lift 1 c) c2)
+ | CPrd(na,t,c2) -> CPrd(na,substrec k c t,substrec (k+1) (lift 1 c) c2)
+ | CLet(na,b,t,c2) -> CLet(na,substrec k c b,substrec k c t,
+ substrec (k+1) (lift 1 c) c2)
+ | _ -> t)
in
substrec 1 c t
-(* same as subst_term, but modulo eta *)
-
-let subst_term_eta_eq c t =
- let rec substrec k c t =
- match prefix_application_eta k c t with
- | Some x -> x
- | None ->
- (if eta_eq_constr t c then Rel(k) else match t with
- | DOPN(Const sp,cl) -> t
- | DOPN(oper,tl) -> DOPN(oper,Array.map (substrec k c) tl)
- | DOP1(i,t) -> DOP1(i,substrec k c t)
- | DOP2(oper,c1,c2) -> DOP2(oper,substrec k c c1,substrec k c c2)
- | DLAM(na,t) -> DLAM(na,substrec (k+1) (lift 1 c) t)
- | DLAMV(na,v)-> DLAMV(na,Array.map (substrec (k+1) (lift 1 c)) v)
- | _ -> t)
- in
- substrec 1 c t
+let subst_term = subst_term_gen eq_constr
+let subst_term_eta = subst_term_gen eta_eq_constr
(* bl : (int,constr) Listmap.t = (int * constr) list *)
(* c : constr *)
(* for each binding (i,c_i) in bl, substitutes the metavar i by c_i in c *)
(* Raises Not_found if c contains a meta that is not in the association list *)
+(* Bogué ? Pourquoi pas de lift en passant sous un lieur ?? *)
+(* Et puis meta doit fusionner avec Evar *)
let rec subst_meta bl c =
match c with
| DOP0(Meta(i)) -> List.assoc i bl
@@ -1317,6 +1522,10 @@ let rec subst_meta bl c =
| DOP2(op,c'1, c'2) -> DOP2(op, subst_meta bl c'1, subst_meta bl c'2)
| DOPN(op, c') -> DOPN(op, Array.map (subst_meta bl) c')
| DLAM(x,c') -> DLAM(x, subst_meta bl c')
+ | CLam(na,t,c) -> CLam(na,subst_meta bl t,subst_meta bl c)
+ | CPrd(na,t,c) -> CPrd(na,subst_meta bl t,subst_meta bl c)
+ | CLet(na,b,t,c) -> CLet(na,subst_meta bl b,subst_meta bl t,
+ subst_meta bl c)
| _ -> c
(* Substitute only a list of locations locs, the empty list is
@@ -1325,55 +1534,61 @@ let rec subst_meta bl c =
that will not be substituted. *)
let subst_term_occ_gen locs occ c t =
+ let pos = ref occ in
let except = List.for_all (fun n -> n<0) locs in
- let rec substcheck k occ c t =
- if except or List.exists (function u -> u>=occ) locs then
- substrec k occ c t
+ let rec substcheck k c t =
+ if except or List.exists (function u -> u >= !pos) locs then
+ substrec k c t
else
- (occ,t)
- and substrec k occ c t =
+ t
+ and substrec k c t =
if eq_constr t c then
- if except then
- if List.mem (-occ) locs then (occ+1,t) else (occ+1,Rel(k))
- else
- if List.mem occ locs then (occ+1,Rel(k)) else (occ+1,t)
- else
+ let r =
+ if except then
+ if List.mem (- !pos) locs then t else (Rel k)
+ else
+ if List.mem !pos locs then (Rel k) else t
+ in incr pos; r
+ else
match t with
- | DOPN(Const sp,tl) -> occ,t
- | DOPN(MutConstruct _,tl) -> occ,t
- | DOPN(MutInd _,tl) -> occ,t
- | DOPN(i,cl) ->
- let (occ',cl') =
- Array.fold_left
- (fun (nocc',lfd) f ->
- let (nocc'',f') = substcheck k nocc' c f in
- (nocc'',f'::lfd))
- (occ,[]) cl
- in
- (occ',DOPN(i,Array.of_list (List.rev cl')))
- | DOP2(i,t1,t2) ->
- let (nocc1,t1')=substrec k occ c t1 in
- let (nocc2,t2')=substcheck k nocc1 c t2 in
- nocc2,DOP2(i,t1',t2')
- | DOP1(i,t) ->
- let (nocc,t')= substrec k occ c t in
- nocc,DOP1(i,t')
- | DLAM(n,t) ->
- let (occ',t') = substcheck (k+1) occ (lift 1 c) t in
- (occ',DLAM(n,t'))
- | DLAMV(n,cl) ->
- let (occ',cl') =
+ | DOPN((Const _ | MutConstruct _ | MutInd _), _) -> t
+ | DOPN(i,cl) ->
+ let cl' =
+ Array.fold_left (fun lfd f -> substcheck k c f :: lfd) [] cl
+ in
+ DOPN(i,Array.of_list (List.rev cl'))
+ | DOP2(i,t1,t2) ->
+ let t1' = substrec k c t1 in
+ let t2' = substcheck k c t2 in
+ DOP2(i,t1',t2')
+ | DOP1(i,t) ->
+ DOP1(i,substrec k c t)
+ | DLAM(n,t) ->
+ DLAM(n,substcheck (k+1) (lift 1 c) t)
+ | DLAMV(n,cl) ->
+ let cl' =
Array.fold_left
- (fun (nocc',lfd) f ->
- let (nocc'',f') =
- substcheck (k+1) nocc' (lift 1 c) f
- in (nocc'',f'::lfd))
- (occ,[]) cl
+ (fun lfd f -> substcheck (k+1) (lift 1 c) f ::lfd)
+ [] cl
in
- (occ',DLAMV(n,Array.of_list (List.rev cl') ))
- | _ -> occ,t
+ DLAMV(n,Array.of_list (List.rev cl'))
+ | CLam(na,t,c2) ->
+ let t' = substrec k c t in
+ let c2' = substcheck (k+1) (lift 1 c) c2 in
+ CLam(na,t',c2')
+ | CPrd(na,t,c2) ->
+ let t' = substrec k c t in
+ let c2' = substcheck (k+1) (lift 1 c) c2 in
+ CPrd(na,t',c2')
+ | CLet(na,b,t,c2) ->
+ let b' = substrec k c b in
+ let t' = substrec k c t in
+ let c2' = substcheck (k+1) (lift 1 c) c2 in
+ CLet(na,b',t',c2')
+ | DOP0 _ | VAR _ | Rel _ -> t
in
- substcheck 1 occ c t
+ let t' = substcheck 1 c t in
+ (!pos, t')
let subst_term_occ locs c t =
if locs = [] then
@@ -1406,24 +1621,25 @@ let subst_term_occ_decl locs c (id,bodyopt,typ as d) =
(***************************)
let rec occur_meta = function
- | DOP2(Prod,t,DLAM(_,c)) -> (occur_meta t) or (occur_meta c)
- | DOP2(Lambda,t,DLAM(_,c)) -> (occur_meta t) or (occur_meta c)
+ | CPrd(_,t,c) -> (occur_meta t) or (occur_meta c)
+ | CLam(_,t,c) -> (occur_meta t) or (occur_meta c)
+ | CLet(_,b,t,c) -> (occur_meta b) or (occur_meta t) or (occur_meta c)
| DOPN(_,cl) -> (array_exists occur_meta cl)
| DOP2(Cast,c,t) -> occur_meta c or occur_meta t
| DOP0(Meta(_)) -> true
| _ -> false
-let rel_vect = (Generic.rel_vect : int -> int -> constr array)
-
let occur_existential =
let rec occrec = function
| DOPN(Evar _,_) -> true
| DOPN(_,cl) -> array_exists occrec cl
- | DOPL(_,cl) -> List.exists occrec cl
| DOP2(_,c1,c2) -> occrec c1 or occrec c2
| DOP1(_,c) -> occrec c
| DLAM(_,c) -> occrec c
| DLAMV(_,cl) -> array_exists occrec cl
+ | CPrd(_,t,c) -> (occrec t) or (occrec c)
+ | CLam(_,t,c) -> (occrec t) or (occrec c)
+ | CLet(_,b,t,c) -> (occrec b) or (occrec t) or (occrec c)
| _ -> false
in
occrec
@@ -1440,13 +1656,14 @@ let comp_term t1 t2 =
| (DOPN(o1,v1), DOPN(o2,v2)) ->
(o1==o2) & (Array.length v1 = Array.length v2)
& array_for_all2 (==) v1 v2
- | (DOPL(o1,l1), DOPL(o2,l2)) ->
- (o1==o2) & (List.length l1 = List.length l2)
- & List.for_all2 (==) l1 l2
| (DLAM(x1,t1), DLAM(x2,t2)) -> x1==x2 & t1==t2
| (DLAMV(x1,v1), DLAMV(x2,v2)) ->
(x1==x2) & (Array.length v1 = Array.length v2)
& array_for_all2 (==) v1 v2
+ | CLam(x1,t1,c1), CLam(x2,t2,c2) -> (x1==x2) & (t1==t2) & (c1==c2)
+ | CPrd(x1,t1,c1), CPrd(x2,t2,c2) -> (x1==x2) & (t1==t2) & (c1==c2)
+ | CLet(x1,b1,t1,c1), CLet (x2,b2,t2,c2) ->
+ (x1==x2) & (b1==b2) & (t1==t2) & (c1==c2)
| (Rel i, Rel j) -> i=j
| (VAR x, VAR y) -> x==y
| _ -> false
@@ -1457,9 +1674,11 @@ let hash_term (sh_rec,(sh_op,sh_na,sh_id)) t =
| DOP1(o,t) -> DOP1(sh_op o, sh_rec t)
| DOP2(o,t1,t2) -> DOP2(sh_op o, sh_rec t1, sh_rec t2)
| DOPN(o,v) -> DOPN(sh_op o, Array.map sh_rec v)
- | DOPL(o,l) -> DOPL(sh_op o, List.map sh_rec l)
| DLAM(n,t) -> DLAM(sh_na n, sh_rec t)
| DLAMV(n,v) -> DLAMV(sh_na n, Array.map sh_rec v)
+ | CLam (n,t,c) -> CLam (sh_na n, sh_rec t, sh_rec c)
+ | CPrd (n,t,c) -> CPrd (sh_na n, sh_rec t, sh_rec c)
+ | CLet (n,b,t,c) -> CLet (sh_na n, sh_rec b, sh_rec t, sh_rec c)
| Rel i -> t
| VAR x -> VAR (sh_id x)
@@ -1568,204 +1787,138 @@ let is_hd_const=function
Some (Const c,Array.of_list (List.tl (Array.to_list t)))
|_ -> None)
|_ -> None
-
-(*Gives the occurences number of t in u*)
-let rec nb_occ_term t u=
- let one_step t=function
- | DOP1(_,c) -> nb_occ_term t c
- | DOP2(_,c0,c1) -> (nb_occ_term t c0)+(nb_occ_term t c1)
- | DOPN(_,a) -> Array.fold_left (fun a x -> a+(nb_occ_term t x)) 0 a
- | DOPL(_,l) -> List.fold_left (fun a x -> a+(nb_occ_term t x)) 0 l
- | DLAM(_,c) -> nb_occ_term t c
- | DLAMV(_,a) -> Array.fold_left (fun a x -> a+(nb_occ_term t x)) 0 a
- | _ -> 0
- in
- if t=u then
- 1
- else
- one_step t u
-
-(*Alpha-conversion*)
-let bind_eq=function
- | (Anonymous,Anonymous) -> true
- | (Name _,Name _) -> true
- | _ -> false
-
- (*Tells if two constrs are equal modulo unification*)
-let rec eq_mod_rel l_meta=function
- | (t,DOP0(Meta n)) ->
- if not(List.mem n (fst (List.split l_meta))) then
- Some ([(n,t)]@l_meta)
- else if (List.assoc n l_meta)=t then
- Some l_meta
- else
- None
- | DOP1(op0,c0), DOP1(op1,c1) ->
- if op0=op1 then
- eq_mod_rel l_meta (c0,c1)
- else
- None
- | DOP2(op0,t0,c0), DOP2(op1,t1,c1) ->
- if op0=op1 then
- match (eq_mod_rel l_meta (t0,t1)) with
- | None -> None
- | Some l -> eq_mod_rel l (c0,c1)
- else
- None
- | DOPN(op0,t0), DOPN(op1,t1) ->
- if (op0=op1) & ((Array.length t0)=(Array.length t1)) then
- List.fold_left2
- (fun a c1 c2 ->
- match a with
- | None -> None
- | Some l -> eq_mod_rel l (c1,c2)) (Some l_meta)
- (Array.to_list t0) (Array.to_list t1)
- else
- None
- | DLAM(n0,t0),DLAM(n1,t1) ->
- if (bind_eq (n0,n1)) then
- eq_mod_rel l_meta (t0,t1)
- else
- None
- | (t,u) ->
- if t=u then Some l_meta else None
-
-(*Substitutes a list of meta l in t*)
-let rec subst_with_lmeta l=function
- | DOP0(Meta n) -> List.assoc n l
- | DOP1(op,t) -> DOP1(op,subst_with_lmeta l t)
- | DOP2(op,t0,t1) -> DOP2(op,subst_with_lmeta l t0,subst_with_lmeta l t1)
- | DOPN(op,t) -> DOPN(op,Array.map (subst_with_lmeta l) t)
- | DOPL(op,ld) -> DOPL(op,List.map (subst_with_lmeta l) ld)
- | DLAM(n,t) -> DLAM(n,subst_with_lmeta l t)
- | DLAMV(n,t) -> DLAMV(n,Array.map (subst_with_lmeta l) t)
- | t -> t
-
-(*Carries out the following translation: DOPN(AppL,[|t|]) -> t and
- DOPN(AppL,[|DOPN(AppL,t);...;t'|]) -> DOPN(AppL;[|t;...;t'|])*)
-let rec appl_elim=function
- | DOPN(AppL,t) ->
- if (Array.length t)=1 then
- appl_elim t.(0)
- else
- (match t.(0) with
- | DOPN(AppL,t') ->
- appl_elim (DOPN(AppL,Array.append t'
- (Array.of_list
- (List.tl (Array.to_list t)))))
- |_ -> DOPN(AppL,Array.map appl_elim t))
- | DOP1(op,t) -> DOP1(op,appl_elim t)
- | DOP2(op,t0,t1) -> DOP2(op,appl_elim t0,appl_elim t1)
- | DOPN(op,t) -> DOPN(op,Array.map appl_elim t)
- | DOPL(op,ld) -> DOPL(op,List.map appl_elim ld)
- | DLAM(n,t) -> DLAM(n,appl_elim t)
- | DLAMV(n,t) -> DLAMV(n,Array.map appl_elim t)
- | t -> t
-
-(*Gives Some(first instance of ceq in cref,occurence number for this
- instance) or None if no instance of ceq can be found in cref*)
-let sub_term_with_unif cref ceq=
- let rec find_match l_meta nb_occ op_ceq t_eq=function
- | DOPN(AppL,t) as u ->
- (match (t.(0)) with
- | DOPN(op,t_op) ->
- let t_args=Array.of_list (List.tl (Array.to_list t)) in
- if op=op_ceq then
- match
- (List.fold_left2
- (fun a c0 c1 ->
- match a with
- | None -> None
- | Some l -> eq_mod_rel l (c0,c1)) (Some l_meta)
- (Array.to_list t_args) (Array.to_list t_eq))
- with
- | None ->
- List.fold_left
- (fun (l_meta,nb_occ) x -> find_match l_meta nb_occ
- op_ceq t_eq x) (l_meta,nb_occ) (Array.to_list
- t_args)
- | Some l -> (l,nb_occ+1)
- else
- List.fold_left
- (fun (l_meta,nb_occ) x -> find_match l_meta
- nb_occ op_ceq t_eq x)
- (l_meta,nb_occ) (Array.to_list t)
- | VAR _ ->
- List.fold_left
- (fun (l_meta,nb_occ) x -> find_match l_meta
- nb_occ op_ceq t_eq x)
- (l_meta,nb_occ) (Array.to_list t)
- |_ -> (l_meta,nb_occ))
- | DOP2(_,t,DLAM(_,c)) ->
- let (lt,nbt)=find_match l_meta nb_occ op_ceq t_eq t in
- find_match lt nbt op_ceq t_eq c
- | DOPN(_,t) ->
- List.fold_left
- (fun (l_meta,nb_occ) x -> find_match l_meta nb_occ op_ceq t_eq x)
- (l_meta,nb_occ) (Array.to_list t)
- |_ -> (l_meta,nb_occ)
- in
- match (is_hd_const ceq) with
- | None ->
- if (occur_meta ceq) then
- None
- else
- let nb_occ=nb_occ_term ceq cref in
- if nb_occ=0 then
- None
- else
- Some (ceq,nb_occ)
- | Some (head,t_args) ->
- let (l,nb)=find_match [] 0 head t_args cref in
- if nb=0 then
- None
- else
- Some ((subst_with_lmeta l ceq),nb)
+
+(* Abstract decomposition of constr to deal with generic functions *)
type constr_operator =
| OpMeta of int
| OpSort of sorts
| OpRel of int | OpVar of identifier
- | OpCast | OpProd of name | OpLambda of name
+ | OpCast | OpProd of name | OpLambda of name | OpLetIn of name
| OpAppL | OpConst of section_path | OpAbst of section_path
| OpEvar of existential_key
| OpMutInd of inductive_path
| OpMutConstruct of constructor_path
| OpMutCase of case_info
- | OpRec of fix_kind
+ | OpRec of fix_kind * name list
let splay_constr = function
- | Rel n -> OpRel n, []
- | VAR id -> OpVar id, []
- | DOP0 (Meta n) -> OpMeta n, []
- | DOP0 (Sort s) -> OpSort s, []
- | DOP2 (Cast, t1, t2) -> OpCast, [t1;t2]
- | DOP2 (Prod, t1, (DLAM (x,t2))) -> OpProd x, [t1;t2]
- | DOP2 (Lambda, t1, (DLAM (x,t2))) -> OpLambda x, [t1;t2]
- | DOPN (AppL,a) -> OpAppL, Array.to_list a
- | DOPN (Const sp, a) -> OpConst sp, Array.to_list a
- | DOPN (Evar sp, a) -> OpEvar sp, Array.to_list a
- | DOPN (MutInd ind_sp, l) -> OpMutInd ind_sp, Array.to_list l
- | DOPN (MutConstruct cstr_sp,l) -> OpMutConstruct cstr_sp, Array.to_list l
- | DOPN (MutCase ci,v) -> OpMutCase ci, Array.to_list v
- | DOPN ((Fix (f,i),a)) -> OpRec (RFix (f,i)), Array.to_list a
- | DOPN ((CoFix i),a) -> OpRec (RCofix i), Array.to_list a
+ | Rel n -> OpRel n, [||]
+ | VAR id -> OpVar id, [||]
+ | DOP0 (Meta n) -> OpMeta n, [||]
+ | DOP0 (Sort s) -> OpSort s, [||]
+ | DOP2 (Cast, t1, t2) -> OpCast, [|t1;t2|]
+ | CPrd (x, t1, t2) -> OpProd x, [|t1;t2|]
+ | CLam (x, t1, t2) -> OpLambda x, [|t1;t2|]
+ | CLet (x, b, t1, t2) -> OpLetIn x, [|b;t1;t2|]
+ | DOPN (AppL,a) -> OpAppL, a
+ | DOPN (Const sp, a) -> OpConst sp, a
+ | DOPN (Evar sp, a) -> OpEvar sp, a
+ | DOPN (MutInd ind_sp, l) -> OpMutInd ind_sp, l
+ | DOPN (MutConstruct cstr_sp,l) -> OpMutConstruct cstr_sp, l
+ | DOPN (MutCase ci,v) -> OpMutCase ci, v
+ | DOPN ((Fix (f,i),a)) as c ->
+ let (fi,(tl,lna,bl)) = destFix c in
+ OpRec (RFix fi,lna), Array.append tl bl
+ | DOPN ((CoFix i),a) as c ->
+ let (fi,(tl,lna,bl)) = destCoFix c in
+ OpRec (RCoFix fi,lna), Array.append tl bl
| _ -> errorlabstrm "Term.splay_term" [< 'sTR "ill-formed constr" >]
let gather_constr = function
- | OpRel n, [] -> Rel n
- | OpVar id, [] -> VAR id
- | OpMeta n, [] -> DOP0 (Meta n)
- | OpSort s, [] -> DOP0 (Sort s)
- | OpCast, [t1;t2] -> DOP2 (Cast, t1, t2)
- | OpProd x, [t1;t2] -> DOP2 (Prod, t1, (DLAM (x,t2)))
- | OpLambda x, [t1;t2] -> DOP2 (Lambda, t1, (DLAM (x,t2)))
- | OpAppL, a -> DOPN (AppL,Array.of_list a)
- | OpConst sp, a -> DOPN (Const sp,Array.of_list a)
- | OpEvar sp, a -> DOPN (Evar sp, Array.of_list a)
- | OpMutInd ind_sp, l -> DOPN (MutInd ind_sp, Array.of_list l)
- | OpMutConstruct cstr_sp, l -> DOPN (MutConstruct cstr_sp,Array.of_list l)
- | OpMutCase ci, v -> DOPN (MutCase ci,Array.of_list v)
- | OpRec (RFix (f,i)), a -> DOPN ((Fix (f,i),Array.of_list a))
- | OpRec (RCofix i), a -> DOPN ((CoFix i),Array.of_list a)
+ | OpRel n, [||] -> Rel n
+ | OpVar id, [||] -> VAR id
+ | OpMeta n, [||] -> DOP0 (Meta n)
+ | OpSort s, [||] -> DOP0 (Sort s)
+ | OpCast, [|t1;t2|] -> DOP2 (Cast, t1, t2)
+ | OpProd x, [|t1;t2|] -> mkProd (x, t1, t2)
+ | OpLambda x, [|t1;t2|] -> mkLambda (x, t1, t2)
+ | OpLetIn x, [|b;t1;t2|] -> mkLetIn (x, b, t1, t2)
+ | OpAppL, a -> DOPN (AppL, a)
+ | OpConst sp, a -> DOPN (Const sp, a)
+ | OpEvar sp, a -> DOPN (Evar sp, a)
+ | OpMutInd ind_sp, l -> DOPN (MutInd ind_sp, l)
+ | OpMutConstruct cstr_sp, l -> DOPN (MutConstruct cstr_sp, l)
+ | OpMutCase ci, v -> DOPN (MutCase ci, v)
+ | OpRec (RFix fi,lna), a ->
+ let n = Array.length a / 2 in
+ mkFix (fi,(Array.sub a 0 n, lna, Array.sub a n n))
+ | OpRec (RCoFix i,lna), a ->
+ let n = Array.length a / 2 in
+ mkCoFix (i,(Array.sub a 0 n, lna, Array.sub a n n))
| _ -> errorlabstrm "Term.gather_term" [< 'sTR "ill-formed constr" >]
+
+let rec mycombine l1 l3 =
+ match (l1, l3) with
+ ([], []) -> []
+ | (a1::l1, a3::l3) -> (a1, None, a3) :: mycombine l1 l3
+ | (_, _) -> invalid_arg "mycombine"
+
+let rec mysplit = function
+ [] -> ([], [])
+ | (x, _, z)::l -> let (rx, rz) = mysplit l in (x::rx, z::rz)
+
+let splay_constr_with_binders = function
+ | Rel n -> OpRel n, [], [||]
+ | VAR id -> OpVar id, [], [||]
+ | DOP0 (Meta n) -> OpMeta n, [], [||]
+ | DOP0 (Sort s) -> OpSort s, [], [||]
+ | DOP2 (Cast, t1, t2) -> OpCast, [], [|t1;t2|]
+ | CPrd (x, t1, t2) -> OpProd x, [x,None,t1], [|t2|]
+ | CLam (x, t1, t2) -> OpLambda x, [x,None,t1], [|t2|]
+ | CLet (x, b, t1, t2) -> OpLetIn x, [x,Some b,t1], [|t2|]
+ | DOPN (AppL,a) -> OpAppL, [], a
+ | DOPN (Const sp, a) -> OpConst sp, [], a
+ | DOPN (Evar sp, a) -> OpEvar sp, [], a
+ | DOPN (MutInd ind_sp, l) -> OpMutInd ind_sp, [], l
+ | DOPN (MutConstruct cstr_sp,l) -> OpMutConstruct cstr_sp, [], l
+ | DOPN (MutCase ci,v) -> OpMutCase ci, [], v
+ | DOPN ((Fix (f,i),a)) as c ->
+ let (fi,(tl,lna,bl)) = destFix c in
+ let n = Array.length bl in
+ let ctxt = mycombine
+ (List.rev lna)
+ (Array.to_list (Array.mapi lift tl)) in
+ OpRec (RFix fi,lna), ctxt, bl
+ | DOPN ((CoFix i),a) as c ->
+ let (fi,(tl,lna,bl)) = destCoFix c in
+ let n = Array.length bl in
+ let ctxt = mycombine
+ (List.rev lna)
+ (Array.to_list (Array.mapi lift tl)) in
+ OpRec (RCoFix fi,lna), ctxt, bl
+ | _ -> errorlabstrm "Term.splay_term" [< 'sTR "ill-formed constr" >]
+
+let gather_constr_with_binders = function
+ | OpRel n, [], [||] -> Rel n
+ | OpVar id, [], [||] -> VAR id
+ | OpMeta n, [], [||] -> DOP0 (Meta n)
+ | OpSort s, [], [||] -> DOP0 (Sort s)
+ | OpCast, [], [|t1;t2|] -> DOP2 (Cast, t1, t2)
+ | OpProd _, [x,None,t1], [|t2|] -> mkProd (x, t1, t2)
+ | OpLambda _, [x,None,t1], [|t2|] -> mkLambda (x, t1, t2)
+ | OpLetIn _, [x,Some b,t1], [|t2|] -> mkLetIn (x, b, t1, t2)
+ | OpAppL, [], a -> DOPN (AppL, a)
+ | OpConst sp, [], a -> DOPN (Const sp, a)
+ | OpEvar sp, [], a -> DOPN (Evar sp, a)
+ | OpMutInd ind_sp, [], l -> DOPN (MutInd ind_sp, l)
+ | OpMutConstruct cstr_sp, [], l -> DOPN (MutConstruct cstr_sp, l)
+ | OpMutCase ci, [], v -> DOPN (MutCase ci, v)
+ | OpRec (RFix fi,lna), ctxt, bl ->
+ let (lna, tl) = mysplit ctxt in
+ let tl = Array.mapi (fun i -> lift (-i)) (Array.of_list tl) in
+ mkFix (fi,(tl, List.rev lna, bl))
+ | OpRec (RCoFix i,lna), ctxt, bl ->
+ let (lna, tl) = mysplit ctxt in
+ let tl = Array.mapi (fun i -> lift (-i)) (Array.of_list tl) in
+ mkCoFix (i,(tl, List.rev lna, bl))
+ | _ -> errorlabstrm "Term.gather_term" [< 'sTR "ill-formed constr" >]
+
+let generic_fold_left f acc bl tl =
+ let acc =
+ List.fold_left
+ (fun acc (_,bo,t) ->
+ match bo with
+ | None -> f acc t
+ | Some b -> f (f acc b) t) acc bl in
+ Array.fold_left f acc tl
diff --git a/kernel/term.mli b/kernel/term.mli
index cd86af675..0eb1d645d 100644
--- a/kernel/term.mli
+++ b/kernel/term.mli
@@ -2,11 +2,28 @@
(* $Id$ *)
(*i*)
+open Util
open Pp
open Names
-open Generic
+(*i open Generic i*)
(*i*)
+(*s The sorts of CCI. *)
+
+type contents = Pos | Null
+
+type sorts =
+ | Prop of contents (* Prop and Set *)
+ | Type of Univ.universe (* Type *)
+
+val str_of_contents : contents -> string
+val contents_of_str : string -> contents
+
+val mk_Set : sorts
+val mk_Prop : sorts
+
+val print_sort : sorts -> std_ppcmds
+
(*s The operators of the Calculus of Inductive Constructions.
['a] is the type of sorts. ([XTRA] is an extra slot, for putting in
whatever sort of operator we need for whatever sort of application.) *)
@@ -34,34 +51,32 @@ type 'a oper =
| CoFix of int
| XTRA of string
-(*s The sorts of CCI. *)
-
-type contents = Pos | Null
-
-val str_of_contents : contents -> string
-val contents_of_str : string -> contents
-
-type sorts =
- | Prop of contents (* Prop and Set *)
- | Type of Univ.universe (* Type *)
-
-val mk_Set : sorts
-val mk_Prop : sorts
-
-val print_sort : sorts -> std_ppcmds
-
(*s The type [constr] of the terms of CCI
- is obtained by instanciating the generic terms (type [term],
- see \refsec{generic_terms}) on the above operators, themselves instanciated
+ is obtained by instanciating a generic notion of terms
+ on the above operators, themselves instanciated
on the above sorts. *)
-type constr = sorts oper term
+(* [VAR] is used for named variables and [Rel] for variables as
+ de Bruijn indices. *)
-type flat_arity = (name * constr) list * sorts
+type constr =
+ | DOP0 of sorts oper
+ | DOP1 of sorts oper * constr
+ | DOP2 of sorts oper * constr * constr
+ | DOPN of sorts oper * constr array
+ | DLAM of name * constr
+ | DLAMV of name * constr array
+ | CLam of name * typed_type * constr
+ | CPrd of name * typed_type * constr
+ | CLet of name * constr * typed_type * constr
+ | VAR of identifier
+ | Rel of int
+
+and typed_type
-(*type 'a judge = { body : constr; typ : 'a }*)
+type flat_arity = (name * constr) list * sorts
-type typed_type
+(*s Functions about typed_type *)
val make_typed : constr -> sorts -> typed_type
val make_typed_lazy : constr -> (constr -> sorts) -> typed_type
@@ -81,9 +96,9 @@ type var_declaration = identifier * constr option * typed_type
type rel_declaration = name * constr option * typed_type
(**********************************************************************)
-type binder_kind = BProd | BLambda
+type binder_kind = BProd | BLambda | BLetIn
-type fix_kind = RFix of (int array * int) | RCofix of int
+type fix_kind = RFix of (int array * int) | RCoFix of int
type 'ctxt reference =
| RConst of section_path * 'ctxt
@@ -119,6 +134,7 @@ type kindOfTerm =
| IsCast of constr * constr
| IsProd of name * constr * constr
| IsLambda of name * constr * constr
+ | IsLetIn of name * constr * constr * constr
| IsAppL of constr * constr list
| IsAbst of section_path * constr array
| IsEvar of existential
@@ -142,9 +158,6 @@ val kind_of_term : constr -> kindOfTerm
(* Constructs a DeBrujin index *)
val mkRel : int -> constr
-(* Constructs an existential variable named "?" *)
-val mkExistential : constr
-
(* Constructs an existential variable named "?n" *)
val mkMeta : int -> constr
@@ -172,15 +185,15 @@ val implicit_sort : sorts
(* Constructs the term $t_1::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 -> constr -> constr
+val mkCast : constr * constr -> constr
(* Constructs the product $(x:t_1)t_2$ *)
-val mkProd : name -> constr -> constr -> constr
+val mkProd : name * constr * constr -> constr
val mkNamedProd : identifier -> constr -> constr -> constr
val mkProd_string : string -> constr -> constr -> constr
(* Constructs the product $(x:t_1)t_2$ *)
-val mkLetIn : name -> constr -> constr -> constr -> constr
+val mkLetIn : name * constr * constr * constr -> constr
val mkNamedLetIn : identifier -> constr -> constr -> constr -> constr
(* Constructs either [(x:t)c] or [[x=b:t]c] *)
@@ -199,7 +212,7 @@ val mkNamedProd_wo_LetIn : var_declaration -> constr -> constr
val mkArrow : constr -> constr -> constr
(* Constructs the abstraction $[x:t_1]t_2$ *)
-val mkLambda : name -> constr -> constr -> constr
+val mkLambda : name * constr * constr -> constr
val mkNamedLambda : identifier -> constr -> constr -> constr
(* [mkLambda_string s t c] constructs $[s:t]c$ *)
@@ -230,7 +243,7 @@ val mkMutInd : inductive -> constr
val mkMutConstruct : constructor -> constr
(* Constructs the term <p>Case c of c1 | c2 .. | cn end *)
-val mkMutCase : case_info -> constr -> constr -> constr list -> constr
+val mkMutCase : case_info * constr * constr * constr list -> constr
val mkMutCaseA : case_info -> constr -> constr -> constr array -> constr
(* If [recindxs = [|i1,...in|]]
@@ -238,7 +251,7 @@ val mkMutCaseA : case_info -> constr -> constr -> constr array -> constr
[funnames = [f1,.....fn]]
[bodies = [b1,.....bn]]
then [ mkFix ((recindxs,i),typarray, funnames, bodies) ]
- constructs the $i$th function of the block
+ constructs the $i$th function of the block (counting from 0)
[Fixpoint f1 [ctx1] = b1
with f2 [ctx2] = b2
@@ -282,7 +295,7 @@ val destRel : constr -> int
(* Destructs an existential variable *)
val destMeta : constr -> int
-val isMETA : constr -> bool
+val isMeta : constr -> bool
(* Destructs a variable *)
val destVar : constr -> identifier
@@ -330,6 +343,9 @@ val hd_is_constructor : constr -> bool
(* Destructs the abstraction $[x:t_1]t_2$ *)
val destLambda : constr -> name * constr * constr
+(* Destructs the let $[x:=b:t_1]t_2$ *)
+val destLetIn : constr -> name * constr * constr * constr
+
(* Destructs an application *)
val destAppL : constr -> constr array
val isAppL : constr -> bool
@@ -339,6 +355,7 @@ val destApplication : constr -> constr * constr array
(* Destructs a constant *)
val destConst : constr -> section_path * constr array
+val isConst : constr -> bool
val path_of_const : constr -> section_path
val args_of_const : constr -> constr array
@@ -358,6 +375,7 @@ val args_of_mind : constr -> constr array
(* Destructs a constructor *)
val destMutConstruct : constr -> constructor
+val isMutConstruct : constr -> bool
val op_of_mconstr : constr -> constructor_path
val args_of_mconstr : constr -> constr array
@@ -541,6 +559,88 @@ val le_kind_implicit : constr -> constr -> bool
val sort_hdchar : sorts -> string
+(* Generic functions *)
+val free_rels : constr -> Intset.t
+
+(* [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] considers only
+ meta-variable applied to some terms (intented to be its local
+ context) (for existential variables, it is necessarily the case) *)
+val noccur_with_meta : int -> int -> constr -> bool
+
+(* [liftn n k c] lifts by [n] indexes above [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
+
+(* [pop c] lifts by -1 the positive indexes in [c] *)
+val pop : constr -> constr
+
+(* [lift_context n ctxt] lifts terms in [ctxt] by [n] preserving
+ (i.e. not lifting) the internal references between terms of [ctxt];
+ more recent terms come first in [ctxt] *)
+val lift_context : int -> (name * constr) list -> (name * constr) list
+
+(* [substnl [a1;...;an] k c] substitutes in parallele [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
+
+(* [global_vars c] returns the list of [id]'s occurring as [VAR id] in [c] *)
+val global_vars : constr -> identifier list
+
+val global_vars_set : constr -> Idset.t
+val replace_vars : (identifier * constr) list -> constr -> constr
+val subst_var : identifier -> 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 keeped *)
+val subst_vars : identifier list -> constr -> constr
+
+(* [rel_list n m] and [rel_vect n m] compute [[Rel (n+m);...;Rel(n+1)]] *)
+val rel_vect : int -> int -> constr array
+val rel_list : int -> int -> constr list
+
+(*i************************************************************************i*)
+(*i Pour Closure
+(* Explicit substitutions of type ['a]. [ESID] = identity.
+ [CONS(t,S)] = $S.t$ i.e. parallel substitution. [SHIFT(n,S)] =
+ $(\uparrow n~o~S)$ i.e. terms in S are relocated with n vars.
+ [LIFT(n,S)] = $(\%n~S)$ stands for $((\uparrow n~o~S).n...1)$. *)
+type 'a subs =
+ | ESID
+ | CONS of 'a * 'a subs
+ | SHIFT of int * 'a subs
+ | LIFT of int * 'a subs
+val subs_cons : 'a * 'a subs -> 'a subs
+val subs_liftn : int -> 'a subs -> 'a subs
+val subs_lift : 'a subs -> 'a subs
+val subs_shft : int * 'a subs -> 'a subs
+val expand_rel : int -> 'a subs -> (int * 'a, int) union
+i*)
+(*s Lifts. [ELSHFT(l,n)] == lift of [n], then apply [lift l].
+ [ELLFT(n,l)] == apply [l] to de Bruijn > [n] i.e under n binders. *)
+type lift_spec =
+ | ELID
+ | ELSHFT of lift_spec * int
+ | ELLFT of int * lift_spec
+val el_shft : int -> lift_spec -> lift_spec
+val el_lift : lift_spec -> lift_spec
+val reloc_rel: int -> lift_spec -> int
+(*i*)
(*s Occur check functions. *)
@@ -550,7 +650,6 @@ val occur_meta : constr -> bool
(*i val max_occur_meta : constr -> int i*)
val occur_existential : constr -> bool
-val rel_vect : int -> int -> constr array
(* [(occur_const (s:section_path) c)] returns [true] if constant [s] occurs
in c, [false] otherwise *)
@@ -562,7 +661,7 @@ val occur_evar : existential_key -> constr -> bool
(* [(occur_var id c)] returns [true] if variable [id] occurs free
in c, [false] otherwise *)
-val occur_var : identifier -> 'a term -> bool
+val occur_var : identifier -> constr -> bool
(* [dependent M N] is true iff M is eq\_constr with a subterm of N
M is appropriately lifted through abstractions of N *)
@@ -579,7 +678,6 @@ val eta_eq_constr : constr -> constr -> bool
(*s The following functions substitutes [what] by [Rel 1] in [where] *)
val subst_term : what:constr -> where:constr -> constr
-val subst_term_eta_eq : what:constr -> where:constr -> constr
val subst_term_occ : occs:int list -> what:constr -> where:constr -> constr
val subst_term_occ_decl : occs:int list -> what:constr ->
where:var_declaration -> var_declaration
@@ -598,16 +696,26 @@ type constr_operator =
| OpMeta of int
| OpSort of sorts
| OpRel of int | OpVar of identifier
- | OpCast | OpProd of name | OpLambda of name
+ | OpCast | OpProd of name | OpLambda of name | OpLetIn of name
| OpAppL | OpConst of section_path | OpAbst of section_path
| OpEvar of existential_key
| OpMutInd of inductive_path
| OpMutConstruct of constructor_path
| OpMutCase of case_info
- | OpRec of fix_kind
+ | OpRec of fix_kind * Names.name list
+
+val splay_constr : constr -> constr_operator * constr array
+val gather_constr : constr_operator * constr array -> constr
+
+val splay_constr_with_binders : constr ->
+ constr_operator * (name * constr option * constr) list * constr array
+val gather_constr_with_binders :
+ constr_operator * (name * constr option * constr) list * constr array
+ -> constr
-val splay_constr : constr -> constr_operator * constr list
-val gather_constr : constr_operator * constr list -> constr
+val generic_fold_left :
+ ('a -> constr -> 'a) -> 'a -> (name * constr option * constr) list
+ -> constr array -> 'a
(*s Hash-consing functions for constr. *)
diff --git a/kernel/type_errors.ml b/kernel/type_errors.ml
index 518809392..34dee81c8 100644
--- a/kernel/type_errors.ml
+++ b/kernel/type_errors.ml
@@ -9,6 +9,24 @@ open Environ
(* Type errors. *)
+type guard_error =
+ (* Fixpoints *)
+ | NotEnoughAbstractionInFixBody
+ | RecursionNotOnInductiveType
+ | RecursionOnIllegalTerm
+ | NotEnoughArgumentsForFixCall
+ (* CoFixpoints *)
+ | CodomainNotInductiveType of constr
+ | NestedRecursiveOccurrences
+ | UnguardedRecursiveCall of constr
+ | RecCallInTypeOfAbstraction of constr
+ | RecCallInNonRecArgOfConstructor of constr
+ | RecCallInTypeOfDef of constr
+ | RecCallInCaseFun of constr
+ | RecCallInCaseArg of constr
+ | RecCallInCasePred of constr
+ | NotGuardedForm
+
type type_error =
| UnboundRel of int
| NotAType of unsafe_judgment
@@ -24,7 +42,7 @@ type type_error =
| CantApplyBadType of (int * constr * constr)
* unsafe_judgment * unsafe_judgment list
| CantApplyNonFunctional of unsafe_judgment * unsafe_judgment list
- | IllFormedRecBody of std_ppcmds * name list * int * constr array
+ | IllFormedRecBody of guard_error * name list * int * constr array
| IllTypedRecBody of int * name list * unsafe_judgment array
* typed_type array
| NotInductive of constr
@@ -82,8 +100,8 @@ let error_cant_apply_not_functional k env rator randl =
let error_cant_apply_bad_type k env sigma t rator randl =
raise(TypeError (k, env_ise sigma env, CantApplyBadType (t,rator,randl)))
-let error_ill_formed_rec_body k env str lna i vdefs =
- raise (TypeError (k, env, IllFormedRecBody (str,lna,i,vdefs)))
+let error_ill_formed_rec_body k env why lna i vdefs =
+ raise (TypeError (k, env, IllFormedRecBody (why,lna,i,vdefs)))
let error_ill_typed_rec_body k env i lna vdefj vargs =
raise (TypeError (k, env, IllTypedRecBody (i,lna,vdefj,vargs)))
diff --git a/kernel/type_errors.mli b/kernel/type_errors.mli
index 20fa410e4..f5e16f3c4 100644
--- a/kernel/type_errors.mli
+++ b/kernel/type_errors.mli
@@ -11,6 +11,26 @@ open Environ
(* Type errors. \label{typeerrors} *)
+(*i Rem: NotEnoughAbstractionInFixBody should only occur with "/i" Fix
+ notation i*)
+type guard_error =
+ (* Fixpoints *)
+ | NotEnoughAbstractionInFixBody
+ | RecursionNotOnInductiveType
+ | RecursionOnIllegalTerm
+ | NotEnoughArgumentsForFixCall
+ (* CoFixpoints *)
+ | CodomainNotInductiveType of constr
+ | NestedRecursiveOccurrences
+ | UnguardedRecursiveCall of constr
+ | RecCallInTypeOfAbstraction of constr
+ | RecCallInNonRecArgOfConstructor of constr
+ | RecCallInTypeOfDef of constr
+ | RecCallInCaseFun of constr
+ | RecCallInCaseArg of constr
+ | RecCallInCasePred of constr
+ | NotGuardedForm
+
type type_error =
| UnboundRel of int
| NotAType of unsafe_judgment
@@ -26,7 +46,7 @@ type type_error =
| CantApplyBadType of (int * constr * constr)
* unsafe_judgment * unsafe_judgment list
| CantApplyNonFunctional of unsafe_judgment * unsafe_judgment list
- | IllFormedRecBody of std_ppcmds * name list * int * constr array
+ | IllFormedRecBody of guard_error * name list * int * constr array
| IllTypedRecBody of int * name list * unsafe_judgment array
* typed_type array
| NotInductive of constr
@@ -80,8 +100,7 @@ val error_cant_apply_bad_type :
unsafe_judgment -> unsafe_judgment list -> 'b
val error_ill_formed_rec_body :
- path_kind -> env -> std_ppcmds
- -> name list -> int -> constr array -> 'b
+ path_kind -> env -> guard_error -> name list -> int -> constr array -> 'b
val error_ill_typed_rec_body :
path_kind -> env -> int -> name list -> unsafe_judgment array
diff --git a/kernel/typeops.ml b/kernel/typeops.ml
index 4077d852f..4b22b0b6a 100644
--- a/kernel/typeops.ml
+++ b/kernel/typeops.ml
@@ -5,7 +5,7 @@ open Pp
open Util
open Names
open Univ
-open Generic
+(*i open Generic i*)
open Term
open Declarations
open Sign
@@ -113,17 +113,17 @@ let type_of_existential env sigma c =
(* Case. *)
let rec mysort_of_arity env sigma c =
- match whd_betadeltaiota env sigma c with
- | DOP0(Sort(s)) -> s
- | DOP2(Prod,_,DLAM(_,c2)) -> mysort_of_arity env sigma c2
+ match kind_of_term (whd_betadeltaiota env sigma c) with
+ | IsSort s -> s
+ | IsProd(_,_,c2) -> mysort_of_arity env sigma c2
| _ -> invalid_arg "mysort_of_arity"
let error_elim_expln env sigma kp ki =
- if is_info_sort env sigma kp && not (is_info_sort env sigma ki) then
+ if is_info_arity env sigma kp && not (is_info_arity env sigma ki) then
"non-informative objects may not construct informative ones."
else
- match (kp,ki) with
- | (DOP0(Sort (Type _)), DOP0(Sort (Prop _))) ->
+ match (kind_of_term kp,kind_of_term ki) with
+ | IsSort (Type _), IsSort (Prop _) ->
"strong elimination on non-small inductive types leads to paradoxes."
| _ -> "wrong arity"
@@ -131,13 +131,15 @@ exception Arity of (constr * constr * string) option
let is_correct_arity env sigma kelim (c,p) indf (pt,t) =
let rec srec (pt,t) =
- match whd_betadeltaiota env sigma pt, whd_betadeltaiota env sigma t with
- | DOP2(Prod,a1,DLAM(_,a2)), DOP2(Prod,a1',DLAM(_,a2')) ->
+ let pt' = whd_betadeltaiota env sigma pt in
+ let t' = whd_betadeltaiota env sigma t in
+ match kind_of_term pt', kind_of_term t' with
+ | IsProd (_,a1,a2), IsProd (_,a1',a2') ->
if is_conv env sigma a1 a1' then
srec (a2,a2')
else
raise (Arity None)
- | DOP2(Prod,a1,DLAM(_,a2)), ki ->
+ | IsProd (_,a1,a2), _ ->
let k = whd_betadeltaiota env sigma a2 in
let ksort = (match k with DOP0(Sort s) -> s
| _ -> raise (Arity None)) in
@@ -146,18 +148,18 @@ let is_correct_arity env sigma kelim (c,p) indf (pt,t) =
if List.exists (base_sort_cmp CONV ksort) kelim then
(true,k)
else
- raise (Arity (Some(k,ki,error_elim_expln env sigma k ki)))
+ raise (Arity (Some(k,t',error_elim_expln env sigma k t')))
else
raise (Arity None)
- | k, DOP2(Prod,_,_) ->
+ | k, IsProd (_,_,_) ->
raise (Arity None)
| k, ki ->
- let ksort = (match k with DOP0(Sort s) -> s
+ let ksort = (match k with IsSort s -> s
| _ -> raise (Arity None)) in
if List.exists (base_sort_cmp CONV ksort) kelim then
- false,k
+ false, pt'
else
- raise (Arity (Some(k,ki,error_elim_expln env sigma k ki)))
+ raise (Arity (Some(pt',t',error_elim_expln env sigma pt' t')))
in
try srec (pt,t)
with Arity kinds ->
@@ -274,12 +276,13 @@ let typed_product env name var c =
let rcst = ref Constraint.empty in
let hacked_sort_of_product s1 s2 =
let (s,cst) = sort_of_product s1 s2 (universes env) in (rcst:=cst; s) in
- typed_combine (mkProd name) hacked_sort_of_product var c, !rcst
+ typed_combine (fun c t -> mkProd (name,c,t)) hacked_sort_of_product var c,
+ !rcst
let abs_rel env sigma name var j =
let cvar = incast_type var in
let typ,cst = typed_product env name var j.uj_type in
- { uj_val = mkLambda name cvar j.uj_val;
+ { uj_val = mkLambda (name, cvar, j.uj_val);
uj_type = typ },
cst
@@ -292,7 +295,7 @@ let gen_rel env sigma name varj j =
let (s',g) = sort_of_product varj.utj_type s (universes env) in
let res_type = mkSort s' in
let (res_kind,g') = type_of_sort res_type in
- { uj_val = mkProd name (incast_type var) j.uj_val;
+ { uj_val = mkProd (name, incast_type var, j.uj_val);
uj_type = make_typed res_type res_kind },
g'
| _ ->
@@ -321,8 +324,8 @@ let apply_rel_list env sigma nocheck argjl funj =
uj_type = typed_app (fun _ -> typ) funj.uj_type },
cst
| hj::restjl ->
- match whd_betadeltaiota env sigma typ with
- | DOP2(Prod,c1,DLAM(_,c2)) ->
+ match kind_of_term (whd_betadeltaiota env sigma typ) with
+ | IsProd (_,c1,c2) ->
if nocheck then
apply_rec (n+1) (subst1 hj.uj_val c2) cst restjl
else
@@ -342,33 +345,6 @@ let apply_rel_list env sigma nocheck argjl funj =
(* Fixpoints. *)
-(* 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 *)
-
-exception Occur
-let noccur_with_meta n m term =
- let rec occur_rec n = function
- | Rel p -> if n<=p & p<n+m then raise Occur
- | VAR _ -> ()
- | DOPN(AppL,cl) ->
- (match strip_outer_cast cl.(0) with
- | DOP0 (Meta _) -> ()
- | _ -> Array.iter (occur_rec n) cl)
- | DOPN(Evar _, _) -> ()
- | DOPN(op,cl) -> Array.iter (occur_rec n) cl
- | DOPL(_,cl) -> List.iter (occur_rec n) cl
- | DOP0(_) -> ()
- | DOP1(_,c) -> occur_rec n c
- | DOP2(_,c1,c2) -> occur_rec n c1; occur_rec n c2
- | DLAM(_,c) -> occur_rec (n+1) c
- | DLAMV(_,v) -> Array.iter (occur_rec (n+1)) v
- in
- try (occur_rec n term; true) with Occur -> false
-
(* Check if t is a subterm of Rel n, and gives its specification,
assuming lst already gives index of
subterms with corresponding specifications of recursive arguments *)
@@ -396,17 +372,17 @@ let rec instantiate_recarg sp lrc ra =
(* propagate checking for F,incorporating recursive arguments *)
let check_term env mind_recvec f =
let rec crec n l (lrec,c) =
- match (lrec,strip_outer_cast c) with
- | (Param(_)::lr,DOP2(Lambda,_,DLAM(_,b))) ->
+ match lrec, kind_of_term (strip_outer_cast c) with
+ | (Param(_)::lr, IsLambda (_,_,b)) ->
let l' = map_lift_fst l in
crec (n+1) l' (lr,b)
- | (Norec::lr,DOP2(Lambda,_,DLAM(_,b))) ->
+ | (Norec::lr, IsLambda (_,_,b)) ->
let l' = map_lift_fst l in
crec (n+1) l' (lr,b)
- | (Mrec(i)::lr,DOP2(Lambda,_,DLAM(_,b))) ->
+ | (Mrec(i)::lr, IsLambda (_,_,b)) ->
let l' = map_lift_fst l in
crec (n+1) ((1,mind_recvec.(i))::l') (lr,b)
- | (Imbr((sp,i) as ind_sp,lrc)::lr,DOP2(Lambda,_,DLAM(_,b))) ->
+ | (Imbr((sp,i) as ind_sp,lrc)::lr, IsLambda (_,_,b)) ->
let l' = map_lift_fst l in
let sprecargs =
mis_recargs (lookup_mind_specif (ind_sp,[||]) env) in
@@ -414,7 +390,7 @@ let check_term env mind_recvec f =
Array.map (List.map (instantiate_recarg sp lrc)) sprecargs.(i)
in
crec (n+1) ((1,lc)::l') (lr,b)
- | _,f_0 -> f n l f_0
+ | _,_ -> f n l (strip_outer_cast c)
in
crec
@@ -425,28 +401,28 @@ let is_inst_var env sigma k c =
let is_subterm_specif env sigma lcx mind_recvec =
let rec crec n lst c =
- match whd_betadeltaiota_stack env sigma c [] with
- | ((Rel k),_) -> find_sorted_assoc k lst
- | (DOPN(MutCase _,_) as x,_) ->
- let ( _,_,c,br) = destCase x in
- if Array.length br = 0 then
- [||]
- else
- let lcv =
- (try
- if is_inst_var env sigma n c then lcx else (crec n lst c)
- with Not_found -> (Array.create (Array.length br) []))
- in
- assert (Array.length br = Array.length lcv);
- let stl =
- array_map2
- (fun lc a ->
- check_term env mind_recvec crec n lst (lc,a)) lcv br
- in
- stl.(0)
+ let f,l = whd_betadeltaiota_stack env sigma c [] in
+ match kind_of_term f with
+ | IsRel k -> find_sorted_assoc k lst
+
+ | IsMutCase ( _,_,c,br) ->
+ if Array.length br = 0 then
+ [||]
+ else
+ let lcv =
+ (try
+ if is_inst_var env sigma n c then lcx else (crec n lst c)
+ with Not_found -> (Array.create (Array.length br) []))
+ in
+ assert (Array.length br = Array.length lcv);
+ let stl =
+ array_map2
+ (fun lc a ->
+ check_term env mind_recvec crec n lst (lc,a)) lcv br
+ in
+ stl.(0)
- | (DOPN(Fix(_),la) as mc,l) ->
- let ((recindxs,i),(typarray,funnames,bodies)) = destFix mc in
+ | IsFix ((recindxs,i),(typarray,funnames,bodies)) ->
let nbfix = List.length funnames in
let decrArg = recindxs.(i) in
let theBody = bodies.(i) in
@@ -470,12 +446,12 @@ let is_subterm_specif env sigma lcx mind_recvec =
in
crec (n+nbOfAbst) newlst strippedBody
- | (DOP2(Lambda,_,DLAM(_,b)),[]) ->
- let lst' = map_lift_fst lst in
- crec (n+1) lst' b
+ | IsLambda (_,_,b) when l=[] ->
+ let lst' = map_lift_fst lst in
+ crec (n+1) lst' b
(*** Experimental change *************************)
- | (DOP0(Meta _),_) -> [||]
+ | IsMeta _ -> [||]
| _ -> raise Not_found
in
crec
@@ -486,26 +462,29 @@ let is_subterm env sigma lcx mind_recvec n lst c =
with Not_found ->
false
+exception FixGuardError of guard_error
+
(* Auxiliary function: it checks a condition f depending on a deBrujin
index for a certain number of abstractions *)
-let rec check_subterm_rec_meta env sigma vectn k def =
+let rec check_subterm_rec_meta env sigma vectn k def =
+ (* If k<0, it is a general fixpoint *)
(k < 0) or
(let nfi = Array.length vectn in
(* check fi does not appear in the k+1 first abstractions,
gives the type of the k+1-eme abstraction *)
let rec check_occur n def =
- (match strip_outer_cast def with
- | DOP2(Lambda,a,DLAM(_,b)) ->
- if noccur_with_meta n nfi a then
- if n = k+1 then (a,b) else check_occur (n+1) b
- else
- error "Bad occurrence of recursive call"
- | _ -> error "Not enough abstractions in the definition") in
+ match kind_of_term (strip_outer_cast def) with
+ | IsLambda (_,a,b) ->
+ if noccur_with_meta n nfi a then
+ if n = k+1 then (a,b) else check_occur (n+1) b
+ else
+ anomaly "check_subterm_rec_meta: Bad occurrence of recursive call"
+ | _ -> raise (FixGuardError NotEnoughAbstractionInFixBody) in
let (c,d) = check_occur 1 def in
let ((sp,tyi),_ as mind, largs) =
- (try find_minductype env sigma c
- with Induc -> error "Recursive definition on a non inductive type") in
+ try find_minductype env sigma c
+ with Induc -> raise (FixGuardError RecursionNotOnInductiveType) in
let mind_recvec = mis_recargs (lookup_mind_specif mind env) in
let lcx = mind_recvec.(tyi) in
(* n = decreasing argument in the definition;
@@ -516,8 +495,9 @@ let rec check_subterm_rec_meta env sigma vectn k def =
(* n gives the index of the recursive variable *)
(noccur_with_meta (n+k+1) nfi t) or
(* no recursive call in the term *)
- (match whd_betadeltaiota_stack env sigma t [] with
- | (Rel p,l) ->
+ (let f,l = whd_betadeltaiota_stack env sigma t [] in
+ match kind_of_term f with
+ | IsRel p ->
if n+k+1 <= p & p < n+k+nfi+1 then
(* recursive call *)
let glob = nfi+n+k-p in (* the index of the recursive call *)
@@ -527,12 +507,12 @@ let rec check_subterm_rec_meta env sigma vectn k def =
(la,(z::lrest)) ->
if (is_subterm env sigma lcx mind_recvec n lst z)
then List.for_all (check_rec_call n lst) (la@lrest)
- else error "Recursive call applied to an illegal term"
+ else raise (FixGuardError RecursionOnIllegalTerm)
| _ -> assert false)
- else error "Not enough arguments for the recursive call"
+ else raise (FixGuardError NotEnoughArgumentsForFixCall)
else List.for_all (check_rec_call n lst) l
- | (DOPN(MutCase _,_) as mc,l) ->
- let (ci,p,c_0,lrest) = destCase mc in
+
+ | IsMutCase (ci,p,c_0,lrest) ->
let lc =
(try
if is_inst_var env sigma n c_0 then
@@ -563,13 +543,16 @@ let rec check_subterm_rec_meta env sigma vectn k def =
Eduardo 7/9/98 *)
- | (DOPN(Fix(_),la) as mc,l) ->
+ | IsFix ((recindxs,i),(typarray,funnames,bodies)) ->
(List.for_all (check_rec_call n lst) l) &&
- let ((recindxs,i),(typarray,funnames,bodies)) = destFix mc in
let nbfix = List.length funnames in
let decrArg = recindxs.(i) in
if (List.length l < (decrArg+1)) then
- (array_for_all (check_rec_call n lst) la)
+ (array_for_all (check_rec_call n lst) typarray)
+ &&
+ (array_for_all
+ (check_rec_call (n+nbfix) (map_lift_fst_n nbfix lst))
+ bodies)
else
let theDecrArg = List.nth l decrArg in
let recArgsDecrArg =
@@ -579,7 +562,11 @@ let rec check_subterm_rec_meta env sigma vectn k def =
Array.create 0 []
in
if (Array.length recArgsDecrArg)=0 then
- array_for_all (check_rec_call n lst) la
+ (array_for_all (check_rec_call n lst) typarray)
+ &&
+ (array_for_all
+ (check_rec_call (n+nbfix) (map_lift_fst_n nbfix lst))
+ bodies)
else
let theBody = bodies.(i) in
let (gamma,strippedBody) =
@@ -594,29 +581,63 @@ let rec check_subterm_rec_meta env sigma vectn k def =
typarray) &&
(list_for_all_i (fun n -> check_rec_call n lst) n absTypes) &
(check_rec_call (n+nbOfAbst) newlst strippedBody))
-
-
- | (DOP2(_,a,b),l) ->
+
+ | IsCast (a,b) ->
(check_rec_call n lst a) &&
(check_rec_call n lst b) &&
(List.for_all (check_rec_call n lst) l)
- | (DOPN(_,la),l) ->
- (array_for_all (check_rec_call n lst) la) &&
- (List.for_all (check_rec_call n lst) l)
+ | IsLambda (_,a,b) ->
+ (check_rec_call n lst a) &&
+ (check_rec_call (n+1) (map_lift_fst lst) b) &&
+ (List.for_all (check_rec_call n lst) l)
+
+ | IsProd (_,a,b) ->
+ (check_rec_call n lst a) &&
+ (check_rec_call (n+1) (map_lift_fst lst) b) &&
+ (List.for_all (check_rec_call n lst) l)
- | (DOP0 (Meta _),l) -> true
+ | IsLetIn (_,a,b,c) ->
+ (check_rec_call n lst a) &&
+ (check_rec_call n lst b) &&
+ (check_rec_call (n+1) (map_lift_fst lst) c) &&
+ (List.for_all (check_rec_call n lst) l)
- | (DLAM(_,t),l) ->
- (check_rec_call (n+1) (map_lift_fst lst) t) &&
+ | IsMutInd (_,la) ->
+ (array_for_all (check_rec_call n lst) la) &&
(List.for_all (check_rec_call n lst) l)
- | (DLAMV(_,vt),l) ->
- (array_for_all (check_rec_call (n+1) (map_lift_fst lst)) vt) &&
+ | IsMutConstruct (_,la) ->
+ (array_for_all (check_rec_call n lst) la) &&
(List.for_all (check_rec_call n lst) l)
- | (_,l) -> List.for_all (check_rec_call n lst) l
- )
+ | IsConst (_,la) ->
+ (array_for_all (check_rec_call n lst) la) &&
+ (List.for_all (check_rec_call n lst) l)
+
+ | IsAppL (f,la) ->
+ (check_rec_call n lst f) &&
+ (List.for_all (check_rec_call n lst) la) &&
+ (List.for_all (check_rec_call n lst) l)
+
+ | IsCoFix (i,(typarray,funnames,bodies)) ->
+ let nbfix = Array.length bodies in
+ (array_for_all (check_rec_call n lst) typarray) &&
+ (List.for_all (check_rec_call n lst) l) &&
+ (array_for_all
+ (check_rec_call (n+nbfix) (map_lift_fst_n nbfix lst))
+ bodies)
+
+ | IsEvar (_,la) ->
+ (array_for_all (check_rec_call n lst) la) &&
+ (List.for_all (check_rec_call n lst) l)
+
+ | IsMeta _ -> true
+
+ | IsVar _ | IsSort _ -> List.for_all (check_rec_call n lst) l
+
+ | IsXtra _ | IsAbst _ -> List.for_all (check_rec_call n lst) l
+ )
in
check_rec_call 1 [] d)
@@ -633,25 +654,30 @@ let check_fix env sigma ((nvect,bodynum),(types,names,bodies)) =
or Array.length nvect <> nbfix
or Array.length types <> nbfix
or List.length names <> nbfix
- then error "Ill-formed fix term";
+ or bodynum < 0
+ or bodynum >= nbfix
+ then anomaly "Ill-formed fix term";
for i = 0 to nbfix - 1 do
try
let _ = check_subterm_rec_meta env sigma nvect nvect.(i) bodies.(i) in ()
- with UserError (s,str) ->
- error_ill_formed_rec_body CCI env str (List.rev names) i bodies
+ with FixGuardError err ->
+ error_ill_formed_rec_body CCI env err (List.rev names) i bodies
done
(* Co-fixpoints. *)
+exception CoFixGuardError of guard_error
+
let check_guard_rec_meta env sigma nbfix def deftype =
let rec codomain_is_coind c =
- match whd_betadeltaiota env sigma (strip_outer_cast c) with
- | DOP2(Prod,a,DLAM(_,b)) -> codomain_is_coind b
- | b ->
- (try find_mcoinductype env sigma b
- with
- | Induc -> error "The codomain is not a coinductive type"
-(* | _ -> error "Type of Cofix function not as expected") ??? *) )
+ let b = whd_betadeltaiota env sigma (strip_outer_cast c) in
+ match kind_of_term b with
+ | IsProd (_,a,b) -> codomain_is_coind b
+ | _ ->
+ try
+ find_mcoinductype env sigma b
+ with Induc ->
+ raise (CoFixGuardError (CodomainNotInductiveType b))
in
let (mind, _) = codomain_is_coind deftype in
let ((sp,tyi),_) = mind in
@@ -671,11 +697,11 @@ let check_guard_rec_meta env sigma nbfix def deftype =
if List.for_all (noccur_with_meta n nbfix) l then
true
else
- error "Nested recursive occurrences"
+ raise (CoFixGuardError NestedRecursiveOccurrences)
else
- error "Unguarded recursive call"
+ raise (CoFixGuardError (UnguardedRecursiveCall t))
else
- error "check_guard_rec_meta: ???"
+ error "check_guard_rec_meta: ???" (* ??? *)
| (DOPN (MutConstruct(_,i as cstr_sp),l), args) ->
let lra =vlra.(i-1) in
@@ -710,7 +736,8 @@ let check_guard_rec_meta env sigma nbfix def deftype =
| _::lrar ->
if (noccur_with_meta n nbfix t)
then (process_args_of_constr lr lrar)
- else error "Recursive call inside a non-recursive argument of constructor")
+ else raise (CoFixGuardError
+ (RecCallInNonRecArgOfConstructor t)))
in (process_args_of_constr realargs lra)
@@ -718,7 +745,7 @@ let check_guard_rec_meta env sigma nbfix def deftype =
if (noccur_with_meta n nbfix a) then
check_rec_call alreadygrd (n+1) vlra b
else
- error "Recursive call in the type of an abstraction"
+ raise (CoFixGuardError (RecCallInTypeOfAbstraction t))
| (DOPN(CoFix(j),vargs) as cofix,l) ->
if (List.for_all (noccur_with_meta n nbfix) l)
@@ -730,8 +757,9 @@ let check_guard_rec_meta env sigma nbfix def deftype =
&&
(List.for_all (check_rec_call alreadygrd (n+1) vlra) l)
else
- error "Recursive call in the type of a declaration"
- else error "Unguarded recursive call"
+ raise (CoFixGuardError (RecCallInTypeOfDef cofix))
+ else
+ raise (CoFixGuardError (UnguardedRecursiveCall cofix))
| (DOPN(MutCase _,_) as mc,l) ->
let (_,p,c,vrest) = destCase mc in
@@ -740,13 +768,13 @@ let check_guard_rec_meta env sigma nbfix def deftype =
if (List.for_all (noccur_with_meta n nbfix) l) then
(array_for_all (check_rec_call alreadygrd n vlra) vrest)
else
- error "Recursive call in the argument of a function defined by cases"
+ raise (CoFixGuardError (RecCallInCaseFun mc))
else
- error "Recursive call in the argument of a case expression"
+ raise (CoFixGuardError (RecCallInCaseArg mc))
else
- error "Recursive call in the type of a Case expression"
+ raise (CoFixGuardError (RecCallInCasePred mc))
- | _ -> error "Definition not in guarded form"
+ | _ -> raise (CoFixGuardError NotGuardedForm)
in
check_rec_call false 1 vlra def
@@ -758,11 +786,9 @@ let check_cofix env sigma (bodynum,(types,names,bodies)) =
let nbfix = Array.length bodies in
for i = 0 to nbfix-1 do
try
- let _ =
- check_guard_rec_meta env sigma nbfix bodies.(i) types.(i) in
- ()
- with UserError (s,str) ->
- error_ill_formed_rec_body CCI env str (List.rev names) i bodies
+ let _ = check_guard_rec_meta env sigma nbfix bodies.(i) types.(i) in ()
+ with CoFixGuardError err ->
+ error_ill_formed_rec_body CCI env err (List.rev names) i bodies
done
(*
let check_cofix env sigma f =
@@ -814,22 +840,28 @@ let type_fixpoint env sigma lna lar vdefj =
syntaxic conditions *)
let control_only_guard env sigma =
- let rec control_rec = function
- | Rel(p) -> ()
- | VAR _ -> ()
- | DOP0(_) -> ()
- | DOPN(CoFix(_),cl) as cofix ->
- check_cofix env sigma (destCoFix cofix);
- Array.iter control_rec cl
- | DOPN(Fix(_),cl) as fix ->
- check_fix env sigma (destFix fix);
- Array.iter control_rec cl
- | DOPN(_,cl) -> Array.iter control_rec cl
- | DOPL(_,cl) -> List.iter control_rec cl
- | DOP1(_,c) -> control_rec c
- | DOP2(_,c1,c2) -> control_rec c1; control_rec c2
- | DLAM(_,c) -> control_rec c
- | DLAMV(_,v) -> Array.iter control_rec v
+ let rec control_rec c = match kind_of_term c with
+ | IsRel _ | IsVar _ -> ()
+ | IsSort _ | IsMeta _ | IsXtra _ -> ()
+ | IsCoFix (_,(tys,_,bds) as cofix) ->
+ check_cofix env sigma cofix;
+ Array.iter control_rec tys;
+ Array.iter control_rec bds;
+ | IsFix (_,(tys,_,bds) as fix) ->
+ check_fix env sigma fix;
+ Array.iter control_rec tys;
+ Array.iter control_rec bds;
+ | IsMutCase(_,p,c,b) ->control_rec p;control_rec c;Array.iter control_rec b
+ | IsMutInd (_,cl) -> Array.iter control_rec cl
+ | IsMutConstruct (_,cl) -> Array.iter control_rec cl
+ | IsConst (_,cl) -> Array.iter control_rec cl
+ | IsEvar (_,cl) -> Array.iter control_rec cl
+ | IsAbst (_,cl) -> Array.iter control_rec cl
+ | IsAppL (_,cl) -> List.iter control_rec cl
+ | IsCast (c1,c2) -> control_rec c1; control_rec c2
+ | IsProd (_,c1,c2) -> control_rec c1; control_rec c2
+ | IsLambda (_,c1,c2) -> control_rec c1; control_rec c2
+ | IsLetIn (_,c1,c2,c3) -> control_rec c1; control_rec c2; control_rec c3
in
control_rec
generated by cgit v1.2.3 (git 2.39.1) at 2024-06-06 23:01:15 +0000