Closed shnarazk closed 7 years ago
{-# LANGUAGE TypeFamilies, DataKinds, GADTs, StandaloneDeriving, FlexibleInstances #-}
module Clause where
-- import Unsafe.Coerce
data ClauseKind = OfNormal | NullCaluse | BinaryClause
data Clause (a :: ClauseKind) where
MkClause :: [Int] -> Clause 'OfNormal
MkBinaryClause :: Int -> Clause 'BinaryClause
instance Eq (Clause a) where
(MkBinaryClause a) == (MkBinaryClause b) = a == b
_ == _ = undefined
instance Show (Clause a) where
show (MkBinaryClause l) = "B{" ++ show l ++ "}"
show (MkClause _) = show "Clause"
-- data Clause (a :: ClauseKind) = Clause [Int] deriving (Eq, Show)
c :: [Clause 'OfNormal]
c = []
This is completely same with #28
Some thought on types and kinds to use recent ghc features.