Add a transform rule making (++) for List tail-recursive. (#1888)

Author: falsifian

libs/base/Data/List.idr

@@ -346,15 +346,6 @@ public export
 replaceOn : Eq a => a -> a -> List a -> List a
 replaceOn a = replaceWhen (== a)
 
-public export
-reverseOnto : List a -> List a -> List a
-reverseOnto acc [] = acc
-reverseOnto acc (x::xs) = reverseOnto (x::acc) xs
-
-public export
-reverse : List a -> List a
-reverse = reverseOnto []
-
 ||| Construct a list with `n` copies of `x`.
 ||| @ n how many copies
 ||| @ x the element to replicate
@@ -739,6 +730,36 @@ consInjective : forall x, xs, y, ys .
                 the (List a) (x :: xs) = the (List b) (y :: ys) -> (x = y, xs = ys)
 consInjective Refl = (Refl, Refl)
 
+reverseReverseOnto : (l, r : List a) -> reverse (reverseOnto l r) = reverseOnto r l
+reverseReverseOnto _ [] = Refl
+reverseReverseOnto l (x :: xs) = reverseReverseOnto (x :: l) xs
+
+||| List reverse applied twice yields the identity function.
+export
+reverseInvolutive : (xs : List a) -> reverse (reverse xs) = xs
+reverseInvolutive = reverseReverseOnto []
+
+consReverse : (x : a) -> (l, r : List a) -> x :: reverseOnto r l = reverseOnto r (reverseOnto [x] (reverse l))
+consReverse _ [] _ = Refl
+consReverse x (y::ys) r
+  = rewrite consReverse x ys (y :: r) in
+      rewrite cong (reverseOnto r . reverse) $ consReverse x ys [y] in
+        rewrite reverseInvolutive (y :: reverseOnto [x] (reverse ys)) in
+          Refl
+
+consTailRecAppend : (x : a) -> (l, r : List a) -> tailRecAppend (x :: l) r = x :: (tailRecAppend l r)
+consTailRecAppend x l r
+  = rewrite consReverse x (reverse l) r in
+      rewrite reverseInvolutive l in
+        Refl
+
+||| Proof that `(++)` and `tailRecAppend` do the same thing, so the %transform
+||| directive is safe.
+tailRecAppendIsAppend : (xs, ys : List a) -> tailRecAppend xs ys = xs ++ ys
+tailRecAppendIsAppend [] ys = Refl
+tailRecAppendIsAppend (x::xs) ys =
+  trans (consTailRecAppend x xs ys) (cong (x ::) $ tailRecAppendIsAppend xs ys)
+
 ||| The empty list is a right identity for append.
 export
 appendNilRightNeutral : (l : List a) -> l ++ [] = l
@@ -768,14 +789,6 @@ revAppend (v :: vs) ns
             rewrite appendAssociative (reverse ns) (reverse vs) [v] in
               Refl
 
-||| List reverse applied twice yields the identity function.
-export
-reverseInvolutive : (xs : List a) -> reverse (reverse xs) = xs
-reverseInvolutive [] = Refl
-reverseInvolutive (x :: xs) = rewrite revOnto [x] xs in
-                                rewrite sym (revAppend (reverse xs) [x]) in
-                                  cong (x ::) $ reverseInvolutive xs
-
 export
 dropFusion : (n, m : Nat) -> (l : List t) -> drop n (drop m l) = drop (n+m) l
 dropFusion  Z     m    l      = Refl

libs/prelude/Prelude/Types.idr

@@ -389,6 +389,26 @@ namespace List
   length []        = Z
   length (x :: xs) = S (length xs)
 
+  public export
+  reverseOnto : List a -> List a -> List a
+  reverseOnto acc [] = acc
+  reverseOnto acc (x::xs) = reverseOnto (x::acc) xs
+
+  public export
+  reverse : List a -> List a
+  reverse = reverseOnto []
+
+  ||| Tail-recursive append. Uses of (++) are automatically transformed to
+  ||| this. The only reason this is exported is that the proof of equivalence
+  ||| lives in a different module.
+  public export
+  tailRecAppend : (xs, ys : List a) -> List a
+  tailRecAppend xs ys = reverseOnto ys (reverse xs)
+
+  -- Always use tailRecAppend at runtime. Data.List.tailRecAppendIsAppend
+  -- proves these are equivalent.
+  %transform "tailRecAppend" (++) = tailRecAppend
+
 public export
 Functor List where
   map f [] = []

tests/Main.idr

@@ -271,6 +271,7 @@ nodeTests = MkTestPool "Node backend" [] (Just Node)
     , "idiom001"
     , "integers"
     , "fix1839"
+    , "tailrec_libs"
     ]
 
 vmcodeInterpTests : IO TestPool

tests/node/tailrec_libs/expected

@@ -0,0 +1 @@
+10001

tests/node/tailrec_libs/run

@@ -0,0 +1,3 @@
+rm -rf build
+
+$1 --cg node --no-banner --no-color --console-width 0 tailrec.idr -x main

tests/node/tailrec_libs/tailrec.idr

@@ -0,0 +1,29 @@
+{-
+
+Test that some library functions don't cause "Maximum call stack size exceeded"
+errors.
+
+So far, only Prelude.List.++ is tested.
+
+-}
+
+module Main
+
+-- Until length and replicate are tail recursive, we roll our own for this test.
+
+lengthPlus : Nat -> List a -> Nat
+lengthPlus n [] = n
+lengthPlus n (x::xs) = lengthPlus (S n) xs
+
+tailRecLength : List a -> Nat
+tailRecLength = lengthPlus Z
+
+replicateOnto : List a -> Nat -> a -> List a
+replicateOnto acc Z x = acc
+replicateOnto acc (S n) x = replicateOnto (x :: acc) n x
+
+tailRecReplicate : Nat -> a -> List a
+tailRecReplicate = replicateOnto []
+
+main : IO ()
+main = putStrLn $ show $ tailRecLength $ tailRecReplicate 10000 () ++ [()]