Laurel parsing #1
Draft
Conversation
This file contains hidden or 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
…-org#221) This modifies the Lean expression generation for dialects to reduce time required to declaring dialects by roughly half. also generates auxilary definitions to reduce the size of the Lean expression for a Strata program. This has a slight performance improvement, but more importantly reduces the stack requirements when parsing large Strata programs. By submitting this pull request, I confirm that you can use, modify, copy, and redistribute this contribution, under the terms of your choice.
*Description of changes:* This pull request updates the expression evaluator (`SemanticEval` in Strata) which previously needed to take two states: one for old expressions, one for normal (‘new’) expressions, but after this pull request it takes only one state. It introduces a couple of `sorry`s, but these will be eventually fixed. By submitting this pull request, I confirm that you can use, modify, copy, and redistribute this contribution, under the terms of your choice.
*Description of changes:* * Reorganize the Python-specific Boogie prelude. * Add PyFactory, a Python-specific Lambda factory that -- for now -- contains a candidate model for Python's `re.compile`. * Turn on elimination of irrelevant axioms for Python analyses. * Suppress any counterexample parsing errors from a SAT solver. By submitting this pull request, I confirm that you can use, modify, copy, and redistribute this contribution, under the terms of your choice. --------- Co-authored-by: Juneyoung Lee <lebjuney@amazon.com> Co-authored-by: Juneyoung Lee <136006969+aqjune-aws@users.noreply.github.com> Co-authored-by: Andrew Wells <130512013+andrewmwells-amazon@users.noreply.github.com>
Add pyAnalyze tests. Inline procedure calls. Move test_helper procedure spec to asserts within body. By submitting this pull request, I confirm that you can use, modify, copy, and redistribute this contribution, under the terms of your choice.
Right now, `TypeFactory` is separate from `LContext` (e.g. in `Lambda.typeCheckAndPartialEval`). This PR bundles them together, simplifying `typeCheckAndPartialEval`, unifying the typechecking for datatypes, and making it possible to add datatypes to Boogie. By submitting this pull request, I confirm that you can use, modify, copy, and redistribute this contribution, under the terms of your choice. --------- Co-authored-by: Josh Cohen <cohenjo@amazon.com>
…trata-org#259) pyTranslate and pyAnalyze search for the Python dialect using a search path despite being known at compile time. This changes Strata main to use the builtin version.
*Issue #, if available:* *Description of changes:* Adds a dependency on Plausible, and creates a number of generators which ultimately allow generating random `LExpr`s which are well-typed, labelled with `LMonoTy`s (and random metadata). Some caveats: - An instance of `Arbitrary` will need to be supplied for the metadata types (in our examples we use `Unit` which has a default instance). - The generators were created using Chamelean (https://github.com/codyroux/plausible), when possible and cleaned up a bit by hand. We've removed all the calls to the Chamelean generators, to avoid taking that dependency, but left them in comments, as documentation. - We use a typing relation derived from `LExpr.HasType`, to allow for easier generation, and remove polymorphism for the time being. - We show examples of how to use these generators for conformance tests, but things can be more convenient with additional helper functions. By submitting this pull request, I confirm that you can use, modify, copy, and redistribute this contribution, under the terms of your choice.
**Description of changes:** Adding ``strata`` and ``BoogieToGoto`` to default targets list. This ensures that all binaries are generated when running ``lake build``. My assumption here is that this was omitted by mistake, but feel free to discard this PR if that was intentional. By submitting this pull request, I confirm that you can use, modify, copy, and redistribute this contribution, under the terms of your choice. Co-authored-by: Vidas Jocius <vjjocius@users.noreply.github.com>
*Issue #, if available:* *Description of changes:* By submitting this pull request, I confirm that you can use, modify, copy, and redistribute this contribution, under the terms of your choice.
…rg#216) Makes some definitions cleaner as they no longer need angle brackets or `{ss := _}`. `Block` is now an `abbrev` for `List Stmt`, and we don't need both `Stmts` and `Block`. This makes the semantics for statements cleaner. This also includes an induction principle for the new version of `Stmt`, though it is unused right now. By submitting this pull request, I confirm that you can use, modify, copy, and redistribute this contribution, under the terms of your choice. --------- Co-authored-by: Josh Cohen <cohenjo@amazon.com> Co-authored-by: Andrew Wells <130512013+andrewmwells-amazon@users.noreply.github.com> Co-authored-by: Andrew Wells <anmwells@amazon.com>
keyboardDrummer
force-pushed
the
laurelParsing
branch
from
2a8e129 to
f3bf3a5
Compare
*Issue #, if available:* *Description of changes:* This is a pull request that adds abstract definitions of date, datetime and timedelta for Python. Datetime is abstractly defined as a pair of (base time, relative timedelta). datetime.now() returns (<the curent datetime>, 0). Adding or subtracting datetime.timedelta updates the relative timedelta field. This is co-authored with @andrewmwells-amazon . By submitting this pull request, I confirm that you can use, modify, copy, and redistribute this contribution, under the terms of your choice. --------- Co-authored-by: Andrew Wells <anmwells@amazon.com>
Addresses TODO in in-progress documentation (PR strata-org#186) By submitting this pull request, I confirm that you can use, modify, copy, and redistribute this contribution, under the terms of your choice. Co-authored-by: Josh Cohen <cohenjo@amazon.com>
## Add DDM Unwrap Capability via Metadata
Adds the ability to unwrap declared category types using @[unwrap]
metadata, generating constructors with raw types instead of Ann
wrappers.
## Usage
op index (@[unwrap] id : Num) : Expression => id;
Generates `Expression.index : α → Nat → Expression α` instead of `α →
Ann Nat α → Expression α`.
Works for all declared categories: Num, Ident, Str, Decimal, ByteArray.
## Implementation
* Added unwrap metadata to StrataDDL dialect
* Elaboration checks argument metadata and unwraps accordingly
* Updated code generation and serialization
* Test: StrataTest/DDM/UnwrapSimple.lean
---------
Co-authored-by: Andrew Wells <130512013+andrewmwells-amazon@users.noreply.github.com>
…#276) *Description of changes:* This change removes `__init__.py` and refactors the imports in the Strata Python bindings package accordingly so that it is exposed as a [native namespace package](https://packaging.python.org/en/latest/guides/packaging-namespace-packages/#native-namespace-packages). Consequently, other Python packages can be added to the `strata` namespace outside of the Strata repository. By submitting this pull request, I confirm that you can use, modify, copy, and redistribute this contribution, under the terms of your choice.
Support for classes. More precise support of datetime. By submitting this pull request, I confirm that you can use, modify, copy, and redistribute this contribution, under the terms of your choice. --------- Co-authored-by: Juneyoung Lee <lebjuney@amazon.com>
Fix pyAnalyze CI. The CI was printing an error message, but not exiting with an error code. By submitting this pull request, I confirm that you can use, modify, copy, and redistribute this contribution, under the terms of your choice.
Fixes strata-org#241 When `Options.quiet` is used (verbose := false), counterexamples are no longer displayed in verification output. This reduces the brittleness of the tests when different solver versions are used. ## Changes - Added `verbose` field to `VCResult` structure - Created `Result.formatWithVerbose` method to conditionally show counterexamples - Updated all `VCResult` creation sites to pass the verbose flag - Updated test expectations for quiet mode (removed CEx from expected output) All tests pass successfully. --------- Co-authored-by: Vidas Jocius <vjjocius@users.noreply.github.com> Co-authored-by: Shilpi Goel <shigoel@gmail.com>
*Issue #, if available:* *Description of changes:* This PR fixes a minor bug in which incorrectly typed `LExpr`s could be generated (with free variables not in context). It also: - Avoids generating lambdas - Improves generating terms that actually use functions in the factory, by introducing redundant typing rules that encourage generating fully applied unary and binary functions. - Generate bit-vector constants with width various powers of 2. - Writes a bare bones generator for the Boogie functional fragment. By submitting this pull request, I confirm that you can use, modify, copy, and redistribute this contribution, under the terms of your choice. --------- Co-authored-by: Juneyoung Lee <136006969+aqjune-aws@users.noreply.github.com> Co-authored-by: Shilpi Goel <shigoel@gmail.com>
…ata-org#274) Before: `lake build 468.95s user 168.55s system 285% cpu 3:42.94 total`, 413 jobs After: `lake build 422.01s user 119.11s system 300% cpu 2:59.78 total`, 360 jobs `lake test` covers the moved example files By submitting this pull request, I confirm that you can use, modify, copy, and redistribute this contribution, under the terms of your choice. --------- Co-authored-by: Juneyoung Lee <136006969+aqjune-aws@users.noreply.github.com>
## Changes This adds support for boolean values in the DDM (Dialect Definition Metalanguage): ## Motivation This provides the foundation for dialects to use Lean boolean values in their abstract syntax tree fields. ## Testing The changes compile and all existing tests pass. --------- Co-authored-by: Andrew Wells <130512013+andrewmwells-amazon@users.noreply.github.com>
By submitting this pull request, I confirm that you can use, modify, copy, and redistribute this contribution, under the terms of your choice.
Switch Z3 timeout from soft to hard By submitting this pull request, I confirm that you can use, modify, copy, and redistribute this contribution, under the terms of your choice.
…ata-org#275) This adds more concrete evaluators for bit-vector operations. This will help the Plausible based test generators including the prototypes which will follow after strata-org#272 do much more interesting tests. This also changes the type of concreteEval to return Option LExpr, to allow deciding whether concrete eval has been successfully done without relying on Beq/DecidableEq. By submitting this pull request, I confirm that you can use, modify, copy, and redistribute this contribution, under the terms of your choice. --------- Co-authored-by: Shilpi Goel <shigoel@gmail.com> Co-authored-by: Aaron Tomb <aarotomb@amazon.com>
Add handling of while loops and FloorDiv. Increase types we support for Mult. By submitting this pull request, I confirm that you can use, modify, copy, and redistribute this contribution, under the terms of your choice.
Adds a document describing the semantics of Strata Core (consisting of `Lambda` and `Imperative` components). The document is written in Verso and imports the Strata library to allow docstrings to appear directly in the text. Note that Strata Core is not a new dialect, but rather a new name for the combination of `Lambda` and `Imperative`. It does not yet have a concrete syntax. Concrete syntax will likely be provided through an evolution of strata-org#224, to assist in the goal of keeping Strata Core as close to B3 as possible. By submitting this pull request, I confirm that you can use, modify, copy, and redistribute this contribution, under the terms of your choice. --------- Co-authored-by: Josh Cohen <cohenjo@amazon.com> Co-authored-by: Mikaël Mayer <MikaelMayer@users.noreply.github.com> Co-authored-by: Shilpi Goel <shigoel@gmail.com> Co-authored-by: Andrew Wells <130512013+andrewmwells-amazon@users.noreply.github.com>
Z3 `-T` param takes seconds By submitting this pull request, I confirm that you can use, modify, copy, and redistribute this contribution, under the terms of your choice. Co-authored-by: Shilpi Goel <shigoel@gmail.com>
This modifies PythonToBoogie translation to accept a signature data structure for types of builtin functions. By submitting this pull request, I confirm that you can use, modify, copy, and redistribute this contribution, under the terms of your choice. --------- Co-authored-by: Shilpi Goel <shigoel@gmail.com>
We need different solver configurations for some of our programs, but with the right configuration the solver finishes quickly. This adds a thin wrapper around Z3 that calls Z3 with various options set, each call with a 1s timeout. Currently calls to Z3 are not raced. By submitting this pull request, I confirm that you can use, modify, copy, and redistribute this contribution, under the terms of your choice.
Implements pipe-delimited identifiers (`|identifier|`) per SMT-LIB 2.6 specification. **Implementation:** - Parser: Handles `|identifier|` with escape sequences (`\|` → `|`, `\\` → `\`) - Formatter: Outputs pipe delimiters when needed, strips Lean's `«»` notation, re-escapes - Disambiguates `||` operator from `|identifier|` **Tests:** - Special characters: hyphens, spaces, `@#$`, Unicode, guillemets, numbers - Escape sequences verified in AST (not just round-trip) - Coexistence with `|` and `||` operators - Explicitly not supported: Binary `|` operator without surrounding spaces All tests pass.
Adds support for dots in identifiers to better support B3-style and Lean-style naming conventions without requiring pipe delimiters. ## Changes - Parser: Extended identifier character set to include `.`, `?`, and `!` - Formatter: Updated to match parser behavior - Tests: Added coverage with AST verification ## Examples - `qualified.name`, `x.y` (qualified names) - `free?`, `result!` (Lean-style suffixes)
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.
No description provided.