diff options
Diffstat (limited to 'src')
| -rw-r--r-- | src/Helium/Data/Pseudocode/Core.agda | 5 | ||||
| -rw-r--r-- | src/Helium/Instructions/Base.agda | 15 | ||||
| -rw-r--r-- | src/Helium/Semantics/Denotational/Core.agda | 1 |
3 files changed, 9 insertions, 12 deletions
diff --git a/src/Helium/Data/Pseudocode/Core.agda b/src/Helium/Data/Pseudocode/Core.agda index 4e57f17..79e34a2 100644 --- a/src/Helium/Data/Pseudocode/Core.agda +++ b/src/Helium/Data/Pseudocode/Core.agda @@ -255,7 +255,7 @@ module Code {o} (Σ : Vec Type o) where referencesState? (if e then e₁ else e₂) = no λ () infix 4 _≔_ - infixl 2 if_then_else_ + infixl 2 if_then_else_ if_then_ infixl 1 _∙_ _∙return_ infix 1 _∙end @@ -266,6 +266,7 @@ module Code {o} (Σ : Vec Type o) where declare : ∀ {t} → Expression Γ t → Statement (t ∷ Γ) → Statement Γ invoke : ∀ {m Δ} → Procedure Δ → All (Expression Γ) {m} Δ → Statement Γ if_then_else_ : Expression Γ bool → Statement Γ → Statement Γ → Statement Γ + if_then_ : Expression Γ bool → Statement Γ → Statement Γ for : ∀ m → Statement (fin m ∷ Γ) → Statement Γ data ChangesState where @@ -274,6 +275,7 @@ module Code {o} (Σ : Vec Type o) where _≔_ : ∀ {t} ref {canAssign : True (canAssign? ref)} {refsState : True (referencesState? ref)} e₂ → ChangesState (_≔_ {t = t} ref {canAssign} e₂) declare : ∀ {t} e {s} → ChangesState s → ChangesState (declare {t = t} e s) invoke : ∀ {m Δ} p es → ChangesState (invoke {m = m} {Δ} p es) + if_then_ : ∀ e {s} → ChangesState s → ChangesState (if e then s) if_then′_else_ : ∀ e {s} → ChangesState s → ∀ s₁ → ChangesState (if e then s else s₁) if_then_else′_ : ∀ e s {s₁} → ChangesState s₁ → ChangesState (if e then s else s₁) for : ∀ m {s} → ChangesState s → ChangesState (for m s) @@ -283,6 +285,7 @@ module Code {o} (Σ : Vec Type o) where changesState? (_≔_ ref e) = map′ (λ refsState → _≔_ ref {refsState = fromWitness refsState} e) (λ { (_≔_ ref {refsState = refsState} e) → toWitness refsState }) (referencesState? ref) changesState? (declare e s) = map′ (declare e) (λ { (declare e s) → s }) (changesState? s) changesState? (invoke p e) = yes (invoke p e) + changesState? (if e then s) = map′ (if e then_) (λ { (if e then s) → s }) (changesState? s) changesState? (if e then s else s₁) = map′ [ if e then′_else s₁ , if e then s else′_ ]′ (λ { (if e then′ s else s₁) → inj₁ s ; (if e then s else′ s₁) → inj₂ s₁ }) (changesState? s ⊎-dec changesState? s₁) changesState? (for m s) = map′ (for m) (λ { (for m s) → s }) (changesState? s) diff --git a/src/Helium/Instructions/Base.agda b/src/Helium/Instructions/Base.agda index 0a0e01f..d157d5a 100644 --- a/src/Helium/Instructions/Base.agda +++ b/src/Helium/Instructions/Base.agda @@ -149,7 +149,6 @@ copyMasked = for 4 ( if hasBit (var 4F) (var 0F) then elem 8 (index (index Q (var 1F)) (var 3F)) (var 0F) ≔ elem 8 (var 2F) (var 0F) - else skip ) ∙end VPTAdvance : Procedure (beat ∷ []) @@ -166,13 +165,10 @@ VPTAdvance = declare (fin div2 (tup (var 0F ∷ []))) ( tup (var 1F ∷ var 0F ∷ []) ≔ call (LSL-C 0) (var 1F ∷ []) ∙ if var 0F ≟ lit (true ′x) then - elem 4 VPR-P0 (var 3F) ≔ not (elem 4 VPR-P0 (var 3F)) - else skip)) - else skip ∙ + elem 4 VPR-P0 (var 3F) ≔ not (elem 4 VPR-P0 (var 3F)))) ∙ if get 0 (asInt (var 2F)) ≟ lit (true ′x) then - elem 4 VPR-mask (var 1F) ≔ var 0F - else skip)) + elem 4 VPR-mask (var 1F) ≔ var 0F)) ∙end VPTActive : Function (beat ∷ []) bool @@ -184,7 +180,6 @@ GetCurInstrBeat = declare (lit (Vec.replicate true ′xs)) ( if call VPTActive (BeatId ∷ []) then var 0F ≔ var 0F and elem 4 VPR-P0 BeatId - else skip ∙return tup (BeatId ∷ var 0F ∷ [])) -- Assumes: @@ -202,8 +197,7 @@ ExecBeats DecodeExec = invoke DecodeExec [] ∙ if AdvanceVPTState then - invoke VPTAdvance (var 0F ∷ []) - else skip) + invoke VPTAdvance (var 0F ∷ [])) ∙end from32 : ∀ size {n Γ} → Expression {n} Γ (bits 32) → Expression Γ (array (bits (toℕ (Instr.Size.esize size))) (toℕ (Instr.Size.elements size))) @@ -285,8 +279,7 @@ private 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))) + FPSCR-QC ≔ lit (true ′x)))) where open Instr.VecOp₂ d diff --git a/src/Helium/Semantics/Denotational/Core.agda b/src/Helium/Semantics/Denotational/Core.agda index df16874..e605439 100644 --- a/src/Helium/Semantics/Denotational/Core.agda +++ b/src/Helium/Semantics/Denotational/Core.agda @@ -260,6 +260,7 @@ module Expression ⟦ _≔_ ref {canAssign = canAssign} e ⟧ˢ σ γ = update (toWitness canAssign) (⟦ e ⟧ᵉ σ γ) σ γ ⟦_⟧ˢ {Γ = Γ} (declare e s) σ γ = P.map₂ (tupTail Γ) (⟦ s ⟧ˢ σ (tupCons Γ (⟦ e ⟧ᵉ σ γ) γ)) ⟦ invoke p e ⟧ˢ σ γ = ⟦ p ⟧ᵖ σ (⟦ e ⟧ᵉ′ σ γ) , γ + ⟦ if e then s₁ ⟧ˢ σ γ = Bool.if ⟦ e ⟧ᵉ σ γ then ⟦ s₁ ⟧ˢ σ γ else (σ , γ) ⟦ if e then s₁ else s₂ ⟧ˢ σ γ = Bool.if ⟦ e ⟧ᵉ σ γ then ⟦ s₁ ⟧ˢ σ γ else ⟦ s₂ ⟧ˢ σ γ ⟦_⟧ˢ {Γ = Γ} (for m s) σ γ = helper m ⟦ s ⟧ˢ σ γ where |