From d94a8b2024497e11ff9392a7fa4401ffcc131cc0 Mon Sep 17 00:00:00 2001
From: Pierre-Marie Pédrot
Date: Thu, 10 Mar 2016 15:20:47 +0100
Subject: Moving the proof mode parsing management to Pcoq.

---
 parsing/g_vernac.ml4 | 12 +-----------
 parsing/pcoq.ml      |  9 +++++++++
 parsing/pcoq.mli     |  6 ++++++
 3 files changed, 16 insertions(+), 11 deletions(-)

(limited to 'parsing')

diff --git a/parsing/g_vernac.ml4 b/parsing/g_vernac.ml4
index 49baeb5560..2eb590132a 100644
--- a/parsing/g_vernac.ml4
+++ b/parsing/g_vernac.ml4
@@ -35,7 +35,6 @@ let _ = List.iter Lexer.add_keyword vernac_kw
 let query_command = Gram.entry_create "vernac:query_command"
 
 let tactic_mode = Gram.entry_create "vernac:tactic_command"
-let noedit_mode = Gram.entry_create "vernac:noedit_command"
 let subprf = Gram.entry_create "vernac:subprf"
 
 let class_rawexpr = Gram.entry_create "vernac:class_rawexpr"
@@ -48,11 +47,6 @@ let subgoal_command = Gram.entry_create "proof_mode:subgoal_command"
 let instance_name = Gram.entry_create "vernac:instance_name"
 let section_subset_expr = Gram.entry_create "vernac:section_subset_expr"
 
-let command_entry = ref noedit_mode
-let set_command_entry e = command_entry := e
-let get_command_entry () = !command_entry
-
-
 (* Registers the Classic Proof Mode (which uses [tactic_mode] as a parser for
     proof editing and changes nothing else). Then sets it as the default proof mode. *)
 let set_tactic_mode () = set_command_entry tactic_mode
@@ -82,10 +76,6 @@ let test_bracket_ident =
 	      | _ -> raise Stream.Failure)
 	| _ -> raise Stream.Failure)
 
-let default_command_entry =
-  Gram.Entry.of_parser "command_entry"
-    (fun strm -> Gram.parse_tokens_after_filter (get_command_entry ()) strm)
-
 GEXTEND Gram
   GLOBAL: vernac gallina_ext tactic_mode noedit_mode subprf subgoal_command;
   vernac: FIRST
@@ -129,7 +119,7 @@ GEXTEND Gram
     ] ]
   ;
   vernac_aux: LAST
-    [ [ prfcom = default_command_entry -> prfcom ] ]
+    [ [ prfcom = command_entry -> prfcom ] ]
   ;
   noedit_mode:
     [ [ c = subgoal_command -> c None] ]
diff --git a/parsing/pcoq.ml b/parsing/pcoq.ml
index 91f933987b..9c2f09db84 100644
--- a/parsing/pcoq.ml
+++ b/parsing/pcoq.ml
@@ -383,6 +383,7 @@ module Vernac_ =
     let rec_definition = gec_vernac "Vernac.rec_definition"
     (* Main vernac entry *)
     let main_entry = Gram.entry_create "vernac"
+    let noedit_mode = gec_vernac "noedit_command"
 
     let () =
       let act_vernac = Gram.action (fun v loc -> Some (!@loc, v)) in
@@ -393,10 +394,18 @@ module Vernac_ =
       ] in
       maybe_uncurry (Gram.extend main_entry) (None, make_rule rule)
 
+    let command_entry_ref = ref noedit_mode
+    let command_entry =
+      Gram.Entry.of_parser "command_entry"
+        (fun strm -> Gram.parse_tokens_after_filter !command_entry_ref strm)
+
   end
 
 let main_entry = Vernac_.main_entry
 
