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   ~(proof_handler: MatitaTypes.proof_handler)
  38   ~(console: MatitaConsole.console)
  39   ()
  40 =
  41   object
  42     method evalPhrase s: state_tag =
  43       let command = CicTextualParser2.parse_command (Stream.of_string s) in
  44       match command with
  45       | CommandAst.Theorem (_, _, Some name, ast, None) ->
  46           let (_, metasenv, expr) = disambiguator#disambiguateTermAst ast in
  47           let _  = CicTypeChecker.type_of_aux' metasenv [] expr in
  48           let proof = MatitaProof.proof ~typ:expr ~metasenv () in
  49           proof_handler.MatitaTypes.new_proof proof;
  50           `Proof
  51       | CommandAst.Quit _ ->
  52           proof_handler.MatitaTypes.quit ();
  53           `Command (* dummy answer *)
  54       | _ ->
  55           MatitaTypes.not_implemented (* TODO Zack *)
  56             "MatitaInterpreter.commandState#evalPhrase: commands other than full theorem ones";
  57           `Proof
  58   end
  59
  60   (* TODO Zack FINQUI
  61   * bisogna rivedere la grammatica di tatticali/comandi
  62   * molti comandi (o addirittura tutti tranne Theorem) hanno senso anche nello
  63   * stato proof, e' quindi un casino parsare la phrase. Un'idea potrebbe essere
  64   * quella di tentare di parsare una tattica e se il parsing fallisce provare a
  65   * parsare un comando (BLEAARGH). Oppure si puo' aggiungere una possibile entry
  66   * nella grammatica delle tattiche che punti ad un comando (RI-BLEAARGH).
  67   * Oppure boh ...
  68   *)
  69 class proofState
  70   ~(disambiguator: MatitaTypes.disambiguator)
  71   ~(proof_handler: MatitaTypes.proof_handler)
  72   ~(console: MatitaConsole.console)
  73   ()
  74 =
  75   object
  76     method evalPhrase (s: string): state_tag =
  77       (* TODO Zack *)
  78       MatitaTypes.not_implemented "MatitaInterpreter.proofState#evalPhrase";
  79       `Command
  80   end
  81
  82 class interpreter
  83   ~(disambiguator: MatitaTypes.disambiguator)
  84   ~(proof_handler: MatitaTypes.proof_handler)
  85   ~(console: MatitaConsole.console)
  86   ()
  87 =
  88   let commandState =
  89     lazy (new commandState ~disambiguator ~proof_handler ~console ())
  90   in
  91   let proofState =
  92     lazy (new proofState ~disambiguator ~proof_handler ~console ())
  93   in
  94   object
  95     val mutable state = Lazy.force commandState
  96
  97     method evalPhrase s =
  98       match state#evalPhrase s with
  99       | `Command -> state <- Lazy.force commandState
 100       | `Proof -> state <- Lazy.force proofState
 101   end
 102