1 files changed, 41 insertions, 75 deletions
diff --git a/src/AST/Types.hs b/src/AST/Types.hs
index 217b2f5..b20fc2d 100644
--- a/src/AST/Types.hs
+++ b/src/AST/Types.hs
@@ -1,34 +1,34 @@
 {-# LANGUAGE DataKinds #-}
 {-# LANGUAGE GADTs #-}
 {-# LANGUAGE LambdaCase #-}
+{-# LANGUAGE PolyKinds #-}
 {-# LANGUAGE RankNTypes #-}
 {-# LANGUAGE StandaloneDeriving #-}
 {-# LANGUAGE StandaloneKindSignatures #-}
 {-# LANGUAGE TypeFamilies #-}
 {-# LANGUAGE TypeOperators #-}
+{-# LANGUAGE TypeData #-}
 module AST.Types where
 
 import Data.Int (Int32, Int64)
+import Data.GADT.Compare
 import Data.GADT.Show
 import Data.Kind (Type)
-import Data.Some
 import Data.Type.Equality
 
 import Data
 
 
-data Ty
+type data Ty
   = TNil
   | TPair Ty Ty
   | TEither Ty Ty
   | TMaybe Ty
   | TArr Nat Ty  -- ^ rank, element type
   | TScal ScalTy
-  | TAccum Ty  -- ^ the accumulator contains D2 of this type
-  deriving (Show, Eq, Ord)
+  | TAccum Ty  -- ^ contained type must be a monoid type
 
-data ScalTy = TI32 | TI64 | TF32 | TF64 | TBool
-  deriving (Show, Eq, Ord)
+type data ScalTy = TI32 | TI64 | TF32 | TF64 | TBool
 
 type STy :: Ty -> Type
 data STy t where
@@ -41,22 +41,25 @@ data STy t where
   STAccum :: STy t -> STy (TAccum t)
 deriving instance Show (STy t)
 
-instance TestEquality STy where
-  testEquality STNil STNil = Just Refl
-  testEquality STNil _ = Nothing
-  testEquality (STPair a b) (STPair a' b') | Just Refl <- testEquality a a', Just Refl <- testEquality b b' = Just Refl
-  testEquality STPair{} _ = Nothing
-  testEquality (STEither a b) (STEither a' b') | Just Refl <- testEquality a a', Just Refl <- testEquality b b' = Just Refl
-  testEquality STEither{} _ = Nothing
-  testEquality (STMaybe a) (STMaybe a') | Just Refl <- testEquality a a' = Just Refl
-  testEquality STMaybe{} _ = Nothing
-  testEquality (STArr a b) (STArr a' b') | Just Refl <- testEquality a a', Just Refl <- testEquality b b' = Just Refl
-  testEquality STArr{} _ = Nothing
-  testEquality (STScal a) (STScal a') | Just Refl <- testEquality a a' = Just Refl
-  testEquality STScal{} _ = Nothing
-  testEquality (STAccum a) (STAccum a') | Just Refl <- testEquality a a' = Just Refl
-  testEquality STAccum{} _ = Nothing
-
+instance GCompare STy where
+  gcompare = \cases
+    STNil STNil -> GEQ
+    STNil _ -> GLT ; _ STNil -> GGT
+    (STPair a b) (STPair a' b') -> gorderingLift2 (gcompare a a') (gcompare b b')
+    STPair{} _ -> GLT ; _ STPair{} -> GGT
+    (STEither a b) (STEither a' b') -> gorderingLift2 (gcompare a a') (gcompare b b')
+    STEither{} _ -> GLT ; _ STEither{} -> GGT
+    (STMaybe a) (STMaybe a') -> gorderingLift1 (gcompare a a')
+    STMaybe{} _ -> GLT ; _ STMaybe{} -> GGT
+    (STArr n t) (STArr n' t') -> gorderingLift2 (gcompare n n') (gcompare t t')
+    STArr{} _ -> GLT ; _ STArr{} -> GGT
+    (STScal t) (STScal t') -> gorderingLift1 (gcompare t t')
+    STScal{} _ -> GLT ; _ STScal{} -> GGT
+    (STAccum t) (STAccum t') -> gorderingLift1 (gcompare t t')
+    -- STAccum{} _ -> GLT ; _ STAccum{} -> GGT
+
+instance TestEquality STy where testEquality = geq
+instance GEq STy where geq = defaultGeq
 instance GShow STy where gshowsPrec = defaultGshowsPrec
 
 data SScalTy t where
@@ -67,14 +70,21 @@ data SScalTy t where
   STBool :: SScalTy TBool
 deriving instance Show (SScalTy t)
 
-instance TestEquality SScalTy where
-  testEquality STI32 STI32 = Just Refl
-  testEquality STI64 STI64 = Just Refl
-  testEquality STF32 STF32 = Just Refl
-  testEquality STF64 STF64 = Just Refl
-  testEquality STBool STBool = Just Refl
-  testEquality _ _ = Nothing
-
+instance GCompare SScalTy where
+  gcompare = \cases
+    STI32 STI32 -> GEQ
+    STI32 _ -> GLT ; _ STI32 -> GGT
+    STI64 STI64 -> GEQ
+    STI64 _ -> GLT ; _ STI64 -> GGT
+    STF32 STF32 -> GEQ
+    STF32 _ -> GLT ; _ STF32 -> GGT
+    STF64 STF64 -> GEQ
+    STF64 _ -> GLT ; _ STF64 -> GGT
+    STBool STBool -> GEQ
+    -- STBool _ -> GLT ; _ STBool -> GGT
+
+instance TestEquality SScalTy where testEquality = geq
+instance GEq SScalTy where geq = defaultGeq
 instance GShow SScalTy where gshowsPrec = defaultGshowsPrec
 
 scalRepIsShow :: SScalTy t -> Dict (Show (ScalRep t))
@@ -89,50 +99,6 @@ type TIx = TScal TI64
 tIx :: STy TIx
 tIx = STScal STI64
 
-unSTy :: STy t -> Ty
-unSTy = \case
-  STNil -> TNil
-  STPair a b -> TPair (unSTy a) (unSTy b)
-  STEither a b -> TEither (unSTy a) (unSTy b)
-  STMaybe t -> TMaybe (unSTy t)
-  STArr n t -> TArr (unSNat n) (unSTy t)
-  STScal t -> TScal (unSScalTy t)
-  STAccum t -> TAccum (unSTy t)
-
-unSEnv :: SList STy env -> [Ty]
-unSEnv SNil = []
-unSEnv (SCons t l) = unSTy t : unSEnv l
-
-unSScalTy :: SScalTy t -> ScalTy
-unSScalTy = \case
-  STI32 -> TI32
-  STI64 -> TI64
-  STF32 -> TF32
-  STF64 -> TF64
-  STBool -> TBool
-
-reSTy :: Ty -> Some STy
-reSTy = \case
-  TNil -> Some STNil
-  TPair a b | Some a' <- reSTy a, Some b' <- reSTy b -> Some $ STPair a' b'
-  TEither a b | Some a' <- reSTy a, Some b' <- reSTy b -> Some $ STEither a' b'
-  TMaybe t | Some t' <- reSTy t -> Some $ STMaybe t'
-  TArr n t | Some n' <- reSNat n, Some t' <- reSTy t -> Some $ STArr n' t'
-  TScal t | Some t' <- reSScalTy t -> Some $ STScal t'
-  TAccum t | Some t' <- reSTy t -> Some $ STAccum t'
-
-reSEnv :: [Ty] -> Some (SList STy)
-reSEnv [] = Some SNil
-reSEnv (t : l) | Some t' <- reSTy t, Some env <- reSEnv l = Some (SCons t' env)
-
-reSScalTy :: ScalTy -> Some SScalTy
-reSScalTy = \case
-  TI32 -> Some STI32
-  TI64 -> Some STI64
-  TF32 -> Some STF32
-  TF64 -> Some STF64
-  TBool -> Some STBool
-
 type family ScalRep t where
   ScalRep TI32 = Int32
   ScalRep TI64 = Int64
@@ -161,7 +127,7 @@ type family ScalIsIntegral t where
   ScalIsIntegral TF64 = False
   ScalIsIntegral TBool = False
 
--- | Returns true for arrays /and/ accumulators;
+-- | Returns true for arrays /and/ accumulators.
 hasArrays :: STy t' -> Bool
 hasArrays STNil = False
 hasArrays (STPair a b) = hasArrays a || hasArrays b