diff options
| author | Greg Brown <greg.brown@cl.cam.ac.uk> | 2021-12-20 16:30:28 +0000 |
|---|---|---|
| committer | Greg Brown <greg.brown@cl.cam.ac.uk> | 2021-12-20 16:30:28 +0000 |
| commit | ee7e46719f428c61ef785ec791c341ddb350cc40 (patch) | |
| tree | df2042ee2bd12b8177d793b43c444fdb24a7a513 /src/Helium/Semantics/Denotational.agda | |
| parent | 79f1d021a7cd230d11cbd76dc4367024566a7bd5 (diff) | |
Improve type-checking efficiency.
Diffstat (limited to 'src/Helium/Semantics/Denotational.agda')
| -rw-r--r-- | src/Helium/Semantics/Denotational.agda | 26 |
1 files changed, 13 insertions, 13 deletions
diff --git a/src/Helium/Semantics/Denotational.agda b/src/Helium/Semantics/Denotational.agda index b80378b..8a6e0b5 100644 --- a/src/Helium/Semantics/Denotational.agda +++ b/src/Helium/Semantics/Denotational.agda @@ -117,21 +117,21 @@ module _ open sliceᶻ ≈ᶻ-trans round∘⟦⟧ round-cong 0#-homo-round 2^n≢0 *ᶻ-identityʳ vadd : VAdd.VAdd → Procedure 2 (Beat , ElmtMask , _) - vadd d = declare ⦇ zeros ⦈ (declare (! &Q ⦇ src₁ ⦈ (!# 1)) (label λ - result op₁ beat elmtMask → - [ (λ src₂ → for (toℕ elements) (lift ( - elem (toℕ esize) (&cast (sym e*e≡32) (wknRef result)) (!# 0) ≔ - ⦇ ! elem (toℕ esize) (&cast (sym e*e≡32) (wknRef op₁)) (!# 0) +ᵇ - ! slice (&R ⦇ src₂ ⦈) ⦇ (esize , zero , refl) ⦈ ⦈)) ) - , (λ src₂ → declare (! &Q ⦇ src₂ ⦈ (! beat)) (for (toℕ elements) (lift ( - elem (toℕ esize) (&cast (sym e*e≡32) (wknRef (wknRef result))) (!# 0) ≔ - ⦇ ! elem (toℕ esize) (&cast (sym e*e≡32) (wknRef (wknRef op₁))) (!# 0) +ᵇ - ! elem (toℕ esize) (&cast (sym e*e≡32) (var (# 1))) (!# 0) ⦈)))) - ]′ src₂ ∙ + vadd d = declare ⦇ zeros ⦈ (declare (! &Q ⦇ src₁ ⦈ (!# 1)) ( + -- op₁ result beat elmtMask + for (toℕ elements) (lift ( + -- e op₁ result beat elmtMask + elem (toℕ esize) (&cast (sym e*e≡32) (var (# 2))) (!# 0) ≔ + ⦇ ! elem (toℕ esize) (&cast (sym e*e≡32) (var (# 1))) (!# 0) +ᵇ + ([ (λ src₂ → ! slice (&R ⦇ src₂ ⦈) ⦇ (esize , zero , refl) ⦈) + , (λ src₂ → ! elem (toℕ esize) (&cast (sym e*e≡32) (&Q ⦇ src₂ ⦈ (!# 3))) (!# 0)) + ]′ src₂) ⦈ + )) ∙ for 4 (lift ( - if ⦇ (λ x y → does (getᵇ y x ≟ᵇ 1b)) (! wknRef elmtMask) (!# 0) ⦈ + -- e op₁ result beat elmtMask + if ⦇ (λ x y → does (getᵇ y x ≟ᵇ 1b)) (!# 4) (!# 0) ⦈ then - elem 8 (&Q ⦇ dest ⦈ (! wknRef beat)) (!# 0) ≔ (! elem 8 (wknRef result) (!# 0)) + elem 8 (&Q ⦇ dest ⦈ (!# 3)) (!# 0) ≔ (! elem 8 (var (# 2)) (!# 0)) else skip)))) where |