diff options
Diffstat (limited to 'pretyping/pattern.ml')
| -rw-r--r-- | pretyping/pattern.ml | 120 |
1 files changed, 87 insertions, 33 deletions
diff --git a/pretyping/pattern.ml b/pretyping/pattern.ml index 057f9d1c..38da0a71 100644 --- a/pretyping/pattern.ml +++ b/pretyping/pattern.ml @@ -6,7 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(* $Id: pattern.ml 11309 2008-08-06 10:30:35Z herbelin $ *) +(* $Id$ *) open Util open Names @@ -21,8 +21,10 @@ open Mod_subst (* Metavariables *) +type constr_under_binders = identifier list * constr + type patvar_map = (patvar * constr) list -let pr_patvar = pr_id +type extended_patvar_map = (patvar * constr_under_binders) list (* Patterns *) @@ -69,8 +71,8 @@ exception BoundPattern;; let rec head_pattern_bound t = match t with - | PProd (_,_,b) -> head_pattern_bound b - | PLetIn (_,_,b) -> head_pattern_bound b + | 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 @@ -89,7 +91,11 @@ let head_of_constr_reference c = match kind_of_term c with | Var id -> VarRef id | _ -> anomaly "Not a rigid reference" -let rec pattern_of_constr t = +open Evd + +let pattern_of_constr sigma t = + let ctx = ref [] in + let rec pattern_of_constr t = match kind_of_term t with | Rel n -> PRel n | Meta n -> PMeta (Some (id_of_string ("META" ^ string_of_int n))) @@ -100,11 +106,29 @@ let rec pattern_of_constr t = | 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) - | App (f,a) -> PApp (pattern_of_constr f,Array.map pattern_of_constr a) - | Const sp -> PRef (ConstRef sp) - | Ind sp -> PRef (IndRef sp) - | Construct sp -> PRef (ConstructRef sp) - | Evar (n,ctxt) -> PEvar (n,Array.map pattern_of_constr ctxt) + | App (f,a) -> + (match + match kind_of_term f with + Evar (evk,args as ev) -> + (match snd (Evd.evar_source evk sigma) with + MatchingVar (true,id) -> + ctx := (id,None,existential_type sigma ev)::!ctx; + Some id + | _ -> None) + | _ -> None + 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)) + | Evar (evk,ctxt as ev) -> + (match snd (Evd.evar_source evk sigma) with + | MatchingVar (b,id) -> + ctx := (id,None,existential_type sigma ev)::!ctx; + assert (not b); PMeta (Some id) + | GoalEvar -> PEvar (evk,Array.map pattern_of_constr ctxt) + | _ -> PMeta None) | Case (ci,p,a,br) -> let cip = ci.ci_pp_info in let no = Some (ci.ci_npar,cip.ind_nargs) in @@ -112,16 +136,20 @@ let rec pattern_of_constr t = pattern_of_constr p,pattern_of_constr a, Array.map pattern_of_constr br) | Fix f -> PFix f - | CoFix f -> PCoFix f + | CoFix f -> PCoFix f in + let p = pattern_of_constr t in + (* side-effect *) + (* Warning: the order of dependencies in ctx is not ensured *) + (!ctx,p) (* To process patterns, we need a translation without typing at all. *) 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) + | PLambda (n,a,b) -> PLambda (n,f l a,f (g n l) b) + | PProd (n,a,b) -> PProd (n,f l a,f (g n l) b) + | PLetIn (n,a,b) -> PLetIn (n,f l a,f (g n 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 *) @@ -129,31 +157,54 @@ let map_pattern_with_binders g f l = function (* Bound to terms *) | PFix _ | PCoFix _ as x) -> x -let map_pattern f = map_pattern_with_binders (fun () -> ()) (fun () -> f) () +let map_pattern f = map_pattern_with_binders (fun _ () -> ()) (fun () -> f) () -let rec instantiate_pattern lvar = function - | PVar id as x -> (try Lazy.force(List.assoc id lvar) with Not_found -> x) +let error_instantiate_pattern id l = + let is = if List.length l = 1 then "is" else "are" in + errorlabstrm "" (str "Cannot substitute the term bound to " ++ pr_id id + ++ strbrk " in pattern because the term refers to " ++ pr_enum pr_id l + ++ strbrk " which " ++ str is ++ strbrk " not bound in the pattern.") + +let instantiate_pattern sigma lvar c = + let rec aux vars = function + | PVar id as x -> + (try + let ctx,c = List.assoc id lvar in + try + let inst = + List.map (fun id -> mkRel (list_index (Name id) vars)) ctx in + let c = substl inst c in + snd (pattern_of_constr sigma c) + with Not_found (* list_index failed *) -> + let vars = + list_map_filter (function Name id -> Some id | _ -> None) vars in + error_instantiate_pattern id (list_subtract ctx vars) + with Not_found (* List.assoc failed *) -> + x) | (PFix _ | PCoFix _) -> error ("Non instantiable pattern.") - | c -> map_pattern (instantiate_pattern lvar) c + | c -> + map_pattern_with_binders (fun id vars -> id::vars) aux vars c in + aux [] 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 + | c -> map_pattern_with_binders (fun _ -> succ) (liftn_pattern k) n c let lift_pattern k = liftn_pattern k 1 -let rec subst_pattern subst pat = match pat with +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 _ + snd (pattern_of_constr Evd.empty t) + | PVar _ | PEvar _ | PRel _ -> pat | PApp (f,args) -> - let f' = subst_pattern subst f in + 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') @@ -176,7 +227,7 @@ let rec subst_pattern subst pat = match pat with let c2' = subst_pattern subst c2 in if c1' == c1 && c2' == c2 then pat else PLetIn (name,c1',c2') - | PSort _ + | PSort _ | PMeta _ -> pat | PIf (c,c1,c2) -> let c' = subst_pattern subst c in @@ -186,12 +237,12 @@ let rec subst_pattern subst pat = match pat with 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 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 @@ -204,7 +255,7 @@ let rec subst_pattern subst pat = match pat with PCoFix cofixpoint' let mkPLambda na b = PLambda(na,PMeta None,b) -let rev_it_mkPLambda = List.fold_right mkPLambda +let rev_it_mkPLambda = List.fold_right mkPLambda let rec pat_of_raw metas vars = function | RVar (_,id) -> @@ -212,21 +263,24 @@ let rec pat_of_raw metas vars = function with Not_found -> PVar id) | RPatVar (_,(false,n)) -> metas := n::!metas; PMeta (Some n) - | RRef (_,r) -> - PRef r + | RRef (_,gr) -> + PRef (canonical_gr gr) (* Hack pour ne pas réécrire une interprétation complète des patterns*) | RApp (_, RPatVar (_,(true,n)), cl) -> metas := n::!metas; PSoApp (n, List.map (pat_of_raw metas vars) cl) - | RApp (_,c,cl) -> + | RApp (_,c,cl) -> PApp (pat_of_raw metas vars c, Array.of_list (List.map (pat_of_raw metas vars) cl)) | RLambda (_,na,bk,c1,c2) -> + name_iter (fun n -> metas := n::!metas) na; PLambda (na, pat_of_raw metas vars c1, pat_of_raw metas (na::vars) c2) | RProd (_,na,bk,c1,c2) -> + name_iter (fun n -> metas := n::!metas) na; PProd (na, pat_of_raw metas vars c1, pat_of_raw metas (na::vars) c2) | RLetIn (_,na,c1,c2) -> + name_iter (fun n -> metas := n::!metas) na; PLetIn (na, pat_of_raw metas vars c1, pat_of_raw metas (na::vars) c2) | RSort (_,s) -> @@ -261,7 +315,7 @@ let rec pat_of_raw metas vars = function let cstr_nargs,brs = (Array.map fst cbrs, Array.map snd cbrs) in PCase ((sty,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"Non supported pattern.") @@ -284,7 +338,7 @@ and pat_of_raw_branch loc metas vars ind brs i = | PatCstr(loc,_,_,_) -> user_err_loc (loc,"pattern_of_rawconstr", Pp.str "Non supported pattern.")) lv in - let vars' = List.rev lna @ vars in + let vars' = List.rev lna @ vars in 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) ++ @@ -292,5 +346,5 @@ and pat_of_raw_branch loc metas vars ind brs i = let pattern_of_rawconstr c = let metas = ref [] in - let p = pat_of_raw metas [] c in + let p = pat_of_raw metas [] c in (!metas,p) |