diff options
Diffstat (limited to 'pretyping/patternops.ml')
| -rw-r--r-- | pretyping/patternops.ml | 29 |
1 files changed, 21 insertions, 8 deletions
diff --git a/pretyping/patternops.ml b/pretyping/patternops.ml index cc13d342a5..8557953cc4 100644 --- a/pretyping/patternops.ml +++ b/pretyping/patternops.ml @@ -81,6 +81,7 @@ and rec_declaration_eq (n1, c1, r1) (n2, c2, r2) = let rec occur_meta_pattern = function | PApp (f,args) -> (occur_meta_pattern f) || (Array.exists occur_meta_pattern args) + | PProj (_,arg) -> occur_meta_pattern arg | PLambda (na,t,c) -> (occur_meta_pattern t) || (occur_meta_pattern c) | PProd (na,t,c) -> (occur_meta_pattern t) || (occur_meta_pattern c) | PLetIn (na,t,c) -> (occur_meta_pattern t) || (occur_meta_pattern c) @@ -105,6 +106,7 @@ let rec head_pattern_bound t = | PCase (_,p,c,br) -> head_pattern_bound c | PRef r -> r | PVar id -> VarRef id + | PProj (p,c) -> ConstRef p | PEvar _ | PRel _ | PMeta _ | PSoApp _ | PSort _ | PFix _ -> raise BoundPattern (* Perhaps they were arguments, but we don't beta-reduce *) @@ -112,9 +114,9 @@ let rec head_pattern_bound t = | PCoFix _ -> anomaly ~label:"head_pattern_bound" (Pp.str "not a type") let head_of_constr_reference c = match kind_of_term c with - | Const sp -> ConstRef sp - | Construct sp -> ConstructRef sp - | Ind sp -> IndRef sp + | Const (sp,_) -> ConstRef sp + | Construct (sp,_) -> ConstructRef sp + | Ind (sp,_) -> IndRef sp | Var id -> VarRef id | _ -> anomaly (Pp.str "Not a rigid reference") @@ -145,9 +147,11 @@ let pattern_of_constr sigma t = with | Some n -> PSoApp (n,Array.to_list (Array.map pattern_of_constr a)) | None -> PApp (pattern_of_constr f,Array.map (pattern_of_constr) a)) - | Const sp -> PRef (ConstRef (constant_of_kn(canonical_con sp))) - | Ind sp -> PRef (canonical_gr (IndRef sp)) - | Construct sp -> PRef (canonical_gr (ConstructRef sp)) + | Const (sp,u) -> PRef (ConstRef (constant_of_kn(canonical_con sp))) + | Ind (sp,u) -> PRef (canonical_gr (IndRef sp)) + | Construct (sp,u) -> PRef (canonical_gr (ConstructRef sp)) + | Proj (p, c) -> + PProj (constant_of_kn(canonical_con p), pattern_of_constr c) | Evar (evk,ctxt as ev) -> (match snd (Evd.evar_source evk sigma) with | Evar_kinds.MatchingVar (b,id) -> @@ -185,6 +189,7 @@ let map_pattern_with_binders g f l = function | 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, List.map (fun (i,n,c) -> (i,n,f l c)) pl) + | PProj (p,pc) -> PProj (p, f l pc) (* Non recursive *) | (PVar _ | PEvar _ | PRel _ | PRef _ | PSort _ | PMeta _ (* Bound to terms *) @@ -240,6 +245,12 @@ let rec subst_pattern subst pat = | PVar _ | PEvar _ | PRel _ -> pat + | PProj (p,c) -> + let p',t = subst_global subst (ConstRef p) in + let p' = destConstRef p' in + let c' = subst_pattern subst c in + if p' == p && c' == c then pat else + PProj(p',c') | PApp (f,args) -> let f' = subst_pattern subst f in let args' = Array.smartmap (subst_pattern subst) args in @@ -274,7 +285,7 @@ let rec subst_pattern subst pat = PIf (c',c1',c2') | PCase (cip,typ,c,branches) -> let ind = cip.cip_ind in - let ind' = Option.smartmap (Inductiveops.subst_inductive subst) ind in + let ind' = Option.smartmap (subst_ind subst) ind in let cip' = if ind' == ind then cip else { cip with cip_ind = ind' } in let typ' = subst_pattern subst typ in let c' = subst_pattern subst c in @@ -308,11 +319,13 @@ let rec pat_of_raw metas vars = function with Not_found -> PVar id) | GPatVar (_,(false,n)) -> metas := n::!metas; PMeta (Some n) - | GRef (_,gr) -> + | GRef (_,gr,_) -> PRef (canonical_gr gr) (* Hack pour ne pas réécrire une interprétation complète des patterns*) | GApp (_, GPatVar (_,(true,n)), cl) -> metas := n::!metas; PSoApp (n, List.map (pat_of_raw metas vars) cl) + | GProj (_, p, c) -> + PProj (p, pat_of_raw metas vars c) | GApp (_,c,cl) -> PApp (pat_of_raw metas vars c, Array.of_list (List.map (pat_of_raw metas vars) cl)) |