/
Shell.hs
58 lines (53 loc) · 2.05 KB
/
Shell.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
module Main where
import qualified System.Console.SimpleLineEditor as Line
import ProofCheck
import Term
import Parser
import qualified Text.Parsec as P
import qualified Data.Map as Map
import qualified Data.Set as Set
import Control.Monad.Trans.Class
import Control.Monad.Trans.State
import Control.Applicative
import Control.Arrow
import Data.Maybe (listToMaybe)
import Debug.Trace
import Data.List (intercalate)
main = Line.initialise >> evalStateT go Map.empty
where
go = do
line <- lift $ fmap concat getParagraph
env <- get
case parseLine env line of
Nothing -> lift (putStrLn "Parse Error") >> go
Just Nothing -> return ()
Just (Just (Left (name, term)))
| Set.null (freeVars term) -> modify (Map.insert name term) >> go
| otherwise -> do
lift . putStrLn $ "Error: term is not closed. Free variables: " ++ intercalate ", " (map (showTerm . Free) (Set.toList (freeVars term)))
go
Just (Just (Right term)) -> do
res <- return $ runProve ["P"] (prove term)
case res of
Left err -> lift $ putStrLn err
Right () -> lift $ putStrLn "OK"
go
parseLine env line =
case results of
Left e -> trace (show e) Nothing
Right x -> Just x
where
results = P.parse (parser env) "<input>" $ line ++ "\n"
parser env = whitespace *> P.option Nothing (Just <$> (defn <|> check))
where
defn = (Left . second (substs env)) `fmap` definition []
check = (Right . substs env) `fmap` Parser.check []
getParagraph = do
Just line <- Line.getLineEdited ">>> "
if null line then getParagraph else do
let rest = do
Just line' <- Line.getLineEdited "... "
if null line' then return [] else fmap (line':) rest
fmap (line:) rest
substs :: Map.Map Name Term -> Term -> Term
substs mp t = Map.foldrWithKey (\k v -> substitute v k) t mp