--- a/src/Tools/Haskell/Term_XML/Encode.hs Fri Nov 30 23:30:42 2018 +0100
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,41 +0,0 @@
-{- 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 }]