aboutsummaryrefslogtreecommitdiffhomepage
diff options
context:
space:
mode:
authorGravatar Maxime Dénès <mail@maximedenes.fr>2018-06-23 17:09:47 +0200
committerGravatar Maxime Dénès <mail@maximedenes.fr>2018-06-23 17:09:47 +0200
commit7836f9319f17a642921cbf9b153077fc195ca8e1 (patch)
tree70dc89c80436adcfde89e2c0a02cf5163fb77266
parentddd99ca6b4a23286405ec995379e4b07d42b0f78 (diff)
parentdb2147fe29ca5d805f94e1a61f8a568dcd9b620f (diff)
Merge PR #7236: [ssr] simpler semantics for delayed clears
-rw-r--r--CHANGES20
-rw-r--r--doc/sphinx/proof-engine/ssreflect-proof-language.rst17
-rw-r--r--plugins/ssr/ssrast.mli2
-rw-r--r--plugins/ssr/ssripats.ml50
-rw-r--r--plugins/ssr/ssrparser.ml419
-rw-r--r--plugins/ssr/ssrprinters.ml3
-rw-r--r--plugins/ssr/ssrview.ml91
-rw-r--r--plugins/ssr/ssrview.mli6
-rw-r--r--test-suite/ssr/ipat_clear_if_id.v23
9 files changed, 166 insertions, 65 deletions
diff --git a/CHANGES b/CHANGES
index c36f59726..6ad2cc548 100644
--- a/CHANGES
+++ b/CHANGES
@@ -61,6 +61,26 @@ Coq binaries and process model
`coq{proof,tactic,query}worker` are in charge of task-specific and
parallel proof checking.
+SSReflect
+
+- The implementation of delayed clear switches in intro patterns
+ is now simpler to explain:
+ 1. The immediate effect of a clear switch like {x} is to rename the
+ variable x to _x_ (i.e. a reserved identifier that cannot be mentioned
+ explicitly)
+ 2. The delayed effect of {x} is that _x_ is cleared at the end of the intro
+ pattern
+ 3. A clear switch immediately before a view application like {x}/v is
+ translated to /v{x}.
+ In particular rule 3 lets one write {x}/v even if v uses the variable x:
+ indeed the view is executed before the renaming.
+
+- An empty clear switch is now accepted in intro patterns before a
+ view application whenever the view is a variable.
+ One can now write {}/v to mean {v}/v. Remark that {}/x is very similar
+ to the idiom {}e for the rewrite tactic (the equation e is used for
+ rewriting and then discarded).
+
Changes from 8.8.0 to 8.8.1
===========================
diff --git a/doc/sphinx/proof-engine/ssreflect-proof-language.rst b/doc/sphinx/proof-engine/ssreflect-proof-language.rst
index ab52c2ce7..6fb73a030 100644
--- a/doc/sphinx/proof-engine/ssreflect-proof-language.rst
+++ b/doc/sphinx/proof-engine/ssreflect-proof-language.rst
@@ -623,7 +623,9 @@ where:
+ In the occurrence switch :token:`occ_switch`, if the first element of the
list is a natural, this element should be a number, and not an Ltac
variable. The empty list ``{}`` is not interpreted as a valid occurrence
- switch.
+ switch, it is rather used as a flag to signal the intent of the user to
+ clear the name following it (see :ref:`ssr_rewrite_occ_switch` and
+ :ref:`introduction_ssr`)
The tactic:
@@ -1539,7 +1541,7 @@ whose general syntax is
:name: =>
.. prodn::
- i_item ::= @i_pattern %| @s_item %| @clear_switch %| /@term
+ i_item ::= @i_pattern %| @s_item %| @clear_switch %| {? %{%} } /@term
.. prodn::
s_item ::= /= %| // %| //=
@@ -1641,6 +1643,11 @@ The view is applied to the top assumption.
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` * ``| … |``
@@ -3236,6 +3243,7 @@ the equality.
Indeed the left hand side of ``H`` does not match
the redex identified by the pattern ``x + y * 4``.
+.. _ssr_rewrite_occ_switch:
Occurrence switches and redex switches
``````````````````````````````````````
@@ -3260,6 +3268,9 @@ the rewrite tactic. The effect of the tactic on the initial goal is to
rewrite this lemma at the second occurrence of the first matching
``x + y + 0`` of the explicit rewrite redex ``_ + y + 0``.
+An empty occurrence switch ``{}`` is not interpreted as a valid occurrence
+switch. It has the effect of clearing the :token:`r_item` (when it is the name
+of a context entry).
Occurrence selection and repetition
```````````````````````````````````
@@ -5279,7 +5290,7 @@ generalization item see :ref:`structure_ssr`
intro pattern :ref:`introduction_ssr`
-.. prodn:: i_item ::= @clear_switch %| @s_item %| @i_pattern %| / @term
+.. prodn:: i_item ::= @clear_switch %| @s_item %| @i_pattern %| {? %{%} } / @term
intro item see :ref:`introduction_ssr`
diff --git a/plugins/ssr/ssrast.mli b/plugins/ssr/ssrast.mli
index 5571c5420..6ba937a2f 100644
--- a/plugins/ssr/ssrast.mli
+++ b/plugins/ssr/ssrast.mli
@@ -88,7 +88,7 @@ type ssripat =
| IPatCase of (* ipats_mod option * *) ssripatss (* 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 ssrview (* /view *)
+ | IPatView of bool * ssrview (* {}/view (true if the clear is present) *)
| IPatClear of ssrclear (* {H1 H2} *)
| IPatSimpl of ssrsimpl
| IPatAbstractVars of Id.t list
diff --git a/plugins/ssr/ssripats.ml b/plugins/ssr/ssripats.ml
index 8207bc11e..46fde4115 100644
--- a/plugins/ssr/ssripats.ml
+++ b/plugins/ssr/ssripats.ml
@@ -119,13 +119,10 @@ let intro_end =
Ssrcommon.tcl0G (isCLR_CONSUME)
(** [=> _] *****************************************************************)
-let intro_clear ids future_ipats =
+let intro_clear ids =
Goal.enter begin fun gl ->
let _, clear_ids, ren =
List.fold_left (fun (used_ids, clear_ids, ren) id ->
- if not(Ssrcommon.is_name_in_ipats id future_ipats) then begin
- used_ids, id :: clear_ids, ren
- end else
let new_id = Ssrcommon.mk_anon_id (Id.to_string id) used_ids in
(new_id :: used_ids, new_id :: clear_ids, (id, new_id) :: ren))
(Tacmach.New.pf_ids_of_hyps gl, [], []) ids
@@ -213,22 +210,22 @@ let tclLOG p t =
tclUNIT ()
end
-let rec ipat_tac1 future_ipats ipat : unit tactic =
+let rec ipat_tac1 ipat : unit tactic =
match ipat with
- | IPatView l ->
- Ssrview.tclIPAT_VIEWS ~views:l
- ~conclusion:(fun ~to_clear:clr -> intro_clear clr future_ipats)
+ | IPatView (clear_if_id,l) ->
+ Ssrview.tclIPAT_VIEWS ~views:l ~clear_if_id
+ ~conclusion:(fun ~to_clear:clr -> intro_clear clr)
| IPatDispatch ipatss ->
- tclEXTEND (List.map (ipat_tac future_ipats) ipatss) (tclUNIT ()) []
+ tclEXTEND (List.map ipat_tac ipatss) (tclUNIT ()) []
| IPatId id -> Ssrcommon.tclINTRO_ID id
| IPatCase ipatss ->
- tclIORPAT (Ssrcommon.tclWITHTOP tac_case) future_ipats ipatss
+ tclIORPAT (Ssrcommon.tclWITHTOP tac_case) ipatss
| IPatInj ipatss ->
tclIORPAT (Ssrcommon.tclWITHTOP
(fun t -> V82.tactic ~nf_evars:false (Ssrelim.perform_injection t)))
- future_ipats ipatss
+ ipatss
| IPatAnon Drop -> intro_drop
| IPatAnon One -> Ssrcommon.tclINTRO_ANON
@@ -239,7 +236,7 @@ let rec ipat_tac1 future_ipats ipat : unit tactic =
| IPatClear ids ->
tacCHECK_HYPS_EXIST ids <*>
- intro_clear (List.map Ssrcommon.hyp_id ids) future_ipats
+ intro_clear (List.map Ssrcommon.hyp_id ids)
| IPatSimpl (Simpl n) ->
V82.tactic ~nf_evars:false (Ssrequality.simpltac (Simpl n))
@@ -256,17 +253,17 @@ let rec ipat_tac1 future_ipats ipat : unit tactic =
| IPatTac t -> t
-and ipat_tac future_ipats pl : unit tactic =
+and ipat_tac pl : unit tactic =
match pl with
| [] -> tclUNIT ()
| pat :: pl ->
- Ssrcommon.tcl0G (tclLOG pat (ipat_tac1 (pl @ future_ipats))) <*>
+ Ssrcommon.tcl0G (tclLOG pat ipat_tac1) <*>
isTICK pat <*>
- ipat_tac future_ipats pl
+ ipat_tac pl
-and tclIORPAT tac future_ipats = function
+and tclIORPAT tac = function
| [[]] -> tac
- | p -> Tacticals.New.tclTHENS tac (List.map (ipat_tac future_ipats) p)
+ | p -> Tacticals.New.tclTHENS tac (List.map ipat_tac p)
let split_at_first_case ipats =
let rec loop acc = function
@@ -282,12 +279,27 @@ let ssr_exception is_on = function
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 p :: rest -> IPatDispatch (List.map elab p) :: elab rest
+ | IPatCase p :: rest -> IPatCase (List.map elab p) :: elab rest
+ | IPatInj p :: rest -> IPatInj (List.map elab p) :: elab rest
+ | (IPatTac _ | IPatId _ | IPatSimpl _ | IPatClear _ |
+ IPatAnon _ | IPatView _ | IPatNoop | IPatRewrite _ |
+ IPatAbstractVars _) as x :: rest -> x :: elab rest
+ in
+ elab l
+
let main ?eqtac ~first_case_is_dispatch ipats =
+ let ipats = elaborate_ipats ipats in
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)
+ Ssrcommon.tcl0G (ipat_tac (ip_before @ case @ eqtac @ ip_after) <*> intro_end)
end (* }}} *)
@@ -576,7 +588,7 @@ let ssrmovetac = function
(tacVIEW_THEN_GRAB view ~conclusion) <*>
tclIPAT (IPatClear clr :: ipats)
| _::_ as view, (_, ({ gens = []; clr }, ipats)) ->
- tclIPAT (IPatView view :: IPatClear clr :: ipats)
+ tclIPAT (IPatView (false,view) :: IPatClear clr :: ipats)
| _, (Some pat, (dgens, ipats)) ->
let dgentac = with_dgens dgens eqmovetac in
dgentac <*> tclIPAT (eqmoveipats pat ipats)
diff --git a/plugins/ssr/ssrparser.ml4 b/plugins/ssr/ssrparser.ml4
index 7a1d06fdc..347a1e4e2 100644
--- a/plugins/ssr/ssrparser.ml4
+++ b/plugins/ssr/ssrparser.ml4
@@ -412,8 +412,8 @@ let pr_docc = function
let pr_ssrdocc _ _ _ = pr_docc
ARGUMENT EXTEND ssrdocc TYPED AS ssrclear option * ssrocc PRINTED BY pr_ssrdocc
-| [ "{" ne_ssrhyp_list(clr) "}" ] -> [ mkclr clr ]
| [ "{" ssrocc(occ) "}" ] -> [ mkocc occ ]
+| [ "{" ssrhyp_list(clr) "}" ] -> [ mkclr clr ]
END
(* Old kinds of terms *)
@@ -578,7 +578,7 @@ let rec map_ipat map_id map_ssrhyp map_ast_closure_term = function
| IPatCase iorpat -> IPatCase (List.map (List.map (map_ipat map_id map_ssrhyp map_ast_closure_term)) iorpat)
| IPatDispatch iorpat -> IPatDispatch (List.map (List.map (map_ipat map_id map_ssrhyp map_ast_closure_term)) iorpat)
| IPatInj iorpat -> IPatInj (List.map (List.map (map_ipat map_id map_ssrhyp map_ast_closure_term)) iorpat)
- | IPatView v -> IPatView (List.map map_ast_closure_term v)
+ | IPatView (clr,v) -> IPatView (clr,List.map map_ast_closure_term v)
| IPatTac _ -> assert false (*internal usage only *)
let wit_ssripatrep = add_genarg "ssripatrep" pr_ipat
@@ -646,7 +646,7 @@ let interp_ipat ist gl =
| 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 l -> IPatView (List.map (fun x -> snd(interp_ast_closure_term ist
+ | 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 *)
@@ -683,11 +683,17 @@ ARGUMENT EXTEND ssripat TYPED AS ssripatrep list PRINTED BY pr_ssripats
(* TODO | [ "+" ] -> [ [IPatAnon Temporary] ] *)
| [ ssrsimpl_ne(sim) ] -> [ [IPatSimpl sim] ]
| [ ssrdocc(occ) "->" ] -> [ match occ with
+ | Some [], _ -> CErrors.user_err ~loc (str"occ_switch expected")
| None, occ -> [IPatRewrite (occ, L2R)]
| Some clr, _ -> [IPatClear clr; IPatRewrite (allocc, L2R)]]
| [ ssrdocc(occ) "<-" ] -> [ match occ with
+ | Some [], _ -> CErrors.user_err ~loc (str"occ_switch expected")
| None, occ -> [IPatRewrite (occ, R2L)]
| Some clr, _ -> [IPatClear clr; IPatRewrite (allocc, R2L)]]
+ | [ ssrdocc(occ) ssrfwdview(v) ] -> [ match occ with
+ | Some [], _ -> [IPatView (true,v)]
+ | Some cl, _ -> check_hyps_uniq [] cl; [IPatClear cl;IPatView (false,v)]
+ | _ -> CErrors.user_err ~loc (str"Only identifiers are allowed here") ]
| [ ssrdocc(occ) ] -> [ match occ with
| Some cl, _ -> check_hyps_uniq [] cl; [IPatClear cl]
| _ -> CErrors.user_err ~loc (str"Only identifiers are allowed here")]
@@ -705,7 +711,7 @@ ARGUMENT EXTEND ssripat TYPED AS ssripatrep list PRINTED BY pr_ssripats
| [ "-/" integer(n) "/=" ] -> [ [IPatNoop;IPatSimpl(SimplCut (n,~-1))] ]
| [ "-/" integer(n) "/" integer (m) "=" ] ->
[ [IPatNoop;IPatSimpl(SimplCut(n,m))] ]
- | [ ssrfwdview(v) ] -> [ [IPatView v] ]
+ | [ ssrfwdview(v) ] -> [ [IPatView (false,v)] ]
| [ "[" ":" ident_list(idl) "]" ] -> [ [IPatAbstractVars idl] ]
| [ "[:" ident_list(idl) "]" ] -> [ [IPatAbstractVars idl] ]
END
@@ -1678,7 +1684,10 @@ let pr_gen (docc, dt) = pr_docc docc ++ pr_cpattern dt
let pr_ssrgen _ _ _ = pr_gen
ARGUMENT EXTEND ssrgen TYPED AS ssrdocc * cpattern PRINTED BY pr_ssrgen
-| [ ssrdocc(docc) cpattern(dt) ] -> [ docc, dt ]
+| [ ssrdocc(docc) cpattern(dt) ] -> [
+ match docc with
+ | Some [], _ -> CErrors.user_err ~loc (str"Clear flag {} not allowed here")
+ | _ -> docc, dt ]
| [ cpattern(dt) ] -> [ nodocc, dt ]
END
diff --git a/plugins/ssr/ssrprinters.ml b/plugins/ssr/ssrprinters.ml
index 11369228c..8f4b2179e 100644
--- a/plugins/ssr/ssrprinters.ml
+++ b/plugins/ssr/ssrprinters.ml
@@ -107,7 +107,8 @@ let rec pr_ipat p =
| IPatAnon All -> str "*"
| IPatAnon Drop -> str "_"
| IPatAnon One -> str "?"
- | IPatView v -> pr_view2 v
+ | IPatView (false,v) -> pr_view2 v
+ | IPatView (true,v) -> str"{}" ++ pr_view2 v
| IPatNoop -> str "-"
| IPatAbstractVars l -> str "[:" ++ pr_list spc Id.print l ++ str "]"
| IPatTac _ -> str "<tac>"
diff --git a/plugins/ssr/ssrview.ml b/plugins/ssr/ssrview.ml
index faebe3179..3f974ea06 100644
--- a/plugins/ssr/ssrview.ml
+++ b/plugins/ssr/ssrview.ml
@@ -67,9 +67,9 @@ end
module State : sig
(* View storage API *)
- val vsINIT : EConstr.t -> unit tactic
- val vsPUSH : (EConstr.t -> EConstr.t tactic) -> unit tactic
- val vsCONSUME : (Id.t option -> EConstr.t -> unit tactic) -> unit tactic
+ val vsINIT : EConstr.t * 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 vsASSERT_EMPTY : unit tactic
end = struct (* {{{ *)
@@ -78,6 +78,7 @@ type vstate = {
subject_name : Id.t option; (* top *)
(* None if views are being applied to a term *)
view : EConstr.t; (* v2 (v1 top) *)
+ to_clear : Id.t list;
}
include Ssrcommon.MakeState(struct
@@ -85,13 +86,14 @@ include Ssrcommon.MakeState(struct
let init = None
end)
-let vsINIT view = tclSET (Some { subject_name = None; view })
+let vsINIT (view, to_clear) =
+ tclSET (Some { subject_name = None; view; to_clear })
let vsPUSH k =
tacUPDATE (fun s -> match s with
- | Some { subject_name; view } ->
- k view >>= fun view ->
- tclUNIT (Some { subject_name; view })
+ | 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
@@ -102,15 +104,15 @@ let vsPUSH k =
| _ -> 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 ->
- tclUNIT (Some { subject_name = Some id; view })
+ 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
- | Some { subject_name; view } ->
+ | Some { subject_name; view; to_clear } ->
tclSET None <*>
- k subject_name view
+ k ~name:subject_name view ~to_clear
| None -> anomaly "vsCONSUME: empty storage")
let vsASSERT_EMPTY =
@@ -187,6 +189,16 @@ end
* modular, see the 2 functions below that would need to "uncommit" *)
let tclKeepOpenConstr (_env, sigma, t) = Unsafe.tclEVARS sigma <*> tclUNIT t
+let tclADD_CLEAR_IF_ID (env, ist, t) x =
+ Ssrprinters.ppdebug (lazy
+ Pp.(str"tclADD_CLEAR_IF_ID: " ++ Printer.pr_econstr_env env ist t));
+ let hd, _ = EConstr.decompose_app ist t in
+ match EConstr.kind ist hd with
+ | Constr.Var id when Ssrcommon.not_section_id id -> tclUNIT (x, [id])
+ | _ -> tclUNIT (x,[])
+
+let tclPAIR p x = tclUNIT (x, p)
+
(* The ssr heuristic : *)
(* Estimate a bound on the number of arguments of a raw constr. *)
(* This is not perfect, because the unifier may fail to *)
@@ -203,14 +215,15 @@ let guess_max_implicits ist glob =
(fun _ -> tclUNIT 5)
let pad_to_inductive ist glob = Goal.enter_one ~__LOC__ begin fun goal ->
- interp_glob ist glob >>= fun (env, sigma, term) ->
+ interp_glob ist glob >>= fun (env, sigma, term as ot) ->
let term_ty = Retyping.get_type_of env sigma term in
let ctx, i = Reductionops.splay_prod env sigma term_ty in
let rel_ctx =
List.map (fun (a,b) -> Context.Rel.Declaration.LocalAssum(a,b)) ctx in
- if Ssrcommon.isAppInd (EConstr.push_rel_context rel_ctx env) sigma i
- then tclUNIT (mkGApp glob (mkGHoles (List.length ctx)))
- else Tacticals.New.tclZEROMSG Pp.(str"not an inductive")
+ if not (Ssrcommon.isAppInd (EConstr.push_rel_context rel_ctx env) sigma i)
+ then Tacticals.New.tclZEROMSG Pp.(str"not an inductive")
+ else tclUNIT (mkGApp glob (mkGHoles (List.length ctx)))
+ >>= tclADD_CLEAR_IF_ID ot
end
(* There are two ways of "applying" a view to term: *)
@@ -221,7 +234,7 @@ end
(* They require guessing the view hints and the number of *)
(* implicits, respectively, which we do by brute force. *)
(* Builds v p *)
-let interp_view ist v p =
+let interp_view ~clear_if_id ist v p =
let is_specialize hd =
match DAst.get hd with Glob_term.GHole _ -> true | _ -> false in
(* We cast the pile of views p into a term p_id *)
@@ -230,25 +243,31 @@ let interp_view ist v p =
match DAst.get v with
| Glob_term.GApp (hd, rargs) when is_specialize hd ->
Ssrprinters.ppdebug (lazy Pp.(str "specialize"));
- interp_glob ist (mkGApp p_id rargs) >>= tclKeepOpenConstr
+ interp_glob ist (mkGApp p_id rargs)
+ >>= tclKeepOpenConstr >>= tclPAIR []
| _ ->
Ssrprinters.ppdebug (lazy Pp.(str "view"));
(* We find out how to build (v p) eventually using an adaptor *)
let adaptors = AdaptorDb.(get Forward) in
Proofview.tclORELSE
- (pad_to_inductive ist v >>= fun vpad ->
+ (pad_to_inductive ist v >>= fun (vpad,clr) ->
Ssrcommon.tclFIRSTa (List.map
- (fun a -> interp_glob ist (mkGApp a [vpad; p_id])) adaptors))
+ (fun a -> interp_glob ist (mkGApp a [vpad; p_id])) adaptors)
+ >>= tclPAIR clr)
(fun _ ->
guess_max_implicits ist v >>= fun n ->
Ssrcommon.tclFIRSTi (fun n ->
- interp_glob ist (mkGApp v (mkGHoles n @ [p_id]))) n)
- >>= tclKeepOpenConstr
+ interp_glob ist (mkGApp v (mkGHoles n @ [p_id]))) n
+ >>= fun x -> tclADD_CLEAR_IF_ID x x)
+ >>= fun (ot,clr) ->
+ if clear_if_id
+ then tclKeepOpenConstr ot >>= tclPAIR clr
+ else tclKeepOpenConstr ot >>= tclPAIR []
(* we store in the state (v top), then (v1 (v2 top))... *)
-let pile_up_view (ist, v) =
+let pile_up_view ~clear_if_id (ist, v) =
let ist = Ssrcommon.option_assert_get ist (Pp.str"not a term") in
- State.vsPUSH (fun p -> interp_view ist v p)
+ State.vsPUSH (fun p -> interp_view ~clear_if_id ist v p)
let finalize_view s0 ?(simple_types=true) p =
Goal.enter_one ~__LOC__ begin fun g ->
@@ -292,7 +311,7 @@ let pose_proof subject_name p =
<*>
Tactics.New.reduce_after_refine
-let rec apply_all_views ending vs s0 =
+let rec apply_all_views ~clear_if_id ending vs s0 =
match vs with
| [] -> ending s0
| v :: vs ->
@@ -301,31 +320,35 @@ let rec apply_all_views ending vs s0 =
| `Tac tac ->
Ssrprinters.ppdebug (lazy Pp.(str"..a tactic"));
ending s0 <*> Tacinterp.eval_tactic tac <*>
- Ssrcommon.tacSIGMA >>= apply_all_views ending vs
+ Ssrcommon.tacSIGMA >>= apply_all_views ~clear_if_id ending vs
| `Term v ->
Ssrprinters.ppdebug (lazy Pp.(str"..a term"));
- pile_up_view v <*> apply_all_views ending vs s0
+ pile_up_view ~clear_if_id v <*>
+ apply_all_views ~clear_if_id ending vs s0
(* Entry points *********************************************************)
-let tclIPAT_VIEWS ~views:vs ~conclusion:tac =
+let tclIPAT_VIEWS ~views:vs ?(clear_if_id=false) ~conclusion:tac =
let end_view_application s0 =
- State.vsCONSUME (fun name t ->
- finalize_view s0 t >>= pose_proof name <*>
- tac ~to_clear:(Option.cata (fun x -> [x]) [] name)) in
+ 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
State.vsASSERT_EMPTY <*>
- Ssrcommon.tacSIGMA >>= apply_all_views end_view_application vs <*>
+ 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 _ t -> finalize_view s0 ~simple_types t >>= tac) in
+ State.vsCONSUME (fun ~name:_ t ~to_clear:_ ->
+ finalize_view s0 ~simple_types t >>= tac) in
tclINDEPENDENT begin
State.vsASSERT_EMPTY <*>
- State.vsINIT subject <*>
- Ssrcommon.tacSIGMA >>= apply_all_views ending_tac vs <*>
+ State.vsINIT (subject,[]) <*>
+ Ssrcommon.tacSIGMA >>=
+ apply_all_views ~clear_if_id:false ending_tac vs <*>
State.vsASSERT_EMPTY
end
diff --git a/plugins/ssr/ssrview.mli b/plugins/ssr/ssrview.mli
index be51fe7f9..b128a95da 100644
--- a/plugins/ssr/ssrview.mli
+++ b/plugins/ssr/ssrview.mli
@@ -20,9 +20,11 @@ module AdaptorDb : sig
end
-(* Apply views to the top of the stack (intro pattern) *)
+(* 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 ->
+ views:ast_closure_term list -> ?clear_if_id:bool ->
conclusion:(to_clear:Names.Id.t list -> unit Proofview.tactic) ->
unit Proofview.tactic
diff --git a/test-suite/ssr/ipat_clear_if_id.v b/test-suite/ssr/ipat_clear_if_id.v
new file mode 100644
index 000000000..7a44db2ea
--- /dev/null
+++ b/test-suite/ssr/ipat_clear_if_id.v
@@ -0,0 +1,23 @@
+Require Import ssreflect.
+
+Axiom v1 : nat -> bool.
+
+Section Foo.
+
+Variable v2 : nat -> bool.
+
+Lemma test (v3 : nat -> bool) (v4 : bool -> bool) (v5 : bool -> bool) : nat -> nat -> nat -> nat -> True.
+Proof.
+move=> {}/v1 b1 {}/v2 b2 {}/v3 b3 {}/v2/v4/v5 b4.
+Check b1 : bool.
+Check b2 : bool.
+Check b3 : bool.
+Check b4 : bool.
+Fail Check v3.
+Fail Check v4.
+Fail Check v5.
+Check v2 : nat -> bool.
+by [].
+Qed.
+
+End Foo.