Agda-style case splitting for tactics #1379
Conversation
|
I'm not sure about that, but it would be better if we can move the cursor to the first generated sub-hole. (and preferably to the "next" hole if it generates none, but that's considerably harder, I guess.) |
|
@Ailrun good idea! It won't happen in this PR, but feel free to file an issue, and I'll get around to it at some point :) |
isovector
changed the title
| @@ -358,7 +471,7 @@ annotateDecl :: DynFlags -> LHsDecl GhcPs -> TransformT (Either String) (Anns, L | |||
| annotateDecl dflags ast = do | |||
| uniq <- show <$> uniqueSrcSpanT | |||
| let rendered = render dflags ast | |||
| (anns, expr') <- lift $ mapLeft show $ parseDecl dflags uniq rendered | |||
| (anns, expr') <- lift $ mapLeft show $ parseDecls dflags uniq rendered | |||
There was a problem hiding this comment.
Your parseDecls function seems to be an alternative version of addAnnotationsForPretty, which is specifically designed to add annotations to an AST element so that it is guaranteed to then parse again as the same AST. It may change layout in the process, but there are extensive tests to ensure that it does work for all ASTs.
There was a problem hiding this comment.
Unfortunately addAnnotationsForPretty doesn't work for newly generated code: alanz/ghc-exactprint#91
| -- | We can't compare 'RdrName' for equality directly. Instead, compare them by | ||
| -- their 'OccName's. | ||
| eqRdrName :: RdrName -> RdrName -> Bool | ||
| eqRdrName = (==) `on` occNameString . occName |
There was a problem hiding this comment.
Each RdrName is Located. The locations can be used as an index between the identifier location in the Parsed AST and the Renamed one, to get the exact identity, via the unique associated with a Name.
We used to construct this name map in HIE, it may still be in HLS. If not, here is it's source.
There was a problem hiding this comment.
Sorry, I'm not sure what you mean by this. The problem I was running into is that the RdrNames that come from VarPats have different locations than the RdrNames from HsVars.
There was a problem hiding this comment.
For each Located RdrName, if you look it up in the nameMap you will get the corresponding Name. If they are the same, as identified by the renaming phase, they will both have the same nameUnique value.
There was a problem hiding this comment.
Upon further thought, I'm not sure this will work for me. This is all a pass over parsed trees, before the renamer has had a chance to run. Since we're simplifying tactics' code, which doesn't ever shadow variables, I don't think this is a concern.
|
Please take another look. I think this is ready to be merged. |
This PR lets tactics manipulate
Matchnodes in the AST when the solved goal is at the top level. It shifts a top-level lambda into function arguments, and then splits top-level case statements into multipleMatches. It looks like this:The underlying tactic search isn't changed, this is all just implemented as a final transformation step in
I.P.T.CaseSplit.Most of the work in this PR is grafting the new matches into the old
ValD, which is a surprisingly tricky thing. @alanz --- is there an easier way to do this in ExactPrint?I've tagged @konn and @alanz to take a look at my ExactPrint changes. I'm not particularly proud of them, but this works and I don't know how to do it better.
@jneira you're my go-to person for changes to the tactics codebase. And @pepeiborra , github suggested I tag you, so feel free to review any bits that interest you (the null set is acceptable too!)
Fixes #582