src/Pure/ProofGeneral/pgip_output.ML

Theorems for converting between wf and wfP are now declared
as hints.

(*  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.content }
    | Errorresponse       of { fatality: PgipTypes.fatality, 
                               area: PgipTypes.displayarea option, 
                               location: PgipTypes.location option, 
                               content: XML.content }
    | Informfileloaded    of { url: PgipTypes.pgipurl, completed: bool }
    | Informfileoutdated  of { url: PgipTypes.pgipurl, completed: bool }
    | Informfileretracted of { url: PgipTypes.pgipurl, completed: bool }
    | Proofstate          of { pgml: XML.content }
    | Metainforesponse    of { attrs: XML.attributes, 
                               content: XML.content }
    | Lexicalstructure    of { content: XML.content }
    | 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 { name: PgipTypes.objname, 
			       objtype: PgipTypes.objtype, 
			       text: XML.content }
    | 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.content } (* 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.content }
    | 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.content }
       | Errorresponse       of { area: displayarea option, fatality: fatality, 
                                  location: location option, content: XML.content }
       | Informfileloaded    of { url: Path.T, completed: bool }
       | Informfileoutdated  of { url: Path.T, completed: bool }
       | Informfileretracted of { url: Path.T, completed: bool }
       | Proofstate          of { pgml: XML.content }
       | Metainforesponse    of { attrs: XML.attributes, content: XML.content }
       | Lexicalstructure    of { content: XML.content }
       | 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 { name: PgipTypes.objname, 
				  objtype: PgipTypes.objtype, 
				  text: XML.content }
       | 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.content } (* 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.content }
       | Ready               of { }


(* Construct output XML messages *)

fun cleardisplay (Cleardisplay vs) =
    let
        val area = #area vs
    in
        XML.Elem ("cleardisplay", attrs_of_displayarea area, [])
    end

fun normalresponse (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 attr "urgent" "true" else []) @
                 attrs_of_messagecategory messagecategory,
                 content)
    end

fun errorresponse (Errorresponse vs) =
    let 
        val area = #area vs
        val fatality = #fatality vs
        val location = #location vs
        val content = #content vs
    in
        XML.Elem ("errorresponse",
                 these (Option.map attrs_of_displayarea area) @
                 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 proofstate (Proofstate vs) =
    let
        val pgml = #pgml vs
    in
        XML.Elem("proofstate", [], pgml)
    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",
		  (Option.getOpt (Option.map attrs_of_pgipurl url,[])) @ 
		  (Option.getOpt (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 name = #name vs
	val objtype_attrs = attrs_of_objtype (#objtype vs)
        val text = #text vs
    in
        XML.Elem("idvalue", attr "name" name @ objtype_attrs, 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 Int.toString 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 vs) = XML.Elem("ready",[],[])


fun output pgipoutput = case pgipoutput of
    Cleardisplay _          => cleardisplay pgipoutput
  | Normalresponse _        => normalresponse pgipoutput
  | Errorresponse _         => errorresponse pgipoutput
  | Informfileloaded _      => informfileloaded pgipoutput
  | Informfileoutdated _    => informfileoutdated pgipoutput
  | Informfileretracted _   => informfileretracted pgipoutput
  | Proofstate _            => proofstate 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