src/HOL/Import/xmlconv.ML
author wenzelm
Thu Feb 11 23:00:22 2010 +0100 (2010-02-11)
changeset 35115 446c5063e4fd
parent 32960 69916a850301
child 35129 ed24ba6f69aa
permissions -rw-r--r--
modernized translations;
formal markup of @{syntax_const} and @{const_syntax};
minor tuning;
obua@19064
     1
signature XML_CONV =
obua@19064
     2
sig
obua@19064
     3
  type 'a input = XML.tree -> 'a
obua@19064
     4
  type 'a output = 'a -> XML.tree
obua@19064
     5
obua@19064
     6
  exception ParseException of string
obua@19064
     7
obua@19064
     8
  val xml_of_typ: typ output
obua@19064
     9
  val typ_of_xml: typ input
obua@19064
    10
obua@19064
    11
  val xml_of_term: term output
obua@19064
    12
  val term_of_xml : term input
obua@19064
    13
obua@19064
    14
  val xml_of_mixfix: mixfix output
obua@19064
    15
  val mixfix_of_xml: mixfix input
obua@19064
    16
  
obua@19064
    17
  val xml_of_proof: Proofterm.proof output
obua@19064
    18
obua@19064
    19
  val xml_of_bool: bool output
obua@19064
    20
  val bool_of_xml: bool input
wenzelm@32960
    21
                  
obua@19064
    22
  val xml_of_int: int output
obua@19064
    23
  val int_of_xml: int input
obua@19064
    24
obua@19064
    25
  val xml_of_string: string output
obua@19064
    26
  val string_of_xml: string input
obua@19064
    27
obua@19064
    28
  val xml_of_list: 'a output -> 'a list output
obua@19064
    29
  val list_of_xml: 'a input -> 'a list input
obua@19064
    30
  
obua@19064
    31
  val xml_of_tuple : 'a output -> 'a list output
obua@19064
    32
  val tuple_of_xml: 'a input -> int -> 'a list input
obua@19064
    33
obua@19064
    34
  val xml_of_option: 'a output -> 'a option output
obua@19064
    35
  val option_of_xml: 'a input -> 'a option input
obua@19064
    36
obua@19064
    37
  val xml_of_pair: 'a output -> 'b output -> ('a * 'b) output
obua@19064
    38
  val pair_of_xml: 'a input -> 'b input -> ('a * 'b) input
obua@19064
    39
obua@19064
    40
  val xml_of_triple: 'a output -> 'b output -> 'c output -> ('a * 'b * 'c) output
obua@19064
    41
  val triple_of_xml: 'a input -> 'b input -> 'c input -> ('a * 'b * 'c) input
obua@19064
    42
  
obua@19064
    43
  val xml_of_unit: unit output
obua@19064
    44
  val unit_of_xml: unit input
obua@19064
    45
obua@19064
    46
  val xml_of_quadruple: 'a output -> 'b output -> 'c output -> 'd output -> ('a * 'b * 'c * 'd) output
obua@19064
    47
  val quadruple_of_xml: 'a input -> 'b input -> 'c input -> 'd input -> ('a * 'b * 'c * 'd) input
obua@19064
    48
obua@19064
    49
  val xml_of_quintuple: 'a output -> 'b output -> 'c output -> 'd output -> 'e output -> ('a * 'b * 'c * 'd * 'e) output
obua@19064
    50
  val quintuple_of_xml: 'a input -> 'b input -> 'c input -> 'd input -> 'e input -> ('a * 'b * 'c * 'd * 'e) input
obua@19064
    51
obua@19064
    52
  val wrap : string -> 'a output -> 'a output
obua@19064
    53
  val unwrap : ('a -> 'b) -> 'a input -> 'b input
obua@19064
    54
  val wrap_empty : string output
obua@19064
    55
  val unwrap_empty : 'a -> 'a input
obua@19064
    56
  val name_of_wrap : XML.tree -> string
