Chore: Dafny to Rust refactorings (#5513)

- extern module as attribute
- Type arguments with type bounds
- Attributes handling
- Type on Select field and TupleSelect
- Name refactoring to ensure we distinguish Dafny names from Rust names
- Binary In operator
- `NoStatementBuffer` to convert
- `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` split into `Apply` for expressions and `ApplyType` for type
arguments
- Conversion from `Type` to `TypeParamDecl` so that we can support
bounds
- Changed `Formals` to `Fields`, and `NamelessFormals` to
`NamelessFields`
- `Visibility` has its own datatype
- Renamed `Self` to `SelfBorrowed`
- Renamed `SeltMut` to `SelfBorrowedMut`
- `Box`/`BoxNew` (for attribute annotations)
- Support for native `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` to be able to simulate macros like expressions
- `Lambda` (makes code prettier)
- Error handling
- `Debug` trait for datatypes
- No more system object, just `std::any::Any`
- New char encoding
- `int!` macro
- Refactoring of DafatypeValue's first argument
- `constant`
- `GenIdent` refactoring

### How has this been tested?
Existing tests should just pass.

<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>

Makefile

@@ -5,7 +5,7 @@ default: exe
 all: exe refman
 
 exe:
-	(cd ${DIR} ; dotnet build Source/Dafny.sln ) ## includes parser
+	(cd "${DIR}" ; dotnet build Source/Dafny.sln ) ## includes parser
 
 format-dfy:
 	(cd "${DIR}"/Source/DafnyCore ; ../../Binaries/Dafny.exe format .)
@@ -14,7 +14,7 @@ dfy-to-cs:
 	(cd "${DIR}"/Source/DafnyCore ; bash DafnyGeneratedFromDafny.sh)
 
 dfy-to-cs-exe: dfy-to-cs
-	(cd ${DIR} ; dotnet build Source/Dafny.sln )
+	(cd "${DIR}" ; dotnet build Source/Dafny.sln )
 
 dfy-to-cs-noverify:
 	(cd "${DIR}"/Source/DafnyCore ; bash DafnyGeneratedFromDafny.sh --no-verify)
@@ -24,74 +24,74 @@ dfy-to-cs-noverify-exe: dfy-to-cs-noverify exe
 boogie: ${DIR}/boogie/Binaries/Boogie.exe
 
 tests:
-	(cd ${DIR}; dotnet test Source/IntegrationTests)
+	(cd "${DIR}"; dotnet test Source/IntegrationTests)
 
 tests-verbose:
-	(cd ${DIR}; dotnet test --logger "console;verbosity=normal" Source/IntegrationTests )
+	(cd "${DIR}"; dotnet test --logger "console;verbosity=normal" Source/IntegrationTests )
 
 ${DIR}/boogie/Binaries/Boogie.exe:
-	(cd ${DIR}/boogie ; dotnet build -c Release Source/Boogie.sln )
+	(cd "${DIR}"/boogie ; dotnet build -c Release Source/Boogie.sln )
 
 refman: exe
-	make -C ${DIR}/docs/DafnyRef
+	make -C "${DIR}"/docs/DafnyRef
 
 refman-release: exe
-	make -C ${DIR}/docs/DafnyRef release
+	make -C "${DIR}"/docs/DafnyRef release
 
 z3-mac:
-	mkdir -p ${DIR}/Binaries/z3/bin
+	mkdir -p "${DIR}"/Binaries/z3/bin
 	wget https://github.com/dafny-lang/solver-builds/releases/download/snapshot-2023-08-02/z3-4.12.1-x64-macos-11-bin.zip
 	unzip z3-4.12.1-x64-macos-11-bin.zip
 	rm z3-4.12.1-x64-macos-11-bin.zip
 	wget https://github.com/dafny-lang/solver-builds/releases/download/snapshot-2023-08-02/z3-4.8.5-x64-macos-11-bin.zip
 	unzip z3-4.8.5-x64-macos-11-bin.zip
 	rm z3-4.8.5-x64-macos-11-bin.zip
-	mv z3-* ${DIR}/Binaries/z3/bin/
-	chmod +x ${DIR}/Binaries/z3/bin/z3-*
+	mv z3-* "${DIR}"/Binaries/z3/bin/
+	chmod +x "${DIR}"/Binaries/z3/bin/z3-*
 
 z3-mac-arm:
-	mkdir -p ${DIR}/Binaries/z3/bin
+	mkdir -p "${DIR}"/Binaries/z3/bin
 	wget https://github.com/dafny-lang/solver-builds/releases/download/snapshot-2023-08-02/z3-4.12.1-arm64-macos-11-bin.zip
 	unzip z3-4.12.1-arm64-macos-11-bin.zip
 	rm z3-4.12.1-arm64-macos-11-bin.zip
 	wget https://github.com/dafny-lang/solver-builds/releases/download/snapshot-2023-08-02/z3-4.8.5-x64-macos-11-bin.zip
 	unzip z3-4.8.5-x64-macos-11-bin.zip
 	rm z3-4.8.5-x64-macos-11-bin.zip
-	mv z3-* ${DIR}/Binaries/z3/bin/
-	chmod +x ${DIR}/Binaries/z3/bin/z3-*
+	mv z3-* "${DIR}"/Binaries/z3/bin/
+	chmod +x "${DIR}"/Binaries/z3/bin/z3-*
 
 z3-ubuntu:
-	mkdir -p ${DIR}/Binaries/z3/bin
+	mkdir -p "${DIR}"/Binaries/z3/bin
 	wget https://github.com/dafny-lang/solver-builds/releases/download/snapshot-2023-08-02/z3-4.12.1-x64-ubuntu-20.04-bin.zip
 	unzip z3-4.12.1-x64-ubuntu-20.04-bin.zip
 	rm z3-4.12.1-x64-ubuntu-20.04-bin.zip
 	wget https://github.com/dafny-lang/solver-builds/releases/download/snapshot-2023-08-02/z3-4.8.5-x64-ubuntu-20.04-bin.zip
 	unzip z3-4.8.5-x64-ubuntu-20.04-bin.zip
 	rm z3-4.8.5-x64-ubuntu-20.04-bin.zip
-	mv z3-* ${DIR}/Binaries/z3/bin/
-	chmod +x ${DIR}/Binaries/z3/bin/z3-*
+	mv z3-* "${DIR}"/Binaries/z3/bin/
+	chmod +x "${DIR}"/Binaries/z3/bin/z3-*
 
 format:
 	dotnet format whitespace Source/Dafny.sln --exclude Source/DafnyCore/Scanner.cs --exclude Source/DafnyCore/Parser.cs --exclude boogie --exclude Source/DafnyCore/GeneratedFromDafny/* --exclude Source/DafnyCore.Test/GeneratedFromDafny/* --exclude Source/DafnyRuntime/DafnyRuntimeSystemModule.cs
 
 clean:
-	(cd ${DIR}; cd Source; rm -rf Dafny/bin Dafny/obj DafnyDriver/bin DafnyDriver/obj DafnyRuntime/obj DafnyRuntime/bin DafnyServer/bin DafnyServer/obj DafnyPipeline/obj DafnyPipeline/bin DafnyCore/obj DafnyCore/bin)
-	(cd ${DIR} ; dotnet build Source/Dafny.sln -v:q --nologo -target:clean )
-	make -C ${DIR}/Source/DafnyCore -f Makefile clean
-	(cd ${DIR}/Source/Dafny && rm -rf Scanner.cs Parser.cs obj )
-	(cd ${DIR}/Source/DafnyRuntime/DafnyRuntimeJava; ./gradlew clean)
-	make -C ${DIR}/docs/DafnyRef clean
-	(cd ${DIR}; cd Source; rm -rf Dafny/bin Dafny/obj DafnyDriver/bin DafnyDriver/obj DafnyRuntime/obj DafnyRuntime/bin DafnyServer/bin DafnyServer/obj DafnyPipeline/obj DafnyPipeline/bin DafnyCore/obj DafnyCore/bin)
+	(cd "${DIR}"; cd Source; rm -rf Dafny/bin Dafny/obj DafnyDriver/bin DafnyDriver/obj DafnyRuntime/obj DafnyRuntime/bin DafnyServer/bin DafnyServer/obj DafnyPipeline/obj DafnyPipeline/bin DafnyCore/obj DafnyCore/bin)
+	(cd "${DIR}" ; dotnet build Source/Dafny.sln -v:q --nologo -target:clean )
+	make -C "${DIR}"/Source/DafnyCore -f Makefile clean
+	(cd "${DIR}"/Source/Dafny && rm -rf Scanner.cs Parser.cs obj )
+	(cd "${DIR}"/Source/DafnyRuntime/DafnyRuntimeJava; ./gradlew clean)
+	make -C "${DIR}"/docs/DafnyRef clean
+	(cd "${DIR}"; cd Source; rm -rf Dafny/bin Dafny/obj DafnyDriver/bin DafnyDriver/obj DafnyRuntime/obj DafnyRuntime/bin DafnyServer/bin DafnyServer/obj DafnyPipeline/obj DafnyPipeline/bin DafnyCore/obj DafnyCore/bin)
 	echo Source/*/bin Source/*/obj
 
 update-cs-module:
-	(cd ${DIR}; cd Source/DafnyRuntime; make update-system-module)
+	(cd "${DIR}"; cd Source/DafnyRuntime; make update-system-module)
 
 update-go-module:
-	(cd ${DIR}; cd Source/DafnyRuntime/DafnyRuntimeGo; make update-system-module)
+	(cd "${DIR}"; cd Source/DafnyRuntime/DafnyRuntimeGo; make update-system-module)
 
 update-runtime-dafny:
-	(cd ${DIR}; cd Source/DafnyRuntime/DafnyRuntimeDafny; make update-go)
+	(cd "${DIR}"; cd Source/DafnyRuntime/DafnyRuntimeDafny; make update-go)
 
 # `make pr` will bring you in a state suitable for submitting a PR
 # - Builds the Dafny executable

Source/DafnyCore/Backends/Dafny/AST.dfy

@@ -15,12 +15,27 @@ module {:extern "DAST.Format"} DAST.Format
     | ImpliesFormat
     | EquivalenceFormat
     | ReverseFormat
+
+  function SeqToHeight<T>(s: seq<T>, f: T --> nat): (r: nat)
+    requires forall t <- s :: f.requires(t)
+    ensures forall t <- s :: f(t) <= r
+  {
+    if |s| == 0 then 0 else
+    var i := f(s[0]);
+    var j := SeqToHeight(s[1..], f);
+    if i < j then j else i
+  }
 }
 
 module {:extern "DAST"} DAST {
   import opened Std.Wrappers
 
-  datatype Module = Module(name: string, isExtern: bool, body: seq<ModuleItem>)
+  // Prevents Dafny names to being direclty integrated into Rust without explicit conversion
+  // Make it a newtype once newtypes are compatible with standard library
+  // See issue https://github.com/dafny-lang/dafny/issues/5345
+  datatype Name = Name(dafny_name: string)
+
+  datatype Module = Module(name: Name, attributes: seq<Attribute>, body: Option<seq<ModuleItem>>)
 
   datatype ModuleItem =
     | Module(Module)
@@ -44,48 +59,71 @@ module {:extern "DAST"} DAST {
     Primitive(Primitive) | Passthrough(string) |
     TypeArg(Ident)
 
+  datatype TypeArgDecl = TypeArgDecl(name: Ident, bounds: seq<TypeArgBound>)
+
+  datatype TypeArgBound =
+    | SupportsEquality
+    | SupportsDefault
+
   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>)
+
   datatype ResolvedType =
-    | Datatype(path: seq<Ident>)
-    | Trait(path: seq<Ident>)
-    | Newtype(baseType: Type, range: NewtypeRange, erase: bool)
+    | Datatype(datatypeType: DatatypeType)
+    | Trait(path: seq<Ident>, attributes: seq<Attribute>)
+    | Newtype(baseType: Type, range: NewtypeRange, erase: bool, attributes: seq<Attribute>)
 
-  datatype Ident = Ident(id: string)
+  datatype Ident = Ident(id: Name)
 
-  datatype Class = Class(name: string, enclosingModule: Ident, typeParams: seq<Type>, superClasses: seq<Type>, fields: seq<Field>, body: seq<ClassItem>)
+  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: string, typeParams: seq<Type>, body: seq<ClassItem>)
+  datatype Trait = Trait(name: Name, typeParams: seq<TypeArgDecl>, body: seq<ClassItem>, attributes: seq<Attribute>)
 
-  datatype Datatype = Datatype(name: string, enclosingModule: Ident, typeParams: seq<Type>, ctors: seq<DatatypeCtor>, body: seq<ClassItem>, isCo: bool)
+  datatype Datatype = Datatype(name: Name, enclosingModule: Ident, typeParams: seq<TypeArgDecl>, ctors: seq<DatatypeCtor>, body: seq<ClassItem>, isCo: bool, attributes: seq<Attribute>)
 
-  datatype DatatypeCtor = DatatypeCtor(name: string, args: seq<Formal>, hasAnyArgs: bool /* includes ghost */)
+  datatype DatatypeDtor = DatatypeDtor(formal: Formal, callName: Option<string>)
 
