mirror of
https://github.com/idris-lang/Idris2.git
synced 2024-09-19 17:27:21 +03:00
[ cleanup ] logging (#1442)
Co-authored-by: Guillaume ALLAIS <guillaume.allais@ens-lyon.org>
This commit is contained in:
Zoe Stafford
GitHub
parent
5aef7a2dff
commit
50d75cc3a4
@ -2,6 +2,7 @@ module Core.Context.Log
|
||||
|
||||
import Core.Context
|
||||
import Core.Options
|
||||
import Data.Strings
|
||||
|
||||
import Libraries.Data.StringMap
|
||||
|
||||
@ -9,7 +10,45 @@ import System.Clock
|
||||
|
||||
%default covering
|
||||
|
||||
-- Log message with a term, translating back to human readable names first
|
||||
-- if this function is called, then logging must be enabled.
|
||||
%inline
|
||||
export
|
||||
logString : String -> Nat -> String -> Core ()
|
||||
logString "" n msg = coreLift $ putStrLn
|
||||
$ "LOG " ++ show n ++ ": " ++ msg
|
||||
logString str n msg = coreLift $ putStrLn
|
||||
$ "LOG " ++ str ++ ":" ++ show n ++ ": " ++ msg
|
||||
|
||||
%inline
|
||||
export
|
||||
logString' : LogLevel -> String -> Core ()
|
||||
logString' lvl =
|
||||
logString (fastAppend (intersperse "." (topics lvl)) ++ ":")
|
||||
(verbosity lvl)
|
||||
|
||||
export
|
||||
logging' : {auto c : Ref Ctxt Defs} ->
|
||||
LogLevel -> Core Bool
|
||||
logging' lvl = do
|
||||
opts <- getSession
|
||||
pure $ verbosity lvl == 0 || (logEnabled opts && keepLog lvl (logLevel opts))
|
||||
|
||||
export
|
||||
unverifiedLogging : {auto c : Ref Ctxt Defs} ->
|
||||
String -> Nat -> Core Bool
|
||||
unverifiedLogging str Z = pure True
|
||||
unverifiedLogging str n = do
|
||||
opts <- getSession
|
||||
pure $ logEnabled opts && keepLog (mkUnverifiedLogLevel str n) (logLevel opts)
|
||||
|
||||
%inline
|
||||
export
|
||||
logging : {auto c : Ref Ctxt Defs} ->
|
||||
(s : String) -> {auto 0 _ : KnownTopic s} ->
|
||||
Nat -> Core Bool
|
||||
logging str n = unverifiedLogging str n
|
||||
|
||||
||| Log message with a term, translating back to human readable names first.
|
||||
export
|
||||
logTerm : {vars : _} ->
|
||||
{auto c : Ref Ctxt Defs} ->
|
||||
@ -17,21 +56,16 @@ logTerm : {vars : _} ->
|
||||
{auto 0 _ : KnownTopic s} ->
|
||||
Nat -> Lazy String -> Term vars -> Core ()
|
||||
logTerm str n msg tm
|
||||
= do opts <- getSession
|
||||
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'
|
||||
else pure ()
|
||||
= when !(logging str n)
|
||||
$ do tm' <- toFullNames tm
|
||||
logString str n $ msg ++ ": " ++ show tm'
|
||||
|
||||
export
|
||||
log' : {auto c : Ref Ctxt Defs} ->
|
||||
LogLevel -> Lazy String -> Core ()
|
||||
log' lvl msg
|
||||
= do opts <- getSession
|
||||
if keepLog lvl (logEnabled opts) (logLevel opts)
|
||||
then coreLift $ putStrLn $ "LOG " ++ show lvl ++ ": " ++ msg
|
||||
else pure ()
|
||||
= when !(logging' lvl)
|
||||
$ logString' lvl msg
|
||||
|
||||
||| Log a message with the given log level. Use increasingly
|
||||
||| high log level numbers for more granular logging.
|
||||
@ -41,21 +75,19 @@ log : {auto c : Ref Ctxt Defs} ->
|
||||
{auto 0 _ : KnownTopic s} ->
|
||||
Nat -> Lazy String -> Core ()
|
||||
log str n msg
|
||||
= do let lvl = mkLogLevel (logEnabled !getSession) str n
|
||||
log' lvl msg
|
||||
= when !(logging str n)
|
||||
$ logString str n msg
|
||||
|
||||
export
|
||||
unverifiedLogC : {auto c : Ref Ctxt Defs} ->
|
||||
(s : String) ->
|
||||
Nat -> Core String -> Core ()
|
||||
unverifiedLogC str n cmsg
|
||||
= do opts <- getSession
|
||||
let lvl = mkUnverifiedLogLevel (logEnabled opts) str n
|
||||
if keepLog lvl (logEnabled opts) (logLevel opts)
|
||||
then do msg <- cmsg
|
||||
coreLift $ putStrLn $ "LOG " ++ show lvl ++ ": " ++ msg
|
||||
else pure ()
|
||||
= when !(unverifiedLogging str n)
|
||||
$ do msg <- cmsg
|
||||
logString str n msg
|
||||
|
||||
%inline
|
||||
export
|
||||
logC : {auto c : Ref Ctxt Defs} ->
|
||||
(s : String) ->
|
||||
@ -63,11 +95,16 @@ logC : {auto c : Ref Ctxt Defs} ->
|
||||
Nat -> Core String -> Core ()
|
||||
logC str = unverifiedLogC str
|
||||
|
||||
nano : Integer
|
||||
nano = 1000000000
|
||||
|
||||
micro : Integer
|
||||
micro = 1000000
|
||||
|
||||
export
|
||||
logTimeOver : Integer -> Core String -> Core a -> Core a
|
||||
logTimeOver nsecs str act
|
||||
= do clock <- coreLift (clockTime Process)
|
||||
let nano = 1000000000
|
||||
let t = seconds clock * nano + nanoseconds clock
|
||||
res <- act
|
||||
clock <- coreLift (clockTime Process)
|
||||
@ -78,7 +115,7 @@ logTimeOver nsecs str act
|
||||
do str' <- str
|
||||
coreLift $ putStrLn $ "TIMING " ++ str' ++ ": " ++
|
||||
show (time `div` nano) ++ "." ++
|
||||
addZeros (unpack (show ((time `mod` nano) `div` 1000000))) ++
|
||||
addZeros (unpack (show ((time `mod` nano) `div` micro))) ++
|
||||
"s"
|
||||
pure res
|
||||
where
|
||||
@ -94,7 +131,6 @@ logTimeWhen : {auto c : Ref Ctxt Defs} ->
|
||||
logTimeWhen p str act
|
||||
= if p
|
||||
then do clock <- coreLift (clockTime Process)
|
||||
let nano = 1000000000
|
||||
let t = seconds clock * nano + nanoseconds clock
|
||||
res <- act
|
||||
clock <- coreLift (clockTime Process)
|
||||
@ -103,7 +139,7 @@ logTimeWhen p str act
|
||||
assert_total $ -- We're not dividing by 0
|
||||
coreLift $ putStrLn $ "TIMING " ++ str ++ ": " ++
|
||||
show (time `div` nano) ++ "." ++
|
||||
addZeros (unpack (show ((time `mod` nano) `div` 1000000))) ++
|
||||
addZeros (unpack (show ((time `mod` nano) `div` micro))) ++
|
||||
"s"
|
||||
pure res
|
||||
else act
|
||||
@ -118,7 +154,6 @@ logTimeRecord' : {auto c : Ref Ctxt Defs} ->
|
||||
String -> Core a -> Core a
|
||||
logTimeRecord' key act
|
||||
= do clock <- coreLift (clockTime Process)
|
||||
let nano = 1000000000
|
||||
let t = seconds clock * nano + nanoseconds clock
|
||||
res <- act
|
||||
clock <- coreLift (clockTime Process)
|
||||
@ -163,10 +198,9 @@ showTimeRecord
|
||||
showTimeLog : (String, (Bool, Integer)) -> Core ()
|
||||
showTimeLog (key, (_, time))
|
||||
= do coreLift $ putStr (key ++ ": ")
|
||||
let nano = 1000000000
|
||||
assert_total $ -- We're not dividing by 0
|
||||
coreLift $ putStrLn $ show (time `div` nano) ++ "." ++
|
||||
addZeros (unpack (show ((time `mod` nano) `div` 1000000))) ++
|
||||
addZeros (unpack (show ((time `mod` nano) `div` micro))) ++
|
||||
"s"
|
||||
|
||||
export
|
||||
|
||||
@ -1200,29 +1200,25 @@ logNF : {vars : _} ->
|
||||
{auto 0 _ : KnownTopic s} ->
|
||||
Nat -> Lazy String -> Env Term vars -> NF vars -> Core ()
|
||||
logNF str n msg env tmnf
|
||||
= do opts <- getSession
|
||||
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
|
||||
coreLift $ putStrLn $ "LOG " ++ show lvl ++ ": " ++ msg
|
||||
++ ": " ++ show tm'
|
||||
= when !(logging str n) $
|
||||
do defs <- get Ctxt
|
||||
tm <- quote defs env tmnf
|
||||
tm' <- toFullNames tm
|
||||
logString str n (msg ++ ": " ++ show tm')
|
||||
|
||||
-- Log message with a term, reducing holes and translating back to human
|
||||
-- readable names first
|
||||
export
|
||||
logTermNF' : {vars : _} ->
|
||||
{auto c : Ref Ctxt Defs} ->
|
||||
LogLevel -> Lazy String -> Env Term vars -> Term vars -> Core ()
|
||||
logTermNF' lvl msg env tm
|
||||
= do opts <- getSession
|
||||
when (keepLog lvl (logEnabled opts) (logLevel opts)) $
|
||||
do defs <- get Ctxt
|
||||
tmnf <- normaliseHoles defs env tm
|
||||
tm' <- toFullNames tmnf
|
||||
coreLift $ putStrLn $ "LOG " ++ show lvl ++ ": " ++ msg
|
||||
++ ": " ++ show tm'
|
||||
(s : String) ->
|
||||
{auto 0 _ : KnownTopic s} ->
|
||||
Nat -> Lazy String -> Env Term vars -> Term vars -> Core ()
|
||||
logTermNF' str n msg env tm
|
||||
= do defs <- get Ctxt
|
||||
tmnf <- normaliseHoles defs env tm
|
||||
tm' <- toFullNames tmnf
|
||||
logString str n (msg ++ ": " ++ show tm')
|
||||
|
||||
export
|
||||
logTermNF : {vars : _} ->
|
||||
@ -1231,8 +1227,7 @@ logTermNF : {vars : _} ->
|
||||
{auto 0 _ : KnownTopic s} ->
|
||||
Nat -> Lazy String -> Env Term vars -> Term vars -> Core ()
|
||||
logTermNF str n msg env tm
|
||||
= do let lvl = mkLogLevel (logEnabled !getSession) str n
|
||||
logTermNF' lvl msg env tm
|
||||
= when !(logging str n) $ logTermNF' str n msg env tm
|
||||
|
||||
export
|
||||
logGlue : {vars : _} ->
|
||||
@ -1241,14 +1236,11 @@ logGlue : {vars : _} ->
|
||||
{auto 0 _ : KnownTopic s} ->
|
||||
Nat -> Lazy String -> Env Term vars -> Glued vars -> Core ()
|
||||
logGlue str n msg env gtm
|
||||
= do opts <- getSession
|
||||
let lvl = mkLogLevel (logEnabled opts) str n
|
||||
when (keepLog lvl (logEnabled opts) (logLevel opts)) $
|
||||
do defs <- get Ctxt
|
||||
tm <- getTerm gtm
|
||||
tm' <- toFullNames tm
|
||||
coreLift $ putStrLn $ "LOG " ++ show lvl ++ ": " ++ msg
|
||||
++ ": " ++ show tm'
|
||||
= when !(logging str n) $
|
||||
do defs <- get Ctxt
|
||||
tm <- getTerm gtm
|
||||
tm' <- toFullNames tm
|
||||
logString str n (msg ++ ": " ++ show tm')
|
||||
|
||||
export
|
||||
logGlueNF : {vars : _} ->
|
||||
@ -1257,15 +1249,12 @@ logGlueNF : {vars : _} ->
|
||||
{auto 0 _ : KnownTopic s} ->
|
||||
Nat -> Lazy String -> Env Term vars -> Glued vars -> Core ()
|
||||
logGlueNF str n msg env gtm
|
||||
= do opts <- getSession
|
||||
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
|
||||
tm' <- toFullNames tmnf
|
||||
coreLift $ putStrLn $ "LOG " ++ show lvl ++ ": " ++ msg
|
||||
++ ": " ++ show tm'
|
||||
= when !(logging str n) $
|
||||
do defs <- get Ctxt
|
||||
tm <- getTerm gtm
|
||||
tmnf <- normaliseHoles defs env tm
|
||||
tm' <- toFullNames tmnf
|
||||
logString str n (msg ++ ": " ++ show tm')
|
||||
|
||||
export
|
||||
logEnv : {vars : _} ->
|
||||
@ -1274,27 +1263,22 @@ logEnv : {vars : _} ->
|
||||
{auto 0 _ : KnownTopic s} ->
|
||||
Nat -> String -> Env Term vars -> Core ()
|
||||
logEnv str n msg env
|
||||
= do opts <- getSession
|
||||
when (logEnabled opts &&
|
||||
keepLog lvl (logEnabled opts) (logLevel opts)) $ do
|
||||
coreLift (putStrLn $ "LOG " ++ show lvl ++ ": " ++ msg)
|
||||
= when !(logging str n) $
|
||||
do logString str n msg
|
||||
dumpEnv env
|
||||
|
||||
where
|
||||
lvl : LogLevel
|
||||
lvl = mkLogLevel True str n
|
||||
|
||||
dumpEnv : {vs : List Name} -> Env Term vs -> Core ()
|
||||
dumpEnv [] = pure ()
|
||||
dumpEnv {vs = x :: _} (Let _ c val ty :: bs)
|
||||
= do logTermNF' lvl (msg ++ ": let " ++ show x) bs val
|
||||
logTermNF' lvl (msg ++ ":" ++ show c ++ " " ++
|
||||
show x) bs ty
|
||||
= do logTermNF' str n (msg ++ ": let " ++ show x) bs val
|
||||
logTermNF' str n (msg ++ ":" ++ show c ++ " " ++ show x) bs ty
|
||||
dumpEnv bs
|
||||
dumpEnv {vs = x :: _} (b :: bs)
|
||||
= do logTermNF' lvl (msg ++ ":" ++ show (multiplicity b) ++ " " ++
|
||||
show (piInfo b) ++ " " ++
|
||||
show x) bs (binderType b)
|
||||
= do logTermNF' str n (msg ++ ":" ++ show (multiplicity b) ++ " " ++
|
||||
show (piInfo b) ++ " " ++
|
||||
show x) bs (binderType b)
|
||||
dumpEnv bs
|
||||
replace' : {auto c : Ref Ctxt Defs} ->
|
||||
{vars : _} ->
|
||||
|
||||
@ -184,16 +184,15 @@ mkLogLevel' ps n = MkLogLevel (maybe [] forget ps) n
|
||||
||| Use this function to create user defined loglevels, for instance, during
|
||||
||| elaborator reflection.
|
||||
export
|
||||
mkUnverifiedLogLevel : Bool -> (s : String) -> Nat -> LogLevel
|
||||
mkUnverifiedLogLevel False _ = mkLogLevel' Nothing
|
||||
mkUnverifiedLogLevel _ "" = mkLogLevel' Nothing
|
||||
mkUnverifiedLogLevel _ ps = mkLogLevel' (Just (split (== '.') ps))
|
||||
mkUnverifiedLogLevel : (s : String) -> Nat -> LogLevel
|
||||
mkUnverifiedLogLevel "" = mkLogLevel' Nothing
|
||||
mkUnverifiedLogLevel ps = mkLogLevel' (Just (split (== '.') ps))
|
||||
|
||||
||| Like `mkUnverifiedLogLevel` but with a compile time check that
|
||||
||| the passed string is a known topic.
|
||||
export
|
||||
mkLogLevel : Bool -> (s : String) -> {auto 0 _ : KnownTopic s} -> Nat -> LogLevel
|
||||
mkLogLevel b s = mkUnverifiedLogLevel b s
|
||||
mkLogLevel : (s : String) -> {auto 0 _ : KnownTopic s} -> Nat -> LogLevel
|
||||
mkLogLevel s = mkUnverifiedLogLevel s
|
||||
|
||||
||| The unsafe constructor should only be used in places where the topic has already
|
||||
||| been appropriately processed.
|
||||
@ -239,7 +238,7 @@ parseLogLevel str = do
|
||||
ns = tail nns in
|
||||
case ns of
|
||||
[] => pure (MkLogLevel [], n)
|
||||
[ns] => pure (mkUnverifiedLogLevel True n, ns)
|
||||
[ns] => pure (mkUnverifiedLogLevel n, ns)
|
||||
_ => Nothing
|
||||
lvl <- parsePositive n
|
||||
pure $ c (fromInteger lvl)
|
||||
@ -268,9 +267,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 -> Bool -> LogLevels -> Bool
|
||||
keepLog (MkLogLevel _ Z) _ _ = True
|
||||
keepLog (MkLogLevel path n) enabled levels = enabled && go path levels where
|
||||
keepLog : LogLevel -> LogLevels -> Bool
|
||||
keepLog (MkLogLevel _ Z) _ = True
|
||||
keepLog (MkLogLevel path n) levels = go path levels where
|
||||
|
||||
go : List String -> StringTrie Nat -> Bool
|
||||
go path (MkStringTrie current) = here || there where
|
||||
|
||||
@ -623,64 +623,70 @@ checkNoGuards : {auto u : Ref UST UState} ->
|
||||
checkNoGuards = checkUserHoles False
|
||||
|
||||
export
|
||||
dumpHole' : {auto u : Ref UST UState} ->
|
||||
{auto c : Ref Ctxt Defs} ->
|
||||
LogLevel -> (hole : Int) -> Core ()
|
||||
dumpHole' lvl hole
|
||||
dumpHole : {auto u : Ref UST UState} ->
|
||||
{auto c : Ref Ctxt Defs} ->
|
||||
(s : String) ->
|
||||
{auto 0 _ : KnownTopic s} ->
|
||||
Nat -> (hole : Int) -> Core ()
|
||||
dumpHole str n hole
|
||||
= do ust <- get UST
|
||||
defs <- get Ctxt
|
||||
sopts <- getSession
|
||||
when (keepLog lvl (logEnabled sopts) (logLevel sopts)) $ do
|
||||
defs <- get Ctxt
|
||||
case !(lookupCtxtExact (Resolved hole) (gamma defs)) of
|
||||
Nothing => pure ()
|
||||
Just gdef => case (definition gdef, type gdef) of
|
||||
(Guess tm envb constraints, ty) =>
|
||||
do log' lvl $ "!" ++ show !(getFullName (Resolved hole)) ++ " : " ++
|
||||
show !(toFullNames !(normaliseHoles defs [] ty))
|
||||
log' lvl $ "\t = " ++ show !(normaliseHoles defs [] tm)
|
||||
++ "\n\twhen"
|
||||
traverse_ dumpConstraint constraints
|
||||
(Hole _ p, ty) =>
|
||||
log' lvl $ "?" ++ show (fullname gdef) ++ " : " ++
|
||||
show !(normaliseHoles defs [] ty)
|
||||
++ if implbind p then " (ImplBind)" else ""
|
||||
++ if invertible gdef then " (Invertible)" else ""
|
||||
(BySearch _ _ _, ty) =>
|
||||
log' lvl $ "Search " ++ show hole ++ " : " ++
|
||||
show !(toFullNames !(normaliseHoles defs [] ty))
|
||||
(PMDef _ args t _ _, ty) =>
|
||||
log' (withVerbosity 4 lvl) $
|
||||
"Solved: " ++ show hole ++ " : " ++
|
||||
show !(normalise defs [] ty) ++
|
||||
" = " ++ show !(normalise defs [] (Ref emptyFC Func (Resolved hole)))
|
||||
(ImpBind, ty) =>
|
||||
log' (withVerbosity 4 lvl) $
|
||||
"Bound: " ++ show hole ++ " : " ++
|
||||
show !(normalise defs [] ty)
|
||||
(Delayed, ty) =>
|
||||
log' (withVerbosity 4 lvl) $
|
||||
"Delayed elaborator : " ++
|
||||
show !(normalise defs [] ty)
|
||||
_ => pure ()
|
||||
defs <- get Ctxt
|
||||
case !(lookupCtxtExact (Resolved hole) (gamma defs)) of
|
||||
Nothing => pure ()
|
||||
Just gdef => case (definition gdef, type gdef) of
|
||||
(Guess tm envb constraints, ty) =>
|
||||
do logString str n $
|
||||
"!" ++ show !(getFullName (Resolved hole)) ++ " : "
|
||||
++ show !(toFullNames !(normaliseHoles defs [] ty))
|
||||
++ "\n\t = "
|
||||
++ show !(normaliseHoles defs [] tm)
|
||||
++ "\n\twhen"
|
||||
traverse_ dumpConstraint constraints
|
||||
(Hole _ p, ty) =>
|
||||
logString str n $
|
||||
"?" ++ show (fullname gdef) ++ " : "
|
||||
++ show !(normaliseHoles defs [] ty)
|
||||
++ if implbind p then " (ImplBind)" else ""
|
||||
++ if invertible gdef then " (Invertible)" else ""
|
||||
(BySearch _ _ _, ty) =>
|
||||
logString str n $
|
||||
"Search " ++ show hole ++ " : " ++
|
||||
show !(toFullNames !(normaliseHoles defs [] ty))
|
||||
(PMDef _ args t _ _, ty) =>
|
||||
log str 4 $
|
||||
"Solved: " ++ show hole ++ " : " ++
|
||||
show !(normalise defs [] ty) ++
|
||||
" = " ++ show !(normalise defs [] (Ref emptyFC Func (Resolved hole)))
|
||||
(ImpBind, ty) =>
|
||||
log str 4 $
|
||||
"Bound: " ++ show hole ++ " : " ++
|
||||
show !(normalise defs [] ty)
|
||||
(Delayed, ty) =>
|
||||
log str 4 $
|
||||
"Delayed elaborator : " ++
|
||||
show !(normalise defs [] ty)
|
||||
_ => pure ()
|
||||
where
|
||||
dumpConstraint : Int -> Core ()
|
||||
dumpConstraint n
|
||||
dumpConstraint cid
|
||||
= do ust <- get UST
|
||||
defs <- get Ctxt
|
||||
case lookup n (constraints ust) of
|
||||
case lookup cid (constraints ust) of
|
||||
Nothing => pure ()
|
||||
Just Resolved => log' lvl "\tResolved"
|
||||
Just Resolved => logString str n "\tResolved"
|
||||
Just (MkConstraint _ lazy env x y) =>
|
||||
do log' lvl $ "\t " ++ show !(toFullNames !(quote defs env x))
|
||||
++ " =?= " ++ show !(toFullNames !(quote defs env y))
|
||||
do logString str n $
|
||||
"\t " ++ show !(toFullNames !(quote defs env x))
|
||||
++ " =?= " ++ show !(toFullNames !(quote defs env y))
|
||||
empty <- clearDefs defs
|
||||
log' (withVerbosity 5 lvl)
|
||||
$ "\t from " ++ show !(toFullNames !(quote empty env x))
|
||||
++ " =?= " ++ show !(toFullNames !(quote empty env y)) ++
|
||||
if lazy then "\n\t(lazy allowed)" else ""
|
||||
log str 5 $
|
||||
"\t from " ++ show !(toFullNames !(quote empty env x))
|
||||
++ " =?= " ++ show !(toFullNames !(quote empty env y))
|
||||
++ if lazy then "\n\t(lazy allowed)" else ""
|
||||
Just (MkSeqConstraint _ _ xs ys) =>
|
||||
log' lvl $ "\t\t" ++ show xs ++ " =?= " ++ show ys
|
||||
logString str n $ "\t\t" ++ show xs ++ " =?= " ++ show ys
|
||||
|
||||
export
|
||||
dumpConstraints : {auto u : Ref UST UState} ->
|
||||
@ -694,11 +700,9 @@ dumpConstraints str n all
|
||||
= do ust <- get UST
|
||||
defs <- get Ctxt
|
||||
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
|
||||
[] => pure ()
|
||||
_ => do log' lvl "--- CONSTRAINTS AND HOLES ---"
|
||||
traverse_ (dumpHole' lvl) (map fst hs)
|
||||
when !(logging str n) $ do
|
||||
let hs = toList (guesses ust) ++
|
||||
toList (if all then holes ust else currentHoles ust)
|
||||
unless (isNil hs) $
|
||||
do logString str n "--- CONSTRAINTS AND HOLES ---"
|
||||
traverse_ (dumpHole str n) (map fst hs)
|
||||
|
||||
@ -1179,9 +1179,5 @@ logRaw : {auto c : Ref Ctxt Defs} ->
|
||||
{auto 0 _ : KnownTopic s} ->
|
||||
Nat -> Lazy String -> RawImp -> Core ()
|
||||
logRaw str n msg tm
|
||||
= do opts <- getSession
|
||||
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 ()
|
||||
= when !(logging str n) $
|
||||
do logString str n (msg ++ ": " ++ show tm)
|
||||
|
||||
Loading…
Reference in New Issue
Block a user