Up 'some' to 1.1HEADmaster

3 files changed, 35 insertions, 1 deletions

diff --git a/src/CHAD/AST/Types.hs b/src/CHAD/AST/Types.hs
index f0feb55..006d023 100644
--- a/src/CHAD/AST/Types.hs
+++ b/src/CHAD/AST/Types.hs
@@ -68,6 +68,11 @@ instance TestEquality STy where testEquality = geq
 instance GEq STy where geq = defaultGeq
 instance GShow STy where gshowsPrec = defaultGshowsPrec
 
+instance Eq (STy t) where (==) = eqpFromGEq
+instance Ord (STy t) where compare = comparepFromGCompare
+instance EqP STy where eqp = eqpFromGEq
+instance OrdP STy where comparep = comparepFromGCompare
+
 -- | Monoid types
 type SMTy :: Ty -> Type
 data SMTy t where
@@ -98,6 +103,11 @@ instance TestEquality SMTy where testEquality = geq
 instance GEq SMTy where geq = defaultGeq
 instance GShow SMTy where gshowsPrec = defaultGshowsPrec
 
+instance Eq (SMTy t) where (==) = eqpFromGEq
+instance Ord (SMTy t) where compare = comparepFromGCompare
+instance EqP SMTy where eqp = eqpFromGEq
+instance OrdP SMTy where comparep = comparepFromGCompare
+
 fromSMTy :: SMTy t -> STy t
 fromSMTy = \case
   SMTNil -> STNil
@@ -132,6 +142,11 @@ instance TestEquality SScalTy where testEquality = geq
 instance GEq SScalTy where geq = defaultGeq
 instance GShow SScalTy where gshowsPrec = defaultGshowsPrec
 
+instance Eq (SScalTy t) where (==) = eqpFromGEq
+instance Ord (SScalTy t) where compare = comparepFromGCompare
+instance EqP SScalTy where eqp = eqpFromGEq
+instance OrdP SScalTy where comparep = comparepFromGCompare
+
 scalRepIsShow :: SScalTy t -> Dict (Show (ScalRep t))
 scalRepIsShow STI32 = Dict
 scalRepIsShow STI64 = Dict
diff --git a/src/CHAD/AST/Weaken.hs b/src/CHAD/AST/Weaken.hs
index ac0d152..f5345d1 100644
--- a/src/CHAD/AST/Weaken.hs
+++ b/src/CHAD/AST/Weaken.hs
@@ -37,6 +37,9 @@ instance GEq (Idx env) where
   geq (IS i) (IS j) | Just Refl <- geq i j = Just Refl
   geq _ _ = Nothing
 
+instance Eq (Idx env t) where _ == _ = True
+instance EqP (Idx env) where eqp = eqpFromGEq
+
 splitIdx :: forall env2 env1 t f. SList f env1 -> Idx (Append env1 env2) t -> Either (Idx env1 t) (Idx env2 t)
 splitIdx SNil i = Right i
 splitIdx (SCons _ _) IZ = Left IZ
diff --git a/src/CHAD/Data.hs b/src/CHAD/Data.hs
index 8c7605c..68b2554 100644
--- a/src/CHAD/Data.hs
+++ b/src/CHAD/Data.hs
@@ -8,11 +8,13 @@
 {-# LANGUAGE StandaloneDeriving #-}
 {-# LANGUAGE TypeFamilies #-}
 {-# LANGUAGE TypeOperators #-}
-module CHAD.Data (module CHAD.Data, (:~:)(Refl), If) where
+module CHAD.Data (module CHAD.Data, (:~:)(Refl), If, EqP(eqp), OrdP(comparep)) where
 
+import Data.EqP
 import Data.Functor.Product
 import Data.GADT.Compare
 import Data.GADT.Show
+import Data.OrdP
 import Data.Some
 import Data.Type.Bool (If)
 import Data.Type.Equality
@@ -86,6 +88,11 @@ instance TestEquality SNat where testEquality = geq
 instance GEq SNat where geq = defaultGeq
 instance GShow SNat where gshowsPrec = defaultGshowsPrec
 
+instance Eq (SNat n) where _ == _ = True
+instance Ord (SNat n) where compare _ _ = EQ
+instance EqP SNat where eqp = eqpFromGEq
+instance OrdP SNat where comparep = comparepFromGCompare
+
 fromSNat :: SNat n -> Int
 fromSNat SZ = 0
 fromSNat (SS n) = succ (fromSNat n)
@@ -190,3 +197,12 @@ data SBool b where
   SF :: SBool False
   ST :: SBool True
 deriving instance Show (SBool b)
+
+eqpFromGEq :: GEq f => f a -> f b -> Bool
+eqpFromGEq x y = case geq x y of
+                   Just Refl -> True
+                   Nothing -> False
+
+comparepFromGCompare :: GCompare f => f a -> f b -> Ordering
+comparepFromGCompare x y = case gcompare x y of
+                             GEQ -> EQ ; GLT -> LT ; GGT -> GT