printf example: idris performance regression 0.5.x (0.4 works fine)

c

set -x

rm -fr build

# exact memory consumption for 0.4
#ulimit -Sv 201060

# set memory limit for this process and children processes
ulimit -Sv 2000000

idris2 --version

time idris2 --timing --typecheck printf.ipkg

printf-bug-notes

++ rm -fr build
++ ulimit -Sv 2000000
++ idris2 --version
Idris 2, version 0.4.0
++ idris2 --timing --typecheck printf.ipkg
1/1: Building Printf (./Printf.idr)
TIMING ++ Parsing ./Printf.idr: 0.033s
TIMING ++ Reading imports: 0.011s
TIMING +++ Check RHS Printf:13:5--13:55: 0.000s
TIMING +++ Check RHS Printf:14:5--14:59: 0.000s
TIMING +++ Check RHS Printf:15:5--15:36: 0.000s
TIMING +++ Checking Coverage Printf.case block in buildArg: 0.000s
TIMING +++ Check RHS Printf:12:1--15:36: 0.000s
TIMING +++ Checking Coverage Printf.buildArg: 0.000s
TIMING +++ Check RHS Printf:19:5--19:57: 0.000s
TIMING +++ Check RHS Printf:20:5--20:50: 0.000s
TIMING +++ Check RHS Printf:21:5--21:32: 0.000s
TIMING +++ Checking Coverage Printf.case block in argToType: 0.000s
TIMING +++ Check RHS Printf:18:1--21:32: 0.000s
TIMING +++ Checking Coverage Printf.argToType: 0.000s
TIMING +++ Check RHS Printf:27:1--27:65: 0.000s
TIMING +++ Checking Coverage Printf.PrintfType: 0.000s
TIMING +++ Check RHS Printf:33:9--33:74: 0.001s
TIMING +++ Check RHS Printf:34:9--34:67: 0.000s
TIMING +++ Check RHS Printf:35:9--35:39: 0.000s
TIMING +++ Checking Coverage Printf.case block in sprintf,go: 0.000s
TIMING +++ Check RHS Printf:32:5--35:39: 0.002s
TIMING +++ Checking Coverage Printf.2099:3733:go: 0.000s
TIMING +++ Check RHS Printf:30:1--35:39: 0.002s
TIMING +++ Checking Coverage Printf.sprintf: 0.000s
TIMING +++ Check RHS Printf:39:1--39:224: 0.460s
TIMING +++ Checking Coverage Printf.test: 0.000s
TIMING +++ Totality check overall: 0.000s
TIMING ++ Processing decls: 0.620s
TIMING ++ Compile defs: 0.000s
TIMING + Elaborating ./Printf.idr: 0.666s

real  0m0.962s
user  0m0.909s
sys 0m0.053s


------------------


++ rm -fr build
++ ulimit -Sv 2000000
++ idris2 --version
Idris 2, version 0.5.1
++ idris2 --timing --typecheck printf.ipkg
1/1: Building Printf (./Printf.idr)
TIMING ++ Parsing ./Printf.idr: 0.026s
TIMING ++ Reading imports: 0.016s
TIMING +++ Check RHS Printf:13:5--13:55: 0.000s
TIMING +++ Check RHS Printf:14:5--14:59: 0.000s
TIMING +++ Check RHS Printf:15:5--15:36: 0.000s
TIMING +++ Checking Coverage Printf.case block in buildArg: 0.000s
TIMING +++ Check RHS Printf:12:1--15:36: 0.000s
TIMING +++ Checking Coverage Printf.buildArg: 0.000s
TIMING +++ Check RHS Printf:19:5--19:57: 0.000s
TIMING +++ Check RHS Printf:20:5--20:50: 0.000s
TIMING +++ Check RHS Printf:21:5--21:32: 0.000s
TIMING +++ Checking Coverage Printf.case block in argToType: 0.000s
TIMING +++ Check RHS Printf:18:1--21:32: 0.000s
TIMING +++ Checking Coverage Printf.argToType: 0.000s
TIMING +++ Check RHS Printf:27:1--27:65: 0.000s
TIMING +++ Checking Coverage Printf.PrintfType: 0.000s
TIMING +++ Check RHS Printf:33:9--33:74: 0.001s
TIMING +++ Check RHS Printf:34:9--34:67: 0.000s
TIMING +++ Check RHS Printf:35:9--35:39: 0.000s
TIMING +++ Checking Coverage Printf.case block in sprintf,go: 0.000s
TIMING +++ Check RHS Printf:32:5--35:39: 0.002s
TIMING +++ Checking Coverage Printf.2554:3836:go: 0.000s
TIMING +++ Check RHS Printf:30:1--35:39: 0.002s
TIMING +++ Checking Coverage Printf.sprintf: 0.000s
out of memory

