module Bit where

open import Data.Bool as Bool using (Bool)
open import Data.Maybe using (Maybe; just; nothing)

-- I am on my three-valued-bits pijul channel.
-- I can try this out, and if I decide it's a bad idea, I can change my mind!

data Bit : Set where
  true : Bit
  false : Bit

  -- When you read from address zero, the six low wires are floating.
  -- Who knows what values you'll get?
  -- And since I don't want my proofs to make unfounded assumptions
  -- about the behavior of the Atari, I can't even choose a reasonable default.
  --
  -- My solution is to track which bits are unknown.
  -- If you try to branch on an unknown bit, I can crash the emulator.
  unknown : Bit

bit-from-bool : Bool → Bit
bit-from-bool Bool.false = false
bit-from-bool Bool.true = true

bool-from-bit : Bit → Maybe Bool
bool-from-bit true = just Bool.true
bool-from-bit false = just Bool.false
bool-from-bit unknown = nothing

--------------------------------------------------------------------------------

infixr 6 _∧_
infixr 5 _∨_ _xor_
not : Bit → Bit
not true = false
not false = true
not unknown = unknown

_∧_ : Bit → Bit → Bit
true ∧ x = x
false ∧ _ = false
unknown ∧ false = false
unknown ∧ _ = unknown

_∨_ : Bit → Bit → Bit
false ∨ x = x
true ∨ _ = true
unknown ∨ true = true
unknown ∨ _ = unknown

_xor_ : Bit → Bit → Bit
false xor false = false
false xor true = true
true xor false = true
true xor true = false
_ xor _ = unknown

majority : Bit → Bit → Bit → Bit
majority true true _ = true
majority true _ true = true
majority _ true true = true
majority false false _ = false
majority false _ false = false
majority _ false false = false
majority _ _ _ = unknown

{-
infix  0 if_then_else_

if_then_else_ : {a : Set} → Bit → Maybe a → Maybe a → Maybe a
if true then t else f = t
if false then t else f = f
if unknown then t else f = nothing
-}