aboutsummaryrefslogtreecommitdiff
path: root/src/CHAD/AST
diff options
context:
space:
mode:
Diffstat (limited to 'src/CHAD/AST')
-rw-r--r--src/CHAD/AST/Types.hs15
-rw-r--r--src/CHAD/AST/Weaken.hs3
2 files changed, 18 insertions, 0 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