diff options
| author |  Enrico Tassi <Enrico.Tassi@inria.fr> | 2018-02-07 10:59:00 +0100 |
|---|---|---|
| committer | Enrico Tassi <Enrico.Tassi@inria.fr> | 2018-03-04 18:01:24 +0100 |
| commit | f35069aec1847068ecb501244507cb5aa9fa9b81 (patch) | |
| tree | 7a47940f36cec47c35d9e73812361f12e22c2202 /plugins/ssr/ssrprinters.mli | |
| parent | 9efd7ac0311f2b55756d7aa2790b0adb75c69579 (diff) | |
ssr: rewrite Ssripats and Ssrview in the tactic monad
Ssripats and Ssrview are now written in the Tactic Monad.
Ssripats implements the => tactical.
Ssrview implements the application of forward views.
The code is, according to my tests, 100% backward compatible.
The code is much more documented than before.
Moreover the "ist" (ltac context) used to interpret views is the correct
one (the one at ARGUMENT EXTEND interp time, not the one at TACTIC
EXTEND execution time). Some of the code not touched by this commit
still uses the incorrect ist, so its visibility in TACTIC EXTEND
can't be removed yet.
The main changes in the code are:
- intro patterns are implemented using a state machine (a goal comes
with a state). Ssrcommon.MakeState provides an easy way for a tactic
to enrich the goal with with data of interest, such as the set of
hyps to be cleared. This cleans up the old implementation that, in
order to thread the state, that to redefine a bunch of tclSTUFF
- the interpretation of (multiple) forward views uses the state to
accumulate intermediate results
- the bottom of Sscommon collects a bunch of utilities written in the
tactic monad. Most of them are the rewriting of already existing
utilities. When possible the old version was removed.
Diffstat (limited to 'plugins/ssr/ssrprinters.mli')
| -rw-r--r-- | plugins/ssr/ssrprinters.mli | 12 |
1 files changed, 12 insertions, 0 deletions
diff --git a/plugins/ssr/ssrprinters.mli b/plugins/ssr/ssrprinters.mli index f23106826..9fe54e0b1 100644 --- a/plugins/ssr/ssrprinters.mli +++ b/plugins/ssr/ssrprinters.mli @@ -27,11 +27,23 @@ val xWithAt : ssrtermkind val xNoFlag : ssrtermkind val xCpattern : ssrtermkind +val pr_clear : (unit -> Pp.t) -> ssrclear -> Pp.t +val pr_clear_ne : ssrclear -> Pp.t +val pr_dir : ssrdir -> Pp.t +val pr_simpl : ssrsimpl -> Pp.t + val pr_term : ssrtermkind * (Glob_term.glob_constr * Constrexpr.constr_expr option) -> Pp.t +val pr_ast_closure_term : ast_closure_term -> Pp.t +val pr_view2 : ast_closure_term list -> Pp.t +val pr_ipat : ssripat -> Pp.t +val pr_ipats : ssripats -> Pp.t +val pr_iorpat : ssripatss -> Pp.t + val pr_hyp : ssrhyp -> Pp.t +val pr_hyps : ssrhyps -> Pp.t val prl_constr_expr : Constrexpr.constr_expr -> Pp.t val prl_glob_constr : Glob_term.glob_constr -> Pp.t |