trainingAgda.agda

-- 1
-- 10
-- 11
-- 100
-- 101
-- 110
-- 111
-- 1000
-- 1001
-- 1010
-- 1011
-- 1100
-- 1101
-- 1110
-- 1111
-- 10000

module trainingAgda where

data Bool : Set where
  true  : Bool
  false : Bool

data Nat : Set where
  zero : Nat
  succ : Nat -> Nat
{-# BUILTIN NATURAL Nat #-}

data Bin : Set where
  be : Bin
  b0 : Bin -> Bin
  b1 : Bin -> Bin

flip : ∀ (bin : Bin) -> Bin
flip be       = be
flip (b0 bin) = b1 (flip bin)
flip (b1 bin) = b0 (flip bin)

count-ones : ∀ (bin : Bin) -> Nat
count-ones be       = zero
count-ones (b0 bin) = (count-ones bin)
count-ones (b1 bin) = succ (count-ones bin)

inc : ∀ (bin : Bin) -> Bin
inc be       = be
inc (b0 bin) = b1 (bin)
inc (b1 bin) = b0 (inc bin)

add : ∀ (n : Nat) -> ∀ (m : Nat) -> Nat
add zero zero      = zero
add zero (succ m)  = (succ m)
add (succ n) zero  = (succ n)
add (succ n) m     = succ (add n m)

addBin : Bin -> Bin -> Bool -> Bin
addBin be be true             = b1 (be)
addBin be be false            = be
addBin be (b0 m) true         = b1 (addBin be m false)
addBin be (b0 m) false        = b0 (addBin be m false)
addBin be (b1 m) true         = b1 (addBin be m false)
addBin be (b1 m) false        = b1 (addBin be m false)
addBin (b0 n) be true         = b1 (addBin n be false)
addBin (b0 n) be false        = b0 (addBin n be false)
addBin (b0 n) (b0 m) true     = b1 (addBin n m false)
addBin (b0 n) (b0 m) false    = b0 (addBin n m false)
addBin (b0 n) (b1 m) true     = b1 (addBin n m false)
addBin (b0 n) (b1 m) false    = b1 (addBin n m false)
addBin (b1 n) be true         = b1 (addBin n be false)
addBin (b1 n) be false        = b1 (addBin n be false)
addBin (b1 n) (b0 m) true     = b1 (addBin n m false)
addBin (b1 n) (b0 m) false    = b1 (addBin n m false)
addBin (b1 n) (b1 m) true     = b1 (addBin n m true)
addBin (b1 n) (b1 m) false    = b0 (addBin n m true)


-- find : ∀ (str : Bin) -> ∀ (bin : Bin) -> Bin
-- find str bin = ?