From ac13ffebefb22ec45e29e7f4bb6d53fa46cf6475 Mon Sep 17 00:00:00 2001 From: Tom Smeding Date: Mon, 25 May 2026 13:08:07 +0100 Subject: Up 'some' to 1.1 --- src/CHAD/AST/Types.hs | 15 +++++++++++++++ src/CHAD/AST/Weaken.hs | 3 +++ 2 files changed, 18 insertions(+) (limited to 'src/CHAD/AST') 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 -- cgit v1.3.1