Support subset types in the Rust backend (#4422)

Support subset types in the Rust backend <small>By submitting this pull request, I confirm that my contribution is made under the terms of the [MIT license](https://github.com/dafny-lang/dafny/blob/master/LICENSE.txt).</small> --- Stack created with [Sapling](https://sapling-scm.com). Best reviewed with [ReviewStack](https://reviewstack.dev/dafny-lang/dafny/pull/4422). * #4438 * #4429 * __->__ #4422
dafny-lang · Aug 18, 2023 · 36c265d · 36c265d
1 parent 2a2e1c4
commit 36c265d
Show file tree

Hide file tree

Showing 11 changed files with 2,627 additions and 1,667 deletions.
diff --git a/.github/workflows/msbuild.yml b/.github/workflows/msbuild.yml
@@ -55,7 +55,7 @@ jobs:
       run: dotnet build Source/Dafny.sln
     - name: Check whitespace and style
       working-directory: dafny
-      run: dotnet tool run dotnet-format -w -s error --check Source/Dafny.sln --exclude DafnyCore/Scanner.cs --exclude DafnyCore/Parser.cs
+      run: dotnet tool run dotnet-format -w -s error --check Source/Dafny.sln --exclude DafnyCore/Scanner.cs --exclude DafnyCore/Parser.cs --exclude DafnyCore/GeneratedFromDafny.cs --exclude DafnyCore/GeneratedFromDafnyRust.cs
     - name: Create NuGet package (just to make sure it works)
       run: dotnet pack --no-build dafny/Source/Dafny.sln
     - name: Check uniformity of integration tests that exercise backends

diff --git a/Makefile b/Makefile
@@ -58,7 +58,7 @@ z3-ubuntu:
 	chmod +x ${DIR}/Binaries/z3/bin/z3-*
 
 format:
-	dotnet tool run dotnet-format -w -s error Source/Dafny.sln --exclude DafnyCore/Scanner.cs --exclude DafnyCore/Parser.cs
+	dotnet tool run dotnet-format -w -s error Source/Dafny.sln --exclude DafnyCore/Scanner.cs --exclude DafnyCore/Parser.cs --exclude DafnyCore/GeneratedFromDafny.cs --exclude DafnyCore/GeneratedFromDafnyRust.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)

diff --git a/Source/DafnyCore/Compilers/Dafny/AST.dfy b/Source/DafnyCore/Compilers/Dafny/AST.dfy
@@ -3,7 +3,7 @@ module {:extern "DAST"} DAST {
 
   datatype ModuleItem = Module(Module) | Class(Class) | Trait(Trait) | Newtype(Newtype) | Datatype(Datatype)
 
-  datatype Newtype = Newtype(name: string, base: Type, witnessExpr: Optional<Expression>)
+  datatype Newtype = Newtype(name: string, typeParams: seq<Type>, base: Type, witnessStmts: seq<Statement>, witnessExpr: Optional<Expression>)
 
   datatype Type =
     Path(seq<Ident>, typeArgs: seq<Type>, resolved: ResolvedType) |
@@ -58,7 +58,8 @@ module {:extern "DAST"} DAST {
     New(path: seq<Ident>, args: seq<Expression>) |
     NewArray(dims: seq<Expression>) |
     DatatypeValue(path: seq<Ident>, variant: string, isCo: bool, contents: seq<(string, Expression)>) |
-    NewtypeValue(tpe: Type, value: Expression) |
+    SubsetUpgrade(value: Expression, typ: Type) |
+    SubsetDowngrade(value: Expression) |
     SeqValue(elements: seq<Expression>) |
     SetValue(elements: seq<Expression>) |
     This() |
@@ -69,7 +70,7 @@ module {:extern "DAST"} DAST {
     SelectFn(expr: Expression, field: string, onDatatype: bool, isStatic: bool, arity: nat) |
     TupleSelect(expr: Expression, index: nat) |
     Call(on: Expression, name: Ident, typeArgs: seq<Type>, args: seq<Expression>) |
-    Lambda(params: seq<Formal>, body: seq<Statement>) |
+    Lambda(params: seq<Formal>, retType: Type, body: seq<Statement>) |
     IIFE(name: Ident, typ: Type, value: Expression, iifeBody: Expression) |
     Apply(expr: Expression, args: seq<Expression>) |
     TypeTest(on: Expression, dType: seq<Ident>, variant: string) |

diff --git a/Source/DafnyCore/Compilers/Dafny/ASTBuilder.cs b/Source/DafnyCore/Compilers/Dafny/ASTBuilder.cs
@@ -149,21 +149,25 @@ public object Finish() {
   interface NewtypeContainer {
     void AddNewtype(Newtype item);
 
-    public NewtypeBuilder Newtype(string name, DAST.Type baseType, DAST.Expression witness) {
-      return new NewtypeBuilder(this, name, baseType, witness);
+    public NewtypeBuilder Newtype(string name, List<DAST.Type> typeParams, DAST.Type baseType, List<DAST.Statement> witnessStmts, DAST.Expression witness) {
+      return new NewtypeBuilder(this, name, typeParams, baseType, witnessStmts, witness);
     }
   }
 
   class NewtypeBuilder : ClassLike {
     readonly NewtypeContainer parent;
     readonly string name;
+    readonly List<DAST.Type> typeParams;
     readonly DAST.Type baseType;
+    readonly List<DAST.Statement> witnessStmts;
     readonly DAST.Expression witness;
 
-    public NewtypeBuilder(NewtypeContainer parent, string name, DAST.Type baseType, DAST.Expression witness) {
+    public NewtypeBuilder(NewtypeContainer parent, string name, List<DAST.Type> typeParams, DAST.Type baseType, List<DAST.Statement> statements, DAST.Expression witness) {
       this.parent = parent;
       this.name = name;
+      this.typeParams = typeParams;
       this.baseType = baseType;
+      this.witnessStmts = statements;
       this.witness = witness;
     }
 
@@ -178,7 +182,9 @@ public void AddField(DAST.Formal item) {
     public object Finish() {
       parent.AddNewtype((Newtype)Newtype.create(
         Sequence<Rune>.UnicodeFromString(this.name),
+        Sequence<DAST.Type>.FromArray(this.typeParams.ToArray()),
         this.baseType,
+        Sequence<DAST.Statement>.FromArray(this.witnessStmts.ToArray()),
         this.witness == null ? Optional<DAST._IExpression>.create_None() : Optional<DAST._IExpression>.create_Some(this.witness)
       ));
       return parent;
@@ -699,6 +705,31 @@ public DAST.Statement Build() {
     }
   }
 
+  class StatementBuffer : StatementContainer {
+    readonly List<object> statements = new();
+
+    public void AddStatement(DAST.Statement item) {
+      statements.Add(item);
+    }
+
+    public void AddBuildable(BuildableStatement item) {
+      statements.Add(item);
+    }
+
+    public List<object> ForkList() {
+      var ret = new List<object>();
+      statements.Add(ret);
+      return ret;
+    }
+
+    public List<DAST.Statement> PopAll() {
+      var builtResult = new List<DAST.Statement>();
+      StatementContainer.RecursivelyBuild(statements, builtResult);
+
+      return builtResult;
+    }
+  }
+
   class ExprBuffer : ExprContainer {
     Stack<object> exprs = new();
     public readonly object parent;
@@ -761,8 +792,8 @@ CallExprBuilder Call() {
       return ret;
     }
 
-    LambdaExprBuilder Lambda(List<DAST.Formal> formals) {
-      var ret = new LambdaExprBuilder(formals);
+    LambdaExprBuilder Lambda(List<DAST.Formal> formals, DAST.Type retType) {
+      var ret = new LambdaExprBuilder(formals, retType);
       AddBuildable(ret);
       return ret;
     }
@@ -773,6 +804,18 @@ IIFEExprBuilder IIFE(string name, DAST.Type tpe) {
       return ret;
     }
 
+    SubsetUpgradeBuilder SubsetUpgrade(DAST.Type tpe) {
+      var ret = new SubsetUpgradeBuilder(tpe);
+      AddBuildable(ret);
+      return ret;
+    }
+
+    SubsetDowngradeBuilder SubsetDowngrade() {
+      var ret = new SubsetDowngradeBuilder();
+      AddBuildable(ret);
+      return ret;
+    }
+
     protected static void RecursivelyBuild(List<object> body, List<DAST.Expression> builtExprs) {
       foreach (var maybeBuilt in body) {
         if (maybeBuilt is DAST.Expression built) {
@@ -886,10 +929,12 @@ public DAST.Expression Build() {
 
 class LambdaExprBuilder : StatementContainer, BuildableExpr {
   readonly List<DAST.Formal> formals;
+  readonly DAST.Type retType;
   readonly List<object> body = new();
 
-  public LambdaExprBuilder(List<DAST.Formal> formals) {
+  public LambdaExprBuilder(List<DAST.Formal> formals, DAST.Type retType) {
     this.formals = formals;
+    this.retType = retType;
   }
 
   public void AddStatement(DAST.Statement item) {
@@ -912,6 +957,7 @@ public DAST.Expression Build() {
 
     return (DAST.Expression)DAST.Expression.create_Lambda(
       Sequence<DAST.Formal>.FromArray(formals.ToArray()),
+      retType,
       Sequence<DAST.Statement>.FromArray(builtBody.ToArray())
     );
   }
@@ -988,3 +1034,67 @@ public void AddBuildable(BuildableExpr item) {
     }
   }
 }
+
+class SubsetUpgradeBuilder : ExprContainer, BuildableExpr {
+  readonly DAST.Type tpe;
+  object value = null;
+
+  public SubsetUpgradeBuilder(DAST.Type tpe) {
+    this.tpe = tpe;
+  }
+
+  public void AddExpr(DAST.Expression item) {
+    if (value != null) {
+      throw new InvalidOperationException();
+    } else {
+      value = item;
+    }
+  }
+
+  public void AddBuildable(BuildableExpr item) {
+    if (value != null) {
+      throw new InvalidOperationException();
+    } else {
+      value = item;
+    }
+  }
+
+  public DAST.Expression Build() {
+    var builtValue = new List<DAST.Expression>();
+    ExprContainer.RecursivelyBuild(new List<object> { value }, builtValue);
+
+    return (DAST.Expression)DAST.Expression.create_SubsetUpgrade(
+      builtValue[0],
+      tpe
+    );
+  }
+}
+
+class SubsetDowngradeBuilder : ExprContainer, BuildableExpr {
+  object value = null;
+
+  public void AddExpr(DAST.Expression item) {
+    if (value != null) {
+      throw new InvalidOperationException();
+    } else {
+      value = item;
+    }
+  }
+
+  public void AddBuildable(BuildableExpr item) {
+    if (value != null) {
+      throw new InvalidOperationException();
+    } else {
+      value = item;
+    }
+  }
+
+  public DAST.Expression Build() {
+    var builtValue = new List<DAST.Expression>();
+    ExprContainer.RecursivelyBuild(new List<object> { value }, builtValue);
+
+    return (DAST.Expression)DAST.Expression.create_SubsetDowngrade(
+      builtValue[0]
+    );
+  }
+}