Include some TODO comments

These all have issues, but these comments help make plans more immediately clear when browsing the code.
dafny-lang · Sep 13, 2022 · fff0d4f · fff0d4f
1 parent 475ed0f
commit fff0d4f
Show file tree

Hide file tree

Showing 5 changed files with 8 additions and 0 deletions.
diff --git a/src/AST/Syntax.dfy b/src/AST/Syntax.dfy
@@ -31,6 +31,7 @@ module Types {
     | Collection(finite: bool, kind: CollectionKind, eltType: Type)
     | Function(args: seq<Type>, ret: Type) // TODO
     | Class(classType: ClassType)
+    // TODO: change string to indicate C# class and include location
     | Unsupported(description: string)
   {
     // TODO: remove?
@@ -259,6 +260,7 @@ module Exprs {
     | Block(stmts: seq<Expr>)
     | Bind(vars: seq<string>, vals: seq<Expr>, body: Expr)
     | If(cond: Expr, thn: Expr, els: Expr) // DISCUSS: Lazy op node?
+    // TODO: change string to indicate C# class and include location
     | Unsupported(description: string, children: seq<Expr>)
   {
     function method Depth() : nat {

diff --git a/src/Passes/EliminateNegatedBinops.dfy b/src/Passes/EliminateNegatedBinops.dfy
@@ -254,12 +254,14 @@ module Bootstrap.Passes.EliminateNegatedBinops {
   function method Apply(p: Program) : (p': Program)
     requires Tr_Pre(p)
     ensures Tr_Post(p')
+    // TODO
     //ensures Tr_Expr_Rel(p.mainMethod.methodBody, p'.mainMethod.methodBody)
     // Apply the transformation to a program.
   {
     Deep.All_Expr_True_Forall(Tr_Expr.f.requires);
     assert Deep.All_Program(p, Tr_Expr.f.requires);
     TrPreservesRel();
+    // TODO
     //Map_Program_PreservesRel(p, Tr_Expr, Tr_Expr_Rel);
     Map_Program(p, Tr_Expr)
   }

diff --git a/src/Passes/SimplifyEmptyBlocks.dfy b/src/Passes/SimplifyEmptyBlocks.dfy
@@ -672,12 +672,14 @@ module Simplify {
   function method Apply(p: Program) : (p': Program)
     requires Tr_Pre(p)
     ensures Tr_Post(p')
+    // TODO
     //ensures Tr_Expr_Rel(p.mainMethod.methodBody, p'.mainMethod.methodBody)
     // Apply the transformation to a program.
   {
     Deep.All_Expr_True_Forall(Tr_Expr.f.requires);
     assert Deep.All_Program(p, Tr_Expr.f.requires);
     EqInterp_Lift(Tr_Expr.f);
+    // TODO
     //Map_Program_PreservesRel(p, Tr_Expr, Tr_Expr_Rel);
     Map_Program(p, Tr_Expr)
   }

diff --git a/src/Tools/Auditor/DafnyAuditor.csproj b/src/Tools/Auditor/DafnyAuditor.csproj
@@ -10,6 +10,7 @@
     <DAFNY_ROOT Condition="'$(DAFNY_ROOT)' == ''">..\..\..\..\</DAFNY_ROOT>
   </PropertyGroup>
 
+  <!-- TODO: get DafnyPipeline from NuGet when we can -->
   <ItemGroup>
     <ProjectReference Include="$(DAFNY_ROOT)\Source\Dafny\DafnyPipeline.csproj" />
     <Compile Include="..\..\Interop\CSharpInterop.cs" />

diff --git a/src/Transforms/BottomUp.dfy b/src/Transforms/BottomUp.dfy
@@ -312,6 +312,7 @@ module Bootstrap.Transforms.BottomUp {
     Shallow.Map_Program(p, Map_Expr_Transformer(tr))
   }
 
+  // TODO: prove
 /*
   lemma {:opaque} Map_Program_PreservesRel(p: Program, tr: BottomUpTransformer, rel: (Expr, Expr) -> bool)
     requires Deep.All_Program(p, tr.f.requires)