X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fmatita%2FmatitaTypes.ml;h=bea4377e6112db7b4802b125d84b9baa072a3d12;hb=ac7687ce66526f905874ed99a845223c853c558a;hp=acae4c9dfe2d4d5cbd89da094823fb4c15a81d67;hpb=07dde6f87105c18b28fc784b7d596a5d242e1225;p=helm.git diff --git a/helm/matita/matitaTypes.ml b/helm/matita/matitaTypes.ml index acae4c9df..bea4377e6 100644 --- a/helm/matita/matitaTypes.ml +++ b/helm/matita/matitaTypes.ml @@ -29,41 +29,24 @@ 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: " ^ 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 *) -exception No_choice (** no choice was made by the user *) -class type observer = - (* "observer" pattern *) - object - method update: unit -> unit - end +let untitled_con_uri = UriManager.uri_of_string "cic:/untitled.con" +let untitled_def_uri = UriManager.uri_of_string "cic:/untitled.ind" -class subject = - (* "observer" pattern *) - 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 - end - -class type command = - (* "command" pattern *) - object - method execute: unit -> unit - method undo: unit -> unit - end +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 parseTactic: char Stream.t -> DisambiguateTypes.tactic method parseTactical: char Stream.t -> DisambiguateTypes.tactical - method parseCommand: char Stream.t -> DisambiguateTypes.command - method parseScript: char Stream.t -> DisambiguateTypes.script end class type disambiguator = @@ -71,16 +54,130 @@ class type disambiguator = 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 -> + ?context:Cic.context -> ?metasenv:Cic.metasenv -> ?env:DisambiguateTypes.environment -> char Stream.t -> - (DisambiguateTypes.environment * Cic.metasenv * Cic.term) list + (DisambiguateTypes.environment * Cic.metasenv * Cic.term) + (** @param env @see disambiguateTerm above *) method disambiguateTermAst: - context:Cic.context -> metasenv:Cic.metasenv -> + ?context:Cic.context -> ?metasenv:Cic.metasenv -> ?env:DisambiguateTypes.environment -> DisambiguateTypes.term -> - (DisambiguateTypes.environment * Cic.metasenv * Cic.term) list + (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 + inherit GMathViewAux.single_selection_math_view + + method load_proof: StatefulProofEngine.proof_status -> unit + end + +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 -> int -> unit + end + +class type sequents_viewer = + object + method reset: unit + method load_sequents: Cic.metasenv -> unit + method goto_sequent: int -> unit (* to be called _after_ load_sequents *) end (** {2 shorthands} *) @@ -88,7 +185,7 @@ class type disambiguator = type namer = ProofEngineTypes.mk_fresh_name_type type choose_uris_callback = - selection_mode:Gtk.Tags.selection_mode -> + selection_mode:[`MULTIPLE|`SINGLE] -> ?title:string -> ?msg:string -> ?nonvars_button:bool -> string list -> string list