summaryrefslogtreecommitdiff
path: root/pretyping/pattern.ml
diff options
context:
space:
mode:
Diffstat (limited to 'pretyping/pattern.ml')
-rw-r--r--pretyping/pattern.ml112
1 files changed, 75 insertions, 37 deletions
diff --git a/pretyping/pattern.ml b/pretyping/pattern.ml
index 390b884c..ef97250a 100644
--- a/pretyping/pattern.ml
+++ b/pretyping/pattern.ml
@@ -6,7 +6,7 @@
(* * GNU Lesser General Public License Version 2.1 *)
(************************************************************************)
-(* $Id: pattern.ml 7732 2005-12-26 13:51:24Z herbelin $ *)
+(* $Id: pattern.ml 8755 2006-04-27 22:22:15Z herbelin $ *)
open Util
open Names
@@ -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 * 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,28 +106,43 @@ 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
+ let no = Some (ci.ci_npar,cip.ind_nargs) in
+ PCase ((cip.style,ci.ci_cstr_nargs,Some ci.ci_ind,no),
+ 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 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)
- | PSoApp (n,pl) -> PSoApp (n, List.map (inst lvar) pl)
- | PLambda (n,a,b) -> PLambda (n,inst lvar a,inst lvar b)
- | PProd (n,a,b) -> PProd (n,inst lvar a,inst lvar b)
- | PLetIn (n,a,b) -> PLetIn (n,inst lvar a,inst lvar b)
- | PCase (ci,po,p,pl) ->
- PCase (ci,option_app (inst lvar) po,inst lvar p,Array.map (inst lvar) pl)
+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 *)
- | (PEvar _ | PRel _ | PRef _ | PSort _ | PMeta _ as x) -> x
+ | (PVar _ | PEvar _ | PRel _ | PRef _ | PSort _ | PMeta _
(* Bound to terms *)
- | (PFix _ | PCoFix _) ->
- error ("Not instantiable pattern")
+ | 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 subst_pattern subst pat = match pat with
| PRef ref ->
@@ -160,12 +178,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 +203,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 +238,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,n,nal) ->
+ rev_it_mkPLambda nal (mkPLambda na (pat_of_raw metas vars p)),
+ Some (n,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 +269,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 +285,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")
generated by cgit v1.2.3 (git 2.39.1) at 2024-05-15 01:24:59 +0000