31 fun typ T = T |> variant |
32 fun typ T = T |> variant |
32 [fn Type (a, b) => ([a], list typ b), |
33 [fn Type (a, b) => ([a], list typ b), |
33 fn TFree (a, b) => ([a], sort b), |
34 fn TFree (a, b) => ([a], sort b), |
34 fn TVar ((a, b), c) => ([a, int_atom b], sort c)]; |
35 fn TVar ((a, b), c) => ([a, int_atom b], sort c)]; |
35 |
36 |
36 fun term t = t |> variant |
37 fun term consts t = t |> variant |
|
38 [fn Const (a, b) => ([a], list typ (Consts.typargs consts (a, b))), |
|
39 fn Free (a, b) => ([a], typ b), |
|
40 fn Var ((a, b), c) => ([a, int_atom b], typ c), |
|
41 fn Bound a => ([int_atom a], []), |
|
42 fn Abs (a, b, c) => ([a], pair typ (term consts) (b, c)), |
|
43 fn op $ a => ([], pair (term consts) (term consts) a)]; |
|
44 |
|
45 fun term_raw t = t |> variant |
37 [fn Const (a, b) => ([a], typ b), |
46 [fn Const (a, b) => ([a], typ b), |
38 fn Free (a, b) => ([a], typ b), |
47 fn Free (a, b) => ([a], typ b), |
39 fn Var ((a, b), c) => ([a, int_atom b], typ c), |
48 fn Var ((a, b), c) => ([a, int_atom b], typ c), |
40 fn Bound a => ([int_atom a], []), |
49 fn Bound a => ([int_atom a], []), |
41 fn Abs (a, b, c) => ([a], pair typ term (b, c)), |
50 fn Abs (a, b, c) => ([a], pair typ term_raw (b, c)), |
42 fn op $ a => ([], pair term term a)]; |
51 fn op $ a => ([], pair term_raw term_raw a)]; |
43 |
52 |
44 end; |
53 end; |
45 |
54 |
46 structure Decode = |
55 structure Decode = |
47 struct |
56 struct |
53 fun typ T = T |> variant |
62 fun typ T = T |> variant |
54 [fn ([a], b) => Type (a, list typ b), |
63 [fn ([a], b) => Type (a, list typ b), |
55 fn ([a], b) => TFree (a, sort b), |
64 fn ([a], b) => TFree (a, sort b), |
56 fn ([a, b], c) => TVar ((a, int_atom b), sort c)]; |
65 fn ([a, b], c) => TVar ((a, int_atom b), sort c)]; |
57 |
66 |
58 fun term t = t |> variant |
67 fun term consts t = t |> variant |
|
68 [fn ([a], b) => Const (a, Consts.instance consts (a, list typ b)), |
|
69 fn ([a], b) => Free (a, typ b), |
|
70 fn ([a, b], c) => Var ((a, int_atom b), typ c), |
|
71 fn ([a], []) => Bound (int_atom a), |
|
72 fn ([a], b) => let val (c, d) = pair typ (term consts) b in Abs (a, c, d) end, |
|
73 fn ([], a) => op $ (pair (term consts) (term consts) a)]; |
|
74 |
|
75 fun term_raw t = t |> variant |
59 [fn ([a], b) => Const (a, typ b), |
76 [fn ([a], b) => Const (a, typ b), |
60 fn ([a], b) => Free (a, typ b), |
77 fn ([a], b) => Free (a, typ b), |
61 fn ([a, b], c) => Var ((a, int_atom b), typ c), |
78 fn ([a, b], c) => Var ((a, int_atom b), typ c), |
62 fn ([a], []) => Bound (int_atom a), |
79 fn ([a], []) => Bound (int_atom a), |
63 fn ([a], b) => let val (c, d) = pair typ term b in Abs (a, c, d) end, |
80 fn ([a], b) => let val (c, d) = pair typ term_raw b in Abs (a, c, d) end, |
64 fn ([], a) => op $ (pair term term a)]; |
81 fn ([], a) => op $ (pair term_raw term_raw a)]; |
65 |
82 |
66 end; |
83 end; |
67 |
84 |
68 end; |
85 end; |