-
Notifications
You must be signed in to change notification settings - Fork 1
New issue
Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.
By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.
Already on GitHub? Sign in to your account
refactor: Make InLvl a handler instead of a command #31
Conversation
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
This is fab - I love that all the awkward Req InLvl
cases are gone, and generally looks great. What do you think about SplitNS
and/or requiring localNS
?
brat/Brat/Checker/Monad.hs
Outdated
@@ -60,8 +60,8 @@ data Context = Ctx { globalVEnv :: VEnv | |||
|
|||
data CheckingSig ty where | |||
Fresh :: String -> CheckingSig Name | |||
-- Run a sub-process on a new namespace-level | |||
InLvl :: String -> Checking a -> CheckingSig a | |||
GetNS :: CheckingSig Namespace |
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
How about a single SplitNS :: String -> CheckingSig Namespace
which both updates the namespace inside handler
(to the second half of the split) and returns the first half of the split?
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
This makes things much nicer! 😄
brat/Brat/Checker/Monad.hs
Outdated
-> Either Error (v,Context,([TypedHole],Graph),Namespace) | ||
handler (Ret v) ctx g ns = return (v, ctx, ([], g), ns) | ||
-> Either Error (v,Context,([TypedHole],Graph)) | ||
handler (Ret v) ctx g _ = return (v, ctx, ([], g)) |
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
I am even wondering if we could remove the Namespace
parameter to handler. Have the top-level command(s) (i.e. GetNS
+SetNS
or SplitNS
) die with an error, and rely on running a localNS
inside it. You could make run
still take a Namespace and invoke handler (localNS c)
.... (so, a bit like localFC
)
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
I was thinking the same thing!
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
And it even works!
brat/Brat/Checker/Monad.hs
Outdated
@@ -300,7 +290,10 @@ typeErr = err . TypeErr | |||
|
|||
instance FreshMonad Checking where | |||
freshName x = req $ Fresh x | |||
str -! c = req $ InLvl str c | |||
str -! c = do |
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
Oh, nice - I wasn't expecting it to be so easy to keep FreshMonad
@@ -153,7 +154,7 @@ loadStmtsWithEnv ns (venv, oldDecls, oldEndData) (fname, pre, stmts, cts) = addS | |||
let vdecls = map fst entries | |||
-- Now generate environment mapping usernames to nodes in the graph | |||
venv <- pure $ venv <> M.fromList [(name, overs) | ((name, _), (_, overs)) <- entries] | |||
((), (holes, newEndData, graph, _)) <- run venv kcStore ns $ withAliases aliases $ do | |||
((), (holes, newEndData, graph)) <- run venv kcStore newRoot $ withAliases aliases $ do |
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
It'd be more consistent with "globals"
to do the split outside run
here, or to use -!
above (as the old code did), but I'm not too bothered if you want to be different!
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
I don't think we need to change the split here, since we don't do anything with the new namespace
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
Super!! Thank you Craig :). I'll merge main
into inference-wip/fork
when this has gone in.
No description provided.