1(* Title: Pure/term_xml.ML 2 Author: Makarius 3 4XML data representation of lambda terms. 5*) 6 7signature TERM_XML_OPS = 8sig 9 type 'a T 10 type 'a P 11 val indexname: indexname P 12 val sort: sort T 13 val typ: typ T 14 val term_raw: term T 15 val typ_body: typ T 16 val term: Consts.T -> term T 17end 18 19signature TERM_XML = 20sig 21 structure Encode: TERM_XML_OPS 22 structure Decode: TERM_XML_OPS 23end; 24 25structure Term_XML: TERM_XML = 26struct 27 28structure Encode = 29struct 30 31open XML.Encode; 32 33fun indexname (a, b) = if b = 0 then [a] else [a, int_atom b]; 34 35val sort = list string; 36 37fun typ T = T |> variant 38 [fn Type (a, b) => ([a], list typ b), 39 fn TFree (a, b) => ([a], sort b), 40 fn TVar (a, b) => (indexname a, sort b)]; 41 42fun term_raw t = t |> variant 43 [fn Const (a, b) => ([a], typ b), 44 fn Free (a, b) => ([a], typ b), 45 fn Var (a, b) => (indexname a, typ b), 46 fn Bound a => ([], int a), 47 fn Abs (a, b, c) => ([a], pair typ term_raw (b, c)), 48 fn op $ a => ([], pair term_raw term_raw a)]; 49 50fun typ_body T = if T = dummyT then [] else typ T; 51 52fun term consts t = t |> variant 53 [fn Const (a, b) => ([a], list typ (Consts.typargs consts (a, b))), 54 fn Free (a, b) => ([a], typ_body b), 55 fn Var (a, b) => (indexname a, typ_body b), 56 fn Bound a => ([], int a), 57 fn Abs (a, b, c) => ([a], pair typ (term consts) (b, c)), 58 fn op $ a => ([], pair (term consts) (term consts) a)]; 59 60end; 61 62structure Decode = 63struct 64 65open XML.Decode; 66 67fun indexname [a] = (a, 0) 68 | indexname [a, b] = (a, int_atom b); 69 70val sort = list string; 71 72fun typ body = body |> variant 73 [fn ([a], b) => Type (a, list typ b), 74 fn ([a], b) => TFree (a, sort b), 75 fn (a, b) => TVar (indexname a, sort b)]; 76 77fun term_raw body = body |> variant 78 [fn ([a], b) => Const (a, typ b), 79 fn ([a], b) => Free (a, typ b), 80 fn (a, b) => Var (indexname a, typ b), 81 fn ([], a) => Bound (int a), 82 fn ([a], b) => let val (c, d) = pair typ term_raw b in Abs (a, c, d) end, 83 fn ([], a) => op $ (pair term_raw term_raw a)]; 84 85fun typ_body [] = dummyT 86 | typ_body body = typ body; 87 88fun term consts body = body |> variant 89 [fn ([a], b) => Const (a, Consts.instance consts (a, list typ b)), 90 fn ([a], b) => Free (a, typ_body b), 91 fn (a, b) => Var (indexname a, typ_body b), 92 fn ([], a) => Bound (int a), 93 fn ([a], b) => let val (c, d) = pair typ (term consts) b in Abs (a, c, d) end, 94 fn ([], a) => op $ (pair (term consts) (term consts) a)]; 95 96end; 97 98end; 99