lattice.agda

module Lattice where

data Nat : Set where
    Z : Nat
    S : Nat -> Nat

data Lattice : Set where
    Lo : Lattice
    Hi : Lattice

-- sketch of how we can add security lattice features
join : Lattice -> Lattice -> Lattice
join Lo Lo = Lo
join _ Hi = Hi
join Hi _ = Hi

data Wire : (n : Nat) -> (l : Lattice) -> Set where
    W : (n : Nat) -> (l : Lattice) -> Wire n l

add : {n : Nat} {l l' : Lattice} -> Wire n l -> Wire n l' -> Wire n (join l l')
add = _

we need a general way to provide "compilers" for these data types so that the user can extend the language with primitives like this, where each wire becomes more complex.