aboutsummaryrefslogtreecommitdiff
path: root/src/Main.hs
blob: f406f1b52245377598a4bc3740ce3fffffaafaac (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
215
216
217
218
219
220
221
222
223
224
225
226
227
228
229
230
231
module Main where

import Control.Monad
import Data.List
import Data.Maybe
import qualified Data.Set as Set
import System.Environment
import System.Exit
import System.IO

import Haskell.AST
import Haskell.Env
import Haskell.Env.Cmd
import Haskell.Env.Context
import Haskell.Rewrite
import Haskell.Parser
import Pretty
import Util


usageString :: String
usageString =
    "\x1B[1mMeta-commands\x1B[0m\n\
    \  env          -- Show the current environment\n\
    \  exit         -- Exit program immediately\n\
    \  undo         -- Undo last operation\n\
    \  focus \x1B[4mx\x1B[0m      -- Watch and operate on given variable\n\
    \  focus        -- Unfocus currently focused variable\n\
    \  log          -- Print list of commands that reproduces current environment\n\
    \  help         -- Show this help\n\
    \  auto         -- Try to simplify the currently focused expression as far as possible\n\
    \  rewall       -- Rewrite as much as possible, but each name at most once\n\
    \\n\
    \\x1B[1mExpression rewrite commands\x1B[0m\n\
    \These commands operate on the currently-focused expression.\n\
    \  rew \x1B[4mx\x1B[0m        -- Replaces occurrences of \x1B[4mx\x1B[0m with its value\n\
    \  beta         -- Applies some beta-reductions ((\\x -> M) y => M[y/x])\n\
    \  eta          -- Applies some eta-reductions ((\\x -> f x) => f)\n\
    \  case         -- Evaluates case statements\n\
    \  case!        -- Evaluates case statements, choosing first hit if multiple branches unify\n\
    \  etacase      -- If all case branches are the same as their patterns, remove case statement\n\
    \  casecase     -- case (case x of {A->a;B->b}) of {C->c;D->d} \n\
    \                    => case x of {A->case a of {C->c;D->d}; B->case b of {C->c;D->d}}\n\
    \  repeat \x1B[4mcmd\x1B[0m   -- Repeat \x1B[4mcmd\x1B[0m until no change occurs\n\
    \\n\
    \To evaluate a rewrite command on an unfocused variable, use:\n\
    \  action \x1B[4mx\x1B[0m \x1B[4mcmd\x1B[0m -- Evaluate \x1B[4mcmd\x1B[0m on variable \x1B[4mx\x1B[0m"


data AppState = AppState { asCtx :: Context, asFocus :: Maybe Name }
  deriving (Show)

data UserCmd = UCCmd RewCmd
             | CAction Action
             | CAuto
             | CRewriteAll
             | CExit
             | CUndo
             | CShowEnv
             | CUnFocus
             | CFocus Name
             | CLog
             | CHelp
  deriving (Show)

ctxTransform :: Context -> Action -> (Expr -> Expr) -> Either String Context
ctxTransform ctx act@(Action _ target) = generalCtxTransform ctx act (\env -> get env target)

generalCtxTransform :: Context -> Action -> (Env -> Either String a) -> (a -> Expr) -> Either String Context
generalCtxTransform ctx act@(Action _ target) getter f = do
    expr <- f <$> getter (topEnv ctx)
    env' <- reAdd (topEnv ctx) (Def target expr)
    return $ pushCtx (act, env') ctx

apply :: Context -> Action -> Either String Context
apply ctx act@(Action cmd target) = case cmd of
    CRewrite name ->
        generalCtxTransform
            ctx act
            (\env -> liftM2 (,) (get env name) (get env target))
            (\(repl, expr) -> normalise $ rewrite name repl expr)
    _ ->
        ctxTransform ctx act (fromJust (exprTransformer cmd))

findChangingTransformer :: Expr -> Maybe RewCmd
findChangingTransformer expr =
    let opts = [CBeta, CEta, CCase, CEtaCase, CCaseCase]
        results = [(cmd, normalise $ fromJust (exprTransformer cmd) expr) | cmd <- opts]
    in fst <$> find (\(_, res) -> res /= expr) results

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 }))
    CAuto ->
        case asFocus appstate of
            Nothing -> return (Left "No focus set")
            Just focus ->
                let nextStep ctx = case findChangingTransformer (fromRight (get (topEnv ctx) focus)) of
                        Nothing  -> Right ctx
                        Just cmd -> case apply ctx (Action cmd focus) of
                            Left err   -> Left err
                            Right ctx' -> nextStep ctx'
                in return $ fmap (\ctx -> Just appstate { asCtx = ctx }) $ nextStep (asCtx appstate)
    CRewriteAll ->
        case asFocus appstate of
            Nothing -> return (Left "No focus set")
            Just focus ->
                let nextStep ctx done =
                        let orig = fromRight (get (topEnv ctx) focus)
                        in case filter (isRight . get (topEnv ctx)) $ Set.toList (freeVariables orig) \\ done of
                            [] -> Right ctx
                            (name:_) -> case apply ctx (Action (CRewrite name) focus) of
                                Left err   -> Left ("Error rewriting '" ++ name ++ "': " ++ err)
                                Right ctx' ->
                                    let newexpr = fromRight (get (topEnv ctx') focus)
                                    in nextStep (if newexpr /= orig then ctx' else ctx) (name : done)
                in return $ fmap (\ctx -> Just appstate { asCtx = ctx }) $ nextStep (asCtx appstate) []
    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 (pprint 80 (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 . pprint 80) $ map fst (reverse $ cStack (asCtx appstate))
        return (Right (Just appstate))
    CHelp ->
        putStrLn usageString >> 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 $ pprint 80 (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 ["help"] = Right CHelp
parseCmd ["auto"] = Right CAuto
parseCmd ["rewall"] = Right CRewriteAll
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 ("repeat" : rest) = parseCmd rest >>= \case
    UCCmd (CRepeat _) -> Left "Cannot repeat 'repeat'"
    UCCmd cmd -> Right (UCCmd (CRepeat cmd))
    _ -> Left "Invalid command within 'repeat'"
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