Delineating a API for Coq inside toplevel/vernac.ml

Coq use case are mostly thoses :
- parsing a char stream to get a vernac expr
- evaluating a vernac expr with backtracking
- turning a knob with a vernac expr, no backtracking
- loading an entire file
- compiling an entire file
- backtracking (no clean API for this yet)
- peeking Coq state info (no clean API for this yet)

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12756 85f007b7-540e-0410-9357-904b9bb8a0f7

3 files changed, 59 insertions, 58 deletions

diff --git a/ide/coq.ml b/ide/coq.ml
index e1bce01281..bcbff419d0 100644
--- a/ide/coq.ml
+++ b/ide/coq.ml
@@ -300,6 +300,11 @@ let is_vernac_tactic_command com =
 let is_vernac_proof_ending_command com =
   List.mem ProofEndingCommand (attribute_of_vernac_command com)
 
+type annotated_vernac =
+  | ControlVernac of vernac_expr * string (* navigation, debug, process control, print opts *)
+  | PureVernac of vernac_expr
+ 
+
 type undo_info = identifier list
 
 let undo_info () = Pfedit.get_all_proof_names ()
@@ -370,11 +375,8 @@ let reset_to_mod id =
   prerr_endline ("Reset called to Mod/Sect with "^(string_of_id id));
   Lib.reset_mod (Util.dummy_loc,id)
 
-let parse_sentence s =
-  Pcoq.Gram.Entry.parse Pcoq.main_entry (Pcoq.Gram.parsable (Stream.of_string s))
-
-let raw_interp s =
-  Vernac.raw_do_vernac (Pcoq.Gram.parsable (Stream.of_string s))
+let parsable_of_string s =
+  Pcoq.Gram.parsable (Stream.of_string s)
 
 module PrintOpt =
 struct
@@ -395,7 +397,8 @@ struct
     Hashtbl.replace state_hack opt value;
     List.iter
       (fun cmd -> 
-         raw_interp ((if value then "Set" else "Unset") ^ " Printing " ^ cmd ^ "."))
+         let str = (if value then "Set" else "Unset") ^ " Printing " ^ cmd ^ "." in
+         Vernac.eval_ctrl (snd (Vernac.parse_sentence (parsable_of_string str,None))))
       opt
 
   let enforce_hack () = Hashtbl.iter set state_hack 
@@ -409,32 +412,31 @@ let forbid_vernac blacklist (loc,vernac) =
 let interp_with_options verbosely s =
   prerr_endline "Starting interp...";
   prerr_endline s;
-  let pa = Pcoq.Gram.parsable (Stream.of_string s) in
-  let pe = Pcoq.Gram.Entry.parse Pcoq.main_entry pa in
+  let pa = parsable_of_string s in
+  try
+    let (loc,vernac) = Vernac.parse_sentence (pa,None) in
   (* Temporary hack to make coqide.byte work (WTF???) - now with less screen
   * pollution *)
-  Pervasives.prerr_string " \r"; Pervasives.flush stderr;
-  match pe with
-    | None -> assert false
-    | Some((loc,vernac) as last) ->
-	if is_vernac_debug_command vernac then
-	  user_error_loc loc (str "Debug mode not available within CoqIDE");
-	if is_vernac_navigation_command vernac then
-	  user_error_loc loc (str "Use CoqIDE navigation instead");
-	if is_vernac_known_option_command vernac then
-	  user_error_loc loc (str "Use CoqIDE display menu instead");
-	if is_vernac_query_command vernac then
-	  flash_info
-	    "Warning: query commands should not be inserted in scripts";
-	if not (is_vernac_goal_printing_command vernac) then
-	  (* Verbose if in small step forward and not a tactic *)
-	  Flags.make_silent (not verbosely);
-        PrintOpt.enforce_hack ();
-	let reset_info = compute_reset_info last in
-	raw_interp s;
-	Flags.make_silent true;
-	prerr_endline ("...Done with interp of : "^s);
-	reset_info
+    Pervasives.prerr_string " \r"; Pervasives.flush stderr;
+    if is_vernac_debug_command vernac then
+      user_error_loc loc (str "Debug mode not available within CoqIDE");
+    if is_vernac_navigation_command vernac then
+      user_error_loc loc (str "Use CoqIDE navigation instead");
+    if is_vernac_known_option_command vernac then
+      user_error_loc loc (str "Use CoqIDE display menu instead");
+    if is_vernac_query_command vernac then
+      flash_info
+        "Warning: query commands should not be inserted in scripts";
+    if not (is_vernac_goal_printing_command vernac) then
+      (* Verbose if in small step forward and not a tactic *)
+      Flags.make_silent (not verbosely);
+    PrintOpt.enforce_hack ();
+    let reset_info = compute_reset_info (loc,vernac) in
+    Vernac.eval_expr (loc,vernac);
+    Flags.make_silent true;
+    prerr_endline ("...Done with interp of : "^s);
+    reset_info
+  with Vernac.End_of_input -> assert false
 
 let interp verbosely phrase =
   interp_with_options verbosely phrase
@@ -478,9 +480,7 @@ let process_exn e = let s,loc= print_toplevel_error e in (msgnl s,loc)
 
 let interp_last last =
   prerr_string "*";
