feat(Python): Support caching const variables

Source/DafnyCore/Backends/Python/PythonCodeGenerator.cs

@@ -148,6 +148,8 @@ private void EmitImports(string moduleName, string pythonModuleName, ConcreteSyn
       wr.WriteLine("from typing import Callable, Any, TypeVar, NamedTuple");
       wr.WriteLine("from math import floor");
       wr.WriteLine("from itertools import count");
+      // If (cacheConstVariablesCliFlag):
+      wr.WriteLine("from functools import lru_cache");
       wr.WriteLine();
       // Don't emit `import module_` for generated modules in the DafnyRuntimePython.
       // The DafnyRuntimePython doesn't have a module.py file, so the import isn't valid.
@@ -563,7 +565,7 @@ public ConcreteSyntaxTree CreateFunction(string name, List<TypeArgumentInstantia
 
       public ConcreteSyntaxTree CreateGetter(string name, TopLevelDecl enclosingDecl, Type resultType, IOrigin tok,
           bool isStatic, bool isConst, bool createBody, MemberDecl member, bool forBodyInheritance) {
-        return Compiler.CreateGetter(name, resultType, tok, isStatic, createBody, MethodWriter);
+        return Compiler.CreateGetter(name, resultType, tok, isStatic, isConst, createBody, MethodWriter);
       }
 
       public ConcreteSyntaxTree CreateGetterSetter(string name, Type resultType, IOrigin tok,
@@ -617,9 +619,17 @@ private ConcreteSyntaxTree CreateGetterSetter(string name, bool createBody, out
       return null;
     }
 
-    private ConcreteSyntaxTree CreateGetter(string name, Type resultType, IOrigin tok, bool isStatic, bool createBody, ConcreteSyntaxTree methodWriter) {
+    private ConcreteSyntaxTree CreateGetter(string name, Type resultType, IOrigin tok, bool isStatic, bool isConst, bool createBody, ConcreteSyntaxTree methodWriter) {
       if (!createBody) { return null; }
       methodWriter.WriteLine(isStatic ? $"@{DafnyRuntimeModule}.classproperty" : "@property");
+      // if (isConst and cacheConstVariablesCliFlag)
+      if (isConst) {
+        // maxsize's value represents the number of unique inputs to the function whose outputs are cached.
+        // Setting this to 1 means that only 1 input/output pair is cached.
+        // Since const methods only take `self` or `instance` and no other parameters, there is only 1 input/output pair.
+        // maxsize can be fixed to 1.
+        methodWriter.WriteLine("@lru_cache(maxsize=1)");
+      }
       return methodWriter.NewBlockPy(header: $"def {name}({(isStatic ? "instance" : "self")}):");
     }
 

Source/DafnyRuntime/DafnyRuntimePython/System_/__init__.py

@@ -2,6 +2,7 @@
 from typing import Callable, Any, TypeVar, NamedTuple
 from math import floor
 from itertools import count
+from functools import lru_cache
 
 import _dafny as _dafny