src/Pure/term_xml.ML
author wenzelm
Fri Oct 07 21:16:48 2016 +0200 (2016-10-07)
changeset 64092 95469c544b82
parent 43789 321ebd051897
permissions -rw-r--r--
accept obscure timezone used in 2011;
wenzelm@43729
     1
(*  Title:      Pure/term_xml.ML
wenzelm@43729
     2
    Author:     Makarius
wenzelm@43729
     3
wenzelm@43729
     4
XML data representation of lambda terms.
wenzelm@43729
     5
*)
wenzelm@43729
     6
wenzelm@43729
     7
signature TERM_XML_OPS =
wenzelm@43729
     8
sig
wenzelm@43729
     9
  type 'a T
wenzelm@43729
    10
  val sort: sort T
wenzelm@43729
    11
  val typ: typ T
wenzelm@43729
    12
  val term: term T
wenzelm@43729
    13
end
wenzelm@43729
    14
wenzelm@43729
    15
signature TERM_XML =
wenzelm@43729
    16
sig
wenzelm@43779
    17
  structure Encode: TERM_XML_OPS
wenzelm@43779
    18
  structure Decode: TERM_XML_OPS
wenzelm@43729
    19
end;
wenzelm@43729
    20
wenzelm@43729
    21
structure Term_XML: TERM_XML =
wenzelm@43729
    22
struct
wenzelm@43729
    23
wenzelm@43731
    24
structure Encode =
wenzelm@43729
    25
struct
wenzelm@43729
    26
wenzelm@43767
    27
open XML.Encode;
wenzelm@43729
    28
wenzelm@43730
    29
val sort = list string;
wenzelm@43729
    30
wenzelm@43729
    31
fun typ T = T |> variant
wenzelm@43789
    32
 [fn Type (a, b) => ([a], list typ b),
wenzelm@43778
    33
  fn TFree (a, b) => ([a], sort b),
wenzelm@43778
    34
  fn TVar ((a, b), c) => ([a, int_atom b], sort c)];
wenzelm@43729
    35
wenzelm@43729
    36
fun term t = t |> variant
wenzelm@43778
    37
 [fn Const (a, b) => ([a], typ b),
wenzelm@43778
    38
  fn Free (a, b) => ([a], typ b),
wenzelm@43778
    39
  fn Var ((a, b), c) => ([a, int_atom b], typ c),
wenzelm@43778
    40
  fn Bound a => ([int_atom a], []),
wenzelm@43778
    41
  fn Abs (a, b, c) => ([a], pair typ term (b, c)),
wenzelm@43789
    42
  fn op $ a => ([], pair term term a)];
wenzelm@43729
    43
wenzelm@43729
    44
end;
wenzelm@43729
    45
wenzelm@43731
    46
structure Decode =
wenzelm@43729
    47
struct
wenzelm@43729
    48
wenzelm@43767
    49
open XML.Decode;
wenzelm@43729
    50
wenzelm@43730
    51
val sort = list string;
wenzelm@43729
    52
wenzelm@43729
    53
fun typ T = T |> variant
wenzelm@43778
    54
 [fn ([a], b) => Type (a, list typ b),
wenzelm@43778
    55
  fn ([a], b) => TFree (a, sort b),
wenzelm@43778
    56
  fn ([a, b], c) => TVar ((a, int_atom b), sort c)];
wenzelm@43729
    57
wenzelm@43729
    58
fun term t = t |> variant
wenzelm@43778
    59
 [fn ([a], b) => Const (a, typ b),
wenzelm@43778
    60
  fn ([a], b) => Free (a, typ b),
wenzelm@43778
    61
  fn ([a, b], c) => Var ((a, int_atom b), typ c),
wenzelm@43778
    62
  fn ([a], []) => Bound (int_atom a),
wenzelm@43778
    63
  fn ([a], b) => let val (c, d) = pair typ term b in Abs (a, c, d) end,
wenzelm@43778
    64
  fn ([], a) => op $ (pair term term a)];
wenzelm@43729
    65
wenzelm@43729
    66
end;
wenzelm@43729
    67
wenzelm@43729
    68
end;