diff options
Diffstat (limited to 'src/Helium/Data/Pseudocode/Core.agda')
| -rw-r--r-- | src/Helium/Data/Pseudocode/Core.agda | 10 |
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 |