src/Pure/ProofGeneral/pgip_input.ML
author haftmann
Wed May 05 18:25:34 2010 +0200 (2010-05-05)
changeset 36692 54b64d4ad524
parent 29606 fedb8be05f24
child 38228 ada3ab6b9085
permissions -rw-r--r--
farewell to old-style mem infixes -- type inference in situations with mem_int and mem_string should provide enough information to resolve the type of (op =)
     1 (*  Title:      Pure/ProofGeneral/pgip_input.ML
     2     Author:     David Aspinall
     3 
     4 PGIP abstraction: input commands.
     5 *)
     6 
     7 signature PGIPINPUT =
     8 sig
     9     (* These are the PGIP commands to which we respond. *) 
    10     datatype pgipinput = 
    11     (* protocol/prover config *)
    12       Askpgip        of { }
    13     | Askpgml        of { } 
    14     | Askconfig      of { }
    15     | Askprefs       of { }
    16     | Setpref        of { name:string, prefcategory:string option, value:string }
    17     | Getpref        of { name:string, prefcategory:string option }
    18     (* prover control *)
    19     | Proverinit     of { }
    20     | Proverexit     of { }
    21     | Setproverflag  of { flagname:string, value: bool }
    22     (* improper proof commands: control proof state *)
    23     | Dostep         of { text: string }
    24     | Undostep       of { times: int }
    25     | Redostep       of { }
    26     | Abortgoal      of { }
    27     | Forget         of { thyname: string option, name: string option, 
    28                           objtype: PgipTypes.objtype option }
    29     | Restoregoal    of { thmname : string }
    30     (* context inspection commands *)
    31     | Askids         of { url: PgipTypes.pgipurl option,
    32                           thyname: PgipTypes.objname option,
    33                           objtype: PgipTypes.objtype option }
    34     | Askrefs        of { url: PgipTypes.pgipurl option,
    35                           thyname: PgipTypes.objname option,
    36                           objtype: PgipTypes.objtype option,
    37                           name: PgipTypes.objname option }
    38     | Showid         of { thyname: PgipTypes.objname option, 
    39                           objtype: PgipTypes.objtype, 
    40                           name: PgipTypes.objname }
    41     | Askguise       of { }
    42     | Parsescript    of { text: string, location: PgipTypes.location,
    43                           systemdata: string option } 
    44     | Showproofstate of { }
    45     | Showctxt       of { }
    46     | Searchtheorems of { arg: string }
    47     | Setlinewidth   of { width: int }
    48     | Viewdoc        of { arg: string }
    49     (* improper theory-level commands *)
    50     | Doitem         of { text: string }
    51     | Undoitem       of { }
    52     | Redoitem       of { }
    53     | Aborttheory    of { }
    54     | Retracttheory  of { thyname: string }
    55     | Loadfile       of { url: PgipTypes.pgipurl }
    56     | Openfile       of { url: PgipTypes.pgipurl }
    57     | Closefile      of { }
    58     | Abortfile      of { }
    59     | Retractfile    of { url: PgipTypes.pgipurl }
    60     | Changecwd      of { url: PgipTypes.pgipurl }
    61     | Systemcmd      of { arg: string }
    62     (* unofficial escape command for debugging *)
    63     | Quitpgip       of { }
    64 
    65     val input: string * XML.attributes * XML.tree list -> pgipinput option  (* raises PGIP *)
    66 end
    67 
    68 structure PgipInput : PGIPINPUT = 
    69 struct
    70 
    71 open PgipTypes
    72 
    73 (*** PGIP input ***)
    74 
    75 datatype pgipinput = 
    76          (* protocol/prover config *)
    77          Askpgip        of { }
    78        | Askpgml        of { } 
    79        | Askconfig      of { }
    80        | Askprefs       of { }
    81        | Setpref        of { name:string, prefcategory:string option, value:string }
    82        | Getpref        of { name:string, prefcategory:string option }
    83        (* prover control *)
    84        | Proverinit     of { }
    85        | Proverexit     of { }
    86        | Setproverflag  of { flagname:string, value: bool }
    87        (* improper proof commands: control proof state *)
    88        | Dostep         of { text: string }
    89        | Undostep       of { times: int }
    90        | Redostep       of { }
    91        | Abortgoal      of { }
    92        | Forget         of { thyname: string option, name: string option, 
    93                              objtype: PgipTypes.objtype option }
    94        | Restoregoal    of { thmname : string }
    95        (* context inspection commands *)
    96        | Askids         of { url: PgipTypes.pgipurl option,
    97                              thyname: PgipTypes.objname option,
    98                              objtype: PgipTypes.objtype option }
    99        | Askrefs        of { url: PgipTypes.pgipurl option,
   100                              thyname: PgipTypes.objname option,
   101                              objtype: PgipTypes.objtype option,
   102                              name: PgipTypes.objname option }
   103        | Showid         of { thyname: PgipTypes.objname option, 
   104                              objtype: PgipTypes.objtype, 
   105                              name: PgipTypes.objname }
   106        | Askguise       of { }
   107        | Parsescript    of { text: string, location: location,
   108                              systemdata: string option } 
   109        | Showproofstate of { }
   110        | Showctxt       of { }
   111        | Searchtheorems of { arg: string }
   112        | Setlinewidth   of { width: int }
   113        | Viewdoc        of { arg: string }
   114        (* improper theory-level commands *)
   115        | Doitem         of { text: string }
   116        | Undoitem       of { }
   117        | Redoitem       of { }
   118        | Aborttheory    of { }
   119        | Retracttheory  of { thyname: string }
   120        | Loadfile       of { url: pgipurl }
   121        | Openfile       of { url: pgipurl }
   122        | Closefile      of { }
   123        | Abortfile      of { }
   124        | Retractfile    of { url: pgipurl }
   125        | Changecwd      of { url: pgipurl }
   126        | Systemcmd      of { arg: string }
   127        (* unofficial escape command for debugging *)
   128        | Quitpgip       of { }
   129 
   130 (* Extracting content from input XML elements to make a PGIPinput *)
   131 local
   132 
   133     val thyname_attro = get_attr_opt "thyname"
   134     val thyname_attr = get_attr "thyname"
   135     val name_attr = get_attr "name"
   136     val name_attro = get_attr_opt "name"
   137     val thmname_attr = get_attr "thmname"
   138     val flagname_attr = get_attr "flagname"
   139     val value_attr = get_attr "value"
   140 
   141     fun objtype_attro attrs = if has_attr "objtype" attrs then
   142                                   SOME (objtype_of_attrs attrs)
   143                               else NONE
   144 
   145     fun pgipurl_attro attrs = if has_attr "url" attrs then
   146                                   SOME (pgipurl_of_attrs attrs)
   147                               else NONE
   148 
   149     val times_attr = read_pgipnat o (get_attr_dflt "times" "1")
   150     val prefcat_attr = get_attr_opt "prefcategory"
   151 
   152     fun xmltext (XML.Text text :: ts) = text ^ xmltext ts
   153       | xmltext [] = ""
   154       | xmltext _ = raise PGIP "Expected text (PCDATA/CDATA)"
   155 
   156     exception Unknown
   157     exception NoAction
   158 in
   159 
   160 (* Return a valid PGIP input command.
   161    Raise PGIP exception for invalid data.
   162    Return NONE for unknown/unhandled commands. 
   163 *)
   164 fun input (elem, attrs, data) =
   165 SOME 
   166  (case elem of 
   167      "askpgip"        => Askpgip { }
   168    | "askpgml"        => Askpgml { }
   169    | "askconfig"      => Askconfig { }
   170    (* proverconfig *)
   171    | "askprefs"       => Askprefs { }
   172    | "getpref"        => Getpref { name = name_attr attrs, 
   173                                    prefcategory = prefcat_attr attrs }
   174    | "setpref"        => Setpref { name = name_attr attrs, 
   175                                    prefcategory = prefcat_attr attrs,
   176                                    value = xmltext data }
   177    (* provercontrol *)
   178    | "proverinit"     => Proverinit { }
   179    | "proverexit"     => Proverexit { }
   180    | "setproverflag"  => Setproverflag { flagname = flagname_attr attrs,
   181                                          value = read_pgipbool (value_attr attrs) }
   182    (* improperproofcmd: improper commands not in script *)
   183    | "dostep"         => Dostep    { text = xmltext data }
   184    | "undostep"       => Undostep  { times = times_attr attrs }
   185    | "redostep"       => Redostep  { } 
   186    | "abortgoal"      => Abortgoal { }
   187    | "forget"         => Forget { thyname = thyname_attro attrs, 
   188                                   name = name_attro attrs,
   189                                   objtype = objtype_attro attrs }
   190    | "restoregoal"    => Restoregoal { thmname = thmname_attr attrs}
   191    (* proofctxt: improper commands *)
   192    | "askids"         => Askids { url = pgipurl_attro attrs,
   193                                   thyname = thyname_attro attrs, 
   194                                   objtype = objtype_attro attrs }
   195    | "askrefs"        => Askrefs { url = pgipurl_attro attrs,
   196                                    thyname = thyname_attro attrs, 
   197                                    objtype = objtype_attro attrs,
   198                                    name = name_attro attrs }
   199    | "showid"         => Showid { thyname = thyname_attro attrs,
   200                                   objtype = objtype_of_attrs attrs,
   201                                   name = name_attr attrs }
   202    | "askguise"       => Askguise { }
   203    | "parsescript"    => Parsescript { text = (xmltext data),
   204                                        systemdata = get_attr_opt "systemdata" attrs,
   205                                        location = location_of_attrs attrs }
   206    | "showproofstate" => Showproofstate { }
   207    | "showctxt"       => Showctxt { }
   208    | "searchtheorems" => Searchtheorems { arg = xmltext data }
   209    | "setlinewidth"   => Setlinewidth   { width = read_pgipnat (xmltext data) }
   210    | "viewdoc"        => Viewdoc { arg = xmltext data }
   211    (* improperfilecmd: theory-level commands not in script *)
   212    | "doitem"         => Doitem  { text = xmltext data }
   213    | "undoitem"       => Undoitem { }
   214    | "redoitem"       => Redoitem { }
   215    | "aborttheory"    => Aborttheory { }
   216    | "retracttheory"  => Retracttheory { thyname = thyname_attr attrs }
   217    | "loadfile"       => Loadfile { url = pgipurl_of_attrs attrs }
   218    | "openfile"       => Openfile { url = pgipurl_of_attrs attrs }
   219    | "closefile"      => Closefile { }
   220    | "abortfile"      => Abortfile { }
   221    | "retractfile"    => Retractfile { url = pgipurl_of_attrs attrs }
   222    | "changecwd"      => Changecwd { url = pgipurl_of_attrs attrs }
   223    | "systemcmd"      => Systemcmd { arg = xmltext data }
   224    (* unofficial command for debugging *)
   225    | "quitpgip" => Quitpgip { }
   226 
   227    (* We allow sending proper document markup too; we map it back to dostep   *)
   228    (* and strip out metainfo elements. Markup correctness isn't checked: this *)
   229    (* is a compatibility measure to make it easy for interfaces.              *)
   230    | x => if member (op =) PgipMarkup.doc_markup_elements x then
   231               if member (op =) PgipMarkup.doc_markup_elements_ignored x then
   232                   raise NoAction
   233               else 
   234                   Dostep { text = xmltext data } (* could separate out Doitem too *)
   235           else raise Unknown) 
   236     handle Unknown => NONE | NoAction => NONE
   237 end
   238 
   239 end