Skip to content

PySpec local import support and API consolidation #651

New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Draft
joehendrix wants to merge 1 commit into
base: main
Choose a base branch
from
Draft

PySpec local import support and API consolidation #651

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
1 commit
Select commit
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
177 changes: 1 addition & 176 deletions Strata/SimpleAPI.lean
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -14,9 +14,7 @@ import Strata.Transform.ProcedureInlining
public import Strata.Languages.Core.Options
public import Strata.Languages.Core.Verifier
import Strata.Languages.Laurel.LaurelToCoreTranslator
public import Strata.Languages.Python.PySpecPipeline
import Strata.Languages.Python.Specs
import Strata.Languages.Python.Specs.DDM
public import Strata.SimpleAPI.Python

/-! ## Simple Strata API

Expand Down Expand Up @@ -54,8 +52,6 @@ namespace Strata

public section

open Strata.Python.Specs (ModuleName)

/-! ### File I/O -/

/--
Expand Down Expand Up @@ -224,175 +220,4 @@ def Core.verifyProgram
| .none => IO.FS.withTempDir runVerification
IO.toEIO (fun e => s!"{e}") ioAction

/-- Controls how translation warnings are reported. -/
inductive WarningOutput where
/-- Suppress all warning output. -/
| none
/-- Print only a count summary (e.g., "3 warning(s)"). -/
| summary
/-- Print each warning followed by a count summary. -/
| detail
deriving Inhabited, BEq

/-- Recursively discover all Python modules under a directory.
Returns `(moduleName, filePath)` pairs. The `components` array
accumulates directory names as we recurse, forming the dotted
module name prefix. -/
private partial def discoverModules (sourceDir : System.FilePath)
: IO (Array (ModuleName × System.FilePath)) := do
let rec go (dir : System.FilePath) (components : Array String)
: IO (Array (ModuleName × System.FilePath)) := do
let mut acc := #[]
let entries ← dir.readDir
for entry in entries do
if ← entry.path.isDir then
acc := acc ++ (← go entry.path (components.push entry.fileName))
else if entry.fileName.endsWith ".py" then
let parts :=
if entry.fileName == "__init__.py" then
components
else
components.push (entry.fileName.takeWhile (· != '.') |>.toString)
if parts.isEmpty then continue
let dotted := ".".intercalate parts.toList
match ModuleName.ofString dotted with
| .ok mod => acc := acc.push (mod, entry.path)
| .error msg =>
let _ ← IO.eprintln s!"warning: skipping {entry.path}: {msg}" |>.toBaseIO
return acc
go sourceDir #[]

/-- Derive the output path for a Python file by mirroring the source directory
structure and replacing `.py` with `.pyspec.st.ion`. -/
def pySpecOutputPath (sourceDir strataDir pythonFile : System.FilePath)
: Option System.FilePath :=
let sourceDirStr := sourceDir.toString
let srcPrefix := if sourceDirStr.endsWith "/" then sourceDirStr else sourceDirStr ++ "/"
let fileStr := pythonFile.toString
let relStr := (fileStr.dropPrefix srcPrefix).toString
if relStr == fileStr then
none -- pythonFile not under sourceDir
else
let outName := if relStr.endsWith ".py"
then (relStr.take (relStr.length - 3)).toString ++ ".pyspec.st.ion"
else relStr ++ ".pyspec.st.ion"
some (strataDir / outName)

