-
Notifications
You must be signed in to change notification settings - Fork 5
/
Logic.hs
182 lines (155 loc) · 6.05 KB
/
Logic.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
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132
133
134
135
136
137
138
139
140
141
142
143
144
145
146
147
148
149
150
151
152
153
154
155
156
157
158
159
160
161
162
163
164
165
166
167
168
169
170
171
172
173
174
175
176
177
178
179
180
181
182
module Logic
( matches
, negate
, converse
, negation
, contrapositive
, apply
, apply'
, addProof
, candidates
, relevantTheorems
, counterexamples
) where
import Import hiding (negate, head)
import Prelude (head)
import qualified Data.Map as M
import qualified Data.Set as S
import qualified Data.Text as Text
import DB (matches', addSupports, addStruts)
import Models
import Util (intersectionN, unionN, encodeText)
-- TODO: don't hardcode this
boolToValueId :: Bool -> TValueId
boolToValueId v = case keyFromValues [PersistInt64 _id] of
Right key -> key
Left e -> error $ Text.unpack e
where _id = if v then 1 else 2
negate :: Formula p -> Formula p
negate (Atom p v) = Atom p $ not v
negate (And fs ) = Or $ map negate fs
negate (Or fs ) = And $ map negate fs
converse :: Implication p -> Implication p
converse (Implication a c) = Implication c a
negation :: Implication p -> Implication p
negation (Implication a c) = Implication (negate a) (negate c)
contrapositive :: Implication p -> Implication p
contrapositive = negation . converse
-- Find (ids of) spaces matching a formula
matches :: MatchType -> Formula PropertyId -> Handler (Set SpaceId)
-- A conjunction is true if all its parts are true and unknown or false if any
-- parts are unknown, respectively
matches Yes (And sf) = intersectionN <$> mapM (matches Yes) sf
matches e (And sf) = unionN <$> mapM (matches e) sf
-- A disjunction is false if all parts or false, unknown or true if any are
matches No (Or sf) = intersectionN <$> mapM (matches No) sf
matches e (Or sf) = unionN <$> mapM (matches e) sf
-- We have to go to the database to find the spaces that match an atom
matches e (Atom p v) = S.fromList <$> matches' p (boolToValueId v) e
filterMatch :: MatchType -> [(MatchType, Set TraitId)] -> [Set TraitId]
filterMatch t pairs = [ts | (m, ts) <- pairs, m == t]
-- TODO: should be able to clean this up
check' :: (Ord p) => TraitMap p -> Formula p -> (MatchType, Set TraitId)
check' ts (And sf) =
let
subs = map (check' ts) sf
no = listToMaybe $ filterMatch No subs
unknown = listToMaybe $ filterMatch Unknown subs
in
case no of
Just evidence -> (No, evidence)
Nothing -> case unknown of
Just _ -> (Unknown, S.empty)
Nothing -> (Yes, unionN . map snd $ subs)
check' ts (Or sf) =
let
subs = map (check' ts) sf
yes = listToMaybe $ filterMatch Yes subs
unknown = listToMaybe $ filterMatch Unknown subs
in
case yes of
Just evidence -> (Yes, evidence)
Nothing -> case unknown of
Just _ -> (Unknown, S.empty)
Nothing -> (No, unionN . map snd $ subs)
check' ts (Atom p e) = case M.lookup p ts of
Nothing -> (Unknown, S.empty)
Just (t,v) -> if v == boolToValueId e
then (Yes, S.singleton t)
else (No, S.singleton t)
apply :: TheoremId -> Implication PropertyId -> SpaceId -> Handler [TraitId]
apply a i s = do
$(logDebug) $ "Applying " <> Text.pack (show . fmap show $ i) <> " to space " <> encodeText s
ts <- spaceTraitMap s (implicationProperties i)
let found = apply' a i ts
mids <- mapM (addProof s) found
return $ catMaybes mids
type Assumptions = (TheoremId, Set TraitId)
type ProofData p = (p, TValueId, Assumptions)
apply' :: (Ord p) => TheoremId -> Implication p -> TraitMap p -> [ProofData p]
apply' thrm (Implication ant con) ts =
case check' ts ant of
(Yes, evidence) -> force ts (thrm, evidence) con
(No, _) -> []
(Unknown, _) -> case check' ts (negate con) of
(Yes, evidence') -> force ts (thrm, evidence') (negate ant)
_ -> []
force :: (Ord p) => TraitMap p -> Assumptions -> Formula p -> [ProofData p]
-- Forcing a conjunction simply forces each subformula separately
force ts as (And sf) = concat . map (force ts as) $ sf
-- Forcing a disjunction can only work if there is only one unknown
-- and the rest are known not to hold
force ts (thrm,evidence) (Or sf) =
let
subs = map (\f -> (f, check' ts f)) sf
yes = [f | (f, (Yes, _)) <- subs]
unknown = [f | (f, (Unknown, _)) <- subs]
evidence' = unionN [ev | (_, (No, ev)) <- subs]
in
if null yes && length unknown == 1
then force ts (thrm, evidence `S.union` evidence') (head unknown)
else []
force ts as (Atom p v) = case M.lookup p ts of
Just _ -> [] -- Forced value is already known
Nothing -> [(p, boolToValueId v, as)]
-- TODO: there is a bit of a race condition here, if another request
-- sets the trait between the getBy check and the insert.
-- It might be better to catch the insert error and then raise a 500
-- if the DB state differs from the thing we tried to assert.
addProof :: SpaceId -> ProofData PropertyId -> Handler (Maybe TraitId)
addProof s (p,v,(thrm,ts)) = do
mt <- runDB . getBy $ TraitSP s p
case mt of
Just (Entity _id t) ->
if traitValueId t == v
then return Nothing
else error $ "Conflicting assertions for (" <> show s <> "," <> show p <> ")"
Nothing -> do
now <- liftIO getCurrentTime
_id <- runDB . insert $ Trait
{ traitSpaceId = s
, traitPropertyId = p
, traitValueId = v
, traitDescription = Textarea ""
, traitDeduced = True
, traitCreatedAt = now
, traitUpdatedAt = now
}
pid <- runDB . insert $ Proof _id thrm now now
mapM_ (runDB . insert_ . Assumption pid) . S.toList $ ts
addSupports _id ts
addStruts _id thrm ts
$(logDebug) $ "Added trait " <> encodeText _id
return $ Just _id
imatch :: MatchType -> MatchType -> Implication PropertyId -> Handler (Set SpaceId)
imatch at ct (Implication ant con) = do
a <- matches at ant
c <- matches ct con
return $ a `S.intersection` c
counterexamples, candidates:: Implication PropertyId -> Handler (Set SpaceId)
counterexamples = imatch Yes No
candidates = imatch Yes Unknown
relevantTheorems :: Trait -> Handler [(TheoremId, Implication PropertyId)]
relevantTheorems t = do
ents <- propertyTheorems . traitPropertyId $ t
return . map (\(Entity _id thrm) -> (_id, theoremImplication thrm)) $ ents