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