agda/examples/Binary.agda

{-
   FP Lunch, Nottingham
   July 27, 2007
   Conor McBride
-}

module Binary where

data Bit : Set where
  O : Bit
  I : Bit

infixl 80 _◃_

data Pos : Set where
  ◃I  : Pos
  _◃_ : Pos -> Bit -> Pos

bsuc : Pos -> Pos
bsuc ◃I      = ◃I ◃ O
bsuc (n ◃ O) = n ◃ I
bsuc (n ◃ I) = bsuc n ◃ O

data Peano : Pos -> Set where
  pI   : Peano ◃I
  psuc : {n : Pos} -> Peano n -> Peano (bsuc n)

pdouble : {n : Pos} -> Peano n -> Peano (n ◃ O)
pdouble pI       = psuc pI
pdouble (psuc p) = psuc (psuc (pdouble p))

peano : (n : Pos) -> Peano n
peano ◃I      = pI
peano (n ◃ O) = pdouble (peano n)
peano (n ◃ I) = psuc (pdouble (peano n))

-- Slow addition (yay!)
_+_ : Pos -> Pos -> Pos
_+_ n m = peano n ⊕ m
  where
    _⊕_ : {n : Pos} -> Peano n -> Pos -> Pos
    pI     ⊕ m = bsuc m
    psuc p ⊕ m = bsuc (p ⊕ m)

infixl 60 _+_
infix  40 _==_

data _==_ {A : Set}(x : A) : A -> Set where
  refl : x == x

test : (◃I ◃ I ◃ O ◃ O ◃ O) == (◃I ◃ I ◃ O ◃ I) + (◃I ◃ O ◃ I ◃ I)
test = refl