- moved command as sub-entries of tactical grammars (as per tactics)

[helm.git] / helm / ocaml / cic_disambiguation / cicTextualParser2.ml

diff --git a/helm/ocaml/cic_disambiguation/cicTextualParser2.ml b/helm/ocaml/cic_disambiguation/cicTextualParser2.ml
index f0de0b521b888593faaedf5468c12f0f9d9f715b..8eca106304e96def0c883fa11885889751abcfcd 100644 (file)
--- a/helm/ocaml/cic_disambiguation/cicTextualParser2.ml
+++ b/helm/ocaml/cic_disambiguation/cicTextualParser2.ml
@@ -36,14 +36,10 @@ let debug_print s =
 let use_fresh_num_instances = false
 
 open Printf
+open DisambiguateTypes
 
 exception Parse_error of string
 
-type tactic = (CicAst.term, string) TacticAst.tactic
-type tactical = (CicAst.term, string) TacticAst.tactic TacticAst.tactical
-type command = CicAst.term CommandAst.command
-type script = CicAst.term CommandAst.Script.script
-
 let fresh_num_instance =
   let n = ref 0 in
   if use_fresh_num_instances then
@@ -63,13 +59,11 @@ let tactic = Grammar.Entry.create grammar "tactic"
 let tactical = Grammar.Entry.create grammar "tactical"
 let tactical0 = Grammar.Entry.create grammar "tactical0"
 let command = Grammar.Entry.create grammar "command"
