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