obua@19064
    57
obua@19064
    58
  val write_to_file: 'a output -> string -> 'a -> unit
obua@19064
    59
  val read_from_file: 'a input -> string -> 'a
obua@19089
    60
obua@19089
    61
  val serialize_to_file : 'a output -> string -> 'a -> unit
obua@19089
    62
  val deserialize_from_file : 'a input -> string -> 'a
obua@19064
    63
end;
obua@19064
    64
obua@19064
    65
structure XMLConv : XML_CONV =
obua@19064
    66
struct
obua@19064
    67
  
obua@19064
    68
type 'a input = XML.tree -> 'a
obua@19064
    69
type 'a output = 'a -> XML.tree
obua@19064
    70
exception ParseException of string
obua@19064
    71
obua@19064
    72
fun parse_err s = raise ParseException s
obua@19064
    73
obua@19064
    74
fun xml_of_class name = XML.Elem ("class", [("name", name)], []);
obua@19064
    75
obua@19064
    76
fun class_of_xml (XML.Elem ("class", [("name", name)], [])) = name
obua@19064
    77
  | class_of_xml _ = parse_err "class"
obua@19064
    78
 
obua@19064
    79
fun xml_of_typ (TVar ((s, i), S)) = XML.Elem ("TVar",
obua@19064
    80
      ("name", s) :: (if i=0 then [] else [("index", string_of_int i)]),
obua@19064
    81
      map xml_of_class S)
obua@19064
    82
  | xml_of_typ (TFree (s, S)) =
obua@19064
    83
      XML.Elem ("TFree", [("name", s)], map xml_of_class S)
obua@19064
    84
  | xml_of_typ (Type (s, Ts)) =
obua@19064
    85
      XML.Elem ("Type", [("name", s)], map xml_of_typ Ts);
obua@19064
    86
obua@19064
    87
fun intofstr s i = 
obua@19064
    88
    case Int.fromString i of 
wenzelm@32960
    89
        NONE => parse_err (s^", invalid index: "^i)
obua@19064
    90
      | SOME i => i
obua@19064
    91
obua@19064
    92
fun typ_of_xml (XML.Elem ("TVar", [("name", s)], cs)) = TVar ((s,0), map class_of_xml cs)
obua@19064
    93
  | typ_of_xml (XML.Elem ("TVar", [("name", s), ("index", i)], cs)) = 
obua@19064
    94
    TVar ((s, intofstr "TVar" i), map class_of_xml cs)
obua@19064
    95
  | typ_of_xml (XML.Elem ("TFree", [("name", s)], cs)) = TFree (s, map class_of_xml cs)
obua@19064
    96
  | typ_of_xml (XML.Elem ("Type", [("name", s)], ts)) = Type (s, map typ_of_xml ts)
obua@19064
    97
  | typ_of_xml _ = parse_err "type"
obua@19064
    98
obua@19064
    99
fun xml_of_term (Bound i) =
obua@19064
   100
      XML.Elem ("Bound", [("index", string_of_int i)], [])
obua@19064
   101
  | xml_of_term (Free (s, T)) =
obua@19064
   102
      XML.Elem ("Free", [("name", s)], [xml_of_typ T])
obua@19064
   103
  | xml_of_term (Var ((s, i), T)) = XML.Elem ("Var",
obua@19064
   104
      ("name", s) :: (if i=0 then [] else [("index", string_of_int i)]),
obua@19064
   105
      [xml_of_typ T])
obua@19064
   106
  | xml_of_term (Const (s, T)) =
obua@19064
   107
      XML.Elem ("Const", [("name", s)], [xml_of_typ T])
obua@19064
   108
  | xml_of_term (t $ u) =
obua@19064
   109
      XML.Elem ("App", [], [xml_of_term t, xml_of_term u])
obua@19064
   110
  | xml_of_term (Abs (s, T, t)) =
obua@19064
   111
      XML.Elem ("Abs", [("vname", s)], [xml_of_typ T, xml_of_term t]);
