(* Title: Pure/ProofGeneral/pgip_output.ML
Author: David Aspinall
PGIP abstraction: output commands.
*)
signature PGIPOUTPUT =
sig
(* These are the PGIP messages which the prover emits. *)
datatype pgipoutput =
Normalresponse of { content: XML.tree list }
| Errorresponse of { fatality: PgipTypes.fatality,
location: PgipTypes.location option,
content: XML.tree list }
| Informfileloaded of { url: PgipTypes.pgipurl, completed: bool }
| Informfileoutdated of { url: PgipTypes.pgipurl, completed: bool }
| Informfileretracted of { url: PgipTypes.pgipurl, completed: bool }
| Metainforesponse of { attrs: XML.attributes,
content: XML.tree list }
| Lexicalstructure of { content: XML.tree list }
| Proverinfo of { name: string,
version: string,
instance: string,
descr: string,
url: Url.T,
filenameextns: string }
| Setids of { idtables: PgipTypes.idtable list }
| Delids of { idtables: PgipTypes.idtable list }
| Addids of { idtables: PgipTypes.idtable list }
| Hasprefs of { prefcategory: string option,
prefs: PgipTypes.preference list }
| Prefval of { name: string, value: string }
| Setrefs of { url: PgipTypes.pgipurl option,
thyname: PgipTypes.objname option,
objtype: PgipTypes.objtype option,
name: PgipTypes.objname option,
idtables: PgipTypes.idtable list,
fileurls : PgipTypes.pgipurl list }
| Idvalue of { thyname: PgipTypes.objname option,
objtype: PgipTypes.objtype,
name: PgipTypes.objname,
text: XML.tree list }
| Informguise of { file : PgipTypes.pgipurl option,
theory: PgipTypes.objname option,
theorem: PgipTypes.objname option,
proofpos: int option }
| Parseresult of { attrs: XML.attributes, doc:PgipMarkup.pgipdocument,
errs: XML.tree list } (* errs to become PGML *)
| Usespgip of { version: string,
pgipelems: (string * bool * string list) list }
| Usespgml of { version: string }
| Pgip of { tag: string option,
class: string,
seq: int, id: string,
destid: string option,
refid: string option,
refseq: int option,
content: XML.tree list }
| Ready of { }
val output : pgipoutput -> XML.tree
end
structure PgipOutput : PGIPOUTPUT =
struct
open PgipTypes
datatype pgipoutput =
Normalresponse of { content: XML.tree list }
| Errorresponse of { fatality: fatality,
location: location option,
content: XML.tree list }
| Informfileloaded of { url: Path.T, completed: bool }
| Informfileoutdated of { url: Path.T, completed: bool }
| Informfileretracted of { url: Path.T, completed: bool }
| Metainforesponse of { attrs: XML.attributes, content: XML.tree list }
| Lexicalstructure of { content: XML.tree list }
| Proverinfo of { name: string, version: string, instance: string,
descr: string, url: Url.T, filenameextns: string }
| Setids of { idtables: PgipTypes.idtable list }
| Delids of { idtables: PgipTypes.idtable list }
| Addids of { idtables: PgipTypes.idtable list }
| Hasprefs of { prefcategory: string option, prefs: preference list }
| Prefval of { name: string, value: string }
| Idvalue of { thyname: PgipTypes.objname option,
objtype: PgipTypes.objtype,
name: PgipTypes.objname,
text: XML.tree list }
| Setrefs of { url: PgipTypes.pgipurl option,
thyname: PgipTypes.objname option,
objtype: PgipTypes.objtype option,
name: PgipTypes.objname option,
idtables: PgipTypes.idtable list,
fileurls : PgipTypes.pgipurl list }
| Informguise of { file : PgipTypes.pgipurl option,
theory: PgipTypes.objname option,
theorem: PgipTypes.objname option,
proofpos: int option }
| Parseresult of { attrs: XML.attributes, doc: PgipMarkup.pgipdocument,
errs: XML.tree list } (* errs to become PGML *)
| Usespgip of { version: string,
pgipelems: (string * bool * string list) list }
| Usespgml of { version: string }
| Pgip of { tag: string option,
class: string,
seq: int, id: string,
destid: string option,
refid: string option,
refseq: int option,
content: XML.tree list }
| Ready of { }
(* Construct output XML messages *)
fun normalresponse (Normalresponse vs) =
let
val content = #content vs
in
XML.Elem (("normalresponse", []), content)
end
fun errorresponse (Errorresponse vs) =
let
val fatality = #fatality vs
val location = #location vs
val content = #content vs
in
XML.Elem (("errorresponse",
attrs_of_fatality fatality @
these (Option.map attrs_of_location location)),
content)
end
fun informfileloaded (Informfileloaded vs) =
let
val url = #url vs
val completed = #completed vs
in
XML.Elem (("informfileloaded",
attrs_of_pgipurl url @
(attr "completed" (PgipTypes.bool_to_pgstring completed))),
[])
end
fun informfileoutdated (Informfileoutdated vs) =
let
val url = #url vs
val completed = #completed vs
in
XML.Elem (("informfileoutdated",
attrs_of_pgipurl url @
(attr "completed" (PgipTypes.bool_to_pgstring completed))),
[])
end
fun informfileretracted (Informfileretracted vs) =
let
val url = #url vs
val completed = #completed vs
in
XML.Elem (("informfileretracted",
attrs_of_pgipurl url @
(attr "completed" (PgipTypes.bool_to_pgstring completed))),
[])
end
fun metainforesponse (Metainforesponse vs) =
let
val attrs = #attrs vs
val content = #content vs
in
XML.Elem (("metainforesponse", attrs), content)
end
fun lexicalstructure (Lexicalstructure vs) =
let
val content = #content vs
in
XML.Elem (("lexicalstructure", []), content)
end
fun proverinfo (Proverinfo vs) =
let
val name = #name vs
val version = #version vs
val instance = #instance vs
val descr = #descr vs
val url = #url vs
val filenameextns = #filenameextns vs
in
XML.Elem (("proverinfo",
[("name", name),
("version", version),
("instance", instance),
("descr", descr),
("url", Url.implode url),
("filenameextns", filenameextns)]),
[])
end
fun setids (Setids vs) =
let
val idtables = #idtables vs
in
XML.Elem (("setids", []), map idtable_to_xml idtables)
end
fun setrefs (Setrefs vs) =
let
val url = #url vs
val thyname = #thyname vs
val objtype = #objtype vs
val name = #name vs
val idtables = #idtables vs
val fileurls = #fileurls vs
fun fileurl_to_xml url = XML.Elem (("fileurl", attrs_of_pgipurl url), [])
in
XML.Elem (("setrefs",
(the_default [] (Option.map attrs_of_pgipurl url)) @
(the_default [] (Option.map attrs_of_objtype objtype)) @
(opt_attr "thyname" thyname) @
(opt_attr "name" name)),
(map idtable_to_xml idtables) @
(map fileurl_to_xml fileurls))
end
fun addids (Addids vs) =
let
val idtables = #idtables vs
in
XML.Elem (("addids", []), map idtable_to_xml idtables)
end
fun delids (Delids vs) =
let
val idtables = #idtables vs
in
XML.Elem (("delids", []), map idtable_to_xml idtables)
end
fun hasprefs (Hasprefs vs) =
let
val prefcategory = #prefcategory vs
val prefs = #prefs vs
in
XML.Elem (("hasprefs", opt_attr "prefcategory" prefcategory), map haspref prefs)
end
fun prefval (Prefval vs) =
let
val name = #name vs
val value = #value vs
in
XML.Elem (("prefval", attr "name" name), [XML.Text value])
end
fun idvalue (Idvalue vs) =
let
val objtype_attrs = attrs_of_objtype (#objtype vs)
val thyname = #thyname vs
val name = #name vs
val text = #text vs
in
XML.Elem (("idvalue",
objtype_attrs @
(opt_attr "thyname" thyname) @
attr "name" name),
text)
end
fun informguise (Informguise vs) =
let
val file = #file vs
val theory = #theory vs
val theorem = #theorem vs
val proofpos = #proofpos vs
fun elto nm attrfn xo = case xo of NONE => [] | SOME x => [XML.Elem ((nm, attrfn x), [])]
val guisefile = elto "guisefile" attrs_of_pgipurl file
val guisetheory = elto "guisetheory" (single o (pair "thyname")) theory
val guiseproof = elto "guiseproof"
(fn thm=>(attr "thmname" thm) @
(opt_attr "proofpos" (Option.map string_of_int proofpos))) theorem
in
XML.Elem (("informguise", []), guisefile @ guisetheory @ guiseproof)
end
fun parseresult (Parseresult vs) =
let
val attrs = #attrs vs
val doc = #doc vs
val errs = #errs vs
val xmldoc = PgipMarkup.output_doc doc
in
XML.Elem (("parseresult", attrs), errs @ xmldoc)
end
fun acceptedpgipelems (Usespgip vs) =
let
val pgipelems = #pgipelems vs
fun async_attrs b = if b then attr "async" "true" else []
fun attrs_attrs attrs = if attrs=[] then [] else attr "attributes" (space_implode "," attrs)
fun singlepgipelem (e,async,attrs) =
XML.Elem (("pgipelem", async_attrs async @ attrs_attrs attrs), [XML.Text e])
in
XML.Elem (("acceptedpgipelems", []), map singlepgipelem pgipelems)
end
fun usespgip (Usespgip vs) =
let
val version = #version vs
val acceptedelems = acceptedpgipelems (Usespgip vs)
in
XML.Elem (("usespgip", attr "version" version), [acceptedelems])
end
fun usespgml (Usespgml vs) =
let
val version = #version vs
in
XML.Elem (("usespgml", attr "version" version), [])
end
fun pgip (Pgip vs) =
let
val tag = #tag vs
val class = #class vs
val seq = #seq vs
val id = #id vs
val destid = #destid vs
val refid = #refid vs
val refseq = #refseq vs
val content = #content vs
in
XML.Elem(("pgip",
opt_attr "tag" tag @
attr "id" id @
opt_attr "destid" destid @
attr "class" class @
opt_attr "refid" refid @
opt_attr_map string_of_int "refseq" refseq @
attr "seq" (string_of_int seq)),
content)
end
fun ready (Ready _) = XML.Elem (("ready", []), [])
fun output pgipoutput = case pgipoutput of
Normalresponse _ => normalresponse pgipoutput
| Errorresponse _ => errorresponse pgipoutput
| Informfileloaded _ => informfileloaded pgipoutput
| Informfileoutdated _ => informfileoutdated pgipoutput
| Informfileretracted _ => informfileretracted pgipoutput
| Metainforesponse _ => metainforesponse pgipoutput
| Lexicalstructure _ => lexicalstructure pgipoutput
| Proverinfo _ => proverinfo pgipoutput
| Setids _ => setids pgipoutput
| Setrefs _ => setrefs pgipoutput
| Addids _ => addids pgipoutput
| Delids _ => delids pgipoutput
| Hasprefs _ => hasprefs pgipoutput
| Prefval _ => prefval pgipoutput
| Idvalue _ => idvalue pgipoutput
| Informguise _ => informguise pgipoutput
| Parseresult _ => parseresult pgipoutput
| Usespgip _ => usespgip pgipoutput
| Usespgml _ => usespgml pgipoutput
| Pgip _ => pgip pgipoutput
| Ready _ => ready pgipoutput
end