]> matita.cs.unibo.it Git - helm.git/blobdiff - helm/matita/matitaTypes.ml
debian: rebuilt against ocaml 3.08.2
[helm.git] / helm / matita / matitaTypes.ml
index 2811fd5d49ff1f61e0995604a6e13e5c6f8c715e..95618d142624e932493666da151773b8d9f412c5 100644 (file)
  * http://helm.cs.unibo.it/
  *)
 
+open Printf
+
 exception Not_implemented of string
 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:\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 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
+  | CicEnvironment.Object_not_found uri ->
+      sprintf "object not found: %s" (UriManager.string_of_uri uri)
+  | exn -> sprintf "Uncaught exception: %s" (Printexc.to_string exn)
+
+exception No_proof
+
+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"
 
@@ -42,6 +60,8 @@ 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
@@ -49,63 +69,114 @@ class type parserr =  (* "parser" is a keyword :-( *)
     method parseTactical: char Stream.t -> DisambiguateTypes.tactical
   end
 
-class type disambiguator =
+class type console =
   object
-    method parserr: parserr
-    method setParserr: parserr -> unit
+    method echo_message   : string -> unit
+    method echo_error     : string -> unit
+    method clear          : unit -> unit
+    method wrap_exn       : 'a. (unit -> 'a) -> 'a option
+    method choose_uri     : string list -> string
+    method show : ?msg:string -> unit -> unit
+  end
 
+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
+
+class type disambiguator =
+  object
     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 chooseUris: choose_uris_callback
+    method setChooseUris: choose_uris_callback -> unit
+
+    method chooseInterp: choose_interp_callback
+    method setChooseInterp: choose_interp_callback -> unit
+
+    method parserr: parserr
+
     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 *)
+          (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)
+          (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
 
 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;  (* set a proof option as current proof *)
-    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
-  }
+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
+
+type script_item =
+  [ `Tactic
+  | `Theorem
+  | `Qed of UriManager.uri
+  | `Def of UriManager.uri
+  | `Inductive of UriManager.uri
+  ]
 
-  (** interpreter for toplevel phrases given via console *)
 class type interpreter =
   object
-    method evalPhrase: string -> unit
+    method evalAst : DisambiguateTypes.tactical -> command_outcome
+    method evalPhrase : string -> command_outcome
+(*     method evalStream: char Stream.t -> command_outcome *)
+    method endOffset : int
+    method lastItem: script_item option
+    method setState: [`Proof | `Command] -> unit
+    method setEvalAstCallback: (DisambiguateTypes.tactical -> unit) -> unit
   end
 
-(** {2 MathML widgets} *)
+type term_source =
+  [ `Ast of DisambiguateTypes.term
+  | `Cic of Cic.term * Cic.metasenv
+  | `String of string
+  ]
+
+class type mathViewer =
+  object
+    method checkTerm: term_source -> unit
+  end
+
+class type cicBrowser =
+  object
+    method loadUri: string -> unit
+    method loadTerm: term_source -> unit
+  end
 
 type mml_of_cic_sequent =
-  Cic.metasenv -> int * Cic.context * Cic.term ->
+  Cic.metasenv -> Cic.conjecture ->
     Gdome.document *
     ((Cic.id, Cic.term) Hashtbl.t *
     (Cic.id, Cic.id option) Hashtbl.t *
@@ -113,47 +184,12 @@ type mml_of_cic_sequent =
 
 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 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 -> Cic.conjecture -> unit
-  end
-
-class type proof_viewer =
-  object
-    inherit GMathViewAux.single_selection_math_view
-
-      (** @return the annotated cic term and the ids_to_inner_types and
-      * ids_to_inner_sorts maps *)
-    method load_proof :
-     UriManager.uri -> Cic.obj ->
-      Cic.annobj * (Cic.id, Cic2acic.anntypes) Hashtbl.t *
-       (Cic.id, string) Hashtbl.t
-
-  end
-
-(** {2 shorthands} *)
+  (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")