From 281a29f01346bd2f00fbaca8391f38d856a45d6d Mon Sep 17 00:00:00 2001
From: Greg Brown <greg.brown@cl.cam.ac.uk>
Date: Mon, 21 Feb 2022 12:18:31 +0000
Subject: Replace nat indices with fins.

---
 src/Helium/Data/Pseudocode/Core.agda        |  12 ++--
 src/Helium/Instructions/Base.agda           | 103 ++++++++++++++--------------
 src/Helium/Semantics/Denotational/Core.agda |  10 +--
 3 files changed, 63 insertions(+), 62 deletions(-)

(limited to 'src')

diff --git a/src/Helium/Data/Pseudocode/Core.agda b/src/Helium/Data/Pseudocode/Core.agda
index d683947..5cdf051 100644
--- a/src/Helium/Data/Pseudocode/Core.agda
+++ b/src/Helium/Data/Pseudocode/Core.agda
@@ -19,7 +19,7 @@ open import Data.Vec.Relation.Unary.All using (All; []; _∷_; reduce)
 open import Data.Vec.Relation.Unary.Any using (Any; here; there)
 open import Function as F using (_∘_; _∘′_; _∋_)
 open import Relation.Binary.PropositionalEquality using (_≡_; refl)
-open import Relation.Nullary using (yes; no)
+open import Relation.Nullary using (Dec; yes; no)
 open import Relation.Nullary.Decidable.Core using (True; False; toWitness; fromWitness; map′)
 open import Relation.Nullary.Product using (_×-dec_)
 open import Relation.Nullary.Sum using (_⊎-dec_)
@@ -131,8 +131,8 @@ module Code {o} (Σ : Vec Type o) where
 
   data Expression {n} Γ where
     lit   : ∀ {t} → Literal t → Expression Γ t
