module Theory.Constraint.System.Guarded (
Guarded(..)
, LGuarded
, LNGuarded
, GAtom(..)
, gfalse
, gtrue
, gdisj
, gconj
, gex
, gall
, gnot
, ginduct
, formulaToGuarded
, formulaToGuarded_
, simplifyGuarded
, mapGuardedAtoms
, atomToGAtom
, sortGAtoms
, isConjunction
, isDisjunction
, isAllGuarded
, isExGuarded
, isSafetyFormula
, guardFactTags
, bvarToLVar
, openGuarded
, substBound
, substBoundAtom
, substFree
, substFreeAtom
, prettyGuarded
) where
import Control.Applicative
import Control.Arrow
import Control.DeepSeq
import Control.Monad.Error
import Control.Monad.Fresh (MonadFresh, scopeFreshness)
import qualified Control.Monad.Trans.PreciseFresh as Precise (Fresh, evalFresh, evalFreshT)
import Debug.Trace
import Data.Binary
import Data.DeriveTH
import Data.Either (partitionEithers)
import Data.Foldable (Foldable(..), foldMap)
import Data.List
import qualified Data.DList as D
import Data.Monoid (Monoid(..))
import Data.Traversable hiding (mapM, sequence)
import Logic.Connectives
import Text.PrettyPrint.Highlight
import Theory.Model
data Guarded s c v = GAto (Atom (VTerm c (BVar v)))
| GDisj (Disj (Guarded s c v))
| GConj (Conj (Guarded s c v))
| GGuarded Quantifier [s] [Atom (VTerm c (BVar v))] (Guarded s c v)
deriving (Eq, Ord, Show)
isConjunction :: Guarded s c v -> Bool
isConjunction (GConj _) = True
isConjunction _ = False
isDisjunction :: Guarded s c v -> Bool
isDisjunction (GDisj _) = True
isDisjunction _ = False
isExGuarded :: Guarded s c v -> Bool
isExGuarded (GGuarded Ex _ _ _) = True
isExGuarded _ = False
isAllGuarded :: Guarded s c v -> Bool
isAllGuarded (GGuarded All _ _ _) = True
isAllGuarded _ = False
isSafetyFormula :: HasFrees (Guarded s c v) => Guarded s c v -> Bool
isSafetyFormula gf0 =
null (frees [gf0]) && noExistential gf0
where
noExistential (GAto _ ) = True
noExistential (GGuarded Ex _ _ _) = False
noExistential (GGuarded All _ _ gf) = noExistential gf
noExistential (GDisj disj) = all noExistential $ getDisj disj
noExistential (GConj conj) = all noExistential $ getConj conj
guardFactTags :: Guarded s c v -> [FactTag]
guardFactTags =
D.toList .
foldGuarded mempty (mconcat . getDisj) (mconcat . getConj) getTags
where
getTags _qua _ss atos inner =
mconcat [ D.singleton tag | Action _ (Fact tag _) <- atos ] <> inner
data GAtom t = GEqE (t,t) | GAction (t,Fact t)
deriving (Eq, Show, Ord)
isGAction :: GAtom t -> Bool
isGAction (GAction _) = True
isGAction _ = False
atomToGAtom :: Show t => Atom t -> GAtom t
atomToGAtom = conv
where conv (EqE s t) = GEqE (s,t)
conv (Action i f) = GAction (i,f)
conv a = error $ "atomsToGAtom: "++ show a
++ "is not a guarded atom."
sortGAtoms :: [GAtom t] -> [GAtom t]
sortGAtoms = uncurry (++) . partition isGAction
foldGuarded :: (Atom (VTerm c (BVar v)) -> b)
-> (Disj b -> b)
-> (Conj b -> b)
-> (Quantifier -> [s] -> [Atom (VTerm c (BVar v))] -> b -> b)
-> Guarded s c v
-> b
foldGuarded fAto fDisj fConj fGuarded =
go
where
go (GAto a) = fAto a
go (GDisj disj) = fDisj $ fmap go disj
go (GConj conj) = fConj $ fmap go conj
go (GGuarded qua ss as gf) = fGuarded qua ss as (go gf)
foldGuardedScope :: (Integer -> Atom (VTerm c (BVar v)) -> b)
-> (Disj b -> b)
-> (Conj b -> b)
-> (Quantifier -> [s] -> Integer -> [Atom (VTerm c (BVar v))] -> b -> b)
-> Guarded s c v
-> b
foldGuardedScope fAto fDisj fConj fGuarded =
go 0
where
go !i (GAto a) = fAto i a
go !i (GDisj disj) = fDisj $ fmap (go i) disj
go !i (GConj conj) = fConj $ fmap (go i) conj
go !i (GGuarded qua ss as gf) =
fGuarded qua ss i' as (go i' gf)
where
i' = i + fromIntegral (length ss)
mapGuardedAtoms :: (Integer -> Atom (VTerm c (BVar v))
-> Atom (VTerm d (BVar w)))
-> Guarded s c v
-> Guarded s d w
mapGuardedAtoms f =
foldGuardedScope (\i a -> GAto $ f i a) GDisj GConj
(\qua ss i as gf -> GGuarded qua ss (map (f i) as) gf)
instance Foldable (Guarded s c) where
foldMap f = foldGuarded (foldMap (foldMap (foldMap (foldMap f))))
(mconcat . getDisj)
(mconcat . getConj)
(\_qua _ss as b -> foldMap (foldMap (foldMap (foldMap (foldMap f)))) as `mappend` b)
traverseGuarded :: (Applicative f, Ord c, Ord v, Ord a)
=> (a -> f v) -> Guarded s c a -> f (Guarded s c v)
traverseGuarded f = foldGuarded (liftA GAto . traverse (traverseTerm (traverse (traverse f))))
(liftA GDisj . sequenceA)
(liftA GConj . sequenceA)
(\qua ss as gf -> GGuarded qua ss <$> traverse (traverse (traverseTerm (traverse (traverse f)))) as <*> gf)
instance Ord c => HasFrees (Guarded (String, LSort) c LVar) where
foldFrees f = foldMap (foldFrees f)
foldFreesOcc _ _ = const mempty
mapFrees f = traverseGuarded (mapFrees f)
type LGuarded c = Guarded (String, LSort) c LVar
substBoundAtom :: Ord c => [(Integer,LVar)] -> Atom (VTerm c (BVar LVar)) -> Atom (VTerm c (BVar LVar))
substBoundAtom s = fmap (fmapTerm (fmap subst))
where subst bv@(Bound i') = case lookup i' s of
Just x -> Free x
Nothing -> bv
subst fv = fv
substBound :: Ord c => [(Integer,LVar)] -> LGuarded c -> LGuarded c
substBound s = mapGuardedAtoms (\j a -> substBoundAtom [(i+j,v) | (i,v) <- s] a)
substFreeAtom :: Ord c
=> [(LVar,Integer)]
-> Atom (VTerm c (BVar LVar)) -> Atom (VTerm c (BVar LVar))
substFreeAtom s = fmap (fmapTerm (fmap subst))
where subst fv@(Free x) = case lookup x s of
Just i -> Bound i
Nothing -> fv
subst bv = bv
substFree :: Ord c => [(LVar,Integer)] -> LGuarded c -> LGuarded c
substFree s = mapGuardedAtoms (\j a -> substFreeAtom [(v,i+j) | (v,i) <- s] a)
bvarToLVar :: Ord c => Atom (VTerm c (BVar LVar)) -> Atom (VTerm c LVar)
bvarToLVar =
fmap (fmapTerm (fmap (foldBVar boundError id)))
where
boundError v = error $ "bvarToLVar: left-over bound variable '"
++ show v ++ "'"
unbindAtom :: (Ord c, Ord v) => Atom (VTerm c (BVar v)) -> Maybe (Atom (VTerm c v))
unbindAtom = traverse (traverseTerm (traverse (foldBVar (const Nothing) Just)))
openGuarded :: (Ord c, MonadFresh m)
=> LGuarded c -> m (Maybe (Quantifier, [LVar], [Atom (VTerm c LVar)], LGuarded c))
openGuarded (GGuarded qua vs as gf) = do
xs <- mapM (\(n,s) -> freshLVar n s) vs
return $ Just (qua, xs, openas xs, opengf xs)
where
openas xs = map (bvarToLVar . substBoundAtom (subst xs)) as
opengf xs = substBound (subst xs) gf
subst xs = zip [0..] (reverse xs)
openGuarded _ = return Nothing
closeGuarded :: Ord c => Quantifier -> [LVar] -> [Atom (VTerm c LVar)]
-> LGuarded c -> LGuarded c
closeGuarded qua vs as gf =
(case qua of Ex -> gex; All -> gall) vs' as' gf'
where
as' = map (substFreeAtom s . fmap (fmapTerm (fmap Free))) as
gf' = substFree s gf
s = zip (reverse vs) [0..]
vs' = map (lvarName &&& lvarSort) vs
type LNGuarded = Guarded (String,LSort) Name LVar
instance Apply LNGuarded where
apply subst = mapGuardedAtoms (const $ apply subst)
gtf :: Bool -> Guarded s c v
gtf False = GDisj (Disj [])
gtf True = GConj (Conj [])
gfalse :: Guarded s c v
gfalse = gtf False
gtrue :: Guarded s c v
gtrue = gtf True
gnotAtom :: Atom (VTerm c (BVar v)) -> Guarded s c v
gnotAtom a = GGuarded All [] [a] gfalse
gconj :: (Ord s, Ord c, Ord v) => [Guarded s c v] -> Guarded s c v
gconj gfs0 = case concatMap flatten gfs0 of
[gf] -> gf
gfs | any (gfalse ==) gfs -> gfalse
| otherwise -> GConj $ Conj $ nub gfs
where
flatten (GConj conj) = concatMap flatten $ getConj conj
flatten gf = [gf]
gdisj :: (Ord s, Ord c, Ord v) => [Guarded s c v] -> Guarded s c v
gdisj gfs0 = case concatMap flatten gfs0 of
[gf] -> gf
gfs | any (gtrue ==) gfs -> gtrue
| otherwise -> GDisj $ Disj $ nub gfs
where
flatten (GDisj disj) = concatMap flatten $ getDisj disj
flatten gf = [gf]
gex :: (Ord s, Ord c, Ord v)
=> [s] -> [Atom (VTerm c (BVar v))] -> Guarded s c v -> Guarded s c v
gex [] as gf = gconj (map GAto as ++ [gf])
gex _ _ gf | gf == gfalse = gfalse
gex ss as gf = GGuarded Ex ss as gf
gall :: (Eq s, Eq c, Eq v)
=> [s] -> [Atom (VTerm c (BVar v))] -> Guarded s c v -> Guarded s c v
gall _ [] gf = gf
gall _ _ gf | gf == gtrue = gtrue
gall ss atos gf = GGuarded All ss atos gf
newtype ErrorDoc d = ErrorDoc { unErrorDoc :: d }
deriving( Monoid, NFData, Document, HighlightDocument )
instance Document d => Error (ErrorDoc d) where
noMsg = emptyDoc
strMsg = text
formulaToGuarded_ :: LNFormula -> LNGuarded
formulaToGuarded_ = either (error . render) id . formulaToGuarded
formulaToGuarded :: HighlightDocument d => LNFormula -> Either d LNGuarded
formulaToGuarded fmOrig =
either (Left . ppError . unErrorDoc) Right
$ Precise.evalFreshT (convert False fmOrig) (avoidPrecise fmOrig)
where
ppFormula :: HighlightDocument a => LNFormula -> a
ppFormula = nest 2 . doubleQuotes . prettyLNFormula
ppError d = d $-$ text "in the formula" $-$ ppFormula fmOrig
convert True (Ato a) = pure $ gnotAtom a
convert False (Ato a) = pure $ GAto a
convert polarity (Not f) = convert (not polarity) f
convert True (Conn And f g) = gdisj <$> mapM (convert True) [f, g]
convert False (Conn And f g) = gconj <$> mapM (convert False) [f, g]
convert True (Conn Or f g) = gconj <$> mapM (convert True) [f, g]
convert False (Conn Or f g) = gdisj <$> mapM (convert False) [f, g]
convert True (Conn Imp f g ) =
gconj <$> sequence [convert False f, convert True g]
convert False (Conn Imp f g ) =
gdisj <$> sequence [convert True f, convert False g]
convert polarity (TF b) = pure $ gtf (polarity /= b)
convert polarity f0@(Qua qua0 _ _) =
case (qua0, polarity) of
(All, True ) -> convAll Ex
(All, False) -> convAll All
(Ex, True ) -> convEx All
(Ex, False) -> convEx Ex
where
noUnguardedVars [] = return ()
noUnguardedVars unguarded = throwError $ vcat
[ fsep $ text "unguarded variable(s)"
: (punctuate comma $
map (quotes . text . show) unguarded)
++ map text ["in", "the", "subformula"]
, ppFormula f0
]
conjActionsEqs (Conn And f1 f2) = conjActionsEqs f1 ++ conjActionsEqs f2
conjActionsEqs (Ato a@(Action _ _)) = [Left $ bvarToLVar a]
conjActionsEqs (Ato e@(EqE _ _)) = [Left $ bvarToLVar e]
conjActionsEqs f = [Right f]
remainingUnguarded ug0 atoms =
go ug0 (sortGAtoms . map atomToGAtom $ atoms)
where go ug [] = ug
go ug ((GAction a) :gatoms) = go (ug \\ frees a) gatoms
go ug ((GEqE (s,t)):gatoms) = go ug' gatoms
where ug' | covered s ug = ug \\ frees t
| covered t ug = ug \\ frees s
| otherwise = ug
covered a vs = frees a `intersect` vs == []
convEx qua = do
(xs,_,f) <- openFormulaPrefix f0
let (as_eqs, fs) = partitionEithers $ conjActionsEqs f
noUnguardedVars (remainingUnguarded xs as_eqs)
gf <- (if polarity then gdisj else gconj)
<$> mapM (convert polarity) fs
return $ closeGuarded qua xs (as_eqs) gf
convAll qua = do
(xs,_,f) <- openFormulaPrefix f0
case f of
Conn Imp ante suc -> do
let (as_eqs, fs) = partitionEithers $ conjActionsEqs ante
noUnguardedVars (remainingUnguarded xs (as_eqs))
gf <- (if polarity then gconj else gdisj)
<$> sequence ( map (convert (not polarity)) fs ++
[convert polarity suc] )
return $ closeGuarded qua xs as_eqs gf
_ -> throwError $
text "universal quantifier without toplevel implication" $-$
ppFormula f0
convert polarity (Conn Iff f1 f2) =
gconj <$> mapM (convert polarity) [Conn Imp f1 f2, Conn Imp f2 f1]
gnot :: (Ord s, Ord c, Ord v)
=> Guarded s c v -> Guarded s c v
gnot =
go
where
go (GGuarded All ss as gf) = gex ss as $ go gf
go (GGuarded Ex ss as gf) = gall ss as $ go gf
go (GAto ato) = gnotAtom ato
go (GDisj disj) = gconj $ map go (getDisj disj)
go (GConj conj) = gdisj $ map go (getConj conj)
satisfiedByEmptyTrace :: Guarded s c v -> Either String Bool
satisfiedByEmptyTrace =
foldGuarded
(\_ato -> throwError "atom outside the scope of a quantifier")
(liftM or . sequence . getDisj)
(liftM and . sequence . getConj)
(\qua _ss _as _gf -> return $ qua == All)
toInductionHypothesis :: Ord c => LGuarded c -> Either String (LGuarded c)
toInductionHypothesis =
go
where
go (GGuarded qua ss as gf)
| any isLastAtom as = throwError "formula not last-free"
| otherwise = do
gf' <- go gf
return $ case qua of
All -> gex ss as (gconj $ (gnotAtom <$> lastAtos) ++ [gf'])
Ex -> gall ss as (gdisj $ (GAto <$> lastAtos) ++ [gf'])
where
lastAtos :: [Atom (VTerm c (BVar LVar))]
lastAtos = do
(j, (_, LSortNode)) <- zip [0..] $ reverse ss
return $ Last (varTerm (Bound j))
go (GAto (Less i j)) = return $ gdisj [GAto (EqE i j), GAto (Less j i)]
go (GAto (Last _)) = throwError "formula not last-free"
go (GAto ato) = return $ gnotAtom ato
go (GDisj disj) = gconj <$> traverse go (getDisj disj)
go (GConj conj) = gdisj <$> traverse go (getConj conj)
ginduct :: Ord c => LGuarded c -> Either String (LGuarded c, LGuarded c)
ginduct gf = do
unless (null $ frees gf) (throwError "formula not closed")
unless (containsAction gf) (throwError "formula contains no action atom")
baseCase <- satisfiedByEmptyTrace gf
gfIH <- toInductionHypothesis gf
return (gtf baseCase, gconj [gf, gfIH])
where
containsAction = foldGuarded (const True) (or . getDisj) (or . getConj)
(\_ _ as body -> not (null as) || body)
simplifyGuarded :: (LNAtom -> Maybe Bool)
-> LNGuarded
-> Maybe LNGuarded
simplifyGuarded valuation fm0
| fm1 /= fm0 = trace (render ppMsg) (Just fm1)
| otherwise = Nothing
where
ppFm = nest 2 . doubleQuotes . prettyGuarded
ppMsg = nest 2 $ text "simplified formula:" $-$
nest 2 (vcat [ ppFm fm0, text "to", ppFm fm1])
fm1 = simp fm0
simp fm@(GAto ato) = maybe fm gtf (valuation =<< unbindAtom ato)
simp (GDisj fms) = gdisj $ map simp $ getDisj fms
simp (GConj fms) = gconj $ map simp $ getConj fms
simp (GGuarded All [] atos gf)
| any ((Just False ==) . snd) annAtos = gtrue
| otherwise =
gall [] (fst <$> filter ((Nothing ==) . snd) annAtos) (simp gf)
where
annAtos = (\x -> (x, valuation =<< unbindAtom x)) <$> atos
simp fm@(GGuarded _ _ _ _) = fm
prettyGuarded :: HighlightDocument d
=> LNGuarded
-> d
prettyGuarded fm =
Precise.evalFresh (pp fm) (avoidPrecise fm)
where
pp :: HighlightDocument d => LNGuarded -> Precise.Fresh d
pp (GAto a) = return $ prettyNAtom $ bvarToLVar a
pp (GDisj (Disj [])) = return $ operator_ "⊥"
pp (GDisj (Disj xs)) = do
ps <- mapM (\x -> opParens <$> pp x) xs
return $ sep $ punctuate (operator_ " ∨") ps
pp (GConj (Conj [])) = return $ operator_ "⊤"
pp (GConj (Conj xs)) = do
ps <- mapM (\x -> opParens <$> pp x) xs
return $ sep $ punctuate (operator_ " ∧") ps
pp gf0@(GGuarded _ _ _ _) =
scopeFreshness $ do
Just (qua, vs, atoms, gf) <- openGuarded gf0
let antecedent = (GAto . fmap (fmapTerm (fmap Free))) <$> atoms
connective = operator_ (case qua of All -> "⇒"; Ex -> "∧")
quantifier = operator_ (ppQuant qua) <-> ppVars vs <> operator_ "."
dante <- nest 1 <$> pp (GConj (Conj antecedent))
case (qua, vs, gf) of
(Ex, _, GConj (Conj [])) ->
return $ sep $ [ quantifier, dante ]
(All, [], GDisj (Disj [])) | gf == gfalse ->
return $ operator_ "¬" <> dante
_ -> do
dsucc <- nest 1 <$> pp gf
return $ sep [ quantifier, sep [dante, connective, dsucc] ]
where
ppVars = fsep . map (text . show)
ppQuant All = "∀"
ppQuant Ex = "∃"
$( derive makeBinary ''Guarded)
$( derive makeNFData ''Guarded)