some agda

bool.agda

{-# OPTIONS --universe-polymorphism #-}

module mybool where

-- http://www.cse.chalmers.se/~ulfn/code/tphols09/ ⟵ ../tphols09/
--------------------------------------------------------------------------------
-- data types
--------------------------------------------------------------------------------

data 𝔹 : Set where
  tt : 𝔹
  ff : 𝔹
{-# BUILTIN BOOL  𝔹  #-}
{-# BUILTIN TRUE  tt #-}
{-# BUILTIN FALSE ff #-}
{-# COMPILE GHC 𝔹 = data Bool (True | False) #-}

--------------------------------------------------------------------------------
-- syntax
--------------------------------------------------------------------------------

infix 7  ~_     ¬_
infix 6 _nand_ _⊼_
infix 6 _&&_   _∧_
infix 6 _nor_  _⊽_
infix 6 _xor_  _⊕_
infix 5 _||_   _∨_
infix 4 if_then_else_
infix 4 if*_then_else_
infix 4 _⇒_

--------------------------------------------------------------------------------
-- operations
--------------------------------------------------------------------------------

-- not
¬_ : 𝔹 → 𝔹
¬ tt = ff
¬ ff = tt
~_ = ¬_

-- nand
_⊼_ : 𝔹 → 𝔹 → 𝔹
tt ⊼ tt = ff
tt ⊼ ff = tt
ff ⊼ tt = tt
ff ⊼ ff = tt
_nand_ = _⊼_

-- and
_∧_ : 𝔹 → 𝔹 → 𝔹
tt ∧ b = b
ff ∧ b = ff
_&&_ = _∧_

-- xor
_⊕_ : 𝔹 → 𝔹 → 𝔹
tt ⊕ tt = ff
tt ⊕ ff = tt
ff ⊕ tt = tt
ff ⊕ ff = ff
_xor_ = _⊕_

-- or
_∨_ : 𝔹 → 𝔹 → 𝔹
tt ∨ b = tt
ff ∨ b = b
_||_ = _∨_

-- nor
_⊽_ : 𝔹 → 𝔹 → 𝔹
x ⊽ y = ¬ (x ∨ y)
_nor_ = _⊽_

-- if_then_else_
if_then_else_ : ∀ {ℓ} {A : Set ℓ} → 𝔹 → A → A → A
if tt then y else z = y
if ff then y else z = z

-- if*_then_else_
if*_then_else_ : ∀ {ℓ} {A B : Set ℓ} → (b : 𝔹) → A → B → if b then A else B
if* tt then a else b = a
if* ff then a else b = b

-- implies
_⇒_ : 𝔹 → 𝔹 → 𝔹
tt ⇒ b = b -- b2?
ff ⇒ b = tt
_imp_ = _⇒_

-- type inference: SPC m d
-- normalize expression: SPC m n