Support while, ite, and char 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>

Source/DafnyCore/Compilers/Dafny/AST.dfy

@@ -7,7 +7,7 @@ module {:extern "DAST"} DAST {
 
  datatype Type = Path(seq<Ident>, typeArgs: seq<Type>, resolved: ResolvedType) | Tuple(seq<Type>) | Primitive(Primitive) | Passthrough(string) | TypeArg(Ident)
 
- datatype Primitive = String | Bool
+ datatype Primitive = String | Bool | Char
 
  datatype ResolvedType = Datatype(path: seq<Ident>) | Newtype
 
@@ -31,6 +31,7 @@ module {:extern "DAST"} DAST {
  DeclareVar(name: string, typ: Type, maybeValue: Optional<Expression>) |
  Assign(name: string, value: Expression) |
  If(cond: Expression, thn: seq<Statement>, els: seq<Statement>) |
+ While(cond: Expression, body: seq<Statement>) |
  Call(on: Expression, name: string, typeArgs: seq<Type>, args: seq<Expression>, outs: Optional<seq<Ident>>) |
  Return(expr: Expression) |
  EarlyReturn() |
@@ -44,6 +45,7 @@ module {:extern "DAST"} DAST {
  New(path: seq<Ident>, args: seq<Expression>) |
  DatatypeValue(path: seq<Ident>, variant: string, isCo: bool, contents: seq<(string, Expression)>) |
  This() |
+ Ite(cond: Expression, thn: Expression, els: Expression) |
  BinOp(op: string, left: Expression, right: Expression) |
  Select(expr: Expression, field: string, onDatatype: bool) |
  TupleSelect(expr: Expression, index: nat) |

Source/DafnyCore/Compilers/Dafny/ASTBuilder.cs

@@ -278,6 +278,12 @@ public IfElseBuilder IfElse() {
  return ret;
  }
 
+ public WhileBuilder While() {
+ var ret = new WhileBuilder(this);
+ AddBuildable(ret);
+ return ret;
+ }
+
  public CallStmtBuilder Call(object returnTo) {
  var ret = new CallStmtBuilder(this, returnTo);
  AddBuildable(ret);
@@ -445,6 +451,49 @@ public void AddBuildable(BuildableStatement item) {
  }
  }
 
+ class WhileBuilder : ExprContainer, StatementContainer, BuildableStatement {
+ public readonly StatementContainer parent;
+
+ DAST.Expression condition = null;
+ readonly List<object> body = new();
+
+ public WhileBuilder(StatementContainer parent) {
+ this.parent = parent;
+ }
+
+ public void AddExpr(DAST.Expression value) {
+ if (condition != null) {
+ throw new InvalidOperationException();
+ } else {
+ condition = value;
+ }
+ }
+
+ public void AddStatement(DAST.Statement item) {
+ body.Add(item);
+ }
+
+ public void AddBuildable(BuildableStatement item) {
+ body.Add(item);
+ }
+
+ public List<object> ForkList() {
+ var ret = new List<object>();
+ this.body.Add(ret);
+ return ret;
+ }
+
+ public DAST.Statement Build() {
+ List<DAST.Statement> builtStatements = new();
+ StatementContainer.RecursivelyBuild(body, builtStatements);
+
+ return (DAST.Statement)DAST.Statement.create_While(
+ condition,
+ Sequence<DAST.Statement>.FromArray(builtStatements.ToArray())
+ );
+ }
+ }
+
  class CallStmtBuilder : ExprContainer, BuildableStatement {
  public readonly StatementContainer parent;
  public readonly object returnTo;

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

@@ -208,6 +208,8 @@ private DAST.Type GenType(Type typ) {
  return (DAST.Type)DAST.Type.create_Passthrough(Sequence<Rune>.UnicodeFromString("f32"));
  } else if (xType.IsStringType) {
  return (DAST.Type)DAST.Type.create_Primitive(DAST.Primitive.create_String());
+ } else if (xType.IsCharType) {
+ return (DAST.Type)DAST.Type.create_Primitive(DAST.Primitive.create_Char());
  } else if (xType is UserDefinedType udt) {
  if (udt.ResolvedClass is TypeParameter tp) {
  if (thisContext != null && thisContext.ParentFormalTypeParametersToActuals.TryGetValue(tp, out var instantiatedTypeParameter)) {
@@ -239,7 +241,9 @@ protected override void DeclareSubsetType(SubsetTypeDecl sst, ConcreteSyntaxTree
  }
 
  protected override void GetNativeInfo(NativeType.Selection sel, out string name, out string literalSuffix, out bool needsCastAfterArithmetic) {
- throw new NotImplementedException();
+ name = null;
+ literalSuffix = null;
+ needsCastAfterArithmetic = false;
  }
 
  private class ClassWriter : IClassWriter {
@@ -707,7 +711,13 @@ protected override ConcreteSyntaxTree EmitForStmt(IToken tok, IVariable loopInde
  }
 
  protected override ConcreteSyntaxTree CreateWhileLoop(out ConcreteSyntaxTree guardWriter, ConcreteSyntaxTree wr) {
- throw new NotImplementedException();
+ if (wr is BuilderSyntaxTree<StatementContainer> statementContainer) {
+ var whileBuilder = statementContainer.Builder.While();
+ guardWriter = new BuilderSyntaxTree<ExprContainer>(whileBuilder);
+ return new BuilderSyntaxTree<StatementContainer>(whileBuilder);
+ } else {
+ throw new InvalidOperationException();
+ }
  }
 
  protected override ConcreteSyntaxTree CreateForLoop(string indexVar, string bound, ConcreteSyntaxTree wr, string start = null) {
@@ -1134,7 +1144,7 @@ protected override ConcreteSyntaxTree CreateIIFE1(int source, Type resultType, I
 
  protected override void EmitUnaryExpr(ResolvedUnaryOp op, Expression expr, bool inLetExprBody,
  ConcreteSyntaxTree wr, ConcreteSyntaxTree wStmts) {
- throw new NotImplementedException();
+ throw new NotImplementedException("Unary expression: " + op);
  }
 
  protected override void CompileBinOp(BinaryExpr.ResolvedOpcode op,
@@ -1217,7 +1227,17 @@ protected override void CompileBinOp(BinaryExpr.ResolvedOpcode op,
 
  protected override void EmitITE(Expression guard, Expression thn, Expression els, Type resultType, bool inLetExprBody, ConcreteSyntaxTree wr, ConcreteSyntaxTree wStmts) {
  if (wr is BuilderSyntaxTree<ExprContainer> builder) {
- throw new NotImplementedException();
+ var guardBuffer = new ExprBuffer(null);
+ var thnBuffer = new ExprBuffer(null);
+ var elsBuffer = new ExprBuffer(null);
+ EmitExpr(guard, false, new BuilderSyntaxTree<ExprContainer>(guardBuffer), wStmts);
+ EmitExpr(thn, false, new BuilderSyntaxTree<ExprContainer>(thnBuffer), wStmts);
+ EmitExpr(els, false, new BuilderSyntaxTree<ExprContainer>(elsBuffer), wStmts);
+ builder.Builder.AddExpr((DAST.Expression)DAST.Expression.create_Ite(
+ guardBuffer.Finish(),
+ thnBuffer.Finish(),
+ elsBuffer.Finish()
+ ));
  } else {
  throw new InvalidOperationException();
  }

Source/DafnyCore/Compilers/Rust/Dafny-compiler-rust.dfy

@@ -286,6 +286,7 @@ module {:extern "DCOMP"} DCOMP {
  match p {
  case String => s := "String";
  case Bool => s := "bool";
+ case Char => s := "char";
  }
  }
  case Passthrough(v) => s := v;
@@ -458,6 +459,11 @@ module {:extern "DCOMP"} DCOMP {
  var elsString := GenStmts(els, params, earlyReturn);
  generated := "if " + condString + " {\n" + thnString + "\n} else {\n" + elsString + "\n}";
  }
+ case While(cond, body) => {
+ var condString, _, _ := GenExpr(cond, params, true);
+ var bodyString := GenStmts(body, params, earlyReturn);
+ generated := "while " + condString + " {\n" + bodyString + "\n}";
+ }
  case Call(on, name, typeArgs, args, maybeOutVars) => {
  var typeArgString := "";
  if (|typeArgs| >= 1) {
@@ -678,9 +684,24 @@ module {:extern "DCOMP"} DCOMP {
  isOwned := true;
  }
  case This() => {
- s := "self";
- isOwned := false;
- readIdents := {};
+ if mustOwn {
+ s := "self.clone()";
+ isOwned := true;
+ } else {
+ s := "self";
+ isOwned := false;
+ }
+
+ readIdents := {"self"};
+ }
+ case Ite(cond, t, f) => {
+ var condString, _, recIdentsCond := GenExpr(cond, params, true);
+ var _, tHasToBeOwned, _ := GenExpr(t, params, mustOwn); // check if t has to be owned even if not requested
+ var fString, fOwned, recIdentsF := GenExpr(f, params, tHasToBeOwned);
+ var tString, _, recIdentsT := GenExpr(t, params, fOwned); // there's a chance that f forced ownership
+ s := "(if " + condString + " {\n" + tString + "\n} else {\n" + fString + "\n})";
+ isOwned := fOwned;
+ readIdents := recIdentsCond + recIdentsT + recIdentsF;
  }
  case BinOp(op, l, r) => {
  var left, _, recIdentsL := GenExpr(l, params, true);