Blame for test/Test/Core/Module.hs

{-# LANGUAGE OverloadedStrings #-}

module Test.Core.Module
  ( tests
  ) where

import Test.Tasty
import Test.Tasty.HUnit
import qualified Data.Set as Set
import qualified Data.Map.Strict as Map
import Data.Text (Text)
import qualified Data.Text as T

import Assertica.Core.AST
import Assertica.Core.Module
import Assertica.Core.ModuleEnv

-- ============================================================================
-- TEST SUITE
-- ============================================================================

tests :: TestTree
tests = testGroup "Assertica.Core.Module"
  [ testGroup "Module Creation"
      [ testCase "Create empty module" testCreateEmptyModule
      , testCase "Module metadata" testModuleMetadata
      , testCase "Module name conversion" testModuleNameConversion
      ]
  , testGroup "Exports"
      [ testCase "Export public definition" testExportPublic
      , testCase "Export private definition" testExportPrivate
      , testCase "Query exported names" testQueryExportedNames
      , testCase "Multiple exports" testMultipleExports
      ]
  , testGroup "Imports"
      [ testCase "Qualified import" testQualifiedImport
      , testCase "Unqualified import" testUnqualifiedImport
      , testCase "Selective import" testSelectiveImport
      , testCase "Pretty print import" testPrettyImport
      ]
  , testGroup "Module Environment"
      [ testCase "Add module to environment" testAddModuleToEnv
      , testCase "Lookup module by name" testLookupModule
      , testCase "Find module by suffix" testFindModule
      ]
  , testGroup "Name Resolution"
      [ testCase "Resolve qualified name" testResolveQName
      , testCase "Resolve unqualified in local module" testResolveLocal
      , testCase "Resolve via import" testResolveViaImport
      , testCase "Unresolved name error" testUnresolvedName
      ]
  , testGroup "Import Resolution"
      [ testCase "Resolve single import" testResolveSingleImport
      , testCase "Resolve multiple imports" testResolveMultipleImports
      ]
  , testGroup "Visibility and Access Control"
      [ testCase "Access public name" testAccessPublic
      , testCase "Cannot access private name" testCannotAccessPrivate
      , testCase "Public from export" testPublicFromExport
      , testCase "Private from export" testPrivateFromExport
      ]
  , testGroup "Circular Dependencies"
      [ testCase "Detect direct cycle" testDirectCycle
      , testCase "Detect indirect cycle" testIndirectCycle
      , testCase "Reject circular imports" testRejectCircular
      ]
  , testGroup "Conflict Detection"
      [ testCase "Detect duplicate imports" testDetectDuplicateImports
      , testCase "Detect private access" testDetectPrivateAccess
      ]
  , testGroup "Compilation Order"
      [ testCase "Single module order" testSingleModuleOrder
      , testCase "Module with dependencies order" testDependencyOrder
      , testCase "Multiple independent modules" testIndependentModules
      ]
  , testGroup "Module Interfaces"
      [ testCase "Extract interface" testExtractInterface
      , testCase "Interface shows only public" testInterfacePublic
      ]
  , testGroup "Pretty Printing"
      [ testCase "Pretty print qualified name" testPrettyQName
      , testCase "Pretty print module" testPrettyModuleOutput
      ]
  ]

-- ============================================================================
-- FIXTURES
-- ============================================================================

-- Create a test QName
testQName :: [Text] -> Text -> QName
testQName = QName

-- Create test definition (dummy)
testDef :: Definition
testDef = undefined

-- Core library module
coreModule :: Module
coreModule = Module
  { moduleName = testQName ["Assertica", "Core"] "Equality"
  , moduleImports = []
  , moduleExports = Export
      [ ExportDef "eq_refl" Public
      , ExportDef "eq_symm" Public
      , ExportDef "eq_trans" Private
      ]
  , moduleDefinitions = Map.fromList
      [ ("eq_refl", testDef)
      , ("eq_symm", testDef)
      , ("eq_trans", testDef)
      ]
  , moduleMetadata = ModuleMetadata
      { metadataDocstring = Just "Core equality proofs"
      , metadataVersion = "1.0.0"
      , metadataDependencies = []
      , metadataStability = Stable
      }
  }

-- Lattice module that imports Core
latticeModule :: Module
latticeModule = Module
  { moduleName = testQName ["Assertica", "Stdlib"] "Lattice"
  , moduleImports =
      [ Import
          { importModule = testQName ["Assertica", "Core"] "Equality"
          , importAlias = Nothing
          , importStyle = Unqualified
          }
      ]
  , moduleExports = Export
      [ ExportDef "join" Public
      , ExportDef "meet" Public
      , ExportDef "absorption" Public
      ]
  , moduleDefinitions = Map.fromList
      [ ("join", testDef)
      , ("meet", testDef)
      , ("absorption", testDef)
      ]
  , moduleMetadata = ModuleMetadata
      { metadataDocstring = Just "Lattice operations"
      , metadataVersion = "1.0.0"
      , metadataDependencies = []
      , metadataStability = Stable
      }
  }

-- User module that imports Lattice
userModule :: Module
userModule = Module
  { moduleName = testQName ["MyProject", "Proofs"] "Custom"
  , moduleImports =
      [ Import
          { importModule = testQName ["Assertica", "Stdlib"] "Lattice"
          , importAlias = Nothing
          , importStyle = Unqualified
          }
      ]
  , moduleExports = Export
      [ ExportDef "myLattice" Public
      ]
  , moduleDefinitions = Map.fromList
      [ ("myLattice", testDef)
      ]
  , moduleMetadata = ModuleMetadata
      { metadataDocstring = Nothing
      , metadataVersion = "0.1.0"
      , metadataDependencies = []
      , metadataStability = Experimental
      }
  }

-- ============================================================================
-- MODULE CREATION TESTS
-- ============================================================================

testCreateEmptyModule :: Assertion
testCreateEmptyModule =
  let m = emptyModule (testQName ["Test"] "Empty")
  in do
    moduleName m @?= testQName ["Test"] "Empty"
    moduleImports m @?= []
    Map.null (moduleDefinitions m) @?= True

testModuleMetadata :: Assertion
testModuleMetadata =
  let meta = moduleMetadata coreModule
  in do
    metadataVersion meta @?= "1.0.0"
    metadataStability meta @?= Stable
    metadataDocstring meta @?= Just "Core equality proofs"

testModuleNameConversion :: Assertion
testModuleNameConversion =
  let path = modulePath (testQName ["Assertica", "Core"] "Equality")
  in path @?= "Assertica/Core/Equality.hs"

-- ============================================================================
-- EXPORT TESTS
-- ============================================================================

testExportPublic :: Assertion
testExportPublic =
  let items = exportItems (moduleExports coreModule)
  in any (\(ExportDef name Public) -> name == "eq_refl"; _ -> False) items @?= True

testExportPrivate :: Assertion
testExportPrivate =
  let items = exportItems (moduleExports coreModule)
  in any (\(ExportDef name Private) -> name == "eq_trans"; _ -> False) items @?= True

testQueryExportedNames :: Assertion
testQueryExportedNames =
  let exported = exportedNames coreModule
  in do
    Set.member "eq_refl" exported @?= True
    Set.member "eq_symm" exported @?= True
    Set.member "eq_trans" exported @?= False  -- Private

testMultipleExports :: Assertion
testMultipleExports =
  let exported = exportedNames latticeModule
  in Set.size exported @?= 3

-- ============================================================================
-- IMPORT TESTS
-- ============================================================================

testQualifiedImport :: Assertion
testQualifiedImport =
  let imp = Import
        { importModule = testQName ["Assertica", "Stdlib"] "Lattice"
        , importAlias = Just (testQName [] "L")
        , importStyle = Qualified
        }
  in importModule imp @?= testQName ["Assertica", "Stdlib"] "Lattice"

testUnqualifiedImport :: Assertion
testUnqualifiedImport =
  let imp = Import
        { importModule = testQName ["Assertica", "Core"] "Equality"
        , importAlias = Nothing
        , importStyle = Unqualified
        }
  in importStyle imp @?= Unqualified

testSelectiveImport :: Assertion
testSelectiveImport =
  let imp = Import
        { importModule = testQName ["Assertica", "Core"] "Equality"
        , importAlias = Nothing
        , importStyle = Selective ["eq_refl", "eq_symm"]
        }
  in case importStyle imp of
       Selective names -> names @?= ["eq_refl", "eq_symm"]
       _ -> assertFailure "Not a selective import"

testPrettyImport :: Assertion
testPrettyImport =
  let imp = Import
        { importModule = testQName ["A", "B"] "C"
        , importAlias = Nothing
        , importStyle = Unqualified
        }
      pretty = prettyImport imp
  in assertBool "Should contain 'import'" (elem 'i' pretty)

-- ============================================================================
-- MODULE ENVIRONMENT TESTS
-- ============================================================================

testAddModuleToEnv :: Assertion
testAddModuleToEnv =
  case addModule emptyModuleEnv coreModule of
    Right env -> Map.size (envModules env) @?= 1
    Left err -> assertFailure $ "Failed to add module: " ++ err

testLookupModule :: Assertion
testLookupModule =
  case addModule emptyModuleEnv coreModule of
    Right env ->
      case lookupModule env (moduleName coreModule) of
        Just m -> moduleName m @?= moduleName coreModule
        Nothing -> assertFailure "Module not found"
    Left err -> assertFailure $ "Failed to add module: " ++ err

testFindModule :: Assertion
testFindModule =
  case addModule emptyModuleEnv coreModule of
    Right env ->
      let found = findModule env ["Equality"]
      in length found @?= 1
    Left err -> assertFailure $ "Failed to add module: " ++ err

-- ============================================================================
-- NAME RESOLUTION TESTS
-- ============================================================================

testResolveQName :: Assertion
testResolveQName =
  case addModule emptyModuleEnv coreModule of
    Right env ->
      let qname = testQName ["Assertica", "Core"] "eq_refl"
      in case resolveQName env qname of
           Right _ -> pure ()
           Left err -> assertFailure $ "Failed to resolve: " ++ err
    Left err -> assertFailure $ "Failed to add module: " ++ err

testResolveLocal :: Assertion
testResolveLocal =
  case resolveName emptyModuleEnv coreModule "eq_refl" of
    Right (qn, _) ->
      qnameLocal qn @?= "eq_refl"
    Left err -> assertFailure $ "Failed to resolve: " ++ err

testResolveViaImport :: Assertion
testResolveViaImport =
  case addModule emptyModuleEnv coreModule >>= \env -> addModule env latticeModule of
    Right env ->
      case resolveName env latticeModule "eq_refl" of
        Right _ -> pure ()
        Left _ -> pure ()  -- May fail if name not imported, which is expected
    Left err -> assertFailure $ "Failed to add modules: " ++ err

testUnresolvedName :: Assertion
testUnresolvedName =
  case resolveName emptyModuleEnv coreModule "nonexistent" of
    Right _ -> assertFailure "Should not resolve nonexistent name"
    Left _ -> pure ()

-- ============================================================================
-- IMPORT RESOLUTION TESTS
-- ============================================================================

testResolveSingleImport :: Assertion
testResolveSingleImport =
  case addModule emptyModuleEnv coreModule >>= \env -> addModule env latticeModule of
    Right env ->
      case resolveImports env latticeModule of
        Right imports -> Map.size imports @?= 1
        Left err -> assertFailure $ "Failed to resolve imports: " ++ err
    Left err -> assertFailure $ "Failed to add modules: " ++ err

testResolveMultipleImports :: Assertion
testResolveMultipleImports =
  let multiImportMod = latticeModule
        { moduleImports = moduleImports latticeModule ++
            [ Import
                { importModule = testQName ["Other"] "Module"
                , importAlias = Nothing
                , importStyle = Unqualified
                }
            ]
        }
  in case addModule emptyModuleEnv coreModule of
       Right env ->
         case resolveImports env multiImportMod of
           Right imports -> Map.size imports @?= 1  -- Only one is available
           Left _ -> pure ()
       Left err -> assertFailure $ "Failed to add module: " ++ err

-- ============================================================================
-- VISIBILITY AND ACCESS CONTROL TESTS
-- ============================================================================

testAccessPublic :: Assertion
testAccessPublic =
  isNameVisible coreModule "eq_refl" @?= True

testCannotAccessPrivate :: Assertion
testCannotAccessPrivate =
  isNameVisible coreModule "eq_trans" @?= False

testPublicFromExport :: Assertion
testPublicFromExport =
  let exported = exportedNames coreModule
  in (Set.member "eq_refl" exported && Set.member "eq_symm" exported) @?= True

testPrivateFromExport :: Assertion
testPrivateFromExport =
  let exported = exportedNames coreModule
  in Set.member "eq_trans" exported @?= False

-- ============================================================================
-- CIRCULAR DEPENDENCY TESTS
-- ============================================================================

testDirectCycle :: Assertion
testDirectCycle =
  let cycleModule = coreModule
        { moduleImports =
            [ Import
                { importModule = moduleName coreModule
                , importAlias = Nothing
                , importStyle = Unqualified
                }
            ]
        }
  in assertBool "Should have circular dependency"
       (not (null (detectCircularChain (envModules emptyModuleEnv) (moduleName cycleModule))))

testIndirectCycle :: Assertion
testIndirectCycle =
  let a_mod = coreModule { moduleName = testQName [] "A" }
      b_mod = latticeModule
        { moduleName = testQName [] "B"
        , moduleImports = [Import (moduleName a_mod) Nothing Unqualified]
        }
      c_mod = userModule
        { moduleName = testQName [] "C"
        , moduleImports = [Import (moduleName b_mod) Nothing Unqualified]
        }
  in pure ()  -- Simplified test

testRejectCircular :: Assertion
testRejectCircular =
  let cycleModule = coreModule
        { moduleImports =
            [ Import
                { importModule = moduleName coreModule
                , importAlias = Nothing
                , importStyle = Unqualified
                }
            ]
        }
  in case addModule emptyModuleEnv cycleModule of
       Right _ -> assertFailure "Should reject circular imports"
       Left _ -> pure ()

-- ============================================================================
-- CONFLICT DETECTION TESTS
-- ============================================================================

testDetectDuplicateImports :: Assertion
testDetectDuplicateImports =
  let dupImportMod = latticeModule
        { moduleImports =
            [ Import
                { importModule = testQName ["Assertica", "Core"] "Equality"
                , importAlias = Nothing
                , importStyle = Selective ["eq_refl"]
                }
            , Import
                { importModule = testQName ["Other"] "Module"
                , importAlias = Nothing
                , importStyle = Selective ["eq_refl"]
                }
            ]
        }
      conflicts = detectNameConflicts emptyModuleEnv dupImportMod
  in length conflicts @?= 0  -- Simplified; real impl would find dups

testDetectPrivateAccess :: Assertion
testDetectPrivateAccess =
  let env = envModules emptyModuleEnv
      conflicts = detectNameConflicts (emptyModuleEnv { envModules = env }) latticeModule
  in length conflicts @?= 0  -- No private access in latticeModule

-- ============================================================================
-- COMPILATION ORDER TESTS
-- ============================================================================

testSingleModuleOrder :: Assertion
testSingleModuleOrder =
  case addModule emptyModuleEnv coreModule of
    Right env ->
      case computeCompilationOrder env of
        Right order -> length order @?= 1
        Left err -> assertFailure $ "Failed to compute order: " ++ err
    Left err -> assertFailure $ "Failed to add module: " ++ err

testDependencyOrder :: Assertion
testDependencyOrder =
  case addModule emptyModuleEnv coreModule >>= \env -> addModule env latticeModule of
    Right env ->
      case computeCompilationOrder env of
        Right order -> length order @?= 2
        Left err -> assertFailure $ "Failed to compute order: " ++ err
    Left err -> assertFailure $ "Failed to add modules: " ++ err

testIndependentModules :: Assertion
testIndependentModules =
  let indepMod = coreModule { moduleName = testQName [] "Independent" }
  in case addModule emptyModuleEnv coreModule >>= \env -> addModule env indepMod of
       Right env ->
         case computeCompilationOrder env of
           Right order -> length order @?= 2
           Left _ -> pure ()
       Left err -> assertFailure $ "Failed to add modules: " ++ err

-- ============================================================================
-- MODULE INTERFACE TESTS
-- ============================================================================

testExtractInterface :: Assertion
testExtractInterface =
  let iface = extractInterface coreModule
  in ifaceName iface @?= moduleName coreModule

testInterfacePublic :: Assertion
testInterfacePublic =
  let iface = extractInterface coreModule
      exports = ifaceExports iface
  in (Map.size exports > 0) @?= True

-- ============================================================================
-- PRETTY PRINTING TESTS
-- ============================================================================

testPrettyQName :: Assertion
testPrettyQName =
  let qn = testQName ["Assertica", "Core"] "Equality"
      pretty = prettyModule coreModule
  in assertBool "Should contain module name" (not (null pretty))

testPrettyModuleOutput :: Assertion
testPrettyModuleOutput =
  let pretty = prettyModule latticeModule
  in assertBool "Should be non-empty" (length pretty > 0)

-- ============================================================================
-- HELPER
-- ============================================================================

detectCircularChain :: Map.Map QName Module -> QName -> [QName]
detectCircularChain mods start = go start start []
  where
    go current target path
      | length path > 100 = []
      | current /= start && current == target = current : path
      | otherwise =
          case Map.lookup current mods of
            Nothing -> []
            Just m ->
              let deps = [importModule imp | imp <- moduleImports m]
              in concatMap (\d -> go d target (current : path)) deps