From 7cfc4e5146be5666419451bdd516f1f3f264d24a Mon Sep 17 00:00:00 2001 From: Enrico Tassi Date: Sun, 25 Jan 2015 14:42:51 +0100 Subject: Imported Upstream version 8.5~beta1+dfsg --- pretyping/patternops.ml | 429 ++++++++++++++++++++++++++++++++++++++++++++++++ 1 file changed, 429 insertions(+) create mode 100644 pretyping/patternops.ml (limited to 'pretyping/patternops.ml') diff --git a/pretyping/patternops.ml b/pretyping/patternops.ml new file mode 100644 index 00000000..c49bec9a --- /dev/null +++ b/pretyping/patternops.ml @@ -0,0 +1,429 @@ +(************************************************************************) +(* v * The Coq Proof Assistant / The Coq Development Team *) +(* eq_gr r1 r2 +| PVar v1, PVar v2 -> Id.equal v1 v2 +| PEvar (ev1, ctx1), PEvar (ev2, ctx2) -> + Evar.equal ev1 ev2 && Array.equal constr_pattern_eq ctx1 ctx2 +| PRel i1, PRel i2 -> + Int.equal i1 i2 +| PApp (t1, arg1), PApp (t2, arg2) -> + constr_pattern_eq t1 t2 && Array.equal constr_pattern_eq arg1 arg2 +| PSoApp (id1, arg1), PSoApp (id2, arg2) -> + Id.equal id1 id2 && List.equal constr_pattern_eq arg1 arg2 +| PLambda (v1, t1, b1), PLambda (v2, t2, b2) -> + Name.equal v1 v2 && constr_pattern_eq t1 t2 && constr_pattern_eq b1 b2 +| PProd (v1, t1, b1), PProd (v2, t2, b2) -> + Name.equal v1 v2 && constr_pattern_eq t1 t2 && constr_pattern_eq b1 b2 +| PLetIn (v1, t1, b1), PLetIn (v2, t2, b2) -> + Name.equal v1 v2 && constr_pattern_eq t1 t2 && constr_pattern_eq b1 b2 +| PSort s1, PSort s2 -> Miscops.glob_sort_eq s1 s2 +| PMeta m1, PMeta m2 -> Option.equal Id.equal m1 m2 +| PIf (t1, l1, r1), PIf (t2, l2, r2) -> + constr_pattern_eq t1 t2 && constr_pattern_eq l1 l2 && constr_pattern_eq r1 r2 +| PCase (info1, p1, r1, l1), PCase (info2, p2, r2, l2) -> + case_info_pattern_eq info1 info2 && + constr_pattern_eq p1 p2 && + constr_pattern_eq r1 r2 && + List.equal pattern_eq l1 l2 +| PFix f1, PFix f2 -> + fixpoint_eq f1 f2 +| PCoFix f1, PCoFix f2 -> + cofixpoint_eq f1 f2 +| _ -> false +(** FIXME: fixpoint and cofixpoint should be relativized to pattern *) + +and pattern_eq (i1, j1, p1) (i2, j2, p2) = + Int.equal i1 i2 && List.equal (==) j1 j2 && constr_pattern_eq p1 p2 + +and fixpoint_eq ((arg1, i1), r1) ((arg2, i2), r2) = + Int.equal i1 i2 && + Array.equal Int.equal arg1 arg2 && + rec_declaration_eq r1 r2 + +and cofixpoint_eq (i1, r1) (i2, r2) = + Int.equal i1 i2 && + rec_declaration_eq r1 r2 + +and rec_declaration_eq (n1, c1, r1) (n2, c2, r2) = + Array.equal Name.equal n1 n2 && + Array.equal Term.eq_constr c1 c2 && + Array.equal Term.eq_constr r1 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) + | PIf (c,c1,c2) -> + (occur_meta_pattern c) || + (occur_meta_pattern c1) || (occur_meta_pattern c2) + | PCase(_,p,c,br) -> + (occur_meta_pattern p) || + (occur_meta_pattern c) || + (List.exists (fun (_,_,p) -> occur_meta_pattern p) br) + | PMeta _ | PSoApp _ -> true + | PEvar _ | PVar _ | PRef _ | PRel _ | PSort _ | PFix _ | PCoFix _ -> false + +exception BoundPattern;; + +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 + | PIf (c,_,_) -> head_pattern_bound c + | PCase (_,p,c,br) -> head_pattern_bound c + | PRef r -> r + | PVar id -> VarRef id + | PProj (p,c) -> ConstRef (Projection.constant p) + | PEvar _ | PRel _ | PMeta _ | PSoApp _ | PSort _ | PFix _ + -> raise BoundPattern + (* Perhaps they were arguments, but we don't beta-reduce *) + | PLambda _ -> raise BoundPattern + | 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 + | Var id -> VarRef id + | _ -> anomaly (Pp.str "Not a rigid reference") + +let pattern_of_constr env sigma t = + let ctx = ref [] in + let rec pattern_of_constr env t = + match kind_of_term t with + | Rel n -> PRel n + | Meta n -> PMeta (Some (Id.of_string ("META" ^ string_of_int n))) + | Var id -> PVar id + | Sort (Prop Null) -> PSort GProp + | Sort (Prop Pos) -> PSort GSet + | Sort (Type _) -> PSort (GType []) + | Cast (c,_,_) -> pattern_of_constr env c + | LetIn (na,c,t,b) -> PLetIn (na,pattern_of_constr env c, + pattern_of_constr (push_rel (na,Some c,t) env) b) + | Prod (na,c,b) -> PProd (na,pattern_of_constr env c, + pattern_of_constr (push_rel (na, None, c) env) b) + | Lambda (na,c,b) -> PLambda (na,pattern_of_constr env c, + pattern_of_constr (push_rel (na, None, c) env) b) + | App (f,a) -> + (match + match kind_of_term f with + Evar (evk,args as ev) -> + (match snd (Evd.evar_source evk sigma) with + Evar_kinds.MatchingVar (true,id) -> + ctx := (id,None,Evarutil.nf_evar sigma (existential_type sigma ev))::!ctx; + Some id + | _ -> None) + | _ -> None + with + | Some n -> PSoApp (n,Array.to_list (Array.map (pattern_of_constr env) a)) + | None -> PApp (pattern_of_constr env f,Array.map (pattern_of_constr env) a)) + | 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) -> + pattern_of_constr env (Retyping.expand_projection env sigma p c []) + | Evar (evk,ctxt as ev) -> + (match snd (Evd.evar_source evk sigma) with + | Evar_kinds.MatchingVar (b,id) -> + ctx := (id,None,Evarutil.nf_evar sigma (existential_type sigma ev))::!ctx; + assert (not b); PMeta (Some id) + | Evar_kinds.GoalEvar -> PEvar (evk,Array.map (pattern_of_constr env) ctxt) + | _ -> PMeta None) + | Case (ci,p,a,br) -> + let cip = + { cip_style = ci.ci_pp_info.style; + cip_ind = Some ci.ci_ind; + cip_ind_tags = Some ci.ci_pp_info.ind_tags; + cip_extensible = false } + in + let branch_of_constr i c = + (i, ci.ci_pp_info.cstr_tags.(i), pattern_of_constr env c) + in + PCase (cip, pattern_of_constr env p, pattern_of_constr env a, + Array.to_list (Array.mapi branch_of_constr br)) + | Fix f -> PFix f + | CoFix f -> PCoFix f in + let p = pattern_of_constr env 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 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, 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 *) + | PFix _ | PCoFix _ as x) -> x + +let error_instantiate_pattern id l = + let is = match l with + | [_] -> "is" + | _ -> "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 env sigma lvar c = + let rec aux vars = function + | PVar id as x -> + (try + let ctx,c = Id.Map.find id lvar in + try + let inst = + List.map + (fun id -> mkRel (List.index Name.equal (Name id) vars)) + ctx + in + let c = substl inst c in + snd (pattern_of_constr env 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 Id.equal ctx vars) + with Not_found (* Map.find failed *) -> + x) + | (PFix _ | PCoFix _) -> error ("Non instantiable pattern.") + | 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 (fun _ -> 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 -> + let ref',t = subst_global subst ref in + if ref' == ref then pat else + snd (pattern_of_constr (Global.env()) Evd.empty t) + | PVar _ + | PEvar _ + | PRel _ -> pat + | PProj (p,c) -> + let p' = Projection.map (fun p -> + destConstRef (fst (subst_global subst (ConstRef p)))) 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 + 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 + | 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 (cip,typ,c,branches) -> + let ind = cip.cip_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 + let subst_branch ((i,n,c) as br) = + let c' = subst_pattern subst c in + if c' == c then br else (i,n,c') + in + let branches' = List.smartmap subst_branch branches in + if cip' == cip && typ' == typ && c' == c && branches' == branches + then pat + else PCase(cip', 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 mkPLambda na b = PLambda(na,PMeta None,b) +let rev_it_mkPLambda = List.fold_right mkPLambda + +let err loc pp = user_err_loc (loc,"pattern_of_glob_constr", pp) + +let rec pat_of_raw metas vars = function + | GVar (_,id) -> + (try PRel (List.index Name.equal (Name id) vars) + with Not_found -> PVar id) + | GPatVar (_,(false,n)) -> + metas := n::!metas; PMeta (Some n) + | GRef (_,gr,_) -> + PRef (canonical_gr gr) + (* Hack to avoid rewriting a complete interpretation of patterns *) + | GApp (_, GPatVar (_,(true,n)), cl) -> + metas := n::!metas; PSoApp (n, List.map (pat_of_raw metas vars) cl) + | GApp (_,c,cl) -> + PApp (pat_of_raw metas vars c, + Array.of_list (List.map (pat_of_raw metas vars) cl)) + | GLambda (_,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) + | GProd (_,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) + | GLetIn (_,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) + | GSort (_,s) -> + PSort s + | GHole _ -> + PMeta None + | GCast (_,c,_) -> + Pp.msg_warning (strbrk "Cast not taken into account in constr pattern"); + pat_of_raw metas vars c + | GIf (_,c,(_,None),b1,b2) -> + PIf (pat_of_raw metas vars c, + pat_of_raw metas vars b1,pat_of_raw metas vars b2) + | GLetTuple (loc,nal,(_,None),b,c) -> + let mkGLambda c na = + GLambda (loc,na,Explicit,GHole (loc,Evar_kinds.InternalHole, IntroAnonymous, None),c) in + let c = List.fold_left mkGLambda c nal in + let cip = + { cip_style = LetStyle; + cip_ind = None; + cip_ind_tags = None; + cip_extensible = false } + in + let tags = List.map (fun _ -> false) nal (* Approximation which can be without let-ins... *) in + PCase (cip, PMeta None, pat_of_raw metas vars b, + [0,tags,pat_of_raw metas vars c]) + | GCases (loc,sty,p,[c,(na,indnames)],brs) -> + let get_ind = function + | (_,_,[PatCstr(_,(ind,_),_,_)],_)::_ -> Some ind + | _ -> None + in + let ind_tags,ind = match indnames with + | Some (_,ind,nal) -> Some (List.length nal), Some ind + | None -> None, get_ind brs + in + let ext,brs = pats_of_glob_branches loc metas vars ind brs + in + let pred = match p,indnames with + | Some p, Some (_,_,nal) -> + let nvars = na :: List.rev nal @ vars in + rev_it_mkPLambda nal (mkPLambda na (pat_of_raw metas nvars p)) + | _ -> PMeta None + in + let info = + { cip_style = sty; + cip_ind = ind; + cip_ind_tags = None; + cip_extensible = ext } + in + (* Nota : when we have a non-trivial predicate, + the inductive type is known. Same when we have at least + one non-trivial branch. These facts are used in [Constrextern]. *) + PCase (info, pred, pat_of_raw metas vars c, brs) + + | r -> err (loc_of_glob_constr r) (Pp.str "Non supported pattern.") + +and pats_of_glob_branches loc metas vars ind brs = + let get_arg = function + | PatVar(_,na) -> na + | PatCstr(loc,_,_,_) -> err loc (Pp.str "Non supported pattern.") + in + let rec get_pat indexes = function + | [] -> false, [] + | [(_,_,[PatVar(_,Anonymous)],GHole _)] -> true, [] (* ends with _ => _ *) + | (_,_,[PatCstr(_,(indsp,j),lv,_)],br) :: brs -> + let () = match ind with + | Some sp when eq_ind sp indsp -> () + | _ -> + err loc (Pp.str "All constructors must be in the same inductive type.") + in + if Int.Set.mem (j-1) indexes then + err loc + (str "No unique branch for " ++ int j ++ str"-th constructor."); + let lna = List.map get_arg lv in + let vars' = List.rev lna @ vars in + let pat = rev_it_mkPLambda lna (pat_of_raw metas vars' br) in + let ext,pats = get_pat (Int.Set.add (j-1) indexes) brs in + let tags = List.map (fun _ -> false) lv (* approximation, w/o let-in *) in + ext, ((j-1, tags, pat) :: pats) + | (loc,_,_,_) :: _ -> err loc (Pp.str "Non supported pattern.") + in + get_pat Int.Set.empty brs + +let pattern_of_glob_constr c = + let metas = ref [] in + let p = pat_of_raw metas [] c in + (!metas,p) -- cgit v1.2.3