Split SimpleAPI.lean across package boundaries#1216
Conversation
…PI.lean, use PipelinePhase, create PipelinePhase for IrrelevantAxiom, update StrataMainLib to use DDM.lean's readStrataProgram, etc
…CoreFactory creator for end user, minor comment move
|
Quite close to the final version - the types in APIs can be regarded as opaque types because APIs will provide the 'creators' of them. For example, users won't have to know what is the definition of Factory because |
…hon,Laurel}/API.lean into {Python,Laurel}/{Python,Laurel.lean}
…tually used by Core verifier
|
I think |
Some of the transformations are on pure Imperative programs (e.g., StructuredToUnstructured). This was under a design assumption that other languages will have been written using Imperative and Lambda. It's hard to decide whether Strata.Transform should be moved to Strata.Languages.Core.Transform or not. :/ |
Most of them are, but there are some transforms that should be moved under DL (e.g., StructuredToUnstructured). I think we should find appropriate homes for them and this can be done in this PR or in the one that creates the StrataCLI package. |
atomb
left a comment
There was a problem hiding this comment.
Just one key change to request: I'd like to avoid module names with duplication. I'd prefer Strata.Languages.Core.Core to be just Strata.Languages.Core
|
Let me fix the conflicts after recent updates..! |
…remove old Strata/DDM.lean and merge it into StrataDDM/StrataDDM.lean
Prepare for the repository split by aligning API boundaries with package boundaries. Each future package (StrataDDM, Strata, StrataPython, etc.) will expose only the API surface it owns, without requiring downstream packages to import the full SimpleAPI and its dependencies.
SimpleAPI.lean is now a thin re-export of the modules in:
Additional changes:
Core.runTransformsextracted to PipelinePhase.lean — the inline transform loop from Verifier.lean is now a standalone function onList PipelinePhase, with optional telemetry and debug-file output.Core.TransformPassinductive removed — replaced byCore.PipelinePhasevalues via openpass*constructors.readStrataProgramin StrataMainLib now delegates to Strata.readStrataText (DDM) instead of manually assembling dialect contexts.coreToGeneric(noncomputable opaque) → coreToStrataProgram — now implemented via CST round-trip.