如何评估Idris交互中的递归函数？

Question

涉足伊德里斯，我试图将this Haskell function移植到伊德里斯。我觉得我成功了，有了这个代码...

windowl : Nat -> List a -> List (List a) 
windowl size = loop 
    where 
    loop xs = case List.splitAt size xs of 
     (ys, []) => if length ys == size then [ys] else [] 
     (ys, _) => ys :: loop (drop 1 xs) 

然而，当我把它叫做互动伊德里斯，似乎只有在第一次调用到函数进行评估，在递归下一步是不是。这是我在控制台上得到的。

*hello> windowl 2 [1,2,3,4,5] 
[1, 2] :: Main.windowl, loop Integer 2 [2, 3, 4, 5] : List (List Integer) 

有人能告诉我发生了什么，我怎么能完全评估功能？

Answer 1

正如manual解释说：

在它知道是总 编译一次[伊德里斯]只会评估的事情...... [跳过] ... 的REPL，为了方便，使用编译时评估的概念。

的总和检查是无法发现，windowl功能其实总的，所以我们可以使用assert_smallerconstruction骗：

total 
windowl : Nat -> List a -> List (List a) 
windowl size = loop 
    where 
    loop : List a -> List (List a) 
    loop xs = case List.splitAt size xs of 
     (ys, []) => if length ys == size then [ys] else [] 
     (ys, _) => ys :: loop (assert_smaller xs $ drop 1 xs) 

或更改loop使整体明显的整体性检查器：

total 
windowl : Nat -> List a -> List (List a) 
windowl size = loop 
    where 
    loop : List a -> List (List a) 
    loop [] = [] 
    loop xs@(x :: xs') = case List.splitAt size xs of 
     (ys, []) => if length ys == size then [ys] else [] 
     (ys, _) => ys :: loop xs' 

是的，我在这里偷工减料，用模式代替硬编码的drop 1以说明这个想法。更一般的情况可能需要更多的工作。

在这一点上，REPL充分计算表达式：

λΠ> windowl 2 [1,2,3,4,5] 
[[1, 2], [2, 3], [3, 4], [4, 5]] : List (List Integer)