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