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 type state_tag = [ `Command | `Proof ]
  27
  28 class type interpreterState =
  29   object
  30       (** eval a toplevel phrase in the current state and return the new state
  31       *)
  32     method evalPhrase: string -> state_tag
  33   end
  34
  35 class commandState
  36   ~(disambiguator: MatitaTypes.disambiguator)
  37   ~(console: MatitaConsole.console)
  38   ~new_proof ()
  39 =
  40   object
  41     method evalPhrase s: state_tag =
  42       let command = CicTextualParser2.parse_command (Stream.of_string s) in
  43       match command with
  44       | CommandAst.Theorem (_, _, Some name, ast, None) ->
  45           let (_, metasenv, expr) = disambiguator#disambiguateTermAst ast in
  46           let _  = CicTypeChecker.type_of_aux' metasenv [] expr in
  47           let proof = MatitaProof.proof ~typ:expr ~metasenv () in
  48           new_proof proof;
  49           `Proof
  50       | _ ->
  51           MatitaTypes.not_implemented (* TODO Zack *)
  52             "MatitaInterpreter.commandState#evalPhrase: commands other than full theorem ones";
  53           `Proof
  54   end
  55
  56 class proofState
  57   ~(disambiguator: MatitaTypes.disambiguator)
  58   ~(console: MatitaConsole.console)
  59   ~get_proof ()
  60 =
  61   object
  62     method evalPhrase (s: string): state_tag =
  63       (* TODO Zack *)
  64       MatitaTypes.not_implemented "MatitaInterpreter.proofState#evalPhrase";
  65       `Command
  66   end
  67
  68 class interpreter
  69   ~(disambiguator: MatitaTypes.disambiguator)
  70   ~(console: MatitaConsole.console)
  71   ~(get_proof: unit -> MatitaTypes.proof)
  72   ~(new_proof: MatitaTypes.proof -> unit)
  73   ()
  74 =
  75   let commandState =
  76     lazy (new commandState ~disambiguator ~console ~new_proof ())
  77   in
  78   let proofState =
  79     lazy (new proofState ~disambiguator ~console ~get_proof ())
  80   in
  81   object
  82     val mutable state = Lazy.force commandState
  83
  84     method evalPhrase s =
  85       match state#evalPhrase s with
  86       | `Command -> state <- Lazy.force commandState
  87       | `Proof -> state <- Lazy.force proofState
  88   end
  89