More fixups

dafny-lang · Jun 13, 2024 · 0a13114 · 0a13114
1 parent b29ffd0
commit 0a13114
Show file tree

Hide file tree

Showing 4 changed files with 45 additions and 44 deletions.
diff --git a/Makefile b/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

diff --git a/Source/DafnyCore/Backends/Dafny/DafnyCodeGenerator.cs b/Source/DafnyCore/Backends/Dafny/DafnyCodeGenerator.cs
@@ -274,19 +274,19 @@ class DafnyCodeGenerator : SinglePassCodeGenerator {
  Sequence<Rune>.UnicodeFromString(compileName), bounds));
  }
 
- IEnumerable<DAST.DatatypeCtor> ctors = 
+ IEnumerable<DAST.DatatypeCtor> ctors =
  from ctor in dt.Ctors
-  let allDtors =
-  from arg in ctor.Formals
-  where !arg.IsGhost
-  let formalName = Sequence<Rune>.UnicodeFromString(GetDestructorFormalName(arg))
-  let formalType = GenType(arg.Type)
-  let formalCallName = GetExtractOverrideName(arg.Attributes, arg.CompileName)
-  let dtorName =
-  Option<Sequence<Rune>>.create_Some((Sequence<Rune>)Sequence<Rune>.UnicodeFromString(formalCallName))
-  let formalAttributes = ParseAttributes(arg.Attributes)
-  select (DAST.DatatypeDtor)DAST.DatatypeDtor.create_DatatypeDtor((DAST.Formal)DAST.Formal.create_Formal(
-  formalName, formalType, formalAttributes), dtorName)
+ let allDtors =
+ from arg in ctor.Formals
+ where !arg.IsGhost
+ let formalName = Sequence<Rune>.UnicodeFromString(GetDestructorFormalName(arg))
+ let formalType = GenType(arg.Type)
+ let formalCallName = GetExtractOverrideName(arg.Attributes, arg.CompileName)
+ let dtorName =
+ Option<Sequence<Rune>>.create_Some((Sequence<Rune>)Sequence<Rune>.UnicodeFromString(formalCallName))
+ let formalAttributes = ParseAttributes(arg.Attributes)
+ select (DAST.DatatypeDtor)DAST.DatatypeDtor.create_DatatypeDtor((DAST.Formal)DAST.Formal.create_Formal(
+ formalName, formalType, formalAttributes), dtorName)
  let args = Sequence<DAST.DatatypeDtor>.FromArray(allDtors.ToArray<DatatypeDtor>())
  select (DAST.DatatypeCtor)DAST.DatatypeCtor.create_DatatypeCtor(
  Sequence<Rune>.UnicodeFromString(ctor.GetCompileName(Options)),
@@ -1676,8 +1676,7 @@ private class ExprLvalue : ILvalue {
  }
  }
 
- private static string GetDestructorFormalName(Formal formal)
- {
+ private static string GetDestructorFormalName(Formal formal) {
  var defaultName = formal.CompileName;
  object externVal = null;
  bool hasExternVal = Attributes.ContainsMatchingValue(formal.Attributes, "extern",
@@ -2367,6 +2366,8 @@ private static string GetDestructorFormalName(Formal formal)
  Not(BinaryOp(BinOp.create_Eq(false, false), left, right))),
  BinaryExpr.ResolvedOpcode.SeqNeq => C((left, right) =>
  Not(BinaryOp(BinOp.create_Eq(false, false), left, right))),
+ BinaryExpr.ResolvedOpcode.MapNeq => C((left, right) =>
+ Not(BinaryOp(BinOp.create_Eq(false, false), left, right))),
  BinaryExpr.ResolvedOpcode.MultiSetNeq => C((left, right) =>
  Not(BinaryOp(BinOp.create_Eq(false, false), left, right))),
 

diff --git a/Source/DafnyCore/Backends/Rust/Dafny-compiler-rust.dfy b/Source/DafnyCore/Backends/Rust/Dafny-compiler-rust.dfy
@@ -1728,7 +1728,7 @@ module {:extern "DCOMP"} DafnyToRustCompiler {
  }
  var printRhs :=
  R.RawExpr("write!(_formatter, \"" + ctorName + (if ctor.hasAnyArgs then "(\")?" else "\")?"));
- 
+
  var isNumeric := false;
  var ctorMatchInner := "";
  for j := 0 to |ctor.args| {
@@ -1740,7 +1740,7 @@ module {:extern "DCOMP"} DafnyToRustCompiler {
  if isNumeric {
  patternName := dtor.callName.GetOr("v" + Strings.OfNat(j));
  }
- 
+
  ctorMatchInner := ctorMatchInner + patternName + ", ";
 
  if (j > 0) {

diff --git a/Source/DafnyCore/GeneratedFromDafny/DCOMP.cs b/Source/DafnyCore/GeneratedFromDafny/DCOMP.cs
@@ -2301,7 +2301,7 @@ public void GenStmt(DAST._IStatement stmt, Std.Wrappers._IOption<Dafny.ISequence
  RAST._IExpr _out163;
  DCOMP._IOwnership _out164;
  Dafny.ISet<Dafny.ISequence<Dafny.Rune>> _out165;
- (this).GenExpr(_1431_e, selfIdent, env, DCOMP.Ownership.create_OwnershipBorrowed(), out _out163, out _out164, out _out165);
+ (this).GenExpr(_1431_e, selfIdent, env, DCOMP.Ownership.create_OwnershipOwned(), out _out163, out _out164, out _out165);
  _1432_printedExpr = _out163;
  _1433_recOwnership = _out164;
  _1434_recIdents = _out165;
@@ -3843,7 +3843,7 @@ public void GenExpr(DAST._IExpression e, Std.Wrappers._IOption<Dafny.ISequence<D
  }
  r = (r).ApplyType(_1598_typeExprs);
  }
- r = (r).MSel(Dafny.Sequence<Dafny.Rune>.UnicodeFromString("_allocated"));
+ r = (r).MSel(Dafny.Sequence<Dafny.Rune>.UnicodeFromString("new"));
  readIdents = Dafny.Set<Dafny.ISequence<Dafny.Rune>>.FromElements();
  Dafny.ISequence<RAST._IExpr> _1601_arguments;
  _1601_arguments = Dafny.Sequence<RAST._IExpr>.FromElements();