-let script = Grammar.Entry.create grammar "script"
 
 let return_term loc term = CicAst.AttributedTerm (`Loc loc, term)
 let return_tactic loc tactic = TacticAst.LocatedTactic (loc, tactic)
 let return_tactical loc tactical = TacticAst.LocatedTactical (loc, tactical)
 let return_command loc cmd = cmd
-let return_script loc script = script
 
 let fail (x, y) msg =
   failwith (Printf.sprintf "Error at characters %d - %d: %s" x y msg)
@@ -79,7 +73,7 @@ let name_of_string = function
   | s -> Cic.Name s
 
 EXTEND
-  GLOBAL: term term0 tactic tactical tactical0 command script;
+  GLOBAL: term term0 tactic tactical tactical0 command;
   int: [
     [ num = NUM ->
         try
@@ -335,6 +329,7 @@ EXTEND
       | [ IDENT "id" | IDENT "Id" ] -> return_tactical loc TacticAst.IdTac
       | PAREN "("; tac = tactical; PAREN ")" -> return_tactical loc tac
       | tac = tactic -> return_tactical loc (TacticAst.Tactic tac)
+      | cmd = command -> return_tactical loc (TacticAst.Command cmd)
       ]
     ];
   theorem_flavour: [  (* all flavours but Goal *)
@@ -343,73 +338,23 @@ EXTEND
     | [ IDENT "lemma"       | IDENT "Lemma"       ] -> `Lemma
     | [ IDENT "remark"      | IDENT "Remark"      ] -> `Remark
     | [ IDENT "theorem"     | IDENT "Theorem"     ] -> `Theorem
-(*     | [ IDENT "goal"        | IDENT "Goal"        ] -> `Goal *)
-    ]
-  ];
-  theorem_cmd: [
-    [ flavour = theorem_flavour; name = OPT IDENT; SYMBOL ":"; typ = term;
-      body = OPT [ SYMBOL <:unicode<def>> (* ≝ *); body = term -> body ];
-      SYMBOL "." ->
-        (loc, flavour, name, typ, body)
-    | [ IDENT "goal" | IDENT "Goal" ]; typ = term;
-      body = OPT [ SYMBOL <:unicode<def>> (* ≝ *); body = term -> body ];
-      SYMBOL "." ->
-        (loc, `Goal, None, typ, body)
-    ]
-  ];
-  proof_cmd: [ [ [ IDENT "proof" | IDENT "Proof" ]; SYMBOL "." -> loc ] ];
-  qed_cmd: [
-    [ [ IDENT "qed" | IDENT "Qed" ]; SYMBOL "." -> (loc, None)
-    | [ IDENT "save" | IDENT "Save" ]; name = IDENT; SYMBOL "." ->
-        (loc, Some name)
     ]
   ];
   command: [
-    [ (loc', flavour, name, typ, body) = theorem_cmd ->
-        return_command loc (CommandAst.Theorem (loc', flavour, name, typ, body))
-    | (loc') = proof_cmd -> return_command loc (CommandAst.Proof loc')
-    | (loc, name) = qed_cmd -> return_command loc (CommandAst.Qed (loc, name))
-    ]
-  ];
-  script_entry: [
-    [ theorem = theorem_cmd;
-      proof = OPT [
-        proof_cmd; tacticals = LIST1 tactical0; qed = qed_cmd ->
-          (tacticals, qed)
-      ] ->
-        let (loc', flavour, name', typ, body_verbatim) = theorem in
-        let name'' =
-          match proof with
-          | None | Some (_, (_, None)) -> None
-          | Some (_, (_, Some name)) -> Some name
-        in
-        let name =
-          match (name', name'') with
-          | Some name, None -> name
-          | None, Some name -> name
-          | None, None ->
-              Stdpp.raise_with_loc loc (Failure "theorem's name is missing")
-          | Some name', Some name'' when name' <> name'' ->
-              Stdpp.raise_with_loc loc (Failure (sprintf
-                "theorem's name mismatch: %s <> %s" name' name''))
-          | Some name, _ -> name
-        in
-        let body =
-          match (body_verbatim, proof) with
-          | Some term, None -> CommandAst.Script.Verbatim (loc', term)
-          | None, Some (tacticals, (loc'', _)) ->
-              CommandAst.Script.Tactics (loc'', tacticals)
-          | Some _, Some _ ->
-              Stdpp.raise_with_loc loc (Failure (sprintf
-                "theorem %s has too many proofs" name))
-          | None, None ->
-              Stdpp.raise_with_loc loc (Failure (sprintf
-                "theorem %s has no proof" name))
-        in
-        return_script loc (CommandAst.Script.Theorem (flavour, name, typ, body))
+    [ [ IDENT "proof" | IDENT "Proof" ] -> return_command loc TacticAst.Proof
+    | [ IDENT "quit"  | IDENT "Quit"  ] -> return_command loc TacticAst.Quit
+    | [ IDENT "qed"   | IDENT "Qed"   ] ->
+        return_command loc (TacticAst.Qed None)
+    | [ IDENT "save"  | IDENT "Save"  ]; name = IDENT ->
+        return_command loc (TacticAst.Qed (Some name))
+    | flavour = theorem_flavour; name = OPT IDENT; SYMBOL ":"; typ = term;
+      body = OPT [ SYMBOL <:unicode<def>> (* ≝ *); body = term -> body ] ->
+        return_command loc (TacticAst.Theorem (flavour, name, typ, body))
+    | [ IDENT "goal" | IDENT "Goal" ]; typ = term;
+      body = OPT [ SYMBOL <:unicode<def>> (* ≝ *); body = term -> body ] ->
+        return_command loc (TacticAst.Theorem (`Goal, None, typ, body))
     ]
   ];
-  script: [ [ entries = LIST0 script_entry; EOI -> entries ] ];
 END
 
 let exc_located_wrapper f =
@@ -425,17 +370,11 @@ let parse_tactic stream =
   exc_located_wrapper (lazy (Grammar.Entry.parse tactic stream))
 let parse_tactical stream =
   exc_located_wrapper (lazy (Grammar.Entry.parse tactical0 stream))
-let parse_command stream =
-  exc_located_wrapper (lazy (Grammar.Entry.parse command stream))
-let parse_script stream =
-  exc_located_wrapper (lazy (Grammar.Entry.parse script stream))
 
 (**/**)
 
 (** {2 Interface for gTopLevel} *)
 
-open DisambiguateTypes
-
 module EnvironmentP3 =
   struct
     type t = environment