From 3ef7797ef6fc605dfafb32523261fe1b023aeecb Mon Sep 17 00:00:00 2001 From: Samuel Mimram Date: Fri, 28 Apr 2006 14:59:16 +0000 Subject: Imported Upstream version 8.0pl3+8.1alpha --- pretyping/pattern.ml | 160 +++++++++++++++++++++------------------------------ 1 file changed, 66 insertions(+), 94 deletions(-) (limited to 'pretyping/pattern.ml') diff --git a/pretyping/pattern.ml b/pretyping/pattern.ml index f58a12c6..390b884c 100644 --- a/pretyping/pattern.ml +++ b/pretyping/pattern.ml @@ -6,7 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(* $Id: pattern.ml,v 1.24.2.2 2004/11/26 17:51:52 herbelin Exp $ *) +(* $Id: pattern.ml 7732 2005-12-26 13:51:24Z herbelin $ *) open Util open Names @@ -17,18 +17,13 @@ open Rawterm open Environ open Nametab open Pp +open Mod_subst (* Metavariables *) type patvar_map = (patvar * constr) list -let patvar_of_int n = - let p = if !Options.v7 & not (Options.do_translate ()) then "?" else "X" - in - Names.id_of_string (p ^ string_of_int n) let pr_patvar = pr_id -let patvar_of_int_v7 n = Names.id_of_string ("?" ^ string_of_int n) - (* Patterns *) type constr_pattern = @@ -62,57 +57,6 @@ let rec occur_meta_pattern = function | PMeta _ | PSoApp _ -> true | PEvar _ | PVar _ | PRef _ | PRel _ | PSort _ | PFix _ | PCoFix _ -> false -let rec subst_pattern subst pat = match pat with - | PRef ref -> - let ref' = subst_global subst ref in - if ref' == ref then pat else - PRef ref' - | PVar _ - | PEvar _ - | PRel _ -> pat - | PApp (f,args) -> - let f' = subst_pattern subst f in - let args' = array_smartmap (subst_pattern subst) args in - if f' == f && args' == args then pat else - PApp (f',args') - | PSoApp (i,args) -> - let args' = list_smartmap (subst_pattern subst) args in - if args' == args then pat else - PSoApp (i,args') - | PLambda (name,c1,c2) -> - let c1' = subst_pattern subst c1 in - let c2' = subst_pattern subst c2 in - if c1' == c1 && c2' == c2 then pat else - PLambda (name,c1',c2') - | PProd (name,c1,c2) -> - let c1' = subst_pattern subst c1 in - let c2' = subst_pattern subst c2 in - if c1' == c1 && c2' == c2 then pat else - PProd (name,c1',c2') - | PLetIn (name,c1,c2) -> - let c1' = subst_pattern subst c1 in - let c2' = subst_pattern subst c2 in - if c1' == c1 && c2' == c2 then pat else - PLetIn (name,c1',c2') - | PSort _ - | PMeta _ -> pat - | PCase (cs,typ, c, branches) -> - let typ' = option_smartmap (subst_pattern subst) typ in - let c' = subst_pattern subst c in - let branches' = array_smartmap (subst_pattern subst) branches in - if typ' == typ && c' == c && branches' == branches then pat else - PCase(cs,typ', c', branches') - | PFix fixpoint -> - let cstr = mkFix fixpoint in - let fixpoint' = destFix (subst_mps subst cstr) in - if fixpoint' == fixpoint then pat else - PFix fixpoint' - | PCoFix cofixpoint -> - let cstr = mkCoFix cofixpoint in - let cofixpoint' = destCoFix (subst_mps subst cstr) in - if cofixpoint' == cofixpoint then pat else - PCoFix cofixpoint' - type constr_label = | ConstNode of constant | IndNode of inductive @@ -121,33 +65,14 @@ type constr_label = exception BoundPattern;; -let label_of_ref = function - | ConstRef sp -> ConstNode sp - | IndRef sp -> IndNode sp - | ConstructRef sp -> CstrNode sp - | VarRef id -> VarNode id - -let ref_of_label = function - | ConstNode sp -> ConstRef sp - | IndNode sp -> IndRef sp - | CstrNode sp -> ConstructRef sp - | VarNode id -> VarRef id - -let subst_label subst cstl = - let ref = ref_of_label cstl in - let ref' = subst_global subst ref in - if ref' == ref then cstl else - label_of_ref ref' - - let rec head_pattern_bound t = match t with | PProd (_,_,b) -> head_pattern_bound b | PLetIn (_,_,b) -> head_pattern_bound b | PApp (c,args) -> head_pattern_bound c | PCase (_,p,c,br) -> head_pattern_bound c - | PRef r -> label_of_ref r - | PVar id -> VarNode id + | PRef r -> r + | PVar id -> VarRef id | PEvar _ | PRel _ | PMeta _ | PSoApp _ | PSort _ | PFix _ -> raise BoundPattern (* Perhaps they were arguments, but we don't beta-reduce *) @@ -155,10 +80,10 @@ let rec head_pattern_bound t = | PCoFix _ -> anomaly "head_pattern_bound: not a type" let head_of_constr_reference c = match kind_of_term c with - | Const sp -> ConstNode sp - | Construct sp -> CstrNode sp - | Ind sp -> IndNode sp - | Var id -> VarNode id + | Const sp -> ConstRef sp + | Construct sp -> ConstructRef sp + | Ind sp -> IndRef sp + | Var id -> VarRef id | _ -> anomaly "Not a rigid reference" let rec pattern_of_constr t = @@ -168,7 +93,7 @@ let rec pattern_of_constr t = | Var id -> PVar id | Sort (Prop c) -> PSort (RProp c) | Sort (Type _) -> PSort (RType None) - | Cast (c,_) -> pattern_of_constr c + | Cast (c,_,_) -> pattern_of_constr c | LetIn (na,c,_,b) -> PLetIn (na,pattern_of_constr c,pattern_of_constr b) | Prod (na,c,b) -> PProd (na,pattern_of_constr c,pattern_of_constr b) | Lambda (na,c,b) -> PLambda (na,pattern_of_constr c,pattern_of_constr b) @@ -198,9 +123,61 @@ let rec inst lvar = function (* Non recursive *) | (PEvar _ | PRel _ | PRef _ | PSort _ | PMeta _ as x) -> x (* Bound to terms *) - | (PFix _ | PCoFix _ as r) -> + | (PFix _ | PCoFix _) -> error ("Not instantiable pattern") +let rec subst_pattern subst pat = match pat with + | PRef ref -> + let ref',t = subst_global subst ref in + if ref' == ref then pat else + pattern_of_constr t + | PVar _ + | PEvar _ + | PRel _ -> pat + | PApp (f,args) -> + let f' = subst_pattern subst f in + let args' = array_smartmap (subst_pattern subst) args in + if f' == f && args' == args then pat else + PApp (f',args') + | PSoApp (i,args) -> + let args' = list_smartmap (subst_pattern subst) args in + if args' == args then pat else + PSoApp (i,args') + | PLambda (name,c1,c2) -> + let c1' = subst_pattern subst c1 in + let c2' = subst_pattern subst c2 in + if c1' == c1 && c2' == c2 then pat else + PLambda (name,c1',c2') + | PProd (name,c1,c2) -> + let c1' = subst_pattern subst c1 in + let c2' = subst_pattern subst c2 in + if c1' == c1 && c2' == c2 then pat else + PProd (name,c1',c2') + | PLetIn (name,c1,c2) -> + let c1' = subst_pattern subst c1 in + let c2' = subst_pattern subst c2 in + if c1' == c1 && c2' == c2 then pat else + PLetIn (name,c1',c2') + | PSort _ + | PMeta _ -> pat + | PCase (cs,typ, c, branches) -> + let typ' = option_smartmap (subst_pattern subst) typ in + let c' = subst_pattern subst c in + let branches' = array_smartmap (subst_pattern subst) branches in + if typ' == typ && c' == c && branches' == branches then pat else + PCase(cs,typ', c', branches') + | PFix fixpoint -> + let cstr = mkFix fixpoint in + let fixpoint' = destFix (subst_mps subst cstr) in + if fixpoint' == fixpoint then pat else + PFix fixpoint' + | PCoFix cofixpoint -> + let cstr = mkCoFix cofixpoint in + let cofixpoint' = destCoFix (subst_mps subst cstr) in + if cofixpoint' == cofixpoint then pat else + PCoFix cofixpoint' + + let instantiate_pattern = inst let rec pat_of_raw metas vars = function @@ -230,30 +207,25 @@ let rec pat_of_raw metas vars = function PSort s | RHole _ -> PMeta None - | RCast (_,c,t) -> + | RCast (_,c,_,t) -> Options.if_verbose Pp.warning "Cast not taken into account in constr pattern"; pat_of_raw metas vars c - | ROrderedCase (_,st,po,c,br,_) -> - PCase ((None,st),option_app (pat_of_raw metas vars) po, - pat_of_raw metas vars c, - Array.map (pat_of_raw metas vars) br) | 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,(po,_),[c,_],brs) -> + | RCases (loc,None,[c,_],brs) -> let sp = match brs with | (_,_,[PatCstr(_,(ind,_),_,_)],_)::_ -> Some ind | _ -> None in - (* When po disappears: switch to rtn type *) - PCase ((sp,Term.RegularStyle),option_app (pat_of_raw metas vars) po, + 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)) | r -> let loc = loc_of_rawconstr r in - user_err_loc (loc,"pattern_of_rawconstr", Pp.str "Not supported pattern") + user_err_loc (loc,"pattern_of_rawconstr", Pp.str "Pattern not supported") and pat_of_raw_branch loc metas vars ind brs i = let bri = List.filter -- cgit v1.2.3