From e978da8c41d8a3c19a29036d9c569fbe2a4616b0 Mon Sep 17 00:00:00 2001 From: Samuel Mimram Date: Fri, 16 Jun 2006 14:41:51 +0000 Subject: Imported Upstream version 8.0pl3+8.1beta --- pretyping/pattern.ml | 112 ++++++++++++++++++++++++++++++++++----------------- 1 file changed, 75 insertions(+), 37 deletions(-) (limited to 'pretyping/pattern.ml') 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") -- cgit v1.2.3