Error Node And Maybe Compilation Wrapper #129
Merged
Conversation
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
mariari
force-pushed
the
artem/maybe
branch
4 times, most recently
from
114d6e9 to
68f084d
Compare
Fixes the compilation of STLC to Geb discarding previous uncurrying changes in favour of uncurrying only the final result. Further this commit adds tests to make sure that furhter issues from this problem does not happen
This includes the generic function and all valid instances, and documentation for how it works
Adds an error node of an arbitrary type as a new STLC constructor. Appropriatelly changes the compilation procedure to Geb in case an STLC term has an error subterm and wraps the compilation in a Maybe monad.
mariari
reviewed
May 30, 2023
Comment on lines
+136
to
+230
| (labels ((rec (context tterm) | ||
| (match-of stlc tterm | ||
| ((absurd tcod term) | ||
| (comp (mcase (->left so1 (maybe-rest tcod)) | ||
| (init (maybe-comp tcod))) | ||
| (rec context term))) | ||
| (unit | ||
| (comp (->right so1 so1) | ||
| (terminal (stlc-ctx-maybe context)))) | ||
| ((left rty term) | ||
| (comp (->right so1 (maybe-rest (ttype tterm))) | ||
| (comp (->left (maybe-comp (ttype term)) | ||
| (maybe-comp rty)) | ||
| (rec context term)))) | ||
| ((right lty term) | ||
| (comp (->right so1 (maybe-rest (ttype tterm))) | ||
| (comp (->right (maybe-comp lty) | ||
| (maybe-comp (ttype term))) | ||
| (rec context term)))) | ||
| ((case-on on ltm rtm) | ||
| (let ((mcartoon (mcar (ttype on))) | ||
| (mcadrtoon (mcadr (ttype on))) | ||
| (ctx (stlc-ctx-maybe context))) | ||
| (comp (mcase (comp (->left so1 (maybe-rest (ttype tterm))) | ||
| (terminal (prod ctx so1))) | ||
| (comp (mcase (commutes-left | ||
| (rec | ||
| (cons mcartoon | ||
| context) | ||
| ltm)) | ||
| (commutes-left | ||
| (rec | ||
| (cons mcadrtoon | ||
| context) | ||
| rtm))) | ||
| (distribute ctx | ||
| (maybe-comp mcartoon) | ||
| (maybe-comp mcadrtoon)))) | ||
| (comp (distribute ctx | ||
| so1 | ||
| (maybe-rest (coprod mcartoon | ||
| mcadrtoon))) | ||
| (geb:pair ctx (rec context on)))))) | ||
| ((pair ltm rtm) | ||
| (let ((lty (ttype ltm)) | ||
| (rty (ttype rtm))) | ||
| (comp (->right so1 (prod (maybe-comp lty) | ||
| (maybe-comp rty))) | ||
| (geb:pair (rec context ltm) | ||
| (rec context rtm))))) | ||
| ((fst term) | ||
| (let ((mcarttot (mcar (ttype term)))) | ||
| (comp (mcase (->left so1 (maybe-rest mcarttot)) | ||
| (<-left (maybe-comp mcarttot) | ||
| (maybe (mcadr (ttype term))))) | ||
| (rec context term)))) | ||
| ((snd term) | ||
| (let ((mcadrttot (mcadr (ttype term)))) | ||
| (comp (mcase (->left so1 (maybe-rest mcadrttot)) | ||
| (<-right (maybe-comp (mcar (ttype term))) | ||
| (maybe-comp mcadrttot))) | ||
| (rec context term)))) | ||
| ((lamb tdom term) | ||
| (comp (->right so1 (maybe-rest (fun-to-hom (ttype tterm)))) | ||
| (apply-n (length tdom) | ||
| #'(lambda (x) (curry (commutes-left x))) | ||
| (rec (append | ||
| (mapcar #'maybe-comp tdom) | ||
| context) term)))) | ||
| ((app fun term) | ||
| (let ((tofun (ttype fun))) | ||
| (comp | ||
| (mcase (->left so1 (maybe-rest tofun)) | ||
| (commutes-left | ||
| (so-eval (maybe-comp (mcar tofun)) | ||
| (maybe-comp (mcadr tofun))))) | ||
| (comp (distribute (reduce #'prod | ||
| (mapcar #'maybe-comp term) | ||
| :from-end t) | ||
| so1 | ||
| (maybe-rest tofun)) | ||
| (geb:pair (reduce #'geb:pair | ||
| (mapcar #'(lambda (x) (rec context x)) term) | ||
| :from-end t) | ||
| (rec context | ||
| fun)))))) | ||
| ((index pos) | ||
| (stlc-ctx-proj (mapcar #'maybe context) pos)) | ||
| ((err ttype) | ||
| (comp (->left so1 (maybe-comp ttype)) | ||
| (terminal (stlc-ctx-maybe context))))))) | ||
| (if (not (well-defp context tterm)) | ||
| (error "not a well-defined ~A in said ~A" tterm context) | ||
| (rec context (ann-term1 context tterm))))) | ||
|
|
There was a problem hiding this comment.
The most painful kind of copy and paste.
Let us remove this with a better strategy later, or find a way to abstract it if it has to live here long term
mariari
reviewed
May 30, 2023
Comment on lines
-101
to
+289
| ((left term) | ||
| (let ((tott (ttype tterm))) | ||
| (comp (->left (mcar tott) (mcadr tott)) | ||
| (rec context term)))) | ||
| ((right term) | ||
| (let ((tott (ttype tterm))) | ||
| (comp (->right (mcar tott) (mcadr tott)) | ||
| (rec context term)))) | ||
| ((left rty term) | ||
| (comp (->left (ttype term) rty) | ||
| (rec context term))) | ||
| ((right lty term) | ||
| (comp (->right lty (ttype term)) | ||
| (rec context term))) |
There was a problem hiding this comment.
You should do these kinds of changes in a different topic, if they are unrelated to your changes.
This was referenced May 31, 2023
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
Add this suggestion to a batch that can be applied as a single commit.
This suggestion is invalid because no changes were made to the code.
Suggestions cannot be applied while the pull request is closed.
Suggestions cannot be applied while viewing a subset of changes.
Only one suggestion per line can be applied in a batch.
Add this suggestion to a batch that can be applied as a single commit.
Applying suggestions on deleted lines is not supported.
You must change the existing code in this line in order to create a valid suggestion.
Outdated suggestions cannot be applied.
This suggestion has been applied or marked resolved.
Suggestions cannot be applied from pending reviews.
Suggestions cannot be applied on multi-line comments.
Suggestions cannot be applied while the pull request is queued to merge.
Suggestion cannot be applied right now. Please check back later.
Adds an error node to the STLC class with possibility to be of an arbitrary type specified by the user. Appropriate helper functions added, such as
errorp. Given that a term fed into the compiler now has an error subterm, it will be compiled thorough a Maybe monad as specified byto-cat-errotherwise compiling as usual without waste of computational resources.Adds test cases for casing compilation to Geb to showcase how the interpreter can help with evaluating errors and where they appear in the STLC code.
This solves issue #90 but further improvements need to be had