make #[fail] run in the current namespace

This commit is contained in:
rhiannon morris 2023-12-21 17:53:46 +01:00
parent 7afcbfe258
commit 54db7e27ef

View file

@ -45,7 +45,8 @@ FromParserIO = FromParserPure ++ [LoadFile]
export
fromParserPure : NameSuf -> Definitions ->
fromParserPure : {default [<] ns : Mods} ->
NameSuf -> Definitions ->
Eff FromParserPure a ->
Either Error (a, NameSuf, Definitions)
fromParserPure suf defs act = runSTErr $ do
@ -54,7 +55,7 @@ fromParserPure suf defs act = runSTErr $ do
res <- runEff act $ with Union.(::)
[handleExcept (\e => stLeft e),
handleStateSTRef defs,
handleStateSTRef !(liftST $ newSTRef [<]),
handleStateSTRef !(liftST $ newSTRef ns),
handleStateSTRef suf]
pure (res, !(liftST $ readSTRef suf), !(liftST $ readSTRef defs))
@ -375,7 +376,7 @@ data HasFail = NoFail | AnyFail | FailWith String
export covering
expectFail : Loc -> Eff FromParserPure a -> Eff FromParserPure Error
expectFail loc act =
case fromParserPure !(getAt GEN) !(getAt DEFS) act of
case fromParserPure !(getAt GEN) !(getAt DEFS) {ns = !(getAt NS)} act of
Left err => pure err
Right _ => throw $ ExpectedFail loc