Remade quicksort demo to be much larger

demo/quicksort.crf

@@ -1,3 +1,4 @@
+
 filter : (a -> Bool) -> List a -> List a
 filter p xs = case xs of
     Nil => Nil
@@ -12,6 +13,10 @@ quicksort xs = case xs of
                  let bigger = quicksort (filter (\y. a < y) xs) in
                  smaller ++ (Cons a bigger)
 
--- [5, 2, 8, 9, 6, 0, 1]
+mkDescList : Int -> Int -> List Int
-main = let list = Cons 5 (Cons 2 (Cons 8 (Cons 9 (Cons 6 (Cons 0 (Cons 1 Nil)))))) in 
+mkDescList from to = case from == to of
-       printList (quicksort list)
+    True => Nil
+    False => Cons from (mkDescList (from - 1) to)    
+    
+main = printList (quicksort (mkDescList 1000 0))
+

src/Codegen/Emits.hs

@@ -381,7 +381,7 @@ preludeFuns def xs arg1 arg2 = case xs of
   "$minus$$Int_Int_Int"   -> pure $ Sub I64 arg1 arg2
   "$plus$$Int_Int_Int"    -> pure $ Add I64 arg1 arg2
   "printChar$Char_Unit"   -> pure . UnsafeRaw $ "add i16 0,0\n    call void (ptr, ...) @printf(ptr noundef @.char_print_no_nl, i8 noundef " <> toIr arg1 <> ")\n"
-  "printInt$Int_Unit"     -> pure . UnsafeRaw $ "add i16 0,0\n    call void (ptr, ...) @printf(ptr noundef @.int_print_no_nl, i8 noundef " <> toIr arg1 <> ")\n"
+  "printInt$Int_Unit"     -> pure . UnsafeRaw $ "add i16 0,0\n    call void (ptr, ...) @printf(ptr noundef @.int_print_no_nl, i64 noundef " <> toIr arg1 <> ")\n"
   _                       -> pure def
 
 -- | Emits a function call.

src/Main.hs

@@ -233,6 +233,9 @@ prelude =
         , "    Nil => Unit"
         , "    Cons x xs => flipConst (printChar x) (printStr xs)"
         , "\n"
+        , "printInt : Int -> Unit"
+        , "printInt xs = Unit"
+        , "\n"
         , "asciiCode : Char -> Int"
         , "asciiCode x = case x of { 'a' => 97; 'b' => 98; 'c' => 99; 'd' => 100; 'e' => 101; 'f' => 102; 'g' => 103; 'h' => 104; 'i' => 105; 'j' => 106; 'k' => 107; 'l' => 108; 'm' => 109; 'n' => 110; 'o' => 111; 'p' => 112; 'q' => 113; 's' => 114; 't' => 115; 'u' => 116; 'v' => 117; 'w' => 118; 'x' => 119; 'y' => 120; 'z' => 121; }"
         , "toChar : Int -> Char"
@@ -243,19 +246,6 @@ prelude =
         , "    Cons a as => Cons (toChar a) (toStr as)"
         , "    Nil => Nil"
         , "\n"
-        , "interleave : Char -> List Char -> List Char"
-        , "interleave c ls = case ls of"
-        , "    Nil => Nil"
-        , "    Cons a as => case as of"
-        , "        Nil => Cons a Nil"
-        , "        Cons y ys => Cons a (Cons c (interleave c as))"
-        , "\n"
-        , "bracketify : List Char -> List Char"
-        , "bracketify xs = Cons '[' (xs ++ (Cons ']' Nil))"
-        , "\n"
-        , "printList : List Int -> Unit"
-        , "printList xs = printStr (bracketify (interleave ',' (toStr xs)))"
-        , "\n"
         , ".++ : List a -> List a -> List a"
         , ".++ as bs = case as of"
         , "    Nil => bs"
@@ -267,4 +257,18 @@ prelude =
         , "\n"
         , "data Pair a b where"
         , "  Pair : a -> b -> Pair a b"
+        , "\n"
+        , "printListH : List Int -> Unit"
+        , "printListH xs = case xs of"
+        , "    Cons a as => flipConst (printInt a) (printListHH as)"
+        , "    Nil => Unit"
+        , "\n"
+        , "printListHH : List Int -> Unit"
+        , "printListHH xs = case xs of"
+        , "    Nil => Unit"
+        , "    Cons a as => flipConst (printChar ',') (flipConst (printInt a) (printListHH as))"
+        , "\n"
+        , "printList : List Int -> Unit"
+        , "printList xs = case Cons (printChar '[') (Cons (printListH xs) (Cons (printChar ']') Nil)) of"
+        , "        _ => Unit"
         ]