rhi/quox
rhi
/
quox
1
0
Fork 0
Code Issues 16 Pull Requests 2 Releases Wiki Activity

wip

This commit is contained in:
rhiannon morris 2024-01-29 18:17:17 +01:00
parent c5e157a169
commit 979f972759
9 changed files with 155 additions and 137 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

3
exe/CompileMonad.idr
View File

@ -69,7 +69,8 @@ withLogFile : Options ->
(IORef LevelStack -> OpenFile -> IO (Either Error a)) -> (IORef LevelStack -> OpenFile -> IO (Either Error a)) ->
IO (Either Error a) IO (Either Error a)
withLogFile opts act = do 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 where
fromError : String -> FileError -> IO (Either Error a) fromError : String -> FileError -> IO (Either Error a)
fromError file err = pure $ Left $ WriteError file err fromError file err = pure $ Left $ WriteError file err

2
exe/Options.idr
View File

@ -156,7 +156,7 @@ splitLogFlag = traverse flag1 . toList . split (== ':') where
case strM second of case strM second of
StrCons '=' lvl => do StrCons '=' lvl => do
cat <- parseLogCategory first cat <- parseLogCategory first
lvl <- parseLogLevel second lvl <- parseLogLevel lvl
pure (Just cat, lvl) pure (Just cat, lvl)
StrNil => (Nothing,) <$> parseLogLevel first StrNil => (Nothing,) <$> parseLogLevel first
_ => Left "invalid log flag \{str}" _ => Left "invalid log flag \{str}"

14
lib/Control/Monad/ST/Extra.idr
View File

@ -62,3 +62,17 @@ export %inline HasST (STErr e) where liftST = STE . map Right
export export
stLeft : e -> STErr e s a stLeft : e -> STErr e s a
stLeft e = STE $ pure $ Left e 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

93
lib/Quox/Equal.idr
View File

