| {-| | |
| Module : Assertica.Core.Module | |
| Description : Module system for proof library organization | |
| Copyright : (c) 2026 Ahmad Ali Parr | |
| License : BSL-1.0 | |
| The Module system provides namespace management, visibility control, and clean | |
| separation of concerns for large proof libraries. It enables: | |
| 1. **Namespaces**: Prevent name collisions across library and user code | |
| - Core library: Assertica.Core | |
| - Standard library: Assertica.Stdlib.Lattice | |
| - User code: MyProject.Proofs | |
| 2. **Visibility Control**: Public/private exports | |
| - Public definitions: Exported in module interface | |
| - Private definitions: Internal only | |
| 3. **Qualified Names**: Enable disambiguation | |
| - List.length vs Vector.length | |
| - Short forms via selective imports | |
| 4. **Deterministic Resolution**: No ambiguity in name lookups | |
| - Import order irrelevant | |
| - Explicit qualification always available | |
| 5. **Dependency Tracking**: Detect cycles and build order | |
| DESIGN PRINCIPLES: | |
| - Each module has clear exports and imports | |
| - Names are resolved deterministically | |
| - Circular dependencies are detected and rejected | |
| - Modules are first-class citizens in the type system | |
| - Interface extraction enables separate compilation | |
| -} | |
| module Assertica.Core.Module | |
| ( -- * Definitions | |
| Definition (..) | |
| -- * Module types | |
| , Module (..) | |
| , ModuleMetadata (..) | |
| , ModuleInterface (..) | |
| -- * Import types | |
| , Import (..) | |
| , ImportStyle (..) | |
| -- * Export types | |
| , Export (..) | |
| , ExportItem (..) | |
| -- * Visibility and stability | |
| , Visibility (..) | |
| , Stability (..) | |
| , Strength (..) | |
| -- * Dependency tracking | |
| , ModuleDependency (..) | |
| , ModuleGraph | |
| -- * Basic operations | |
| , emptyModule | |
| , modulePath | |
| , qualifyName | |
| , isCircularDependency | |
| , extractInterface | |
| , exportedNames | |
| , visibleNames | |
| , prettyModule | |
| , prettyImport | |
| , prettyExport | |
| ) where | |
| import Data.Text (Text) | |
| import qualified Data.Text as T | |
| import Data.Map.Strict (Map) | |
| import qualified Data.Map.Strict as Map | |
| import Data.Set (Set) | |
| import qualified Data.Set as Set | |
| import Data.List (intercalate) | |
| import GHC.Generics (Generic) | |
| import Data.Data (Data) | |
| import Data.Typeable (Typeable) | |
| import qualified Data.Graph as Graph | |
| import Data.Maybe (catMaybes, mapMaybe) | |
| import Assertica.Core.AST (QName(..), Term, Type, Proposition, Assertion) | |
| -- ============================================================================ | |
| -- DEFINITIONS | |
| -- ============================================================================ | |
| {-| A definition is any named entity in a module. | |
| Can be a type, function, assertion, or other named construct. | |
| -} | |
| data Definition | |
| = DefTerm Term -- ^ A term (function/value) | |
| | DefType Type -- ^ A type definition | |
| | DefAssertion Assertion -- ^ An assertion | |
| | DefOpaque String -- ^ An opaque definition (from external library) | |
| deriving (Eq, Show, Generic, Typeable, Data) | |
| -- ============================================================================ | |
| -- VISIBILITY AND EXPORTS | |
| -- ============================================================================ | |
| {-| Visibility of a definition within and outside its module. | |
| -} | |
| data Visibility | |
| = Public -- ^ Exported by the module, accessible externally | |
| | Private -- ^ Module-internal only, not accessible externally | |
| deriving (Eq, Ord, Show, Generic, Typeable, Data) | |
| {-| An item that can be exported from a module. | |
| -} | |
| data ExportItem | |
| = ExportDef Text Visibility -- ^ A definition (type, function, etc.) | |
| | ExportModule QName -- ^ Re-export all public items from another module | |
| deriving (Eq, Show, Generic, Typeable, Data) | |
| {-| Export list for a module. | |
| -} | |
| data Export = Export | |
| { exportItems :: [ExportItem] -- ^ What this module exports | |
| } | |
| deriving (Eq, Show, Generic, Typeable, Data) | |
| -- ============================================================================ | |
| -- IMPORTS | |
| -- ============================================================================ | |
| {-| How a module is imported. | |
| -} | |
| data ImportStyle | |
| = Qualified -- ^ import X as Y → only Y.name accessible | |
| | Unqualified -- ^ import X → names from X directly accessible | |
| | Selective [Text] -- ^ import X (foo, bar) → only foo, bar imported | |
| deriving (Eq, Show, Generic, Typeable, Data) | |
| {-| An import statement in a module. | |
| -} | |
| data Import = Import | |
| { importModule :: QName -- ^ The module being imported | |
| , importAlias :: Maybe QName -- ^ Optional alias (for qualified imports) | |
| , importStyle :: ImportStyle -- ^ How to import | |
| } | |
| deriving (Eq, Show, Generic, Typeable, Data) | |
| -- ============================================================================ | |
| -- DEPENDENCY TRACKING | |
| -- ============================================================================ | |
| {-| A dependency relationship between modules. | |
| -} | |
| data ModuleDependency = ModuleDependency | |
| { depModule :: QName -- ^ The depended-upon module | |
| , depStrength :: Strength -- ^ How strong the dependency is | |
| } | |
| deriving (Eq, Show, Generic, Typeable, Data) | |
| {-| Strength of a dependency. | |
| -} | |
| data Strength | |
| = Direct -- ^ Direct import | |
| | Transitive -- ^ Transitively imported | |
| deriving (Eq, Ord, Show, Generic, Typeable, Data) | |
| {-| A directed graph of modules and their dependencies. | |
| Enables cycle detection and topological sorting. | |
| -} | |
| type ModuleGraph = Map QName (Set QName) | |
| -- ============================================================================ | |
| -- MODULE METADATA | |
| -- ============================================================================ | |
| {-| Metadata about a module. | |
| -} | |
| data ModuleMetadata = ModuleMetadata | |
| { metadataDocstring :: Maybe String -- ^ Module documentation | |
| , metadataVersion :: String -- ^ Version (e.g., "1.0.0") | |
| , metadataDependencies :: [ModuleDependency] -- ^ Known dependencies | |
| , metadataStability :: Stability -- ^ Stability level | |
| } | |
| deriving (Eq, Show, Generic, Typeable, Data) | |
| {-| Stability level of a module. | |
| -} | |
| data Stability | |
| = Experimental -- ^ May change significantly | |
| | Stable -- ^ Unlikely to change | |
| | Deprecated -- ^ Use alternative instead | |
| deriving (Eq, Show, Generic, Typeable, Data) | |
| -- ============================================================================ | |
| -- MODULES | |
| -- ============================================================================ | |
| {-| A module is the unit of organization in Assertica. | |
| Modules contain definitions organized by namespaces. | |
| -} | |
| data Module = Module | |
| { moduleName :: QName -- ^ e.g., "Assertica.Stdlib.Lattice" | |
| , moduleImports :: [Import] -- ^ What this module imports | |
| , moduleExports :: Export -- ^ What this module exports | |
| , moduleDefinitions :: Map Text Definition -- ^ Definitions by name | |
| , moduleMetadata :: ModuleMetadata -- ^ Metadata | |
| } | |
| deriving (Eq, Show, Generic, Typeable, Data) | |
| -- ============================================================================ | |
| -- MODULE INTERFACE | |
| -- ============================================================================ | |
| {-| A module interface reveals only the public API. | |
| Enables separate compilation and type checking. | |
| -} | |
| data ModuleInterface = ModuleInterface | |
| { ifaceName :: QName -- ^ Module name | |
| , ifaceExports :: Map Text ExportItem -- ^ Exported items | |
| , ifaceDocstring :: Maybe String -- ^ Module documentation | |
| } | |
| deriving (Eq, Show, Generic, Typeable, Data) | |
| -- ============================================================================ | |
| -- BASIC OPERATIONS | |
| -- ============================================================================ | |
| {-| Create an empty module with defaults. | |
| -} | |
| emptyModule :: QName -> Module | |
| emptyModule name = Module | |
| { moduleName = name | |
| , moduleImports = [] | |
| , moduleExports = Export [] | |
| , moduleDefinitions = Map.empty | |
| , moduleMetadata = ModuleMetadata | |
| { metadataDocstring = Nothing | |
| , metadataVersion = "0.1.0" | |
| , metadataDependencies = [] | |
| , metadataStability = Experimental | |
| } | |
| } | |
| {-| Convert module name to file path. | |
| Example: QName ["Assertica", "Stdlib"] "Lattice" → "Assertica/Stdlib/Lattice.hs" | |
| -} | |
| modulePath :: QName -> FilePath | |
| modulePath (QName mod name) = | |
| intercalate "/" (map T.unpack (mod ++ [name])) ++ ".hs" | |
| {-| Qualify a name with the module's namespace. | |
| -} | |
| qualifyName :: Module -> Text -> QName | |
| qualifyName m name = QName (qnameModule (moduleName m)) name | |
| {-| Extract the public interface of a module. | |
| Only includes public exports, type signatures, and documentation. | |
| -} | |
| extractInterface :: Module -> ModuleInterface | |
| extractInterface m = ModuleInterface | |
| { ifaceName = moduleName m | |
| , ifaceExports = exportedItemsAsMap m | |
| , ifaceDocstring = metadataDocstring (moduleMetadata m) | |
| } | |
| where | |
| exportedItemsAsMap m = | |
| Map.fromList [(itemName item, item) | item <- exportItems (moduleExports m)] | |
| itemName (ExportDef name _) = name | |
| itemName (ExportModule _) = "" -- Re-exports handled separately | |
| {-| Get all names exported by a module. | |
| -} | |
| exportedNames :: Module -> Set Text | |
| exportedNames m = | |
| Set.fromList [name | ExportDef name Public <- exportItems (moduleExports m)] | |
| {-| Check if a name is visible in the module. | |
| A name is visible if it's defined and exported. | |
| -} | |
| visibleNames :: Module -> Set Text | |
| visibleNames m = exportedNames m | |
| {-| Check if a dependency would create a circular import. | |
| -} | |
| isCircularDependency :: ModuleGraph -> QName -> QName -> Bool | |
| isCircularDependency graph from to = | |
| case Map.lookup to graph of | |
| Nothing -> False | |
| Just deps -> Set.member from deps | |
| {-| Build a module dependency graph. | |
| -} | |
| buildModuleGraph :: [Module] -> ModuleGraph | |
| buildModuleGraph mods = | |
| Map.fromList [(moduleName m, directDependencies m) | m <- mods] | |
| where | |
| directDependencies m = | |
| Set.fromList [importModule imp | imp <- moduleImports m] | |
| {-| Detect cycles in the module dependency graph. | |
| Returns a list of cycles (each cycle is a list of modules forming a loop). | |
| -} | |
| detectCycles :: ModuleGraph -> [[QName]] | |
| detectCycles graph = | |
| let (scc, _) = stronglyConnected graph | |
| in filter (\cycle -> length cycle > 1 || any hasSelfLoop cycle) scc | |
| where | |
| hasSelfLoop (QName _ name) = | |
| case Map.lookup (QName [] name) graph of | |
| Nothing -> False | |
| Just deps -> Set.member (QName [] name) deps | |
| stronglyConnected _ = ([], id) -- Simplified; full Tarjan's algorithm would go here | |
| {-| Topologically sort modules by dependencies. | |
| Returns modules in order suitable for compilation (dependencies first). | |
| Fails if cycles are detected. | |
| -} | |
| topologicalSort :: [Module] -> Either String [Module] | |
| topologicalSort mods = | |
| let graph = buildModuleGraph mods | |
| cycles = detectCycles graph | |
| in if not (null cycles) | |
| then Left $ "Circular dependencies detected: " ++ show cycles | |
| else Right mods -- Simplified; real implementation would sort | |
| -- ============================================================================ | |
| -- PRETTY PRINTING | |
| -- ============================================================================ | |
| {-| Pretty-print an import statement. | |
| -} | |
| prettyImport :: Import -> String | |
| prettyImport imp = | |
| let modStr = prettyQName (importModule imp) | |
| styleStr = case importStyle imp of | |
| Qualified -> "" | |
| Unqualified -> "" | |
| Selective names -> " (" ++ intercalate ", " (map T.unpack names) ++ ")" | |
| aliasStr = case importAlias imp of | |
| Nothing -> "" | |
| Just alias -> " as " ++ prettyQName alias | |
| in "import " ++ modStr ++ aliasStr ++ styleStr | |
| {-| Pretty-print an export statement. | |
| -} | |
| prettyExport :: Export -> String | |
| prettyExport (Export items) = | |
| "(" ++ intercalate ", " (map prettyExportItem items) ++ ")" | |
| where | |
| prettyExportItem (ExportDef name vis) = | |
| T.unpack name ++ (if vis == Public then "" else " [private]") | |
| prettyExportItem (ExportModule m) = | |
| "module " ++ prettyQName m | |
| {-| Pretty-print a module definition. | |
| -} | |
| prettyModule :: Module -> String | |
| prettyModule m = | |
| "module " ++ prettyQName (moduleName m) ++ " where\n" ++ | |
| (if null (moduleImports m) then "" else unlines (map prettyImport (moduleImports m)) ++ "\n") ++ | |
| (if null (exportItems (moduleExports m)) then "" else "exports " ++ prettyExport (moduleExports m) ++ "\n") ++ | |
| "-- " ++ show (Map.size (moduleDefinitions m)) ++ " definitions" | |
| {-| Helper: pretty-print a qualified name. | |
| -} | |
| prettyQName :: QName -> String | |
| prettyQName (QName mod name) = | |
| intercalate "." (map T.unpack (mod ++ [name])) | |