-    state : ∀ i {i<o : True (i ℕ.<? o)} → Expression Γ (lookup Σ (#_ i {m<n = i<o}))
-    var   : ∀ i {i<n : True (i ℕ.<? n)} → Expression Γ (lookup Γ (#_ i {m<n = i<n}))
+    state : ∀ i → Expression Γ (lookup Σ i)
+    var   : ∀ i → Expression Γ (lookup Γ i)
     abort : ∀ {t} → Expression Γ (fin 0) → Expression Γ t
     _≟_   : ∀ {t} {hasEquality : True (hasEquality? t)} → Expression Γ t → Expression Γ t → Expression Γ bool
     _<?_  : ∀ {t} {isNumeric : True (isNumeric? t)} → Expression Γ t → Expression Γ t → Expression Γ bool
@@ -161,8 +161,8 @@ module Code {o} (Σ : Vec Type o) where
     if_then_else_ : ∀ {t} → Expression Γ bool → Expression Γ t → Expression Γ t → Expression Γ t
 
   data CanAssign {n} {Γ} where
-    state : ∀ i {i<o : True (i ℕ.<? o)} → CanAssign (state i {i<o})
-    var   : ∀ i {i<n : True (i ℕ.<? n)} → CanAssign (var i {i<n})
+    state : ∀ i → CanAssign (state i)
+    var   : ∀ i → CanAssign (var i)
     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 Γ (elemType t)} → CanAssign e → CanAssign ([_] {t = t} e)
@@ -205,7 +205,7 @@ module Code {o} (Σ : Vec Type o) where
   canAssignAll? (e ∷ es) = map′ (uncurry _∷_) (λ { (e ∷ es) → e , es }) (canAssign? e ×-dec canAssignAll? es)
 
   data AssignsState where
-    state : ∀ i {i<o} → AssignsState (state i {i<o})
+    state : ∀ i → AssignsState (state i)
     _∶ˡ_ : ∀ {m n t e₁ e₂ a₁} → AssignsState a₁ → ∀ a₂ → AssignsState (_∶_ {m = m} {n} {t} {e₁} {e₂} a₁ a₂)
     _∶ʳ_ : ∀ {m n t e₁ e₂} a₁ {a₂} → AssignsState a₂ → AssignsState (_∶_ {m = m} {n} {t} {e₁} {e₂} a₁ a₂)
     [_] : ∀ {t e a} → AssignsState a → AssignsState ([_] {t = t} {e} a)
diff --git a/src/Helium/Instructions/Base.agda b/src/Helium/Instructions/Base.agda
index 3261107..0a0e01f 100644
--- a/src/Helium/Instructions/Base.agda
+++ b/src/Helium/Instructions/Base.agda
@@ -10,6 +10,7 @@ module Helium.Instructions.Base where
 
 open import Data.Bool as Bool using (true; false)
 open import Data.Fin as Fin using (Fin; Fin′; zero; suc; toℕ)
+open import Data.Fin.Patterns
 open import Data.Nat as ℕ using (ℕ; zero; suc)
 import Data.Nat.Properties as ℕₚ
 open import Data.Sum using ([_,_]′; inj₂)
@@ -49,25 +50,25 @@ open Core.Code State public
 -- Direct from State
 
 S : ∀ {n Γ} → Expression {n} Γ (array (bits 32) 32)
-S = state 0
+S = state 0F
 
 R : ∀ {n Γ} → Expression {n} Γ (array (bits 32) 16)
-R = state 1
+R = state 1F
 
 VPR-P0 : ∀ {n Γ} → Expression {n} Γ (bits 16)
-VPR-P0 = state 2
+VPR-P0 = state 2F
 
 VPR-mask : ∀ {n Γ} → Expression {n} Γ (bits 8)
-VPR-mask = state 3
+VPR-mask = state 3F
 
 FPSCR-QC : ∀ {n Γ} → Expression {n} Γ bit
-FPSCR-QC = state 4
+FPSCR-QC = state 4F
 
 AdvanceVPTState : ∀ {n Γ} → Expression {n} Γ bool
-AdvanceVPTState = state 5
+AdvanceVPTState = state 5F
 
 BeatId : ∀ {n Γ} → Expression {n} Γ beat
-BeatId = state 6
+BeatId = state 6F
 
 -- Indirect
 
@@ -106,30 +107,30 @@ sliceⁱ {m = suc m} n i = sliceⁱ (suc n) i ∶ [ get n i ]
 --- Functions
 
 Int : ∀ {n} → Function (bits n ∷ bool ∷ []) int
-Int = skip ∙return (if var 1 then uint (var 0) else sint (var 0))
+Int = skip ∙return (if var 1F then uint (var 0F) else sint (var 0F))
 
 -- arguments swapped, pred n
 SignedSatQ : ∀ n → Function (int ∷ []) (tuple 2 (bits (suc n) ∷ bool ∷ []))
 SignedSatQ n = declare (lit (true ′b)) (
-  if max <? var 1
+  if max <? var 1F
   then
-    var 1 ≔ max
-  else if var 1 <? min
+    var 1F ≔ max
+  else if var 1F <? min
   then
-    var 1 ≔ min
+    var 1F ≔ min
   else
-    var 0 ≔ lit (false ′b)
-  ∙return tup (sliceⁱ 0 (var 1) ∷ var 0 ∷ []))
+    var 0F ≔ lit (false ′b)
+  ∙return tup (sliceⁱ 0 (var 1F) ∷ var 0F ∷ []))
   where
   max = lit (2 ′i) ^ n + - lit (1 ′i)
   min = - (lit (2 ′i) ^ n)
 
 -- 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) ′xs))
