git.iko.soy/Idris-dev
on 465cc1c help sign in
Idris-dev/src/IRTS/Lang.hs
373 lines 15 kB history raw
1{-# LANGUAGE PatternGuards, DeriveFunctor #-}
3module IRTS.Lang where
5import Control.Monad.State hiding (lift)
6import Control.Applicative hiding (Const)
8import Idris.Core.TT
9import Idris.Core.CaseTree
11import Data.List
12import Debug.Trace
14data Endianness = Native | BE | LE deriving (Show, Eq)
16data LVar = Loc Int | Glob Name
17 deriving (Show, Eq)
19-- ASSUMPTION: All variable bindings have unique names here
20data LExp = LV LVar
21 | LApp Bool LExp [LExp] -- True = tail call
22 | LLazyApp Name [LExp] -- True = tail call
23 | LLazyExp LExp
24 | LForce LExp -- make sure Exp is evaluted
25 | LLet Name LExp LExp -- name just for pretty printing
26 | LLam [Name] LExp -- lambda, lifted out before compiling
27 | LProj LExp Int -- projection
28 | LCon (Maybe LVar) -- Location to reallocate, if available
29 Int Name [LExp]
30 | LCase CaseType LExp [LAlt]
31 | LConst Const
32 | LForeign FDesc -- Function descriptor (usually name as string)
33 FDesc -- Return type descriptor
34 [(FDesc, LExp)] -- first LExp is the FFI type description
35 | LOp PrimFn [LExp]
36 | LNothing
37 | LError String
38 deriving Eq
40data FDesc = FCon Name
41 | FStr String
42 | FUnknown
43 | FIO FDesc
44 | FApp Name [FDesc]
45 deriving (Show, Eq)
47data Export = ExportData FDesc -- Exported data descriptor (usually string)
48 | ExportFun Name -- Idris name
49 FDesc -- Exported function descriptor
50 FDesc -- Return type descriptor
51 [FDesc] -- Argument types
52 deriving (Show, Eq)
54data ExportIFace = Export Name -- FFI descriptor
55 String -- interface file
56 [Export]
57 deriving (Show, Eq)
59-- Primitive operators. Backends are not *required* to implement all
60-- of these, but should report an error if they are unable
62data PrimFn = LPlus ArithTy | LMinus ArithTy | LTimes ArithTy
63 | LUDiv IntTy | LSDiv ArithTy | LURem IntTy | LSRem ArithTy
64 | LAnd IntTy | LOr IntTy | LXOr IntTy | LCompl IntTy
65 | LSHL IntTy | LLSHR IntTy | LASHR IntTy
66 | LEq ArithTy | LLt IntTy | LLe IntTy | LGt IntTy | LGe IntTy
67 | LSLt ArithTy | LSLe ArithTy | LSGt ArithTy | LSGe ArithTy
68 | LSExt IntTy IntTy | LZExt IntTy IntTy | LTrunc IntTy IntTy
69 | LStrConcat | LStrLt | LStrEq | LStrLen
70 | LIntFloat IntTy | LFloatInt IntTy | LIntStr IntTy | LStrInt IntTy
71 | LFloatStr | LStrFloat | LChInt IntTy | LIntCh IntTy
72 | LReadStr | LWriteStr | LReadFile | LWriteFile
73 | LBitCast ArithTy ArithTy -- Only for values of equal width
75 | LFExp | LFLog | LFSin | LFCos | LFTan | LFASin | LFACos | LFATan
76 | LFSqrt | LFFloor | LFCeil | LFNegate
78 -- construction element extraction element insertion
79 | LMkVec NativeTy Int | LIdxVec NativeTy Int | LUpdateVec NativeTy Int
81 | LStrHead | LStrTail | LStrCons | LStrIndex | LStrRev
82 | LStdIn | LStdOut | LStdErr
84 -- Buffers
85 | LAllocate
86 | LAppendBuffer
87 -- system info
88 | LSystemInfo
89 -- Note that for Bits8 only Native endianness is actually used
90 -- and the user-exposed interface for Bits8 doesn't mention
91 -- endianness
92 | LAppend IntTy Endianness
93 | LPeek IntTy Endianness
95 | LFork
96 | LPar -- evaluate argument anywhere, possibly on another
97 -- core or another machine. 'id' is a valid implementation
98 | LVMPtr
99 | LNullPtr
100 | LRegisterPtr
101 | LNoOp
102 deriving (Show, Eq)
104-- Supported target languages for foreign calls
106data FCallType = FStatic | FObject | FConstructor
107 deriving (Show, Eq)
109data FType = FArith ArithTy
110 | FFunction
111 | FFunctionIO
112 | FString
113 | FUnit
114 | FPtr
115 | FManagedPtr
116 | FAny
117 deriving (Show, Eq)
119-- FIXME: Why not use this for all the IRs now?
120data LAlt' e = LConCase Int Name [Name] e
121 | LConstCase Const e
122 | LDefaultCase e
123 deriving (Show, Eq, Functor)
125type LAlt = LAlt' LExp
127data LDecl = LFun [LOpt] Name [Name] LExp -- options, name, arg names, def
128 | LConstructor Name Int Int -- constructor name, tag, arity
129 deriving (Show, Eq)
131type LDefs = Ctxt LDecl
133data LOpt = Inline | NoInline
134 deriving (Show, Eq)
136addTags :: Int -> [(Name, LDecl)] -> (Int, [(Name, LDecl)])
137addTags i ds = tag i ds []
138 where tag i ((n, LConstructor n' (-1) a) : as) acc
139 = tag (i + 1) as ((n, LConstructor n' i a) : acc)
140 tag i ((n, LConstructor n' t a) : as) acc
141 = tag i as ((n, LConstructor n' t a) : acc)
142 tag i (x : as) acc = tag i as (x : acc)
143 tag i [] acc = (i, reverse acc)
145data LiftState = LS Name Int [(Name, LDecl)]
147lname (NS n x) i = NS (lname n i) x
148lname (UN n) i = MN i n
149lname x i = sMN i (show x)
151liftAll :: [(Name, LDecl)] -> [(Name, LDecl)]
152liftAll xs = concatMap (\ (x, d) -> lambdaLift x d) xs
154lambdaLift :: Name -> LDecl -> [(Name, LDecl)]
155lambdaLift n (LFun opts _ args e)
156 = let (e', (LS _ _ decls)) = runState (lift args e) (LS n 0 []) in
157 (n, LFun opts n args e') : decls
158lambdaLift n x = [(n, x)]
160getNextName :: State LiftState Name
161getNextName = do LS n i ds <- get
162 put (LS n (i + 1) ds)
163 return (lname n i)
165addFn :: Name -> LDecl -> State LiftState ()
166addFn fn d = do LS n i ds <- get
167 put (LS n i ((fn, d) : ds))
169lift :: [Name] -> LExp -> State LiftState LExp
170lift env (LV v) = return (LV v) -- Lifting happens before these can exist...
171lift env (LApp tc (LV (Glob n)) args) = do args' <- mapM (lift env) args
172 return (LApp tc (LV (Glob n)) args')
173lift env (LApp tc f args) = do f' <- lift env f
174 fn <- getNextName
175 addFn fn (LFun [Inline] fn env f')
176 args' <- mapM (lift env) args
177 return (LApp tc (LV (Glob fn)) (map (LV . Glob) env ++ args'))
178lift env (LLazyApp n args) = do args' <- mapM (lift env) args
179 return (LLazyApp n args')
180lift env (LLazyExp (LConst c)) = return (LConst c)
181-- lift env (LLazyExp (LApp tc (LV (Glob f)) args))
182-- = lift env (LLazyApp f args)
183lift env (LLazyExp e) = do e' <- lift env e
184 let usedArgs = nub $ usedIn env e'
185 fn <- getNextName
186 addFn fn (LFun [NoInline] fn usedArgs e')
187 return (LLazyApp fn (map (LV . Glob) usedArgs))
188lift env (LForce e) = do e' <- lift env e
189 return (LForce e')
190lift env (LLet n v e) = do v' <- lift env v
191 e' <- lift (env ++ [n]) e
192 return (LLet n v' e')
193lift env (LLam args e) = do e' <- lift (env ++ args) e
194 let usedArgs = nub $ usedIn env e'
195 fn <- getNextName
196 addFn fn (LFun [Inline] fn (usedArgs ++ args) e')
197 return (LApp False (LV (Glob fn)) (map (LV . Glob) usedArgs))
198lift env (LProj t i) = do t' <- lift env t
199 return (LProj t' i)
200lift env (LCon loc i n args) = do args' <- mapM (lift env) args
201 return (LCon loc i n args')
202lift env (LCase up e alts) = do alts' <- mapM liftA alts
203 e' <- lift env e
204 return (LCase up e' alts')
205 where
206 liftA (LConCase i n args e) = do e' <- lift (env ++ args) e
207 return (LConCase i n args e')
208 liftA (LConstCase c e) = do e' <- lift env e
209 return (LConstCase c e')
210 liftA (LDefaultCase e) = do e' <- lift env e
211 return (LDefaultCase e')
212lift env (LConst c) = return (LConst c)
213lift env (LForeign t s args) = do args' <- mapM (liftF env) args
214 return (LForeign t s args')
215 where
216 liftF env (t, e) = do e' <- lift env e
217 return (t, e')
218lift env (LOp f args) = do args' <- mapM (lift env) args
219 return (LOp f args')
220lift env (LError str) = return $ LError str
221lift env LNothing = return $ LNothing
223allocUnique :: LDefs -> (Name, LDecl) -> (Name, LDecl)
224allocUnique defs p@(n, LConstructor _ _ _) = p
225allocUnique defs (n, LFun opts fn args e)
226 = let e' = evalState (findUp e) [] in
227 (n, LFun opts fn args e')
228 where
229 -- Keep track of 'updatable' names in the state, i.e. names whose heap
230 -- entry may be reused, along with the arity which was there
231 findUp :: LExp -> State [(Name, Int)] LExp
232 findUp (LApp t (LV (Glob n)) as)
233 | Just (LConstructor _ i ar) <- lookupCtxtExact n defs,
234 ar == length as
235 = findUp (LCon Nothing i n as)
236 findUp (LV (Glob n))
237 | Just (LConstructor _ i 0) <- lookupCtxtExact n defs
238 = return $ LCon Nothing i n [] -- nullary cons are global, no need to update
239 findUp (LApp t f as) = LApp t <$> findUp f <*> mapM findUp as
240 findUp (LLazyApp n as) = LLazyApp n <$> mapM findUp as
241 findUp (LLazyExp e) = LLazyExp <$> findUp e
242 findUp (LForce e) = LForce <$> findUp e
243 -- use assumption that names are unique!
244 findUp (LLet n val sc) = LLet n <$> findUp val <*> findUp sc
245 findUp (LLam ns sc) = LLam ns <$> findUp sc
246 findUp (LProj e i) = LProj <$> findUp e <*> return i
247 findUp (LCon (Just l) i n es) = LCon (Just l) i n <$> mapM findUp es
248 findUp (LCon Nothing i n es)
249 = do avail <- get
250 v <- findVar [] avail (length es)
251 LCon v i n <$> mapM findUp es
252 findUp (LForeign t s es)
253 = LForeign t s <$> mapM (\ (t, e) -> do e' <- findUp e
254 return (t, e')) es
255 findUp (LOp o es) = LOp o <$> mapM findUp es
256 findUp (LCase Updatable e@(LV (Glob n)) as)
257 = LCase Updatable e <$> mapM (doUpAlt n) as
258 findUp (LCase t e as)
259 = LCase t <$> findUp e <*> mapM findUpAlt as
260 findUp t = return t
262 findUpAlt (LConCase i t args rhs) = do avail <- get
263 rhs' <- findUp rhs
264 put avail
265 return $ LConCase i t args rhs'
266 findUpAlt (LConstCase i rhs) = LConstCase i <$> findUp rhs
267 findUpAlt (LDefaultCase rhs) = LDefaultCase <$> findUp rhs
269 doUpAlt n (LConCase i t args rhs)
270 = do avail <- get
271 put ((n, length args) : avail)
272 rhs' <- findUp rhs
273 put avail
274 return $ LConCase i t args rhs'
275 doUpAlt n (LConstCase i rhs) = LConstCase i <$> findUp rhs
276 doUpAlt n (LDefaultCase rhs) = LDefaultCase <$> findUp rhs
278 findVar _ [] i = return Nothing
279 findVar acc ((n, l) : ns) i | l == i = do put (reverse acc ++ ns)
280 return (Just (Glob n))
281 findVar acc (n : ns) i = findVar (n : acc) ns i
284-- Return variables in list which are used in the expression
286usedArg env n | n `elem` env = [n]
287 | otherwise = []
289usedIn :: [Name] -> LExp -> [Name]
290usedIn env (LV (Glob n)) = usedArg env n
291usedIn env (LApp _ e args) = usedIn env e ++ concatMap (usedIn env) args
292usedIn env (LLazyApp n args) = concatMap (usedIn env) args ++ usedArg env n
293usedIn env (LLazyExp e) = usedIn env e
294usedIn env (LForce e) = usedIn env e
295usedIn env (LLet n v e) = usedIn env v ++ usedIn (env \\ [n]) e
296usedIn env (LLam ns e) = usedIn (env \\ ns) e
297usedIn env (LCon v i n args) = let rest = concatMap (usedIn env) args in
298 case v of
299 Nothing -> rest
300 Just (Glob n) -> usedArg env n ++ rest
301usedIn env (LProj t i) = usedIn env t
302usedIn env (LCase up e alts) = usedIn env e ++ concatMap (usedInA env) alts
303 where usedInA env (LConCase i n ns e) = usedIn env e
304 usedInA env (LConstCase c e) = usedIn env e
305 usedInA env (LDefaultCase e) = usedIn env e
306usedIn env (LForeign _ _ args) = concatMap (usedIn env) (map snd args)
307usedIn env (LOp f args) = concatMap (usedIn env) args
308usedIn env _ = []
310instance Show LExp where
311 show e = show' [] "" e where
312 show' env ind (LV (Loc i)) = env!!i
313 show' env ind (LV (Glob n)) = show n
315 show' env ind (LLazyApp e args)
316 = show e ++ "|(" ++ showSep ", " (map (show' env ind) args) ++")"
318 show' env ind (LApp _ e args)
319 = show' env ind e ++ "(" ++ showSep ", " (map (show' env ind) args) ++")"
321 show' env ind (LLazyExp e) = "lazy{ " ++ show' env ind e ++ " }"
322 show' env ind (LForce e) = "force{ " ++ show' env ind e ++ " }"
323 show' env ind (LLet n v e)
324 = "let " ++ show n ++ " = " ++ show' env ind v
325 ++ " in " ++ show' (env ++ [show n]) ind e
327 show' env ind (LLam args e)
328 = "\\ " ++ showSep "," (map show args)
329 ++ " => " ++ show' (env ++ (map show args)) ind e
331 show' env ind (LProj t i) = show t ++ "!" ++ show i
333 show' env ind (LCon loc i n args)
334 = atloc loc ++ show n ++ "(" ++ showSep ", " (map (show' env ind) args) ++ ")"
335 where atloc Nothing = ""
336 atloc (Just l) = "@" ++ show (LV l) ++ ":"
338 show' env ind (LCase up e alts)
339 = "case" ++ update ++ show' env ind e ++ " of \n" ++ fmt alts
340 where
341 update = case up of
342 Shared -> " "
343 Updatable -> "! "
344 fmt [] = ""
345 fmt [alt]
346 = "\t" ++ ind ++ "| " ++ showAlt env (ind ++ " ") alt
347 fmt (alt:as)
348 = "\t" ++ ind ++ "| " ++ showAlt env (ind ++ ". ") alt
349 ++ "\n" ++ fmt as
351 show' env ind (LConst c) = show c
353 show' env ind (LForeign ty n args) = concat
354 [ "foreign{ "
355 , show n ++ "("
356 , showSep ", " (map (\(ty,x) -> show' env ind x ++ " : " ++ show ty) args)
357 , ") : "
358 , show ty
359 , " }"
360 ]
362 show' env ind (LOp f args)
363 = show f ++ "(" ++ showSep ", " (map (show' env ind) args) ++ ")"
365 show' env ind (LError str) = "error " ++ show str
366 show' env ind LNothing = "____"
368 showAlt env ind (LConCase _ n args e)
369 = show n ++ "(" ++ showSep ", " (map show args) ++ ") => "
370 ++ show' env ind e
372 showAlt env ind (LConstCase c e) = show c ++ " => " ++ show' env ind e
373 showAlt env ind (LDefaultCase e) = "_ => " ++ show' env ind e