aboutsummaryrefslogtreecommitdiff
path: root/test/Arith
diff options
context:
space:
mode:
Diffstat (limited to 'test/Arith')
-rw-r--r--test/Arith/NonBase.hs45
1 files changed, 45 insertions, 0 deletions
diff --git a/test/Arith/NonBase.hs b/test/Arith/NonBase.hs
new file mode 100644
index 0000000..79c4428
--- /dev/null
+++ b/test/Arith/NonBase.hs
@@ -0,0 +1,45 @@
+{-# LANGUAGE StandaloneDeriving #-}
+{-# LANGUAGE GADTs #-}
+{-# LANGUAGE StandaloneKindSignatures #-}
+module Arith.NonBase where
+
+import Data.Kind
+import Data.Type.Equality
+
+-- import NonBaseTH
+
+
+data Typ t where
+ TInt :: Typ Int
+ TBool :: Typ Bool
+ TPair :: Typ a -> Typ b -> Typ (a, b)
+ TFun :: Typ a -> Typ b -> Typ (a -> b)
+deriving instance Show (Typ t)
+
+instance TestEquality Typ where
+ testEquality TInt TInt = Just Refl
+ testEquality TBool TBool = Just Refl
+ testEquality (TPair a b) (TPair a' b')
+ | Just Refl <- testEquality a a'
+ , Just Refl <- testEquality b b'
+ = Just Refl
+ testEquality (TFun a b) (TFun a' b')
+ | Just Refl <- testEquality a a'
+ , Just Refl <- testEquality b b'
+ = Just Refl
+ testEquality _ _ = Nothing
+
+data PrimOp a b where
+ POAddI :: PrimOp (Int, Int) Int
+ POMulI :: PrimOp (Int, Int) Int
+ POEqI :: PrimOp (Int, Int) Bool
+deriving instance Show (PrimOp a b)
+
+type Arith :: Type -> Type
+data Arith t where
+ A_Var :: Typ t -> String -> Arith t
+ A_Let :: String -> Typ a -> Arith a -> Arith b -> Arith b
+ A_Prim :: PrimOp a b -> Arith a -> Arith b
+ A_Pair :: Arith a -> Arith b -> Arith (a, b)
+ A_If :: Arith Bool -> Arith a -> Arith a -> Arith a
+ A_Mono :: Arith Bool -> Arith Bool