aboutsummaryrefslogtreecommitdiffhomepage
path: root/pretyping
diff options
context:
space:
mode:
Diffstat (limited to 'pretyping')
-rw-r--r--pretyping/cases.ml50
-rw-r--r--pretyping/indrec.ml4
-rw-r--r--pretyping/inductiveops.ml9
-rw-r--r--pretyping/inductiveops.mli6
-rw-r--r--pretyping/pretyping.ml6
5 files changed, 23 insertions, 52 deletions
diff --git a/pretyping/cases.ml b/pretyping/cases.ml
index eb2d88f3d..f8c8e0a13 100644
--- a/pretyping/cases.ml
+++ b/pretyping/cases.ml
@@ -142,8 +142,7 @@ type equation =
rhs : rhs;
alias_stack : name list;
eqn_loc : loc;
- used : bool ref;
- tag : pattern_source }
+ used : bool ref }
type matrix = equation list
@@ -460,25 +459,6 @@ let remove_current_pattern eqn =
let prepend_pattern tms eqn = {eqn with patterns = tms@eqn.patterns }
(**********************************************************************)
-(* Dealing with regular and default patterns *)
-let is_regular eqn = eqn.tag = RegularPat
-
-let lower_pattern_status = function
- | RegularPat -> DefaultPat 0
- | DefaultPat n -> DefaultPat (n+1)
-
-let pattern_status pats =
- if array_exists ((=) RegularPat) pats then RegularPat
- else
- let min =
- Array.fold_right
- (fun pat n -> match pat with
- | DefaultPat i when i<n -> i
- | _ -> n)
- pats 0 in
- DefaultPat min
-
-(**********************************************************************)
(* Well-formedness tests *)
(* Partial check on patterns *)
@@ -536,7 +516,7 @@ let extract_rhs pb =
| [] -> errorlabstrm "build_leaf" (mssg_may_need_inversion())
| eqn::_ ->
set_used_pattern eqn;
- eqn.tag, eqn.rhs
+ eqn.rhs
(**********************************************************************)
(* Functions to deal with matrix factorization *)
@@ -1139,7 +1119,6 @@ let group_equations pb ind current cstrs mat =
(* This is a default clause that we expand *)
for i=1 to Array.length cstrs do
let args = make_anonymous_patvars cstrs.(i-1).cs_nargs in
- let rest = {rest with tag = lower_pattern_status rest.tag} in
brs.(i-1) <- (args, rest) :: brs.(i-1)
done
| PatCstr (loc,((_,i)),args,_) ->
@@ -1165,12 +1144,12 @@ let rec generalize_problem pb = function
(* No more patterns: typing the right-hand-side of equations *)
let build_leaf pb =
- let tag, rhs = extract_rhs pb in
+ let rhs = extract_rhs pb in
let tycon = match pb.pred with
| None -> empty_tycon
| Some (PrCcl typ) -> mk_tycon typ
| Some _ -> anomaly "not all parameters of pred have been consumed" in
- tag, pb.typing_function tycon rhs.rhs_env rhs.it
+ pb.typing_function tycon rhs.rhs_env rhs.it
(* Building the sub-problem when all patterns are variables *)
let shift_problem (current,t) pb =
@@ -1292,23 +1271,21 @@ and match_current pb tomatch =
let brs = array_map2 (compile_branch current deps pb) eqns cstrs in
(* We build the (elementary) case analysis *)
- let tags = Array.map (fun (t,_,_) -> t) brs in
- let brvals = Array.map (fun (_,v,_) -> v) brs in
- let brtyps = Array.map (fun (_,_,t) -> t) brs in
+ let brvals = Array.map (fun (v,_) -> v) brs in
+ let brtyps = Array.map (fun (_,t) -> t) brs in
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 tags in
+ let ci = make_case_info pb.env mind RegularStyle in
let case = mkCase (ci,nf_betaiota pred,current,brvals) in
let inst = List.map mkRel deps in
- pattern_status tags,
{ uj_val = applist (case, inst);
uj_type = substl inst typ }
and compile_branch current deps pb eqn cstr =
let sign, pb = build_branch current deps pb eqn cstr in
- let tag, j = compile pb in
- (tag, it_mkLambda_or_LetIn j.uj_val sign, j.uj_type)
+ let j = compile pb in
+ (it_mkLambda_or_LetIn j.uj_val sign, j.uj_type)
and compile_generalization pb d rest =
let pb =
@@ -1317,8 +1294,7 @@ and compile_generalization pb d rest =
tomatch = rest;
pred = option_map ungeneralize_predicate pb.pred;
mat = List.map (push_rels_eqn [d]) pb.mat } in
- let patstat,j = compile pb in
- patstat,
+ let j = compile pb in
{ uj_val = mkLambda_or_LetIn d j.uj_val;
uj_type = mkProd_or_LetIn d j.uj_type }
@@ -1344,8 +1320,7 @@ and compile_alias pb (deppat,nondeppat,d,t) rest =
pred = option_map (lift_predicate n) pb.pred;
history = history;
mat = mat } in
- let patstat,j = compile pb in
- patstat,
+ let j = compile pb in
List.fold_left mkSpecialLetInJudge j sign
(* pour les alias des initiaux, enrichir les env de ce qu'il faut et
@@ -1366,7 +1341,6 @@ let matx_of_eqns env tomatchl eqns =
avoid_ids = ids@(ids_of_named_context (named_context env));
it = initial_rhs } in
{ patterns = initial_lpat;
- tag = RegularPat;
alias_stack = [];
eqn_loc = loc;
used = ref false;
@@ -1632,7 +1606,7 @@ let compile_cases loc (typing_fun, isevars) (tycon : Evarutil.type_constraint) e
caseloc = loc;
typing_function = typing_fun } in
- let _, j = compile pb in
+ let j = compile pb in
(* We check for unused patterns *)
List.iter (check_unused_pattern env) matx;
inh_conv_coerce_to_tycon loc env isevars j tycon
diff --git a/pretyping/indrec.ml b/pretyping/indrec.ml
index 88bb055dc..7fd65050c 100644
--- a/pretyping/indrec.ml
+++ b/pretyping/indrec.ml
@@ -78,7 +78,7 @@ let mis_make_case_com depopt env sigma ind (mib,mip as specif) kind =
let depind = build_dependent_inductive env indf' in
let deparsign = (Anonymous,None,depind)::arsign in
- let ci = make_default_case_info env RegularStyle ind in
+ let ci = make_case_info env ind RegularStyle in
let pbody =
appvect
(mkRel (ndepar + nbprod),
@@ -350,7 +350,7 @@ let mis_make_indrec env sigma listdepkind mib =
(* body of i-th component of the mutual fixpoint *)
let deftyi =
- let ci = make_default_case_info env RegularStyle indi in
+ let ci = make_case_info env indi RegularStyle in
let concl = applist (mkRel (dect+j+ndepar),pargs) in
let pred =
it_mkLambda_or_LetIn_name env
diff --git a/pretyping/inductiveops.ml b/pretyping/inductiveops.ml
index 041187d84..69f921b79 100644
--- a/pretyping/inductiveops.ml
+++ b/pretyping/inductiveops.ml
@@ -131,21 +131,16 @@ let allowed_sorts env (kn,i as ind) =
mip.mind_kelim
(* Annotation for cases *)
-let make_case_info env ind style pats_source =
+let make_case_info env ind style =
let (mib,mip) = Inductive.lookup_mind_specif env ind in
- let print_info =
- { ind_nargs = mip.mind_nrealargs;
- style = style;
- source = pats_source } in
+ let print_info = { ind_nargs = mip.mind_nrealargs; style = style } in
{ ci_ind = ind;
ci_npar = mib.mind_nparams;
ci_cstr_nargs = mip.mind_consnrealdecls;
ci_pp_info = print_info }
let make_default_case_info env style ind =
- let (mib,mip) = Inductive.lookup_mind_specif env ind in
make_case_info env ind style
- (Array.map (fun _ -> RegularPat) mip.mind_consnames)
(*s Useful functions *)
diff --git a/pretyping/inductiveops.mli b/pretyping/inductiveops.mli
index 8285b8167..3cc24a184 100644
--- a/pretyping/inductiveops.mli
+++ b/pretyping/inductiveops.mli
@@ -105,9 +105,11 @@ val arity_of_case_predicate :
val type_case_branches_with_names :
env -> inductive * constr list -> unsafe_judgment -> constr ->
types array * types
-val make_case_info :
- env -> inductive -> case_style -> pattern_source array -> case_info
+val make_case_info : env -> inductive -> case_style -> case_info
+
+(*i Compatibility
val make_default_case_info : env -> case_style -> inductive -> case_info
+i*)
(********************)
val control_only_guard : env -> types -> unit
diff --git a/pretyping/pretyping.ml b/pretyping/pretyping.ml
index 81bd6987f..dc3ea869c 100644
--- a/pretyping/pretyping.ml
+++ b/pretyping/pretyping.ml
@@ -479,7 +479,7 @@ module Pretyping_F (Coercion : Coercion.S) = struct
let f = it_mkLambda_or_LetIn fj.uj_val fsign in
let v =
let mis,_ = dest_ind_family indf in
- let ci = make_default_case_info env LetStyle mis in
+ let ci = make_case_info env mis LetStyle in
mkCase (ci, p, cj.uj_val,[|f|]) in
{ uj_val = v; uj_type = substl (realargs@[cj.uj_val]) ccl }
@@ -498,7 +498,7 @@ module Pretyping_F (Coercion : Coercion.S) = struct
let p = it_mkLambda_or_LetIn (lift (nar+1) ccl) psign in
let v =
let mis,_ = dest_ind_family indf in
- let ci = make_default_case_info env LetStyle mis in
+ let ci = make_case_info env mis LetStyle in
mkCase (ci, p, cj.uj_val,[|f|] )
in
{ uj_val = v; uj_type = ccl })
@@ -568,7 +568,7 @@ module Pretyping_F (Coercion : Coercion.S) = struct
let b2 = f cstrs.(1) b2 in
let v =
let mis,_ = dest_ind_family indf in
- let ci = make_default_case_info env IfStyle mis in
+ let ci = make_case_info env mis IfStyle in
mkCase (ci, pred, cj.uj_val, [|b1;b2|])
in
{ uj_val = v; uj_type = p }
generated by cgit v1.2.3 (git 2.39.1) at 2024-07-03 00:26:36 +0000