forked from liamoc/holbert
-
Notifications
You must be signed in to change notification settings - Fork 0
/
Prop.hs
123 lines (96 loc) · 4.24 KB
/
Prop.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
{-# LANGUAGE TupleSections, FlexibleContexts, GADTs, DeriveAnyClass, DeriveGeneric, OverloadedStrings #-}
module Prop where
import Unification
import qualified StringRep as SR
import Miso.String(MisoString)
import qualified Terms as T
import GHC.Generics(Generic)
import Data.Aeson (ToJSON,FromJSON)
import Data.Maybe (fromJust)
import Optics.Indexed.Core
import Optics.IxAffineTraversal
import Optics.Lens
import Optics.Iso
import Optics.Core
import Control.Applicative
type RuleName = MisoString
data RuleRef = Defn RuleName
| Local Int
-- below are for presentation only in proofs
| Rewrite RuleRef Bool -- bool is if it is flipped
| Elim RuleRef RuleRef
deriving (Eq, Show, Generic, ToJSON, FromJSON)
defnName :: RuleRef -> Maybe RuleName
defnName v = case v of Defn n -> Just n; _ -> Nothing
type NamedProp = (RuleRef, Prop)
data Prop = Forall [T.Name] [Prop] T.Term deriving (Eq, Ord, Show, Generic, ToJSON, FromJSON)
type Path = [Int]
type RuleContext = [T.Name]
infixl 9 %.
(%.) a b = icompose (flip (++)) (a % b)
premise :: Int -> IxAffineTraversal' RuleContext Prop Prop
premise n = premises % ix n
path :: [Int] -> IxAffineTraversal' RuleContext Prop Prop
path [] = iatraversal (Right . ([],)) (const id)
path (x:xs) = path xs %. premise x
premises :: IxLens' RuleContext Prop [Prop]
premises = ilens (\(Forall xs lcls _) -> (reverse xs, lcls))
(\(Forall xs _ t) lcls -> Forall xs lcls t)
conclusion :: IxLens' RuleContext Prop T.Term
conclusion = ilens (\(Forall xs _ t) -> (reverse xs, t))
(\(Forall xs lcls _) t -> Forall xs lcls t)
metabinders :: Lens' Prop [T.Name]
metabinders = lens (\(Forall xs _ _) -> xs)
(\(Forall _ lcls t) xs -> Forall xs lcls t)
blank :: Prop
blank = Forall [] [] (T.Const "???")
removePremise :: Int -> Prop -> Prop
removePremise i (Forall vs lcls g) = let (first,_:rest) = splitAt i lcls
in Forall vs (first ++ rest) g
addBinder :: T.Name -> Prop -> Prop
addBinder new (Forall vs lcls g) = Forall (vs ++ [new]) (map (raise 1) lcls) (T.raise 1 g)
isBinderUsed :: Int -> Prop -> Bool
isBinderUsed x (Forall vs lcls g) = let
dbi = length vs - x - 1
used = T.isUsed dbi g || any (isUsed dbi) lcls
in used
removeBinder :: Int -> Prop -> Prop
removeBinder x (Forall vs lcls g) = let
dbi = length vs - x - 1
(first,_:last) = splitAt x vs
g' = T.subst (T.Const "???") dbi g
lcls' = map (subst (T.Const "???") dbi) lcls
in Forall (first ++ last) lcls' g'
isUsed :: Int -> Prop -> Bool
isUsed x (Forall vs lcls g) = T.isUsed (x + length vs) g || any (isUsed (x + length vs)) lcls
raise :: Int -> Prop -> Prop
raise = raise' 0
raise' :: Int -> Int -> Prop -> Prop
raise' l n (Forall xs ps g) = Forall xs (map (raise' (l + length xs) n) ps) (T.raise' (l + length xs) n g )
subst :: T.Term -> Int -> Prop -> Prop
subst t n (Forall xs rls g) = let
t' = T.raise (length xs) t
n' = n + length xs
rls' = map (subst t' n') rls
g' = T.subst t' n' g
in Forall xs rls' g'
-- we do no raising because substitutions should only map metavariables to closed terms
applySubst :: T.Subst -> Prop -> Prop
applySubst subst (Forall vs lcls g) = Forall vs (map (applySubst subst) lcls) (T.applySubst subst g)
-- A bit disappointing that this can't be cleanly lensified.
getConclusionString :: SR.SyntaxTable -> Path -> Prop -> MisoString
getConclusionString tbl p prp = let (ctx, trm) = fromJust (ipreview (path p %. conclusion) prp)
in SR.prettyPrint tbl ctx trm
setConclusionString :: SR.SyntaxTable -> Path -> MisoString -> Prop -> Either MisoString Prop
setConclusionString tbl p txt prp = iatraverseOf (path p %. conclusion) Right parse prp
where
parse ctx _ = SR.parse tbl ctx txt
isRewrite :: Prop -> Bool
isRewrite (Forall _ _ c) | (T.Const "_=_", rest) <- T.peelApTelescope c = True
isRewrite _ = False
isIntroduction :: Prop -> Bool
isIntroduction (Forall _ _ c) | (T.Const _, rest) <- T.peelApTelescope c = True
isIntroduction _ = False
unifierProp :: Prop -> Prop -> UnifyM T.Subst
unifierProp (Forall [] [] p1) (Forall [] [] p2) = unifier p1 p2 -- [CPM] Simple case
unifierProp _ _ = empty -- [CPM] Complex case (empty for now)