-  try
-    vernac_com (States.with_heavy_rollback Vernacentries.interp) last;
-    Lib.add_frozen_state()
+  try Vernac.eval_expr last
   with e ->
     let s,_ = process_exn e in prerr_endline ("Replay during undo failed because: "^s);
     raise e
diff --git a/toplevel/vernac.ml b/toplevel/vernac.ml
index 6d4ecf7740..0bdb68f495 100644
--- a/toplevel/vernac.ml
+++ b/toplevel/vernac.ml
@@ -89,7 +89,7 @@ let verbose_phrase verbch loc =
 
 exception End_of_input
 
-let parse_phrase (po, verbch) =
+let parse_sentence (po, verbch) =
   match Pcoq.Gram.Entry.parse Pcoq.main_entry po with
     | Some (loc,_ as com) -> verbose_phrase verbch loc; com
     | None -> raise End_of_input
@@ -193,22 +193,21 @@ let rec vernac_com interpfun (loc,com) =
       Format.set_formatter_out_channel stdout;
       raise (DuringCommandInterp (loc, e))
 
-and vernac interpfun input =
-  vernac_com interpfun (parse_phrase input)
-
 and read_vernac_file verbosely s =
   Flags.make_warn verbosely;
   let interpfun =
-    if verbosely then
-      Vernacentries.interp
-    else
-      Flags.silently Vernacentries.interp
+    if verbosely then Vernacentries.interp
+    else Flags.silently Vernacentries.interp
   in
-  let (in_chan, fname, input) = open_file_twice_if verbosely s in
+  let (in_chan, fname, input) =
+    open_file_twice_if verbosely s in
   try
     (* we go out of the following infinite loop when a End_of_input is
      * raised, which means that we raised the end of the file being loaded *)
-    while true do vernac interpfun input; pp_flush () done
+    while true do
+      vernac_com interpfun (parse_sentence input);
+      pp_flush ()
+    done
   with e ->   (* whatever the exception *)
     Format.set_formatter_out_channel stdout;
     close_input in_chan input;    (* we must close the file first *)
@@ -217,17 +216,23 @@ and read_vernac_file verbosely s =
           if do_beautify () then pr_new_syntax (make_loc (max_int,max_int)) None
       | _ -> raise_with_file fname e
 
-(* raw_do_vernac : char Stream.t -> unit
- * parses and executes one command of the vernacular char stream.
- * Marks the end of the command in the lib_stk with a new label to
- * make vernac undoing easier. Also freeze state to speed up
- * backtracking. *)
 
-let raw_do_vernac po =
-  vernac (States.with_heavy_rollback Vernacentries.interp) (po,None);
+(* eval_expr : Util.loc * Vernacexpr.vernac_expr -> unit
+ * execute one vernacular command. Marks the end of the command in the lib_stk
+ * with a new label to make vernac undoing easier. Also freeze state to speed up
+ * backtracking. *)
+let eval_expr last =
+  vernac_com (States.with_heavy_rollback Vernacentries.interp) last;
   Lib.add_frozen_state();
   Lib.mark_end_of_command()
 
+let eval_ctrl ast =
+  vernac_com Vernacentries.interp (Util.dummy_loc,ast)
+
+(* raw_do_vernac : Pcoq.Gram.parsable -> unit
+ * vernac_step . parse_sentence *)
+let raw_do_vernac po = eval_expr (parse_sentence (po,None))
+
 (* XML output hooks *)
 let xml_start_library = ref (fun _ -> ())
 let xml_end_library = ref (fun _ -> ())
diff --git a/toplevel/vernac.mli b/toplevel/vernac.mli
index 4dff36e53e..747c02afe3 100644
--- a/toplevel/vernac.mli
+++ b/toplevel/vernac.mli
@@ -13,8 +13,8 @@
 (* Read a vernac command on the specified input (parse only).
    Raises [End_of_file] if EOF (or Ctrl-D) is reached. *)
 
-val parse_phrase : Pcoq.Gram.parsable * in_channel option ->
-  Util.loc * Vernacexpr.vernac_expr
+val parse_sentence : Pcoq.Gram.parsable * in_channel option ->
+ Util.loc * Vernacexpr.vernac_expr
 
 (* Reads and executes vernac commands from a stream.
    The boolean [just_parsing] disables interpretation of commands. *)
@@ -23,6 +23,8 @@ exception DuringCommandInterp of Util.loc * exn
 exception End_of_input
 
 val just_parsing : bool ref
+val eval_expr : Util.loc * Vernacexpr.vernac_expr -> unit
+val eval_ctrl : Vernacexpr.vernac_expr -> unit
 val raw_do_vernac : Pcoq.Gram.parsable -> unit
 
 (* Set XML hooks *)
@@ -38,9 +40,3 @@ val load_vernac : bool -> string -> unit
 (* Compile a vernac file, verbosely or not (f is assumed without .v suffix) *)
 
 val compile : bool -> string -> unit
-
-(* Interpret a vernac AST *)
-
-val vernac_com :
-  (Vernacexpr.vernac_expr -> unit) ->
-  Util.loc * Vernacexpr.vernac_expr -> unit