Copyright	(c) Levent Erkok
License	BSD3
Maintainer	erkokl@gmail.com
Stability	experimental
Safe Haskell	None
Language	Haskell2010

Documentation.SBV.Examples.Puzzles.KnightsAndKnaves

Description

From Raymond Smullyan: On a fictional island, all inhabitants are either knights, who always tell the truth, or knaves, who always lie. John and Bill are residents of the island of knights and knaves. John and Bill make several utterances. Determine which one is a knave or a knight, depending on their answers.

Synopsis

data Inhabitant
type SInhabitant = SBV Inhabitant
data Identity
- = Knave
- | Knight
type SIdentity = SBV Identity
sKnave :: SBV Identity
sKnight :: SBV Identity
data Statement
- = Truth
- | Falsity
type SStatement = SBV Statement
sTruth :: SBV Statement
sFalsity :: SBV Statement
john :: SInhabitant
bill :: SInhabitant
is :: SInhabitant -> SIdentity -> SStatement
says :: SInhabitant -> SStatement -> SBool
holds :: SStatement -> SBool
and :: SStatement -> SStatement -> SStatement
not :: SStatement -> SStatement
iff :: SStatement -> SStatement -> SStatement
puzzle :: IO ()

Documentation

data Inhabitant Source #

Inhabitants of the island, as an uninterpreted sort

Instances

Instances details

Data Inhabitant Source #
Instance details Defined in Documentation.SBV.Examples.Puzzles.KnightsAndKnaves Methods gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b) -> (forall g. g -> c g) -> Inhabitant -> c Inhabitant # gunfold :: (forall b r. Data b => c (b -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c Inhabitant # toConstr :: Inhabitant -> Constr # dataTypeOf :: Inhabitant -> DataType # dataCast1 :: Typeable t => (forall d. Data d => c (t d)) -> Maybe (c Inhabitant) # dataCast2 :: Typeable t => (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c Inhabitant) # gmapT :: (forall b. Data b => b -> b) -> Inhabitant -> Inhabitant # gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> Inhabitant -> r # gmapQr :: forall r r'. (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> Inhabitant -> r # gmapQ :: (forall d. Data d => d -> u) -> Inhabitant -> [u] # gmapQi :: Int -> (forall d. Data d => d -> u) -> Inhabitant -> u # gmapM :: Monad m => (forall d. Data d => d -> m d) -> Inhabitant -> m Inhabitant # gmapMp :: MonadPlus m => (forall d. Data d => d -> m d) -> Inhabitant -> m Inhabitant # gmapMo :: MonadPlus m => (forall d. Data d => d -> m d) -> Inhabitant -> m Inhabitant #
Read Inhabitant Source #
Instance details Defined in Documentation.SBV.Examples.Puzzles.KnightsAndKnaves Methods readsPrec :: Int -> ReadS Inhabitant # readList :: ReadS [Inhabitant] # readPrec :: ReadPrec Inhabitant # readListPrec :: ReadPrec [Inhabitant] #
Show Inhabitant Source #
Instance details Defined in Documentation.SBV.Examples.Puzzles.KnightsAndKnaves Methods showsPrec :: Int -> Inhabitant -> ShowS # show :: Inhabitant -> String # showList :: [Inhabitant] -> ShowS #
SymVal Inhabitant Source #
Instance details Defined in Documentation.SBV.Examples.Puzzles.KnightsAndKnaves Methods mkSymVal :: MonadSymbolic m => VarContext -> Maybe String -> m (SBV Inhabitant) Source # literal :: Inhabitant -> SBV Inhabitant Source # fromCV :: CV -> Inhabitant Source # isConcretely :: SBV Inhabitant -> (Inhabitant -> Bool) -> Bool Source # free :: MonadSymbolic m => String -> m (SBV Inhabitant) Source # free_ :: MonadSymbolic m => m (SBV Inhabitant) Source # mkFreeVars :: MonadSymbolic m => Int -> m [SBV Inhabitant] Source # symbolic :: MonadSymbolic m => String -> m (SBV Inhabitant) Source # symbolics :: MonadSymbolic m => [String] -> m [SBV Inhabitant] Source # unliteral :: SBV Inhabitant -> Maybe Inhabitant Source # isConcrete :: SBV Inhabitant -> Bool Source # isSymbolic :: SBV Inhabitant -> Bool Source #
HasKind Inhabitant Source #
Instance details Defined in Documentation.SBV.Examples.Puzzles.KnightsAndKnaves Methods kindOf :: Inhabitant -> Kind Source # hasSign :: Inhabitant -> Bool Source # intSizeOf :: Inhabitant -> Int Source # isBoolean :: Inhabitant -> Bool Source # isBounded :: Inhabitant -> Bool Source # isReal :: Inhabitant -> Bool Source # isFloat :: Inhabitant -> Bool Source # isDouble :: Inhabitant -> Bool Source # isRational :: Inhabitant -> Bool Source # isFP :: Inhabitant -> Bool Source # isUnbounded :: Inhabitant -> Bool Source # isUserSort :: Inhabitant -> Bool Source # isChar :: Inhabitant -> Bool Source # isString :: Inhabitant -> Bool Source # isList :: Inhabitant -> Bool Source # isSet :: Inhabitant -> Bool Source # isTuple :: Inhabitant -> Bool Source # isMaybe :: Inhabitant -> Bool Source # isEither :: Inhabitant -> Bool Source # showType :: Inhabitant -> String Source #
SatModel Inhabitant Source #
Instance details Defined in Documentation.SBV.Examples.Puzzles.KnightsAndKnaves Methods parseCVs :: [CV] -> Maybe (Inhabitant, [CV]) Source # cvtModel :: (Inhabitant -> Maybe b) -> Maybe (Inhabitant, [CV]) -> Maybe (b, [CV]) Source #

