idris-lang/Idris2
1
1
Fork 0
mirror of https://github.com/idris-lang/Idris2.git synced 2024-11-28 19:13:02 +03:00
Code Issues Projects Releases Wiki Activity

Merge pull request #1357 from edwinb/optimising

Browse Source 
A couple of optimisations
This commit is contained in:
Edwin Brady 2021-04-30 18:56:32 +01:00 committed by GitHub
commit 93f4092e94
No known key found for this signature in database
GPG Key ID: 4AEE18F83AFDEB23
11 changed files with 88 additions and 58 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

21
libs/base/Data/String.idr
View File

@ -18,25 +18,6 @@ partial
foldl1 : (a -> a -> a) -> List a -> a
foldl1 f (x::xs) = foldl f x xs
-- This function runs fast when compiled but won't compute at compile time.
-- If you need to unpack strings at compile time, use Prelude.unpack.
%foreign
"scheme:string-unpack"
"javascript:lambda:(str)=>__prim_js2idris_array(Array.from(str))"
export
fastUnpack : String -> List Char
-- This works quickly because when string-concat builds the result, it allocates
-- enough room in advance so there's only one allocation, rather than lots!
--
-- Like fastUnpack, this function won't reduce at compile time.
-- If you need to concatenate strings at compile time, use Prelude.concat.
%foreign
"scheme:string-concat"
"javascript:lambda:(xs)=>''.concat(...__prim_idris2js_array(xs))"
export
fastConcat : List String -> String
-- This uses fastConcat internally so it won't compute at compile time.
export
fastUnlines : List String -> String
@ -132,6 +113,8 @@ export
unlines : List String -> String
unlines = pack . unlines' . map unpack
%transform "fastUnlines" unlines = fastUnlines
||| A view checking whether a string is empty
||| and, if not, returning its head and tail
public export

27
libs/prelude/Prelude/Types.idr
View File

