-(* Copyright (C) 2004, HELM Team.
+(* Copyright (C) 2004-2005, HELM Team.
*
* This file is part of HELM, an Hypertextual, Electronic
* Library of Mathematics, developed at the Computer Science
* http://helm.cs.unibo.it/
*)
- (** exceptions whose content should be presented to the user *)
-exception Not_implemented of string
-exception Failure of string
-
-val not_implemented : string -> 'a
-val error : string -> 'a
-val warning : string -> unit
-val debug_print : string -> unit
-
-exception No_proof (** no current proof is available *)
exception Cancel
-exception Unbound_identifier of string
-
- (** @param exn an exception
- * @return a string which is meant to be a textual explaination of the
- exception understandable by a user *)
-val explain: exn -> string
-
-val unopt_uri : 'a option -> 'a
+exception Statement_error of string
+val statement_error : string -> 'a
- (** {3 disambiguator callbacks} *)
+exception Command_error of string
+val command_error : string -> 'a
-type choose_uris_callback =
- selection_mode:[ `MULTIPLE | `SINGLE ] ->
- ?title:string ->
- ?msg:string -> ?nonvars_button:bool -> string list -> string list
-
-type choose_interp_callback = (string * string) list list -> int list
-
- (** @raise Failure if called, use if unambiguous input is required *)
-val mono_uris_callback: choose_uris_callback
- (** @raise Failure if called, use if unambiguous input is required *)
-val mono_interp_callback: choose_interp_callback
-
-(** {2 major matita objects} *)
+exception Option_error of string * string
+exception Unbound_identifier of string
-class type parserr =
- object
- method parseTactical : char Stream.t -> DisambiguateTypes.tactical
- method parseTerm : char Stream.t -> DisambiguateTypes.term
- end
+type incomplete_proof = {
+ proof: ProofEngineTypes.proof;
+ stack: Continuationals.Stack.t;
+}
+
+type proof_status =
+ No_proof
+ | Incomplete_proof of incomplete_proof
+ | Proof of ProofEngineTypes.proof
+ | Intermediate of Cic.metasenv
+
+module StringMap : Map.S with type key = String.t
+
+type option_value =
+ | String of string
+ | Int of int
+type options = option_value StringMap.t
+val no_options : 'a StringMap.t
+
+type ast_command = (CicNotationPt.term, GrafiteAst.obj) GrafiteAst.command
+type moo = ast_command list * GrafiteAst.metadata list (** <moo, metadata> *)
+
+type status = {
+ aliases: DisambiguateTypes.environment; (** disambiguation aliases *)
+ multi_aliases: DisambiguateTypes.multiple_environment;
+ moo_content_rev: moo;
+ proof_status: proof_status; (** logical status *)
+ options: options;
+ objects: (UriManager.uri * string) list; (** in-scope objects, with paths *)
+ coercions: UriManager.uri list; (** defined coercions *)
+ notation_ids: CicNotation.notation_id list; (** in-scope notation ids *)
+}
+
+val set_metasenv: Cic.metasenv -> status -> status
+
+ (** list is not reversed, head command will be the first emitted *)
+val add_moo_content: ast_command list -> status -> status
+val add_moo_metadata: GrafiteAst.metadata list -> status -> status
+
+val dump_status : status -> unit
+val get_option : status -> StringMap.key -> option_value
+val get_string_option : status -> StringMap.key -> string
+val set_option : status -> StringMap.key -> string -> status
- (* subset of MatitaConsole.console methods needed by MatitaInterpreter *)
class type console =
object
+ method choose_uri : string list -> string
method clear : unit -> unit
method echo_error : string -> unit
method echo_message : string -> unit
- method wrap_exn : 'a. (unit -> 'a) -> 'a option
- method choose_uri : string list -> string
method show : ?msg:string -> unit -> unit
+ method wrap_exn : (unit -> 'a) -> 'a option
end
-class type disambiguator =
- object
- method env : DisambiguateTypes.environment
- method setEnv : DisambiguateTypes.environment -> unit
-
- method chooseUris: choose_uris_callback
- method setChooseUris: choose_uris_callback -> unit
-
- method chooseInterp: choose_interp_callback
- method setChooseInterp: choose_interp_callback -> unit
-
- method parserr: parserr
-
- (* TODO Zack: as long as matita doesn't support MDI inteface,
- * disambiguateTerm will return a single term *)
- (** @param env disambiguation environment. If this parameter is given the
- * disambiguator act statelessly, that is internal disambiguation status
- * want be changed but only returned. If this parameter is not given the
- * internal one will be used and updated with the disambiguation status
- * resulting from the disambiguation *)
- method disambiguateTerm :
- ?context:Cic.context ->
- ?metasenv:Cic.metasenv ->
- ?env:DisambiguateTypes.environment ->
- char Stream.t ->
- DisambiguateTypes.environment * Cic.metasenv * Cic.term *
- CicUniv.universe_graph
-
- (** @param env @see disambiguateTerm above *)
- method disambiguateTermAst :
- ?context:Cic.context ->
- ?metasenv:Cic.metasenv ->
- ?env:DisambiguateTypes.environment ->
- DisambiguateTypes.term ->
- DisambiguateTypes.environment * Cic.metasenv * Cic.term *
- CicUniv.universe_graph
-
- (** as disambiguateTermAst, but disambiguate a list of ASTs at once. All
- * AST should be closed hence no context param is permitted on this method
- *)
- method disambiguateTermAsts :
- ?metasenv:Cic.metasenv ->
- ?env:DisambiguateTypes.environment ->
- DisambiguateTypes.term list ->
- DisambiguateTypes.environment * Cic.metasenv * Cic.term list *
- CicUniv.universe_graph
- end
-
-class type proof =
- object
- inherit [unit] StatefulProofEngine.status
-
- (** return a pair of "xml" (as defined in Xml module) representing the *
- * current proof type and body, respectively *)
- method toXml : Xml.token Stream.t * Xml.token Stream.t
-
- method toString : string
- end
-
-class type currentProof =
- object
- method onGoing: unit -> bool (** true if a proof is on going *)
- method proof: proof (** @raise Failure "No current proof" *)
- method start: proof -> unit (** starts a new proof *)
- method abort: unit -> unit (** abort the on going proof *)
- method quit: unit -> unit (** quit matita *)
- end
-
- (** first component represents success: true = success, false = failure
- * second component represents console action: true = hide, false = keep *)
-type command_outcome = bool * bool
-
- (** schematic representation of items scripts are made of *)
-type script_item =
- [ `Tactic (** action on proof status *)
- | `Theorem (** start of proof, to be proved *)
- | `Qed of UriManager.uri (** end of proof, successfull *)
- | `Def of UriManager.uri (** constant with body *)
- | `Inductive of UriManager.uri (** inductive definition *)
- ]
-
- (** interpreter for toplevel phrases given via console *)
-class type interpreter =
- object
- (** parse a single phrase contained in the input string. Additional
- * garbage at the end of the phrase is ignored
- * @return true if no exception has been raised by the evaluation, false
- * otherwise
- *)
- method evalPhrase: string -> command_outcome
-
- (** as evalPhrase above, but parses a character stream. Only characters
- * composing next phrases are consumed *)
-(* method evalStream: char Stream.t -> command_outcome *)
-
- (** as above, evaluating a command/tactics AST *)
- method evalAst: DisambiguateTypes.tactical -> command_outcome
-
- (** {3 callbacks} *)
-
- method setEvalAstCallback: (DisambiguateTypes.tactical -> unit) -> unit
-
- (** {3 stateful methods}
- * bookkeeping of last interpreted phrase *)
-
- (** offset from the starting of the last string parser by evalPhrase where
- * parsing stop.
- * @raise Failure when no offset has been recorded *)
- method endOffset: int
-
- (** last item parsed *)
- method lastItem: script_item option
-
- (** change internal interpreter state *)
- method setState: [`Proof | `Command] -> unit
-
- end
-
-(** {2 MathML widgets} *)
+type abouts = [ `Blank | `Current_proof | `Us ]
-type term_source =
- [ `Ast of DisambiguateTypes.term
+type mathViewer_entry =
+ [ `About of abouts
+ | `Check of string
| `Cic of Cic.term * Cic.metasenv
- | `String of string
- ]
+ | `Dir of string
+ | `Uri of UriManager.uri
+ | `Whelp of string * UriManager.uri list ]
+
+val string_of_entry :
+ [< `About of [< `Blank | `Current_proof | `Us ]
+ | `Check of 'a
+ | `Cic of 'b * 'c
+ | `Dir of string
+ | `Uri of UriManager.uri
+ | `Whelp of string * 'd ] ->
+ string
+
+val entry_of_string :
+ string -> [> `About of [> `Blank | `Current_proof | `Us ] ]
class type mathViewer =
object
- method checkTerm: term_source -> unit
+ method show_entry : ?reuse:bool -> mathViewer_entry -> unit
+ method show_uri_list :
+ ?reuse:bool -> entry:mathViewer_entry -> UriManager.uri list -> unit
end
-class type cicBrowser =
- object
- method loadUri: string -> unit
- method loadTerm: term_source -> unit
- end
-
-type mml_of_cic_sequent =
- Cic.metasenv ->
- Cic.conjecture ->
- Gdome.document *
- ((Cic.id, Cic.term) Hashtbl.t * (Cic.id, Cic.id option) Hashtbl.t *
- (string, Cic.hypothesis) Hashtbl.t)
-
-type mml_of_cic_object =
- explode_all:bool ->
- UriManager.uri ->
- Cic.annobj ->
- (string, string) Hashtbl.t ->
- (string, Cic2acic.anntypes) Hashtbl.t -> Gdome.document
+val qualify: status -> string -> string
-(** {2 shorthands} *)
+val get_current_proof: status -> ProofEngineTypes.proof
+val get_proof_metasenv: status -> Cic.metasenv
+val get_proof_context: status -> ProofEngineTypes.goal -> Cic.context
+val get_proof_conclusion: status -> ProofEngineTypes.goal -> Cic.term
+val get_stack: status -> Continuationals.Stack.t
-type namer = ProofEngineTypes.mk_fresh_name_type
+val set_stack: Continuationals.Stack.t -> status -> status
projects / helm.git / blobdiff