Feat rust externs subsets eta names tests

.github/workflows/runtime-tests.yml

@@ -48,7 +48,7 @@ jobs:
           cd ./Source/DafnyCore
           make test
           make check-format
-      - name: Test DafnyRuntime (C#)
+      - name: Test DafnyRuntime (C#, Rust)
         run: |
           cd ./Source/DafnyRuntime
           make all
@@ -72,3 +72,7 @@ jobs:
         run: |
           cd ./Source/DafnyRuntime/DafnyRuntimeJs
           make all
+      - name: Test DafnyRuntimeRust
+        run: |
+          cd ./Source/DafnyRuntime/DafnyRuntimeRust
+          cargo test

Makefile

@@ -87,17 +87,25 @@ clean:
 update-cs-module:
 	(cd "${DIR}"; cd Source/DafnyRuntime; make update-system-module)
 
+update-rs-module:
+	(cd "${DIR}"; cd Source/DafnyRuntime; make update-system-module-rs)
+
 update-go-module:
 	(cd "${DIR}"; cd Source/DafnyRuntime/DafnyRuntimeGo; make update-system-module)
 
 update-runtime-dafny:
 	(cd "${DIR}"; cd Source/DafnyRuntime/DafnyRuntimeDafny; make update-go)
 
+pr-nogeneration: format-dfy format update-runtime-dafny update-cs-module update-rs-module update-go-module
+
 # `make pr` will bring you in a state suitable for submitting a PR
 # - Builds the Dafny executable
 # - Use the build to convert core .dfy files to .cs
 # - Rebuilds the Dafny executable with this .cs files
 # - Apply dafny format on all dfy files
 # - Apply dotnet format on all cs files except the generated ones
 # - Rebuild the Go and C# runtime modules as needed.
-pr: exe dfy-to-cs-exe format-dfy format update-runtime-dafny update-cs-module update-go-module
+pr: exe dfy-to-cs-exe pr-nogeneration
+
+# Same as `make pr` but useful when resolving conflicts, to take the last compiled version of Dafny first
+pr-conflict: dfy-to-cs-exe dfy-to-cs-exe pr-nogeneration

Source/DafnyCore.Test/GeneratedFromDafny/FactorPathsOptimizationTest.cs

@@ -0,0 +1,47 @@
+// Dafny program the_program compiled into C#
+// To recompile, you will need the libraries
+//     System.Runtime.Numerics.dll System.Collections.Immutable.dll
+// but the 'dotnet' tool in net6.0 should pick those up automatically.
+// Optionally, you may want to include compiler switches like
+//     /debug /nowarn:162,164,168,183,219,436,1717,1718
+
+using System;
+using System.Numerics;
+using System.Collections;
+#pragma warning disable CS0164 // This label has not been referenced
+#pragma warning disable CS0162 // Unreachable code detected
+#pragma warning disable CS1717 // Assignment made to same variable
+
+namespace FactorPathsOptimizationTest {
+
+  public partial class __default {
+    public static void ShouldBeEqual(RAST._IMod a, RAST._IMod b)
+    {
+      Dafny.ISequence<Dafny.Rune> _0_sA;
+      _0_sA = (a)._ToString(Dafny.Sequence<Dafny.Rune>.UnicodeFromString(""));
+      Dafny.ISequence<Dafny.Rune> _1_sB;
+      _1_sB = (b)._ToString(Dafny.Sequence<Dafny.Rune>.UnicodeFromString(""));
+      if (!(_0_sA).Equals(_1_sB)) {
+        Dafny.Helpers.Print((Dafny.Sequence<Dafny.Rune>.Concat(Dafny.Sequence<Dafny.Rune>.Concat(Dafny.Sequence<Dafny.Rune>.UnicodeFromString("Got:\n"), _0_sA), Dafny.Sequence<Dafny.Rune>.UnicodeFromString("\n"))).ToVerbatimString(false));
+        Dafny.Helpers.Print((Dafny.Sequence<Dafny.Rune>.Concat(Dafny.Sequence<Dafny.Rune>.Concat(Dafny.Sequence<Dafny.Rune>.UnicodeFromString("Expected:\n"), _1_sB), Dafny.Sequence<Dafny.Rune>.UnicodeFromString("\n"))).ToVerbatimString(false));
+        if (!((_0_sA).Equals(_1_sB))) {
+          throw new Dafny.HaltException("Backends/Rust/Dafny-compiler-rust-path-simplification.dfy(12,6): " + Dafny.Sequence<Dafny.Rune>.UnicodeFromString("expectation violation").ToVerbatimString(false));}
+      }
+    }
+    public static void TestApply()
+    {
+      RAST._ITypeParamDecl _0_T__Decl;
+      _0_T__Decl = RAST.TypeParamDecl.create(Dafny.Sequence<Dafny.Rune>.UnicodeFromString("T"), Dafny.Sequence<RAST._IType>.FromElements(RAST.__default.DafnyType));
+      RAST._ITypeParamDecl _1_T__Decl__simp;
+      _1_T__Decl__simp = RAST.TypeParamDecl.create(Dafny.Sequence<Dafny.Rune>.UnicodeFromString("T"), Dafny.Sequence<RAST._IType>.FromElements(RAST.Type.create_TIdentifier(Dafny.Sequence<Dafny.Rune>.UnicodeFromString("DafnyType"))));
+      RAST._IType _2_T;
+      _2_T = RAST.Type.create_TIdentifier(Dafny.Sequence<Dafny.Rune>.UnicodeFromString("T"));
+      RAST._IPath _3_std__any__Any;
+      _3_std__any__Any = (((RAST.__default.@global).MSel(Dafny.Sequence<Dafny.Rune>.UnicodeFromString("std"))).MSel(Dafny.Sequence<Dafny.Rune>.UnicodeFromString("any"))).MSel(Dafny.Sequence<Dafny.Rune>.UnicodeFromString("Any"));
+      RAST._IType _4_Any;
+      _4_Any = RAST.Type.create_TIdentifier(Dafny.Sequence<Dafny.Rune>.UnicodeFromString("Any"));
+      FactorPathsOptimizationTest.__default.ShouldBeEqual(FactorPathsOptimization.__default.apply(RAST.Mod.create_Mod(Dafny.Sequence<Dafny.Rune>.UnicodeFromString("onemodule"), Dafny.Sequence<RAST._IModDecl>.FromElements(RAST.ModDecl.create_StructDecl(RAST.Struct.create(Dafny.Sequence<Dafny.ISequence<Dafny.Rune>>.FromElements(), Dafny.Sequence<Dafny.Rune>.UnicodeFromString("test"), Dafny.Sequence<RAST._ITypeParamDecl>.FromElements(_0_T__Decl), RAST.Fields.create_NamedFields(Dafny.Sequence<RAST._IField>.FromElements(RAST.Field.create(RAST.Visibility.create_PUB(), RAST.Formal.create(Dafny.Sequence<Dafny.Rune>.UnicodeFromString("a"), (_3_std__any__Any).AsType())))))), RAST.ModDecl.create_ImplDecl(RAST.Impl.create_Impl(Dafny.Sequence<RAST._ITypeParamDecl>.FromElements(_0_T__Decl), (RAST.Type.create_TIdentifier(Dafny.Sequence<Dafny.Rune>.UnicodeFromString("test"))).Apply(Dafny.Sequence<RAST._IType>.FromElements(_2_T)), Dafny.Sequence<Dafny.Rune>.UnicodeFromString(""), Dafny.Sequence<RAST._IImplMember>.FromElements())), RAST.ModDecl.create_ImplDecl(RAST.Impl.create_ImplFor(Dafny.Sequence<RAST._ITypeParamDecl>.FromElements(_0_T__Decl), (_3_std__any__Any).AsType(), ((((RAST.__default.crate).MSel(Dafny.Sequence<Dafny.Rune>.UnicodeFromString("onemodule"))).MSel(Dafny.Sequence<Dafny.Rune>.UnicodeFromString("test"))).AsType()).Apply(Dafny.Sequence<RAST._IType>.FromElements(_2_T)), Dafny.Sequence<Dafny.Rune>.UnicodeFromString(""), Dafny.Sequence<RAST._IImplMember>.FromElements()))))), RAST.Mod.create_Mod(Dafny.Sequence<Dafny.Rune>.UnicodeFromString("onemodule"), Dafny.Sequence<RAST._IModDecl>.FromElements(RAST.ModDecl.create_UseDecl(RAST.Use.create(RAST.Visibility.create_PUB(), (RAST.__default.dafny__runtime).MSel(Dafny.Sequence<Dafny.Rune>.UnicodeFromString("DafnyType")))), RAST.ModDecl.create_UseDecl(RAST.Use.create(RAST.Visibility.create_PUB(), _3_std__any__Any)), RAST.ModDecl.create_StructDecl(RAST.Struct.create(Dafny.Sequence<Dafny.ISequence<Dafny.Rune>>.FromElements(), Dafny.Sequence<Dafny.Rune>.UnicodeFromString("test"), Dafny.Sequence<RAST._ITypeParamDecl>.FromElements(_1_T__Decl__simp), RAST.Fields.create_NamedFields(Dafny.Sequence<RAST._IField>.FromElements(RAST.Field.create(RAST.Visibility.create_PUB(), RAST.Formal.create(Dafny.Sequence<Dafny.Rune>.UnicodeFromString("a"), _4_Any)))))), RAST.ModDecl.create_ImplDecl(RAST.Impl.create_Impl(Dafny.Sequence<RAST._ITypeParamDecl>.FromElements(_1_T__Decl__simp), (RAST.Type.create_TIdentifier(Dafny.Sequence<Dafny.Rune>.UnicodeFromString("test"))).Apply(Dafny.Sequence<RAST._IType>.FromElements(_2_T)), Dafny.Sequence<Dafny.Rune>.UnicodeFromString(""), Dafny.Sequence<RAST._IImplMember>.FromElements())), RAST.ModDecl.create_ImplDecl(RAST.Impl.create_ImplFor(Dafny.Sequence<RAST._ITypeParamDecl>.FromElements(_1_T__Decl__simp), _4_Any, (RAST.Type.create_TIdentifier(Dafny.Sequence<Dafny.Rune>.UnicodeFromString("test"))).Apply(Dafny.Sequence<RAST._IType>.FromElements(_2_T)), Dafny.Sequence<Dafny.Rune>.UnicodeFromString(""), Dafny.Sequence<RAST._IImplMember>.FromElements())))));
+      FactorPathsOptimizationTest.__default.ShouldBeEqual(FactorPathsOptimization.__default.apply(RAST.Mod.create_Mod(Dafny.Sequence<Dafny.Rune>.UnicodeFromString("onemodule"), Dafny.Sequence<RAST._IModDecl>.FromElements(RAST.ModDecl.create_ImplDecl(RAST.Impl.create_ImplFor(Dafny.Sequence<RAST._ITypeParamDecl>.FromElements(_0_T__Decl), (((RAST.__default.dafny__runtime).MSel(Dafny.Sequence<Dafny.Rune>.UnicodeFromString("UpcastObject"))).AsType()).Apply(Dafny.Sequence<RAST._IType>.FromElements(RAST.Type.create_TIdentifier(Dafny.Sequence<Dafny.Rune>.UnicodeFromString("x")))), (RAST.Type.create_TIdentifier(Dafny.Sequence<Dafny.Rune>.UnicodeFromString("test"))).Apply(Dafny.Sequence<RAST._IType>.FromElements(_2_T)), Dafny.Sequence<Dafny.Rune>.UnicodeFromString(""), Dafny.Sequence<RAST._IImplMember>.FromElements()))))), RAST.Mod.create_Mod(Dafny.Sequence<Dafny.Rune>.UnicodeFromString("onemodule"), Dafny.Sequence<RAST._IModDecl>.FromElements(RAST.ModDecl.create_UseDecl(RAST.Use.create(RAST.Visibility.create_PUB(), (RAST.__default.dafny__runtime).MSel(Dafny.Sequence<Dafny.Rune>.UnicodeFromString("DafnyType")))), RAST.ModDecl.create_UseDecl(RAST.Use.create(RAST.Visibility.create_PUB(), (RAST.__default.dafny__runtime).MSel(Dafny.Sequence<Dafny.Rune>.UnicodeFromString("UpcastObject")))), RAST.ModDecl.create_ImplDecl(RAST.Impl.create_ImplFor(Dafny.Sequence<RAST._ITypeParamDecl>.FromElements(_1_T__Decl__simp), (RAST.Type.create_TIdentifier(Dafny.Sequence<Dafny.Rune>.UnicodeFromString("UpcastObject"))).Apply(Dafny.Sequence<RAST._IType>.FromElements(RAST.Type.create_TIdentifier(Dafny.Sequence<Dafny.Rune>.UnicodeFromString("x")))), (RAST.Type.create_TIdentifier(Dafny.Sequence<Dafny.Rune>.UnicodeFromString("test"))).Apply(Dafny.Sequence<RAST._IType>.FromElements(_2_T)), Dafny.Sequence<Dafny.Rune>.UnicodeFromString(""), Dafny.Sequence<RAST._IImplMember>.FromElements())))));
+    }
+  }
+} // end of namespace FactorPathsOptimizationTest

Source/DafnyCore/Backends/Dafny/AST.dfy

@@ -35,8 +35,10 @@ module {:extern "DAST"} DAST {
   // 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)
+  // None would need to be escaped.
+  datatype VarName = VarName(dafny_name: string)
 
-  datatype Module = Module(name: Name, attributes: seq<Attribute>, body: Option<seq<ModuleItem>>)
+  datatype Module = Module(name: Name, attributes: seq<Attribute>, requiresExterns: bool, body: Option<seq<ModuleItem>>)
 
   datatype ModuleItem =
     | Module(Module)
@@ -45,6 +47,28 @@ module {:extern "DAST"} DAST {
     | Newtype(Newtype)
     | SynonymType(SynonymType)
     | Datatype(Datatype)
+  {
+    function name(): Name {
+      match this {
+        case Module(m) => m.name
+        case Class(m) => m.name
+        case Trait(m) => m.name
+        case Newtype(m) => m.name
+        case SynonymType(m) => m.name
+        case Datatype(m) => m.name
+      }
+    }
+    function attributes(): seq<Attribute> {
+      match this {
+        case Module(m) => m.attributes
+        case Class(m) => m.attributes
+        case Trait(m) => m.attributes
+        case Newtype(m) => m.attributes
+        case SynonymType(m) => m.attributes
+        case Datatype(m) => m.attributes
+      }
+    }
+  }
 
   datatype Type =
     UserDefined(resolved: ResolvedType) |
@@ -127,7 +151,7 @@ module {:extern "DAST"} DAST {
     typeArgs: seq<Type>,
     kind: ResolvedTypeBase,
     attributes: seq<Attribute>,
-    properMethods: seq<Ident>,
+    properMethods: seq<Name>,
     extendedTypes: seq<Type>) {
     function Replace(mapping: map<Type, Type>): ResolvedType {
       ResolvedType(
@@ -175,7 +199,7 @@ module {:extern "DAST"} DAST {
 
   datatype Field = Field(formal: Formal, defaultValue: Option<Expression>)
 
-  datatype Formal = Formal(name: Name, typ: Type, attributes: seq<Attribute>)
+  datatype Formal = Formal(name: VarName, typ: Type, attributes: seq<Attribute>)
 
   datatype Method = Method(
     isStatic: bool,
@@ -188,22 +212,22 @@ module {:extern "DAST"} DAST {
     params: seq<Formal>,
     body: seq<Statement>,
     outTypes: seq<Type>,
-    outVars: Option<seq<Ident>>)
+    outVars: Option<seq<VarName>>)
 
   datatype CallSignature = CallSignature(parameters: seq<Formal>)
 
   datatype CallName =
-    CallName(name: Name, onType: Option<Type>, receiverArgs: Option<Formal>, signature: CallSignature) |
+    CallName(name: Name, onType: Option<Type>, receiverArg: Option<Formal>, receiverAsArgument: bool, signature: CallSignature) |
     MapBuilderAdd | MapBuilderBuild | SetBuilderAdd | SetBuilderBuild
 
   datatype Statement =
-    DeclareVar(name: Name, typ: Type, maybeValue: Option<Expression>) |
+    DeclareVar(name: VarName, 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: Name, boundType: Type, over: Expression, body: seq<Statement>) |
-    Call(on: Expression, callName: CallName, typeArgs: seq<Type>, args: seq<Expression>, outs: Option<seq<Ident>>) |
+    Foreach(boundName: VarName, boundType: Type, over: Expression, body: seq<Statement>) |
+    Call(on: Expression, callName: CallName, typeArgs: seq<Type>, args: seq<Expression>, outs: Option<seq<VarName>>) |
     Return(expr: Expression) |
     EarlyReturn() |
     Break(toLabel: Option<string>) |
@@ -216,8 +240,8 @@ module {:extern "DAST"} DAST {
   }
 
   datatype AssignLhs =
-    Ident(ident: Ident) |
-    Select(expr: Expression, field: Name) |
+    Ident(ident: VarName) |
+    Select(expr: Expression, field: VarName) |
     Index(expr: Expression, indices: seq<Expression>)
 
   datatype CollKind = Seq | Array | Map
@@ -244,14 +268,15 @@ module {:extern "DAST"} DAST {
 
   datatype Expression =
     Literal(Literal) |
-    Ident(name: Name) |
+    Ident(name: VarName) |
     Companion(seq<Ident>, typeArgs: seq<Type>) |
+    ExternCompanion(seq<Ident>) |
     Tuple(seq<Expression>) |
     New(path: seq<Ident>, typeArgs: seq<Type>, args: seq<Expression>) |
     NewUninitArray(dims: seq<Expression>, typ: Type) |
     ArrayIndexToInt(value: Expression) |
     FinalizeNewArray(value: Expression, typ: Type) |
-    DatatypeValue(datatypeType: ResolvedType, typeArgs: seq<Type>, variant: Name, isCo: bool, contents: seq<(string, Expression)>) |
+    DatatypeValue(datatypeType: ResolvedType, typeArgs: seq<Type>, variant: Name, isCo: bool, contents: seq<(VarName, Expression)>) |
     Convert(value: Expression, from: Type, typ: Type) |
     SeqConstruct(length: Expression, elem: Expression) |
     SeqValue(elements: seq<Expression>, typ: Type) |
@@ -270,23 +295,25 @@ module {:extern "DAST"} DAST {
     ArrayLen(expr: Expression, exprType: Type, dim: nat, native: bool) |
     MapKeys(expr: Expression) |
     MapValues(expr: Expression) |
-    Select(expr: Expression, field: Name, isConstant: bool, onDatatype: bool, fieldType: Type) |
-    SelectFn(expr: Expression, field: Name, onDatatype: bool, isStatic: bool, arity: nat) |
+    MapItems(expr: Expression) |
+    Select(expr: Expression, field: VarName, isConstant: bool, onDatatype: bool, fieldType: Type) |
+    SelectFn(expr: Expression, field: VarName, onDatatype: bool, isStatic: bool, isConstant: bool, arguments: seq<Type>) |
     Index(expr: Expression, collKind: CollKind, indices: seq<Expression>) |
     IndexRange(expr: Expression, isArray: bool, low: Option<Expression>, high: Option<Expression>) |
     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(ident: Ident, typ: Type, value: Expression, iifeBody: Expression) |
+    IIFE(ident: VarName, typ: Type, value: Expression, iifeBody: Expression) |
     Apply(expr: Expression, args: seq<Expression>) |
     TypeTest(on: Expression, dType: seq<Ident>, variant: Name) |
+    Is(expr: Expression, fromType: Type, toType: Type) |
     InitializationValue(typ: Type) |
     BoolBoundedPool() |
     SetBoundedPool(of: Expression) |
     MapBoundedPool(of: Expression) |
     SeqBoundedPool(of: Expression, includeDuplicates: bool) |
-    IntRange(lo: Expression, hi: Expression, up: bool) |
+    IntRange(elemType: Type, lo: Expression, hi: Expression, up: bool) |
     UnboundedIntRange(start: Expression, up: bool) |
     Quantifier(elemType: Type, collection: Expression, is_forall: bool, lambda: Expression)
 

Source/DafnyCore/Backends/Dafny/ASTBuilder.cs

@@ -35,13 +35,13 @@ public void AddUnsupported(string why) {
   interface ModuleContainer : Container {
     void AddModule(Module item);
 
-    public ModuleBuilder Module(string name, Sequence<Attribute> attributes) {
-      return new ModuleBuilder(this, name, attributes);
+    public ModuleBuilder Module(string name, Sequence<Attribute> attributes, bool requiresExterns) {
+      return new ModuleBuilder(this, name, attributes, requiresExterns);
     }
 
     static public Module UnsupportedToModule(string why) {
       return new Module(Sequence<Rune>.UnicodeFromString(why), Sequence<Attribute>.FromElements((Attribute)Attribute.create_Attribute(
-          Sequence<Rune>.UnicodeFromString(why), Sequence<Sequence<Rune>>.Empty)),
+          Sequence<Rune>.UnicodeFromString(why), Sequence<Sequence<Rune>>.Empty)), false,
         Std.Wrappers.Option<Sequence<ModuleItem>>.create_None());
     }
   }
@@ -51,11 +51,13 @@ class ModuleBuilder : ClassContainer, TraitContainer, NewtypeContainer, Datatype
     readonly string name;
     readonly Sequence<Attribute> attributes;
     readonly List<ModuleItem> body = new();
+    private readonly bool requiresExterns;
 
-    public ModuleBuilder(ModuleContainer parent, string name, Sequence<Attribute> attributes) {
+    public ModuleBuilder(ModuleContainer parent, string name, Sequence<Attribute> attributes, bool requiresExterns) {
       this.parent = parent;
       this.name = name;
       this.attributes = attributes;
+      this.requiresExterns = requiresExterns;
     }
 
     public void AddModule(Module item) {
@@ -82,6 +84,7 @@ public object Finish() {
       parent.AddModule((Module)Module.create(
         Sequence<Rune>.UnicodeFromString(this.name),
         attributes,
+        requiresExterns,
         Std.Wrappers.Option<Sequence<ModuleItem>>.create_Some((Sequence<ModuleItem>)Sequence<ModuleItem>.FromArray(body.ToArray()))
       ));
 
@@ -1834,6 +1837,7 @@ public DAST.Expression Build() {
       }
 
       return (DAST.Expression)DAST.Expression.create_IntRange(
+        DAST.Type.create_Primitive(DAST.Primitive.create_Int()),
         startExpr, endExpr, true);
     }