module Encoded.Bool

import Term.Semantics
import Term.Syntax

-- Type ------------------------------------------------------------------------

export
B : Ty
B = N

-- Universal Properties --------------------------------------------------------

export
True : Term B ctx
True = Lit 0
  
export
False : Term B ctx
False = Lit 1

export
if' : Term (B ~> ty ~> ty ~> ty) ctx
if' = Abs' (\b =>
  Rec b
    (Abs $ Const $ Var Here)
    (Const $ Const $ Abs $ Var Here))

-- Utilities -------------------------------------------------------------------

export
and : Term (B ~> B ~> B) ctx
and = Abs' (\b => App if' [<b, Id, Const False])

export
or : Term (B ~> B ~> B) ctx
or = Abs' (\b => App if' [<b, Const True, Id])

export
not : Term (B ~> B) ctx
not = Abs' (\b => App if' [<b, False, True])

export
isZero : Term (N ~> B) ctx
isZero = Id

-- Semantics -------------------------------------------------------------------

-- Conversion to Idris

export
toBool : TypeOf B -> Bool
toBool = (== 0)

export
fromBool : Bool -> TypeOf B
fromBool b = if b then 0 else 1

export
toFromId : (b : Bool) -> toBool (fromBool b) = b
toFromId False = Refl
toFromId True = Refl

-- Redefinition in Idris

namespace Sem
  public export
  True : TypeOf B
  True = 0

  public export
  False : TypeOf B
  False = 1

  public export
  if' : TypeOf B -> a -> a -> a
  if' b = rec b (\t, _ => t) (\_, _, f => f)

-- Homomorphism

export
trueHomo : toBool True = True
trueHomo = Refl

export
falseHomo : toBool False = False
falseHomo = Refl

export
ifHomo : (b : Bool) -> (0 x, y : a) -> if' (fromBool b) x y = if b then x else y
ifHomo True x y = Refl
ifHomo False x y = Refl