From 8a71afd27620a5d6c507b115d6fd408d879544c5 Mon Sep 17 00:00:00 2001 From: letouzey Date: Tue, 29 May 2012 11:08:53 +0000 Subject: Pattern as a mli-only file, operations in Patternops git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15376 85f007b7-540e-0410-9357-904b9bb8a0f7 --- dev/printers.mllib | 2 +- interp/constrintern.ml | 1 + intf/pattern.mli | 80 ++++++++++ parsing/grammar.mllib | 1 - parsing/q_constr.ml4 | 2 +- plugins/quote/quote.ml | 1 + pretyping/matching.ml | 1 + pretyping/pattern.ml | 381 ---------------------------------------------- pretyping/pattern.mli | 127 ---------------- pretyping/patternops.ml | 348 ++++++++++++++++++++++++++++++++++++++++++ pretyping/patternops.mli | 57 +++++++ pretyping/pretyping.mllib | 2 +- pretyping/tacred.ml | 1 + proofs/redexpr.ml | 2 +- tactics/auto.ml | 7 +- tactics/class_tactics.ml4 | 1 + tactics/eauto.ml4 | 1 + tactics/rewrite.ml4 | 1 + tactics/tacinterp.ml | 1 + tactics/termdn.ml | 1 + 20 files changed, 502 insertions(+), 516 deletions(-) create mode 100644 intf/pattern.mli delete mode 100644 pretyping/pattern.ml delete mode 100644 pretyping/pattern.mli create mode 100644 pretyping/patternops.ml create mode 100644 pretyping/patternops.mli diff --git a/dev/printers.mllib b/dev/printers.mllib index c3b5742ac..a5e0d27be 100644 --- a/dev/printers.mllib +++ b/dev/printers.mllib @@ -86,7 +86,7 @@ Recordops Evarconv Arguments_renaming Typing -Pattern +Patternops Matching Tacred Classops diff --git a/interp/constrintern.ml b/interp/constrintern.ml index 91e0cf6a1..5a1dea89e 100644 --- a/interp/constrintern.ml +++ b/interp/constrintern.ml @@ -18,6 +18,7 @@ open Impargs open Glob_term open Glob_ops open Pattern +open Patternops open Pretyping open Cases open Constrexpr diff --git a/intf/pattern.mli b/intf/pattern.mli new file mode 100644 index 000000000..63d4ffa7a --- /dev/null +++ b/intf/pattern.mli @@ -0,0 +1,80 @@ +(************************************************************************) +(* v * The Coq Proof Assistant / The Coq Development Team *) +(* ?p,fun y x => ?p)] => [forall x y => p]] + + will be accepted. Thanks to the reference by index, a matching + problem like + + [match ... with [(fun x => ?p)] => [forall x => p]] + + will work even if [x] is also the name of an existing goal + variable. + + Note: we do not keep types in the signature. Besides simplicity, + the main reason is that it would force to close the signature over + binders that occur only in the types of effective binders but not + in the term itself (e.g. for a term [f x] with [f:A -> True] and + [x:A]). + + On the opposite side, by not keeping the types, we loose + opportunity to propagate type informations which otherwise would + not be inferable, as e.g. when matching [forall x, x = 0] with + pattern [forall x, ?h = 0] and using the solution "x|-h:=x" in + expression [forall x, h = x] where nothing tells how the type of x + could be inferred. We also loose the ability of typing ltac + variables before calling the right-hand-side of ltac matching clauses. *) + +type constr_under_binders = identifier list * constr + +(** Types of substitutions with or w/o bound variables *) + +type patvar_map = (patvar * constr) list +type extended_patvar_map = (patvar * constr_under_binders) list + +(** {5 Patterns} *) + +type case_info_pattern = + { cip_style : case_style; + cip_ind : inductive option; + cip_ind_args : 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 + | PEvar of existential_key * constr_pattern array + | PRel of int + | PApp of constr_pattern * constr_pattern array + | PSoApp of patvar * constr_pattern list + | PLambda of name * constr_pattern * constr_pattern + | PProd of name * constr_pattern * constr_pattern + | PLetIn of name * constr_pattern * constr_pattern + | PSort of glob_sort + | PMeta of patvar option + | PIf of constr_pattern * constr_pattern * constr_pattern + | PCase of case_info_pattern * constr_pattern * constr_pattern * + (int * int * constr_pattern) list (** index of constructor, nb of args *) + | PFix of fixpoint + | PCoFix of cofixpoint + +(** Nota : in a [PCase], the array of branches might be shorter than + expected, denoting the use of a final "_ => _" branch *) diff --git a/parsing/grammar.mllib b/parsing/grammar.mllib index c2dce0231..7ab65b443 100644 --- a/parsing/grammar.mllib +++ b/parsing/grammar.mllib @@ -65,7 +65,6 @@ Inductiveops Miscops Glob_ops Detyping -Pattern Topconstr Genarg Ppextend diff --git a/parsing/q_constr.ml4 b/parsing/q_constr.ml4 index 543240a82..d78b6c8c0 100644 --- a/parsing/q_constr.ml4 +++ b/parsing/q_constr.ml4 @@ -31,7 +31,7 @@ EXTEND GLOBAL: expr; expr: [ [ "PATTERN"; "["; c = constr; "]" -> - <:expr< snd (Pattern.pattern_of_glob_constr $c$) >> ] ] + <:expr< snd (Patternops.pattern_of_glob_constr $c$) >> ] ] ; sort: [ [ "Set" -> GSet diff --git a/plugins/quote/quote.ml b/plugins/quote/quote.ml index fe025e6da..e8ee433c6 100644 --- a/plugins/quote/quote.ml +++ b/plugins/quote/quote.ml @@ -107,6 +107,7 @@ open Util open Names open Term open Pattern +open Patternops open Matching open Tacmach open Tactics diff --git a/pretyping/matching.ml b/pretyping/matching.ml index 6be95cd82..554face37 100644 --- a/pretyping/matching.ml +++ b/pretyping/matching.ml @@ -20,6 +20,7 @@ open Glob_term open Sign open Environ open Pattern +open Patternops open Misctypes (*i*) diff --git a/pretyping/pattern.ml b/pretyping/pattern.ml deleted file mode 100644 index 08e5ac75c..000000000 --- a/pretyping/pattern.ml +++ /dev/null @@ -1,381 +0,0 @@ -(************************************************************************) -(* v * The Coq Proof Assistant / The Coq Development Team *) -(* _ ? *) } - -type constr_pattern = - | PRef of global_reference - | PVar of identifier - | PEvar of existential_key * constr_pattern array - | PRel of int - | PApp of constr_pattern * constr_pattern array - | PSoApp of patvar * constr_pattern list - | PLambda of name * constr_pattern * constr_pattern - | PProd of name * constr_pattern * constr_pattern - | PLetIn of name * constr_pattern * constr_pattern - | PSort of glob_sort - | PMeta of patvar option - | PIf of constr_pattern * constr_pattern * constr_pattern - | 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 - -let rec occur_meta_pattern = function - | PApp (f,args) -> - (occur_meta_pattern f) or (array_exists occur_meta_pattern args) - | PLambda (na,t,c) -> (occur_meta_pattern t) or (occur_meta_pattern c) - | PProd (na,t,c) -> (occur_meta_pattern t) or (occur_meta_pattern c) - | PLetIn (na,t,c) -> (occur_meta_pattern t) or (occur_meta_pattern c) - | PIf (c,c1,c2) -> - (occur_meta_pattern c) or - (occur_meta_pattern c1) or (occur_meta_pattern c2) - | PCase(_,p,c,br) -> - (occur_meta_pattern p) or - (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 - -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 - | PEvar _ | PRel _ | PMeta _ | PSoApp _ | PSort _ | PFix _ - -> raise BoundPattern - (* Perhaps they were arguments, but we don't beta-reduce *) - | PLambda _ -> raise BoundPattern - | PCoFix _ -> anomaly "head_pattern_bound: 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 "Not a rigid reference" - -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))) - | Var id -> PVar id - | Sort (Prop Null) -> PSort GProp - | Sort (Prop Pos) -> PSort GSet - | 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) - | Lambda (na,c,b) -> PLambda (na,pattern_of_constr c,pattern_of_constr 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,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 - | Evar_kinds.MatchingVar (b,id) -> - ctx := (id,None,existential_type sigma ev)::!ctx; - assert (not b); PMeta (Some id) - | Evar_kinds.GoalEvar -> PEvar (evk,Array.map pattern_of_constr 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_args = Some (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 - (* 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) - (* Non recursive *) - | (PVar _ | PEvar _ | PRel _ | PRef _ | PSort _ | PMeta _ - (* Bound to terms *) - | PFix _ | PCoFix _ as x) -> 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_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 Evd.empty 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 - | 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 (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 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 id) vars) - with Not_found -> PVar id) - | GPatVar (_,(false,n)) -> - metas := n::!metas; PMeta (Some n) - | 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) - | 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,_) -> - Flags.if_warn - Pp.msg_warning (str "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),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,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) -> - 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 - (* 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 -> - 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_glob_constr c = - let metas = ref [] in - let p = pat_of_raw metas [] c in - (!metas,p) diff --git a/pretyping/pattern.mli b/pretyping/pattern.mli deleted file mode 100644 index f9c2358b7..000000000 --- a/pretyping/pattern.mli +++ /dev/null @@ -1,127 +0,0 @@ -(************************************************************************) -(* v * The Coq Proof Assistant / The Coq Development Team *) -(* ?p,fun y x => ?p)] => [forall x y => p]] - - will be accepted. Thanks to the reference by index, a matching - problem like - - [match ... with [(fun x => ?p)] => [forall x => p]] - - will work even if [x] is also the name of an existing goal - variable. - - Note: we do not keep types in the signature. Besides simplicity, - the main reason is that it would force to close the signature over - binders that occur only in the types of effective binders but not - in the term itself (e.g. for a term [f x] with [f:A -> True] and - [x:A]). - - On the opposite side, by not keeping the types, we loose - opportunity to propagate type informations which otherwise would - not be inferable, as e.g. when matching [forall x, x = 0] with - pattern [forall x, ?h = 0] and using the solution "x|-h:=x" in - expression [forall x, h = x] where nothing tells how the type of x - could be inferred. We also loose the ability of typing ltac - variables before calling the right-hand-side of ltac matching clauses. *) - -type constr_under_binders = identifier list * constr - -(** Types of substitutions with or w/o bound variables *) - -type patvar_map = (patvar * constr) list -type extended_patvar_map = (patvar * constr_under_binders) list - -(** {5 Patterns} *) - -type case_info_pattern = - { cip_style : case_style; - cip_ind : inductive option; - cip_ind_args : 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 - | PEvar of existential_key * constr_pattern array - | PRel of int - | PApp of constr_pattern * constr_pattern array - | PSoApp of patvar * constr_pattern list - | PLambda of name * constr_pattern * constr_pattern - | PProd of name * constr_pattern * constr_pattern - | PLetIn of name * constr_pattern * constr_pattern - | PSort of glob_sort - | PMeta of patvar option - | PIf of constr_pattern * constr_pattern * constr_pattern - | PCase of case_info_pattern * constr_pattern * constr_pattern * - (int * int * constr_pattern) list (** index of constructor, nb of args *) - | PFix of fixpoint - | PCoFix of cofixpoint - -(** Nota : in a [PCase], the array of branches might be shorter than - expected, denoting the use of a final "_ => _" branch *) - -(** {5 Functions on patterns} *) - -val occur_meta_pattern : constr_pattern -> bool - -val subst_pattern : substitution -> constr_pattern -> constr_pattern - -exception BoundPattern - -(** [head_pattern_bound t] extracts the head variable/constant of the - type [t] or raises [BoundPattern] (even if a sort); it raises an anomaly - if [t] is an abstraction *) - -val head_pattern_bound : constr_pattern -> global_reference - -(** [head_of_constr_reference c] assumes [r] denotes a reference and - returns its label; raises an anomaly otherwise *) - -val head_of_constr_reference : Term.constr -> global_reference - -(** [pattern_of_constr c] translates a term [c] with metavariables into - a pattern; currently, no destructor (Cases, Fix, Cofix) and no - existential variable are allowed in [c] *) - -val pattern_of_constr : Evd.evar_map -> constr -> named_context * constr_pattern - -(** [pattern_of_glob_constr l c] translates a term [c] with metavariables into - a pattern; variables bound in [l] are replaced by the pattern to which they - are bound *) - -val pattern_of_glob_constr : glob_constr -> - patvar list * constr_pattern - -val instantiate_pattern : - Evd.evar_map -> (identifier * (identifier list * constr)) list -> - constr_pattern -> constr_pattern - -val lift_pattern : int -> constr_pattern -> constr_pattern diff --git a/pretyping/patternops.ml b/pretyping/patternops.ml new file mode 100644 index 000000000..244d03021 --- /dev/null +++ b/pretyping/patternops.ml @@ -0,0 +1,348 @@ +(************************************************************************) +(* v * The Coq Proof Assistant / The Coq Development Team *) +(* + (occur_meta_pattern f) or (array_exists occur_meta_pattern args) + | PLambda (na,t,c) -> (occur_meta_pattern t) or (occur_meta_pattern c) + | PProd (na,t,c) -> (occur_meta_pattern t) or (occur_meta_pattern c) + | PLetIn (na,t,c) -> (occur_meta_pattern t) or (occur_meta_pattern c) + | PIf (c,c1,c2) -> + (occur_meta_pattern c) or + (occur_meta_pattern c1) or (occur_meta_pattern c2) + | PCase(_,p,c,br) -> + (occur_meta_pattern p) or + (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 + +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 + | PEvar _ | PRel _ | PMeta _ | PSoApp _ | PSort _ | PFix _ + -> raise BoundPattern + (* Perhaps they were arguments, but we don't beta-reduce *) + | PLambda _ -> raise BoundPattern + | PCoFix _ -> anomaly "head_pattern_bound: 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 "Not a rigid reference" + +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))) + | Var id -> PVar id + | Sort (Prop Null) -> PSort GProp + | Sort (Prop Pos) -> PSort GSet + | 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) + | Lambda (na,c,b) -> PLambda (na,pattern_of_constr c,pattern_of_constr 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,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 + | Evar_kinds.MatchingVar (b,id) -> + ctx := (id,None,existential_type sigma ev)::!ctx; + assert (not b); PMeta (Some id) + | Evar_kinds.GoalEvar -> PEvar (evk,Array.map pattern_of_constr 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_args = Some (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 + (* 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) + (* Non recursive *) + | (PVar _ | PEvar _ | PRel _ | PRef _ | PSort _ | PMeta _ + (* Bound to terms *) + | PFix _ | PCoFix _ as x) -> 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_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 Evd.empty 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 + | 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 (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 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 id) vars) + with Not_found -> PVar id) + | GPatVar (_,(false,n)) -> + metas := n::!metas; PMeta (Some n) + | 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) + | 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,_) -> + Flags.if_warn + Pp.msg_warning (str "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),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,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) -> + 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 + (* 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 -> + 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_glob_constr c = + let metas = ref [] in + let p = pat_of_raw metas [] c in + (!metas,p) diff --git a/pretyping/patternops.mli b/pretyping/patternops.mli new file mode 100644 index 000000000..74e5a81ae --- /dev/null +++ b/pretyping/patternops.mli @@ -0,0 +1,57 @@ +(************************************************************************) +(* v * The Coq Proof Assistant / The Coq Development Team *) +(* bool + +val subst_pattern : substitution -> constr_pattern -> constr_pattern + +exception BoundPattern + +(** [head_pattern_bound t] extracts the head variable/constant of the + type [t] or raises [BoundPattern] (even if a sort); it raises an anomaly + if [t] is an abstraction *) + +val head_pattern_bound : constr_pattern -> global_reference + +(** [head_of_constr_reference c] assumes [r] denotes a reference and + returns its label; raises an anomaly otherwise *) + +val head_of_constr_reference : Term.constr -> global_reference + +(** [pattern_of_constr c] translates a term [c] with metavariables into + a pattern; currently, no destructor (Cases, Fix, Cofix) and no + existential variable are allowed in [c] *) + +val pattern_of_constr : Evd.evar_map -> constr -> named_context * constr_pattern + +(** [pattern_of_glob_constr l c] translates a term [c] with metavariables into + a pattern; variables bound in [l] are replaced by the pattern to which they + are bound *) + +val pattern_of_glob_constr : glob_constr -> + patvar list * constr_pattern + +val instantiate_pattern : + Evd.evar_map -> (identifier * (identifier list * constr)) list -> + constr_pattern -> constr_pattern + +val lift_pattern : int -> constr_pattern -> constr_pattern diff --git a/pretyping/pretyping.mllib b/pretyping/pretyping.mllib index fca2d714f..2d25b1413 100644 --- a/pretyping/pretyping.mllib +++ b/pretyping/pretyping.mllib @@ -17,7 +17,7 @@ Typing Miscops Glob_ops Redops -Pattern +Patternops Matching Tacred Typeclasses_errors diff --git a/pretyping/tacred.ml b/pretyping/tacred.ml index 6ff469012..05136d25d 100644 --- a/pretyping/tacred.ml +++ b/pretyping/tacred.ml @@ -24,6 +24,7 @@ open Reductionops open Cbv open Glob_term open Pattern +open Patternops open Matching open Locus diff --git a/proofs/redexpr.ml b/proofs/redexpr.ml index 12aec9142..d0782e970 100644 --- a/proofs/redexpr.ml +++ b/proofs/redexpr.ml @@ -223,7 +223,7 @@ let subst_red_expr subs e = subst_gen_red_expr (Mod_subst.subst_mps subs) (Mod_subst.subst_evaluable_reference subs) - (Pattern.subst_pattern subs) + (Patternops.subst_pattern subs) e let inReduction : bool * string * red_expr -> obj = diff --git a/tactics/auto.ml b/tactics/auto.ml index f580f839c..158221d79 100644 --- a/tactics/auto.ml +++ b/tactics/auto.ml @@ -22,6 +22,7 @@ open Evd open Reduction open Typing open Pattern +open Patternops open Matching open Tacmach open Proof_type @@ -485,7 +486,7 @@ let make_exact_entry sigma pri ?(name=PathAny) (c,cty) = match kind_of_term cty with | Prod _ -> failwith "make_exact_entry" | _ -> - let pat = snd (Pattern.pattern_of_constr sigma cty) in + let pat = snd (Patternops.pattern_of_constr sigma cty) in let hd = try head_pattern_bound pat with BoundPattern -> failwith "make_exact_entry" @@ -502,7 +503,7 @@ let make_apply_entry env sigma (eapply,hnf,verbose) pri ?(name=PathAny) (c,cty) | Prod _ -> let ce = mk_clenv_from dummy_goal (c,cty) in let c' = clenv_type (* ~reduce:false *) ce in - let pat = snd (Pattern.pattern_of_constr sigma c') in + let pat = snd (Patternops.pattern_of_constr sigma c') in let hd = try head_pattern_bound pat with BoundPattern -> failwith "make_apply_entry" in @@ -576,7 +577,7 @@ let make_trivial env sigma ?(name=PathAny) c = let hd = head_of_constr_reference (fst (head_constr t)) in let ce = mk_clenv_from dummy_goal (c,t) in (Some hd, { pri=1; - pat = Some (snd (Pattern.pattern_of_constr sigma (clenv_type ce))); + pat = Some (snd (Patternops.pattern_of_constr sigma (clenv_type ce))); name = name; code=Res_pf_THEN_trivial_fail(c,t) }) diff --git a/tactics/class_tactics.ml4 b/tactics/class_tactics.ml4 index cafe17ad9..bfebf7810 100644 --- a/tactics/class_tactics.ml4 +++ b/tactics/class_tactics.ml4 @@ -24,6 +24,7 @@ open Tacmach open Evar_refiner open Tactics open Pattern +open Patternops open Clenv open Auto open Glob_term diff --git a/tactics/eauto.ml4 b/tactics/eauto.ml4 index e9602762d..fb692873e 100644 --- a/tactics/eauto.ml4 +++ b/tactics/eauto.ml4 @@ -24,6 +24,7 @@ open Tacmach open Evar_refiner open Tactics open Pattern +open Patternops open Clenv open Auto open Genredexpr diff --git a/tactics/rewrite.ml4 b/tactics/rewrite.ml4 index 4a0d143dc..75f6bdb7c 100644 --- a/tactics/rewrite.ml4 +++ b/tactics/rewrite.ml4 @@ -25,6 +25,7 @@ open Tacmach open Evar_refiner open Tactics open Pattern +open Patternops open Clenv open Auto open Glob_term diff --git a/tactics/tacinterp.ml b/tactics/tacinterp.ml index 88767a363..9b4df0ad5 100644 --- a/tactics/tacinterp.ml +++ b/tactics/tacinterp.ml @@ -13,6 +13,7 @@ open Declarations open Entries open Libobject open Pattern +open Patternops open Matching open Pp open Genredexpr diff --git a/tactics/termdn.ml b/tactics/termdn.ml index 5f6e5580e..0e7009113 100644 --- a/tactics/termdn.ml +++ b/tactics/termdn.ml @@ -12,6 +12,7 @@ open Names open Nameops open Term open Pattern +open Patternops open Glob_term open Libnames open Nametab -- cgit v1.2.3