aboutsummaryrefslogtreecommitdiff
path: root/pretyping
diff options
context:
space:
mode:
Diffstat (limited to 'pretyping')
-rw-r--r--pretyping/matching.ml34
-rw-r--r--pretyping/pattern.ml102
-rw-r--r--pretyping/pattern.mli7
3 files changed, 109 insertions, 34 deletions
diff --git a/pretyping/matching.ml b/pretyping/matching.ml
index 462fe1eb1d..2b0a0ac7b2 100644
--- a/pretyping/matching.ml
+++ b/pretyping/matching.ml
@@ -17,6 +17,7 @@ open Termops
open Reductionops
open Term
open Rawterm
+open Sign
open Environ
open Pattern
(*i*)
@@ -70,6 +71,11 @@ let memb_metavars m n =
let eq_context ctxt1 ctxt2 = array_for_all2 eq_constr ctxt1 ctxt2
+let same_case_structure (_,cs1,ind,_) ci2 br1 br2 =
+ match ind with
+ | Some ind -> ind = ci2.ci_ind
+ | None -> cs1 = ci2.ci_cstr_nargs
+
let matches_core convert allow_partial_app pat c =
let rec sorec stk sigma p t =
let cT = strip_outer_cast t in
@@ -79,7 +85,7 @@ let matches_core convert allow_partial_app pat c =
List.map
(function
| PRel n -> n
- | _ -> error "Only bound indices are currently allowed in second order pattern matching")
+ | _ -> error "Only bound indices allowed in second order pattern matching")
args in
let frels = Intset.elements (free_rels cT) in
if list_subset frels relargs then
@@ -150,15 +156,27 @@ let matches_core convert allow_partial_app pat c =
if is_conv env evars c cT then sigma
else raise PatternMatchingFailure
- | PCase (_,_,a1,br1), Case (_,_,a2,br2) ->
- (* On ne teste pas le prédicat *)
- if (Array.length br1) = (Array.length br2) then
- array_fold_left2 (sorec stk) (sorec stk sigma a1 a2) br1 br2
+ | PIf (a1,b1,b1'), Case (ci,_,a2,[|b2;b2'|]) ->
+ let ctx,b2 = decompose_prod_n_assum ci.ci_cstr_nargs.(0) b2 in
+ let ctx',b2' = decompose_prod_n_assum ci.ci_cstr_nargs.(1) b2' in
+ let n = List.length ctx and n' = List.length ctx' in
+ if noccur_between 1 n b2 & noccur_between 1 n' b2' then
+ let s = List.fold_left (fun l (na,_,t) -> (na,t)::l) stk ctx in
+ let s' = List.fold_left (fun l (na,_,t) -> (na,t)::l) stk ctx' in
+ let b1 = lift_pattern n b1 and b1' = lift_pattern n' b1' in
+ sorec s' (sorec s (sorec stk sigma a1 a2) b1 b2) b1' b2'
else
raise PatternMatchingFailure
- (* À faire *)
- | PFix f0, Fix f1 when f0 = f1 -> sigma
- | PCoFix c0, CoFix c1 when c0 = c1 -> sigma
+
+ | PCase (ci1,p1,a1,br1), Case (ci2,p2,a2,br2) ->
+ if same_case_structure ci1 ci2 br1 br2 then
+ array_fold_left2 (sorec stk)
+ (sorec stk (sorec stk sigma a1 a2) p1 p2) br1 br2
+ else
+ raise PatternMatchingFailure
+
+ | PFix c1, Fix _ when eq_constr (mkFix c1) cT -> sigma
+ | PCoFix c1, CoFix _ when eq_constr (mkCoFix c1) cT -> sigma
| _ -> raise PatternMatchingFailure
in
diff --git a/pretyping/pattern.ml b/pretyping/pattern.ml
index 634f0b5915..9029578cd2 100644
--- a/pretyping/pattern.ml
+++ b/pretyping/pattern.ml
@@ -38,8 +38,9 @@ type constr_pattern =
| PLetIn of name * constr_pattern * constr_pattern
| PSort of rawsort
| PMeta of patvar option
- | PCase of (inductive option * case_style)
- * constr_pattern option * constr_pattern * constr_pattern array
+ | PIf of constr_pattern * constr_pattern * constr_pattern
+ | PCase of (case_style * int array * inductive option * int option)
+ * constr_pattern * constr_pattern * constr_pattern array
| PFix of fixpoint
| PCoFix of cofixpoint
@@ -49,9 +50,10 @@ let rec occur_meta_pattern = function
| PLambda (na,t,c) -> (occur_meta_pattern t) or (occur_meta_pattern c)
| PProd (na,t,c) -> (occur_meta_pattern t) or (occur_meta_pattern c)
| PLetIn (na,t,c) -> (occur_meta_pattern t) or (occur_meta_pattern c)
- | PCase(_,None,c,br) ->
- (occur_meta_pattern c) or (array_exists occur_meta_pattern br)
- | PCase(_,Some p,c,br) ->
+ | PIf (c,c1,c2) ->
+ (occur_meta_pattern c) or
+ (occur_meta_pattern c1) or (occur_meta_pattern c2)
+ | PCase(_,p,c,br) ->
(occur_meta_pattern p) or
(occur_meta_pattern c) or (array_exists occur_meta_pattern br)
| PMeta _ | PSoApp _ -> true
@@ -70,6 +72,7 @@ let rec head_pattern_bound t =
| PProd (_,_,b) -> head_pattern_bound b
| PLetIn (_,_,b) -> head_pattern_bound b
| PApp (c,args) -> head_pattern_bound c
+ | PIf (c,_,_) -> head_pattern_bound c
| PCase (_,p,c,br) -> head_pattern_bound c
| PRef r -> r
| PVar id -> VarRef id
@@ -103,14 +106,44 @@ let rec pattern_of_constr t =
| Construct sp -> PRef (ConstructRef sp)
| Evar (n,ctxt) -> PEvar (n,Array.map pattern_of_constr ctxt)
| Case (ci,p,a,br) ->
- PCase ((Some ci.ci_ind,ci.ci_pp_info.style),
- Some (pattern_of_constr p),pattern_of_constr a,
+ let cip = ci.ci_pp_info in
+ PCase ((cip.style,ci.ci_cstr_nargs,Some ci.ci_ind,Some cip.ind_nargs),
+ pattern_of_constr p,pattern_of_constr a,
Array.map pattern_of_constr br)
| Fix f -> PFix f
| CoFix f -> PCoFix f
(* To process patterns, we need a translation without typing at all. *)
+let map_pattern_with_binders g f l = function
+ | PApp (p,pl) -> PApp (f l p, Array.map (f l) pl)
+ | PSoApp (n,pl) -> PSoApp (n, List.map (f l) pl)
+ | PLambda (n,a,b) -> PLambda (n,f l a,f (g l) b)
+ | PProd (n,a,b) -> PProd (n,f l a,f (g l) b)
+ | PLetIn (n,a,b) -> PLetIn (n,f l a,f (g l) b)
+ | PIf (c,b1,b2) -> PIf (f l c,f l b1,f l b2)
+ | PCase (ci,po,p,pl) -> PCase (ci,f l po,f l p,Array.map (f l) pl)
+ (* Non recursive *)
+ | (PVar _ | PEvar _ | PRel _ | PRef _ | PSort _ | PMeta _
+ (* Bound to terms *)
+ | PFix _ | PCoFix _ as x) -> x
+
+let map_pattern f = map_pattern_with_binders (fun () -> ()) (fun () -> f) ()
+
+let rec instantiate_pattern lvar = function
+ | PVar id as x -> (try List.assoc id lvar with Not_found -> x)
+ | (PFix _ | PCoFix _) -> error ("Not instantiable pattern")
+ | c -> map_pattern (instantiate_pattern lvar) c
+
+let rec liftn_pattern k n = function
+ | PRel i as x -> if i >= n then PRel (i+k) else x
+ | PFix x -> PFix (destFix (liftn k n (mkFix x)))
+ | PCoFix x -> PCoFix (destCoFix (liftn k n (mkCoFix x)))
+ | c -> map_pattern_with_binders succ (liftn_pattern k) n c
+
+let lift_pattern k = liftn_pattern k 1
+
+(*
let rec inst lvar = function
| PVar id as x -> (try List.assoc id lvar with Not_found -> x)
| PApp (p,pl) -> PApp (inst lvar p, Array.map (inst lvar) pl)
@@ -125,6 +158,7 @@ let rec inst lvar = function
(* Bound to terms *)
| (PFix _ | PCoFix _) ->
error ("Not instantiable pattern")
+*)
let rec subst_pattern subst pat = match pat with
| PRef ref ->
@@ -160,12 +194,20 @@ let rec subst_pattern subst pat = match pat with
PLetIn (name,c1',c2')
| PSort _
| PMeta _ -> pat
- | PCase (cs,typ, c, branches) ->
- let typ' = option_smartmap (subst_pattern subst) typ in
+ | PIf (c,c1,c2) ->
+ let c' = subst_pattern subst c in
+ let c1' = subst_pattern subst c1 in
+ let c2' = subst_pattern subst c2 in
+ if c' == c && c1' == c1 && c2' == c2 then pat else
+ PIf (c',c1',c2')
+ | PCase ((a,b,ind,n as cs),typ,c,branches) ->
+ let ind' = option_smartmap (Inductiveops.subst_inductive subst) ind in
+ let typ' = subst_pattern subst typ in
let c' = subst_pattern subst c in
let branches' = array_smartmap (subst_pattern subst) branches in
+ let cs' = if ind == ind' then cs else (a,b,ind',n) in
if typ' == typ && c' == c && branches' == branches then pat else
- PCase(cs,typ', c', branches')
+ PCase(cs',typ', c', branches')
| PFix fixpoint ->
let cstr = mkFix fixpoint in
let fixpoint' = destFix (subst_mps subst cstr) in
@@ -177,8 +219,8 @@ let rec subst_pattern subst pat = match pat with
if cofixpoint' == cofixpoint then pat else
PCoFix cofixpoint'
-
-let instantiate_pattern = inst
+let mkPLambda na b = PLambda(na,PMeta None,b)
+let rev_it_mkPLambda = List.fold_right mkPLambda
let rec pat_of_raw metas vars = function
| RVar (_,id) ->
@@ -212,17 +254,30 @@ let rec pat_of_raw metas vars = function
Pp.warning "Cast not taken into account in constr pattern";
pat_of_raw metas vars c
| RIf (_,c,(_,None),b1,b2) ->
- PCase ((None,IfStyle),None, pat_of_raw metas vars c,
- [|pat_of_raw metas vars b1; pat_of_raw metas vars b2|])
- | RCases (loc,None,[c,_],brs) ->
- let sp =
+ PIf (pat_of_raw metas vars c,
+ pat_of_raw metas vars b1,pat_of_raw metas vars b2)
+ | RLetTuple (loc,nal,(_,None),b,c) ->
+ let mkRLambda c na = RLambda (loc,na,RHole (loc,Evd.InternalHole),c) in
+ 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) ->
+ let pred,ind_nargs, ind = match p,indnames with
+ | Some p, Some (_,ind,nal) ->
+ rev_it_mkPLambda nal (mkPLambda na (pat_of_raw metas vars p)),
+ Some (List.length nal),Some ind
+ | _ -> PMeta None, None, None in
+ let ind = match ind with Some _ -> ind | None ->
match brs with
| (_,_,[PatCstr(_,(ind,_),_,_)],_)::_ -> Some ind
| _ -> None in
- PCase ((sp,Term.RegularStyle),None,
- pat_of_raw metas vars c,
- Array.init (List.length brs)
- (pat_of_raw_branch loc metas vars sp brs))
+ let cbrs =
+ 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,
+ pat_of_raw metas vars c, brs)
+
| r ->
let loc = loc_of_rawconstr r in
user_err_loc (loc,"pattern_of_rawconstr", Pp.str "Pattern not supported")
@@ -230,12 +285,12 @@ let rec pat_of_raw metas vars = function
and pat_of_raw_branch loc metas vars ind brs i =
let bri = List.filter
(function
- (_,_,[PatCstr(_,c,lv,_)],_) -> snd c = i+1
+ (_,_,[PatCstr(_,c,lv,Anonymous)],_) -> snd c = i+1
| (loc,_,_,_) ->
user_err_loc (loc,"pattern_of_rawconstr",
Pp.str "Not supported pattern")) brs in
match bri with
- [(_,_,[PatCstr(_,(indsp,_),lv,_)],br)] ->
+ | [(_,_,[PatCstr(_,(indsp,_),lv,_)],br)] ->
if ind <> None & ind <> Some indsp then
user_err_loc (loc,"pattern_of_rawconstr",
Pp.str "All constructors must be in the same inductive type");
@@ -246,8 +301,7 @@ and pat_of_raw_branch loc metas vars ind brs i =
user_err_loc (loc,"pattern_of_rawconstr",
Pp.str "Not supported pattern")) lv in
let vars' = List.rev lna @ vars in
- List.fold_right (fun na b -> PLambda(na,PMeta None,b)) lna
- (pat_of_raw metas vars' br)
+ List.length lv, rev_it_mkPLambda lna (pat_of_raw metas vars' br)
| _ -> user_err_loc (loc,"pattern_of_rawconstr",
str "No unique branch for " ++ int (i+1) ++
str"-th constructor")
diff --git a/pretyping/pattern.mli b/pretyping/pattern.mli
index 0815f87211..4093f5e110 100644
--- a/pretyping/pattern.mli
+++ b/pretyping/pattern.mli
@@ -39,8 +39,9 @@ type constr_pattern =
| PLetIn of name * constr_pattern * constr_pattern
| PSort of rawsort
| PMeta of patvar option
- | PCase of (inductive option * case_style)
- * constr_pattern option * constr_pattern * constr_pattern array
+ | PIf of constr_pattern * constr_pattern * constr_pattern
+ | PCase of (case_style * int array * inductive option * int option)
+ * constr_pattern * constr_pattern * constr_pattern array
| PFix of fixpoint
| PCoFix of cofixpoint
@@ -76,3 +77,5 @@ val pattern_of_rawconstr : rawconstr ->
val instantiate_pattern :
(identifier * constr_pattern) list -> constr_pattern -> constr_pattern
+
+val lift_pattern : int -> constr_pattern -> constr_pattern
generated by cgit v1.2.3 (git 2.25.1) at 2026-05-05 03:38:55 +0000