Revert "Feat: Rust operators and immutable collections (#5081)" (#5377)

This reverts commit 3e38580 to fix
failing nightly:
https://github.com/dafny-lang/dafny/actions/runs/8868313153

---------

Co-authored-by: Fabio Madge <[email protected]>

.github/workflows/msbuild.yml

@@ -37,7 +37,7 @@ jobs:
  run: dotnet tool restore
  - name: Check whitespace and style
  working-directory: dafny
- run: dotnet format whitespace Source/Dafny.sln --verify-no-changes --exclude Source/DafnyCore/Scanner.cs --exclude Source/DafnyCore/Parser.cs --exclude Source/DafnyCore/GeneratedFromDafny/* --exclude Source/DafnyCore.Test/GeneratedFromDafny/* --exclude Source/DafnyRuntime/DafnyRuntimeSystemModule.cs
+ run: dotnet format whitespace Source/Dafny.sln --verify-no-changes --exclude Source/DafnyCore/Scanner.cs --exclude Source/DafnyCore/Parser.cs --exclude Source/DafnyCore/GeneratedFromDafny.cs --exclude Source/DafnyRuntime/DafnyRuntimeSystemModule.cs
  - name: Get Boogie Version
  run: |
  sudo apt-get update

.pre-commit-config.yaml

@@ -4,5 +4,5 @@ repos:
  - id: dotnet-format
  name: dotnet-format
  language: system
- entry: dotnet format whitespace Source/Dafny.sln -v:d --include 
+ entry: dotnet format whitespace Source/Dafny.sln --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)
+ (cd "${DIR}"/Source/DafnyCore ; bash DafnyGeneratedFromDafny.sh --no-verify --no-format)
 
 dfydev: dfydevinit
  (cd "${DIR}" ; dotnet build Source/Dafny.sln ) ## includes parser
@@ -73,7 +73,7 @@ z3-ubuntu:
  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
+ dotnet format whitespace Source/Dafny.sln --exclude Source/DafnyCore/Scanner.cs --exclude Source/DafnyCore/Parser.cs --exclude boogie --exclude Source/DafnyCore/GeneratedFromDafny.cs --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)

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

@@ -24,10 +24,6 @@ public interface IVariable : ISymbol {
  string SanitizedName {
  get;
  }
- string SanitizedNameShadowable { // A name suitable for compilation, but without the unique identifier.
- // Useful to generate readable identifiers in the generated source code.
- get;
- }
  string CompileName {
  get;
  }

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

@@ -41,13 +41,6 @@ public abstract class IVariableContracts : TokenNode, IVariable {
  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,14 +74,9 @@ public abstract class NonglobalVariable : TokenNode, IVariable {
  }
  }
 
- private string sanitizedNameShadowable;
-
- public virtual string SanitizedNameShadowable =>
- sanitizedNameShadowable ??= SanitizeName(Name);
-
  private string sanitizedName;
  public virtual string SanitizedName =>
- sanitizedName ??= $"_{IVariable.CompileNameIdGenerator.FreshNumericId()}_{SanitizedNameShadowable}";
+ sanitizedName ??= $"_{IVariable.CompileNameIdGenerator.FreshNumericId()}_{SanitizeName(Name)}";
 
  protected string compileName;
  public virtual string CompileName =>

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

@@ -68,15 +68,9 @@ public LocalVariable(RangeToken rangeToken, string name, Type type, bool isGhost
  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()}_{SanitizedNameShadowable}";
+ sanitizedName ??= $"_{IVariable.CompileNameIdGenerator.FreshNumericId()}_{NonglobalVariable.SanitizeName(Name)}";
 
  string compileName;
  public string CompileName =>

Source/DafnyCore/AST/TypeDeclarations/NewtypeDecl.cs

@@ -174,7 +174,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, UDoubleLong, DoubleLong }
+ public enum Selection { Byte, SByte, UShort, Short, UInt, Int, Number, ULong, Long }
  public readonly Selection Sel;
  public NativeType(string Name, BigInteger LowerBound, BigInteger UpperBound, int bitwidth, Selection sel) {
  Contract.Requires(Name != null);

Source/DafnyCore/Backends/CSharp/CsharpCodeGenerator.cs

@@ -3422,16 +3422,15 @@ protected class ClassWriter : IClassWriter {
  return termLeftWriter;
  }
 
- protected override void GetCollectionBuilder_Build(CollectionType ct, IToken tok, string collName,
- ConcreteSyntaxTree wr, ConcreteSyntaxTree wStmt) {
+ protected override string GetCollectionBuilder_Build(CollectionType ct, IToken tok, string collName, ConcreteSyntaxTree wr) {
  if (ct is SetType) {
  var typeName = TypeName(ct.Arg, wr, tok);
- wr.Write(string.Format($"{DafnySetClass}<{typeName}>.FromCollection({collName})"));
+ return 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);
- wr.Write($"{DafnyMapClass}<{domtypeName},{rantypeName}>.FromCollection({collName})");
+ return $"{DafnyMapClass}<{domtypeName},{rantypeName}>.FromCollection({collName})";
  } else {
  Contract.Assume(false); // unexpected collection type
  throw new cce.UnreachableException(); // please compiler

Source/DafnyCore/Backends/Cplusplus/CppCodeGenerator.cs

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

Source/DafnyCore/Backends/Dafny/AST.dfy

@@ -1,22 +1,3 @@
-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 UnaryOpFormat =
- | NoFormat
- | CombineFormat
- datatype BinaryOpFormat =
- | NoFormat
- | ImpliesFormat
- | EquivalenceFormat
- | ReverseFormat
-}
-
 module {:extern "DAST"} DAST {
  import opened Std.Wrappers
 
@@ -38,22 +19,13 @@ 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 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 ResolvedType = Datatype(path: seq<Ident>) | Trait(path: seq<Ident>) | Newtype(Type)
 
  datatype Ident = Ident(id: string)
 
@@ -65,7 +37,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, range: NewtypeRange, witnessStmts: seq<Statement>, witnessExpr: Option<Expression>)
+ datatype Newtype = Newtype(name: string, typeParams: seq<Type>, base: Type, witnessStmts: seq<Statement>, witnessExpr: Option<Expression>)
 
  datatype ClassItem = Method(Method)
 
@@ -75,18 +47,14 @@ 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, callName: CallName, typeArgs: seq<Type>, args: seq<Expression>, outs: Option<seq<Ident>>) |
+ Call(on: Expression, name: string, typeArgs: seq<Type>, args: seq<Expression>, outs: Option<seq<Ident>>) |
  Return(expr: Expression) |
  EarlyReturn() |
  Break(toLabel: Option<string>) |
@@ -104,21 +72,13 @@ module {:extern "DAST"} DAST {
 
  datatype BinOp =
  Eq(referential: bool, nullable: bool) |
+ Neq(referential: bool, nullable: bool) |
  Div() | EuclidianDiv() |
  Mod() | EuclidianMod() |
- Lt() | // a <= b is !(b < a)
- LtChar() |
- Plus() | Minus() | Times() |
- BitwiseAnd() | BitwiseOr() | BitwiseXor() |
- BitwiseShiftRight() | BitwiseShiftLeft() |
- And() | Or() |
+ Implies() | // TODO: REplace by Not Or
  In() |
- SeqProperPrefix() | SeqPrefix() |
- SetMerge() | SetSubtraction() | SetIntersection() |
- Subset() | ProperSubset() | SetDisjoint() |
- MapMerge() | MapSubtraction() |
- MultisetMerge() | MultisetSubtraction() | MultisetIntersection() |
- Submultiset() | ProperSubmultiset() | MultisetDisjoint() |
+ NotIn() | // TODO: Replace by Not In
+ SetDifference() |
  Concat() |
  Passthrough(string)
 
@@ -134,26 +94,18 @@ 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, format1: Format.UnaryOpFormat) |
- BinOp(op: BinOp, left: Expression, right: Expression, format2: Format.BinaryOpFormat) |
+ UnOp(unOp: UnaryOp, expr: Expression) |
+ BinOp(op: BinOp, left: Expression, right: Expression) |
  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, callName: CallName, typeArgs: seq<Type>, args: seq<Expression>) |
+ Call(on: Expression, name: Ident, 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) |