module Theory.Constraint.Solver.ProofMethod (
CaseName
, ProofMethod(..)
, execProofMethod
, GoalRanking(..)
, goalRankingName
, rankProofMethods
, Heuristic
, roundRobinHeuristic
, useHeuristic
, prettyProofMethod
) where
import Data.Binary
import Data.DeriveTH
import Data.Function (on)
import Data.Label hiding (get)
import qualified Data.Label as L
import Data.List
import qualified Data.Map as M
import Data.Maybe (catMaybes)
import Data.Monoid
import Data.Ord (comparing)
import qualified Data.Set as S
import Extension.Prelude (sortOn)
import Control.Basics
import Control.DeepSeq
import qualified Control.Monad.Trans.PreciseFresh as Precise
import Theory.Constraint.Solver.CaseDistinctions
import Theory.Constraint.Solver.Contradictions
import Theory.Constraint.Solver.Goals
import Theory.Constraint.Solver.Reduction
import Theory.Constraint.Solver.Simplify
import Theory.Constraint.Solver.Types
import Theory.Constraint.System
import Theory.Model
import Theory.Text.Pretty
uniqueListBy :: (a -> a -> Ordering) -> (a -> a) -> (Int -> [a -> a]) -> [a] -> [a]
uniqueListBy ord single distinguish xs0 =
map fst
$ sortBy (comparing snd)
$ concat $ map uniquify $ groupBy (\x y -> ord (fst x) (fst y) == EQ)
$ sortBy (ord `on` fst)
$ zip xs0 [(0::Int)..]
where
uniquify [] = error "impossible"
uniquify [(x,i)] = [(single x, i)]
uniquify xs = zipWith (\f (x,i) -> (f x, i)) dist xs
where
dist = distinguish $ length xs
type CaseName = String
data ProofMethod =
Sorry (Maybe String)
| Solved
| Simplify
| SolveGoal Goal
| Contradiction (Maybe Contradiction)
| Induction
deriving( Eq, Ord, Show )
instance HasFrees ProofMethod where
foldFrees f (SolveGoal g) = foldFrees f g
foldFrees f (Contradiction c) = foldFrees f c
foldFrees _ _ = mempty
foldFreesOcc _ _ = const mempty
mapFrees f (SolveGoal g) = SolveGoal <$> mapFrees f g
mapFrees f (Contradiction c) = Contradiction <$> mapFrees f c
mapFrees _ method = pure method
execProofMethod :: ProofContext
-> ProofMethod -> System -> Maybe (M.Map CaseName System)
execProofMethod ctxt method sys =
case method of
Sorry _ -> return M.empty
Solved
| null (openGoals sys) -> return M.empty
| otherwise -> Nothing
SolveGoal goal
| goal `M.member` L.get sGoals sys -> execSolveGoal goal
| otherwise -> Nothing
Simplify -> singleCase simplifySystem
Induction -> M.map cleanupSystem <$> execInduction
Contradiction _
| null (contradictions ctxt sys) -> Nothing
| otherwise -> Just M.empty
where
cleanupSystem =
(`Precise.evalFresh` Precise.nothingUsed)
. renamePrecise
. set sSubst emptySubst
singleCase m =
case removeRedundantCases ctxt [] id . map cleanupSystem
. map fst . getDisj $ execReduction m ctxt sys (avoid sys) of
[] -> return $ M.empty
[sys'] | check sys' -> return $ M.singleton "" sys'
| otherwise -> mzero
syss ->
return $ M.fromList (zip (map show [(1::Int)..]) syss)
where check sys' = cleanupSystem sys /= sys'
execSolveGoal goal =
return . makeCaseNames . removeRedundantCases ctxt [] snd
. map (second cleanupSystem) . map fst . getDisj
$ runReduction solver ctxt sys (avoid sys)
where
ths = L.get pcCaseDists ctxt
solver = do name <- maybe (solveGoal goal)
(fmap $ concat . intersperse "_")
(solveWithCaseDistinction ctxt ths goal)
simplifySystem
return name
makeCaseNames =
M.fromListWith (error "case names not unique")
. uniqueListBy (comparing fst) id distinguish
where
distinguish n =
[ (\(x,y) -> (x ++ "_case_" ++ pad (show i), y))
| i <- [(1::Int)..] ]
where
l = length (show n)
pad cs = replicate (l length cs) '0' ++ cs
execInduction
| sys == sys0 =
case S.toList $ L.get sFormulas sys of
[gf] -> case ginduct gf of
Right (bc, sc) -> Just $ insCase "empty_trace" bc
$ insCase "non_empty_trace" sc
$ M.empty
_ -> Nothing
_ -> Nothing
| otherwise = Nothing
where
sys0 = set sFormulas (L.get sFormulas sys)
$ set sLemmas (L.get sLemmas sys)
$ emptySystem (L.get sCaseDistKind sys)
insCase name gf = M.insert name (set sFormulas (S.singleton gf) sys)
data GoalRanking =
GoalNrRanking
| UsefulGoalNrRanking
| SmartRanking Bool
deriving( Eq, Ord, Show )
goalRankingName :: GoalRanking -> String
goalRankingName ranking =
"Goals sorted according to " ++ case ranking of
GoalNrRanking -> "their order of creation"
UsefulGoalNrRanking -> "their usefulness and order of creation"
SmartRanking useLoopBreakers -> smart useLoopBreakers
where
smart b = "the 'smart' heuristic (loop breakers " ++
(if b then "allowed" else "delayed") ++ ")."
rankGoals :: ProofContext -> GoalRanking -> System -> [AnnotatedGoal] -> [AnnotatedGoal]
rankGoals ctxt ranking = case ranking of
GoalNrRanking -> \_sys -> goalNrRanking
UsefulGoalNrRanking ->
\_sys -> sortOn (\(_, (nr, useless)) -> (useless, nr))
SmartRanking useLoopsBreakers -> smartRanking ctxt useLoopsBreakers
rankProofMethods :: GoalRanking -> ProofContext -> System
-> [(ProofMethod, (M.Map CaseName System, String))]
rankProofMethods ranking ctxt sys = do
(m, expl) <-
(contradiction <$> contradictions ctxt sys)
<|> (case L.get pcUseInduction ctxt of
AvoidInduction -> [(Simplify, ""), (Induction, "")]
UseInduction -> [(Induction, ""), (Simplify, "")]
)
<|> (solveGoalMethod <$> (rankGoals ctxt ranking sys $ openGoals sys))
case execProofMethod ctxt m sys of
Just cases -> return (m, (cases, expl))
Nothing -> []
where
contradiction c = (Contradiction (Just c), "")
solveGoalMethod (goal, (nr, usefulness)) =
( SolveGoal goal
, "nr. " ++ show nr ++ case usefulness of
Useful -> ""
LoopBreaker -> " (loop breaker)"
ProbablyConstructible -> " (probably constructible)"
CurrentlyDeducible -> " (currently deducible)"
)
newtype Heuristic = Heuristic [GoalRanking]
deriving( Eq, Ord, Show )
roundRobinHeuristic :: [GoalRanking] -> Heuristic
roundRobinHeuristic = Heuristic
useHeuristic :: Heuristic -> Int -> GoalRanking
useHeuristic (Heuristic [] ) = error "useHeuristic: empty list of rankings"
useHeuristic (Heuristic rankings) =
ranking
where
n = length rankings
ranking depth
| depth < 0 = error $ "useHeuristic: negative proof depth " ++ show depth
| otherwise = rankings !! (depth `mod` n)
goalNrRanking :: [AnnotatedGoal] -> [AnnotatedGoal]
goalNrRanking = sortOn (fst . snd)
smartRanking :: ProofContext
-> Bool
-> System
-> [AnnotatedGoal] -> [AnnotatedGoal]
smartRanking ctxt allowPremiseGLoopBreakers sys =
sortOnUsefulness . unmark . sortDecisionTree solveFirst . goalNrRanking
where
oneCaseOnly = catMaybes . map getMsgOneCase . L.get pcCaseDists $ ctxt
getMsgOneCase cd = case msgPremise (L.get cdGoal cd) of
Just (viewTerm -> FApp o _)
| length (getDisj (L.get cdCases cd)) == 1 -> Just o
_ -> Nothing
sortOnUsefulness = sortOn (tagUsefulness . snd . snd)
tagUsefulness Useful = 0 :: Int
tagUsefulness ProbablyConstructible = 1
tagUsefulness LoopBreaker = 1
tagUsefulness CurrentlyDeducible = 2
unmark | allowPremiseGLoopBreakers = map unmarkPremiseG
| otherwise = id
unmarkPremiseG (goal@(PremiseG _ _), (nr, _)) = (goal, (nr, Useful))
unmarkPremiseG annGoal = annGoal
solveFirst =
[ isChainGoal . fst
, isDisjGoal . fst
, isNonLoopBreakerProtoFactGoal
, isStandardActionGoal . fst
, isPrivateKnowsGoal . fst
, isFreshKnowsGoal . fst
, isSplitGoalSmall . fst
, isMsgOneCaseGoal . fst
, isDoubleExpGoal . fst
, isNoLargeSplitGoal . fst ]
smallSplitGoalSize = 3
isNonLoopBreakerProtoFactGoal (PremiseG _ fa, (_, Useful)) = not $ isKFact fa
isNonLoopBreakerProtoFactGoal _ = False
msgPremise (ActionG _ fa) = do (UpK, m) <- kFactView fa; return m
msgPremise _ = Nothing
isFreshKnowsGoal goal = case msgPremise goal of
Just (viewTerm -> Lit (Var lv)) | lvarSort lv == LSortFresh -> True
_ -> False
isMsgOneCaseGoal goal = case msgPremise goal of
Just (viewTerm -> FApp o _) | o `elem` oneCaseOnly -> True
_ -> False
isPrivateKnowsGoal goal = case msgPremise goal of
Just t -> isPrivateFunction t
_ -> False
isDoubleExpGoal goal = case msgPremise goal of
Just (viewTerm2 -> FExp _ (viewTerm2 -> FMult _)) -> True
_ -> False
isSplitGoalSmall (SplitG sid) =
maybe False (<= smallSplitGoalSize) $ splitSize (L.get sEqStore sys) sid
isSplitGoalSmall _ = False
isNoLargeSplitGoal goal@(SplitG _) = isSplitGoalSmall goal
isNoLargeSplitGoal _ = True
sortDecisionTree :: [a -> Bool] -> [a] -> [a]
sortDecisionTree [] xs = xs
sortDecisionTree (p:ps) xs = sat ++ sortDecisionTree ps nonsat
where (sat, nonsat) = partition p xs
prettyProofMethod :: HighlightDocument d => ProofMethod -> d
prettyProofMethod method = case method of
Solved -> keyword_ "SOLVED" <-> lineComment_ "trace found"
Induction -> keyword_ "induction"
Sorry reason ->
fsep [keyword_ "sorry", maybe emptyDoc lineComment_ reason]
SolveGoal goal ->
keyword_ "solve(" <-> prettyGoal goal <-> keyword_ ")"
Simplify -> keyword_ "simplify"
Contradiction reason ->
sep [ keyword_ "contradiction"
, maybe emptyDoc (lineComment . prettyContradiction) reason
]
$( derive makeBinary ''ProofMethod)
$( derive makeBinary ''GoalRanking)
$( derive makeBinary ''Heuristic)
$( derive makeNFData ''ProofMethod)
$( derive makeNFData ''GoalRanking)
$( derive makeNFData ''Heuristic)