Parse all DefaultFun builtin functions. #4546
Conversation
effectfully
left a comment
effectfully
left a comment
There was a problem hiding this comment.
LGTM. It would be nice to generalize the machinery, though.
| builtinFunction = lexeme $ choice $ map parseBuiltin [minBound .. maxBound] | ||
| where parseBuiltin builtin = try $ string (display builtin) >> pure builtin |
There was a problem hiding this comment.
Given that we know a builtin is expected here, we could parse a raw textual name and then look it up in a cached Map Text fun. I don't think we care about performance here though, so that definition should be perfectly fine.
There was a problem hiding this comment.
It does seem somewhat wasteful to print every builtin each time we try to parse one!
There was a problem hiding this comment.
I think I just did it?
| , (MkNilPairData,"mkNilPairData") | ||
| ] | ||
|
|
||
| builtinFunction :: Parser DefaultFun |
There was a problem hiding this comment.
Generalize to an arbitrary fun (implementing Pretty, Bounded etc)?
There was a problem hiding this comment.
The parser can only parse terms in the DefaultUni and is a DefaultFun...the old parser also did that. (Now a parsable term is Term Name DefaultUni DefaultFun SourcePos). I can still parse it more generically but it probably still won't work for other funs.
There was a problem hiding this comment.
I think we decided to leave the current parser monomorphic for now. I think we can leave making it generic over universes for a future chunk of work.
There was a problem hiding this comment.
I did add a comment reminding people that only DefaultFun will work. Will the error be easier to read this way? Or maybe restricting the parser to DefaultFun will show better errors I think? If so I'll drop the last commit and make it parse to DefaultFun only.
There was a problem hiding this comment.
Oh, I see you generalized it anyway. That seems fine!
There was a problem hiding this comment.
I think we can leave making it generic over universes for a future chunk of work.
I'm not suggesting to make it generic over universes. It's harder and we have only one universe anyway. However generalizing over sets of built-in functions is fairly trivial and we do have multiple of them. I don't really care, just proposing.
thealmarty
force-pushed
the
thealmarty/autogen-builtins-parser
branch
from
0a6a6f0 to
50adb0c
Compare
| mkCachedBuiltin :: [DefaultFun] -> Map T.Text DefaultFun -> Map T.Text DefaultFun | ||
| mkCachedBuiltin (hdFns:tlFns) builtinMap = | ||
| mkCachedBuiltin tlFns (insert (display hdFns) hdFns builtinMap) | ||
| mkCachedBuiltin [] builtinMap = builtinMap |
There was a problem hiding this comment.
Nitpicking (i.e. not important at all): instead of writing the recursion manually you define mkCachedBuiltin as Map.fromList . map (\fun -> (display fun, fun)) or something like that.
There was a problem hiding this comment.
yeah HLint told me to do that too but I thought it's harder to read. Maybe not. I can change that. I was gonna open a follow up PR for the error anyway.
| builtinFunction = lexeme $ do | ||
| txt <- takeWhileP (Just "identifier") isIdentifierChar | ||
| case lookup txt cachedBuiltin of | ||
| Nothing -> error $ "Not a builtin" <> show cachedBuiltin <> show txt |
There was a problem hiding this comment.
You shouldn't call error here! There's nothing exceptional about a bulitin not being recognized. The Parser monad allows you to throw an error in it. I think the right function is customFailure, but not sure.
There was a problem hiding this comment.
Oh, yeah, the error to throw is UnknownBuiltinFunction from ParserError.
There was a problem hiding this comment.
Yes, thank you! I was rushing to merge the rest so that the blocked PR can go through. I want to show the cachedBuiltin somehow, I think it's useful to see. I'll work on that today.
As mentioned in #4368. It's similar to before the megaparsec merge, but now it parses to
DefaultFun.Pre-submit checklist: