* 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
~(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
()
=
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