diff options
Diffstat (limited to 'src')
| -rw-r--r-- | src/Helium/Data/Pseudocode/Core.agda | 38 | ||||
| -rw-r--r-- | src/Helium/Instructions/Base.agda | 35 | ||||
| -rw-r--r-- | src/Helium/Semantics/Core.agda | 82 | ||||
| -rw-r--r-- | src/Helium/Semantics/Denotational/Core.agda | 67 |
4 files changed, 93 insertions, 129 deletions
diff --git a/src/Helium/Data/Pseudocode/Core.agda b/src/Helium/Data/Pseudocode/Core.agda index 4dbf552..6ae1d34 100644 --- a/src/Helium/Data/Pseudocode/Core.agda +++ b/src/Helium/Data/Pseudocode/Core.agda @@ -31,18 +31,17 @@ data Type : Set where int : Type fin : (n : ℕ) → Type real : Type + bit : Type bits : (n : ℕ) → Type tuple : ∀ n → Vec Type n → Type array : Type → (n : ℕ) → Type -bit : Type -bit = bits 1 - data HasEquality : Type → Set where bool : HasEquality bool int : HasEquality int fin : ∀ {n} → HasEquality (fin n) real : HasEquality real + bit : HasEquality bit bits : ∀ {n} → HasEquality (bits n) hasEquality? : Decidable HasEquality @@ -50,6 +49,7 @@ hasEquality? bool = yes bool hasEquality? int = yes int hasEquality? (fin n) = yes fin hasEquality? real = yes real +hasEquality? bit = yes bit hasEquality? (bits n) = yes bits hasEquality? (tuple n x) = no (λ ()) hasEquality? (array t n) = no (λ ()) @@ -61,8 +61,9 @@ data IsNumeric : Type → Set where isNumeric? : Decidable IsNumeric isNumeric? bool = no (λ ()) isNumeric? int = yes int -isNumeric? real = yes real isNumeric? (fin n) = no (λ ()) +isNumeric? real = yes real +isNumeric? bit = no (λ ()) isNumeric? (bits n) = no (λ ()) isNumeric? (tuple n x) = no (λ ()) isNumeric? (array t n) = no (λ ()) @@ -87,12 +88,13 @@ elemType (array t) = t --- Literals data Literal : Type → Set where - _′b : Bool → Literal bool - _′i : ℕ → Literal int - _′f : ∀ {n} → Fin n → Literal (fin n) - _′r : ℕ → Literal real - _′x : ∀ {n} → Vec Bool n → Literal (bits n) - _′a : ∀ {n t} → Literal t → Literal (array t n) + _′b : Bool → Literal bool + _′i : ℕ → Literal int + _′f : ∀ {n} → Fin n → Literal (fin n) + _′r : ℕ → Literal real + _′x : Bool → Literal bit + _′xs : ∀ {n} → Vec Bool n → Literal (bits n) + _′a : ∀ {n t} → Literal t → Literal (array t n) --- Expressions, references, statements, functions and procedures @@ -130,8 +132,8 @@ module Code {o} (Σ : Vec Type o) where not : ∀ {m} → Expression Γ (bits m) → Expression Γ (bits m) _and_ : ∀ {m} → Expression Γ (bits m) → Expression Γ (bits m) → Expression Γ (bits m) _or_ : ∀ {m} → Expression Γ (bits m) → Expression Γ (bits m) → Expression Γ (bits m) - [_] : ∀ {t} → Expression Γ t → Expression Γ (array t 1) - unbox : ∀ {t} → Expression Γ (array t 1) → Expression Γ t + [_] : ∀ {t} → Expression Γ (elemType t) → Expression Γ (asType t 1) + unbox : ∀ {t} → Expression Γ (asType t 1) → Expression Γ (elemType t) _∶_ : ∀ {m n t} → Expression Γ (asType t m) → Expression Γ (asType t n) → Expression Γ (asType t (n ℕ.+ m)) slice : ∀ {i j t} → Expression Γ (asType t (i ℕ.+ j)) → Expression Γ (fin (suc i)) → Expression Γ (asType t j) cast : ∀ {i j t} → .(eq : i ≡ j) → Expression Γ (asType t i) → Expression Γ (asType t j) @@ -153,8 +155,8 @@ module Code {o} (Σ : Vec Type o) where var : ∀ i {i<n : True (i ℕ.<? n)} → CanAssign (var i {i<n}) abort : ∀ {t} {e : Expression Γ (fin 0)} → CanAssign (abort {t = t} e) _∶_ : ∀ {m n t} {e₁ : Expression Γ (asType t m)} {e₂ : Expression Γ (asType t n)} → CanAssign e₁ → CanAssign e₂ → CanAssign (e₁ ∶ e₂) - [_] : ∀ {t} {e : Expression Γ t} → CanAssign e → CanAssign [ e ] - unbox : ∀ {t} {e : Expression Γ (array t 1)} → CanAssign e → CanAssign (unbox e) + [_] : ∀ {t} {e : Expression Γ (elemType t)} → CanAssign e → CanAssign ([_] {t = t} e) + unbox : ∀ {t} {e : Expression Γ (asType t 1)} → CanAssign e → CanAssign (unbox e) slice : ∀ {i j t} {e₁ : Expression Γ (asType t (i ℕ.+ j))} → CanAssign e₁ → (e₂ : Expression Γ (fin (suc i))) → CanAssign (slice e₁ e₂) cast : ∀ {i j t} {e : Expression Γ (asType t i)} .(eq : i ≡ j) → CanAssign e → CanAssign (cast eq e) tup : ∀ {m ts} {es : All (Expression Γ) {m} ts} → All (CanAssign ∘ proj₂) (reduce (λ {x} e → x , e) es) → CanAssign (tup es) @@ -267,21 +269,21 @@ module Code {o} (Σ : Vec Type o) where x << n = rnd (x * lit (2 ′r) ^ n) get : ∀ {n Γ} → ℕ → Expression {n} Γ int → Expression Γ bit - get i x = if x - x >> suc i << suc i <? lit (2 ′i) ^ i then lit ((false ∷ []) ′x) else lit ((true ∷ []) ′x) + get i x = if x - x >> suc i << suc i <? lit (2 ′i) ^ i then lit (false ′x) else lit (true ′x) uint : ∀ {n Γ m} → Expression {n} Γ (bits m) → Expression Γ int uint {m = zero} x = lit (0 ′i) uint {m = suc m} x = lit (2 ′i) * uint {m = m} (slice x (lit ((# 1) ′f))) + - ( if slice′ x (lit ((# 0) ′f)) ≟ lit ((true ∷ []) ′x) + ( if slice′ x (lit ((# 0) ′f)) ≟ lit ((true ∷ []) ′xs) then lit (1 ′i) else lit (0 ′i)) sint : ∀ {n Γ m} → Expression {n} Γ (bits m) → Expression Γ int sint {m = zero} x = lit (0 ′i) - sint {m = suc zero} x = if x ≟ lit ((true ∷ []) ′x) then - lit (1 ′i) else lit (0 ′i) + sint {m = suc zero} x = if x ≟ lit ((true ∷ []) ′xs) then - lit (1 ′i) else lit (0 ′i) sint {m = suc (suc m)} x = lit (2 ′i) * sint (slice {i = 1} x (lit ((# 1) ′f))) + - ( if slice′ x (lit ((# 0) ′f)) ≟ lit ((true ∷ []) ′x) + ( if slice′ x (lit ((# 0) ′f)) ≟ lit ((true ∷ []) ′xs) then lit (1 ′i) else lit (0 ′i)) diff --git a/src/Helium/Instructions/Base.agda b/src/Helium/Instructions/Base.agda index a76b2b1..3261107 100644 --- a/src/Helium/Instructions/Base.agda +++ b/src/Helium/Instructions/Base.agda @@ -84,8 +84,7 @@ join {k = k} {suc m} x = cast eq (join (slice x (lit (Fin.fromℕ 1 ′f))) ∶ eq = P.trans (P.cong (k ℕ.+_) (ℕₚ.*-comm k (suc m))) (ℕₚ.*-comm (suc (suc m)) k) index : ∀ {n Γ t m} → Expression {n} Γ (asType t (suc m)) → Expression Γ (fin (suc m)) → Expression Γ (elemType t) -index {t = bits} {m} x i = slice (cast (ℕₚ.+-comm 1 m) x) i -index {t = array _} {m} x i = unbox (slice (cast (ℕₚ.+-comm 1 m) x) i) +index {m = m} x i = unbox (slice (cast (ℕₚ.+-comm 1 m) x) i) Q : ∀ {n Γ} → Expression {n} Γ (array (array (bits 32) 4) 8) Q = group 7 S @@ -98,11 +97,11 @@ elem {k = suc k} (suc m) x i = index (group k (cast (ℕₚ.*-comm (suc k) (suc --- Other utiliies hasBit : ∀ {n Γ m} → Expression {n} Γ (bits (suc m)) → Expression Γ (fin (suc m)) → Expression Γ bool -hasBit {n} x i = index x i ≟ lit ((true ∷ []) ′x) +hasBit {n} x i = index x i ≟ lit (true ′x) sliceⁱ : ∀ {n Γ m} → ℕ → Expression {n} Γ int → Expression Γ (bits m) -sliceⁱ {m = zero} n i = lit ([] ′x) -sliceⁱ {m = suc m} n i = sliceⁱ (suc n) i ∶ get n i +sliceⁱ {m = zero} n i = lit ([] ′xs) +sliceⁱ {m = suc m} n i = sliceⁱ (suc n) i ∶ [ get n i ] --- Functions @@ -127,10 +126,10 @@ SignedSatQ n = declare (lit (true ′b)) ( -- actual shift if 'shift + 1' LSL-C : ∀ {n} (shift : ℕ) → Function (bits n ∷ []) (tuple 2 (bits n ∷ bit ∷ [])) -LSL-C {n} shift = declare (var 0 ∶ lit ((Vec.replicate {n = (suc shift)} false) ′x)) +LSL-C {n} shift = declare (var 0 ∶ lit ((Vec.replicate {n = (suc shift)} false) ′xs)) (skip ∙return tup ( slice (var 0) (lit (zero ′f)) - ∷ slice (cast eq (var 0)) (lit (Fin.inject+ shift (Fin.fromℕ n) ′f)) + ∷ unbox (slice (cast eq (var 0)) (lit (Fin.inject+ shift (Fin.fromℕ n) ′f))) ∷ [])) where eq = P.trans (ℕₚ.+-comm 1 (shift ℕ.+ n)) (P.cong (ℕ._+ 1) (ℕₚ.+-comm shift n)) @@ -156,30 +155,30 @@ VPTAdvance : Procedure (beat ∷ []) VPTAdvance = declare (fin div2 (tup (var 0 ∷ []))) ( declare (elem 4 VPR-mask (var 0)) ( -- 0:vptState 1:maskId 2:beat - if var 0 ≟ lit ((true ∷ false ∷ false ∷ false ∷ []) ′x) + if var 0 ≟ lit ((true ∷ false ∷ false ∷ false ∷ []) ′xs) then - var 0 ≔ lit (Vec.replicate false ′x) - else if inv (var 0 ≟ lit (Vec.replicate false ′x)) + var 0 ≔ lit (Vec.replicate false ′xs) + else if inv (var 0 ≟ lit (Vec.replicate false ′xs)) then ( - declare (lit ((false ∷ []) ′x)) ( + declare (lit (false ′x)) ( -- 0:inv 1:vptState 2:maskId 3:beat tup (var 1 ∷ var 0 ∷ []) ≔ call (LSL-C 0) (var 1 ∷ []) ∙ - if var 0 ≟ lit ((true ∷ []) ′x) + if var 0 ≟ lit (true ′x) then elem 4 VPR-P0 (var 3) ≔ not (elem 4 VPR-P0 (var 3)) else skip)) else skip ∙ - if get 0 (asInt (var 2)) ≟ lit ((true ∷ []) ′x) + if get 0 (asInt (var 2)) ≟ lit (true ′x) then elem 4 VPR-mask (var 1) ≔ var 0 else skip)) ∙end VPTActive : Function (beat ∷ []) bool -VPTActive = skip ∙return inv (elem 4 VPR-mask (fin div2 (tup (var 0 ∷ []))) ≟ lit (Vec.replicate false ′x)) +VPTActive = skip ∙return inv (elem 4 VPR-mask (fin div2 (tup (var 0 ∷ []))) ≟ lit (Vec.replicate false ′xs)) GetCurInstrBeat : Function [] (tuple 2 (beat ∷ elmtMask ∷ [])) -GetCurInstrBeat = declare (lit (Vec.replicate true ′x)) ( +GetCurInstrBeat = declare (lit (Vec.replicate true ′xs)) ( -- 0:elmtMask 1:beat if call VPTActive (BeatId ∷ []) then @@ -222,10 +221,10 @@ module _ (d : Instr.VecOp₂) where -- 0:op₂ 1:e 2:op₁ 3:result 4:elmtMask 5:curBeat vec-op₂′ : Statement (bits (toℕ esize) ∷ fin (toℕ elements) ∷ array (bits (toℕ esize)) (toℕ elements) ∷ array (bits (toℕ esize)) (toℕ elements) ∷ elmtMask ∷ beat ∷ []) → Procedure [] vec-op₂′ op = declare (lit (zero ′f)) ( - declare (lit (Vec.replicate false ′x)) ( + declare (lit (Vec.replicate false ′xs)) ( -- 0:elmtMask 1:curBeat tup (var 1 ∷ var 0 ∷ []) ≔ call GetCurInstrBeat [] ∙ - declare (lit ((Vec.replicate false ′x) ′a)) ( + declare (lit ((Vec.replicate false ′xs) ′a)) ( declare (from32 size (index (index Q (lit (src₁ ′f))) (var 2))) ( -- 0:op₁ 1:result 2:elmtMask 3:curBeat for (toℕ elements) ( @@ -285,7 +284,7 @@ private tup (index (var 5) (var 3) ∷ var 0 ∷ []) ≔ call (SignedSatQ (toℕ esize-1)) (var 1 ∷ []) ∙ if var 0 && hasBit (var 6) (fin e*esize>>3 (tup ((var 3) ∷ []))) then - FPSCR-QC ≔ lit ((true ∷ []) ′x) + FPSCR-QC ≔ lit (true ′x) else skip))) where open Instr.VecOp₂ d diff --git a/src/Helium/Semantics/Core.agda b/src/Helium/Semantics/Core.agda deleted file mode 100644 index 749e1ca..0000000 --- a/src/Helium/Semantics/Core.agda +++ /dev/null @@ -1,82 +0,0 @@ ------------------------------------------------------------------------- --- Agda Helium --- --- Shared definitions between semantic systems ------------------------------------------------------------------------- - -{-# OPTIONS --safe --without-K #-} - -open import Helium.Data.Pseudocode.Types using (RawPseudocode) - -module Helium.Semantics.Core - {b₁ b₂ i₁ i₂ i₃ r₁ r₂ r₃} - (rawPseudocode : RawPseudocode b₁ b₂ i₁ i₂ i₃ r₁ r₂ r₃) - where - -private - open module C = RawPseudocode rawPseudocode - -open import Data.Bool using (Bool) -open import Data.Fin using (Fin; zero; suc) -open import Data.Product using (_×_; _,_) -open import Data.Unit using (⊤) -open import Data.Vec using (Vec; []; _∷_; lookup) -open import Helium.Data.Pseudocode.Core -open import Level hiding (zero; suc) - -⟦_⟧ₗ : Type → Level -⟦ bool ⟧ₗ = 0ℓ -⟦ int ⟧ₗ = i₁ -⟦ fin n ⟧ₗ = 0ℓ -⟦ real ⟧ₗ = r₁ -⟦ bits n ⟧ₗ = b₁ -⟦ tuple n ts ⟧ₗ = helper ts - where - helper : ∀ {n} → Vec Type n → Level - helper [] = 0ℓ - helper (t ∷ ts) = ⟦ t ⟧ₗ ⊔ helper ts -⟦ array t n ⟧ₗ = ⟦ t ⟧ₗ - -⟦_⟧ₜ : ∀ t → Set ⟦ t ⟧ₗ -⟦_⟧ₜ′ : ∀ {n} ts → Set ⟦ tuple n ts ⟧ₗ - -⟦ bool ⟧ₜ = Bool -⟦ int ⟧ₜ = ℤ -⟦ fin n ⟧ₜ = Fin n -⟦ real ⟧ₜ = ℝ -⟦ bits n ⟧ₜ = Bits n -⟦ tuple n ts ⟧ₜ = ⟦ ts ⟧ₜ′ -⟦ array t n ⟧ₜ = Vec ⟦ t ⟧ₜ n - -⟦ [] ⟧ₜ′ = ⊤ -⟦ t ∷ [] ⟧ₜ′ = ⟦ t ⟧ₜ -⟦ t ∷ t′ ∷ ts ⟧ₜ′ = ⟦ t ⟧ₜ × ⟦ t′ ∷ ts ⟧ₜ′ - -⟦_⟧ₜˡ : Type → Set (b₁ ⊔ i₁ ⊔ r₁) -⟦_⟧ₜˡ′ : ∀ {n} → Vec Type n → Set (b₁ ⊔ i₁ ⊔ r₁) - -⟦ bool ⟧ₜˡ = Lift (b₁ ⊔ i₁ ⊔ r₁) Bool -⟦ int ⟧ₜˡ = Lift (b₁ ⊔ r₁) ℤ -⟦ fin n ⟧ₜˡ = Lift (b₁ ⊔ i₁ ⊔ r₁) (Fin n) -⟦ real ⟧ₜˡ = Lift (b₁ ⊔ i₁) ℝ -⟦ bits n ⟧ₜˡ = Lift (i₁ ⊔ r₁) (Bits n) -⟦ tuple n ts ⟧ₜˡ = ⟦ ts ⟧ₜˡ′ -⟦ array t n ⟧ₜˡ = Vec ⟦ t ⟧ₜˡ n - -⟦ [] ⟧ₜˡ′ = Lift (b₁ ⊔ i₁ ⊔ r₁) ⊤ -⟦ t ∷ [] ⟧ₜˡ′ = ⟦ t ⟧ₜˡ -⟦ t ∷ t′ ∷ ts ⟧ₜˡ′ = ⟦ t ⟧ₜˡ × ⟦ t′ ∷ ts ⟧ₜˡ′ - -fetch : ∀ {n} ts → ⟦ tuple n ts ⟧ₜ → ∀ i → ⟦ lookup ts i ⟧ₜ -fetch (_ ∷ []) x zero = x -fetch (_ ∷ _ ∷ _) (x , xs) zero = x -fetch (_ ∷ t ∷ ts) (x , xs) (suc i) = fetch (t ∷ ts) xs i - -fetchˡ : ∀ {n} ts → ⟦ tuple n ts ⟧ₜˡ → ∀ i → ⟦ lookup ts i ⟧ₜˡ -fetchˡ (_ ∷ []) x zero = x -fetchˡ (_ ∷ _ ∷ _) (x , xs) zero = x -fetchˡ (_ ∷ t ∷ ts) (x , xs) (suc i) = fetchˡ (t ∷ ts) xs i - -consˡ : ∀ {n t} ts → ⟦ t ⟧ₜˡ → ⟦ tuple n ts ⟧ₜˡ → ⟦ t ∷ ts ⟧ₜˡ′ -consˡ [] x xs = x -consˡ (_ ∷ _) x xs = x , xs diff --git a/src/Helium/Semantics/Denotational/Core.agda b/src/Helium/Semantics/Denotational/Core.agda index 6ec0b24..46d68bc 100644 --- a/src/Helium/Semantics/Denotational/Core.agda +++ b/src/Helium/Semantics/Denotational/Core.agda @@ -29,21 +29,57 @@ open import Data.Vec.Relation.Unary.All using (All; []; _∷_) import Data.Vec.Functional as VecF open import Function using (case_of_; _∘′_; id) open import Helium.Data.Pseudocode.Core -open import Helium.Semantics.Core rawPseudocode import Induction as I import Induction.WellFounded as Wf +open import Level using (Level; _⊔_; 0ℓ) open import Relation.Binary.PropositionalEquality as ≡ using (_≡_; module ≡-Reasoning) open import Relation.Nullary using (does) open import Relation.Nullary.Decidable.Core using (True; False; toWitness; fromWitness) +⟦_⟧ₗ : Type → Level +⟦ bool ⟧ₗ = 0ℓ +⟦ int ⟧ₗ = i₁ +⟦ fin n ⟧ₗ = 0ℓ +⟦ real ⟧ₗ = r₁ +⟦ bit ⟧ₗ = b₁ +⟦ bits n ⟧ₗ = b₁ +⟦ tuple n ts ⟧ₗ = helper ts + where + helper : ∀ {n} → Vec Type n → Level + helper [] = 0ℓ + helper (t ∷ ts) = ⟦ t ⟧ₗ ⊔ helper ts +⟦ array t n ⟧ₗ = ⟦ t ⟧ₗ + +⟦_⟧ₜ : ∀ t → Set ⟦ t ⟧ₗ +⟦_⟧ₜ′ : ∀ {n} ts → Set ⟦ tuple n ts ⟧ₗ + +⟦ bool ⟧ₜ = Bool +⟦ int ⟧ₜ = ℤ +⟦ fin n ⟧ₜ = Fin n +⟦ real ⟧ₜ = ℝ +⟦ bit ⟧ₜ = Bit +⟦ bits n ⟧ₜ = Bits n +⟦ tuple n ts ⟧ₜ = ⟦ ts ⟧ₜ′ +⟦ array t n ⟧ₜ = Vec ⟦ t ⟧ₜ n + +⟦ [] ⟧ₜ′ = ⊤ +⟦ t ∷ [] ⟧ₜ′ = ⟦ t ⟧ₜ +⟦ t ∷ t′ ∷ ts ⟧ₜ′ = ⟦ t ⟧ₜ × ⟦ t′ ∷ ts ⟧ₜ′ + -- The case for bitvectors looks odd so that the right-most bit is bit 0. 𝒦 : ∀ {t} → Literal t → ⟦ t ⟧ₜ -𝒦 (x ′b) = x -𝒦 (x ′i) = x ℤ′.×′ 1ℤ -𝒦 (x ′f) = x -𝒦 (x ′r) = x ℝ′.×′ 1ℝ -𝒦 (xs ′x) = Vec.foldl Bits (λ bs b → (Bool.if b then 1𝔹 else 0𝔹) VecF.∷ bs) VecF.[] xs -𝒦 (x ′a) = Vec.replicate (𝒦 x) +𝒦 (x ′b) = x +𝒦 (x ′i) = x ℤ′.×′ 1ℤ +𝒦 (x ′f) = x +𝒦 (x ′r) = x ℝ′.×′ 1ℝ +𝒦 (x ′x) = Bool.if x then 1𝔹 else 0𝔹 +𝒦 (xs ′xs) = Vec.foldl Bits (λ bs b → (Bool.if b then 1𝔹 else 0𝔹) VecF.∷ bs) VecF.[] xs +𝒦 (x ′a) = Vec.replicate (𝒦 x) + +fetch : ∀ {n} ts → ⟦ tuple n ts ⟧ₜ → ∀ i → ⟦ Vec.lookup ts i ⟧ₜ +fetch (_ ∷ []) x zero = x +fetch (_ ∷ _ ∷ _) (x , xs) zero = x +fetch (_ ∷ t ∷ ts) (x , xs) (suc i) = fetch (t ∷ ts) xs i updateAt : ∀ {n} ts i → ⟦ Vec.lookup ts i ⟧ₜ → ⟦ tuple n ts ⟧ₜ → ⟦ tuple n ts ⟧ₜ updateAt (_ ∷ []) zero v _ = v @@ -66,6 +102,7 @@ equal bool x y = does (x Bool.≟ y) equal int x y = does (x ≟ᶻ y) equal fin x y = does (x Fin.≟ y) equal real x y = does (x ≟ʳ y) +equal bit x y = does (x ≟ᵇ₁ y) equal bits x y = does (x ≟ᵇ y) comp : ∀ {t} → IsNumeric t → ⟦ t ⟧ₜ → ⟦ t ⟧ₜ → Bool @@ -118,6 +155,14 @@ updateSliced t {i} {j} orig off v f = f (casted t (≡.sym eq) (join t (join t u dropped = take t (Fin.toℕ off) (casted t eq orig) untaken = drop t j (drop t (Fin.toℕ off) (casted t eq orig)) +box : ∀ t → ⟦ elemType t ⟧ₜ → ⟦ asType t 1 ⟧ₜ +box bits v = v VecF.∷ VecF.[] +box (array t) v = v ∷ [] + +unboxed : ∀ t → ⟦ asType t 1 ⟧ₜ → ⟦ elemType t ⟧ₜ +unboxed bits v = v (Fin.zero) +unboxed (array t) (v ∷ []) = v + neg : ∀ {t} → IsNumeric t → ⟦ t ⟧ₜ → ⟦ t ⟧ₜ neg int x = ℤ.- x neg real x = ℝ.- x @@ -167,8 +212,8 @@ module Expression ⟦ not e ⟧ᵉ σ γ = Bits.¬_ (⟦ e ⟧ᵉ σ γ) ⟦ e and e₁ ⟧ᵉ σ γ = ⟦ e ⟧ᵉ σ γ Bits.∧ ⟦ e₁ ⟧ᵉ σ γ ⟦ e or e₁ ⟧ᵉ σ γ = ⟦ e ⟧ᵉ σ γ Bits.∨ ⟦ e₁ ⟧ᵉ σ γ - ⟦ [ e ] ⟧ᵉ σ γ = ⟦ e ⟧ᵉ σ γ Vec.∷ [] - ⟦ unbox e ⟧ᵉ σ γ = Vec.head (⟦ e ⟧ᵉ σ γ) + ⟦ [_] {t = t} e ⟧ᵉ σ γ = box t (⟦ e ⟧ᵉ σ γ) + ⟦ unbox {t = t} e ⟧ᵉ σ γ = unboxed t (⟦ e ⟧ᵉ σ γ) ⟦ _∶_ {t = t} e e₁ ⟧ᵉ σ γ = join t (⟦ e ⟧ᵉ σ γ) (⟦ e₁ ⟧ᵉ σ γ) ⟦ slice {t = t} e e₁ ⟧ᵉ σ γ = sliced t (⟦ e ⟧ᵉ σ γ) (⟦ e₁ ⟧ᵉ σ γ) ⟦ cast {t = t} eq e ⟧ᵉ σ γ = casted t eq (⟦ e ⟧ᵉ σ γ) @@ -224,8 +269,8 @@ module Expression update (_∶_ {m = m} {t = t} e e₁) v σ γ = do let σ′ , γ′ = update e (sliced t v (Fin.fromℕ _)) σ γ update e₁ (sliced t (casted t (ℕₚ.+-comm _ m) v) zero) σ′ γ′ - update [ e ] v σ γ = update e (Vec.head v) σ γ - update (unbox e) v σ γ = update e (v ∷ []) σ γ + update ([_] {t = t} e) v σ γ = update e (unboxed t v) σ γ + update (unbox {t = t} e) v σ γ = update e (box t v) σ γ update (slice {t = t} {e₁ = e₁} a e₂) v σ γ = updateSliced t (⟦ e₁ ⟧ᵉ σ γ) (⟦ e₂ ⟧ᵉ σ γ) v (λ v → update a v σ γ) update (cast {t = t} eq e) v σ γ = update e (casted t (≡.sym eq) v) σ γ update (tup {es = []} x) v σ γ = σ , γ |