-
Notifications
You must be signed in to change notification settings - Fork 0
/
Solver.hs
106 lines (84 loc) · 3.52 KB
/
Solver.hs
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
module Solver where
import Control.Applicative (empty)
import Control.Monad (liftM2, msum, when)
import Control.Monad.Reader (ReaderT (runReaderT), asks, local)
import Control.Monad.State (StateT (runStateT), gets, modify)
import Control.Monad.Trans.Class (MonadTrans (lift))
import Data.Either (isLeft)
import qualified Data.List as List (find)
import Formula
( Assumption (Assumption),
AssumptionCounter,
DeductionTree (Assumption', Tree),
Formula,
Theory,
collectKnown,
conclusion,
)
import Util (ifM)
data System = Intuitionistic | Classical
data SolverEnviron = Environ {theory :: Theory, system :: System}
data SolverState = State {counter :: AssumptionCounter, assumptions :: [Assumption]}
type Solver = ReaderT SolverEnviron (StateT SolverState Maybe)
initialState :: SolverState
initialState = State 1 []
runSolver :: Solver a -> SolverEnviron -> Maybe (a, SolverState)
runSolver s environ = runStateT (runReaderT s environ) initialState
getTheory :: Solver Theory
getTheory = asks theory
getSystem :: Solver System
getSystem = asks system
getAssumptions :: Solver [Assumption]
getAssumptions = gets assumptions
getAssumptionCounter :: Solver AssumptionCounter
getAssumptionCounter = gets counter
withAssumption :: Solver a -> Either Formula Assumption -> Solver (a, AssumptionCounter)
withAssumption solver assumption =
ifM
(isKnown $ either id (\(Assumption f _) -> f) assumption)
empty
( do
assumptionNumber <- getAssumptionCounter
addAssumption $ either (`Assumption` assumptionNumber) id assumption
when (isLeft assumption) incrementAssumptionCounter
result <- solver
popAssumption
return $ case assumption of
Left _ -> (result, assumptionNumber)
Right (Assumption _ number) -> (result, number)
)
isKnown :: Formula -> Solver Bool
isKnown f = elem f <$> knownFormulas
incrementAssumptionCounter :: Solver ()
incrementAssumptionCounter = modify (\state -> state {counter = counter state + 1})
addAssumption :: Assumption -> Solver ()
addAssumption assumption = modify (\state -> state {assumptions = assumption : assumptions state})
popAssumption :: Solver ()
popAssumption = modify (\state -> state {assumptions = case assumptions state of [] -> []; (_ : other) -> other})
findKnown :: (Formula -> Bool) -> Solver DeductionTree
findKnown predicate = find (predicate . conclusion) knownDeductions
constructFromKnownDeduction :: (DeductionTree -> Solver a) -> Solver a
constructFromKnownDeduction p = knownDeductions >>= msum . map p
knownFormulas :: Solver [Formula]
knownFormulas = map conclusion <$> knownDeductions
knownDeductions :: Solver [DeductionTree]
knownDeductions =
collectKnown
<$> liftM2
(++)
(map (\formula -> Tree formula Nothing []) <$> getTheory)
(map Assumption' <$> getAssumptions)
{-
If it's a tree, then f was in the theory so we temporarily remove it from the environment.
Otherwise we temporarily remove the assumption from the state.
-}
withoutKnown :: Solver a -> DeductionTree -> Solver a
withoutKnown solver (Tree f _ _) = local (\env -> env {theory = filter (/= f) (theory env)}) solver
withoutKnown solver (Assumption' (Assumption f _)) = do
origininalAssumptions <- getAssumptions
modify (\state -> state {assumptions = filter (\(Assumption f' _) -> f /= f') (assumptions state)})
result <- solver
modify (\state -> state {assumptions = origininalAssumptions})
return result
find :: (a -> Bool) -> Solver [a] -> Solver a
find predicate solver = solver >>= lift . lift . List.find predicate