aboutsummaryrefslogtreecommitdiffhomepage
path: root/plugins/ssr
diff options
context:
space:
mode:
authorGravatar Emilio Jesus Gallego Arias <e+git@x80.org>2018-02-20 20:39:27 +0100
committerGravatar Emilio Jesus Gallego Arias <e+git@x80.org>2018-03-05 13:42:01 +0100
commit0b1032f2acdb6f7d92c84ba3afcbf3818cc107a9 (patch)
treed9ba31a2560c3f3d51db15ad22cd16bcab724357 /plugins/ssr
parent15331729aaab16678c2f7e29dd391f72df53d76e (diff)
[ssreflect] Export parsing witnesses in mli file.
This is needed in order to manipulate/serialize SSR's AST. A quicker [and maybe better] alternative would be to just remove `ssrparser.mli`, as there are many grammar entries that still need exporting.
Diffstat (limited to 'plugins/ssr')
-rw-r--r--plugins/ssr/ssrast.mli12
-rw-r--r--plugins/ssr/ssrbwd.mli2
-rw-r--r--plugins/ssr/ssripats.mli6
-rw-r--r--plugins/ssr/ssrparser.mli13
4 files changed, 24 insertions, 9 deletions
diff --git a/plugins/ssr/ssrast.mli b/plugins/ssr/ssrast.mli
index 9783bc61d..7f5f2f63d 100644
--- a/plugins/ssr/ssrast.mli
+++ b/plugins/ssr/ssrast.mli
@@ -138,7 +138,7 @@ type ssrclseq = InGoal | InHyps
type 'tac ssrhint = bool * 'tac option list
type 'tac fwdbinders =
- bool * (ssrhpats * ((ssrfwdfmt * ssrterm) * 'tac ssrhint))
+ bool * (ssrhpats * ((ssrfwdfmt * ast_closure_term) * 'tac ssrhint))
type clause =
(ssrclear * ((ssrhyp_or_id * string) *
@@ -157,13 +157,15 @@ type 'a ssrseqarg = ssrindex * ('a ssrhint * 'a option)
open Ssrmatching_plugin
open Ssrmatching
+
+type 'a ssrcasearg = ssripat option * ('a * ssripats)
+type 'a ssrmovearg = ssrview * 'a ssrcasearg
+
type ssrdgens = { dgens : (ssrdocc * cpattern) list;
gens : (ssrdocc * cpattern) list;
clr : ssrclear }
-type ssrcasearg = ssripat option * (ssrdgens * ssripats)
-type ssrmovearg = ssrview * ssrcasearg
-type ssragens = ((ssrhyps option * occ) * ssrterm) list list * ssrclear
-type ssrapplyarg = ssrterm list * (ssragens * ssripats)
+type 'a ssragens = (ssrdocc * 'a) list list * ssrclear
+type ssrapplyarg = ssrterm list * (ssrterm ssragens * ssripats)
(* OOP : these are general shortcuts *)
type gist = Tacintern.glob_sign
diff --git a/plugins/ssr/ssrbwd.mli b/plugins/ssr/ssrbwd.mli
index 6243e5e68..694ecfa37 100644
--- a/plugins/ssr/ssrbwd.mli
+++ b/plugins/ssr/ssrbwd.mli
@@ -13,4 +13,4 @@ open Proofview
val apply_top_tac : unit tactic
-val inner_ssrapplytac : ssrterm list -> ssragens -> ist -> unit tactic
+val inner_ssrapplytac : ssrterm list -> ssrterm ssragens -> ist -> unit tactic
diff --git a/plugins/ssr/ssripats.mli b/plugins/ssr/ssripats.mli
index b8716c0c4..89cba4be7 100644
--- a/plugins/ssr/ssripats.mli
+++ b/plugins/ssr/ssripats.mli
@@ -29,11 +29,11 @@ val tclIPATssr : ssripats -> unit Proofview.tactic
[tac E: gens => ipats]
where [E] is injected into [ipats] (at the right place) and [gens] are
generalized before calling [tac] *)
-val ssrmovetac : ssrmovearg -> unit Proofview.tactic
+val ssrmovetac : ssrdgens ssrmovearg -> unit Proofview.tactic
val ssrsmovetac : unit Proofview.tactic
-val ssrelimtac : ssrmovearg -> unit Proofview.tactic
+val ssrelimtac : ssrdgens ssrmovearg -> unit Proofview.tactic
val ssrselimtoptac : unit Proofview.tactic
-val ssrcasetac : ssrmovearg -> unit Proofview.tactic
+val ssrcasetac : ssrdgens ssrmovearg -> unit Proofview.tactic
val ssrscasetoptac : unit Proofview.tactic
(* The implementation of abstract: is half here, for the [[: var ]]
diff --git a/plugins/ssr/ssrparser.mli b/plugins/ssr/ssrparser.mli
index a52248614..130550388 100644
--- a/plugins/ssr/ssrparser.mli
+++ b/plugins/ssr/ssrparser.mli
@@ -20,3 +20,16 @@ val pr_ssrtclarg : 'a -> 'b -> (Notation_term.tolerability -> 'c -> 'd) -> 'c ->
val add_genarg : string -> ('a -> Pp.t) -> 'a Genarg.uniform_genarg_type
+(* Parsing witnesses, needed to serialize ssreflect syntax *)
+open Ssrmatching_plugin
+open Ssrmatching
+open Ssrast
+open Ssrequality
+
+val wit_ssrrwargs : ssrrwarg list Genarg.uniform_genarg_type
+val wit_ssrclauses : clauses Genarg.uniform_genarg_type
+val wit_ssrcasearg : (cpattern ssragens) ssrmovearg Genarg.uniform_genarg_type
+val wit_ssrmovearg : (cpattern ssragens) ssrmovearg Genarg.uniform_genarg_type
+val wit_ssrapplyarg : ssrapplyarg Genarg.uniform_genarg_type
+val wit_ssrhavefwdwbinders :
+ (Tacexpr.raw_tactic_expr fwdbinders, Tacexpr.glob_tactic_expr fwdbinders, Tacinterp.Value.t fwdbinders) Genarg.genarg_type