chore-rust-refactorings

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

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,69 @@ 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 DatatypeCtor = DatatypeCtor(name: Name, args: seq<Formal>, hasAnyArgs: bool /* includes ghost */)
 
- datatype Newtype = Newtype(name: string, typeParams: seq<Type>, base: Type, range: NewtypeRange, witnessStmts: seq<Statement>, witnessExpr: Option<Expression>)
+ 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 +132,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 +160,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 +184,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) |