{-# OPTIONS --safe --cubical #-}

module Tutorials.Project01.Main where

open import Spartan6.API.Circuit
open Expression
open Design

-- A half-adder is the smallest useful example with more than one output.
-- It adds two one-bit inputs without any stored state.  XOR is the sum bit;
-- AND is the carry bit.

inputA inputB : Expr  
inputA = input fzero
inputB = input (fsuc fzero)

sumBit carryBit : Expr  
sumBit = inputA xorE inputB
carryBit = inputA andE inputB

halfAdder : Design   
halfAdder = combinationalDesign (sumBit ∷ carryBit ∷ [])

-- These four reduction proofs are the complete truth table.  `refl` works
-- because evaluation computes to the stated result.

half-adder-00 : observe halfAdder (low ∷ low ∷ []) [] ≡ low ∷ low ∷ []
half-adder-00 = refl

half-adder-01 : observe halfAdder (low ∷ high ∷ []) [] ≡ high ∷ low ∷ []
half-adder-01 = refl

half-adder-10 : observe halfAdder (high ∷ low ∷ []) [] ≡ high ∷ low ∷ []
half-adder-10 = refl

half-adder-11 : observe halfAdder (high ∷ high ∷ []) [] ≡ low ∷ high ∷ []
half-adder-11 = refl

-- A combinational design has an empty state vector.  Neither an idle event
-- nor a rising edge can create state that the type says is absent.

half-adder-has-no-idle-state-change :
  step halfAdder idle (high ∷ high ∷ []) [] ≡ []
half-adder-has-no-idle-state-change = refl

half-adder-has-no-edge-state-change :
  step halfAdder risingEdge (high ∷ high ∷ []) [] ≡ []
half-adder-has-no-edge-state-change = refl