Skip to content

Commit

Permalink
Feat rust classes traits arrays (#5591)
Browse files Browse the repository at this point in the history 
### Description
Lots of updates in the Rust compiler.

It's easier to review commit by commit

<small>By submitting this pull request, I confirm that my contribution
is made under the terms of the [MIT
license](https://github.com/dafny-lang/dafny/blob/master/LICENSE.txt).</small>

---------

Co-authored-by: Siva Somayyajula <[email protected]>
Co-authored-by: Fabio Madge <[email protected]>
  • Loading branch information
@MikaelMayer @fabiomadge
3 people authored Jul 9, 2024
1 parent bf592b8 commit 2c4dd00
Show file tree
Hide file tree
Showing 55 changed files with 17,519 additions and 6,721 deletions.
212 changes: 106 additions & 106 deletions Source/DafnyCore.Test/GeneratedFromDafny/DafnyToRustCompilerCoverage_RASTCoverage.cs
View file

Large diffs are not rendered by default.

131 changes: 109 additions & 22 deletions Source/DafnyCore/Backends/Dafny/AST.dfy
View file
Original file line number Diff line number Diff line change
Expand Up @@ -29,6 +29,7 @@ module {:extern "DAST.Format"} DAST.Format

module {:extern "DAST"} DAST {
import opened Std.Wrappers
import Std

// Prevents Dafny names to being direclty integrated into Rust without explicit conversion
// Make it a newtype once newtypes are compatible with standard library
Expand All @@ -42,11 +43,11 @@ module {:extern "DAST"} DAST {
| Class(Class)
| Trait(Trait)
| Newtype(Newtype)
| SynonymType(SynonymType)
| Datatype(Datatype)

datatype Type =
Path(seq<Ident>, typeArgs: seq<Type>, resolved: ResolvedType) |
Nullable(Type) |
UserDefined(resolved: ResolvedType) |
Tuple(seq<Type>) |
Array(element: Type, dims: nat) |
Seq(element: Type) |
Expand All @@ -57,9 +58,45 @@ module {:extern "DAST"} DAST {
MapBuilder(key: Type, value: Type) |
Arrow(args: seq<Type>, result: Type) |
Primitive(Primitive) | Passthrough(string) |
TypeArg(Ident)
TypeArg(Ident) | Object()
{
function Replace(mapping: map<Type, Type>): Type {
if this in mapping then mapping[this] else
match this {
case UserDefined(resolved: ResolvedType) =>
Type.UserDefined(resolved.Replace(mapping))
case Tuple(arguments) =>
Type.Tuple(Std.Collections.Seq.Map(
t requires t in arguments => t.Replace(mapping), arguments))
case Array(element, dims) =>
Type.Array(element.Replace(mapping), dims)
case Seq(element) =>
Type.Seq(element.Replace(mapping))
case Set(element) =>
Type.Set(element.Replace(mapping))
case Multiset(element) =>
Type.Multiset(element.Replace(mapping))
case Map(key, value) =>
Type.Map(key.Replace(mapping), value.Replace(mapping))
case SetBuilder(element) =>
Type.SetBuilder(element.Replace(mapping))
case MapBuilder(key, value) =>
Type.MapBuilder(key.Replace(mapping), value.Replace(mapping))
case Arrow(args: seq<Type>, result: Type) =>
Type.Arrow(Std.Collections.Seq.Map(
t requires t in args => t.Replace(mapping), args), result.Replace(mapping))
case Primitive(_) | Passthrough(_) | Object() | TypeArg(_) =>
this
}
}
}

datatype Variance =
| Nonvariant
| Covariant
| Contravariant

datatype TypeArgDecl = TypeArgDecl(name: Ident, bounds: seq<TypeArgBound>)
datatype TypeArgDecl = TypeArgDecl(name: Ident, bounds: seq<TypeArgBound>, variance: Variance)

datatype TypeArgBound =
| SupportsEquality
Expand All @@ -73,26 +110,66 @@ module {:extern "DAST"} DAST {

datatype Attribute = Attribute(name: string, args: seq<string>)

datatype DatatypeType = DatatypeType(path: seq<Ident>, attributes: seq<Attribute>)

datatype ResolvedType =
| Datatype(datatypeType: DatatypeType)
| Trait(path: seq<Ident>, attributes: seq<Attribute>)
| Newtype(baseType: Type, range: NewtypeRange, erase: bool, attributes: seq<Attribute>)
datatype DatatypeType = DatatypeType()

datatype TraitType = TraitType()

datatype NewtypeType = NewtypeType(baseType: Type, range: NewtypeRange, erase: bool)

datatype ResolvedTypeBase =
| Class()
| Datatype(variances: seq<Variance>)
| Trait()
| Newtype(baseType: Type, range: NewtypeRange, erase: bool)

datatype ResolvedType = ResolvedType(
path: seq<Ident>,
typeArgs: seq<Type>,
kind: ResolvedTypeBase,
attributes: seq<Attribute>,
properMethods: seq<Ident>,
extendedTypes: seq<Type>) {
function Replace(mapping: map<Type, Type>): ResolvedType {
ResolvedType(
path,
Std.Collections.Seq.Map(
t requires t in typeArgs => t.Replace(mapping), typeArgs),
match kind {
case Newtype(baseType, range, erase) =>
ResolvedTypeBase.Newtype(baseType.Replace(mapping), range, erase)
case _ => kind
},
attributes,
properMethods,
Std.Collections.Seq.Map(
t requires t in extendedTypes => t.Replace(mapping), extendedTypes)
)
}
}

datatype Ident = Ident(id: Name)

datatype Class = Class(name: Name, enclosingModule: Ident, typeParams: seq<TypeArgDecl>, superClasses: seq<Type>, fields: seq<Field>, body: seq<ClassItem>, attributes: seq<Attribute>)

datatype Trait = Trait(name: Name, typeParams: seq<TypeArgDecl>, body: seq<ClassItem>, attributes: seq<Attribute>)
datatype Trait = Trait(name: Name, typeParams: seq<TypeArgDecl>, parents: seq<Type>, body: seq<ClassItem>, attributes: seq<Attribute>)

datatype Datatype = Datatype(name: Name, enclosingModule: Ident, typeParams: seq<TypeArgDecl>, ctors: seq<DatatypeCtor>, body: seq<ClassItem>, isCo: bool, attributes: seq<Attribute>)

datatype DatatypeDtor = DatatypeDtor(formal: Formal, callName: Option<string>)

datatype DatatypeCtor = DatatypeCtor(name: Name, args: seq<DatatypeDtor>, hasAnyArgs: bool /* includes ghost */)

datatype Newtype = Newtype(name: Name, typeParams: seq<TypeArgDecl>, base: Type, range: NewtypeRange, witnessStmts: seq<Statement>, witnessExpr: Option<Expression>, attributes: seq<Attribute>)
datatype Newtype =
Newtype(
name: Name, typeParams: seq<TypeArgDecl>, base: Type,
range: NewtypeRange, constraint: Option<NewtypeConstraint>,
witnessStmts: seq<Statement>, witnessExpr: Option<Expression>, attributes: seq<Attribute>)

datatype NewtypeConstraint = NewtypeConstraint(variable: Formal, constraintStmts: seq<Statement>)

// At this point, constraints have been entirely removed,
// but synonym types might have different witnesses to use for by the compiler
datatype SynonymType = SynonymType(name: Name, typeParams: seq<TypeArgDecl>, base: Type, witnessStmts: seq<Statement>, witnessExpr: Option<Expression>, attributes: seq<Attribute>)

datatype ClassItem = Method(Method)

Expand All @@ -103,6 +180,8 @@ module {:extern "DAST"} DAST {
datatype Method = Method(
isStatic: bool,
hasBody: bool,
outVarsAreUninitFieldsToAssign: bool, // For constructors
wasFunction: bool, // To choose between "&self" and "&mut self"
overridingPath: Option<seq<Ident>>,
name: Name,
typeParams: seq<TypeArgDecl>,
Expand All @@ -114,7 +193,7 @@ module {:extern "DAST"} DAST {
datatype CallSignature = CallSignature(parameters: seq<Formal>)

datatype CallName =
CallName(name: Name, onType: Option<Type>, signature: CallSignature) |
CallName(name: Name, onType: Option<Type>, receiverArgs: Option<Formal>, signature: CallSignature) |
MapBuilderAdd | MapBuilderBuild | SetBuilderAdd | SetBuilderBuild

datatype Statement =
Expand All @@ -131,7 +210,10 @@ module {:extern "DAST"} DAST {
TailRecursive(body: seq<Statement>) |
JumpTailCallStart() |
Halt() |
Print(Expression)
Print(Expression) |
ConstructorNewSeparator(fields: seq<Formal>)
{
}

datatype AssignLhs =
Ident(ident: Ident) |
Expand All @@ -141,7 +223,7 @@ module {:extern "DAST"} DAST {
datatype CollKind = Seq | Array | Map

datatype BinOp =
Eq(referential: bool, nullable: bool) |
Eq(referential: bool) |
Div() | EuclidianDiv() |
Mod() | EuclidianMod() |
Lt() | // a <= b is !(b < a)
Expand All @@ -162,12 +244,14 @@ module {:extern "DAST"} DAST {

datatype Expression =
Literal(Literal) |
Ident(Name) |
Companion(seq<Ident>) |
Ident(name: Name) |
Companion(seq<Ident>, typeArgs: seq<Type>) |
Tuple(seq<Expression>) |
New(path: seq<Ident>, typeArgs: seq<Type>, args: seq<Expression>) |
NewArray(dims: seq<Expression>, typ: Type) |
DatatypeValue(datatypeType: DatatypeType, typeArgs: seq<Type>, variant: Name, isCo: bool, contents: seq<(string, Expression)>) |
NewUninitArray(dims: seq<Expression>, typ: Type) |
ArrayIndexToInt(value: Expression) |
FinalizeNewArray(value: Expression, typ: Type) |
DatatypeValue(datatypeType: ResolvedType, typeArgs: seq<Type>, variant: Name, isCo: bool, contents: seq<(string, Expression)>) |
Convert(value: Expression, from: Type, typ: Type) |
SeqConstruct(length: Expression, elem: Expression) |
SeqValue(elements: seq<Expression>, typ: Type) |
Expand All @@ -183,7 +267,7 @@ module {:extern "DAST"} DAST {
Ite(cond: Expression, thn: Expression, els: Expression) |
UnOp(unOp: UnaryOp, expr: Expression, format1: Format.UnaryOpFormat) |
BinOp(op: BinOp, left: Expression, right: Expression, format2: Format.BinaryOpFormat) |
ArrayLen(expr: Expression, dim: nat) |
ArrayLen(expr: Expression, exprType: Type, dim: nat, native: bool) |
MapKeys(expr: Expression) |
MapValues(expr: Expression) |
Select(expr: Expression, field: Name, isConstant: bool, onDatatype: bool, fieldType: Type) |
Expand All @@ -194,14 +278,17 @@ module {:extern "DAST"} DAST {
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) |
IIFE(ident: Ident, typ: Type, value: Expression, iifeBody: Expression) |
Apply(expr: Expression, args: seq<Expression>) |
TypeTest(on: Expression, dType: seq<Ident>, variant: Name) |
InitializationValue(typ: Type) |
BoolBoundedPool() |
SetBoundedPool(of: Expression) |
MapBoundedPool(of: Expression) |
SeqBoundedPool(of: Expression, includeDuplicates: bool) |
IntRange(lo: Expression, hi: Expression)
IntRange(lo: Expression, hi: Expression, up: bool) |
UnboundedIntRange(start: Expression, up: bool) |
Quantifier(elemType: Type, collection: Expression, is_forall: bool, lambda: Expression)

datatype UnaryOp = Not | BitwiseNot | Cardinality

Expand Down
Loading

0 comments on commit 2c4dd00

Please sign in to comment.