diff options
| author | Greg Brown <greg.brown@cl.cam.ac.uk> | 2021-12-21 15:14:54 +0000 |
|---|---|---|
| committer | Greg Brown <greg.brown@cl.cam.ac.uk> | 2021-12-21 15:14:54 +0000 |
| commit | 0b581ec922b40284291d6814578bd2e68049c8b7 (patch) | |
| tree | a4092b2cff7016426dd5a57e0c351627d1c1ea71 /src/Helium/Semantics/Denotational/Core.agda | |
| parent | 63f9978f448574d4df1ebacec52125a957482260 (diff) | |
Define execBeats, a wrapper to execute beat-wise instructions.
Diffstat (limited to 'src/Helium/Semantics/Denotational/Core.agda')
| -rw-r--r-- | src/Helium/Semantics/Denotational/Core.agda | 5 |
1 files changed, 4 insertions, 1 deletions
diff --git a/src/Helium/Semantics/Denotational/Core.agda b/src/Helium/Semantics/Denotational/Core.agda index bbddc57..54f0375 100644 --- a/src/Helium/Semantics/Denotational/Core.agda +++ b/src/Helium/Semantics/Denotational/Core.agda @@ -104,7 +104,7 @@ _,′_ : ∀ {n ls} {Γ : Sets n ls} → Reference n Γ τ → Reference n Γ τ -- Statements infixr 1 _∙_ -infix 4 _≔_ +infix 4 _≔_ _⟵_ infixl 2 if_then_else_ skip : ∀ {n ls} {Γ : Sets n ls} → Statement n Γ τ @@ -119,6 +119,9 @@ return e _ = e _≔_ : ∀ {n ls} {Γ : Sets n ls} → Reference n Γ τ → Expr n Γ τ → Statement n Γ τ′ (ref ≔ e) cont σ ρ = e σ ρ >>= λ (σ , v) → Reference.set ref σ ρ v >>= λ (σ , v) → cont σ v +_⟵_ : ∀ {n ls} {Γ : Sets n ls} → Reference n Γ τ → Op₁ τ → Statement n Γ τ′ +ref ⟵ e = ref ≔ ⦇ e (! ref) ⦈ + label : ∀ {n ls} {Γ : Sets n ls} → smap _ (Reference n Γ) n Γ ⇉ Statement n Γ τ → Statement n Γ τ label {n = n} s = uncurry⊤ₙ n s vars where |