Add BoundedInts to DafnyStdLibs

Source/DafnyCore/AST/Members/ICodeContext.cs

@@ -49,7 +49,7 @@ public static ICodeContext Unwrap(ICodeContext codeContext) {
 /// <summary>
 /// An ICallable is a Function, Method, IteratorDecl, or (less fitting for the name ICallable) RedirectingTypeDecl or DatatypeDecl.
 /// </summary>
-public interface ICallable : ICodeContext, INode {
+public interface ICallable : ICodeContext, ISymbol {
  string WhatKind { get; }
  string NameRelativeToModule { get; }
  Specification<Expression> Decreases { get; }
@@ -74,24 +74,29 @@ public CallableWrapper(ICallable callable, bool isGhostContext)
  : base(callable, isGhostContext) {
  }
 
- protected ICallable cwInner => (ICallable)inner;
- public IToken Tok => cwInner.Tok;
- public IEnumerable<INode> Children => cwInner.Children;
- public IEnumerable<INode> PreResolveChildren => cwInner.PreResolveChildren;
+ public ICallable CwInner => (ICallable)inner;
+ public IToken Tok => CwInner.Tok;
+ public IEnumerable<INode> Children => CwInner.Children;
+ public IEnumerable<INode> PreResolveChildren => CwInner.PreResolveChildren;
 
- public string WhatKind => cwInner.WhatKind;
- public string NameRelativeToModule => cwInner.NameRelativeToModule;
- public Specification<Expression> Decreases => cwInner.Decreases;
+ public string WhatKind => CwInner.WhatKind;
+ public string NameRelativeToModule => CwInner.NameRelativeToModule;
+ public Specification<Expression> Decreases => CwInner.Decreases;
 
  public bool InferredDecreases {
- get => cwInner.InferredDecreases;
- set { cwInner.InferredDecreases = value; }
+ get => CwInner.InferredDecreases;
+ set { CwInner.InferredDecreases = value; }
  }
 
- public bool AllowsAllocation => cwInner.AllowsAllocation;
+ public bool AllowsAllocation => CwInner.AllowsAllocation;
 
- public IEnumerable<IToken> OwnedTokens => cwInner.OwnedTokens;
- public RangeToken RangeToken => cwInner.RangeToken;
+ public IEnumerable<IToken> OwnedTokens => CwInner.OwnedTokens;
+ public RangeToken RangeToken => CwInner.RangeToken;
+ public IToken NameToken => CwInner.NameToken;
+ public DafnySymbolKind Kind => CwInner.Kind;
+ public string GetDescription(DafnyOptions options) {
+ return CwInner.GetDescription(options);
+ }
 }
 
 
@@ -121,6 +126,11 @@ public IEnumerable<INode> GetConcreteChildren() {
 
  public IEnumerable<IToken> OwnedTokens => throw new cce.UnreachableException();
  public RangeToken RangeToken => throw new cce.UnreachableException();
+ public IToken NameToken => throw new cce.UnreachableException();
+ public DafnySymbolKind Kind => throw new cce.UnreachableException();
+ public string GetDescription(DafnyOptions options) {
+ throw new cce.UnreachableException();
+ }
 }
 
 /// <summary>

Source/DafnyCore/AST/TypeDeclarations/NonNullTypeDecl.cs

@@ -3,8 +3,8 @@
 
 namespace Microsoft.Dafny;
 
-public class NonNullTypeDecl : SubsetTypeDecl, ISymbol {
- public override string WhatKind { get { return "non-null type"; } }
+public class NonNullTypeDecl : SubsetTypeDecl {
+ public override string WhatKind => "non-null type";
  public readonly ClassLikeDecl Class;
 
  /// <summary>

Source/DafnyCore/AST/TypeDeclarations/SubsetTypeDecl.cs

@@ -46,8 +46,8 @@ public override List<Type> ParentTypes(List<Type> typeArgs) {
  }
  public bool ShouldVerify => true; // This could be made more accurate
  public ModuleDefinition ContainingModule => EnclosingModuleDefinition;
- public virtual DafnySymbolKind Kind => DafnySymbolKind.Class;
- public virtual string GetDescription(DafnyOptions options) {
+ public override DafnySymbolKind Kind => DafnySymbolKind.Class;
+ public override string GetDescription(DafnyOptions options) {
  return "subset type";
  }
 

Source/DafnyCore/AST/TypeDeclarations/TypeSynonymDecl.cs

@@ -3,18 +3,28 @@
 namespace Microsoft.Dafny;
 
 public class TypeSynonymDecl : TypeSynonymDeclBase, RevealableTypeDecl {
- public override string WhatKind { get { return "type synonym"; } }
+ public override string WhatKind => "type synonym";
+
  public TypeSynonymDecl(RangeToken rangeToken, Name name, TypeParameter.TypeParameterCharacteristics characteristics, List<TypeParameter> typeArgs, ModuleDefinition module, Type rhs, Attributes attributes)
  : base(rangeToken, name, characteristics, typeArgs, module, rhs, attributes) {
  this.NewSelfSynonym();
  }
  public TopLevelDecl AsTopLevelDecl => this;
  public TypeDeclSynonymInfo SynonymInfo { get; set; }
+ public override DafnySymbolKind Kind => DafnySymbolKind.Class;
+ public override string GetDescription(DafnyOptions options) {
+ return "type synonym";
+ }
 }
 
 public class InternalTypeSynonymDecl : TypeSynonymDeclBase {
  public override string WhatKind { get { return "export-provided type"; } }
  public InternalTypeSynonymDecl(RangeToken rangeToken, Name name, TypeParameter.TypeParameterCharacteristics characteristics, List<TypeParameter> typeArgs, ModuleDefinition module, Type rhs, Attributes attributes)
  : base(rangeToken, name, characteristics, typeArgs, module, rhs, attributes) {
  }
+
+ public override DafnySymbolKind Kind => DafnySymbolKind.Class;
+ public override string GetDescription(DafnyOptions options) {
+ return "type synonym";
+ }
 }

Source/DafnyCore/AST/TypeDeclarations/TypeSynonymDeclBase.cs

@@ -115,4 +115,7 @@ public string GetTriviaContainingDocstring() {
 
  return GetTriviaContainingDocstringFromStartTokenOrNull();
  }
+
+ public abstract DafnySymbolKind Kind { get; }
+ public abstract string GetDescription(DafnyOptions options);
 }

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

@@ -154,7 +154,7 @@ protected override void EmitBuiltInDecls(SystemModuleManager systemModuleManager
  wr.WriteLine("#if ISDAFNYRUNTIMELIB");
  }
 
- var dafnyNamespace = CreateModule("Dafny", false, false, null, wr);
+ var dafnyNamespace = CreateModule("Dafny", false, null, null, wr);
  EmitInitNewArrays(systemModuleManager, dafnyNamespace);
  if (Synthesize) {
  CsharpSynthesizer.EmitMultiMatcher(dafnyNamespace);
@@ -255,7 +255,8 @@ protected override ConcreteSyntaxTree CreateStaticMain(IClassWriter cw, string a
  return wr.NewBlock($"public static void _StaticMain(Dafny.ISequence<Dafny.ISequence<{CharTypeName}>> {argsParameterName})");
  }
 
- protected override ConcreteSyntaxTree CreateModule(string moduleName, bool isDefault, bool isExtern, string /*?*/ libraryName, ConcreteSyntaxTree wr) {
+ protected override ConcreteSyntaxTree CreateModule(string moduleName, bool isDefault, ModuleDefinition externModule,
+ string libraryName /*?*/, ConcreteSyntaxTree wr) {
  return wr.NewBlock($"namespace {IdProtect(moduleName)}", " // end of " + $"namespace {IdProtect(moduleName)}");
  }
 

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

@@ -158,7 +158,8 @@ protected override ConcreteSyntaxTree CreateStaticMain(IClassWriter cw, string a
  return wr.NewBlock($"int main(DafnySequence<DafnySequence<char>> {argsParameterName})");
  }
 
- protected override ConcreteSyntaxTree CreateModule(string moduleName, bool isDefault, bool isExtern, string/*?*/ libraryName, ConcreteSyntaxTree wr) {
+ protected override ConcreteSyntaxTree CreateModule(string moduleName, bool isDefault, ModuleDefinition externModule,
+ string libraryName /*?*/, ConcreteSyntaxTree wr) {
  var s = $"namespace {IdProtect(moduleName)} ";
  string footer = "// end of " + s + " declarations";
  this.modDeclWr = this.modDeclsWr.NewBlock(s, footer);

Source/DafnyCore/Compilers/Dafny/Compiler-dafny.cs

@@ -104,10 +104,10 @@ protected override ConcreteSyntaxTree CreateStaticMain(IClassWriter cw, string a
  throw new UnsupportedFeatureException(Token.NoToken, Feature.RunAllTests);
  }
 
- protected override ConcreteSyntaxTree CreateModule(string moduleName, bool isDefault, bool isExtern,
-  string libraryName, ConcreteSyntaxTree wr) {
+ protected override ConcreteSyntaxTree CreateModule(string moduleName, bool isDefault, ModuleDefinition externModule,
+ string libraryName, ConcreteSyntaxTree wr) {
  if (currentBuilder is ModuleContainer moduleBuilder) {
- currentBuilder = moduleBuilder.Module(moduleName, isExtern);
+ currentBuilder = moduleBuilder.Module(moduleName, externModule != null);
  } else {
  throw new UnsupportedFeatureException(Token.NoToken, Feature.RunAllTests);
  }

Source/DafnyCore/Compilers/GoLang/Compiler-go.cs

@@ -37,7 +37,7 @@ string FormatDefaultTypeParameterValue(TopLevelDecl tp) {
  return $"_default_{tp.GetCompileName(Options)}";
  }
 
- private readonly List<Import> Imports = new List<Import>(StandardImports);
+ private readonly List<Import> Imports = new(StandardImports);
  private string ModuleName;
  private ConcreteSyntaxTree RootImportWriter;
  private ConcreteSyntaxTree RootImportDummyWriter;
@@ -52,7 +52,7 @@ string FormatDefaultTypeParameterValue(TopLevelDecl tp) {
 
  private struct Import {
  public string Name, Path;
- public bool SuppressDummy;
+ public ModuleDefinition ExternModule;
  }
 
  protected override void EmitHeader(Program program, ConcreteSyntaxTree wr) {
@@ -134,7 +134,7 @@ protected override ConcreteSyntaxTree CreateStaticMain(IClassWriter cw, string a
  return wr.NewNamedBlock("func (_this * {0}) Main({1} _dafny.Sequence)", FormatCompanionTypeName(((GoCompiler.ClassWriter)cw).ClassName), argsParameterName);
  }
 
- private Import CreateImport(string moduleName, bool isDefault, bool isExtern, string /*?*/ libraryName) {
+ private Import CreateImport(string moduleName, bool isDefault, ModuleDefinition externModule, string /*?*/ libraryName) {
  string pkgName;
  if (libraryName != null) {
  pkgName = libraryName;
@@ -151,24 +151,18 @@ private Import CreateImport(string moduleName, bool isDefault, bool isExtern, st
  }
  }
 
- var import = new Import { Name = moduleName, Path = pkgName };
- if (isExtern) {
- // Allow the library name to be "" to import built-in things like the error type
- if (pkgName != "") {
- import.SuppressDummy = true;
- }
- }
-
- return import;
+ return new Import { Name = moduleName, Path = pkgName, ExternModule = externModule };
  }
 
- protected override ConcreteSyntaxTree CreateModule(string moduleName, bool isDefault, bool isExtern, string/*?*/ libraryName, ConcreteSyntaxTree wr) {
+ protected override ConcreteSyntaxTree CreateModule(string moduleName, bool isDefault,
+ ModuleDefinition externModule,
+ string libraryName /*?*/, ConcreteSyntaxTree wr) {
  if (isDefault) {
  // Fold the default module into the main module
  return wr;
  }
 
- var import = CreateImport(moduleName, isDefault, isExtern, libraryName);
+ var import = CreateImport(moduleName, isDefault, externModule, libraryName);
 
  var filename = string.Format("{0}/{0}.go", import.Path);
  var w = wr.NewFile(filename);
@@ -180,8 +174,9 @@ protected override ConcreteSyntaxTree CreateModule(string moduleName, bool isDef
  return w;
  }
 
- protected override void DependOnModule(string moduleName, bool isDefault, bool isExtern, string libraryName) {
- var import = CreateImport(moduleName, isDefault, isExtern, libraryName);
+ protected override void DependOnModule(string moduleName, bool isDefault, ModuleDefinition externModule,
+ string libraryName) {
+ var import = CreateImport(moduleName, isDefault, externModule, libraryName);
  AddImport(import);
  }
 
@@ -202,11 +197,32 @@ private void EmitImport(Import import, ConcreteSyntaxTree importWriter, Concrete
 
  importWriter.WriteLine("{0} \"{1}\"", id, path);
 
- if (!import.SuppressDummy) {
- if (id == "os") {
- importDummyWriter.WriteLine("var _ = os.Args");
+ bool isType;
+ string memberName = null;
+ if (id == "os") {
+ memberName = "Args";
+ isType = false;
+ } else {
+ isType = true;
+ if (import.ExternModule != null) {
+ var attributes = Attributes.Find(import.ExternModule.Attributes, "dummyImportMember");
+ if (attributes != null && attributes.Args.Count == 2) {
+ if (attributes.Args[0] is LiteralExpr expr1 && expr1.Value is string isNameValue &&
+ attributes.Args[1] is LiteralExpr expr2 && expr2.Value is bool isTypeValue) {
+ memberName = isNameValue;
+ isType = isTypeValue;
+ }
+ }
+ } else {
+ memberName = DummyTypeName;
+ }
+ }
+
+ if (memberName != null) {
+ if (isType) {
+ importDummyWriter.WriteLine("var _ {0}.{1}", id, memberName);
  } else {
- importDummyWriter.WriteLine("var _ {0}.{1}", id, DummyTypeName);
+ importDummyWriter.WriteLine("var _ = {0}.{1}", id, memberName);
  }
  }
  }

Source/DafnyCore/Compilers/Java/Compiler-java.cs

@@ -370,7 +370,8 @@ private void EmitImport(Import import, ConcreteSyntaxTree importWriter) {
  importWriter.WriteLine($"import {import.Path.Replace('/', '.')}.*;");
  }
 
- protected override ConcreteSyntaxTree CreateModule(string moduleName, bool isDefault, bool isExtern, string /*?*/ libraryName, ConcreteSyntaxTree wr) {
+ protected override ConcreteSyntaxTree CreateModule(string moduleName, bool isDefault, ModuleDefinition externModule,
+ string libraryName /*?*/, ConcreteSyntaxTree wr) {
  if (isDefault) {
  // Fold the default module into the main module
  moduleName = "_System";

Source/DafnyCore/Compilers/JavaScript/Compiler-js.cs

@@ -59,16 +59,17 @@ protected override ConcreteSyntaxTree CreateStaticMain(IClassWriter cw, string a
  return wr.NewBlock($"static Main({argsParameterName})");
  }
 
- protected override ConcreteSyntaxTree CreateModule(string moduleName, bool isDefault, bool isExtern, string/*?*/ libraryName, ConcreteSyntaxTree wr) {
+ protected override ConcreteSyntaxTree CreateModule(string moduleName, bool isDefault, ModuleDefinition externModule,
+ string libraryName /*?*/, ConcreteSyntaxTree wr) {
  moduleName = IdProtect(moduleName);
- if (!isExtern || libraryName != null) {
+ if (externModule == null || libraryName != null) {
  wr.Write("let {0} = ", moduleName);
  }
 
  string footer = ")(); // end of module " + moduleName;
  var block = wr.NewBlock("(function()", footer);
  var beforeReturnBody = block.Fork(0);
- if (!isExtern) {
+ if (externModule == null) {
  // create new module here
  beforeReturnBody.WriteLine("let $module = {};");
  } else if (libraryName == null) {

Source/DafnyCore/Compilers/Python/Compiler-python.cs

@@ -87,15 +87,16 @@ protected override ConcreteSyntaxTree CreateStaticMain(IClassWriter cw, string a
  return mw.NewBlockPy($"def StaticMain({argsParameterName}):");
  }
 
- protected override ConcreteSyntaxTree CreateModule(string moduleName, bool isDefault, bool isExtern,
-  string libraryName, ConcreteSyntaxTree wr) {
+ protected override ConcreteSyntaxTree CreateModule(string moduleName, bool isDefault, ModuleDefinition externModule,
+ string libraryName, ConcreteSyntaxTree wr) {
  moduleName = IdProtect(moduleName);
  var file = wr.NewFile($"{moduleName}.py");
  EmitImports(moduleName, file);
  return file;
  }
 
- protected override void DependOnModule(string moduleName, bool isDefault, bool isExtern, string libraryName) {
+ protected override void DependOnModule(string moduleName, bool isDefault, ModuleDefinition externModule,
+ string libraryName) {
  moduleName = IdProtect(moduleName);
  Imports.Add(moduleName);
  }

Source/DafnyCore/Compilers/SinglePassCompiler.cs

@@ -167,12 +167,14 @@ protected void CheckSystemModulePopulatedToCommonLimits(SystemModuleManager syst
  /// call to the instance Main method in the enclosing class.
  /// </summary>
  protected abstract ConcreteSyntaxTree CreateStaticMain(IClassWriter wr, string argsParameterName);
- protected abstract ConcreteSyntaxTree CreateModule(string moduleName, bool isDefault, bool isExtern, string/*?*/ libraryName, ConcreteSyntaxTree wr);
+ protected abstract ConcreteSyntaxTree CreateModule(string moduleName, bool isDefault, ModuleDefinition externModule,
+ string libraryName /*?*/, ConcreteSyntaxTree wr);
  /// <summary>
  /// Indicates the current program depends on the given module without creating it.
  /// Called when a module is out of scope for compilation, such as when using --library.
  /// </summary>
- protected virtual void DependOnModule(string moduleName, bool isDefault, bool isExtern, string/*?*/ libraryName) { }
+ protected virtual void DependOnModule(string moduleName, bool isDefault, ModuleDefinition externModule,
+ string libraryName /*?*/) { }
  protected abstract string GetHelperModuleName();
  protected interface IClassWriter {
  ConcreteSyntaxTree/*?*/ CreateMethod(Method m, List<TypeArgumentInstantiation> typeArgs, bool createBody, bool forBodyInheritance, bool lookasideBody);
@@ -1449,7 +1451,7 @@ private void EmitModule(Program program, ConcreteSyntaxTree programNode, ModuleD
 
  DetectAndMarkCapitalizationConflicts(module);
 
- var moduleIsExtern = false;
+ ModuleDefinition externModule = null;
  string libraryName = null;
  if (!Options.DisallowExterns) {
  var args = Attributes.FindExpressions(module.Attributes, "extern");
@@ -1458,16 +1460,16 @@ private void EmitModule(Program program, ConcreteSyntaxTree programNode, ModuleD
  libraryName = (string)(args[1] as StringLiteralExpr)?.Value;
  }
 
- moduleIsExtern = true;
+ externModule = module;
  }
  }
 
  if (!module.ShouldCompile(program.Compilation)) {
- DependOnModule(module.GetCompileName(Options), module.IsDefaultModule, moduleIsExtern, libraryName);
+ DependOnModule(module.GetCompileName(Options), module.IsDefaultModule, externModule, libraryName);
  return;
  }
 
- var wr = CreateModule(module.GetCompileName(Options), module.IsDefaultModule, moduleIsExtern, libraryName, programNode);
+ var wr = CreateModule(module.GetCompileName(Options), module.IsDefaultModule, externModule, libraryName, programNode);
  var v = new CheckHasNoAssumes_Visitor(this, wr);
  Contract.Assert(enclosingModule == null);
  enclosingModule = module;

Source/DafnyRuntime/DafnyRuntimeJava/gradle/wrapper/gradle-wrapper.properties

@@ -1,6 +1,6 @@
 distributionBase=GRADLE_USER_HOME
 distributionPath=wrapper/dists
-distributionUrl=https\://services.gradle.org/distributions/gradle-8.1.1-bin.zip
+distributionUrl=https\://services.gradle.org/distributions/gradle-8.4-rc-3-bin.zip
 networkTimeout=10000
 zipStoreBase=GRADLE_USER_HOME
 zipStorePath=wrapper/dists

Source/DafnyStandardLibraries/Makefile

@@ -23,11 +23,11 @@ update-binary: build-binary
 # with deeper coverage of module functionality.
 test:
  $(DAFNY) build -t:lib examples/dfyconfig.toml --output:build/stdlibexamples.doo
- $(DAFNY) test -t:cs build/stdlibexamples.doo --output:build/stdlibexamples
- $(DAFNY) test -t:java build/stdlibexamples.doo --output:build/stdlibexamples
- $(DAFNY) test -t:go build/stdlibexamples.doo --output:build/stdlibexamples
- $(DAFNY) test -t:py build/stdlibexamples.doo --output:build/stdlibexamples
- $(DAFNY) test -t:js build/stdlibexamples.doo --output:build/stdlibexamples
+ $(DAFNY) test -t:cs build/stdlibexamples.doo examples/BoundedInts/NonDefault.cs --output:build/stdlibexamples
+ $(DAFNY) test -t:java build/stdlibexamples.doo examples/BoundedInts/Externs/NonDefault.java --output:build/stdlibexamples
+ $(DAFNY) test -t:go build/stdlibexamples.doo examples/BoundedInts/NonDefault.go --output:build/stdlibexamples
+ $(DAFNY) test -t:py build/stdlibexamples.doo examples/BoundedInts/NonDefault.py --output:build/stdlibexamples
+ $(DAFNY) test -t:js build/stdlibexamples.doo examples/BoundedInts/NonDefault.js --output:build/stdlibexamples
 
 format:
  $(DAFNY) format .