1 (* Copyright (C) 2004, HELM Team.
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.
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.
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.
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,
22 * For details, see the HELM World-Wide-Web page,
23 * http://helm.cs.unibo.it/
26 (** exceptions whose content should be presented to the user *)
27 exception Not_implemented of string
28 exception Failure of string
30 val not_implemented : string -> 'a
31 val error : string -> 'a
32 val warning : string -> unit
33 val debug_print : string -> unit
35 exception No_proof (** no current proof is available *)
37 exception Unbound_identifier of string
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
44 val unopt_uri : 'a option -> 'a
46 (** {3 disambiguator callbacks} *)
48 type choose_uris_callback =
49 selection_mode:[ `MULTIPLE | `SINGLE ] ->
51 ?msg:string -> ?nonvars_button:bool -> string list -> string list
53 type choose_interp_callback = (string * string) list list -> int list
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
60 (** {2 major matita objects} *)
64 method parseTactical : char Stream.t -> DisambiguateTypes.tactical
65 method parseTerm : char Stream.t -> DisambiguateTypes.term
68 (* subset of MatitaConsole.console methods needed by MatitaInterpreter *)
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
79 class type disambiguator =
81 method env : DisambiguateTypes.environment
82 method setEnv : DisambiguateTypes.environment -> unit
84 method chooseUris: choose_uris_callback
85 method setChooseUris: choose_uris_callback -> unit
87 method chooseInterp: choose_interp_callback
88 method setChooseInterp: choose_interp_callback -> unit
90 method parserr: parserr
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 ->
104 DisambiguateTypes.environment * Cic.metasenv * Cic.term *
105 CicUniv.universe_graph
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
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
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
129 inherit [unit] StatefulProofEngine.status
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
135 method toString : string
138 class type currentProof =
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 *)
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
151 (** schematic representation of items scripts are made of *)
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 *)
160 (** interpreter for toplevel phrases given via console *)
161 class type interpreter =
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
168 method evalPhrase: string -> command_outcome
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 *)
174 (** as above, evaluating a command/tactics AST *)
175 method evalAst: DisambiguateTypes.tactical -> command_outcome
179 method setEvalAstCallback: (DisambiguateTypes.tactical -> unit) -> unit
181 (** {3 stateful methods}
182 * bookkeeping of last interpreted phrase *)
184 (** offset from the starting of the last string parser by evalPhrase where
186 * @raise Failure when no offset has been recorded *)
187 method endOffset: int
189 (** last item parsed *)
190 method lastItem: script_item option
192 (** change internal interpreter state *)
193 method setState: [`Proof | `Command] -> unit
197 (** {2 MathML widgets} *)
200 [ `Ast of DisambiguateTypes.term
201 | `Cic of Cic.term * Cic.metasenv
205 class type mathViewer =
207 method checkTerm: term_source -> unit
210 class type cicBrowser =
212 method loadUri: string -> unit
213 method loadTerm: term_source -> unit
216 type mml_of_cic_sequent =
220 ((Cic.id, Cic.term) Hashtbl.t * (Cic.id, Cic.id option) Hashtbl.t *
221 (string, Cic.hypothesis) Hashtbl.t)
223 type mml_of_cic_object =
227 (string, string) Hashtbl.t ->
228 (string, Cic2acic.anntypes) Hashtbl.t -> Gdome.document
230 (** {2 shorthands} *)
232 type namer = ProofEngineTypes.mk_fresh_name_type