{-# LINE 26 "definitions.fmt" #-}
{- 

Idris code extracted from the paper 
"Continuation-Passing Style, Defunctionalization, Accumulations, and Associativity"
Jeremy Gibbons

 -}
{-# LINE 184 "continued-idris.ltx" #-}
fact1 : Nat -> Nat
fact1 Z      = 1
fact1 (S n)  = S n * fact1 n
{-# LINE 199 "continued-idris.ltx" #-}
fact2 : Nat -> Nat
fact2 n = fact2' n id
{-# LINE 204 "continued-idris.ltx" #-}
  where
{-# LINE 231 "continued-idris.ltx" #-}
    fact2' : Nat -> (Nat -> r) -> r
    fact2' Z k      = k 1
    fact2' (S n) k  = fact2' n (k . (\ m => S n * m))
{-# LINE 250 "continued-idris.ltx" #-}
factabs3 : List Nat -> (Nat -> Nat)
factabs3 []      = id
factabs3 (n::k)  = (n *) . factabs3 k
{-# LINE 261 "continued-idris.ltx" #-}
fact3 : Nat -> Nat
fact3 n = fact3' n [] where
  fact3' : Nat -> List Nat -> Nat
  fact3' Z k      = foldr (*) 1 k   --  |= product k|
  fact3' (S n) k  = fact3' n (k ++ [S n])
{-# LINE 273 "continued-idris.ltx" #-}
factabs4 : Nat -> (Nat -> Nat)
factabs4 k  = (k *)
{-# LINE 282 "continued-idris.ltx" #-}
fact4 : Nat -> Nat
fact4 n = fact4' n 1 where
  fact4' : Nat -> Nat -> Nat
  fact4' Z k  = k
  fact4' (S n) k  = fact4' n (k * S n)
{-# LINE 307 "continued-idris.ltx" #-}
subt1 : Integer -> Integer
subt1 0      = 1
subt1 n  = n - subt1 n
{-# LINE 315 "continued-idris.ltx" #-}
runTests_factorial : IO ()
runTests_factorial = do
    putStrLn "Testing factorial..."
    sequence_ (zipWith test [2..4] [fact2,fact3,fact4])
  where
    test : Nat -> (Nat -> Nat) -> IO ()
    test i f = putStrLn ("  fact" ++ show i ++ " ok: " ++ show (and [ f n == fact1 n | n <- [0..10] ]))
{-# LINE 330 "continued-idris.ltx" #-}
reverse1 : List a -> List a
reverse1 []       = []
reverse1 (x::xs)  = reverse1 xs ++ [x]
{-# LINE 341 "continued-idris.ltx" #-}
reverse2 : List a -> List a
reverse2 xs = reverse2' xs id where
  reverse2' : List a -> (List a->List a) -> List a
  reverse2' []  k      = k []
  reverse2' (x::xs) k  = reverse2' xs (\ zs => k (zs ++ [x]))
{-# LINE 356 "continued-idris.ltx" #-}
revabs3 : List a -> (List a->List a)
revabs3 ys = \ zs => zs++ys
{-# LINE 395 "continued-idris.ltx" #-}
reverse3 : List a -> List a
reverse3 xs = reverse3' xs [] where
  reverse3' : List a -> List a -> List a
  reverse3' [] k       = k 
  reverse3' (x::xs) k  = reverse3' xs (x::k)
{-# LINE 405 "continued-idris.ltx" #-}
runTests_reverse : IO ()
runTests_reverse = do
    putStrLn "Testing reverse... " 
    sequence_ (zipWith test [2..3] [reverse2,reverse3])
  where
    xss : List (List Integer)
    xss = [ [], [1,2,3], [3,2,1], [1,1,2] ]
    test : Integer -> (List Integer -> List Integer) -> IO ()
    test i f = putStrLn ("  reverse" ++ show i ++ " ok: " ++ show (and [ f xs == reverse1 xs | xs <- xss ]))
{-# LINE 421 "continued-idris.ltx" #-}
data Tree a = Tip a | Bin (Tree a) (Tree a) 
{-# LINE 425 "continued-idris.ltx" #-}
Show a => Show (Tree a) where
  show (Tip a)    = "Tip (" ++ show a ++ ")"
  show (Bin t u)  = "Bin (" ++ show t ++ ") (" ++ show u ++ ")"

tree : Tree Integer
tree = Bin (Bin (Tip 1) (Tip 2)) (Tip 3)
{-# LINE 435 "continued-idris.ltx" #-}
flatten1 : Tree a -> List a
flatten1 (Tip x)    = [x]
flatten1 (Bin t u)  = flatten1 t ++ flatten1 u
{-# LINE 445 "continued-idris.ltx" #-}
flatten2 : Tree a -> List a
flatten2 t = flatten2' t id where
  flatten2' : Tree a -> (List a->List a) -> List a
  flatten2' (Tip x) k    = k [x]
  flatten2' (Bin t u) k  = flatten2' t (\ xs => flatten2' u (\ ys => k (xs++ys)))
{-# LINE 475 "continued-idris.ltx" #-}
data FlatCont3 a  =  FlatRoot3
                  |  FlatLeftTree3 (Tree a) (FlatCont3 a)
                  |  FlatRightList3 (List a) (FlatCont3 a)
{-# LINE 489 "continued-idris.ltx" #-}
flatten3 : Tree a -> List a
flatten3 t = flatten3' t FlatRoot3 where
  mutual 
    flatten3' : Tree a -> FlatCont3 a -> List a
    flatten3' (Tip x) k    = flatabs3 k [x]
    flatten3' (Bin t u) k  = flatten3' t (FlatLeftTree3 u k)

    flatabs3 : FlatCont3 a -> (List a -> List a)
    flatabs3 FlatRoot3              = id
    flatabs3 (FlatLeftTree3 u k)    = \ xs => flatten3' u (FlatRightList3 xs k)
    flatabs3 (FlatRightList3 xs k)  = \ ys => flatabs3 k (xs++ys)
{-# LINE 507 "continued-idris.ltx" #-}
FlatCont4 : Type -> Type
FlatCont4 a = List (Either (Tree a) (List a))
{-# LINE 513 "continued-idris.ltx" #-}
flatten4 : Tree a -> List a
flatten4 t = flatten4' t [] where
  mutual
    flatten4' : Tree a -> FlatCont4 a -> List a
    flatten4' (Tip x) k    = flatabs4 k [x]
    flatten4' (Bin t u) k  = flatten4' t (Left u :: k)

    flatabs4 : FlatCont4 a -> (List a -> List a)
    flatabs4 []               = id
    flatabs4 (Left u :: k)    = \ xs => flatten4' u (Right xs :: k)
    flatabs4 (Right xs :: k)  = \ ys => flatabs4 k (xs++ys)
{-# LINE 533 "continued-idris.ltx" #-}
flatten5 : Tree a -> List a
flatten5 t = flatten5' t id where
  flatten5' : Tree a -> (List a->List a) -> List a
  flatten5' (Tip x) k    = k [x]
  flatten5' (Bin t u) k  = flatten5' u (\ ys => flatten5' t (\ xs => k (xs++ys)))
{-# LINE 541 "continued-idris.ltx" #-}
FlatCont6 : Type -> Type
FlatCont6 a = List (Either (List a) (Tree a))
{-# LINE 548 "continued-idris.ltx" #-}
flatten6 : Tree a -> List a
flatten6 t = flatten6' t [] where
  mutual
    flatten6' : Tree a -> FlatCont6 a -> List a
    flatten6' (Tip x) k    = flatabs6 k [x]
    flatten6' (Bin t u) k  = flatten6' u (Right t :: k)

    flatabs6 : FlatCont6 a -> (List a -> List a)
    flatabs6 []               = id
    flatabs6 (Left ys :: k)   = \ xs => flatabs6 k (xs++ys)
    flatabs6 (Right t :: k)   = \ ys => flatten6' t (Left ys :: k)
{-# LINE 598 "continued-idris.ltx" #-}
FlatCont7 : Type -> Type
FlatCont7 a = (List a, List (Tree a))
{-# LINE 608 "continued-idris.ltx" #-}
flatten7 : Tree a -> List a
flatten7 t = flatten7' t ([],[]) where
  mutual
    flatten7' : Tree a -> FlatCont7 a -> List a
    flatten7' (Tip x) (ys,ts)    = flatabs7 (ys,ts) [x]
    flatten7' (Bin t u) (ys,ts)  = flatten7' u (ys,t::ts)

    flatabs7 : FlatCont7 a -> (List a->List a)
    flatabs7 (ys,[])        = \ xs =>  xs++ys
    flatabs7 (ys,t :: ts)   = \ xs => flatten7' t (xs++ys, ts)
{-# LINE 623 "continued-idris.ltx" #-}
flatten8 : Tree a -> List a
flatten8 t = flatten8' ([],[t]) where
  mutual
    flatten8' : (List a, List (Tree a)) -> List a
    flatten8' (ys, Tip x :: ts)    = flatabs8 (ys,ts) [x]
    flatten8' (ys, Bin t u :: ts)  = flatten8' (ys,u::t::ts)

    flatabs8 : (List a, List (Tree a)) -> (List a -> List a)
    flatabs8 (ys,[])        = \ xs =>  xs++ys
    flatabs8 (ys,t :: ts)   = \ xs => flatten8' (xs++ys, t::ts)
{-# LINE 636 "continued-idris.ltx" #-}
flatten9 : Tree a -> List a
flatten9 t = flatten9' [t] [] where
  flatten9' : List (Tree a) -> List a -> List a
  flatten9' [Tip x]          ys  = x :: ys
  flatten9' (Tip x :: ts)    ys  = flatten9' ts (x::ys) 
  flatten9' (Bin t u :: ts)  ys  = flatten9' (u::t::ts) ys
{-# LINE 648 "continued-idris.ltx" #-}
runTests_flatten : IO ()
runTests_flatten = do
    putStrLn "Testing flatten... " 
    sequence_ (zipWith test [2..9] flattens)
  where
    ts : List (Tree Integer)
    ts = [ Tip 3, Bin (Tip 4) (Tip 5), Bin (Tip 6) (Bin (Tip 7) (Tip 8)) ]
    test : Integer -> (Tree Integer -> List Integer) -> IO ()
    test i f = putStrLn ("  flatten" ++ show i ++ " ok: " ++ show (and [ f t == flatten1 t | t <- ts ]))
    flattens : List (Tree a -> List a)
    flattens = [flatten2, flatten3, flatten4, flatten5, flatten6, flatten7, flatten8, flatten9]
{-# LINE 680 "continued-idris.ltx" #-}
data Expr = Lit Integer | Diff Expr Expr 
{-# LINE 684 "continued-idris.ltx" #-}
Show Expr where
  show (Lit n)      = show n
  show (Diff e e')  = "(" ++ show e ++ ") - (" ++ show e' ++ ")"
{-# LINE 691 "continued-idris.ltx" #-}
eval1 : Expr -> Integer
eval1 (Lit n)      = n
eval1 (Diff e e')  = eval1 e - eval1 e'
{-# LINE 698 "continued-idris.ltx" #-}
expr : Expr
{-# LINE 702 "continued-idris.ltx" #-}
expr = Diff (Diff (Lit 3) (Lit 4)) (Lit 5)
{-# LINE 717 "continued-idris.ltx" #-}
eval2 : Expr -> Integer
eval2 e = eval2' e id where
  eval2' : Expr -> (Integer->Integer) -> Integer
  eval2' (Lit n) k      = k n
  eval2' (Diff e e') k  = eval2' e (\ m => eval2' e' (\ n => k (m-n)))
{-# LINE 725 "continued-idris.ltx" #-}
data EvalFrame3 = EvalLeftExpr3 Expr | EvalRightValue3 Integer

EvalCont3 : Type
EvalCont3 = List EvalFrame3

eval3 : Expr -> Integer
eval3 e = eval3' e [] where
  mutual
    eval3' : Expr -> EvalCont3 -> Integer
    eval3' (Lit n)      k = evalabs3 k n
    eval3' (Diff e e')  k = eval3' e (EvalLeftExpr3 e' :: k)

    evalabs3 : EvalCont3 -> (Integer -> Integer)
    evalabs3 []                        n  = n
    evalabs3 (EvalLeftExpr3 e' :: k)   m  = eval3' e' (EvalRightValue3 m :: k)
    evalabs3 (EvalRightValue3 m :: k)  n  = evalabs3 k (m-n)
{-# LINE 750 "continued-idris.ltx" #-}
data Instr = PushI Integer | SubI  
Prog4 : Type
Prog4 = List Instr
{-# LINE 756 "continued-idris.ltx" #-}
exec4 : Prog4 -> List Integer -> List Integer
exec4 p s = foldl step s p where
                                  step ns          (PushI n)  = n::ns
                                  step (n::m::ns)  SubI       = (m-n)::ns   --  note reversal of arguments
{-# LINE 763 "continued-idris.ltx" #-}
compile4 : Expr -> Prog4
compile4 (Lit n)      = [PushI n]
compile4 (Diff e e')  = compile4 e ++ compile4 e' ++ [SubI]
{-# LINE 777 "continued-idris.ltx" #-}
eval4 : Expr -> Integer
eval4 e = case exec4 (compile4 e) [] of [n] => n
{-# LINE 884 "continued-idris.ltx" #-}
Arrow : List Type -> Type -> Type
Arrow []         b = b
Arrow (a :: as)  b = a -> Arrow as b
{-# LINE 895 "continued-idris.ltx" #-}
b_n : {as : List Type} -> (b -> c) -> Arrow as b -> Arrow as c
b_n {as = []}      g f = g f
b_n {as = _ :: _}  g f = b_n g . f
{-# LINE 901 "continued-idris.ltx" #-}
b0 : (b -> c) -> b -> c
b0 = b_n {as = []}

b1 : (b -> c) -> (a -> b) -> (a -> c)
b1 = b_n {as = [a]}

b2 : (b -> c) -> (a -> a' -> b) -> (a -> a' -> c)
b2 = b_n {as = [a,a']}
{-# LINE 914 "continued-idris.ltx" #-}
halt : r -> r
ret : Integer -> (Integer -> r) -> r
sub : (Integer -> r) -> Integer -> Integer -> r
{-# LINE 920 "continued-idris.ltx" #-}
eval5 : Expr -> Integer
eval5 e = eval5' e halt where
  eval5' : Expr -> (Integer->Integer) -> Integer
  eval5' (Lit n)      = ret n
  eval5' (Diff e e')  = b1 (eval5' e) (b2 (eval5' e') sub)
{-# LINE 928 "continued-idris.ltx" #-}
halt   = id
ret n  = \ k => k n
sub    = \ k => \ m => \ n => k (m - n)
{-# LINE 949 "continued-idris.ltx" #-}
data ExprRep6 : List Type -> Type where
  Ret6  : Integer ->                                    ExprRep6 [] 
  Sub6  :                                               ExprRep6 [ Integer,Integer]
  B16   : ExprRep6 [] -> ExprRep6 [ Integer] ->         ExprRep6 []
  B26   : ExprRep6 [] -> ExprRep6 [Integer,Integer] ->  ExprRep6 [ Integer]
{-# LINE 961 "continued-idris.ltx" #-}
rep6 : Expr -> ExprRep6 []
rep6 (Lit n)      = Ret6 n
rep6 (Diff e e')  = B16 (rep6 e) (B26 (rep6 e') Sub6)
{-# LINE 968 "continued-idris.ltx" #-}
abs6 : ExprRep6 r -> (Integer -> Integer) -> Arrow r Integer
abs6 (Ret6 n)   = ret n
abs6 Sub6       = sub
abs6 (B16 x y)  = b1 (abs6 x) (abs6 y)
abs6 (B26 x y)  = b2 (abs6 x) (abs6 y)
{-# LINE 977 "continued-idris.ltx" #-}
eval6 : Expr -> Integer
eval6 e = abs6 (rep6 e) halt
{-# LINE 1024 "continued-idris.ltx" #-}
calc5 : List Integer
calc5 = [
  eval5 expr,
  b0 (b1 (b1 (ret 3) (b2 (ret 4) sub)) (b2 (ret 5) sub)) halt,
  b0 (b1 (ret 3) (b2 (ret 4) sub)) (b0 (b2 (ret 5) sub) halt),
  b0 (ret 3) (b0 (b2 (ret 4) sub) (b0 (b2 (ret 5) sub) halt)),
  b0 (ret 3) (b1 (ret 4) (b0 sub (b0 (b2 (ret 5) sub) halt))),
  b0 (ret 3) (b1 (ret 4) (b0 sub (b1 (ret 5) (b0 sub halt)))),
  ret 3 (b1 (ret 4) (b0 sub (b1 (ret 5) (b0 sub halt)))),
  b1 (ret 4) (b0 sub (b1 (ret 5) (b0 sub halt))) 3,
  ret 4 (b0 sub (b1 (ret 5) (b0 sub halt)) 3),
  b0 sub (b1 (ret 5) (b0 sub halt)) 3 4,
  sub (b1 (ret 5) (b0 sub halt)) 3 4,
  b1 (ret 5) (b0 sub halt) (3-4),
  ret 5 (b0 sub halt (3-4)),
  b0 sub halt (3-4) 5,
  sub halt (3-4) 5,
  halt ((3-4)-5),
  (3-4)-5,
  -6
  ]
{-# LINE 1050 "continued-idris.ltx" #-}
data ExprRep7 : List Type -> Type where
  Halt7  :                                         ExprRep7 [Integer]
  BRet7  : Integer -> ExprRep7 (Integer ::  r) ->  ExprRep7 r
  BSub7  : ExprRep7 (Integer ::  r) ->             ExprRep7 (Integer ::  Integer ::  r)
{-# LINE 1061 "continued-idris.ltx" #-}
append7 : ExprRep7 r -> ExprRep7 (Integer :: s) -> ExprRep7 (r ++ s)
append7 Halt7 y        = y
append7 (BRet7 n k) y  = BRet7 n (append7 k y)
append7 (BSub7 k) y    = BSub7 (append7 k y)
{-# LINE 1069 "continued-idris.ltx" #-}
rotate7 : ExprRep6 r -> ExprRep7 r
rotate7 (Ret6 n)   = BRet7 n Halt7
rotate7 Sub6       = BSub7 Halt7
rotate7 (B16 x y)  = append7 (rotate7 x) (rotate7 y)
rotate7 (B26 x y)  = append7 (rotate7 x) (rotate7 y)
{-# LINE 1077 "continued-idris.ltx" #-}
rep7 : Expr -> ExprRep7 []
rep7 (Lit n)      = BRet7 n Halt7
rep7 (Diff e e')  = append7  (rep7 e) (append7 (rep7 e') (BSub7 Halt7))
{-# LINE 1083 "continued-idris.ltx" #-}
abs7 : ExprRep7 r -> Arrow r Integer
abs7 Halt7        = halt
abs7 (BRet7 n k)  = ret n (abs7 k)     
abs7 (BSub7 k)    = flip (sub (abs7 k))   --  note reversal of arguments again
{-# LINE 1104 "continued-idris.ltx" #-}
eval7 : Expr -> Integer
eval7 e = abs7 (rep7 e)
{-# LINE 1109 "continued-idris.ltx" #-}
compile7 : Expr -> Prog4
compile7 = compileRep7 . rep7 where
  compileRep7 : ExprRep7 r -> Prog4
  compileRep7 Halt7        = []
  compileRep7 (BRet7 n k)  = PushI n :: compileRep7 k
  compileRep7 (BSub7 k)    = SubI :: compileRep7 k
{-# LINE 1118 "continued-idris.ltx" #-}
eval7' : Expr -> Integer
eval7' e = case exec4 (compile7 e) [] of [n] => n
{-# LINE 1128 "continued-idris.ltx" #-}
runTests_expr : IO ()
runTests_expr = do
    putStrLn "Testing eval... " 
    sequence_ (zipWith test [2..8] [eval2,eval3,eval4,eval5,eval6,eval7,eval7'])
  where
    test : Integer -> (Expr -> Integer) -> IO ()
    test i f = putStrLn ("  eval" ++ show i ++ " ok: " ++ show (f expr == eval1 expr))
{-# LINE 1238 "continued-idris.ltx" #-}
parity : Nat -> Bool
parity n = odd n where
  mutual
    odd   : Nat -> Bool
    odd Z       = False
    odd (S n)   = even n

    even  : Nat -> Bool
    even Z      = True
    even (S n)  = odd n
{-# LINE 1276 "continued-idris.ltx" #-}
main : IO ()
main = do
  runTests_factorial
  runTests_reverse
  runTests_flatten
  runTests_expr