-  datatype Newtype = Newtype(name: string, typeParams: seq<Type>, base: Type, range: NewtypeRange, witnessStmts: seq<Statement>, witnessExpr: Option<Expression>)
+  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 ClassItem = Method(Method)
 
   datatype Field = Field(formal: Formal, defaultValue: Option<Expression>)
 
-  datatype Formal = Formal(name: string, typ: Type)
+  datatype Formal = Formal(name: Name, typ: Type, attributes: seq<Attribute>)
+
+  datatype Method = Method(
+    isStatic: bool,
+    hasBody: bool,
+    overridingPath: Option<seq<Ident>>,
+    name: Name,
+    typeParams: seq<TypeArgDecl>,
+    params: seq<Formal>,
+    body: seq<Statement>,
+    outTypes: seq<Type>,
+    outVars: Option<seq<Ident>>)
 
-  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 CallSignature = CallSignature(parameters: seq<Formal>)
 
   datatype CallName =
-    Name(name: string) |
+    CallName(name: Name, onType: Option<Type>, signature: CallSignature) |
     MapBuilderAdd | MapBuilderBuild | SetBuilderAdd | SetBuilderBuild
 
   datatype Statement =
-    DeclareVar(name: string, typ: Type, maybeValue: Option<Expression>) |
+    DeclareVar(name: Name, 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>) |
+    Foreach(boundName: Name, boundType: Type, over: Expression, body: seq<Statement>) |
     Call(on: Expression, callName: CallName, typeArgs: seq<Type>, args: seq<Expression>, outs: Option<seq<Ident>>) |
     Return(expr: Expression) |
     EarlyReturn() |
