forked from liamoc/holbert
-
Notifications
You must be signed in to change notification settings - Fork 0
/
Rule.hs
332 lines (284 loc) · 13.7 KB
/
Rule.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
183
184
185
186
187
188
189
190
191
192
193
194
195
196
197
198
199
200
201
202
203
204
205
206
207
208
209
210
211
212
213
214
215
216
217
218
219
220
221
222
223
224
225
226
227
228
229
230
231
232
233
234
235
236
237
238
239
240
241
242
243
244
245
246
247
248
249
250
251
252
253
254
255
256
257
258
259
260
261
262
263
264
265
266
267
268
269
270
271
272
273
274
275
276
277
278
279
280
281
282
283
284
285
286
287
288
289
290
291
292
293
294
295
296
297
298
299
300
301
302
303
304
305
306
307
308
309
310
311
312
313
314
315
316
317
318
319
320
321
322
323
324
325
326
327
328
329
330
331
332
{-# LANGUAGE TypeFamilies, DeriveAnyClass, DeriveGeneric, OverloadedStrings #-}
module Rule where
import qualified ProofTree as PT
import qualified Prop as P
import qualified Terms as T
import Controller
import Unification
import Debug.Trace
import Miso.String (MisoString, pack)
import Data.String
import qualified Miso.String as MS
import Optics.Core
import StringRep
import Control.Monad(when)
import Data.Maybe(fromMaybe,fromJust,mapMaybe)
import Data.List
import GHC.Generics(Generic)
import Data.Aeson (ToJSON,FromJSON)
data RuleType
= Axiom
| Theorem
deriving (Show, Eq, Generic, ToJSON, FromJSON)
data RuleItem = RI P.RuleName P.Prop (Maybe ProofState)
deriving (Show, Eq, Generic, ToJSON, FromJSON)
data Rule = R RuleType [RuleItem]
deriving (Show, Eq, Generic, ToJSON, FromJSON)
type Counter = Int
data ProofState = PS PT.ProofTree Counter
deriving (Show, Eq, Generic, ToJSON, FromJSON)
name :: Lens' RuleItem P.RuleName
name = lensVL $ \act (RI n prp m) -> (\n' -> RI n' prp m) <$> act n
blankAxiom :: RuleType -> P.RuleName -> Rule
blankAxiom ruleType n = (R ruleType [RI n P.blank Nothing])
blankTheorem :: RuleType -> P.RuleName -> Rule
blankTheorem ruleType n = (R ruleType [RI n P.blank (Just $ PS (PT.fromProp P.blank) 0)])
-- possibly source of `invalidated` and `renamed` being broken
ruleItems :: IxTraversal' Int Rule RuleItem
ruleItems = itraversalVL guts
where
--guts :: forall f. Applicative f => (RuleItem -> f RuleItem) -> Rule -> f Rule
guts f (R t ls) = R t <$> traverse (\(i, e) -> f i e) (zip [0..] ls)
deleteItemFromRI :: Int -> [RuleItem] -> [RuleItem]
deleteItemFromRI _ [] = []
deleteItemFromRI n ris = left ++ right
where
(left , x:right) = splitAt n ris
-- warning, do not use this lens to assign to anything that might invalidate the proof state
-- use propUpdate for that (which will reset the proof state)
prop :: Lens' RuleItem P.Prop
prop = lensVL $ \act (RI n prp m) -> (\prp' -> RI n prp' m) <$> act prp
-- disjoint product of prop and name
namedProp :: Lens' RuleItem P.NamedProp
namedProp = lensVL $ \act (RI n prp m) -> (\(P.Defn n',prp') -> RI n' prp' m) <$> act (P.Defn n, prp)
propUpdate :: Setter' RuleItem P.Prop
propUpdate = sets guts
where
guts act (RI n p s)
| p' <- act p
= RI n p' (fmap (const $ PS (PT.fromProp p') 0) s)
proofState :: AffineTraversal' RuleItem ProofState
proofState = atraversal
(\i -> case i of RI _ _ (Just s) -> Right s
i -> Left i)
(\i s -> case i of RI n p (Just _) -> RI n p (Just s)
i -> i)
applyRewriteTactic :: RuleItem -> P.NamedProp -> Bool -> PT.Path -> Maybe RuleAction
applyRewriteTactic state np rev pth =
case traverseOf proofState (runUnifyPS $ PT.applyRewrite np rev pth) state of
Left _ -> Nothing
Right st' -> flip Tactic pth <$> preview proofState st'
applyERuleTactic :: RuleItem -> P.NamedProp -> P.NamedProp -> PT.Path -> Maybe RuleAction
applyERuleTactic state assm np pth =
case traverseOf proofState (runUnifyPS $ PT.applyElim np pth assm) state of
Left _ -> Nothing
Right st' -> flip Tactic pth <$> preview proofState st'
applyRuleTactic :: RuleItem -> P.NamedProp -> PT.Path -> Maybe RuleAction
applyRuleTactic state np pth =
case traverseOf proofState (runUnifyPS $ PT.apply np pth) state of
Left _ -> Nothing
Right st' -> flip Tactic pth <$> preview proofState st'
unresolved :: ProofState -> Bool
unresolved (PS pt c) = has PT.outstandingGoals pt
proofTree :: Lens' ProofState PT.ProofTree
proofTree = lensVL $ \act (PS pt c) -> flip PS c <$> act pt
runUnifyPS :: (PT.ProofTree -> UnifyM PT.ProofTree) -> ProofState -> Either UnifyError ProofState
runUnifyPS act (PS pt c) = case runUnifyM (act pt) c of
(Left e, c) -> Left e
(Right pt',c') -> Right (PS pt' c')
checkVariableName :: MS.MisoString -> Controller f ()
checkVariableName new = case T.invalidName new of
Just e -> errorMessage $ "Invalid variable name: " <> pack e
Nothing -> pure ()
data ProofFocus = GoalFocus [(P.NamedProp, RuleAction)]
| RewriteGoalFocus Bool [(P.NamedProp, RuleAction)]
| AssumptionFocus Int [(P.NamedProp, RuleAction)]
| MetavariableFocus Int
| SubtitleFocus PT.Path
| ProofBinderFocus PT.Path Int deriving (Show, Eq)
data GoalSummary = GS [(PT.Path,Int,T.Name)] [(P.NamedProp, Maybe RuleAction)] T.Term PT.Path Bool deriving (Show, Eq)
getGoalSummary :: RuleItem -> PT.Path -> Maybe GoalSummary
getGoalSummary state' f = GS <$> pure (associate state' f)
<*> fmap (map tryApply . zip (map P.Local [0 ..]) . PT.locals . fst) (ipreview (PT.path f PT.%+ PT.step) =<< preview (proofState % proofTree) state')
<*> preview (proofState % proofTree % PT.path f % PT.inference) state'
<*> pure f <*> pure False
where
tryApply r = (r, applyRuleTactic state' r f)
associate (RI _ _ (Just (PS pt _))) f = go [] (reverse f) pt
go pth [] pt = zipWith (\i n -> (pth, i, n)) [0..] (view PT.goalbinders pt)
go pth (x:xs) pt = zipWith (\i n -> (pth, i, n)) [0..] (view PT.goalbinders pt) ++ case preview (PT.subgoal x) pt of
Nothing -> []
Just sg -> go (x:pth) xs sg
data RuleFocus = ProofFocus ProofFocus (Maybe GoalSummary)
| RuleBinderFocus P.Path Int
| NewRuleBinderFocus P.Path
| RuleTermFocus P.Path
| NameFocus
deriving (Show, Eq)
data RuleAction = Tactic ProofState PT.Path
| ToggleStyle PT.Path
| SetSubgoalHeading PT.Path
| Nix PT.Path
| SelectGoal PT.Path
| ExamineAssumption Int
| RewriteGoal Bool
| RenameProofBinder PT.Path Int
| AddRuleBinder P.Path
| RenameRuleBinder P.Path Int
| DeleteRuleBinder P.Path Int
| UpdateTerm P.Path
| AddPremise P.Path
| DeletePremise P.Path
| Rename
| InstantiateMetavariable Int
| DeleteRI
deriving (Show, Eq)
editableRI tbl (ProofFocus (ProofBinderFocus pth i) g) = preview (proofState % proofTree % PT.path pth % PT.goalbinders % ix i)
editableRI tbl (RuleBinderFocus pth i) = preview (prop % P.path pth % P.metabinders % ix i)
editableRI tbl (RuleTermFocus pth) = Just . P.getConclusionString tbl pth . view prop
editableRI tbl (ProofFocus (MetavariableFocus i) g) = const (Just ("?" <> pack (show i)))
editableRI tbl NameFocus = preview name
editableRI tbl (ProofFocus (SubtitleFocus pth) g) = fmap (fromMaybe "Show:" . fmap PT.subtitle) . preview (proofState % proofTree % PT.path pth % PT.style)
editableRI _ _ = const Nothing
leaveFocusRI (ProofFocus (ProofBinderFocus p i) g) = noFocus . handleRI (RenameProofBinder p i) --These define the action when the user leaves focus on an item
leaveFocusRI (RuleBinderFocus p i) = noFocus . handleRI (RenameRuleBinder p i)
leaveFocusRI (NewRuleBinderFocus p) = noFocus . handleRI (AddRuleBinder p)
leaveFocusRI (RuleTermFocus p) = noFocus . handleRI (UpdateTerm p)
leaveFocusRI NameFocus = noFocus . handleRI Rename
--TODO handle other foci?
leaveFocusRI _ = pure
handleRI :: RuleAction -> RuleItem -> Controller RuleFocus RuleItem
handleRI (SelectGoal pth) state = do
let summary = getGoalSummary state pth
rules <- filter (P.isIntroduction . snd) <$> getKnownRules
setFocus (ProofFocus (GoalFocus $ mapMaybe (\r -> (,) r <$> applyRuleTactic state r pth) rules) summary)
pure state
handleRI (ExamineAssumption i) state = do
foc <- getOriginalFocus
case foc of
Just (ProofFocus _ (Just gs@(GS _ lcls _ p _))) | (it:_) <- drop i lcls -> do
rules <- getKnownRules
setFocus (ProofFocus (AssumptionFocus i (mapMaybe (\r -> (,) r <$> applyERuleTactic state (fst it) r p) rules)) (Just gs))
pure state
_ -> pure state
handleRI (RewriteGoal rev) state = do
foc <- getOriginalFocus
case foc of
Just (ProofFocus _ (Just gs@(GS _ _ t p _))) -> do
rules <- filter (P.isRewrite . snd) <$> getKnownRules
setFocus (ProofFocus (RewriteGoalFocus rev (mapMaybe (\r -> (,) r <$> applyRewriteTactic state r rev p ) rules)) (Just gs))
pure state
_ -> pure state
handleRI (Tactic ps pth) state = let
state' = set proofState ps state
newFocus = if has (proofState % proofTree % PT.path (0:pth)) state'
then Just (0:pth)
else fst <$> ipreview (isingular (proofState % proofTree % PT.outstandingGoals)) state'
in do
case newFocus of
Just f -> handleRI (SelectGoal f) state'
_ -> clearFocus >> pure state'
handleRI (ToggleStyle pth) state = do
let f Nothing = Just (PT.PDD { PT.proseStyle = True, PT.subtitle = "Show:" })
f (Just pdd) = Just $ pdd { PT.proseStyle = not (PT.proseStyle pdd)}
pure $ over (proofState % proofTree % PT.path pth % PT.style) f state
handleRI (SetSubgoalHeading pth) state = do
new <- textInput
let f Nothing = Just (PT.PDD { PT.proseStyle = False, PT.subtitle = new })
f (Just pdd) = Just $ pdd { PT.subtitle = new }
foc <- getOriginalFocus
let state' = over (proofState % proofTree % PT.path pth % PT.style) f state
case foc of
Just (ProofFocus _ (Just (GS _ _ _ p _))) -> handleRI (SelectGoal p) state'
_ -> pure state'
handleRI (Nix pth) state = do
clearFocus
pure $ set (proofState % proofTree % PT.path pth % PT.step) Nothing state
handleRI (RenameProofBinder pth i) state = do
new <- textInput
checkVariableName new
let state' = set (proofState % proofTree % PT.path pth % PT.goalbinders % ix i) new state
foc <- getOriginalFocus
case foc of
Just (ProofFocus _ (Just (GS _ _ _ p _))) -> handleRI (SelectGoal p) state'
_ -> pure state'
handleRI (AddRuleBinder pth) state = do
new <- textInput
checkVariableName new
invalidate (view name state)
setFocus (RuleTermFocus pth)
pure $ over (propUpdate % P.path pth) (P.addBinder new) state
handleRI (RenameRuleBinder pth i) state = do
new <- textInput
checkVariableName new
clearFocus -- should it be updateterm?
pure $ set (prop % P.path pth % P.metabinders % ix i) new state
handleRI (DeleteRuleBinder pth i) state = do
when (maybe False (P.isBinderUsed i) $ preview (prop % P.path pth) state) $ errorMessage "Cannot remove binder: is in use"
invalidate (view name state)
clearFocus
pure $ over (propUpdate % P.path pth) (P.removeBinder i) state
handleRI (UpdateTerm pth) state = do
new <- textInput
tbl <- syntaxTable
case toLensVL prop (P.setConclusionString tbl pth new) state of
Left e -> errorMessage $ "Parse error: " <> e
Right state' -> do
invalidate (view name state')
case pth of [] -> clearFocus
(_:pth') -> setFocus (RuleTermFocus pth')
pure $ over propUpdate id state' --hack..
handleRI (InstantiateMetavariable i) state = do
new <- textInput
tbl <- syntaxTable
case parse tbl [] new of
Left e -> errorMessage $ "Parse error: " <> e
Right obj -> do
foc <- getOriginalFocus
let state' = over (proofState % proofTree) (PT.applySubst (T.fromUnifier [(i,obj)])) state
case foc of
Just (ProofFocus _ (Just (GS _ _ _ p _))) -> handleRI (SelectGoal p) state'
_ -> pure state'
handleRI (AddPremise pth) state = do
invalidate (view name state)
let newIndex = length $ fromMaybe [] (preview (prop % P.path pth % P.premises) state)
setFocusWithLeaving (RuleTermFocus (newIndex:pth))
pure $ over (propUpdate % P.path pth % P.premises) (++[P.blank]) state
handleRI (DeletePremise []) state = pure state -- shouldn't happen
handleRI (DeletePremise (x:pth)) state = do
invalidate (view name state)
setFocus (RuleTermFocus (pth))
pure $ over (propUpdate % P.path pth) (P.removePremise x) state
handleRI Rename state = do
new <- textInput
when (new == "") $ errorMessage "Name cannot be empty"
renameResource (view name state) new
clearFocus
pure $ set name new state
instance Control Rule where
data Focus Rule = RF Int RuleFocus
| AddingRule
deriving (Show, Eq)
data Action Rule = RA Int RuleAction
| AddRule
deriving (Show, Eq)
defined (R _ ls) = map (\(RI n prp _) -> (P.Defn n,prp) ) ls
inserted _ = RF 0 (RuleTermFocus []) --When you've inserted an item switches to the relevant focus
invalidated s r = over (ruleItems % proofState % proofTree) (PT.clear s) r --Whenever we change a rule this goes through the document and removes it from use in proofs
renamed (s,s') r = over (ruleItems % proofState % proofTree) (PT.renameRule (s,s')) r --If we change the *name* of a rule we just update its name throughout the document
editable tbl (RF i rf) (R _ ls) = editableRI tbl rf (ls !! i)
editable tbl AddingRule _ = Nothing
leaveFocus (RF i rf) r = atraverseOf (elementOf ruleItems i) pure (leaveFocusRI rf) r
leaveFocus AddingRule r = pure r -- [CPM] Leave add rule button focus
handle (RA i DeleteRI) r@(R ruleType lst) = do
let (left , x:right) = splitAt i lst
let ruleName = view name x
invalidate ruleName
pure $ (R ruleType (left ++ right))
handle (RA i a) r = zoomFocus (RF i) (\(RF i' rf) -> if i == i' then Just rf else Nothing) (atraverseOf (elementOf ruleItems i) pure (handleRI a) r)
handle AddRule (R t ls) = do
name <- textInput
newResource name
let s' = R t (RI name P.blank Nothing:ls)
setFocus (RF 0 $ RuleTermFocus [])
pure s'