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