aboutsummaryrefslogtreecommitdiff
path: root/pretyping
diff options
context:
space:
mode:
Diffstat (limited to 'pretyping')
-rw-r--r--pretyping/cases.ml24
-rw-r--r--pretyping/cbv.ml88
-rw-r--r--pretyping/cbv.mli3
-rw-r--r--pretyping/constr_matching.ml31
-rw-r--r--pretyping/detyping.ml26
-rw-r--r--pretyping/evarconv.ml18
-rw-r--r--pretyping/evarsolve.ml18
-rw-r--r--pretyping/find_subterm.ml16
-rw-r--r--pretyping/find_subterm.mli4
-rw-r--r--pretyping/heads.ml2
-rw-r--r--pretyping/indrec.ml18
-rw-r--r--pretyping/inductiveops.ml5
-rw-r--r--pretyping/inductiveops.mli2
-rw-r--r--pretyping/nativenorm.ml3
-rw-r--r--pretyping/patternops.ml5
-rw-r--r--pretyping/pretyping.ml4
-rw-r--r--pretyping/reductionops.ml69
-rw-r--r--pretyping/reductionops.mli5
-rw-r--r--pretyping/retyping.ml5
-rw-r--r--pretyping/tacred.ml58
-rw-r--r--pretyping/typing.ml10
-rw-r--r--pretyping/unification.ml22
-rw-r--r--pretyping/vnorm.ml2
23 files changed, 281 insertions, 157 deletions
diff --git a/pretyping/cases.ml b/pretyping/cases.ml
index d2859b1b4e..6370bd4f9a 100644
--- a/pretyping/cases.ml
+++ b/pretyping/cases.ml
@@ -1165,17 +1165,16 @@ let rec ungeneralize sigma n ng body =
| LetIn (na,b,t,c) ->
(* We traverse an alias *)
mkLetIn (na,b,t,ungeneralize sigma (n+1) ng c)
- | Case (ci,p,iv,c,brs) ->
+ | Case (ci,u,pms,p,iv,c,brs) ->
(* We traverse a split *)
let p =
- let sign,p = decompose_lam_assum sigma p in
+ let (nas, p) = p in
let sign2,p = decompose_prod_n_assum sigma ng p in
- let p = prod_applist sigma p [mkRel (n+List.length sign+ng)] in
- it_mkLambda_or_LetIn (it_mkProd_or_LetIn p sign2) sign in
- mkCase (ci,p,iv,c,Array.map2 (fun q c ->
- let sign,b = decompose_lam_n_decls sigma q c in
- it_mkLambda_or_LetIn (ungeneralize sigma (n+q) ng b) sign)
- ci.ci_cstr_ndecls brs)
+ let p = prod_applist sigma p [mkRel (n+Array.length nas+ng)] in
+ nas, it_mkProd_or_LetIn p sign2
+ in
+ let map (nas, br) = nas, ungeneralize sigma (n + Array.length nas) ng br in
+ mkCase (ci, u, pms, p, iv, c, Array.map map brs)
| App (f,args) ->
(* We traverse an inner generalization *)
assert (isCase sigma f);
@@ -1195,12 +1194,9 @@ let rec is_dependent_generalization sigma ng body =
| LetIn (na,b,t,c) ->
(* We traverse an alias *)
is_dependent_generalization sigma ng c
- | Case (ci,p,iv,c,brs) ->
+ | Case (ci,u,pms,p,iv,c,brs) ->
(* We traverse a split *)
- Array.exists2 (fun q c ->
- let _,b = decompose_lam_n_decls sigma q c in
- is_dependent_generalization sigma ng b)
- ci.ci_cstr_ndecls brs
+ Array.exists (fun (_, b) -> is_dependent_generalization sigma ng b) brs
| App (g,args) ->
(* We traverse an inner generalization *)
assert (isCase sigma g);
@@ -1759,7 +1755,7 @@ let abstract_tycon ?loc env sigma subst tycon extenv t =
let good = List.filter (fun (_,u,_) -> is_conv_leq !!env sigma t u) subst in
match good with
| [] ->
- map_constr_with_full_binders sigma (push_binder sigma) aux x t
+ map_constr_with_full_binders !!env sigma (push_binder sigma) aux x t
| (_, _, u) :: _ -> (* u is in extenv *)
let vl = List.map pi1 good in
let ty =
diff --git a/pretyping/cbv.ml b/pretyping/cbv.ml
index bada2c3a60..7930c3d634 100644
--- a/pretyping/cbv.ml
+++ b/pretyping/cbv.ml
@@ -76,8 +76,7 @@ type cbv_value =
and cbv_stack =
| TOP
| APP of cbv_value array * cbv_stack
- | CASE of constr * constr array * (constr,Univ.Instance.t) case_invert
- * case_info * cbv_value subs * cbv_stack
+ | CASE of Univ.Instance.t * constr array * case_return * case_branch array * Constr.case_invert * case_info * cbv_value subs * cbv_stack
| PROJ of Projection.t * cbv_stack
(* les vars pourraient etre des constr,
@@ -143,7 +142,7 @@ let rec stack_concat stk1 stk2 =
match stk1 with
TOP -> stk2
| APP(v,stk1') -> APP(v,stack_concat stk1' stk2)
- | CASE(c,b,iv,i,s,stk1') -> CASE(c,b,iv,i,s,stack_concat stk1' stk2)
+ | CASE(u,pms,c,b,iv,i,s,stk1') -> CASE(u,pms,c,b,iv,i,s,stack_concat stk1' stk2)
| PROJ (p,stk1') -> PROJ (p,stack_concat stk1' stk2)
(* merge stacks when there is no shifts in between *)
@@ -357,9 +356,9 @@ let rec reify_stack t = function
| TOP -> t
| APP (args,st) ->
reify_stack (mkApp(t,Array.map reify_value args)) st
- | CASE (ty,br,iv,ci,env,st) ->
+ | CASE (u,pms,ty,br,iv,ci,env,st) ->
reify_stack
- (mkCase (ci, ty, iv, t, br))
+ (mkCase (ci, u, pms, ty, iv, t,br))
st
| PROJ (p, st) ->
reify_stack (mkProj (p, t)) st
@@ -410,6 +409,29 @@ let rec subs_consn v i n s =
if Int.equal i n then s
else subs_consn v (i + 1) n (subs_cons v.(i) s)
+(* TODO: share the common parts with EConstr *)
+let expand_branch env u pms (ind, i) br =
+ let open Declarations in
+ let nas, _br = br.(i - 1) in
+ let (mib, mip) = Inductive.lookup_mind_specif env ind in
+ let paramdecl = Vars.subst_instance_context u mib.mind_params_ctxt in
+ let paramsubst = Vars.subst_of_rel_context_instance paramdecl (Array.to_list pms) in
+ let subst = paramsubst @ Inductive.ind_subst (fst ind) mib u in
+ let (ctx, _) = mip.mind_nf_lc.(i - 1) in
+ let (ctx, _) = List.chop mip.mind_consnrealdecls.(i - 1) ctx in
+ Inductive.instantiate_context u subst nas ctx
+
+let cbv_subst_of_rel_context_instance mkclos sign args env =
+ let rec aux subst sign l =
+ let open Context.Rel.Declaration in
+ match sign, l with
+ | LocalAssum _ :: sign', a::args' -> aux (subs_cons a subst) sign' args'
+ | LocalDef (_,c,_)::sign', args' ->
+ aux (subs_cons (mkclos subst c) subst) sign' args'
+ | [], [] -> subst
+ | _ -> CErrors.anomaly (Pp.str "Instance and signature do not match.")
+ in aux env (List.rev sign) (Array.to_list args)
+
(* The main recursive functions
*
* Go under applications and cases/projections (pushed in the stack),
@@ -429,7 +451,7 @@ let rec norm_head info env t stack =
they could be computed when getting out of the stack *)
let nargs = Array.map (cbv_stack_term info TOP env) args in
norm_head info env head (stack_app nargs stack)
- | Case (ci,p,iv,c,v) -> norm_head info env c (CASE(p,v,iv,ci,env,stack))
+ | Case (ci,u,pms,p,iv,c,v) -> norm_head info env c (CASE(u,pms,p,v,iv,ci,env,stack))
| Cast (ct,_,_) -> norm_head info env ct stack
| Proj (p, c) ->
@@ -557,16 +579,33 @@ and cbv_stack_value info env = function
cbv_stack_term info stk envf redfix
(* constructor in a Case -> IOTA *)
- | (CONSTR(((sp,n),u),[||]), APP(args,CASE(_,br,iv,ci,env,stk)))
+ | (CONSTR(((sp,n),_),[||]), APP(args,CASE(u,pms,_p,br,iv,ci,env,stk)))
when red_set info.reds fMATCH ->
+ let nargs = Array.length args - ci.ci_npar in
let cargs =
- Array.sub args ci.ci_npar (Array.length args - ci.ci_npar) in
- cbv_stack_term info (stack_app cargs stk) env br.(n-1)
+ Array.sub args ci.ci_npar nargs in
+ let env =
+ if (Int.equal ci.ci_cstr_ndecls.(n - 1) ci.ci_cstr_nargs.(n - 1)) then (* no lets *)
+ subs_consn cargs 0 nargs env
+ else
+ let mkclos env c = cbv_stack_term info TOP env c in
+ let ctx = expand_branch info.env u pms (sp, n) br in
+ cbv_subst_of_rel_context_instance mkclos ctx cargs env
+ in
+ cbv_stack_term info stk env (snd br.(n-1))
(* constructor of arity 0 in a Case -> IOTA *)
- | (CONSTR(((_,n),u),[||]), CASE(_,br,_,_,env,stk))
+ | (CONSTR(((sp, n), _),[||]), CASE(u,pms,_,br,_,ci,env,stk))
when red_set info.reds fMATCH ->
- cbv_stack_term info stk env br.(n-1)
+ let env =
+ if (Int.equal ci.ci_cstr_ndecls.(n - 1) ci.ci_cstr_nargs.(n - 1)) then (* no lets *)
+ env
+ else
+ let mkclos env c = cbv_stack_term info TOP env c in
+ let ctx = expand_branch info.env u pms (sp, n) br in
+ cbv_subst_of_rel_context_instance mkclos ctx [||] env
+ in
+ cbv_stack_term info stk env (snd br.(n-1))
(* constructor in a Projection -> IOTA *)
| (CONSTR(((sp,n),u),[||]), APP(args,PROJ(p,stk)))
@@ -640,10 +679,31 @@ let rec apply_stack info t = function
| TOP -> t
| APP (args,st) ->
apply_stack info (mkApp(t,Array.map (cbv_norm_value info) args)) st
- | CASE (ty,br,iv,ci,env,st) ->
+ | CASE (u,pms,ty,br,iv,ci,env,st) ->
+ (* FIXME: Prevent this expansion by caching whether an inductive contains let-bindings *)
+ let (_, ty, _, _, br) = Inductive.expand_case info.env (ci, u, pms, ty, iv, mkProp, br) in
+ let ty =
+ let (_, mip) = Inductive.lookup_mind_specif info.env ci.ci_ind in
+ Term.decompose_lam_n_decls (mip.Declarations.mind_nrealdecls + 1) ty
+ in
+ let mk_br c n = Term.decompose_lam_n_decls n c in
+ let br = Array.map2 mk_br br ci.ci_cstr_ndecls in
+ let map_ctx (nas, c) =
+ let open Context.Rel.Declaration in
+ let fold decl e = match decl with
+ | LocalAssum _ -> subs_lift e
+ | LocalDef (_, b, _) ->
+ let b = cbv_stack_term info TOP e b in
+ (* The let-binding persists, so we have to shift *)
+ subs_shft (1, subs_cons b e)
+ in
+ let env = List.fold_right fold nas env in
+ let nas = Array.of_list (List.rev_map get_annot nas) in
+ (nas, cbv_norm_term info env c)
+ in
apply_stack info
- (mkCase (ci, cbv_norm_term info env ty, iv, t,
- Array.map (cbv_norm_term info env) br))
+ (mkCase (ci, u, Array.map (cbv_norm_term info env) pms, map_ctx ty, iv, t,
+ Array.map map_ctx br))
st
| PROJ (p, st) ->
apply_stack info (mkProj (p, t)) st
diff --git a/pretyping/cbv.mli b/pretyping/cbv.mli
index 409f4c0f70..4d81678200 100644
--- a/pretyping/cbv.mli
+++ b/pretyping/cbv.mli
@@ -42,8 +42,7 @@ type cbv_value =
and cbv_stack =
| TOP
| APP of cbv_value array * cbv_stack
- | CASE of constr * constr array * (constr,Univ.Instance.t) case_invert
- * case_info * cbv_value subs * cbv_stack
+ | CASE of Univ.Instance.t * constr array * case_return * case_branch array * Constr.case_invert * case_info * cbv_value subs * cbv_stack
| PROJ of Projection.t * cbv_stack
val shift_value : int -> cbv_value -> cbv_value
diff --git a/pretyping/constr_matching.ml b/pretyping/constr_matching.ml
index 0e69b814c7..c77feeafbb 100644
--- a/pretyping/constr_matching.ml
+++ b/pretyping/constr_matching.ml
@@ -351,7 +351,9 @@ let matches_core env sigma allow_bound_rels
sorec (push_binder na1 na2 t2 ctx) (EConstr.push_rel (LocalDef (na2,c2,t2)) env)
(add_binders na1 na2 binding_vars (sorec ctx env subst c1 c2)) d1 d2
- | PIf (a1,b1,b1'), Case (ci,_,_,a2,[|b2;b2'|]) ->
+ | PIf (a1,b1,b1'), Case (ci, u2, pms2, p2, iv, a2, ([|b2;b2'|] as br2)) ->
+ let (ci2, p2, _, a2, br2) = EConstr.expand_case env sigma (ci, u2, pms2, p2, iv, a2, br2) in
+ let b2, b2' = match br2 with [|b2; b2'|] -> b2, b2' | _ -> assert false in
let ctx_b2,b2 = decompose_lam_n_decls sigma ci.ci_cstr_ndecls.(0) b2 in
let ctx_b2',b2' = decompose_lam_n_decls sigma ci.ci_cstr_ndecls.(1) b2' in
let n = Context.Rel.length ctx_b2 in
@@ -367,7 +369,8 @@ let matches_core env sigma allow_bound_rels
else
raise PatternMatchingFailure
- | PCase (ci1,p1,a1,br1), Case (ci2,p2,_,a2,br2) ->
+ | PCase (ci1, p1, a1, br1), Case (ci2, u2, pms2, p2, iv, a2, br2) ->
+ let (ci2, p2, _, a2, br2) = EConstr.expand_case env sigma (ci2, u2, pms2, p2, iv, a2, br2) in
let n2 = Array.length br2 in
let () = match ci1.cip_ind with
| None -> ()
@@ -504,12 +507,30 @@ let sub_match ?(closed=true) env sigma pat c =
| [app';c] -> mk_ctx (mkApp (app',[|c|]))
| _ -> assert false in
try_aux [(env, app); (env, Array.last lc)] mk_ctx next
- | Case (ci,hd,iv,c1,lc) ->
+ | Case (ci,u,pms,hd0,iv,c1,lc0) ->
+ let (mib, mip) = Inductive.lookup_mind_specif env ci.ci_ind in
+ let (_, hd, _, _, br) = expand_case env sigma (ci, u, pms, hd0, iv, c1, lc0) in
+ let hd =
+ let (ctx, hd) = decompose_lam_assum sigma hd in
+ (push_rel_context ctx env, hd)
+ in
+ let map i br =
+ let decls = mip.Declarations.mind_consnrealdecls.(i) in
+ let (ctx, c) = decompose_lam_n_decls sigma decls br in
+ (push_rel_context ctx env, c)
+ in
+ let lc = Array.to_list (Array.mapi map br) in
let next_mk_ctx = function
- | c1 :: hd :: lc -> mk_ctx (mkCase (ci,hd,iv,c1,Array.of_list lc))
+ | c1 :: rem ->
+ let pms, rem = List.chop (Array.length pms) rem in
+ let pms = Array.of_list pms in
+ let hd, lc = match rem with [] -> assert false | x :: l -> (x, l) in
+ let hd = (fst hd0, hd) in
+ let map_br (nas, _) br = (nas, br) in
+ mk_ctx (mkCase (ci,u,pms,hd,iv,c1,Array.map2 map_br lc0 (Array.of_list lc)))
| _ -> assert false
in
- let sub = (env, c1) :: (env, hd) :: subargs env lc in
+ let sub = (env, c1) :: Array.fold_right (fun c accu -> (env, c) :: accu) pms (hd :: lc) in
try_aux sub next_mk_ctx next
| Fix (indx,(names,types,bodies as recdefs)) ->
let nb_fix = Array.length types in
diff --git a/pretyping/detyping.ml b/pretyping/detyping.ml
index 402a6f6ed3..27b193f144 100644
--- a/pretyping/detyping.ml
+++ b/pretyping/detyping.ml
@@ -241,16 +241,9 @@ let print_primproj_params =
(* Auxiliary function for MutCase printing *)
(* [computable] tries to tell if the predicate typing the result is inferable*)
-let computable sigma p k =
+let computable sigma (nas, ccl) =
(* We first remove as many lambda as the arity, then we look
- if it remains a lambda for a dependent elimination. This function
- works for normal eta-expanded term. For non eta-expanded or
- non-normal terms, it may affirm the pred is synthetisable
- because of an undetected ultimate dependent variable in the second
- clause, or else, it may affirm the pred non synthetisable
- because of a non normal term in the fourth clause.
- A solution could be to store, in the MutCase, the eta-expanded
- normal form of pred to decide if it depends on its variables
+ if it remains a lambda for a dependent elimination.
Lorsque le prédicat est dépendant de manière certaine, on
ne déclare pas le prédicat synthétisable (même si la
@@ -258,10 +251,7 @@ let computable sigma p k =
sinon on perd la réciprocité de la synthèse (qui, lui,
engendrera un prédicat non dépendant) *)
- let sign,ccl = decompose_lam_assum sigma p in
- Int.equal (Context.Rel.length sign) (k + 1)
- &&
- noccur_between sigma 1 (k+1) ccl
+ noccur_between sigma 1 (Array.length nas) ccl
let lookup_name_as_displayed env sigma t s =
let rec lookup avoid n c = match EConstr.kind sigma c with
@@ -429,11 +419,12 @@ and align_tree nal isgoal (e,c as rhs) sigma = match nal with
| [] -> [Id.Set.empty,[],rhs]
| na::nal ->
match EConstr.kind sigma c with
- | Case (ci,p,iv,c,cl) when
+ | Case (ci,u,pms,p,iv,c,cl) when
eq_constr sigma c (mkRel (List.index Name.equal na (fst (snd e))))
&& not (Int.equal (Array.length cl) 0)
&& (* don't contract if p dependent *)
- computable sigma p (List.length ci.ci_pp_info.ind_tags) (* FIXME: can do better *) ->
+ computable sigma p (* FIXME: can do better *) ->
+ let (ci, _, _, _, cl) = EConstr.expand_case (snd (snd e)) sigma (ci, u, pms, p, iv, c, cl) in
let clauses = build_tree na isgoal e sigma ci cl in
List.flatten
(List.map (fun (ids,pat,rhs) ->
@@ -788,8 +779,9 @@ and detype_r d flags avoid env sigma t =
GRef (GlobRef.IndRef ind_sp, detype_instance sigma u)
| Construct (cstr_sp,u) ->
GRef (GlobRef.ConstructRef cstr_sp, detype_instance sigma u)
- | Case (ci,p,iv,c,bl) ->
- let comp = computable sigma p (List.length (ci.ci_pp_info.ind_tags)) in
+ | Case (ci,u,pms,p,iv,c,bl) ->
+ let comp = computable sigma p in
+ let (ci, p, iv, c, bl) = EConstr.expand_case (snd env) sigma (ci, u, pms, p, iv, c, bl) in
detype_case comp (detype d flags avoid env sigma)
(detype_eqns d flags avoid env sigma ci comp)
(is_nondep_branch sigma) avoid
diff --git a/pretyping/evarconv.ml b/pretyping/evarconv.ml
index 4b0974ae03..990e84e5a7 100644
--- a/pretyping/evarconv.ml
+++ b/pretyping/evarconv.ml
@@ -206,7 +206,7 @@ let occur_rigidly flags env evd (evk,_) t =
if rigid_normal_occ b' || rigid_normal_occ t' then Rigid true
else Reducible
| Rel _ | Var _ -> Reducible
- | Case (_,_,_,c,_) ->
+ | Case (_,_,_,_,_,c,_) ->
(match aux c with
| Rigid b -> Rigid b
| _ -> Reducible)
@@ -381,7 +381,10 @@ let rec ise_stack2 no_app env evd f sk1 sk2 =
else None, x in
match revsk1, revsk2 with
| [], [] -> None, Success i
- | Stack.Case (_,t1,_,c1)::q1, Stack.Case (_,t2,_,c2)::q2 ->
+ | Stack.Case (ci1,u1,pms1,t1,iv1,c1)::q1, Stack.Case (ci2,u2,pms2,t2,iv2,c2)::q2 ->
+ let dummy = mkProp in
+ let (_, t1, _, _, c1) = EConstr.expand_case env evd (ci1,u1,pms1,t1,iv1,dummy,c1) in
+ let (_, t2, _, _, c2) = EConstr.expand_case env evd (ci2,u2,pms2,t2,iv2,dummy,c2) in
begin
match ise_and i [
(fun i -> f env i CONV t1 t2);
@@ -418,7 +421,10 @@ let rec exact_ise_stack2 env evd f sk1 sk2 =
let rec ise_rev_stack2 i revsk1 revsk2 =
match revsk1, revsk2 with
| [], [] -> Success i
- | Stack.Case (_,t1,_,c1)::q1, Stack.Case (_,t2,_,c2)::q2 ->
+ | Stack.Case (ci1,u1,pms1,t1,iv1,c1)::q1, Stack.Case (ci2,u2,pms2,t2,iv2,c2)::q2 ->
+ let dummy = mkProp in
+ let (_, t1, _, _, c1) = EConstr.expand_case env evd (ci1,u1,pms1,t1,iv1,dummy,c1) in
+ let (_, t2, _, _, c2) = EConstr.expand_case env evd (ci2,u2,pms2,t2,iv2,dummy,c2) in
ise_and i [
(fun i -> ise_rev_stack2 i q1 q2);
(fun i -> ise_array2 i (fun ii -> f env ii CONV) c1 c2);
@@ -1278,7 +1284,7 @@ let apply_on_subterm env evd fixed f test c t =
if occur_evars !evdref !fixedref t then
match EConstr.kind !evdref t with
| Evar (ev, args) when Evar.Set.mem ev !fixedref -> t
- | _ -> map_constr_with_binders_left_to_right !evdref
+ | _ -> map_constr_with_binders_left_to_right env !evdref
(fun d (env,(k,c)) -> (push_rel d env, (k+1,lift 1 c)))
applyrec acc t
else
@@ -1293,7 +1299,7 @@ let apply_on_subterm env evd fixed f test c t =
evdref := evd'; t')
else (
if debug_ho_unification () then Feedback.msg_debug (Pp.str "failed");
- map_constr_with_binders_left_to_right !evdref
+ map_constr_with_binders_left_to_right env !evdref
(fun d (env,(k,c)) -> (push_rel d env, (k+1,lift 1 c)))
applyrec acc t))
in
@@ -1383,7 +1389,7 @@ let thin_evars env sigma sign c =
if not (Id.Set.mem id ctx) then raise (TypingFailed !sigma)
else t
| _ ->
- map_constr_with_binders_left_to_right !sigma
+ map_constr_with_binders_left_to_right env !sigma
(fun d (env,acc) -> (push_rel d env, acc+1))
applyrec (env,acc) t
in
diff --git a/pretyping/evarsolve.ml b/pretyping/evarsolve.ml
index f9f6f74a66..cb3eef9df0 100644
--- a/pretyping/evarsolve.ml
+++ b/pretyping/evarsolve.ml
@@ -232,7 +232,7 @@ let recheck_applications unify flags env evdref t =
else ()
in aux 0 fty
| _ ->
- iter_with_full_binders !evdref (fun d env -> push_rel d env) aux env t
+ iter_with_full_binders env !evdref (fun d env -> push_rel d env) aux env t
in aux env t
@@ -304,7 +304,7 @@ let noccur_evar env evd evk c =
| LocalAssum _ -> ()
| LocalDef (_,b,_) -> cache := Int.Set.add (i-k) !cache; occur_rec false acc (lift i (EConstr.of_constr b)))
| Proj (p,c) -> occur_rec true acc c
- | _ -> iter_with_full_binders evd (fun rd (k,env) -> (succ k, push_rel rd env))
+ | _ -> iter_with_full_binders env evd (fun rd (k,env) -> (succ k, push_rel rd env))
(occur_rec check_types) acc c
in
try occur_rec false (0,env) c; true with Occur -> false
@@ -490,14 +490,14 @@ let expansion_of_var sigma aliases x =
| Some a, _ -> (true, Alias.repr sigma a)
| None, a :: _ -> (true, Some a)
-let rec expand_vars_in_term_using sigma aliases t = match EConstr.kind sigma t with
+let rec expand_vars_in_term_using env sigma aliases t = match EConstr.kind sigma t with
| Rel n -> of_alias (normalize_alias sigma aliases (RelAlias n))
| Var id -> of_alias (normalize_alias sigma aliases (VarAlias id))
| _ ->
- let self aliases c = expand_vars_in_term_using sigma aliases c in
- map_constr_with_full_binders sigma (extend_alias sigma) self aliases t
+ let self aliases c = expand_vars_in_term_using env sigma aliases c in
+ map_constr_with_full_binders env sigma (extend_alias sigma) self aliases t
-let expand_vars_in_term env sigma = expand_vars_in_term_using sigma (make_alias_map env sigma)
+let expand_vars_in_term env sigma = expand_vars_in_term_using env sigma (make_alias_map env sigma)
let free_vars_and_rels_up_alias_expansion env sigma aliases c =
let acc1 = ref Int.Set.empty and acc2 = ref Id.Set.empty in
@@ -533,7 +533,7 @@ let free_vars_and_rels_up_alias_expansion env sigma aliases c =
| Const _ | Ind _ | Construct _ ->
acc2 := Id.Set.union (vars_of_global env (fst @@ EConstr.destRef sigma c)) !acc2
| _ ->
- iter_with_full_binders sigma
+ iter_with_full_binders env sigma
(fun d (aliases,depth) -> (extend_alias sigma d aliases,depth+1))
frec (aliases,depth) c
in
@@ -1645,7 +1645,7 @@ let rec invert_definition unify flags choose imitate_defs
let candidates =
try
let t =
- map_constr_with_full_binders !evdref (fun d (env,k) -> push_rel d env, k+1)
+ map_constr_with_full_binders env' !evdref (fun d (env,k) -> push_rel d env, k+1)
imitate envk t in
(* Less dependent solutions come last *)
l@[t]
@@ -1659,7 +1659,7 @@ let rec invert_definition unify flags choose imitate_defs
evar'')
| None ->
(* Evar/Rigid problem (or assimilated if not normal): we "imitate" *)
- map_constr_with_full_binders !evdref (fun d (env,k) -> push_rel d env, k+1)
+ map_constr_with_full_binders env' !evdref (fun d (env,k) -> push_rel d env, k+1)
imitate envk t
in
let rhs = whd_beta env evd rhs (* heuristic *) in
diff --git a/pretyping/find_subterm.ml b/pretyping/find_subterm.ml
index 52e3364109..9f84b7683f 100644
--- a/pretyping/find_subterm.ml
+++ b/pretyping/find_subterm.ml
@@ -73,7 +73,7 @@ type 'a testing_function = {
(b,l), b=true means no occurrence except the ones in l and b=false,
means all occurrences except the ones in l *)
-let replace_term_occ_gen_modulo sigma occs like_first test bywhat cl occ t =
+let replace_term_occ_gen_modulo env sigma occs like_first test bywhat cl occ t =
let count = ref (Locusops.initialize_occurrence_counter occs) in
let nested = ref false in
let add_subst pos t subst =
@@ -107,23 +107,23 @@ let replace_term_occ_gen_modulo sigma occs like_first test bywhat cl occ t =
with NotUnifiable _ ->
subst_below k t
and subst_below k t =
- map_constr_with_binders_left_to_right sigma (fun d k -> k+1) substrec k t
+ map_constr_with_binders_left_to_right env sigma (fun d k -> k+1) substrec k t
in
let t' = substrec 0 t in
(!count, t')
-let replace_term_occ_modulo evd occs test bywhat t =
+let replace_term_occ_modulo env evd occs test bywhat t =
let occs',like_first =
match occs with AtOccs occs -> occs,false | LikeFirst -> AllOccurrences,true in
proceed_with_occurrences
- (replace_term_occ_gen_modulo evd occs' like_first test bywhat None) occs' t
+ (replace_term_occ_gen_modulo env evd occs' like_first test bywhat None) occs' t
-let replace_term_occ_decl_modulo evd occs test bywhat d =
+let replace_term_occ_decl_modulo env evd occs test bywhat d =
let (plocs,hyploc),like_first =
match occs with AtOccs occs -> occs,false | LikeFirst -> (AllOccurrences,InHyp),true in
proceed_with_occurrences
(map_named_declaration_with_hyploc
- (replace_term_occ_gen_modulo evd plocs like_first test bywhat)
+ (replace_term_occ_gen_modulo env evd plocs like_first test bywhat)
hyploc)
plocs d
@@ -145,7 +145,7 @@ let make_eq_univs_test env evd c =
let subst_closed_term_occ env evd occs c t =
let test = make_eq_univs_test env evd c in
let bywhat () = mkRel 1 in
- let t' = replace_term_occ_modulo evd occs test bywhat t in
+ let t' = replace_term_occ_modulo env evd occs test bywhat t in
t', test.testing_state
let subst_closed_term_occ_decl env evd occs c d =
@@ -155,6 +155,6 @@ let subst_closed_term_occ_decl env evd occs c d =
let bywhat () = mkRel 1 in
proceed_with_occurrences
(map_named_declaration_with_hyploc
- (fun _ -> replace_term_occ_gen_modulo evd plocs like_first test bywhat None)
+ (fun _ -> replace_term_occ_gen_modulo env evd plocs like_first test bywhat None)
hyploc) plocs d,
test.testing_state
diff --git a/pretyping/find_subterm.mli b/pretyping/find_subterm.mli
index 1ddae01e2b..c71cb207ab 100644
--- a/pretyping/find_subterm.mli
+++ b/pretyping/find_subterm.mli
@@ -43,13 +43,13 @@ val make_eq_univs_test : env -> evar_map -> constr -> evar_map testing_function
matching subterms at the indicated occurrences [occl] with [mk
()]; it turns a NotUnifiable exception raised by the testing
function into a SubtermUnificationError. *)
-val replace_term_occ_modulo : evar_map -> occurrences or_like_first ->
+val replace_term_occ_modulo : env -> evar_map -> occurrences or_like_first ->
'a testing_function -> (unit -> constr) -> constr -> constr
(** [replace_term_occ_decl_modulo] is similar to
[replace_term_occ_modulo] but for a named_declaration. *)
val replace_term_occ_decl_modulo :
- evar_map ->
+ env -> evar_map ->
(occurrences * hyp_location_flag) or_like_first ->
'a testing_function -> (unit -> constr) ->
named_declaration -> named_declaration
diff --git a/pretyping/heads.ml b/pretyping/heads.ml
index a012f1cb15..f6e45613e1 100644
--- a/pretyping/heads.ml
+++ b/pretyping/heads.ml
@@ -76,7 +76,7 @@ and kind_of_head env t =
| App (c,al) -> aux k (Array.to_list al @ l) c b
| Proj (p,c) -> RigidHead RigidOther
- | Case (_,_,_,c,_) -> aux k [] c true
+ | Case (_,_,_,_,_,c,_) -> aux k [] c true
| Int _ | Float _ | Array _ -> ConstructorHead
| Fix ((i,j),_) ->
let n = i.(j) in
diff --git a/pretyping/indrec.ml b/pretyping/indrec.ml
index 5ffd919312..dd7cf8abaa 100644
--- a/pretyping/indrec.ml
+++ b/pretyping/indrec.ml
@@ -122,12 +122,24 @@ let mis_make_case_com dep env sigma (ind, u as pind) (mib,mip as specif) kind =
| None ->
let iv = make_case_invert env (find_rectype env sigma (EConstr.of_constr (lift 1 depind))) ci in
let iv = EConstr.Unsafe.to_case_invert iv in
- mkCase (ci, lift ndepar p, iv, mkRel 1, Termops.rel_vect ndepar k)
+ let ncons = Array.length mip.mind_consnames in
+ let mk_branch i =
+ (* eta-expansion to please branch contraction *)
+ let ft = get_type (lookup_rel (ncons - i) env) in
+ (* we need that to get the generated names for the branch *)
+ let (ctx, _) = decompose_prod_assum ft in
+ let n = mkRel (List.length ctx + 1) in
+ let args = Context.Rel.to_extended_vect mkRel 0 ctx in
+ let br = it_mkLambda_or_LetIn (mkApp (n, args)) ctx in
+ lift (ndepar + ncons - i - 1) br
+ in
+ let br = Array.init ncons mk_branch in
+ mkCase (Inductive.contract_case env (ci, lift ndepar p, iv, mkRel 1, br))
| Some ps ->
let term =
mkApp (mkRel 2,
- Array.map
- (fun p -> mkProj (Projection.make p true, mkRel 1)) ps) in
+ Array.map
+ (fun p -> mkProj (Projection.make p true, mkRel 1)) ps) in
if dep then
let ty = mkApp (mkRel 3, [| mkRel 1 |]) in
mkCast (term, DEFAULTcast, ty)
diff --git a/pretyping/inductiveops.ml b/pretyping/inductiveops.ml
index bd875cf68b..04feae35d8 100644
--- a/pretyping/inductiveops.ml
+++ b/pretyping/inductiveops.ml
@@ -356,8 +356,7 @@ let make_case_or_project env sigma indt ci pred c branches =
let IndType (((ind,_),_),_) = indt in
let projs = get_projections env ind in
match projs with
- | None ->
- mkCase (ci, pred, make_case_invert env indt ci, c, branches)
+ | None -> (mkCase (EConstr.contract_case env sigma (ci, pred, make_case_invert env indt ci, c, branches)))
| Some ps ->
assert(Array.length branches == 1);
let na, ty, t = destLambda sigma pred in
@@ -749,6 +748,6 @@ let control_only_guard env sigma c =
in
let rec iter env c =
check_fix_cofix env c;
- EConstr.iter_with_full_binders sigma EConstr.push_rel iter env c
+ EConstr.iter_with_full_binders env sigma EConstr.push_rel iter env c
in
iter env c
diff --git a/pretyping/inductiveops.mli b/pretyping/inductiveops.mli
index 3705d39280..8e83814fa0 100644
--- a/pretyping/inductiveops.mli
+++ b/pretyping/inductiveops.mli
@@ -213,7 +213,7 @@ val make_case_or_project :
(* pred *) EConstr.constr -> (* term *) EConstr.constr -> (* branches *) EConstr.constr array -> EConstr.constr
val make_case_invert : env -> inductive_type -> case_info
- -> (EConstr.constr,EConstr.EInstance.t) case_invert
+ -> EConstr.case_invert
(*i Compatibility
val make_default_case_info : env -> case_style -> inductive -> case_info
diff --git a/pretyping/nativenorm.ml b/pretyping/nativenorm.ml
index d06d6e01d1..8da615acfc 100644
--- a/pretyping/nativenorm.ml
+++ b/pretyping/nativenorm.ml
@@ -343,7 +343,8 @@ and nf_atom_type env sigma atom =
in
let branchs = Array.mapi mkbranch bsw in
let tcase = build_case_type p realargs a in
- mkCase(ans.asw_ci, p, iv, a, branchs), tcase
+ let ci = ans.asw_ci in
+ mkCase (Inductive.contract_case env (ci, p, iv, a, branchs)), tcase
| Afix(tt,ft,rp,s) ->
let tt = Array.map (fun t -> nf_type_sort env sigma t) tt in
let tt = Array.map fst tt and rt = Array.map snd tt in
diff --git a/pretyping/patternops.ml b/pretyping/patternops.ml
index b259945d9e..47097a0e32 100644
--- a/pretyping/patternops.ml
+++ b/pretyping/patternops.ml
@@ -202,7 +202,8 @@ let pattern_of_constr env sigma t =
| Evar_kinds.MatchingVar (Evar_kinds.SecondOrderPatVar ido) -> assert false
| _ ->
PMeta None)
- | Case (ci,p,_,a,br) ->
+ | Case (ci, u, pms, p, iv, a, br) ->
+ let (ci, p, iv, a, br) = Inductive.expand_case env (ci, u, pms, p, iv, a, br) in
let cip =
{ cip_style = ci.ci_pp_info.style;
cip_ind = Some ci.ci_ind;
@@ -213,7 +214,7 @@ let pattern_of_constr env sigma t =
(i, ci.ci_pp_info.cstr_tags.(i), pattern_of_constr env c)
in
PCase (cip, pattern_of_constr env p, pattern_of_constr env a,
- Array.to_list (Array.mapi branch_of_constr br))
+ Array.to_list (Array.mapi branch_of_constr br))
| Fix (lni,(lna,tl,bl)) ->
let push env na2 c2 = push_rel (LocalAssum (na2,c2)) env in
let env' = Array.fold_left2 push env lna tl in
diff --git a/pretyping/pretyping.ml b/pretyping/pretyping.ml
index 9dbded75ba..e86a8a28c9 100644
--- a/pretyping/pretyping.ml
+++ b/pretyping/pretyping.ml
@@ -1043,7 +1043,7 @@ struct
if not record then
let f = it_mkLambda_or_LetIn f fsign in
let ci = make_case_info !!env (ind_of_ind_type indt) rci LetStyle in
- mkCase (ci, p, make_case_invert !!env indt ci, cj.uj_val,[|f|])
+ mkCase (EConstr.contract_case !!env sigma (ci, p, make_case_invert !!env indt ci, cj.uj_val,[|f|]))
else it_mkLambda_or_LetIn f fsign
in
(* Make dependencies from arity signature impossible *)
@@ -1159,7 +1159,7 @@ struct
let pred = nf_evar sigma pred in
let rci = Typing.check_allowed_sort !!env sigma ind cj.uj_val pred in
let ci = make_case_info !!env (fst ind) rci IfStyle in
- mkCase (ci, pred, make_case_invert !!env indty ci, cj.uj_val, [|b1;b2|])
+ mkCase (EConstr.contract_case !!env sigma (ci, pred, make_case_invert !!env indty ci, cj.uj_val, [|b1;b2|]))
in
let cj = { uj_val = v; uj_type = p } in
discard_trace @@ inh_conv_coerce_to_tycon ?loc ~program_mode resolve_tc env sigma cj tycon
diff --git a/pretyping/reductionops.ml b/pretyping/reductionops.ml
index 52f60fbc5e..85214eb245 100644
--- a/pretyping/reductionops.ml
+++ b/pretyping/reductionops.ml
@@ -177,9 +177,12 @@ sig
type 'a app_node
val pr_app_node : ('a -> Pp.t) -> 'a app_node -> Pp.t
+ type 'a case_stk =
+ case_info * EInstance.t * 'a array * 'a pcase_return * ('a, EInstance.t) pcase_invert * 'a pcase_branch array
+
type 'a member =
| App of 'a app_node
- | Case of case_info * 'a * ('a, EInstance.t) case_invert * 'a array
+ | Case of 'a case_stk
| Proj of Projection.t
| Fix of ('a, 'a) pfixpoint * 'a t
| Primitive of CPrimitives.t * (Constant.t * EInstance.t) * 'a t * CPrimitives.args_red
@@ -230,9 +233,12 @@ struct
)
+ type 'a case_stk =
+ case_info * EInstance.t * 'a array * 'a pcase_return * ('a, EInstance.t) pcase_invert * 'a pcase_branch array
+
type 'a member =
| App of 'a app_node
- | Case of case_info * 'a * ('a, EInstance.t) case_invert * 'a array
+ | Case of 'a case_stk
| Proj of Projection.t
| Fix of ('a, 'a) pfixpoint * 'a t
| Primitive of CPrimitives.t * (Constant.t * EInstance.t) * 'a t * CPrimitives.args_red
@@ -245,9 +251,9 @@ struct
let pr_c x = hov 1 (pr_c x) in
match member with
| App app -> str "ZApp" ++ pr_app_node pr_c app
- | Case (_,_,_,br) ->
+ | Case (_,_,_,_,_,br) ->
str "ZCase(" ++
- prvect_with_sep (pr_bar) pr_c br
+ prvect_with_sep (pr_bar) (fun (_, c) -> pr_c c) br
++ str ")"
| Proj p ->
str "ZProj(" ++ Constant.debug_print (Projection.constant p) ++ str ")"
@@ -284,7 +290,7 @@ struct
([],[]) -> Int.equal bal 0
| (App (i,_,j)::s1, _) -> compare_rec (bal + j + 1 - i) s1 stk2
| (_, App (i,_,j)::s2) -> compare_rec (bal - j - 1 + i) stk1 s2
- | (Case(c1,_,_,_)::s1, Case(c2,_,_,_)::s2) ->
+ | (Case _ :: s1, Case _::s2) ->
Int.equal bal 0 (* && c1.ci_ind = c2.ci_ind *) && compare_rec 0 s1 s2
| (Proj (p)::s1, Proj(p2)::s2) ->
Int.equal bal 0 && compare_rec 0 s1 s2
@@ -304,8 +310,9 @@ struct
let t1,l1 = decomp_node_last n1 q1 in
let t2,l2 = decomp_node_last n2 q2 in
aux (f o t1 t2) l1 l2
- | Case (_,t1,_,a1) :: q1, Case (_,t2,_,a2) :: q2 ->
- aux (Array.fold_left2 f (f o t1 t2) a1 a2) q1 q2
+ | Case ((_,_,pms1,(_, t1),_,a1)) :: q1, Case ((_,_,pms2, (_, t2),_,a2)) :: q2 ->
+ let f' o (_, t1) (_, t2) = f o t1 t2 in
+ aux (Array.fold_left2 f' (f (Array.fold_left2 f o pms1 pms2) t1 t2) a1 a2) q1 q2
| Proj (p1) :: q1, Proj (p2) :: q2 ->
aux o q1 q2
| Fix ((_,(_,a1,b1)),s1) :: q1, Fix ((_,(_,a2,b2)),s2) :: q2 ->
@@ -320,8 +327,8 @@ struct
| App (i,a,j) ->
let le = j - i + 1 in
App (0,Array.map f (Array.sub a i le), le-1)
- | Case (info,ty,iv,br) ->
- Case (info, f ty, map_invert f iv, Array.map f br)
+ | Case (info,u,pms,ty,iv,br) ->
+ Case (info, u, Array.map f pms, on_snd f ty, iv, Array.map (on_snd f) br)
| Fix ((r,(na,ty,bo)),arg) ->
Fix ((r,(na,Array.map f ty, Array.map f bo)),map f arg)
| Primitive (p,c,args,kargs) ->
@@ -408,7 +415,7 @@ struct
then a
else Array.sub a i (j - i + 1) in
zip (mkApp (f, a'), s)
- | f, (Case (ci,rt,iv,br)::s) -> zip (mkCase (ci,rt,iv,f,br), s)
+ | f, (Case (ci,u,pms,rt,iv,br)::s) -> zip (mkCase (ci,u,pms,rt,iv,f,br), s)
| f, (Fix (fix,st)::s) -> zip
(mkFix fix, st @ (append_app [|f|] s))
| f, (Proj (p)::s) -> zip (mkProj (p,f),s)
@@ -469,13 +476,13 @@ let strong_with_flags whdfun flags env sigma t =
| d -> d in
push_rel d env in
let rec strongrec env t =
- map_constr_with_full_binders sigma
+ map_constr_with_full_binders env sigma
push_rel_check_zeta strongrec env (whdfun flags env sigma t) in
strongrec env t
let strong whdfun env sigma t =
let rec strongrec env t =
- map_constr_with_full_binders sigma push_rel strongrec env (whdfun env sigma t) in
+ map_constr_with_full_binders env sigma push_rel strongrec env (whdfun env sigma t) in
strongrec env t
(*************************************)
@@ -702,6 +709,20 @@ let debug_RAKAM =
~key:["Debug";"RAKAM"]
~value:false
+let apply_branch env sigma (ind, i) args (ci, u, pms, iv, r, lf) =
+ let args = Stack.tail ci.ci_npar args in
+ let args = Option.get (Stack.list_of_app_stack args) in
+ let br = lf.(i - 1) in
+ let subst =
+ if Int.equal ci.ci_cstr_nargs.(i - 1) ci.ci_cstr_ndecls.(i - 1) then
+ (* No let-bindings *)
+ List.rev args
+ else
+ let ctx = expand_branch env sigma u pms (ind, i) br in
+ subst_of_rel_context_instance ctx args
+ in
+ Vars.substl subst (snd br)
+
let rec whd_state_gen flags env sigma =
let open Context.Named.Declaration in
let rec whrec (x, stack) : state =
@@ -785,8 +806,8 @@ let rec whd_state_gen flags env sigma =
| _ -> fold ())
| _ -> fold ())
- | Case (ci,p,iv,d,lf) ->
- whrec (d, Stack.Case (ci,p,iv,lf) :: stack)
+ | Case (ci,u,pms,p,iv,d,lf) ->
+ whrec (d, Stack.Case (ci,u,pms,p,iv,lf) :: stack)
| Fix ((ri,n),_ as f) ->
(match Stack.strip_n_app ri.(n) stack with
@@ -794,13 +815,14 @@ let rec whd_state_gen flags env sigma =
|Some (bef,arg,s') ->
whrec (arg, Stack.Fix(f,bef)::s'))
- | Construct ((ind,c),u) ->
+ | Construct (cstr ,u) ->
let use_match = CClosure.RedFlags.red_set flags CClosure.RedFlags.fMATCH in
let use_fix = CClosure.RedFlags.red_set flags CClosure.RedFlags.fFIX in
if use_match || use_fix then
match Stack.strip_app stack with
- |args, (Stack.Case(ci, _, _, lf)::s') when use_match ->
- whrec (lf.(c-1), (Stack.tail ci.ci_npar args) @ s')
+ |args, (Stack.Case case::s') when use_match ->
+ let r = apply_branch env sigma cstr args case in
+ whrec (r, s')
|args, (Stack.Proj (p)::s') when use_match ->
whrec (Stack.nth args (Projection.npars p + Projection.arg p), s')
|args, (Stack.Fix (f,s')::s'') when use_fix ->
@@ -850,7 +872,7 @@ let rec whd_state_gen flags env sigma =
whrec
(** reduction machine without global env and refold machinery *)
-let local_whd_state_gen flags _env sigma =
+let local_whd_state_gen flags env sigma =
let rec whrec (x, stack) =
let c0 = EConstr.kind sigma x in
let s = (EConstr.of_kind c0, stack) in
@@ -882,8 +904,8 @@ let local_whd_state_gen flags _env sigma =
| Proj (p,c) when CClosure.RedFlags.red_projection flags p ->
(whrec (c, Stack.Proj (p) :: stack))
- | Case (ci,p,iv,d,lf) ->
- whrec (d, Stack.Case (ci,p,iv,lf) :: stack)
+ | Case (ci,u,pms,p,iv,d,lf) ->
+ whrec (d, Stack.Case (ci,u,pms,p,iv,lf) :: stack)
| Fix ((ri,n),_ as f) ->
(match Stack.strip_n_app ri.(n) stack with
@@ -896,13 +918,14 @@ let local_whd_state_gen flags _env sigma =
Some c -> whrec (c,stack)
| None -> s)
- | Construct ((ind,c),u) ->
+ | Construct (cstr, u) ->
let use_match = CClosure.RedFlags.red_set flags CClosure.RedFlags.fMATCH in
let use_fix = CClosure.RedFlags.red_set flags CClosure.RedFlags.fFIX in
if use_match || use_fix then
match Stack.strip_app stack with
- |args, (Stack.Case(ci, _, _, lf)::s') when use_match ->
- whrec (lf.(c-1), (Stack.tail ci.ci_npar args) @ s')
+ |args, (Stack.Case case :: s') when use_match ->
+ let r = apply_branch env sigma cstr args case in
+ whrec (r, s')
|args, (Stack.Proj (p) :: s') when use_match ->
whrec (Stack.nth args (Projection.npars p + Projection.arg p), s')
|args, (Stack.Fix (f,s')::s'') when use_fix ->
diff --git a/pretyping/reductionops.mli b/pretyping/reductionops.mli
index ae93eb48b4..e60def72f6 100644
--- a/pretyping/reductionops.mli
+++ b/pretyping/reductionops.mli
@@ -57,9 +57,12 @@ module Stack : sig
val pr_app_node : ('a -> Pp.t) -> 'a app_node -> Pp.t
+ type 'a case_stk =
+ case_info * EInstance.t * 'a array * 'a pcase_return * ('a, EInstance.t) pcase_invert * 'a pcase_branch array
+
type 'a member =
| App of 'a app_node
- | Case of case_info * 'a * ('a, EInstance.t) case_invert * 'a array
+ | Case of 'a case_stk
| Proj of Projection.t
| Fix of ('a, 'a) pfixpoint * 'a t
| Primitive of CPrimitives.t * (Constant.t * EInstance.t) * 'a t * CPrimitives.args_red
diff --git a/pretyping/retyping.ml b/pretyping/retyping.ml
index 34bcd0982c..064990f6bf 100644
--- a/pretyping/retyping.ml
+++ b/pretyping/retyping.ml
@@ -129,7 +129,8 @@ let retype ?(polyprop=true) sigma =
| Evar ev -> existential_type sigma ev
| Ind (ind, u) -> EConstr.of_constr (rename_type_of_inductive env (ind, EInstance.kind sigma u))
| Construct (cstr, u) -> EConstr.of_constr (rename_type_of_constructor env (cstr, EInstance.kind sigma u))
- | Case (_,p,_iv,c,lf) ->
+ | Case (ci,u,pms,p,iv,c,lf) ->
+ let (_,p,iv,c,lf) = EConstr.expand_case env sigma (ci,u,pms,p,iv,c,lf) in
let Inductiveops.IndType(indf,realargs) =
let t = type_of env c in
try Inductiveops.find_rectype env sigma t
@@ -309,7 +310,7 @@ let relevance_of_term env sigma c =
| Const (c,_) -> Relevanceops.relevance_of_constant env c
| Ind _ -> Sorts.Relevant
| Construct (c,_) -> Relevanceops.relevance_of_constructor env c
- | Case (ci, _, _, _, _) -> ci.ci_relevance
+ | Case (ci, _, _, _, _, _, _) -> ci.ci_relevance
| Fix ((_,i),(lna,_,_)) -> (lna.(i)).binder_relevance
| CoFix (i,(lna,_,_)) -> (lna.(i)).binder_relevance
| Proj (p, _) -> Relevanceops.relevance_of_projection env p
diff --git a/pretyping/tacred.ml b/pretyping/tacred.ml
index 411fb0cd89..01819a650b 100644
--- a/pretyping/tacred.ml
+++ b/pretyping/tacred.ml
@@ -296,8 +296,8 @@ let compute_consteval_direct env sigma ref =
| Fix fix when not onlyproj ->
(try check_fix_reversibility sigma labs l fix
with Elimconst -> NotAnElimination)
- | Case (_,_,_,d,_) when isRel sigma d && not onlyproj -> EliminationCases n
- | Case (_,_,_,d,_) -> srec env n labs true d
+ | Case (_,_,_,_,_,d,_) when isRel sigma d && not onlyproj -> EliminationCases n
+ | Case (_,_,_,_,_,d,_) -> srec env n labs true d
| Proj (p, d) when isRel sigma d -> EliminationProj n
| _ -> NotAnElimination
in
@@ -478,29 +478,36 @@ let contract_cofix_use_function env sigma f
sigma (nf_beta env sigma bodies.(bodynum))
type 'a miota_args = {
- mP : constr; (** the result type *)
+ mU : EInstance.t; (* Universe instance of the return clause *)
+ mParams : constr array; (* Parameters of the inductive *)
+ mP : case_return; (* the result type *)
mconstr : constr; (** the constructor *)
mci : case_info; (** special info to re-build pattern *)
mcargs : 'a list; (** the constructor's arguments *)
- mlf : 'a array } (** the branch code vector *)
+ mlf : 'a pcase_branch array } (** the branch code vector *)
-let reduce_mind_case sigma mia =
+let reduce_mind_case env sigma mia =
match EConstr.kind sigma mia.mconstr with
- | Construct ((ind_sp,i),u) ->
-(* let ncargs = (fst mia.mci).(i-1) in*)
+ | Construct ((_, i as cstr), u) ->
let real_cargs = List.skipn mia.mci.ci_npar mia.mcargs in
- applist (mia.mlf.(i-1),real_cargs)
+ let br = mia.mlf.(i - 1) in
+ let ctx = EConstr.expand_branch env sigma mia.mU mia.mParams cstr br in
+ let br = it_mkLambda_or_LetIn (snd br) ctx in
+ applist (br, real_cargs)
| CoFix cofix ->
let cofix_def = contract_cofix sigma cofix in
(* XXX Is NoInvert OK here? *)
- mkCase (mia.mci, mia.mP, NoInvert, applist(cofix_def,mia.mcargs), mia.mlf)
+ mkCase (mia.mci, mia.mU, mia.mParams, mia.mP, NoInvert, applist(cofix_def,mia.mcargs), mia.mlf)
| _ -> assert false
let reduce_mind_case_use_function func env sigma mia =
match EConstr.kind sigma mia.mconstr with
- | Construct ((ind_sp,i),u) ->
+ | Construct ((_, i as cstr),u) ->
let real_cargs = List.skipn mia.mci.ci_npar mia.mcargs in
- applist (mia.mlf.(i-1), real_cargs)
+ let br = mia.mlf.(i - 1) in
+ let ctx = EConstr.expand_branch env sigma mia.mU mia.mParams cstr br in
+ let br = it_mkLambda_or_LetIn (snd br) ctx in
+ applist (br, real_cargs)
| CoFix (bodynum,(names,_,_) as cofix) ->
let build_cofix_name =
if isConst sigma func then
@@ -526,8 +533,7 @@ let reduce_mind_case_use_function func env sigma mia =
fun _ -> None in
let cofix_def =
contract_cofix_use_function env sigma build_cofix_name cofix in
- (* Is NoInvert OK here? *)
- mkCase (mia.mci, mia.mP, NoInvert, applist(cofix_def,mia.mcargs), mia.mlf)
+ mkCase (mia.mci, mia.mU, mia.mParams, mia.mP, NoInvert, applist(cofix_def,mia.mcargs), mia.mlf)
| _ -> assert false
@@ -728,9 +734,9 @@ and whd_simpl_stack env sigma =
| LetIn (n,b,t,c) -> redrec (Vars.substl [b] c, stack)
| App (f,cl) -> assert false (* see push_app above *)
| Cast (c,_,_) -> redrec (c, stack)
- | Case (ci,p,iv,c,lf) ->
+ | Case (ci,u,pms,p,iv,c,lf) ->
(try
- redrec (special_red_case env sigma (ci,p,iv,c,lf), stack)
+ redrec (special_red_case env sigma (ci,u,pms,p,iv,c,lf), stack)
with
Redelimination -> s')
| Fix fix ->
@@ -842,15 +848,15 @@ and reduce_proj env sigma c =
let proj_narg = Projection.npars proj + Projection.arg proj in
List.nth cargs proj_narg
| _ -> raise Redelimination)
- | Case (n,p,iv,c,brs) ->
+ | Case (n,u,pms,p,iv,c,brs) ->
let c' = redrec c in
- let p = (n,p,iv,c',brs) in
+ let p = (n,u,pms,p,iv,c',brs) in
(try special_red_case env sigma p
with Redelimination -> mkCase p)
| _ -> raise Redelimination
in redrec c
-and special_red_case env sigma (ci, p, iv, c, lf) =
+and special_red_case env sigma (ci, u, pms, p, iv, c, lf) =
let rec redrec s =
let (constr, cargs) = whd_simpl_stack env sigma s in
match match_eval_ref env sigma constr cargs with
@@ -860,14 +866,14 @@ and special_red_case env sigma (ci, p, iv, c, lf) =
| Some gvalue ->
if reducible_mind_case sigma gvalue then
reduce_mind_case_use_function constr env sigma
- {mP=p; mconstr=gvalue; mcargs=cargs;
+ {mP=p; mU = u; mParams = pms; mconstr=gvalue; mcargs=cargs;
mci=ci; mlf=lf}
else
redrec (gvalue, cargs))
| None ->
if reducible_mind_case sigma constr then
- reduce_mind_case sigma
- {mP=p; mconstr=constr; mcargs=cargs;
+ reduce_mind_case env sigma
+ {mP=p; mU = u; mParams = pms; mconstr=constr; mcargs=cargs;
mci=ci; mlf=lf}
else
raise Redelimination
@@ -915,7 +921,7 @@ let try_red_product env sigma c =
let open Context.Rel.Declaration in
mkProd (x, a, redrec (push_rel (LocalAssum (x, a)) env) b)
| LetIn (x,a,b,t) -> redrec env (Vars.subst1 a t)
- | Case (ci,p,iv,d,lf) -> simpfun (mkCase (ci,p,iv,redrec env d,lf))
+ | Case (ci,u,pms,p,iv,d,lf) -> simpfun (mkCase (ci,u,pms,p,iv,redrec env d,lf))
| Proj (p, c) ->
let c' =
match EConstr.kind sigma c with
@@ -1062,7 +1068,7 @@ let change_map_constr_with_binders_left_to_right g f (env, l as acc) sigma c =
(* Still the same projection, we ignore the change in parameters *)
mkProj (p, a')
else mkApp (app', [| a' |])
- | _ -> map_constr_with_binders_left_to_right sigma g f acc c
+ | _ -> map_constr_with_binders_left_to_right env sigma g f acc c
let e_contextually byhead (occs,c) f = begin fun env sigma t ->
let count = ref (Locusops.initialize_occurrence_counter occs) in
@@ -1131,7 +1137,7 @@ let substlin env sigma evalref occs c =
count := count';
if ok then value u else c
| None ->
- map_constr_with_binders_left_to_right sigma
+ map_constr_with_binders_left_to_right env sigma
(fun _ () -> ())
substrec () c
in
@@ -1295,9 +1301,9 @@ let one_step_reduce env sigma c =
| App (f,cl) -> redrec (f, (Array.to_list cl)@stack)
| LetIn (_,f,_,cl) -> (Vars.subst1 f cl,stack)
| Cast (c,_,_) -> redrec (c,stack)
- | Case (ci,p,iv,c,lf) ->
+ | Case (ci,u,pms,p,iv,c,lf) ->
(try
- (special_red_case env sigma (ci,p,iv,c,lf), stack)
+ (special_red_case env sigma (ci,u,pms,p,iv,c,lf), stack)
with Redelimination -> raise NotStepReducible)
| Fix fix ->
(try match reduce_fix env sigma fix stack with
diff --git a/pretyping/typing.ml b/pretyping/typing.ml
index e3e5244a8c..b0ce4fd63a 100644
--- a/pretyping/typing.ml
+++ b/pretyping/typing.ml
@@ -178,7 +178,7 @@ let type_case_branches env sigma (ind,largs) pj c =
let ty = whd_betaiota env sigma (lambda_applist_assum sigma (n+1) p (realargs@[c])) in
sigma, (lc, ty, Sorts.relevance_of_sort ps)
-let judge_of_case env sigma ci pj iv cj lfj =
+let judge_of_case env sigma case ci pj iv cj lfj =
let ((ind, u), spec) =
try find_mrectype env sigma cj.uj_type
with Not_found -> error_case_not_inductive env sigma cj in
@@ -189,7 +189,7 @@ let judge_of_case env sigma ci pj iv cj lfj =
let () = if (match iv with | NoInvert -> false | CaseInvert _ -> true) != should_invert_case env ci
then Type_errors.error_bad_invert env
in
- sigma, { uj_val = mkCase (ci, pj.uj_val, iv, cj.uj_val, Array.map j_val lfj);
+ sigma, { uj_val = mkCase case;
uj_type = rslty }
let check_type_fixpoint ?loc env sigma lna lar vdefj =
@@ -383,7 +383,9 @@ let rec execute env sigma cstr =
let sigma, ty = type_of_constructor env sigma ctor in
sigma, make_judge cstr ty
- | Case (ci,p,iv,c,lf) ->
+ | Case (ci, u, pms, p, iv, c, lf) ->
+ let case = (ci, u, pms, p, iv, c, lf) in
+ let (ci, p, iv, c, lf) = EConstr.expand_case env sigma case in
let sigma, cj = execute env sigma c in
let sigma, pj = execute env sigma p in
let sigma, lfj = execute_array env sigma lf in
@@ -396,7 +398,7 @@ let rec execute env sigma cstr =
let sigma = check_actual_type env sigma cj tj.utj_val in
sigma
in
- judge_of_case env sigma ci pj iv cj lfj
+ judge_of_case env sigma case ci pj iv cj lfj
| Fix ((vn,i as vni),recdef) ->
let sigma, (_,tys,_ as recdef') = execute_recdef env sigma recdef in
diff --git a/pretyping/unification.ml b/pretyping/unification.ml
index 3d3010d1a4..a845fc3246 100644
--- a/pretyping/unification.ml
+++ b/pretyping/unification.ml
@@ -563,7 +563,7 @@ let is_rigid_head sigma flags t =
| Construct _ | Int _ | Float _ | Array _ -> true
| Fix _ | CoFix _ -> true
| Rel _ | Var _ | Meta _ | Evar _ | Sort _ | Cast (_, _, _) | Prod _
- | Lambda _ | LetIn _ | App (_, _) | Case (_, _, _, _, _)
+ | Lambda _ | LetIn _ | App (_, _) | Case _
| Proj (_, _) -> false (* Why aren't Prod, Sort rigid heads ? *)
let force_eqs c =
@@ -652,7 +652,7 @@ let rec is_neutral env sigma ts t =
not (TransparentState.is_transparent_variable ts id)
| Rel n -> true
| Evar _ | Meta _ -> true
- | Case (_, p, _, c, _) -> is_neutral env sigma ts c
+ | Case (_, _, _, _, _, c, _) -> is_neutral env sigma ts c
| Proj (p, c) -> is_neutral env sigma ts c
| Lambda _ | LetIn _ | Construct _ | CoFix _ | Int _ | Float _ | Array _ -> false
| Sort _ | Cast (_, _, _) | Prod (_, _, _) | Ind _ -> false (* Really? *)
@@ -853,7 +853,9 @@ let rec unify_0_with_initial_metas (sigma,ms,es as subst : subst0) conv_at_top e
unify_app_pattern true curenvnb pb opt substn cM f1 l1 cN f2 l2
| _ -> raise ex)
- | Case (ci1,p1,_,c1,cl1), Case (ci2,p2,_,c2,cl2) ->
+ | Case (ci1, u1, pms1, p1, iv1, c1, cl1), Case (ci2, u2, pms2, p2, iv2, c2, cl2) ->
+ let (ci1, p1, iv1, c1, cl1) = EConstr.expand_case env sigma (ci1, u1, pms1, p1, iv1, c1, cl1) in
+ let (ci2, p2, iv2, c2, cl2) = EConstr.expand_case env sigma (ci2, u2, pms2, p2, iv2, c2, cl2) in
(try
if not (Ind.CanOrd.equal ci1.ci_ind ci2.ci_ind) then error_cannot_unify curenv sigma (cM,cN);
let opt' = {opt with at_top = true; with_types = false} in
@@ -1678,7 +1680,7 @@ let make_abstraction_core name (test,out) env sigma c ty occs check_occs concl =
(push_named_context_val d sign,depdecls)
| (AllOccurrences | AtLeastOneOccurrence), InHyp as occ ->
let occ = if likefirst then LikeFirst else AtOccs occ in
- let newdecl = replace_term_occ_decl_modulo sigma occ test mkvarid d in
+ let newdecl = replace_term_occ_decl_modulo env sigma occ test mkvarid d in
if Context.Named.Declaration.equal (EConstr.eq_constr sigma) d newdecl
&& not (indirectly_dependent sigma c d depdecls)
then
@@ -1689,7 +1691,7 @@ let make_abstraction_core name (test,out) env sigma c ty occs check_occs concl =
(push_named_context_val newdecl sign, newdecl :: depdecls)
| occ ->
(* There are specific occurrences, hence not like first *)
- let newdecl = replace_term_occ_decl_modulo sigma (AtOccs occ) test mkvarid d in
+ let newdecl = replace_term_occ_decl_modulo env sigma (AtOccs occ) test mkvarid d in
(push_named_context_val newdecl sign, newdecl :: depdecls) in
try
let sign,depdecls =
@@ -1699,7 +1701,7 @@ let make_abstraction_core name (test,out) env sigma c ty occs check_occs concl =
| NoOccurrences -> concl
| occ ->
let occ = if likefirst then LikeFirst else AtOccs occ in
- replace_term_occ_modulo sigma occ test mkvarid concl
+ replace_term_occ_modulo env sigma occ test mkvarid concl
in
let lastlhyp =
if List.is_empty depdecls then None else Some (NamedDecl.get_id (List.last depdecls)) in
@@ -1787,11 +1789,11 @@ let w_unify_to_subterm env evd ?(flags=default_unify_flags ()) (op,cl) =
matchrec c1
with ex when precatchable_exception ex ->
matchrec c2)
- | Case(_,_,_,c,lf) -> (* does not search in the predicate *)
+ | Case(_,_,_,_,_,c,lf) -> (* does not search in the predicate *)
(try
matchrec c
with ex when precatchable_exception ex ->
- iter_fail matchrec lf)
+ iter_fail matchrec (Array.map snd lf))
| LetIn(_,c1,_,c2) ->
(try
matchrec c1
@@ -1881,8 +1883,8 @@ let w_unify_to_subterm_all env evd ?(flags=default_unify_flags ()) (op,cl) =
let c2 = args.(n-1) in
bind (matchrec c1) (matchrec c2)
- | Case(_,_,_,c,lf) -> (* does not search in the predicate *)
- bind (matchrec c) (bind_iter matchrec lf)
+ | Case(_,_,_,_,_,c,lf) -> (* does not search in the predicate *)
+ bind (matchrec c) (bind_iter matchrec (Array.map snd lf))
| Proj (p,c) -> matchrec c
diff --git a/pretyping/vnorm.ml b/pretyping/vnorm.ml
index 1420401875..314cada2d7 100644
--- a/pretyping/vnorm.ml
+++ b/pretyping/vnorm.ml
@@ -287,7 +287,7 @@ and nf_stk ?from:(from=0) env sigma c t stk =
CaseInvert {univs=u; args=allargs}
else NoInvert
in
- nf_stk env sigma (mkCase(ci, p, iv, c, branchs)) tcase stk
+ nf_stk env sigma (mkCase (Inductive.contract_case env (ci, p, iv, c, branchs))) tcase stk
| Zproj p :: stk ->
assert (from = 0) ;
let p' = Projection.make p true in
generated by cgit v1.2.3 (git 2.25.1) at 2026-01-31 12:16:43 +0000