-- http://en.wikipedia.org/wiki/NAND_logic
open import Type
open import FunUniverse.Core
open import Level.NP
--open import FunUniverse.Rewiring

module FunUniverse.Nand {t} {T : ★_ t} {funU : FunUniverse T} (rewiring : Rewiring funU) where

open FunUniverse funU
open Rewiring rewiring

module FromNand (nand : `𝟚  `𝟚 `→ `𝟚) where
  not : `𝟚 `→ `𝟚
  not  = dup  nand 

  and or nor xor xnor : `𝟚  `𝟚 `→ `𝟚

  and  = nand  not
  or   = < not × not >  nand
  nor  = or  not
  xor  = < dup × dup >  inner2 (nand  dup)  < nand × nand >  nand
  xnor = xor  not

  -- xnor is _==_

  module _ {A B C D E}
    (f : A  B `→ D)
    (g : A  C `→ E) where

    dispatch : A  B  C `→ D  E
    dispatch = first dup  inner2 swap  < f × g > 

  -- 2-to-1 multiplexer
  -- mux (s , (e₀ , e₁)) = eₛ
  -- or
  -- mux (s , (e₀ , e₁)) = (not s ∧ e₀) ∨ (s ∧ e₁)
  mux : `𝟚  (`𝟚  `𝟚) `→ `𝟚
  mux = dispatch (< not × id >  and) and  or