Skip to content
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

feat: add global references and arguments #10

Merged
merged 1 commit into from
Dec 30, 2024
Merged

feat: add global references and arguments #10

merged 1 commit into from
Dec 30, 2024

Conversation

govereau
Copy link
Collaborator

Add ability to capture global references, including function arguments when parsing kernels. Globals and arguments are directly encoded as KLR terms.

@govereau govereau added the enhancement New feature or request label Dec 28, 2024
@govereau govereau requested a review from seanmcl December 28, 2024 20:41
@govereau govereau self-assigned this Dec 28, 2024
@govereau govereau requested a review from jtristan as a code owner December 28, 2024 20:41
@govereau govereau enabled auto-merge (rebase) December 28, 2024 20:41
Add ability to capture global references, including function
arguments when parsing kernels.
NKL/Python.lean Show resolved Hide resolved
NKL/Python.lean Show resolved Hide resolved
NKL/Python.lean Show resolved Hide resolved
@@ -191,29 +210,30 @@ private def withPos (p : String -> Json -> Parser b) (f : b -> Pos -> a) : Json
return (f exp pos)
| _ => throw "expecting object"

def genError (source err : String) (pos : Pos) : String :=
Copy link
Collaborator

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Maybe an example of what you're parsing here would be nice.

-- evaluable in the default environment.
partial def global : Json -> Parser Expr'
| .null => return .const .none
| .obj (.node _ _ "fun" (.str s) _) => return .name s .load
Copy link
Collaborator

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

I still don't understand what .load does.

interop/nkl/parser.py Show resolved Hide resolved
@govereau govereau merged commit 18f41e4 into main Dec 30, 2024
1 check passed
@govereau govereau deleted the pg-globals branch December 30, 2024 16:41
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Labels
enhancement New feature or request
Projects
None yet
Development

Successfully merging this pull request may close these issues.

2 participants