diff options
Diffstat (limited to 'pretyping/pattern.ml')
| -rw-r--r-- | pretyping/pattern.ml | 107 |
1 files changed, 57 insertions, 50 deletions
diff --git a/pretyping/pattern.ml b/pretyping/pattern.ml index b091d797ad..6e06f978f2 100644 --- a/pretyping/pattern.ml +++ b/pretyping/pattern.ml @@ -63,56 +63,11 @@ 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 + | CstrNode of constructor + | VarNode of identifier exception BoundPattern;; @@ -177,6 +132,58 @@ let rec inst lvar = function | (PFix _ | PCoFix _ as r) -> 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 |