helm/matita/matitaInterpreter.ml

   1 (* Copyright (C) 2004, HELM Team.
   2  *
   3  * This file is part of HELM, an Hypertextual, Electronic
   4  * Library of Mathematics, developed at the Computer Science
   5  * Department, University of Bologna, Italy.
   6  *
   7  * HELM is free software; you can redistribute it and/or
   8  * modify it under the terms of the GNU General Public License
   9  * as published by the Free Software Foundation; either version 2
  10  * of the License, or (at your option) any later version.
  11  *
  12  * HELM is distributed in the hope that it will be useful,
  13  * but WITHOUT ANY WARRANTY; without even the implied warranty of
  14  * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE.  See the
  15  * GNU General Public License for more details.
  16  *
  17  * You should have received a copy of the GNU General Public License
  18  * along with HELM; if not, write to the Free Software
  19  * Foundation, Inc., 59 Temple Place - Suite 330, Boston,
  20  * MA  02111-1307, USA.
  21  *
  22  * For details, see the HELM World-Wide-Web page,
  23  * http://helm.cs.unibo.it/
  24  *)
  25
  26 open Printf
  27
  28 type state_tag = [ `Command | `Proof ]
  29
  30 exception Command_not_found of string
  31
  32 class virtual interpreterState ~(console: MatitaConsole.console) =
  33   object (self)
  34       (** eval a toplevel phrase in the current state and return the new state
  35       *)
  36     method parsePhrase s = CicTextualParser2.parse_tactical (Stream.of_string s)
  37
  38     method virtual evalTactical:
  39       (CicAst.term, string) TacticAst.tactical -> state_tag
  40
  41     method evalPhrase s = self#evalTactical (self#parsePhrase s)
  42   end
  43
  44 class commandState
  45   ~(disambiguator: MatitaTypes.disambiguator)
  46   ~(proof_handler: MatitaTypes.proof_handler)
  47   ~(console: MatitaConsole.console)
  48   ()
  49 =
  50   object (self)
  51     inherit interpreterState ~console
  52
  53     method evalTactical = function
  54 (*
  55       | TacticAst.Command _ -> failwith "1"
  56       | TacticAst.Tactic _ -> failwith "2"
  57       | TacticAst.LocatedTactical _ -> failwith "3"
  58       | TacticAst.Fail -> failwith "4"
  59       | TacticAst.Do (_, _) -> failwith "5"
  60       | TacticAst.IdTac -> failwith "6"
  61       | TacticAst.Repeat _ -> failwith "7"
  62       | TacticAst.Seq _ -> failwith "8"
  63       | TacticAst.Then (_, _) -> failwith "9"
  64       | TacticAst.Tries _ -> failwith "10"
  65       | TacticAst.Try _ -> failwith "11"
  66 *)
  67       | TacticAst.LocatedTactical (_, tactical) -> self#evalTactical tactical
  68       | TacticAst.Command (TacticAst.Theorem (_, Some name, ast, None)) ->
  69           let (_, metasenv, expr) = disambiguator#disambiguateTermAst ast in
  70           let _  = CicTypeChecker.type_of_aux' metasenv [] expr in
  71           let proof = MatitaProof.proof ~typ:expr ~metasenv () in
  72           proof_handler.MatitaTypes.new_proof proof;
  73           `Proof
  74       | TacticAst.Command TacticAst.Quit ->
  75           proof_handler.MatitaTypes.quit ();
  76           `Command (* dummy answer, useless *)
  77       | TacticAst.Command TacticAst.Proof ->
  78             (* do nothing, just for compatibility with coq syntax *)
  79           `Command
  80       | tactical ->
  81           raise (Command_not_found (TacticAstPp.pp_tactical tactical))
  82   end
  83
  84 class proofState
  85   ~(disambiguator: MatitaTypes.disambiguator)
  86   ~(proof_handler: MatitaTypes.proof_handler)
  87   ~(console: MatitaConsole.console)
  88   ()
  89 =
  90   let commandState =
  91     new commandState ~disambiguator ~proof_handler ~console ()
  92   in
  93   object
  94     inherit interpreterState ~console
  95
  96     method evalTactical = function
  97       | TacticAst.Command TacticAst.Abort ->
  98           proof_handler.MatitaTypes.set_proof None;
  99           `Command
 100       | tactical -> (* fallback on command state *)
 101           commandState#evalTactical tactical
 102   end
 103
 104 class interpreter
 105   ~(disambiguator: MatitaTypes.disambiguator)
 106   ~(proof_handler: MatitaTypes.proof_handler)
 107   ~(console: MatitaConsole.console)
 108   ()
 109 =
 110   let commandState =
 111     new commandState ~disambiguator ~proof_handler ~console ()
 112   in
 113   let proofState = new proofState ~disambiguator ~proof_handler ~console () in
 114   object
 115     val mutable state = commandState
 116
 117     method evalPhrase s =
 118       try
 119         (match state#evalPhrase s with
 120         | `Command -> state <- commandState
 121         | `Proof -> state <- proofState)
 122       with exn ->
 123         console#echo_error (sprintf "Uncaught exception: %s"
 124           (Printexc.to_string exn))
 125   end
 126