type SInhabitant = SBV Inhabitant Source #

Symbolic version of the type Inhabitant.

data Identity Source #

Each inhabitant is either a knave or a knight

Constructors

Knave
Knight

Instances

Instances details

Data Identity Source #
Instance details Defined in Documentation.SBV.Examples.Puzzles.KnightsAndKnaves Methods gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b) -> (forall g. g -> c g) -> Identity -> c Identity # gunfold :: (forall b r. Data b => c (b -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c Identity # toConstr :: Identity -> Constr # dataTypeOf :: Identity -> DataType # dataCast1 :: Typeable t => (forall d. Data d => c (t d)) -> Maybe (c Identity) # dataCast2 :: Typeable t => (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c Identity) # gmapT :: (forall b. Data b => b -> b) -> Identity -> Identity # gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> Identity -> r # gmapQr :: forall r r'. (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> Identity -> r # gmapQ :: (forall d. Data d => d -> u) -> Identity -> [u] # gmapQi :: Int -> (forall d. Data d => d -> u) -> Identity -> u # gmapM :: Monad m => (forall d. Data d => d -> m d) -> Identity -> m Identity # gmapMp :: MonadPlus m => (forall d. Data d => d -> m d) -> Identity -> m Identity # gmapMo :: MonadPlus m => (forall d. Data d => d -> m d) -> Identity -> m Identity #
Read Identity Source #
Instance details Defined in Documentation.SBV.Examples.Puzzles.KnightsAndKnaves Methods readsPrec :: Int -> ReadS Identity # readList :: ReadS [Identity] # readPrec :: ReadPrec Identity # readListPrec :: ReadPrec [Identity] #
Show Identity Source #
Instance details Defined in Documentation.SBV.Examples.Puzzles.KnightsAndKnaves Methods showsPrec :: Int -> Identity -> ShowS # show :: Identity -> String # showList :: [Identity] -> ShowS #
Eq Identity Source #
Instance details Defined in Documentation.SBV.Examples.Puzzles.KnightsAndKnaves Methods (==) :: Identity -> Identity -> Bool # (/=) :: Identity -> Identity -> Bool #
Ord Identity Source #
Instance details Defined in Documentation.SBV.Examples.Puzzles.KnightsAndKnaves Methods compare :: Identity -> Identity -> Ordering # (<) :: Identity -> Identity -> Bool # (<=) :: Identity -> Identity -> Bool # (>) :: Identity -> Identity -> Bool # (>=) :: Identity -> Identity -> Bool # max :: Identity -> Identity -> Identity # min :: Identity -> Identity -> Identity #
SymVal Identity Source #
Instance details Defined in Documentation.SBV.Examples.Puzzles.KnightsAndKnaves Methods mkSymVal :: MonadSymbolic m => VarContext -> Maybe String -> m (SBV Identity) Source # literal :: Identity -> SBV Identity Source # fromCV :: CV -> Identity Source # isConcretely :: SBV Identity -> (Identity -> Bool) -> Bool Source # free :: MonadSymbolic m => String -> m (SBV Identity) Source # free_ :: MonadSymbolic m => m (SBV Identity) Source # mkFreeVars :: MonadSymbolic m => Int -> m [SBV Identity] Source # symbolic :: MonadSymbolic m => String -> m (SBV Identity) Source # symbolics :: MonadSymbolic m => [String] -> m [SBV Identity] Source # unliteral :: SBV Identity -> Maybe Identity Source # isConcrete :: SBV Identity -> Bool Source # isSymbolic :: SBV Identity -> Bool Source #
HasKind Identity Source #
Instance details Defined in Documentation.SBV.Examples.Puzzles.KnightsAndKnaves Methods kindOf :: Identity -> Kind Source # hasSign :: Identity -> Bool Source # intSizeOf :: Identity -> Int Source # isBoolean :: Identity -> Bool Source # isBounded :: Identity -> Bool Source # isReal :: Identity -> Bool Source # isFloat :: Identity -> Bool Source # isDouble :: Identity -> Bool Source # isRational :: Identity -> Bool Source # isFP :: Identity -> Bool Source # isUnbounded :: Identity -> Bool Source # isUserSort :: Identity -> Bool Source # isChar :: Identity -> Bool Source # isString :: Identity -> Bool Source # isList :: Identity -> Bool Source # isSet :: Identity -> Bool Source # isTuple :: Identity -> Bool Source # isMaybe :: Identity -> Bool Source # isEither :: Identity -> Bool Source # showType :: Identity -> String Source #
SatModel Identity Source #
Instance details Defined in Documentation.SBV.Examples.Puzzles.KnightsAndKnaves Methods parseCVs :: [CV] -> Maybe (Identity, [CV]) Source # cvtModel :: (Identity -> Maybe b) -> Maybe (Identity, [CV]) -> Maybe (b, [CV]) Source #

