Nagini Conversion

JetBrains-Research · Jul 12, 2024 · 2fe1c55 · 2fe1c55
1 parent 0860638
commit 2fe1c55
Show file tree

Hide file tree

Showing 13 changed files with 468 additions and 79 deletions.
diff --git a/Source/DafnyCore/AST/Statements/Assignment/LocalVariable.cs b/Source/DafnyCore/AST/Statements/Assignment/LocalVariable.cs
@@ -80,8 +80,14 @@ public string AssignUniqueName(FreshIdGenerator generator) {
     sanitizedName ??= $"_{IVariable.CompileNameIdGenerator.FreshNumericId()}_{SanitizedNameShadowable}";
 
   string compileName;
-  public string CompileName =>
-    compileName ??= SanitizedName;
+  public string CompileName {
+    get {
+      return compileName ??= SanitizedName;
+    }
+    set {
+      compileName = value;
+    }
+  }
 
   // TODO rename and update comment? Or make it nullable?
   public readonly Type SyntacticType;  // this is the type mentioned in the declaration, if any

diff --git a/Source/DafnyCore/AST/Types/UserDefinedType.cs b/Source/DafnyCore/AST/Types/UserDefinedType.cs
@@ -17,7 +17,7 @@ void ObjectInvariant() {
   }
 
   public readonly Expression NamePath;  // either NameSegment or ExprDotName (with the inner expression satisfying this same constraint)
-  public readonly string Name;
+  public string Name;
   [Rep]
 
   public string FullName {

diff --git a/Source/DafnyCore/Backends/CSharp/CsharpCodeGenerator.cs b/Source/DafnyCore/Backends/CSharp/CsharpCodeGenerator.cs
@@ -2046,7 +2046,7 @@ protected override void EmitHalt(IToken tok, Expression/*?*/ messageExpr, Concre
     }
 
     protected override ConcreteSyntaxTree EmitForStmt(IToken tok, IVariable loopIndex, bool goingUp, string /*?*/ endVarName,
-      List<Statement> body, LList<Label> labels, ConcreteSyntaxTree wr) {
+      List<Statement> body, LList<Label> labels, out ConcreteSyntaxTree annotWriter, ConcreteSyntaxTree wr) {
 
       wr.Write($"for ({TypeName(loopIndex.Type, wr, tok)} {loopIndex.CompileName} = ");
       var startWr = wr.Fork();
@@ -2062,6 +2062,7 @@ protected override ConcreteSyntaxTree EmitForStmt(IToken tok, IVariable loopInde
         bodyWr.WriteLine($"{loopIndex.CompileName}--;");
       }
       bodyWr = EmitContinueLabel(labels, bodyWr);
+      annotWriter = bodyWr.Fork();
       TrStmtList(body, bodyWr);
 
       return startWr;

diff --git a/Source/DafnyCore/Backends/Cplusplus/CppCodeGenerator.cs b/Source/DafnyCore/Backends/Cplusplus/CppCodeGenerator.cs
@@ -1324,7 +1324,7 @@ protected override void EmitHalt(IToken tok, Expression messageExpr, ConcreteSyn
     }
 
     protected override ConcreteSyntaxTree EmitForStmt(IToken tok, IVariable loopIndex, bool goingUp, string /*?*/ endVarName,
-      List<Statement> body, LList<Label> labels, ConcreteSyntaxTree wr) {
+      List<Statement> body, LList<Label> labels, out ConcreteSyntaxTree annotWriter, ConcreteSyntaxTree wr) {
       throw new UnsupportedFeatureException(tok, Feature.ForLoops, "for loops have not yet been implemented");
     }
 

diff --git a/Source/DafnyCore/Backends/Dafny/DafnyCodeGenerator.cs b/Source/DafnyCore/Backends/Dafny/DafnyCodeGenerator.cs
@@ -1170,15 +1170,17 @@ protected override ConcreteSyntaxTree EmitBlock(ConcreteSyntaxTree wr) {
     }
 
     protected override ConcreteSyntaxTree EmitForStmt(IToken tok, IVariable loopIndex, bool goingUp, string endVarName,
-      List<Statement> body, LList<Label> labels, ConcreteSyntaxTree wr) {
+      List<Statement> body, LList<Label> labels, out ConcreteSyntaxTree annotWriter, ConcreteSyntaxTree wr) {
       AddUnsupportedFeature(tok, Feature.ForLoops);
+      annotWriter = null;
       return wr;
     }
 
-    protected override ConcreteSyntaxTree CreateWhileLoop(out ConcreteSyntaxTree guardWriter, ConcreteSyntaxTree wr) {
+    protected override ConcreteSyntaxTree CreateWhileLoop(out ConcreteSyntaxTree guardWriter, out ConcreteSyntaxTree annotWriter, ConcreteSyntaxTree wr) {
       if (wr is BuilderSyntaxTree<StatementContainer> statementContainer) {
         var whileBuilder = statementContainer.Builder.While();
         guardWriter = new BuilderSyntaxTree<ExprContainer>(whileBuilder, this);
+        annotWriter = guardWriter.Fork();
         return new BuilderSyntaxTree<StatementContainer>(whileBuilder, this);
       } else {
         throw new InvalidOperationException();

diff --git a/Source/DafnyCore/Backends/GoLang/GoCodeGenerator.cs b/Source/DafnyCore/Backends/GoLang/GoCodeGenerator.cs
@@ -2065,15 +2065,16 @@ protected override void EmitHalt(IToken tok, Expression messageExpr, ConcreteSyn
       }
     }
 
-    protected override ConcreteSyntaxTree CreateWhileLoop(out ConcreteSyntaxTree guardWriter, ConcreteSyntaxTree wr) {
+    protected override ConcreteSyntaxTree CreateWhileLoop(out ConcreteSyntaxTree guardWriter, out ConcreteSyntaxTree annotWriter, ConcreteSyntaxTree wr) {
       wr.Write("for ");
       guardWriter = wr.Fork();
       var wBody = wr.NewBlock("");
+      annotWriter = wr.Fork();
       return wBody;
     }
 
     protected override ConcreteSyntaxTree EmitForStmt(IToken tok, IVariable loopIndex, bool goingUp, string /*?*/ endVarName,
-      List<Statement> body, LList<Label> labels, ConcreteSyntaxTree wr) {
+      List<Statement> body, LList<Label> labels, out ConcreteSyntaxTree annotWriter, ConcreteSyntaxTree wr) {
 
       wr.Write($"for {loopIndex.CompileName} := ");
       var startWr = wr.Fork();
@@ -2109,6 +2110,7 @@ protected override ConcreteSyntaxTree EmitForStmt(IToken tok, IVariable loopInde
         }
       }
       bodyWr = EmitContinueLabel(labels, bodyWr);
+      annotWriter = bodyWr.Fork();
       TrStmtList(body, bodyWr);
 
       return startWr;

diff --git a/Source/DafnyCore/Backends/Java/JavaCodeGenerator.cs b/Source/DafnyCore/Backends/Java/JavaCodeGenerator.cs
@@ -3823,7 +3823,7 @@ protected override ConcreteSyntaxTree CreateForLoop(string indexVar, Action<Conc
     }
 
     protected override ConcreteSyntaxTree EmitForStmt(IToken tok, IVariable loopIndex, bool goingUp, string /*?*/ endVarName,
-      List<Statement> body, LList<Label> labels, ConcreteSyntaxTree wr) {
+      List<Statement> body, LList<Label> labels, out ConcreteSyntaxTree annotWriter, ConcreteSyntaxTree wr) {
 
       var nativeType = AsNativeType(loopIndex.Type);
 
@@ -3865,6 +3865,7 @@ protected override ConcreteSyntaxTree EmitForStmt(IToken tok, IVariable loopInde
         }
       }
       bodyWr = EmitContinueLabel(labels, bodyWr);
+      annotWriter = bodyWr.Fork();
       TrStmtList(body, bodyWr);
 
       return startWr;

diff --git a/Source/DafnyCore/Backends/JavaScript/JavaScriptCodeGenerator.cs b/Source/DafnyCore/Backends/JavaScript/JavaScriptCodeGenerator.cs
@@ -1242,7 +1242,7 @@ protected override void EmitHalt(IToken tok, Expression/*?*/ messageExpr, Concre
     }
 
     protected override ConcreteSyntaxTree EmitForStmt(IToken tok, IVariable loopIndex, bool goingUp, string /*?*/ endVarName,
-      List<Statement> body, LList<Label> labels, ConcreteSyntaxTree wr) {
+      List<Statement> body, LList<Label> labels, out ConcreteSyntaxTree annotWriter, ConcreteSyntaxTree wr) {
 
       var nativeType = AsNativeType(loopIndex.Type);
 
@@ -1280,6 +1280,7 @@ protected override ConcreteSyntaxTree EmitForStmt(IToken tok, IVariable loopInde
         }
       }
       bodyWr = EmitContinueLabel(labels, bodyWr);
+      annotWriter = bodyWr.Fork();
       TrStmtList(body, bodyWr);
 
       return startWr;