X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fmatita%2FmatitaTypes.ml;h=4631fa351a23749905cd36e1f03eab5bd8b032ab;hb=72e5ddf0f07b0e692f5e3544438f77f2e346b12a;hp=92fc79b7c288fb979f65d136eb510c148c04fee4;hpb=e89486cad653803954662a5e543537acd49a866f;p=helm.git diff --git a/helm/matita/matitaTypes.ml b/helm/matita/matitaTypes.ml index 92fc79b7c..4631fa351 100644 --- a/helm/matita/matitaTypes.ml +++ b/helm/matita/matitaTypes.ml @@ -35,39 +35,33 @@ let debug_print s = exception No_proof (** no current proof is available *) +exception Cancel +exception Unbound_identifier of string + +(* 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) +*) +let unopt_uri = function Some uri -> uri | None -> assert false 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 + + (* subset of MatitaConsole.console methods needed by MatitaInterpreter *) +class type console = + object + method echo_message : string -> unit + method echo_error : string -> unit + method clear : unit -> unit + method wrap_exn : (unit -> unit) -> bool end class type disambiguator = @@ -89,32 +83,48 @@ class type disambiguator = ?context:Cic.context -> ?metasenv:Cic.metasenv -> ?env:DisambiguateTypes.environment -> char Stream.t -> - (DisambiguateTypes.environment * Cic.metasenv * Cic.term) + (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) - end - -class type proofStatus = - object - inherit subject + (DisambiguateTypes.environment * Cic.metasenv * Cic.term * CicUniv.universe_graph) - (** {3 properties} *) - - method proof: ProofEngineTypes.proof - method setProof: ProofEngineTypes.proof -> unit - - method goal: ProofEngineTypes.goal option - method setGoal: ProofEngineTypes.goal option -> unit + (** 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 - (** @raise MatitaTypes.No_proof *) - method status: ProofEngineTypes.status (* proof, goal *) - method setStatus: ProofEngineTypes.status -> unit +(* +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 +*) - (** {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 +132,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 +145,67 @@ type proof_handler = (** interpreter for toplevel phrases given via console *) class type interpreter = object - method evalPhrase: string -> unit + 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 -> bool + + (** as above, evaluating a command/tactics AST *) + method evalAst: DisambiguateTypes.tactical -> bool + + (** 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 + +(** {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} *)