[Agda] evaluation in compilation

[Serge D. Mechveliani]

On Mon, Oct 01, 2012 at 03:52:20PM +0200, Andreas Abel wrote:
[..]
>   twothousand = 2000
>   ... sort (f twothousand) ...

This does not help.


> Can you post your code such that we can see what is going on in MAlonzo?


Here is a simplified code.
The below program 
* concats  n  copies of   xs0 = 1 :: 3 :: 4 :: 6 :: []    to  xs, 
* merges  xs  with a similarly built list  ys
  (ignore the fact that the argument lists for `merge' are not ordered),
* prints the first and the last elements in the result list. 

For  n = 16000  it is compiled.
For  n = 32000  compilation exheeds stack.
This stack overflow is probably due to that the compiler tries to 
evaluate the list  xs.  

This is for   Agda-2.3.0.1 + MAlonzo + lib-06.

*** How to prevent this evaluation in compilation time? ***

For this letter I replace the math symbols:
                  \bn  ->  Nat,    \::  ->  ::,    \<=  ->  <=
:
----------------------------------------------------------
module Main where
open import Foreign.Haskell
open import IO.Primitive
open import Relation.Nullary
open import Function using ( _$_ )
open import Data.Nat as Nat 
open import Data.Nat.Show
open import Data.List as List
open import Data.List.NonEmpty renaming ( fromList to fromL )
open import Data.String renaming ( _++_ to _Str++_ ) 
open import Prelude using ( toCostring )             -- by F. Kettelhoit 

showNatList : List Nat -> String
showNatList xs = "[" Str++ (showL xs) Str++ "]"
  where
  showL : List Nat -> String
  showL []        = ""
  showL (x :: []) = show x
  showL (x :: xs) = (show x) Str++ "," Str++ showL xs

merge : List Nat -> List Nat -> List Nat
merge []        ys        =  ys
merge xs        []        =  xs
merge (x :: xs) (y :: ys)  with  
                       x <=? y | merge xs (y :: ys) | merge (x :: xs) ys
...                  | yes _ | zs | _  =  x :: zs
...                  | _     | _  | zs =  y :: zs

concatCopies : {A : Set} -> Nat -> List A -> List A
concatCopies 0       xs =  []
concatCopies (suc n) xs =  xs ++ (concatCopies n xs)

xs0 : List Nat
xs0 = 1 :: 3 :: 4 :: 6 :: [] 

n : Nat
n = 16000  -- 32000

xs = concatCopies n xs0
ys = concatCopies n $ List.reverse xs0
zs : List Nat
zs = merge xs ys

hl : List Nat 
hl   with zs
... | z :: zs' =  z :: (last $ fromL z zs') :: []
... | _       =  []

main : IO Unit
main = putStrLn (toCostring $ showNatList hl)
----------------------------------------------------------------


Thanks,

------
Sergei