X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fmatita%2FmatitaTypes.ml;h=bea4377e6112db7b4802b125d84b9baa072a3d12;hb=ac7687ce66526f905874ed99a845223c853c558a;hp=92fc79b7c288fb979f65d136eb510c148c04fee4;hpb=e89486cad653803954662a5e543537acd49a866f;p=helm.git diff --git a/helm/matita/matitaTypes.ml b/helm/matita/matitaTypes.ml index 92fc79b7c..bea4377e6 100644 --- a/helm/matita/matitaTypes.ml +++ b/helm/matita/matitaTypes.ml @@ -38,36 +38,15 @@ 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" -class type observer = - (* "observer" pattern *) - object - method update: unit -> unit - end - -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 = @@ -98,23 +77,29 @@ class type disambiguator = (DisambiguateTypes.environment * Cic.metasenv * Cic.term) end -class type proofStatus = - object - inherit subject - - (** {3 properties} *) +(* +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 +*) - method proof: ProofEngineTypes.proof - method setProof: ProofEngineTypes.proof -> unit - - method goal: ProofEngineTypes.goal option - method setGoal: ProofEngineTypes.goal option -> unit - - (** @raise MatitaTypes.No_proof *) - method status: ProofEngineTypes.status (* proof, goal *) - method setStatus: ProofEngineTypes.status -> unit - - (** {3 actions} *) +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 *) @@ -122,16 +107,10 @@ class type proofStatus = method toString: string end -class type proof = - object - (** {3 status} *) - method status: proofStatus - method setStatus: proofStatus -> unit - 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 *) + 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 *) @@ -141,7 +120,64 @@ type proof_handler = (** 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} *)