aboutsummaryrefslogtreecommitdiff
path: root/pretyping
diff options
context:
space:
mode:
Diffstat (limited to 'pretyping')
-rw-r--r--pretyping/cases.ml97
-rw-r--r--pretyping/cases.mli2
-rw-r--r--pretyping/detyping.ml32
-rw-r--r--pretyping/pattern.ml4
-rw-r--r--pretyping/pretyping.ml18
-rw-r--r--pretyping/rawterm.ml18
-rw-r--r--pretyping/rawterm.mli3
7 files changed, 91 insertions, 83 deletions
diff --git a/pretyping/cases.ml b/pretyping/cases.ml
index b7317b5be0..e1c5beeea2 100644
--- a/pretyping/cases.ml
+++ b/pretyping/cases.ml
@@ -65,7 +65,7 @@ let error_needs_inversion env x t =
module type S = sig
val compile_cases :
- loc ->
+ loc -> case_style ->
(type_constraint -> env -> rawconstr -> unsafe_judgment) *
Evd.evar_defs ref ->
type_constraint ->
@@ -275,13 +275,14 @@ let push_history_pattern n current cont =
*)
type pattern_matching_problem =
- { env : env;
- evdref : Evd.evar_defs ref;
- pred : predicate_signature option;
- tomatch : tomatch_stack;
- history : pattern_continuation;
- mat : matrix;
- caseloc : loc;
+ { env : env;
+ evdref : Evd.evar_defs ref;
+ pred : predicate_signature option;
+ tomatch : tomatch_stack;
+ history : pattern_continuation;
+ mat : matrix;
+ caseloc : loc;
+ casestyle : case_style;
typing_function: type_constraint -> env -> rawconstr -> unsafe_judgment }
(*--------------------------------------------------------------------------*
@@ -1275,7 +1276,7 @@ and match_current pb tomatch =
let (pred,typ,s) =
find_predicate pb.caseloc pb.env pb.evdref
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);
@@ -1504,7 +1505,7 @@ let extract_arity_signature env0 tomatchl tmsign =
| Some (loc,_,_,_) ->
user_err_loc (loc,"",
str "Unexpected type annotation for a term of non inductive type"))
- | IsInd (_,IndType(indf,realargs)) ->
+ | IsInd (term,IndType(indf,realargs)) ->
let indf' = lift_inductive_family n indf in
let (ind,params) = dest_ind_family indf' in
let nrealargs = List.length realargs in
@@ -1519,6 +1520,14 @@ let extract_arity_signature env0 tomatchl tmsign =
List.rev realnal
| None -> list_tabulate (fun _ -> Anonymous) nrealargs in
let arsign = fst (get_arity env0 indf') in
+(* let na = *)
+(* match na with *)
+(* | Name _ -> na *)
+(* | Anonymous -> *)
+(* match kind_of_term term with *)
+(* | Rel n -> pi1 (lookup_rel n (Environ.rel_context env0)) *)
+(* | _ -> Anonymous *)
+(* in *)
(na,None,build_dependent_inductive env0 indf')
::(List.map2 (fun x (_,c,t) ->(x,c,t)) realnal arsign) in
let rec buildrec n = function
@@ -1537,6 +1546,34 @@ let inh_conv_coerce_to_tycon loc env evdref j tycon =
j
| None -> j
+(* We put the tycon inside the arity signature, possibly discovering dependencies. *)
+
+let prepare_predicate_from_arsign_tycon loc env evdref tomatchs sign arsign c =
+ let nar = List.fold_left (fun n sign -> List.length sign + n) 0 arsign in
+ let subst, len =
+ List.fold_left2 (fun (subst, len) (tm, tmtype) sign ->
+ let signlen = List.length sign in
+ match kind_of_term tm with
+ | Rel n when dependent tm c
+ && signlen = 1 (* The term to match is not of a dependent type itself *) ->
+ ((n, len) :: subst, len - signlen)
+ | _ -> (subst, len - signlen))
+ ([], nar) tomatchs arsign
+ in
+ let rec predicate lift c =
+ match kind_of_term c with
+ | Rel n when n > lift ->
+ (try
+ (* Make the predicate dependent on the matched variable *)
+ let idx = List.assoc (n - lift) subst in
+ mkRel (idx + lift)
+ with Not_found ->
+ (* A variable that is not matched, lift over the arsign. *)
+ mkRel (n + nar))
+ | _ ->
+ map_constr_with_binders succ predicate lift c
+ in predicate 0 c
+
(* Builds the predicate. If the predicate is dependent, its context is
* made of 1+nrealargs assumptions for each matched term in an inductive
@@ -1545,7 +1582,8 @@ let inh_conv_coerce_to_tycon loc env evdref j tycon =
* Each matched terms are independently considered dependent or not.
- * A type constraint but no annotation case: it is assumed non dependent.
+ * A type constraint but no annotation case: we try to specialize the
+ * tycon to make the predicate if it is not closed.
*)
let prepare_predicate loc typing_fun evdref env tomatchs sign tycon = function
@@ -1553,9 +1591,23 @@ let prepare_predicate loc typing_fun evdref env tomatchs sign tycon = function
| None ->
(match tycon with
| Some (None, t) ->
- let names,pred =
- prepare_predicate_from_tycon loc false env evdref tomatchs sign t
- in Some (build_initial_predicate false names pred)
+ if noccur_with_meta 0 max_int t then
+ let names,pred =
+ prepare_predicate_from_tycon loc false env evdref tomatchs sign t
+ in
+ Some (build_initial_predicate false names pred)
+ else
+ let arsign = extract_arity_signature env tomatchs sign in
+ let env' = List.fold_right push_rels arsign env in
+ let names = List.rev (List.map (List.map pi1) arsign) in
+ let pred = prepare_predicate_from_arsign_tycon loc env' evdref tomatchs sign arsign t in
+ if eq_constr pred t then
+ let names,pred =
+ prepare_predicate_from_tycon loc false env evdref tomatchs sign t
+ in
+ Some (build_initial_predicate false names pred)
+ else
+ Some (build_initial_predicate true names pred)
| _ -> None)
(* Some type annotation *)
@@ -1577,7 +1629,7 @@ let prepare_predicate loc typing_fun evdref env tomatchs sign tycon = function
(**************************************************************************)
(* Main entry of the matching compilation *)
-let compile_cases loc (typing_fun, evdref) (tycon : Evarutil.type_constraint) env (predopt, tomatchl, eqns)=
+let compile_cases loc style (typing_fun, evdref) (tycon : Evarutil.type_constraint) env (predopt, tomatchl, eqns)=
(* We build the matrix of patterns and right-hand-side *)
let matx = matx_of_eqns env tomatchl eqns in
@@ -1596,13 +1648,14 @@ let compile_cases loc (typing_fun, evdref) (tycon : Evarutil.type_constraint) en
let initial_pushed = List.map (fun tm -> Pushed (tm,[])) tomatchs in
let pb =
- { env = env;
- evdref = evdref;
- pred = pred;
- tomatch = initial_pushed;
- history = start_history (List.length initial_pushed);
- mat = matx;
- caseloc = loc;
+ { env = env;
+ evdref = evdref;
+ pred = pred;
+ tomatch = initial_pushed;
+ 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/pretyping/cases.mli b/pretyping/cases.mli
index d105ca2d0f..a2015c2b17 100644
--- a/pretyping/cases.mli
+++ b/pretyping/cases.mli
@@ -50,7 +50,7 @@ val error_needs_inversion : env -> constr -> types -> 'a
module type S = sig
val compile_cases :
- loc ->
+ loc -> case_style ->
(type_constraint -> env -> rawconstr -> unsafe_judgment) * evar_defs ref ->
type_constraint ->
env -> rawconstr option * tomatch_tuples * cases_clauses ->
diff --git a/pretyping/detyping.ml b/pretyping/detyping.ml
index 34e6945584..164043cf7c 100644
--- a/pretyping/detyping.ml
+++ b/pretyping/detyping.ml
@@ -349,8 +349,6 @@ let detype_case computable detype detype_eqns testdep avoid data p c bl =
let bl' = Array.map detype bl in
let (nal,d) = it_destRLambda_or_LetIn_names consnargsl.(0) bl'.(0) in
RLetTuple (dl,nal,(alias,pred),tomatch,d)
- | LetPatternStyle when List.length eqnl = 1 -> (* If irrefutable due to some inversion, print as match *)
- RLetPattern (dl,(tomatch,(alias,aliastyp)),List.hd eqnl)
| IfStyle when aliastyp = None ->
let bl' = Array.map detype bl in
let nondepbrs =
@@ -359,9 +357,9 @@ let detype_case computable detype detype_eqns testdep avoid data p c bl =
RIf (dl,tomatch,(alias,pred),
Option.get nondepbrs.(0),Option.get nondepbrs.(1))
else
- RCases (dl,pred,[tomatch,(alias,aliastyp)],eqnl)
+ RCases (dl,tag,pred,[tomatch,(alias,aliastyp)],eqnl)
| _ ->
- RCases (dl,pred,[tomatch,(alias,aliastyp)],eqnl)
+ RCases (dl,tag,pred,[tomatch,(alias,aliastyp)],eqnl)
let detype_sort = function
| Prop c -> RProp c
@@ -605,7 +603,7 @@ let rec subst_rawconstr subst raw =
if r1' == r1 && r2' == r2 then raw else
RLetIn (loc,n,r1',r2')
- | RCases (loc,rtno,rl,branches) ->
+ | RCases (loc,sty,rtno,rl,branches) ->
let rtno' = Option.smartmap (subst_rawconstr subst) rtno
and rl' = list_smartmap (fun (a,x as y) ->
let a' = subst_rawconstr subst a in
@@ -625,7 +623,7 @@ let rec subst_rawconstr subst raw =
branches
in
if rtno' == rtno && rl' == rl && branches' == branches then raw else
- RCases (loc,rtno',rl',branches')
+ RCases (loc,sty,rtno',rl',branches')
| RLetTuple (loc,nal,(na,po),b,c) ->
let po' = Option.smartmap (subst_rawconstr subst) po
@@ -633,28 +631,6 @@ let rec subst_rawconstr subst raw =
and c' = subst_rawconstr subst c in
if po' == po && b' == b && c' == c then raw else
RLetTuple (loc,nal,(na,po'),b',c')
-
- | RLetPattern (loc, (a,x as c), (loc',idl,cpl,r as branch)) ->
- let c' =
- let a' = subst_rawconstr subst a in
- let (n,topt) = x in
- let topt' = Option.smartmap
- (fun (loc,(sp,i),x,y as t) ->
- let sp' = subst_kn subst sp in
- if sp == sp' then t else (loc,(sp',i),x,y))
- topt
- in
- if a == a' && topt == topt' then c else (a',(n,topt'))
- in
- let p' =
- let cpl' =
- list_smartmap (subst_cases_pattern subst) cpl
- and r' = subst_rawconstr subst r in
- if cpl' == cpl && r' == r then branch else
- (loc',idl,cpl',r')
- in
- if c' == c && p' == branch then raw else
- RLetPattern (loc, c', p')
| RIf (loc,c,(na,po),b1,b2) ->
let po' = Option.smartmap (subst_rawconstr subst) po
diff --git a/pretyping/pattern.ml b/pretyping/pattern.ml
index 845f9fae1f..90a3728ebb 100644
--- a/pretyping/pattern.ml
+++ b/pretyping/pattern.ml
@@ -245,7 +245,7 @@ let rec pat_of_raw metas vars = function
let c = List.fold_left mkRLambda c nal in
PCase ((LetStyle,[|1|],None,None),PMeta None,pat_of_raw metas vars b,
[|pat_of_raw metas vars c|])
- | RCases (loc,p,[c,(na,indnames)],brs) ->
+ | RCases (loc,sty,p,[c,(na,indnames)],brs) ->
let pred,ind_nargs, ind = match p,indnames with
| Some p, Some (_,ind,n,nal) ->
rev_it_mkPLambda nal (mkPLambda na (pat_of_raw metas vars p)),
@@ -259,7 +259,7 @@ let rec pat_of_raw metas vars = function
Array.init (List.length brs) (pat_of_raw_branch loc metas vars ind brs)
in
let cstr_nargs,brs = (Array.map fst cbrs, Array.map snd cbrs) in
- PCase ((RegularStyle,cstr_nargs,ind,ind_nargs), pred,
+ PCase ((sty,cstr_nargs,ind,ind_nargs), pred,
pat_of_raw metas vars c, brs)
| r ->
diff --git a/pretyping/pretyping.ml b/pretyping/pretyping.ml
index f9fcdb7b63..83381710d3 100644
--- a/pretyping/pretyping.ml
+++ b/pretyping/pretyping.ml
@@ -582,23 +582,9 @@ module Pretyping_F (Coercion : Coercion.S) = struct
mkCase (ci, pred, cj.uj_val, [|b1;b2|])
in
{ uj_val = v; uj_type = p }
-
- | RLetPattern (loc, c, p) ->
- (* Just use cases typing *)
- let j =
- pretype tycon env evdref 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 evdref lvar),evdref)
tycon env (* loc *) (po,tml,eqns)
diff --git a/pretyping/rawterm.ml b/pretyping/rawterm.ml
index e7f5de028f..fe48cd4fa7 100644
--- a/pretyping/rawterm.ml
+++ b/pretyping/rawterm.ml
@@ -62,10 +62,9 @@ type rawconstr =
| RLambda of loc * name * binding_kind * rawconstr * rawconstr
| RProd of loc * name * binding_kind * rawconstr * rawconstr
| RLetIn of loc * name * rawconstr * rawconstr
- | RCases of loc * rawconstr option * tomatch_tuples * cases_clauses
+ | RCases of loc * case_style * rawconstr option * tomatch_tuples * cases_clauses
| RLetTuple of loc * name list * (name * rawconstr option) *
rawconstr * rawconstr
- | RLetPattern of loc * tomatch_tuple * cases_clause
| RIf of loc * rawconstr * (name * rawconstr option) * rawconstr * rawconstr
| RRec of loc * fix_kind * identifier array * rawdecl list array *
rawconstr array * rawconstr array
@@ -115,14 +114,12 @@ let map_rawconstr f = function
| RLambda (loc,na,bk,ty,c) -> RLambda (loc,na,bk,f ty,f c)
| RProd (loc,na,bk,ty,c) -> RProd (loc,na,bk,f ty,f c)
| RLetIn (loc,na,b,c) -> RLetIn (loc,na,f b,f c)
- | RCases (loc,rtntypopt,tml,pl) ->
- RCases (loc,Option.map f rtntypopt,
+ | RCases (loc,sty,rtntypopt,tml,pl) ->
+ RCases (loc,sty,Option.map f rtntypopt,
List.map (fun (tm,x) -> (f tm,x)) tml,
List.map (fun (loc,idl,p,c) -> (loc,idl,p,f c)) pl)
| RLetTuple (loc,nal,(na,po),b,c) ->
RLetTuple (loc,nal,(na,Option.map f po),f b,f c)
- | RLetPattern (loc,(b,x),(loc',idl,p,c)) ->
- RLetPattern (loc,(f b,x),(loc',idl,p,f c))
| RIf (loc,c,(na,po),b1,b2) ->
RIf (loc,f c,(na,Option.map f po),f b1,f b2)
| RRec (loc,fk,idl,bl,tyl,bv) ->
@@ -177,14 +174,13 @@ let occur_rawconstr id =
| RLambda (loc,na,bk,ty,c) -> (occur ty) or ((na <> Name id) & (occur c))
| RProd (loc,na,bk,ty,c) -> (occur ty) or ((na <> Name id) & (occur c))
| RLetIn (loc,na,b,c) -> (occur b) or ((na <> Name id) & (occur c))
- | RCases (loc,rtntypopt,tml,pl) ->
+ | RCases (loc,sty,rtntypopt,tml,pl) ->
(occur_option rtntypopt)
or (List.exists (fun (tm,_) -> occur tm) tml)
or (List.exists occur_pattern pl)
| RLetTuple (loc,nal,rtntyp,b,c) ->
occur_return_type rtntyp id
or (occur b) or (not (List.mem (Name id) nal) & (occur c))
- | RLetPattern (loc, (b, _), p) -> (occur b) or (occur_pattern p)
| RIf (loc,c,rtntyp,b1,b2) ->
occur_return_type rtntyp id or (occur c) or (occur b1) or (occur b2)
| RRec (loc,fk,idl,bl,tyl,bv) ->
@@ -224,7 +220,7 @@ let free_rawvars =
let vs' = vars bounded vs ty in
let bounded' = add_name_to_ids bounded na in
vars bounded' vs' c
- | RCases (loc,rtntypopt,tml,pl) ->
+ | RCases (loc,sty,rtntypopt,tml,pl) ->
let vs1 = vars_option bounded vs rtntypopt in
let vs2 = List.fold_left (fun vs (tm,_) -> vars bounded vs tm) vs1 tml in
List.fold_left (vars_pattern bounded) vs2 pl
@@ -233,7 +229,6 @@ let free_rawvars =
let vs2 = vars bounded vs1 b in
let bounded' = List.fold_left add_name_to_ids bounded nal in
vars bounded' vs2 c
- | RLetPattern (loc, (c, _), p) -> vars_pattern bounded (vars bounded vs c) p
| RIf (loc,c,rtntyp,b1,b2) ->
let vs1 = vars_return_type bounded vs rtntyp in
let vs2 = vars bounded vs1 c in
@@ -285,8 +280,7 @@ let loc_of_rawconstr = function
| RLambda (loc,_,_,_,_) -> loc
| RProd (loc,_,_,_,_) -> loc
| RLetIn (loc,_,_,_) -> loc
- | RLetPattern (loc,_,_) -> loc
- | RCases (loc,_,_,_) -> loc
+ | RCases (loc,_,_,_,_) -> loc
| RLetTuple (loc,_,_,_,_) -> loc
| RIf (loc,_,_,_,_) -> loc
| RRec (loc,_,_,_,_,_) -> loc
diff --git a/pretyping/rawterm.mli b/pretyping/rawterm.mli
index 7b342c4115..ab67a0922b 100644
--- a/pretyping/rawterm.mli
+++ b/pretyping/rawterm.mli
@@ -66,10 +66,9 @@ type rawconstr =
| RLambda of loc * name * binding_kind * rawconstr * rawconstr
| RProd of loc * name * binding_kind * rawconstr * rawconstr
| RLetIn of loc * name * rawconstr * rawconstr
- | RCases of loc * rawconstr option * tomatch_tuples * cases_clauses
+ | RCases of loc * case_style * rawconstr option * tomatch_tuples * cases_clauses
| RLetTuple of loc * name list * (name * rawconstr option) *
rawconstr * rawconstr
- | RLetPattern of loc * tomatch_tuple * cases_clause
| RIf of loc * rawconstr * (name * rawconstr option) * rawconstr * rawconstr
| RRec of loc * fix_kind * identifier array * rawdecl list array *
rawconstr array * rawconstr array
generated by cgit v1.2.3 (git 2.25.1) at 2026-05-04 06:42:42 +0000