exception Unbound_identifier of string
+type incomplete_proof = {
+ proof: ProofEngineTypes.proof;
+ stack: Continuationals.Stack.t;
+}
+
type proof_status =
| No_proof
- | Incomplete_proof of ProofEngineTypes.status
+ | 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
type options = option_value StringMap.t
let no_options = StringMap.empty
+type ast_command = (CicNotationPt.term, GrafiteAst.obj) GrafiteAst.command
+type moo = ast_command list * GrafiteAst.metadata list
+
type status = {
- aliases: DisambiguateTypes.environment; (** disambiguation aliases *)
+ aliases: DisambiguateTypes.environment;
+ multi_aliases: DisambiguateTypes.multiple_environment;
+ moo_content_rev: moo;
proof_status: proof_status;
options: options;
- coercions: CoercGraph.coercions;
objects: (UriManager.uri * string) list;
- (** in-scope objects, with their paths *)
+ coercions: UriManager.uri list;
+ notation_ids: CicNotation.notation_id list;
}
+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 }
+
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
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 Failure _ ->
command_error (sprintf "Not an integer value \"%s\"" value))
in
- { status with options = StringMap.add name value status.options }
+ 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 }
+
+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' }
(* subset of MatitaConsole.console methods needed by MatitaInterpreter *)
class type console =
method show : ?msg:string -> unit -> unit
end
+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 *)
+ ]
+
+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 mathViewer =
+ object
+ (** @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
+
+let get_current_proof status =
+ match status.proof_status with
+ | Incomplete_proof { proof = p } -> p
+ | _ -> statement_error "no ongoing proof"
+
+let get_proof_metasenv status =
+ match status.proof_status with
+ | No_proof -> []
+ | Proof (_, metasenv, _, _)
+ | Incomplete_proof { proof = (_, metasenv, _, _) }
+ | Intermediate metasenv ->
+ metasenv
+
+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 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