Merge pull request #3314 from mtzguido/tac_ide_primtiive

Tactics: introduce ide() to check if running interactively

ocaml/fstar-lib/FStar_Tactics_V2_Builtins.ml

@@ -87,6 +87,7 @@ let t_apply                 = from_tac_4 "B.t_apply" B.t_apply
 let t_apply_lemma           = from_tac_3 "B.t_apply_lemma" B.t_apply_lemma
 let print                   = from_tac_1 "B.print" B.print
 let debugging               = from_tac_1 "B.debugging" B.debugging
+let ide                     = from_tac_1 "B.ide" B.ide
 let dump                    = from_tac_1 "B.dump" B.dump
 let dump_all                = from_tac_2 "B.dump_all" B.dump_all
 let dump_uvars_of           = from_tac_2 "B.dump_uvars_of" B.dump_uvars_of

src/tactics/FStar.Tactics.V2.Basic.fst

@@ -60,6 +60,7 @@ module Z      = FStar.BigInt
 module Core   = FStar.TypeChecker.Core
 module PO     = FStar.TypeChecker.Primops
 
+let dbg_Tac        = Debug.get_toggle "Tac"
 let dbg_TacUnify   = Debug.get_toggle "TacUnify"
 let dbg_2635       = Debug.get_toggle "2635"
 let dbg_ReflTc     = Debug.get_toggle "ReflTc"
@@ -132,11 +133,14 @@ let print (msg:string) : tac unit =
       tacprint msg;
     return ()
 
-let dbg_Tac = Debug.get_toggle "Tac"
 let debugging () : tac bool =
-    let! ps = get in
+    return ();! (* thunk *)
     return !dbg_Tac
 
+let ide () : tac bool =
+    return ();! (* thunk *)
+    return (Options.ide ())
+
 let do_dump_ps (msg:string) (ps:proofstate) : unit =
   let psc = ps.psc in
   let subst = PO.psc_subst psc in

src/tactics/FStar.Tactics.V2.Basic.fsti

@@ -70,6 +70,7 @@ val t_apply                : bool -> bool -> bool -> term -> tac unit
 val t_apply_lemma          : bool -> bool -> term -> tac unit
 val print                  : string -> tac unit
 val debugging              : unit -> tac bool
+val ide                    : unit -> tac bool
 val dump                   : string -> tac unit
 val dump_all               : bool -> string -> tac unit
 val dump_uvars_of          : goal -> string -> tac unit

src/tactics/FStar.Tactics.V2.Primops.fst

@@ -146,6 +146,7 @@ let ops = [
   mk_tac_step_1 0 "addns" addns addns;
   mk_tac_step_1 0 "print" print print;
   mk_tac_step_1 0 "debugging" debugging debugging;
+  mk_tac_step_1 0 "ide" ide ide;
   mk_tac_step_1 0 "dump" dump dump;
   mk_tac_step_2 0 "dump_all" dump_all dump_all;
   mk_tac_step_2 0 "dump_uvars_of" dump_uvars_of dump_uvars_of;

ulib/FStar.Stubs.Tactics.V2.Builtins.fsti

@@ -193,6 +193,11 @@ val print : string -> Tac unit
 on, i.e. when [--debug Tac] was passed in. *)
 val debugging : unit -> Tac bool
 
+(** [ide ()] return true if F* is running in interactive mode. This is
+useful to only print diagnostics messages in interactive mode but not in
+batch. *)
+val ide : unit -> Tac bool
+
 (** Similar to [print], but will dump a text representation of the proofstate
 along with the message. *)
 val dump : string -> Tac unit