@ -412,6 +412,19 @@ Traversable List where
traverse f [] = pure []
traverse f (x::xs) = pure (::) <*> (f x) <*> (traverse f xs)
-- This works quickly because when string-concat builds the result, it allocates
-- enough room in advance so there's only one allocation, rather than lots!
--
-- Like fastUnpack, this function won't reduce at compile time.
-- If you need to concatenate strings at compile time, use Prelude.concat.
%foreign
"scheme:string-concat"
"javascript:lambda:(xs)=>''.concat(...__prim_idris2js_array(xs))"
export
fastConcat : List String -> String
%transform "fastConcat" concat {t = List} {a = String} = fastConcat
||| Check if something is a member of a list using the default Boolean equality.
public export
elem : Eq a => a -> List a -> Bool
@ -537,6 +550,9 @@ pack (x :: xs) = strCons x (pack xs)
export
fastPack : List Char -> String
-- always use 'fastPack' at run time
%transform "fastPack" pack = fastPack
||| Turns a string into a list of characters.
|||
||| ```idris example
@ -552,6 +568,17 @@ unpack str = unpack' (prim__cast_IntegerInt (natToInteger (length str)) - 1) str
then acc
else assert_total $ unpack' (pos - 1) str (assert_total (prim__strIndex str pos)::acc)
-- This function runs fast when compiled but won't compute at compile time.
-- If you need to unpack strings at compile time, use Prelude.unpack.
%foreign
"scheme:string-unpack"
"javascript:lambda:(str)=>__prim_js2idris_array(Array.from(str))"
export
fastUnpack : String -> List Char
-- always use 'fastPack' at run time
%transform "fastUnpack" unpack = fastUnpack
public export
Semigroup String where
(<+>) = (++)

6
src/Core/Context.idr
View File

@ -2479,8 +2479,10 @@ addLogLevel : {auto c : Ref Ctxt Defs} ->
addLogLevel lvl
= do defs <- get Ctxt
case lvl of
Nothing => put Ctxt (record { options->session->logLevel = defaultLogLevel } defs)
Just l => put Ctxt (record { options->session->logLevel $= insertLogLevel l } defs)
Nothing => put Ctxt (record { options->session->logEnabled = True,
options->session->logLevel = defaultLogLevel } defs)
Just l => put Ctxt (record { options->session->logEnabled = True,
options->session->logLevel $= insertLogLevel l } defs)
export
withLogLevel : {auto c : Ref Ctxt Defs} ->

12
src/Core/Context/Log.idr
View File

@ -16,8 +16,8 @@ logTerm : {vars : _} ->
String -> Nat -> Lazy String -> Term vars -> Core ()
logTerm str n msg tm
= do opts <- getSession
let lvl = mkLogLevel str n
if keepLog lvl (logLevel opts)
let lvl = mkLogLevel (logEnabled opts) str n
if keepLog lvl (logEnabled opts) (logLevel opts)
then do tm' <- toFullNames tm
coreLift $ putStrLn $ "LOG " ++ show lvl ++ ": " ++ msg
++ ": " ++ show tm'
@ -27,7 +27,7 @@ log' : {auto c : Ref Ctxt Defs} ->
LogLevel -> Lazy String -> Core ()
log' lvl msg
= do opts <- getSession
if keepLog lvl (logLevel opts)
if keepLog lvl (logEnabled opts) (logLevel opts)
then coreLift $ putStrLn $ "LOG " ++ show lvl ++ ": " ++ msg
else pure ()
@ -37,7 +37,7 @@ export
log : {auto c : Ref Ctxt Defs} ->
String -> Nat -> Lazy String -> Core ()
log str n msg
= do let lvl = mkLogLevel str n
= do let lvl = mkLogLevel (logEnabled !getSession) str n
log' lvl msg
export
@ -45,8 +45,8 @@ logC : {auto c : Ref Ctxt Defs} ->
String -> Nat -> Core String -> Core ()
logC str n cmsg
= do opts <- getSession
let lvl = mkLogLevel str n
if keepLog lvl (logLevel opts)
let lvl = mkLogLevel (logEnabled opts) str n
if keepLog lvl (logEnabled opts) (logLevel opts)
then do msg <- cmsg
coreLift $ putStrLn $ "LOG " ++ show lvl ++ ": " ++ msg
else pure ()

41
src/Core/Normalise.idr
View File

@ -219,6 +219,9 @@ parameters (defs : Defs, topopts : EvalOpts)
= evalRef env True fc Func (Resolved i) (map (EmptyFC,) args ++ stk)
(NApp fc (NMeta nm i args) stk)
-- The commented out logging here might still be useful one day, but
-- evalRef is used a lot and even these tiny checks turn out to be
-- worth skipping if we can
evalRef : {auto c : Ref Ctxt Defs} ->
{free : _} ->
Env Term free ->
@ -226,24 +229,31 @@ parameters (defs : Defs, topopts : EvalOpts)
FC -> NameType -> Name -> Stack free -> (def : Lazy (NF free)) ->
Core (NF free)
evalRef env meta fc (DataCon tag arity) fn stk def
= do logC "eval.ref.data" 50 $ pure $ "Found data constructor: " ++ show !(toFullNames fn)
= do -- logC "eval.ref.data" 50 $ do fn' <- toFullNames fn -- Can't use ! here, it gets lifted too far
-- pure $ "Found data constructor: " ++ show fn'
pure $ NDCon fc fn tag arity stk
evalRef env meta fc (TyCon tag arity) fn stk def
= do logC "eval.ref.type" 50 $ pure $ "Found type constructor: " ++ show !(toFullNames fn)
= do -- logC "eval.ref.type" 50 $ do fn' <- toFullNames fn
-- pure $ "Found type constructor: " ++ show fn'
pure $ ntCon fc fn tag arity stk
evalRef env meta fc Bound fn stk def
= do logC "eval.ref.bound" 50 $ pure $ "Found bound variable: " ++ show !(toFullNames fn)
= do -- logC "eval.ref.bound" 50 $ do fn' <- toFullNames fn
-- pure $ "Found bound variable: " ++ show fn'
pure def
evalRef env meta fc nt@Func n stk def
= do logC "eval.ref.func" 50 $ pure $ "Found function: " ++ show !(toFullNames n)
= do -- logC "eval.ref.func" 50 $ do n' <- toFullNames n
-- pure $ "Found function: " ++ show n'
Just res <- lookupCtxtExact n (gamma defs)
| Nothing => pure def
let redok1 = evalAll topopts
let redok2 = reducibleInAny (currentNS defs :: nestedNS defs)
(fullname res)
(visibility res)
-- want to shortcut that second check, if we're evaluating
-- everything, so don't let bind unless we need that log!
let redok = redok1 || redok2
unless redok2 $ logC "eval.stuck" 5 $ pure $ "Stuck function: " ++ show !(toFullNames n)
unless redok2 $ logC "eval.stuck" 5 $ do n' <- toFullNames n
pure $ "Stuck function: " ++ show n'
if redok
then do
Just opts' <- useMeta (noCycles res) fc n defs topopts
@ -1166,8 +1176,8 @@ logNF : {vars : _} ->
String -> Nat -> Lazy String -> Env Term vars -> NF vars -> Core ()
logNF str n msg env tmnf
= do opts <- getSession
let lvl = mkLogLevel str n
when (keepLog lvl (logLevel opts)) $
let lvl = mkLogLevel (logEnabled opts) str n
when (keepLog lvl (logEnabled opts) (logLevel opts)) $
do defs <- get Ctxt
tm <- quote defs env tmnf
tm' <- toFullNames tm
@ -1182,7 +1192,7 @@ logTermNF' : {vars : _} ->
LogLevel -> Lazy String -> Env Term vars -> Term vars -> Core ()
logTermNF' lvl msg env tm
= do opts <- getSession
when (keepLog lvl (logLevel opts)) $
when (keepLog lvl (logEnabled opts) (logLevel opts)) $
do defs <- get Ctxt
tmnf <- normaliseHoles defs env tm
tm' <- toFullNames tmnf
@ -1194,7 +1204,7 @@ logTermNF : {vars : _} ->
{auto c : Ref Ctxt Defs} ->
String -> Nat -> Lazy String -> Env Term vars -> Term vars -> Core ()
logTermNF str n msg env tm
= do let lvl = mkLogLevel str n
= do let lvl = mkLogLevel (logEnabled !getSession) str n
logTermNF' lvl msg env tm
export
@ -1203,8 +1213,8 @@ logGlue : {vars : _} ->
String -> Nat -> Lazy String -> Env Term vars -> Glued vars -> Core ()
logGlue str n msg env gtm
= do opts <- getSession
let lvl = mkLogLevel str n
when (keepLog lvl (logLevel opts)) $
let lvl = mkLogLevel (logEnabled opts) str n
when (keepLog lvl (logEnabled opts) (logLevel opts)) $
do defs <- get Ctxt
tm <- getTerm gtm
tm' <- toFullNames tm
@ -1217,8 +1227,8 @@ logGlueNF : {vars : _} ->
String -> Nat -> Lazy String -> Env Term vars -> Glued vars -> Core ()
logGlueNF str n msg env gtm
= do opts <- getSession
let lvl = mkLogLevel str n
when (keepLog lvl (logLevel opts)) $
let lvl = mkLogLevel (logEnabled opts) str n
when (keepLog lvl (logEnabled opts) (logLevel opts)) $
do defs <- get Ctxt
tm <- getTerm gtm
tmnf <- normaliseHoles defs env tm
@ -1232,13 +1242,14 @@ logEnv : {vars : _} ->
String -> Nat -> String -> Env Term vars -> Core ()
logEnv str n msg env
= do opts <- getSession
when (keepLog lvl (logLevel opts)) $ do
when (logEnabled opts &&
keepLog lvl (logEnabled opts) (logLevel opts)) $ do
coreLift (putStrLn $ "LOG " ++ show lvl ++ ": " ++ msg)
dumpEnv env
where
lvl : LogLevel
lvl = mkLogLevel str n
lvl = mkLogLevel True str n
dumpEnv : {vs : List Name} -> Env Term vs -> Core ()
dumpEnv [] = pure ()

4
src/Core/Options.idr
View File

@ -141,6 +141,8 @@ record Session where
findipkg : Bool
codegen : CG
directives : List String
logEnabled : Bool -- do we check logging flags at all? This is 'False' until
-- any logging is enabled.
logLevel : LogLevels
logTimings : Bool
ignoreMissingPkg : Bool -- fail silently on missing packages. This is because
@ -197,7 +199,7 @@ defaultPPrint = MkPPOpts False True False
export
defaultSession : Session
defaultSession = MkSessionOpts False False False Chez [] defaultLogLevel
defaultSession = MkSessionOpts False False False Chez [] False defaultLogLevel
False False False Nothing Nothing
Nothing Nothing False

14
src/Core/Options/Log.idr
View File

@ -50,9 +50,10 @@ mkLogLevel' ps n = MkLogLevel (maybe [] forget ps) n
||| list. This bypasses the fact that the function `split` returns a non-empty
||| list no matter what.
export
mkLogLevel : String -> Nat -> LogLevel
mkLogLevel "" = mkLogLevel' Nothing
mkLogLevel ps = mkLogLevel' (Just (split (== '.') ps))
mkLogLevel : Bool -> String -> Nat -> LogLevel
mkLogLevel False _ = mkLogLevel' Nothing
mkLogLevel _ "" = mkLogLevel' Nothing
mkLogLevel _ ps = mkLogLevel' (Just (split (== '.') ps))
||| The unsafe constructor should only be used in places where the topic has already
||| been appropriately processed.
@ -98,7 +99,7 @@ parseLogLevel str = do
ns = tail nns in
case ns of
[] => pure (MkLogLevel [], n)
[ns] => pure (mkLogLevel n, ns)
[ns] => pure (mkLogLevel True n, ns)
_ => Nothing
lvl <- parsePositive n
pure $ c (fromInteger lvl)
@ -127,8 +128,9 @@ insertLogLevel (MkLogLevel ps n) = insert ps n
||| We keep a log if there is a prefix of its path associated to a larger number
||| in the LogLevels.
export
keepLog : LogLevel -> LogLevels -> Bool
keepLog (MkLogLevel path n) levels = go path levels where
keepLog : LogLevel -> Bool -> LogLevels -> Bool
keepLog (MkLogLevel _ Z) _ _ = True
keepLog (MkLogLevel path n) enabled levels = enabled && go path levels where
go : List String -> StringTrie Nat -> Bool
go path (MkStringTrie current) = here || there where

8
src/Core/UnifyState.idr
View File

@ -663,7 +663,8 @@ dumpHole' : {auto u : Ref UST UState} ->
dumpHole' lvl hole
= do ust <- get UST
defs <- get Ctxt
when (keepLog lvl (logLevel $ session $ options defs)) $ do
sopts <- getSession
when (keepLog lvl (logEnabled sopts) (logLevel sopts)) $ do
defs <- get Ctxt
case !(lookupCtxtExact (Resolved hole) (gamma defs)) of
Nothing => pure ()
@ -723,8 +724,9 @@ dumpConstraints : {auto u : Ref UST UState} ->
dumpConstraints str n all
= do ust <- get UST
defs <- get Ctxt
let lvl = mkLogLevel str n
when (keepLog lvl (logLevel $ session $ options defs)) $
sopts <- getSession
let lvl = mkLogLevel (logEnabled sopts) str n
when (keepLog lvl (logEnabled sopts) (logLevel sopts)) $
do let hs = toList (guesses ust) ++
toList (if all then holes ust else currentHoles ust)
case hs of

3
src/Idris/SetOptions.idr
View File

@ -202,7 +202,8 @@ preOptions (DumpVMCode f :: opts)
= do setSession (record { dumpvmcode = Just f } !getSession)
preOptions opts
preOptions (Logging n :: opts)
= do setSession (record { logLevel $= insertLogLevel n } !getSession)
= do setSession (record { logEnabled = True,
logLevel $= insertLogLevel n } !getSession)
preOptions opts
preOptions (ConsoleWidth n :: opts)
= do setConsoleWidth n

4
src/TTImp/TTImp.idr
View File

@ -1165,8 +1165,8 @@ logRaw : {auto c : Ref Ctxt Defs} ->
String -> Nat -> Lazy String -> RawImp -> Core ()
logRaw str n msg tm
= do opts <- getSession
let lvl = mkLogLevel str n
if keepLog lvl (logLevel opts)
let lvl = mkLogLevel (logEnabled opts) str n
if keepLog lvl (logEnabled opts) (logLevel opts)
then do coreLift $ putStrLn $ "LOG " ++ show lvl ++ ": " ++ msg
++ ": " ++ show tm
else pure ()

6
tests/idris2/coverage015/expected
View File

@ -1,11 +1,11 @@
1/1: Building Issue1169 (Issue1169.idr)
LOG coverage.missing:50: Getting constructors for: $resolved1926 [2 closures]
LOG coverage.missing:50: Getting constructors for: $resolved1928 [2 closures]
LOG coverage.missing:20: Getting constructors for: (Builtin.Pair String Builtin.Unit)
LOG coverage.missing:50: Looking for missing alts at type String
LOG coverage.missing:50: Getting constructors for: $resolved1923 [0 closures]
LOG coverage.missing:50: Getting constructors for: $resolved1925 [0 closures]
LOG coverage.missing:20: Getting constructors for: Builtin.Unit
LOG coverage.missing:20: (Builtin.MkPair {e:0} {e:1} {e:2} {e:3})
LOG coverage.empty:10: Checking type: TyCon 100 0 params: [] constructors: [$resolved1927] mutual with: [] detaggable by: Just []
LOG coverage.empty:10: Checking type: TyCon 100 0 params: [] constructors: [$resolved1929] mutual with: [] detaggable by: Just []
LOG coverage:5: Checking coverage for: (Main.test (Builtin.MkPair String Builtin.Unit {_:368} {_:369}))
LOG coverage:10: (raw term: (Main.test (Builtin.MkPair String Builtin.Unit {_:368} {_:369})))
LOG coverage:5: Erased to: (Main.test (Builtin.MkPair [__] [__] {_:368} {_:369}))