aboutsummaryrefslogtreecommitdiffhomepage
diff options
context:
space:
mode:
Diffstat
-rw-r--r--kernel/abstraction.ml9
-rw-r--r--kernel/generic.ml250
-rw-r--r--kernel/generic.mli112
-rw-r--r--kernel/instantiate.ml2
-rw-r--r--kernel/reduction.ml21
-rw-r--r--kernel/term.ml139
-rw-r--r--kernel/term.mli50
-rw-r--r--kernel/typeops.ml89
-rw-r--r--kernel/typeops.mli4
-rw-r--r--library/indrec.ml10
-rw-r--r--parsing/termast.ml6
-rw-r--r--pretyping/cases.ml28
-rw-r--r--pretyping/detyping.ml6
-rw-r--r--pretyping/evarutil.ml2
-rw-r--r--pretyping/pretyping.ml19
-rw-r--r--pretyping/retyping.ml4
-rw-r--r--pretyping/tacred.ml15
-rw-r--r--pretyping/typing.ml18
-rw-r--r--proofs/clenv.ml4
-rw-r--r--proofs/evar_refiner.ml27
-rw-r--r--proofs/logic.ml53
-rw-r--r--tactics/equality.ml5
-rw-r--r--tactics/wcclausenv.ml4
-rw-r--r--toplevel/command.ml89
-rw-r--r--toplevel/discharge.ml19
-rw-r--r--toplevel/record.ml3
26 files changed, 443 insertions, 545 deletions
diff --git a/kernel/abstraction.ml b/kernel/abstraction.ml
index e0b86dbf2..9df751b46 100644
--- a/kernel/abstraction.ml
+++ b/kernel/abstraction.ml
@@ -11,6 +11,15 @@ type abstraction_body = {
abs_arity : int array;
abs_rhs : constr }
+let rec count_dlam = function
+ | DLAM (_,c) -> 1 + (count_dlam c)
+ | _ -> 0
+
+let sAPP c n =
+ match c with
+ | DLAM(na,m) -> subst1 n m
+ | _ -> invalid_arg "SAPP"
+
let contract_abstraction ab args =
if array_for_all2 (fun c i -> (count_dlam c) = i) args ab.abs_arity then
Sosub.soexecute (Array.fold_left sAPP ab.abs_rhs args)
diff --git a/kernel/generic.ml b/kernel/generic.ml
index 2a8af630d..70acca45d 100644
--- a/kernel/generic.ml
+++ b/kernel/generic.ml
@@ -23,9 +23,6 @@ type 'oper term =
exception FreeVar
exception Occur
-let isRel = function Rel _ -> true | _ -> false
-let isVAR = function VAR _ -> true | _ -> false
-
(* returns the list of free debruijn indices in a term *)
let free_rels m =
@@ -59,7 +56,7 @@ let closedn =
in
closed_rec
-(* (closed M) is true iff M is a (deBruijn) closed term *)
+(* [closed0 M] is true iff [M] is a (deBruijn) closed term *)
let closed0 term =
try closedn 0 term; true with FreeVar -> false
@@ -80,10 +77,10 @@ let noccurn n term =
in
try occur_rec n term; true with Occur -> false
-(* (noccur_bet n m M) returns true iff (Rel p) does NOT occur in term M
+(* (noccur_between n m M) returns true iff (Rel p) does NOT occur in term M
for n <= p < n+m *)
-let noccur_bet n m term =
+let noccur_between n m term =
let rec occur_rec n = function
| Rel(p) -> if n<=p && p<n+m then raise Occur
| VAR _ -> ()
@@ -146,7 +143,8 @@ let liftn k n =
| el -> exliftn el
let lift k = liftn k 1
-let lift1 c = exliftn (ELSHFT(ELID,1)) c
+
+let pop t = lift (-1) t
let lift_context n l =
let k = List.length l in
@@ -242,85 +240,11 @@ let substn_many lamv n =
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]
-let pop t = lift (-1) t
-
-
-(* 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
- | _ -> false
- in
- occur_rec
-
-let occur_oper0 s =
- let rec occur_rec = function
- | DOPN(_,cl) -> (array_exists occur_rec cl)
- | DOPL(_,cl) -> (List.exists occur_rec cl)
- | DOP0 oper -> s=oper
- | 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
- | _ -> false
- in
- occur_rec
-
-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
- | _ -> false
- in
- occur_rec
-
-let occur_oper 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
- | DOP0 oper -> s=oper
- | DOP1(oper,c) -> s=oper or occur_rec c
- | DOP2(oper,c1,c2) -> s=oper or (occur_rec c1) or (occur_rec c2)
- | DLAM(_,c) -> occur_rec c
- | DLAMV(_,v) -> array_exists occur_rec v
- | _ -> false
- in
- occur_rec
-
-let process_opers_of_term p f l constr =
- let rec filtrec acc = function
- | DOP0 oper -> if p oper then ((f oper)::acc) else acc
- | VAR _ -> acc
- | DOP1(oper,c) -> let newacc = filtrec acc c in
- if p oper then ((f oper)::newacc) else newacc
- | DOP2(oper,c1,c2) -> let newacc = filtrec (filtrec acc c1) c2 in
- if p oper then ((f oper)::newacc) else newacc
- | DOPN(oper,cl) -> let newacc = (Array.fold_left filtrec acc cl) in
- if p oper then ((f oper)::newacc) else newacc
- | DOPL(oper,cl) -> let newacc = (List.fold_left filtrec acc cl) in
- if p oper then ((f oper)::newacc) else newacc
- | DLAM(_,c) -> filtrec acc c
- | DLAMV(_,v) -> Array.fold_left filtrec acc v
- | _ -> acc
- in
- filtrec l constr
(* Returns the list of global variables in a term *)
@@ -352,42 +276,6 @@ let global_vars_set constr =
in
filtrec Idset.empty constr
-(* alpha equality for generic terms : checks first if M and M' are equal,
- otherwise checks equality forgetting the name annotation of DLAM and DLAMV*)
-
-let rec eq_term m m' =
- (m == m')
- or (m = m')
- or (match (m,m') with
- | (DOP1(oper1,c1),DOP1(oper2,c2)) ->
- oper1 = oper2 & eq_term c1 c2
- | (DOP2(oper1,c1,t1),DOP2(oper2,c2,t2)) ->
- oper1 = oper2 & eq_term c1 c2 & eq_term t1 t2
- | (DOPN(oper1,cl1),DOPN(oper2,cl2)) ->
- oper1 = oper2 & array_for_all2 eq_term cl1 cl2
- | (DOPL(oper1,cl1),DOPL(oper2,cl2)) ->
- oper1 = oper2 & List.for_all2 eq_term cl1 cl2
- | (DLAM(_,c1),DLAM(_,c2)) -> eq_term c1 c2
- | (DLAMV(_,cl1),DLAMV(_,cl2)) -> array_for_all2 eq_term 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 = function t ->
- (eq_term 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 (lift1 m) c
- | DLAMV(_,v) -> array_exists (deprec (lift1 m)) v
- | _ -> false)
- in
- deprec
-
(* (thin_val sigma) removes identity substitutions from sigma *)
let rec thin_val = function
@@ -398,6 +286,8 @@ let rec thin_val = function
(* (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) ->
@@ -414,54 +304,22 @@ let replace_vars var_alist =
in
if var_alist = [] then (function x -> x) else substrec 0
-let subst_varn str n = replace_vars [(str,make_substituend (Rel n))]
+let subst_varn str n = replace_vars [(str, (Rel n))]
(* (subst_var str t) substitute (VAR str) by (Rel 1) in t *)
let subst_var str = subst_varn str 1
+(* [Rel (n+m);...;Rel(n+1)] *)
-(* renames different ocurrences of (VAR id) in t with a fresh identifier
- wrt. acc *)
-let rename_diff_occ id acc t =
- let rec rename_occ acc = function
- | (VAR(x) as c) ->
- if x <> id then
- acc,c
- else
- let nid = next_ident_away id acc in (nid::acc), (VAR nid)
- | DOPN(oper,cl) ->
- let nacc,ncl = vrename_occ acc cl in nacc,DOPN(oper, ncl)
- | DOPL(oper,cl) ->
- let nacc,ncl = lrename_occ acc cl in nacc, DOPL(oper,ncl)
- | DOP1(oper,c) ->
- let nacc,nc = rename_occ acc c in nacc, DOP1(oper,nc)
- | DOP2(oper,c1,c2) ->
- let nacc,nc1 = rename_occ acc c1 in
- let nacc2,nc2 = rename_occ nacc c2 in
- nacc2, DOP2(oper,nc1,nc2)
- | DLAM(na,c) ->
- let nacc,nc = rename_occ acc c in (nacc, DLAM(na,nc))
- | DLAMV(na,v) ->
- let nacc,nv = vrename_occ acc v in (nacc, DLAMV(na, nv))
- | x -> acc,x
- and lrename_occ acc = function
- | [] -> acc,[]
- | (t::lt) ->
- let nacc,nt = rename_occ acc t in
- let nacc2,nlt = lrename_occ nacc lt
- in nacc2,(nt::nlt)
- and vrename_occ acc v =
- let nacc,nl = lrename_occ acc (Array.to_list v)
- in nacc, Array.of_list nl
- in
- rename_occ acc t
+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
-let sAPP c n =
- match c with
- | DLAM(na,m) -> subst1 n m
- | _ -> invalid_arg "SAPP"
-
+(* Obsolète
let sAPPV c n =
match c with
| DLAMV(na,mV) -> Array.map (subst1 n) mV
@@ -480,22 +338,6 @@ let sAPPList constr cl =
in
srec [] (constr,cl)
-let sAPPVList constr cl =
- let rec srec stack = function
- | (DLAM(_,c), (h::t)) -> srec (h::stack) (c,t)
- | (DLAMV(_,c), [h]) -> Array.map (substl (h::stack)) c
- | (_, _) -> failwith "SAPPVList"
- in
- srec [] (constr,cl)
-
-let sAPPViList i constr cl=
- let rec srec stack = function
- | (DLAM(_,c), (h::t)) -> srec (h::stack) (c,t)
- | (DLAMV(_,c), [h]) -> substl (h::stack) c.(i)
- | (_, _) -> failwith "SAPPViList"
- in
- srec [] (constr,cl)
-
let under_dlams f =
let rec apprec = function
| DLAMV(na,c) -> DLAMV(na,Array.map f c)
@@ -504,19 +346,11 @@ let under_dlams f =
in
apprec
-
let put_DLAMSV lna lc =
match lna with
| [] -> anomaly "put_DLAM"
| na::lrest -> List.fold_left (fun c na -> DLAM(na,c)) (DLAMV(na,lc)) lrest
-let put_DLAMSV_subst lid lc =
- match lid with
- | [] -> anomaly "put_DLAM"
- | id::lrest ->
- List.fold_left (fun c id' -> DLAM(Name id',subst_var id' c))
- (DLAMV(Name id,Array.map (subst_var id) lc)) lrest
-
let rec decomp_DLAMV n = function
| DLAM(_,lc) -> decomp_DLAMV (n-1) lc
| DLAMV(_,lc) -> if n = 1 then lc else error "decomp_DLAMV 0"
@@ -537,50 +371,4 @@ let decomp_all_DLAMV_name constr =
| _ -> assert false
in
decomprec [] 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
-
-let rec count_dlam = function
- | DLAM (_,c) -> 1 + (count_dlam c)
- | _ -> 0
-
-(* Hash-consing *)
-let comp_term t1 t2 =
- match (t1,t2) with
- | (DOP0 o1, DOP0 o2) -> o1==o2
- | (DOP1(o1,t1), DOP1(o2,t2)) -> o1==o2 & t1==t2
- | (DOP2(o1,t1,u1), DOP2(o2,t2,u2)) -> o1==o2 & t1==t2 & u1==u2
- | (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
- | (Rel i, Rel j) -> i=j
- | (VAR x, VAR y) -> x==y
- | _ -> false
-
-let hash_term (sh_rec,(sh_op,sh_na,sh_id)) t =
- match t with
- | DOP0 o -> DOP0 (sh_op o)
- | 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)
- | Rel i -> t
- | VAR x -> VAR (sh_id x)
+*)
diff --git a/kernel/generic.mli b/kernel/generic.mli
index 5f632a94a..4f2afa9a0 100644
--- a/kernel/generic.mli
+++ b/kernel/generic.mli
@@ -23,84 +23,91 @@ type 'oper term =
| VAR of identifier
| Rel of int
-val isRel : 'a term -> bool
-val isVAR : 'a term -> bool
val free_rels : 'a term -> Intset.t
-exception FreeVar
-exception Occur
-
-val closedn : int -> 'a term -> unit
+(* [closed0 M] is true iff [M] is a (deBruijn) closed term *)
val closed0 : 'a term -> bool
-val noccurn : int -> 'a term -> bool
-val noccur_bet : int -> int -> 'a term -> bool
-(*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. *)
+(* [noccurn n M] returns true iff [Rel n] does NOT occur in term [M] *)
+val noccurn : int -> 'a term -> bool
-type lift_spec =
- | ELID
- | ELSHFT of lift_spec * int
- | ELLFT of int * lift_spec
+(* [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 -> 'a term -> bool
-val el_shft : int -> lift_spec -> lift_spec
-val el_lift : lift_spec -> lift_spec
-val el_liftn : int -> lift_spec -> lift_spec
-val reloc_rel: int -> lift_spec -> int
-val exliftn : lift_spec -> 'a term -> 'a term
+(* [liftn n k c] lifts by [n] indexes above [k] in [c] *)
val liftn : int -> int -> 'a term -> 'a term
+
+(* [lift n c] lifts by [n] the positive indexes in [c] *)
val lift : int -> 'a term -> 'a term
+
+(* [pop c] lifts by -1 the positive indexes in [c] *)
val pop : 'a term -> 'a term
(* [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 * 'a term) list -> (name * 'a term) list
-(*s Explicit substitutions of type ['a]. [ESID] = identity.
+val substnl : 'a term list -> int -> 'a term -> 'a term
+val substl : 'a term list -> 'a term -> 'a term
+val subst1 : 'a term -> 'a term -> 'a term
+
+(* [global_vars c] returns the list of [id]'s occurring as [VAR id] in [c] *)
+val global_vars : 'a term -> identifier list
+
+val global_vars_set : 'a term -> Idset.t
+val subst_var : identifier -> 'a term -> 'a term
+val replace_vars : (identifier * 'a term) list -> 'a term -> 'a term
+
+(* [rel_list n m] and [rel_vect n m] compute [[Rel (n+m);...;Rel(n+1)]] *)
+val rel_vect : int -> int -> 'a term array
+val rel_list : int -> int -> 'a term 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_lift : 'a subs -> 'a subs
val subs_shft : int * 'a subs -> 'a subs
-val exp_rel : int -> int -> 'a subs -> (int * 'a, int) union
val expand_rel : int -> 'a subs -> (int * 'a, int) union
+(*
+val exp_rel : int -> int -> 'a subs -> (int * 'a, int) union
+*)
+(*i*)
-type info = Closed | Open | Unknown
-type 'a substituend = { mutable sinfo : info; sit : 'a }
+(*i Pour Closure *)
+(*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
+(*
+val exliftn : lift_spec -> 'a term -> 'a term
+val el_liftn : int -> lift_spec -> lift_spec
+*)
+(*i*)
-val lift_substituend : int -> 'a term substituend -> 'a term
-val make_substituend : 'a term -> 'a term substituend
-val substn_many : 'a term substituend array -> int -> 'a term -> 'a term
-val substl : 'a term list -> 'a term -> 'a term
-val subst1 : 'a term -> 'a term -> 'a term
-val occur_opern : 'a -> 'a term -> bool
-val occur_oper0 : 'a -> 'a term -> bool
-val occur_var : identifier -> 'a term -> bool
-val occur_oper : 'a -> 'a term -> bool
-val process_opers_of_term :
- ('a -> bool) -> ('a -> 'b) -> 'b list -> 'a term -> 'b list
-val dependent : 'a term -> 'a term -> bool
+(*i À virer...
+exception FreeVar
+val closedn : int -> 'a term -> unit
+
+exception Occur
+type info = Closed | Open | Unknown
val global_varsl : identifier list -> 'a term -> identifier list
-val global_vars : 'a term -> identifier list
-val global_vars_set : 'a term -> Idset.t
-val subst_var : identifier -> 'a term -> 'a term
val subst_varn : identifier -> int -> 'a term -> 'a term
-val replace_vars :
- (identifier * 'a term substituend) list -> 'a term -> 'a term
-
-val rename_diff_occ :
- identifier -> identifier list ->'a term -> identifier list * 'a term
-
val sAPP : 'a term -> 'a term -> 'a term
val sAPPV : 'a term -> 'a term -> 'a term array
val sAPPVi : int -> 'a term -> 'a term -> 'a term
@@ -109,24 +116,17 @@ val sAPPList : 'a term -> 'a term list -> 'a term
val sAPPVList : 'a term -> 'a term list-> 'a term array
val sAPPViList : int -> 'a term -> 'a term list -> 'a term
val under_dlams : ('a term -> 'a term) -> 'a term -> 'a term
-val eq_term : 'a term -> 'a term -> bool
-
val put_DLAMSV : name list -> 'a term array -> 'a term
val decomp_DLAMV : int -> 'a term -> 'a term array
val decomp_DLAMV_name : int -> 'a term -> name list * 'a term array
val decomp_all_DLAMV_name : 'a term -> name list * 'a term array
val put_DLAMSV_subst : identifier list -> 'a term array -> 'a term
-
-(* [rel_list n m] and [rel_vect n m] compute [[Rel (n+m);...;Rel(n+1)]] *)
-val rel_vect : int -> int -> 'a term array
-val rel_list : int -> int -> 'a term list
-
val count_dlam : 'a term -> int
-(*s For hash-consing. *)
-
+(*s For hash-consing. (déplacé dans term) *)
val hash_term :
('a term -> 'a term)
* (('a -> 'a) * (name -> name) * (identifier -> identifier))
-> 'a term -> 'a term
val comp_term : 'a term -> 'a term -> bool
+i*)
diff --git a/kernel/instantiate.ml b/kernel/instantiate.ml
index 7a929b9fa..5ec0e01b0 100644
--- a/kernel/instantiate.ml
+++ b/kernel/instantiate.ml
@@ -22,7 +22,7 @@ let instantiate_constr ids c args =
if is_id_inst ids args then
c
else
- replace_vars (List.combine ids (List.map make_substituend args)) c
+ replace_vars (List.combine ids args) c
let instantiate_type ids tty args =
typed_app (fun c -> instantiate_constr ids c args) tty
diff --git a/kernel/reduction.ml b/kernel/reduction.ml
index 4dfeca882..85a335ee8 100644
--- a/kernel/reduction.ml
+++ b/kernel/reduction.ml
@@ -486,12 +486,19 @@ let reducible_mind_case = function
| DOPN(MutConstruct _,_) | DOPN(CoFix _,_) -> true
| _ -> false
+(*
let contract_cofix = function
| DOPN(CoFix(bodynum),bodyvect) ->
let nbodies = (Array.length bodyvect) -1 in
let make_Fi j = DOPN(CoFix(j),bodyvect) in
sAPPViList bodynum (array_last bodyvect) (list_tabulate make_Fi nbodies)
| _ -> assert false
+*)
+
+let contract_cofix (bodynum,(types,names,bodies as typedbodies)) =
+ let nbodies = Array.length bodies in
+ let make_Fi j = mkCoFix (nbodies-j-1,typedbodies) in
+ substl (list_tabulate make_Fi nbodies) bodies.(bodynum)
let reduce_mind_case mia =
match mia.mconstr with
@@ -500,19 +507,25 @@ let reduce_mind_case mia =
let real_cargs = list_lastn ncargs mia.mcargs in
applist (mia.mlf.(i-1),real_cargs)
| DOPN(CoFix _,_) as cofix ->
- let cofix_def = contract_cofix cofix in
+ let cofix_def = contract_cofix (destCoFix cofix) in
mkMutCaseA mia.mci mia.mP (applist(cofix_def,mia.mcargs)) mia.mlf
| _ -> assert false
(* contracts fix==FIX[nl;i](A1...Ak;[F1...Fk]{B1....Bk}) to produce
Bi[Fj --> FIX[nl;j](A1...Ak;[F1...Fk]{B1...Bk})] *)
+(*
let contract_fix = function
| DOPN(Fix(recindices,bodynum),bodyvect) ->
let nbodies = Array.length recindices in
let make_Fi j = DOPN(Fix(recindices,j),bodyvect) in
sAPPViList bodynum (array_last bodyvect) (list_tabulate make_Fi nbodies)
| _ -> assert false
+*)
+let contract_fix ((recindices,bodynum),(types,names,bodies as typedbodies)) =
+ let nbodies = Array.length recindices in
+ let make_Fi j = mkFix ((recindices,nbodies-j-1),typedbodies) in
+ substl (list_tabulate make_Fi nbodies) bodies.(bodynum)
let fix_recarg fix stack =
match fix with
@@ -537,7 +550,7 @@ let reduce_fix whfun fix stack =
let stack' = list_assign stack recargnum (applist recarg') in
(match recarg'hd with
| DOPN(MutConstruct _,_) ->
- (true,(contract_fix fix,stack'))
+ (true,(contract_fix (destFix fix),stack'))
| _ -> (false,(fix,stack'))))
| _ -> assert false
@@ -981,7 +994,7 @@ let instance s c =
let hnf_prod_app env sigma t n =
match whd_betadeltaiota env sigma t with
- | DOP2(Prod,_,b) -> sAPP b n
+ | DOP2(Prod,_,DLAM(_,b)) -> subst1 n b
| _ -> anomaly "hnf_prod_app: Need a product"
let hnf_prod_appvect env sigma t nl =
@@ -992,7 +1005,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,_,b) -> sAPP b n
+ | DOP2(Lambda,_,DLAM(_,b)) -> subst1 n b
| _ -> anomaly "hnf_lam_app: Need an abstraction"
let hnf_lam_appvect env sigma t nl =
diff --git a/kernel/term.ml b/kernel/term.ml
index 3a58c9266..6b8e094b9 100644
--- a/kernel/term.ml
+++ b/kernel/term.ml
@@ -153,7 +153,7 @@ let mkCast t1 t2 =
(* Constructs the product (x:t1)t2 *)
let mkProd x t1 t2 = (DOP2 (Prod,t1,(DLAM (x,t2))))
-(* non-dependant product t1 -> t2 *)
+(* non-dependent product t1 -> t2 *)
let mkArrow t1 t2 = mkProd Anonymous t1 t2
(* named product *)
@@ -215,15 +215,14 @@ let mkMutCaseA ci p c ac =
(* Here, we assume the body already constructed *)
let mkFixDlam recindxs i jtypsarray body =
- let typsarray = Array.map incast_type jtypsarray in
+ let typsarray = (*Array.map incast_type*) jtypsarray in
DOPN (Fix (recindxs,i),Array.append typsarray body)
-let mkFix recindxs i jtypsarray funnames bodies =
- let rec wholebody l =
- match l with
- | [h] -> (DLAMV (h,bodies))
- | (x::l) -> (DLAM (x, wholebody l))
- | [] -> anomaly "in Term.mkFix : empty list of funnames"
+let mkFix ((recindxs, i), (jtypsarray, funnames, bodies)) =
+ let rec wholebody = function
+ | [h] -> (DLAMV (h,bodies))
+ | (x::l) -> (DLAM (x, wholebody l))
+ | [] -> anomaly "in Term.mkFix : empty list of funnames"
in
mkFixDlam recindxs i jtypsarray [|(wholebody funnames)|]
@@ -244,10 +243,10 @@ let mkFix recindxs i jtypsarray funnames bodies =
*)
(* Here, we assume the body already constructed *)
let mkCoFixDlam i jtypsarray body =
- let typsarray = Array.map incast_type jtypsarray in
+ let typsarray = (*Array.map incast_type*) jtypsarray in
DOPN ((CoFix i),(Array.append typsarray body))
-let mkCoFix i jtypsarray funnames bodies =
+let mkCoFix (i, (jtypsarray, funnames, bodies)) =
let rec wholebody l =
match l with
| [h] -> (DLAMV (h,bodies))
@@ -387,6 +386,12 @@ let rec strip_all_casts t =
| VAR _ as t -> t
| Rel _ as t -> t
+(* Tests if a de Bruijn index *)
+let isRel = function Rel _ -> true | _ -> false
+
+(* Tests if a variable *)
+let isVar = function VAR _ -> true | _ -> false
+
(* Destructs the product (x:t1)t2 *)
let destProd = function
| DOP2 (Prod, t1, (DLAM (x,t2))) -> (x,t1,t2)
@@ -525,13 +530,13 @@ let destGralFix a =
let destFix = function
| DOPN (Fix (recindxs,i),a) ->
let (types,funnames,bodies) = destGralFix a in
- (recindxs,i,Array.map out_fixcast types,funnames,bodies)
+ ((recindxs,i),((*Array.map out_fixcast *) types,funnames,bodies))
| _ -> invalid_arg "destFix"
let destCoFix = function
| DOPN ((CoFix i),a) ->
let (types,funnames,bodies) = destGralFix a in
- (i,Array.map out_fixcast types,funnames,bodies)
+ (i,((*Array.map out_fixcast *) types,funnames,bodies))
| _ -> invalid_arg "destCoFix"
(* Provisoire, le temps de maitriser les cast *)
@@ -551,7 +556,7 @@ let destUntypedCoFix = function
type binder_kind = BProd | BLambda
-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
@@ -565,6 +570,8 @@ type existential = int * constr array
type constant = section_path * constr array
type constructor = constructor_path * constr array
type inductive = inductive_path * constr array
+type fixpoint = (int array * int) * (constr array * name list * constr array)
+type cofixpoint = int * (constr array * name list * constr array)
(******************)
(* Term analysis *)
@@ -586,9 +593,8 @@ type kindOfTerm =
| IsMutInd of inductive
| IsMutConstruct of constructor
| IsMutCase of case_info * constr * constr * constr array
- | IsFix of int array * int * constr array * name list * constr array
- | IsCoFix of int * constr array * name list * constr array
-
+ | IsFix of fixpoint
+ | IsCoFix of cofixpoint
(* Discriminates which kind of term is it.
@@ -616,11 +622,11 @@ let kind_of_term c =
| DOPN (MutCase ci,v) ->
IsMutCase (ci,v.(0),v.(1),Array.sub v 2 (Array.length v - 2))
| DOPN ((Fix (recindxs,i),a)) ->
- let (types,funnames,bodies) = destGralFix a in
- IsFix (recindxs,i,types,funnames,bodies)
+ let typedbodies = destGralFix a in
+ IsFix ((recindxs,i),typedbodies)
| DOPN ((CoFix i),a) ->
- let (types,funnames,bodies) = destGralFix a in
- IsCoFix (i,types,funnames,bodies)
+ let typedbodies = destGralFix a in
+ IsCoFix (i,typedbodies)
| _ -> errorlabstrm "Term.kind_of_term" [< 'sTR "ill-formed constr" >]
(***************************)
@@ -711,7 +717,7 @@ let rec to_prod n lam =
let prod_app t n =
match strip_outer_cast t with
- | DOP2(Prod,_,b) -> sAPP b n
+ | DOP2(Prod,_,DLAM(na,b)) -> subst1 n b
| _ ->
errorlabstrm "prod_app"
[< 'sTR"Needed a product, but didn't find one" ; 'fNL >]
@@ -969,7 +975,7 @@ let rec decomp_app c =
| c -> (c,[])
(* strips head casts and flattens head applications *)
-let strip_head_cast = function
+let rec strip_head_cast = function
| DOPN(AppL,cl) ->
let rec collapse_rec = function
| (DOPN(AppL,cl),l2) -> collapse_rec(array_hd cl, array_app_tl cl l2)
@@ -978,11 +984,41 @@ let strip_head_cast = function
| (f,l) -> let v = Array.of_list (f::l) in DOPN(AppL,v)
in
collapse_rec(array_hd cl, array_app_tl cl [])
+ | DOP2(Cast,c,t) -> strip_head_cast c
| c -> c
+(* 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
+ | _ -> false
+ in
+ occur_rec
+
(* (occur_const (s:section_path) c) -> true if constant s occurs in c,
* false otherwise *)
let occur_const s = occur_opern (Const s)
+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
+ | _ -> false
+ in
+ occur_rec
(* let sigma be a finite function mapping sections paths to
constants represented as (identifier list * constr) option.
@@ -1010,9 +1046,7 @@ let replace_consts const_alist =
if List.length hyps <> Array.length cl then
anomaly "found a constant with a bad number of args"
else
- replace_vars
- (List.combine hyps
- (array_map_to_list make_substituend cl')) body
+ replace_vars (List.combine hyps (Array.to_list cl')) body
| None -> anomaly ("a constant which was never"^
" supposed to appear has just appeared")
with Not_found -> DOPN(Const sp,cl'))
@@ -1048,10 +1082,9 @@ let whd_castapp x = applist(whd_castapp_stack x [])
(* alpha conversion : ignore print names and casts *)
let rec eq_constr_rec m n =
+ (m == n) or
(m = n) or
match (strip_head_cast m,strip_head_cast n) with
- | (DOP2(Cast,c1,_),c2) -> eq_constr_rec c1 c2
- | (c1,DOP2(Cast,c2,_)) -> eq_constr_rec c1 c2
| (Rel p1,Rel p2) -> p1=p2
| (DOPN(oper1,cl1),DOPN(oper2,cl2)) ->
oper1=oper2 & array_for_all2 eq_constr_rec cl1 cl2
@@ -1067,10 +1100,9 @@ let rec eq_constr_rec m n =
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
- | (DOP2(Cast,c1,_),c2) -> eq_constr_rec c1 c2
- | (c1,DOP2(Cast,c2,_)) -> eq_constr_rec c1 c2
| (Rel p1,Rel p2) -> p1=p2
| (DOPN(oper1,cl1),DOPN(oper2,cl2)) ->
oper1=oper2 & array_for_all2 eq_constr_rec cl1 cl2
@@ -1083,6 +1115,24 @@ let rec eq_constr_with_meta_rec m n=
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)
+ in
+ deprec
+
(* On reduit une serie d'eta-redex de tete ou rien du tout *)
(* [x1:c1;...;xn:cn]@(f;a1...an;x1;...;xn) --> @(f;a1...an) *)
(* Remplace 2 versions précédentes buggées *)
@@ -1330,6 +1380,37 @@ let occur_existential =
(* hash-consing functions *)
(***************************)
+let comp_term t1 t2 =
+ match (t1,t2) with
+ | (DOP0 o1, DOP0 o2) -> o1==o2
+ | (DOP1(o1,t1), DOP1(o2,t2)) -> o1==o2 & t1==t2
+ | (DOP2(o1,t1,u1), DOP2(o2,t2,u2)) -> o1==o2 & t1==t2 & u1==u2
+ | (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
+ | (Rel i, Rel j) -> i=j
+ | (VAR x, VAR y) -> x==y
+ | _ -> false
+
+let hash_term (sh_rec,(sh_op,sh_na,sh_id)) t =
+ match t with
+ | DOP0 o -> DOP0 (sh_op o)
+ | 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)
+ | Rel i -> t
+ | VAR x -> VAR (sh_id x)
+
module Hsorts =
Hashcons.Make(
struct
diff --git a/kernel/term.mli b/kernel/term.mli
index 7320b8be8..cc5a8954d 100644
--- a/kernel/term.mli
+++ b/kernel/term.mli
@@ -76,7 +76,7 @@ val outcast_type : constr -> typed_type
(**********************************************************************)
type binder_kind = BProd | BLambda
-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
@@ -96,6 +96,9 @@ type existential = int * constr array
type constant = section_path * constr array
type constructor = constructor_path * constr array
type inductive = inductive_path * constr array
+type fixpoint = (int array * int) * (constr array * name list * constr array)
+type cofixpoint = int * (constr array * name list * constr array)
+
type kindOfTerm =
| IsRel of int
@@ -113,8 +116,8 @@ type kindOfTerm =
| IsMutInd of inductive
| IsMutConstruct of constructor
| IsMutCase of case_info * constr * constr * constr array
- | IsFix of int array * int * constr array * name list * constr array
- | IsCoFix of int * constr array * name list * constr array
+ | IsFix of fixpoint
+ | IsCoFix of cofixpoint
(* Discriminates which kind of term is it.
Note that there is no cases for [DLAM] and [DLAMV]. These terms do not
@@ -212,7 +215,7 @@ val mkMutCaseA : case_info -> constr -> constr -> constr array -> constr
[typarray = [|t1,...tn|]]
[funnames = [f1,.....fn]]
[bodies = [b1,.....bn]]
- then [ mkFix recindxs i typarray funnames bodies]
+ then [ mkFix ((recindxs,i),typarray, funnames, bodies) ]
constructs the $i$th function of the block
[Fixpoint f1 [ctx1] = b1
@@ -222,17 +225,15 @@ val mkMutCaseA : case_info -> constr -> constr -> constr array -> constr
\noindent where the lenght of the $j$th context is $ij$.
*)
-val mkFix : int array -> int -> typed_type array -> name list
- -> constr array -> constr
+val mkFix : fixpoint -> constr
(* Similarly, but we assume the body already constructed *)
-val mkFixDlam : int array -> int -> typed_type array
- -> constr array -> constr
+val mkFixDlam : int array -> int -> constr array -> constr array -> constr
(* If [typarray = [|t1,...tn|]]
[funnames = [f1,.....fn]]
[bodies = [b1,.....bn]] \par\noindent
- then [mkCoFix i typsarray funnames bodies]
+ then [mkCoFix (i, (typsarray, funnames, bodies))]
constructs the ith function of the block
[CoFixpoint f1 = b1
@@ -240,11 +241,10 @@ val mkFixDlam : int array -> int -> typed_type array
...
with fn = bn.]
*)
-val mkCoFix : int -> typed_type array -> name list
- -> constr array -> constr
+val mkCoFix : cofixpoint -> constr
(* Similarly, but we assume the body already constructed *)
-val mkCoFixDlam : int -> typed_type array -> constr array -> constr
+val mkCoFixDlam : int -> constr array -> constr array -> constr
(*s Term destructors.
@@ -292,6 +292,12 @@ val strip_outer_cast : constr -> constr
(* Special function, which keep the key casts under Fix and MutCase. *)
val strip_all_casts : constr -> constr
+(* Tests if a de Bruijn index *)
+val isRel : constr -> bool
+
+(* Tests if a variable *)
+val isVar : constr -> bool
+
(* Destructs the product $(x:t_1)t_2$ *)
val destProd : constr -> name * constr * constr
val hd_of_prod : constr -> constr
@@ -316,7 +322,7 @@ val args_of_const : constr -> constr array
val destEvar : constr -> int * constr array
val num_of_evar : constr -> int
-(* Destrucy an abstract term *)
+(* Destructs an abstract term *)
val destAbst : constr -> section_path * constr array
val path_of_abst : constr -> section_path
val args_of_abst : constr -> constr array
@@ -343,11 +349,9 @@ val destCase : constr -> case_info * constr * constr * constr array
*)
val destGralFix :
constr array -> constr array * Names.name list * constr array
-val destFix : constr ->
- int array * int * typed_type array * Names.name list * constr array
+val destFix : constr -> fixpoint
-val destCoFix :
- constr -> int * typed_type array * Names.name list * constr array
+val destCoFix : constr -> cofixpoint
(* Provisoire, le temps de maitriser les cast *)
val destUntypedFix :
@@ -534,6 +538,18 @@ val rel_vect : int -> int -> constr array
in c, [false] otherwise *)
val occur_const : section_path -> constr -> bool
+(* [(occur_evar ev c)] returns [true] if existential variable [ev] occurs
+ in c, [false] otherwise *)
+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
+
+(* [dependent M N] is true iff M is eq_constr with a subterm of N
+ M is appropriately lifted through abstractions of N *)
+val dependent : constr -> constr -> bool
+
(* strips head casts and flattens head applications *)
val strip_head_cast : constr -> constr
val whd_castapp_stack : constr -> constr list -> constr * constr list
diff --git a/kernel/typeops.ml b/kernel/typeops.ml
index 1a6c1d885..e227111d0 100644
--- a/kernel/typeops.ml
+++ b/kernel/typeops.ml
@@ -351,6 +351,7 @@ let apply_rel_list env sigma nocheck argjl funj =
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
@@ -629,30 +630,19 @@ nvect is [|n1;..;nk|] which gives for each recursive definition
the inductive-decreasing index
the function checks the convertibility of ti with Ai *)
-let check_fix env sigma = function
- | DOPN(Fix(nvect,j),vargs) ->
- let nbfix = let nv = Array.length vargs in
- if nv < 2 then error "Ill-formed recursive definition" else nv-1 in
- let varit = Array.sub vargs 0 nbfix in
- let ldef = array_last vargs in
- let ln = Array.length nvect
- and la = Array.length varit in
- if ln <> la then
- error "Ill-formed fix term"
- else
- let (lna,vdefs) = decomp_DLAMV_name ln ldef in
- let vlna = Array.of_list lna in
- let check_type i =
- try
- let _ =
- check_subterm_rec_meta env sigma nvect nvect.(i) vdefs.(i) in
- ()
- with UserError (s,str) ->
- error_ill_formed_rec_body CCI env str lna i vdefs
- in
- for i = 0 to ln-1 do check_type i done
-
- | _ -> assert false
+let check_fix env sigma ((nvect,bodynum),(types,names,bodies)) =
+ let nbfix = Array.length bodies in
+ if nbfix = 0
+ or Array.length nvect <> nbfix
+ or Array.length types <> nbfix
+ or List.length names <> nbfix
+ then error "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
+ done
(* Co-fixpoints. *)
@@ -733,28 +723,18 @@ let check_guard_rec_meta env sigma nbfix def deftype =
else
error "Recursive call in the type of an abstraction"
- | (DOPN(CoFix(j),vargs),l) ->
- if (List.for_all (noccur_with_meta n nbfix) l)
- then
- let nbfix = let nv = Array.length vargs in
- if nv < 2 then
- error "Ill-formed recursive definition"
- else
- nv-1
- in
- let varit = Array.sub vargs 0 nbfix in
- let ldef = array_last vargs in
- let la = Array.length varit in
- let (lna,vdefs) = decomp_DLAMV_name la ldef in
- let vlna = Array.of_list lna
- in
- if (array_for_all (noccur_with_meta n nbfix) varit) then
- (array_for_all (check_rec_call alreadygrd (n+1) vlra) vdefs)
- &&
- (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"
+ | (DOPN(CoFix(j),vargs) as cofix,l) ->
+ if (List.for_all (noccur_with_meta n nbfix) l)
+ then
+ let (j,(varit,lna,vdefs)) = destFix cofix in
+ let nbfix = Array.length vdefs in
+ if (array_for_all (noccur_with_meta n nbfix) varit) then
+ (array_for_all (check_rec_call alreadygrd (n+1) vlra) vdefs)
+ &&
+ (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"
| (DOPN(MutCase _,_) as mc,l) ->
let (_,p,c,vrest) = destCase mc in
@@ -777,6 +757,17 @@ let check_guard_rec_meta env sigma nbfix def deftype =
(* The function which checks that the whole block of definitions
satisfies the guarded condition *)
+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
+ done
+(*
let check_cofix env sigma f =
match f with
| DOPN(CoFix(j),vargs) ->
@@ -801,7 +792,7 @@ let check_cofix env sigma f =
in
for i = 0 to nbfix-1 do check_type i done
| _ -> assert false
-
+*)
(* Checks the type of a (co)fixpoint.
Fix and CoFix are typed the same way; only the guard condition differs. *)
@@ -831,10 +822,10 @@ let control_only_guard env sigma =
| VAR _ -> ()
| DOP0(_) -> ()
| DOPN(CoFix(_),cl) as cofix ->
- check_cofix env sigma cofix;
+ check_cofix env sigma (destCoFix cofix);
Array.iter control_rec cl
| DOPN(Fix(_),cl) as fix ->
- check_fix env sigma 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
diff --git a/kernel/typeops.mli b/kernel/typeops.mli
index 7ab2404f8..3d2074c97 100644
--- a/kernel/typeops.mli
+++ b/kernel/typeops.mli
@@ -67,8 +67,8 @@ val apply_rel_list :
env -> 'a evar_map -> bool -> unsafe_judgment list -> unsafe_judgment
-> unsafe_judgment * constraints
-val check_fix : env -> 'a evar_map -> constr -> unit
-val check_cofix : env -> 'a evar_map -> constr -> unit
+val check_fix : env -> 'a evar_map -> fixpoint -> unit
+val check_cofix : env -> 'a evar_map -> cofixpoint -> unit
val control_only_guard : env -> 'a evar_map -> constr -> unit
val type_fixpoint : env -> 'a evar_map -> name list -> typed_type array
diff --git a/library/indrec.ml b/library/indrec.ml
index a8f708c45..f83138b3d 100644
--- a/library/indrec.ml
+++ b/library/indrec.ml
@@ -253,12 +253,8 @@ let mis_make_indrec env sigma listdepkind mispec =
let fixn = Array.of_list (List.rev ln) in
let fixtyi = Array.of_list (List.rev ltyp) in
let fixdef = Array.of_list (List.rev ldef) in
- let makefixdef =
- put_DLAMSV
- (list_tabulate (fun _ -> Name(id_of_string "F")) nrec) fixdef
- in
- let fixspec = Array.append fixtyi [|makefixdef|] in
- DOPN(Fix(fixn,p),fixspec)
+ let names = list_tabulate (fun _ -> Name(id_of_string "F")) nrec in
+ mkFix ((fixn,p),(fixtyi,names,fixdef))
in
mrec 0 [] [] []
in
@@ -442,7 +438,7 @@ let pred_case_ml_fail env sigma isrec (IndType (indf,realargs)) (i,ft) =
let nbrec = if isrec then count_rec_arg j recargi else 0 in
let nb_arg = List.length (recargs.(i-1)) + nbrec in
let pred = concl_n env sigma nb_arg ft in
- if noccur_bet 1 nb_arg pred then
+ if noccur_between 1 nb_arg pred then
lift (-nb_arg) pred
else
failwith "Dependent"
diff --git a/parsing/termast.ml b/parsing/termast.ml
index 9adc75473..4bc238c4c 100644
--- a/parsing/termast.ml
+++ b/parsing/termast.ml
@@ -474,7 +474,7 @@ let computable p k =
let rec striprec = function
| (0,DOP2(Lambda,_,DLAM(_,d))) -> false
- | (0,d ) -> noccur_bet 1 k d
+ | (0,d ) -> noccur_between 1 k d
| (n,DOP2(Lambda,_,DLAM(_,d))) -> striprec (n-1,d)
| _ -> false
in
@@ -606,7 +606,7 @@ let old_bdize at_top env t =
ope(tag,pred::asttomatch::eqnl)
end
- | IsFix (nv,n,cl,lfn,vt) ->
+ | IsFix ((nv,n),(cl,lfn,vt)) ->
let lfi = List.map (fun na -> next_name_away na avoid) lfn in
let def_env =
List.fold_left
@@ -651,7 +651,7 @@ let old_bdize at_top env t =
in
ope("FIX", (nvar (string_of_id f))::listdecl)
- | IsCoFix (n,cl,lfn,vt) ->
+ | IsCoFix (n,(cl,lfn,vt)) ->
let lfi = List.map (fun na -> next_name_away na avoid) lfn in
let def_env =
List.fold_left
diff --git a/pretyping/cases.ml b/pretyping/cases.ml
index 85bce776a..67d279867 100644
--- a/pretyping/cases.ml
+++ b/pretyping/cases.ml
@@ -220,12 +220,11 @@ let lift_tomatch_type n = liftn_tomatch_type n 1
let lift_tomatch n ((current,typ),info) =
((lift n current,lift_tomatch_type n typ),info)
-let substn_many_tomatch v depth = function
- | IsInd (t,indt) ->
- IsInd (substn_many v depth t,substn_many_ind_type v depth indt)
- | NotInd t -> NotInd (substn_many v depth t)
+let substnl_tomatch v depth = function
+ | IsInd (t,indt) -> IsInd (substnl v depth t,substnl_ind_type v depth indt)
+ | NotInd t -> NotInd (substnl v depth t)
-let subst_tomatch (depth,c) = substn_many_tomatch [|make_substituend c|] depth
+let subst_tomatch (depth,c) = substnl_tomatch [c] depth
(**********************************************************************)
@@ -361,8 +360,7 @@ let rec lift_subst_tomatch n (depth,ci as binder) = function
| Pushed (lift,tm)::rest ->
Pushed (n+lift, tm)::(lift_subst_tomatch n binder rest)
-let subst_in_subst id t (id2,c) =
- (id2,replace_vars [(id,make_substituend t)] c)
+let subst_in_subst id t (id2,c) = (id2,replace_vars [(id,t)] c)
let replace_id_in_rhs id t rhs =
if List.mem id rhs.private_ids then
@@ -454,9 +452,9 @@ let prepare_unif_pb typ cs =
(* We may need to invert ci if its parameters occur in p *)
let p' =
- if noccur_bet 1 n p then lift (-n) p
+ if noccur_between 1 n p then lift (-n) p
else
- (* Il faudrait que noccur_bet ne regarde pas la subst des Evar *)
+ (* Il faudrait que noccur_between ne regarde pas la subst des Evar *)
if match p with DOPN(Evar _,_) -> true | _ -> false then lift (-n) p
else failwith "TODO4-1" in
let ci = applist
@@ -494,15 +492,15 @@ let lift_predicate n pred =
let subst_predicate (args,copt) pred =
let sigma = match copt with
- | None -> Array.map make_substituend (Array.of_list args)
- | Some c -> Array.map make_substituend (Array.of_list (args@[c])) in
+ | None -> args
+ | Some c -> args@[c] in
let rec substrec k = function
- | PrCcl ccl -> PrCcl (substn_many sigma k ccl)
+ | PrCcl ccl -> PrCcl (substnl sigma k ccl)
| PrProd ((dep,na,t),pred) ->
- PrProd ((dep,na,substn_many_tomatch sigma k t), substrec (k+1) pred)
+ PrProd ((dep,na,substnl_tomatch sigma k t), substrec (k+1) pred)
| PrLetIn ((args,copt),pred) ->
- let args' = List.map (substn_many sigma k) args in
- let copt' = option_app (substn_many sigma k) copt in
+ let args' = List.map (substnl sigma k) args in
+ let copt' = option_app (substnl sigma k) copt in
PrLetIn ((args',copt'), substrec (k+1) pred) in
substrec 0 pred
diff --git a/pretyping/detyping.ml b/pretyping/detyping.ml
index 901e60b8c..01ed9dc3b 100644
--- a/pretyping/detyping.ml
+++ b/pretyping/detyping.ml
@@ -247,7 +247,7 @@ let computable p k =
let rec striprec = function
| (0,DOP2(Lambda,_,DLAM(_,d))) -> false
- | (0,d ) -> noccur_bet 1 k d
+ | (0,d ) -> noccur_between 1 k d
| (n,DOP2(Lambda,_,DLAM(_,d))) -> striprec (n-1,d)
| _ -> false
in
@@ -356,8 +356,8 @@ let rec detype avoid env t =
RCases (dummy_loc,tag,pred,[tomatch],eqnl)
end
- | IsFix (nv,n,cl,lfn,vt) -> detype_fix (RFix (nv,n)) avoid env cl lfn vt
- | IsCoFix (n,cl,lfn,vt) -> detype_fix (RCofix n) avoid env cl lfn vt)
+ | IsFix (nvn,(cl,lfn,vt)) -> detype_fix (RFix nvn) avoid env cl lfn vt
+ | IsCoFix (n,(cl,lfn,vt)) -> detype_fix (RCofix n) avoid env cl lfn vt)
and detype_fix fk avoid env cl lfn vt =
let lfi = List.map (fun id -> next_name_away id avoid) lfn in
diff --git a/pretyping/evarutil.ml b/pretyping/evarutil.ml
index 5e89dbc5d..863843d4f 100644
--- a/pretyping/evarutil.ml
+++ b/pretyping/evarutil.ml
@@ -244,7 +244,7 @@ let new_isevar isevars env typ k =
*)
let evar_define isevars lhs rhs =
let (ev,argsv) = destEvar lhs in
- if occur_opern (Evar ev) rhs then error_occur_check CCI empty_env ev rhs;
+ if occur_evar ev rhs then error_occur_check CCI empty_env ev rhs;
let args = List.map (function (VAR _ | Rel _) as t -> t | _ -> mkImplicit)
(Array.to_list argsv) in
let evd = ise_map isevars ev in
diff --git a/pretyping/pretyping.ml b/pretyping/pretyping.ml
index 5d64f6e23..2493ae7a0 100644
--- a/pretyping/pretyping.ml
+++ b/pretyping/pretyping.ml
@@ -329,15 +329,16 @@ match cstr with (* Où teste-t-on que le résultat doit satisfaire tycon ? *)
pretype (mk_tycon (lift nbfix (larj.(i).uj_val))) newenv isevars lvar
lmeta def) vdef in
(evar_type_fixpoint env isevars lfi lara vdefj;
- match fixkind with
- | RFix(vn,i) ->
- let fix = mkFix vn i lara (List.rev lfi) (Array.map j_val_only vdefj) in
- check_fix env !isevars fix;
- make_judge fix lara.(i)
- | RCofix i ->
- let cofix = mkCoFix i lara (List.rev lfi) (Array.map j_val_only vdefj) in
- check_cofix env !isevars cofix;
- make_judge cofix lara.(i))
+ let larav = Array.map body_of_type lara in
+ match fixkind with
+ | RFix (vn,i as vni) ->
+ let fix = (vni,(larav,List.rev lfi,Array.map j_val_only vdefj)) in
+ check_fix env !isevars fix;
+ make_judge (mkFix fix) lara.(i)
+ | RCofix i ->
+ let cofix = (i,(larav,List.rev lfi,Array.map j_val_only vdefj)) in
+ check_cofix env !isevars cofix;
+ make_judge (mkCoFix cofix) lara.(i))
| RSort (loc,s) -> pretype_sort s
diff --git a/pretyping/retyping.ml b/pretyping/retyping.ml
index 96de2fc0a..e4554527d 100644
--- a/pretyping/retyping.ml
+++ b/pretyping/retyping.ml
@@ -64,8 +64,8 @@ let rec type_of env cstr=
| IsLambda (name,c1,c2) ->
let var = make_typed c1 (sort_of env c1) in
mkProd name c1 (type_of (push_rel (name,var) env) c2)
- | IsFix (vn,i,lar,lfi,vdef) -> lar.(i)
- | IsCoFix (i,lar,lfi,vdef) -> lar.(i)
+ | IsFix ((vn,i),(lar,lfi,vdef)) -> lar.(i)
+ | IsCoFix (i,(lar,lfi,vdef)) -> lar.(i)
| IsAppL(f,args)->
strip_outer_cast (subst_type env sigma (type_of env f) args)
| IsCast (c,t) -> t
diff --git a/pretyping/tacred.ml b/pretyping/tacred.ml
index 2f3b674f6..836b5e3ef 100644
--- a/pretyping/tacred.ml
+++ b/pretyping/tacred.ml
@@ -85,14 +85,11 @@ let reduce_fix_use_function f whfun fix stack =
| _ -> (false,(fix,stack'))))
| _ -> assert false
-let contract_cofix_use_function f cofix =
- match cofix with
- | DOPN(CoFix(bodynum),bodyvect) ->
- let nbodies = (Array.length bodyvect) -1 in
- let make_Fi j = DOPN(CoFix(j),bodyvect) in
- let lbodies = list_assign (list_tabulate make_Fi nbodies) bodynum f in
- sAPPViList bodynum (array_last bodyvect) lbodies
- | _ -> assert false
+let contract_cofix_use_function f (bodynum,(_,_,bodies as typedbodies)) =
+ let nbodies = Array.length bodies in
+ let make_Fi j = mkCoFix (nbodies-j-1,typedbodies) in
+ let subbodies = list_assign (list_tabulate make_Fi nbodies) bodynum f in
+ substl subbodies bodies.(bodynum)
let reduce_mind_case_use_function env f mia =
match mia.mconstr with
@@ -101,7 +98,7 @@ let reduce_mind_case_use_function env f mia =
let real_cargs = list_lastn ncargs mia.mcargs in
applist (mia.mlf.(i-1),real_cargs)
| DOPN(CoFix _,_) as cofix ->
- let cofix_def = contract_cofix_use_function f cofix in
+ let cofix_def = contract_cofix_use_function f (destCoFix cofix) in
mkMutCaseA mia.mci mia.mP (applist(cofix_def,mia.mcargs)) mia.mlf
| _ -> assert false
diff --git a/pretyping/typing.ml b/pretyping/typing.ml
index 583d395c8..92ad4cf5c 100644
--- a/pretyping/typing.ml
+++ b/pretyping/typing.ml
@@ -58,19 +58,21 @@ let rec execute mf env sigma cstr =
let lfj = execute_array mf env sigma lf in
type_of_case env sigma ci pj cj lfj
- | IsFix (vn,i,lar,lfi,vdef) ->
+ | IsFix ((vn,i as vni),(lar,lfi,vdef)) ->
if (not mf.fix) && array_exists (fun n -> n < 0) vn then
error "General Fixpoints not allowed";
- let larv,vdefv = execute_fix mf env sigma lar lfi vdef in
- let fix = mkFix vn i larv lfi vdefv in
+ let larjv,vdefv = execute_fix mf env sigma lar lfi vdef in
+ let larv = Array.map body_of_type larjv in
+ let fix = vni,(larv,lfi,vdefv) in
check_fix env sigma fix;
- make_judge fix larv.(i)
+ make_judge (mkFix fix) larjv.(i)
- | IsCoFix (i,lar,lfi,vdef) ->
- let (larv,vdefv) = execute_fix mf env sigma lar lfi vdef in
- let cofix = mkCoFix i larv lfi vdefv in
+ | IsCoFix (i,(lar,lfi,vdef)) ->
+ let (larjv,vdefv) = execute_fix mf env sigma lar lfi vdef in
+ let larv = Array.map body_of_type larjv in
+ let cofix = i,(larv,lfi,vdefv) in
check_cofix env sigma cofix;
- make_judge cofix larv.(i)
+ make_judge (mkCoFix cofix) larjv.(i)
| IsSort (Prop c) ->
judge_of_prop_contents c
diff --git a/proofs/clenv.ml b/proofs/clenv.ml
index 80bef43d8..2ad3f5896 100644
--- a/proofs/clenv.ml
+++ b/proofs/clenv.ml
@@ -53,12 +53,12 @@ let applyHead n c wc =
(wc,c)
else
match w_whd_betadeltaiota wc cty with
- | DOP2(Prod,c1,c2) ->
+ | DOP2(Prod,c1,DLAM(_,c2)) ->
let c1ty = w_type_of wc c1 in
let evar = new_evar_in_sign (w_env wc) in
let (evar_n, _) = destEvar evar in
(compose
- (apprec (n-1) (applist(c,[evar])) (sAPP c2 evar))
+ (apprec (n-1) (applist(c,[evar])) (subst1 evar c2))
(w_Declare evar_n (DOP2(Cast,c1,c1ty))))
wc
| _ -> error "Apply_Head_Then"
diff --git a/proofs/evar_refiner.ml b/proofs/evar_refiner.ml
index 004bc5c47..b73d19ee9 100644
--- a/proofs/evar_refiner.ml
+++ b/proofs/evar_refiner.ml
@@ -133,16 +133,23 @@ let w_Declare sp c (wc : walking_constraints) =
let w_Declare_At sp sp' c = w_Focusing sp (w_Declare sp' c)
-let evars_of sigma c =
- List.fold_right Intset.add
- (list_uniquize (process_opers_of_term
- (function
- | Evar ev -> Evd.in_dom (ts_it sigma).decls ev
- | _ -> false)
- (function
- | Evar ev -> ev
- | _ -> assert false) [] c))
- Intset.empty
+let evars_of sigma constr =
+ let rec filtrec acc = function
+ | DOP0 oper -> acc
+ | VAR _ -> acc
+ | DOP1(oper,c) -> filtrec acc c
+ | DOP2(oper,c1,c2) -> filtrec (filtrec acc c1) c2
+ | DOPN(Evar ev,cl) ->
+ let newacc = (Array.fold_left filtrec acc cl) in
+ if Evd.in_dom (ts_it sigma).decls ev
+ then Intset.add ev newacc else newacc
+ | DOPN(oper,cl) -> Array.fold_left filtrec acc cl
+ | DOPL(oper,cl) -> List.fold_left filtrec acc cl
+ | DLAM(_,c) -> filtrec acc c
+ | DLAMV(_,v) -> Array.fold_left filtrec acc v
+ | _ -> acc
+ in
+ filtrec Intset.empty constr
let w_Define sp c wc =
let spdecl = Evd.map (w_Underlying wc) sp in
diff --git a/proofs/logic.ml b/proofs/logic.ml
index 6a12e8d35..2f59990d6 100644
--- a/proofs/logic.ml
+++ b/proofs/logic.ml
@@ -114,9 +114,9 @@ and mk_arggoals sigma goal goalacc funty = function
| harg::tlargs ->
let env = goal.evar_env in
(match whd_betadeltaiota env sigma funty with
- | DOP2(Prod,c1,b) ->
+ | DOP2(Prod,c1,DLAM(_,b)) ->
let (acc',hargty) = mk_refgoals sigma goal goalacc c1 harg in
- mk_arggoals sigma goal acc' (sAPP b harg) tlargs
+ mk_arggoals sigma goal acc' (subst1 harg b) tlargs
| t -> raise (RefinerError (CannotApply (t,harg))))
and mk_casegoals sigma goal goalacc p c =
@@ -234,18 +234,18 @@ let prim_refiner r sigma goal =
| { name = Intro; newids = [id] } ->
if mem_sign sign id then error "New variable is already declared";
(match strip_outer_cast cl with
- | DOP2(Prod,c1,b) ->
+ | DOP2(Prod,c1,DLAM(_,b)) ->
if occur_meta c1 then error_use_instantiate();
let a = mk_assumption env sigma c1
and v = VAR id in
- let sg = mk_goal info (push_var (id,a) env) (sAPP b v) in
+ let sg = mk_goal info (push_var (id,a) env) (subst1 v b) in
[sg]
| _ -> error "Introduction needs a product")
| { name = Intro_after; newids = [id]; hypspecs = [whereid] } ->
if mem_sign sign id then error "New variable is already declared";
(match strip_outer_cast cl with
- | DOP2(Prod,c1,b) ->
+ | DOP2(Prod,c1,DLAM(_,b)) ->
if occur_meta c1 then error_use_instantiate();
if not (List.for_all
(mem_sign (sign_prefix whereid sign))
@@ -255,13 +255,13 @@ let prim_refiner r sigma goal =
let a = mk_assumption env sigma c1
and v = VAR id in
let env' = change_hyps (add_sign_after whereid (id,a)) env in
- let sg = mk_goal info env' (sAPP b v) in
+ let sg = mk_goal info env' (subst1 v b) in
[sg]
| _ -> error "Introduction needs a product")
| { name = Intro_replacing; newids = []; hypspecs = [id] } ->
(match strip_outer_cast cl with
- | DOP2(Prod,c1,b) ->
+ | DOP2(Prod,c1,DLAM(_,b)) ->
if occur_meta c1 then error_use_instantiate();
if not (List.for_all
(mem_sign (tl_sign (sign_prefix id sign)))
@@ -274,7 +274,7 @@ let prim_refiner r sigma goal =
let a = mk_assumption env sigma c1
and v = VAR id in
let env' = change_hyps (add_sign_replacing id (id,a)) env in
- let sg = mk_goal info env' (sAPP b v) in
+ let sg = mk_goal info env' (subst1 v b) in
[sg]
| _ -> error "Introduction needs a product")
@@ -432,25 +432,23 @@ let extract_constr =
let u1 = crec vl c1 in
DOP2(Lambda,u1,DLAM(na,crec (add_rel (Anonymous,u1) vl) c2))
- | DOPN(Term.Fix (x_0,x_1),cl) ->
- let listar = Array.sub cl 0 ((Array.length cl) -1)
- and def = array_last cl in
- let newar = Array.map (crec vl) listar in
+ | DOPN(Term.Fix _,_) as fix ->
+ let (vn,(lar,lna,defs)) = destFix fix in
+ let newar = Array.map (crec vl) lar in
let newenv =
- Array.fold_left
- (fun env ar -> add_rel (Anonymous,ar) env) vl newar in
- let newdef = under_dlams (crec newenv) def in
- DOPN(Term.Fix (x_0,x_1),Array.append newar [|newdef|])
-
- | DOPN(CoFix par,cl) ->
- let listar = Array.sub cl 0 ((Array.length cl) -1)
- and def = array_last cl in
- let newar = Array.map (crec vl) listar in
+ array_fold_left2
+ (fun env na ar -> add_rel (na,ar) env) vl
+ (Array.of_list lna) newar in
+ mkFix (vn,(newar,lna,Array.map (crec newenv) defs))
+
+ | DOPN(CoFix _,_) as cofix ->
+ let (n,(lar,lna,defs)) = destCoFix cofix in
+ let newar = Array.map (crec vl) lar in
let newenv =
- Array.fold_left (fun env ar -> add_rel (Anonymous,ar) env) vl newar
- in
- let newdef = under_dlams (crec newenv) def in
- DOPN(CoFix par,Array.append newar [|newdef|])
+ array_fold_left2
+ (fun env na ar -> add_rel (na,ar) env) vl
+ (Array.of_list lna) newar in
+ mkCoFix (n,(newar,lna,Array.map (crec newenv) defs))
| DOP2(Prod,c1,DLAM(na,c2)) ->
let u1 = crec vl c1 in
@@ -510,8 +508,7 @@ let prim_extractor subfun vl pft =
let newvl = List.fold_left2 (fun sign na ar -> (add_rel (na,ar) sign))
vl lna lcty in
let lfix =Array.map (subfun newvl) (Array.of_list spfl) in
- DOPN(Term.Fix(vn,0),
- Array.of_list (lcty@[put_DLAMSV (List.rev lna) lfix]))
+ mkFix ((vn,0),(Array.of_list lcty,lna,lfix))
| {ref=Some(Prim{name=Cofix;newids=lf;terms=lar},spfl) } ->
let lcty = List.map (extract_constr vl) (cl::lar) in
@@ -521,7 +518,7 @@ let prim_extractor subfun vl pft =
vl lna lcty
in
let lfix =Array.map (subfun newvl) (Array.of_list spfl) in
- DOPN(CoFix(0),Array.of_list (lcty@[put_DLAMSV (List.rev lna) lfix]))
+ mkCoFix (0,(Array.of_list lcty,lna,lfix))
| {ref=Some(Prim{name=Refine;terms=[c]},spfl) } ->
let mvl = collect_meta_variables c in
diff --git a/tactics/equality.ml b/tactics/equality.ml
index 955767cef..c923cfe17 100644
--- a/tactics/equality.ml
+++ b/tactics/equality.ml
@@ -726,7 +726,7 @@ let make_tuple env sigma (rterm,rty) lind =
find_sigma_data (get_sort_of env sigma rty) in
let a = type_of env sigma (Rel lind) in
(* We replace (Rel lind) by (Rel 1) in rty then abstract on (na:a) *)
- let rty' = substn_many [|make_substituend (Rel 1)|] lind rty in
+ let rty' = substnl [Rel 1] lind rty in
let na = fst (lookup_rel lind env) in
let p = mkLambda na a rty' in
(applist(exist_term,[a;p;(Rel lind);rterm]),
@@ -1228,8 +1228,7 @@ let substInHyp eqn id gls =
let (lbeq,(t,e1,e2)) = (find_eq_data_decompose eqn) in
let body = subst_term e1 (clause_type (Some id) gls) in
if not (dependent (Rel 1) body) then errorlabstrm "SubstInHyp" [<>];
- let pB = DLAM(Environ.named_hd (pf_env gls) t Anonymous,body) in
- (tclTHENS (cut_replacing id (sAPP pB e2))
+ (tclTHENS (cut_replacing id (subst1 e2 body))
([tclIDTAC;
(tclTHENS (bareRevSubstInConcl lbeq body (t,e1,e2))
([exact (VAR id);tclIDTAC]))])) gls
diff --git a/tactics/wcclausenv.ml b/tactics/wcclausenv.ml
index 8a76a0e6f..48ae03cc9 100644
--- a/tactics/wcclausenv.ml
+++ b/tactics/wcclausenv.ml
@@ -134,9 +134,9 @@ let elim_res_pf_THEN_i kONT clenv tac gls =
let rec build_args acc ce p_0 p_1 =
match p_0,p_1 with
- | ((DOP2(Prod,a,(DLAM(na,_) as b))), (a_0::bargs)) ->
+ | ((DOP2(Prod,a,DLAM(na,b))), (a_0::bargs)) ->
let (newa,ce') = (build_term ce (na,Some a) a_0) in
- build_args (newa::acc) ce' (sAPP b a_0) bargs
+ build_args (newa::acc) ce' (subst1 a_0 b) bargs
| (_, []) -> (List.rev acc,ce)
| (_, (_::_)) -> failwith "mk_clenv_using"
diff --git a/toplevel/command.ml b/toplevel/command.ml
index 49d6bf7b2..7b507f5aa 100644
--- a/toplevel/command.ml
+++ b/toplevel/command.ml
@@ -122,56 +122,54 @@ let corecursive_message = function
| l -> hOV 0 [< prlist_with_sep pr_coma print_id l;
'sPC; 'sTR "are corecursively defined">]
+let put_DLAMSV_subst lid lc =
+ match lid with
+ | [] -> anomaly "put_DLAM"
+ | id::lrest ->
+ List.fold_left (fun c id' -> DLAM(Name id',subst_var id' c))
+ (DLAMV(Name id,Array.map (subst_var id) lc)) lrest
+
let build_mutual lparams lnamearconstrs finite =
let allnames =
List.fold_left
(fun acc (id,_,l) -> id::(List.map fst l)@acc) [] lnamearconstrs in
if not (list_distinct allnames) then
error "Two inductive objects have the same name";
- let lrecnames = List.map (fun (x,_,_)->x) lnamearconstrs
+ let lrecnames = List.map (fun (x,_,_) -> x) lnamearconstrs
and nparams = List.length lparams
and sigma = Evd.empty
and env0 = Global.env() in
-(* let fs = States.freeze() in*)
- try
- let mispecvec =
- let (ind_env,arityl) =
- List.fold_left
- (fun (env,arl) (recname,arityc,_) ->
- let arity =
- typed_type_of_com Evd.empty env (mkProdCit lparams arityc) in
- let env' = Environ.push_var (recname,arity) env in
-(* A quoi cela sert ?
- declare_variable recname (arity.body,NeverDischarge,false);*)
- (env', (arity::arl)))
- (env0,[]) lnamearconstrs
- in
- List.map2
- (fun ar (name,_,lname_constr) ->
- let consconstrl =
- List.map
- (fun (_,constr) -> interp_constr sigma ind_env
- (mkProdCit lparams constr))
- lname_constr
- in
- (name, (body_of_type ar), List.map fst lname_constr,
- put_DLAMSV_subst (List.rev lrecnames) (Array.of_list consconstrl)))
- (List.rev arityl) lnamearconstrs
- in
- let mie = {
- mind_entry_nparams = nparams;
- mind_entry_finite = finite;
- mind_entry_inds = mispecvec }
+ let mispecvec =
+ let (ind_env,arityl) =
+ List.fold_left
+ (fun (env,arl) (recname,arityc,_) ->
+ let arity =
+ typed_type_of_com Evd.empty env (mkProdCit lparams arityc) in
+ let env' = Environ.push_rel (Name recname,arity) env in
+ (env', (arity::arl)))
+ (env0,[]) lnamearconstrs
in
-(* States.unfreeze fs;*)
- let sp = declare_mind mie in
- if is_verbose() then pPNL(minductive_message lrecnames);
- for i = 0 to List.length mispecvec - 1 do
- declare_eliminations sp i
- done
- with e ->
-(* States.unfreeze fs; *)raise e
-
+ List.map2
+ (fun ar (name,_,lname_constr) ->
+ let consconstrl =
+ List.map
+ (fun (_,constr) -> interp_constr sigma ind_env
+ (mkProdCit lparams constr))
+ lname_constr
+ in
+ (name, (body_of_type ar), List.map fst lname_constr, consconstrl))
+ (List.rev arityl) lnamearconstrs
+ in
+ let mie = {
+ mind_entry_nparams = nparams;
+ mind_entry_finite = finite;
+ mind_entry_inds = mispecvec }
+ in
+ let sp = declare_mind mie in
+ if is_verbose() then pPNL(minductive_message lrecnames);
+ for i = 0 to List.length mispecvec - 1 do
+ declare_eliminations sp i
+ done
(* try to find non recursive definitions *)
@@ -241,7 +239,7 @@ let build_recursive lnameargsardef =
if lnamerec <> [] then begin
let recvec = [|put_DLAMSV_subst (List.rev lnamerec)
(Array.of_list ldefrec)|] in
- let varrec = Array.of_list larrec in
+ let varrec = Array.of_list (List.map incast_type larrec) in
let rec declare i = function
| fi::lf ->
let ce =
@@ -258,7 +256,7 @@ let build_recursive lnameargsardef =
if is_verbose() then pPNL(recursive_message lnamerec)
end;
(* The others are declared as normal definitions *)
- let var_subst id = (id,make_substituend (global_reference CCI id)) in
+ let var_subst id = (id, global_reference CCI id) in
let _ =
List.fold_left
(fun subst (f,def) ->
@@ -308,11 +306,11 @@ let build_corecursive lnameardef =
else
[|put_DLAMSV_subst (List.rev lnamerec) (Array.of_list ldefrec)|]
in
+ let varrec = Array.of_list (List.map incast_type larrec) in
let rec declare i = function
| fi::lf ->
let ce =
- { const_entry_body =
- Cooked (mkCoFixDlam i (Array.of_list larrec) recvec);
+ { const_entry_body = Cooked (mkCoFixDlam i varrec recvec);
const_entry_type = None }
in
declare_constant fi (ce,n);
@@ -322,8 +320,7 @@ let build_corecursive lnameardef =
declare 0 lnamerec;
if is_verbose() then pPNL(corecursive_message lnamerec)
end;
- let var_subst id =
- (id,make_substituend (global_reference CCI id)) in
+ let var_subst id = (id, global_reference CCI id) in
let _ =
List.fold_left
(fun subst (f,def) ->
diff --git a/toplevel/discharge.ml b/toplevel/discharge.ml
index 1e8501f12..67ecd9139 100644
--- a/toplevel/discharge.ml
+++ b/toplevel/discharge.ml
@@ -99,6 +99,14 @@ let modify_opers replfun absfun oper_alist =
(**)
+let under_dlams f =
+ let rec apprec = function
+ | DLAMV(na,c) -> DLAMV(na,Array.map f c)
+ | DLAM(na,c) -> DLAM(na,apprec c)
+ | _ -> failwith "under_dlams"
+ in
+ apprec
+
let abstract_inductive ids_to_abs hyps inds =
let abstract_one_var id ty inds =
let ntyp = List.length inds in
@@ -108,8 +116,7 @@ let abstract_inductive ids_to_abs hyps inds =
(function (tname,arity,cnames,lc) ->
let arity' = generalize_type id ty arity in
let lc' =
- under_dlams
- (fun b -> casted_generalize id ty (substl new_refs b)) lc
+ List.map (fun b-> casted_generalize id ty (substl new_refs b)) lc
in
(tname,arity',cnames,lc'))
inds
@@ -119,9 +126,9 @@ let abstract_inductive ids_to_abs hyps inds =
let abstract_once ((hyps,inds,modl) as sofar) id =
if isnull_sign hyps or id <> fst (hd_sign hyps) then
sofar
- else
- let (inds',modif) = abstract_one_var id (snd (hd_sign hyps)) inds in
- (tl_sign hyps,inds',modif::modl)
+ else
+ let (inds',modif) = abstract_one_var id (snd (hd_sign hyps)) inds in
+ (tl_sign hyps,inds',modif::modl)
in
let (_,inds',revmodl) =
List.fold_left abstract_once (hyps,inds,[]) ids_to_abs in
@@ -206,7 +213,7 @@ let process_inductive osecsp nsecsp oldenv (ids_to_discard,modlist) mib =
(mip.mind_typename,
expmod_type oldenv modlist mip.mind_arity,
Array.to_list mip.mind_consnames,
- under_dlams (expmod_constr oldenv modlist) mip.mind_lc))
+ array_map_to_list (expmod_constr oldenv modlist) mip.mind_lc))
mib.mind_packets
in
let (inds',modl) = abstract_inductive ids_to_discard mib.mind_hyps inds in
diff --git a/toplevel/record.ml b/toplevel/record.ml
index 8f3052441..268ebd437 100644
--- a/toplevel/record.ml
+++ b/toplevel/record.ml
@@ -152,8 +152,7 @@ let definition_structure (is_coe,idstruc,ps,cfs,idbuild,s) =
let constr_fip = (* Rel 1 refers to "x" *)
applist (constr_fi,(List.map (fun id -> VAR id) idps)@[Rel 1])
in (Some(path_of_const constr_fi)::sp_projs,
- ids_not_ok,
- (fi,{sinfo=Closed;sit=constr_fip})::subst)
+ ids_not_ok, (fi,constr_fip)::subst)
end)
([],[],[]) coers newfs
in
generated by cgit v1.2.3 (git 2.39.1) at 2024-06-29 15:22:27 +0000