diff options
| -rw-r--r-- | CHANGES | 5 | ||||
| -rw-r--r-- | contrib/funind/indfun.ml | 2 | ||||
| -rw-r--r-- | contrib/subtac/subtac_command.ml | 4 | ||||
| -rw-r--r-- | contrib/subtac/subtac_command.mli | 2 | ||||
| -rw-r--r-- | doc/refman/RefMan-ltac.tex | 68 | ||||
| -rw-r--r-- | interp/constrintern.ml | 16 | ||||
| -rw-r--r-- | interp/constrintern.mli | 4 | ||||
| -rw-r--r-- | parsing/g_constr.ml4 | 5 | ||||
| -rw-r--r-- | pretyping/pattern.ml | 2 | ||||
| -rw-r--r-- | tactics/tacinterp.ml | 2 | ||||
| -rw-r--r-- | test-suite/success/ltac.v | 13 |
11 files changed, 83 insertions, 40 deletions
@@ -4,6 +4,11 @@ Changes from V8.1gamma to ... - Added option Global to "Implicit Arguments" and "Arguments Scope" for section surviving. +Tactic Language + +- Second-order pattern-matching now working in Ltac "match" clauses + (syntax for second-order unification variable is "@?X"). + Tactics - New tactic ring, ring_simplify and new tactic field now able to manage diff --git a/contrib/funind/indfun.ml b/contrib/funind/indfun.ml index 82bb28695..a131c95a5 100644 --- a/contrib/funind/indfun.ml +++ b/contrib/funind/indfun.ml @@ -146,7 +146,7 @@ let rec abstract_rawconstr c = function let interp_casted_constr_with_implicits sigma env impls c = (* Constrintern.interp_rawconstr_with_implicits sigma env [] impls c *) Constrintern.intern_gen false sigma env ~impls:([],impls) - ~allow_soapp:false ~ltacvars:([],[]) c + ~allow_patvar:false ~ltacvars:([],[]) c (* diff --git a/contrib/subtac/subtac_command.ml b/contrib/subtac/subtac_command.ml index e624b5f32..cab8829db 100644 --- a/contrib/subtac/subtac_command.ml +++ b/contrib/subtac/subtac_command.ml @@ -53,9 +53,9 @@ let evar_nf isevars c = Evarutil.nf_isevar !isevars c let interp_gen kind isevars env - ?(impls=([],[])) ?(allow_soapp=false) ?(ltacvars=([],[])) + ?(impls=([],[])) ?(allow_patvar=false) ?(ltacvars=([],[])) c = - let c' = Constrintern.intern_gen (kind=IsType) ~impls ~allow_soapp ~ltacvars (Evd.evars_of !isevars) env c in + let c' = Constrintern.intern_gen (kind=IsType) ~impls ~allow_patvar ~ltacvars (Evd.evars_of !isevars) env c in let c' = Subtac_utils.rewrite_cases env c' in (* (try trace (str "Pretyping " ++ my_print_constr_expr c) with _ -> ()); *) let c' = SPretyping.pretype_gen isevars env ([],[]) kind c' in diff --git a/contrib/subtac/subtac_command.mli b/contrib/subtac/subtac_command.mli index 846e06cfb..6de45d17f 100644 --- a/contrib/subtac/subtac_command.mli +++ b/contrib/subtac/subtac_command.mli @@ -14,7 +14,7 @@ val interp_gen : evar_defs ref -> env -> ?impls:full_implicits_env -> - ?allow_soapp:bool -> + ?allow_patvar:bool -> ?ltacvars:ltac_sign -> constr_expr -> constr val interp_constr : diff --git a/doc/refman/RefMan-ltac.tex b/doc/refman/RefMan-ltac.tex index ad2ffdc63..79a33712d 100644 --- a/doc/refman/RefMan-ltac.tex +++ b/doc/refman/RefMan-ltac.tex @@ -29,18 +29,28 @@ problems. The syntax of the tactic language is given Figures~\ref{ltac} and~\ref{ltac_aux}. See page~\pageref{BNF-syntax} for a description of -the BNF metasyntax used in these grammar rules. Various already defined -entries will be used in this chapter: entries {\naturalnumber}, -{\integer}, {\ident}, {\qualid}, {\term}, {\cpattern} and {\atomictac} -represent respectively the natural and integer numbers, the authorized -identificators and qualified names, {\Coq}'s terms and patterns and -all the atomic tactics described in chapter~\ref{Tactics}. The syntax -of {\cpattern} is the same as that of terms, but there can be specific -variables like {\tt ?id} where {\tt id} is a {\ident} or {\tt \_}, -which are metavariables for pattern matching. {\tt ?id} allows us to +the BNF metasyntax used in these grammar rules. Various already +defined entries will be used in this chapter: entries +{\naturalnumber}, {\integer}, {\ident}, {\qualid}, {\term}, +{\cpattern} and {\atomictac} represent respectively the natural and +integer numbers, the authorized identificators and qualified names, +{\Coq}'s terms and patterns and all the atomic tactics described in +chapter~\ref{Tactics}. The syntax of {\cpattern} is the same as that +of terms, but it is extended with pattern matching metavariables. In +{\cpattern}, a pattern-matching metavariable is represented with the +syntax {\tt ?id} where {\tt id} is a {\ident}. The notation {\tt \_} +can also be used to denote metavariable whose instance is +irrelevant. In the notation {\tt ?id}, the identifier allows us to keep instantiations and to make constraints whereas {\tt \_} shows that we are not interested in what will be matched. On the right hand -side, they are used without the question mark. +side of pattern-matching clauses, the named metavariable are used +without the question mark prefix. There is also a special notation for +second-order pattern-matching problems: in an applicative pattern of +the form {\tt @?id id$_1$ \ldots id$_n$}, the variable {\tt id} +matches any complex expression with (possible) dependencies in the +variables {\tt id$_1$ \ldots id$_n$} and returns a functional term of +the form {\tt fun id$_1$ \ldots id$_n$ => {\term}}. + The main entry of the grammar is {\tacexpr}. This language is used in proof mode but it can also be used in toplevel definitions as shown in @@ -483,19 +493,33 @@ We can carry out pattern matching on terms with: ~{\tt |} {\tt \_} {\tt =>} {\tacexpr}$_{n+1}$\\ {\tt end} \end{quote} -The {\tacexpr} is evaluated and should yield a term which is matched -(non-linear first order unification) against {\cpattern}$_1$ then -{\tacexpr}$_1$ is evaluated into some value by substituting the -pattern matching instantiations to the metavariables. If the matching -with {\cpattern}$_1$ fails, {\cpattern}$_2$ is used and so on. The +The expression {\tacexpr} is evaluated and should yield a term which +is matched against {\cpattern}$_1$. The matching is non-linear: if a +metavariable occurs more than once, it should match the same +expression every time. It is first-order except on the +variables of the form {\tt @?id} that occur in head position of an +application. For these variables, the matching is second-order and +returns a functional term. + +If the matching with {\cpattern}$_1$ succeeds, then {\tacexpr}$_1$ is +evaluated into some value by substituting the pattern matching +instantiations to the metavariables. If {\tacexpr}$_1$ evaluates to a +tactic and the {\tt match} expression is in position to be applied to +a goal (e.g. it is not bound to a variable by a {\tt let in}), then +this tactic is applied. If the tactic succeeds, the list of resulting +subgoals is the result of the {\tt match} expression. If +{\tacexpr}$_1$ does not evaluate to a tactic or if the {\tt match} +expression is not in position to be applied to a goal, then the result +of the evaluation of {\tacexpr}$_1$ is the result of the {\tt match} +expression. + +If the matching with {\cpattern}$_1$ fails, or if it succeeds but the +evaluation of {\tacexpr}$_1$ fails, or if the evaluation of +{\tacexpr}$_1$ succeeds but returns a tactic in execution position +whose execution fails, then {\cpattern}$_2$ is used and so on. The pattern {\_} matches any term and shunts all remaining patterns if -any. If {\tacexpr}$_1$ evaluates to a tactic and the {\tt match} -expression is in position to be applied to a goal (e.g. it is not -bound to a variable by a {\tt let in}, then this tactic is applied. If -the tactic succeeds, the list of resulting subgoals is the result of -the {\tt match} expression. On the opposite, if it fails, the next -pattern is tried. If all clauses fail (in particular, there is no -pattern {\_}) then a no-matching error is raised. +any. If all clauses fail (in particular, there is no pattern {\_}) +then a no-matching-clause error is raised. \begin{ErrMsgs} diff --git a/interp/constrintern.ml b/interp/constrintern.ml index 0a42d2ba9..244f8228a 100644 --- a/interp/constrintern.ml +++ b/interp/constrintern.ml @@ -776,7 +776,7 @@ let reset_tmp_scope (ids,tmp_scope,scopes) = (**********************************************************************) (* Main loop *) -let internalise sigma globalenv env allow_soapp lvar c = +let internalise sigma globalenv env allow_patvar lvar c = let rec intern (ids,tmp_scope,scopes as env) = function | CRef ref as x -> let (c,imp,subscopes,l) = intern_reference env lvar ref in @@ -916,10 +916,8 @@ let internalise sigma globalenv env allow_soapp lvar c = RIf (loc, c', (na', p'), intern env b1, intern env b2) | CHole loc -> RHole (loc, Evd.QuestionMark) - | CPatVar (loc, n) when allow_soapp -> + | CPatVar (loc, n) when allow_patvar -> RPatVar (loc, n) - | CPatVar (loc, (false,n)) -> - error_unbound_patvar loc n | CPatVar (loc, _) -> raise (InternalisationError (loc,NegativeMetavariable)) | CEvar (loc, n) -> @@ -1078,12 +1076,12 @@ let extract_ids env = Idset.empty let intern_gen isarity sigma env - ?(impls=([],[])) ?(allow_soapp=false) ?(ltacvars=([],[])) + ?(impls=([],[])) ?(allow_patvar=false) ?(ltacvars=([],[])) c = let tmp_scope = if isarity then Some Notation.type_scope else None in internalise sigma env (extract_ids env, tmp_scope,[]) - allow_soapp (ltacvars,Environ.named_context env, [], impls) c + allow_patvar (ltacvars,Environ.named_context env, [], impls) c let intern_constr sigma env c = intern_gen false sigma env c @@ -1102,10 +1100,10 @@ let intern_ltac isarity ltacvars sigma env c = (* Functions to parse and interpret constructions *) let interp_gen kind sigma env - ?(impls=([],[])) ?(allow_soapp=false) ?(ltacvars=([],[])) + ?(impls=([],[])) ?(allow_patvar=false) ?(ltacvars=([],[])) c = Default.understand_gen kind sigma env - (intern_gen (kind=IsType) ~impls ~allow_soapp ~ltacvars sigma env c) + (intern_gen (kind=IsType) ~impls ~allow_patvar ~ltacvars sigma env c) let interp_constr sigma env c = interp_gen (OfType None) sigma env c @@ -1140,7 +1138,7 @@ let interp_constr_judgment_evars isevars env c = type ltac_sign = identifier list * unbound_ltac_var_map let interp_constrpattern sigma env c = - pattern_of_rawconstr (intern_gen false sigma env ~allow_soapp:true c) + pattern_of_rawconstr (intern_gen false sigma env ~allow_patvar:true c) let interp_aconstr impls vars a = let env = Global.env () in diff --git a/interp/constrintern.mli b/interp/constrintern.mli index 12aaeec17..1af6854d3 100644 --- a/interp/constrintern.mli +++ b/interp/constrintern.mli @@ -52,7 +52,7 @@ type ltac_sign = identifier list * unbound_ltac_var_map val intern_constr : evar_map -> env -> constr_expr -> rawconstr val intern_gen : bool -> evar_map -> env -> - ?impls:full_implicits_env -> ?allow_soapp:bool -> ?ltacvars:ltac_sign -> + ?impls:full_implicits_env -> ?allow_patvar:bool -> ?ltacvars:ltac_sign -> constr_expr -> rawconstr val intern_pattern : env -> cases_pattern_expr -> @@ -68,7 +68,7 @@ val intern_pattern : env -> cases_pattern_expr -> (* Main interpretation function *) val interp_gen : typing_constraint -> evar_map -> env -> - ?impls:full_implicits_env -> ?allow_soapp:bool -> ?ltacvars:ltac_sign -> + ?impls:full_implicits_env -> ?allow_patvar:bool -> ?ltacvars:ltac_sign -> constr_expr -> constr (* Particular instances *) diff --git a/parsing/g_constr.ml4 b/parsing/g_constr.ml4 index b29b82607..1a721a2e3 100644 --- a/parsing/g_constr.ml4 +++ b/parsing/g_constr.ml4 @@ -151,7 +151,10 @@ GEXTEND Gram | c1 = operconstr; "->"; c2 = SELF -> CArrow(loc,c1,c2)] | "10" LEFTA [ f=operconstr; args=LIST1 appl_arg -> CApp(loc,(None,f),args) - | "@"; f=global; args=LIST0 NEXT -> CAppExpl(loc,(None,f),args) ] + | "@"; f=global; args=LIST0 NEXT -> CAppExpl(loc,(None,f),args) + | "@"; "?"; (locid,id) = identref; args=LIST1 identref -> + let args = List.map (fun x -> CRef (Ident x), None) args in + CApp(loc,(None,CPatVar(locid,(true,id))),args) ] | "9" [ ".."; c = operconstr LEVEL "0"; ".." -> CAppExpl (loc,(None,Ident (loc,Topconstr.ldots_var)),[c]) ] diff --git a/pretyping/pattern.ml b/pretyping/pattern.ml index 979ecb0b1..b0fd76cb7 100644 --- a/pretyping/pattern.ml +++ b/pretyping/pattern.ml @@ -216,7 +216,7 @@ let rec pat_of_raw metas vars = function PRef r (* Hack pour ne pas réécrire une interprétation complète des patterns*) | RApp (_, RPatVar (_,(true,n)), cl) -> - PSoApp (n, List.map (pat_of_raw metas vars) cl) + metas := n::!metas; PSoApp (n, List.map (pat_of_raw metas vars) cl) | RApp (_,c,cl) -> PApp (pat_of_raw metas vars c, Array.of_list (List.map (pat_of_raw metas vars) cl)) diff --git a/tactics/tacinterp.ml b/tactics/tacinterp.ml index 799361a27..1bbf87a40 100644 --- a/tactics/tacinterp.ml +++ b/tactics/tacinterp.ml @@ -536,7 +536,7 @@ let intern_hyp_location ist ((occs,id),hl) = ((List.map (intern_or_var ist) occs,intern_hyp ist (skip_metaid id)), hl) let interp_constrpattern_gen sigma env ltacvar c = - let c = intern_gen false ~allow_soapp:true ~ltacvars:(ltacvar,[]) + let c = intern_gen false ~allow_patvar:true ~ltacvars:(ltacvar,[]) sigma env c in pattern_of_rawconstr c diff --git a/test-suite/success/ltac.v b/test-suite/success/ltac.v index 3f25f7035..05a6a70f3 100644 --- a/test-suite/success/ltac.v +++ b/test-suite/success/ltac.v @@ -175,3 +175,16 @@ Abort. Goal True. match None with @None => exact I end. Abort. + +(* Check second-order pattern unification *) + +Ltac to_exist := + match goal with + |- forall x y, @?P x y => + let Q := eval lazy beta in (exists x, forall y, P x y) in + assert (Q->Q) + end. + +Goal forall x y : nat, x = y. +to_exist. exact (fun H => H). +Abort. |