-- | Explicit finite covers and overlap compatibility checks.
module Foundational.Descent
  ( FiniteCover (..)
  , LocalSection (..)
  , validCover
  , compatibleSections
  , genValidCover
  ) where

import Data.List (nub, sort)
import Test.QuickCheck (Gen, chooseInt)

-- | A universe together with finite patch sets. Patch-label order is ignored;
-- repeated labels inside a patch are malformed and rejected.
data FiniteCover = FiniteCover
  { coverUniverse :: [String]
  , coverPatches :: [[String]]
  }
  deriving (Eq, Show)

-- | Values assigned to every label of one declared patch.
data LocalSection value = LocalSection
  { sectionPatch :: [String]
  , sectionValues :: [(String, value)]
  }
  deriving (Eq, Show)

-- | Check that patches are distinct nonempty sets whose union is the universe.
validCover :: FiniteCover -> Bool
validCover (FiniteCover universe patches) =
  unique universe
    && not (null universe)
    && unique (map canonicalPatch patches)
    && not (null patches)
    && all validPatch patches
    && sort (nub (concat patches)) == sort universe
  where
    validPatch patch =
      unique patch
        && not (null patch)
        && all (`elem` universe) patch

-- | Check that one well-formed local section exists per patch and that values
-- agree on every overlapping label.
compatibleSections :: Eq value => FiniteCover -> [LocalSection value] -> Bool
compatibleSections cover sections =
  validCover cover
    && sort (map (canonicalPatch . sectionPatch) sections) == sort (map canonicalPatch (coverPatches cover))
    && all wellFormedSection sections
    && all labelsAgree (nub (concatMap (map fst . sectionValues) sections))
  where
    wellFormedSection section =
      sort (map fst (sectionValues section)) == sort (sectionPatch section)
        && unique (map fst (sectionValues section))
    labelsAgree label =
      allEqual [value | section <- sections, (name, value) <- sectionValues section, name == label]

canonicalPatch :: [String] -> [String]
canonicalPatch = sort

unique :: Eq value => [value] -> Bool
unique values = length values == length (nub values)

allEqual :: Eq value => [value] -> Bool
allEqual values = case values of
  [] -> True
  first : rest -> all (== first) rest

-- | Generate a complete finite cover with two distinct overlapping patches.
genValidCover :: Gen FiniteCover
genValidCover = do
  size <- chooseInt (3, 4)
  let universe = take size ["a", "b", "c", "d"]
  pure (FiniteCover universe [take (size - 1) universe, drop 1 universe])