|
1 {- generated by Isabelle -} |
|
2 |
|
3 {- Title: Tools/Haskell/Term_XML/Decode.hs |
|
4 Author: Makarius |
|
5 LICENSE: BSD 3-clause (Isabelle) |
|
6 |
|
7 XML data representation of lambda terms. |
|
8 -} |
|
9 |
|
10 module Isabelle.Term_XML.Decode (sort, typ, term) |
|
11 where |
|
12 |
|
13 import Isabelle.Library |
|
14 import qualified Isabelle.XML as XML |
|
15 import Isabelle.XML.Decode |
|
16 import Isabelle.Term |
|
17 |
|
18 |
|
19 sort :: T Sort |
|
20 sort = list string |
|
21 |
|
22 typ :: T Typ |
|
23 typ ty = |
|
24 ty |> variant |
|
25 [\([a], b) -> Type (a, list typ b), |
|
26 \([a], b) -> TFree (a, sort b), |
|
27 \([a, b], c) -> TVar ((a, int_atom b), sort c)] |
|
28 |
|
29 term :: T Term |
|
30 term t = |
|
31 t |> variant |
|
32 [\([a], b) -> Const (a, typ b), |
|
33 \([a], b) -> Free (a, typ b), |
|
34 \([a, b], c) -> Var ((a, int_atom b), typ c), |
|
35 \([a], []) -> Bound (int_atom a), |
|
36 \([a], b) -> let (c, d) = pair typ term b in Abs (a, c, d), |
|
37 \([], a) -> App (pair term term a)] |