mirror of
https://github.com/edwinb/Idris2-boot.git
synced 2025-01-02 17:52:09 +03:00
Move options out of Core and into Defs
This is quite a performance win, because there's less thunking (and I imagine more scope for inlining?)
This commit is contained in:
Edwin Brady
parent
f95205b8b9
commit
871ca6603c
@ -15,6 +15,8 @@ import Data.NameMap
|
||||
import Data.StringMap
|
||||
import Data.IntMap
|
||||
|
||||
import System
|
||||
|
||||
%default covering
|
||||
|
||||
-- Label for array references
|
||||
@ -98,8 +100,7 @@ getPosition (Resolved idx) ctxt = pure (idx, ctxt)
|
||||
getPosition n ctxt
|
||||
= case lookup n (resolvedAs ctxt) of
|
||||
Just idx =>
|
||||
do log 10 $ "Found " ++ show n ++ " " ++ show idx
|
||||
pure (idx, ctxt)
|
||||
do pure (idx, ctxt)
|
||||
Nothing =>
|
||||
do let idx = nextEntry ctxt
|
||||
let a = content ctxt
|
||||
@ -107,7 +108,6 @@ getPosition n ctxt
|
||||
when (idx >= max arr) $
|
||||
do arr' <- coreLift $ newArrayCopy (max arr + Grow) arr
|
||||
put Arr arr'
|
||||
log 10 $ "Added " ++ show n ++ " " ++ show idx
|
||||
pure (idx, record { nextEntry = idx + 1,
|
||||
resolvedAs $= insert n idx,
|
||||
possibles $= addPossible n idx
|
||||
@ -1205,15 +1205,83 @@ fromCharName : Defs -> Maybe Name
|
||||
fromCharName defs
|
||||
= fromCharName (primnames (options defs))
|
||||
|
||||
export
|
||||
setLogLevel : {auto c : Ref Ctxt Defs} ->
|
||||
Nat -> Core ()
|
||||
setLogLevel l
|
||||
= do defs <- get Ctxt
|
||||
put Ctxt (record { options->session->logLevel = l } defs)
|
||||
|
||||
export
|
||||
setLogTimings : {auto c : Ref Ctxt Defs} ->
|
||||
Bool -> Core ()
|
||||
setLogTimings b
|
||||
= do defs <- get Ctxt
|
||||
put Ctxt (record { options->session->logTimings = b } defs)
|
||||
|
||||
export
|
||||
getSession : {auto c : Ref Ctxt Defs} ->
|
||||
Core Session
|
||||
getSession
|
||||
= do defs <- get Ctxt
|
||||
pure (session (options defs))
|
||||
|
||||
-- Log message with a term, translating back to human readable names first
|
||||
export
|
||||
logTerm : {auto c : Ref Ctxt Defs} ->
|
||||
Nat -> Lazy String -> Term vars -> Core ()
|
||||
logTerm lvl msg tm
|
||||
= do opts <- getOpts
|
||||
= do opts <- getSession
|
||||
if logLevel opts >= lvl
|
||||
then do tm' <- toFullNames tm
|
||||
coreLift $ putStrLn $ "LOG " ++ show lvl ++ ": " ++ msg
|
||||
++ ": " ++ show tm'
|
||||
else pure ()
|
||||
|
||||
export
|
||||
log : {auto c : Ref Ctxt Defs} ->
|
||||
Nat -> Lazy String -> Core ()
|
||||
log lvl msg
|
||||
= do opts <- getSession
|
||||
if logLevel opts >= lvl
|
||||
then coreLift $ putStrLn $ "LOG " ++ show lvl ++ ": " ++ msg
|
||||
else pure ()
|
||||
|
||||
export
|
||||
logC : {auto c : Ref Ctxt Defs} ->
|
||||
Nat -> Core String -> Core ()
|
||||
logC lvl cmsg
|
||||
= do opts <- getSession
|
||||
if logLevel opts >= lvl
|
||||
then do msg <- cmsg
|
||||
coreLift $ putStrLn $ "LOG " ++ show lvl ++ ": " ++ msg
|
||||
else pure ()
|
||||
|
||||
|
||||
export
|
||||
logTime : {auto c : Ref Ctxt Defs} ->
|
||||
Lazy String -> Core a -> Core a
|
||||
logTime str act
|
||||
= do opts <- getSession
|
||||
if logTimings opts
|
||||
then do clock <- coreLift clockTime
|
||||
let nano = 1000000000
|
||||
let t = seconds clock * nano + nanoseconds clock
|
||||
res <- act
|
||||
clock <- coreLift clockTime
|
||||
let t' = seconds clock * nano + nanoseconds clock
|
||||
let time = t' - t
|
||||
assert_total $ -- We're not dividing by 0
|
||||
coreLift $ putStrLn $ "TIMING " ++ str ++ ": " ++
|
||||
show (time `div` nano) ++ "." ++
|
||||
addZeros (unpack (show ((time `mod` nano) `div` 1000000))) ++
|
||||
"s"
|
||||
pure res
|
||||
else act
|
||||
where
|
||||
addZeros : List Char -> String
|
||||
addZeros [] = "000"
|
||||
addZeros [x] = "00" ++ cast x
|
||||
addZeros [x,y] = "0" ++ cast x ++ cast y
|
||||
addZeros str = pack str
|
||||
|
||||
|
||||
@ -295,39 +295,26 @@ getErrorLoc (InCon x y err) = getErrorLoc err
|
||||
getErrorLoc (InLHS x y err) = getErrorLoc err
|
||||
getErrorLoc (InRHS x y err) = getErrorLoc err
|
||||
|
||||
public export
|
||||
record GlobalOpts where
|
||||
constructor MkGlobalOpts
|
||||
logLevel : Nat
|
||||
logTimings : Bool
|
||||
|
||||
export
|
||||
defaultOpts : GlobalOpts
|
||||
defaultOpts = MkGlobalOpts 0 False
|
||||
|
||||
-- Core is a wrapper around IO that is specialised for efficiency.
|
||||
export
|
||||
record Core t where
|
||||
constructor MkCore
|
||||
runCore : IORef GlobalOpts -> IO (Either Error t)
|
||||
runCore : IO (Either Error t)
|
||||
|
||||
export
|
||||
coreRun : GlobalOpts ->
|
||||
Core a ->
|
||||
coreRun : Core a ->
|
||||
(Error -> IO b) -> (a -> IO b) -> IO b
|
||||
coreRun opts (MkCore act) err ok
|
||||
= do oref <- newIORef opts
|
||||
either err ok !(act oref)
|
||||
coreRun (MkCore act) err ok
|
||||
= either err ok !act
|
||||
|
||||
export
|
||||
coreFail : Error -> Core a
|
||||
coreFail e = MkCore (\oref => pure (Left e))
|
||||
coreFail e = MkCore (pure (Left e))
|
||||
|
||||
export
|
||||
wrapError : (Error -> Error) -> Core a -> Core a
|
||||
wrapError fe (MkCore prog)
|
||||
= MkCore (\oref =>
|
||||
prog oref >>=
|
||||
= MkCore (prog >>=
|
||||
(\x => case x of
|
||||
Left err => pure (Left (fe err))
|
||||
Right val => pure (Right val)))
|
||||
@ -336,7 +323,7 @@ wrapError fe (MkCore prog)
|
||||
export
|
||||
%inline
|
||||
coreLift : IO a -> Core a
|
||||
coreLift op = MkCore (\oref => map Right op)
|
||||
coreLift op = MkCore (map Right op)
|
||||
|
||||
{- Monad, Applicative, Traversable are specialised by hand for Core.
|
||||
In theory, this shouldn't be necessary, but it turns out that Idris 1 doesn't
|
||||
@ -351,20 +338,19 @@ in the next version (i.e., in this project...)! -}
|
||||
export %inline
|
||||
(>>=) : Core a -> (a -> Core b) -> Core b
|
||||
(>>=) (MkCore act) f
|
||||
= MkCore (\oref =>
|
||||
act oref >>=
|
||||
= MkCore (act >>=
|
||||
(\x => case x of
|
||||
Left err => pure (Left err)
|
||||
Right val => runCore (f val) oref))
|
||||
Right val => runCore (f val)))
|
||||
|
||||
-- Applicative (specialised)
|
||||
export %inline
|
||||
pure : a -> Core a
|
||||
pure x = MkCore (\oref => pure (pure x))
|
||||
pure x = MkCore (pure (pure x))
|
||||
|
||||
export
|
||||
(<*>) : Core (a -> b) -> Core a -> Core b
|
||||
(<*>) (MkCore f) (MkCore a) = MkCore (\oref => [| f oref <*> a oref |])
|
||||
(<*>) (MkCore f) (MkCore a) = MkCore [| f <*> a |]
|
||||
|
||||
export %inline
|
||||
when : Bool -> Lazy (Core ()) -> Core ()
|
||||
@ -374,11 +360,10 @@ when False f = pure ()
|
||||
export
|
||||
Catchable Core Error where
|
||||
catch (MkCore prog) h
|
||||
= MkCore (\oref =>
|
||||
do p' <- prog oref
|
||||
case p' of
|
||||
Left e => let MkCore he = h e in he oref
|
||||
Right val => pure (Right val))
|
||||
= MkCore ( do p' <- prog
|
||||
case p' of
|
||||
Left e => let MkCore he = h e in he
|
||||
Right val => pure (Right val))
|
||||
throw = coreFail
|
||||
|
||||
-- Traversable (specialised)
|
||||
@ -419,71 +404,8 @@ export %inline
|
||||
put : (x : label) -> {auto ref : Ref x a} -> a -> Core ()
|
||||
put x {ref = MkRef io} val = coreLift (writeIORef io val)
|
||||
|
||||
export %inline
|
||||
getOpts : Core GlobalOpts
|
||||
getOpts = MkCore (\oref => pure (Right !(readIORef oref)))
|
||||
|
||||
export %inline
|
||||
putOpts : GlobalOpts -> Core ()
|
||||
putOpts opts = MkCore (\oref => pure (Right !(writeIORef oref opts)))
|
||||
|
||||
export
|
||||
cond : List (Lazy Bool, Lazy a) -> a -> a
|
||||
cond [] def = def
|
||||
cond ((x, y) :: xs) def = if x then y else cond xs def
|
||||
|
||||
export
|
||||
log : Nat -> Lazy String -> Core ()
|
||||
log lvl msg
|
||||
= do opts <- getOpts
|
||||
if logLevel opts >= lvl
|
||||
then coreLift $ putStrLn $ "LOG " ++ show lvl ++ ": " ++ msg
|
||||
else pure ()
|
||||
|
||||
export
|
||||
logC : Nat -> Core String -> Core ()
|
||||
logC lvl cmsg
|
||||
= do opts <- getOpts
|
||||
if logLevel opts >= lvl
|
||||
then do msg <- cmsg
|
||||
coreLift $ putStrLn $ "LOG " ++ show lvl ++ ": " ++ msg
|
||||
else pure ()
|
||||
|
||||
export
|
||||
setLogLevel : Nat -> Core ()
|
||||
setLogLevel n
|
||||
= do opts <- getOpts
|
||||
putOpts (record { logLevel = n } opts)
|
||||
|
||||
export
|
||||
setLogTimings : Bool -> Core ()
|
||||
setLogTimings b
|
||||
= do opts <- getOpts
|
||||
putOpts (record { logTimings = b } opts)
|
||||
|
||||
export
|
||||
logTime : Lazy String -> Core a -> Core a
|
||||
logTime str act
|
||||
= do opts <- getOpts
|
||||
if logTimings opts
|
||||
then do clock <- coreLift clockTime
|
||||
let nano = 1000000000
|
||||
let t = seconds clock * nano + nanoseconds clock
|
||||
res <- act
|
||||
clock <- coreLift clockTime
|
||||
let t' = seconds clock * nano + nanoseconds clock
|
||||
let time = t' - t
|
||||
assert_total $ -- We're not dividing by 0
|
||||
coreLift $ putStrLn $ "TIMING " ++ str ++ ": " ++
|
||||
show (time `div` nano) ++ "." ++
|
||||
addZeros (unpack (show ((time `mod` nano) `div` 1000000))) ++
|
||||
"s"
|
||||
pure res
|
||||
else act
|
||||
where
|
||||
addZeros : List Char -> String
|
||||
addZeros [] = "000"
|
||||
addZeros [x] = "00" ++ cast x
|
||||
addZeros [x,y] = "0" ++ cast x ++ cast y
|
||||
addZeros str = pack str
|
||||
|
||||
|
||||
@ -4,6 +4,7 @@ import Core.CaseTree
|
||||
import Core.Context
|
||||
import Core.Core
|
||||
import Core.Env
|
||||
import Core.Options
|
||||
import Core.Primitives
|
||||
import Core.TT
|
||||
import Core.Value
|
||||
@ -705,7 +706,7 @@ export
|
||||
logNF : {auto c : Ref Ctxt Defs} ->
|
||||
Nat -> Lazy String -> Env Term vars -> NF vars -> Core ()
|
||||
logNF lvl msg env tmnf
|
||||
= do opts <- getOpts
|
||||
= do opts <- getSession
|
||||
if logLevel opts >= lvl
|
||||
then do defs <- get Ctxt
|
||||
tm <- quote defs env tmnf
|
||||
@ -720,7 +721,7 @@ export
|
||||
logTermNF : {auto c : Ref Ctxt Defs} ->
|
||||
Nat -> Lazy String -> Env Term vars -> Term vars -> Core ()
|
||||
logTermNF lvl msg env tm
|
||||
= do opts <- getOpts
|
||||
= do opts <- getSession
|
||||
if logLevel opts >= lvl
|
||||
then do defs <- get Ctxt
|
||||
tmnf <- normaliseHoles defs env tm
|
||||
@ -733,7 +734,7 @@ export
|
||||
logGlue : {auto c : Ref Ctxt Defs} ->
|
||||
Nat -> Lazy String -> Env Term vars -> Glued vars -> Core ()
|
||||
logGlue lvl msg env gtm
|
||||
= do opts <- getOpts
|
||||
= do opts <- getSession
|
||||
if logLevel opts >= lvl
|
||||
then do defs <- get Ctxt
|
||||
tm <- getTerm gtm
|
||||
@ -746,7 +747,7 @@ export
|
||||
logGlueNF : {auto c : Ref Ctxt Defs} ->
|
||||
Nat -> Lazy String -> Env Term vars -> Glued vars -> Core ()
|
||||
logGlueNF lvl msg env gtm
|
||||
= do opts <- getOpts
|
||||
= do opts <- getSession
|
||||
if logLevel opts >= lvl
|
||||
then do defs <- get Ctxt
|
||||
tm <- getTerm gtm
|
||||
@ -761,7 +762,7 @@ logEnv : {vars : _} ->
|
||||
{auto c : Ref Ctxt Defs} ->
|
||||
Nat -> String -> Env Term vars -> Core ()
|
||||
logEnv lvl msg env
|
||||
= do opts <- getOpts
|
||||
= do opts <- getSession
|
||||
if logLevel opts >= lvl
|
||||
then dumpEnv env
|
||||
else pure ()
|
||||
|
||||
@ -140,6 +140,8 @@ record Session where
|
||||
constructor MkSessionOpts
|
||||
noprelude : Bool
|
||||
codegen : CG
|
||||
logLevel : Nat
|
||||
logTimings : Bool
|
||||
|
||||
public export
|
||||
record PPrinter where
|
||||
@ -167,7 +169,7 @@ defaultPPrint : PPrinter
|
||||
defaultPPrint = MkPPOpts False True False
|
||||
|
||||
defaultSession : Session
|
||||
defaultSession = MkSessionOpts False Chez
|
||||
defaultSession = MkSessionOpts False Chez 0 False
|
||||
|
||||
export
|
||||
defaults : Options
|
||||
|
||||
@ -57,6 +57,6 @@ main
|
||||
= do (_ :: fname :: rest) <- getArgs
|
||||
| _ => do putStrLn usage
|
||||
exitWith (ExitFailure 1)
|
||||
coreRun defaultOpts (coreMain fname rest)
|
||||
coreRun (coreMain fname rest)
|
||||
(\err : Error => putStrLn ("Uncaught error: " ++ show err))
|
||||
(\res => pure ())
|
||||
|
||||
Loading…
Reference in New Issue
Block a user