Use axiom instead of variable for globals, consts

Source/Provers/LeanAuto/LeanAutoGenerator.cs

@@ -18,8 +18,6 @@ public class LeanAutoGenerator : ReadOnlyVisitor
 {
   private readonly TextWriter writer;
   private readonly VCGenOptions options;
-  private readonly List<NamedDeclaration> globalVars = new();
-  private readonly HashSet<string> usedNames = new();
   private bool usesMaps;
   private readonly List<string> mapAxiomNames =
     new(new[]
@@ -216,7 +214,6 @@ public override ReturnCmd VisitReturnCmd(ReturnCmd node)
   public override Expr VisitIdentifierExpr(IdentifierExpr node)
   {
     var name = SanitizeNameForLean(node.Name);
-    usedNames.Add(name);
     WriteText(name);
     return node;
   }
@@ -279,13 +276,13 @@ public override Type VisitBvType(BvType node)
   public override Constant VisitConstant(Constant node)
   {
     var ti = node.TypedIdent;
-    WriteText("variable ");
-    Visit(ti);
+    var name = SanitizeNameForLean(ti.Name);
+    WriteText($"axiom {name} : ");
+    Visit(ti.Type);
     if (node.Unique) {
       AddUniqueConst(ti.Type, Name(node));
     }
     WriteLine();
-    globalVars.Add(node);
     return node;
   }
 
@@ -340,10 +337,8 @@ public override QuantifierExpr VisitQuantifierExpr(QuantifierExpr node)
 
   public override TypedIdent VisitTypedIdent(TypedIdent node)
   {
-    WriteText("(");
     var name = SanitizeNameForLean(node.Name);
-    WriteText(name);
-    WriteText(" : ");
+    WriteText($"( {name} : ");
     Visit(node.Type);
     WriteText(")");
     return node;
@@ -385,10 +380,11 @@ public override Expr VisitLetExpr(LetExpr node)
 
   public override GlobalVariable VisitGlobalVariable(GlobalVariable node)
   {
-    WriteText("variable ");
-    Visit(node.TypedIdent);
+    var ti = node.TypedIdent;
+    var name = SanitizeNameForLean(ti.Name);
+    WriteText($"axiom {name} : ");
+    Visit(ti.Type);
     WriteLine();
-    globalVars.Add(node);
     return node;
   }
 
@@ -822,7 +818,6 @@ public override Implementation VisitImplementation(Implementation node)
     var name = Name(node);
     var entryLabel = BlockName(node.Blocks[0]);
 
-    usedNames.Clear(); // Skip any globals used only by axioms, etc.
     WriteLine();
     WriteLine($"namespace impl_{name}");
     WriteLine();
@@ -837,8 +832,7 @@ public override Implementation VisitImplementation(Implementation node)
     WriteLine($"theorem {name}_correct");
     WriteParams(node);
     var paramNames =
-      globalVars.Select(Name).Where(x => usedNames.Contains(x))
-        .Concat(node.InParams.Select(Name))
+        node.InParams.Select(Name)
         .Concat(node.OutParams.Select(Name))
         .Concat(node.LocVars.Select(Name));
     var paramString = String.Join(' ', paramNames);
@@ -852,7 +846,6 @@ public override Implementation VisitImplementation(Implementation node)
     WriteLine($"end impl_{name}");
 
     usesMaps = false; // Skip map axioms in the next implementation if it doesn't need them
-    usedNames.Clear(); // Skip any globals not used by the next implementation
 
     return node;
   }

Test/lean-auto/lean-tests

@@ -1,3 +1,13 @@
+../extractloops/detLoopExtract.bpl
+../extractloops/detLoopExtractNested.bpl
+../extractloops/t1.bpl
+../extractloops/t2.bpl
+../inline/expansion4.bpl
+../inline/inline_n_0.bpl
+../inline/test1.bpl
+../inline/test2.bpl
+../inline/test3.bpl
+../inline/test6.bpl
 ../textbook/TuringFactorial.bpl
 ../textbook/DutchFlag.bpl
 ../textbook/Bubble.bpl