Skip to content

Commit

Permalink
Merge pull request #67 from bruderj15/63-default-codec
Browse files Browse the repository at this point in the history
63-default-codec: TypeError on impossible DefaultDecoded
  • Loading branch information
bruderj15 authored Aug 12, 2024
2 parents 7ed1717 + 2e03924 commit a22ee40
Showing 1 changed file with 9 additions and 3 deletions.
12 changes: 9 additions & 3 deletions src/Language/Hasmtlib/Codec.hs
Original file line number Diff line number Diff line change
Expand Up @@ -24,6 +24,7 @@ import Data.Functor.Identity (Identity)
import qualified Data.Vector.Sized as V
import Control.Monad
import GHC.Generics
import GHC.TypeLits

-- | Computes a default 'Decoded' 'Type' by distributing 'Decoded' to it's type arguments.
type family DefaultDecoded a :: Type where
Expand All @@ -35,13 +36,18 @@ type family DefaultDecoded a :: Type where
DefaultDecoded (t a b c) = t (Decoded a) (Decoded b) (Decoded c)
DefaultDecoded (t a b) = t (Decoded a) (Decoded b)
DefaultDecoded (t a) = t (Decoded a)
DefaultDecoded () = ()
DefaultDecoded x = TypeError (
Text "DefaultDecoded (" :<>: ShowType x :<>: Text ") is not allowed."
:$$: Text "Try providing the associated Type Decoded (" :<>: ShowType x :<>: Text ") manually:"
:$$: Text "instance Codec (" :<>: ShowType x :<>: Text ") where "
:$$: Text " type Decoded (" :<>: ShowType x :<>: Text ") = ... "
)

-- | Lift values to SMT-Values or decode them.
--
-- You can derive an instance of this class if your type is 'Generic'.
class Codec a where
-- | Resulting of decoding @a@
-- | Result of decoding @a@.
type Decoded a :: Type
type Decoded a = DefaultDecoded a

Expand Down Expand Up @@ -131,7 +137,7 @@ instance KnownSMTSort t => Codec (Expr t) where

encode = Constant . wrapValue

instance Codec ()
instance Codec () where type Decoded () = ()
instance (Codec a, Codec b) => Codec (a,b)
instance (Codec a, Codec b, Codec c) => Codec (a,b,c)
instance (Codec a, Codec b, Codec c, Codec d) => Codec (a,b,c,d)
Expand Down

0 comments on commit a22ee40

Please sign in to comment.