type SIdentity = SBV Identity Source #

Symbolic version of the type Identity.

sKnave :: SBV Identity Source #

Symbolic version of the constructor Knave.

sKnight :: SBV Identity Source #

Symbolic version of the constructor Knight.

data Statement Source #

Statements are utterances which are either true or false

Constructors

Truth
Falsity

Instances

Instances details

Data Statement Source #
Instance details Defined in Documentation.SBV.Examples.Puzzles.KnightsAndKnaves Methods gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b) -> (forall g. g -> c g) -> Statement -> c Statement # gunfold :: (forall b r. Data b => c (b -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c Statement # toConstr :: Statement -> Constr # dataTypeOf :: Statement -> DataType # dataCast1 :: Typeable t => (forall d. Data d => c (t d)) -> Maybe (c Statement) # dataCast2 :: Typeable t => (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c Statement) # gmapT :: (forall b. Data b => b -> b) -> Statement -> Statement # gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> Statement -> r # gmapQr :: forall r r'. (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> Statement -> r # gmapQ :: (forall d. Data d => d -> u) -> Statement -> [u] # gmapQi :: Int -> (forall d. Data d => d -> u) -> Statement -> u # gmapM :: Monad m => (forall d. Data d => d -> m d) -> Statement -> m Statement # gmapMp :: MonadPlus m => (forall d. Data d => d -> m d) -> Statement -> m Statement # gmapMo :: MonadPlus m => (forall d. Data d => d -> m d) -> Statement -> m Statement #
Read Statement Source #
Instance details Defined in Documentation.SBV.Examples.Puzzles.KnightsAndKnaves Methods readsPrec :: Int -> ReadS Statement # readList :: ReadS [Statement] # readPrec :: ReadPrec Statement # readListPrec :: ReadPrec [Statement] #
Show Statement Source #
Instance details Defined in Documentation.SBV.Examples.Puzzles.KnightsAndKnaves Methods showsPrec :: Int -> Statement -> ShowS # show :: Statement -> String # showList :: [Statement] -> ShowS #
Eq Statement Source #
Instance details Defined in Documentation.SBV.Examples.Puzzles.KnightsAndKnaves Methods (==) :: Statement -> Statement -> Bool # (/=) :: Statement -> Statement -> Bool #
Ord Statement Source #
Instance details Defined in Documentation.SBV.Examples.Puzzles.KnightsAndKnaves Methods compare :: Statement -> Statement -> Ordering # (<) :: Statement -> Statement -> Bool # (<=) :: Statement -> Statement -> Bool # (>) :: Statement -> Statement -> Bool # (>=) :: Statement -> Statement -> Bool # max :: Statement -> Statement -> Statement # min :: Statement -> Statement -> Statement #
SymVal Statement Source #
Instance details Defined in Documentation.SBV.Examples.Puzzles.KnightsAndKnaves Methods mkSymVal :: MonadSymbolic m => VarContext -> Maybe String -> m (SBV Statement) Source # literal :: Statement -> SBV Statement Source # fromCV :: CV -> Statement Source # isConcretely :: SBV Statement -> (Statement -> Bool) -> Bool Source # free :: MonadSymbolic m => String -> m (SBV Statement) Source # free_ :: MonadSymbolic m => m (SBV Statement) Source # mkFreeVars :: MonadSymbolic m => Int -> m [SBV Statement] Source # symbolic :: MonadSymbolic m => String -> m (SBV Statement) Source # symbolics :: MonadSymbolic m => [String] -> m [SBV Statement] Source # unliteral :: SBV Statement -> Maybe Statement Source # isConcrete :: SBV Statement -> Bool Source # isSymbolic :: SBV Statement -> Bool Source #
HasKind Statement Source #
Instance details Defined in Documentation.SBV.Examples.Puzzles.KnightsAndKnaves Methods kindOf :: Statement -> Kind Source # hasSign :: Statement -> Bool Source # intSizeOf :: Statement -> Int Source # isBoolean :: Statement -> Bool Source # isBounded :: Statement -> Bool Source # isReal :: Statement -> Bool Source # isFloat :: Statement -> Bool Source # isDouble :: Statement -> Bool Source # isRational :: Statement -> Bool Source # isFP :: Statement -> Bool Source # isUnbounded :: Statement -> Bool Source # isUserSort :: Statement -> Bool Source # isChar :: Statement -> Bool Source # isString :: Statement -> Bool Source # isList :: Statement -> Bool Source # isSet :: Statement -> Bool Source # isTuple :: Statement -> Bool Source # isMaybe :: Statement -> Bool Source # isEither :: Statement -> Bool Source # showType :: Statement -> String Source #
SatModel Statement Source #
Instance details Defined in Documentation.SBV.Examples.Puzzles.KnightsAndKnaves Methods parseCVs :: [CV] -> Maybe (Statement, [CV]) Source # cvtModel :: (Statement -> Maybe b) -> Maybe (Statement, [CV]) -> Maybe (b, [CV]) Source #

