blob: 3ed39f931cff5a1ed4fb17113786e7d2306bf5d2 (
plain)
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
|
module Main where
import Control.Monad
import Haskell.AST
import Haskell.Env
import Haskell.Rewrite
import Haskell.SimpleParser
import System.Environment
import System.Exit
import System.IO
tryEither :: Either String a -> IO a
tryEither (Left err) = die err
tryEither (Right x) = return x
tryEither' :: Show e => Either e a -> IO a
tryEither' (Left err) = die (show err)
tryEither' (Right x) = return x
while :: Monad m => a -> (a -> m (Maybe a)) -> m ()
while val f = f val >>= \case
Nothing -> return ()
Just val' -> while val' f
whenM :: Monad m => m Bool -> m a -> m ()
whenM b a = b >>= \b' -> if b' then void a else return ()
ifM :: Monad m => m Bool -> m a -> m a -> m a
ifM b t e = b >>= \b' -> if b' then t else e
splitOn :: Eq a => a -> [a] -> [[a]]
splitOn _ [] = [[]]
splitOn spl (x:xs)
| x == spl = [] : splitOn spl xs
| otherwise = let (r : rs) = splitOn spl xs in (x:r) : rs
data AppState = AppState { asCtx :: Context, asFocus :: Maybe Name }
deriving (Show)
data Context = Context { cStack :: [(Action, Env)], cBaseEnv :: Env }
deriving (Show)
data Action = Action Cmd Name
deriving (Show)
data Cmd = CForget
| CRewrite Name
| CBeta
| CEta
| CCase
| CCaseForce
| CEtaCase
| CCaseCase
deriving (Show)
data UserCmd = UCCmd Cmd
| CAction Action
| CExit
| CUndo
| CShowEnv
| CUnFocus
| CFocus Name
| CLog
deriving (Show)
instance Pretty Action where
pretty (Action cmd target) = "action " ++ target ++ " " ++ pretty cmd
instance Pretty Cmd where
pretty CForget = "forget"
pretty (CRewrite name) = "rew " ++ name
pretty CBeta = "beta"
pretty CEta = "eta"
pretty CCase = "case"
pretty CCaseForce = "case!"
pretty CEtaCase = "etacase"
pretty CCaseCase = "casecase"
topEnv :: Context -> Env
topEnv (Context [] env) = env
topEnv (Context ((_, env):_) _) = env
pushCtx :: (Action, Env) -> Context -> Context
pushCtx pair ctx = ctx { cStack = pair : cStack ctx }
apply :: Context -> Action -> Either String Context
apply ctx act@(Action cmd target) = case cmd of
CForget -> do
env' <- forget (topEnv ctx) target
return $ pushCtx (act, env') ctx
CRewrite name -> genTransform (\env -> liftM2 (,) (get env name) (get env target))
(\(repl, expr) -> rewrite name repl expr)
CBeta -> transform betared
CEta -> transform etared
CCase -> transform (casered False)
CCaseForce -> transform (casered True)
CEtaCase -> transform etacase
CCaseCase -> transform casecase
where
transform :: (Expr -> Expr) -> Either String Context
transform = genTransform (\env -> get env target)
genTransform :: (Env -> Either String a) -> (a -> Expr) -> Either String Context
genTransform getter f = do
expr <- normalise . f <$> getter (topEnv ctx)
env' <- reAdd (topEnv ctx) (Def target expr)
return $ pushCtx (act, env') ctx
applyUserCmd :: AppState -> UserCmd -> IO (Either String (Maybe AppState))
applyUserCmd appstate = \case
UCCmd cmd ->
case asFocus appstate of
Nothing -> return (Left "No focus set")
Just focus ->
case apply (asCtx appstate) (Action cmd focus) of
Left err -> return (Left err)
Right ctx -> return (Right (Just appstate { asCtx = ctx }))
CAction act -> case apply (asCtx appstate) act of
Left err -> return (Left err)
Right ctx -> return (Right (Just appstate { asCtx = ctx }))
CExit -> return (Right Nothing)
CUndo ->
let ctx = asCtx appstate
in case cStack ctx of
[] -> return (Left "Empty environment stack")
(_:stk) -> return (Right (Just appstate { asCtx = ctx { cStack = stk } }))
CShowEnv -> putStrLn (pretty (topEnv (asCtx appstate))) >> return (Right (Just appstate))
CUnFocus -> return (Right (Just appstate { asFocus = Nothing }))
CFocus name -> if envContains (topEnv (asCtx appstate)) name
then return (Right (Just appstate { asFocus = Just name }))
else return (Left "Name doesn't exist")
CLog -> do
mapM_ (putStrLn . pretty) $ map fst (reverse $ cStack (asCtx appstate))
return (Right (Just appstate))
applyUserCmds :: AppState -> [UserCmd] -> IO (Either String (Maybe AppState))
applyUserCmds appstate [] = return (Right (Just appstate))
applyUserCmds appstate (ucmd : ucmds) =
applyUserCmd appstate ucmd >>= \case
Left err -> return (Left err)
Right Nothing -> return (Right Nothing)
Right (Just as) -> applyUserCmds as ucmds
interface :: AppState -> IO (Maybe AppState)
interface appstate = do
putStrLn ""
let appstate' = case asFocus appstate of
Nothing -> appstate
Just focus ->
if envContains (topEnv (asCtx appstate)) focus
then appstate
else appstate { asFocus = Nothing }
case asFocus appstate' of
Nothing -> return ()
Just n ->
case get (topEnv (asCtx appstate')) n of
Left _ -> return ()
Right expr -> putStrLn $ pretty (Def n expr)
putStr "> " >> hFlush stdout
ifM isEOF (return Nothing)
(getLine >>= handleInputLine appstate')
handleInputLine :: AppState -> String -> IO (Maybe AppState)
handleInputLine appstate line = do
let phrases = map words $ splitOn ';' line
ucmds <- case mapM parseCmd $ filter (not . null) phrases of
Left err -> putStrLn err >> return []
Right ucmds -> return ucmds
applyUserCmds appstate ucmds >>= \case
Left err -> putStrLn err >> return (Just appstate)
Right Nothing -> return Nothing
Right (Just as) -> return (Just as)
parseCmd :: [String] -> Either String UserCmd
parseCmd ("action" : target : rest) = parseCmd rest >>= \case
UCCmd cmd -> Right (CAction (Action cmd target))
_ -> Left "Invalid command within 'action'"
parseCmd ["exit"] = Right CExit
parseCmd ["undo"] = Right CUndo
parseCmd ["env"] = Right CShowEnv
parseCmd ["focus"] = Right CUnFocus
parseCmd ["focus", name] = Right (CFocus name)
parseCmd ["log"] = Right CLog
parseCmd ["forget"] = Right (UCCmd CForget)
parseCmd ["rew", func] = Right (UCCmd (CRewrite func))
parseCmd ["beta"] = Right (UCCmd CBeta)
parseCmd ["eta"] = Right (UCCmd CEta)
parseCmd ["case"] = Right (UCCmd CCase)
parseCmd ["case!"] = Right (UCCmd CCaseForce)
parseCmd ["etacase"] = Right (UCCmd CEtaCase)
parseCmd ["casecase"] = Right (UCCmd CCaseCase)
parseCmd cmd = Left $ "Unrecognised command: " ++ show cmd
main :: IO ()
main = do
fname <- getArgs >>= \case
[fname] -> return fname
_ -> die "Usage: verify-hs <file.hs>"
source <- readFile fname
ast <- tryEither' (parseAST fname source)
print ast
env0 <- tryEither (envFromAST ast)
print env0
while (AppState (Context [] env0) Nothing) interface
|