module Theory.Constraint.Solver.Types (
ProofContext(..)
, InductionHint(..)
, pcSignature
, pcRules
, pcInjectiveFactInsts
, pcCaseDists
, pcCaseDistKind
, pcUseInduction
, pcTraceQuantifier
, pcMaudeHandle
, ClassifiedRules(..)
, emptyClassifiedRules
, crConstruct
, crDestruct
, crProtocol
, joinAllRules
, nonSilentRules
, CaseDistinction(..)
, cdGoal
, cdCases
, prettyCaseDistinction
) where
import Prelude hiding (id, (.))
import Data.Binary
import Data.DeriveTH
import Data.Label hiding (get)
import qualified Data.Label as L
import Data.Monoid (Monoid(..))
import qualified Data.Set as S
import Control.Basics
import Control.Category
import Control.DeepSeq
import Logic.Connectives
import Theory.Constraint.System
import Theory.Text.Pretty
import Theory.Model
data ClassifiedRules = ClassifiedRules
{ _crProtocol :: [RuleAC]
, _crDestruct :: [RuleAC]
, _crConstruct :: [RuleAC]
}
deriving( Eq, Ord, Show )
$(mkLabels [''ClassifiedRules])
emptyClassifiedRules :: ClassifiedRules
emptyClassifiedRules = ClassifiedRules [] [] []
joinAllRules :: ClassifiedRules -> [RuleAC]
joinAllRules (ClassifiedRules a b c) = a ++ b ++ c
nonSilentRules :: ClassifiedRules -> [RuleAC]
nonSilentRules = filter (not . null . L.get rActs) . joinAllRules
data CaseDistinction = CaseDistinction
{ _cdGoal :: Goal
, _cdCases :: Disj ([String], System)
}
deriving( Eq, Ord, Show )
data InductionHint = UseInduction | AvoidInduction
deriving( Eq, Ord, Show )
data ProofContext = ProofContext
{ _pcSignature :: SignatureWithMaude
, _pcRules :: ClassifiedRules
, _pcInjectiveFactInsts :: S.Set FactTag
, _pcCaseDistKind :: CaseDistKind
, _pcCaseDists :: [CaseDistinction]
, _pcUseInduction :: InductionHint
, _pcTraceQuantifier :: SystemTraceQuantifier
}
deriving( Eq, Ord, Show )
$(mkLabels [''ProofContext, ''CaseDistinction])
pcMaudeHandle :: ProofContext :-> MaudeHandle
pcMaudeHandle = sigmMaudeHandle . pcSignature
instance HasFrees CaseDistinction where
foldFrees f th =
foldFrees f (L.get cdGoal th) `mappend`
foldFrees f (L.get cdCases th)
foldFreesOcc _ _ = const mempty
mapFrees f th = CaseDistinction <$> mapFrees f (L.get cdGoal th)
<*> mapFrees f (L.get cdCases th)
prettyCaseDistinction :: HighlightDocument d => CaseDistinction -> d
prettyCaseDistinction th = vcat $
[ prettyGoal $ L.get cdGoal th ]
++ map combine (zip [(1::Int)..] $ map snd . getDisj $ (L.get cdCases th))
where
combine (i, sys) = fsep [keyword_ ("Case " ++ show i) <> colon, nest 2 (prettySystem sys)]
$( derive makeBinary ''CaseDistinction)
$( derive makeBinary ''ClassifiedRules)
$( derive makeBinary ''InductionHint)
$( derive makeNFData ''CaseDistinction)
$( derive makeNFData ''ClassifiedRules)
$( derive makeNFData ''InductionHint)