@@ -262,20 +262,67 @@ irTerm vs env tm@(App f a) = case unApply tm of
262 ,LConCase 1 (sNS (sUN "True" ) ["Bool","Prelude"]) [] t'
262 ,LConCase 1 (sNS (sUN "True" ) ["Bool","Prelude"]) [] t'
265 (P (DCon t arity) n _, args) -> do
266 (P (DCon t arity) n _, args) -> do
266 detag <- fgetState (opt_detaggable . ist_optimisation n)
267 detag <- fgetState (opt_detaggable . ist_optimisation n)
267 used <- map fst <$> fgetState (cg_usedpos . ist_callgraph n)
268 used <- map fst <$> fgetState (cg_usedpos . ist_callgraph n)
269− when (length args > arity) $
270+ let isNewtype = length used == 1 && detag
270− ifail ("oversaturated data ctor: " ++ show tm)
272− let args' = [a | (i,a) <- zip [0..] args, i `elem` used]
271+ let argsPruned = [a | (i,a) <- zip [0..] args, i `elem` used]
273− if length args' == 1 && detag -- detaggable
272+
273+ -- The following code removes fields from data constructors
274+ -- and performs the newtype optimisation.
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.
281+ -- It's only the data that leaves this point that's erased
282+ -- and possibly no longer typed as the original TT version.
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).
288+ -- This will probably need rethinking when we get erasure from functions.
290+ -- "padLams" will wrap our term in LLam-bdas and give us
291+ -- the "list of future unerased args" coming from these lambdas.
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
297+ case compare arity (length args) of
300+ GT -> ifail ("overapplied data constructor: " ++ show tm)
302+ -- exactly saturated
274− then irTerm vs env (head args') -- newtype
304+ -> irTerm vs env (head argsPruned)
275− else irCon vs env (length used) n args'
305+
276−
306+ | otherwise -- not newtype, plain data ctor
307+ -> buildApp (LV $ Glob n) argsPruned
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)
315+ | isNewtype -- newtype but the value is not among args yet
316+ -> return . padLams $ \[vn] -> LApp False (LV $ Glob n) [LV $ Glob vn]
318+ -- not a newtype, just apply to a constructor
320+ -> padLams . applyToNames <$> buildApp (LV $ Glob n) argsPruned
277 (P (TCon t a) n _, args) -> return LNothing
323 (P (TCon t a) n _, args) -> return LNothing
325+ -- a name applied to arguments
279 (P _ n _, args) -> do
326 (P _ n _, args) -> do
280 ist <- getIState
327 ist <- getIState
281 case lookup n (idris_scprims ist) of
328 case lookup n (idris_scprims ist) of
@@ -296,29 +343,44 @@ irTerm vs env tm@(App f a) = case unApply tm of
296 <*> mapM (irTerm vs env) args
343 <*> mapM (irTerm vs env) args
346+ buildApp :: LExp -> [Term] -> Idris LExp
347+ buildApp e [] = return e
348+ buildApp e xs = LApp False e <$> mapM (irTerm vs env) xs
350+ applyToNames :: LExp -> [Name] -> LExp
351+ applyToNames tm [] = tm
352+ applyToNames tm ns = LApp False tm $ map (LV . Glob) ns
354+ padLambdas :: [Int] -> Int -> Int -> ([Name] -> LExp) -> LExp
355+ padLambdas used startIdx endSIdx mkTerm
356+ = LLam allNames $ mkTerm nonerasedNames
358+ allNames = [sMN i "sat" | i <- [startIdx .. endSIdx-1]]
359+ nonerasedNames = [sMN i "sat" | i <- [startIdx .. endSIdx-1], i `elem` used]
299 applyName :: Name -> IState -> [Term] -> Idris LExp
361 applyName :: Name -> IState -> [Term] -> Idris LExp
300 applyName n ist args =
362 applyName n ist args =
301 LApp False (LV $ Glob n) <$> mapM (irTerm vs env . erase) (zip [0..] args)
363 LApp False (LV $ Glob n) <$> mapM (irTerm vs env . erase) (zip [0..] args)
303− erase (i, x)
365+ erase (i, x)
304− | i >= arity || i `elem` used = x
366+ | i >= arity || i `elem` used = x
305− | otherwise = Erased
367+ | otherwise = Erased
307− arity = case fst4 <$> lookupCtxtExact n (definitions . tt_ctxt $ ist) of
369+ arity = case fst4 <$> lookupCtxtExact n (definitions . tt_ctxt $ ist) of
308− Just (CaseOp ci ty tys def tot cdefs) -> length tys
370+ Just (CaseOp ci ty tys def tot cdefs) -> length tys
309− Just (TyDecl (DCon tag ar) _) -> ar
371+ Just (TyDecl (DCon tag ar) _) -> ar
310− Just (TyDecl Ref ty) -> length $ getArgTys ty
372+ Just (TyDecl Ref ty) -> length $ getArgTys ty
311− Just (Operator ty ar op) -> ar
373+ Just (Operator ty ar op) -> ar
312− Just def -> error $ "unknown arity: " ++ show (n, def)
374+ Just def -> error $ "unknown arity: " ++ show (n, def)
313− Nothing -> 0 -- no definition, probably local name => can't erase anything
375+ Nothing -> 0 -- no definition, probably local name => can't erase anything
315− -- name for purposes of usage info lookup
377+ -- name for purposes of usage info lookup
317− | Just n' <- viMethod =<< M.lookup n vs = n'
379+ | Just n' <- viMethod =<< M.lookup n vs = n'
318− | otherwise = n
380+ | otherwise = n
320− used = maybe [] (map fst . usedpos) $ lookupCtxtExact uName (idris_callgraph ist)
382+ used = maybe [] (map fst . usedpos) $ lookupCtxtExact uName (idris_callgraph ist)
321− fst4 (x,_,_,_) = x
383+ fst4 (x,_,_,_) = x
323irTerm vs env (P _ n _) = return $ LV (Glob n)
385irTerm vs env (P _ n _) = return $ LV (Glob n)
324irTerm vs env (V i)
386irTerm vs env (V i)
@@ -345,24 +407,6 @@ irTerm vs env (TType _) = return $ LNothing
345irTerm vs env Erased = return $ LNothing
407irTerm vs env Erased = return $ LNothing
346irTerm vs env Impossible = return $ LNothing
408irTerm vs env Impossible = return $ LNothing
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)
354− | length args == arity
355− = buildApp (LV (Glob n)) args
357− -- undersaturated, wrap in lambdas
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)
363− buildApp e [] = return e
364− buildApp e xs = LApp False e <$> mapM (irTerm vs env) xs
366doForeign :: Vars -> [Name] -> [TT Name] -> Idris LExp
410doForeign :: Vars -> [Name] -> [TT Name] -> Idris LExp
367doForeign vs env (_ : fgn : args)
411doForeign vs env (_ : fgn : args)
368 | (_, (Constant (Str fgnName) : fgnArgTys : ret : [])) <- unApply fgn
412 | (_, (Constant (Str fgnName) : fgnArgTys : ret : [])) <- unApply fgn
@@ -470,6 +514,7 @@ irSC vs (Case n [ConCase (UN delay) i [_, _, n'] sc])
471-- Hence, we check whether the variables are used at all
515-- Hence, we check whether the variables are used at all
472-- and erase the casesplit if they are not.
516-- and erase the casesplit if they are not.
473irSC vs (Case n [alt]) = do
518irSC vs (Case n [alt]) = do
474 replacement <- case alt of
519 replacement <- case alt of
475 ConCase cn a ns sc -> do
520 ConCase cn a ns sc -> do
@@ -498,7 +543,41 @@ irSC vs (Case n [alt]) = do
498 subexpr (LConstCase _ e) = e
543 subexpr (LConstCase _ e) = e
499 subexpr (LDefaultCase e) = e
544 subexpr (LDefaultCase e) = e
546+-- FIXME: When we have a non-singleton case-tree of the form
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.
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.
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.
562+irSC vs (Case n alts@[ConCase cn a ns sc, DefaultCase sc']) = do
563+ detag <- fgetState (opt_detaggable . ist_optimisation cn)
565+ then irSC vs (Case n [ConCase cn a ns sc])
501−irSC vs (Case n alts) = LCase (LV (Glob n)) <$> mapM (irAlt vs (LV (Glob n))) alts
566+ else LCase (LV (Glob n)) <$> mapM (irAlt vs (LV (Glob n))) alts
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
573+ $ ifail ("irSC: non-trivial case-match on detaggable data: " ++ show sc)
576+ LCase (LV (Glob n)) <$> mapM (irAlt vs (LV (Glob n))) alts
578+ isDetaggable (ConCase cn _ _ _) = fgetState $ opt_detaggable . ist_optimisation cn
579+ isDetaggable _ = return False
502irSC vs ImpossibleCase = return LNothing
581irSC vs ImpossibleCase = return LNothing
504irAlt :: Vars -> LExp -> CaseAlt -> Idris LAlt
583irAlt :: Vars -> LExp -> CaseAlt -> Idris LAlt