aboutsummaryrefslogtreecommitdiff
path: root/pretyping
diff options
context:
space:
mode:
Diffstat (limited to 'pretyping')
-rw-r--r--pretyping/cases.ml8
-rw-r--r--pretyping/cbv.ml19
-rw-r--r--pretyping/cbv.mli3
-rw-r--r--pretyping/constr_matching.ml8
-rw-r--r--pretyping/detyping.ml30
-rw-r--r--pretyping/evarconv.ml6
-rw-r--r--pretyping/heads.ml2
-rw-r--r--pretyping/indrec.ml9
-rw-r--r--pretyping/inductiveops.ml20
-rw-r--r--pretyping/inductiveops.mli6
-rw-r--r--pretyping/nativenorm.ml8
-rw-r--r--pretyping/patternops.ml4
-rw-r--r--pretyping/pretyping.ml16
-rw-r--r--pretyping/reductionops.ml39
-rw-r--r--pretyping/reductionops.mli2
-rw-r--r--pretyping/retyping.ml4
-rw-r--r--pretyping/tacred.ml23
-rw-r--r--pretyping/typing.ml20
-rw-r--r--pretyping/unification.ml10
-rw-r--r--pretyping/vnorm.ml9
20 files changed, 148 insertions, 98 deletions
diff --git a/pretyping/cases.ml b/pretyping/cases.ml
index 25353b7c12..a459229256 100644
--- a/pretyping/cases.ml
+++ b/pretyping/cases.ml
@@ -1131,14 +1131,14 @@ 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,c,brs) ->
+ | Case (ci,p,iv,c,brs) ->
(* We traverse a split *)
let p =
let sign,p = decompose_lam_assum sigma 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,c,Array.map2 (fun q c ->
+ 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)
@@ -1161,7 +1161,7 @@ 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,c,brs) ->
+ | Case (ci,p,iv,c,brs) ->
(* We traverse a split *)
Array.exists2 (fun q c ->
let _,b = decompose_lam_n_decls sigma q c in
@@ -1448,7 +1448,7 @@ let compile ~program_mode sigma pb =
let rci = Typing.check_allowed_sort !!(pb.env) sigma mind current pred in
let ci = make_case_info !!(pb.env) (fst mind) rci pb.casestyle in
let pred = nf_betaiota !!(pb.env) sigma pred in
- let case = make_case_or_project !!(pb.env) sigma indf ci pred current brvals in
+ let case = make_case_or_project !!(pb.env) sigma indt ci pred current brvals in
let sigma, _ = Typing.type_of !!(pb.env) sigma pred in
sigma, { uj_val = applist (case, inst);
uj_type = prod_applist sigma typ inst }
diff --git a/pretyping/cbv.ml b/pretyping/cbv.ml
index b39ec37cd1..b713d7812e 100644
--- a/pretyping/cbv.ml
+++ b/pretyping/cbv.ml
@@ -75,7 +75,8 @@ type cbv_value =
and cbv_stack =
| TOP
| APP of cbv_value array * cbv_stack
- | CASE of constr * constr array * case_info * cbv_value subs * cbv_stack
+ | CASE of constr * constr array * (constr,Univ.Instance.t) case_invert
+ * case_info * cbv_value subs * cbv_stack
| PROJ of Projection.t * cbv_stack
(* les vars pourraient etre des constr,
@@ -134,7 +135,7 @@ let rec stack_concat stk1 stk2 =
match stk1 with
TOP -> stk2
| APP(v,stk1') -> APP(v,stack_concat stk1' stk2)
- | CASE(c,b,i,s,stk1') -> CASE(c,b,i,s,stack_concat stk1' stk2)
+ | CASE(c,b,iv,i,s,stk1') -> CASE(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 *)
@@ -339,9 +340,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,ci,env,st) ->
+ | CASE (ty,br,iv,ci,env,st) ->
reify_stack
- (mkCase (ci, ty, t,br))
+ (mkCase (ci, ty, iv, t, br))
st
| PROJ (p, st) ->
reify_stack (mkProj (p, t)) st
@@ -400,7 +401,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,c,v) -> norm_head info env c (CASE(p,v,ci,env,stack))
+ | Case (ci,p,iv,c,v) -> norm_head info env c (CASE(p,v,iv,ci,env,stack))
| Cast (ct,_,_) -> norm_head info env ct stack
| Proj (p, c) ->
@@ -514,14 +515,14 @@ 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,ci,env,stk)))
+ | (CONSTR(((sp,n),u),[||]), APP(args,CASE(_,br,iv,ci,env,stk)))
when red_set info.reds fMATCH ->
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)
(* constructor of arity 0 in a Case -> IOTA *)
- | (CONSTR(((_,n),u),[||]), CASE(_,br,_,env,stk))
+ | (CONSTR(((_,n),u),[||]), CASE(_,br,_,_,env,stk))
when red_set info.reds fMATCH ->
cbv_stack_term info stk env br.(n-1)
@@ -597,9 +598,9 @@ 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,ci,env,st) ->
+ | CASE (ty,br,iv,ci,env,st) ->
apply_stack info
- (mkCase (ci, cbv_norm_term info env ty, t,
+ (mkCase (ci, cbv_norm_term info env ty, iv, t,
Array.map (cbv_norm_term info env) br))
st
| PROJ (p, st) ->
diff --git a/pretyping/cbv.mli b/pretyping/cbv.mli
index fdd4370613..d7804edf6d 100644
--- a/pretyping/cbv.mli
+++ b/pretyping/cbv.mli
@@ -41,7 +41,8 @@ type cbv_value =
and cbv_stack =
| TOP
| APP of cbv_value array * cbv_stack
- | CASE of constr * constr array * case_info * cbv_value subs * cbv_stack
+ | CASE of constr * constr array * (constr,Univ.Instance.t) 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 25aa8915ba..656739657d 100644
--- a/pretyping/constr_matching.ml
+++ b/pretyping/constr_matching.ml
@@ -351,7 +351,7 @@ 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,_,_,a2,[|b2;b2'|]) ->
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 +367,7 @@ 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,p2,_,a2,br2) ->
let n2 = Array.length br2 in
let () = match ci1.cip_ind with
| None -> ()
@@ -498,9 +498,9 @@ 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,c1,lc) ->
+ | Case (ci,hd,iv,c1,lc) ->
let next_mk_ctx = function
- | c1 :: hd :: lc -> mk_ctx (mkCase (ci,hd,c1,Array.of_list lc))
+ | c1 :: hd :: lc -> mk_ctx (mkCase (ci,hd,iv,c1,Array.of_list lc))
| _ -> assert false
in
let sub = (env, c1) :: (env, hd) :: subargs env lc in
diff --git a/pretyping/detyping.ml b/pretyping/detyping.ml
index 13946208bc..02c04c2300 100644
--- a/pretyping/detyping.ml
+++ b/pretyping/detyping.ml
@@ -429,7 +429,7 @@ 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,c,cl) when
+ | Case (ci,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 *)
@@ -498,40 +498,46 @@ let it_destRLambda_or_LetIn_names l c =
| _ -> DAst.make @@ GApp (c,[a]))
in aux l [] c
-let detype_case computable detype detype_eqns testdep avoid data p c bl =
- let (indsp,st,constagsl,k) = data in
+let detype_case computable detype detype_eqns testdep avoid ci p iv c bl =
let synth_type = synthetize_type () in
let tomatch = detype c in
+ let tomatch = match iv with
+ | NoInvert -> tomatch
+ | CaseInvert {univs;args} ->
+ let t = mkApp (mkIndU (ci.ci_ind,univs), args) in
+ DAst.make @@ GCast (tomatch, CastConv (detype t))
+ in
let alias, aliastyp, pred=
if (not !Flags.raw_print) && synth_type && computable && not (Int.equal (Array.length bl) 0)
then
Anonymous, None, None
else
let p = detype p in
- let nl,typ = it_destRLambda_or_LetIn_names k p in
+ let nl,typ = it_destRLambda_or_LetIn_names ci.ci_pp_info.ind_tags p in
let n,typ = match DAst.get typ with
| GLambda (x,_,t,c) -> x, c
| _ -> Anonymous, typ in
let aliastyp =
if List.for_all (Name.equal Anonymous) nl then None
- else Some (CAst.make (indsp,nl)) in
+ else Some (CAst.make (ci.ci_ind,nl)) in
n, aliastyp, Some typ
in
- let constructs = Array.init (Array.length bl) (fun i -> (indsp,i+1)) in
- let tag =
+ let constructs = Array.init (Array.length bl) (fun i -> (ci.ci_ind,i+1)) in
+ let tag = let st = ci.ci_pp_info.style in
try
if !Flags.raw_print then
RegularStyle
else if st == LetPatternStyle then
st
- else if PrintingLet.active indsp then
+ else if PrintingLet.active ci.ci_ind then
LetStyle
- else if PrintingIf.active indsp then
+ else if PrintingIf.active ci.ci_ind then
IfStyle
else
st
with Not_found -> st
in
+ let constagsl = ci.ci_pp_info.cstr_tags in
match tag, aliastyp with
| LetStyle, None ->
let bl' = Array.map detype bl in
@@ -793,14 +799,12 @@ 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,c,bl) ->
+ | Case (ci,p,iv,c,bl) ->
let comp = computable sigma p (List.length (ci.ci_pp_info.ind_tags)) in
detype_case comp (detype d flags avoid env sigma)
(detype_eqns d flags avoid env sigma ci comp)
(is_nondep_branch sigma) avoid
- (ci.ci_ind,ci.ci_pp_info.style,
- ci.ci_pp_info.cstr_tags,ci.ci_pp_info.ind_tags)
- p c bl
+ ci p iv c bl
| Fix (nvn,recdef) -> detype_fix (detype d) flags avoid env sigma nvn recdef
| CoFix (n,recdef) -> detype_cofix (detype d) flags avoid env sigma n recdef
| Int i -> GInt i
diff --git a/pretyping/evarconv.ml b/pretyping/evarconv.ml
index 366203faeb..0206d4e70d 100644
--- a/pretyping/evarconv.ml
+++ b/pretyping/evarconv.ml
@@ -208,7 +208,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)
@@ -382,7 +382,7 @@ let ise_stack2 no_app env evd f sk1 sk2 =
else None, x in
match sk1, sk2 with
| [], [] -> None, Success i
- | Stack.Case (_,t1,c1)::q1, Stack.Case (_,t2,c2)::q2 ->
+ | Stack.Case (_,t1,_,c1)::q1, Stack.Case (_,t2,_,c2)::q2 ->
(match f env i CONV t1 t2 with
| Success i' ->
(match ise_array2 i' (fun ii -> f env ii CONV) c1 c2 with
@@ -417,7 +417,7 @@ let exact_ise_stack2 env evd f sk1 sk2 =
let rec ise_stack2 i sk1 sk2 =
match sk1, sk2 with
| [], [] -> Success i
- | Stack.Case (_,t1,c1)::q1, Stack.Case (_,t2,c2)::q2 ->
+ | Stack.Case (_,t1,_,c1)::q1, Stack.Case (_,t2,_,c2)::q2 ->
ise_and i [
(fun i -> ise_stack2 i q1 q2);
(fun i -> ise_array2 i (fun ii -> f env ii CONV) c1 c2);
diff --git a/pretyping/heads.ml b/pretyping/heads.ml
index 908b8b00d6..98cfbf7fa7 100644
--- a/pretyping/heads.ml
+++ b/pretyping/heads.ml
@@ -78,7 +78,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 _ -> ConstructorHead
| Fix ((i,j),_) ->
let n = i.(j) in
diff --git a/pretyping/indrec.ml b/pretyping/indrec.ml
index 6132365b27..0e7fac35f1 100644
--- a/pretyping/indrec.ml
+++ b/pretyping/indrec.ml
@@ -119,8 +119,10 @@ let mis_make_case_com dep env sigma (ind, u as pind) (mib,mip as specif) kind =
in
let obj =
match projs with
- | None -> mkCase (ci, lift ndepar p, mkRel 1,
- Termops.rel_vect ndepar k)
+ | 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)
| Some ps ->
let term =
mkApp (mkRel 2,
@@ -407,7 +409,8 @@ let mis_make_indrec env sigma ?(force_mutual=false) listdepkind mib u =
arsign'
in
let obj =
- Inductiveops.make_case_or_project env !evdref indf ci (EConstr.of_constr pred)
+ let indty = find_rectype env sigma (EConstr.of_constr depind) in
+ Inductiveops.make_case_or_project env !evdref indty ci (EConstr.of_constr pred)
(EConstr.mkRel 1) (Array.map EConstr.of_constr branches)
in
let obj = EConstr.to_constr !evdref obj in
diff --git a/pretyping/inductiveops.ml b/pretyping/inductiveops.ml
index e77c5082dd..23145b1629 100644
--- a/pretyping/inductiveops.ml
+++ b/pretyping/inductiveops.ml
@@ -66,6 +66,8 @@ let relevance_of_inductive_family env ((ind,_),_ : inductive_family) =
type inductive_type = IndType of inductive_family * EConstr.constr list
+let ind_of_ind_type = function IndType (((ind,_),_),_) -> ind
+
let make_ind_type (indf, realargs) = IndType (indf,realargs)
let dest_ind_type (IndType (indf,realargs)) = (indf,realargs)
@@ -332,16 +334,26 @@ let get_constructors env (ind,params) =
let get_projections = Environ.get_projections
-let make_case_or_project env sigma indf ci pred c branches =
+let make_case_invert env (IndType (((ind,u),params),indices)) ci =
+ if Typeops.should_invert_case env ci
+ then
+ let univs = EConstr.EInstance.make u in
+ let params = Array.map_of_list EConstr.of_constr params in
+ let args = Array.append params (Array.of_list indices) in
+ CaseInvert {univs;args}
+ else NoInvert
+
+let make_case_or_project env sigma indt ci pred c branches =
let open EConstr in
- let projs = get_projections env (fst (fst indf)) in
+ let IndType (((ind,_),_),_) = indt in
+ let projs = get_projections env ind in
match projs with
- | None -> (mkCase (ci, pred, c, branches))
+ | None ->
+ mkCase (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
let () =
- let (ind, _), _ = dest_ind_family indf in
let mib, _ = Inductive.lookup_mind_specif env ind in
if (* dependent *) not (Vars.noccurn sigma 1 t) &&
not (has_dependent_elim mib) then
diff --git a/pretyping/inductiveops.mli b/pretyping/inductiveops.mli
index 2bec86599e..1e2bba9f73 100644
--- a/pretyping/inductiveops.mli
+++ b/pretyping/inductiveops.mli
@@ -48,6 +48,7 @@ val map_inductive_type : (EConstr.constr -> EConstr.constr) -> inductive_type ->
val liftn_inductive_type : int -> int -> inductive_type -> inductive_type
val lift_inductive_type : int -> inductive_type -> inductive_type
val substnl_ind_type : EConstr.constr list -> int -> inductive_type -> inductive_type
+val ind_of_ind_type : inductive_type -> inductive
val relevance_of_inductive_type : env -> inductive_type -> Sorts.relevance
@@ -204,9 +205,12 @@ val make_case_info : env -> inductive -> Sorts.relevance -> case_style -> case_i
Fail with an error if the elimination is dependent while the
inductive type does not allow dependent elimination. *)
val make_case_or_project :
- env -> evar_map -> inductive_family -> case_info ->
+ env -> evar_map -> inductive_type -> case_info ->
(* 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
+
(*i Compatibility
val make_default_case_info : env -> case_style -> inductive -> case_info
i*)
diff --git a/pretyping/nativenorm.ml b/pretyping/nativenorm.ml
index d672ddc906..89bd7e196f 100644
--- a/pretyping/nativenorm.ml
+++ b/pretyping/nativenorm.ml
@@ -317,6 +317,11 @@ and nf_atom_type env sigma atom =
| Avar id ->
mkVar id, Typeops.type_of_variable env id
| Acase(ans,accu,p,bs) ->
+ let () = if Typeops.should_invert_case env ans.asw_ci then
+ (* TODO implement case inversion readback (properly reducing
+ it is a problem for the kernel) *)
+ CErrors.user_err Pp.(str "Native compute readback of case inversion not implemented.")
+ in
let a,ta = nf_accu_type env sigma accu in
let ((mind,_),u as ind),allargs = find_rectype_a env ta in
let (mib,mip) = Inductive.lookup_mind_specif env (fst ind) in
@@ -338,8 +343,7 @@ and nf_atom_type env sigma atom =
in
let branchs = Array.mapi mkbranch bsw in
let tcase = build_case_type p realargs a in
- let ci = ans.asw_ci in
- mkCase(ci, p, a, branchs), tcase
+ mkCase(ans.asw_ci, p, NoInvert, 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 6d30e0338e..4aedeb43e3 100644
--- a/pretyping/patternops.ml
+++ b/pretyping/patternops.ml
@@ -193,8 +193,8 @@ let pattern_of_constr env sigma t =
else PEvar (evk,List.map (pattern_of_constr env) ctxt)
| Evar_kinds.MatchingVar (Evar_kinds.SecondOrderPatVar ido) -> assert false
| _ ->
- PMeta None)
- | Case (ci,p,a,br) ->
+ PMeta None)
+ | Case (ci,p,_,a,br) ->
let cip =
{ cip_style = ci.ci_pp_info.style;
cip_ind = Some ci.ci_ind;
diff --git a/pretyping/pretyping.ml b/pretyping/pretyping.ml
index 1b6c17fcf9..e4403d5bf4 100644
--- a/pretyping/pretyping.ml
+++ b/pretyping/pretyping.ml
@@ -991,7 +991,7 @@ struct
let pretype tycon env sigma c = eval_pretyper self ~program_mode ~poly resolve_tc tycon env sigma c in
let pretype_type tycon env sigma c = eval_type_pretyper self ~program_mode ~poly resolve_tc tycon env sigma c in
let sigma, cj = pretype empty_tycon env sigma c in
- let (IndType (indf,realargs)) =
+ let (IndType (indf,realargs)) as indty =
try find_rectype !!env sigma cj.uj_type
with Not_found ->
let cloc = loc_of_glob_constr c in
@@ -1028,11 +1028,11 @@ struct
let fsign = Context.Rel.map (whd_betaiota !!env sigma) fsign in
let hypnaming = if program_mode then ProgramNaming else KeepUserNameAndRenameExistingButSectionNames in
let fsign,env_f = push_rel_context ~hypnaming sigma fsign env in
- let obj ind rci p v f =
+ let obj indt rci p v f =
if not record then
let f = it_mkLambda_or_LetIn f fsign in
- let ci = make_case_info !!env (fst ind) rci LetStyle in
- mkCase (ci, p, cj.uj_val,[|f|])
+ 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|])
else it_mkLambda_or_LetIn f fsign
in
(* Make dependencies from arity signature impossible *)
@@ -1060,7 +1060,7 @@ struct
let v =
let ind,_ = dest_ind_family indf in
let rci = Typing.check_allowed_sort !!env sigma ind cj.uj_val p in
- obj ind rci p cj.uj_val fj.uj_val
+ obj indty rci p cj.uj_val fj.uj_val
in
sigma, { uj_val = v; uj_type = (substl (realargs@[cj.uj_val]) ccl) }
@@ -1079,7 +1079,7 @@ struct
let v =
let ind,_ = dest_ind_family indf in
let rci = Typing.check_allowed_sort !!env sigma ind cj.uj_val p in
- obj ind rci p cj.uj_val fj.uj_val
+ obj indty rci p cj.uj_val fj.uj_val
in sigma, { uj_val = v; uj_type = ccl })
let pretype_cases self (sty, po, tml, eqns) =
@@ -1092,7 +1092,7 @@ struct
let open Context.Rel.Declaration in
let pretype tycon env sigma c = eval_pretyper self ~program_mode ~poly resolve_tc tycon env sigma c in
let sigma, cj = pretype empty_tycon env sigma c in
- let (IndType (indf,realargs)) =
+ let (IndType (indf,realargs)) as indty =
try find_rectype !!env sigma cj.uj_type
with Not_found ->
let cloc = loc_of_glob_constr c in
@@ -1148,7 +1148,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, cj.uj_val, [|b1;b2|])
+ mkCase (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 8ab040b3b1..18a0637efa 100644
--- a/pretyping/reductionops.ml
+++ b/pretyping/reductionops.ml
@@ -179,7 +179,7 @@ sig
type 'a member =
| App of 'a app_node
- | Case of case_info * 'a * 'a array
+ | Case of case_info * 'a * ('a, EInstance.t) case_invert * 'a array
| Proj of Projection.t
| Fix of ('a, 'a) pfixpoint * 'a t
| Primitive of CPrimitives.t * (Constant.t * EInstance.t) * 'a t * CPrimitives.args_red
@@ -231,7 +231,7 @@ struct
type 'a member =
| App of 'a app_node
- | Case of case_info * 'a * 'a array
+ | Case of case_info * 'a * ('a, EInstance.t) case_invert * 'a array
| Proj of Projection.t
| Fix of ('a, 'a) pfixpoint * 'a t
| Primitive of CPrimitives.t * (Constant.t * EInstance.t) * 'a t * CPrimitives.args_red
@@ -244,7 +244,7 @@ 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
++ str ")"
@@ -285,7 +285,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(c1,_,_,_)::s1, Case(c2,_,_,_)::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
@@ -305,7 +305,7 @@ 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 ->
+ | Case (_,t1,_,a1) :: q1, Case (_,t2,_,a2) :: q2 ->
aux (Array.fold_left2 f (f o t1 t2) a1 a2) q1 q2
| Proj (p1) :: q1, Proj (p2) :: q2 ->
aux o q1 q2
@@ -321,7 +321,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,br) -> Case (info, f ty, Array.map f br)
+ | Case (info,ty,iv,br) ->
+ Case (info, f ty, map_invert f iv, Array.map 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) ->
@@ -403,7 +404,7 @@ struct
then a
else Array.sub a i (j - i + 1) in
zip (mkApp (f, a'), s)
- | f, (Case (ci,rt,br)::s) -> zip (mkCase (ci,rt,f,br), s)
+ | f, (Case (ci,rt,iv,br)::s) -> zip (mkCase (ci,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)
@@ -536,12 +537,13 @@ let reduce_and_refold_cofix recfun env sigma cofix sk =
let reduce_mind_case sigma mia =
match EConstr.kind sigma mia.mconstr with
| Construct ((ind_sp,i),u) ->
-(* let ncargs = (fst mia.mci).(i-1) in*)
+(* let ncargs = (fst mia.mci).(i-1) in*)
let real_cargs = List.skipn mia.mci.ci_npar mia.mcargs in
applist (mia.mlf.(i-1),real_cargs)
| CoFix cofix ->
let cofix_def = contract_cofix sigma cofix in
- mkCase (mia.mci, mia.mP, applist(cofix_def,mia.mcargs), mia.mlf)
+ (* XXX Is NoInvert OK here? *)
+ mkCase (mia.mci, mia.mP, NoInvert, applist(cofix_def,mia.mcargs), mia.mlf)
| _ -> assert false
(* contracts fix==FIX[nl;i](A1...Ak;[F1...Fk]{B1....Bk}) to produce
@@ -805,8 +807,8 @@ let rec whd_state_gen flags env sigma =
| _ -> fold ())
| _ -> fold ())
- | Case (ci,p,d,lf) ->
- whrec (d, Stack.Case (ci,p,lf) :: stack)
+ | Case (ci,p,iv,d,lf) ->
+ whrec (d, Stack.Case (ci,p,iv,lf) :: stack)
| Fix ((ri,n),_ as f) ->
(match Stack.strip_n_app ri.(n) stack with
@@ -819,7 +821,7 @@ let rec whd_state_gen flags env sigma =
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 ->
+ |args, (Stack.Case(ci, _, _, lf)::s') when use_match ->
whrec (lf.(c-1), (Stack.tail ci.ci_npar args) @ s')
|args, (Stack.Proj (p)::s') when use_match ->
whrec (Stack.nth args (Projection.npars p + Projection.arg p), s')
@@ -901,8 +903,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,d,lf) ->
- whrec (d, Stack.Case (ci,p,lf) :: stack)
+ | Case (ci,p,iv,d,lf) ->
+ whrec (d, Stack.Case (ci,p,iv,lf) :: stack)
| Fix ((ri,n),_ as f) ->
(match Stack.strip_n_app ri.(n) stack with
@@ -920,7 +922,7 @@ let local_whd_state_gen flags _env sigma =
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 ->
+ |args, (Stack.Case(ci, _, _, lf)::s') when use_match ->
whrec (lf.(c-1), (Stack.tail ci.ci_npar args) @ s')
|args, (Stack.Proj (p) :: s') when use_match ->
whrec (Stack.nth args (Projection.npars p + Projection.arg p), s')
@@ -1035,7 +1037,7 @@ let clos_norm_flags flgs env sigma t =
try
let evars ev = safe_evar_value sigma ev in
EConstr.of_constr (CClosure.norm_val
- (CClosure.create_clos_infos ~evars flgs env)
+ (CClosure.create_clos_infos ~univs:(Evd.universes sigma) ~evars flgs env)
(CClosure.create_tab ())
(CClosure.inject (EConstr.Unsafe.to_constr t)))
with e when is_anomaly e -> user_err Pp.(str "Tried to normalize ill-typed term")
@@ -1044,7 +1046,7 @@ let clos_whd_flags flgs env sigma t =
try
let evars ev = safe_evar_value sigma ev in
EConstr.of_constr (CClosure.whd_val
- (CClosure.create_clos_infos ~evars flgs env)
+ (CClosure.create_clos_infos ~univs:(Evd.universes sigma) ~evars flgs env)
(CClosure.create_tab ())
(CClosure.inject (EConstr.Unsafe.to_constr t)))
with e when is_anomaly e -> user_err Pp.(str "Tried to normalize ill-typed term")
@@ -1148,7 +1150,8 @@ let sigma_check_inductive_instances cv_pb variance u1 u2 sigma =
let sigma_univ_state =
let open Reduction in
- { compare_sorts = sigma_compare_sorts;
+ { compare_graph = Evd.universes;
+ compare_sorts = sigma_compare_sorts;
compare_instances = sigma_compare_instances;
compare_cumul_instances = sigma_check_inductive_instances; }
diff --git a/pretyping/reductionops.mli b/pretyping/reductionops.mli
index a0cbd8ccf7..58fff49faa 100644
--- a/pretyping/reductionops.mli
+++ b/pretyping/reductionops.mli
@@ -58,7 +58,7 @@ module Stack : sig
type 'a member =
| App of 'a app_node
- | Case of case_info * 'a * 'a array
+ | Case of case_info * 'a * ('a, EInstance.t) case_invert * 'a array
| 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 5ec5005b3e..bb518bc2f9 100644
--- a/pretyping/retyping.ml
+++ b/pretyping/retyping.ml
@@ -121,7 +121,7 @@ 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,c,lf) ->
+ | Case (_,p,_iv,c,lf) ->
let Inductiveops.IndType(indf,realargs) =
let t = type_of env c in
try Inductiveops.find_rectype env sigma t
@@ -297,7 +297,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 5b9bc91b84..baa32565f6 100644
--- a/pretyping/tacred.ml
+++ b/pretyping/tacred.ml
@@ -277,8 +277,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
@@ -538,7 +538,8 @@ 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
- mkCase (mia.mci, mia.mP, applist(cofix_def,mia.mcargs), mia.mlf)
+ (* Is NoInvert OK here? *)
+ mkCase (mia.mci, mia.mP, NoInvert, applist(cofix_def,mia.mcargs), mia.mlf)
| _ -> assert false
@@ -573,7 +574,7 @@ let match_eval_ref_value env sigma constr stack =
env |> lookup_rel n |> RelDecl.get_value |> Option.map (lift n)
| _ -> None
-let special_red_case env sigma whfun (ci, p, c, lf) =
+let special_red_case env sigma whfun (ci, p, iv, c, lf) =
let rec redrec s =
let (constr, cargs) = whfun s in
match match_eval_ref env sigma constr cargs with
@@ -619,9 +620,9 @@ let reduce_proj env sigma whfun whfun' c =
let proj_narg = Projection.npars proj + Projection.arg proj in
List.nth cargs proj_narg
| _ -> raise Redelimination)
- | Case (n,p,c,brs) ->
+ | Case (n,p,iv,c,brs) ->
let c' = redrec c in
- let p = (n,p,c',brs) in
+ let p = (n,p,iv,c',brs) in
(try special_red_case env sigma whfun' p
with Redelimination -> mkCase p)
| _ -> raise Redelimination
@@ -772,9 +773,9 @@ and whd_simpl_stack env sigma =
| LetIn (n,b,t,c) -> redrec (applist (Vars.substl [b] c, stack))
| App (f,cl) -> redrec (applist(f, (Array.to_list cl)@stack))
| Cast (c,_,_) -> redrec (applist(c, stack))
- | Case (ci,p,c,lf) ->
+ | Case (ci,p,iv,c,lf) ->
(try
- redrec (applist(special_red_case env sigma redrec (ci,p,c,lf), stack))
+ redrec (applist(special_red_case env sigma redrec (ci,p,iv,c,lf), stack))
with
Redelimination -> s')
| Fix fix ->
@@ -867,7 +868,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,d,lf) -> simpfun (mkCase (ci,p,redrec env d,lf))
+ | Case (ci,p,iv,d,lf) -> simpfun (mkCase (ci,p,iv,redrec env d,lf))
| Proj (p, c) ->
let c' =
match EConstr.kind sigma c with
@@ -1264,10 +1265,10 @@ 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,c,lf) ->
+ | Case (ci,p,iv,c,lf) ->
(try
(special_red_case env sigma (whd_simpl_stack env sigma)
- (ci,p,c,lf), stack)
+ (ci,p,iv,c,lf), stack)
with Redelimination -> raise NotStepReducible)
| Fix fix ->
(try match reduce_fix (whd_construct_stack env) sigma fix stack with
diff --git a/pretyping/typing.ml b/pretyping/typing.ml
index f0882d4594..b4a1153731 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 cj lfj =
+let judge_of_case env sigma 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
@@ -186,7 +186,10 @@ let judge_of_case env sigma ci pj cj lfj =
let sigma, (bty,rslty,rci) = type_case_branches env sigma indspec pj cj.uj_val in
let () = check_case_info env (fst indspec) rci ci in
let sigma = check_branch_types env sigma (fst indspec) cj (lfj,bty) in
- sigma, { uj_val = mkCase (ci, pj.uj_val, cj.uj_val, Array.map j_val 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);
uj_type = rslty }
let check_type_fixpoint ?loc env sigma lna lar vdefj =
@@ -361,11 +364,20 @@ let rec execute env sigma cstr =
let sigma, ty = type_of_constructor env sigma ctor in
sigma, make_judge cstr ty
- | Case (ci,p,c,lf) ->
+ | Case (ci,p,iv,c,lf) ->
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
- judge_of_case env sigma ci pj cj lfj
+ let sigma = match iv with
+ | NoInvert -> sigma
+ | CaseInvert {univs;args} ->
+ let t = mkApp (mkIndU (ci.ci_ind,univs), args) in
+ let sigma, tj = execute env sigma t in
+ let sigma, tj = type_judgment env sigma tj in
+ let sigma = Evarconv.unify_leq_delay env sigma cj.uj_type tj.utj_val in
+ sigma
+ in
+ judge_of_case env sigma 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 95b07e227e..ef58f41489 100644
--- a/pretyping/unification.ml
+++ b/pretyping/unification.ml
@@ -567,7 +567,7 @@ let is_rigid_head sigma flags t =
| Construct _ | Int _ | Float _ -> 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 =
@@ -657,7 +657,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, cl) -> is_neutral env sigma ts c
+ | Case (_, p, _, c, _) -> is_neutral env sigma ts c
| Proj (p, c) -> is_neutral env sigma ts c
| Lambda _ | LetIn _ | Construct _ | CoFix _ | Int _ | Float _ -> false
| Sort _ | Cast (_, _, _) | Prod (_, _, _) | Ind _ -> false (* Really? *)
@@ -847,7 +847,7 @@ 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,p1,_,c1,cl1), Case (ci2,p2,_,c2,cl2) ->
(try
if not (eq_ind 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
@@ -1782,7 +1782,7 @@ 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 ->
@@ -1867,7 +1867,7 @@ 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 *)
+ | Case(_,_,_,c,lf) -> (* does not search in the predicate *)
bind (matchrec c) (bind_iter matchrec lf)
| Proj (p,c) -> matchrec c
diff --git a/pretyping/vnorm.ml b/pretyping/vnorm.ml
index 37c34d55cf..efe1efd74e 100644
--- a/pretyping/vnorm.ml
+++ b/pretyping/vnorm.ml
@@ -261,6 +261,12 @@ and nf_stk ?from:(from=0) env sigma c t stk =
nf_stk env sigma (mkApp(fa,[|c|])) (subst1 c codom) stk
| Zswitch sw :: stk ->
assert (from = 0) ;
+ let ci = sw.sw_annot.Vmvalues.ci in
+ let () = if Typeops.should_invert_case env ci then
+ (* TODO implement case inversion readback (properly reducing
+ it is a problem for the kernel) *)
+ CErrors.user_err Pp.(str "VM compute readback of case inversion not implemented.")
+ in
let ((mind,_ as ind), u), allargs = find_rectype_a env t in
let (mib,mip) = Inductive.lookup_mind_specif env ind in
let nparams = mib.mind_nparams in
@@ -280,8 +286,7 @@ and nf_stk ?from:(from=0) env sigma c t stk =
in
let branchs = Array.mapi mkbranch bsw in
let tcase = build_case_type p realargs c in
- let ci = sw.sw_annot.Vmvalues.ci in
- nf_stk env sigma (mkCase(ci, p, c, branchs)) tcase stk
+ nf_stk env sigma (mkCase(ci, p, NoInvert, 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 14:54:26 +0000