type SStatement = SBV Statement Source #

Symbolic version of the type Statement.

sTruth :: SBV Statement Source #

Symbolic version of the constructor Truth.

sFalsity :: SBV Statement Source #

Symbolic version of the constructor Falsity.

john :: SInhabitant Source #

John is an inhabitant of the island.

bill :: SInhabitant Source #

Bill is an inhabitant of the island.

is :: SInhabitant -> SIdentity -> SStatement Source #

The connective is makes a statement about an inhabitant regarding his/her identity.

says :: SInhabitant -> SStatement -> SBool Source #

The connective says makes a predicate from what an inhabitant states

holds :: SStatement -> SBool Source #

The connective holds is will be true if the statement is true

and :: SStatement -> SStatement -> SStatement Source #

The connective and creates the conjunction of two statements

not :: SStatement -> SStatement Source #

The connective not negates a statement

iff :: SStatement -> SStatement -> SStatement Source #

The connective iff creates a statement that equates the truth values of its argument statements

puzzle :: IO () Source #

Encode Smullyan's puzzle. We have:

>>> puzzle
Question 1.
  John says, We are both knaves
    Then, John is: Knave
    And,  Bill is: Knight
Question 2.
  John says If (and only if) Bill is a knave, then I am a knave.
  Bill says We are of different kinds.
    Then, John is: Knave
    And,  Bill is: Knight