X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fmatita%2FmatitaTypes.ml;h=c49bce0040049595cbcceda5b405559dc4bb713b;hb=87ff483dd776e580fa97fca0e3bf888cc8a8d540;hp=b26c2f677221ba96c3180e5963815f3708b6f0db;hpb=b5d69130dd83587b5fb9cbb39251aaa8df8c456e;p=helm.git

diff --git a/helm/matita/matitaTypes.ml b/helm/matita/matitaTypes.ml
index b26c2f677..c49bce004 100644
--- a/helm/matita/matitaTypes.ml
+++ b/helm/matita/matitaTypes.ml
@@ -23,33 +23,144 @@
  * http://helm.cs.unibo.it/
  *)
 
-  (** no current proof is available *)
+open Printf
+
+exception Not_implemented of string
+let not_implemented feature = raise (Not_implemented feature)
+
+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)
+
+let explain = function
+  | StatefulProofEngine.Tactic_failure exn ->
+      sprintf "Tactic failed: %s"(Printexc.to_string exn)
+  | StatefulProofEngine.Observer_failures exns ->
+      String.concat "\n"
+        (List.map (fun (_, exn) -> Printexc.to_string exn) exns)
+  | CicTextualParser2.Parse_error (floc, msg) ->
+      let (x, y) = CicAst.loc_of_floc floc in
+      sprintf "parse error at character %d-%d: %s" x y msg
+  | exn -> sprintf "Uncaught exception: %s" (Printexc.to_string exn)
+
 exception No_proof
 
-class type observer =
-  (* "observer" pattern *)
+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"
+
+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 update: unit -> unit
+    method parseTerm:     char Stream.t -> DisambiguateTypes.term
+    method parseTactical: char Stream.t -> DisambiguateTypes.tactical
   end
 
-class subject =
-  (* "observer" pattern *)
+class type console =
   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
+    method echo_message   : string -> unit
+    method echo_error     : string -> unit
+    method clear          : unit -> unit
+    method wrap_exn       : 'a. (unit -> 'a) -> 'a option
   end
 
-class type command =
-  (* "command" pattern *)
+class type disambiguator =
   object
-    method execute: unit -> unit
-    method undo: unit -> unit
+    method parserr: parserr
+    method setParserr: parserr -> unit
+
+    method env: DisambiguateTypes.environment
+    method setEnv: DisambiguateTypes.environment -> unit
+
+    method disambiguateTerm:
+      ?context:Cic.context -> ?metasenv:Cic.metasenv ->
+      ?env:DisambiguateTypes.environment ->
+        char Stream.t ->
+          (DisambiguateTypes.environment * Cic.metasenv * Cic.term *
+           CicUniv.universe_graph)
+    method disambiguateTermAst:
+      ?context:Cic.context -> ?metasenv:Cic.metasenv ->
+      ?env:DisambiguateTypes.environment ->
+        DisambiguateTypes.term ->
+          (DisambiguateTypes.environment * Cic.metasenv * Cic.term *
+           CicUniv.universe_graph) 
+
+    method disambiguateTermAsts:
+      ?metasenv:Cic.metasenv ->
+      ?env:DisambiguateTypes.environment ->
+      DisambiguateTypes.term list ->
+          (DisambiguateTypes.environment * Cic.metasenv * Cic.term list *
+          CicUniv.universe_graph)
   end
 
-(** {2 shorthands} *)
+class type proof =
+  object
+    inherit [unit] StatefulProofEngine.status
+
+    method toXml: Xml.token Stream.t * Xml.token Stream.t
+    method toString: string
+  end
+
+class type currentProof =
+  object
+    method onGoing: unit -> bool
+    method proof: proof
+    method start: proof -> unit
+    method abort: unit -> unit
+    method quit: unit -> unit
+  end
+
+type command_outcome = bool * bool
+
+class type interpreter =
+  object
+    method endOffset : int
+    method evalAst : DisambiguateTypes.tactical -> command_outcome
+    method evalPhrase : string -> command_outcome
+(*     method evalStream: char Stream.t -> command_outcome *)
+    method reset : unit
+  end
+
+class type mathViewer =
+  object
+    method checkTerm: Cic.conjecture -> Cic.metasenv -> unit
+    method unload: unit -> unit
+    method set_href_callback: (UriManager.uri -> unit) option -> unit
+  end
+
+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
 
 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
+
+let mono_uris_callback ~selection_mode ?title ?msg ?nonvars_button _ =
+  raise (Failure "ambiguous input")
+let mono_interp_callback _ = raise (Failure "ambiguous input")
+