curryhoward.idr

module F1

import System
import Data.Bool
import Data.List
import Data.Vect
import Decidable.Equality

data Fruit = Apple | Banana

implementation Show Fruit where
  show Apple = "Apple"
  show Banana = "Banana"

appleString : String
appleString = "apple"

bananaString : String
bananaString = "banana"

knownFruit : String -> Bool
knownFruit s = s == appleString || s == bananaString

data FruitObserver : String -> Bool -> Type where
  FO : (s : String) -> FruitObserver s (knownFruit s)

stringOfFruitObserver : {s : String} -> FruitObserver s k -> String
stringOfFruitObserver (FO s) = s

makeDefaultFruitObserver : {s : String} -> FruitObserver s (knownFruit s)
makeDefaultFruitObserver = FO s

appleT : Type
appleT = FruitObserver appleString True

bananaT : Type
bananaT = FruitObserver bananaString True

apple : F1.appleT
apple = makeDefaultFruitObserver

banana : F1.bananaT
banana = makeDefaultFruitObserver

interface WhichFruit t where
  whichFruit : t -> Maybe Fruit

implementation WhichFruit (FruitObserver F1.appleString True) where
  whichFruit _ = Just Apple

implementation WhichFruit (FruitObserver F1.bananaString True) where
  whichFruit _ = Just Banana

implementation WhichFruit (FruitObserver f False) where
  whichFruit _ = Nothing

bi : {b : Bool} -> (not b = True) -> (b = False)
bi {b = True} p impossible
bi {b = False} p = Refl

anyOrTrueIsTrue : (a : Bool) -> (a || True) = True
anyOrTrueIsTrue False = Refl
anyOrTrueIsTrue True = Refl

contradiction : (a : Bool) -> a = False -> a = True -> Void
contradiction False p1 p2 impossible
contradiction True p1 p2 impossible

toFruit : String -> Maybe Fruit
toFruit f with (decEq (f == F1.appleString) True)
  toFruit f | (Yes prf) = whichFruit F1.apple
  toFruit f | (No contra) with (decEq (f == F1.bananaString) True)
    toFruit f | (No contra) | Yes prf = whichFruit F1.banana
    toFruit f | (No contra1) | (No contra2) with (decEq (knownFruit f) True)
      toFruit f | (No contra1) | (No contra2) | Yes prf =
        let
          notApple : (f == F1.appleString = False)
          notApple = bi (invertContraBool (f == F1.appleString) True contra1)

          notBanana : (f == F1.bananaString = False)
          notBanana = bi (invertContraBool (f == F1.bananaString) True contra2)

          notIdentified : (knownFruit f = False)
          notIdentified =
            rewrite notApple in
            rewrite notBanana in
            Refl
        in
        absurd (contradiction (knownFruit f) notIdentified prf)

      toFruit f | (No contra1) | (No contra2) | (No contra3) =
        let
          f1 : FruitObserver f False
          f1 =
            let
              notIdentified : ((knownFruit f) = False)
              notIdentified = bi (invertContraBool (f == F1.appleString || f == F1.bananaString) True contra3)
            in
            rewrite sym notIdentified in
            FO f
        in
        whichFruit f1

main : IO ()
main = do
  args <- getArgs
  case args of
    [_,f] => putStrLn $ show $ toFruit f
    _ => putStrLn "give a fruit"