diff options
author | Stephane Glondu <steph@glondu.net> | 2012-01-12 16:02:20 +0100 |
---|---|---|
committer | Stephane Glondu <steph@glondu.net> | 2012-01-12 16:02:20 +0100 |
commit | 97fefe1fcca363a1317e066e7f4b99b9c1e9987b (patch) | |
tree | 97ec6b7d831cc5fb66328b0c63a11db1cbb2f158 /pretyping/pattern.ml | |
parent | 300293c119981054c95182a90c829058530a6b6f (diff) |
Imported Upstream version 8.4~betaupstream/8.4_beta
Diffstat (limited to 'pretyping/pattern.ml')
-rw-r--r-- | pretyping/pattern.ml | 205 |
1 files changed, 115 insertions, 90 deletions
diff --git a/pretyping/pattern.ml b/pretyping/pattern.ml index 83bfe9ea..65f342d8 100644 --- a/pretyping/pattern.ml +++ b/pretyping/pattern.ml @@ -1,19 +1,17 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2011 *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2010 *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(* $Id: pattern.ml 14641 2011-11-06 11:59:10Z herbelin $ *) - open Util open Names open Libnames open Nameops open Term -open Rawterm +open Glob_term open Environ open Nametab open Pp @@ -28,6 +26,12 @@ type extended_patvar_map = (patvar * constr_under_binders) list (* Patterns *) +type case_info_pattern = + { cip_style : case_style; + cip_ind : inductive option; + cip_ind_args : (int * int) option; (** number of params and args *) + cip_extensible : bool (** does this match end with _ => _ ? *) } + type constr_pattern = | PRef of global_reference | PVar of identifier @@ -38,11 +42,11 @@ type constr_pattern = | PLambda of name * constr_pattern * constr_pattern | PProd of name * constr_pattern * constr_pattern | PLetIn of name * constr_pattern * constr_pattern - | PSort of rawsort + | PSort of glob_sort | PMeta of patvar option | PIf of constr_pattern * constr_pattern * constr_pattern - | PCase of (case_style * int array * inductive option * (int * int) option) - * constr_pattern * constr_pattern * constr_pattern array + | PCase of case_info_pattern * constr_pattern * constr_pattern * + (int * int * constr_pattern) list (** constructor index, nb of args *) | PFix of fixpoint | PCoFix of cofixpoint @@ -57,16 +61,11 @@ let rec occur_meta_pattern = function (occur_meta_pattern c1) or (occur_meta_pattern c2) | PCase(_,p,c,br) -> (occur_meta_pattern p) or - (occur_meta_pattern c) or (array_exists occur_meta_pattern br) + (occur_meta_pattern c) or + (List.exists (fun (_,_,p) -> occur_meta_pattern p) br) | PMeta _ | PSoApp _ -> true | PEvar _ | PVar _ | PRef _ | PRel _ | PSort _ | PFix _ | PCoFix _ -> false -type constr_label = - | ConstNode of constant - | IndNode of inductive - | CstrNode of constructor - | VarNode of identifier - exception BoundPattern;; let rec head_pattern_bound t = @@ -100,8 +99,8 @@ let pattern_of_constr sigma t = | Rel n -> PRel n | Meta n -> PMeta (Some (id_of_string ("META" ^ string_of_int n))) | Var id -> PVar id - | Sort (Prop c) -> PSort (RProp c) - | Sort (Type _) -> PSort (RType None) + | Sort (Prop c) -> PSort (GProp c) + | Sort (Type _) -> PSort (GType None) | 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) @@ -130,11 +129,17 @@ let pattern_of_constr sigma t = | 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 - PCase ((cip.style,ci.ci_cstr_nargs,Some ci.ci_ind,no), - pattern_of_constr p,pattern_of_constr a, - Array.map pattern_of_constr br) + let cip = + { cip_style = ci.ci_pp_info.style; + cip_ind = Some ci.ci_ind; + cip_ind_args = Some (ci.ci_npar, ci.ci_pp_info.ind_nargs); + cip_extensible = false } + in + let branch_of_constr i c = + (i, ci.ci_cstr_ndecls.(i), pattern_of_constr c) + in + PCase (cip, pattern_of_constr p, pattern_of_constr a, + Array.to_list (Array.mapi branch_of_constr br)) | Fix f -> PFix f | CoFix f -> PCoFix f in let p = pattern_of_constr t in @@ -151,14 +156,13 @@ let map_pattern_with_binders g f l = function | 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) + | 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) (* Non recursive *) | (PVar _ | PEvar _ | PRel _ | PRef _ | PSort _ | PMeta _ (* Bound to terms *) | PFix _ | PCoFix _ as x) -> x -let map_pattern f = map_pattern_with_binders (fun _ () -> ()) (fun () -> f) () - 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 @@ -235,14 +239,20 @@ let rec subst_pattern subst pat = let c2' = subst_pattern subst c2 in if c' == c && c1' == c1 && c2' == c2 then pat else PIf (c',c1',c2') - | PCase ((a,b,ind,n as cs),typ,c,branches) -> + | PCase (cip,typ,c,branches) -> + let ind = cip.cip_ind in let ind' = Option.smartmap (Inductiveops.subst_inductive 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 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') + 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 @@ -257,94 +267,109 @@ let rec subst_pattern subst pat = 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 - | RVar (_,id) -> + | GVar (_,id) -> (try PRel (list_index (Name id) vars) with Not_found -> PVar id) - | RPatVar (_,(false,n)) -> + | GPatVar (_,(false,n)) -> metas := n::!metas; PMeta (Some n) - | RRef (_,gr) -> + | GRef (_,gr) -> PRef (canonical_gr gr) (* Hack pour ne pas réécrire une interprétation complète des patterns*) - | RApp (_, RPatVar (_,(true,n)), cl) -> + | GApp (_, GPatVar (_,(true,n)), cl) -> metas := n::!metas; PSoApp (n, List.map (pat_of_raw metas vars) cl) - | RApp (_,c,cl) -> + | GApp (_,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) -> + | 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) - | RProd (_,na,bk,c1,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) - | RLetIn (_,na,c1,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) - | RSort (_,s) -> + | GSort (_,s) -> PSort s - | RHole _ -> + | GHole _ -> PMeta None - | RCast (_,c,_) -> - Flags.if_verbose - Pp.warning "Cast not taken into account in constr pattern"; + | GCast (_,c,_) -> + Flags.if_warn + Pp.msg_warning (str "Cast not taken into account in constr pattern"); pat_of_raw metas vars c - | RIf (_,c,(_,None),b1,b2) -> + | GIf (_,c,(_,None),b1,b2) -> PIf (pat_of_raw metas vars c, pat_of_raw metas vars b1,pat_of_raw metas vars b2) - | RLetTuple (loc,nal,(_,None),b,c) -> - let mkRLambda c na = RLambda (loc,na,Explicit,RHole (loc,Evd.InternalHole),c) in - let c = List.fold_left mkRLambda c nal in - PCase ((LetStyle,[|1|],None,None),PMeta None,pat_of_raw metas vars b, - [|pat_of_raw metas vars c|]) - | RCases (loc,sty,p,[c,(na,indnames)],brs) -> - let pred,ind_nargs, ind = match p,indnames with - | Some p, Some (_,ind,n,nal) -> - rev_it_mkPLambda nal (mkPLambda na (pat_of_raw metas vars p)), - Some (n,List.length nal),Some ind - | _ -> PMeta None, None, None in - let ind = match ind with Some _ -> ind | None -> - match brs with - | (_,_,[PatCstr(_,(ind,_),_,_)],_)::_ -> Some ind - | _ -> None in - let cbrs = - Array.init (List.length brs) (pat_of_raw_branch loc metas vars ind brs) + | GLetTuple (loc,nal,(_,None),b,c) -> + let mkGLambda c na = GLambda (loc,na,Explicit,GHole (loc,Evd.InternalHole),c) in + let c = List.fold_left mkGLambda c nal in + let cip = + { cip_style = LetStyle; + cip_ind = None; + cip_ind_args = None; + cip_extensible = false } + in + PCase (cip, PMeta None, pat_of_raw metas vars b, + [0,1,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_nargs,ind = match indnames with + | Some (_,ind,n,nal) -> Some (n,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) -> + rev_it_mkPLambda nal (mkPLambda na (pat_of_raw metas vars p)) + | _ -> PMeta None + in + let info = + { cip_style = sty; + cip_ind = ind; + cip_ind_args = ind_nargs; + cip_extensible = ext } in - 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) + (* 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 -> - let loc = loc_of_rawconstr r in - user_err_loc (loc,"pattern_of_rawconstr", Pp.str"Non supported pattern.") + | r -> err (loc_of_glob_constr r) (Pp.str "Non supported pattern.") -and pat_of_raw_branch loc metas vars ind brs i = - let bri = List.filter - (function - (_,_,[PatCstr(_,c,lv,Anonymous)],_) -> snd c = i+1 - | (loc,_,_,_) -> - user_err_loc (loc,"pattern_of_rawconstr", - Pp.str "Non supported pattern.")) brs in - match bri with - | [(_,_,[PatCstr(_,(indsp,_),lv,_)],br)] -> - if ind <> None & ind <> Some indsp then - user_err_loc (loc,"pattern_of_rawconstr", - Pp.str "All constructors must be in the same inductive type."); - let lna = - List.map - (function PatVar(_,na) -> na - | PatCstr(loc,_,_,_) -> - user_err_loc (loc,"pattern_of_rawconstr", - Pp.str "Non supported pattern.")) lv 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) ++ - str"-th constructor.") +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 -> + if ind <> None && ind <> Some indsp then + err loc (Pp.str "All constructors must be in the same inductive type."); + if Intset.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 (Intset.add (j-1) indexes) brs in + ext, ((j-1, List.length lv, pat) :: pats) + | (loc,_,_,_) :: _ -> err loc (Pp.str "Non supported pattern.") + in + get_pat Intset.empty brs -let pattern_of_rawconstr c = +let pattern_of_glob_constr c = let metas = ref [] in let p = pat_of_raw metas [] c in (!metas,p) |