X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fmatita%2FmatitaTypes.mli;h=e54fe5c7e7fc0ceef806b562f97f53f6f21f7f0d;hb=97c2d258a5c524eb5c4b85208899d80751a2c82f;hp=b165740aade4081290fd3851568998eee98dd49b;hpb=ef9ec8cb57d15426a96fe40d056eb07804753bb9;p=helm.git diff --git a/helm/matita/matitaTypes.mli b/helm/matita/matitaTypes.mli index b165740aa..e54fe5c7e 100644 --- a/helm/matita/matitaTypes.mli +++ b/helm/matita/matitaTypes.mli @@ -1,4 +1,4 @@ -(* 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 @@ -23,182 +23,106 @@ * 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 +exception Statement_error of string +val statement_error : string -> 'a - (** @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 +exception Command_error of string +val command_error : string -> 'a -val unopt_uri : 'a option -> 'a +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 (** *) + +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 - end - -class type disambiguator = - object - method parserr : parserr - method setParserr : parserr -> unit - - method env : DisambiguateTypes.environment - method setEnv : DisambiguateTypes.environment -> unit - - (* 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 *) + method show : ?msg:string -> unit -> unit + method wrap_exn : (unit -> 'a) -> 'a option end - (** first component represents success: true = success, false = failure - * second component represents console action: true = hide, false = keep *) -type command_outcome = bool * bool - - (** interpreter for toplevel phrases given via console *) -class type interpreter = - object - method reset: unit (** return the interpreter to the initial state *) - - (** 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 +type abouts = [ `Blank | `Current_proof | `Us ] - (** 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 - - (** 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 - - end +type mathViewer_entry = + [ `About of abouts + | `Check of string + | `Cic of Cic.term * Cic.metasenv + | `Dir of string + | `Uri of UriManager.uri + | `Whelp of string * UriManager.uri list ] -(** {2 MathML widgets} *) +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 -type term_source = - [ `Ast of DisambiguateTypes.term - | `Cic of Cic.term - | `String of 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 - -(** {2 shorthands} *) - -type namer = ProofEngineTypes.mk_fresh_name_type - - (** {3 disambiguator callbacks} *) - -type choose_uris_callback = - selection_mode:[ `MULTIPLE | `SINGLE ] -> - ?title:string -> - ?msg:string -> ?nonvars_button:bool -> string list -> string list +val qualify: status -> string -> string -type choose_interp_callback = (string * string) list list -> int list +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 - (** @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 +val set_stack: Continuationals.Stack.t -> status -> status