obua@19064
   112
obua@19064
   113
fun term_of_xml (XML.Elem ("Bound", [("index", i)], [])) = Bound (intofstr "Bound" i)
obua@19064
   114
  | term_of_xml (XML.Elem ("Free", [("name", s)], [T])) = Free (s, typ_of_xml T)
obua@19064
   115
  | term_of_xml (XML.Elem ("Var",[("name", s)], [T])) = Var ((s,0), typ_of_xml T)
obua@19064
   116
  | term_of_xml (XML.Elem ("Var",[("name", s), ("index", i)], [T])) = Var ((s,intofstr "Var" i), typ_of_xml T)
obua@19064
   117
  | term_of_xml (XML.Elem ("Const", [("name", s)], [T])) = Const (s, typ_of_xml T)
obua@19064
   118
  | term_of_xml (XML.Elem ("App", [], [t, u])) = (term_of_xml t) $ (term_of_xml u)
obua@19064
   119
  | term_of_xml (XML.Elem ("Abs", [("vname", s)], [T, t])) = Abs (s, typ_of_xml T, term_of_xml t)
obua@19064
   120
  | term_of_xml _ = parse_err "term"
obua@19064
   121
obua@19064
   122
fun xml_of_opttypes NONE = []
obua@19064
   123
  | xml_of_opttypes (SOME Ts) = [XML.Elem ("types", [], map xml_of_typ Ts)];
obua@19064
   124
obua@19064
   125
(* FIXME: the t argument of PThm and PAxm is actually redundant, since *)
obua@19064
   126
(* it can be looked up in the theorem database. Thus, it could be      *)
obua@19064
   127
(* omitted from the xml representation.                                *)
obua@19064
   128
obua@19064
   129
fun xml_of_proof (PBound i) =
obua@19064
   130
      XML.Elem ("PBound", [("index", string_of_int i)], [])
obua@19064
   131
  | xml_of_proof (Abst (s, optT, prf)) =
obua@19064
   132
      XML.Elem ("Abst", [("vname", s)],
obua@19064
   133
        (case optT of NONE => [] | SOME T => [xml_of_typ T]) @
obua@19064
   134
        [xml_of_proof prf])
obua@19064
   135
  | xml_of_proof (AbsP (s, optt, prf)) =
obua@19064
   136
      XML.Elem ("AbsP", [("vname", s)],
obua@19064
   137
        (case optt of NONE => [] | SOME t => [xml_of_term t]) @
obua@19064
   138
        [xml_of_proof prf])
obua@19064
   139
  | xml_of_proof (prf % optt) =
obua@19064
   140
      XML.Elem ("Appt", [],
obua@19064
   141
        xml_of_proof prf ::
obua@19064
   142
        (case optt of NONE => [] | SOME t => [xml_of_term t]))