+LSL-C {n} shift = declare (var 0F ∶ lit ((Vec.replicate {n = (suc shift)} false) ′xs))
   (skip ∙return tup
-    ( slice (var 0) (lit (zero ′f))
-    ∷ unbox (slice (cast eq (var 0)) (lit (Fin.inject+ shift (Fin.fromℕ n) ′f)))
+    ( slice (var 0F) (lit (zero ′f))
+    ∷ unbox (slice (cast eq (var 0F)) (lit (Fin.inject+ shift (Fin.fromℕ n) ′f)))
     ∷ []))
   where
   eq = P.trans (ℕₚ.+-comm 1 (shift ℕ.+ n)) (P.cong (ℕ._+ 1) (ℕₚ.+-comm shift n))
@@ -145,46 +146,46 @@ private
 copyMasked : Procedure (fin 8 ∷ bits 32 ∷ beat ∷ elmtMask ∷ [])
 copyMasked = for 4
   -- 0:e 1:dest 2:result 3:beat 4:elmtMask
-  ( if hasBit (var 4) (var 0)
+  ( if hasBit (var 4F) (var 0F)
     then
-      elem 8 (index (index Q (var 1)) (var 3)) (var 0) ≔ elem 8 (var 2) (var 0)
+      elem 8 (index (index Q (var 1F)) (var 3F)) (var 0F) ≔ elem 8 (var 2F) (var 0F)
     else skip
   ) ∙end
 
 VPTAdvance : Procedure (beat ∷ [])
-VPTAdvance = declare (fin div2 (tup (var 0 ∷ []))) (
-  declare (elem 4 VPR-mask (var 0)) (
+VPTAdvance = declare (fin div2 (tup (var 0F ∷ []))) (
+  declare (elem 4 VPR-mask (var 0F)) (
     -- 0:vptState 1:maskId 2:beat
-    if var 0 ≟ lit ((true ∷ false ∷ false ∷ false ∷ []) ′xs)
+    if var 0F ≟ lit ((true ∷ false ∷ false ∷ false ∷ []) ′xs)
     then
-      var 0 ≔ lit (Vec.replicate false ′xs)
-    else if inv (var 0 ≟ lit (Vec.replicate false ′xs))
+      var 0F ≔ lit (Vec.replicate false ′xs)
+    else if inv (var 0F ≟ lit (Vec.replicate false ′xs))
     then (
       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)
+        tup (var 1F ∷ var 0F ∷ []) ≔ call (LSL-C 0) (var 1F ∷ []) ∙
+        if var 0F ≟ lit (true ′x)
         then
-          elem 4 VPR-P0 (var 3) ≔ not (elem 4 VPR-P0 (var 3))
+          elem 4 VPR-P0 (var 3F) ≔ not (elem 4 VPR-P0 (var 3F))
         else skip))
     else skip ∙
-    if get 0 (asInt (var 2)) ≟ lit (true ′x)
+    if get 0 (asInt (var 2F)) ≟ lit (true ′x)
     then
-      elem 4 VPR-mask (var 1) ≔ var 0
+      elem 4 VPR-mask (var 1F) ≔ var 0F
     else skip))
     ∙end
 
 VPTActive : Function (beat ∷ []) bool
-VPTActive = skip ∙return inv (elem 4 VPR-mask (fin div2 (tup (var 0 ∷ []))) ≟ lit (Vec.replicate false ′xs))
+VPTActive = skip ∙return inv (elem 4 VPR-mask (fin div2 (tup (var 0F ∷ []))) ≟ lit (Vec.replicate false ′xs))
 
 GetCurInstrBeat : Function [] (tuple 2 (beat ∷ elmtMask ∷ []))
 GetCurInstrBeat = declare (lit (Vec.replicate true ′xs)) (
   -- 0:elmtMask 1:beat
   if call VPTActive (BeatId ∷ [])
   then
-    var 0 ≔ var 0 and elem 4 VPR-P0 BeatId
+    var 0F ≔ var 0F and elem 4 VPR-P0 BeatId
   else skip
-  ∙return tup (BeatId ∷ var 0 ∷ []))
+  ∙return tup (BeatId ∷ var 0F ∷ []))
 
 -- Assumes:
 --   MAX_OVERLAPPING_INSTRS = 1
@@ -196,12 +197,12 @@ ExecBeats : Procedure [] → Procedure []
 ExecBeats DecodeExec =
   for 4 (
     -- 0:beatId
-    BeatId ≔ var 0 ∙
+    BeatId ≔ var 0F ∙
     AdvanceVPTState ≔ lit (true ′b) ∙
     invoke DecodeExec [] ∙
     if AdvanceVPTState
     then
-      invoke VPTAdvance (var 0 ∷ [])
+      invoke VPTAdvance (var 0F ∷ [])
     else skip)
   ∙end
 
@@ -223,51 +224,51 @@ module _ (d : Instr.VecOp₂) where
   vec-op₂′ op = declare (lit (zero ′f)) (
     declare (lit (Vec.replicate false ′xs)) (
     -- 0:elmtMask 1:curBeat
-    tup (var 1 ∷ var 0 ∷ []) ≔ call GetCurInstrBeat [] ∙
+    tup (var 1F ∷ var 0F ∷ []) ≔ call GetCurInstrBeat [] ∙
     declare (lit ((Vec.replicate false ′xs) ′a)) (
-    declare (from32 size (index (index Q (lit (src₁ ′f))) (var 2))) (
+    declare (from32 size (index (index Q (lit (src₁ ′f))) (var 2F))) (
     -- 0:op₁ 1:result 2:elmtMask 3:curBeat
     for (toℕ elements) (
        -- 0:e 1:op₁ 2:result 3:elmtMask 4:curBeat
       declare op₂ op ) ∙
     -- 0:op₁ 1:result 2:elmtMask 3:curBeat
-    invoke copyMasked (lit (dest ′f) ∷ to32 size (var 1) ∷ var 3 ∷ var 2 ∷ [])))))
+    invoke copyMasked (lit (dest ′f) ∷ to32 size (var 1F) ∷ var 3F ∷ var 2F ∷ [])))))
     ∙end
     where
     -- 0:e 1:op₁ 2:result 3:elmtMask 4:curBeat
     op₂ =
       [ (λ src₂ → index (from32 size (index R (lit (src₂ ′f)))) (lit (zero ′f)))
-      , (λ src₂ → index (from32 size (index (index Q (lit (src₂ ′f))) (var 4))) (var 0))
+      , (λ src₂ → index (from32 size (index (index Q (lit (src₂ ′f))) (var 4F))) (var 0F))
       ]′ src₂
 
   vec-op₂ : Function (bits (toℕ esize) ∷ bits (toℕ esize) ∷ []) (bits (toℕ esize)) → Procedure []
