module Theory.Constraint.Solver.CaseDistinctions (
unsolvedChainConstraints
, precomputeCaseDistinctions
, refineWithTypingAsms
, solveWithCaseDistinction
, removeRedundantCases
) where
import Prelude hiding (id, (.))
import Safe
import Data.Foldable (asum)
import qualified Data.Map as M
import qualified Data.Set as S
import Control.Basics
import Control.Category
import Control.Monad.Disj
import Control.Monad.Reader
import Control.Monad.State (gets)
import Control.Parallel.Strategies
import Text.PrettyPrint.Highlight
import Extension.Data.Label
import Extension.Prelude
import Theory.Constraint.Solver.Contradictions (contradictorySystem)
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 Control.Monad.Bind
unsolvedChainConstraints :: CaseDistinction -> [Int]
unsolvedChainConstraints =
map (length . unsolvedChains . snd) . getDisj . get cdCases
initialCaseDistinction
:: ProofContext
-> [LNGuarded]
-> Goal
-> CaseDistinction
initialCaseDistinction ctxt axioms goal =
CaseDistinction goal cases
where
polish ((name, se), _) = ([name], se)
se0 = insertLemmas axioms $ emptySystem UntypedCaseDist
cases = fmap polish $
runReduction instantiate ctxt se0 (avoid (goal, se0))
instantiate = do
insertGoal goal False
solveGoal goal
refineCaseDistinction
:: ProofContext
-> Reduction (a, [String])
-> CaseDistinction
-> ([a], CaseDistinction)
refineCaseDistinction ctxt proofStep th =
( map fst $ getDisj refinement
, set cdCases newCases th )
where
newCases = Disj . removeRedundantCases ctxt stableVars snd
. map (second (modify sSubst (restrict stableVars)))
. getDisj $ snd <$> refinement
stableVars = frees (get cdGoal th)
fs = avoid th
refinement = do
(names, se) <- get cdCases th
((x, names'), se') <- fst <$> runReduction proofStep ctxt se fs
return (x, (combine names names', se'))
combine [] ns' = ns'
combine ("coerce":ns) ns' = combine ns ns'
combine (n :_) _ = [n]
solveAllSafeGoals :: [CaseDistinction] -> Reduction [String]
solveAllSafeGoals ths =
solve []
where
safeGoal _ (_, (_, LoopBreaker)) = False
safeGoal doSplit (goal, _ ) =
case goal of
ChainG _ _ -> True
ActionG _ fa -> not (isKUFact fa)
PremiseG _ fa -> not (isKUFact fa)
DisjG _ -> doSplit
SplitG _ -> False
usefulGoal (_, (_, Useful)) = True
usefulGoal _ = False
isKDPrem (PremiseG _ fa,_) = isKDFact fa
isKDPrem _ = False
isChainPrem1 (ChainG _ (_,PremIdx 1),_) = True
isChainPrem1 _ = False
solve caseNames = do
simplifySystem
ctxt <- ask
contradictoryIf =<< gets (contradictorySystem ctxt)
goals <- gets openGoals
chains <- gets unsolvedChains
let noChainGoals = null [ () | (ChainG _ _, _) <- goals ]
splitAllowed = noChainGoals && not (null chains)
safeGoals = fst <$> filter (safeGoal splitAllowed) goals
kdPremGoals = fst <$> filter (\g -> isKDPrem g || isChainPrem1 g) goals
usefulGoals = fst <$> filter usefulGoal goals
nextStep =
((fmap return . solveGoal) <$> headMay kdPremGoals) <|>
((fmap return . solveGoal) <$> headMay safeGoals) <|>
(asum $ map (solveWithCaseDistinction ctxt ths) usefulGoals)
case nextStep of
Nothing -> return $ caseNames
Just step -> solve . (caseNames ++) =<< step
removeRedundantCases :: ProofContext -> [LVar] -> (a -> System) -> [a] -> [a]
removeRedundantCases ctxt stableVars getSys cases0 =
if enableBP msig || enableMSet msig then cases else cases0
where
decoratedCases = map (second addNormSys) $ zip [(0::Int)..] cases0
cases = map (fst . snd) . sortOn fst . sortednubOn (snd . snd) $ decoratedCases
addNormSys = id &&& ((modify sEqStore dropNameHintsBound) . renameDropNameHints . getSys)
orderedVars sys =
filter ((/= LSortNode) . lvarSort) $ map fst . sortOn snd . varOccurences $ sys
renameDropNameHints sys =
(`evalFresh` avoid stableVars) . (`evalBindT` stableVarBindings) $ do
_ <- renameDropNamehint (orderedVars sys)
renameDropNamehint sys
where
stableVarBindings = M.fromList (map (\v -> (v, v)) stableVars)
msig = mhMaudeSig . get pcMaudeHandle $ ctxt
matchToGoal
:: ProofContext
-> CaseDistinction
-> Goal
-> Maybe CaseDistinction
matchToGoal ctxt th0 goalTerm =
if not $ maybeMatcher (goalTerm, get cdGoal th0) then Nothing else
case (goalTerm, get cdGoal th) of
( PremiseG (iTerm, premIdxTerm) faTerm
,PremiseG pPat@(iPat, _ ) faPat ) ->
case doMatch (faTerm `matchFact` faPat <> iTerm `matchLVar` iPat) of
[] -> Nothing
subst:_ ->
let refine = do
modM sEdges (substNodePrem pPat (iPat, premIdxTerm))
refineSubst subst
in Just $ snd $ refineCaseDistinction ctxt refine (set cdGoal goalTerm th)
(ActionG iTerm faTerm, ActionG iPat faPat) ->
case doMatch (faTerm `matchFact` faPat <> iTerm `matchLVar` iPat) of
[] -> Nothing
subst:_ -> Just $ snd $ refineCaseDistinction ctxt
(refineSubst subst) (set cdGoal goalTerm th)
_ -> Nothing
where
maybeMatcher (PremiseG _ faTerm, PremiseG _ faPat) = factTag faTerm == factTag faPat
maybeMatcher ( ActionG _ (Fact KUFact [tTerm])
, ActionG _ (Fact KUFact [tPat])) =
case (viewTerm tPat, viewTerm tTerm) of
(Lit (Var v),_) | lvarSort v == LSortFresh -> sortOfLNTerm tPat == LSortFresh
(FApp o _, FApp o' _) -> o == o'
_ -> True
maybeMatcher _ = False
th = (`evalFresh` avoid goalTerm) . rename $ th0
substNodePrem from to = S.map
(\ e@(Edge c p) -> if p == from then Edge c to else e)
doMatch match = runReader (solveMatchLNTerm match) (get pcMaudeHandle ctxt)
refineSubst subst = do
void (solveSubstEqs SplitNow subst)
void substSystem
return ((), [])
solveWithCaseDistinction :: ProofContext
-> [CaseDistinction]
-> Goal
-> Maybe (Reduction [String])
solveWithCaseDistinction hnd ths goal = do
asum [ applyCaseDistinction hnd th goal | th <- ths ]
applyCaseDistinction :: ProofContext
-> CaseDistinction
-> Goal
-> Maybe (Reduction [String])
applyCaseDistinction ctxt th0 goal = case matchToGoal ctxt th0 goal of
Just th -> Just $ do
markGoalAsSolved "precomputed" goal
(names, sysTh0) <- disjunctionOfList $ getDisj $ get cdCases th
sysTh <- (`evalBindT` keepVarBindings) . someInst $ sysTh0
conjoinSystem sysTh
return names
Nothing -> Nothing
where
keepVarBindings = M.fromList (map (\v -> (v, v)) (frees goal))
saturateCaseDistinctions
:: ProofContext -> [CaseDistinction] -> [CaseDistinction]
saturateCaseDistinctions ctxt =
go
where
go ths =
if any or (changes `using` parList rdeepseq)
then go ths'
else ths'
where
(changes, ths') = unzip $ map (refineCaseDistinction ctxt solver) ths
goodTh th = length (getDisj (get cdCases th)) <= 1
solver = do names <- solveAllSafeGoals (filter goodTh ths)
return (not $ null names, names)
precomputeCaseDistinctions
:: ProofContext
-> [LNGuarded]
-> [CaseDistinction]
precomputeCaseDistinctions ctxt axioms =
map cleanupCaseNames $ saturateCaseDistinctions ctxt rawCaseDists
where
cleanupCaseNames = modify cdCases $ fmap $ first $
filter (not . null)
. map (filter (`elem` '_' : ['a'..'z'] ++ ['A'..'Z'] ++ ['0'..'9']))
rawCaseDists =
initialCaseDistinction ctxt axioms <$> (protoGoals ++ msgGoals)
protoGoals = someProtoGoal <$> absProtoFacts
msgGoals = someKUGoal <$> absMsgFacts
getProtoFact (Fact KUFact _ ) = mzero
getProtoFact (Fact KDFact _ ) = mzero
getProtoFact fa = return fa
absFact (Fact tag ts) = (tag, length ts)
nMsgVars n = [ varTerm (LVar "t" LSortMsg i) | i <- [1..fromIntegral n] ]
someProtoGoal :: (FactTag, Int) -> Goal
someProtoGoal (tag, arity) =
PremiseG (someNodeId, PremIdx 0) (Fact tag (nMsgVars arity))
someKUGoal :: LNTerm -> Goal
someKUGoal m = ActionG someNodeId (kuFact m)
someNodeId = LVar "i" LSortNode 0
rules = get pcRules ctxt
absProtoFacts = sortednub $ do
ru <- joinAllRules rules
fa <- absFact <$> (getProtoFact =<< (get rConcs ru ++ get rPrems ru))
guard (not $ fst fa `elem` [OutFact, InFact, FreshFact])
return fa
absMsgFacts :: [LNTerm]
absMsgFacts = asum $ sortednub $
[ return $ varTerm (LVar "t" LSortFresh 1)
, if enableBP msig then return $ fAppC EMap $ nMsgVars (2::Int) else []
, [ fAppNoEq o $ nMsgVars k
| o@(_,(k,priv)) <- S.toList . noEqFunSyms $ msig
, NoEq o `S.notMember` implicitFunSig, k > 0 || priv==Private]
]
msig = mhMaudeSig . get pcMaudeHandle $ ctxt
refineWithTypingAsms
:: [LNGuarded]
-> ProofContext
-> [CaseDistinction]
-> [CaseDistinction]
refineWithTypingAsms [] _ cases0 =
fmap ((modify cdCases . fmap . second) (set sCaseDistKind TypedCaseDist)) $ cases0
refineWithTypingAsms assumptions ctxt cases0 =
fmap (modifySystems removeFormulas) $
saturateCaseDistinctions ctxt $
modifySystems updateSystem <$> cases0
where
modifySystems = modify cdCases . fmap . second
updateSystem se =
modify sFormulas (S.union (S.fromList assumptions)) $
set sCaseDistKind TypedCaseDist $ se
removeFormulas =
modify sGoals (M.filterWithKey isNoDisjGoal)
. set sFormulas S.empty
. set sSolvedFormulas S.empty
isNoDisjGoal (DisjG _) _ = False
isNoDisjGoal _ _ = True