X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fmatita%2FmatitaTypes.ml;h=9b100ca718c8f3b4ebf82b1322fa3bfddfb46e5b;hb=aac382f935bc72578119fa7ff9f53c3b649dd0dd;hp=70f912ae08fd586abe7fad584cdcfb4845010886;hpb=06c2b37f3d7d4e14cabeef3b18211e5d12b9b4eb;p=helm.git diff --git a/helm/matita/matitaTypes.ml b/helm/matita/matitaTypes.ml index 70f912ae0..9b100ca71 100644 --- a/helm/matita/matitaTypes.ml +++ b/helm/matita/matitaTypes.ml @@ -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,144 +23,159 @@ * http://helm.cs.unibo.it/ *) -exception Not_implemented of string -let not_implemented feature = raise (Not_implemented feature) - - (** exceptions whose content should be presented to the user *) -exception Failure of string -let error s = raise (Failure s) -let warning s = prerr_endline ("MATITA WARNING:\t" ^ s) -let debug_print s = - if BuildTimeConf.debug then prerr_endline ("MATITA DEBUG:\t" ^ s) - -exception No_proof (** no current proof is available *) - -let untitled_con_uri = UriManager.uri_of_string "cic:/untitled.con" -let untitled_def_uri = UriManager.uri_of_string "cic:/untitled.ind" - -let unopt_uri ?(kind = `Con) = function - | Some uri -> uri - | None -> - (match kind with `Con -> untitled_con_uri | `Def -> untitled_def_uri) - -class type parserr = (* "parser" is a keyword :-( *) - object - method parseTerm: char Stream.t -> DisambiguateTypes.term - method parseTactical: char Stream.t -> DisambiguateTypes.tactical - 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) - (** @param env @see disambiguateTerm above *) - method disambiguateTermAst: - ?context:Cic.context -> ?metasenv:Cic.metasenv -> - ?env:DisambiguateTypes.environment -> - DisambiguateTypes.term -> - (DisambiguateTypes.environment * Cic.metasenv * Cic.term) - end - -type hist_metadata = - Cic.annobj * - (Cic.id, Cic.term) Hashtbl.t * - (Cic.id, Cic.id option) Hashtbl.t * - (Cic.id, string) Hashtbl.t * - (Cic.id, Cic2acic.anntypes) Hashtbl.t * - (Cic.id, Cic.conjecture) Hashtbl.t * - (Cic.id, Cic.hypothesis) Hashtbl.t - -class type proof = - object - inherit [hist_metadata] 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 - -type proof_handler = - { get_proof: unit -> proof; (* return current proof or fail *) - set_proof: proof option -> unit; (* set a proof option as current proof *) - has_proof: unit -> bool; (* check if a current proof is available or not *) - new_proof: proof -> unit; (* as a set_proof but takes care also to register - observers *) - quit: unit -> unit - } - - (** interpreter for toplevel phrases given via console *) -class type interpreter = +open Printf + + (** user hit the cancel button *) +exception Cancel + + (** statement invoked in the wrong context (e.g. tactic with no ongoing proof) + *) +exception Statement_error of string +let statement_error msg = raise (Statement_error msg) + +exception Command_error of string +let command_error msg = raise (Command_error msg) + + (** parameters are: option name, error message *) +exception Option_error of string * string + +exception Unbound_identifier of string + +type proof_status = + | No_proof + | Incomplete_proof of ProofEngineTypes.status + | Proof of ProofEngineTypes.proof + | Intermediate of Cic.metasenv + (* Status in which the proof could be while it is being processed by the + * engine. No status entering/exiting the engine could be in it. *) + +module StringMap = Map.Make (String) + +type option_value = + | String of string + | Int of int +type options = option_value StringMap.t +let no_options = StringMap.empty + +type status = { + aliases: DisambiguateTypes.environment; (** disambiguation aliases *) + proof_status: proof_status; + options: options; + coercions: CoercGraph.coercions; + objects: (UriManager.uri * string) list; + (** in-scope objects, with their paths *) +} + +let dump_status status = + MatitaLog.message "status.aliases:\n"; + MatitaLog.message + (CicTextualParser2.EnvironmentP3.to_string status.aliases ^ "\n"); + MatitaLog.message "status.proof_status:"; + MatitaLog.message + (match status.proof_status with + | No_proof -> "no proof\n" + | Incomplete_proof _ -> "incomplete proof\n" + | Proof _ -> "proof\n" + | Intermediate _ -> "Intermediate\n"); + MatitaLog.message "status.options\n"; + StringMap.iter (fun k v -> + let v = + match v with + | String s -> s + | Int i -> string_of_int i + in + MatitaLog.message (k ^ "::=" ^ v)) status.options; + MatitaLog.message "status.coercions\n"; + List.iter + (fun (u1,u2,u3) -> MatitaLog.message + ((UriManager.string_of_uri u1) ^ + (UriManager.string_of_uri u2) ^ + (UriManager.string_of_uri u3))) status.coercions; + MatitaLog.message "status.objects:\n"; + List.iter + (fun (u,_) -> + MatitaLog.message (UriManager.string_of_uri u)) status.objects + + +let get_option status name = + try + StringMap.find name status.options + with Not_found -> raise (Option_error (name, "not found")) + +let get_string_option status name = + match get_option status name with + | String s -> s + | _ -> raise (Option_error (name, "not a string value")) + +let set_option status name value = + let mangle_dir s = + let s = Str.global_replace (Str.regexp "//+") "/" s in + let s = Str.global_replace (Str.regexp "/$") "" s in + s + in + let types = + [ "baseuri", (`String, mangle_dir); + "basedir", (`String, mangle_dir); + ] + in + let ty_and_mangler = + try + List.assoc name types + with Not_found -> command_error (sprintf "Unknown option \"%s\"" name) + in + let value = + match ty_and_mangler with + | `String, f -> String (f value) + | `Int, f -> + (try + Int (int_of_string (f value)) + with Failure _ -> + command_error (sprintf "Not an integer value \"%s\"" value)) + in + { status with options = StringMap.add name value status.options } + + (* subset of MatitaConsole.console methods needed by MatitaInterpreter *) +class type console = object - method evalPhrase: string -> unit + 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 end -(** {2 MathML widgets} *) - -type mml_of_cic_sequent = - Cic.metasenv -> int * Cic.context * Cic.term -> - 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 - - (** TODO Zack to be reviewed and unified with proof_viewer above *) -class type sequent_viewer = - object - inherit GMathViewAux.multi_selection_math_view - - (** @return the list of selected terms. Selections which are not terms are - * ignored *) - method get_selected_terms: Cic.term list - - (** @return the list of selected hypothese. Selections which are not - * hypotheses are ignored *) - method get_selected_hypotheses: Cic.hypothesis list - - (** load a sequent and render it into parent widget *) - method load_sequent: Cic.metasenv -> Cic.conjecture -> unit - end - -class type proof_viewer = +type abouts = + [ `Blank + | `Current_proof + | `Us + ] + +type mathViewer_entry = + [ `About of abouts (* current proof *) + | `Check of string (* term *) + | `Cic of Cic.term * Cic.metasenv + | `Dir of string (* "directory" in cic uris namespace *) + | `Uri of string (* cic object uri *) + | `Whelp of string * string list (* query and results *) + ] + +let string_of_entry = function + | `About `Blank -> "about:blank" + | `About `Current_proof -> "about:proof" + | `About `Us -> "about:us" + | `Check _ -> "check:" + | `Cic (_, _) -> "term:" + | `Dir uri | `Uri uri -> uri + | `Whelp (query, _) -> query + +class type mathViewer = object - inherit GMathViewAux.single_selection_math_view - - (** @return the annotated cic term and the ids_to_inner_types and - * ids_to_inner_sorts maps *) - method load_proof: Gdome.document -> hist_metadata -> unit - + (** @param reuse if set reused last opened cic browser otherwise + * opens a new one. default is false + *) + method show_entry: ?reuse:bool -> mathViewer_entry -> unit + method show_uri_list: + ?reuse:bool -> entry:mathViewer_entry -> string list -> unit end - -(** {2 shorthands} *) - -type namer = ProofEngineTypes.mk_fresh_name_type - -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 - +