Chore: Dafny to Rust refactorings

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