-  vec-op₂ op = vec-op₂′ (index (var 3) (var 1) ≔ call op (index (var 2) (var 1) ∷ var 0 ∷ []))
+  vec-op₂ op = vec-op₂′ (index (var 3F) (var 1F) ≔ call op (index (var 2F) (var 1F) ∷ var 0F ∷ []))
 
 vadd : Instr.VAdd → Procedure []
-vadd d = vec-op₂ d (skip ∙return sliceⁱ 0 (uint (var 0) + uint (var 1)))
+vadd d = vec-op₂ d (skip ∙return sliceⁱ 0 (uint (var 0F) + uint (var 1F)))
 
 vsub : Instr.VSub → Procedure []
-vsub d = vec-op₂ d (skip ∙return sliceⁱ 0 (uint (var 0) - uint (var 1)))
+vsub d = vec-op₂ d (skip ∙return sliceⁱ 0 (uint (var 0F) - uint (var 1F)))
 
 vhsub : Instr.VHSub → Procedure []
-vhsub d = vec-op₂ op₂ (skip ∙return sliceⁱ 1 (toInt (var 0) - toInt (var 1)))
+vhsub d = vec-op₂ op₂ (skip ∙return sliceⁱ 1 (toInt (var 0F) - toInt (var 1F)))
   where open Instr.VHSub d; toInt = λ i → call Int (i ∷ lit (unsigned ′b) ∷ [])
 
 vmul : Instr.VMul → Procedure []
-vmul d = vec-op₂ d (skip ∙return sliceⁱ 0 (sint (var 0) * sint (var 1)))
+vmul d = vec-op₂ d (skip ∙return sliceⁱ 0 (sint (var 0F) * sint (var 1F)))
 
 vmulh : Instr.VMulH → Procedure []
-vmulh d = vec-op₂ op₂ (skip ∙return sliceⁱ (toℕ esize) (toInt (var 0) * toInt (var 1)))
+vmulh d = vec-op₂ op₂ (skip ∙return sliceⁱ (toℕ esize) (toInt (var 0F) * toInt (var 1F)))
   where
   open Instr.VMulH d; toInt = λ i → call Int (i ∷ lit (unsigned ′b) ∷ [])
 
 vrmulh : Instr.VRMulH → Procedure []
-vrmulh d = vec-op₂ op₂ (skip ∙return sliceⁱ (toℕ esize) (toInt (var 0) * toInt (var 1) + lit (1 ′i) << toℕ esize-1))
+vrmulh d = vec-op₂ op₂ (skip ∙return sliceⁱ (toℕ esize) (toInt (var 0F) * toInt (var 1F) + lit (1 ′i) << toℕ esize-1))
   where
   open Instr.VRMulH d; toInt = λ i → call Int (i ∷ lit (unsigned ′b) ∷ [])
 
 vmla : Instr.VMlA → Procedure []
-vmla d = vec-op₂ op₂ (skip ∙return sliceⁱ (toℕ esize) (toInt (var 0) * element₂ + toInt (var 1)))
+vmla d = vec-op₂ op₂ (skip ∙return sliceⁱ (toℕ esize) (toInt (var 0F) * element₂ + toInt (var 1F)))
   where
   open Instr.VMlA d
   op₂ = record { size = size ; dest = acc ; src₁ = src₁ ; src₂ = inj₂ acc }
@@ -278,11 +279,11 @@ private
   vqr?dmulh : Instr.VQDMulH → Function (int ∷ int ∷ []) int → Procedure []
   vqr?dmulh d f = vec-op₂′ d (
     -- 0:op₂ 1:e 2:op₁ 3:result 4:elmtMask 5:curBeat
-    declare (call f (sint (index (var 2) (var 1)) ∷ sint (var 0) ∷ [])) (
+    declare (call f (sint (index (var 2F) (var 1F)) ∷ sint (var 0F) ∷ [])) (
     declare (lit (false ′b)) (
       -- 0:sat 1:value 2:op₂ 3:e 4:op₁ 5:result 6:elmtMask 7:curBeat
-      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) ∷ [])))
+      tup (index (var 5F) (var 3F) ∷ var 0F ∷ []) ≔ call (SignedSatQ (toℕ esize-1)) (var 1F ∷ []) ∙
+      if var 0F && hasBit (var 6F) (fin e*esize>>3 (tup ((var 3F) ∷ [])))
       then
         FPSCR-QC ≔ lit (true ′x)
       else skip)))
