src/Tools/Haskell/Term_XML/Encode.hs

more formal references;

{- generated by Isabelle -}

{-  Title:      Tools/Haskell/Term_XML/Encode.hs
    Author:     Makarius
    LICENSE:    BSD 3-clause (Isabelle)

XML data representation of lambda terms.

See also "$ISABELLE_HOME/src/Pure/term_xml.ML".
-}

{-# 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 }]