Add predicate for being a sliced type.

1 files changed, 10 insertions, 0 deletions

diff --git a/src/Helium/Data/Pseudocode/Core.agda b/src/Helium/Data/Pseudocode/Core.agda
index 6ae1d34..d683947 100644
--- a/src/Helium/Data/Pseudocode/Core.agda
+++ b/src/Helium/Data/Pseudocode/Core.agda
@@ -81,6 +81,16 @@ asType : Sliced → ℕ → Type
 asType bits      n = bits n
 asType (array t) n = array t n
 
+sliced? : ∀ t → Dec (∃ λ t′ → ∃ λ n → asType t′ n ≡ t)
+sliced? bool = no (λ { (bits , ()) ; (array _ , ()) })
+sliced? int = no (λ { (bits , ()) ; (array _ , ()) })
+sliced? (fin n) = no (λ { (bits , ()) ; (array _ , ()) })
+sliced? real = no (λ { (bits , ()) ; (array _ , ()) })
+sliced? bit = no (λ { (bits , ()) ; (array _ , ()) })
+sliced? (bits n) = yes (bits , n , refl)
+sliced? (tuple n x) = no (λ { (bits , ()) ; (array _ , ()) })
+sliced? (array t n) = yes (array t , n , refl)
+
 elemType : Sliced → Type
 elemType bits      = bit
 elemType (array t) = t