Adding a command to evaluate Ltac2 expressions.

4 files changed, 54 insertions, 2 deletions

diff --git a/doc/ltac2.md b/doc/ltac2.md
index d7c8719a14..6cbe0988d0 100644
--- a/doc/ltac2.md
+++ b/doc/ltac2.md
@@ -727,6 +727,20 @@ foo 0 ↦ (fun x => x ()) (fun _ => 0)
 Note that abbreviations are not typechecked at all, and may result in typing
 errors after expansion.
 
+# Evaluation
+
+Ltac2 features a toplevel loop that can be used to evaluate expressions.
+
+```
+VERNAC ::=
+| "Ltac2" "Eval" TERM
+```
+
+This command evaluates the term in the current proof if there is one, or in the
+global environment otherwise, and displays the resulting value to the user
+together with its type. This function is pure in the sense that it does not
+modify the state of the proof, and in particular all side-effects are discarded.
+
 # Debug
 
 When the option `Ltac2 Backtrace` is set, toplevel failures will be printed with
diff --git a/src/g_ltac2.ml4 b/src/g_ltac2.ml4
index be6c2de5a9..a979b1e9b8 100644
--- a/src/g_ltac2.ml4
+++ b/src/g_ltac2.ml4
@@ -88,6 +88,7 @@ let tac2def_typ = Gram.entry_create "tactic:tac2def_typ"
 let tac2def_ext = Gram.entry_create "tactic:tac2def_ext"
 let tac2def_syn = Gram.entry_create "tactic:tac2def_syn"
 let tac2def_mut = Gram.entry_create "tactic:tac2def_mut"
+let tac2def_run = Gram.entry_create "tactic:tac2def_run"
 let tac2mode = Gram.entry_create "vernac:ltac2_command"
 
 (** FUCK YOU API *)
@@ -109,7 +110,7 @@ let pattern_of_qualid ?loc id =
 
 GEXTEND Gram
   GLOBAL: tac2expr tac2type tac2def_val tac2def_typ tac2def_ext tac2def_syn
-          tac2def_mut;
+          tac2def_mut tac2def_run;
   tac2pat:
     [ "1" LEFTA
       [ id = Prim.qualid; pl = LIST1 tac2pat LEVEL "0" ->
@@ -273,6 +274,9 @@ GEXTEND Gram
   tac2def_mut:
     [ [ "Set"; qid = Prim.qualid; ":="; e = tac2expr -> StrMut (qid, e) ] ]
   ;
+  tac2def_run:
+    [ [ "Eval"; e = tac2expr -> StrRun e ] ]
+  ;
   tac2typ_knd:
     [ [ t = tac2type -> CTydDef (Some t)
       | "["; ".."; "]" -> CTydOpn
@@ -801,11 +805,12 @@ PRINTED BY pr_ltac2entry
 | [ tac2def_ext(e) ] -> [ e ]
 | [ tac2def_syn(e) ] -> [ e ]
 | [ tac2def_mut(e) ] -> [ e ]
+| [ tac2def_run(e) ] -> [ e ]
 END
 
 let classify_ltac2 = function
 | StrSyn _ -> Vernacexpr.VtUnknown, Vernacexpr.VtNow
-| StrMut _ | StrVal _ | StrPrm _  | StrTyp _ -> Vernac_classifier.classify_as_sideeff
+| StrMut _ | StrVal _ | StrPrm _  | StrTyp _ | StrRun _ -> Vernac_classifier.classify_as_sideeff
 
 VERNAC COMMAND EXTEND VernacDeclareTactic2Definition
 | [ "Ltac2" ltac2_entry(e) ] => [ classify_ltac2 e ] -> [
diff --git a/src/tac2entries.ml b/src/tac2entries.ml
index 04bf21f656..b803278929 100644
--- a/src/tac2entries.ml
+++ b/src/tac2entries.ml
@@ -739,6 +739,36 @@ let register_redefinition ?(local = false) (loc, qid) e =
   } in
   Lib.add_anonymous_leaf (inTac2Redefinition def)
 
+let perform_eval e =
+  let open Proofview.Notations in
+  let env = Global.env () in
+  let (e, ty) = Tac2intern.intern ~strict:false e in
+  let v = Tac2interp.interp Tac2interp.empty_environment e in
+  let selector, proof =
+    try
+      Proof_bullet.get_default_goal_selector (),
+      Proof_global.give_me_the_proof ()
+    with Proof_global.NoCurrentProof ->
+      let sigma = Evd.from_env env in
+      Vernacexpr.SelectAll, Proof.start sigma []
+  in
+  let v = match selector with
+  | Vernacexpr.SelectNth i -> Proofview.tclFOCUS i i v
+  | Vernacexpr.SelectList l -> Proofview.tclFOCUSLIST l v
+  | Vernacexpr.SelectId id -> Proofview.tclFOCUSID id v
+  | Vernacexpr.SelectAll -> v
+  in
+  (** HACK: the API doesn't allow to return a value *)
+  let ans = ref None in
+  let tac = (v >>= fun r -> ans := Some r; Proofview.tclUNIT ()) in
+  let (proof, _) = Proof.run_tactic (Global.env ()) tac proof in
+  let sigma = Proof.in_proof proof (fun sigma -> sigma) in
+  let ans = match !ans with None -> assert false | Some r -> r in
+  let name = int_name () in
+  Feedback.msg_notice (str "- : " ++ pr_glbtype name (snd ty)
+    ++ spc () ++  str "=" ++ spc () ++
+    Tac2print.pr_valexpr env sigma ans (snd ty))
+
 (** Toplevel entries *)
 
 let register_struct ?local str = match str with
@@ -747,6 +777,7 @@ let register_struct ?local str = match str with
 | StrPrm (id, t, ml) -> register_primitive ?local id t ml
 | StrSyn (tok, lev, e) -> register_notation ?local tok lev e
 | StrMut (qid, e) -> register_redefinition ?local qid e
+| StrRun e -> perform_eval e
 
 (** Toplevel exception *)
 
diff --git a/src/tac2expr.mli b/src/tac2expr.mli
index e57b0ba3ef..89152dffe7 100644
--- a/src/tac2expr.mli
+++ b/src/tac2expr.mli
@@ -168,6 +168,8 @@ type strexpr =
   (** Syntactic extensions *)
 | StrMut of qualid located * raw_tacexpr
   (** Redefinition of mutable globals *)
+| StrRun of raw_tacexpr
+  (** Toplevel evaluation of an expression *)
 
 (** {5 Dynamic semantics} *)