From c25d3de0bc41ed7f09ccda97b1cf16dfda09220c Mon Sep 17 00:00:00 2001 From: Greg Brown Date: Mon, 21 Feb 2022 14:48:35 +0000 Subject: Introduce tuple deconstructor expressions --- src/Helium/Semantics/Denotational/Core.agda | 2 ++ 1 file changed, 2 insertions(+) (limited to 'src/Helium/Semantics') 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₂ ⟧ᵉ σ γ -- cgit v1.2.3