snapshot (notably: first working version of the console)

[helm.git] / helm / matita / matitaInterpreter.ml

diff --git a/helm/matita/matitaInterpreter.ml b/helm/matita/matitaInterpreter.ml
index 4b87ec8f808012fcac907889e7484b4089dd18d5..f5dd123f53ef6a18c6e29a43c7a9587621d7888e 100644 (file)
--- a/helm/matita/matitaInterpreter.ml
+++ b/helm/matita/matitaInterpreter.ml
@@ -23,13 +23,22 @@
  * http://helm.cs.unibo.it/
  *)
 
+open Printf
+
 type state_tag = [ `Command | `Proof ]
 
-class type interpreterState =
-  object
+exception Command_not_found of string
+
+class virtual interpreterState ~(console: MatitaConsole.console) =
+  object (self)
       (** eval a toplevel phrase in the current state and return the new state
       *)
-    method evalPhrase: string -> state_tag
+    method parsePhrase s = CicTextualParser2.parse_tactical (Stream.of_string s)
+
+    method virtual evalTactical:
+      (CicAst.term, string) TacticAst.tactical -> state_tag
+
+    method evalPhrase s = self#evalTactical (self#parsePhrase s)
   end
 
 class commandState
@@ -38,45 +47,58 @@ class commandState
   ~(console: MatitaConsole.console)
   ()
 =
-  object
-    method evalPhrase s: state_tag =
-      let command = CicTextualParser2.parse_command (Stream.of_string s) in
-      match command with
-      | CommandAst.Theorem (_, _, Some name, ast, None) ->
+  object (self)
+    inherit interpreterState ~console
+
+    method evalTactical = function
+(*
+      | TacticAst.Command _ -> failwith "1"
+      | TacticAst.Tactic _ -> failwith "2"
+      | TacticAst.LocatedTactical _ -> failwith "3"
+      | TacticAst.Fail -> failwith "4"
+      | TacticAst.Do (_, _) -> failwith "5"
+      | TacticAst.IdTac -> failwith "6"
+      | TacticAst.Repeat _ -> failwith "7"
+      | TacticAst.Seq _ -> failwith "8"
+      | TacticAst.Then (_, _) -> failwith "9"
+      | TacticAst.Tries _ -> failwith "10"
+      | TacticAst.Try _ -> failwith "11"
+*)
+      | TacticAst.LocatedTactical (_, tactical) -> self#evalTactical tactical
+      | TacticAst.Command (TacticAst.Theorem (_, Some name, ast, None)) ->
           let (_, metasenv, expr) = disambiguator#disambiguateTermAst ast in
           let _  = CicTypeChecker.type_of_aux' metasenv [] expr in
           let proof = MatitaProof.proof ~typ:expr ~metasenv () in
           proof_handler.MatitaTypes.new_proof proof;
           `Proof
-      | CommandAst.Quit _ ->
+      | TacticAst.Command TacticAst.Quit ->
           proof_handler.MatitaTypes.quit ();
-          `Command (* dummy answer *)
-      | _ ->
-          MatitaTypes.not_implemented (* TODO Zack *)
-            "MatitaInterpreter.commandState#evalPhrase: commands other than full theorem ones";
-          `Proof
+          `Command (* dummy answer, useless *)
+      | TacticAst.Command TacticAst.Proof ->
+            (* do nothing, just for compatibility with coq syntax *)
+          `Command
+      | tactical ->
+          raise (Command_not_found (TacticAstPp.pp_tactical tactical))
   end
 
-  (* TODO Zack FINQUI
-  * bisogna rivedere la grammatica di tatticali/comandi
-  * molti comandi (o addirittura tutti tranne Theorem) hanno senso anche nello
-  * stato proof, e' quindi un casino parsare la phrase. Un'idea potrebbe essere
-  * quella di tentare di parsare una tattica e se il parsing fallisce provare a
-  * parsare un comando (BLEAARGH). Oppure si puo' aggiungere una possibile entry
-  * nella grammatica delle tattiche che punti ad un comando (RI-BLEAARGH).
-  * Oppure boh ...
-  *)
 class proofState
   ~(disambiguator: MatitaTypes.disambiguator)
   ~(proof_handler: MatitaTypes.proof_handler)
   ~(console: MatitaConsole.console)
   ()
 =
+  let commandState =
+    new commandState ~disambiguator ~proof_handler ~console ()
+  in
   object
-    method evalPhrase (s: string): state_tag =
-      (* TODO Zack *)
-      MatitaTypes.not_implemented "MatitaInterpreter.proofState#evalPhrase";
-      `Command
+    inherit interpreterState ~console
+
+    method evalTactical = function
+      | TacticAst.Command TacticAst.Abort ->
+          proof_handler.MatitaTypes.set_proof None;
+          `Command
+      | tactical -> (* fallback on command state *)
+          commandState#evalTactical tactical
   end
 
 class interpreter
@@ -86,17 +108,19 @@ class interpreter
   ()
 =
   let commandState =
-    lazy (new commandState ~disambiguator ~proof_handler ~console ())
-  in
-  let proofState =
-    lazy (new proofState ~disambiguator ~proof_handler ~console ())
+    new commandState ~disambiguator ~proof_handler ~console ()
   in
+  let proofState = new proofState ~disambiguator ~proof_handler ~console () in
   object
-    val mutable state = Lazy.force commandState
+    val mutable state = commandState
 
     method evalPhrase s =
-      match state#evalPhrase s with
-      | `Command -> state <- Lazy.force commandState
-      | `Proof -> state <- Lazy.force proofState
+      try
+        (match state#evalPhrase s with
+        | `Command -> state <- commandState
+        | `Proof -> state <- proofState)
+      with exn ->
+        console#echo_error (sprintf "Uncaught exception: %s"
+          (Printexc.to_string exn))
   end