[ re #155 ] Add vecToList + vector reverse examples to CompileTo.agda

Author: jespercockx

test/CompileTo.agda

@@ -23,11 +23,18 @@ listToVec (x ∷ xs) = x ∷ listToVec xs
 
 {-# COMPILE AGDA2HS listToVec transparent #-}
 
+vecToList : Vec a n → List a
+vecToList [] = []
+vecToList (x ∷ xs) = x ∷ vecToList xs
+
+{-# COMPILE AGDA2HS vecToList transparent #-}
+
 test2 : Vec Int 3
-test2 = listToVec (map (_+ 1) (1 ∷ 2 ∷ 3 ∷ []))
+test2 = listToVec (map (_+ 1) (vecToList (1 ∷ 2 ∷ 3 ∷ [])))
 
 {-# COMPILE AGDA2HS test2 #-}
 
+-- Not using `length` since compile-to is not yet compatible with type classes
 llength : List a → Nat
 llength [] = 0
 llength (x ∷ xs) = 1 + llength xs
@@ -46,3 +53,20 @@ test3 : ∃ Nat (_≡ 3)
 test3 = vlength test1
 
 {-# COMPILE AGDA2HS test3 #-}
+
+lfoldl : (b → a → b) → b → List a → b
+lfoldl f v [] = v
+lfoldl f v (x ∷ xs) = lfoldl f (f v x) xs
+
+{-# COMPILE AGDA2HS lfoldl #-}
+
+vfoldl : (b : @0 Nat → Set) → (∀ {@0 n} → b n → a → b (suc n)) → b 0 → Vec a n → b n
+vfoldl b f v [] = v
+vfoldl b f v (x ∷ xs) = vfoldl (λ n → b (suc n)) f (f v x) xs
+
+{-# COMPILE AGDA2HS vfoldl to lfoldl #-}
+
+vreverse : Vec a n → Vec a n
+vreverse {a = a} = vfoldl (Vec a) (λ xs x → x ∷ xs) []
+
+{-# COMPILE AGDA2HS vreverse #-}

test/golden/CompileTo.hs

@@ -15,3 +15,10 @@ llength (x : xs) = 1 + llength xs
 test3 :: Natural
 test3 = llength test1
 
+lfoldl :: (b -> a -> b) -> b -> [a] -> b
+lfoldl f v [] = v
+lfoldl f v (x : xs) = lfoldl f (f v x) xs
+
+vreverse :: [a] -> [a]
+vreverse = lfoldl (\ xs x -> x : xs) []
+