Chore: Dafny to Rust refactorings #5513
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
Chore: Dafny to Rust refactorings - extern module as attribute - Type arguments with type bounds (can be tested) - Attributes handling - Type on Select field and TupleSelect - Name refactoring - every In - NoStatementBuffer - GenFormals - EmitNameAndActualTypeArgs (for classes) - ParseAttributes - GetExtractOverrideName (to be able to model Rust options) Dafny - StructBuild first argument to be an expression instead of a string - Apply and ApplyType - Type to TypeParamDecl - Formals to Fields, NamelessFormals to NamelessFields - Visibility to string - Self to SelfBorrowed - SeltMut to SelfBorrowedMut - Box/BoxNew (for attribute annotations) - bool - ToOwned (used in tail recursion) - IsImmutableConversion - Formal.self becomes Formal.selfBorrowed - Formal.selfMut becomes Formal.selfBorrowedMut - AssignMember and all new variants ExtractTuple and Index - ExprFromType - Lambda (makes code prettier) - Error handling - Debug for datatypes - No more system object, just any - New char encoding - int! - Refactoring of DafatypeValue's first argument - constant - GenIdent refactoring
…ng/dafny into chore-rust-refactorings
MikaelMayer
added
run-integration-tests
ssomayyajula
approved these changes
Jun 21, 2024
| datatype Primitive = Int | Real | String | Bool | Char | ||
|
|
||
| datatype NewtypeRange = | ||
| | U8 | I8 | U16 | I16 | U32 | I32 | U64 | I64 | U128 | I128 | BigInt | ||
| | NoRange | ||
|
|
||
| datatype Attribute = Attribute(name: string, args: seq<string>) | ||
|
|
||
| datatype DatatypeType = DatatypeType(path: seq<Ident>, attributes: seq<Attribute>) |
There was a problem hiding this comment.
Side note: we should eventually give this a better name
There was a problem hiding this comment.
Any suggestion? DataType? ResolvedDatatype ?
| @@ -509,15 +600,17 @@ module RAST | |||
| PrecedenceAssociativity(110, RightToLeft) | |||
| case _ => PrecedenceAssociativity(0, RequiresParentheses) | |||
| } | |||
| case Lambda(_, _, _) => PrecedenceAssociativity(300, LeftToRight) | |||
| case _ => UnknownPrecedence() | |||
| } | |||
|
|
|||
| ghost function Height(): nat { | |||
There was a problem hiding this comment.
Could turn ToString() into a big lexicographic induction
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.
NoStatementBufferto convertGenFormalsEmitNameAndActualTypeArgs(for classes)ParseAttributesGetExtractOverrideName(to be able to model Rust options) DafnyStructBuildfirst argument to be an expression instead of a stringApplysplit intoApplyfor expressions andApplyTypefor type argumentsTypetoTypeParamDeclso that we can support boundsFormalstoFields, andNamelessFormalstoNamelessFieldsVisibilityhas its own datatypeSelftoSelfBorrowedSeltMuttoSelfBorrowedMutBox/BoxNew(for attribute annotations)boolToOwned(used in tail recursion)IsImmutableConversionFormal.selfbecomesFormal.selfBorrowedFormal.selfMutbecomesFormal.selfBorrowedMutAssignMemberand all new variantsExtractTupleandIndexExprFromTypeto be able to simulate macros like expressionsLambda(makes code prettier)Debugtrait for datatypesstd::any::Anyint!macroconstantGenIdentrefactoringHow has this been tested?
Existing tests should just pass.
By submitting this pull request, I confirm that my contribution is made under the terms of the MIT license.