real  0m2.988s
user  0m2.650s
sys 0m0.337s


------------------

++ rm -fr build
++ ulimit -Sv 2000000
++ idris2 --version
Idris 2, version 0.5.1-1ebe204c3
++ idris2 --timing --typecheck printf.ipkg
1/1: Building Printf (./Printf.idr)
TIMING ++ Parsing ./Printf.idr: 0.026s
TIMING ++ Reading imports: 0.018s
TIMING +++ Check RHS Printf:13:5--13:55: 0.000s
TIMING +++ Check RHS Printf:14:5--14:59: 0.000s
TIMING +++ Check RHS Printf:15:5--15:36: 0.000s
TIMING +++ Checking Coverage Printf.case block in buildArg: 0.000s
TIMING +++ Check RHS Printf:12:1--15:36: 0.000s
TIMING +++ Checking Coverage Printf.buildArg: 0.000s
TIMING +++ Check RHS Printf:19:5--19:57: 0.000s
TIMING +++ Check RHS Printf:20:5--20:50: 0.000s
TIMING +++ Check RHS Printf:21:5--21:32: 0.000s
TIMING +++ Checking Coverage Printf.case block in argToType: 0.000s
TIMING +++ Check RHS Printf:18:1--21:32: 0.000s
TIMING +++ Checking Coverage Printf.argToType: 0.000s
TIMING +++ Check RHS Printf:27:1--27:65: 0.000s
TIMING +++ Checking Coverage Printf.PrintfType: 0.000s
TIMING +++ Check RHS Printf:33:9--33:74: 0.001s
TIMING +++ Check RHS Printf:34:9--34:67: 0.000s
TIMING +++ Check RHS Printf:35:9--35:39: 0.000s
TIMING +++ Checking Coverage Printf.case block in sprintf,go: 0.000s
TIMING +++ Check RHS Printf:32:5--35:39: 0.002s
TIMING +++ Checking Coverage Printf.2554:3836:go: 0.000s
TIMING +++ Check RHS Printf:30:1--35:39: 0.002s
TIMING +++ Checking Coverage Printf.sprintf: 0.000s
out of memory

real  0m2.992s
user  0m2.623s
sys 0m0.368s

Printf.idr

module Printf

import Prelude
import Data.String

data Arg
    = AInt      Arg
    | AOther    Char Arg
    | AEnd

buildArg : List Char -> Arg
buildArg fmt = case fmt of
    '%' :: 'i' :: fmtTail   => AInt (buildArg fmtTail)
    c :: fmtTail            => AOther c (buildArg fmtTail)
    Nil                     => AEnd

argToType : Arg -> Type -> Type
argToType a result = case a of
    AInt fmtTail      => Int -> argToType fmtTail result
    AOther _ fmtTail  => argToType fmtTail result
    AEnd              => result

-- PrintfType "foo" result = result
-- PrintfType "%i\n" result = Int -> result
-- etc
PrintfType : String -> Type -> Type
PrintfType fmt result = argToType (buildArg (unpack fmt)) result

sprintf : (fmt : String) -> PrintfType fmt String
sprintf fmt = go "" (buildArg (unpack fmt)) where
    go : String -> (arg : Arg) -> argToType arg String
    go strTail arg = case arg of
        AInt fmtTail        => \i : Int => go (strTail ++ show i) fmtTail
        AOther c fmtTail    => go (strTail ++ singleton c) fmtTail
        AEnd                => strTail

test : ?result
--test = sprintf "%i%i"
test = sprintf "%i%i%i%i%i%i%i%i%i%i%i%i%i%i%i%i%i%i%i%i%i%i%i%i%i%i%i%i%i%i%i%i%i%i%i%i%i%i%i%i%i%i%i%i%i%i%i%i%i%i%i%i%i%i%i%i%i%i%i%i%i%i%i%i%i%i%i%i%i%i%i%i%i%i%i%i%i%i%i%i%i%i%i%i%i%i%i%i%i%i%i%i%i%i%i%i%i%i%i%i%i%i%i"
--test = sprintf "%i%i%i%i%i%i%i%i%i%i%i%i"

printf.ipkg

package printf

depends = prelude

modules = Printf

sourcedir = "."