src/Pure/term_xml.ML
author wenzelm
Tue Jul 12 10:44:30 2011 +0200 (2011-07-12)
changeset 43767 e0219ef7f84c
parent 43731 70072780e095
child 43778 ce9189450447
permissions -rw-r--r--
tuned XML modules;
     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 indexname: indexname T
    11   val sort: sort T
    12   val typ: typ T
    13   val term: term T
    14 end
    15 
    16 signature TERM_XML =
    17 sig
    18   structure Encode: TERM_XML_OPS where type 'a T = 'a XML.Encode.T
    19   structure Decode: TERM_XML_OPS where type 'a T = 'a XML.Decode.T
    20 end;
    21 
    22 structure Term_XML: TERM_XML =
    23 struct
    24 
    25 (* encode *)
    26 
    27 structure Encode =
    28 struct
    29 
    30 open XML.Encode;
    31 
    32 val indexname = pair string int;
    33 
    34 val sort = list string;
    35 
    36 fun typ T = T |> variant
    37  [fn Type x => pair string (list typ) x,
    38   fn TFree x => pair string sort x,
    39   fn TVar x => pair indexname sort x];
    40 
    41 fun term t = t |> variant
    42  [fn Const x => pair string typ x,
    43   fn Free x => pair string typ x,
    44   fn Var x => pair indexname typ x,
    45   fn Bound x => int x,
    46   fn Abs x => triple string typ term x,
    47   fn op $ x => pair term term x];
    48 
    49 end;
    50 
    51 
    52 (* decode *)
    53 
    54 structure Decode =
    55 struct
    56 
    57 open XML.Decode;
    58 
    59 val indexname = pair string int;
    60 
    61 val sort = list string;
    62 
    63 fun typ T = T |> variant
    64  [Type o pair string (list typ),
    65   TFree o pair string sort,
    66   TVar o pair indexname sort];
    67 
    68 fun term t = t |> variant
    69  [Const o pair string typ,
    70   Free o pair string typ,
    71   Var o pair indexname typ,
    72   Bound o int,
    73   Abs o triple string typ term,
    74   op $ o pair term term];
    75 
    76 end;
    77 
    78 end;