Feat: Rust operators and immutable collections

.pre-commit-config.yaml

@@ -1,8 +1,8 @@
 repos:
 - repo: local
- hooks:
- - id: dotnet-format
- name: dotnet-format
- language: system
- entry: dotnet format whitespace Source/Dafny.sln --include
- types_or: ["c#"]
+# hooks:
+# - id: dotnet-format
+# name: dotnet-format
+# language: system
+# entry: dotnet format whitespace Source/Dafny.sln -v:d --exclude Source/DafnyCore/GeneratedFromDafny.cs --include 
+# types_or: ["c#"]

Makefile

@@ -17,7 +17,7 @@ dfyprod: dfyprodformat dfyprodinit
  (cd "${DIR}" ; dotnet build Source/Dafny.sln ) ## includes parser
 
 dfydevinit:
- (cd "${DIR}"/Source/DafnyCore ; bash DafnyGeneratedFromDafny.sh --no-verify --no-format)
+ (cd "${DIR}"/Source/DafnyCore ; bash DafnyGeneratedFromDafny.sh --no-verify)
 
 dfydev: dfydevinit
  (cd "${DIR}" ; dotnet build Source/Dafny.sln ) ## includes parser

Source/DafnyCore/AST/Expressions/Variables/IVariable.cs

@@ -24,6 +24,9 @@ string UniqueName {
  string SanitizedName {
  get;
  }
+ string SanitizedNameShadowable {
+ get;
+ }
  string CompileName {
  get;
  }

Source/DafnyCore/AST/Expressions/Variables/IVariableContracts.cs

@@ -41,6 +41,13 @@ public string SanitizedName {
  throw new NotImplementedException(); // this getter implementation is here only so that the Ensures contract can be given here
  }
  }
+
+ public string SanitizedNameShadowable {
+ get {
+ Contract.Ensures(Contract.Result<string>() != null);
+ throw new NotImplementedException(); // this getter implementation is here only so that the Ensures contract can be given here
+ }
+ }
  public string CompileName {
  get {
  Contract.Ensures(Contract.Result<string>() != null);

Source/DafnyCore/AST/Expressions/Variables/NonglobalVariable.cs

@@ -74,9 +74,14 @@ public static string SanitizeName(string nm) {
  }
  }
 
+ private string sanitizedNameShadowable;
+
+ public virtual string SanitizedNameShadowable =>
+ sanitizedNameShadowable ??= SanitizeName(Name);
+
  private string sanitizedName;
  public virtual string SanitizedName =>
- sanitizedName ??= $"_{IVariable.CompileNameIdGenerator.FreshNumericId()}_{SanitizeName(Name)}";
+ sanitizedName ??= $"_{IVariable.CompileNameIdGenerator.FreshNumericId()}_{SanitizedNameShadowable}";
 
  protected string compileName;
  public virtual string CompileName =>

Source/DafnyCore/AST/Statements/Assignment/LocalVariable.cs

@@ -68,9 +68,15 @@ public string AssignUniqueName(FreshIdGenerator generator) {
  return uniqueName ??= generator.FreshId(Name + "#");
  }
 
+ private string sanitizedNameShadowable;
+
+ public string SanitizedNameShadowable =>
+ sanitizedNameShadowable ??= NonglobalVariable.SanitizeName(Name);
+
  private string sanitizedName;
+
  public string SanitizedName =>
- sanitizedName ??= $"_{IVariable.CompileNameIdGenerator.FreshNumericId()}_{NonglobalVariable.SanitizeName(Name)}";
+ sanitizedName ??= $"_{IVariable.CompileNameIdGenerator.FreshNumericId()}_{SanitizedNameShadowable}";
 
  string compileName;
  public string CompileName =>

Source/DafnyCore/AST/TypeDeclarations/NewtypeDecl.cs

@@ -158,7 +158,7 @@ public class NativeType {
  public readonly BigInteger LowerBound;
  public readonly BigInteger UpperBound;
  public readonly int Bitwidth; // for unassigned types, this shows the number of bits in the type; else is 0
- public enum Selection { Byte, SByte, UShort, Short, UInt, Int, Number, ULong, Long }
+ public enum Selection { Byte, SByte, UShort, Short, UInt, Int, Number, ULong, Long, UDoubleLong, DoubleLong }
  public readonly Selection Sel;
  public NativeType(string Name, BigInteger LowerBound, BigInteger UpperBound, int bitwidth, Selection sel) {
  Contract.Requires(Name != null);

Source/DafnyCore/Compilers/CSharp/Compiler-Csharp.cs

@@ -3387,15 +3387,16 @@ protected override ConcreteSyntaxTree EmitMapBuilder_Add(MapType mt, IToken tok,
  return termLeftWriter;
  }
 
- protected override string GetCollectionBuilder_Build(CollectionType ct, IToken tok, string collName, ConcreteSyntaxTree wr) {
+ protected override void GetCollectionBuilder_Build(CollectionType ct, IToken tok, string collName,
+ ConcreteSyntaxTree wr, ConcreteSyntaxTree wStmt) {
  if (ct is SetType) {
  var typeName = TypeName(ct.Arg, wr, tok);
- return string.Format($"{DafnySetClass}<{typeName}>.FromCollection({collName})");
+ wr.Write(string.Format($"{DafnySetClass}<{typeName}>.FromCollection({collName})"));
  } else if (ct is MapType) {
  var mt = (MapType)ct;
  var domtypeName = TypeName(mt.Domain, wr, tok);
  var rantypeName = TypeName(mt.Range, wr, tok);
- return $"{DafnyMapClass}<{domtypeName},{rantypeName}>.FromCollection({collName})";
+ wr.Write($"{DafnyMapClass}<{domtypeName},{rantypeName}>.FromCollection({collName})");
  } else {
  Contract.Assume(false); // unexpected collection type
  throw new cce.UnreachableException(); // please compiler

Source/DafnyCore/Compilers/Cplusplus/Compiler-cpp.cs

@@ -2444,9 +2444,10 @@ protected override ConcreteSyntaxTree EmitMapBuilder_Add(MapType mt, IToken tok,
  throw new UnsupportedFeatureException(tok, Feature.MapComprehensions);
  }
 
- protected override string GetCollectionBuilder_Build(CollectionType ct, IToken tok, string collName, ConcreteSyntaxTree wr) {
+ protected override void GetCollectionBuilder_Build(CollectionType ct, IToken tok, string collName,
+ ConcreteSyntaxTree wr, ConcreteSyntaxTree wStmt) {
  // collections are built in place
- return collName;
+ wr.Write(collName);
  }
 
  protected override void EmitSingleValueGenerator(Expression e, bool inLetExprBody, string type,

Source/DafnyCore/Compilers/Dafny/AST.dfy

@@ -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 UnOpFormat =
+ NoFormat()
+ | CombineNotInner()
+ datatype BinOpFormat = 
+ NoFormat()
+ | ImpliesFormat()
+ | Equivalence()
+ | ReverseOperands()
+}
+
 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 =
+ | U8 | I8 | U16 | I16 | U32 | I32 | U64 | I64 | U128 | I128 | BigInt
+ | NoRange
+
+ 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.UnOpFormat) |
+ BinOp(op: BinOp, left: Expression, right: Expression, format2: Format.BinOpFormat) |
  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) |