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.

Sign up for GitHub

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

Jump to bottom

Add Multiple Argument Functionality to STLC Interface #115

Merged
merged 4 commits into from
May 7, 2023
Merged

Add Multiple Argument Functionality to STLC Interface #115

merged 4 commits into from
May 7, 2023

Conversation

agureev
Copy link
Collaborator

@agureev agureev commented May 3, 2023

This commit adds following functionality:

  1. lamb now accepts a list of types for its tdom accessor allowing for functions to be defined in a complex context. The domain of such a lambda term will then be the iterated product.

  2. 'app' now accepts a list of terms for its term accessor allowing for a multi-argument function to be iteratively applied.

  3. Change index functionality to follow usual convention of reading contexts from left to right.

  4. Change the STLC -> GEB compilation to be uncurried solving Uncurry Pipeline Usage #106 and allowing for a neater solution to Geb should expose VampIR error conditions through its STLC API #90

@agureev agureev requested a review from mariari May 3, 2023 13:28
@rokopt rokopt mentioned this pull request May 3, 2023
Closed
@agureev agureev force-pushed the artem/multi-lambda branch from 1ca7e1f to 0e383e0 Compare May 4, 2023 09:47
@agureev agureev requested a review from rokopt May 4, 2023 09:52
@agureev
Copy link
Collaborator Author

agureev commented May 4, 2023

Adding @rokopt as a new reviewer to receive approval on the new compilation pass. Note that the application interpretation follows from composition-as-substitution definition in the term model.

@agureev agureev force-pushed the artem/multi-lambda branch 2 times, most recently from e716b3f to 56d088a Compare May 4, 2023 12:48
@mariari mariari force-pushed the artem/multi-lambda branch 2 times, most recently from 1fd156d to 4a10cd5 Compare May 5, 2023 04:43
mariari
mariari requested changes May 5, 2023
View reviewed changes
Copy link
Member

@mariari mariari left a comment

Choose a reason for hiding this comment

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

I'd like to see updated docs on the classes. Since the semantics of lambda and app changed, I wish for the class documentation to be updated to reflect this, and type signatures added to the classes and constructors as well, so I can see them at a glance.

Overall after some docs changes I did manually the pr seems to work, I want the HOF example put into a test as well

src/util/utils.lisp Outdated
Comment on lines 210 to 219
(defun apply-n (times f initial)
(let ((value initial))
(dotimes (n times value)
(setf value (funcall f value)))))
Copy link
Member

Choose a reason for hiding this comment

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

Probably would good to have a doc string with this

src/lambda/lambda.lisp
Comment on lines +58 to +59
(nth i ctx)
(error "Argument exceeds length of context"))))
Copy link
Member

Choose a reason for hiding this comment

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

Yeah much nicer

src/lambda/lambda.lisp
@@ -121,10 +121,10 @@ functions taking in context and terms below as well."))
(if (typep type-of-term 'prod)
(snd ann-term :ttype (mcadr type-of-term))
(error "type of term not of product type"))))
((lamb tdom term) (let ((ant (ann-term1 (cons tdom ctx) term)))
((lamb tdom term) (let ((ant (ann-term1 (append tdom ctx) term)))
Copy link
Member

Choose a reason for hiding this comment

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

This causes tests to fail, as tdom is still so1 in some situations

Copy link
Member

Choose a reason for hiding this comment

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

With the merged commits this is no longer an issue

src/lambda/lambda.lisp
Comment on lines -136 to +149
(ann-left (ann-term1 (cons (mcar type-of-on) ctx) ltm))
(ann-left (ann-term1 (cons (mcar type-of-on) ctx) ltm))
Copy link
Member

Choose a reason for hiding this comment

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

Seems like a needless change that makes formatting worse

src/lambda/trans.lisp Outdated
fun)
(rec context
term)))))
(comp (rec context fun)
Copy link
Member

Choose a reason for hiding this comment

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

change

(comp  (rec context fun) ...)

into

(comp (rec context fun) ...)

src/specs/lambda.lisp
Comment on lines +336 to +364
The intended semnatics are: [TDOM][generic-function] is a list of types (and
hence a list of [SUBSTOBJ][GEB.SPEC:SUBSTOBJ]) whose iterative product of
components form the domain of the function type. [TERM][generic-function]
is a term (and hence an [STLC][type]) of the codomain of the function type
gotten in the context to whom we append the list of the domains.
Copy link
Member

Choose a reason for hiding this comment

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

Some of these docs need to propagate into the class docs

@agureev agureev force-pushed the artem/multi-lambda branch from 4a10cd5 to 27315c9 Compare May 5, 2023 16:28
@mariari mariari force-pushed the artem/multi-lambda branch 4 times, most recently from 97cf2dc to dc40019 Compare May 7, 2023 19:48
@agureev @mariari
Apply-n Utility Added
b040949 
Adds a utility function applying a given function
n-times recursively. Useful for iterative calls
of Geb functions.
@mariari mariari force-pushed the artem/multi-lambda branch from dc40019 to 89299f8 Compare May 7, 2023 19:48
agureev added 2 commits May 8, 2023 03:52
@agureev @mariari
New Lambda and Application API
e0cc20a 
Updates lambda term API and documentation for multi-domain
function-forming. Additionally, curries the compilation pass.

Introduces a new API for function application term
allowing for a multi-value function to be applied
to several arguments.

Fixes tests accordingly.
@agureev @mariari
Add Tests
3ec5428 
Adds tests for multi-argument interface of lambda and
function application terms.
@mariari mariari force-pushed the artem/multi-lambda branch from 89299f8 to 6465c06 Compare May 7, 2023 19:52
@agureev @mariari
Add Documentation and Typing for STLC Terms
9ad208d 
Add lambda documentation specifying the indexing of free variables.

Adds more documentation for upgraded STLC API and adds typing so that
the constructors of STLC do not accept arguments other than the ones
intended by the operational semantics.

Further adds some examples of some uses of lambda
@mariari mariari force-pushed the artem/multi-lambda branch from 6465c06 to 9ad208d Compare May 7, 2023 19:58
rokopt
rokopt approved these changes May 7, 2023
View reviewed changes
Copy link
Member

@rokopt rokopt left a comment

Choose a reason for hiding this comment

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

This makes sense to me -- thank you!

As a general comment: I suggest we ask the Juvix team how much it'll take for them to adapt to the change to the indexing; if it's at all difficult then we could provide a utility that just syntactically transforms a program written with the old indexing to one written with the new.

@mariari mariari merged commit 113f15b into main May 7, 2023
This was referenced May 9, 2023
Open
Closed
Open
@jonaprieto jonaprieto deleted the artem/multi-lambda branch July 10, 2023 14:51
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Reviewers

@mariari mariari mariari requested changes

@rokopt rokopt rokopt approved these changes

Assignees
No one assigned
Labels
None yet
Projects
None yet
Milestone
No milestone
Development

Successfully merging this pull request may close these issues.
3 participants
@agureev @rokopt @mariari