+let set_command_entry e = Vernac_.command_entry_ref := e
+let get_command_entry () = !Vernac_.command_entry_ref
+
 (**********************************************************************)
 (* This determines (depending on the associativity of the current
    level and on the expected associativity) if a reference to constr_n is
diff --git a/parsing/pcoq.mli b/parsing/pcoq.mli
index d6bfe3eb39..7410d4e44c 100644
--- a/parsing/pcoq.mli
+++ b/parsing/pcoq.mli
@@ -241,11 +241,17 @@ module Vernac_ :
     val vernac : vernac_expr Gram.entry
     val rec_definition : (fixpoint_expr * decl_notation list) Gram.entry
     val vernac_eoi : vernac_expr Gram.entry
+    val noedit_mode : vernac_expr Gram.entry
+    val command_entry : vernac_expr Gram.entry
   end
 
 (** The main entry: reads an optional vernac command *)
 val main_entry : (Loc.t * vernac_expr) option Gram.entry
 
+(** Handling of the proof mode entry *)
+val get_command_entry : unit -> vernac_expr Gram.entry
+val set_command_entry : vernac_expr Gram.entry -> unit
+
 (** Mapping formal entries into concrete ones *)
 
 (** Binding constr entry keys to entries and symbols *)
-- 
cgit v1.2.3


From 5c8fc9aebe072237a65fc9ed7acf8ae559a78243 Mon Sep 17 00:00:00 2001
From: Pierre-Marie Pédrot
Date: Wed, 16 Mar 2016 19:27:00 +0100
Subject: Moving the parsing of the Ltac proof mode to G_ltac.

---
 parsing/g_ltac.ml4   | 42 +++++++++++++++++++++++++++++++++++++++++-
 parsing/g_vernac.ml4 | 44 ++------------------------------------------
 2 files changed, 43 insertions(+), 43 deletions(-)

(limited to 'parsing')

diff --git a/parsing/g_ltac.ml4 b/parsing/g_ltac.ml4
index e4ca936a69..35a9fede1b 100644
--- a/parsing/g_ltac.ml4
+++ b/parsing/g_ltac.ml4
@@ -6,6 +6,7 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
+open Util
 open Pp
 open Compat
 open Constrexpr
@@ -36,11 +37,35 @@ let reference_to_id = function
       Errors.user_err_loc (loc, "",
         str "This expression should be a simple identifier.")
 
+let tactic_mode = Gram.entry_create "vernac:tactic_command"
+let selector = Gram.entry_create "vernac:selector"
+
+(* Registers the Classic Proof Mode (which uses [tactic_mode] as a parser for
+    proof editing and changes nothing else). Then sets it as the default proof mode. *)
+let _ =
+  let mode = {
+    Proof_global.name = "Classic";
+    set = (fun () -> set_command_entry tactic_mode);
+    reset = (fun () -> set_command_entry Pcoq.Vernac_.noedit_mode);
+  } in
+  Proof_global.register_proof_mode mode
+
+(* Hack to parse "[ id" without dropping [ *)
+let test_bracket_ident =
+  Gram.Entry.of_parser "test_bracket_ident"
+    (fun strm ->
+      match get_tok (stream_nth 0 strm) with
+        | KEYWORD "[" ->
+            (match get_tok (stream_nth 1 strm) with
+              | IDENT _ -> ()
+	      | _ -> raise Stream.Failure)
+	| _ -> raise Stream.Failure)
+
 (* Tactics grammar rules *)
 
 GEXTEND Gram
   GLOBAL: tactic tacdef_body tactic_expr binder_tactic tactic_arg
-          constr_may_eval constr_eval;
+          tactic_mode constr_may_eval constr_eval selector;
 
   tactic_then_last:
     [ [ "|"; lta = LIST0 OPT tactic_expr SEP "|" ->
@@ -262,4 +287,19 @@ GEXTEND Gram
   tactic:
     [ [ tac = tactic_expr -> tac ] ]
   ;
+  selector:
+    [ [ n=natural; ":" -> Vernacexpr.SelectNth n
+      | test_bracket_ident; "["; id = ident; "]"; ":" -> Vernacexpr.SelectId id
+      | IDENT "all" ; ":" -> Vernacexpr.SelectAll
+      | IDENT "par" ; ":" -> Vernacexpr.SelectAllParallel ] ]
+  ;
+  tactic_mode:
+    [ [ g = OPT selector;
+        tac = G_vernac.subgoal_command -> tac g
+      | g = OPT selector; info = OPT [IDENT "Info";n=natural -> n];
+        tac = Tactic.tactic; use_dft_tac = [ "." -> false | "..." -> true ] ->
+        let g = Option.default (Proof_global.get_default_goal_selector ()) g in
+        Vernacexpr.VernacSolve (g, info, tac, use_dft_tac)
+    ] ]
+  ;
   END
diff --git a/parsing/g_vernac.ml4 b/parsing/g_vernac.ml4
index 2eb590132a..c89238d296 100644
--- a/parsing/g_vernac.ml4
+++ b/parsing/g_vernac.ml4
@@ -34,7 +34,6 @@ let _ = List.iter Lexer.add_keyword vernac_kw
 
 let query_command = Gram.entry_create "vernac:query_command"
 
-let tactic_mode = Gram.entry_create "vernac:tactic_command"
 let subprf = Gram.entry_create "vernac:subprf"
 
 let class_rawexpr = Gram.entry_create "vernac:class_rawexpr"
@@ -47,16 +46,6 @@ let subgoal_command = Gram.entry_create "proof_mode:subgoal_command"
 let instance_name = Gram.entry_create "vernac:instance_name"
 let section_subset_expr = Gram.entry_create "vernac:section_subset_expr"
 
-(* Registers the Classic Proof Mode (which uses [tactic_mode] as a parser for
-    proof editing and changes nothing else). Then sets it as the default proof mode. *)
-let set_tactic_mode () = set_command_entry tactic_mode
-let set_noedit_mode () = set_command_entry noedit_mode
-let _ = Proof_global.register_proof_mode {Proof_global.
-					    name = "Classic" ;
-					    set = set_tactic_mode ;
-					    reset = set_noedit_mode
-					 }
-
 let make_bullet s =
   let n = String.length s in
   match s.[0] with
@@ -65,19 +54,8 @@ let make_bullet s =
   | '*' -> Star n
   | _ -> assert false
 
-(* Hack to parse "[ id" without dropping [ *)
-let test_bracket_ident =
-  Gram.Entry.of_parser "test_bracket_ident"
-    (fun strm ->
-      match get_tok (stream_nth 0 strm) with
-        | KEYWORD "[" ->
-            (match get_tok (stream_nth 1 strm) with
-              | IDENT _ -> ()
-	      | _ -> raise Stream.Failure)
-	| _ -> raise Stream.Failure)
-
 GEXTEND Gram
-  GLOBAL: vernac gallina_ext tactic_mode noedit_mode subprf subgoal_command;
+  GLOBAL: vernac gallina_ext noedit_mode subprf subgoal_command;
   vernac: FIRST
     [ [ IDENT "Time"; c = located_vernac -> VernacTime c
       | IDENT "Redirect"; s = ne_string; c = located_vernac -> VernacRedirect (s, c)
@@ -125,18 +103,6 @@ GEXTEND Gram
     [ [ c = subgoal_command -> c None] ]
   ;
 
-  selector:
-    [ [ n=natural; ":" -> SelectNth n
-      | test_bracket_ident; "["; id = ident; "]"; ":" -> SelectId id
-      | IDENT "all" ; ":" -> SelectAll
-      | IDENT "par" ; ":" -> SelectAllParallel ] ]
-  ;
-
-  tactic_mode:
-  [ [ gln = OPT selector;
-      tac = subgoal_command -> tac gln ] ]
-  ;
-
   subprf:
   [ [ s = BULLET -> VernacBullet (make_bullet s)
     | "{" -> VernacSubproof None
@@ -151,13 +117,7 @@ GEXTEND Gram
                     | None -> c None
                     | _ ->
                         VernacError (UserError ("",str"Typing and evaluation commands, cannot be used with the \"all:\" selector."))
-                  end
-      | info = OPT [IDENT "Info";n=natural -> n];
-        tac = Tactic.tactic;
-        use_dft_tac = [ "." -> false | "..." -> true ] ->
-        (fun g ->
-            let g = Option.default (Proof_global.get_default_goal_selector ()) g in
-            VernacSolve(g,info,tac,use_dft_tac)) ] ]
+                  end ] ]
   ;
   located_vernac:
     [ [ v = vernac -> !@loc, v ] ]
-- 
cgit v1.2.3


From ce2ffd090bd64963279cbbb84012d1b266ed9918 Mon Sep 17 00:00:00 2001
From: Pierre-Marie Pédrot
Date: Sat, 19 Mar 2016 01:43:29 +0100
Subject: Moving VernacSolve to an EXTEND-based definition.

---
 parsing/g_ltac.ml4 | 86 +++++++++++++++++++++++++++++++++++++++++++++++-------
 1 file changed, 76 insertions(+), 10 deletions(-)

(limited to 'parsing')

diff --git a/parsing/g_ltac.ml4 b/parsing/g_ltac.ml4
index 35a9fede1b..79392195fb 100644
--- a/parsing/g_ltac.ml4
+++ b/parsing/g_ltac.ml4
@@ -6,6 +6,8 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
+(*i camlp4deps: "grammar/grammar.cma" i*)
+
 open Util
 open Pp
 open Compat
@@ -38,7 +40,14 @@ let reference_to_id = function
         str "This expression should be a simple identifier.")
 
 let tactic_mode = Gram.entry_create "vernac:tactic_command"
-let selector = Gram.entry_create "vernac:selector"
+
+let new_entry name =
+  let e = Gram.entry_create name in
+  let entry = Entry.create name in
+  let () = Pcoq.set_grammar entry e in
+  e
+
+let selector = new_entry "vernac:selector"
 
 (* Registers the Classic Proof Mode (which uses [tactic_mode] as a parser for
     proof editing and changes nothing else). Then sets it as the default proof mode. *)
@@ -290,16 +299,73 @@ GEXTEND Gram
   selector:
     [ [ n=natural; ":" -> Vernacexpr.SelectNth n
       | test_bracket_ident; "["; id = ident; "]"; ":" -> Vernacexpr.SelectId id
-      | IDENT "all" ; ":" -> Vernacexpr.SelectAll
-      | IDENT "par" ; ":" -> Vernacexpr.SelectAllParallel ] ]
+      | IDENT "all" ; ":" -> Vernacexpr.SelectAll ] ]
   ;
   tactic_mode:
-    [ [ g = OPT selector;
-        tac = G_vernac.subgoal_command -> tac g
-      | g = OPT selector; info = OPT [IDENT "Info";n=natural -> n];
-        tac = Tactic.tactic; use_dft_tac = [ "." -> false | "..." -> true ] ->
-        let g = Option.default (Proof_global.get_default_goal_selector ()) g in
-        Vernacexpr.VernacSolve (g, info, tac, use_dft_tac)
-    ] ]
+    [ [ g = OPT selector; tac = G_vernac.subgoal_command -> tac g ] ]
   ;
   END
+
+open Stdarg
+open Constrarg
+open Vernacexpr
+open Vernac_classifier
+
+let print_info_trace = ref None
+
+let _ = let open Goptions in declare_int_option {
+  optsync = true;
+  optdepr = false;
+  optname = "print info trace";
+  optkey = ["Info" ; "Level"];
+  optread = (fun () -> !print_info_trace);
+  optwrite = fun n -> print_info_trace := n;
+}
+
+let vernac_solve n info tcom b =
+  let status = Proof_global.with_current_proof (fun etac p ->
+    let with_end_tac = if b then Some etac else None in
+    let global = match n with SelectAll -> true | _ -> false in
+    let info = Option.append info !print_info_trace in
+    let (p,status) =
+      Pfedit.solve n info (Tacinterp.hide_interp global tcom None) ?with_end_tac p
+    in
+    (* in case a strict subtree was completed,
+       go back to the top of the prooftree *)
+    let p = Proof.maximal_unfocus Vernacentries.command_focus p in
+    p,status) in
+    if not status then Pp.feedback Feedback.AddedAxiom
+
+let pr_ltac_selector = function
+| SelectNth i -> int i ++ str ":"
+| SelectId id -> str "[" ++ Nameops.pr_id id ++ str "]" ++ str ":"
+| SelectAll -> str "all" ++ str ":"
+
+VERNAC ARGUMENT EXTEND ltac_selector PRINTED BY pr_ltac_selector
+| [ selector(s) ] -> [ s ]
+END
+
+let pr_ltac_info n = str "Info" ++ spc () ++ int n
+
+VERNAC ARGUMENT EXTEND ltac_info PRINTED BY pr_ltac_info
+| [ "Info" natural(n) ] -> [ n ]
+END
+
+let pr_ltac_use_default b = if b then str ".." else mt ()
+
+VERNAC ARGUMENT EXTEND ltac_use_default PRINTED BY pr_ltac_use_default
+| [ "." ] -> [ false ]
+| [ "..." ] -> [ true ]
+END
+
+VERNAC tactic_mode EXTEND VernacSolve
+| [ - ltac_selector_opt(g) ltac_info_opt(n) tactic(t) ltac_use_default(def) ] =>
+    [ classify_as_proofstep ] -> [
+    let g = Option.default (Proof_global.get_default_goal_selector ()) g in
+    vernac_solve g n t def
+  ]
+| [ - "par" ":" ltac_info_opt(n) tactic(t) ltac_use_default(def) ] =>
+    [ VtProofStep true, VtLater ] -> [
+    vernac_solve SelectAll n t def
+  ]
+END
-- 
cgit v1.2.3