69240
|
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)]
|