* http://helm.cs.unibo.it/
*)
-class proofStatus ~uri ~typ =
- object
+class proofStatus ~typ ~metasenv ~uri () =
+ object (self)
inherit MatitaTypes.subject
- val mutable _proof = (uri, [ 1, [], typ ], Cic.Meta (1, []), typ)
+ val mutable _proof = (uri, (1, [], typ) :: metasenv, Cic.Meta (1, []), typ)
val mutable _goal = Some 1
method proof = _proof
_proof <- p;
_goal <- Some g
- method to_xml =
+ method toXml =
let (uri, metasenv, bo, ty) = _proof in
let currentproof =
(* TODO CSC: Wrong: [] is just plainly wrong *)
- Cic.CurrentProof (UriManager.name_of_uri uri,metasenv,bo,ty,[])
+ Cic.CurrentProof (UriManager.name_of_uri uri,metasenv, bo, ty, [])
in
let (acurrentproof,_,_,ids_to_inner_sorts,_,_,_) =
Cic2acic.acic_object_of_cic_object ~eta_fix:false currentproof
in
(xml, bodyxml)
+ method toString =
+ let (xml, bodyxml) = self#toXml in
+ let buf = Buffer.create 10240 in
+ Buffer.add_string buf "<?xml version=\"1.0\" encoding=\"ISO-8859-1\"?>\n";
+ Buffer.add_string buf "<!DOCTYPE ConstantType SYSTEM \"http://mowgli.cs.unibo.it:58081/getdtd?uri=cic.dtd\">\n";
+ Buffer.add_string buf "<ProofStatus>\n";
+ Buffer.add_string buf (Misc.strip_xml_headings (Xml.pp_to_string xml));
+ Buffer.add_string buf (Misc.strip_xml_headings(Xml.pp_to_string bodyxml));
+ Buffer.add_string buf
+ (match _goal with
+ | None -> "<CurrentGoal />"
+ | Some goal -> Printf.sprintf "<CurrentGoal>%d</CurrentGoal>" goal);
+ Buffer.add_string buf "\n</ProofStatus>";
+ Buffer.contents buf
+
end
-class proof ~uri ~typ =
+let proofStatus ~typ ?(metasenv = []) ?(uri = MatitaTypes.untitled_con_uri) () =
+ new proofStatus ~typ ~metasenv ~uri ()
+
+let proofStatus_of_string s =
+ MatitaTypes.not_implemented "MatitaProof.proofStatus_of_string"
+
+class proof ~typ ?metasenv ?uri () =
object
- val mutable _status = new proofStatus ~uri ~typ
+ val mutable _status = proofStatus ~typ ?metasenv ?uri ()
method status = _status
method setStatus s = _status <- s
end
+let proof = new proof
+
class tacticCommand ~(tactic:ProofEngineTypes.tactic) (status: proofStatus) =
object
val statusBackup = status#status