git.iko.soy/Idris-dev
on master help sign in
Different approach to bytecode
109b291Edwin Brady
idris.cabal+1−1
compare with master
unifiedsplit
@@ -68,7 +68,7 @@ Executable idris
68
68
69 Util.Pretty,
69 Util.Pretty,
70
70
71− RTS.BCParser, RTS.Bytecode, RTS.Assembler, RTS.SC,
71+ RTS.Bytecode, RTS.SC,
72
72
73 Paths_idris
73 Paths_idris
74
74
src/Idris/ElabTerm.hs+1−1
@@ -424,7 +424,7 @@ resolveTC depth fn ist
424 [] -> []
424 [] -> []
425 [args] -> map isImp (snd args) -- won't be overloaded!
425 [args] -> map isImp (snd args) -- won't be overloaded!
426 args <- apply (Var n) imps
426 args <- apply (Var n) imps
427−-- traceWhen (all boundVar ttypes) ("Progress: " ++ show t ++ " with " ++ show n) $
427+ -- traceWhen (all boundVar ttypes) ("Progress: " ++ show t ++ " with " ++ show n) $
428 mapM_ (\ (_,n) -> do focus n
428 mapM_ (\ (_,n) -> do focus n
429 t' <- goal
429 t' <- goal
430 let (tc', ttype) = unApply t'
430 let (tc', ttype) = unApply t'
src/Main.hs+1−5
@@ -25,10 +25,6 @@ import Idris.Primitives
25import Idris.Imports
25import Idris.Imports
26import Idris.Error
26import Idris.Error
27
27
28−import RTS.BCParser
29−import RTS.Bytecode
30−import RTS.Assembler
31−
32import Paths_idris
28import Paths_idris
33
29
34-- Main program reads command line options, parses the main program, and gets
30-- Main program reads command line options, parses the main program, and gets
@@ -58,7 +54,7 @@ runIdris opts =
58 -- if we have the --bytecode flag, drop into the bytecode assembler
54 -- if we have the --bytecode flag, drop into the bytecode assembler
59 case bcs of
55 case bcs of
60 [] -> return ()
56 [] -> return ()
61− xs -> liftIO $ mapM_ bcAsm xs
57+ xs -> return () -- liftIO $ mapM_ bcAsm xs
62 case ibcsubdir of
58 case ibcsubdir of
63 [] -> setIBCSubDir ""
59 [] -> setIBCSubDir ""
64 (d:_) -> setIBCSubDir d
60 (d:_) -> setIBCSubDir d
src/RTS/Bytecode.hs+83−115
@@ -7,126 +7,94 @@ import Core.Evaluate
7import Idris.AbsSyntax
7import Idris.AbsSyntax
8import RTS.SC
8import RTS.SC
9
9
10−data SValue = VInt Int
10+import Control.Monad.State
11− | VFloat Double
11+
12− | VString String
12+type Local = Int
13− | VChar Char
14− | VBigInt Integer
15− | VRef Int
16− deriving Show
17
13
18−data BCOp = PUSH SValue
14+data BAtom = BP Name | BL Local | BC Const
19− | SLIDE Int -- Keep top stack value, discard n below it
20− | DISCARD Int
21− | DISCARDINT Int
22− | DISCARDFLOAT Int
23− | EVAL Bool
24− | MKCON Tag Arity
25− | MKTHUNK Name Int Arity
26− | MKUNIT
27− | CASE [(Int, Bytecode)] (Maybe Bytecode)
28− | INTCASE [(Int, Bytecode)] (Maybe Bytecode)
29− -- case looks at top stack item, discards immediately,
30− -- places constructor args on stack, last to first (first at ref 0)
31− | SPLIT -- get arguments from constructor form
32− | CALL Name Int -- name, number of arguments to take
33− | CLOSURE Name Int -- as CALL, but always make the closure
34− | CALLVAR Int Int -- stack ref, number of arguments to take
35− | FOREIGNCALL String CType [CType] -- TT constants for types
36− | PRIMOP SPrim [Int] -- apply to list of stack references
37− | ERROR String
38− | DUMP
39 deriving Show
15 deriving Show
40
16
17+-- Like SC, but with explicit evaluation, de Bruijn levels for locals, and all
18+-- intermediate values put into variables (which can be stored on the stack or
19+-- in registers when generating code)
20+
41−type Bytecode = [BCOp]
21+data Bytecode = BAtom BAtom
22+ | BApp BAtom [BAtom]
23+ | BLazy BAtom [BAtom]
24+ | BLet Local Bytecode Bytecode
25+ | BEval Local Bytecode
26+ | BFCall String CType [(BAtom, CType)]
27+ | BCon Tag [BAtom]
28+ | BCase Local [BAlt]
29+ | BPrimOp SPrim [BAtom]
30+ | BError String
31+ | GetArgs [Name] Bytecode -- get function arguments
32+ | Reserve Int Bytecode -- reserve stack space, clear on exit
33+ deriving Show
42
34
43−data BCProg = BCProg [(Name, Bytecode)]
35+data BAlt = BConCase Tag [Name] Bytecode
36+ | BConstCase Const Bytecode
37+ | BDefaultCase Bytecode
44 deriving Show
38 deriving Show
45
39
46bcdefs :: [(Name, SCDef)] -> [(Name, Bytecode)]
40bcdefs :: [(Name, SCDef)] -> [(Name, Bytecode)]
47−bcdefs = map (\ (n, s) -> (n, bc [] s))
41+bcdefs = map (\ (n, s) -> (n, bc s))
48−
42+
49−class BC a where
43+bc (SCDef args max c) = GetArgs (map fst args) (bcExp max (length args) c)
50− bc :: [(Name, Int)] -> -- local variables + stack offset
44+
51− a -> Bytecode
45+bcExp v arity x
52−
46+ = let (code, max) = runState (bc' x) v
53−offset :: [(Name, Int)] -> [(Name, Int)]
47+ space = max - arity in
54−offset = map (\ (n, i) -> (n, i+1))
48+ if (space > 0) then Reserve space code else code
55−
49+ where
56−-- A bytecode sequence for an expression evaluates that expression and
50+ ref i = do s <- get
57−-- places the result at the top of the stack.
51+ when (i > s) $ put i
58−
52+ next = do s <- get
59−instance BC SCDef where
53+ put (s + 1)
60− bc [] (SCDef args def) = bc (zip (map fst args) [0..]) def
54+ return s
61− ++ [SLIDE (length args)]
55+
62−
56+ bc' :: SCExp -> State Int Bytecode
63−instance BC SCExp where
57+ bc' (SRef n) = return $ BAtom (BP n)
64− bc locs (SRef n) = case lookup n locs of
58+ bc' (SLoc i) = do ref i; return $ BAtom (BL i)
65− Nothing -> [CALL n 0]
59+ bc' (SApp f args) = do f' <- bc' f
66− Just i -> [PUSH (VRef i)]
60+ args' <- mapM bc' args
67− bc locs (SApp (SRef f) args)
61+ case f' of
68− = bc' locs (reverse args) f
62+ BAtom r -> mkApp (\x -> BApp r x) args' []
69− where bc' locs [] n
63+ bc -> do v <- next
70− = case lookup n locs of
64+ mkApp (\x -> BLet v bc (BApp (BL v) x)) args' []
71− Just i -> [CALLVAR i (length args)]
72− Nothing -> [CALL n (length args)]
73− bc' locs (x : xs) f = bc locs x ++
74− bc' (offset locs) xs f
75− bc locs (SApp e args)
76− = bc locs e ++ bc' (offset locs) (reverse args) ++ [SLIDE 1]
77− where bc' locs []
78− = [CALLVAR (length args) (length args)]
79− bc' locs (x : xs) = bc locs x ++
80− bc' (offset locs) xs
81− bc locs (SLazyApp f args)
65+ bc' (SLazyApp f args) = do args' <- mapM bc' args
82− = bc' locs (reverse args) f
66+ mkApp (\x -> BApp (BP f) x) args' []
83− where bc' locs [] n
67+ bc' (SCon t args) = do args' <- mapM bc' args
84− = case lookup n locs of
68+ mkApp (\x -> BCon t x) args' []
85− Just i -> error "Internal error: Lazy call"
86− Nothing -> [CLOSURE n (length args)]
87− bc' locs (x : xs) f = bc locs x ++
88− bc' (offset locs) xs f
89− bc locs (SLet n v sc)
90− = bc locs v ++
91− bc ((n, 0) : offset locs) sc ++
92− [SLIDE 1]
93−
94− bc locs (SFCall cname ty args)
69+ bc' (SFCall c t args) = do args' <- mapM bc' (map fst args)
95− = bc' locs (reverse (map fst args))
70+ mkFApp c t (zip args' (map snd args)) []
96− where bc' locs [] = [FOREIGNCALL cname ty (map snd args)]
71+ bc' (SConst c) = return $ BAtom (BC c)
97− bc' locs (x : xs) = bc locs x ++ EVAL True : bc' (offset locs) xs
72+ bc' (SError s) = return $ BError s
98−
99− bc locs (SCon t args)
100− = bc' locs (reverse args)
101− where bc' locs [] = [MKCON t (length args)]
102− bc' locs (x : xs) = bc locs x ++ bc' (offset locs) xs
103−
104− bc locs (SConst (I i)) = [PUSH (VInt i)]
105− bc locs (SConst (BI i)) = [PUSH (VBigInt i)]
106− bc locs (SConst (Fl f)) = [PUSH (VFloat f)]
107− bc locs (SConst (Ch c)) = [PUSH (VChar c)]
108− bc locs (SConst (Str s)) = [PUSH (VString s)]
109− bc locs (SConst _) = [MKUNIT]
110−
111− bc locs (SError str) = [ERROR str]
112−
113− bc locs (SCase n alts)
73+ bc' (SCase e alts) = do e' <- bc' e
114− = let (def, cases, ty) = getCases CASE Nothing [] alts in
74+ alts' <- mapM bcAlt alts
115− bc locs (SRef n) ++ [EVAL True, ty cases def]
75+ case e' of
116− where getCases ty def cs [] = (def, reverse cs, ty)
76+ BAtom (BL i) -> return $ BCase i alts'
77+ bc -> do v <- next
78+ return $ BLet v bc (BCase v alts')
79+ bc' (SPrimOp p args) = do args' <- mapM bc' args
80+ mkApp (\x -> BPrimOp p x) args' []
81+
82+ mkApp ap [] locs = return $ ap locs
83+ mkApp ap (BAtom (BL i) : as) locs = mkApp ap as (locs ++ [BL i])
84+ mkApp ap (a : as) locs = do v <- next
85+ app <- mkApp ap as (locs ++ [BL v])
86+ return $ BLet v a app
87+
88+ bcAlt (SConCase t args e) = do e' <- bc' e
89+ return $ BConCase t args e'
90+ bcAlt (SConstCase i e) = do e' <- bc' e
91+ return $ BConstCase i e'
117− getCases ty _ cs (SDefaultCase e : rest)
92+ bcAlt (SDefaultCase e) = do e' <- bc' e
118− = getCases ty (Just (bc locs e)) cs rest
93+ return $ BDefaultCase e'
119− getCases _ def cs (SConstCase (I c) e : rest)
94+
120− = getCases INTCASE def ((c, bc locs e): cs) rest
95+ mkFApp c ty [] locs = return $ BFCall c ty locs
121− getCases _ def cs (SConCase t ns e : rest)
96+ mkFApp c ty ((BAtom (BL i), t) : as) locs = mkFApp c ty as (locs ++ [(BL i, t)])
122− = let locs' = addLocs (reverse ns) locs in
97+ mkFApp c ty ((a, t) : as) locs = do v <- next
123− getCases CASE def ((t, bc locs' e ++ [SLIDE (length locs')])
98+ app <- mkFApp c ty as (locs ++ [(BL v, t)])
124− : cs) rest
99+ return $ BLet v a app
125− addLocs [] l = l
126− addLocs (n : ns) locs = addLocs ns ((n, 0) : offset locs)
127−
128− bc locs (SPrimOp p args)
129− = bc' locs (reverse args)
130− where bc' locs [] = [PRIMOP p [0..length args-1]]
131− bc' locs (x : xs) = bc locs x ++ EVAL True : bc' (offset locs) xs
132
100
src/RTS/SC.hs+59−10
@@ -13,10 +13,12 @@ type Tag = Int
13type Arity = Int
13type Arity = Int
14
14
15data SCDef = SCDef { sc_args :: [(Name, CType)],
15data SCDef = SCDef { sc_args :: [(Name, CType)],
16+ sc_locals :: Int,
16 sc_def :: SCExp }
17 sc_def :: SCExp }
17 deriving Show
18 deriving Show
18
19
19data SCExp = SRef Name
20data SCExp = SRef Name
21+ | SLoc Int -- de Bruijn level
20 | SApp SCExp [SCExp]
22 | SApp SCExp [SCExp]
21 | SLazyApp Name [SCExp]
23 | SLazyApp Name [SCExp]
22 | SLet Name SCExp SCExp
24 | SLet Name SCExp SCExp
@@ -24,7 +26,7 @@ data SCExp = SRef Name
24 | SCon Tag [SCExp] -- constructor, assume saturated (forcing does this)
26 | SCon Tag [SCExp] -- constructor, assume saturated (forcing does this)
25 | SConst Const
27 | SConst Const
26 | SError String
28 | SError String
27− | SCase Name [SAlt]
29+ | SCase SCExp [SAlt]
28 | SPrimOp SPrim [SCExp]
30 | SPrimOp SPrim [SCExp]
29 deriving Show
31 deriving Show
30
32
@@ -71,14 +73,17 @@ toSC prims (n, d)
71 Nothing -> sclift (n, d)
73 Nothing -> sclift (n, d)
72 Just (args, rt, op) ->
74 Just (args, rt, op) ->
73 let anames = zipWith mkA args [0..] in
75 let anames = zipWith mkA args [0..] in
76+ [(n, SCDef anames (length anames)
74− [(n, SCDef anames (SPrimOp op (map (SRef . fst) anames)))]
77+ (SPrimOp op (map (SRef . fst) anames)))]
75 where mkA t i = (MN i "primArg", t)
78 where mkA t i = (MN i "primArg", t)
76
79
77sclift :: (Name, Def) -> [(Name, SCDef)]
80sclift :: (Name, Def) -> [(Name, SCDef)]
78sclift (n, d) = fst (execState (sc [] d) ([], n))
81sclift (n, d) = fst (execState (sc [] d) ([], n))
79
82
83+add (n, SCDef args _ def)
80−add x = do (xs, b) <- get
84+ = do (xs, b) <- get
81− put (x : xs, b)
85+ let (def', maxloc) = dbl (map fst args) def
86+ put ((n, SCDef args maxloc def') : xs, b)
82
87
83nextSC :: State SCState Name
88nextSC :: State SCState Name
84nextSC = do (xs, n) <- get
89nextSC = do (xs, n) <- get
@@ -99,15 +104,15 @@ class Lift s t | s -> t where
99instance Lift Def () where
104instance Lift Def () where
100 sc env (Function ty tm) = do n <- sname
105 sc env (Function ty tm) = do n <- sname
101 tm' <- sc env tm
106 tm' <- sc env tm
102− add (n, SCDef (zip env (repeat Nothing)) tm')
107+ add (n, SCDef (zip env (repeat Nothing)) 0 tm')
103 sc env (TyDecl _ _) = do n <- sname
108 sc env (TyDecl _ _) = do n <- sname
104− add (n, SCDef (zip env (repeat Nothing))
109+ add (n, SCDef (zip env (repeat Nothing)) 0
105 (SError $ "undefined " ++ show n))
110 (SError $ "undefined " ++ show n))
106 sc env (Operator _ _ _) = return ()
111 sc env (Operator _ _ _) = return ()
107 sc env (CaseOp _ _ _ _ _ args cases)
112 sc env (CaseOp _ _ _ _ _ args cases)
108 = do n <- sname
113 = do n <- sname
109 cases' <- sc (env ++ args) cases
114 cases' <- sc (env ++ args) cases
110− add (n, SCDef (zip (env ++ args) (repeat Nothing)) cases')
115+ add (n, SCDef (zip (env ++ args) (repeat Nothing)) 0 cases')
111
116
112instance Lift (TT Name) SCExp where
117instance Lift (TT Name) SCExp where
113 sc env (P _ n _) = return $ SRef n
118 sc env (P _ n _) = return $ SRef n
@@ -132,14 +137,14 @@ instance Lift (TT Name) SCExp where
132 scLam args (Bind n (Lam _) e) = scLam (n : args) e
137 scLam args (Bind n (Lam _) e) = scLam (n : args) e
133 scLam args x = do x' <- sc (args ++ env) x
138 scLam args x = do x' <- sc (args ++ env) x
134 fn <- nextSC
139 fn <- nextSC
135− add (fn, SCDef (zip (env ++ reverse args) (repeat Nothing)) x')
140+ add (fn, SCDef (zip (env ++ reverse args) (repeat Nothing)) 0 x')
136 return $ SApp (SRef fn) (map SRef env)
141 return $ SApp (SRef fn) (map SRef env)
137 sc _ _ = return $ SConst (I 42424242)
142 sc _ _ = return $ SConst (I 42424242)
138
143
139
144
140instance Lift SC SCExp where
145instance Lift SC SCExp where
141 sc env (Case n alts) = do alts' <- mapM (sc env) alts
146 sc env (Case n alts) = do alts' <- mapM (sc env) alts
142− return (SCase n alts')
147+ return (SCase (SRef n) alts')
143 sc env (STerm t) = do t' <- sc env t
148 sc env (STerm t) = do t' <- sc env t
144 return t'
149 return t'
145 sc env (UnmatchedCase s) = return (SError s)
150 sc env (UnmatchedCase s) = return (SError s)
@@ -160,7 +165,7 @@ sPrim env (P _ (UN "mkForeign") _) args = do x <- doForeign env args
160sPrim env (P _ (UN "lazy") _) [_, arg]
165sPrim env (P _ (UN "lazy") _) [_, arg]
161 = do arg' <- sc env arg
166 = do arg' <- sc env arg
162 fn <- nextSC
167 fn <- nextSC
163− add (fn, SCDef (zip env (repeat Nothing)) arg')
168+ add (fn, SCDef (zip env (repeat Nothing)) 0 arg')
164 return $ Just $ SLazyApp fn (map SRef env)
169 return $ Just $ SLazyApp fn (map SRef env)
165sPrim env (P _ (UN "prim__IO") _) [v] = do v' <- sc env v
170sPrim env (P _ (UN "prim__IO") _) [v] = do v' <- sc env v
166 return $ Just v'
171 return $ Just v'
@@ -195,3 +200,47 @@ mkEty "FString" = Just StrType
195mkEty "FPtr" = Just PtrType
200mkEty "FPtr" = Just PtrType
196mkEty "FUnit" = Just VoidType
201mkEty "FUnit" = Just VoidType
197
202
203+-- Convert local variable names to de Bruijn levels, return the biggest
204+
205+dbl :: [Name] -> SCExp -> (SCExp, Int)
206+dbl ns exp = runState (db' (extends [] ns) exp) (length ns) where
207+ db' :: [(Name, Int)] -> SCExp -> State Int SCExp
208+ db' env (SRef n) = case lookup n env of
209+ Just i -> do ref i; return $ SLoc i
210+ Nothing -> return $ SRef n
211+ db' env (SApp f args) = do f' <- db' env f
212+ args' <- mapM (db' env) args
213+ return $ SApp f' args'
214+ db' env (SLazyApp n args) = do args' <- mapM (db' env) args
215+ return $ SLazyApp n args'
216+ db' env (SLet n v sc) = do v' <- db' env v
217+ sc' <- db' (extend env n) sc
218+ ref (length env + 1)
219+ return $ SLet n v' sc'
220+ db' env (SFCall n t args) = do args' <- mapM (\ (e,t) -> do e' <- db' env e
221+ return (e', t)) args
222+ return $ SFCall n t args'
223+ db' env (SCon t args) = do args' <- mapM (db' env) args
224+ return $ SCon t args'
225+ db' env (SCase n alts) = do n' <- db' env n
226+ alts' <- mapM (dbAlt env) alts
227+ return $ SCase n' alts'
228+ db' env (SPrimOp p args) = do args' <- mapM (db' env) args
229+ return $ SPrimOp p args'
230+ db' env x = return x
231+
232+ dbAlt env (SConCase t ns exp) = do exp' <- db' (extends env ns) exp
233+ ref (length env + length ns)
234+ return $ SConCase t ns exp'
235+ dbAlt env (SConstCase c e) = do e' <- db' env e
236+ return $ SConstCase c e'
237+ dbAlt env (SDefaultCase e) = do e' <- db' env e
238+ return $ SDefaultCase e'
239+
240+ extend env n = env ++ [(n, length env)]
241+ extends env [] = env
242+ extends env (n : ns) = extends (extend env n) ns
243+
244+ ref i = do s <- get
245+ when (i > s) $ put i
246+