@ -86,12 +86,13 @@ isEmptyNoLog :
Definitions -> EqContext n -> SQty -> Term 0 n -> Eff EqualInner Bool Definitions -> EqContext n -> SQty -> Term 0 n -> Eff EqualInner Bool
isEmpty defs ctx sg ty = do isEmpty defs ctx sg ty = do
say "equal" logLevel "isEmpty" say "equal" logLevel ty.loc "isEmpty"
say "equal" 95 $ hsep ["ctx =", runPretty $ prettyEqContext ctx] say "equal" 95 ty.loc $ hsep ["ctx =", runPretty $ prettyEqContext ctx]
say "equal" 95 $ hsep ["sg =", runPretty $ prettyQty sg.qty] say "equal" 95 ty.loc $ hsep ["sg =", runPretty $ prettyQty sg.qty]
say "equal" logLevel $ hsep ["ty =", runPretty $ prettyTerm [<] ctx.tnames ty] say "equal" logLevel ty.loc $
hsep ["ty =", runPretty $ prettyTerm [<] ctx.tnames ty]
res <- isEmptyNoLog defs ctx sg 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 pure res
isEmptyNoLog defs ctx sg ty0 = do isEmptyNoLog defs ctx sg ty0 = do
@ -134,12 +135,13 @@ isSubSingNoLog :
Definitions -> EqContext n -> SQty -> Term 0 n -> Eff EqualInner Bool Definitions -> EqContext n -> SQty -> Term 0 n -> Eff EqualInner Bool
isSubSing defs ctx sg ty = do isSubSing defs ctx sg ty = do
say "equal" logLevel "isSubSing" say "equal" logLevel ty.loc "isSubSing"
say "equal" 95 $ hsep ["ctx =", runPretty $ prettyEqContext ctx] say "equal" 95 ty.loc $ hsep ["ctx =", runPretty $ prettyEqContext ctx]
say "equal" 95 $ hsep ["sg =", runPretty $ prettyQty sg.qty] say "equal" 95 ty.loc $ hsep ["sg =", runPretty $ prettyQty sg.qty]
say "equal" logLevel $ hsep ["ty =", runPretty $ prettyTerm [<] ctx.tnames ty] say "equal" logLevel ty.loc $
hsep ["ty =", runPretty $ prettyTerm [<] ctx.tnames ty]
res <- isSubSingNoLog defs ctx sg 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 pure res
isSubSingNoLog defs ctx sg ty0 = do 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) Right n => throw $ NotType loc (toTyContext ctx) (ty // shift0 ctx.dimLen)
ensureTyCon loc ctx ty = do ensureTyCon loc ctx ty = do
say "equal" 60 "ensureTyCon" say "equal" 60 ty.loc "ensureTyCon"
say "equal" 95 $ hsep ["ctx =", runPretty $ prettyEqContext ctx] say "equal" 95 ty.loc $ hsep ["ctx =", runPretty $ prettyEqContext ctx]
say "equal" 60 $ hsep ["ty =", runPretty $ prettyTerm [<] ctx.tnames ty] say "equal" 60 ty.loc $
hsep ["ty =", runPretty $ prettyTerm [<] ctx.tnames ty]
ensureTyConNoLog loc ctx ty ensureTyConNoLog loc ctx ty
@ -804,13 +807,14 @@ namespace Term
compare0' defs ctx sg ty' s' t' compare0' defs ctx sg ty' s' t'
compare0 defs ctx sg ty s t = do compare0 defs ctx sg ty s t = do
say "equal" 30 "Term.compare0" say "equal" 30 s.loc "Term.compare0"
say "equal" 30 $ hsep ["mode =", pshow !mode] say "equal" 30 s.loc $ hsep ["mode =", pshow !mode]
say "equal" 95 $ hsep ["ctx =", runPretty $ prettyEqContext ctx] say "equal" 95 s.loc $ hsep ["ctx =", runPretty $ prettyEqContext ctx]
say "equal" 95 $ hsep ["sg =", runPretty $ prettyQty sg.qty] say "equal" 95 s.loc $ hsep ["sg =", runPretty $ prettyQty sg.qty]
say "equal" 31 $ hsep ["ty =", runPretty $ prettyTerm [<] ctx.tnames ty] say "equal" 31 s.loc $
say "equal" 30 $ hsep ["s =", runPretty $ prettyTerm [<] ctx.tnames s] hsep ["ty =", runPretty $ prettyTerm [<] ctx.tnames ty]
say "equal" 30 $ hsep ["t =", runPretty $ prettyTerm [<] ctx.tnames t] 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 compare0NoLog defs ctx sg ty s t
namespace Elim namespace Elim
@ -823,14 +827,15 @@ namespace Elim
maybe (pure ty) throw err maybe (pure ty) throw err
compare0 defs ctx sg e f = do compare0 defs ctx sg e f = do
say "equal" 30 "Elim.compare0" say "equal" 30 e.loc "Elim.compare0"
say "equal" 30 $ hsep ["mode =", pshow !mode] say "equal" 30 e.loc $ hsep ["mode =", pshow !mode]
say "equal" 95 $ hsep ["ctx =", runPretty $ prettyEqContext ctx] say "equal" 95 e.loc $ hsep ["ctx =", runPretty $ prettyEqContext ctx]
say "equal" 95 $ hsep ["sg =", runPretty $ prettyQty sg.qty] say "equal" 95 e.loc $ hsep ["sg =", runPretty $ prettyQty sg.qty]
say "equal" 30 $ hsep ["e =", runPretty $ prettyElim [<] ctx.tnames e] say "equal" 30 e.loc $ hsep ["e =", runPretty $ prettyElim [<] ctx.tnames e]
say "equal" 30 $ hsep ["f =", runPretty $ prettyElim [<] ctx.tnames f] say "equal" 30 e.loc $ hsep ["f =", runPretty $ prettyElim [<] ctx.tnames f]
ty <- compare0NoLog defs ctx sg e 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 pure ty
export covering %inline export covering %inline
@ -845,11 +850,11 @@ compareTypeNoLog defs ctx s t = do
compareType' defs ctx s' t' compareType' defs ctx s' t'
compareType defs ctx s t = do compareType defs ctx s t = do
say "equal" 30 "compareType" say "equal" 30 s.loc "compareType"
say "equal" 30 $ hsep ["mode =", pshow !mode] say "equal" 30 s.loc $ hsep ["mode =", pshow !mode]
say "equal" 95 $ hsep ["ctx =", runPretty $ prettyEqContext ctx] say "equal" 95 s.loc $ hsep ["ctx =", runPretty $ prettyEqContext ctx]
say "equal" 30 $ hsep ["s =", runPretty $ prettyTerm [<] ctx.tnames s] say "equal" 30 s.loc $ hsep ["s =", runPretty $ prettyTerm [<] ctx.tnames s]
say "equal" 30 $ hsep ["t =", runPretty $ prettyTerm [<] ctx.tnames t] say "equal" 30 s.loc $ hsep ["t =", runPretty $ prettyTerm [<] ctx.tnames t]
compareTypeNoLog defs ctx s t compareTypeNoLog defs ctx s t
@ -873,10 +878,10 @@ parameters (loc : Loc) (ctx : TyContext d n)
fromInner = lift . map fst . runState mode fromInner = lift . map fst . runState mode
private private
eachCorner : Has Log fs => FreeVars d -> eachCorner : Has Log fs => Loc -> FreeVars d ->
(EqContext n -> DSubst d 0 -> Eff fs ()) -> Eff fs () (EqContext n -> DSubst d 0 -> Eff fs ()) -> Eff fs ()
eachCorner fvs act = do eachCorner loc fvs act = do
say "equal" 50 $ say "equal" 50 loc $
hsep $ "eachCorner: split on" :: map prettyBind' (getVars ctx fvs) hsep $ "eachCorner: split on" :: map prettyBind' (getVars ctx fvs)
for_ (splits loc ctx.dctx fvs) $ \th => for_ (splits loc ctx.dctx fvs) $ \th =>
act (makeEqContext ctx th) th act (makeEqContext ctx th) th
@ -887,8 +892,8 @@ parameters (loc : Loc) (ctx : TyContext d n)
Definitions -> EqContext n -> DSubst d 0 -> Eff EqualInner () Definitions -> EqContext n -> DSubst d 0 -> Eff EqualInner ()
private private
runCompare : FreeVars d -> CompareAction d n -> Eff Equal () runCompare : Loc -> FreeVars d -> CompareAction d n -> Eff Equal ()
runCompare fvs act = fromInner $ eachCorner fvs $ act !(askAt DEFS) runCompare loc fvs act = fromInner $ eachCorner loc fvs $ act !(askAt DEFS)
private private
foldMap1 : Semigroup b => (a -> b) -> List1 a -> b foldMap1 : Semigroup b => (a -> b) -> List1 a -> b
@ -902,21 +907,21 @@ parameters (loc : Loc) (ctx : TyContext d n)
namespace Term namespace Term
export covering export covering
compare : SQty -> (ty, s, t : Term d n) -> Eff Equal () compare : SQty -> (ty, s, t : Term d n) -> Eff Equal ()
compare sg ty s t = runCompare (fdvAll [ty, s, t]) $ \defs, ectx, th => compare sg ty s t = runCompare s.loc (fdvAll [ty, s, t]) $
compare0 defs ectx sg (ty // th) (s // th) (t // th) \defs, ectx, th => compare0 defs ectx sg (ty // th) (s // th) (t // th)
export covering export covering
compareType : (s, t : Term d n) -> Eff Equal () compareType : (s, t : Term d n) -> Eff Equal ()
compareType s t = runCompare (fdvAll [s, t]) $ \defs, ectx, th => compareType s t = runCompare s.loc (fdvAll [s, t]) $
compareType defs ectx (s // th) (t // th) \defs, ectx, th => compareType defs ectx (s // th) (t // th)
namespace Elim namespace Elim
||| you don't have to pass the type in but the arguments must still be ||| you don't have to pass the type in but the arguments must still be
||| of the same type!! ||| of the same type!!
export covering export covering
compare : SQty -> (e, f : Elim d n) -> Eff Equal () compare : SQty -> (e, f : Elim d n) -> Eff Equal ()
compare sg e f = runCompare (fdvAll [e, f]) $ \defs, ectx, th => compare sg e f = runCompare e.loc (fdvAll [e, f]) $
ignore $ compare0 defs ectx sg (e // th) (f // th) \defs, ectx, th => ignore $ compare0 defs ectx sg (e // th) (f // th)
namespace Term namespace Term
export covering %inline export covering %inline

121
lib/Quox/Log.idr
View File

@ -1,11 +1,12 @@
module Quox.Log module Quox.Log
import Quox.Loc
import Quox.Pretty
import Data.So import Data.So
import Data.DPair import Data.DPair
import Data.Maybe import Data.Maybe
import Data.List1 import Data.List1
import Quox.Pretty
import Control.Eff import Control.Eff
import Control.Monad.ST.Extra import Control.Monad.ST.Extra
import Data.IORef import Data.IORef
@ -28,18 +29,26 @@ public export %inline
isLogLevel : Nat -> Bool isLogLevel : Nat -> Bool
isLogLevel l = l <= maxLogLevel isLogLevel l = l <= maxLogLevel
public export
IsLogLevel : Nat -> Type
IsLogLevel l = So $ isLogLevel l
public export %inline public export %inline
isLogCategory : String -> Bool isLogCategory : String -> Bool
isLogCategory cat = cat `elem` logCategories isLogCategory cat = cat `elem` logCategories
public export
IsLogCategory : String -> Type
IsLogCategory cat = So $ isLogCategory cat
public export public export
LogLevel : Type LogLevel : Type
LogLevel = Subset Nat (So . isLogLevel) LogLevel = Subset Nat IsLogLevel
public export public export
LogCategory : Type LogCategory : Type
LogCategory = Subset String (So . isLogCategory) LogCategory = Subset String IsLogCategory
public export %inline public export %inline
@ -82,25 +91,6 @@ export %inline
initStack : LevelStack initStack : LevelStack
initStack = singleton defaultLogLevels 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 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 ||| right biased for the default and for overlapping elements
public export %inline public export %inline
mergeLevels : LogLevels -> LogLevels -> LogLevels mergeLevels : LogLevels -> LogLevels -> LogLevels
@ -122,48 +112,48 @@ data PushArg = SetDefault LogLevel | SetCats LevelMap
%name PushArg push %name PushArg push
export %inline export %inline
mergePush : LogLevels -> PushArg -> LogLevels mergePush : PushArg -> LogLevels -> LogLevels
mergePush lvls (SetDefault def) = {defLevel := def} lvls mergePush (SetDefault def) = {defLevel := def}
mergePush lvls (SetCats map) = {levels $= (map ++)} lvls mergePush (SetCats map) = {levels $= (map ++)}
public export public export
data LogL : tag -> Type -> Type where data LogL : (lbl : tag) -> Type -> Type where
Say : (cat : LogCategory) -> (lvl : LogLevel) -> (msg : Lazy LogDoc) -> Say : (cat : LogCategory) -> (lvl : LogLevel) ->
LogL tag () (loc : Loc) -> (msg : Lazy LogDoc) -> LogL lbl ()
Push : (push : PushArg) -> LogL tag () Push : (push : PushArg) -> LogL lbl ()
Pop : LogL tag () Pop : LogL lbl ()
CurLevels : LogL tag LogLevels CurLevels : LogL lbl LogLevels
public export public export
Log : Type -> Type Log : Type -> Type
Log = LogL () Log = LogL ()
parameters (0 tag : a) {auto _ : Has (LogL tag) fs} parameters (0 lbl : tag) {auto _ : Has (LogL lbl) fs}
public export %inline public export %inline
sayAt : (cat : String) -> (0 _ : So $ isLogCategory cat) => sayAt : (cat : String) -> (0 catOk : IsLogCategory cat) =>
(lvl : Nat) -> (0 _ : So $ isLogLevel lvl) => (lvl : Nat) -> (0 lvlOk : IsLogLevel lvl) =>
Lazy LogDoc -> Eff fs () Loc -> Lazy LogDoc -> Eff fs ()
sayAt cat lvl msg = sayAt cat lvl loc msg {catOk, lvlOk} =
send $ Say {tag} (Element cat %search) (Element lvl %search) msg send $ Say {lbl} (Element cat catOk) (Element lvl lvlOk) loc msg
public export %inline public export %inline
pushAt : PushArg -> Eff fs () pushAt : PushArg -> Eff fs ()
pushAt lvls = send $ Push {tag} lvls pushAt lvls = send $ Push {lbl} lvls
public export %inline public export %inline
popAt : Eff fs () popAt : Eff fs ()
popAt = send $ Pop {tag} popAt = send $ Pop {lbl}
public export %inline public export %inline
curLevelsAt : Eff fs LogLevels curLevelsAt : Eff fs LogLevels
curLevelsAt = send $ CurLevels {tag} curLevelsAt = send $ CurLevels {lbl}
parameters {auto _ : Has Log fs} parameters {auto _ : Has Log fs}
public export %inline public export %inline
say : (cat : String) -> (0 _ : So $ isLogCategory cat) => say : (cat : String) -> (0 _ : IsLogCategory cat) =>
(lvl : Nat) -> (0 _ : So $ isLogLevel lvl) => (lvl : Nat) -> (0 _ : IsLogLevel lvl) =>
Lazy LogDoc -> Eff fs () Loc -> Lazy LogDoc -> Eff fs ()
say = sayAt () say = sayAt ()
public export %inline public export %inline
@ -179,47 +169,48 @@ parameters {auto _ : Has Log fs}
curLevels = curLevelsAt () curLevels = curLevelsAt ()
export %inline export
doPush : PushArg -> LevelStack -> LevelStack doPush : PushArg -> LevelStack -> LevelStack
doPush push list = mergePush (head list) push `cons` list doPush push list = mergePush push (head list) `cons` list
export %inline export
doPop : List1 a -> List1 a doPop : List1 a -> List1 a
doPop list = fromMaybe list $ fromList list.tail doPop list = fromMaybe list $ fromList list.tail
export %inline export
doSay : Applicative m => doSay : Applicative m =>
LevelStack -> (LogDoc -> m ()) -> LevelStack -> (LogDoc -> m ()) ->
LogCategory -> LogLevel -> LogDoc -> m () LogCategory -> LogLevel -> Loc -> Lazy LogDoc -> m ()
doSay list act cat lvl msg = doSay (map ::: _) act cat lvl loc msg =
when (lvl <= getLevel cat (head list)) $ when (lvl <= getLevel cat map) $ do
act $ hcat [text cat.fst, ":", pshow lvl.fst, ":"] <++> msg let loc = runPretty $ prettyLoc loc
act $ hcat [loc, text cat.fst, "@", pshow lvl.fst, ":"] <++> msg
export %inline export
handleLogIO : HasIO m => (FileError -> m ()) -> handleLogIO : HasIO m => (FileError -> m ()) ->
IORef LevelStack -> File -> LogL tag a -> m a IORef LevelStack -> File -> LogL tag a -> m a
handleLogIO th lvls h = \case handleLogIO th lvls h = \case
Push push => modifyIORef lvls $ doPush push Push push => modifyIORef lvls $ doPush push
Pop => modifyIORef lvls doPop Pop => modifyIORef lvls doPop
Say cat lvl msg => doSay !(readIORef lvls) printMsg cat lvl msg Say cat lvl loc msg => doSay !(readIORef lvls) printMsg cat lvl loc msg
CurLevels => head <$> readIORef lvls CurLevels => head <$> readIORef lvls
where printMsg : LogDoc -> m () 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)) => handleLogST : (HasST m, Monad (m s)) =>
STRef s (SnocList LogDoc) -> STRef s (SnocList LogDoc) ->
STRef s LevelStack -> STRef s LevelStack ->
LogL tag a -> m s a LogL tag a -> m s a
handleLogST docs lvls = \case handleLogST docs lvls = \case
Push push => liftST $ modifySTRef lvls $ doPush push Push push => modifySTRef' lvls $ doPush push
Pop => liftST $ modifySTRef lvls doPop Pop => modifySTRef' lvls doPop
Say cat lvl msg => doSay !(liftST $ readSTRef lvls) printMsg cat lvl msg Say cat lvl loc msg => doSay !(readSTRef' lvls) printMsg cat lvl loc msg
CurLevels => head <$> liftST (readSTRef lvls) CurLevels => head <$> readSTRef' lvls
where printMsg : LogDoc -> m s () 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 : Applicative m => LogL tag a -> m a
handleLogDiscard = \case handleLogDiscard = \case
Say {} => pure () Say {} => pure ()

19
lib/Quox/Typechecker.idr
View File

@ -52,13 +52,12 @@ private
checkLogs : String -> TyContext d n -> SQty -> checkLogs : String -> TyContext d n -> SQty ->
Term d n -> Maybe (Term d n) -> Eff TC () Term d n -> Maybe (Term d n) -> Eff TC ()
checkLogs fun ctx sg subj ty = do checkLogs fun ctx sg subj ty = do
say "check" 10 $ text fun say "check" 10 subj.loc $ text fun
say "check" 95 $ hsep ["ctx =", runPretty $ prettyTyContext ctx] say "check" 95 subj.loc $ hsep ["ctx =", runPretty $ prettyTyContext ctx]
say "check" 95 $ hsep ["sg =", runPretty $ prettyQty sg.qty] say "check" 95 subj.loc $ hsep ["sg =", runPretty $ prettyQty sg.qty]
say "check" 10 $ hsep ["subj =", runPretty $ prettyTermTC ctx subj] say "check" 10 subj.loc $ hsep ["subj =", runPretty $ prettyTermTC ctx subj]
case ty of let Just ty = ty | Nothing => pure ()
Just ty => say "check" 10 $ hsep ["ty =", runPretty $ prettyTermTC ctx ty] say "check" 10 subj.loc $ hsep ["ty =", runPretty $ prettyTermTC ctx ty]
_ => pure ()
mutual mutual
||| "Ψ | Γ ⊢ σ · s ⇐ A ⊳ Σ" ||| "Ψ | Γ ⊢ σ · s ⇐ A ⊳ Σ"
@ -76,7 +75,7 @@ mutual
checkLogs "check" ctx sg subj (Just ty) checkLogs "check" ctx sg subj (Just ty)
ifConsistentElse ctx.dctx ifConsistentElse ctx.dctx
(checkC ctx sg subj ty) (checkC ctx sg subj ty)
(say "check" 20 "check: 0=1") (say "check" 20 subj.loc "check: 0=1")
||| "Ψ | Γ ⊢₀ s ⇐ A" ||| "Ψ | Γ ⊢₀ s ⇐ A"
||| |||
@ -112,7 +111,7 @@ mutual
checkLogs "checkType" ctx SZero subj univ checkLogs "checkType" ctx SZero subj univ
ignore $ ifConsistentElse ctx.dctx ignore $ ifConsistentElse ctx.dctx
(checkTypeC ctx subj l) (checkTypeC ctx subj l)
(say "check" 20 "checkType: 0=1") (say "check" 20 subj.loc "checkType: 0=1")
export covering %inline export covering %inline
checkTypeC : TyContext d n -> Term d n -> Maybe Universe -> Eff TC () checkTypeC : TyContext d n -> Term d n -> Maybe Universe -> Eff TC ()
@ -139,7 +138,7 @@ mutual
checkLogs "infer" ctx sg (E subj) Nothing checkLogs "infer" ctx sg (E subj) Nothing
ifConsistentElse ctx.dctx ifConsistentElse ctx.dctx
(inferC ctx sg subj) (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 ||| `infer`, assuming the dimension context is consistent
export covering %inline export covering %inline

4
lib/Quox/Typing.idr
View File

@ -88,7 +88,7 @@ parameters (defs : Definitions)
expect what err pat rhs = Prelude.do expect what err pat rhs = Prelude.do
match <- check `(\case ~(pat) => Just ~(rhs); _ => Nothing) match <- check `(\case ~(pat) => Just ~(rhs); _ => Nothing)
pure $ \term => do pure $ \term => do
say "check" 30 $ hsep ["expecting:", text what] say "check" 30 term.loc $ hsep ["expecting:", text what]
res <- whnf term res <- whnf term
maybe (throw $ err loc ctx.names term) pure $ match $ fst res maybe (throw $ err loc ctx.names term) pure $ match $ fst res
@ -144,7 +144,7 @@ parameters (defs : Definitions)
expect what err pat rhs = do expect what err pat rhs = do
match <- check `(\case ~(pat) => Just ~(rhs); _ => Nothing) match <- check `(\case ~(pat) => Just ~(rhs); _ => Nothing)
pure $ \term => do pure $ \term => do
say "equal" 30 $ hsep ["expecting:", text what] say "equal" 30 term.loc $ hsep ["expecting:", text what]
res <- whnf term res <- whnf term
let t0 = delay $ term // shift0 ctx.dimLen let t0 = delay $ term // shift0 ctx.dimLen
maybe (throw $ err loc ctx.names t0) pure $ match $ fst res maybe (throw $ err loc ctx.names t0) pure $ match $ fst res

10
lib/Quox/Whnf/ComputeElimType.idr
View File

@ -93,11 +93,13 @@ computeElimTypeNoLog defs ctx sg e =
computeElimType defs ctx sg e {ne} = do computeElimType defs ctx sg e {ne} = do
let Val n = ctx.termLen let Val n = ctx.termLen
say "whnf" 90 "computeElimType" say "whnf" 90 e.loc "computeElimType"
say "whnf" 95 $ hsep ["ctx =", runPretty $ prettyWhnfContext ctx] say "whnf" 95 e.loc $ hsep ["ctx =", runPretty $ prettyWhnfContext ctx]
say "whnf" 90 $ hsep ["e =", runPretty $ prettyElim ctx.dnames ctx.tnames e] say "whnf" 90 e.loc $
hsep ["e =", runPretty $ prettyElim ctx.dnames ctx.tnames e]
res <- computeElimTypeNoLog defs ctx sg e {ne} 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 pure res
computeWhnfElimType0 defs ctx sg e = computeWhnfElimType0 defs ctx sg e =

26
lib/Quox/Whnf/Main.idr
View File

@ -15,24 +15,30 @@ export covering CanWhnf Term Interface.isRedexT
export covering CanWhnf Elim Interface.isRedexE export covering CanWhnf Elim Interface.isRedexE
-- the String is what to call the "s" argument in logs (maybe "s", or "e")
private %inline private %inline
whnfDefault : whnfDefault :
{0 isRedex : RedexTest tm} -> CanWhnf tm isRedex => {0 isRedex : RedexTest tm} ->
String -> (forall d, n. WhnfContext d n -> tm d n -> Eff Pretty LogDoc) -> (CanWhnf tm isRedex, Located2 tm) =>
(defs : Definitions) -> (ctx : WhnfContext d n) -> (q : SQty) -> String ->
tm d n -> Eff Whnf (Subset (tm d n) (No . isRedex defs ctx q)) (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 whnfDefault name ppr defs ctx sg s = do
say "whnf" 10 "whnf" say "whnf" 10 s.loc "whnf"
say "whnf" 95 $ hsep ["ctx =", runPretty $ prettyWhnfContext ctx] say "whnf" 95 s.loc $ hsep ["ctx =", runPretty $ prettyWhnfContext ctx]
say "whnf" 95 $ hsep ["sg =", runPretty $ prettyQty sg.qty] say "whnf" 95 s.loc $ hsep ["sg =", runPretty $ prettyQty sg.qty]
say "whnf" 10 $ hsep [text name, "=", runPretty $ ppr ctx s] say "whnf" 10 s.loc $ hsep [text name, "=", runPretty $ ppr ctx s]
res <- whnfNoLog defs ctx sg 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 pure res
covering covering
CanWhnf Elim Interface.isRedexE where 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 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 _ | Just y = whnf defs ctx sg $ setLoc loc $ injElim ctx y