module HyLo.Model.Herbrand( HerbrandModel, herbrand, inducedModel,
                            expand, removeWorld,
                            unit_tests )
where

import Test.QuickCheck ( Arbitrary(..), Property, (==>) )
import HyLo.Test       ( UnitTest, runTest )

import Data.Set ( Set )
import qualified Data.Set as Set

import Data.Map ( Map )
import qualified Data.Map as Map

import Data.Foldable ( Foldable, foldMap, toList )

import Text.Read ( Read(..), get, lift )
import Text.ParserCombinators.ReadP ( skipSpaces )

import HyLo.Formula ( Formula(At, Nom, Prop, Diam) )

import HyLo.Model ( Model, ModelsRel(..), model, equiv )
import qualified HyLo.Model as M

import HyLo.Signature ( HasSignature(..), Signature, merge,
                        nomSymbols, delNomFromSig )
import HyLo.Signature.Simple ( NomSymbol, PropSymbol, RelSymbol )

data HerbrandModel n p r where
    H :: (Ord n, Ord p, Ord r)
      => Set (n,n)
      -> Set (n,p)
      -> Set (n,r,n)
      -> Maybe (Signature n p r)
      -> HerbrandModel n p r

herbrand :: (Ord n, Ord p, Ord r)
         => Set (n,n)
         -> Set (n,p)
         -> Set (n,r,n)
         -> HerbrandModel n p r
herbrand es ps rs = H es ps rs Nothing

instance (Ord r, Ord n, Ord p, ModelsRel (Model n n p r, n) f n p r)
      => ModelsRel (HerbrandModel n p r, n) f n p r where
    (m,w) |= f = (inducedModel m, w) |= f

instance (Ord r, Ord n, Ord p, ModelsRel (Model n n p r)  f n p r)
      => ModelsRel (HerbrandModel n p r) f n p r where
    m |= f = (inducedModel m) |= f

instance (Ord r, Ord n, Ord p) => HasSignature (HerbrandModel n p r) where
    type NomsOf  (HerbrandModel n p r) = n
    type PropsOf (HerbrandModel n p r) = p
    type RelsOf  (HerbrandModel n p r) = r
    getSignature = getSignature . inducedModel

inducedModel :: (Ord r, Ord n, Ord p) => HerbrandModel n p r -> Model n n p r
inducedModel (H es ps rs expS) = model w rel vp vn s
    where s   = maybe id merge expS $ getSig es ps rs
          vn  = repr (foldr addEquiv emptyMF $ toList es)
          vp  = map (\(i,p)   -> (p,vn i))      . toList $ ps
          rel = map (\(i,r,j) -> (vn i,r,vn j)) . toList $ rs
          w   = Set.map vn (nomSymbols s)

getSig :: (Ord n, Ord p, Ord r)
       => Set (n,n)
       -> Set (n,p)
       -> Set (n,r,n)
       -> Signature n p r
getSig es ps rs = foldMap sigFromEqs es `merge`
                  foldMap sigFromPrs ps `merge`
                  foldMap sigFromRls rs
  where sigFromEqs (i,j)   = getSignature $ At i (Nom j)
        sigFromPrs (i,p)   = getSignature $ At i (Prop p)
        sigFromRls (i,r,j) = getSignature $ At i (Diam r $ Nom j)

expand :: (Ord n, Ord p, Ord r)
       => Signature n p r
       -> HerbrandModel n p r
       -> HerbrandModel n p r
expand s (H es ps rs Nothing)   = H es ps rs (Just s)
expand s (H es ps rs (Just s')) = H es ps rs (Just $ s `merge` s')

removeWorld :: (Ord n, Ord p, Ord r)
            => n
            -> HerbrandModel n p r
            -> HerbrandModel n p r
removeWorld n (H ns ps rs s) = H ns' ps' rs' (Just $ delNomFromSig n s')
  where (ns', nout) = Set.partition (\(i,j)   -> n /= i && n /= j) ns
        (ps', pout) = Set.partition (\(i,_)   -> n/= i) ps
        (rs', rout) = Set.partition (\(i,_,j) -> n /= i && n /= j) rs
        s' = maybe id merge s $ getSig nout pout rout

newtype MF a = MF{unMF :: Map a a} deriving Show

emptyMF :: MF a
emptyMF = MF Map.empty

repr :: Ord a => MF a -> a -> a
repr mf a = maybe a (repr mf) (Map.lookup a $ unMF mf)

addEquiv :: Ord a => (a,a) -> MF a -> MF a
addEquiv (a,b) mf@(MF m) = case compare a b of
                             EQ -> mf
                             LT -> addOrd b a
                             GT -> addOrd a b
    where addOrd x y = case Map.lookup x m of
                         Nothing -> MF (Map.insert x y m)
                         Just z  -> addEquiv (repr mf y, repr mf z) mf

-- -----------------------
-- QuickCheck stuff
-- -----------------------

instance (Arbitrary n, Arbitrary p, Arbitrary r, Ord n, Ord p, Ord r)
      => Arbitrary (HerbrandModel n p r) where
    arbitrary = do es <- arbitrary
                   ps <- arbitrary
                   rs <- arbitrary
                   s  <- arbitrary
                   return $ H es ps rs s
    coarbitrary (H es ps rs s) = coarbitrary (Set.size es) .
                                 coarbitrary (Set.size ps) .
                                 coarbitrary (Set.size rs) .
                                 coarbitrary s

instance (Show n, Show p, Show r) => Show (HerbrandModel n p r) where
    show (H ns pr rs s) = unwords ["H", show ns, show pr, show rs, show s]

instance (Read n, Read p, Read r, Ord n, Ord p, Ord r)
      => Read (HerbrandModel n p r) where
    readPrec = do 'H' <- get
                  blanks
                  ns <- readPrec
                  blanks
                  ps <- readPrec
                  blanks
                  rs <- readPrec
                  blanks
                  s  <- readPrec
                  return $ H ns ps rs s
        where blanks = lift skipSpaces


type TestHerbrandModel = HerbrandModel NomSymbol PropSymbol RelSymbol

prop_sets_are_true :: Set (NomSymbol, NomSymbol)
                   -> Set (NomSymbol, PropSymbol)
                   -> Set (NomSymbol, RelSymbol, NomSymbol)
                   -> Bool
prop_sets_are_true es ps rs =
    and $ [m |= At i (Nom j)          | (i,j)   <- Set.toList es] ++
          [m |= At i (Prop p)         | (i,p)   <- Set.toList ps] ++
          [m |= At i (Diam r $ Nom j) | (i,r,j) <- Set.toList rs]
  where m = herbrand es ps rs


prop_expandAlmostCommutes :: TestHerbrandModel
                          -> Signature NomSymbol PropSymbol RelSymbol
                          -> Property
prop_expandAlmostCommutes h s = Set.null (nomSymbols s) ==>
                  inducedModel (expand s h) `equiv` M.expand s (inducedModel h)


prop_readShow :: TestHerbrandModel -> Bool
prop_readShow h = inducedModel h `equiv` (inducedModel . read . show $ h)

unit_tests :: UnitTest
unit_tests = [
  ("read/show - HerbrandModel",           runTest prop_readShow),
  ("forms in sets are true",              runTest prop_sets_are_true),
  ("expand/inducedModel almost commutes", runTest prop_expandAlmostCommutes)]