for my project in Programming Languages I am doing a very shallow and simple embedding VHDL digital circuits in agda. The aim is to write the syntax, static semantics, dynamic semantics and then write some proofs to show our understanding of the material. Up till now I have written the following code:
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₂
What I am stuck at is how can I convert this program so as to carry out the program execution i-e I don't know how to start writing the dynamic semantics. Also, if there is any way to improve the syntax or statics of my current program then please let me know.
