diff options
| author | Greg Brown <greg.brown@cl.cam.ac.uk> | 2022-02-21 14:48:35 +0000 |
|---|---|---|
| committer | Greg Brown <greg.brown@cl.cam.ac.uk> | 2022-02-21 14:48:35 +0000 |
| commit | c25d3de0bc41ed7f09ccda97b1cf16dfda09220c (patch) | |
| tree | 969b3c9cc4464b3cbc67f28f1d1730dc4ccc49d9 /src/Helium/Semantics | |
| parent | 281a29f01346bd2f00fbaca8391f38d856a45d6d (diff) | |
Introduce tuple deconstructor expressions
Diffstat (limited to 'src/Helium/Semantics')
| -rw-r--r-- | src/Helium/Semantics/Denotational/Core.agda | 2 |
1 files changed, 2 insertions, 0 deletions
diff --git a/src/Helium/Semantics/Denotational/Core.agda b/src/Helium/Semantics/Denotational/Core.agda index 4897b61..474a60f 100644 --- a/src/Helium/Semantics/Denotational/Core.agda +++ b/src/Helium/Semantics/Denotational/Core.agda @@ -234,6 +234,8 @@ module Expression ⟦ tup [] ⟧ᵉ σ γ = _ ⟦ tup (e ∷ []) ⟧ᵉ σ γ = ⟦ e ⟧ᵉ σ γ ⟦ tup (e ∷ e′ ∷ es) ⟧ᵉ σ γ = ⟦ e ⟧ᵉ σ γ , ⟦ tup (e′ ∷ es) ⟧ᵉ σ γ + ⟦ head {ts = ts} e ⟧ᵉ σ γ = tupHead ts (⟦ e ⟧ᵉ σ γ) + ⟦ tail {ts = ts} e ⟧ᵉ σ γ = tupTail ts (⟦ e ⟧ᵉ σ γ) ⟦ call f e ⟧ᵉ σ γ = ⟦ f ⟧ᶠ σ (⟦ e ⟧ᵉ′ σ γ) ⟦ if e then e₁ else e₂ ⟧ᵉ σ γ = Bool.if ⟦ e ⟧ᵉ σ γ then ⟦ e₁ ⟧ᵉ σ γ else ⟦ e₂ ⟧ᵉ σ γ |