Well-Definedness Predicate for Morphisms #150
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
Adds two new constrictors to the VampIR spec, allowing for making of the empty bracket used for induction on lists and of the curly brackets for function specification.
Adds a new primitive operation of conditional division to the VampIR spec. The primitive stands for the VampIR operation which is capable of dividing by 0, producing 0.
…ipeline-functions
Upgrade the Vamp-IR package to include basic functions of the library such as checking whether something is zero, checking whether a number is negative etc. Alongside that, arithmetic operations with appropriate range checks are introduced in order to be used in the upgraded pipeline which will allow for the compilation of natural number functions and predicates of fixed bitwidth.
Upgrades the standard library needed to compile JuvixCore functions containing natural numbers functions and predicates.
Introduces a new category SeqN with appropriate API alongside with the compilation of it to appropriate Vamp-IR code. SeqN can be thought of as a category of finite sequences of natural numbers with morphisms from (x1,...,xn) to (y1,...,ym) being Vamp-IR functions taking in n entries of sizes x1 to xn and spitting out m outputs of sizes y1 to ym.
Makes the so-eval function into a generic function in order to be compatible with further Geb extensions.
Upgrades the pipeline to now support compiling to Vamp-IR through SeqN. That includes adding natural number support for STLC, adding natural numbers in a Geb extension and subsequently upgrading appropriate compilation steps with a new pass from Geb to SeqN.
1) Upgrades gapply for Geb to allow interpetation of natural numbers extension morphisms whose inputs will be lists of natural numbers. 2) Adds gapply for SeqN, computing appropriate natural number inputs.
Updates test files to include interpretations of compiled STLC code in SeqN and other individual tests for interpreters in Geb and SeqN.
Introduces a well-defp-cat function to Geb and SeqN which takes in a morphism in the appropriate category and either gives true if the morphism is well-defined or produces an error message pointing to the point at which the moprhism fails to be well-defined, e.g. appropriate domains and codomains do not coincide for composition of morphisms.
mariari
force-pushed
the
artem/well-defp
branch
from
5318676 to
5bcfc00
Compare
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.
Introduces a
well-defp-catfunction to Geb and SeqN which takes in amorphism in the appropriate category and either gives true if the
morphism is well-defined or produces an error message pointing to the
point at which the morphism fails to be well-defined, e.g. appropriate
domains and codomains do not coincide for composition of morphisms.