@@ -151,14 +151,8 @@ mkLDecl n (CaseOp ci _ _ _ pats cd)
151151 do e <- ir (args, sc)
152152 return (declArgs [] (case_inlinable ci) n e)
153153
154−mkLDecl n (TyDecl (DCon tag arity) _) = do
155− ist <- getIState
156−
157− let realArity = case lookupCtxt n (idris_callgraph ist) of
158− [CGInfo _ _ _ _ xs] -> length xs
159− _ -> arity
160−
161− return $ LConstructor n tag realArity
154+mkLDecl n (TyDecl (DCon tag arity) _) =
155+ LConstructor n tag . maybe arity (length . usedpos) . lookupCtxtExact n . idris_callgraph <$> getIState
162156
163157mkLDecl n (TyDecl (TCon t a) _) = return $ LConstructor n (-1) a
164158mkLDecl n _ = return $ (declArgs [] True n LNothing) -- postulate, never run
@@ -166,80 +160,87 @@ mkLDecl n _ = return $ (declArgs [] True n LNothing) -- postulate, never run
166160instance ToIR (TT Name) where
167161 ir tm = ir' [] tm where
168162 ir' env tm@(App f a)
169− | (P _ (UN m) _, args) <- unApply tm,
163+ | (P _ (UN m) _, args) <- unApply tm,
170164 m == txt "mkForeignPrim"
171− = doForeign env args
172− | (P _ (UN u) _, [_, arg]) <- unApply tm,
165+ = doForeign env args
166+ | (P _ (UN u) _, [_, arg]) <- unApply tm,
173167 u == txt "unsafePerformPrimIO"
174− = ir' env arg
168+ = ir' env arg
175169 -- TMP HACK - until we get inlining.
176− | (P _ (UN r) _, [_, _, _, _, _, arg]) <- unApply tm,
170+ | (P _ (UN r) _, [_, _, _, _, _, arg]) <- unApply tm,
177171 r == txt "replace"
178− = ir' env arg
179− -- Laziness, the old way
180− | (P _ (UN l) _, [_, arg]) <- unApply tm,
172+ = ir' env arg
173+ -- Laziness, the old way
174+ | (P _ (UN l) _, [_, arg]) <- unApply tm,
181175 l == txt "lazy"
182− = do arg' <- ir' env arg
183− error "lazy has crept in somehow"
176+ = do arg' <- ir' env arg
177+ error "lazy has crept in somehow"
184178-- return $ LLazyExp arg'
185− | (P _ (UN l) _, [_, arg]) <- unApply tm,
179+ | (P _ (UN l) _, [_, arg]) <- unApply tm,
186180 l == txt "force"
187− = do arg' <- ir' env arg
188− return $ LForce arg'
189− -- Laziness, the new way
190− | (P _ (UN l) _, [_, arg]) <- unApply tm,
181+ = do arg' <- ir' env arg
182+ return $ LForce arg'
183+ -- Laziness, the new way
184+ | (P _ (UN l) _, [_, arg]) <- unApply tm,
191185 l == txt "Delay"
192− = do arg' <- ir' env arg
193− return $ LLazyExp arg'
194− | (P _ (UN l) _, [_, _, arg]) <- unApply tm,
186+ = do arg' <- ir' env arg
187+ return $ LLazyExp arg'
188+ | (P _ (UN l) _, [_, arg]) <- unApply tm,
195189 l == txt "Force"
196− = do arg' <- ir' env arg
197− return $ LForce arg'
198− | (P _ (UN a) _, [_, _, arg]) <- unApply tm,
190+ = do arg' <- ir' env arg
191+ return $ LForce arg'
192+ | (P _ (UN a) _, [_, _, arg]) <- unApply tm,
199193 a == txt "assert_smaller"
200− = ir' env arg
201− | (P _ (UN a) _, [_, arg]) <- unApply tm,
194+ = ir' env arg
195+ | (P _ (UN a) _, [_, arg]) <- unApply tm,
202196 a == txt "assert_total"
203− = ir' env arg
204− | (P _ (UN p) _, [_, arg]) <- unApply tm,
197+ = ir' env arg
198+ | (P _ (UN p) _, [_, arg]) <- unApply tm,
205199 p == txt "par"
206− = do arg' <- ir' env arg
207− return $ LOp LPar [LLazyExp arg']
208− | (P _ (UN pf) _, [arg]) <- unApply tm,
200+ = do arg' <- ir' env arg
201+ return $ LOp LPar [LLazyExp arg']
202+ | (P _ (UN pf) _, [arg]) <- unApply tm,
209203 pf == txt "prim_fork"
210− = do arg' <- ir' env arg
211− return $ LOp LFork [LLazyExp arg']
212− | (P _ (UN m) _, [_,size,t]) <- unApply tm,
204+ = do arg' <- ir' env arg
205+ return $ LOp LFork [LLazyExp arg']
206+ | (P _ (UN m) _, [_,size,t]) <- unApply tm,
213207 m == txt "malloc"
214− = do size' <- ir' env size
215− t' <- ir' env t
216− return t' -- TODO $ malloc_ size' t'
217− | (P _ (UN tm) _, [_,t]) <- unApply tm,
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,
218212 tm == txt "trace_malloc"
219− = do t' <- ir' env t
220− return t' -- TODO
213+ = do t' <- ir' env t
214+ return t' -- TODO
221215
222− -- This case is here until we get more general inlining. It's just
223− -- a really common case, and the laziness hurts...
224− | (P _ (NS (UN be) [b,p]) _, [_,x,(App (P _ (UN d) _) t),
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),
225219 (App (P _ (UN d') _) e)]) <- unApply tm,
226220 be == txt "boolElim" && d == txt "Delay" && d' == txt "Delay"
227− = do x' <- ir' env x
228− t' <- ir' env t
229− e' <- ir' env e
230− return (LCase x' [LConCase 0 (sNS (sUN "False") ["Bool","Prelude"]) [] e',
231− LConCase 1 (sNS (sUN "True") ["Bool","Prelude"]) [] t'])
232−
233− | (P (DCon t a) n _, args) <- unApply tm = do
234− cg <- idris_callgraph <$> getIState
235− let used = maybe [] (map fst . usedpos) $ lookupCtxtExact n cg
236− args' = [if i `elem` used then a else Erased | (i,a) <- zip [0..] args]
237− irCon env t a n args'
238−
239− | (P (TCon t a) n _, args) <- unApply tm
240− = return LNothing
241−
242− | (P _ n _, args) <- unApply tm = do
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
243244 ist <- getIState
244245 case lookup n (idris_scprims ist) of
245246 -- if it's a primitive which is already saturated,
@@ -249,39 +250,28 @@ instance ToIR (TT Name) where
249250
250251 _ -> applyName n ist args
251252
252−{- collapsibility is turned off for now
253− _
254− -- if it's collapsible, compile to LNothing
255− | (collapsible <$> lookupCtxtExact n (idris_optimisation ist)) == Just True
256− -> return LNothing
257−
258− -- otherwise, compile normally
259− | otherwise -> applyName n ist args
260−
261−-}
262−
263− | (f, args) <- unApply tm
264− = do f' <- ir' env f
265− args' <- mapM (ir' env) args
266− return (LApp False f' args')
253+ | (f, args) <- unApply tm
254+ = do f' <- ir' env f
255+ args' <- mapM (ir' env) args
256+ return (LApp False f' args')
267257
268− where
258+ where
269259 applyName :: Name -> IState -> [Term] -> Idris LExp
270260 applyName n ist args =
271261 LApp False (LV $ Glob n) <$> mapM (ir' env . erase) (zip [0..] args)
272− where
273− erase (i, x)
274− | i >= arity || i `elem` used = x
275− | otherwise = Erased
276−
277− arity = case fst4 <$> lookupCtxt n (definitions . tt_ctxt $ ist) of
278− [CaseOp ci ty tys def tot cdefs] -> length tys
279− [TyDecl (DCon tag ar) _] -> ar
280− [Operator ty ar op] -> ar
281− _ -> 0
282−
283− used = maybe [] (map fst . usedpos) $ lookupCtxtExact n (idris_callgraph ist)
284− fst4 (x,_,_,_) = x
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+ [Operator ty ar op] -> ar
271+ _ -> 0
272+
273+ used = maybe [] (map fst . usedpos) $ lookupCtxtExact n (idris_callgraph ist)
274+ fst4 (x,_,_,_) = x
285275
286276-- ir' env (P _ (NS (UN "Z") ["Nat", "Prelude"]) _)
287277-- = return $ LConst (BI 0)