git.iko.soy/Idris-dev
on master help sign in
Add scope checking for FOVM code
bf55193Edwin Brady
iif/testvm.iif+1−1
compare with master
unifiedsplit
@@ -8,7 +8,7 @@ fun plus(x, y) = case x of {
8
8
9fun natToInt(x) = case x of {
9fun natToInt(x) = case x of {
10 O => 0
10 O => 0
11− | S(k) => natToInt(k) + 1
11+ | S(k) => let y = natToInt(k) in y + 1
12 }
12 }
13
13
14fun main() = printNum(natToInt(plus(S(S(O)), S(S(O)))))
14fun main() = printNum(natToInt(plus(S(S(O)), S(S(O)))))
src/IRTS/LParser.hs+13−10
@@ -42,19 +42,22 @@ lchar = lexeme.char
42
42
43fovm :: FilePath -> IO ()
43fovm :: FilePath -> IO ()
44fovm f = do defs <- parseFOVM f
44fovm f = do defs <- parseFOVM f
45− print $ toAlist defs
45+ let tagged = addTags defs
46+ let ctxtIn = addAlist tagged emptyContext
47+ let checked = checkDefs ctxtIn tagged
48+ print checked
46
49
47−parseFOVM :: FilePath -> IO LDefs
50+parseFOVM :: FilePath -> IO [(Name, LDecl)]
48parseFOVM fname = do putStrLn $ "Reading " ++ fname
51parseFOVM fname = do putStrLn $ "Reading " ++ fname
49 fp <- readFile fname
52 fp <- readFile fname
50 case runParser pProgram () fname fp of
53 case runParser pProgram () fname fp of
51 Left err-> fail (show err)
54 Left err-> fail (show err)
52 Right x -> return x
55 Right x -> return x
53
56
54−pProgram :: LParser LDefs
57+pProgram :: LParser [(Name, LDecl)]
55pProgram = do fs <- many1 pLDecl
58pProgram = do fs <- many1 pLDecl
56 eof
59 eof
57− return $ addAlist fs emptyContext
60+ return fs
58
61
59pLDecl :: LParser (Name, LDecl)
62pLDecl :: LParser (Name, LDecl)
60pLDecl = do reserved "data"
63pLDecl = do reserved "data"
@@ -81,7 +84,11 @@ optable = [[binary "*" (\x y -> LOp LTimes [x,y]) AssocLeft,
81binary name f assoc = Infix (do reservedOp name; return f) assoc
84binary name f assoc = Infix (do reservedOp name; return f) assoc
82
85
83pLExp' :: LParser LExp
86pLExp' :: LParser LExp
87+pLExp' = try (do reserved "printNum"; e <- pLExp
88+ return (LOp LPrintNum [e]))
89+ <|> try (do reserved "print"; e <- pLExp
90+ return (LOp LPrintStr [e]))
84−pLExp' = try (do x <- iName [];
91+ <|> try (do x <- iName [];
85 lchar '('
92 lchar '('
86 args <- sepBy pLExp (lchar ',')
93 args <- sepBy pLExp (lchar ',')
87 lchar ')'
94 lchar ')'
@@ -90,12 +97,8 @@ pLExp' = try (do x <- iName [];
90 <|> pLConst
97 <|> pLConst
91 <|> do reserved "let"; x <- iName []; lchar '='; v <- pLExp
98 <|> do reserved "let"; x <- iName []; lchar '='; v <- pLExp
92 reserved "in"; e <- pLExp
99 reserved "in"; e <- pLExp
93− return (LLet (Glob x) v e)
100+ return (LLet x v e)
94 <|> pCase
101 <|> pCase
95− <|> do reserved "printNum"; e <- pLExp
96− return (LOp LPrintNum [e])
97− <|> do reserved "print"; e <- pLExp
98− return (LOp LPrintStr [e])
99 <|> do x <- iName []
102 <|> do x <- iName []
100 return (LV (Glob x))
103 return (LV (Glob x))
101
104
src/IRTS/Lang.hs+69−3
@@ -7,8 +7,8 @@ data LVar = Loc Int | Glob Name
7
7
8data LExp = LV LVar
8data LExp = LV LVar
9 | LApp Name [LExp]
9 | LApp Name [LExp]
10− | LLet LVar LExp LExp
10+ | LLet Name LExp LExp -- name just for pretty printing
11− | LCon Int [LExp]
11+ | LCon Int Name [LExp]
12 | LCase LExp [LAlt]
12 | LCase LExp [LAlt]
13 | LConst Const
13 | LConst Const
14 | LOp PrimFn [LExp]
14 | LOp PrimFn [LExp]
@@ -29,5 +29,71 @@ data LDecl = LFun Name [Name] LExp -- name, arg names, definition
29
29
30type LDefs = Ctxt LDecl
30type LDefs = Ctxt LDecl
31
31
32−-- TODO: Add constructor tags, then scope and arity checker.
32+-- TODO: scope and arity checker.
33+
34+addTags :: [(Name, LDecl)] -> [(Name, LDecl)]
35+addTags ds = tag 0 ds
36+ where tag i ((n, LConstructor n' t a) : as)
37+ = (n, LConstructor n' i a) : tag (i + 1) as
38+ tag i (x : as) = x : tag i as
39+ tag i [] = []
40+
41+checkDefs :: LDefs -> [(Name, LDecl)] -> TC [(Name, LDecl)]
42+checkDefs ctxt [] = return []
43+checkDefs ctxt (con@(n, LConstructor _ _ _) : xs) = do xs' <- checkDefs ctxt xs
44+ return (con : xs')
45+checkDefs ctxt ((n, LFun n' args exp) : xs)
46+ = do exp' <- scopecheck ctxt (zip args [0..]) exp
47+ xs' <- checkDefs ctxt xs
48+ return ((n, LFun n' args exp') : xs')
49+
50+scopecheck :: LDefs -> [(Name, Int)] -> LExp -> TC LExp
51+scopecheck ctxt env tm = sc env tm where
52+ sc env (LV (Glob n))
53+ = case lookup n (reverse env) of -- most recent first
54+ Just i -> return (LV (Loc i))
55+ Nothing -> case lookupCtxt Nothing n ctxt of
56+ [LConstructor _ i ar] ->
57+ if ar == 0 then return (LCon i n [])
58+ else fail $ "Codegen error: Constructor " ++ show n ++
59+ " has arity " ++ show ar
60+ [_] -> return (LV (Glob n))
61+ [] -> fail $ "Codegen error: No such variable " ++ show n
62+ sc env (LApp f args)
63+ = do args' <- mapM (sc env) args
64+ case lookupCtxt Nothing f ctxt of
65+ [LConstructor n tag ar] ->
66+ if (ar == length args)
67+ then return $ LCon tag n args'
68+ else fail $ "Codegen error: Constructor " ++ show f ++
69+ " has arity " ++ show ar
70+ [_] -> return $ LApp f args'
71+ [] -> fail $ "Codegen error: No such variable " ++ show f
72+ sc env (LCase e alts)
73+ = do e' <- sc env e
74+ alts' <- mapM (scalt env) alts
75+ return (LCase e' alts')
76+ sc env (LLet n v e)
77+ = do v' <- sc env v
78+ e' <- sc (env ++ [(n, length env)]) e
79+ return (LLet n v' e')
80+ sc env (LOp prim args)
81+ = do args' <- mapM (sc env) args
82+ return (LOp prim args')
83+ sc env x = return x
84+
85+ scalt env (LConCase i n args e)
86+ = do let env' = env ++ zip args [length env..]
87+ tag <- case lookupCtxt Nothing n ctxt of
88+ [LConstructor _ i ar] ->
89+ if (length args == ar) then return i
90+ else fail $ "Codegen error: Constructor " ++ show n ++
91+ " has arity " ++ show ar
92+ _ -> fail $ "Codegen error: No constructor " ++ show n
93+ e' <- sc env' e
94+ return (LConCase tag n args e')
95+ scalt env (LConstCase c e) = do e' <- sc env e
96+ return (LConstCase c e')
97+ scalt env (LDefaultCase e) = do e' <- sc env e
98+ return (LDefaultCase e')
33
99