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
-}