module Theory.Proof (
LTree(..)
, mergeMapsWith
, ProofStep(..)
, Proof
, ProofPath
, atPath
, insertPaths
, mapProofInfo
, foldProof
, annotateProof
, ProofStatus(..)
, proofStepStatus
, sorry
, unproven
, IncrementalProof
, Prover
, runProver
, mapProverProof
, orelse
, tryProver
, sorryProver
, oneStepProver
, focus
, checkAndExtendProver
, replaceSorryProver
, contradictionProver
, SolutionExtractor(..)
, AutoProver(..)
, runAutoProver
, prettyProof
, prettyProofWith
, showProofStatus
, parLTreeDFS
, module Theory.Constraint.Solver
) where
import Data.Binary
import Data.DeriveTH
import Data.Foldable (Foldable, foldMap)
import Data.List
import qualified Data.Map as M
import Data.Maybe
import Data.Monoid
import Data.Traversable
import Debug.Trace
import Control.Basics
import Control.DeepSeq
import qualified Control.Monad.State as S
import Control.Parallel.Strategies
import Theory.Constraint.Solver
import Theory.Model
import Theory.Text.Pretty
data LTree l a = LNode
{ root :: a
, children :: M.Map l (LTree l a)
}
deriving( Eq, Ord, Show )
instance Functor (LTree l) where
fmap f (LNode r cs) = LNode (f r) (M.map (fmap f) cs)
instance Foldable (LTree l) where
foldMap f (LNode x cs) = f x `mappend` foldMap (foldMap f) cs
instance Traversable (LTree l) where
traverse f (LNode x cs) = LNode <$> f x <*> traverse (traverse f) cs
parLTreeDFS :: Strategy (LTree l a)
parLTreeDFS (LNode x0 cs0) = do
cs0' <- (`parTraversable` cs0) $ \(LNode x cs) -> LNode x <$> rseq cs
return $ LNode x0 (M.map (runEval . parLTreeDFS) cs0')
mergeMapsWith :: Ord k
=> (a -> c) -> (b -> c) -> (a -> b -> c)
-> M.Map k a -> M.Map k b -> M.Map k c
mergeMapsWith leftOnly rightOnly combine l r =
M.map extract $ M.unionWith combine' l' r'
where
l' = M.map (Left . Left) l
r' = M.map (Left . Right) r
combine' (Left (Left a)) (Left (Right b)) = Right $ combine a b
combine' _ _ = error "mergeMapsWith: impossible"
extract (Left (Left a)) = leftOnly a
extract (Left (Right b)) = rightOnly b
extract (Right c) = c
data ProofStep a = ProofStep
{ psMethod :: ProofMethod
, psInfo :: a
}
deriving( Eq, Ord, Show )
instance Functor ProofStep where
fmap f (ProofStep m i) = ProofStep m (f i)
instance Foldable ProofStep where
foldMap f = f . psInfo
instance Traversable ProofStep where
traverse f (ProofStep m i) = ProofStep m <$> f i
instance HasFrees a => HasFrees (ProofStep a) where
foldFrees f (ProofStep m i) = foldFrees f m `mappend` foldFrees f i
foldFreesOcc _ _ = const mempty
mapFrees f (ProofStep m i) = ProofStep <$> mapFrees f m <*> mapFrees f i
type ProofPath = [CaseName]
type Proof a = LTree CaseName (ProofStep a)
sorry :: Maybe String -> a -> Proof a
sorry reason ann = LNode (ProofStep (Sorry reason) ann) M.empty
unproven :: a -> Proof a
unproven = sorry Nothing
atPath :: Proof a -> ProofPath -> Maybe (Proof a)
atPath = foldM (flip M.lookup . children)
modifyAtPath :: (Proof a -> Maybe (Proof a)) -> ProofPath
-> Proof a -> Maybe (Proof a)
modifyAtPath f =
go
where
go [] prf = f prf
go (l:ls) prf = do
let cs = children prf
prf' <- go ls =<< M.lookup l cs
return (prf { children = M.insert l prf' cs })
insertPaths :: Proof a -> Proof (a, ProofPath)
insertPaths =
insertPath []
where
insertPath path (LNode ps cs) =
LNode (fmap (,reverse path) ps)
(M.mapWithKey (\n prf -> insertPath (n:path) prf) cs)
mapProofInfo :: (a -> b) -> Proof a -> Proof b
mapProofInfo = fmap . fmap
boundProofDepth :: Int -> Proof a -> Proof a
boundProofDepth bound =
go bound
where
go n (LNode ps@(ProofStep _ info) cs)
| 0 < n = LNode ps $ M.map (go (pred n)) cs
| otherwise = sorry (Just $ "bound " ++ show bound ++ " hit") info
foldProof :: Monoid m => (ProofStep a -> m) -> Proof a -> m
foldProof f =
go
where
go (LNode step cs) = f step `mappend` foldMap go (M.elems cs)
annotateProof :: (ProofStep a -> [b] -> b) -> Proof a -> Proof b
annotateProof f =
go
where
go (LNode step@(ProofStep method _) cs) =
LNode (ProofStep method info') cs'
where
cs' = M.map go cs
info' = f step (map (psInfo . root . snd) (M.toList cs'))
data ProofStatus =
UndeterminedProof
| CompleteProof
| IncompleteProof
| TraceFound
instance Monoid ProofStatus where
mempty = CompleteProof
mappend TraceFound _ = TraceFound
mappend _ TraceFound = TraceFound
mappend IncompleteProof _ = IncompleteProof
mappend _ IncompleteProof = IncompleteProof
mappend _ CompleteProof = CompleteProof
mappend CompleteProof _ = CompleteProof
mappend UndeterminedProof UndeterminedProof = UndeterminedProof
proofStepStatus :: ProofStep (Maybe a) -> ProofStatus
proofStepStatus (ProofStep _ Nothing ) = UndeterminedProof
proofStepStatus (ProofStep Solved (Just _)) = TraceFound
proofStepStatus (ProofStep (Sorry _) (Just _)) = IncompleteProof
proofStepStatus (ProofStep _ (Just _)) = CompleteProof
checkProof :: ProofContext
-> (Int -> System -> Proof (Maybe System))
-> Int
-> System
-> Proof a
-> Proof (Maybe a, Maybe System)
checkProof ctxt prover d sys prf@(LNode (ProofStep method info) cs) =
case (method, execProofMethod ctxt method sys) of
(Sorry reason, _ ) -> sorryNode reason cs
(_ , Just cases) -> node method $ checkChildren cases
(_ , Nothing ) ->
sorryNode (Just "invalid proof step encountered")
(M.singleton "" prf)
where
node m = LNode (ProofStep m (Just info, Just sys))
sorryNode reason cases = node (Sorry reason) (M.map noSystemPrf cases)
noSystemPrf = mapProofInfo (\i -> (Just i, Nothing))
checkChildren cases = mergeMapsWith
unhandledCase noSystemPrf (checkProof ctxt prover (d + 1)) cases cs
where
unhandledCase = mapProofInfo ((,) Nothing) . prover d
annotateWithSystems :: ProofContext -> System -> Proof () -> Proof System
annotateWithSystems ctxt =
go
where
go sysOrig (LNode (ProofStep method _) csOrig) =
LNode (ProofStep method sysOrig) $ M.fromList $ do
(name, prf) <- M.toList csOrig
let sysAnn = extract ("case '" ++ name ++ "' non-existent") $
M.lookup name csAnn
return (name, go sysAnn prf)
where
extract msg = fromMaybe (error $ "annotateWithSystems: " ++ msg)
csAnn = extract "proof method execution failed" $
execProofMethod ctxt method sysOrig
type IncrementalProof = Proof (Maybe System)
newtype Prover = Prover
{ runProver
:: ProofContext
-> Int
-> System
-> IncrementalProof
-> Maybe IncrementalProof
}
instance Monoid Prover where
mempty = Prover $ \_ _ _ -> Just
p1 `mappend` p2 = Prover $ \ctxt d se ->
runProver p1 ctxt d se >=> runProver p2 ctxt d se
mapProverProof :: (IncrementalProof -> IncrementalProof) -> Prover -> Prover
mapProverProof f p = Prover $ \ ctxt d se prf -> f <$> runProver p ctxt d se prf
failProver :: Prover
failProver = Prover (\ _ _ _ _ -> Nothing)
orelse :: Prover -> Prover -> Prover
orelse p1 p2 = Prover $ \ctxt d se prf ->
runProver p1 ctxt d se prf `mplus` runProver p2 ctxt d se prf
tryProver :: Prover -> Prover
tryProver = (`orelse` mempty)
oneStepProver :: ProofMethod -> Prover
oneStepProver method = Prover $ \ctxt _ se _ -> do
cases <- execProofMethod ctxt method se
return $ LNode (ProofStep method (Just se)) (M.map (unproven . Just) cases)
sorryProver :: Maybe String -> Prover
sorryProver reason = Prover $ \_ _ se _ -> return $ sorry reason (Just se)
focus :: ProofPath -> Prover -> Prover
focus [] prover = prover
focus path prover =
Prover $ \ctxt d _ prf ->
modifyAtPath (prover' ctxt (d + length path)) path prf
where
prover' ctxt d prf = do
se <- psInfo (root prf)
runProver prover ctxt d se prf
checkAndExtendProver :: Prover -> Prover
checkAndExtendProver prover0 = Prover $ \ctxt d se prf ->
return $ mapProofInfo snd $ checkProof ctxt (prover ctxt) d se prf
where
unhandledCase = sorry (Just "unhandled case") Nothing
prover ctxt d se =
fromMaybe unhandledCase $ runProver prover0 ctxt d se unhandledCase
replaceSorryProver :: Prover -> Prover
replaceSorryProver prover0 = Prover prover
where
prover ctxt d _ = return . replace
where
replace prf@(LNode (ProofStep (Sorry _) (Just se)) _) =
fromMaybe prf $ runProver prover0 ctxt d se prf
replace (LNode ps cases) =
LNode ps $ M.map replace cases
firstProver :: [Prover] -> Prover
firstProver = foldr orelse failProver
contradictionProver :: Prover
contradictionProver = Prover $ \ctxt d sys prf ->
runProver
(firstProver $ map oneStepProver $
(Contradiction . Just <$> contradictions ctxt sys))
ctxt d sys prf
data SolutionExtractor = CutDFS | CutBFS | CutNothing
deriving( Eq, Ord, Show, Read )
data AutoProver = AutoProver
{ apHeuristic :: Heuristic
, apBound :: Maybe Int
, apCut :: SolutionExtractor
}
runAutoProver :: AutoProver -> Prover
runAutoProver (AutoProver heuristic bound cut) =
mapProverProof cutSolved $ maybe id boundProver bound autoProver
where
cutSolved = case cut of
CutDFS -> cutOnSolvedDFS
CutBFS -> cutOnSolvedBFS
CutNothing -> id
autoProver :: Prover
autoProver = Prover $ \ctxt depth sys _ ->
return $ fmap (fmap Just)
$ annotateWithSystems ctxt sys
$ proveSystemDFS heuristic ctxt depth sys
boundProver :: Int -> Prover -> Prover
boundProver b p = Prover $ \ctxt d se prf ->
boundProofDepth b <$> runProver p ctxt d se prf
data IterDeepRes = NoSolution | MaybeNoSolution | Solution ProofPath
instance Monoid IterDeepRes where
mempty = NoSolution
x@(Solution _) `mappend` _ = x
_ `mappend` y@(Solution _) = y
MaybeNoSolution `mappend` _ = MaybeNoSolution
_ `mappend` MaybeNoSolution = MaybeNoSolution
NoSolution `mappend` NoSolution = NoSolution
cutOnSolvedDFS :: Proof (Maybe a) -> Proof (Maybe a)
cutOnSolvedDFS prf0 =
go (4 :: Integer) $ insertPaths prf0
where
go dMax prf = case findSolved 0 prf of
NoSolution -> prf0
MaybeNoSolution -> go (2 * dMax) prf
Solution path -> extractSolved path prf0
where
findSolved d node
| d >= dMax = MaybeNoSolution
| otherwise = case node of
LNode (ProofStep _ (Nothing, _ )) _ -> NoSolution
LNode (ProofStep Solved (Just _ , path)) _ -> Solution path
LNode (ProofStep _ (Just _ , _ )) cs ->
foldMap (findSolved (succ d))
(cs `using` parTraversable nfProofMethod)
nfProofMethod node = do
void $ rseq (psMethod $ root node)
void $ rseq (psInfo $ root node)
void $ rseq (children node)
return node
extractSolved [] p = p
extractSolved (label:ps) (LNode pstep m) = case M.lookup label m of
Just subprf ->
LNode pstep (M.fromList [(label, extractSolved ps subprf)])
Nothing ->
error "Theory.Constraint.cutOnSolvedDFS: impossible, extractSolved failed, invalid path"
cutOnSolvedBFS :: Proof (Maybe a) -> Proof (Maybe a)
cutOnSolvedBFS =
go (1::Int)
where
go l prf =
trace ("searching for attacks at depth: " ++ show l) $
case S.runState (checkLevel l prf) CompleteProof of
(_, UndeterminedProof) -> error "cutOnSolvedBFS: impossible"
(_, CompleteProof) -> prf
(_, IncompleteProof) -> go (l+1) prf
(prf', TraceFound) ->
trace ("attack found at depth: " ++ show l) prf'
checkLevel 0 (LNode step@(ProofStep Solved (Just _)) _) =
S.put TraceFound >> return (LNode step M.empty)
checkLevel 0 prf@(LNode (ProofStep _ x) cs)
| M.null cs = return prf
| otherwise = do
st <- S.get
msg <- case st of
TraceFound -> return $ "ignored (attack exists)"
_ -> S.put IncompleteProof >> return "bound reached"
return $ LNode (ProofStep (Sorry (Just msg)) x) M.empty
checkLevel l prf@(LNode step cs)
| isNothing (psInfo step) = return prf
| otherwise = LNode step <$> traverse (checkLevel (l1)) cs
proveSystemDFS :: Heuristic -> ProofContext -> Int -> System -> Proof ()
proveSystemDFS heuristic ctxt d0 sys0 =
prove d0 sys0
where
prove !depth sys =
case rankProofMethods (useHeuristic heuristic depth) ctxt sys of
[] -> node Solved M.empty
(method, (cases, _expl)):_ -> node method cases
where
node method cases =
LNode (ProofStep method ()) (M.map (prove (succ depth)) cases)
prettyProof :: HighlightDocument d => Proof a -> d
prettyProof = prettyProofWith (prettyProofMethod . psMethod) (const id)
prettyProofWith :: HighlightDocument d
=> (ProofStep a -> d)
-> (ProofStep a -> d -> d)
-> Proof a
-> d
prettyProofWith prettyStep prettyCase =
ppPrf
where
ppPrf (LNode ps cs) = ppCases ps (M.toList cs)
ppCases ps@(ProofStep Solved _) [] = prettyStep ps
ppCases ps [] = prettyCase ps (kwBy <> text " ")
<> prettyStep ps
ppCases ps [("", prf)] = prettyStep ps $-$ ppPrf prf
ppCases ps cases =
prettyStep ps $-$
(vcat $ intersperse (prettyCase ps kwNext) $ map ppCase cases) $-$
prettyCase ps kwQED
ppCase (name, prf) = nest 2 $
(prettyCase (root prf) $ kwCase <-> text name) $-$
ppPrf prf
showProofStatus :: SystemTraceQuantifier -> ProofStatus -> String
showProofStatus ExistsNoTrace TraceFound = "falsified - found trace"
showProofStatus ExistsNoTrace CompleteProof = "verified"
showProofStatus ExistsSomeTrace CompleteProof = "falsified - no trace found"
showProofStatus ExistsSomeTrace TraceFound = "verified"
showProofStatus _ IncompleteProof = "analysis incomplete"
showProofStatus _ UndeterminedProof = "analysis undetermined"
$( derive makeBinary ''ProofStep)
$( derive makeBinary ''ProofStatus)
$( derive makeBinary ''SolutionExtractor)
$( derive makeBinary ''AutoProver)
$( derive makeNFData ''ProofStep)
$( derive makeNFData ''ProofStatus)
$( derive makeNFData ''SolutionExtractor)
$( derive makeNFData ''AutoProver)
instance (Ord l, NFData l, NFData a) => NFData (LTree l a) where
rnf (LNode r m) = rnf r `seq` rnf m
instance (Ord l, Binary l, Binary a) => Binary (LTree l a) where
put (LNode r m) = put r >> put m
get = LNode <$> get <*> get