git.iko.soy/Idris-dev
on master help sign in
Add IRTS/Bytecode
commit9b1587b08a5d67c29489f9b093fda5021576983c authorEdwin Brady <eb@cs.st-andrews.ac.uk> dateTue 7 Aug 2012, 12:13 (14 years ago) parentbf55193
3 files changed+26−1
compare with master
unifiedsplit
idris.cabal+1−1 src/IRTS/Bytecode.hs+21 src/IRTS/LParser.hs+4
idris.cabal+1−1
@@ -70,7 +70,7 @@ Executable idris
7070 Util.Pretty,
7171
7272 RTS.Bytecode, RTS.SC, RTS.PreC, RTS.CodegenC,
73− IRTS.Lang, IRTS.LParser,
73+ IRTS.Lang, IRTS.LParser, IRTS.Bytecode,
7474
7575 Paths_idris
7676
src/IRTS/Bytecode.hsnew file+21
@@ -0,0 +1,21 @@
1+module IRTS.Bytecode where
2+
3+import IRTS.Lang
4+import Core.TT
5+
6+data BC = PUSH Int
7+ | PUSHCONST Const
8+ | MKCON Int Int
9+ | CASE [(Int, [BC])] (Maybe [BC])
10+ | CONSTCASE [(Const, [BC])] (Maybe [BC])
11+ | PRINTNUM
12+ | PRINTSTR
13+ | INTOP PrimFn
14+ deriving Show
15+
16+toBC :: (Name, LDecl) -> Maybe (Name, [BC])
17+toBC (n, LConstructor _ _ _) = Nothing
18+toBC (n, LFun n' args exp) = Just (n, bc exp)
19+
20+bc :: LExp -> [BC]
21+bc x = []
src/IRTS/LParser.hs+4
@@ -3,6 +3,7 @@ module IRTS.LParser where
33import Core.CoreParser
44import Core.TT
55import IRTS.Lang
6+import IRTS.Bytecode
67
78import Text.ParserCombinators.Parsec
89import Text.ParserCombinators.Parsec.Error
@@ -46,6 +47,9 @@ fovm f = do defs <- parseFOVM f
4647 let ctxtIn = addAlist tagged emptyContext
4748 let checked = checkDefs ctxtIn tagged
4849 print checked
50+ case checked of
51+ OK c -> do let bc = mapMaybe toBC c
52+ print bc
4953
5054parseFOVM :: FilePath -> IO [(Name, LDecl)]
5155parseFOVM fname = do putStrLn $ "Reading " ++ fname