-----------------------------------------------------------------------------
-- |
-- Module    : Documentation.SBV.Examples.Puzzles.Orangutans
-- Copyright : (c) Levent Erkok
-- License   : BSD3
-- Maintainer: erkokl@gmail.com
-- Stability : experimental
--
-- Based on <http://github.com/goldfirere/video-resources/blob/main/2022-08-12-java/Haskell.hs>
-----------------------------------------------------------------------------

{-# LANGUAGE CPP                 #-}
{-# LANGUAGE DeriveAnyClass      #-}
{-# LANGUAGE DeriveDataTypeable  #-}
{-# LANGUAGE DeriveGeneric       #-}
{-# LANGUAGE FlexibleContexts    #-}
{-# LANGUAGE TemplateHaskell     #-}
{-# LANGUAGE StandaloneDeriving  #-}
{-# LANGUAGE OverloadedRecordDot #-}

{-# OPTIONS_GHC -Wall -Werror #-}

module Documentation.SBV.Examples.Puzzles.Orangutans where

import Data.SBV
import GHC.Generics (Generic)

#ifndef HADDOCK
-- $setup
-- >>> -- For doctest purposes only:
-- >>> import Data.SBV
#endif

-- | Orangutans in the puzzle.
data Orangutan = Merah   | Ofallo  | Quirrel  | Shamir   deriving (Int -> Orangutan
Orangutan -> Int
Orangutan -> [Orangutan]
Orangutan -> Orangutan
Orangutan -> Orangutan -> [Orangutan]
Orangutan -> Orangutan -> Orangutan -> [Orangutan]
(Orangutan -> Orangutan)
-> (Orangutan -> Orangutan)
-> (Int -> Orangutan)
-> (Orangutan -> Int)
-> (Orangutan -> [Orangutan])
-> (Orangutan -> Orangutan -> [Orangutan])
-> (Orangutan -> Orangutan -> [Orangutan])
-> (Orangutan -> Orangutan -> Orangutan -> [Orangutan])
-> Enum Orangutan
forall a.
(a -> a)
-> (a -> a)
-> (Int -> a)
-> (a -> Int)
-> (a -> [a])
-> (a -> a -> [a])
-> (a -> a -> [a])
-> (a -> a -> a -> [a])
-> Enum a
$csucc :: Orangutan -> Orangutan
succ :: Orangutan -> Orangutan
$cpred :: Orangutan -> Orangutan
pred :: Orangutan -> Orangutan
$ctoEnum :: Int -> Orangutan
toEnum :: Int -> Orangutan
$cfromEnum :: Orangutan -> Int
fromEnum :: Orangutan -> Int
$cenumFrom :: Orangutan -> [Orangutan]
enumFrom :: Orangutan -> [Orangutan]
$cenumFromThen :: Orangutan -> Orangutan -> [Orangutan]
enumFromThen :: Orangutan -> Orangutan -> [Orangutan]
$cenumFromTo :: Orangutan -> Orangutan -> [Orangutan]
enumFromTo :: Orangutan -> Orangutan -> [Orangutan]
$cenumFromThenTo :: Orangutan -> Orangutan -> Orangutan -> [Orangutan]
enumFromThenTo :: Orangutan -> Orangutan -> Orangutan -> [Orangutan]
Enum, Orangutan
Orangutan -> Orangutan -> Bounded Orangutan
forall a. a -> a -> Bounded a
$cminBound :: Orangutan
minBound :: Orangutan
$cmaxBound :: Orangutan
maxBound :: Orangutan
Bounded)

-- | Handlers for each orangutan.
data Handler   = Dolly   | Eva     | Francine | Gracie

-- | Location for each orangutan.
data Location  = Ambalat | Basahan | Kendisi  | Tarakan

mkSymbolicEnumeration ''Orangutan
mkSymbolicEnumeration ''Handler
mkSymbolicEnumeration ''Location

-- | An assignment is solution to the puzzle
data Assignment = MkAssignment { Assignment -> SBV Orangutan
orangutan :: SOrangutan
                               , Assignment -> SHandler
handler   :: SHandler
                               , Assignment -> SLocation
location  :: SLocation
                               , Assignment -> SInteger
age       :: SInteger
                               }
                               deriving ((forall x. Assignment -> Rep Assignment x)
-> (forall x. Rep Assignment x -> Assignment) -> Generic Assignment
forall x. Rep Assignment x -> Assignment
forall x. Assignment -> Rep Assignment x
forall a.
(forall x. a -> Rep a x) -> (forall x. Rep a x -> a) -> Generic a
$cfrom :: forall x. Assignment -> Rep Assignment x
from :: forall x. Assignment -> Rep Assignment x
$cto :: forall x. Rep Assignment x -> Assignment
to :: forall x. Rep Assignment x -> Assignment
Generic, Bool -> SBool -> Assignment -> Assignment -> Assignment
(Bool -> SBool -> Assignment -> Assignment -> Assignment)
-> (forall b.
    (Ord b, SymVal b, Num b, Num (SBV b)) =>
    [Assignment] -> Assignment -> SBV b -> Assignment)
-> Mergeable Assignment
forall b.
(Ord b, SymVal b, Num b, Num (SBV b)) =>
[Assignment] -> Assignment -> SBV b -> Assignment
forall a.
(Bool -> SBool -> a -> a -> a)
-> (forall b.
    (Ord b, SymVal b, Num b, Num (SBV b)) =>
    [a] -> a -> SBV b -> a)
-> Mergeable a
$csymbolicMerge :: Bool -> SBool -> Assignment -> Assignment -> Assignment
symbolicMerge :: Bool -> SBool -> Assignment -> Assignment -> Assignment
$cselect :: forall b.
(Ord b, SymVal b, Num b, Num (SBV b)) =>
[Assignment] -> Assignment -> SBV b -> Assignment
select :: forall b.
(Ord b, SymVal b, Num b, Num (SBV b)) =>
[Assignment] -> Assignment -> SBV b -> Assignment
Mergeable)

-- | Create a symbolic assignment, using symbolic fields.
mkSym :: Orangutan -> Symbolic Assignment
mkSym :: Orangutan -> Symbolic Assignment
mkSym Orangutan
o = do let h :: String
h = Orangutan -> String
forall a. Show a => a -> String
show Orangutan
o String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
".handler"
                 l :: String
l = Orangutan -> String
forall a. Show a => a -> String
show Orangutan
o String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
".location"
                 a :: String
a = Orangutan -> String
forall a. Show a => a -> String
show Orangutan
o String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
".age"
             s <- SBV Orangutan -> SHandler -> SLocation -> SInteger -> Assignment
MkAssignment (Orangutan -> SBV Orangutan
forall a. SymVal a => a -> SBV a
literal Orangutan
o) (SHandler -> SLocation -> SInteger -> Assignment)
-> SymbolicT IO SHandler
-> SymbolicT IO (SLocation -> SInteger -> Assignment)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> String -> SymbolicT IO SHandler
forall a. SymVal a => String -> Symbolic (SBV a)
free String
h SymbolicT IO (SLocation -> SInteger -> Assignment)
-> SymbolicT IO SLocation -> SymbolicT IO (SInteger -> Assignment)
forall a b.
SymbolicT IO (a -> b) -> SymbolicT IO a -> SymbolicT IO b
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> String -> SymbolicT IO SLocation
forall a. SymVal a => String -> Symbolic (SBV a)
free String
l SymbolicT IO (SInteger -> Assignment)
-> SymbolicT IO SInteger -> Symbolic Assignment
forall a b.
SymbolicT IO (a -> b) -> SymbolicT IO a -> SymbolicT IO b
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> String -> SymbolicT IO SInteger
forall a. SymVal a => String -> Symbolic (SBV a)
free String
a
             constrain $ s.age `sElem` [4, 7, 10, 13]
             pure s

-- | We get:
--
-- >>> allSat puzzle
-- Solution #1:
--   Merah.handler    =   Gracie :: Handler
--   Merah.location   =  Tarakan :: Location
--   Merah.age        =       10 :: Integer
--   Ofallo.handler   =      Eva :: Handler
--   Ofallo.location  =  Kendisi :: Location
--   Ofallo.age       =       13 :: Integer
--   Quirrel.handler  =    Dolly :: Handler
--   Quirrel.location =  Basahan :: Location
--   Quirrel.age      =        4 :: Integer
--   Shamir.handler   = Francine :: Handler
--   Shamir.location  =  Ambalat :: Location
--   Shamir.age       =        7 :: Integer
-- This is the only solution.
puzzle :: ConstraintSet
puzzle :: SymbolicT IO ()
puzzle = do
   solution@[_merah, ofallo, quirrel, shamir] <- (Orangutan -> Symbolic Assignment)
-> [Orangutan] -> SymbolicT IO [Assignment]
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
forall (m :: * -> *) a b. Monad m => (a -> m b) -> [a] -> m [b]
mapM Orangutan -> Symbolic Assignment
mkSym [Orangutan
forall a. Bounded a => a
minBound .. Orangutan
forall a. Bounded a => a
maxBound]

   let find Assignment -> SBool
f = (Assignment -> Assignment -> Assignment)
-> [Assignment] -> Assignment
forall a. (a -> a -> a) -> [a] -> a
forall (t :: * -> *) a. Foldable t => (a -> a -> a) -> t a -> a
foldr1 (\Assignment
a1 Assignment
a2 -> SBool -> Assignment -> Assignment -> Assignment
forall a. Mergeable a => SBool -> a -> a -> a
ite (Assignment -> SBool
f Assignment
a1) Assignment
a1 Assignment
a2) [Assignment]
solution

   -- 0. All are different in terms of handlers, locations, and ages
   constrain $ distinct (map (.handler)  solution)
   constrain $ distinct (map (.location) solution)
   constrain $ distinct (map (.age)      solution)

   -- 1. Shamir is 7 years old.
   constrain $ shamir.age .== 7

   -- 2. Shamir came from Ambalat.
   constrain $ shamir.location .== sAmbalat

   -- 3. Quirrel is younger than the ape that was found in Tarakan.
   let tarakan = (Assignment -> SBool) -> Assignment
find (\Assignment
a -> Assignment
a.location SLocation -> SLocation -> SBool
forall a. EqSymbolic a => a -> a -> SBool
.== SLocation
sTarakan)
   constrain $ quirrel.age .< tarakan.age

   -- 4. Of Ofallo and the ape that was found in Tarakan, one is cared for by Gracie and the other is 13 years old.
   let clue4 r
a1 r
a2 = r
a1.handler SHandler -> SHandler -> SBool
forall a. EqSymbolic a => a -> a -> SBool
.== SHandler
sGracie SBool -> SBool -> SBool
.&& r
a2.age a -> a -> SBool
forall a. EqSymbolic a => a -> a -> SBool
.== a
13
   constrain $ clue4 ofallo tarakan .|| clue4 tarakan ofallo
   constrain $ sOfallo ./= tarakan.orangutan

   -- 5. The animal that was found in Ambalat is either the 10-year-old or the animal Francine works with.
   let ambalat = (Assignment -> SBool) -> Assignment
find (\Assignment
a -> Assignment
a.location SLocation -> SLocation -> SBool
forall a. EqSymbolic a => a -> a -> SBool
.== SLocation
sAmbalat)
   constrain $ ambalat.age .== 10 .|| ambalat.handler .== sFrancine

   -- 6. Ofallo isn't 10 years old.
   constrain $ ofallo.age ./= 10

   -- 7. The ape that was found in Kendisi is older than the ape Dolly works with.
   let kendisi = (Assignment -> SBool) -> Assignment
find (\Assignment
a -> Assignment
a.location SLocation -> SLocation -> SBool
forall a. EqSymbolic a => a -> a -> SBool
.== SLocation
sKendisi)
   let dolly   = (Assignment -> SBool) -> Assignment
find (\Assignment
a -> Assignment
a.handler  SHandler -> SHandler -> SBool
forall a. EqSymbolic a => a -> a -> SBool
.== SHandler
sDolly)
   constrain $ kendisi.age .> dolly.age