obua@19064
   143
  | xml_of_proof (prf %% prf') =
obua@19064
   144
      XML.Elem ("AppP", [], [xml_of_proof prf, xml_of_proof prf'])
obua@19064
   145
  | xml_of_proof (Hyp t) = XML.Elem ("Hyp", [], [xml_of_term t])
wenzelm@28811
   146
  | xml_of_proof (PThm (_, ((s, t, optTs), _))) =
obua@19064
   147
      XML.Elem ("PThm", [("name", s)], xml_of_term t :: xml_of_opttypes optTs)
obua@19064
   148
  | xml_of_proof (PAxm (s, t, optTs)) =
obua@19064
   149
      XML.Elem ("PAxm", [("name", s)], xml_of_term t :: xml_of_opttypes optTs)
obua@19064
   150
  | xml_of_proof (Oracle (s, t, optTs)) =
obua@19064
   151
      XML.Elem ("Oracle", [("name", s)], xml_of_term t :: xml_of_opttypes optTs)
wenzelm@28811
   152
  | xml_of_proof MinProof = XML.Elem ("MinProof", [], []);
obua@19064
   153
obua@19064
   154
fun xml_of_bool b = XML.Elem ("bool", [("value", if b then "true" else "false")], [])
obua@19064
   155
fun xml_of_int i = XML.Elem ("int", [("value", string_of_int i)], [])
obua@19064
   156
fun xml_of_string s = XML.Elem ("string", [("value", s)], [])
obua@19064
   157
fun xml_of_unit () = XML.Elem ("unit", [], [])
obua@19064
   158
fun xml_of_list output ls = XML.Elem ("list", [], map output ls)
obua@19064
   159
fun xml_of_tuple output ls = XML.Elem ("tuple", [], map output ls)
obua@19064
   160
fun xml_of_option output opt = XML.Elem ("option", [], case opt of NONE => [] | SOME x => [output x])
obua@19064
   161
fun wrap s output x = XML.Elem (s, [], [output x])
obua@19064
   162
fun wrap_empty s = XML.Elem (s, [], [])
obua@19064
   163
fun xml_of_pair output1 output2 (x1, x2) = XML.Elem ("pair", [], [output1 x1, output2 x2])
obua@19064
   164
fun xml_of_triple output1 output2 output3 (x1, x2, x3) = XML.Elem ("triple", [], [output1 x1, output2 x2, output3 x3])
obua@19064
   165
fun xml_of_quadruple output1 output2 output3 output4 (x1, x2, x3, x4) = 
obua@19064
   166
    XML.Elem ("quadruple", [], [output1 x1, output2 x2, output3 x3, output4 x4])
obua@19064
   167
fun xml_of_quintuple output1 output2 output3 output4 output5 (x1, x2, x3, x4, x5) = 
obua@19064
   168
    XML.Elem ("quintuple", [], [output1 x1, output2 x2, output3 x3, output4 x4, output5 x5])
wenzelm@32960
   169
                                                                                  
obua@19064
   170
fun bool_of_xml (XML.Elem ("bool", [("value", "true")], [])) = true
obua@19064
   171
  | bool_of_xml (XML.Elem ("bool", [("value", "false")], [])) = false
obua@19064
   172
  | bool_of_xml _ = parse_err "bool"
obua@19064
   173
obua@19064
   174
fun int_of_xml (XML.Elem ("int", [("value", i)], [])) = intofstr "int" i
obua@19064
   175
  | int_of_xml _ = parse_err "int"
obua@19064
   176
obua@19064
   177
fun unit_of_xml (XML.Elem ("unit", [], [])) = ()
obua@19064
   178
  | unit_of_xml _ = parse_err "unit"
obua@19064
   179
obua@19064
   180
fun list_of_xml input (XML.Elem ("list", [], ls)) = map input ls
obua@19064
   181
  | list_of_xml _ _ = parse_err "list"
obua@19064
   182
obua@19064
   183
fun tuple_of_xml input i (XML.Elem ("tuple", [], ls)) = 
obua@19064
   184
    if i = length ls then map input ls else parse_err "tuple"
obua@19064
   185
  | tuple_of_xml _ _ _ = parse_err "tuple"
obua@19064
   186
obua@19064
   187
fun option_of_xml input (XML.Elem ("option", [], [])) = NONE
obua@19064
   188
  | option_of_xml input (XML.Elem ("option", [], [opt])) = SOME (input opt)
obua@19064
   189
  | option_of_xml _ _ = parse_err "option"
obua@19064
   190
obua@19064
   191
fun pair_of_xml input1 input2 (XML.Elem ("pair", [], [x1, x2])) = (input1 x1, input2 x2)
obua@19064
   192
  | pair_of_xml _ _ _ = parse_err "pair"
obua@19064
   193
obua@19064
   194
fun triple_of_xml input1 input2 input3 (XML.Elem ("triple", [], [x1, x2, x3])) = (input1 x1, input2 x2, input3 x3)
obua@19064
   195
  | triple_of_xml _ _ _ _ = parse_err "triple"
obua@19064
   196
obua@19064
   197
fun quadruple_of_xml input1 input2 input3 input4 (XML.Elem ("quadruple", [], [x1, x2, x3, x4])) = 
obua@19064
   198
    (input1 x1, input2 x2, input3 x3, input4 x4)
obua@19064
   199
  | quadruple_of_xml _ _ _ _ _ = parse_err "quadruple"
obua@19064
   200
obua@19064
   201
fun quintuple_of_xml input1 input2 input3 input4 input5 (XML.Elem ("quintuple", [], [x1, x2, x3, x4, x5])) = 
obua@19064
   202
    (input1 x1, input2 x2, input3 x3, input4 x4, input5 x5)
obua@19064
   203
  | quintuple_of_xml _ _ _ _ _ _ = parse_err "quintuple"
obua@19064
   204
obua@19064
   205
fun unwrap f input (XML.Elem (_, [], [x])) = f (input x)
obua@19064
   206
  | unwrap _ _ _  = parse_err "unwrap"
obua@19064
   207
obua@19064
   208
fun unwrap_empty x (XML.Elem (_, [], [])) = x 
obua@19064
   209
  | unwrap_empty _ _ = parse_err "unwrap_unit"
obua@19064
   210
obua@19064
   211
fun name_of_wrap (XML.Elem (name, _, _)) = name
obua@19064
   212
  | name_of_wrap _ = parse_err "name_of_wrap"
obua@19064
   213
obua@19064
   214
fun string_of_xml (XML.Elem ("string", [("value", s)], [])) = s
obua@19064
   215
  | string_of_xml _ = parse_err "string"
obua@19064
   216
obua@19064
   217
fun xml_of_mixfix NoSyn = wrap_empty "nosyn"
obua@19064
   218
  | xml_of_mixfix Structure = wrap_empty "structure"
obua@19064
   219
  | xml_of_mixfix (Mixfix args) = wrap "mixfix" (xml_of_triple xml_of_string (xml_of_list xml_of_int) xml_of_int) args
obua@19064
   220
  | xml_of_mixfix (Delimfix s) = wrap "delimfix" xml_of_string s
obua@19064
   221
  | xml_of_mixfix (InfixName args) = wrap "infixname" (xml_of_pair xml_of_string xml_of_int) args
obua@19064
   222
  | xml_of_mixfix (InfixlName args) = wrap "infixlname" (xml_of_pair xml_of_string xml_of_int) args
obua@19064
   223
  | xml_of_mixfix (InfixrName args) = wrap "infixrname" (xml_of_pair xml_of_string xml_of_int) args
obua@19064
   224
  | xml_of_mixfix (Infix i) = wrap "infix" xml_of_int i
obua@19064
   225
  | xml_of_mixfix (Infixl i) = wrap "infixl" xml_of_int i
obua@19064
   226
  | xml_of_mixfix (Infixr i) = wrap "infixr" xml_of_int i
obua@19064
   227
  | xml_of_mixfix (Binder args) = wrap "binder" (xml_of_triple xml_of_string xml_of_int xml_of_int) args
wenzelm@32960
   228
                                  
obua@19064
   229
fun mixfix_of_xml e = 
obua@19064
   230
    (case name_of_wrap e of 
wenzelm@32960
   231
         "nosyn" => unwrap_empty NoSyn 
obua@19064
   232
       | "structure" => unwrap_empty Structure 
obua@19064
   233
       | "mixfix" => unwrap Mixfix (triple_of_xml string_of_xml (list_of_xml int_of_xml) int_of_xml)
obua@19064
   234
       | "delimfix" => unwrap Delimfix string_of_xml
obua@19064
   235
       | "infixname" => unwrap InfixName (pair_of_xml string_of_xml int_of_xml) 
obua@19064
   236
       | "infixlname" => unwrap InfixlName (pair_of_xml string_of_xml int_of_xml)  
obua@19064
   237
       | "infixrname" => unwrap InfixrName (pair_of_xml string_of_xml int_of_xml)
obua@19064
   238
       | "infix" => unwrap Infix int_of_xml
obua@19064
   239
       | "infixl" => unwrap Infixl int_of_xml 
obua@19064
   240
       | "infixr" => unwrap Infixr int_of_xml
obua@19064
   241
       | "binder" => unwrap Binder (triple_of_xml string_of_xml int_of_xml int_of_xml)
obua@19064
   242
       | _ => parse_err "mixfix"
obua@19064
   243
    ) e
obua@19064
   244
obua@19064
   245
wenzelm@21858
   246
fun to_file f output fname x = File.write (Path.explode fname) (f (output x))
obua@19064
   247
 
obua@19089
   248
fun from_file f input fname = 
obua@19064
   249
    let
wenzelm@32960
   250
        val _ = writeln "read_from_file enter"
wenzelm@32960
   251
        val s = File.read (Path.explode fname)
wenzelm@32960
   252
        val _ = writeln "done: read file"
wenzelm@32960
   253
        val tree = timeit (fn () => f s)
wenzelm@32960
   254
        val _ = writeln "done: tree"
wenzelm@32960
   255
        val x = timeit (fn () => input tree)
wenzelm@32960
   256
        val _ = writeln "done: input"
obua@19064
   257
    in
wenzelm@32960
   258
        x
obua@19064
   259
    end
obua@19064
   260
obua@19089
   261
fun write_to_file x = to_file XML.string_of_tree x
obua@19089
   262
fun read_from_file x = timeit (fn () => (writeln "read_from_file"; from_file XML.tree_of_string x))
obua@19089
   263
obua@19089
   264
fun serialize_to_file x = to_file XML.encoded_string_of_tree x
obua@19089
   265
fun deserialize_from_file x = timeit (fn () => (writeln "deserialize_from_file"; from_file XML.tree_of_encoded_string x))
obua@19089
   266
obua@19064
   267
end;
obua@19064
   268
obua@19064
   269
structure XMLConvOutput =
obua@19064
   270
struct
obua@19064
   271
open XMLConv
obua@19064
   272
 
obua@19064
   273
val typ = xml_of_typ
obua@19064
   274
val term = xml_of_term
obua@19064
   275
val mixfix = xml_of_mixfix
obua@19064
   276
val proof = xml_of_proof
obua@19064
   277
val bool = xml_of_bool
obua@19064
   278
val int = xml_of_int
obua@19064
   279
val string = xml_of_string
obua@19064
   280
val unit = xml_of_unit
obua@19064
   281
val list = xml_of_list
obua@19064
   282
val pair = xml_of_pair
obua@19064
   283
val option = xml_of_option
obua@19064
   284
val triple = xml_of_triple
obua@19064
   285
val quadruple = xml_of_quadruple
obua@19064
   286
val quintuple = xml_of_quintuple
obua@19064
   287
obua@19064
   288
end
obua@19064
   289
obua@19064
   290
structure XMLConvInput = 
obua@19064
   291
struct
obua@19064
   292
open XMLConv
obua@19064
   293
obua@19064
   294
val typ = typ_of_xml
obua@19064
   295
val term = term_of_xml
obua@19064
   296
val mixfix = mixfix_of_xml
obua@19064
   297
val bool = bool_of_xml
obua@19064
   298
val int = int_of_xml
obua@19064
   299
val string = string_of_xml
obua@19064
   300
val unit = unit_of_xml
obua@19064
   301
val list = list_of_xml
obua@19064
   302
val pair = pair_of_xml
obua@19064
   303
val option = option_of_xml
obua@19064
   304
val triple = triple_of_xml
obua@19064
   305
val quadruple = quadruple_of_xml
obua@19064
   306
val quintuple = quintuple_of_xml
obua@19064
   307
obua@19064
   308
end
obua@19064
   309