Romeo & Juliet made safe

romeo.idr

data Health = JustFine | LooksDead | IsDead

record Character : Type where
  MkCharacter : (name:String) ->
                (health:Health) ->
                Character

instance Show Health where
  show IsDead = "is dead"
  show LooksDead = "looks dead"
  show JustFine = "is just fine"

instance Show Character where
  show (MkCharacter name health) = name ++ " " ++ show health

romeo : Character
romeo = MkCharacter "Romeo" JustFine

juliet : Character
juliet = MkCharacter "Juliet" JustFine

isTrueLove : Character -> Character -> Bool
isTrueLove (MkCharacter n _) (MkCharacter m _) = isTrueLove' n m
  where isTrueLove' "Romeo" "Juliet" = True
        isTrueLove' "Juliet" "Romeo" = True
        isTrueLove' _ _ = False

isDead : Character -> Bool
isDead (MkCharacter _ IsDead) = True
isDead _ = False

looksDead : Character -> Bool
looksDead (MkCharacter _ JustFine) = False
looksDead _ = True

killSelf : so (isTrueLove love char) ->
           so (isDead love) ->
           (char:Character) -> Character
killSelf _ _ c = record { health = IsDead } c

checkVitals : (c:Character) -> Maybe (so (isDead c))
checkVitals (MkCharacter _ IsDead) = Just oh
checkVitals _ = Nothing

checkAppearance : (c:Character) -> Maybe (so (looksDead c))
checkAppearance (MkCharacter _ IsDead) = Just oh
checkAppearance (MkCharacter _ LooksDead) = Just oh
checkAppearance _ = Nothing

checkTrueLove : (c1:Character) ->
                (c2:Character) ->
                Maybe (so (isTrueLove c1 c2))
checkTrueLove c1 c2 with (isTrueLove c1 c2)
  | True = Just oh
  | False = Nothing

drinkPotion : Character -> Character
drinkPotion (MkCharacter n IsDead) = MkCharacter n IsDead
drinkPotion (MkCharacter n _) = MkCharacter n LooksDead

discoverBody : Character -> Character -> String
discoverBody c1 c2 =
  case checkVitals c2 of
    Just proofOfDeath =>
      case checkTrueLove c2 c1 of
        Just loveProof => show (killSelf loveProof proofOfDeath c1)
        Nothing => "He's dead, but at least it's not my true love"

    Nothing =>
      "No one is dead, no reason to die"

-- Gives "No one is dead, no reason to die"
romeoDiscoversJuliet : String
romeoDiscoversJuliet = discoverBody romeo (drinkPotion juliet)

-- Gives "Romeo is dead"
romeoDiscoversJulietDead : String
romeoDiscoversJulietDead = discoverBody romeo (MkCharacter "Juliet" IsDead)

-- Gives "He's dead, but at least it's not my true love"
romeoDiscoversMercutio : String
romeoDiscoversMercutio = discoverBody romeo (MkCharacter "Mercutio" IsDead)

-- The following function fails to compile, because
-- checkAppearance doesn't prove to the compiler that
-- the character is dead
--
-- unsafeDiscoverBody : Character -> Character -> String
-- unsafeDiscoverBody c1 c2 =
--   case checkAppearance c2 of
--     Just proofOfDeath =>
--       case checkTrueLove c2 c1 of
--         Just loveProof => show (killSelf loveProof proofOfDeath c1)
--         Nothing => "He's dead, but at least it's not my true love"
--
--     Nothing =>
--       "No one is dead, no reason to die"