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
|
module Frontend where
import qualified Compiler as C
import Control.Monad.IO.Class
import Control.Monad.Trans.Class
import Control.Monad.Trans.State.Lazy
import Data.Foldable (traverse_)
import qualified Data.Map as M
import qualified Interpreter as I
import qualified Parser as P
import System.Console.Haskeline
import qualified Text.Megaparsec as MP
import Text.Pretty.Simple
data PrlgState =
PrlgState
{ defs :: I.Defs
, ops :: P.Ops
, strtable :: I.StrTable
}
deriving (Show)
type PrlgEnv a = StateT PrlgState (InputT IO) a
ppr :: Show a => a -> PrlgEnv ()
ppr x =
liftIO $
pPrintOpt
CheckColorTty
defaultOutputOptionsDarkBg
{ outputOptionsCompactParens = True
, outputOptionsIndentAmount = 2
, outputOptionsPageWidth = 80
}
x
withStrTable :: (I.StrTable -> (I.StrTable, a)) -> PrlgEnv a
withStrTable f = do
st <- gets strtable
let (st', x) = f st
modify (\s -> s {strtable = st'})
return x
findStruct :: String -> Int -> PrlgEnv I.Id
findStruct str arity = do
stri <- findAtom str
return I.Id {I.str = stri, I.arity = arity}
findAtom :: String -> PrlgEnv Int
findAtom = withStrTable . flip I.strtablize
interpret :: String -> PrlgEnv Bool
interpret = (>> return True) . lex
where
lex input = do
case MP.parse P.lexPrlg "-" input of
Left bundle -> liftIO $ putStr (MP.errorBundlePretty bundle)
Right toks -> parse toks
parse toks = do
case MP.parse P.parsePrlg "-" toks of
Left bundle -> liftIO $ putStr (MP.errorBundlePretty bundle)
Right asts -> traverse_ prologize asts
prologize ast = do
o <- gets ops
case P.ast2prlg o ast of
Left err -> liftIO $ putStrLn $ "expression parsing: " ++ err
Right prlg -> intern prlg
intern prlgs = do
prlgi <-
withStrTable $ \st -> C.strtablizePrlg (C.varnames prlgs) st prlgs
compile prlgi
compile prlgi
{- TODO: switch between prove goal/compile clause here -}
= do
commaId <- findStruct "," 2
let code = C.seqGoals $ C.compileGoals commaId prlgi
execute code
execute code = do
ds <- gets defs
let (_, res) = I.prove code ds
case res of
Left err -> liftIO $ putStrLn err
Right res ->
liftIO $
putStrLn $
if res
then "yes."
else "no proof."
addBuiltins = do
a1 <- findStruct "a" 1
a <- findAtom "a"
b <- findAtom "b"
c <- findAtom "c"
b0 <- findStruct "b" 0
any <- findStruct "any" 1
eq <- findStruct "=" 2
modify $ \s ->
s
{ defs =
M.fromList
[ (eq, [[I.U (I.LocalRef 0),I.U (I.LocalRef 0), I.NoGoal]])
, (a1, [[I.U (I.Atom a), I.NoGoal], [I.U (I.Atom b), I.NoGoal]])
, ( b0
, [ [I.Goal, I.U (I.Struct a1), I.U (I.Atom c), I.LastCall]
, [I.Goal, I.U (I.Struct a1), I.U (I.Atom b), I.LastCall]
])
, (any, [[I.U I.VoidRef, I.NoGoal]])
]
, ops =
[ (",", P.Op 1000 $ P.Infix P.X P.Y)
, ("=", P.Op 700 $ P.Infix P.X P.X)
]
}
interpreterStart :: PrlgEnv ()
interpreterStart = do
addBuiltins
interpreterLoop
interpreterLoop :: PrlgEnv ()
interpreterLoop = do
minput <- lift $ getInputLine "prlg> "
case minput of
Nothing -> return ()
Just input -> do
continue <- interpret input
if continue
then interpreterLoop
else return ()
interpreter :: InputT IO ()
interpreter =
evalStateT
interpreterStart
(PrlgState {defs = M.empty, ops = [], strtable = I.emptystrtable})
|
