AGDA 中极浅嵌入 VHDL 的指南

对于我的编程语言项目，我正在 agda 中做一个非常浅且简单的 VHDL 数字电路嵌入。目的是写出语法、静态语义、动态语义，然后写一些证明来展示我们对材料的理解。到目前为止我已经编写了以下代码：

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₂

我所困惑的是如何转换这个程序以便执行程序，即我不知道如何开始编写动态语义。另外，如果有任何方法可以改进我当前程序的语法或静态，请告诉我。