Compare commits
12 Commits
2de2bd1f04
...
8b8bec250a
Author | SHA1 | Date |
---|---|---|
rhiannon morris | 8b8bec250a | |
rhiannon morris | 103700d882 | |
rhiannon morris | 642ac25a71 | |
rhiannon morris | 05a688d49e | |
rhiannon morris | 1c8c50f3e2 | |
rhiannon morris | f337625801 | |
rhiannon morris | 1f01cec322 | |
rhiannon morris | 103f019dbd | |
rhiannon morris | 2cafb35bc1 | |
rhiannon morris | 47069a9316 | |
rhiannon morris | fb14b756c7 | |
rhiannon morris | 81783dbae0 |
|
@ -69,7 +69,8 @@ withLogFile : Options ->
|
|||
(IORef LevelStack -> OpenFile -> IO (Either Error a)) ->
|
||||
IO (Either Error a)
|
||||
withLogFile opts act = do
|
||||
withOutFile CErr opts.logFile fromError $ act !(newIORef initStack)
|
||||
lvlStack <- newIORef $ singleton opts.logLevels
|
||||
withOutFile CErr opts.logFile fromError $ act lvlStack
|
||||
where
|
||||
fromError : String -> FileError -> IO (Either Error a)
|
||||
fromError file err = pure $ Left $ WriteError file err
|
||||
|
|
|
@ -156,7 +156,7 @@ splitLogFlag = traverse flag1 . toList . split (== ':') where
|
|||
case strM second of
|
||||
StrCons '=' lvl => do
|
||||
cat <- parseLogCategory first
|
||||
lvl <- parseLogLevel second
|
||||
lvl <- parseLogLevel lvl
|
||||
pure (Just cat, lvl)
|
||||
StrNil => (Nothing,) <$> parseLogLevel first
|
||||
_ => Left "invalid log flag \{str}"
|
||||
|
@ -164,7 +164,7 @@ splitLogFlag = traverse flag1 . toList . split (== ':') where
|
|||
private
|
||||
setLogFlag : LogLevels -> (Maybe LogCategory, LogLevel) -> LogLevels
|
||||
setLogFlag lvls (Nothing, lvl) = {defLevel := lvl} lvls
|
||||
setLogFlag lvls (Just name, lvl) = {levels $= insert name lvl} lvls
|
||||
setLogFlag lvls (Just name, lvl) = {levels $= ((name, lvl) ::)} lvls
|
||||
|
||||
private
|
||||
logFlag : String -> OptAction
|
||||
|
|
|
@ -62,3 +62,17 @@ export %inline HasST (STErr e) where liftST = STE . map Right
|
|||
export
|
||||
stLeft : e -> STErr e s a
|
||||
stLeft e = STE $ pure $ Left e
|
||||
|
||||
|
||||
parameters {auto _ : HasST m}
|
||||
export %inline
|
||||
readSTRef' : STRef s a -> m s a
|
||||
readSTRef' r = liftST $ ST.readSTRef r
|
||||
|
||||
export %inline
|
||||
writeSTRef' : STRef s a -> a -> m s ()
|
||||
writeSTRef' r x = liftST $ ST.writeSTRef r x
|
||||
|
||||
export %inline
|
||||
modifySTRef' : STRef s a -> (a -> a) -> m s ()
|
||||
modifySTRef' r f = liftST $ ST.modifySTRef r f
|
||||
|
|
|
@ -86,12 +86,13 @@ isEmptyNoLog :
|
|||
Definitions -> EqContext n -> SQty -> Term 0 n -> Eff EqualInner Bool
|
||||
|
||||
isEmpty defs ctx sg ty = do
|
||||
say "equal" logLevel "isEmpty"
|
||||
say "equal" 95 $ hsep ["ctx =", runPretty $ prettyEqContext ctx]
|
||||
say "equal" 95 $ hsep ["sg =", runPretty $ prettyQty sg.qty]
|
||||
say "equal" logLevel $ hsep ["ty =", runPretty $ prettyTerm [<] ctx.tnames ty]
|
||||
say "equal" logLevel ty.loc "isEmpty"
|
||||
say "equal" 95 ty.loc $ hsep ["ctx =", runPretty $ prettyEqContext ctx]
|
||||
say "equal" 95 ty.loc $ hsep ["sg =", runPretty $ prettyQty sg.qty]
|
||||
say "equal" logLevel ty.loc $
|
||||
hsep ["ty =", runPretty $ prettyTerm [<] ctx.tnames ty]
|
||||
res <- isEmptyNoLog defs ctx sg ty
|
||||
say "equal" logLevel $ hsep ["isEmpty ⇝", pshow res]
|
||||
say "equal" logLevel ty.loc $ hsep ["isEmpty ⇝", pshow res]
|
||||
pure res
|
||||
|
||||
isEmptyNoLog defs ctx sg ty0 = do
|
||||
|
@ -134,12 +135,13 @@ isSubSingNoLog :
|
|||
Definitions -> EqContext n -> SQty -> Term 0 n -> Eff EqualInner Bool
|
||||
|
||||
isSubSing defs ctx sg ty = do
|
||||
say "equal" logLevel "isSubSing"
|
||||
say "equal" 95 $ hsep ["ctx =", runPretty $ prettyEqContext ctx]
|
||||
say "equal" 95 $ hsep ["sg =", runPretty $ prettyQty sg.qty]
|
||||
say "equal" logLevel $ hsep ["ty =", runPretty $ prettyTerm [<] ctx.tnames ty]
|
||||
say "equal" logLevel ty.loc "isSubSing"
|
||||
say "equal" 95 ty.loc $ hsep ["ctx =", runPretty $ prettyEqContext ctx]
|
||||
say "equal" 95 ty.loc $ hsep ["sg =", runPretty $ prettyQty sg.qty]
|
||||
say "equal" logLevel ty.loc $
|
||||
hsep ["ty =", runPretty $ prettyTerm [<] ctx.tnames ty]
|
||||
res <- isSubSingNoLog defs ctx sg ty
|
||||
say "equal" logLevel $ hsep ["isSubsing ⇝", pshow res]
|
||||
say "equal" logLevel ty.loc $ hsep ["isSubsing ⇝", pshow res]
|
||||
pure res
|
||||
|
||||
isSubSingNoLog defs ctx sg ty0 = do
|
||||
|
@ -180,9 +182,10 @@ ensureTyConNoLog loc ctx ty = do
|
|||
Right n => throw $ NotType loc (toTyContext ctx) (ty // shift0 ctx.dimLen)
|
||||
|
||||
ensureTyCon loc ctx ty = do
|
||||
say "equal" 60 "ensureTyCon"
|
||||
say "equal" 95 $ hsep ["ctx =", runPretty $ prettyEqContext ctx]
|
||||
say "equal" 60 $ hsep ["ty =", runPretty $ prettyTerm [<] ctx.tnames ty]
|
||||
say "equal" 60 ty.loc "ensureTyCon"
|
||||
say "equal" 95 ty.loc $ hsep ["ctx =", runPretty $ prettyEqContext ctx]
|
||||
say "equal" 60 ty.loc $
|
||||
hsep ["ty =", runPretty $ prettyTerm [<] ctx.tnames ty]
|
||||
ensureTyConNoLog loc ctx ty
|
||||
|
||||
|
||||
|
@ -805,13 +808,14 @@ namespace Term
|
|||
compare0' defs ctx sg ty' s' t'
|
||||
|
||||
compare0 defs ctx sg ty s t = do
|
||||
say "equal" 30 "Term.compare0"
|
||||
say "equal" 30 $ hsep ["mode =", pshow !mode]
|
||||
say "equal" 95 $ hsep ["ctx =", runPretty $ prettyEqContext ctx]
|
||||
say "equal" 95 $ hsep ["sg =", runPretty $ prettyQty sg.qty]
|
||||
say "equal" 31 $ hsep ["ty =", runPretty $ prettyTerm [<] ctx.tnames ty]
|
||||
say "equal" 30 $ hsep ["s =", runPretty $ prettyTerm [<] ctx.tnames s]
|
||||
say "equal" 30 $ hsep ["t =", runPretty $ prettyTerm [<] ctx.tnames t]
|
||||
say "equal" 30 s.loc "Term.compare0"
|
||||
say "equal" 30 s.loc $ hsep ["mode =", pshow !mode]
|
||||
say "equal" 95 s.loc $ hsep ["ctx =", runPretty $ prettyEqContext ctx]
|
||||
say "equal" 95 s.loc $ hsep ["sg =", runPretty $ prettyQty sg.qty]
|
||||
say "equal" 31 s.loc $
|
||||
hsep ["ty =", runPretty $ prettyTerm [<] ctx.tnames ty]
|
||||
say "equal" 30 s.loc $ hsep ["s =", runPretty $ prettyTerm [<] ctx.tnames s]
|
||||
say "equal" 30 s.loc $ hsep ["t =", runPretty $ prettyTerm [<] ctx.tnames t]
|
||||
compare0NoLog defs ctx sg ty s t
|
||||
|
||||
namespace Elim
|
||||
|
@ -824,14 +828,15 @@ namespace Elim
|
|||
maybe (pure ty) throw err
|
||||
|
||||
compare0 defs ctx sg e f = do
|
||||
say "equal" 30 "Elim.compare0"
|
||||
say "equal" 30 $ hsep ["mode =", pshow !mode]
|
||||
say "equal" 95 $ hsep ["ctx =", runPretty $ prettyEqContext ctx]
|
||||
say "equal" 95 $ hsep ["sg =", runPretty $ prettyQty sg.qty]
|
||||
say "equal" 30 $ hsep ["e =", runPretty $ prettyElim [<] ctx.tnames e]
|
||||
say "equal" 30 $ hsep ["f =", runPretty $ prettyElim [<] ctx.tnames f]
|
||||
say "equal" 30 e.loc "Elim.compare0"
|
||||
say "equal" 30 e.loc $ hsep ["mode =", pshow !mode]
|
||||
say "equal" 95 e.loc $ hsep ["ctx =", runPretty $ prettyEqContext ctx]
|
||||
say "equal" 95 e.loc $ hsep ["sg =", runPretty $ prettyQty sg.qty]
|
||||
say "equal" 30 e.loc $ hsep ["e =", runPretty $ prettyElim [<] ctx.tnames e]
|
||||
say "equal" 30 e.loc $ hsep ["f =", runPretty $ prettyElim [<] ctx.tnames f]
|
||||
ty <- compare0NoLog defs ctx sg e f
|
||||
say "equal" 31 $ hsep ["ty ⇝", runPretty $ prettyTerm [<] ctx.tnames ty]
|
||||
say "equal" 31 e.loc $
|
||||
hsep ["ty ⇝", runPretty $ prettyTerm [<] ctx.tnames ty]
|
||||
pure ty
|
||||
|
||||
export covering %inline
|
||||
|
@ -846,11 +851,11 @@ compareTypeNoLog defs ctx s t = do
|
|||
compareType' defs ctx s' t'
|
||||
|
||||
compareType defs ctx s t = do
|
||||
say "equal" 30 "compareType"
|
||||
say "equal" 30 $ hsep ["mode =", pshow !mode]
|
||||
say "equal" 95 $ hsep ["ctx =", runPretty $ prettyEqContext ctx]
|
||||
say "equal" 30 $ hsep ["s =", runPretty $ prettyTerm [<] ctx.tnames s]
|
||||
say "equal" 30 $ hsep ["t =", runPretty $ prettyTerm [<] ctx.tnames t]
|
||||
say "equal" 30 s.loc "compareType"
|
||||
say "equal" 30 s.loc $ hsep ["mode =", pshow !mode]
|
||||
say "equal" 95 s.loc $ hsep ["ctx =", runPretty $ prettyEqContext ctx]
|
||||
say "equal" 30 s.loc $ hsep ["s =", runPretty $ prettyTerm [<] ctx.tnames s]
|
||||
say "equal" 30 s.loc $ hsep ["t =", runPretty $ prettyTerm [<] ctx.tnames t]
|
||||
compareTypeNoLog defs ctx s t
|
||||
|
||||
|
||||
|
@ -874,10 +879,10 @@ parameters (loc : Loc) (ctx : TyContext d n)
|
|||
fromInner = lift . map fst . runState mode
|
||||
|
||||
private
|
||||
eachCorner : Has Log fs => FreeVars d ->
|
||||
(EqContext n -> DSubst d 0 -> Eff fs ()) -> Eff fs ()
|
||||
eachCorner fvs act = do
|
||||
say "equal" 50 $
|
||||
eachCorner : Has Log fs => Loc -> FreeVars d ->
|
||||
(EqContext n -> DSubst d 0 -> Eff fs ()) -> Eff fs ()
|
||||
eachCorner loc fvs act = do
|
||||
say "equal" 50 loc $
|
||||
hsep $ "eachCorner: split on" :: map prettyBind' (getVars ctx fvs)
|
||||
for_ (splits loc ctx.dctx fvs) $ \th =>
|
||||
act (makeEqContext ctx th) th
|
||||
|
@ -888,8 +893,8 @@ parameters (loc : Loc) (ctx : TyContext d n)
|
|||
Definitions -> EqContext n -> DSubst d 0 -> Eff EqualInner ()
|
||||
|
||||
private
|
||||
runCompare : FreeVars d -> CompareAction d n -> Eff Equal ()
|
||||
runCompare fvs act = fromInner $ eachCorner fvs $ act !(askAt DEFS)
|
||||
runCompare : Loc -> FreeVars d -> CompareAction d n -> Eff Equal ()
|
||||
runCompare loc fvs act = fromInner $ eachCorner loc fvs $ act !(askAt DEFS)
|
||||
|
||||
private
|
||||
foldMap1 : Semigroup b => (a -> b) -> List1 a -> b
|
||||
|
@ -903,21 +908,21 @@ parameters (loc : Loc) (ctx : TyContext d n)
|
|||
namespace Term
|
||||
export covering
|
||||
compare : SQty -> (ty, s, t : Term d n) -> Eff Equal ()
|
||||
compare sg ty s t = runCompare (fdvAll [ty, s, t]) $ \defs, ectx, th =>
|
||||
compare0 defs ectx sg (ty // th) (s // th) (t // th)
|
||||
compare sg ty s t = runCompare s.loc (fdvAll [ty, s, t]) $
|
||||
\defs, ectx, th => compare0 defs ectx sg (ty // th) (s // th) (t // th)
|
||||
|
||||
export covering
|
||||
compareType : (s, t : Term d n) -> Eff Equal ()
|
||||
compareType s t = runCompare (fdvAll [s, t]) $ \defs, ectx, th =>
|
||||
compareType defs ectx (s // th) (t // th)
|
||||
compareType s t = runCompare s.loc (fdvAll [s, t]) $
|
||||
\defs, ectx, th => compareType defs ectx (s // th) (t // th)
|
||||
|
||||
namespace Elim
|
||||
||| you don't have to pass the type in but the arguments must still be
|
||||
||| of the same type!!
|
||||
export covering
|
||||
compare : SQty -> (e, f : Elim d n) -> Eff Equal ()
|
||||
compare sg e f = runCompare (fdvAll [e, f]) $ \defs, ectx, th =>
|
||||
ignore $ compare0 defs ectx sg (e // th) (f // th)
|
||||
compare sg e f = runCompare e.loc (fdvAll [e, f]) $
|
||||
\defs, ectx, th => ignore $ compare0 defs ectx sg (e // th) (f // th)
|
||||
|
||||
namespace Term
|
||||
export covering %inline
|
||||
|
|
137
lib/Quox/Log.idr
137
lib/Quox/Log.idr
|
@ -1,12 +1,12 @@
|
|||
module Quox.Log
|
||||
|
||||
import Quox.Loc
|
||||
import Quox.Pretty
|
||||
|
||||
import Data.So
|
||||
import Data.DPair
|
||||
import Data.Maybe
|
||||
import Data.List1
|
||||
import Data.SortedMap
|
||||
|
||||
import Quox.Pretty
|
||||
import Control.Eff
|
||||
import Control.Monad.ST.Extra
|
||||
import Data.IORef
|
||||
|
@ -25,32 +25,40 @@ public export
|
|||
logCategories : List String
|
||||
logCategories = ["whnf", "equal", "check"]
|
||||
|
||||
public export
|
||||
public export %inline
|
||||
isLogLevel : Nat -> Bool
|
||||
isLogLevel l = l <= maxLogLevel
|
||||
|
||||
public export
|
||||
IsLogLevel : Nat -> Type
|
||||
IsLogLevel l = So $ isLogLevel l
|
||||
|
||||
public export %inline
|
||||
isLogCategory : String -> Bool
|
||||
isLogCategory cat = cat `elem` logCategories
|
||||
|
||||
public export
|
||||
IsLogCategory : String -> Type
|
||||
IsLogCategory cat = So $ isLogCategory cat
|
||||
|
||||
|
||||
public export
|
||||
LogLevel : Type
|
||||
LogLevel = Subset Nat (So . isLogLevel)
|
||||
LogLevel = Subset Nat IsLogLevel
|
||||
|
||||
public export
|
||||
LogCategory : Type
|
||||
LogCategory = Subset String (So . isLogCategory)
|
||||
LogCategory = Subset String IsLogCategory
|
||||
|
||||
|
||||
public export
|
||||
public export %inline
|
||||
toLogLevel : Nat -> Maybe LogLevel
|
||||
toLogLevel l =
|
||||
case choose $ isLogLevel l of
|
||||
Left y => Just $ Element l y
|
||||
Right _ => Nothing
|
||||
|
||||
public export
|
||||
public export %inline
|
||||
toLogCategory : String -> Maybe LogCategory
|
||||
toLogCategory c =
|
||||
case choose $ isLogCategory c of
|
||||
|
@ -60,7 +68,8 @@ toLogCategory c =
|
|||
|
||||
public export
|
||||
LevelMap : Type
|
||||
LevelMap = SortedMap LogCategory LogLevel
|
||||
LevelMap = List (LogCategory, LogLevel)
|
||||
-- i tried SortedMap first, but it is too much overhead for LevelMaps
|
||||
|
||||
public export
|
||||
record LogLevels where
|
||||
|
@ -74,40 +83,21 @@ public export
|
|||
LevelStack : Type
|
||||
LevelStack = List1 LogLevels
|
||||
|
||||
export
|
||||
export %inline
|
||||
defaultLogLevels : LogLevels
|
||||
defaultLogLevels = MkLogLevels (Element 0 Oh) empty
|
||||
defaultLogLevels = MkLogLevels (Element 0 Oh) []
|
||||
|
||||
export
|
||||
export %inline
|
||||
initStack : LevelStack
|
||||
initStack = singleton defaultLogLevels
|
||||
|
||||
export
|
||||
makeLogLevels : Nat -> List (String, Nat) -> Either String LogLevels
|
||||
makeLogLevels d ls = do
|
||||
d <- toLevel d
|
||||
ls <- traverse (bitraverse toCat toLevel) ls
|
||||
pure $ MkLogLevels d $ fromList ls
|
||||
where
|
||||
toCat : String -> Either String LogCategory
|
||||
toCat str = do
|
||||
let Left p = choose $ isLogCategory str
|
||||
| _ => Left "not a log category: \{str}"
|
||||
Right $ Element str p
|
||||
|
||||
toLevel : Nat -> Either String LogLevel
|
||||
toLevel l = do
|
||||
let Left p = choose $ isLogLevel l
|
||||
| _ => Left "log level not in range: \{show l}"
|
||||
Right $ Element l p
|
||||
|
||||
||| right biased for the default and for overlapping elements
|
||||
public export
|
||||
public export %inline
|
||||
mergeLevels : LogLevels -> LogLevels -> LogLevels
|
||||
mergeLevels (MkLogLevels _ map1) (MkLogLevels def map2) =
|
||||
MkLogLevels def $ mergeWith (\_, y => y) map1 map2
|
||||
MkLogLevels def $ map1 ++ map2
|
||||
|
||||
export
|
||||
export %inline
|
||||
getLevel : LogCategory -> LogLevels -> LogLevel
|
||||
getLevel cat lvls = fromMaybe lvls.defLevel $ lookup cat lvls.levels
|
||||
|
||||
|
@ -121,49 +111,49 @@ public export
|
|||
data PushArg = SetDefault LogLevel | SetCats LevelMap
|
||||
%name PushArg push
|
||||
|
||||
export
|
||||
mergePush : LogLevels -> PushArg -> LogLevels
|
||||
mergePush lvls (SetDefault def) = {defLevel := def} lvls
|
||||
mergePush lvls (SetCats map) = {levels $= mergeWith const map} lvls
|
||||
export %inline
|
||||
mergePush : PushArg -> LogLevels -> LogLevels
|
||||
mergePush (SetDefault def) = {defLevel := def}
|
||||
mergePush (SetCats map) = {levels $= (map ++)}
|
||||
|
||||
|
||||
public export
|
||||
data LogL : tag -> Type -> Type where
|
||||
Say : (cat : LogCategory) -> (lvl : LogLevel) -> (msg : Lazy LogDoc) ->
|
||||
LogL tag ()
|
||||
Push : (push : PushArg) -> LogL tag ()
|
||||
Pop : LogL tag ()
|
||||
CurLevels : LogL tag LogLevels
|
||||
data LogL : (lbl : tag) -> Type -> Type where
|
||||
Say : (cat : LogCategory) -> (lvl : LogLevel) ->
|
||||
(loc : Loc) -> (msg : Lazy LogDoc) -> LogL lbl ()
|
||||
Push : (push : PushArg) -> LogL lbl ()
|
||||
Pop : LogL lbl ()
|
||||
CurLevels : LogL lbl LogLevels
|
||||
|
||||
public export
|
||||
Log : Type -> Type
|
||||
Log = LogL ()
|
||||
|
||||
parameters (0 tag : a) {auto _ : Has (LogL tag) fs}
|
||||
parameters (0 lbl : tag) {auto _ : Has (LogL lbl) fs}
|
||||
public export %inline
|
||||
sayAt : (cat : String) -> (0 _ : So $ isLogCategory cat) =>
|
||||
(lvl : Nat) -> (0 _ : So $ isLogLevel lvl) =>
|
||||
Lazy LogDoc -> Eff fs ()
|
||||
sayAt cat lvl msg =
|
||||
send $ Say {tag} (Element cat %search) (Element lvl %search) msg
|
||||
sayAt : (cat : String) -> (0 catOk : IsLogCategory cat) =>
|
||||
(lvl : Nat) -> (0 lvlOk : IsLogLevel lvl) =>
|
||||
Loc -> Lazy LogDoc -> Eff fs ()
|
||||
sayAt cat lvl loc msg {catOk, lvlOk} =
|
||||
send $ Say {lbl} (Element cat catOk) (Element lvl lvlOk) loc msg
|
||||
|
||||
public export %inline
|
||||
pushAt : PushArg -> Eff fs ()
|
||||
pushAt lvls = send $ Push {tag} lvls
|
||||
pushAt lvls = send $ Push {lbl} lvls
|
||||
|
||||
public export %inline
|
||||
popAt : Eff fs ()
|
||||
popAt = send $ Pop {tag}
|
||||
popAt = send $ Pop {lbl}
|
||||
|
||||
public export %inline
|
||||
curLevelsAt : Eff fs LogLevels
|
||||
curLevelsAt = send $ CurLevels {tag}
|
||||
curLevelsAt = send $ CurLevels {lbl}
|
||||
|
||||
parameters {auto _ : Has Log fs}
|
||||
public export %inline
|
||||
say : (cat : String) -> (0 _ : So $ isLogCategory cat) =>
|
||||
(lvl : Nat) -> (0 _ : So $ isLogLevel lvl) =>
|
||||
Lazy LogDoc -> Eff fs ()
|
||||
say : (cat : String) -> (0 _ : IsLogCategory cat) =>
|
||||
(lvl : Nat) -> (0 _ : IsLogLevel lvl) =>
|
||||
Loc -> Lazy LogDoc -> Eff fs ()
|
||||
say = sayAt ()
|
||||
|
||||
public export %inline
|
||||
|
@ -181,7 +171,7 @@ parameters {auto _ : Has Log fs}
|
|||
|
||||
export
|
||||
doPush : PushArg -> LevelStack -> LevelStack
|
||||
doPush push list = mergePush (head list) push `cons` list
|
||||
doPush push list = mergePush push (head list) `cons` list
|
||||
|
||||
export
|
||||
doPop : List1 a -> List1 a
|
||||
|
@ -190,36 +180,37 @@ doPop list = fromMaybe list $ fromList list.tail
|
|||
export
|
||||
doSay : Applicative m =>
|
||||
LevelStack -> (LogDoc -> m ()) ->
|
||||
LogCategory -> LogLevel -> LogDoc -> m ()
|
||||
doSay list act cat lvl msg =
|
||||
when (lvl >= getLevel cat (head list)) $
|
||||
act $ hcat [text cat.fst, ":", pshow lvl.fst, ":"] <++> msg
|
||||
LogCategory -> LogLevel -> Loc -> Lazy LogDoc -> m ()
|
||||
doSay (map ::: _) act cat lvl loc msg =
|
||||
when (lvl <= getLevel cat map) $ do
|
||||
let loc = runPretty $ prettyLoc loc
|
||||
act $ hcat [loc, text cat.fst, "@", pshow lvl.fst, ":"] <++> msg
|
||||
|
||||
export
|
||||
handleLogIO : HasIO m => (FileError -> m ()) ->
|
||||
IORef LevelStack -> File -> LogL tag a -> m a
|
||||
handleLogIO th lvls h = \case
|
||||
Push push => modifyIORef lvls $ doPush push
|
||||
Pop => modifyIORef lvls doPop
|
||||
Say cat lvl msg => doSay !(readIORef lvls) printMsg cat lvl msg
|
||||
CurLevels => head <$> readIORef lvls
|
||||
Push push => modifyIORef lvls $ doPush push
|
||||
Pop => modifyIORef lvls doPop
|
||||
Say cat lvl loc msg => doSay !(readIORef lvls) printMsg cat lvl loc msg
|
||||
CurLevels => head <$> readIORef lvls
|
||||
where printMsg : LogDoc -> m ()
|
||||
printMsg msg = fPutStrLn h (render _ msg) >>= either th pure
|
||||
printMsg msg = fPutStr h (render _ msg) >>= either th pure
|
||||
|
||||
export %inline
|
||||
export
|
||||
handleLogST : (HasST m, Monad (m s)) =>
|
||||
STRef s (SnocList LogDoc) ->
|
||||
STRef s LevelStack ->
|
||||
LogL tag a -> m s a
|
||||
handleLogST docs lvls = \case
|
||||
Push push => liftST $ modifySTRef lvls $ doPush push
|
||||
Pop => liftST $ modifySTRef lvls doPop
|
||||
Say cat lvl msg => doSay !(liftST $ readSTRef lvls) printMsg cat lvl msg
|
||||
CurLevels => head <$> liftST (readSTRef lvls)
|
||||
Push push => modifySTRef' lvls $ doPush push
|
||||
Pop => modifySTRef' lvls doPop
|
||||
Say cat lvl loc msg => doSay !(readSTRef' lvls) printMsg cat lvl loc msg
|
||||
CurLevels => head <$> readSTRef' lvls
|
||||
where printMsg : LogDoc -> m s ()
|
||||
printMsg msg = liftST $ modifySTRef docs (:< msg)
|
||||
printMsg msg = modifySTRef' docs (:< msg)
|
||||
|
||||
export %inline
|
||||
export
|
||||
handleLogDiscard : Applicative m => LogL tag a -> m a
|
||||
handleLogDiscard = \case
|
||||
Say {} => pure ()
|
||||
|
|
|
@ -52,13 +52,12 @@ private
|
|||
checkLogs : String -> TyContext d n -> SQty ->
|
||||
Term d n -> Maybe (Term d n) -> Eff TC ()
|
||||
checkLogs fun ctx sg subj ty = do
|
||||
say "check" 10 $ text fun
|
||||
say "check" 95 $ hsep ["ctx =", runPretty $ prettyTyContext ctx]
|
||||
say "check" 95 $ hsep ["sg =", runPretty $ prettyQty sg.qty]
|
||||
say "check" 10 $ hsep ["subj =", runPretty $ prettyTermTC ctx subj]
|
||||
case ty of
|
||||
Just ty => say "check" 10 $ hsep ["ty =", runPretty $ prettyTermTC ctx ty]
|
||||
_ => pure ()
|
||||
say "check" 10 subj.loc $ text fun
|
||||
say "check" 95 subj.loc $ hsep ["ctx =", runPretty $ prettyTyContext ctx]
|
||||
say "check" 95 subj.loc $ hsep ["sg =", runPretty $ prettyQty sg.qty]
|
||||
say "check" 10 subj.loc $ hsep ["subj =", runPretty $ prettyTermTC ctx subj]
|
||||
let Just ty = ty | Nothing => pure ()
|
||||
say "check" 10 subj.loc $ hsep ["ty =", runPretty $ prettyTermTC ctx ty]
|
||||
|
||||
mutual
|
||||
||| "Ψ | Γ ⊢ σ · s ⇐ A ⊳ Σ"
|
||||
|
@ -76,7 +75,7 @@ mutual
|
|||
checkLogs "check" ctx sg subj (Just ty)
|
||||
ifConsistentElse ctx.dctx
|
||||
(checkC ctx sg subj ty)
|
||||
(say "check" 20 "check: 0=1")
|
||||
(say "check" 20 subj.loc "check: 0=1")
|
||||
|
||||
||| "Ψ | Γ ⊢₀ s ⇐ A"
|
||||
|||
|
||||
|
@ -112,7 +111,7 @@ mutual
|
|||
checkLogs "checkType" ctx SZero subj univ
|
||||
ignore $ ifConsistentElse ctx.dctx
|
||||
(checkTypeC ctx subj l)
|
||||
(say "check" 20 "checkType: 0=1")
|
||||
(say "check" 20 subj.loc "checkType: 0=1")
|
||||
|
||||
export covering %inline
|
||||
checkTypeC : TyContext d n -> Term d n -> Maybe Universe -> Eff TC ()
|
||||
|
@ -139,7 +138,7 @@ mutual
|
|||
checkLogs "infer" ctx sg (E subj) Nothing
|
||||
ifConsistentElse ctx.dctx
|
||||
(inferC ctx sg subj)
|
||||
(say "check" 20 "infer: 0=1")
|
||||
(say "check" 20 subj.loc "infer: 0=1")
|
||||
|
||||
||| `infer`, assuming the dimension context is consistent
|
||||
export covering %inline
|
||||
|
|
|
@ -88,7 +88,7 @@ parameters (defs : Definitions)
|
|||
expect what err pat rhs = Prelude.do
|
||||
match <- check `(\case ~(pat) => Just ~(rhs); _ => Nothing)
|
||||
pure $ \term => do
|
||||
say "check" 30 $ hsep ["expecting:", text what]
|
||||
say "check" 30 term.loc $ hsep ["expecting:", text what]
|
||||
res <- whnf term
|
||||
maybe (throw $ err loc ctx.names term) pure $ match $ fst res
|
||||
|
||||
|
@ -144,7 +144,7 @@ parameters (defs : Definitions)
|
|||
expect what err pat rhs = do
|
||||
match <- check `(\case ~(pat) => Just ~(rhs); _ => Nothing)
|
||||
pure $ \term => do
|
||||
say "equal" 30 $ hsep ["expecting:", text what]
|
||||
say "equal" 30 term.loc $ hsep ["expecting:", text what]
|
||||
res <- whnf term
|
||||
let t0 = delay $ term // shift0 ctx.dimLen
|
||||
maybe (throw $ err loc ctx.names t0) pure $ match $ fst res
|
||||
|
|
|
@ -219,19 +219,22 @@ parameters {auto _ : CanWhnf Term Interface.isRedexT}
|
|||
STRING tyLoc =>
|
||||
whnf defs ctx sg $ Ann s (STRING tyLoc) loc
|
||||
|
||||
-- η expand
|
||||
-- η expand.... kinda
|
||||
--
|
||||
-- (coe (𝑖 ⇒ [π. A]) @p @q s)
|
||||
-- ⇝
|
||||
-- [case1 coe (𝑖 ⇒ [π. A]) @p @q s return A‹q/𝑖› of {[x] ⇒ x}]
|
||||
-- ∷ [π. A]‹q/𝑖›
|
||||
BOX qty inner tyLoc =>
|
||||
-- [case1 s ∷ [π.A]‹p/𝑖› return A‹q/𝑖›
|
||||
-- of {[x] ⇒ coe (𝑖 ⇒ A) @p @q x}] ∷ [π.A]‹q/𝑖›
|
||||
--
|
||||
-- a literal η expansion of `e ⇝ [case e of {[x] ⇒ x}]` causes a loop in
|
||||
-- the equality checker because whnf of `case e ⋯` requires whnf of `e`
|
||||
BOX qty inner tyLoc => do
|
||||
let inner = CaseBox {
|
||||
qty = One,
|
||||
box = Coe (SY [< i] ty) p q s loc,
|
||||
ret = SN $ ty // one q,
|
||||
body = SY [< !(mnb "x" loc)] $ BVT 0 loc,
|
||||
box = Ann s (ty // one p) s.loc,
|
||||
ret = SN $ inner // one q,
|
||||
body = SY [< !(mnb "x" loc)] $ E $
|
||||
Coe (ST [< i] $ weakT 1 inner) p q (BVT 0 s.loc) s.loc,
|
||||
loc
|
||||
}
|
||||
in
|
||||
whnf defs ctx sg $ Ann (Box (E inner) loc) (ty // one q) loc
|
||||
|
|
|
@ -93,11 +93,13 @@ computeElimTypeNoLog defs ctx sg e =
|
|||
|
||||
computeElimType defs ctx sg e {ne} = do
|
||||
let Val n = ctx.termLen
|
||||
say "whnf" 90 "computeElimType"
|
||||
say "whnf" 95 $ hsep ["ctx =", runPretty $ prettyWhnfContext ctx]
|
||||
say "whnf" 90 $ hsep ["e =", runPretty $ prettyElim ctx.dnames ctx.tnames e]
|
||||
say "whnf" 90 e.loc "computeElimType"
|
||||
say "whnf" 95 e.loc $ hsep ["ctx =", runPretty $ prettyWhnfContext ctx]
|
||||
say "whnf" 90 e.loc $
|
||||
hsep ["e =", runPretty $ prettyElim ctx.dnames ctx.tnames e]
|
||||
res <- computeElimTypeNoLog defs ctx sg e {ne}
|
||||
say "whnf" 91 $ hsep ["⇝", runPretty $ prettyTerm ctx.dnames ctx.tnames res]
|
||||
say "whnf" 91 e.loc $
|
||||
hsep ["⇝", runPretty $ prettyTerm ctx.dnames ctx.tnames res]
|
||||
pure res
|
||||
|
||||
computeWhnfElimType0 defs ctx sg e =
|
||||
|
|
|
@ -15,24 +15,30 @@ export covering CanWhnf Term Interface.isRedexT
|
|||
export covering CanWhnf Elim Interface.isRedexE
|
||||
|
||||
|
||||
-- the String is what to call the "s" argument in logs (maybe "s", or "e")
|
||||
private %inline
|
||||
whnfDefault :
|
||||
{0 isRedex : RedexTest tm} -> CanWhnf tm isRedex =>
|
||||
String -> (forall d, n. WhnfContext d n -> tm d n -> Eff Pretty LogDoc) ->
|
||||
(defs : Definitions) -> (ctx : WhnfContext d n) -> (q : SQty) ->
|
||||
tm d n -> Eff Whnf (Subset (tm d n) (No . isRedex defs ctx q))
|
||||
{0 isRedex : RedexTest tm} ->
|
||||
(CanWhnf tm isRedex, Located2 tm) =>
|
||||
String ->
|
||||
(forall d, n. WhnfContext d n -> tm d n -> Eff Pretty LogDoc) ->
|
||||
(defs : Definitions) ->
|
||||
(ctx : WhnfContext d n) ->
|
||||
(sg : SQty) ->
|
||||
(s : tm d n) ->
|
||||
Eff Whnf (Subset (tm d n) (No . isRedex defs ctx sg))
|
||||
whnfDefault name ppr defs ctx sg s = do
|
||||
say "whnf" 10 "whnf"
|
||||
say "whnf" 95 $ hsep ["ctx =", runPretty $ prettyWhnfContext ctx]
|
||||
say "whnf" 95 $ hsep ["sg =", runPretty $ prettyQty sg.qty]
|
||||
say "whnf" 10 $ hsep [text name, "=", runPretty $ ppr ctx s]
|
||||
say "whnf" 10 s.loc "whnf"
|
||||
say "whnf" 95 s.loc $ hsep ["ctx =", runPretty $ prettyWhnfContext ctx]
|
||||
say "whnf" 95 s.loc $ hsep ["sg =", runPretty $ prettyQty sg.qty]
|
||||
say "whnf" 10 s.loc $ hsep [text name, "=", runPretty $ ppr ctx s]
|
||||
res <- whnfNoLog defs ctx sg s
|
||||
say "whnf" 11 $ hsep ["whnf ⇝", runPretty $ ppr ctx res.fst]
|
||||
say "whnf" 11 s.loc $ hsep ["whnf ⇝", runPretty $ ppr ctx res.fst]
|
||||
pure res
|
||||
|
||||
covering
|
||||
CanWhnf Elim Interface.isRedexE where
|
||||
whnf = whnfDefault "s" $ \ctx, e => prettyElim ctx.dnames ctx.tnames e
|
||||
whnf = whnfDefault "e" $ \ctx, e => prettyElim ctx.dnames ctx.tnames e
|
||||
|
||||
whnfNoLog defs ctx sg (F x u loc) with (lookupElim0 x u defs) proof eq
|
||||
_ | Just y = whnf defs ctx sg $ setLoc loc $ injElim ctx y
|
||||
|
|
Loading…
Reference in New Issue