Руководство по очень мелкому встраиванию VHDL в AGDA

Question

Для моего проекта в Языки программирования я делаю очень поверхностное и простое встраивание цифровых схем VHDL в agda. Цель состоит в том, чтобы написать синтаксис, статическую семантику, динамическую семантику, а затем написать некоторые доказательства, чтобы показать наше понимание материала. До сих пор я написал следующий код:

data Ckt : Set where

   var      : String → Ckt
   bool     : Bool → Ckt 
   empty    : Ckt
   gate     : String →  ℕ → ℕ → Ckt  -- name in out 
   series   : String →  Ckt → Ckt → Ckt -- name  ckt1 ckt2
   parallel : String →  Ckt → Ckt → Ckt --name ckt1 ckt2  

And : Ckt 
And = gate "And"  2 1    

data Ctxt : Set where
  □   : Ctxt
  _,_ : (String ×  ℕ ×  ℕ) → Ctxt → Ctxt


_≈_ : Ctxt → Ctxt → Set
□ ≈ □                               = ⊤
□ ≈ (_ , _)                         = ⊥
(_ , _) ≈ □                         = ⊥
((s₁ , (in₁ , out₂)) , Γ₁) ≈ ((s₂ , (in₃ , out₄)) , Γ₂) = True (s₁ ≟ s₂) × in₁ ≡ in₃ × out₂ ≡ out₄  × Γ₁ ≈ Γ₂


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

  VarT      : ∀ {Γ s τ} → ((s , τ) ∈ Γ) → Γ ⊢ var s
  BoolT     : ∀ {Γ b} → Γ ⊢ bool b 
  EmptyT    : ∀ {Γ} → Γ ⊢ empty 
  GateT     : ∀ {Γ s i o} → (s , (i , o)) ∈ Γ  → Γ ⊢ gate s i o
  SeriesT   : ∀ {Γ s c₁ c₂} →  Γ ⊢ c₁ → Γ ⊢ c₂  → Γ ⊢ series s c₁ c₂ 
  ParallelT : ∀ {Γ s c₁ c₂} →  Γ ⊢ c₁ → Γ ⊢ c₂  → Γ ⊢ parallel s c₁ c₂

Я застрял в том, как я могу преобразовать эту программу для выполнения программы, т.е. я не знаю, как начать писать динамическую семантику. Кроме того, если есть какой-либо способ улучшить синтаксис или статику моей текущей программы, пожалуйста, дайте мне знать.