@@ -105,8 +105,9 @@ compile codegen f tm
105105 if ex then return f else return h
106106
107107irMain :: TT Name -> Idris LDecl
108−irMain tm = do i <- ir tm
109− return $ LFun [] (sMN 0 "runMain") [] (LForce i)
108+irMain tm = do
109+ i <- irTerm M.empty [] tm
110+ return $ LFun [] (sMN 0 "runMain") [] (LForce i)
110111
111112mkDecls :: Term -> [Name] -> Idris [(Name, LDecl)]
112113mkDecls t used
@@ -126,9 +127,6 @@ showCaseTrees ds = showSep "\n\n" (map showCT ds)
126127isCon (TyDecl _ _) = True
127128isCon _ = False
128129
129−class ToIR a where
130− ir :: a -> Idris LExp
131−
132130build :: (Name, Def) -> Idris (Name, LDecl)
133131build (n, d)
134132 = do i <- getIState
@@ -144,361 +142,392 @@ build (n, d)
144142declArgs args inl n (LLam xs x) = declArgs (args ++ xs) inl n x
145143declArgs args inl n x = LFun (if inl then [Inline] else []) n args x
146144
147−mkLDecl n (Function tm _) = do e <- ir tm
148− return (declArgs [] True n e)
145+mkLDecl n (Function tm _)
146+ = declArgs [] True n <$> irTerm M.empty [] tm
147+
149148mkLDecl n (CaseOp ci _ _ _ pats cd)
150− = let (args, sc) = cases_runtime cd in
151− do e <- ir (args, sc)
152− return (declArgs [] (case_inlinable ci) n e)
149+ = declArgs [] (case_inlinable ci) n <$> irTree args sc
150+ where
151+ (args, sc) = cases_runtime cd
153152
154153mkLDecl n (TyDecl (DCon tag arity) _) =
155− LConstructor n tag . maybe 0 (length . usedpos) . lookupCtxtExact n . idris_callgraph <$> getIState
154+ LConstructor n tag . erasedArity . lookup n <$> getIState
155+ where
156+ lookup n = lookupCtxtExact n . idris_callgraph
157+ erasedArity = maybe 0 (length . usedpos)
156158
157159mkLDecl n (TyDecl (TCon t a) _) = return $ LConstructor n (-1) a
158160mkLDecl n _ = return $ (declArgs [] True n LNothing) -- postulate, never run
159161
160−instance ToIR (TT Name) where
161− ir tm = ir' [] tm where
162− ir' env tm@(App f a)
163− | (P _ (UN m) _, args) <- unApply tm,
164− m == txt "mkForeignPrim"
165− = doForeign env args
166− | (P _ (UN u) _, [_, arg]) <- unApply tm,
167− u == txt "unsafePerformPrimIO"
168− = ir' env arg
169− -- TMP HACK - until we get inlining.
170− | (P _ (UN r) _, [_, _, _, _, _, arg]) <- unApply tm,
171− r == txt "replace"
172− = ir' env arg
173− -- Laziness, the old way
174− | (P _ (UN l) _, [_, arg]) <- unApply tm,
175− l == txt "lazy"
176− = do arg' <- ir' env arg
177− error "lazy has crept in somehow"
178−-- return $ LLazyExp arg'
179− | (P _ (UN l) _, [_, arg]) <- unApply tm,
180− l == txt "force"
181− = do arg' <- ir' env arg
182− return $ LForce arg'
183− -- Laziness, the new way
184− | (P _ (UN l) _, [_, arg]) <- unApply tm,
185− l == txt "Delay"
186− = do arg' <- ir' env arg
187− return $ LLazyExp arg'
188− | (P _ (UN l) _, [_, arg]) <- unApply tm,
189− l == txt "Force"
190− = do arg' <- ir' env arg
191− return $ LForce arg'
192− | (P _ (UN a) _, [_, _, arg]) <- unApply tm,
193− a == txt "assert_smaller"
194− = ir' env arg
195− | (P _ (UN a) _, [_, arg]) <- unApply tm,
196− a == txt "assert_total"
197− = ir' env arg
198− | (P _ (UN p) _, [_, arg]) <- unApply tm,
199− p == txt "par"
200− = do arg' <- ir' env arg
201− return $ LOp LPar [LLazyExp arg']
202− | (P _ (UN pf) _, [arg]) <- unApply tm,
203− pf == txt "prim_fork"
204− = do arg' <- ir' env arg
205− return $ LOp LFork [LLazyExp arg']
206− | (P _ (UN m) _, [_,size,t]) <- unApply tm,
207− m == txt "malloc"
208− = do size' <- ir' env size
209− t' <- ir' env t
210− return t' -- TODO $ malloc_ size' t'
211− | (P _ (UN tm) _, [_,t]) <- unApply tm,
212− tm == txt "trace_malloc"
213− = do t' <- ir' env t
214− return t' -- TODO
215−
216− -- This case is here until we get more general inlining. It's just
217− -- a really common case, and the laziness hurts...
218− | (P _ (NS (UN be) [b,p]) _, [_,x,(App (P _ (UN d) _) t),
219− (App (P _ (UN d') _) e)]) <- unApply tm,
220− be == txt "boolElim" && d == txt "Delay" && d' == txt "Delay"
221− = do x' <- ir' env x
222− t' <- ir' env t
223− e' <- ir' env e
224− return (LCase x' [LConCase 0 (sNS (sUN "False") ["Bool","Prelude"]) [] e',
225− LConCase 1 (sNS (sUN "True") ["Bool","Prelude"]) [] t'])
226−
227− | (P (DCon t arity) n _, args) <- unApply tm = do
228− ist <- getIState
229− let detag = maybe False detaggable . lookupCtxtExact n $ idris_optimisation ist
230− used = maybe [] (map fst . usedpos) . lookupCtxtExact n $ idris_callgraph ist
231− args' = [a | (i,a) <- zip [0..] args, i `elem` used]
232−
233− when (length args > arity) $
234− ifail ("oversaturated data ctor: " ++ show tm)
235−
236− if length args' == 1 && detag -- detaggable
237− then ir' env (head args') -- newtype
238− else irCon env t (length used) n args'
239−
240− | (P (TCon t a) n _, args) <- unApply tm
241− = return LNothing
242−
243− | (P _ n _, args) <- unApply tm = do
244− ist <- getIState
245− case lookup n (idris_scprims ist) of
246− -- if it's a primitive which is already saturated,
247− -- compile to the corresponding op here already to save work
248− Just (arity, op) | length args == arity
249− -> LOp op <$> mapM (ir' env) args
250−
251− _ -> applyName n ist args
252−
253− | (f, args) <- unApply tm
254− = do f' <- ir' env f
255− args' <- mapM (ir' env) args
256− return (LApp False f' args')
257−
258− where
259− applyName :: Name -> IState -> [Term] -> Idris LExp
260− applyName n ist args =
261− LApp False (LV $ Glob n) <$> mapM (ir' env . erase) (zip [0..] args)
262− where
263− erase (i, x)
264− | i >= arity || i `elem` used = x
265− | otherwise = Erased
266−
267− arity = case fst4 <$> lookupCtxt n (definitions . tt_ctxt $ ist) of
268− [CaseOp ci ty tys def tot cdefs] -> length tys
269− [TyDecl (DCon tag ar) _] -> ar
270− [TyDecl Ref ty] -> length $ getArgTys ty
271− [Operator ty ar op] -> ar
272− [] -> 0 -- no definition, probably local name => can't erase anything
273− def -> error $ "unknown arity: " ++ show (n, def)
274−
275− used = maybe [] (map fst . usedpos) $ lookupCtxtExact n (idris_callgraph ist)
276− fst4 (x,_,_,_) = x
162+data VarInfo = VI
163+ { viMethod :: Maybe Name
164+ }
165+ deriving Show
166+
167+type Vars = M.Map Name VarInfo
168+
169+irTerm :: Vars -> [Name] -> Term -> Idris LExp
170+irTerm vs env tm@(App f a) = case unApply tm of
171+ (P _ (UN m) _, args)
172+ | m == txt "mkForeignPrim"
173+ -> doForeign vs env args
174+
175+ (P _ (UN u) _, [_, arg])
176+ | u == txt "unsafePerformPrimIO"
177+ -> irTerm vs env arg
178+
179+ -- TMP HACK - until we get inlining.
180+ (P _ (UN r) _, [_, _, _, _, _, arg])
181+ | r == txt "replace"
182+ -> irTerm vs env arg
183+
184+ -- Laziness, the old way
185+ (P _ (UN l) _, [_, arg])
186+ | l == txt "lazy"
187+ -> error "lazy has crept in somehow"
188+
189+ (P _ (UN l) _, [_, arg])
190+ | l == txt "force"
191+ -> LForce <$> irTerm vs env arg
192+
193+ -- Laziness, the new way
194+ (P _ (UN l) _, [_, arg])
195+ | l == txt "Delay"
196+ -> LLazyExp <$> irTerm vs env arg
197+
198+ (P _ (UN l) _, [_, arg])
199+ | l == txt "Force"
200+ -> LForce <$> irTerm vs env arg
201+
202+ (P _ (UN a) _, [_, _, arg])
203+ | a == txt "assert_smaller"
204+ -> irTerm vs env arg
205+
206+ (P _ (UN a) _, [_, arg])
207+ | a == txt "assert_total"
208+ -> irTerm vs env arg
209+
210+ (P _ (UN p) _, [_, arg])
211+ | p == txt "par"
212+ -> do arg' <- irTerm vs env arg
213+ return $ LOp LPar [LLazyExp arg']
214+
215+ (P _ (UN pf) _, [arg])
216+ | pf == txt "prim_fork"
217+ -> do arg' <- irTerm vs env arg
218+ return $ LOp LFork [LLazyExp arg']
219+
220+ (P _ (UN m) _, [_,size,t])
221+ | m == txt "malloc"
222+ -> irTerm vs env t
223+{-
224+ = do size' <- ir' env size
225+ t' <- ir' env t
226+ return t' -- TODO $ malloc_ size' t'
227+-}
228+
229+ (P _ (UN tm) _, [_,t])
230+ | tm == txt "trace_malloc"
231+ -> irTerm vs env t -- TODO
232+
233+ -- This case is here until we get more general inlining. It's just
234+ -- a really common case, and the laziness hurts...
235+ (P _ (NS (UN be) [b,p]) _, [_,x,(App (P _ (UN d) _) t),
236+ (App (P _ (UN d') _) e)])
237+ | be == txt "boolElim"
238+ , d == txt "Delay"
239+ , d' == txt "Delay"
240+ -> do
241+ x' <- irTerm vs env x
242+ t' <- irTerm vs env t
243+ e' <- irTerm vs env e
244+ return (LCase x' [LConCase 0 (sNS (sUN "False") ["Bool","Prelude"]) [] e'
245+ ,LConCase 1 (sNS (sUN "True" ) ["Bool","Prelude"]) [] t'
246+ ])
247+
248+ (P (DCon t arity) n _, args) -> do
249+ ist <- getIState
250+ let detag = maybe False detaggable . lookupCtxtExact n $ idris_optimisation ist
251+ used = maybe [] (map fst . usedpos) . lookupCtxtExact n $ idris_callgraph ist
252+ args' = [a | (i,a) <- zip [0..] args, i `elem` used]
253+
254+ when (length args > arity) $
255+ ifail ("oversaturated data ctor: " ++ show tm)
256+
257+ if length args' == 1 && detag -- detaggable
258+ then irTerm vs env (head args') -- newtype
259+ else irCon vs env (length used) n args'
260+
261+ (P (TCon t a) n _, args) -> return LNothing
262+
263+ (P _ n _, args) -> do
264+ ist <- getIState
265+ case lookup n (idris_scprims ist) of
266+ -- if it's a primitive that is already saturated,
267+ -- compile to the corresponding op here already to save work
268+ Just (arity, op) | length args == arity
269+ -> LOp op <$> mapM (irTerm vs env) args
270+
271+ -- otherwise, just apply the name
272+ _ -> applyName n ist args
273+
274+ (f, args)
275+ -> LApp False
276+ <$> irTerm vs env f
277+ <*> mapM (irTerm vs env) args
278+
279+ where
280+ applyName :: Name -> IState -> [Term] -> Idris LExp
281+ applyName n ist args =
282+ LApp False (LV $ Glob n) <$> mapM (irTerm vs env . erase) (zip [0..] args)
283+ where
284+ erase (i, x)
285+ | i >= arity || i `elem` used = x
286+ | otherwise = Erased
287+
288+ arity = case fst4 <$> lookupCtxt n (definitions . tt_ctxt $ ist) of
289+ [CaseOp ci ty tys def tot cdefs] -> length tys
290+ [TyDecl (DCon tag ar) _] -> ar
291+ [TyDecl Ref ty] -> length $ getArgTys ty
292+ [Operator ty ar op] -> ar
293+ [] -> 0 -- no definition, probably local name => can't erase anything
294+ def -> error $ "unknown arity: " ++ show (n, def)
295+
296+ used = maybe [] (map fst . usedpos) $ lookupCtxtExact n (idris_callgraph ist)
297+ fst4 (x,_,_,_) = x
277298
278299-- ir' env (P _ (NS (UN "Z") ["Nat", "Prelude"]) _)
279300-- = return $ LConst (BI 0)
280− ir' env (P _ n _) = return $ LV (Glob n)
281− ir' env (V i) | i >= 0 && i < length env = return $ LV (Glob (env!!i))
282− | otherwise = ifail $ "IR fail " ++ show i ++ " " ++ show tm
283− ir' env (Bind n (Lam _) sc)
284− = do let n' = uniqueName n env
285− sc' <- ir' (n' : env) sc
286− return $ LLam [n'] sc'
287− ir' env (Bind n (Let _ v) sc)
288− = do sc' <- ir' (n : env) sc
289− v' <- ir' env v
290− return $ LLet n v' sc'
291− ir' env (Bind _ _ _) = return $ LNothing
292− ir' env (Proj t i) | i == -1
293− = do t' <- ir' env t
294− return $ LOp (LMinus (ATInt ITBig))
295− [t', LConst (BI 1)]
296− ir' env (Proj t i) = do t' <- ir' env t
297− return $ LProj t' i
298− ir' env (Constant c) = return $ LConst c
299− ir' env (TType _) = return $ LNothing
300− ir' env Erased = return $ LNothing
301− ir' env Impossible = return $ LNothing
301+
302+irTerm vs env (P _ n _) = return $ LV (Glob n)
303+irTerm vs env (V i)
304+ | i >= 0 && i < length env = return $ LV (Glob (env!!i))
305+ | otherwise = ifail $ "bad de bruijn index: " ++ show i
306+
307+irTerm vs env (Bind n (Lam _) sc) = LLam [n'] <$> irTerm vs (n':env) sc
308+ where
309+ n' = uniqueName n env
310+
311+irTerm vs env (Bind n (Let _ v) sc)
312+ = LLet n <$> irTerm vs env v <*> irTerm vs (n : env) sc
313+
314+irTerm vs env (Bind _ _ _) = return $ LNothing
315+
316+irTerm vs env (Proj t (-1)) = do
317+ t' <- irTerm vs env t
318+ return $ LOp (LMinus (ATInt ITBig))
319+ [t', LConst (BI 1)]
320+
321+irTerm vs env (Proj t i) = LProj <$> irTerm vs env t <*> pure i
322+irTerm vs env (Constant c) = return $ LConst c
323+irTerm vs env (TType _) = return $ LNothing
324+irTerm vs env Erased = return $ LNothing
325+irTerm vs env Impossible = return $ LNothing
302326-- ir' env _ = return $ LError "Impossible"
303327
304− irCon env t arity n args
305− | length args == arity = buildApp env (LV (Glob n)) args
306− | otherwise = let extra = satArgs (arity - length args) in
307− do sc' <- irCon env t arity n
308− (args ++ map (\n -> P Bound n undefined) extra)
309− return $ LLam extra sc'
310−
311− satArgs n = map (\i -> sMN i "sat") [1..n]
312−
313− buildApp env e [] = return e
314− buildApp env e xs = do xs' <- mapM (ir' env) xs
315− return $ LApp False e xs'
316−
317− doForeign :: [Name] -> [TT Name] -> Idris LExp
318− doForeign env (_ : fgn : args)
319− | (_, (Constant (Str fgnName) : fgnArgTys : ret : [])) <- unApply fgn
320− = let maybeTys = getFTypes fgnArgTys
321− rty = mkIty' ret in
322− case maybeTys of
323− Nothing -> ifail $ "Foreign type specification is not a constant list: " ++ show (fgn:args)
324− Just tys -> do
325− args' <- mapM (ir' env) (init args)
326− -- wrap it in a prim__IO
327− -- return $ con_ 0 @@ impossible @@
328− return $ -- LLazyExp $
329− LForeign LANG_C rty fgnName (zip tys args')
330− | otherwise = ifail "Badly formed foreign function call"
331−
332−getFTypes :: TT Name -> Maybe [FType]
333−getFTypes tm = case unApply tm of
334− -- nil : {a : Type} -> List a
335− (nil, [_]) -> Just []
336− -- cons : {a : Type} -> a -> List a -> List a
337− (cons, [_, ty, xs]) -> (mkIty' ty :) <$> getFTypes xs
338− _ -> Nothing
339−
340−mkIty' (P _ (UN ty) _) = mkIty (str ty)
341−mkIty' (App (P _ (UN fi) _) (P _ (UN intTy) _))
342− | fi == txt "FIntT" = mkIntIty (str intTy)
343−mkIty' (App (App (P _ (UN ff) _) _) (App (P _ (UN fa) _) (App (P _ (UN io) _) _)))
344− | ff == txt "FFunction" && fa == txt "FAny" &&
345− io == txt "IO"
328+irCon :: Vars -> [Name] -> Int -> Name -> [Term] -> Idris LExp
329+irCon vs env arity n args
330+ | length args > arity
331+ = error $ "oversaturated data constructor: " ++ show (n, args)
332+
333+ -- saturated
334+ | length args == arity
335+ = buildApp (LV (Glob n)) args
336+
337+ -- undersaturated, wrap in lambdas
338+ | otherwise
339+ = let extraNs = [sMN i "sat" | i <- [length args .. arity-1]]
340+ extraTs = [P Bound n undefined | n <- extraNs]
341+ in LLam extraNs <$> irCon vs env arity n (args ++ extraTs)
342+ where
343+ buildApp e [] = return e
344+ buildApp e xs = LApp False e <$> mapM (irTerm vs env) xs
345+
346+doForeign :: Vars -> [Name] -> [TT Name] -> Idris LExp
347+doForeign vs env (_ : fgn : args)
348+ | (_, (Constant (Str fgnName) : fgnArgTys : ret : [])) <- unApply fgn
349+ = case getFTypes fgnArgTys of
350+ Nothing -> ifail $ "Foreign type specification is not a constant list: " ++ show (fgn:args)
351+ Just tys -> do
352+ args' <- mapM (irTerm vs env) (init args)
353+ return $ LForeign LANG_C (mkIty' ret) fgnName (zip tys args')
354+
355+ | otherwise = ifail "Badly formed foreign function call"
356+ where
357+ getFTypes :: TT Name -> Maybe [FType]
358+ getFTypes tm = case unApply tm of
359+ -- nil : {a : Type} -> List a
360+ (nil, [_]) -> Just []
361+ -- cons : {a : Type} -> a -> List a -> List a
362+ (cons, [_, ty, xs]) -> (mkIty' ty :) <$> getFTypes xs
363+ _ -> Nothing
364+
365+ mkIty' (P _ (UN ty) _) = mkIty (str ty)
366+ mkIty' (App (P _ (UN fi) _) (P _ (UN intTy) _))
367+ | fi == txt "FIntT"
368+ = mkIntIty (str intTy)
369+
370+ mkIty' (App (App (P _ (UN ff) _) _) (App (P _ (UN fa) _) (App (P _ (UN io) _) _)))
371+ | ff == txt "FFunction"
372+ , fa == txt "FAny"
373+ , io == txt "IO"
346374 = FFunctionIO
347−mkIty' (App (App (P _ (UN ff) _) _) _)
348− | ff == txt "FFunction" = FFunction
349−mkIty' _ = FAny
350−
351−-- would be better if these FInt types were evaluated at compile time
352−-- TODO: add %eval directive for such things
353−
354−mkIty "FFloat" = FArith ATFloat
355−mkIty "FInt" = mkIntIty "ITNative"
356−mkIty "FChar" = mkIntIty "ITChar"
357−mkIty "FByte" = mkIntIty "IT8"
358−mkIty "FShort" = mkIntIty "IT16"
359−mkIty "FLong" = mkIntIty "IT64"
360−mkIty "FBits8" = mkIntIty "IT8"
361−mkIty "FBits16" = mkIntIty "IT16"
362−mkIty "FBits32" = mkIntIty "IT32"
363−mkIty "FBits64" = mkIntIty "IT64"
364−mkIty "FString" = FString
365−mkIty "FPtr" = FPtr
366−mkIty "FManagedPtr" = FManagedPtr
367−mkIty "FUnit" = FUnit
368−mkIty "FFunction" = FFunction
369−mkIty "FFunctionIO" = FFunctionIO
370−mkIty "FBits8x16" = FArith (ATInt (ITVec IT8 16))
371−mkIty "FBits16x8" = FArith (ATInt (ITVec IT16 8))
372−mkIty "FBits32x4" = FArith (ATInt (ITVec IT32 4))
373−mkIty "FBits64x2" = FArith (ATInt (ITVec IT64 2))
374−mkIty x = error $ "Unknown type " ++ x
375−
376−mkIntIty "ITNative" = FArith (ATInt ITNative)
377−mkIntIty "ITChar" = FArith (ATInt ITChar)
378−mkIntIty "IT8" = FArith (ATInt (ITFixed IT8))
379−mkIntIty "IT16" = FArith (ATInt (ITFixed IT16))
380−mkIntIty "IT32" = FArith (ATInt (ITFixed IT32))
381−mkIntIty "IT64" = FArith (ATInt (ITFixed IT64))
382−
383−zname = sNS (sUN "Z") ["Nat","Prelude"]
384−sname = sNS (sUN "S") ["Nat","Prelude"]
385−
386−instance ToIR ([Name], SC) where
387− ir (args, tree) = do logLvl 3 $ "Compiling " ++ show args ++ "\n" ++ show tree
388− tree' <- ir tree
389− return $ LLam args tree'
390−
391−instance ToIR SC where
392− ir t = ir' t where
393−
394− ir' (STerm t) = ir t
395− ir' (UnmatchedCase str) = return $ LError str
396− ir' (ProjCase tm alt) = do tm' <- ir tm
397− alt' <- mkIRAlt tm' alt
398− return $ LCase tm' [alt']
399−
400− -- There are two transformations in this case:
401− --
402− -- 1. Newtype-case elimination:
403− -- case {e0} of
404− -- wrap({e1}) -> P({e1}) ==> P({e0})
405− --
406− -- This is important because newtyped constructors are compiled away entirely
407− -- and we need to do that everywhere.
408− --
409− -- 2. Unused-case elimination:
410− -- case {e0} of ==> P
411− -- C(x,y) -> P[... x,y not used ...]
412− --
413− -- This is important for runtime because sometimes we case on irrelevant data:
414− --
415− -- In the example above, {e0} will most probably have been erased
416− -- so this vain projection would make the resulting program segfault
417− -- because the code generator still emits a PROJECT(...) STG instruction.
418− --
419− -- Hence, we check whether the variables are used at all
420− -- and erase the casesplit if they are not.
421− ir' (Case n [alt]) = do
422− replacement <- case alt of
423− ConCase cn a ns sc -> do
424− detag <- maybe False detaggable . lookupCtxtExact cn . idris_optimisation <$> getIState
425− used <- maybe [] (map fst . usedpos) . lookupCtxtExact cn . idris_callgraph <$> getIState
426− if detag && length used == 1
427− then return . Just $ substSC (ns !! head used) n sc
428− else return Nothing
429− _ -> return Nothing
430−
431− case replacement of
432− Just sc -> ir' sc
433− _ -> do
434− alt' <- mkIRAlt (LV (Glob n)) alt
435− return $ case namesBoundIn alt' `usedIn` subexpr alt' of
436− [] -> subexpr alt' -- strip the unused top-most case
437− _ -> LCase (LV (Glob n)) [alt']
438− where
439− namesBoundIn :: LAlt -> [Name]
440− namesBoundIn (LConCase cn i ns sc) = ns
441− namesBoundIn (LConstCase c sc) = []
442− namesBoundIn (LDefaultCase sc) = []
443−
444− subexpr :: LAlt -> LExp
445− subexpr (LConCase _ _ _ e) = e
446− subexpr (LConstCase _ e) = e
447− subexpr (LDefaultCase e) = e
448−
449− ir' (Case n alts) = do alts' <- mapM (mkIRAlt (LV (Glob n))) alts
450− return $ LCase (LV (Glob n)) alts'
451− ir' ImpossibleCase = return LNothing
452−
453− -- special cases for Z and S
454− -- Needs rethink: projections make this fail
455−-- mkIRAlt n (ConCase z _ [] rhs) | z == zname
456−-- = mkIRAlt n (ConstCase (BI 0) rhs)
457−-- mkIRAlt n (ConCase s _ [arg] rhs) | s == sname
375+
376+ mkIty' (App (App (P _ (UN ff) _) _) _)
377+ | ff == txt "FFunction"
378+ = FFunction
379+
380+ mkIty' _ = FAny
381+
382+ -- would be better if these FInt types were evaluated at compile time
383+ -- TODO: add %eval directive for such things
384+
385+ mkIty "FFloat" = FArith ATFloat
386+ mkIty "FInt" = mkIntIty "ITNative"
387+ mkIty "FChar" = mkIntIty "ITChar"
388+ mkIty "FByte" = mkIntIty "IT8"
389+ mkIty "FShort" = mkIntIty "IT16"
390+ mkIty "FLong" = mkIntIty "IT64"
391+ mkIty "FBits8" = mkIntIty "IT8"
392+ mkIty "FBits16" = mkIntIty "IT16"
393+ mkIty "FBits32" = mkIntIty "IT32"
394+ mkIty "FBits64" = mkIntIty "IT64"
395+ mkIty "FString" = FString
396+ mkIty "FPtr" = FPtr
397+ mkIty "FManagedPtr" = FManagedPtr
398+ mkIty "FUnit" = FUnit
399+ mkIty "FFunction" = FFunction
400+ mkIty "FFunctionIO" = FFunctionIO
401+ mkIty "FBits8x16" = FArith (ATInt (ITVec IT8 16))
402+ mkIty "FBits16x8" = FArith (ATInt (ITVec IT16 8))
403+ mkIty "FBits32x4" = FArith (ATInt (ITVec IT32 4))
404+ mkIty "FBits64x2" = FArith (ATInt (ITVec IT64 2))
405+ mkIty x = error $ "Unknown type " ++ x
406+
407+ mkIntIty "ITNative" = FArith (ATInt ITNative)
408+ mkIntIty "ITChar" = FArith (ATInt ITChar)
409+ mkIntIty "IT8" = FArith (ATInt (ITFixed IT8))
410+ mkIntIty "IT16" = FArith (ATInt (ITFixed IT16))
411+ mkIntIty "IT32" = FArith (ATInt (ITFixed IT32))
412+ mkIntIty "IT64" = FArith (ATInt (ITFixed IT64))
413+
414+irTree :: [Name] -> SC -> Idris LExp
415+irTree args tree = do
416+ logLvl 3 $ "Compiling " ++ show args ++ "\n" ++ show tree
417+ LLam args <$> irSC M.empty tree
418+
419+irSC :: Vars -> SC -> Idris LExp
420+irSC vs (STerm t) = irTerm vs [] t
421+irSC vs (UnmatchedCase str) = return $ LError str
422+irSC vs (ProjCase tm alt) = do
423+ tm' <- irTerm vs [] tm
424+ alt' <- irAlt vs tm' alt
425+ return $ LCase tm' [alt']
426+
427+-- There are two transformations in this case:
428+--
429+-- 1. Newtype-case elimination:
430+-- case {e0} of
431+-- wrap({e1}) -> P({e1}) ==> P({e0})
432+--
433+-- This is important because newtyped constructors are compiled away entirely
434+-- and we need to do that everywhere.
435+--
436+-- 2. Unused-case elimination:
437+-- case {e0} of ==> P
438+-- C(x,y) -> P[... x,y not used ...]
439+--
440+-- This is important for runtime because sometimes we case on irrelevant data:
441+--
442+-- In the example above, {e0} will most probably have been erased
443+-- so this vain projection would make the resulting program segfault
444+-- because the code generator still emits a PROJECT(...) STG instruction.
445+--
446+-- Hence, we check whether the variables are used at all
447+-- and erase the casesplit if they are not.
448+irSC vs (Case n [alt]) = do
449+ replacement <- case alt of
450+ ConCase cn a ns sc -> do
451+ detag <- maybe False detaggable . lookupCtxtExact cn . idris_optimisation <$> getIState
452+ used <- maybe [] (map fst . usedpos) . lookupCtxtExact cn . idris_callgraph <$> getIState
453+ if detag && length used == 1
454+ then return . Just $ substSC (ns !! head used) n sc
455+ else return Nothing
456+ _ -> return Nothing
457+
458+ case replacement of
459+ Just sc -> irSC vs sc
460+ _ -> do
461+ alt' <- irAlt vs (LV (Glob n)) alt
462+ return $ case namesBoundIn alt' `usedIn` subexpr alt' of
463+ [] -> subexpr alt' -- strip the unused top-most case
464+ _ -> LCase (LV (Glob n)) [alt']
465+ where
466+ namesBoundIn :: LAlt -> [Name]
467+ namesBoundIn (LConCase cn i ns sc) = ns
468+ namesBoundIn (LConstCase c sc) = []
469+ namesBoundIn (LDefaultCase sc) = []
470+
471+ subexpr :: LAlt -> LExp
472+ subexpr (LConCase _ _ _ e) = e
473+ subexpr (LConstCase _ e) = e
474+ subexpr (LDefaultCase e) = e
475+
476+irSC vs (Case n alts) = LCase (LV (Glob n)) <$> mapM (irAlt vs (LV (Glob n))) alts
477+irSC vs ImpossibleCase = return LNothing
478+
479+-- zname = sNS (sUN "Z") ["Nat","Prelude"]
480+-- sname = sNS (sUN "S") ["Nat","Prelude"]
481+
482+-- special cases for Z and S
483+-- Needs rethink: projections make this fail
484+-- irAlt n (ConCase z _ [] rhs) | z == zname
485+-- = irAlt n (ConstCase (BI 0) rhs)
486+-- irAlt n (ConCase s _ [arg] rhs) | s == sname
458487-- = do n' <- ir n
459488-- rhs' <- ir rhs
460489-- return $ LDefaultCase
461490-- (LLet arg (LOp LBMinus [n', LConst (BI 1)])
462491-- rhs')
463− mkIRAlt _ (ConCase n t args sc) = do
464− sc' <- ir sc
465− used <- maybe [] (map fst . usedpos) . lookupCtxtExact n . idris_callgraph <$> getIState
466− return $ LConCase (-1) n [a | (i,a) <- zip [0..] args, i `elem` used] sc'
467−
468− mkIRAlt _ (ConstCase x rhs)
469− | matchable x
470− = do rhs' <- ir rhs
471− return $ LConstCase x rhs'
472− | matchableTy x
473− = do rhs' <- ir rhs
474− return $ LDefaultCase rhs'
475− mkIRAlt tm (SucCase n rhs)
476− = do rhs' <- ir rhs
477− return $ LDefaultCase (LLet n (LOp (LMinus (ATInt ITBig))
478− [tm,
479− LConst (BI 1)]) rhs')
480−-- return $ LSucCase n rhs'
481− mkIRAlt _ (ConstCase c rhs)
482− = ifail $ "Can't match on (" ++ show c ++ ")"
483− mkIRAlt _ (DefaultCase rhs)
484− = do rhs' <- ir rhs
485− return $ LDefaultCase rhs'
486−
487− matchable (I _) = True
488− matchable (BI _) = True
489− matchable (Ch _) = True
490− matchable (Str _) = True
491− matchable _ = False
492−
493− matchableTy (AType (ATInt ITNative)) = True
494− matchableTy (AType (ATInt ITBig)) = True
495− matchableTy (AType (ATInt ITChar)) = True
496− matchableTy StrType = True
497−
498− matchableTy (AType (ATInt (ITFixed IT8))) = True
499− matchableTy (AType (ATInt (ITFixed IT16))) = True
500− matchableTy (AType (ATInt (ITFixed IT32))) = True
501− matchableTy (AType (ATInt (ITFixed IT64))) = True
502−
503− matchableTy _ = False
504492
493+irAlt :: Vars -> LExp -> CaseAlt -> Idris LAlt
494+
495+-- this leaves out all unused arguments of the constructor
496+irAlt vs _ (ConCase n t args sc) = do
497+ sc' <- irSC vs sc
498+ used <- maybe [] (map fst . usedpos) . lookupCtxtExact n . idris_callgraph <$> getIState
499+ return $ LConCase (-1) n [a | (i,a) <- zip [0..] args, i `elem` used] sc'
500+
501+irAlt vs _ (ConstCase x rhs)
502+ | matchable x = LConstCase x <$> irSC vs rhs
503+ | matchableTy x = LDefaultCase <$> irSC vs rhs
504+ where
505+ matchable (I _) = True
506+ matchable (BI _) = True
507+ matchable (Ch _) = True
508+ matchable (Str _) = True
509+ matchable _ = False
510+
511+ matchableTy (AType (ATInt ITNative)) = True
512+ matchableTy (AType (ATInt ITBig)) = True
513+ matchableTy (AType (ATInt ITChar)) = True
514+ matchableTy StrType = True
515+
516+ matchableTy (AType (ATInt (ITFixed IT8))) = True
517+ matchableTy (AType (ATInt (ITFixed IT16))) = True
518+ matchableTy (AType (ATInt (ITFixed IT32))) = True
519+ matchableTy (AType (ATInt (ITFixed IT64))) = True
520+
521+ matchableTy _ = False
522+
523+irAlt vs tm (SucCase n rhs) = do
524+ rhs' <- irSC vs rhs
525+ return $ LDefaultCase (LLet n (LOp (LMinus (ATInt ITBig))
526+ [tm,
527+ LConst (BI 1)]) rhs')
528+
529+irAlt vs _ (ConstCase c rhs)
530+ = ifail $ "Can't match on (" ++ show c ++ ")"
531+
532+irAlt vs _ (DefaultCase rhs)
533+ = LDefaultCase <$> irSC vs rhs