-(* 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
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
- | 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
-
+ (** 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
-(*
-let untitled_con_uri = UriManager.uri_of_string "cic:/untitled.con"
-let untitled_def_uri = UriManager.uri_of_string "cic:/untitled.ind"
+type incomplete_proof = {
+ proof: ProofEngineTypes.proof;
+ stack: Continuationals.Stack.t;
+}
-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
+type proof_status =
+ | No_proof
+ | Incomplete_proof of incomplete_proof
+ | 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. *)
-class type parserr = (* "parser" is a keyword :-( *)
- object
- method parseTerm: char Stream.t -> DisambiguateTypes.term
- method parseTactical: char Stream.t -> DisambiguateTypes.tactical
- end
+module StringMap = Map.Make (String)
-class type console =
- object
- method echo_message : string -> unit
- method echo_error : string -> unit
- method clear : unit -> unit
- method wrap_exn : 'a. (unit -> 'a) -> 'a option
- end
+type option_value =
+ | String of string
+ | Int of int
+type options = option_value StringMap.t
+let no_options = StringMap.empty
-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
+type ast_command = (CicNotationPt.term, GrafiteAst.obj) GrafiteAst.command
+type moo = ast_command list * GrafiteAst.metadata list
-class type disambiguator =
- object
- method env: DisambiguateTypes.environment
- method setEnv: DisambiguateTypes.environment -> unit
-
- 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 *
- 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
+type status = {
+ aliases: DisambiguateTypes.environment;
+ multi_aliases: DisambiguateTypes.multiple_environment;
+ moo_content_rev: moo;
+ proof_status: proof_status;
+ options: options;
+ objects: (UriManager.uri * string) list;
+ coercions: UriManager.uri list;
+ notation_ids: CicNotation.notation_id list;
+}
-class type proof =
- object
- inherit [unit] StatefulProofEngine.status
+let set_metasenv metasenv status =
+ let proof_status =
+ match status.proof_status with
+ | No_proof -> Intermediate metasenv
+ | Incomplete_proof ({ proof = (uri, _, proof, ty) } as incomplete_proof) ->
+ Incomplete_proof
+ { incomplete_proof with proof = (uri, metasenv, proof, ty) }
+ | Intermediate _ -> Intermediate metasenv
+ | Proof _ -> assert false
+ in
+ { status with proof_status = proof_status }
- method toXml: Xml.token Stream.t * Xml.token Stream.t
- method toString: string
- end
+let dump_status status =
+ MatitaLog.message "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";
+ 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"))
-class type currentProof =
- object
- method onGoing: unit -> bool
- method proof: proof
- method start: proof -> unit
- method abort: unit -> unit
- method quit: unit -> unit
- end
+let get_string_option status name =
+ match get_option status name with
+ | String s -> s
+ | _ -> raise (Option_error (name, "not a string value"))
-type command_outcome = bool * bool
+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
+ if StringMap.mem name status.options && name = "baseuri" then
+ command_error "Redefinition of 'baseuri' is forbidden."
+ else
+ { status with options = StringMap.add name value status.options }
-type script_item =
- [ `Tactic
- | `Theorem
- | `Qed of UriManager.uri
- | `Def of UriManager.uri
- | `Inductive of UriManager.uri
- ]
+let add_moo_content cmds status =
+ let content, metadata = status.moo_content_rev in
+ let content' =
+ List.fold_right
+ (fun cmd acc ->
+(* prerr_endline ("adding to moo command: " ^ GrafiteAstPp.pp_command cmd); *)
+ match cmd with
+ | GrafiteAst.Interpretation _
+ | GrafiteAst.Default _ ->
+ if List.mem cmd content then acc
+ else cmd :: acc
+ | GrafiteAst.Alias _ -> (* move Alias as the last inserted one *)
+ cmd :: (List.filter ((<>) cmd) acc)
+ | _ -> cmd :: acc)
+ cmds content
+ in
+(* prerr_endline ("new moo content: " ^ String.concat " " (List.map
+ GrafiteAstPp.pp_command content')); *)
+ { status with moo_content_rev = content', metadata }
+
+let add_moo_metadata new_metadata status =
+ let content, metadata = status.moo_content_rev in
+ let metadata' =
+ List.fold_left
+ (fun acc m ->
+ match m with
+ | GrafiteAst.Dependency buri ->
+ let is_self = (* self dependency *)
+ try
+ get_string_option status "baseuri" = buri
+ with Option_error _ -> false (* baseuri not yet set *)
+ in
+ if is_self
+ || List.exists (GrafiteAst.eq_metadata m) metadata (* duplicate *)
+ then acc
+ else m :: acc
+ | _ -> m :: acc)
+ metadata new_metadata
+ in
+ { status with moo_content_rev = content, metadata' }
-class type interpreter =
+ (* subset of MatitaConsole.console methods needed by MatitaInterpreter *)
+class type console =
object
- 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
+ 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
-type term_source =
- [ `Ast of DisambiguateTypes.term
- | `Cic of Cic.term
- | `String of string
+type abouts =
+ [ `Blank
+ | `Current_proof
+ | `Us
+ ]
+
+type mathViewer_entry =
+ [ `About of abouts (* current proof *)
+ | `Check of string (* term *)
+ | `Cic of Cic.term * Cic.metasenv
+ | `Dir of string (* "directory" in cic uris namespace *)
+ | `Uri of UriManager.uri (* cic object uri *)
+ | `Whelp of string * UriManager.uri list (* query and results *)
]
-class type mathViewer =
- object
- method checkTerm: term_source -> unit
- end
+let string_of_entry = function
+ | `About `Blank -> "about:blank"
+ | `About `Current_proof -> "about:proof"
+ | `About `Us -> "about:us"
+ | `Check _ -> "check:"
+ | `Cic (_, _) -> "term:"
+ | `Dir uri -> uri
+ | `Uri uri -> UriManager.string_of_uri uri
+ | `Whelp (query, _) -> query
+
+let entry_of_string = function
+ | "about:blank" -> `About `Blank
+ | "about:proof" -> `About `Current_proof
+ | "about:us" -> `About `Us
+ | _ -> (* only about entries supported ATM *)
+ raise (Invalid_argument "entry_of_string")
-class type cicBrowser =
+class type mathViewer =
object
- method loadUri: string -> unit
- method loadTerm: term_source -> unit
+ (** @param reuse if set reused last opened cic browser otherwise
+ * opens a new one. default is false
+ *)
+ method show_entry: ?reuse:bool -> mathViewer_entry -> unit
+ method show_uri_list:
+ ?reuse:bool -> entry:mathViewer_entry -> UriManager.uri list -> unit
end
+
+let qualify status name = get_string_option status "baseuri" ^ "/" ^ name
-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)
+let get_current_proof status =
+ match status.proof_status with
+ | Incomplete_proof { proof = p } -> p
+ | _ -> statement_error "no ongoing proof"
-type mml_of_cic_object =
- explode_all:bool -> UriManager.uri -> Cic.annobj ->
- (string, string) Hashtbl.t -> (string, Cic2acic.anntypes) Hashtbl.t ->
- Gdome.document
+let get_proof_metasenv status =
+ match status.proof_status with
+ | No_proof -> []
+ | Proof (_, metasenv, _, _)
+ | Incomplete_proof { proof = (_, metasenv, _, _) }
+ | Intermediate metasenv ->
+ metasenv
-type namer = ProofEngineTypes.mk_fresh_name_type
+let get_proof_context status goal =
+ match status.proof_status with
+ | Incomplete_proof { proof = (_, metasenv, _, _) } ->
+ let (_, context, _) = CicUtil.lookup_meta goal metasenv in
+ context
+ | _ -> []
+
+let get_proof_conclusion status goal =
+ match status.proof_status with
+ | Incomplete_proof { proof = (_, metasenv, _, _) } ->
+ let (_, _, conclusion) = CicUtil.lookup_meta goal metasenv in
+ conclusion
+ | _ -> statement_error "no ongoing proof"
-let mono_uris_callback ~selection_mode ?title ?msg ?nonvars_button _ =
- raise (Failure "ambiguous input")
-let mono_interp_callback _ = raise (Failure "ambiguous input")
+let get_stack status =
+ match status.proof_status with
+ | Incomplete_proof p -> p.stack
+ | Proof _ -> Continuationals.Stack.empty
+ | _ -> assert false
+let set_stack stack status =
+ match status.proof_status with
+ | Incomplete_proof p ->
+ { status with proof_status = Incomplete_proof { p with stack = stack } }
+ | Proof _ ->
+ assert (Continuationals.Stack.is_empty stack);
+ status
+ | _ -> assert false
+
projects / helm.git / blobdiff