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