-(* Copyright (C) 2004, HELM Team.
+(* Copyright (C) 2004-2005, HELM Team.
*
* This file is part of HELM, an Hypertextual, Electronic
* Library of Mathematics, developed at the Computer Science
* http://helm.cs.unibo.it/
*)
-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 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 *)
+open Printf
+
+ (** user hit the cancel button *)
+exception Cancel
+
+ (** statement invoked in the wrong context (e.g. tactic with no ongoing proof)
+ *)
+exception Statement_error of string
+let statement_error msg = raise (Statement_error msg)
+
+exception Command_error of string
+let command_error msg = raise (Command_error msg)
+
+ (** parameters are: option name, error message *)
+exception Option_error of string * string
+
+exception Unbound_identifier of string
+
+type proof_status =
+ | No_proof
+ | Incomplete_proof of ProofEngineTypes.status
+ | Proof of ProofEngineTypes.proof
+ | Intermediate of Cic.metasenv
+ (* Status in which the proof could be while it is being processed by the
+ * engine. No status entering/exiting the engine could be in it. *)
+
+module StringMap = Map.Make (String)
+
+type option_value =
+ | String of string
+ | Int of int
+type options = option_value StringMap.t
+let no_options = StringMap.empty
+
+type status = {
+ aliases: DisambiguateTypes.environment; (** disambiguation aliases *)
+ proof_status: proof_status;
+ options: options;
+ coercions: CoercGraph.coercions;
+ objects: (UriManager.uri * string) list;
+ (** in-scope objects, with their paths *)
+}
+
+let dump_status status =
+ MatitaLog.message "status.aliases:\n";
+ MatitaLog.message
+ (CicTextualParser2.EnvironmentP3.to_string status.aliases ^ "\n");
+ MatitaLog.message "status.proof_status:";
+ MatitaLog.message
+ (match status.proof_status with
+ | No_proof -> "no proof\n"
+ | Incomplete_proof _ -> "incomplete proof\n"
+ | Proof _ -> "proof\n"
+ | Intermediate _ -> "Intermediate\n");
+ MatitaLog.message "status.options\n";
+ StringMap.iter (fun k v ->
+ let v =
+ match v with
+ | String s -> s
+ | Int i -> string_of_int i
+ in
+ MatitaLog.message (k ^ "::=" ^ v)) status.options;
+ MatitaLog.message "status.coercions\n";
+ List.iter
+ (fun (u1,u2,u3) -> MatitaLog.message
+ ((UriManager.string_of_uri u1) ^
+ (UriManager.string_of_uri u2) ^
+ (UriManager.string_of_uri u3))) status.coercions;
+ MatitaLog.message "status.objects:\n";
+ List.iter
+ (fun (u,_) ->
+ MatitaLog.message (UriManager.string_of_uri u)) status.objects
+
+
+let get_option status name =
+ try
+ StringMap.find name status.options
+ with Not_found -> raise (Option_error (name, "not found"))
+
+let get_string_option status name =
+ match get_option status name with
+ | String s -> s
+ | _ -> raise (Option_error (name, "not a string value"))
+
+let set_option status name value =
+ let mangle_dir s =
+ let s = Str.global_replace (Str.regexp "//+") "/" s in
+ let s = Str.global_replace (Str.regexp "/$") "" s in
+ s
+ in
+ let types =
+ [ "baseuri", (`String, mangle_dir);
+ "basedir", (`String, mangle_dir);
+ ]
+ in
+ let ty_and_mangler =
+ try
+ List.assoc name types
+ with Not_found -> command_error (sprintf "Unknown option \"%s\"" name)
+ in
+ let value =
+ match ty_and_mangler with
+ | `String, f -> String (f value)
+ | `Int, f ->
+ (try
+ Int (int_of_string (f value))
+ with Failure _ ->
+ command_error (sprintf "Not an integer value \"%s\"" value))
+ in
+ { status with options = StringMap.add name value status.options }
+
+ (* subset of MatitaConsole.console methods needed by MatitaInterpreter *)
+class type console =
object
- method execute: unit -> unit
- method undo: unit -> unit
+ method clear : unit -> unit
+ method echo_error : string -> unit
+ method echo_message : string -> unit
+ method wrap_exn : 'a. (unit -> 'a) -> 'a option
+ method choose_uri : string list -> string
+ method show : ?msg:string -> unit -> unit
end
-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 =
- object
- 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 ->
- ?env:DisambiguateTypes.environment ->
- char Stream.t ->
- (DisambiguateTypes.environment * Cic.metasenv * Cic.term)
- (** @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
-
- (** {3 properties} *)
-
- 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} *)
-
- (** 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
-
-class type proof =
- object
- (** {3 status} *)
- method status: proofStatus
- method setStatus: proofStatus -> unit
- end
-
- (** interpreter for toplevel phrases given via console *)
-class type interpreter =
- object
- method evalPhrase: string -> unit
- end
-
-(** {2 shorthands} *)
-
-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
-