@@ -262,20 +262,67 @@ irTerm vs env tm@(App f a) = case unApply tm of
262262 ,LConCase 1 (sNS (sUN "True" ) ["Bool","Prelude"]) [] t'
263263 ])
264264
265+ -- data constructor
265266 (P (DCon t arity) n _, args) -> do
266267 detag <- fgetState (opt_detaggable . ist_optimisation n)
267268 used <- map fst <$> fgetState (cg_usedpos . ist_callgraph n)
268269
269− when (length args > arity) $
270− ifail ("oversaturated data ctor: " ++ show tm)
271−
272− let args' = [a | (i,a) <- zip [0..] args, i `elem` used]
273− if length args' == 1 && detag -- detaggable
274− then irTerm vs env (head args') -- newtype
275− else irCon vs env (length used) n args'
276−
270+ let isNewtype = length used == 1 && detag
271+ let argsPruned = [a | (i,a) <- zip [0..] args, i `elem` used]
272+
273+ -- The following code removes fields from data constructors
274+ -- and performs the newtype optimisation.
275+ --
276+ -- The general rule here is:
277+ -- Everything we get as input is not touched by erasure,
278+ -- so it conforms to the official arities and types
279+ -- and we can reason about it like it's plain TT.
280+ --
281+ -- It's only the data that leaves this point that's erased
282+ -- and possibly no longer typed as the original TT version.
283+ --
284+ -- Especially, underapplied constructors must yield functions
285+ -- even if all the remaining arguments are erased
286+ -- (the resulting function *will* be applied, to NULLs).
287+ --
288+ -- This will probably need rethinking when we get erasure from functions.
289+
290+ -- "padLams" will wrap our term in LLam-bdas and give us
291+ -- the "list of future unerased args" coming from these lambdas.
292+ --
293+ -- We can do whatever we like with the list of unerased args,
294+ -- hence it takes a lambda: \unerased_argname_list -> resulting_LExp.
295+ let padLams = padLambdas used (length args) arity
296+
297+ case compare arity (length args) of
298+
299+ -- overapplied
300+ GT -> ifail ("overapplied data constructor: " ++ show tm)
301+
302+ -- exactly saturated
303+ EQ | isNewtype
304+ -> irTerm vs env (head argsPruned)
305+
306+ | otherwise -- not newtype, plain data ctor
307+ -> buildApp (LV $ Glob n) argsPruned
308+
309+ -- not saturated, underapplied
310+ LT | isNewtype -- newtype
311+ , length argsPruned == 1 -- and we already have the value
312+ -> padLams . (\tm [] -> tm) -- the [] asserts there are no unerased args
313+ <$> irTerm vs env (head argsPruned)
314+
315+ | isNewtype -- newtype but the value is not among args yet
316+ -> return . padLams $ \[vn] -> LApp False (LV $ Glob n) [LV $ Glob vn]
317+
318+ -- not a newtype, just apply to a constructor
319+ | otherwise
320+ -> padLams . applyToNames <$> buildApp (LV $ Glob n) argsPruned
321+
322+ -- type constructor
277323 (P (TCon t a) n _, args) -> return LNothing
278324
325+ -- a name applied to arguments
279326 (P _ n _, args) -> do
280327 ist <- getIState
281328 case lookup n (idris_scprims ist) of
@@ -296,29 +343,44 @@ irTerm vs env tm@(App f a) = case unApply tm of
296343 <*> mapM (irTerm vs env) args
297344
298345 where
346+ buildApp :: LExp -> [Term] -> Idris LExp
347+ buildApp e [] = return e
348+ buildApp e xs = LApp False e <$> mapM (irTerm vs env) xs
349+
350+ applyToNames :: LExp -> [Name] -> LExp
351+ applyToNames tm [] = tm
352+ applyToNames tm ns = LApp False tm $ map (LV . Glob) ns
353+
354+ padLambdas :: [Int] -> Int -> Int -> ([Name] -> LExp) -> LExp
355+ padLambdas used startIdx endSIdx mkTerm
356+ = LLam allNames $ mkTerm nonerasedNames
357+ where
358+ allNames = [sMN i "sat" | i <- [startIdx .. endSIdx-1]]
359+ nonerasedNames = [sMN i "sat" | i <- [startIdx .. endSIdx-1], i `elem` used]
360+
299361 applyName :: Name -> IState -> [Term] -> Idris LExp
300362 applyName n ist args =
301363 LApp False (LV $ Glob n) <$> mapM (irTerm vs env . erase) (zip [0..] args)
302− where
303− erase (i, x)
304− | i >= arity || i `elem` used = x
305− | otherwise = Erased
306−
307− arity = case fst4 <$> lookupCtxtExact n (definitions . tt_ctxt $ ist) of
308− Just (CaseOp ci ty tys def tot cdefs) -> length tys
309− Just (TyDecl (DCon tag ar) _) -> ar
310− Just (TyDecl Ref ty) -> length $ getArgTys ty
311− Just (Operator ty ar op) -> ar
312− Just def -> error $ "unknown arity: " ++ show (n, def)
313− Nothing -> 0 -- no definition, probably local name => can't erase anything
314−
315− -- name for purposes of usage info lookup
316− uName
317− | Just n' <- viMethod =<< M.lookup n vs = n'
318− | otherwise = n
319−
320− used = maybe [] (map fst . usedpos) $ lookupCtxtExact uName (idris_callgraph ist)
321− fst4 (x,_,_,_) = x
364+ where
365+ erase (i, x)
366+ | i >= arity || i `elem` used = x
367+ | otherwise = Erased
368+
369+ arity = case fst4 <$> lookupCtxtExact n (definitions . tt_ctxt $ ist) of
370+ Just (CaseOp ci ty tys def tot cdefs) -> length tys
371+ Just (TyDecl (DCon tag ar) _) -> ar
372+ Just (TyDecl Ref ty) -> length $ getArgTys ty
373+ Just (Operator ty ar op) -> ar
374+ Just def -> error $ "unknown arity: " ++ show (n, def)
375+ Nothing -> 0 -- no definition, probably local name => can't erase anything
376+
377+ -- name for purposes of usage info lookup
378+ uName
379+ | Just n' <- viMethod =<< M.lookup n vs = n'
380+ | otherwise = n
381+
382+ used = maybe [] (map fst . usedpos) $ lookupCtxtExact uName (idris_callgraph ist)
383+ fst4 (x,_,_,_) = x
322384
323385irTerm vs env (P _ n _) = return $ LV (Glob n)
324386irTerm vs env (V i)
@@ -345,24 +407,6 @@ irTerm vs env (TType _) = return $ LNothing
345407irTerm vs env Erased = return $ LNothing
346408irTerm vs env Impossible = return $ LNothing
347409
348−irCon :: Vars -> [Name] -> Int -> Name -> [Term] -> Idris LExp
349−irCon vs env arity n args
350− | length args > arity
351− = error $ "oversaturated data constructor: " ++ show (n, args)
352−
353− -- saturated
354− | length args == arity
355− = buildApp (LV (Glob n)) args
356−
357− -- undersaturated, wrap in lambdas
358− | otherwise
359− = let extraNs = [sMN i "sat" | i <- [length args .. arity-1]]
360− extraTs = [P Bound n undefined | n <- extraNs]
361− in LLam extraNs <$> irCon vs env arity n (args ++ extraTs)
362− where
363− buildApp e [] = return e
364− buildApp e xs = LApp False e <$> mapM (irTerm vs env) xs
365−
366410doForeign :: Vars -> [Name] -> [TT Name] -> Idris LExp
367411doForeign vs env (_ : fgn : args)
368412 | (_, (Constant (Str fgnName) : fgnArgTys : ret : [])) <- unApply fgn
@@ -470,6 +514,7 @@ irSC vs (Case n [ConCase (UN delay) i [_, _, n'] sc])
470514--
471515-- Hence, we check whether the variables are used at all
472516-- and erase the casesplit if they are not.
517+--
473518irSC vs (Case n [alt]) = do
474519 replacement <- case alt of
475520 ConCase cn a ns sc -> do
@@ -498,7 +543,41 @@ irSC vs (Case n [alt]) = do
498543 subexpr (LConstCase _ e) = e
499544 subexpr (LDefaultCase e) = e
500545
501−irSC vs (Case n alts) = LCase (LV (Glob n)) <$> mapM (irAlt vs (LV (Glob n))) alts
546+-- FIXME: When we have a non-singleton case-tree of the form
547+--
548+-- case {e0} of
549+-- C(x) => ...
550+-- ... => ...
551+--
552+-- and C is detaggable (the only constructor of the family), we can be sure
553+-- that the first branch will be always taken -- so we add special handling
554+-- to remove the dead default branch.
555+--
556+-- If we don't do so and C is newtype-optimisable, we will miss this newtype
557+-- transformation and the resulting code will probably segfault.
558+--
559+-- This work-around is not entirely optimal; the best approach would be
560+-- to ensure that such case trees don't arise in the first place.
561+--
562+irSC vs (Case n alts@[ConCase cn a ns sc, DefaultCase sc']) = do
563+ detag <- fgetState (opt_detaggable . ist_optimisation cn)
564+ if detag
565+ then irSC vs (Case n [ConCase cn a ns sc])
566+ else LCase (LV (Glob n)) <$> mapM (irAlt vs (LV (Glob n))) alts
567+
568+irSC vs sc@(Case n alts) = do
569+ -- check that neither alternative needs the newtype optimisation,
570+ -- see comment above
571+ goneWrong <- or <$> mapM isDetaggable alts
572+ when goneWrong
573+ $ ifail ("irSC: non-trivial case-match on detaggable data: " ++ show sc)
574+
575+ -- everything okay
576+ LCase (LV (Glob n)) <$> mapM (irAlt vs (LV (Glob n))) alts
577+ where
578+ isDetaggable (ConCase cn _ _ _) = fgetState $ opt_detaggable . ist_optimisation cn
579+ isDetaggable _ = return False
580+
502581irSC vs ImpossibleCase = return LNothing
503582
504583irAlt :: Vars -> LExp -> CaseAlt -> Idris LAlt