aboutsummaryrefslogtreecommitdiff
path: root/contrib
diff options
context:
space:
mode:
Diffstat (limited to 'contrib')
-rw-r--r--contrib/funind/indfun.ml11
-rw-r--r--contrib/funind/rawterm_to_relation.ml8
-rw-r--r--contrib/funind/rawtermops.ml46
-rw-r--r--contrib/interface/depends.ml9
-rw-r--r--contrib/interface/xlate.ml6
-rw-r--r--contrib/recdef/recdef.ml42
-rw-r--r--contrib/subtac/subtac_cases.ml7
-rw-r--r--contrib/subtac/subtac_pretyping_F.ml18
8 files changed, 31 insertions, 76 deletions
diff --git a/contrib/funind/indfun.ml b/contrib/funind/indfun.ml
index 7385bf652f..aaa1b466da 100644
--- a/contrib/funind/indfun.ml
+++ b/contrib/funind/indfun.ml
@@ -224,11 +224,9 @@ let rec is_rec names =
)
b
| RApp(_,f,args) -> List.exists (lookup names) (f::args)
- | RCases(_,_,el,brl) ->
+ | RCases(_,_,_,el,brl) ->
List.exists (fun (e,_) -> lookup names e) el ||
List.exists (lookup_br names) brl
- | RLetPattern (_,(c,_),p) ->
- lookup names c || lookup_br names p
and lookup_br names (_,idl,_,rt) =
let new_names = List.fold_right Idset.remove idl names in
lookup new_names rt
@@ -590,8 +588,8 @@ let rec add_args id new_args b =
| CApp(loc,(pf,b),bl) ->
CApp(loc,(pf,add_args id new_args b),
List.map (fun (e,o) -> add_args id new_args e,o) bl)
- | CCases(loc,b_option,cel,cal) ->
- CCases(loc,Option.map (add_args id new_args) b_option,
+ | CCases(loc,sty,b_option,cel,cal) ->
+ CCases(loc,sty,Option.map (add_args id new_args) b_option,
List.map (fun (b,(na,b_option)) ->
add_args id new_args b,
(na,Option.map (add_args id new_args) b_option)) cel,
@@ -603,9 +601,6 @@ let rec add_args id new_args b =
add_args id new_args b2
)
- | CLetPattern(loc,p,b,c) ->
- CLetPattern(loc,p,add_args id new_args b,add_args id new_args c)
-
| CIf(loc,b1,(na,b_option),b2,b3) ->
CIf(loc,add_args id new_args b1,
(na,Option.map (add_args id new_args) b_option),
diff --git a/contrib/funind/rawterm_to_relation.ml b/contrib/funind/rawterm_to_relation.ml
index 9276898e18..08a97fd221 100644
--- a/contrib/funind/rawterm_to_relation.ml
+++ b/contrib/funind/rawterm_to_relation.ml
@@ -567,7 +567,7 @@ let rec build_entry_lc env funnames avoid rt : rawconstr build_entry_return =
funnames
avoid
(mkRLetIn(new_n,t,mkRApp(new_b,args)))
- | RCases _ | RLambda _ | RIf _ | RLetTuple _ | RLetPattern _ ->
+ | RCases _ | RLambda _ | RIf _ | RLetTuple _ ->
(* we have [(match e1, ...., en with ..... end) t1 tn]
we first compute the result from the case and
then combine each of them with each of args one
@@ -627,14 +627,12 @@ let rec build_entry_lc env funnames avoid rt : rawconstr build_entry_return =
in
let b_res = build_entry_lc new_env funnames avoid b in
combine_results (combine_letin n) v_res b_res
- | RCases(_,_,el,brl) ->
+ | RCases(_,_,_,el,brl) ->
(* we create the discrimination function
and treat the case itself
*)
let make_discr = make_discr_match brl in
build_entry_lc_from_case env funnames make_discr el brl avoid
- | RLetPattern (loc,c,p) ->
- build_entry_lc env funnames avoid (RCases (loc, None, [c], [p]))
| RIf(_,b,(na,e_option),lhs,rhs) ->
let b_as_constr = Pretyping.Default.understand Evd.empty env b in
let b_typ = Typing.type_of env Evd.empty b_as_constr in
@@ -1021,7 +1019,7 @@ let rec compute_cst_params relnames params = function
| RLambda(_,_,_,t,b) | RProd(_,_,_,t,b) | RLetIn(_,_,t,b) | RLetTuple(_,_,_,t,b) ->
let t_params = compute_cst_params relnames params t in
compute_cst_params relnames t_params b
- | RCases _ | RLetPattern _ ->
+ | RCases _ ->
params (* If there is still cases at this point they can only be
discriminitation ones *)
| RSort _ -> params
diff --git a/contrib/funind/rawtermops.ml b/contrib/funind/rawtermops.ml
index c9341ba998..92396af590 100644
--- a/contrib/funind/rawtermops.ml
+++ b/contrib/funind/rawtermops.ml
@@ -15,7 +15,7 @@ let mkRApp(rt,rtl) = RApp(dummy_loc,rt,rtl)
let mkRLambda(n,t,b) = RLambda(dummy_loc,n,Explicit,t,b)
let mkRProd(n,t,b) = RProd(dummy_loc,n,Explicit,t,b)
let mkRLetIn(n,t,b) = RLetIn(dummy_loc,n,t,b)
-let mkRCases(rto,l,brl) = RCases(dummy_loc,rto,l,brl)
+let mkRCases(rto,l,brl) = RCases(dummy_loc,Term.RegularStyle,rto,l,brl)
let mkRSort s = RSort(dummy_loc,s)
let mkRHole () = RHole(dummy_loc,Evd.BinderType Anonymous)
let mkRCast(b,t) = RCast(dummy_loc,b,CastConv (Term.DEFAULTcast,t))
@@ -163,14 +163,12 @@ let change_vars =
change_vars mapping b,
change_vars new_mapping e
)
- | RCases(loc,infos,el,brl) ->
- RCases(loc,
+ | RCases(loc,sty,infos,el,brl) ->
+ RCases(loc,sty,
infos,
List.map (fun (e,x) -> (change_vars mapping e,x)) el,
List.map (change_vars_br mapping) brl
)
- | RLetPattern(loc, (e,x), br) ->
- RLetPattern(loc, (change_vars mapping e, x), change_vars_br mapping br)
| RIf(loc,b,(na,e_option),lhs,rhs) ->
RIf(loc,
change_vars mapping b,
@@ -348,13 +346,11 @@ let rec alpha_rt excluded rt =
let new_b = alpha_rt new_excluded new_b in
let new_rto = Option.map (alpha_rt new_excluded) new_rto in
RLetTuple(loc,new_nal,(na,new_rto),new_t,new_b)
- | RCases(loc,infos,el,brl) ->
+ | RCases(loc,sty,infos,el,brl) ->
let new_el =
List.map (function (rt,i) -> alpha_rt excluded rt, i) el
in
- RCases(loc,infos,new_el,List.map (alpha_br excluded) brl)
- | RLetPattern(loc,(rt,i),br) ->
- RLetPattern(loc, (alpha_rt excluded rt, i), alpha_br excluded br)
+ RCases(loc,sty,infos,new_el,List.map (alpha_br excluded) brl)
| RIf(loc,b,(na,e_o),lhs,rhs) ->
RIf(loc,alpha_rt excluded b,
(na,Option.map (alpha_rt excluded) e_o),
@@ -402,10 +398,9 @@ let is_free_in id =
| _ -> true
in
is_free_in t || (check_in_b && is_free_in b)
- | RCases(_,_,el,brl) ->
+ | RCases(_,_,_,el,brl) ->
(List.exists (fun (e,_) -> is_free_in e) el) ||
List.exists is_free_in_br brl
- | RLetPattern(_,(e,_),br) -> is_free_in e || is_free_in_br br
| RLetTuple(_,nal,_,b,t) ->
let check_in_nal =
not (List.exists (function Name id' -> id'= id | _ -> false) nal)
@@ -499,14 +494,12 @@ let replace_var_by_term x_id term =
replace_var_by_pattern def,
replace_var_by_pattern b
)
- | RCases(loc,infos,el,brl) ->
- RCases(loc,
+ | RCases(loc,sty,infos,el,brl) ->
+ RCases(loc,sty,
infos,
List.map (fun (e,x) -> (replace_var_by_pattern e,x)) el,
List.map replace_var_by_pattern_br brl
)
- | RLetPattern(loc,(e,x),br) ->
- RLetPattern(loc,(replace_var_by_pattern e, x), replace_var_by_pattern_br br)
| RIf(loc,b,(na,e_option),lhs,rhs) ->
RIf(loc, replace_var_by_pattern b,
(na,Option.map replace_var_by_pattern e_option),
@@ -608,10 +601,8 @@ let ids_of_rawterm c =
| RIf (loc,c,(na,po),b1,b2) -> ids_of_rawterm [] c @ ids_of_rawterm [] b1 @ ids_of_rawterm [] b2 @ acc
| RLetTuple (_,nal,(na,po),b,c) ->
List.map idof nal @ ids_of_rawterm [] b @ ids_of_rawterm [] c @ acc
- | RCases (loc,rtntypopt,tml,brchl) ->
+ | RCases (loc,sty,rtntypopt,tml,brchl) ->
List.flatten (List.map (fun (_,idl,patl,c) -> idl @ ids_of_rawterm [] c) brchl)
- | RLetPattern (loc,tm,(_,idl,patl,c)) ->
- idl @ ids_of_rawterm [] c
| RRec _ -> failwith "Fix inside a constructor branch"
| (RSort _ | RHole _ | RRef _ | REvar _ | RPatVar _ | RDynamic _) -> []
in
@@ -658,17 +649,12 @@ let zeta_normalize =
zeta_normalize_term def,
zeta_normalize_term b
)
- | RCases(loc,infos,el,brl) ->
- RCases(loc,
+ | RCases(loc,sty,infos,el,brl) ->
+ RCases(loc,sty,
infos,
List.map (fun (e,x) -> (zeta_normalize_term e,x)) el,
List.map zeta_normalize_br brl
)
- | RLetPattern(loc,(e,x),br) ->
- RLetPattern(loc,
- (zeta_normalize_term e,x),
- zeta_normalize_br br
- )
| RIf(loc,b,(na,e_option),lhs,rhs) ->
RIf(loc, zeta_normalize_term b,
(na,Option.map zeta_normalize_term e_option),
@@ -723,14 +709,10 @@ let expand_as =
| RDynamic _ -> error "Not handled RDynamic"
| RCast(loc,b,CastConv(kind,t)) -> RCast(loc,expand_as map b,CastConv(kind,expand_as map t))
| RCast(loc,b,CastCoerce) -> RCast(loc,expand_as map b,CastCoerce)
- | RCases(loc,po,el,brl) ->
- RCases(loc, Option.map (expand_as map) po, List.map (fun (rt,t) -> expand_as map rt,t) el,
+ | RCases(loc,sty,po,el,brl) ->
+ RCases(loc, sty, Option.map (expand_as map) po, List.map (fun (rt,t) -> expand_as map rt,t) el,
List.map (expand_as_br map) brl)
- | RLetPattern(loc,(rt,t),br) ->
- RLetPattern(loc, (expand_as map rt,t),
- expand_as_br map br)
-
and expand_as_br map (loc,idl,cpl,rt) =
- (loc,idl,cpl, expand_as (List.fold_left add_as map cpl) rt)
+ (loc,idl,cpl, expand_as (List.fold_left add_as map cpl) rt)
in
expand_as Idmap.empty
diff --git a/contrib/interface/depends.ml b/contrib/interface/depends.ml
index 16357fc472..39eaa0b98b 100644
--- a/contrib/interface/depends.ml
+++ b/contrib/interface/depends.ml
@@ -210,7 +210,7 @@ let rec depends_of_rawconstr rc acc = match rc with
| RLambda (_, _, _, rct, rcb)
| RProd (_, _, _, rct, rcb)
| RLetIn (_, _, rct, rcb) -> depends_of_rawconstr rcb (depends_of_rawconstr rct acc)
- | RCases (_, rco, tmt, cc) ->
+ | RCases (_, _, rco, tmt, cc) ->
(* LEM TODO: handle the cc *)
(Option.fold_right depends_of_rawconstr rco
(list_union_map
@@ -221,13 +221,6 @@ let rec depends_of_rawconstr rc acc = match rc with
acc))
| RLetTuple (_,_,(_,rco),rc0,rc1) ->
depends_of_rawconstr rc1 (depends_of_rawconstr rc0 (Option.fold_right depends_of_rawconstr rco acc))
- | RLetPattern (_, tmt, cc) ->
- (* LEM TODO: handle the cc *)
- (fun (rc, pp) acc ->
- Option.fold_right (fun (_,ind,_,_) acc -> (IndRef ind)::acc) (snd pp)
- (depends_of_rawconstr rc acc))
- tmt
- acc
| RIf (_, rcC, (_, rco), rcT, rcF) -> let dorc = depends_of_rawconstr in
dorc rcF (dorc rcT (dorc rcF (dorc rcC (Option.fold_right dorc rco acc))))
| RRec (_, _, _, rdla, rca0, rca1) -> let dorca = array_union_map depends_of_rawconstr in
diff --git a/contrib/interface/xlate.ml b/contrib/interface/xlate.ml
index 2219e327ca..aa7a50dce2 100644
--- a/contrib/interface/xlate.ml
+++ b/contrib/interface/xlate.ml
@@ -360,8 +360,6 @@ and (xlate_formula:Topconstr.constr_expr -> Ascent.ct_FORMULA) = function
| CLambdaN(_,ll,b)-> CT_lambdac(xlate_binder_ne_list ll, xlate_formula b)
| CLetIn(_, v, a, b) ->
CT_letin(CT_def(xlate_id_opt v, xlate_formula a), xlate_formula b)
- | CLetPattern(_, v, a, b) ->
- error "TODO: xlate_formula let | pattern"
| CAppExpl(_, (Some n, r), l) ->
let l', last = decompose_last l in
CT_proj(xlate_formula last,
@@ -379,8 +377,8 @@ and (xlate_formula:Topconstr.constr_expr -> Ascent.ct_FORMULA) = function
(xlate_formula f, List.map xlate_formula_expl l'))
| CApp(_, (_,f), l) ->
CT_appc(xlate_formula f, xlate_formula_expl_ne_list l)
- | CCases (_, _, [], _) -> assert false
- | CCases (_, ret_type, tm::tml, eqns)->
+ | CCases (_, _, _, [], _) -> assert false
+ | CCases (_, _, ret_type, tm::tml, eqns)->
CT_cases(CT_matched_formula_ne_list(xlate_matched_formula tm,
List.map xlate_matched_formula tml),
xlate_formula_opt ret_type,
diff --git a/contrib/recdef/recdef.ml4 b/contrib/recdef/recdef.ml4
index dd776088cc..8d9bfdbc51 100644
--- a/contrib/recdef/recdef.ml4
+++ b/contrib/recdef/recdef.ml4
@@ -1070,7 +1070,7 @@ let (value_f:constr list -> global_reference -> constr) =
in
let fun_body =
RCases
- (d0,None,
+ (d0,RegularStyle,None,
[RApp(d0, RRef(d0,fterm), List.rev_map (fun x_id -> RVar(d0, x_id)) rev_x_id_l),
(Anonymous,None)],
[d0, [v_id], [PatCstr(d0,(ind_of_ref
diff --git a/contrib/subtac/subtac_cases.ml b/contrib/subtac/subtac_cases.ml
index 54ed30a5dc..5b8bb9c0f8 100644
--- a/contrib/subtac/subtac_cases.ml
+++ b/contrib/subtac/subtac_cases.ml
@@ -241,6 +241,7 @@ type pattern_matching_problem =
history : pattern_continuation;
mat : matrix;
caseloc : loc;
+ casestyle: case_style;
typing_function: type_constraint -> env -> rawconstr -> unsafe_judgment }
(*--------------------------------------------------------------------------*
@@ -1263,7 +1264,7 @@ and match_current pb tomatch =
let (pred,typ,s) =
find_predicate pb.caseloc pb.env pb.isevars
pb.pred brtyps cstrs current indt pb.tomatch in
- let ci = make_case_info pb.env mind RegularStyle in
+ let ci = make_case_info pb.env mind pb.casestyle in
let case = mkCase (ci,nf_betaiota pred,current,brvals) in
let inst = List.map mkRel deps in
{ uj_val = applist (case, inst);
@@ -2081,7 +2082,7 @@ let nf_evars_env evar_defs (env : env) : env =
Environ.fold_rel_context (fun e (na, b, t) e' -> Environ.push_rel (na, Option.map nf b, nf t) e')
~init:env' env
-let compile_cases loc (typing_fun, isevars) (tycon : Evarutil.type_constraint) env (predopt, tomatchl, eqns) =
+let compile_cases loc style (typing_fun, isevars) (tycon : Evarutil.type_constraint) env (predopt, tomatchl, eqns) =
(* We build the matrix of patterns and right-hand-side *)
let matx = matx_of_eqns env eqns in
@@ -2151,6 +2152,7 @@ let compile_cases loc (typing_fun, isevars) (tycon : Evarutil.type_constraint) e
history = start_history (List.length initial_pushed);
mat = matx;
caseloc = loc;
+ casestyle= style;
typing_function = typing_fun } in
let j = compile pb in
@@ -2180,6 +2182,7 @@ let compile_cases loc (typing_fun, isevars) (tycon : Evarutil.type_constraint) e
history = start_history (List.length initial_pushed);
mat = matx;
caseloc = loc;
+ casestyle= style;
typing_function = typing_fun } in
let j = compile pb in
diff --git a/contrib/subtac/subtac_pretyping_F.ml b/contrib/subtac/subtac_pretyping_F.ml
index 730b12605e..d3edb6e3cd 100644
--- a/contrib/subtac/subtac_pretyping_F.ml
+++ b/contrib/subtac/subtac_pretyping_F.ml
@@ -488,22 +488,8 @@ module SubtacPretyping_F (Coercion : Coercion.S) = struct
in
{ uj_val = v; uj_type = p }
- | RLetPattern (loc, c, p) ->
- (* Just use cases typing *)
- let j =
- pretype tycon env isevars lvar
- (RCases (loc, None, [c], [p]))
- in
- (* Change case info *)
- let j' = match kind_of_term j.uj_val with
- Case (ci, po, c, br) ->
- let pp_info = { ci.ci_pp_info with style = LetPatternStyle } in
- { j with uj_val = mkCase ({ ci with ci_pp_info = pp_info }, po, c, br) }
- | _ -> j
- in j'
-
- | RCases (loc,po,tml,eqns) ->
- Cases.compile_cases loc
+ | RCases (loc,sty,po,tml,eqns) ->
+ Cases.compile_cases loc sty
((fun vtyc env -> pretype vtyc env isevars lvar),isevars)
tycon env (* loc *) (po,tml,eqns)
generated by cgit v1.2.3 (git 2.25.1) at 2026-04-18 19:42:01 +0000