Herbrand.hs

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

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

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

import Data.Foldable ( toList )

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

import HyLo.Model ( Model, ModelsRel(..), model )

import HyLo.Signature ( HasSignature(..), Signature, merge,
                        nomSymbols, delNomFromSig )

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