{- generated by Isabelle -}
{- Title: Tools/Haskell/Term_XML/Encode.hs
Author: Makarius
LICENSE: BSD 3-clause (Isabelle)
XML data representation of lambda terms.
-}
{-# LANGUAGE LambdaCase #-}
module Isabelle.Term_XML.Encode (sort, typ, term)
where
import Isabelle.Library
import qualified Isabelle.XML as XML
import Isabelle.XML.Encode
import Isabelle.Term
sort :: T Sort
sort = list string
typ :: T Typ
typ ty =
ty |> variant
[\case { Type (a, b) -> Just ([a], list typ b); _ -> Nothing },
\case { TFree (a, b) -> Just ([a], sort b); _ -> Nothing },
\case { TVar ((a, b), c) -> Just ([a, int_atom b], sort c); _ -> Nothing }]
term :: T Term
term t =
t |> variant
[\case { Const (a, b) -> Just ([a], typ b); _ -> Nothing },
\case { Free (a, b) -> Just ([a], typ b); _ -> Nothing },
\case { Var ((a, b), c) -> Just ([a, int_atom b], typ c); _ -> Nothing },
\case { Bound a -> Just ([int_atom a], []); _ -> Nothing },
\case { Abs (a, b, c) -> Just ([a], pair typ term (b, c)); _ -> Nothing },
\case { App a -> Just ([], pair term term a); _ -> Nothing }]