diff options
| -rw-r--r-- | src/Helium/Data/Pseudocode/Core.agda | 4 | ||||
| -rw-r--r-- | src/Helium/Semantics/Denotational/Core.agda | 2 |
2 files changed, 6 insertions, 0 deletions
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 λ () 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₂ ⟧ᵉ σ γ |