--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/Tools/Haskell/Term_XML/Decode.hs Mon Nov 05 17:06:50 2018 +0100
@@ -0,0 +1,37 @@
+{- generated by Isabelle -}
+
+{- Title: Tools/Haskell/Term_XML/Decode.hs
+ Author: Makarius
+ LICENSE: BSD 3-clause (Isabelle)
+
+XML data representation of lambda terms.
+-}
+
+module Isabelle.Term_XML.Decode (sort, typ, term)
+where
+
+import Isabelle.Library
+import qualified Isabelle.XML as XML
+import Isabelle.XML.Decode
+import Isabelle.Term
+
+
+sort :: T Sort
+sort = list string
+
+typ :: T Typ
+typ ty =
+ ty |> variant
+ [\([a], b) -> Type (a, list typ b),
+ \([a], b) -> TFree (a, sort b),
+ \([a, b], c) -> TVar ((a, int_atom b), sort c)]
+
+term :: T Term
+term t =
+ t |> variant
+ [\([a], b) -> Const (a, typ b),
+ \([a], b) -> Free (a, typ b),
+ \([a, b], c) -> Var ((a, int_atom b), typ c),
+ \([a], []) -> Bound (int_atom a),
+ \([a], b) -> let (c, d) = pair typ term b in Abs (a, c, d),
+ \([], a) -> App (pair term term a)]