Python progress - getting the file picked up at least

robin-aws · Nov 15, 2023 · 29206be · 29206be
1 parent ac6fe4e
commit 29206be
Show file tree

Hide file tree

Showing 15 changed files with 39 additions and 6 deletions.
diff --git a/Source/DafnyCore/AST/ShouldCompileOrVerify.cs b/Source/DafnyCore/AST/ShouldCompileOrVerify.cs
@@ -24,6 +24,14 @@ public static bool ShouldCompile(this ModuleDefinition module, CompilationData p
       // https://github.com/dafny-lang/dafny/issues/4009
       return true;
     }
+
+    if (program.Options.Backend?.TargetId != "lib") {
+      bool compileIt = true;
+      if (Attributes.ContainsBool(module.Attributes, "compile", ref compileIt) && !compileIt) {
+        return false;
+      }
+    }
+
     return program.UrisToCompile.Contains(module.Tok.Uri);
   }
 

diff --git a/Source/DafnyCore/Compilers/Python/Compiler-python.cs b/Source/DafnyCore/Compilers/Python/Compiler-python.cs
@@ -62,6 +62,9 @@ protected override void EmitHeader(Program program, ConcreteSyntaxTree wr) {
       if (Options.IncludeRuntime) {
         EmitRuntimeSource("DafnyRuntimePython", wr);
       }
+      if (Options.Get(CommonOptionBag.UseStandardLibraries)) {
+        EmitRuntimeSource("DafnyStandardLibraries_py", wr);
+      }
 
       Imports.Add(DafnyRuntimeModule);
       EmitImports(null, wr);

diff --git a/Source/DafnyPipeline/DafnyPipeline.csproj b/Source/DafnyPipeline/DafnyPipeline.csproj
@@ -72,6 +72,10 @@
       <LinkBase>DafnyStandardLibraries_go</LinkBase>
       <CopyToOutputDirectory>Always</CopyToOutputDirectory>
     </EmbeddedResource>
+    <EmbeddedResource Include="..\DafnyStandardLibraries\src\**\*.py">
+      <LinkBase>DafnyStandardLibraries_py</LinkBase>
+      <CopyToOutputDirectory>Always</CopyToOutputDirectory>
+    </EmbeddedResource>
 
     <EmbeddedResource Include="..\DafnyStandardLibraries\binaries\DafnyStandardLibraries.doo">
       <LogicalName>DafnyStandardLibraries.doo</LogicalName>

diff --git a/Source/DafnyStandardLibraries/binaries/DafnyStandardLibraries-arithmetic.doo b/Source/DafnyStandardLibraries/binaries/DafnyStandardLibraries-arithmetic.doo
diff --git a/Source/DafnyStandardLibraries/binaries/DafnyStandardLibraries-cs.doo b/Source/DafnyStandardLibraries/binaries/DafnyStandardLibraries-cs.doo
diff --git a/Source/DafnyStandardLibraries/binaries/DafnyStandardLibraries-go.doo b/Source/DafnyStandardLibraries/binaries/DafnyStandardLibraries-go.doo
diff --git a/Source/DafnyStandardLibraries/binaries/DafnyStandardLibraries-java.doo b/Source/DafnyStandardLibraries/binaries/DafnyStandardLibraries-java.doo
diff --git a/Source/DafnyStandardLibraries/binaries/DafnyStandardLibraries-js.doo b/Source/DafnyStandardLibraries/binaries/DafnyStandardLibraries-js.doo
diff --git a/Source/DafnyStandardLibraries/binaries/DafnyStandardLibraries-notarget.doo b/Source/DafnyStandardLibraries/binaries/DafnyStandardLibraries-notarget.doo
diff --git a/Source/DafnyStandardLibraries/binaries/DafnyStandardLibraries-py.doo b/Source/DafnyStandardLibraries/binaries/DafnyStandardLibraries-py.doo
diff --git a/Source/DafnyStandardLibraries/binaries/DafnyStandardLibraries.doo b/Source/DafnyStandardLibraries/binaries/DafnyStandardLibraries.doo
diff --git a/.../FileIO/FileIO-notarget-java-cs-js-go.dfy → ...leIO/FileIO-notarget-java-cs-js-go-py.dfy b/.../FileIO/FileIO-notarget-java-cs-js-go.dfy → ...leIO/FileIO-notarget-java-cs-js-go-py.dfy
diff --git a/Source/DafnyStandardLibraries/src/DafnyStdLibs/FileIO/FileIO-py.dfy b/Source/DafnyStandardLibraries/src/DafnyStdLibs/FileIO/FileIO-py.dfy
diff --git a/Source/DafnyStandardLibraries/src/DafnyStdLibs/FileIO/FileIOInternalExterns-py.dfy b/Source/DafnyStandardLibraries/src/DafnyStdLibs/FileIO/FileIOInternalExterns-py.dfy
@@ -0,0 +1,19 @@
+/*******************************************************************************
+ *  Copyright by the contributors to the Dafny Project
+ *  SPDX-License-Identifier: MIT
+ *******************************************************************************/
+
+/*
+ * Private API - these are intentionally not exported from the module and should not be used elsewhere
+ */
+module {:compile false} DafnyStdLibs.FileIOInternalExterns {
+  method
+    {:extern}
+  INTERNAL_ReadBytesFromFile(path: string)
+    returns (isError: bool, bytesRead: seq<bv8>, errorMsg: string)
+
+  method
+    {:extern}
+  INTERNAL_WriteBytesToFile(path: string, bytes: seq<bv8>)
+    returns (isError: bool, errorMsg: string)
+}
diff --git a/Source/DafnyStandardLibraries/src/DafnyStdLibs_FileIOInternalExterns.py b/Source/DafnyStandardLibraries/src/DafnyStdLibs_FileIOInternalExterns.py
@@ -0,0 +1,5 @@
+# Module: DafnyStdLibs_FileIOInternalExterns
+
+@staticmethod
+def INTERNAL_ReadBytesFromFile(i):
+  return i * i