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