diff options
| author | Greg Brown <greg.brown@cl.cam.ac.uk> | 2022-02-17 16:34:54 +0000 |
|---|---|---|
| committer | Greg Brown <greg.brown@cl.cam.ac.uk> | 2022-02-17 16:34:54 +0000 |
| commit | 60b201d0c8752b84194753bb72eee777bf245fe3 (patch) | |
| tree | 59a7eb2e8189ee84e7664dc1e562e88bbb09bac1 /src/Helium/Semantics | |
| parent | 273b6354ea17be93a0dfe4f50cd047b328762b02 (diff) | |
Make call and invoke take All instead of tuple.
Diffstat (limited to 'src/Helium/Semantics')
| -rw-r--r-- | src/Helium/Semantics/Denotational/Core.agda | 9 |
1 files changed, 7 insertions, 2 deletions
diff --git a/src/Helium/Semantics/Denotational/Core.agda b/src/Helium/Semantics/Denotational/Core.agda index 25f0448..d4060f5 100644 --- a/src/Helium/Semantics/Denotational/Core.agda +++ b/src/Helium/Semantics/Denotational/Core.agda @@ -152,6 +152,7 @@ module Expression ⟦_⟧ˢ : ∀ {n} {Γ : Vec Type n} → Statement Γ → ⟦ Σ ⟧ₜ′ → ⟦ Γ ⟧ₜ′ → ⟦ Σ ⟧ₜ′ × ⟦ Γ ⟧ₜ′ ⟦_⟧ᶠ : ∀ {n} {Γ : Vec Type n} {ret} → Function Γ ret → ⟦ Σ ⟧ₜ′ → ⟦ Γ ⟧ₜ′ → ⟦ ret ⟧ₜ ⟦_⟧ᵖ : ∀ {n} {Γ : Vec Type n} → Procedure Γ → ⟦ Σ ⟧ₜ′ → ⟦ Γ ⟧ₜ′ → ⟦ Σ ⟧ₜ′ + ⟦_⟧ᵉ′ : ∀ {n} {Γ : Vec Type n} {m ts} → All (Expression Γ) ts → ⟦ Σ ⟧ₜ′ → ⟦ Γ ⟧ₜ′ → ⟦ tuple m ts ⟧ₜ update : ∀ {n Γ t e} → CanAssign {n} {Γ} {t} e → ⟦ t ⟧ₜ → ⟦ Σ ⟧ₜ′ → ⟦ Γ ⟧ₜ′ → ⟦ Σ ⟧ₜ′ × ⟦ Γ ⟧ₜ′ ⟦ lit x ⟧ᵉ σ γ = 𝒦 x @@ -188,14 +189,18 @@ module Expression ⟦ tup [] ⟧ᵉ σ γ = _ ⟦ tup (e ∷ []) ⟧ᵉ σ γ = ⟦ e ⟧ᵉ σ γ ⟦ tup (e ∷ e′ ∷ es) ⟧ᵉ σ γ = ⟦ e ⟧ᵉ σ γ , ⟦ tup (e′ ∷ es) ⟧ᵉ σ γ - ⟦ call f e ⟧ᵉ σ γ = ⟦ f ⟧ᶠ σ (⟦ e ⟧ᵉ σ γ) + ⟦ call f e ⟧ᵉ σ γ = ⟦ f ⟧ᶠ σ (⟦ e ⟧ᵉ′ σ γ) ⟦ if e then e₁ else e₂ ⟧ᵉ σ γ = Bool.if ⟦ e ⟧ᵉ σ γ then ⟦ e₁ ⟧ᵉ σ γ else ⟦ e₂ ⟧ᵉ σ γ + ⟦ [] ⟧ᵉ′ σ γ = _ + ⟦ e ∷ [] ⟧ᵉ′ σ γ = ⟦ e ⟧ᵉ σ γ + ⟦ e ∷ e′ ∷ es ⟧ᵉ′ σ γ = ⟦ e ⟧ᵉ σ γ , ⟦ e′ ∷ es ⟧ᵉ′ σ γ + ⟦ s ∙ s₁ ⟧ˢ σ γ = P.uncurry ⟦ s ⟧ˢ (⟦ s ⟧ˢ σ γ) ⟦ skip ⟧ˢ σ γ = σ , γ ⟦ _≔_ ref {canAssign = canAssign} e ⟧ˢ σ γ = update (toWitness canAssign) (⟦ e ⟧ᵉ σ γ) σ γ ⟦_⟧ˢ {Γ = Γ} (declare e s) σ γ = P.map₂ (tupTail Γ) (⟦ s ⟧ˢ σ (tupCons Γ (⟦ e ⟧ᵉ σ γ) γ)) - ⟦ invoke p e ⟧ˢ σ γ = ⟦ p ⟧ᵖ σ (⟦ e ⟧ᵉ σ γ) , γ + ⟦ invoke p e ⟧ˢ σ γ = ⟦ p ⟧ᵖ σ (⟦ e ⟧ᵉ′ σ γ) , γ ⟦ if e then s₁ else s₂ ⟧ˢ σ γ = Bool.if ⟦ e ⟧ᵉ σ γ then ⟦ s₁ ⟧ˢ σ γ else ⟦ s₂ ⟧ˢ σ γ ⟦_⟧ˢ {Γ = Γ} (for m s) σ γ = helper m ⟦ s ⟧ˢ σ γ where |