@@ -298,9 +299,9 @@ private
       helper Instr.32bit i = Fin.combine i zero
 
 vqdmulh : Instr.VQDMulH → Procedure []
-vqdmulh d = vqr?dmulh d (skip ∙return lit (2 ′i) * var 0 * var 1 >> toℕ esize)
+vqdmulh d = vqr?dmulh d (skip ∙return lit (2 ′i) * var 0F * var 1F >> toℕ esize)
   where open Instr.VecOp₂ d using (esize)
 
 vqrdmulh : Instr.VQRDMulH → Procedure []
-vqrdmulh d = vqr?dmulh d (skip ∙return lit (2 ′i) * var 0 * var 1 + lit (1 ′i) << toℕ esize-1 >> toℕ esize)
+vqrdmulh d = vqr?dmulh d (skip ∙return lit (2 ′i) * var 0F * var 1F + lit (1 ′i) << toℕ esize-1 >> toℕ esize)
   where open Instr.VecOp₂ d using (esize; esize-1)
diff --git a/src/Helium/Semantics/Denotational/Core.agda b/src/Helium/Semantics/Denotational/Core.agda
index 46d68bc..4897b61 100644
--- a/src/Helium/Semantics/Denotational/Core.agda
+++ b/src/Helium/Semantics/Denotational/Core.agda
@@ -17,7 +17,7 @@ private
   open module C = RawPseudocode rawPseudocode
 
 open import Data.Bool as Bool using (Bool; true; false)
-open import Data.Fin as Fin using (Fin; zero; suc; #_)
+open import Data.Fin as Fin using (Fin; zero; suc)
 import Data.Fin.Properties as Finₚ
 open import Data.Nat as ℕ using (ℕ; zero; suc)
 import Data.Nat.Properties as ℕₚ
@@ -201,8 +201,8 @@ module Expression
   update : ∀ {n Γ t e} → CanAssign {n} {Γ} {t} e → ⟦ t ⟧ₜ → ⟦ Σ ⟧ₜ′ → ⟦ Γ ⟧ₜ′ → ⟦ Σ ⟧ₜ′ × ⟦ Γ ⟧ₜ′
 
   ⟦ lit x ⟧ᵉ σ γ = 𝒦 x
-  ⟦ state i ⟧ᵉ σ γ = fetch Σ σ (# i)
-  ⟦_⟧ᵉ {Γ = Γ} (var i) σ γ = fetch Γ γ (# i)
+  ⟦ state i ⟧ᵉ σ γ = fetch Σ σ i
+  ⟦_⟧ᵉ {Γ = Γ} (var i) σ γ = fetch Γ γ i
   ⟦ abort e ⟧ᵉ σ γ = case ⟦ e ⟧ᵉ σ γ of λ ()
   ⟦ _≟_ {hasEquality = hasEq} e e₁ ⟧ᵉ σ γ = equal (toWitness hasEq) (⟦ e ⟧ᵉ σ γ) (⟦ e₁ ⟧ᵉ σ γ)
   ⟦ _<?_ {isNumeric = isNum} e e₁ ⟧ᵉ σ γ = comp (toWitness isNum) (⟦ e ⟧ᵉ σ γ) (⟦ e₁ ⟧ᵉ σ γ)
@@ -263,8 +263,8 @@ module Expression
 
   ⟦ s ∙end ⟧ᵖ σ γ = P.proj₁ (⟦ s ⟧ˢ σ γ)
 
-  update (state i {i<o}) v σ γ = updateAt Σ (#_ i {m<n = i<o}) v σ , γ
-  update {Γ = Γ} (var i {i<n}) v σ γ = σ , updateAt Γ (#_ i {m<n = i<n}) v γ
+  update (state i) v σ γ = updateAt Σ i v σ , γ
+  update {Γ = Γ} (var i) v σ γ = σ , updateAt Γ i v γ
   update abort v σ γ = σ , γ
   update (_∶_ {m = m} {t = t} e e₁) v σ γ = do
     let σ′ , γ′ = update e (sliced t v (Fin.fromℕ _)) σ γ
-- 
cgit v1.2.3