/-- Translate all (or selected) Python modules in a directory to PySpec Ion format.
If `modules` is empty, discovers and translates all `.py` files under `sourceDir`.
If `modules` is non-empty, translates only the named modules. -/
def pySpecsDir (sourceDir strataDir dialectFile : System.FilePath)
(modules : Array String := #[])
(events : Std.HashSet String := {})
(skipNames : Array String := #[])
(warningOutput : WarningOutput := .detail)
: EIO String Unit := do
-- Create output dir
match ← IO.FS.createDirAll strataDir |>.toBaseIO with
| .ok () => pure ()
| .error e => throw s!"Could not create {strataDir}: {e}"

-- Build skip identifiers
let skipIdents := skipNames.foldl (init := {}) fun acc s =>
match Python.PythonIdent.ofString s with
| some id => acc.insert id
| none => acc -- Unqualified skip names can't be resolved without a module context

-- Determine which modules to process
let modulesToProcess : Array (ModuleName × System.FilePath) ←
if modules.isEmpty then
match ← discoverModules sourceDir |>.toBaseIO with
| .ok r => pure r
| .error e => throw s!"Could not discover modules: {e}"
else
let mut result := #[]
for m in modules do
let mod ← match ModuleName.ofString m with
| .ok r => pure r
| .error e => throw s!"Invalid module name '{m}': {e}"
let (path, _) ←
match ← ModuleName.findInPath mod sourceDir |>.toBaseIO with
| .ok r => pure r
| .error e => throw s!"Module '{m}' not found in {sourceDir}: {e}"
result := result.push (mod, path)
pure result

-- Translate each module
let mut failures : Array (String × String) := #[]
for (mod, pythonFile) in modulesToProcess do
-- Derive output path
let some outPath := pySpecOutputPath sourceDir strataDir pythonFile
| do failures := failures.push (toString mod, s!"Could not derive output path for {pythonFile}")
continue

let .ok pythonMd ← pythonFile.metadata |>.toBaseIO
| do failures := failures.push (toString mod, s!"Could not find {pythonFile}")
continue

-- Timestamp check: skip if output is newer than source
if ← Python.Specs.isNewer outPath pythonMd then
Python.Specs.baseLogEvent events "import" s!"Skipping {mod} (up to date)"
continue

-- Ensure output subdirectory exists
if let some parent := outPath.parent then
match ← IO.FS.createDirAll parent |>.toBaseIO with
| .ok () => pure ()
| .error e =>
failures := failures.push (toString mod, s!"Could not create directory: {e}")
continue

-- Translate
Python.Specs.baseLogEvent events "import" s!"Translating {mod}"
match ← Strata.Python.Specs.translateFile
dialectFile strataDir pythonFile sourceDir
(events := events) (skipNames := skipIdents)
(moduleName := mod) |>.toBaseIO with
| .error msg =>
Python.Specs.baseLogEvent events "import" s!"Failed {mod}: {msg}"
failures := failures.push (toString mod, msg)
| .ok (sigs, warnings) =>
-- Write output
match ← Strata.Python.Specs.writeDDM outPath sigs |>.toBaseIO with
| .ok () => pure ()
| .error e =>
failures := failures.push (toString mod, s!"Could not write {outPath}: {e}")
continue
-- Report warnings per module
if warnings.size > 0 then
match warningOutput with
| .none => pure ()
| .summary =>
let _ ← IO.eprintln s!"{toString mod}: {warnings.size} warning(s)" |>.toBaseIO
| .detail =>
for w in warnings do
let _ ← IO.eprintln s!"{toString mod}: warning: {w}" |>.toBaseIO

-- Report failures
if failures.size > 0 then
let mut msg := s!"{failures.size} module(s) failed to translate:\n"
for (modName, err) in failures do
msg := msg ++ s!" {modName}: {err}\n"
throw msg

/-! ### Python-to-Core via Laurel pipeline -/

/-- Translate a Python Ion file all the way to Core. Composes
`pyAnalyzeLaurel` (Python → combined Laurel) and
`translateCombinedLaurel` (Laurel → Core with prelude). -/
def pyTranslateLaurel
(pythonIonPath : String)
(dispatchModules : Array String := #[])
(pyspecModules : Array String := #[])
(specDir : System.FilePath := ".")
: EIO String (Core.Program × List DiagnosticModel) := do
let laurel ←
match ← pyAnalyzeLaurel pythonIonPath dispatchModules pyspecModules (specDir := specDir) |>.toBaseIO with
| .ok r => pure r
| .error err => throw (toString err)
let (coreOption, laurelTranslateErrors) := translateCombinedLaurel laurel
match coreOption with
| none => throw s!"Laurel to Core translation failed: {laurelTranslateErrors}"
| some core => pure (core, laurelTranslateErrors)

end -- public section
Loading
Loading