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
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)]