X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fmatita%2FmatitaTypes.ml;h=bea4377e6112db7b4802b125d84b9baa072a3d12;hb=ac7687ce66526f905874ed99a845223c853c558a;hp=b26c2f677221ba96c3180e5963815f3708b6f0db;hpb=b5d69130dd83587b5fb9cbb39251aaa8df8c456e;p=helm.git diff --git a/helm/matita/matitaTypes.ml b/helm/matita/matitaTypes.ml index b26c2f677..bea4377e6 100644 --- a/helm/matita/matitaTypes.ml +++ b/helm/matita/matitaTypes.ml @@ -23,33 +23,172 @@ * http://helm.cs.unibo.it/ *) - (** no current proof is available *) -exception No_proof +exception Not_implemented of string +let not_implemented feature = raise (Not_implemented feature) -class type observer = - (* "observer" pattern *) + (** 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 sequents_metadata = + (int * (** sequent (meta) index *) + (Cic.annconjecture * (** annotated conjecture *) + (Cic.id, Cic.term) Hashtbl.t * (** ids_to_terms *) + (Cic.id, Cic.id option) Hashtbl.t * (** ids_to_father_ids *) + (Cic.id, string) Hashtbl.t * (** ids_to_inner_sorts *) + (Cic.id, Cic.hypothesis) Hashtbl.t)) (** ids_to_hypotheses *) + list +type proof_metadata = + Cic.annobj * (** annotated object *) + (Cic.id, Cic.term) Hashtbl.t * (** ids_to_terms *) + (Cic.id, Cic.id option) Hashtbl.t * (** ids_to_father_ids *) + (Cic.id, string) Hashtbl.t * (** ids_to_inner_sorts *) + (Cic.id, Cic2acic.anntypes) Hashtbl.t * (** ids_to_inner_types *) + (Cic.id, Cic.conjecture) Hashtbl.t * (** ids_to_conjectures *) + (Cic.id, Cic.hypothesis) Hashtbl.t (** ids_to_hypotheses *) +type hist_metadata = proof_metadata * sequents_metadata +*) + +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 + +type proof_handler = + { get_proof: unit -> proof; (* return current proof or fail *) + set_proof: proof option -> unit; + abort_proof: unit -> unit;(* abort current proof, cleaning up garbage *) + 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 = + 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 *) + method evalPhrase: string -> unit + +(* + (** eval zero or more phrases contained in the input string. Additional + * garbage contained at the end of the last phrase is ignored. + * @return offset from the beginning of the string pointing to the end of + * the last parsed phrase. Next invocations of evalAll should start from + * there *) + method evalAll: string -> int +*) + end + +(** {2 MathML widgets} *) + +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 + +class type proof_viewer = object - method update: unit -> unit + inherit GMathViewAux.single_selection_math_view + + method load_proof: StatefulProofEngine.proof_status -> unit end -class subject = - (* "observer" pattern *) +class type sequent_viewer = object - val mutable observers = [] - method attach (o: observer) = observers <- o :: observers - method detach (o: observer) = - observers <- List.filter (fun o' -> o' != o) observers - method notify () = List.iter (fun o -> o#update ()) observers + 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 -> int -> unit end -class type command = - (* "command" pattern *) +class type sequents_viewer = object - method execute: unit -> unit - method undo: unit -> unit + method reset: unit + method load_sequents: Cic.metasenv -> unit + method goto_sequent: int -> unit (* to be called _after_ load_sequents *) 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 +