diff options
| -rw-r--r-- | CHANGES.md | 9 | ||||
| -rw-r--r-- | doc/sphinx/proof-engine/ssreflect-proof-language.rst | 115 | ||||
| -rw-r--r-- | plugins/ssr/ssrast.mli | 25 | ||||
| -rw-r--r-- | plugins/ssr/ssrcommon.ml | 66 | ||||
| -rw-r--r-- | plugins/ssr/ssrcommon.mli | 31 | ||||
| -rw-r--r-- | plugins/ssr/ssreflect.v | 8 | ||||
| -rw-r--r-- | plugins/ssr/ssrelim.ml | 104 | ||||
| -rw-r--r-- | plugins/ssr/ssrelim.mli | 16 | ||||
| -rw-r--r-- | plugins/ssr/ssrequality.ml | 21 | ||||
| -rw-r--r-- | plugins/ssr/ssrfwd.ml | 6 | ||||
| -rw-r--r-- | plugins/ssr/ssripats.ml | 331 | ||||
| -rw-r--r-- | plugins/ssr/ssrparser.mlg | 125 | ||||
| -rw-r--r-- | plugins/ssr/ssrprinters.ml | 18 | ||||
| -rw-r--r-- | plugins/ssr/ssrview.ml | 170 | ||||
| -rw-r--r-- | plugins/ssr/ssrview.mli | 9 | ||||
| -rw-r--r-- | test-suite/ssr/elim.v | 2 | ||||
| -rw-r--r-- | test-suite/ssr/ipat_clear_if_id.v | 9 | ||||
| -rw-r--r-- | test-suite/ssr/ipat_fastid.v | 31 | ||||
| -rw-r--r-- | test-suite/ssr/ipat_seed.v | 60 | ||||
| -rw-r--r-- | test-suite/ssr/ipat_tac.v | 38 | ||||
| -rw-r--r-- | test-suite/ssr/ipat_tmp.v | 22 |
21 files changed, 889 insertions, 327 deletions
diff --git a/CHANGES.md b/CHANGES.md index fe9f758597..d64b5accd7 100644 --- a/CHANGES.md +++ b/CHANGES.md @@ -139,6 +139,15 @@ Misc - Option "Typeclasses Axioms Are Instances" is deprecated. Use Declare Instance for axioms which should be instances. +SSReflect + +- New intro patterns: + - temporary introduction: => + + - block introduction: => [^ prefix ] [^~ suffix ] + - fast introduction: => >H + - tactics as views: => /ltac:mytac + See the reference manual for the actual documentation. + Changes from 8.8.2 to 8.9+beta1 =============================== diff --git a/doc/sphinx/proof-engine/ssreflect-proof-language.rst b/doc/sphinx/proof-engine/ssreflect-proof-language.rst index b664eb4ec5..bffbe3e284 100644 --- a/doc/sphinx/proof-engine/ssreflect-proof-language.rst +++ b/doc/sphinx/proof-engine/ssreflect-proof-language.rst @@ -1550,20 +1550,26 @@ whose general syntax is :undocumented: .. prodn:: - i_item ::= @i_pattern %| @s_item %| @clear_switch %| {? %{%} } /@term + i_item ::= @i_pattern %| @s_item %| @clear_switch %| @i_view %| @i_block .. prodn:: s_item ::= /= %| // %| //= .. prodn:: - i_pattern ::= @ident %| _ %| ? %| * %| {? @occ_switch } -> %| {? @occ_switch }<- %| [ {?| @i_item } ] %| - %| [: {+ @ident } ] + i_view ::= {? %{%} } /@term %| /ltac:( @tactic ) -The ``=>`` tactical first executes tactic, then the :token:`i_item` s, +.. prodn:: + i_pattern ::= @ident %| > @ident %| _ %| ? %| * %| + %| {? @occ_switch } -> %| {? @occ_switch }<- %| [ {?| @i_item } ] %| - %| [: {+ @ident } ] + +.. prodn:: + i_block ::= [^ @ident ] %| [^~ @ident ] %| [^~ @num ] + +The ``=>`` tactical first executes :token:`tactic`, then the :token:`i_item`\s, left to right. An :token:`s_item` specifies a simplification operation; a :token:`clear_switch` -h specifies context pruning as in :ref:`discharge_ssr`. -The :token:`i_pattern` s can be seen as a variant of *intro patterns* -:ref:`tactics`: each performs an introduction operation, i.e., pops some +specifies context pruning as in :ref:`discharge_ssr`. +The :token:`i_pattern`\s can be seen as a variant of *intro patterns* +(see :tacn:`intros`:) each performs an introduction operation, i.e., pops some variables or assumptions from the goal. An :token:`s_item` can simplify the set of subgoals or the subgoals themselves: @@ -1572,7 +1578,7 @@ An :token:`s_item` can simplify the set of subgoals or the subgoals themselves: |SSR| tactic :tacn:`done` described in :ref:`terminators_ssr`, i.e., it executes ``try done``. + ``/=`` simplifies the goal by performing partial evaluation, as per the - tactic ``simpl`` [#5]_. + tactic :tacn:`simpl` [#5]_. + ``//=`` combines both kinds of simplification; it is equivalent to ``/= //``, i.e., ``simpl; try done``. @@ -1583,21 +1589,42 @@ When an :token:`s_item` bears a :token:`clear_switch`, then the possibly using the fact ``IHn``, and will erase ``IHn`` from the context of the remaining subgoals. -The last entry in the :token:`i_item` grammar rule, ``/``:token:`term`, +The first entry in the :token:`i_view` grammar rule, :n:`/@term`, represents a view (see section :ref:`views_and_reflection_ssr`). +It interprets the top of the stack with the view :token:`term`. +It is equivalent to ``move/term``. The optional flag ``{}`` can +be used to signal that the :token:`term`, when it is a context entry, +has to be cleared. If the next :token:`i_item` is a view, then the view is applied to the assumption in top position once all the previous :token:`i_item` have been performed. -The view is applied to the top assumption. +The second entry in the :token:`i_view` grammar rule, +``/ltac:(`` :token:`tactic` ``)``, executes :token:`tactic`. +Notations can be used to name tactics, for example:: + + Notation myop := (ltac:(some ltac code)) : ssripat_scope. -|SSR| supports the following :token:`i_pattern` s: +lets one write just ``/myop`` in the intro pattern. Note the scope +annotation: views are interpreted opening the ``ssripat`` scope. + +|SSR| supports the following :token:`i_pattern`\s: :token:`ident` pops the top variable, assumption, or local definition into a new constant, fact, or defined constant :token:`ident`, respectively. Note that defined constants cannot be introduced when δ-expansion is required to expose the top variable or assumption. +``>``:token:`ident` + pops the first assumption. Type class instances are not considered + as assumptions. + The tactic ``move=> >H`` is equivalent to + ``move=> ? ? H`` with enough ``?`` to name ``H`` the first assumption. + On a goal:: + + forall x y, x < y -> G + + it names ``H`` the assumption ``x < y``. ``?`` pops the top variable into an anonymous constant or fact, whose name is picked by the tactic interpreter. |SSR| only generates names that cannot @@ -1620,7 +1647,17 @@ The view is applied to the top assumption. a first ``move=> *`` adds only ``_a_ : bool`` and ``_b_ : bool`` to the context; it takes a second ``move=> *`` to add ``_Hyp_ : _a_ = _b_``. -:token:`occ_switch` ``->`` +``+`` + temporarily introduces the top variable. It is discharged at the end + of the intro pattern. For example ``move=> + y`` on a goal:: + + forall x y, P + + is equivalent to ``move=> _x_ y; move: _x_`` that results in the goal:: + + forall x, P + +:n:`{? occ_switch } ->` (resp. :token:`occ_switch` ``<-``) pops the top assumption (which should be a rewritable proposition) into an anonymous fact, rewrites (resp. rewrites right to left) the goal with this @@ -1645,18 +1682,13 @@ The view is applied to the top assumption. variable, using the |SSR| ``case`` tactic described in :ref:`the_defective_tactics_ssr`. It then behaves as the corresponding branching :token:`i_pattern`, executing the - sequence:token:`i_item`:math:`_i` in the i-th subgoal generated by the + sequence :n:`@i_item__i` in the i-th subgoal generated by the case analysis; unless we have the trivial destructing :token:`i_pattern` ``[]``, the latter should generate exactly m subgoals, i.e., the top variable should have an inductive type with exactly m constructors [#7]_. While it is good style to use the :token:`i_item` i * to pop the variables and assumptions corresponding to each constructor, this is not enforced by |SSR|. -``/`` :token:`term` - Interprets the top of the stack with the view :token:`term`. - It is equivalent to ``move/term``. The optional flag ``{}`` can - be used to signal that the :token:`term`, when it is a context entry, - has to be cleared. ``-`` does nothing, but counts as an intro pattern. It can also be used to force the interpretation of ``[`` :token:`i_item` * ``| … |`` @@ -1721,6 +1753,40 @@ interpretation, e.g.: are all equivalent. +|SSR| supports the following :token:`i_block`\s: + +:n:`[^ @ident ]` + *block destructing* :token:`i_pattern`. It performs a case analysis + on the top variable and introduces, in one go, all the variables coming + from the case analysis. The names of these variables are obtained by + taking the names used in the inductive type declaration and prefixing them + with :token:`ident`. If the intro pattern immediately follows a call + to ``elim`` with a custom eliminator (see :ref:`custom_elim_ssr`) then + the names are taken from the ones used in the type of the eliminator. + + .. example:: + + .. coqtop:: reset + + From Coq Require Import ssreflect. + Set Implicit Arguments. + Unset Strict Implicit. + Unset Printing Implicit Defensive. + + .. coqtop:: all + + Record r := { a : nat; b := (a, 3); _ : bool; }. + + Lemma test : r -> True. + Proof. move => [^ x ]. + +:n:`[^~ @ident ]` + *block destructing* using :token:`ident` as a suffix. +:n:`[^~ @num ]` + *block destructing* using :token:`num` as a suffix. + + Only a :token:`s_item` is allowed between the elimination tactic and + the block destructing. .. _generation_of_equations_ssr: @@ -4160,6 +4226,7 @@ interpretation operations with the proof stack operations. This *view mechanism* relies on the combination of the ``/`` view switch with bookkeeping tactics and tacticals. +.. _custom_elim_ssr: Interpreting eliminations ~~~~~~~~~~~~~~~~~~~~~~~~~ @@ -5238,11 +5305,21 @@ discharge item see :ref:`discharge_ssr` generalization item see :ref:`structure_ssr` -.. prodn:: i_pattern ::= @ident %| _ %| ? %| * %| {? @occ_switch } -> %| {? @occ_switch } <- %| [ {*| {* @i_item } } %| - %| [: {+ @ident } ] +.. prodn:: i_pattern ::= @ident %| > @ident %| _ %| ? %| * %| + %| {? @occ_switch } -> %| {? @occ_switch } <- %| [ {?| @i_item } ] %| - %| [: {+ @ident } ] intro pattern :ref:`introduction_ssr` -.. prodn:: i_item ::= @clear_switch %| @s_item %| @i_pattern %| {? %{%} } / @term +.. prodn:: i_item ::= @clear_switch %| @s_item %| @i_pattern %| @i_view %| @i_block + +view :ref:`introduction_ssr` + +.. prodn:: + i_view ::= {? %{%} } /@term %| /ltac:( @tactic ) + +intro block :ref:`introduction_ssr` + +.. prodn:: + i_block ::= [^ @ident ] %| [^~ @ident ] %| [^~ @num ] intro item see :ref:`introduction_ssr` diff --git a/plugins/ssr/ssrast.mli b/plugins/ssr/ssrast.mli index 11e282e4f5..fac524da6b 100644 --- a/plugins/ssr/ssrast.mli +++ b/plugins/ssr/ssrast.mli @@ -64,38 +64,37 @@ type ast_closure_term = { type ssrview = ast_closure_term list -(* TODO -type id_mod = Hat | HatTilde | Sharp - *) +type id_mod = Dependent + +type id_block = Prefix of Id.t | SuffixId of Id.t | SuffixNum of int (* Only [One] forces an introduction, possibly reducing the goal. *) type anon_iter = - | One + | One of string option (* name hint *) | Drop | All -(* TODO - | Dependent (* fast mode *) - | UntilMark - | Temporary (* "+" *) - *) + | Temporary type ssripat = | IPatNoop - | IPatId of (*TODO id_mod option * *) Id.t + | IPatId of id_mod option * Id.t | IPatAnon of anon_iter (* inaccessible name *) (* TODO | IPatClearMark *) - | IPatDispatch of bool (* ssr exception: accept a dispatch on the empty list even when there are subgoals *) * ssripatss (* (..|..) *) - | IPatCase of (* ipats_mod option * *) ssripatss (* this is not equivalent to /case /[..|..] if there are already multiple goals *) + | IPatDispatch of bool (* ssr exception: accept a dispatch on the empty list even when there are subgoals *) * ssripatss_or_block (* (..|..) *) + | IPatCase of (* ipats_mod option * *) ssripatss_or_block (* this is not equivalent to /case /[..|..] if there are already multiple goals *) | IPatInj of ssripatss | IPatRewrite of (*occurrence option * rewrite_pattern **) ssrocc * ssrdir | IPatView of bool * ssrview (* {}/view (true if the clear is present) *) | IPatClear of ssrclear (* {H1 H2} *) | IPatSimpl of ssrsimpl | IPatAbstractVars of Id.t list - | IPatTac of unit Proofview.tactic + | IPatEqGen of unit Proofview.tactic (* internal use: generation of eqn *) and ssripats = ssripat list and ssripatss = ssripats list +and ssripatss_or_block = + | Block of id_block + | Regular of ssripats list type ssrhpats = ((ssrclear * ssripats) * ssripats) * ssripats type ssrhpats_wtransp = bool * ssrhpats diff --git a/plugins/ssr/ssrcommon.ml b/plugins/ssr/ssrcommon.ml index cd9af84ed9..311d912efd 100644 --- a/plugins/ssr/ssrcommon.ml +++ b/plugins/ssr/ssrcommon.ml @@ -401,6 +401,7 @@ let max_suffix m (t, j0 as tj0) id = dt < ds && skip_digits s i = n in loop m +(** creates a fresh (w.r.t. `gl_ids` and internal names) inaccessible name of the form _tXX_ *) let mk_anon_id t gl_ids = let m, si0, id0 = let s = ref (Printf.sprintf "_%s_" t) in @@ -409,7 +410,7 @@ let mk_anon_id t gl_ids = let rec loop i j = let d = !s.[i] in if not (is_digit d) then i + 1, j else loop (i - 1) (if d = '0' then j else i) in - let m, j = loop (n - 1) n in m, (!s, j), Id.of_string !s in + let m, j = loop (n - 1) n in m, (!s, j), Id.of_string_soft !s in if not (List.mem id0 gl_ids) then id0 else let s, i = List.fold_left (max_suffix m) si0 gl_ids in let open Bytes in @@ -419,7 +420,7 @@ let mk_anon_id t gl_ids = if get s i = '9' then (set s i '0'; loop (i - 1)) else if i < m then (set s n '0'; set s m '1'; cat s (of_string "_")) else (set s i (Char.chr (Char.code (get s i) + 1)); s) in - Id.of_bytes (loop (n - 1)) + Id.of_string_soft (Bytes.to_string (loop (n - 1))) let convert_concl_no_check t = Tactics.convert_concl_no_check t DEFAULTcast let convert_concl t = Tactics.convert_concl t DEFAULTcast @@ -808,18 +809,6 @@ let clear_wilds_and_tmp_and_delayed_ids gl = (clear_with_wilds ctx.wild_ids ctx.delayed_clears) (clear_wilds (List.map fst ctx.tmp_ids @ ctx.wild_ids))) gl -let rec is_name_in_ipats name = function - | IPatClear clr :: tl -> - List.exists (function SsrHyp(_,id) -> id = name) clr - || is_name_in_ipats name tl - | IPatId id :: tl -> id = name || is_name_in_ipats name tl - | IPatAbstractVars ids :: tl -> - CList.mem_f Id.equal name ids || is_name_in_ipats name tl - | (IPatCase l | IPatDispatch (_,l) | IPatInj l) :: tl -> - List.exists (is_name_in_ipats name) l || is_name_in_ipats name tl - | (IPatView _ | IPatAnon _ | IPatSimpl _ | IPatRewrite _ | IPatTac _ | IPatNoop) :: tl -> is_name_in_ipats name tl - | [] -> false - let view_error s gv = errorstrm (str ("Cannot " ^ s ^ " view ") ++ pr_term gv) @@ -1187,9 +1176,23 @@ let gen_tmp_ids ctx.tmp_ids) gl) ;; -let pf_interp_gen gl to_ind gen = +let pf_interp_gen to_ind gen gl = let _, _, a, b, c, ucst,gl = pf_interp_gen_aux gl to_ind gen in - a, b ,c, pf_merge_uc ucst gl + (a, b ,c), pf_merge_uc ucst gl + +let pfLIFT f = + let open Proofview.Notations in + let hack = ref None in + Proofview.V82.tactic (fun gl -> + let g = sig_it gl in + let x, gl = f gl in + hack := Some (x,project gl); + re_sig [g] (project gl)) + >>= fun () -> + let x, sigma = option_assert_get !hack (Pp.str"pfLIFT") in + Proofview.Unsafe.tclEVARS sigma <*> + Proofview.tclUNIT x +;; (* TASSI: This version of unprotects inlines the unfold tactic definition, * since we don't want to wipe out let-ins, and it seems there is no flag @@ -1273,7 +1276,7 @@ let unfold cl = open Proofview open Notations -let tacSIGMA = Goal.enter_one begin fun g -> +let tacSIGMA = Goal.enter_one ~__LOC__ begin fun g -> let k = Goal.goal g in let sigma = Goal.sigma g in tclUNIT (Tacmach.re_sig k sigma) @@ -1347,6 +1350,11 @@ let tclFULL_BETAIOTA = Goal.enter begin fun gl -> Tactics.e_reduct_in_concl ~check:false (r,Constr.DEFAULTcast) end +type intro_id = + | Anon + | Id of Id.t + | Seed of string + (** [intro id k] introduces the first premise (product or let-in) of the goal under the name [id], reducing the head of the goal (using beta, iota, delta but not zeta) if necessary. If [id] is None, a name is generated, that will @@ -1360,11 +1368,12 @@ let tclINTRO ~id ~conclusion:k = Goal.enter begin fun gl -> let original_name = Rel.Declaration.get_name decl in let already_used = Tacmach.New.pf_ids_of_hyps gl in let id = match id, original_name with - | Some id, _ -> id - | _, Name id -> + | Id id, _ -> id + | Seed id, _ -> mk_anon_id id already_used + | Anon, Name id -> if is_discharged_id id then id else mk_anon_id (Id.to_string id) already_used - | _, _ -> + | Anon, Anonymous -> let ids = Tacmach.New.pf_ids_of_hyps gl in mk_anon_id ssr_anon_hyp ids in @@ -1377,8 +1386,11 @@ end let return ~orig_name:_ ~new_name:_ = tclUNIT () -let tclINTRO_ID id = tclINTRO ~id:(Some id) ~conclusion:return -let tclINTRO_ANON = tclINTRO ~id:None ~conclusion:return +let tclINTRO_ID id = tclINTRO ~id:(Id id) ~conclusion:return +let tclINTRO_ANON ?seed () = + match seed with + | None -> tclINTRO ~id:Anon ~conclusion:return + | Some seed -> tclINTRO ~id:(Seed seed) ~conclusion:return let tclRENAME_HD_PROD name = Goal.enter begin fun gl -> let convert_concl_no_check t = @@ -1391,8 +1403,8 @@ let tclRENAME_HD_PROD name = Goal.enter begin fun gl -> | _ -> CErrors.anomaly (Pp.str "rename_hd_prod: no head product") end -let tcl0G tac = - numgoals >>= fun ng -> if ng = 0 then tclUNIT () else tac +let tcl0G ~default tac = + numgoals >>= fun ng -> if ng = 0 then tclUNIT default else tac let rec tclFIRSTa = function | [] -> Tacticals.New.tclZEROMSG Pp.(str"No applicable tactic.") @@ -1491,6 +1503,12 @@ let tclGET k = Goal.enter begin fun gl -> k (Option.default S.init (get (Goal.state gl) state_field)) end +let tclGET1 k = Goal.enter_one begin fun gl -> + let open Proofview_monad.StateStore in + k (Option.default S.init (get (Goal.state gl) state_field)) +end + + let tclSET new_s = let open Proofview_monad.StateStore in Unsafe.tclGETGOALS >>= fun gls -> diff --git a/plugins/ssr/ssrcommon.mli b/plugins/ssr/ssrcommon.mli index 824827e90c..51116ccd75 100644 --- a/plugins/ssr/ssrcommon.mli +++ b/plugins/ssr/ssrcommon.mli @@ -359,24 +359,17 @@ val genstac : Tacmach.tactic val pf_interp_gen : - Goal.goal Evd.sigma -> bool -> (Ssrast.ssrhyp list option * Ssrmatching.occ) * Ssrmatching.cpattern -> - EConstr.t * EConstr.t * Ssrast.ssrhyp list * - Goal.goal Evd.sigma - -val pf_interp_gen_aux : Goal.goal Evd.sigma -> - bool -> - (Ssrast.ssrhyp list option * Ssrmatching.occ) * - Ssrmatching.cpattern -> - bool * Ssrmatching.pattern * EConstr.t * - EConstr.t * Ssrast.ssrhyp list * UState.t * - Goal.goal Evd.sigma + (EConstr.t * EConstr.t * Ssrast.ssrhyp list) * + Goal.goal Evd.sigma -val is_name_in_ipats : - Id.t -> ssripats -> bool +(* HACK: use to put old pf_code in the tactic monad *) +val pfLIFT + : (Goal.goal Evd.sigma -> 'a * Goal.goal Evd.sigma) + -> 'a Proofview.tactic (** Basic tactics *) @@ -431,18 +424,23 @@ val tacREDUCE_TO_QUANTIFIED_IND : val tacTYPEOF : EConstr.t -> EConstr.types Proofview.tactic val tclINTRO_ID : Id.t -> unit Proofview.tactic -val tclINTRO_ANON : unit Proofview.tactic +val tclINTRO_ANON : ?seed:string -> unit -> unit Proofview.tactic (* Lower level API, calls conclusion with the name taken from the prod *) +type intro_id = + | Anon + | Id of Id.t + | Seed of string + val tclINTRO : - id:Id.t option -> + id:intro_id -> conclusion:(orig_name:Name.t -> new_name:Id.t -> unit Proofview.tactic) -> unit Proofview.tactic val tclRENAME_HD_PROD : Name.t -> unit Proofview.tactic (* calls the tactic only if there are more than 0 goals *) -val tcl0G : unit Proofview.tactic -> unit Proofview.tactic +val tcl0G : default:'a -> 'a Proofview.tactic -> 'a Proofview.tactic (* like tclFIRST but with 'a tactic *) val tclFIRSTa : 'a Proofview.tactic list -> 'a Proofview.tactic @@ -474,6 +472,7 @@ end module MakeState(S : StateType) : sig val tclGET : (S.state -> unit Proofview.tactic) -> unit Proofview.tactic + val tclGET1 : (S.state -> 'a Proofview.tactic) -> 'a Proofview.tactic val tclSET : S.state -> unit Proofview.tactic val tacUPDATE : (S.state -> S.state Proofview.tactic) -> unit Proofview.tactic diff --git a/plugins/ssr/ssreflect.v b/plugins/ssr/ssreflect.v index 01af67912a..7596f6638a 100644 --- a/plugins/ssr/ssreflect.v +++ b/plugins/ssr/ssreflect.v @@ -86,10 +86,16 @@ Export SsrMatchingSyntax. Export SsrSyntax. (** + To define notations for tactic in intro patterns. + When "=> /t" is parsed, "t:%ssripat" is actually interpreted. **) +Declare Scope ssripat_scope. +Delimit Scope ssripat_scope with ssripat. + +(** Make the general "if" into a notation, so that we can override it below. The notations are "only parsing" because the Coq decompiler will not recognize the expansion of the boolean if; using the default printer - avoids a spurrious trailing %%GEN_IF. **) + avoids a spurrious trailing %%GEN_IF. **) Declare Scope general_if_scope. Delimit Scope general_if_scope with GEN_IF. diff --git a/plugins/ssr/ssrelim.ml b/plugins/ssr/ssrelim.ml index 2c9ec3a7cf..a0b1d784f1 100644 --- a/plugins/ssr/ssrelim.ml +++ b/plugins/ssr/ssrelim.ml @@ -102,20 +102,28 @@ let get_eq_type gl = let eq, gl = pf_fresh_global Coqlib.(lib_ref "core.eq.type") gl in gl, EConstr.of_constr eq -let ssrelim ?(ind=ref None) ?(is_case=false) deps what ?elim eqid elim_intro_tac gl = +let ssrelim ?(is_case=false) deps what ?elim eqid elim_intro_tac = + let open Proofview.Notations in + Proofview.tclEVARMAP >>= begin fun sigma -> (* some sanity checks *) - let oc, orig_clr, occ, c_gen, gl = match what with - | `EConstr(_,_,t) when EConstr.isEvar (project gl) t -> - anomaly "elim called on a constr evar" + match what with + | `EConstr(_,_,t) when EConstr.isEvar sigma t -> + anomaly "elim called on a constr evar" | `EGen (_, g) when elim = None && is_wildcard g -> errorstrm Pp.(str"Indeterminate pattern and no eliminator") | `EGen ((Some clr,occ), g) when is_wildcard g -> - None, clr, occ, None, gl - | `EGen ((None, occ), g) when is_wildcard g -> None,[],occ,None,gl + Proofview.tclUNIT (None, clr, occ, None) + | `EGen ((None, occ), g) when is_wildcard g -> + Proofview.tclUNIT (None,[],occ,None) | `EGen ((_, occ), p as gen) -> - let _, c, clr,gl = pf_interp_gen gl true gen in - Some c, clr, occ, Some p,gl - | `EConstr (clr, occ, c) -> Some c, clr, occ, None,gl in + pfLIFT (pf_interp_gen true gen) >>= fun (_,c,clr) -> + Proofview.tclUNIT (Some c, clr, occ, Some p) + | `EConstr (clr, occ, c) -> + Proofview.tclUNIT (Some c, clr, occ, None) + end >>= + + fun (oc, orig_clr, occ, c_gen) -> pfLIFT begin fun gl -> + let orig_gl, concl, env = gl, pf_concl gl, pf_env gl in ppdebug(lazy(Pp.str(if is_case then "==CASE==" else "==ELIM=="))); let fire_subst gl t = Reductionops.nf_evar (project gl) t in @@ -145,13 +153,26 @@ let ssrelim ?(ind=ref None) ?(is_case=false) deps what ?elim eqid elim_intro_tac (* finds the eliminator applies it to evars and c saturated as needed *) (* obtaining "elim ??? (c ???)". pred is the higher order evar *) (* cty is None when the user writes _ (hence we can't make a pattern *) - let cty, elim, elimty, elim_args, n_elim_args, elim_is_dep, is_rec, pred, gl = + (* `seed` represents the array of types from which we derive the name seeds + for the block intro patterns *) + let seed, cty, elim, elimty, elim_args, n_elim_args, elim_is_dep, is_rec, pred, gl = match elim with | Some elim -> let gl, elimty = pf_e_type_of gl elim in + let elimty = + let rename_elimty r = + EConstr.of_constr + (Arguments_renaming.rename_type + (EConstr.to_constr ~abort_on_undefined_evars:false (project gl) + elimty) r) in + match EConstr.kind (project gl) elim with + | Constr.Var kn -> rename_elimty (GlobRef.VarRef kn) + | Constr.Const (kn,_) -> rename_elimty (GlobRef.ConstRef kn) + | _ -> elimty + in let pred_id, n_elim_args, is_rec, elim_is_dep, n_pred_args,ctx_concl = analyze_eliminator elimty env (project gl) in - ind := Some (0, subgoals_tys (project gl) ctx_concl); + let seed = subgoals_tys (project gl) ctx_concl in let elim, elimty, elim_args, gl = pf_saturate ~beta:is_case gl elim ~ty:elimty n_elim_args in let pred = List.assoc pred_id elim_args in @@ -164,7 +185,7 @@ let ssrelim ?(ind=ref None) ?(is_case=false) deps what ?elim eqid elim_intro_tac | Some p -> interp_cpattern orig_gl p None | _ -> mkTpat gl c in Some(c, c_ty, pc), gl in - cty, elim, elimty, elim_args, n_elim_args, elim_is_dep, is_rec, pred, gl + seed, cty, elim, elimty, elim_args, n_elim_args, elim_is_dep, is_rec, pred, gl | None -> let c = Option.get oc in let gl, c_ty = pfe_type_of gl c in let ((kn, i),_ as indu), unfolded_c_ty = @@ -183,11 +204,26 @@ let ssrelim ?(ind=ref None) ?(is_case=false) deps what ?elim eqid elim_intro_tac let gl, elimty = pfe_type_of gl elim in let pred_id,n_elim_args,is_rec,elim_is_dep,n_pred_args,ctx_concl = analyze_eliminator elimty env (project gl) in - if is_case then - let mind,indb = Inductive.lookup_mind_specif env (kn,i) in - ind := Some(mind.Declarations.mind_nparams,Array.map EConstr.of_constr indb.Declarations.mind_nf_lc); - else - ind := Some (0, subgoals_tys (project gl) ctx_concl); + let seed = + if is_case then + let mind,indb = Inductive.lookup_mind_specif env (kn,i) in + let tys = indb.Declarations.mind_nf_lc in + let renamed_tys = + Array.mapi (fun j t -> + ppdebug(lazy Pp.(str "Search" ++ Printer.pr_constr_env env (project gl) t)); + let t = Arguments_renaming.rename_type t + (GlobRef.ConstructRef((kn,i),j+1)) in + ppdebug(lazy Pp.(str"Done Search " ++ Printer.pr_constr_env env (project gl) t)); + t) + tys + in + let drop_params x = + snd @@ EConstr.decompose_prod_n_assum (project gl) + mind.Declarations.mind_nparams (EConstr.of_constr x) in + Array.map drop_params renamed_tys + else + subgoals_tys (project gl) ctx_concl + in let rctx = fst (EConstr.decompose_prod_assum (project gl) unfolded_c_ty) in let n_c_args = Context.Rel.length rctx in let c, c_ty, t_args, gl = pf_saturate gl c ~ty:c_ty n_c_args in @@ -199,7 +235,7 @@ let ssrelim ?(ind=ref None) ?(is_case=false) deps what ?elim eqid elim_intro_tac | _ -> mkTpat gl c in let cty = Some (c, c_ty, pc) in let elimty = Reductionops.whd_all env (project gl) elimty in - cty, elim, elimty, elim_args, n_elim_args, elim_is_dep, is_rec, pred, gl + seed, cty, elim, elimty, elim_args, n_elim_args, elim_is_dep, is_rec, pred, gl in ppdebug(lazy Pp.(str"elim= "++ pr_constr_pat (EConstr.Unsafe.to_constr elim))); ppdebug(lazy Pp.(str"elimty= "++ pr_constr_pat (EConstr.Unsafe.to_constr elimty))); @@ -377,16 +413,29 @@ let ssrelim ?(ind=ref None) ?(is_case=false) deps what ?elim eqid elim_intro_tac in (* the elim tactic, with the eliminator and the predicated we computed *) let elim = project gl, elim in - let elim_tac gl = - Tacticals.tclTHENLIST [refine_with ~with_evars:false elim; old_cleartac clr] gl in - Tacticals.tclTHENLIST [gen_eq_tac; elim_intro_tac what eqid elim_tac is_rec clr] orig_gl + let seed = + Array.map (fun ty -> + let ctx,_ = EConstr.decompose_prod_assum (project gl) ty in + CList.rev_map Context.Rel.Declaration.get_name ctx) seed in + (elim,seed,clr,is_rec,gen_eq_tac), orig_gl -let no_intro ?ist what eqid elim_tac is_rec clr = elim_tac + end >>= fun (elim, seed,clr,is_rec,gen_eq_tac) -> + + let elim_tac = + Tacticals.New.tclTHENLIST [ + Proofview.V82.tactic (refine_with ~with_evars:false elim); + cleartac clr] in + let gen_eq_tac = Proofview.V82.tactic gen_eq_tac in + Tacticals.New.tclTHENLIST [gen_eq_tac; elim_intro_tac ?seed:(Some seed) what eqid elim_tac is_rec clr] +;; let elimtac x = - Proofview.V82.tactic ~nf_evars:false - (ssrelim ~is_case:false [] (`EConstr ([],None,x)) None no_intro) -let casetac x = ssrelim ~is_case:true [] (`EConstr ([],None,x)) None no_intro + let k ?seed:_ _what _eqid elim_tac _is_rec _clr = elim_tac in + ssrelim ~is_case:false [] (`EConstr ([],None,x)) None k + +let casetac x k = + let k ?seed _what _eqid elim_tac _is_rec _clr = k ?seed elim_tac in + ssrelim ~is_case:true [] (`EConstr ([],None,x)) None k let pf_nb_prod gl = nb_prod (project gl) (pf_concl gl) @@ -444,7 +493,4 @@ let perform_injection c gl = let ssrscase_or_inj_tac c = Proofview.V82.tactic ~nf_evars:false (fun gl -> if is_injection_case c gl then perform_injection c gl - else casetac c gl) - -let ssrscasetac c = - Proofview.V82.tactic ~nf_evars:false (fun gl -> casetac c gl) + else Proofview.V82.of_tactic (casetac c (fun ?seed:_ k -> k)) gl) diff --git a/plugins/ssr/ssrelim.mli b/plugins/ssr/ssrelim.mli index c7ffba917e..a1e2f63b8f 100644 --- a/plugins/ssr/ssrelim.mli +++ b/plugins/ssr/ssrelim.mli @@ -13,7 +13,6 @@ open Ssrmatching_plugin val ssrelim : - ?ind:(int * EConstr.types array) option ref -> ?is_case:bool -> ((Ssrast.ssrhyps option * Ssrast.ssrocc) * Ssrmatching.cpattern) @@ -29,27 +28,24 @@ val ssrelim : as 'a) -> ?elim:EConstr.constr -> Ssrast.ssripat option -> - ( 'a -> + (?seed:Names.Name.t list array -> 'a -> Ssrast.ssripat option -> - (Goal.goal Evd.sigma -> Goal.goal list Evd.sigma) -> - bool -> Ssrast.ssrhyp list -> Tacmach.tactic) -> - Goal.goal Evd.sigma -> Goal.goal list Evd.sigma + unit Proofview.tactic -> + bool -> Ssrast.ssrhyp list -> unit Proofview.tactic) -> + unit Proofview.tactic val elimtac : EConstr.constr -> unit Proofview.tactic val casetac : EConstr.constr -> - Goal.goal Evd.sigma -> Goal.goal list Evd.sigma + (?seed:Names.Name.t list array -> unit Proofview.tactic -> unit Proofview.tactic) -> + unit Proofview.tactic val is_injection_case : EConstr.t -> Goal.goal Evd.sigma -> bool val perform_injection : EConstr.constr -> Goal.goal Evd.sigma -> Goal.goal list Evd.sigma -val ssrscasetac : - EConstr.constr -> - unit Proofview.tactic - val ssrscase_or_inj_tac : EConstr.constr -> unit Proofview.tactic diff --git a/plugins/ssr/ssrequality.ml b/plugins/ssr/ssrequality.ml index 490e8fbdbc..64e023c68a 100644 --- a/plugins/ssr/ssrequality.ml +++ b/plugins/ssr/ssrequality.ml @@ -181,13 +181,18 @@ let norwocc = noclr, None let simplintac occ rdx sim gl = let simptac m gl = - if m <> ~-1 then - CErrors.user_err (Pp.str "Localized custom simpl tactic not supported"); - let sigma0, concl0, env0 = project gl, pf_concl gl, pf_env gl in - let simp env c _ _ = EConstr.Unsafe.to_constr (red_safe Tacred.simpl env sigma0 (EConstr.of_constr c)) in - Proofview.V82.of_tactic - (convert_concl_no_check (EConstr.of_constr (eval_pattern env0 sigma0 (EConstr.Unsafe.to_constr concl0) rdx occ simp))) - gl in + if m <> ~-1 then begin + if rdx <> None then + CErrors.user_err (Pp.str "Custom simpl tactic does not support patterns"); + if occ <> None then + CErrors.user_err (Pp.str "Custom simpl tactic does not support occurrence numbers"); + simpltac (Simpl m) gl + end else + let sigma0, concl0, env0 = project gl, pf_concl gl, pf_env gl in + let simp env c _ _ = EConstr.Unsafe.to_constr (red_safe Tacred.simpl env sigma0 (EConstr.of_constr c)) in + Proofview.V82.of_tactic + (convert_concl_no_check (EConstr.of_constr (eval_pattern env0 sigma0 (EConstr.Unsafe.to_constr concl0) rdx occ simp))) + gl in match sim with | Simpl m -> simptac m gl | SimplCut (n,m) -> tclTHEN (simptac m) (tclTRY (donetac n)) gl @@ -644,6 +649,6 @@ let unlocktac ist args gl = let key, gl = pf_mkSsrConst "master_key" gl in let ktacs = [ (fun gl -> unfoldtac None None (project gl,locked) xInParens gl); - Ssrelim.casetac key ] in + Proofview.V82.of_tactic (Ssrelim.casetac key (fun ?seed:_ k -> k)) ] in tclTHENLIST (List.map utac args @ ktacs) gl diff --git a/plugins/ssr/ssrfwd.ml b/plugins/ssr/ssrfwd.ml index 8cebe62e16..37c583ab53 100644 --- a/plugins/ssr/ssrfwd.ml +++ b/plugins/ssr/ssrfwd.ml @@ -104,7 +104,7 @@ let havetac ist let itac_c = introstac (IPatClear clr :: pats) in let itac, id, clr = introstac pats, Tacticals.tclIDTAC, old_cleartac clr in let binderstac n = - let rec aux = function 0 -> [] | n -> IPatAnon One :: aux (n-1) in + let rec aux = function 0 -> [] | n -> IPatAnon (One None) :: aux (n-1) in Tacticals.tclTHEN (if binders <> [] then introstac (aux n) else Tacticals.tclIDTAC) (introstac binders) in let simpltac = introstac simpl in @@ -206,7 +206,7 @@ let wlogtac ist (((clr0, pats),_),_) (gens, ((_, ct))) hint suff ghave gl = let mkabs gen = abs_wgen false (fun x -> x) gen in let mkclr gen clrs = clr_of_wgen gen clrs in let mkpats = function - | _, Some ((x, _), _) -> fun pats -> IPatId (hoi_id x) :: pats + | _, Some ((x, _), _) -> fun pats -> IPatId (None,hoi_id x) :: pats | _ -> fun x -> x in let ct = match Ssrcommon.ssrterm_of_ast_closure_term ct with | (a, (b, Some ct)) -> @@ -265,7 +265,7 @@ let wlogtac ist (((clr0, pats),_),_) (gens, ((_, ct))) hint suff ghave gl = if gens = [] then errorstrm(str"gen have requires some generalizations"); let clear0 = old_cleartac clr0 in let id, name_general_hyp, cleanup, pats = match id, pats with - | None, (IPatId id as ip)::pats -> Some id, tacipat [ip], clear0, pats + | None, (IPatId(_, id) as ip)::pats -> Some id, tacipat [ip], clear0, pats | None, _ -> None, Tacticals.tclIDTAC, clear0, pats | Some (Some id),_ -> Some id, introid id, clear0, pats | Some _,_ -> diff --git a/plugins/ssr/ssripats.ml b/plugins/ssr/ssripats.ml index 18b4aeab1e..e71e1bae0d 100644 --- a/plugins/ssr/ssripats.ml +++ b/plugins/ssr/ssripats.ml @@ -27,15 +27,31 @@ module IpatMachine : sig val main : ?eqtac:unit tactic -> first_case_is_dispatch:bool -> ssripats -> unit tactic + + val tclSEED_SUBGOALS : Names.Name.t list array -> unit tactic -> unit tactic + end = struct (* {{{ *) module State : sig + type delayed_gen = { + tmp_id : Id.t; (* Temporary name *) + orig_name : Name.t (* Old name *) + } + (* to_clear API *) val isCLR_PUSH : Id.t -> unit tactic val isCLR_PUSHL : Id.t list -> unit tactic val isCLR_CONSUME : unit tactic + (* to_generalize API *) + val isGEN_PUSH : delayed_gen -> unit tactic + val isGEN_CONSUME : unit tactic + + (* name_seed API *) + val isNSEED_SET : Names.Name.t list -> unit tactic + val isNSEED_CONSUME : (Names.Name.t list option -> unit tactic) -> unit tactic + (* Some data may expire *) val isTICK : ssripat -> unit tactic @@ -48,10 +64,23 @@ type istate = { (* Delayed clear *) to_clear : Id.t list; + (* Temporary intros, to be generalized back *) + to_generalize : delayed_gen list; + + (* The type of the inductive constructor corresponding to the current proof + * branch: name seeds are taken from that in an intro block *) + name_seed : Names.Name.t list option; + +} +and delayed_gen = { + tmp_id : Id.t; (* Temporary name *) + orig_name : Name.t (* Old name *) } let empty_state = { to_clear = []; + to_generalize = []; + name_seed = None; } include Ssrcommon.MakeState(struct @@ -59,28 +88,69 @@ include Ssrcommon.MakeState(struct let init = empty_state end) +let print_name_seed env sigma = function + | None -> Pp.str "-" + | Some nl -> Pp.prlist Names.Name.print nl + +let print_delayed_gen { tmp_id; orig_name } = + Pp.(Id.print tmp_id ++ str"->" ++ Name.print orig_name) + let isPRINT g = + let env, sigma = Goal.env g, Goal.sigma g in let state = get g in Pp.(str"{{ to_clear: " ++ prlist_with_sep spc Id.print state.to_clear ++ spc () ++ - str" }}") + str"to_generalize: " ++ + prlist_with_sep spc print_delayed_gen state.to_generalize ++ spc () ++ + str"name_seed: " ++ print_name_seed env sigma state.name_seed ++ str" }}") let isCLR_PUSH id = - tclGET (fun { to_clear = ids } -> - tclSET { to_clear = id :: ids }) + tclGET (fun ({ to_clear = ids } as s) -> + tclSET { s with to_clear = id :: ids }) let isCLR_PUSHL more_ids = - tclGET (fun { to_clear = ids } -> - tclSET { to_clear = more_ids @ ids }) + tclGET (fun ({ to_clear = ids } as s) -> + tclSET { s with to_clear = more_ids @ ids }) let isCLR_CONSUME = - tclGET (fun { to_clear = ids } -> - tclSET { to_clear = [] } <*> + tclGET (fun ({ to_clear = ids } as s) -> + tclSET { s with to_clear = [] } <*> Tactics.clear ids) -let isTICK _ = tclUNIT () +let isGEN_PUSH dg = + tclGET (fun s -> + tclSET { s with to_generalize = dg :: s.to_generalize }) + +(* generalize `id` as `new_name` *) +let gen_astac id new_name = + let gen = ((None,Some(false,[])),Ssrmatching.cpattern_of_id id) in + V82.tactic (Ssrcommon.gentac gen) + <*> Ssrcommon.tclRENAME_HD_PROD new_name + +(* performs and resets all delayed generalizations *) +let isGEN_CONSUME = + tclGET (fun ({ to_generalize = dgs } as s) -> + tclSET { s with to_generalize = [] } <*> + Tacticals.New.tclTHENLIST + (List.map (fun { tmp_id; orig_name } -> + gen_astac tmp_id orig_name) dgs) <*> + Tactics.clear (List.map (fun gen -> gen.tmp_id) dgs)) + + +let isNSEED_SET ty = + tclGET (fun s -> + tclSET { s with name_seed = Some ty }) + +let isNSEED_CONSUME k = + tclGET (fun ({ name_seed = x } as s) -> + tclSET { s with name_seed = None } <*> + k x) + +let isTICK = function + | IPatSimpl _ | IPatClear _ -> tclUNIT () + | _ -> tclGET (fun s -> tclSET { s with name_seed = None }) end (* }}} *************************************************************** *) @@ -105,18 +175,49 @@ let intro_anon_all = Goal.enter begin fun gl -> let sigma = Goal.sigma gl in let g = Goal.concl gl in let n = nb_assums env sigma g in - Tacticals.New.tclDO n Ssrcommon.tclINTRO_ANON + Tacticals.New.tclDO n (Ssrcommon.tclINTRO_ANON ()) +end + +(*** [=> >*] **************************************************************) +(** [nb_deps_assums] returns the number of dependent premises *) +let rec nb_deps_assums cur env sigma t = + let t' = Reductionops.whd_allnolet env sigma t in + match EConstr.kind sigma t' with + | Constr.Prod(name,ty,body) -> + if EConstr.Vars.noccurn sigma 1 body && + not (Typeclasses.is_class_type sigma ty) then cur + else nb_deps_assums (cur+1) env sigma body + | Constr.LetIn(name,ty,t1,t2) -> + nb_deps_assums (cur+1) env sigma t2 + | Constr.Cast(t,_,_) -> + nb_deps_assums cur env sigma t + | _ -> cur +let nb_deps_assums = nb_deps_assums 0 + +let intro_anon_deps = Goal.enter begin fun gl -> + let env = Goal.env gl in + let sigma = Goal.sigma gl in + let g = Goal.concl gl in + let n = nb_deps_assums env sigma g in + Tacticals.New.tclDO n (Ssrcommon.tclINTRO_ANON ()) end (** [intro_drop] behaves like [intro_anon] but registers the id of the introduced assumption for a delayed clear. *) let intro_drop = - Ssrcommon.tclINTRO ~id:None + Ssrcommon.tclINTRO ~id:Ssrcommon.Anon ~conclusion:(fun ~orig_name:_ ~new_name -> isCLR_PUSH new_name) +(** [intro_temp] behaves like [intro_anon] but registers the id of the + introduced assumption for a regeneralization. *) +let intro_anon_temp = + Ssrcommon.tclINTRO ~id:Ssrcommon.Anon + ~conclusion:(fun ~orig_name ~new_name -> + isGEN_PUSH { tmp_id = new_name; orig_name }) + (** [intro_end] performs the actions that have been delayed. *) let intro_end = - Ssrcommon.tcl0G (isCLR_CONSUME) + Ssrcommon.tcl0G ~default:() (isCLR_CONSUME <*> isGEN_CONSUME) (** [=> _] *****************************************************************) let intro_clear ids = @@ -138,6 +239,27 @@ let tacCHECK_HYPS_EXIST hyps = Goal.enter begin fun gl -> end (** [=> []] *****************************************************************) + +(* calls t1 then t2 on each subgoal passing to t2 the index of the current + * subgoal (starting from 0) as well as the number of subgoals *) +let tclTHENin t1 t2 = + tclUNIT () >>= begin fun () -> let i = ref (-1) in + t1 <*> numgoals >>= fun n -> + Goal.enter begin fun g -> incr i; t2 !i n end +end + +(* Attaches one element of `seeds` to each of the last k goals generated by +`tac`, where k is the size of `seeds` *) +let tclSEED_SUBGOALS seeds tac = + tclTHENin tac (fun i n -> + Ssrprinters.ppdebug (lazy Pp.(str"seeding")); + (* eg [case: (H _ : nat)] generates 3 goals: + - 1 for _ + - 2 for the nat constructors *) + let extra_goals = n - Array.length seeds in + if i < extra_goals then tclUNIT () + else isNSEED_SET seeds.(i - extra_goals)) + let tac_case t = Goal.enter begin fun _ -> Ssrcommon.tacTYPEOF t >>= fun ty -> @@ -145,10 +267,36 @@ let tac_case t = if is_inj then V82.tactic ~nf_evars:false (Ssrelim.perform_injection t) else - Ssrelim.ssrscasetac t + Goal.enter begin fun g -> + (Ssrelim.casetac t (fun ?seed k -> + match seed with + | None -> k + | Some seed -> tclSEED_SUBGOALS seed k)) + end end -(***[=> [: id]] ************************************************************) +(** [=> [^ seed ]] *********************************************************) +let tac_intro_seed interp_ipats fix = Goal.enter begin fun gl -> + isNSEED_CONSUME begin fun seeds -> + let seeds = + Ssrcommon.option_assert_get seeds Pp.(str"tac_intro_seed: no seed") in + let ipats = List.map (function + | Anonymous -> + let s = match fix with + | Prefix id -> Id.to_string id ^ "?" + | SuffixNum n -> "?" ^ string_of_int n + | SuffixId id -> "?" ^ Id.to_string id in + IPatAnon (One (Some s)) + | Name id -> + let s = match fix with + | Prefix fix -> Id.to_string fix ^ Id.to_string id + | SuffixNum n -> Id.to_string id ^ string_of_int n + | SuffixId fix -> Id.to_string id ^ Id.to_string fix in + IPatId (None, Id.of_string s)) seeds in + interp_ipats ipats +end end + +(*** [=> [: id]] ************************************************************) [@@@ocaml.warning "-3"] let mk_abstract_id = let open Coqlib in @@ -205,95 +353,112 @@ let tclLOG p t = end <*> t p - <*> + >>= fun ret -> Goal.enter begin fun g -> Ssrprinters.ppdebug (lazy Pp.(str "done: " ++ isPRINT g)); tclUNIT () end + >>= fun () -> tclUNIT ret -let rec ipat_tac1 ipat : unit tactic = +let notTAC = tclUNIT false + +(* returns true if it was a tactic (eg /ltac:tactic) *) +let rec ipat_tac1 ipat : bool tactic = match ipat with | IPatView (clear_if_id,l) -> - Ssrview.tclIPAT_VIEWS ~views:l ~clear_if_id + Ssrview.tclIPAT_VIEWS + ~views:l ~clear_if_id ~conclusion:(fun ~to_clear:clr -> intro_clear clr) - | IPatDispatch(true,[[]]) -> - tclUNIT () - | IPatDispatch(_,ipatss) -> - tclDISPATCH (List.map ipat_tac ipatss) + | IPatDispatch(true, Regular [[]]) -> + notTAC + | IPatDispatch(_, Regular ipatss) -> + tclDISPATCH (List.map ipat_tac ipatss) <*> notTAC + | IPatDispatch(_,Block id_block) -> + tac_intro_seed ipat_tac id_block <*> notTAC + + | IPatId (None, id) -> Ssrcommon.tclINTRO_ID id <*> notTAC + | IPatId (Some Dependent, id) -> + intro_anon_deps <*> Ssrcommon.tclINTRO_ID id <*> notTAC - | IPatId id -> Ssrcommon.tclINTRO_ID id + | IPatCase (Block id_block) -> + Ssrcommon.tclWITHTOP tac_case <*> tac_intro_seed ipat_tac id_block <*> notTAC - | IPatCase ipatss -> - tclIORPAT (Ssrcommon.tclWITHTOP tac_case) ipatss + | IPatCase (Regular ipatss) -> + tclIORPAT (Ssrcommon.tclWITHTOP tac_case) ipatss <*> notTAC | IPatInj ipatss -> tclIORPAT (Ssrcommon.tclWITHTOP (fun t -> V82.tactic ~nf_evars:false (Ssrelim.perform_injection t))) ipatss + <*> notTAC - | IPatAnon Drop -> intro_drop - | IPatAnon One -> Ssrcommon.tclINTRO_ANON - | IPatAnon All -> intro_anon_all + | IPatAnon Drop -> intro_drop <*> notTAC + | IPatAnon (One seed) -> Ssrcommon.tclINTRO_ANON ?seed () <*> notTAC + | IPatAnon All -> intro_anon_all <*> notTAC + | IPatAnon Temporary -> intro_anon_temp <*> notTAC - | IPatNoop -> tclUNIT () - | IPatSimpl Nop -> tclUNIT () + | IPatNoop -> notTAC + | IPatSimpl Nop -> notTAC | IPatClear ids -> tacCHECK_HYPS_EXIST ids <*> - intro_clear (List.map Ssrcommon.hyp_id ids) + intro_clear (List.map Ssrcommon.hyp_id ids) <*> + notTAC - | IPatSimpl (Simpl n) -> - V82.tactic ~nf_evars:false (Ssrequality.simpltac (Simpl n)) - | IPatSimpl (Cut n) -> - V82.tactic ~nf_evars:false (Ssrequality.simpltac (Cut n)) - | IPatSimpl (SimplCut (n,m)) -> - V82.tactic ~nf_evars:false (Ssrequality.simpltac (SimplCut (n,m))) + | IPatSimpl x -> + V82.tactic ~nf_evars:false (Ssrequality.simpltac x) <*> notTAC | IPatRewrite (occ,dir) -> Ssrcommon.tclWITHTOP - (fun x -> V82.tactic ~nf_evars:false (Ssrequality.ipat_rewrite occ dir x)) + (fun x -> V82.tactic ~nf_evars:false (Ssrequality.ipat_rewrite occ dir x)) <*> notTAC - | IPatAbstractVars ids -> tclMK_ABSTRACT_VARS ids + | IPatAbstractVars ids -> tclMK_ABSTRACT_VARS ids <*> notTAC - | IPatTac t -> t + | IPatEqGen t -> t <*> notTAC and ipat_tac pl : unit tactic = match pl with | [] -> tclUNIT () | pat :: pl -> - Ssrcommon.tcl0G (tclLOG pat ipat_tac1) <*> - isTICK pat <*> - ipat_tac pl + Ssrcommon.tcl0G ~default:false (tclLOG pat ipat_tac1) >>= fun was_tac -> + isTICK pat (* drops expired seeds *) >>= fun () -> + if was_tac then (* exception *) + let ip_before, case, ip_after = split_at_first_case pl in + let case = ssr_exception true case in + let case = option_to_list case in + ipat_tac (ip_before @ case @ ip_after) + else ipat_tac pl and tclIORPAT tac = function | [[]] -> tac | p -> Tacticals.New.tclTHENS tac (List.map ipat_tac p) -let split_at_first_case ipats = +and ssr_exception is_on = function + | Some (IPatCase l) when is_on -> Some (IPatDispatch(true, l)) + | x -> x + +and option_to_list = function None -> [] | Some x -> [x] + +and split_at_first_case ipats = let rec loop acc = function | (IPatSimpl _ | IPatClear _) as x :: rest -> loop (x :: acc) rest - | IPatCase _ as x :: xs -> CList.rev acc, Some x, xs + | (IPatCase _ | IPatDispatch _) as x :: xs -> CList.rev acc, Some x, xs | pats -> CList.rev acc, None, pats in loop [] ipats - -let ssr_exception is_on = function - | Some (IPatCase l) when is_on -> Some (IPatDispatch(true, l)) - | x -> x - -let option_to_list = function None -> [] | Some x -> [x] +;; (* Simple pass doing {x}/v -> /v{x} *) let elaborate_ipats l = let rec elab = function | [] -> [] | (IPatClear _ as p1) :: (IPatView _ as p2) :: rest -> p2 :: p1 :: elab rest - | IPatDispatch(s,p) :: rest -> IPatDispatch (s,List.map elab p) :: elab rest - | IPatCase p :: rest -> IPatCase (List.map elab p) :: elab rest + | IPatDispatch(s, Regular p) :: rest -> IPatDispatch (s, Regular (List.map elab p)) :: elab rest + | IPatCase (Regular p) :: rest -> IPatCase (Regular (List.map elab p)) :: elab rest | IPatInj p :: rest -> IPatInj (List.map elab p) :: elab rest - | (IPatTac _ | IPatId _ | IPatSimpl _ | IPatClear _ | + | (IPatEqGen _ | IPatId _ | IPatSimpl _ | IPatClear _ | IPatAnon _ | IPatView _ | IPatNoop | IPatRewrite _ | - IPatAbstractVars _) as x :: rest -> x :: elab rest + IPatAbstractVars _ | IPatDispatch(_, Block _) | IPatCase(Block _)) as x :: rest -> x :: elab rest in elab l @@ -302,8 +467,8 @@ let main ?eqtac ~first_case_is_dispatch ipats = let ip_before, case, ip_after = split_at_first_case ipats in let case = ssr_exception first_case_is_dispatch case in let case = option_to_list case in - let eqtac = option_to_list (Option.map (fun x -> IPatTac x) eqtac) in - Ssrcommon.tcl0G (ipat_tac (ip_before @ case @ eqtac @ ip_after) <*> intro_end) + let eqtac = option_to_list (Option.map (fun x -> IPatEqGen x) eqtac) in + Ssrcommon.tcl0G ~default:() (ipat_tac (ip_before @ case @ eqtac @ ip_after) <*> intro_end) end (* }}} *) @@ -344,10 +509,11 @@ let mkCoqRefl t c env sigma = (** Intro patterns processing for elim tactic, in particular when used in conjunction with equation generation as in [elim E: x] *) -let elim_intro_tac ipats ?ist what eqid ssrelim is_rec clr = +let elim_intro_tac ipats ?seed what eqid ssrelim is_rec clr = let intro_eq = match eqid with - | Some (IPatId ipat) when not is_rec -> + | Some (IPatId (Some _, _)) -> assert false (* parser *) + | Some (IPatId (None,ipat)) when not is_rec -> let rec intro_eq () = Goal.enter begin fun g -> let sigma, env, concl = Goal.(sigma g, env g, concl g) in match EConstr.kind_of_type sigma concl with @@ -356,12 +522,12 @@ let elim_intro_tac ipats ?ist what eqid ssrelim is_rec clr = | Term.AtomicType (hd, _) when Ssrcommon.is_protect hd env sigma -> V82.tactic ~nf_evars:false Ssrcommon.unprotecttac <*> Ssrcommon.tclINTRO_ID ipat - | _ -> Ssrcommon.tclINTRO_ANON <*> intro_eq () + | _ -> Ssrcommon.tclINTRO_ANON () <*> intro_eq () end |_ -> Ssrcommon.errorstrm (Pp.str "Too many names in intro pattern") end in intro_eq () - | Some (IPatId ipat) -> + | Some (IPatId (None,ipat)) -> let intro_lhs = Goal.enter begin fun g -> let sigma = Goal.sigma g in let elim_name = match clr, what with @@ -369,12 +535,9 @@ let elim_intro_tac ipats ?ist what eqid ssrelim is_rec clr = | _, `EConstr(_,_,t) when EConstr.isVar sigma t -> EConstr.destVar sigma t | _ -> Ssrcommon.mk_anon_id "K" (Tacmach.New.pf_ids_of_hyps g) in - let elim_name = - if Ssrcommon.is_name_in_ipats elim_name ipats then - Ssrcommon.mk_anon_id "K" (Tacmach.New.pf_ids_of_hyps g) - else elim_name - in - Ssrcommon.tclINTRO_ID elim_name + Tacticals.New.tclFIRST + [ Ssrcommon.tclINTRO_ID elim_name + ; Ssrcommon.tclINTRO_ANON ~seed:"K" ()] end in let rec gen_eq_tac () = Goal.enter begin fun g -> let sigma, env, concl = Goal.(sigma g, env g, concl g) in @@ -389,7 +552,7 @@ let elim_intro_tac ipats ?ist what eqid ssrelim is_rec clr = | _ -> assert false in let case = args.(Array.length args-1) in if not(EConstr.Vars.closed0 sigma case) - then Ssrcommon.tclINTRO_ANON <*> gen_eq_tac () + then Ssrcommon.tclINTRO_ANON () <*> gen_eq_tac () else Ssrcommon.tacTYPEOF case >>= fun case_ty -> let open EConstr in @@ -407,13 +570,14 @@ let elim_intro_tac ipats ?ist what eqid ssrelim is_rec clr = intro_lhs <*> Ssrcommon.tclINTRO_ID ipat | _ -> tclUNIT () in - let unprot = + let unprotect = if eqid <> None && is_rec then V82.tactic ~nf_evars:false Ssrcommon.unprotecttac else tclUNIT () in - V82.of_tactic begin - V82.tactic ~nf_evars:false ssrelim <*> - tclIPAT_EQ (intro_eq <*> unprot) ipats - end + begin match seed with + | None -> ssrelim + | Some s -> IpatMachine.tclSEED_SUBGOALS s ssrelim end <*> + tclIPAT_EQ (intro_eq <*> unprotect) ipats +;; let mkEq dir cl c t n env sigma = let open EConstr in @@ -506,13 +670,11 @@ let ssrelimtac (view, (eqid, (dgens, ipats))) = | [v] -> Ssrcommon.tclINTERP_AST_CLOSURE_TERM_AS_CONSTR v >>= fun cs -> tclDISPATCH (List.map (fun elim -> - V82.tactic ~nf_evars:false (Ssrelim.ssrelim deps (`EGen gen) ~elim eqid (elim_intro_tac ipats))) cs) | [] -> tclINDEPENDENT - (V82.tactic ~nf_evars:false - (Ssrelim.ssrelim deps (`EGen gen) eqid (elim_intro_tac ipats))) + (Ssrelim.ssrelim deps (`EGen gen) eqid (elim_intro_tac ipats)) | _ -> Ssrcommon.errorstrm Pp.(str "elim: only one elimination lemma can be provided") @@ -535,9 +697,8 @@ let ssrcasetac (view, (eqid, (dgens, ipats))) = if view <> [] && eqid <> None && deps = [] then [gen], [], None else deps, clear, occ in - V82.tactic ~nf_evars:false - (Ssrelim.ssrelim ~is_case:true deps (`EConstr (clear, occ, vc)) - eqid (elim_intro_tac ipats)) + Ssrelim.ssrelim ~is_case:true deps (`EConstr (clear, occ, vc)) + eqid (elim_intro_tac ipats) in if view = [] then conclusion false c clear c else tacVIEW_THEN_GRAB ~simple_types:false view ~conclusion info) @@ -556,18 +717,16 @@ let pushmoveeqtac cl c = Goal.enter begin fun g -> Tactics.apply_type ~typecheck:true (EConstr.mkProd (x, t, cl2)) [c; eqc] end -let eqmovetac _ gen = Goal.enter begin fun g -> - Ssrcommon.tacSIGMA >>= fun gl -> - let cl, c, _, gl = Ssrcommon.pf_interp_gen gl false gen in - Unsafe.tclEVARS (Tacmach.project gl) <*> - pushmoveeqtac cl c -end +let eqmovetac _ gen = + Ssrcommon.pfLIFT (Ssrcommon.pf_interp_gen false gen) >>= + fun (cl, c, _) -> pushmoveeqtac cl c +;; let rec eqmoveipats eqpat = function | (IPatSimpl _ | IPatClear _ as ipat) :: ipats -> ipat :: eqmoveipats eqpat ipats | (IPatAnon All :: _ | []) as ipats -> - IPatAnon One :: eqpat :: ipats + IPatAnon (One None) :: eqpat :: ipats | ipat :: ipats -> ipat :: eqpat :: ipats @@ -700,8 +859,8 @@ let ssrabstract dgens = let open Ssrmatching in let ipats = List.map (fun (_,cp) -> match id_of_pattern (interp_cpattern gl0 cp None) with - | None -> IPatAnon One - | Some id -> IPatId id) + | None -> IPatAnon (One None) + | Some id -> IPatId (None,id)) (List.tl gens) in conclusion ipats end in diff --git a/plugins/ssr/ssrparser.mlg b/plugins/ssr/ssrparser.mlg index c9221ef758..6938bbc9f6 100644 --- a/plugins/ssr/ssrparser.mlg +++ b/plugins/ssr/ssrparser.mlg @@ -605,18 +605,18 @@ let remove_loc x = x.CAst.v let ipat_of_intro_pattern p = Tactypes.( let rec ipat_of_intro_pattern = function - | IntroNaming (IntroIdentifier id) -> IPatId id + | IntroNaming (IntroIdentifier id) -> IPatId (None,id) | IntroAction IntroWildcard -> IPatAnon Drop | IntroAction (IntroOrAndPattern (IntroOrPattern iorpat)) -> - IPatCase - (List.map (List.map ipat_of_intro_pattern) - (List.map (List.map remove_loc) iorpat)) + IPatCase (Regular( + List.map (List.map ipat_of_intro_pattern) + (List.map (List.map remove_loc) iorpat))) | IntroAction (IntroOrAndPattern (IntroAndPattern iandpat)) -> IPatCase - [List.map ipat_of_intro_pattern (List.map remove_loc iandpat)] - | IntroNaming IntroAnonymous -> IPatAnon One + (Regular [List.map ipat_of_intro_pattern (List.map remove_loc iandpat)]) + | IntroNaming IntroAnonymous -> IPatAnon (One None) | IntroAction (IntroRewrite b) -> IPatRewrite (allocc, if b then L2R else R2L) - | IntroNaming (IntroFresh id) -> IPatAnon One + | IntroNaming (IntroFresh id) -> IPatAnon (One None) | IntroAction (IntroApplyOn _) -> (* to do *) CErrors.user_err (Pp.str "TO DO") | IntroAction (IntroInjection ips) -> IPatInj [List.map ipat_of_intro_pattern (List.map remove_loc ips)] @@ -630,14 +630,20 @@ let ipat_of_intro_pattern p = Tactypes.( let rec map_ipat map_id map_ssrhyp map_ast_closure_term = function | (IPatSimpl _ | IPatAnon _ | IPatRewrite _ | IPatNoop) as x -> x - | IPatId id -> IPatId (map_id id) + | IPatId (m,id) -> IPatId (m,map_id id) | IPatAbstractVars l -> IPatAbstractVars (List.map map_id l) | IPatClear clr -> IPatClear (List.map map_ssrhyp clr) - | IPatCase iorpat -> IPatCase (List.map (List.map (map_ipat map_id map_ssrhyp map_ast_closure_term)) iorpat) - | IPatDispatch (s,iorpat) -> IPatDispatch (s,List.map (List.map (map_ipat map_id map_ssrhyp map_ast_closure_term)) iorpat) + | IPatCase (Regular iorpat) -> IPatCase (Regular (List.map (List.map (map_ipat map_id map_ssrhyp map_ast_closure_term)) iorpat)) + | IPatCase (Block(hat)) -> IPatCase (Block(map_block map_id hat)) + | IPatDispatch (s, Regular iorpat) -> IPatDispatch (s, Regular (List.map (List.map (map_ipat map_id map_ssrhyp map_ast_closure_term)) iorpat)) + | IPatDispatch (s, Block (hat)) -> IPatDispatch (s, Block(map_block map_id hat)) | IPatInj iorpat -> IPatInj (List.map (List.map (map_ipat map_id map_ssrhyp map_ast_closure_term)) iorpat) | IPatView (clr,v) -> IPatView (clr,List.map map_ast_closure_term v) - | IPatTac _ -> assert false (*internal usage only *) + | IPatEqGen _ -> assert false (*internal usage only *) +and map_block map_id = function + | Prefix id -> Prefix (map_id id) + | SuffixId id -> SuffixId (map_id id) + | SuffixNum _ as x -> x type ssripatrep = ssripat let wit_ssripatrep = add_genarg "ssripatrep" pr_ipat @@ -688,8 +694,20 @@ let rec add_intro_pattern_hyps ipat hyps = * we have no clue what a name could be bound to (maybe another ipat) *) let interp_ipat ist gl = let ltacvar id = Id.Map.mem id ist.Tacinterp.lfun in + let interp_block = function + | Prefix id when ltacvar id -> + begin match interp_introid ist gl id with + | IntroNaming (IntroIdentifier id) -> Prefix id + | _ -> Ssrcommon.errorstrm Pp.(str"Variable " ++ Id.print id ++ str" in block intro pattern should be bound to an identifier.") + end + | SuffixId id when ltacvar id -> + begin match interp_introid ist gl id with + | IntroNaming (IntroIdentifier id) -> SuffixId id + | _ -> Ssrcommon.errorstrm Pp.(str"Variable " ++ Id.print id ++ str" in block intro pattern should be bound to an identifier.") + end + | x -> x in let rec interp = function - | IPatId id when ltacvar id -> + | IPatId(_, id) when ltacvar id -> ipat_of_intro_pattern (interp_introid ist gl id) | IPatId _ as x -> x | IPatClear clr -> @@ -698,17 +716,21 @@ let interp_ipat ist gl = add_intro_pattern_hyps CAst.(make ?loc (interp_introid ist gl id)) hyps in let clr' = List.fold_right add_hyps clr [] in check_hyps_uniq [] clr'; IPatClear clr' - | IPatCase(iorpat) -> - IPatCase(List.map (List.map interp) iorpat) - | IPatDispatch(s,iorpat) -> - IPatDispatch(s,List.map (List.map interp) iorpat) + | IPatCase(Regular iorpat) -> + IPatCase(Regular(List.map (List.map interp) iorpat)) + | IPatCase(Block(hat)) -> IPatCase(Block(interp_block hat)) + + | IPatDispatch(s,Regular iorpat) -> + IPatDispatch(s,Regular (List.map (List.map interp) iorpat)) + | IPatDispatch(s,Block(hat)) -> IPatDispatch(s,Block(interp_block hat)) + | IPatInj iorpat -> IPatInj (List.map (List.map interp) iorpat) | IPatAbstractVars l -> IPatAbstractVars (List.map get_intro_id (List.map (interp_introid ist gl) l)) | IPatView (clr,l) -> IPatView (clr,List.map (fun x -> snd(interp_ast_closure_term ist gl x)) l) | (IPatSimpl _ | IPatAnon _ | IPatRewrite _ | IPatNoop) as x -> x - | IPatTac _ -> assert false (*internal usage only *) + | IPatEqGen _ -> assert false (*internal usage only *) in interp @@ -729,19 +751,11 @@ ARGUMENT EXTEND ssripat TYPED AS ssripatrep list PRINTED BY { pr_ssripats } GLOBALIZED BY { intern_ipats } | [ "_" ] -> { [IPatAnon Drop] } | [ "*" ] -> { [IPatAnon All] } - (* - | [ "^" "*" ] -> { [IPatFastMode] } - | [ "^" "_" ] -> { [IPatSeed `Wild] } - | [ "^_" ] -> { [IPatSeed `Wild] } - | [ "^" "?" ] -> { [IPatSeed `Anon] } - | [ "^?" ] -> { [IPatSeed `Anon] } - | [ "^" ident(id) ] -> { [IPatSeed (`Id(id,`Pre))] } - | [ "^" "~" ident(id) ] -> { [IPatSeed (`Id(id,`Post))] } - | [ "^~" ident(id) ] -> { [IPatSeed (`Id(id,`Post))] } - *) - | [ ident(id) ] -> { [IPatId id] } - | [ "?" ] -> { [IPatAnon One] } -(* TODO | [ "+" ] -> [ [IPatAnon Temporary] ] *) + | [ ">" ident(id) ] -> { [IPatId(Some Dependent,id)] } + | [ ident(id) ] -> { [IPatId (None,id)] } + | [ "?" ] -> { [IPatAnon (One None)] } + | [ "+" ] -> { [IPatAnon Temporary] } + | [ "++" ] -> { [IPatAnon Temporary; IPatAnon Temporary] } | [ ssrsimpl_ne(sim) ] -> { [IPatSimpl sim] } | [ ssrdocc(occ) "->" ] -> { match occ with | Some [], _ -> CErrors.user_err ~loc (str"occ_switch expected") @@ -805,28 +819,42 @@ let reject_ssrhid strm = let test_nohidden = Pcoq.Entry.of_parser "test_ssrhid" reject_ssrhid +let rec reject_binder crossed_paren k s = + match + try Some (Util.stream_nth k s) + with Stream.Failure -> None + with + | Some (Tok.KEYWORD "(") when not crossed_paren -> reject_binder true (k+1) s + | Some (Tok.IDENT _) when crossed_paren -> reject_binder true (k+1) s + | Some (Tok.KEYWORD ":" | Tok.KEYWORD ":=") when crossed_paren -> + raise Stream.Failure + | Some (Tok.KEYWORD ")") when crossed_paren -> raise Stream.Failure + | _ -> if crossed_paren then () else raise Stream.Failure + +let _test_nobinder = Pcoq.Entry.of_parser "test_nobinder" (reject_binder false 0) + } ARGUMENT EXTEND ssrcpat TYPED AS ssripatrep PRINTED BY { pr_ssripat } - | [ "YouShouldNotTypeThis" ssriorpat(x) ] -> { IPatCase(x) } + | [ "YouShouldNotTypeThis" ssriorpat(x) ] -> { IPatCase(Regular x) } END (* Pcoq *) GRAMMAR EXTEND Gram GLOBAL: ssrcpat; + hat: [ + [ "^"; id = ident -> { Prefix id } + | "^"; "~"; id = ident -> { SuffixId id } + | "^"; "~"; n = natural -> { SuffixNum n } + | "^~"; id = ident -> { SuffixId id } + | "^~"; n = natural -> { SuffixNum n } + ]]; ssrcpat: [ - [ test_nohidden; "["; iorpat = ssriorpat; "]" -> { -(* check_no_inner_seed !@loc false iorpat; - IPatCase (understand_case_type iorpat) *) - IPatCase iorpat } -(* - | test_nohidden; "("; iorpat = ssriorpat; ")" -> -(* check_no_inner_seed !@loc false iorpat; - IPatCase (understand_case_type iorpat) *) - IPatDispatch iorpat -*) + [ test_nohidden; "["; hat_id = hat; "]" -> { + IPatCase (Block(hat_id)) } + | test_nohidden; "["; iorpat = ssriorpat; "]" -> { + IPatCase (Regular iorpat) } | test_nohidden; "[="; iorpat = ssriorpat; "]" -> { -(* check_no_inner_seed !@loc false iorpat; *) IPatInj iorpat } ]]; END @@ -1464,7 +1492,7 @@ END { let intro_id_to_binder = List.map (function - | IPatId id -> + | IPatId (None,id) -> let { CAst.loc=xloc } as x = bvar_lname (mkCVar id) in (FwdPose, [BFvar]), CAst.make @@ CLambdaN ([CLocalAssum([x], Default Explicit, mkCHole xloc)], @@ -1474,9 +1502,9 @@ let intro_id_to_binder = List.map (function let binder_to_intro_id = CAst.(List.map (function | (FwdPose, [BFvar]), { v = CLambdaN ([CLocalAssum(ids,_,_)],_) } | (FwdPose, [BFdecl _]), { v = CLambdaN ([CLocalAssum(ids,_,_)],_) } -> - List.map (function {v=Name id} -> IPatId id | _ -> IPatAnon One) ids - | (FwdPose, [BFdef]), { v = CLetIn ({v=Name id},_,_,_) } -> [IPatId id] - | (FwdPose, [BFdef]), { v = CLetIn ({v=Anonymous},_,_,_) } -> [IPatAnon One] + List.map (function {v=Name id} -> IPatId (None,id) | _ -> IPatAnon (One None)) ids + | (FwdPose, [BFdef]), { v = CLetIn ({v=Name id},_,_,_) } -> [IPatId (None,id)] + | (FwdPose, [BFdef]), { v = CLetIn ({v=Anonymous},_,_,_) } -> [IPatAnon (One None)] | _ -> anomaly "ssrbinder is not a binder")) let pr_ssrhavefwdwbinders _ _ prt (tr,((hpats, (fwd, hint)))) = @@ -1966,9 +1994,10 @@ let test_ssreqid = Pcoq.Entry.of_parser "test_ssreqid" accept_ssreqid GRAMMAR EXTEND Gram GLOBAL: ssreqid; ssreqpat: [ - [ id = Prim.ident -> { IPatId id } + [ id = Prim.ident -> { IPatId (None,id) } | "_" -> { IPatAnon Drop } - | "?" -> { IPatAnon One } + | "?" -> { IPatAnon (One None) } + | "+" -> { IPatAnon Temporary } | occ = ssrdocc; "->" -> { match occ with | None, occ -> IPatRewrite (occ, L2R) | _ -> CErrors.user_err ~loc (str"Only occurrences are allowed here") } diff --git a/plugins/ssr/ssrprinters.ml b/plugins/ssr/ssrprinters.ml index 8bf4816e99..6ccefa1cab 100644 --- a/plugins/ssr/ssrprinters.ml +++ b/plugins/ssr/ssrprinters.ml @@ -97,24 +97,30 @@ let pr_view2 = pr_list mt (fun c -> str "/" ++ pr_ast_closure_term c) let rec pr_ipat p = match p with - | IPatId id -> Id.print id + | IPatId (None,id) -> Id.print id + | IPatId (Some Dependent,id) -> str">" ++ Id.print id | IPatSimpl sim -> pr_simpl sim | IPatClear clr -> pr_clear mt clr - | IPatCase iorpat -> hov 1 (str "[" ++ pr_iorpat iorpat ++ str "]") - | IPatDispatch(_,iorpat) -> hov 1 (str "/[" ++ pr_iorpat iorpat ++ str "]") + | IPatCase (Regular iorpat) -> hov 1 (str "[" ++ pr_iorpat iorpat ++ str "]") + | IPatCase (Block m) -> hov 1 (str"[" ++ pr_block m ++ str"]") + | IPatDispatch(_,Regular iorpat) -> hov 1 (str "(" ++ pr_iorpat iorpat ++ str ")") + | IPatDispatch (_,Block m) -> hov 1 (str"(" ++ pr_block m ++ str")") | IPatInj iorpat -> hov 1 (str "[=" ++ pr_iorpat iorpat ++ str "]") | IPatRewrite (occ, dir) -> pr_occ occ ++ pr_dir dir | IPatAnon All -> str "*" | IPatAnon Drop -> str "_" - | IPatAnon One -> str "?" + | IPatAnon (One _) -> str "?" | IPatView (false,v) -> pr_view2 v | IPatView (true,v) -> str"{}" ++ pr_view2 v + | IPatAnon Temporary -> str "+" | IPatNoop -> str "-" | IPatAbstractVars l -> str "[:" ++ pr_list spc Id.print l ++ str "]" - | IPatTac _ -> str "<tac>" -(* TODO | IPatAnon Temporary -> str "+" *) + | IPatEqGen _ -> str "<tac>" and pr_ipats ipats = pr_list spc pr_ipat ipats and pr_iorpat iorpat = pr_list pr_bar pr_ipats iorpat +and pr_block = function (Prefix id) -> str"^" ++ Id.print id + | (SuffixId id) -> str"^~" ++ Id.print id + | (SuffixNum n) -> str"^~" ++ int n (* 0 cost pp function. Active only if Debug Ssreflect is Set *) let ppdebug_ref = ref (fun _ -> ()) diff --git a/plugins/ssr/ssrview.ml b/plugins/ssr/ssrview.ml index 1aa64d7141..4816027296 100644 --- a/plugins/ssr/ssrview.ml +++ b/plugins/ssr/ssrview.ml @@ -59,18 +59,23 @@ end (* Forward View application code *****************************************) +let reduce_or l = tclUNIT (List.fold_left (||) false l) + module State : sig (* View storage API *) - val vsINIT : EConstr.t * Id.t list -> unit tactic + val vsINIT : view:EConstr.t -> subject_name:Id.t list -> to_clear:Id.t list -> unit tactic val vsPUSH : (EConstr.t -> (EConstr.t * Id.t list) tactic) -> unit tactic - val vsCONSUME : (name:Id.t option -> EConstr.t -> to_clear:Id.t list -> unit tactic) -> unit tactic + val vsCONSUME : (names:Id.t list -> EConstr.t -> to_clear:Id.t list -> unit tactic) -> unit tactic + + (* The bool is the || of the bool returned by the continuations *) + val vsCONSUME_IF_PRESENT : (names:Id.t list -> EConstr.t option -> to_clear:Id.t list -> bool tactic) -> bool tactic val vsASSERT_EMPTY : unit tactic end = struct (* {{{ *) type vstate = { - subject_name : Id.t option; (* top *) + subject_name : Id.t list; (* top *) (* None if views are being applied to a term *) view : EConstr.t; (* v2 (v1 top) *) to_clear : Id.t list; @@ -81,34 +86,43 @@ include Ssrcommon.MakeState(struct let init = None end) -let vsINIT (view, to_clear) = - tclSET (Some { subject_name = None; view; to_clear }) +let vsINIT ~view ~subject_name ~to_clear = + tclSET (Some { subject_name; view; to_clear }) + +(** Initializes the state in which view data is accumulated when views are +applied to the first assumption in the goal *) +let vsBOOTSTRAP = Goal.enter_one ~__LOC__ begin fun gl -> + let concl = Goal.concl gl in + let id = (* We keep the orig name for checks in "in" tcl *) + match EConstr.kind_of_type (Goal.sigma gl) concl with + | Term.ProdType(Name.Name id, _, _) + when Ssrcommon.is_discharged_id id -> id + | _ -> mk_anon_id "view_subject" (Tacmach.New.pf_ids_of_hyps gl) in + let view = EConstr.mkVar id in + Ssrcommon.tclINTRO_ID id <*> + tclSET (Some { subject_name = [id]; view; to_clear = [] }) +end -let vsPUSH k = - tacUPDATE (fun s -> match s with +let rec vsPUSH k = + tclINDEPENDENT (tclGET (function | Some { subject_name; view; to_clear } -> k view >>= fun (view, clr) -> - tclUNIT (Some { subject_name; view; to_clear = to_clear @ clr }) - | None -> - Goal.enter_one ~__LOC__ begin fun gl -> - let concl = Goal.concl gl in - let id = (* We keep the orig name for checks in "in" tcl *) - match EConstr.kind_of_type (Goal.sigma gl) concl with - | Term.ProdType(Name.Name id, _, _) - when Ssrcommon.is_discharged_id id -> id - | _ -> mk_anon_id "view_subject" (Tacmach.New.pf_ids_of_hyps gl) in - let view = EConstr.mkVar id in - Ssrcommon.tclINTRO_ID id <*> - k view >>= fun (view, to_clear) -> - tclUNIT (Some { subject_name = Some id; view; to_clear }) - end) - -let vsCONSUME k = - tclGET (fun s -> match s with + tclSET (Some { subject_name; view; to_clear = to_clear @ clr }) + | None -> vsBOOTSTRAP <*> vsPUSH k)) + +let rec vsCONSUME k = + tclINDEPENDENT (tclGET (function | Some { subject_name; view; to_clear } -> tclSET None <*> - k ~name:subject_name view ~to_clear - | None -> anomaly "vsCONSUME: empty storage") + k ~names:subject_name view ~to_clear + | None -> vsBOOTSTRAP <*> vsCONSUME k)) + +let vsCONSUME_IF_PRESENT k = + tclINDEPENDENTL (tclGET1 (function + | Some { subject_name; view; to_clear } -> + tclSET None <*> + k ~names:subject_name (Some view) ~to_clear + | None -> k ~names:[] None ~to_clear:[])) >>= reduce_or let vsASSERT_EMPTY = tclGET (function @@ -128,13 +142,19 @@ let intern_constr_expr { Genintern.genv; ltacvars = vars } sigma ce = To allow for t being a notation, like "Notation foo x := ltac:(foo x)", we need to internalize t. *) -let is_tac_in_term { body; glob_env; interp_env } = +let is_tac_in_term ?extra_scope { body; glob_env; interp_env } = Goal.(enter_one ~__LOC__ begin fun goal -> let genv = env goal in let sigma = sigma goal in let ist = Ssrcommon.option_assert_get glob_env (Pp.str"not a term") in (* We use the env of the goal, not the global one *) let ist = { ist with Genintern.genv } in + (* We open extra_scope *) + let body = + match extra_scope with + | None -> body + | Some s -> CAst.make (Constrexpr.CDelimiters(s,body)) + in (* We unravel notations *) let g = intern_constr_expr ist sigma body in match DAst.get g with @@ -300,51 +320,83 @@ end let pose_proof subject_name p = Tactics.generalize [p] <*> - Option.cata - (fun id -> Ssrcommon.tclRENAME_HD_PROD (Name.Name id)) (tclUNIT()) - subject_name + begin match subject_name with + | id :: _ -> Ssrcommon.tclRENAME_HD_PROD (Name.Name id) + | _ -> tclUNIT() end <*> Tactics.New.reduce_after_refine -let rec apply_all_views ~clear_if_id ending vs s0 = +(* returns true if the last item was a tactic *) +let rec apply_all_views_aux ~clear_if_id vs finalization conclusion s0 = match vs with - | [] -> ending s0 + | [] -> finalization s0 (fun name p -> + (match p with + | None -> conclusion ~to_clear:[] + | Some p -> + pose_proof name p <*> conclusion ~to_clear:name) <*> + tclUNIT false) | v :: vs -> Ssrprinters.ppdebug (lazy Pp.(str"piling...")); - is_tac_in_term v >>= function - | `Tac tac -> - Ssrprinters.ppdebug (lazy Pp.(str"..a tactic")); - ending s0 <*> Tacinterp.eval_tactic tac <*> - Ssrcommon.tacSIGMA >>= apply_all_views ~clear_if_id ending vs + is_tac_in_term ~extra_scope:"ssripat" v >>= function | `Term v -> Ssrprinters.ppdebug (lazy Pp.(str"..a term")); pile_up_view ~clear_if_id v <*> - apply_all_views ~clear_if_id ending vs s0 + apply_all_views_aux ~clear_if_id vs finalization conclusion s0 + | `Tac tac -> + Ssrprinters.ppdebug (lazy Pp.(str"..a tactic")); + finalization s0 (fun name p -> + (match p with + | None -> tclUNIT () + | Some p -> pose_proof name p) <*> + Tacinterp.eval_tactic tac <*> + if vs = [] then begin + Ssrprinters.ppdebug (lazy Pp.(str"..was the last view")); + conclusion ~to_clear:name <*> tclUNIT true + end else + Tactics.clear name <*> + tclINDEPENDENTL begin + Ssrprinters.ppdebug (lazy Pp.(str"..was NOT the last view")); + Ssrcommon.tacSIGMA >>= + apply_all_views_aux ~clear_if_id vs finalization conclusion + end >>= reduce_or) + +let apply_all_views vs ~conclusion ~clear_if_id = + let finalization s0 k = + State.vsCONSUME_IF_PRESENT (fun ~names t ~to_clear -> + match t with + | None -> k [] None + | Some t -> + finalize_view s0 t >>= fun p -> k (names @ to_clear) (Some p)) in + Ssrcommon.tacSIGMA >>= + apply_all_views_aux ~clear_if_id vs finalization conclusion + +(* We apply a view to a term given by the user, e.g. `case/V: x`. `x` is + `subject` *) +let apply_all_views_to subject ~simple_types vs ~conclusion = begin + let rec process_all_vs = function + | [] -> tclUNIT () + | v :: vs -> is_tac_in_term v >>= function + | `Tac _ -> Ssrcommon.errorstrm Pp.(str"tactic view not supported") + | `Term v -> pile_up_view ~clear_if_id:false v <*> process_all_vs vs in + State.vsASSERT_EMPTY <*> + State.vsINIT ~subject_name:[] ~to_clear:[] ~view:subject <*> + Ssrcommon.tacSIGMA >>= fun s0 -> + process_all_vs vs <*> + State.vsCONSUME (fun ~names:_ t ~to_clear:_ -> + finalize_view s0 ~simple_types t >>= conclusion) +end (* Entry points *********************************************************) -let tclIPAT_VIEWS ~views:vs ?(clear_if_id=false) ~conclusion:tac = - let end_view_application s0 = - State.vsCONSUME (fun ~name t ~to_clear -> - let to_clear = Option.cata (fun x -> [x]) [] name @ to_clear in - finalize_view s0 t >>= pose_proof name <*> tac ~to_clear) in - tclINDEPENDENT begin +let tclIPAT_VIEWS ~views:vs ?(clear_if_id=false) ~conclusion = + tclINDEPENDENTL begin State.vsASSERT_EMPTY <*> - Ssrcommon.tacSIGMA >>= - apply_all_views ~clear_if_id end_view_application vs <*> - State.vsASSERT_EMPTY - end - -let tclWITH_FWD_VIEWS ~simple_types ~subject ~views:vs ~conclusion:tac = - let ending_tac s0 = - State.vsCONSUME (fun ~name:_ t ~to_clear:_ -> - finalize_view s0 ~simple_types t >>= tac) in - tclINDEPENDENT begin + apply_all_views vs ~conclusion ~clear_if_id >>= fun was_tac -> State.vsASSERT_EMPTY <*> - State.vsINIT (subject,[]) <*> - Ssrcommon.tacSIGMA >>= - apply_all_views ~clear_if_id:false ending_tac vs <*> - State.vsASSERT_EMPTY - end + tclUNIT was_tac + end >>= reduce_or + +let tclWITH_FWD_VIEWS ~simple_types ~subject ~views:vs ~conclusion = + tclINDEPENDENT (apply_all_views_to subject ~simple_types vs ~conclusion) (* vim: set filetype=ocaml foldmethod=marker: *) diff --git a/plugins/ssr/ssrview.mli b/plugins/ssr/ssrview.mli index b128a95da7..fb9203263a 100644 --- a/plugins/ssr/ssrview.mli +++ b/plugins/ssr/ssrview.mli @@ -22,11 +22,12 @@ end (* Apply views to the top of the stack (intro pattern). If clear_if_id is * true (default false) then views that happen to be a variable are considered - * as to be cleared (see the to_clear argument to the continuation) *) -val tclIPAT_VIEWS : - views:ast_closure_term list -> ?clear_if_id:bool -> + * as to be cleared (see the to_clear argument to the continuation) + * + * returns true if the last view was a tactic *) +val tclIPAT_VIEWS : views:ast_closure_term list -> ?clear_if_id:bool -> conclusion:(to_clear:Names.Id.t list -> unit Proofview.tactic) -> - unit Proofview.tactic + bool Proofview.tactic (* Apply views to a given subject (as if was the top of the stack), then call conclusion on the obtained term (something like [v2 (v1 subject)]). diff --git a/test-suite/ssr/elim.v b/test-suite/ssr/elim.v index 908249a369..720f4f6607 100644 --- a/test-suite/ssr/elim.v +++ b/test-suite/ssr/elim.v @@ -33,7 +33,7 @@ Qed. (* The same but without names for variables involved in the generated eq *) Lemma testL3 : forall A (s : seq A), s = s. Proof. -move=> A s; elim branch: s; move: (s) => _. +move=> A s; elim branch: s. match goal with _ : _ = [::] |- [::] = [::] => move: branch => // | _ => fail end. move=> _; match goal with _ : _ = _ :: _ |- _ :: _ = _ :: _ => move: branch => // | _ => fail end. Qed. diff --git a/test-suite/ssr/ipat_clear_if_id.v b/test-suite/ssr/ipat_clear_if_id.v index 7a44db2ea0..cc087a62ad 100644 --- a/test-suite/ssr/ipat_clear_if_id.v +++ b/test-suite/ssr/ipat_clear_if_id.v @@ -8,6 +8,7 @@ Variable v2 : nat -> bool. Lemma test (v3 : nat -> bool) (v4 : bool -> bool) (v5 : bool -> bool) : nat -> nat -> nat -> nat -> True. Proof. +Set Debug Ssreflect. move=> {}/v1 b1 {}/v2 b2 {}/v3 b3 {}/v2/v4/v5 b4. Check b1 : bool. Check b2 : bool. @@ -20,4 +21,12 @@ Check v2 : nat -> bool. by []. Qed. +Lemma test2 (v : True <-> False) : True -> False. +Proof. +move=> {}/v. +Fail Check v. +by []. +Qed. + + End Foo. diff --git a/test-suite/ssr/ipat_fastid.v b/test-suite/ssr/ipat_fastid.v new file mode 100644 index 0000000000..8dc0c6cf0b --- /dev/null +++ b/test-suite/ssr/ipat_fastid.v @@ -0,0 +1,31 @@ +Require Import ssreflect. + +Axiom odd : nat -> Prop. + +Lemma simple : + forall x, 3 <= x -> forall y, odd (y+x) -> x = y -> True. +Proof. +move=> >x_ge_3 >xy_odd. +lazymatch goal with +| |- ?x = ?y -> True => done +end. +Qed. + + +Definition stuff x := 3 <= x -> forall y, odd (y+x) -> x = y -> True. + +Lemma harder : forall x, stuff x. +Proof. +move=> >x_ge_3 >xy_odd. +lazymatch goal with +| |- ?x = ?y -> True => done +end. +Qed. + +Lemma homotop : forall x : nat, forall e : x = x, e = e -> True. +Proof. +move=> >eq_ee. +lazymatch goal with +| |- True => done +end. +Qed. diff --git a/test-suite/ssr/ipat_seed.v b/test-suite/ssr/ipat_seed.v new file mode 100644 index 0000000000..e418d66917 --- /dev/null +++ b/test-suite/ssr/ipat_seed.v @@ -0,0 +1,60 @@ +Require Import ssreflect. + +Section foo. + +Variable A : Type. + +Record bar (X : Type) := mk_bar { + a : X * A; + b : A; + c := (a,7); + _ : X; + _ : X +}. + +Inductive baz (X : Type) (Y : Type) : nat -> Type := +| K1 x (e : 0=1) (f := 3) of x=x:>X : baz X Y O +| K2 n of n=n & baz X nat 0 : baz X Y (n+1). + +Axiom Q : nat -> Prop. +Axiom Qx : forall x, Q x. +Axiom my_ind : + forall P : nat -> Prop, P O -> (forall n m (w : P n /\ P m), P (n+m)) -> + forall w, P w. + +Lemma test x : bar nat -> baz nat nat x -> forall n : nat, Q n. +Proof. + +(* record *) +move => [^~ _ccc ]. +Check (refl_equal _ : c_ccc = (a_ccc, 7)). + +(* inductive *) +move=> [^ xxx_ ]. +Check (refl_equal _ : xxx_f = 3). + by []. +Check (refl_equal _ : xxx_n = xxx_n). + +(* eliminator *) +elim/my_ind => [^ wow_ ]. + exact: Qx 0. +Check (wow_w : Q wow_n /\ Q wow_m). +exact: Qx (wow_n + wow_m). + +Qed. + +Arguments mk_bar A x y z w : rename. +Arguments K1 A B a b c : rename. + + +Lemma test2 x : bar nat -> baz nat nat x -> forall n : nat, Q n. +Proof. +move=> [^~ _ccc ]. +Check (refl_equal _ : c_ccc = (x_ccc, 7)). +move=> [^ xxx_ ]. +Check (refl_equal _ : xxx_f = 3). + by []. +Check (refl_equal _ : xxx_n = xxx_n). +Abort. + +End foo. diff --git a/test-suite/ssr/ipat_tac.v b/test-suite/ssr/ipat_tac.v new file mode 100644 index 0000000000..cfef2e37be --- /dev/null +++ b/test-suite/ssr/ipat_tac.v @@ -0,0 +1,38 @@ +Require Import ssreflect. + +Ltac fancy := case; last first. + +Notation fancy := (ltac:( fancy )). + +Ltac replicate n := + let what := fresh "_replicate_" in + move=> what; do n! [ have := what ]; clear what. + +Notation replicate n := (ltac:( replicate n )). + +Lemma foo x (w : nat) (J : bool -> nat -> nat) : exists y, x=0+y. +Proof. +move: (w) => /ltac:(idtac) _. +move: w => /(replicate 6) w1 w2 w3 w4 w5 w6. +move: w1 => /J/fancy [w'||];last exact: false. + move: w' => /J/fancy[w''||]; last exact: false. + by exists x. + by exists x. +by exists x. +Qed. + +Ltac unfld what := rewrite /what. + +Notation "% n" := (ltac:( unfld n )) (at level 0) : ssripat_scope. +Notation "% n" := n : nat_scope. + +Open Scope nat_scope. + + +Definition def := 4. + +Lemma test : True -> def = 4. +Proof. +move=> _ /(% def). +match goal with |- 4 = 4 => reflexivity end. +Qed. diff --git a/test-suite/ssr/ipat_tmp.v b/test-suite/ssr/ipat_tmp.v new file mode 100644 index 0000000000..5f5421ac74 --- /dev/null +++ b/test-suite/ssr/ipat_tmp.v @@ -0,0 +1,22 @@ +Require Import ssreflect ssrbool. + + Axiom eqn : nat -> nat -> bool. + Infix "==" := eqn (at level 40). + Axiom eqP : forall x y : nat, reflect (x = y) (x == y). + + Lemma test1 : + forall x y : nat, x = y -> forall z : nat, y == z -> x = z. + Proof. + by move=> x y + z /eqP <-; apply. + Qed. + + Lemma test2 : forall (x y : nat) (e : x = y), e = e -> x = y. + Proof. + move=> + y + _ => x def_x; exact: (def_x : x = y). + Qed. + + Lemma test3 : + forall x y : nat, x = y -> forall z : nat, y == z -> x = z. + Proof. + move=> ++++ /eqP <- => x y e z; exact: e. + Qed. |