mirror of
https://github.com/edwinb/Idris2-boot.git
synced 2024-11-27 18:53:42 +03:00
Faster generation of Scheme
fastAppend allocates the whole string at once, rather than concatenating and therefore reallocating a lot
This commit is contained in:
parent
7dcb1cfd34
commit
b94c31a442
@ -101,6 +101,7 @@ findUsedNames tm
|
||||
natHackNames' <- traverse toResolvedNames natHackNames
|
||||
allNs <- getAllDesc (natHackNames' ++ keys ns) empty defs
|
||||
cns <- traverse toFullNames (keys allNs)
|
||||
let cns = nub cns
|
||||
-- Initialise the type constructor list with explicit names for
|
||||
-- the primitives (this is how we look up the tags)
|
||||
-- Use '1' for '->' constructor
|
||||
@ -208,3 +209,17 @@ copyLib (lib, fullname)
|
||||
Right _ <- coreLift $ writeToFile lib bin
|
||||
| Left err => throw (FileErr lib err)
|
||||
pure ()
|
||||
|
||||
export
|
||||
fastAppend : List String -> String
|
||||
fastAppend xs
|
||||
= let len = cast (foldr (+) 0 (map length xs)) in
|
||||
unsafePerformIO $
|
||||
do b <- newStringBuffer (len+1)
|
||||
build b xs
|
||||
getStringFromBuffer b
|
||||
where
|
||||
build : StringBuffer -> List String -> IO ()
|
||||
build b [] = pure ()
|
||||
build b (x :: xs) = do addToStringBuffer b x
|
||||
build b xs
|
||||
|
@ -334,7 +334,7 @@ compileToSS c tm outfile
|
||||
s <- newRef {t = List String} Structs []
|
||||
fgndefs <- traverse getFgnCall ns
|
||||
compdefs <- traverse (getScheme chezExtPrim chezString defs) ns
|
||||
let code = concat (map snd fgndefs) ++ concat compdefs
|
||||
let code = fastAppend (map snd fgndefs ++ compdefs)
|
||||
main <- schExp chezExtPrim chezString 0 [] !(compileExp tags tm)
|
||||
chez <- coreLift findChez
|
||||
support <- readDataFile "chez/support.ss"
|
||||
|
@ -296,7 +296,7 @@ compileToRKT c tm outfile
|
||||
s <- newRef {t = List String} Structs []
|
||||
fgndefs <- traverse getFgnCall ns
|
||||
compdefs <- traverse (getScheme racketPrim racketString defs) ns
|
||||
let code = concat (map snd fgndefs) ++ concat compdefs
|
||||
let code = fastAppend (map snd fgndefs ++ compdefs)
|
||||
main <- schExp racketPrim racketString 0 [] !(compileExp tags tm)
|
||||
support <- readDataFile "racket/support.rkt"
|
||||
let scm = schHeader (concat (map fst fgndefs)) ++
|
||||
|
@ -23,8 +23,6 @@ import TTImp.Unelab
|
||||
|
||||
import Parser.Support
|
||||
|
||||
import Control.Catchable
|
||||
|
||||
%default covering
|
||||
|
||||
showInfo : (Name, Int, GlobalDef) -> Core ()
|
||||
|
Loading…
Reference in New Issue
Block a user