69240
|
1 |
{- generated by Isabelle -}
|
|
2 |
|
|
3 |
{- Title: Tools/Haskell/Term_XML/Encode.hs
|
|
4 |
Author: Makarius
|
|
5 |
LICENSE: BSD 3-clause (Isabelle)
|
|
6 |
|
|
7 |
XML data representation of lambda terms.
|
|
8 |
-}
|
|
9 |
|
|
10 |
{-# LANGUAGE LambdaCase #-}
|
|
11 |
|
|
12 |
module Isabelle.Term_XML.Encode (sort, typ, term)
|
|
13 |
where
|
|
14 |
|
|
15 |
import Isabelle.Library
|
|
16 |
import qualified Isabelle.XML as XML
|
|
17 |
import Isabelle.XML.Encode
|
|
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 |
[\case { Type (a, b) -> Just ([a], list typ b); _ -> Nothing },
|
|
28 |
\case { TFree (a, b) -> Just ([a], sort b); _ -> Nothing },
|
|
29 |
\case { TVar ((a, b), c) -> Just ([a, int_atom b], sort c); _ -> Nothing }]
|
|
30 |
|
|
31 |
term :: T Term
|
|
32 |
term t =
|
|
33 |
t |> variant
|
|
34 |
[\case { Const (a, b) -> Just ([a], typ b); _ -> Nothing },
|
|
35 |
\case { Free (a, b) -> Just ([a], typ b); _ -> Nothing },
|
|
36 |
\case { Var ((a, b), c) -> Just ([a, int_atom b], typ c); _ -> Nothing },
|
|
37 |
\case { Bound a -> Just ([int_atom a], []); _ -> Nothing },
|
|
38 |
\case { Abs (a, b, c) -> Just ([a], pair typ term (b, c)); _ -> Nothing },
|
|
39 |
\case { App a -> Just ([], pair term term a); _ -> Nothing }]
|