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/Data/Pseudocode/Core.agda | 4 ++++ 1 file changed, 4 insertions(+) (limited to 'src/Helium/Data/Pseudocode/Core.agda') diff --git a/src/Helium/Data/Pseudocode/Core.agda b/src/Helium/Data/Pseudocode/Core.agda index 5cdf051..0e85c0d 100644 --- a/src/Helium/Data/Pseudocode/Core.agda +++ b/src/Helium/Data/Pseudocode/Core.agda @@ -157,6 +157,8 @@ module Code {o} (Σ : Vec Type o) where fin : ∀ {k ms n} → (All (Fin) ms → Fin n) → Expression Γ (tuple k (map fin ms)) → Expression Γ (fin n) asInt : ∀ {m} → Expression Γ (fin m) → Expression Γ int tup : ∀ {m ts} → All (Expression Γ) ts → Expression Γ (tuple m ts) + head : ∀ {m t ts} → Expression Γ (tuple (suc m) (t ∷ ts)) → Expression Γ t + tail : ∀ {m t ts} → Expression Γ (tuple (suc m) (t ∷ ts)) → Expression Γ (tuple m ts) call : ∀ {t m Δ} → Function Δ t → All (Expression Γ) {m} Δ → Expression Γ t if_then_else_ : ∀ {t} → Expression Γ bool → Expression Γ t → Expression Γ t → Expression Γ t @@ -198,6 +200,8 @@ module Code {o} (Σ : Vec Type o) where canAssign? (fin x e) = no λ () canAssign? (asInt e) = no λ () canAssign? (tup es) = map′ tup (λ { (tup es) → es }) (canAssignAll? es) + canAssign? (head e) = no λ () + canAssign? (tail e) = no λ () canAssign? (call x e) = no λ () canAssign? (if e then e₁ else e₂) = no λ () -- cgit v1.2.3