helm/matita/matitaTypes.mli

   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   (** exceptions whose content should be presented to the user *)
  27 exception Not_implemented of string
  28 exception Failure of string
  29
  30 val not_implemented : string -> 'a
  31 val error : string -> 'a
  32 val warning : string -> unit
  33 val debug_print : string -> unit
  34
  35 exception No_proof  (** no current proof is available *)
  36 exception Cancel
  37 exception Unbound_identifier of string
  38
  39   (** @param exn an exception
  40   * @return a string which is meant to be a textual explaination of the
  41    exception understandable by a user *)
  42 val explain: exn -> string
  43
  44 val unopt_uri : 'a option -> 'a
  45
  46   (** {3 disambiguator callbacks} *)
  47
  48 type choose_uris_callback =
  49   selection_mode:[ `MULTIPLE | `SINGLE ] ->
  50   ?title:string ->
  51   ?msg:string -> ?nonvars_button:bool -> string list -> string list
  52
  53 type choose_interp_callback = (string * string) list list -> int list
  54
  55   (** @raise Failure if called, use if unambiguous input is required *)
  56 val mono_uris_callback: choose_uris_callback
  57   (** @raise Failure if called, use if unambiguous input is required *)
  58 val mono_interp_callback: choose_interp_callback
  59
  60 (** {2 major matita objects} *)
  61
  62 class type parserr =
  63   object
  64     method parseTactical : char Stream.t -> DisambiguateTypes.tactical
  65     method parseTerm : char Stream.t -> DisambiguateTypes.term
  66   end
  67
  68   (* subset of MatitaConsole.console methods needed by MatitaInterpreter *)
  69 class type console =
  70   object
  71     method clear : unit -> unit
  72     method echo_error : string -> unit
  73     method echo_message : string -> unit
  74     method wrap_exn : 'a. (unit -> 'a) -> 'a option
  75     method choose_uri : string list -> string
  76     method show : ?msg:string -> unit -> unit
  77   end
  78
  79 class type disambiguator =
  80   object
  81     method env : DisambiguateTypes.environment
  82     method setEnv : DisambiguateTypes.environment -> unit
  83
  84     method chooseUris: choose_uris_callback
  85     method setChooseUris: choose_uris_callback -> unit
  86
  87     method chooseInterp: choose_interp_callback
  88     method setChooseInterp: choose_interp_callback -> unit
  89
  90     method parserr: parserr
  91
  92       (* TODO Zack: as long as matita doesn't support MDI inteface,
  93       * disambiguateTerm will return a single term *)
  94       (** @param env disambiguation environment. If this parameter is given the
  95       * disambiguator act statelessly, that is internal disambiguation status
  96       * want be changed but only returned. If this parameter is not given the
  97       * internal one will be used and updated with the disambiguation status
  98       * resulting from the disambiguation *)
  99     method disambiguateTerm :
 100       ?context:Cic.context ->
 101       ?metasenv:Cic.metasenv ->
 102       ?env:DisambiguateTypes.environment ->
 103       char Stream.t ->
 104       DisambiguateTypes.environment * Cic.metasenv * Cic.term *
 105       CicUniv.universe_graph
 106
 107       (** @param env @see disambiguateTerm above *)
 108     method disambiguateTermAst :
 109       ?context:Cic.context ->
 110       ?metasenv:Cic.metasenv ->
 111       ?env:DisambiguateTypes.environment ->
 112       DisambiguateTypes.term ->
 113       DisambiguateTypes.environment * Cic.metasenv * Cic.term *
 114       CicUniv.universe_graph
 115
 116       (** as disambiguateTermAst, but disambiguate a list of ASTs at once. All
 117       * AST should be closed hence no context param is permitted on this method
 118       *)
 119     method disambiguateTermAsts :
 120       ?metasenv:Cic.metasenv ->
 121       ?env:DisambiguateTypes.environment ->
 122       DisambiguateTypes.term list ->
 123       DisambiguateTypes.environment * Cic.metasenv * Cic.term list *
 124       CicUniv.universe_graph
 125   end
 126
 127 class type proof =
 128   object
 129     inherit [unit] StatefulProofEngine.status
 130
 131     (** return a pair of "xml" (as defined in Xml module) representing the *
 132      * current proof type and body, respectively *)
 133     method toXml : Xml.token Stream.t * Xml.token Stream.t
 134
 135     method toString : string
 136   end
 137
 138 class type currentProof =
 139   object
 140     method onGoing: unit -> bool  (** true if a proof is on going *)
 141     method proof: proof           (** @raise Failure "No current proof" *)
 142     method start: proof -> unit   (** starts a new proof *)
 143     method abort: unit -> unit    (** abort the on going proof *)
 144     method quit: unit -> unit     (** quit matita *)
 145   end
 146
 147   (** first component represents success: true = success, false = failure
 148   * second component represents console action: true = hide, false = keep *)
 149 type command_outcome = bool * bool
 150
 151   (** schematic representation of items scripts are made of *)
 152 type script_item =
 153   [ `Tactic                       (** action on proof status *)
 154   | `Theorem                      (** start of proof, to be proved *)
 155   | `Qed of UriManager.uri        (** end of proof, successfull *)
 156   | `Def of UriManager.uri        (** constant with body *)
 157   | `Inductive of UriManager.uri  (** inductive definition *)
 158   ]
 159
 160   (** interpreter for toplevel phrases given via console *)
 161 class type interpreter =
 162   object
 163       (** parse a single phrase contained in the input string. Additional
 164       * garbage at the end of the phrase is ignored
 165       * @return true if no exception has been raised by the evaluation, false
 166       * otherwise
 167       *)
 168     method evalPhrase: string -> command_outcome
 169
 170       (** as evalPhrase above, but parses a character stream. Only characters
 171       * composing next phrases are consumed *)
 172 (*     method evalStream: char Stream.t -> command_outcome *)
 173
 174       (** as above, evaluating a command/tactics AST *)
 175     method evalAst: DisambiguateTypes.tactical -> command_outcome
 176
 177     (** {3 callbacks} *)
 178
 179     method setEvalAstCallback: (DisambiguateTypes.tactical -> unit) -> unit
 180
 181     (** {3 stateful methods}
 182      * bookkeeping of last interpreted phrase *)
 183
 184       (** offset from the starting of the last string parser by evalPhrase where
 185       * parsing stop.
 186       * @raise Failure when no offset has been recorded *)
 187     method endOffset: int
 188
 189       (** last item parsed *)
 190     method lastItem: script_item option
 191
 192       (** change internal interpreter state *)
 193     method setState: [`Proof | `Command] -> unit
 194
 195   end
 196
 197 (** {2 MathML widgets} *)
 198
 199 type term_source =
 200   [ `Ast of DisambiguateTypes.term
 201   | `Cic of Cic.term
 202   | `String of string
 203   ]
 204
 205 class type mathViewer =
 206   object
 207     method checkTerm: term_source -> unit
 208   end
 209
 210 class type cicBrowser =
 211   object
 212     method loadUri: string -> unit
 213     method loadTerm: term_source -> unit
 214   end
 215
 216 type mml_of_cic_sequent =
 217   Cic.metasenv ->
 218   Cic.conjecture ->
 219   Gdome.document *
 220   ((Cic.id, Cic.term) Hashtbl.t * (Cic.id, Cic.id option) Hashtbl.t *
 221    (string, Cic.hypothesis) Hashtbl.t)
 222
 223 type mml_of_cic_object =
 224   explode_all:bool ->
 225   UriManager.uri ->
 226   Cic.annobj ->
 227   (string, string) Hashtbl.t ->
 228   (string, Cic2acic.anntypes) Hashtbl.t -> Gdome.document
 229
 230 (** {2 shorthands} *)
 231
 232 type namer = ProofEngineTypes.mk_fresh_name_type
 233