--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/Pure/ProofGeneral/pgip_output.ML Mon Dec 04 20:40:11 2006 +0100
@@ -0,0 +1,366 @@
+(* Title: Pure/ProofGeneral/pgip_output.ML
+ ID: $Id$
+ Author: David Aspinall
+
+PGIP abstraction: output commands
+*)
+
+signature PGIPOUTPUT =
+sig
+ (* These are the PGIP messages which the prover emits. *)
+ datatype pgipoutput =
+ Cleardisplay of { area: PgipTypes.displayarea }
+ | Normalresponse of { area: PgipTypes.displayarea,
+ urgent: bool,
+ messagecategory: PgipTypes.messagecategory,
+ content: XML.tree list }
+ | Errorresponse of { fatality: PgipTypes.fatality,
+ area: PgipTypes.displayarea option,
+ location: PgipTypes.location option,
+ content: XML.tree list }
+ | Informfileloaded of { url: PgipTypes.pgipurl }
+ | Informfileretracted of { url: PgipTypes.pgipurl }
+ | Proofstate of { pgml: XML.tree list }
+ | 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 }
+ | Idtable of { objtype: string,
+ context: string option,
+ ids: string list }
+ | Setids of { idtables: XML.tree list }
+ | Delids of { idtables: XML.tree list }
+ | Addids of { idtables: XML.tree list }
+ | Hasprefs of { prefcategory: string option,
+ prefs: PgipTypes.preference list }
+ | Prefval of { name: string, value: string }
+ | Idvalue of { name: string, objtype: string, text: XML.tree list }
+ | Informguise of { file : PgipTypes.pgipurl option,
+ theory: string option,
+ theorem: string option,
+ proofpos: int option }
+ | Parseresult of { attrs: XML.attributes, content: XML.tree list }
+ | 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 =
+ Cleardisplay of { area: displayarea }
+ | Normalresponse of { area: displayarea, urgent: bool,
+ messagecategory: messagecategory, content: XML.tree list }
+ | Errorresponse of { area: displayarea option, fatality: fatality,
+ location: location option, content: XML.tree list }
+ | Informfileloaded of { url: Path.T }
+ | Informfileretracted of { url: Path.T }
+ | Proofstate of { pgml: XML.tree list }
+ | 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 }
+ | Idtable of { objtype: string, context: string option, ids: string list }
+ | Setids of { idtables: XML.tree list }
+ | Delids of { idtables: XML.tree list }
+ | Addids of { idtables: XML.tree list }
+ | Hasprefs of { prefcategory: string option, prefs: preference list }
+ | Prefval of { name: string, value: string }
+ | Idvalue of { name: string, objtype: string, text: XML.tree list }
+ | Informguise of { file : pgipurl option, theory: string option,
+ theorem: string option, proofpos: int option }
+ | Parseresult of { attrs: XML.attributes, content: XML.tree list }
+ | 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 { }
+
+
+(* util *)
+
+fun attrsome attr f x = case x of NONE => [] | SOME x => [(attr,f x)]
+
+(* Construct output XML messages *)
+
+fun cleardisplay vs =
+ let
+ val area = #area vs
+ in
+ XML.Elem ("cleardisplay", (attrs_of_displayarea area), [])
+ end
+
+fun normalresponse vs =
+ let
+ val area = #area vs
+ val urgent = #urgent vs
+ val messagecategory = #messagecategory vs
+ val content = #content vs
+ in
+ XML.Elem ("normalresponse",
+ (attrs_of_displayarea area) @
+ (if urgent then [("urgent", "true")] else []) @
+ (attrs_of_messagecategory messagecategory),
+ content)
+ end
+
+fun errorresponse vs =
+ let
+ val area = #area vs
+ val fatality = #fatality vs
+ val location = #location vs
+ val content = #content vs
+ in
+ XML.Elem ("errorresponse",
+ (the_default [] (Option.map attrs_of_displayarea area)) @
+ (attrs_of_fatality fatality) @
+ (the_default [] (Option.map attrs_of_location location)),
+ content)
+ end
+
+
+fun informfile lr vs =
+ let
+ val url = #url vs
+ in
+ XML.Elem ("informfile" ^ lr, attrs_of_pgipurl url, [])
+ end
+
+val informfileloaded = informfile "loaded"
+val informfileretracted = informfile "retracted"
+
+fun proofstate vs =
+ let
+ val pgml = #pgml vs
+ in
+ XML.Elem("proofstate", [], pgml)
+ end
+
+fun metainforesponse vs =
+ let
+ val attrs = #attrs vs
+ val content = #content vs
+ in
+ XML.Elem ("metainforesponse", attrs, content)
+ end
+
+fun lexicalstructure vs =
+ let
+ val content = #content vs
+ in
+ XML.Elem ("lexicalstructure", [], content)
+ end
+
+fun 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.pack url),
+ ("filenameextns", filenameextns)],
+ [])
+ end
+
+fun idtable vs =
+ let
+ val objtype = #objtype vs
+ val objtype_attrs = [("objtype", objtype)]
+ val context = #context vs
+ val context_attrs = opt_attr "context" context
+ val ids = #ids vs
+ val ids_content = map (fn x => XML.Elem("identifier",[],[XML.Text x])) ids
+ in
+ XML.Elem ("idtable",
+ objtype_attrs @ context_attrs,
+ ids_content)
+ end
+
+fun setids vs =
+ let
+ val idtables = #idtables vs
+ in
+ XML.Elem ("setids",[],idtables)
+ end
+
+fun addids vs =
+ let
+ val idtables = #idtables vs
+ in
+ XML.Elem ("addids",[],idtables)
+ end
+
+fun delids vs =
+ let
+ val idtables = #idtables vs
+ in
+ XML.Elem ("delids",[],idtables)
+ end
+
+
+fun acceptedpgipelems vs =
+ let
+ val pgipelems = #pgipelems vs
+ fun async_attrs b = if b then [("async","true")] else []
+ fun attrs_attrs attrs = if attrs=[] then [] else [("attributes",space_implode "," attrs)]
+ fun singlepgipelem (e,async,attrs) =
+ XML.Elem("pgipelem", ((async_attrs async) @ (attrs_attrs attrs)),[])
+
+ in
+ XML.Elem ("acceptedpgipelems", [],
+ map singlepgipelem pgipelems)
+ end
+
+
+fun attro x yo = case yo of NONE => [] | SOME y => [(x,y)] : XML.attributes
+
+fun hasprefs vs =
+ let
+ val prefcategory = #prefcategory vs
+ val prefs = #prefs vs
+ in
+ XML.Elem("hasprefs",attro "prefcategory" prefcategory, map haspref prefs)
+ end
+
+fun prefval vs =
+ let
+ val name = #name vs
+ val value = #value vs
+ in
+ XML.Elem("prefval", [("name",name)], [XML.Text value])
+ end
+
+fun idvalue vs =
+ let
+ val name = #name vs
+ val objtype = #objtype vs
+ val text = #text vs
+ in
+ XML.Elem("idvalue", [("name",name),("objtype",objtype)], text)
+ end
+
+
+fun 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=>[("thmname",thm)]@
+ (attro "proofpos" (Option.map Int.toString proofpos))) theorem
+ in
+ XML.Elem("informguise", [], guisefile @ guisetheory @ guiseproof)
+ end
+
+fun parseresult vs =
+ let
+ val attrs = #attrs vs
+ val content = #content vs
+ in
+ XML.Elem("parseresult", attrs, content)
+ end
+
+fun usespgip vs =
+ let
+ val version = #version vs
+ val acceptedelems = acceptedpgipelems vs
+ in
+ XML.Elem("usespgip", [("version", version)], [acceptedelems])
+ end
+
+fun usespgml vs =
+ let
+ val version = #version vs
+ in
+ XML.Elem("usespgml", [("version", version)], [])
+ end
+
+fun 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 @
+ [("id", id)] @
+ opt_attr "destid" destid @
+ [("class", class)] @
+ opt_attr "refid" refid @
+ opt_attr_map string_of_int "refseq" refseq @
+ [("seq", string_of_int seq)],
+ content)
+ end
+
+fun ready vs =
+ XML.Elem("ready",[],[])
+
+
+fun output pgipoutput = case pgipoutput of
+ Cleardisplay vs => cleardisplay vs
+ | Normalresponse vs => normalresponse vs
+ | Errorresponse vs => errorresponse vs
+ | Informfileloaded vs => informfileloaded vs
+ | Informfileretracted vs => informfileretracted vs
+ | Proofstate vs => proofstate vs
+ | Metainforesponse vs => metainforesponse vs
+ | Lexicalstructure vs => lexicalstructure vs
+ | Proverinfo vs => proverinfo vs
+ | Idtable vs => idtable vs
+ | Setids vs => setids vs
+ | Addids vs => addids vs
+ | Delids vs => delids vs
+ | Hasprefs vs => hasprefs vs
+ | Prefval vs => prefval vs
+ | Idvalue vs => idvalue vs
+ | Informguise vs => informguise vs
+ | Parseresult vs => parseresult vs
+ | Usespgip vs => usespgip vs
+ | Usespgml vs => usespgml vs
+ | Pgip vs => pgip vs
+ | Ready vs => ready vs
+
+end
+