@@ -274,120 +274,123 @@ elabClauses :: ElabInfo -> FC -> FnOpts -> Name -> [PClause] -> Idris ()
274274elabClauses info fc opts n_in cs = let n = liftname info n_in in
275275 do ctxt <- getContext
276276 -- Check n actually exists
277− fty <- case lookupTy Nothing n ctxt of
278− [] -> -- TODO: turn into a CAF if there's no arguments
279− -- question: CAFs in where blocks?
280− tclift $ tfail $ (At fc (NoTypeDecl n))
281− [ty] -> return ty
282− pats_in <- mapM (elabClause info (TCGen `elem` opts))
283− (zip [0..] cs)
284− -- if the return type of 'ty' is collapsible, the optimised version should
285− -- just do nothing
286− ist <- get
287− let (ap, _) = unApply (getRetTy fty)
288− logLvl 5 $ "Checking collapsibility of " ++ show (ap, fty)
289− -- FIXME: Really ought to only do this for total functions!
290− let doNothing = case ap of
291− P _ tn _ -> case lookupCtxt Nothing tn
292− (idris_optimisation ist) of
293− [oi] -> collapsible oi
294− _ -> False
295− _ -> False
296− solveDeferred n
297− ist <- get
298− when doNothing $
299− case lookupCtxt Nothing n (idris_optimisation ist) of
300− [oi] -> do let opts = addDef n (oi { collapsible = True })
301− (idris_optimisation ist)
302− put (ist { idris_optimisation = opts })
303− _ -> do let opts = addDef n (Optimise True [] [])
304− (idris_optimisation ist)
305− put (ist { idris_optimisation = opts })
306− addIBC (IBCOpt n)
307− ist <- get
308− let pats = pats_in
309−-- logLvl 3 (showSep "\n" (map (\ (l,r) ->
310−-- show l ++ " = " ++
311−-- show r) pats))
312− let tcase = opt_typecase (idris_options ist)
313− let pdef = map debind $ map (simpl False (tt_ctxt ist)) pats
314−
315− numArgs <- tclift $ sameLength pdef
316−
317− optpats <- if doNothing
318− then return $ [Right (mkApp (P Bound n Erased)
319− (take numArgs (repeat Erased)), Erased)]
320− else stripCollapsed pats
321−
322− logLvl 5 $ "Patterns:\n" ++ show pats
323−
324− let optpdef = map debind $ map (simpl True (tt_ctxt ist)) optpats
325− tree@(CaseDef scargs sc _) <- tclift $
326− simpleCase tcase False CompileTime fc pdef
327− cov <- coverage
328− pmissing <-
329− if cov
330− then do missing <- genClauses fc n (map getLHS pdef) cs
331− -- missing <- genMissing n scargs sc
332− missing' <- filterM (checkPossible info fc True n) missing
333− logLvl 2 $ "Must be unreachable:\n" ++
334− showSep "\n" (map (showImp True) missing') ++
335− "\nAgainst: " ++
336− showSep "\n" (map (\t -> showImp True (delab ist t)) (map getLHS pdef))
337− return missing'
338− else return []
339− let pcover = null pmissing
340− pdef' <- applyOpts optpdef
341− logLvl 5 $ "Optimised patterns:\n" ++ show pdef'
342− ist <- get
343−-- let wf = wellFounded ist n sc
344− let tot = if pcover || AssertTotal `elem` opts
345− then Unchecked -- finish checking later
346− else Partial NotCovering -- already know it's not total
347−-- case lookupCtxt (namespace info) n (idris_flags ist) of
348−-- [fs] -> if TotalFn `elem` fs
349−-- then case tot of
350−-- Total _ -> return ()
351−-- t -> tclift $ tfail (At fc (Msg (show n ++ " is " ++ show t)))
352−-- else return ()
353−-- _ -> return ()
354− case tree of
355− CaseDef _ _ [] -> return ()
356− CaseDef _ _ xs -> mapM_ (\x ->
357− iputStrLn $ show fc ++
358− ":warning - Unreachable case: " ++
359− show (delab ist x)) xs
360− let knowncovering = pcover && cov
361−
362− tree' <- tclift $ simpleCase tcase knowncovering RunTime fc pdef'
363− logLvl 3 (show tree)
364− logLvl 3 $ "Optimised: " ++ show tree'
365− ctxt <- getContext
366− ist <- get
367− put (ist { idris_patdefs = addDef n pdef' (idris_patdefs ist) })
368− case lookupTy (namespace info) n ctxt of
369− [ty] -> do updateContext (addCasedef n (inlinable opts)
370− tcase knowncovering pats
371− pdef pdef' ty)
372− addIBC (IBCDef n)
373− setTotality n tot
374− totcheck (fc, n)
375− when (tot /= Unchecked) $ addIBC (IBCTotal n tot)
376− i <- get
377− case lookupDef Nothing n (tt_ctxt i) of
378− (CaseOp _ _ _ _ _ scargs sc scargs' sc' : _) ->
379− do let calls = findCalls sc' scargs'
380− let used = findUsedArgs sc' scargs'
381− -- let scg = buildSCG i sc scargs
382− -- add SCG later, when checking totality
383− let cg = CGInfo scargs' calls [] used []
384− logLvl 2 $ "Called names: " ++ show cg
385− addToCG n cg
386− addToCalledG n (nub (map fst calls)) -- plus names in type!
387− addIBC (IBCCG n)
388− _ -> return ()
389−-- addIBC (IBCTotal n tot)
390− [] -> return ()
277+ let tys = lookupTy Nothing n ctxt
278+ unless (length tys > 1) $ do
279+ fty <- case tys of
280+ [] -> -- TODO: turn into a CAF if there's no arguments
281+ -- question: CAFs in where blocks?
282+ tclift $ tfail $ At fc (NoTypeDecl n)
283+ [ty] -> return ty
284+ pats_in <- mapM (elabClause info (TCGen `elem` opts))
285+ (zip [0..] cs)
286+ -- if the return type of 'ty' is collapsible, the optimised version should
287+ -- just do nothing
288+ ist <- get
289+ let (ap, _) = unApply (getRetTy fty)
290+ logLvl 5 $ "Checking collapsibility of " ++ show (ap, fty)
291+ -- FIXME: Really ought to only do this for total functions!
292+ let doNothing = case ap of
293+ P _ tn _ -> case lookupCtxt Nothing tn
294+ (idris_optimisation ist) of
295+ [oi] -> collapsible oi
296+ _ -> False
297+ _ -> False
298+ solveDeferred n
299+ ist <- get
300+ when doNothing $
301+ case lookupCtxt Nothing n (idris_optimisation ist) of
302+ [oi] -> do let opts = addDef n (oi { collapsible = True })
303+ (idris_optimisation ist)
304+ put (ist { idris_optimisation = opts })
305+ _ -> do let opts = addDef n (Optimise True [] [])
306+ (idris_optimisation ist)
307+ put (ist { idris_optimisation = opts })
308+ addIBC (IBCOpt n)
309+ ist <- get
310+ let pats = pats_in
311+ -- logLvl 3 (showSep "\n" (map (\ (l,r) ->
312+ -- show l ++ " = " ++
313+ -- show r) pats))
314+ let tcase = opt_typecase (idris_options ist)
315+ let pdef = map debind $ map (simpl False (tt_ctxt ist)) pats
316+
317+ numArgs <- tclift $ sameLength pdef
318+
319+ optpats <- if doNothing
320+ then return $ [Right (mkApp (P Bound n Erased)
321+ (take numArgs (repeat Erased)), Erased)]
322+ else stripCollapsed pats
323+
324+ logLvl 5 $ "Patterns:\n" ++ show pats
325+
326+ let optpdef = map debind $ map (simpl True (tt_ctxt ist)) optpats
327+ tree@(CaseDef scargs sc _) <- tclift $
328+ simpleCase tcase False CompileTime fc pdef
329+ cov <- coverage
330+ pmissing <-
331+ if cov
332+ then do missing <- genClauses fc n (map getLHS pdef) cs
333+ -- missing <- genMissing n scargs sc
334+ missing' <- filterM (checkPossible info fc True n) missing
335+ logLvl 2 $ "Must be unreachable:\n" ++
336+ showSep "\n" (map (showImp True) missing') ++
337+ "\nAgainst: " ++
338+ showSep "\n" (map (\t -> showImp True (delab ist t)) (map getLHS pdef))
339+ return missing'
340+ else return []
341+ let pcover = null pmissing
342+ pdef' <- applyOpts optpdef
343+ logLvl 5 $ "Optimised patterns:\n" ++ show pdef'
344+ ist <- get
345+ -- let wf = wellFounded ist n sc
346+ let tot = if pcover || AssertTotal `elem` opts
347+ then Unchecked -- finish checking later
348+ else Partial NotCovering -- already know it's not total
349+ -- case lookupCtxt (namespace info) n (idris_flags ist) of
350+ -- [fs] -> if TotalFn `elem` fs
351+ -- then case tot of
352+ -- Total _ -> return ()
353+ -- t -> tclift $ tfail (At fc (Msg (show n ++ " is " ++ show t)))
354+ -- else return ()
355+ -- _ -> return ()
356+ case tree of
357+ CaseDef _ _ [] -> return ()
358+ CaseDef _ _ xs -> mapM_ (\x ->
359+ iputStrLn $ show fc ++
360+ ":warning - Unreachable case: " ++
361+ show (delab ist x)) xs
362+ let knowncovering = pcover && cov
363+
364+ tree' <- tclift $ simpleCase tcase knowncovering RunTime fc pdef'
365+ logLvl 3 (show tree)
366+ logLvl 3 $ "Optimised: " ++ show tree'
367+ ctxt <- getContext
368+ ist <- get
369+ put (ist { idris_patdefs = addDef n pdef' (idris_patdefs ist) })
370+ case lookupTy (namespace info) n ctxt of
371+ [ty] -> do updateContext (addCasedef n (inlinable opts)
372+ tcase knowncovering pats
373+ pdef pdef' ty)
374+ addIBC (IBCDef n)
375+ setTotality n tot
376+ totcheck (fc, n)
377+ when (tot /= Unchecked) $ addIBC (IBCTotal n tot)
378+ i <- get
379+ case lookupDef Nothing n (tt_ctxt i) of
380+ (CaseOp _ _ _ _ _ scargs sc scargs' sc' : _) ->
381+ do let calls = findCalls sc' scargs'
382+ let used = findUsedArgs sc' scargs'
383+ -- let scg = buildSCG i sc scargs
384+ -- add SCG later, when checking totality
385+ let cg = CGInfo scargs' calls [] used []
386+ logLvl 2 $ "Called names: " ++ show cg
387+ addToCG n cg
388+ addToCalledG n (nub (map fst calls)) -- plus names in type!
389+ addIBC (IBCCG n)
390+ _ -> return ()
391+ -- addIBC (IBCTotal n tot)
392+ [] -> return ()
393+ return ()
391394 where
392395 debind (Right (x, y)) = let (vs, x') = depat [] x
393396 (_, y') = depat [] y in