-
Notifications
You must be signed in to change notification settings - Fork 261
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.
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
Feat: Rust operators and immutable collections #5081
Changes from all commits
0628309
7649600
06c65ba
5fc5bf4
b72cec9
c2f8b24
bed8f90
79f1503
4b0fae7
754022c
22a2897
ae3081c
705b1ca
13defc6
ded93a3
70e1dcf
6c6236a
aa3e84a
eccae5e
5ba5c93
c7fb7c0
770da14
70732a7
b09c1a0
21a0074
a2ef3f8
9704661
58229de
43c60ae
ec7188a
136b368
3cacd1f
eaad5be
71f2a08
2c1e7ee
42f3bd3
7e4457c
541d9fe
bc6ef02
70d95d5
e715090
2ede243
6d825fb
a4bbd0e
dca95f9
1a0c3f5
31c4a31
ab90d9d
a85a31c
b361f98
84a280c
bce6df2
79d9767
ec471f7
805628d
f204d29
6af66d2
fc489c7
450c34c
5b47e79
2c734f4
0de8444
084fd8f
fca0a64
48bb366
231b877
a667a51
2f2a34a
77d6fc0
8dd3e91
591a108
7df7a43
ab8713f
5c507ee
9d84841
e06ba55
974a622
978de94
494ec95
6185aea
7262e2e
2388a16
2ba549f
927e0ce
b8fa9be
ae9c6a5
8fa13f8
9fa45e9
b08160e
7a1112b
428edc1
ff40edc
628f55b
dc3e8eb
bd632f5
04f055e
1adb784
4b9323e
0787071
d160b19
94060a0
ea057e3
71f9e96
File filter
Filter by extension
Conversations
Jump to
Diff view
Diff view
There are no files selected for viewing
Original file line number | Diff line number | Diff line change |
---|---|---|
@@ -0,0 +1,11 @@ | ||
using System.Collections.Concurrent; | ||
using Microsoft.Dafny; | ||
|
||
namespace DafnyCore.Test; | ||
|
||
public class GeneratedDafnyTest { | ||
[Fact] | ||
public void TestDafnyGeneratedCode() { | ||
DafnyToRustCompilerCoverage.RASTCoverage.__default.TestExpr(); | ||
} | ||
} |
Large diffs are not rendered by default.
Original file line number | Diff line number | Diff line change |
---|---|---|
@@ -1,3 +1,22 @@ | ||
module {:extern "DAST.Format"} DAST.Format | ||
/* Cues about how to format different AST elements if necessary, | ||
e.g. to generate idiomatic code when needed. */ | ||
{ | ||
// Dafny AST compilation tenets: | ||
// - The Compiled Dafny AST should be minimal | ||
// - The generated code should look idiomatic and close to the original Dafny file if possible | ||
// Since the two might conflict, the second one is taken care of by adding formatting information | ||
|
||
datatype UnaryOpFormat = | ||
| NoFormat | ||
| CombineFormat | ||
datatype BinaryOpFormat = | ||
| NoFormat | ||
| ImpliesFormat | ||
| EquivalenceFormat | ||
| ReverseFormat | ||
} | ||
|
||
module {:extern "DAST"} DAST { | ||
import opened Std.Wrappers | ||
|
||
|
@@ -19,13 +38,22 @@ module {:extern "DAST"} DAST { | |
Set(element: Type) | | ||
Multiset(element: Type) | | ||
Map(key: Type, value: Type) | | ||
SetBuilder(element: Type) | | ||
MapBuilder(key: Type, value: Type) | | ||
Arrow(args: seq<Type>, result: Type) | | ||
Primitive(Primitive) | Passthrough(string) | | ||
TypeArg(Ident) | ||
|
||
datatype Primitive = Int | Real | String | Bool | Char | ||
|
||
datatype ResolvedType = Datatype(path: seq<Ident>) | Trait(path: seq<Ident>) | Newtype(Type) | ||
datatype NewtypeRange = | ||
There was a problem hiding this comment. Choose a reason for hiding this commentThe reason will be displayed to describe this comment to others. Learn more. Consider naming something like There was a problem hiding this comment. Choose a reason for hiding this commentThe reason will be displayed to describe this comment to others. Learn more. As per the previous comment, I'm not renaming this to IntegerNewtypeRange because it accounts for other possible ranges in the future. |
||
| U8 | I8 | U16 | I16 | U32 | I32 | U64 | I64 | U128 | I128 | BigInt | ||
| NoRange | ||
There was a problem hiding this comment. Choose a reason for hiding this commentThe reason will be displayed to describe this comment to others. Learn more. What's the difference between There was a problem hiding this comment. Choose a reason for hiding this commentThe reason will be displayed to describe this comment to others. Learn more. More newtypes are coming which are not just integers, like sequences. They will get NoRange instead of BigInt until we might find other categories for them. |
||
|
||
datatype ResolvedType = | ||
| Datatype(path: seq<Ident>) | ||
| Trait(path: seq<Ident>) | ||
| Newtype(baseType: Type, range: NewtypeRange, erase: bool) | ||
|
||
datatype Ident = Ident(id: string) | ||
|
||
|
@@ -37,7 +65,7 @@ module {:extern "DAST"} DAST { | |
|
||
datatype DatatypeCtor = DatatypeCtor(name: string, args: seq<Formal>, hasAnyArgs: bool /* includes ghost */) | ||
|
||
datatype Newtype = Newtype(name: string, typeParams: seq<Type>, base: Type, witnessStmts: seq<Statement>, witnessExpr: Option<Expression>) | ||
datatype Newtype = Newtype(name: string, typeParams: seq<Type>, base: Type, range: NewtypeRange, witnessStmts: seq<Statement>, witnessExpr: Option<Expression>) | ||
|
||
datatype ClassItem = Method(Method) | ||
|
||
|
@@ -47,14 +75,18 @@ module {:extern "DAST"} DAST { | |
|
||
datatype Method = Method(isStatic: bool, hasBody: bool, overridingPath: Option<seq<Ident>>, name: string, typeParams: seq<Type>, params: seq<Formal>, body: seq<Statement>, outTypes: seq<Type>, outVars: Option<seq<Ident>>) | ||
|
||
datatype CallName = | ||
Name(name: string) | | ||
MapBuilderAdd | MapBuilderBuild | SetBuilderAdd | SetBuilderBuild | ||
|
||
datatype Statement = | ||
DeclareVar(name: string, typ: Type, maybeValue: Option<Expression>) | | ||
Assign(lhs: AssignLhs, value: Expression) | | ||
If(cond: Expression, thn: seq<Statement>, els: seq<Statement>) | | ||
Labeled(lbl: string, body: seq<Statement>) | | ||
While(cond: Expression, body: seq<Statement>) | | ||
Foreach(boundName: string, boundType: Type, over: Expression, body: seq<Statement>) | | ||
Call(on: Expression, name: string, typeArgs: seq<Type>, args: seq<Expression>, outs: Option<seq<Ident>>) | | ||
Call(on: Expression, callName: CallName, typeArgs: seq<Type>, args: seq<Expression>, outs: Option<seq<Ident>>) | | ||
Return(expr: Expression) | | ||
EarlyReturn() | | ||
Break(toLabel: Option<string>) | | ||
|
@@ -72,13 +104,21 @@ module {:extern "DAST"} DAST { | |
|
||
datatype BinOp = | ||
Eq(referential: bool, nullable: bool) | | ||
Neq(referential: bool, nullable: bool) | | ||
Div() | EuclidianDiv() | | ||
Mod() | EuclidianMod() | | ||
Implies() | // TODO: REplace by Not Or | ||
Lt() | // a <= b is !(b < a) | ||
LtChar() | | ||
Plus() | Minus() | Times() | | ||
BitwiseAnd() | BitwiseOr() | BitwiseXor() | | ||
BitwiseShiftRight() | BitwiseShiftLeft() | | ||
And() | Or() | | ||
In() | | ||
NotIn() | // TODO: Replace by Not In | ||
SetDifference() | | ||
SeqProperPrefix() | SeqPrefix() | | ||
SetMerge() | SetSubtraction() | SetIntersection() | | ||
Subset() | ProperSubset() | SetDisjoint() | | ||
MapMerge() | MapSubtraction() | | ||
MultisetMerge() | MultisetSubtraction() | MultisetIntersection() | | ||
Submultiset() | ProperSubmultiset() | MultisetDisjoint() | | ||
Concat() | | ||
Passthrough(string) | ||
|
||
|
@@ -94,18 +134,26 @@ module {:extern "DAST"} DAST { | |
SeqConstruct(length: Expression, elem: Expression) | | ||
SeqValue(elements: seq<Expression>, typ: Type) | | ||
SetValue(elements: seq<Expression>) | | ||
MultisetValue(elements: seq<Expression>) | | ||
MapValue(mapElems: seq<(Expression, Expression)>) | | ||
MapBuilder(keyType: Type, valueType: Type) | | ||
SeqUpdate(expr: Expression, indexExpr: Expression, value: Expression) | | ||
MapUpdate(expr: Expression, indexExpr: Expression, value: Expression) | | ||
SetBuilder(elemType: Type) | | ||
ToMultiset(Expression) | | ||
This() | | ||
Ite(cond: Expression, thn: Expression, els: Expression) | | ||
UnOp(unOp: UnaryOp, expr: Expression) | | ||
BinOp(op: BinOp, left: Expression, right: Expression) | | ||
UnOp(unOp: UnaryOp, expr: Expression, format1: Format.UnaryOpFormat) | | ||
BinOp(op: BinOp, left: Expression, right: Expression, format2: Format.BinaryOpFormat) | | ||
ArrayLen(expr: Expression, dim: nat) | | ||
MapKeys(expr: Expression) | | ||
MapValues(expr: Expression) | | ||
Select(expr: Expression, field: string, isConstant: bool, onDatatype: bool) | | ||
SelectFn(expr: Expression, field: string, onDatatype: bool, isStatic: bool, arity: nat) | | ||
Index(expr: Expression, collKind: CollKind, indices: seq<Expression>) | | ||
IndexRange(expr: Expression, isArray: bool, low: Option<Expression>, high: Option<Expression>) | | ||
TupleSelect(expr: Expression, index: nat) | | ||
Call(on: Expression, name: Ident, typeArgs: seq<Type>, args: seq<Expression>) | | ||
Call(on: Expression, callName: CallName, typeArgs: seq<Type>, args: seq<Expression>) | | ||
Lambda(params: seq<Formal>, retType: Type, body: seq<Statement>) | | ||
BetaRedex(values: seq<(Formal, Expression)>, retType: Type, expr: Expression) | | ||
IIFE(name: Ident, typ: Type, value: Expression, iifeBody: Expression) | | ||
|
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
nit: inconsistent naming. Probably better to always end with
Format