module Theory.Model.Fact (
Fact(..)
, Multiplicity(..)
, FactTag(..)
, matchFact
, isLinearFact
, isPersistentFact
, isProtoFact
, factTagName
, showFactTag
, showFactTagArity
, factTagArity
, factTagMultiplicity
, factArity
, factMultiplicity
, DirTag(..)
, kuFact
, kdFact
, kFactView
, dedFactView
, isKFact
, isKUFact
, isKDFact
, freshFact
, outFact
, inFact
, kLogFact
, dedLogFact
, protoFact
, NFact
, LFact
, LNFact
, unifyLNFactEqs
, unifiableLNFacts
, prettyFact
, prettyNFact
, prettyLNFact
) where
import Control.Basics
import Control.DeepSeq
import Data.Binary
import Data.DeriveTH
import Data.Foldable (Foldable(..))
import Data.Generics
import Data.Maybe (isJust)
import Data.Monoid
import Data.Traversable (Traversable(..))
import Term.Unification
import Text.PrettyPrint.Class
data Multiplicity = Persistent | Linear
deriving( Eq, Ord, Show, Typeable, Data )
data FactTag = ProtoFact Multiplicity String Int
| FreshFact
| OutFact
| InFact
| KUFact
| KDFact
| DedFact
deriving( Eq, Ord, Show, Typeable, Data )
data Fact t = Fact
{ factTag :: FactTag
, factTerms :: [t]
}
deriving( Eq, Ord, Show, Typeable, Data )
instance Functor Fact where
fmap f (Fact tag ts) = Fact tag (fmap f ts)
instance Foldable Fact where
foldMap f (Fact _ ts) = foldMap f ts
instance Traversable Fact where
sequenceA (Fact tag ts) = Fact tag <$> sequenceA ts
traverse f (Fact tag ts) = Fact tag <$> traverse f ts
instance Sized t => Sized (Fact t) where
size (Fact _ args) = size args
instance HasFrees t => HasFrees (Fact t) where
foldFrees f = foldMap (foldFrees f)
foldFreesOcc f c fa = foldFreesOcc f ((show $ factTag fa):c) (factTerms fa)
mapFrees f = traverse (mapFrees f)
instance Apply t => Apply (Fact t) where
apply subst = fmap (apply subst)
data DirTag = UpK | DnK
deriving( Eq, Ord, Show )
kdFact, kuFact :: t -> Fact t
kdFact = Fact KDFact . return
kuFact = Fact KUFact . return
kFactView :: LNFact -> Maybe (DirTag, LNTerm)
kFactView fa = case fa of
Fact KUFact [m] -> Just (UpK, m)
Fact KUFact _ -> errMalformed "kFactView" fa
Fact KDFact [m] -> Just (DnK, m)
Fact KDFact _ -> errMalformed "kFactView" fa
_ -> Nothing
dedFactView :: LNFact -> Maybe LNTerm
dedFactView fa = case fa of
Fact DedFact [m] -> Just m
Fact DedFact _ -> errMalformed "dedFactView" fa
_ -> Nothing
isKFact :: LNFact -> Bool
isKFact = isJust . kFactView
isKUFact :: LNFact -> Bool
isKUFact (Fact KUFact _) = True
isKUFact _ = False
isKDFact :: LNFact -> Bool
isKDFact (Fact KDFact _) = True
isKDFact _ = False
errMalformed :: String -> LNFact -> a
errMalformed caller fa =
error $ caller ++ show ": malformed fact: " ++ show fa
outFact :: t -> Fact t
outFact = Fact OutFact . return
freshFact :: t -> Fact t
freshFact = Fact FreshFact . return
inFact :: t -> Fact t
inFact = Fact InFact . return
kLogFact :: t -> Fact t
kLogFact = protoFact Linear "K" . return
dedLogFact :: t -> Fact t
dedLogFact = Fact DedFact . return
protoFact :: Multiplicity -> String -> [t] -> Fact t
protoFact multi name ts = Fact (ProtoFact multi name (length ts)) ts
isProtoFact :: Fact t -> Bool
isProtoFact (Fact (ProtoFact _ _ _) _) = True
isProtoFact _ = False
isLinearFact :: Fact t -> Bool
isLinearFact = (Linear ==) . factMultiplicity
isPersistentFact :: Fact t -> Bool
isPersistentFact = (Persistent ==) . factMultiplicity
factTagMultiplicity :: FactTag -> Multiplicity
factTagMultiplicity tag = case tag of
ProtoFact multi _ _ -> multi
KUFact -> Persistent
KDFact -> Persistent
_ -> Linear
factTagArity :: FactTag -> Int
factTagArity tag = case tag of
ProtoFact _ _ k -> k
KUFact -> 1
KDFact -> 1
DedFact -> 1
FreshFact -> 1
InFact -> 1
OutFact -> 1
factArity :: Fact t -> Int
factArity (Fact tag ts)
| length ts == k = k
| otherwise = error $ "factArity: tag of arity " ++ show k ++
" applied to " ++ show (length ts) ++ " terms"
where
k = factTagArity tag
factMultiplicity :: Fact t -> Multiplicity
factMultiplicity = factTagMultiplicity . factTag
type NFact v = Fact (NTerm v)
type LFact c = Fact (LTerm c)
type LNFact = Fact LNTerm
unifyLNFactEqs :: [Equal LNFact] -> WithMaude [LNSubstVFresh]
unifyLNFactEqs eqs
| all (evalEqual . fmap factTag) eqs =
unifyLNTerm (map (fmap (fAppList . factTerms)) eqs)
| otherwise = return []
unifiableLNFacts :: LNFact -> LNFact -> WithMaude Bool
unifiableLNFacts fa1 fa2 = (not . null) <$> unifyLNFactEqs [Equal fa1 fa2]
matchFact :: Fact t
-> Fact t
-> Match t
matchFact t p =
matchOnlyIf (factTag t == factTag p &&
length (factTerms t) == length (factTerms p))
<> mconcat (zipWith matchWith (factTerms t) (factTerms p))
factTagName :: FactTag -> String
factTagName tag = case tag of
KUFact -> "KU"
KDFact -> "KD"
DedFact -> "Ded"
InFact -> "In"
OutFact -> "Out"
FreshFact -> "Fr"
(ProtoFact _ n _) -> n
showFactTag :: FactTag -> String
showFactTag tag =
(++ factTagName tag) $ case factTagMultiplicity tag of
Linear -> ""
Persistent -> "!"
showFactTagArity :: FactTag -> String
showFactTagArity tag = showFactTag tag ++ "/" ++ show (factTagArity tag)
prettyFact :: Document d => (t -> d) -> Fact t -> d
prettyFact ppTerm (Fact tag ts)
| factTagArity tag /= length ts = ppFact ("MALFORMED-" ++ show tag) ts
| otherwise = ppFact (showFactTag tag) ts
where
ppFact n = nestShort' (n ++ "(") ")" . fsep . punctuate comma . map ppTerm
prettyNFact :: Document d => LNFact -> d
prettyNFact = prettyFact prettyNTerm
prettyLNFact :: Document d => LNFact -> d
prettyLNFact fa = prettyFact prettyNTerm fa
$( derive makeBinary ''Multiplicity)
$( derive makeBinary ''FactTag)
$( derive makeBinary ''Fact)
$( derive makeNFData ''Multiplicity)
$( derive makeNFData ''FactTag)
$( derive makeNFData ''Fact)