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 See also "$ISABELLE_HOME/src/Pure/term_xml.ML". |
|
10 -} |
|
11 |
|
12 module Isabelle.Term_XML.Decode (sort, typ, term) |
|
13 where |
|
14 |
|
15 import Isabelle.Library |
|
16 import qualified Isabelle.XML as XML |
|
17 import Isabelle.XML.Decode |
|
18 import Isabelle.Term |
|
19 |
|
20 |
|
21 sort :: T Sort |
|
22 sort = list string |
|
23 |
|
24 typ :: T Typ |
|
25 typ ty = |
|
26 ty |> variant |
|
27 [\([a], b) -> Type (a, list typ b), |
|
28 \([a], b) -> TFree (a, sort b), |
|
29 \([a, b], c) -> TVar ((a, int_atom b), sort c)] |
|
30 |
|
31 term :: T Term |
|
32 term t = |
|
33 t |> variant |
|
34 [\([a], b) -> Const (a, typ b), |
|
35 \([a], b) -> Free (a, typ b), |
|
36 \([a, b], c) -> Var ((a, int_atom b), typ c), |
|
37 \([a], []) -> Bound (int_atom a), |
|
38 \([a], b) -> let (c, d) = pair typ term b in Abs (a, c, d), |
|
39 \([], a) -> App (pair term term a)] |
|