@@ -96,8 +134,8 @@ module {:extern "DAST"} DAST {
     Print(Expression)
 
   datatype AssignLhs =
-    Ident(Ident) |
-    Select(expr: Expression, field: string) |
+    Ident(ident: Ident) |
+    Select(expr: Expression, field: Name) |
     Index(expr: Expression, indices: seq<Expression>)
 
   datatype CollKind = Seq | Array | Map
@@ -124,12 +162,12 @@ module {:extern "DAST"} DAST {
 
   datatype Expression =
     Literal(Literal) |
-    Ident(string) |
+    Ident(Name) |
     Companion(seq<Ident>) |
     Tuple(seq<Expression>) |
     New(path: seq<Ident>, typeArgs: seq<Type>, args: seq<Expression>) |
     NewArray(dims: seq<Expression>, typ: Type) |
-    DatatypeValue(path: seq<Ident>, typeArgs: seq<Type>, variant: string, isCo: bool, contents: seq<(string, Expression)>) |
+    DatatypeValue(datatypeType: DatatypeType, 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) |
@@ -148,17 +186,17 @@ module {:extern "DAST"} DAST {
     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) |
+    Select(expr: Expression, field: Name, isConstant: bool, onDatatype: bool, fieldType: Type) |
+    SelectFn(expr: Expression, field: Name, 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) |
+    TupleSelect(expr: Expression, index: nat, fieldType: Type) |
     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) |
     Apply(expr: Expression, args: seq<Expression>) |
-    TypeTest(on: Expression, dType: seq<Ident>, variant: string) |
+    TypeTest(on: Expression, dType: seq<Ident>, variant: Name) |
     InitializationValue(typ: Type) |
     BoolBoundedPool() |
     SetBoundedPool(of: Expression) |
@@ -167,5 +205,12 @@ module {:extern "DAST"} DAST {
 
   datatype UnaryOp = Not | BitwiseNot | Cardinality
 
-  datatype Literal = BoolLiteral(bool) | IntLiteral(string, Type) | DecLiteral(string, string, Type) | StringLiteral(string) | CharLiteral(char) | Null(Type)
+  datatype Literal =
+    | BoolLiteral(bool)
+    | IntLiteral(string, Type)
+    | DecLiteral(string, string, Type)
+    | StringLiteral(string, verbatim: bool)
+    | CharLiteral(char)
+    | CharLiteralUTF16(nat)
+    | Null(Type)
 }