author wenzelm Sun, 01 Aug 2021 23:18:13 +0200 changeset 74100 fb9c119e5b49 parent 74099 0bda15b1b937 child 74101 d804e93ae9ff
more operations;
```--- a/src/Tools/Haskell/Haskell.thy	Sun Aug 01 18:12:32 2021 +0200
@@ -1777,7 +1777,8 @@

Sort, dummyS,

-  Typ(..), dummyT, is_dummyT, Term(..))
+  Typ(..), dummyT, is_dummyT, Term(..),
+  aconv, list_comb, strip_comb, head_of, lambda)
where

import Isabelle.Bytes (Bytes)
@@ -1796,7 +1797,7 @@
Type (Bytes, [Typ])
| TFree (Bytes, Sort)
| TVar (Indexname, Sort)
-  deriving Show
+  deriving (Show, Eq, Ord)

dummyT :: Typ
dummyT = Type (\<open>\<^type_name>\<open>dummy\<close>\<close>, [])
@@ -1813,7 +1814,34 @@
| Bound Int
| Abs (Bytes, Typ, Term)
| App (Term, Term)
-  deriving Show
+  deriving (Show, Eq, Ord)
+
+aconv :: Term -> Term -> Bool
+aconv (App (t1, u1)) (App (t2, u2)) = aconv t1 t2 && aconv u1 u2
+aconv (Abs (_, ty1, t1)) (Abs (_, ty2, t2)) = aconv t1 t2 && ty1 == ty2
+aconv a1 a2 = a1 == a2
+
+list_comb :: Term -> [Term] -> Term
+list_comb f [] = f
+list_comb f (t : ts) = list_comb (App (f, t)) ts
+
+strip_comb :: Term -> (Term, [Term])
+strip_comb tm = strip (tm, [])
+  where
+    strip (App (f, t), ts) = strip (f, t : ts)
+    strip x = x
+