@@ -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,9 +343,24 @@ 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
@@ -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