Guidance on very shallow embedding VHDL in AGDA Part II

Question

Hi I asked a question regarding my project here I have worked on it a fair amount and have made the following progress:

module project1 where

open import Data.Empty

open import Data.Unit hiding (_≟_)
open import Data.Nat hiding (_≟_; _⊔_)
open import Data.String
open import Data.List
open import Data.Vec hiding (_∈_)

open import Data.Sum
open import Data.Product
open import Function
open import Relation.Nullary
open import Relation.Binary

open import Relation.Binary.PropositionalEquality

open import Data.Vec hiding (_∈_)

data Bool : Set where
  true  : Bool
  false : Bool

-- The definition of a circuit and series and parallel combination of the circuit
data Ckt   :  Set where
  bool     : Bool → Ckt
  gate     : ℕ → ℕ → Ckt
  series   : Ckt → Ckt → Ckt
  parallel : Ckt → Ckt → Ckt


And : Ckt
And = gate 2 1

Not :  Ckt
Not = gate 1 1

Or : Ckt
Or = gate 2 1

Nand : Ckt
Nand = gate 2 1

Nand₁ : Ckt
Nand₁ = series And Not 


--Static Semantics


data Ctxt : Set where
  □   : Ctxt


data _⊢_  : (Γ : Ctxt) → (e : Ckt)  → Set where

  BoolT     : ∀ {Γ b} → Γ ⊢ bool b 
  GateT     : ∀ {Γ i o} →  Γ ⊢ gate  i o
  SeriesT   : ∀ {Γ c₁ c₂} →  Γ ⊢ c₁ → Γ ⊢ c₂  → Γ ⊢ series  c₁ c₂ 
  ParallelT : ∀ {Γ c₁ c₂} →  Γ ⊢ c₁ → Γ ⊢ c₂  → Γ ⊢ parallel  c₁ c₂

--dynamic semantics

--The type of input and output from the dynamics
in/out =   List Bool 

--closure is made up if the ckt and input/output
ClosureL : Set
ClosureL =   Ckt × in/out  


data FrameL  : Set where
  SeriesLK   : ClosureL → FrameL
  ParallelLK : ClosureL → FrameL
  SeriesRK   : in/out → FrameL
  ParallelRk : in/out → FrameL

ContL : Set
ContL = List FrameL


data StateL : Set where
  Enter : ClosureL → ContL → StateL
  Return : ContL → in/out → StateL

stepL : StateL → StateL
stepL (Enter (bool b , ρ) κ) = Return κ {!!}
stepL (Enter (gate i o , ρ) κ) = Return κ {!!}
stepL (Enter (series c₁ c₂ , ρ) κ) = Enter (c₁ , ρ) (SeriesLK (c₂ , ρ) ∷  κ)
stepL (Enter (parallel c₁ c₂ , ρ) κ) =  Enter (c₁ , ρ) (ParallelLK (c₂ , ρ) ∷  κ)

stepL (Return [] output) = Return [] output

stepL (Return (SeriesLK (e₂ , ρ) ∷ κ) output) = Enter (e₂ , {!!}) {!!} 

stepL (Return (ParallelLK (e₂ , ρ) ∷ κ) output) =  Enter (e₂ , {!!}) {!!} 

stepL (Return (SeriesRK x  ∷ κ) output) = {!!}
stepL (Return (ParallelRk x ∷ κ) output) = {!!}

My problem here is in the dynamic semantics. How do I ensure here that the input to the CEK machine(modified cek cuz its ckt input and stack instead of ckt env and stack) and the output are of the same length as that specified by the circuit. I short how do i specify the length of the input/output list when giving it as input to the machine? Please feel free to point out any other problems that you see in in my code.

Guidance on very shallow embedding VHDL in AGDA Part II

0 Answers0