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