Add if_then_ statements

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