51f3340 · Idris-dev · git.iko.soy

git.iko.soy/Idris-dev

on master help sign in

Merge pull request #99 from raichoo/master

51f3340Edwin Brady14 years ago

src/Idris/ElabDecls.hs+117−114

compare with master

unifiedsplit

@@ -298,120 +298,123 @@ elabClauses :: ElabInfo -> FC -> FnOpts -> Name -> [PClause] -> Idris ()

298elabClauses info fc opts n_in cs = let n = liftname info n_in in

299 do ctxt <- getContext

300 -- Check n actually exists

301− fty <- case lookupTy Nothing n ctxt of

301+ let tys = lookupTy Nothing n ctxt

302+ unless (length tys > 1) $ do

303+ fty <- case tys of

302− [] -> -- TODO: turn into a CAF if there's no arguments

304+ [] -> -- TODO: turn into a CAF if there's no arguments

303− -- question: CAFs in where blocks?

305+ -- question: CAFs in where blocks?

304− tclift $ tfail $ (At fc (NoTypeDecl n))

306+ tclift $ tfail $ At fc (NoTypeDecl n)

305− [ty] -> return ty

307+ [ty] -> return ty

306− pats_in <- mapM (elabClause info (TCGen `elem` opts))

308+ pats_in <- mapM (elabClause info (TCGen `elem` opts))

307− (zip [0..] cs)

309+ (zip [0..] cs)

308− -- if the return type of 'ty' is collapsible, the optimised version should

310+ -- if the return type of 'ty' is collapsible, the optimised version should

309− -- just do nothing

311+ -- just do nothing

310− ist <- get

312+ ist <- get

311− let (ap, _) = unApply (getRetTy fty)

313+ let (ap, _) = unApply (getRetTy fty)

312− logLvl 5 $ "Checking collapsibility of " ++ show (ap, fty)

314+ logLvl 5 $ "Checking collapsibility of " ++ show (ap, fty)

313− -- FIXME: Really ought to only do this for total functions!

315+ -- FIXME: Really ought to only do this for total functions!

314− let doNothing = case ap of

316+ let doNothing = case ap of

315− P _ tn _ -> case lookupCtxt Nothing tn

317+ P _ tn _ -> case lookupCtxt Nothing tn

316− (idris_optimisation ist) of

318+ (idris_optimisation ist) of

317− [oi] -> collapsible oi

319+ [oi] -> collapsible oi

318− _ -> False

320+ _ -> False

319− _ -> False

321+ _ -> False

320− solveDeferred n

322+ solveDeferred n

321− ist <- get

323+ ist <- get

322− when doNothing $

324+ when doNothing $

323− case lookupCtxt Nothing n (idris_optimisation ist) of

325+ case lookupCtxt Nothing n (idris_optimisation ist) of

324− [oi] -> do let opts = addDef n (oi { collapsible = True })

326+ [oi] -> do let opts = addDef n (oi { collapsible = True })

325− (idris_optimisation ist)

327+ (idris_optimisation ist)

326− put (ist { idris_optimisation = opts })

328+ put (ist { idris_optimisation = opts })

327− _ -> do let opts = addDef n (Optimise True [] [])

329+ _ -> do let opts = addDef n (Optimise True [] [])

328− (idris_optimisation ist)

330+ (idris_optimisation ist)

329− put (ist { idris_optimisation = opts })

331+ put (ist { idris_optimisation = opts })

330− addIBC (IBCOpt n)

332+ addIBC (IBCOpt n)

331− ist <- get

333+ ist <- get

332− let pats = pats_in

334+ let pats = pats_in

333−-- logLvl 3 (showSep "\n" (map (\ (l,r) ->

335+ -- logLvl 3 (showSep "\n" (map (\ (l,r) ->

334−-- show l ++ " = " ++

336+ -- show l ++ " = " ++

335−-- show r) pats))

337+ -- show r) pats))

336− let tcase = opt_typecase (idris_options ist)

338+ let tcase = opt_typecase (idris_options ist)

337− let pdef = map debind $ map (simpl False (tt_ctxt ist)) pats

339+ let pdef = map debind $ map (simpl False (tt_ctxt ist)) pats

338−

340+

339− numArgs <- tclift $ sameLength pdef

341+ numArgs <- tclift $ sameLength pdef

340−

342+

341− optpats <- if doNothing

343+ optpats <- if doNothing

342− then return $ [Right (mkApp (P Bound n Erased)

344+ then return $ [Right (mkApp (P Bound n Erased)

343− (take numArgs (repeat Erased)), Erased)]

345+ (take numArgs (repeat Erased)), Erased)]

344− else stripCollapsed pats

346+ else stripCollapsed pats

345−

347+

346− logLvl 5 $ "Patterns:\n" ++ show pats

348+ logLvl 5 $ "Patterns:\n" ++ show pats

347−

349+

348− let optpdef = map debind $ map (simpl True (tt_ctxt ist)) optpats

350+ let optpdef = map debind $ map (simpl True (tt_ctxt ist)) optpats

349− tree@(CaseDef scargs sc _) <- tclift $

351+ tree@(CaseDef scargs sc _) <- tclift $

350− simpleCase tcase False CompileTime fc pdef

352+ simpleCase tcase False CompileTime fc pdef

351− cov <- coverage

353+ cov <- coverage

352− pmissing <-

354+ pmissing <-

353− if cov

355+ if cov

354− then do missing <- genClauses fc n (map getLHS pdef) cs

356+ then do missing <- genClauses fc n (map getLHS pdef) cs

355− -- missing <- genMissing n scargs sc

357+ -- missing <- genMissing n scargs sc

356− missing' <- filterM (checkPossible info fc True n) missing

358+ missing' <- filterM (checkPossible info fc True n) missing

357− logLvl 2 $ "Must be unreachable:\n" ++

359+ logLvl 2 $ "Must be unreachable:\n" ++

358− showSep "\n" (map (showImp True) missing') ++

360+ showSep "\n" (map (showImp True) missing') ++

359− "\nAgainst: " ++

361+ "\nAgainst: " ++

360− showSep "\n" (map (\t -> showImp True (delab ist t)) (map getLHS pdef))

362+ showSep "\n" (map (\t -> showImp True (delab ist t)) (map getLHS pdef))

361− return missing'

363+ return missing'

362− else return []

364+ else return []

363− let pcover = null pmissing

365+ let pcover = null pmissing

364− pdef' <- applyOpts optpdef

366+ pdef' <- applyOpts optpdef

365− logLvl 5 $ "Optimised patterns:\n" ++ show pdef'

367+ logLvl 5 $ "Optimised patterns:\n" ++ show pdef'

366− ist <- get

368+ ist <- get

367−-- let wf = wellFounded ist n sc

369+ -- let wf = wellFounded ist n sc

368− let tot = if pcover || AssertTotal `elem` opts

370+ let tot = if pcover || AssertTotal `elem` opts

369− then Unchecked -- finish checking later

371+ then Unchecked -- finish checking later

370− else Partial NotCovering -- already know it's not total

372+ else Partial NotCovering -- already know it's not total

371−-- case lookupCtxt (namespace info) n (idris_flags ist) of

373+ -- case lookupCtxt (namespace info) n (idris_flags ist) of

372−-- [fs] -> if TotalFn `elem` fs

374+ -- [fs] -> if TotalFn `elem` fs

373−-- then case tot of

375+ -- then case tot of

374−-- Total _ -> return ()

376+ -- Total _ -> return ()

375−-- t -> tclift $ tfail (At fc (Msg (show n ++ " is " ++ show t)))

377+ -- t -> tclift $ tfail (At fc (Msg (show n ++ " is " ++ show t)))

376−-- else return ()

378+ -- else return ()

377−-- _ -> return ()

379+ -- _ -> return ()

378− case tree of

380+ case tree of

379− CaseDef _ _ [] -> return ()

381+ CaseDef _ _ [] -> return ()

380− CaseDef _ _ xs -> mapM_ (\x ->

382+ CaseDef _ _ xs -> mapM_ (\x ->

381− iputStrLn $ show fc ++

383+ iputStrLn $ show fc ++

382− ":warning - Unreachable case: " ++

384+ ":warning - Unreachable case: " ++

383− show (delab ist x)) xs

385+ show (delab ist x)) xs

384− let knowncovering = pcover && cov

386+ let knowncovering = pcover && cov

385−

387+

386− tree' <- tclift $ simpleCase tcase knowncovering RunTime fc pdef'

388+ tree' <- tclift $ simpleCase tcase knowncovering RunTime fc pdef'

387− logLvl 3 (show tree)

389+ logLvl 3 (show tree)

388− logLvl 3 $ "Optimised: " ++ show tree'

390+ logLvl 3 $ "Optimised: " ++ show tree'

389− ctxt <- getContext

391+ ctxt <- getContext

390− ist <- get

392+ ist <- get

391− put (ist { idris_patdefs = addDef n pdef' (idris_patdefs ist) })

393+ put (ist { idris_patdefs = addDef n pdef' (idris_patdefs ist) })

392− case lookupTy (namespace info) n ctxt of

394+ case lookupTy (namespace info) n ctxt of

393− [ty] -> do updateContext (addCasedef n (inlinable opts)

395+ [ty] -> do updateContext (addCasedef n (inlinable opts)

394− tcase knowncovering pats

396+ tcase knowncovering pats

395− pdef pdef' ty)

397+ pdef pdef' ty)

396− addIBC (IBCDef n)

398+ addIBC (IBCDef n)

397− setTotality n tot

399+ setTotality n tot

398− totcheck (fc, n)

400+ totcheck (fc, n)

399− when (tot /= Unchecked) $ addIBC (IBCTotal n tot)

401+ when (tot /= Unchecked) $ addIBC (IBCTotal n tot)

400− i <- get

402+ i <- get

401− case lookupDef Nothing n (tt_ctxt i) of

403+ case lookupDef Nothing n (tt_ctxt i) of

402− (CaseOp _ _ _ _ _ scargs sc scargs' sc' : _) ->

404+ (CaseOp _ _ _ _ _ scargs sc scargs' sc' : _) ->

403− do let calls = findCalls sc' scargs'

405+ do let calls = findCalls sc' scargs'

404− let used = findUsedArgs sc' scargs'

406+ let used = findUsedArgs sc' scargs'

405− -- let scg = buildSCG i sc scargs

407+ -- let scg = buildSCG i sc scargs

406− -- add SCG later, when checking totality

408+ -- add SCG later, when checking totality

407− let cg = CGInfo scargs' calls [] used []

409+ let cg = CGInfo scargs' calls [] used []

408− logLvl 2 $ "Called names: " ++ show cg

410+ logLvl 2 $ "Called names: " ++ show cg

409− addToCG n cg

411+ addToCG n cg

410− addToCalledG n (nub (map fst calls)) -- plus names in type!

412+ addToCalledG n (nub (map fst calls)) -- plus names in type!

411− addIBC (IBCCG n)

413+ addIBC (IBCCG n)

412− _ -> return ()

414+ _ -> return ()

413−-- addIBC (IBCTotal n tot)

415+ -- addIBC (IBCTotal n tot)

414− [] -> return ()

416+ [] -> return ()

417+ return ()

415 where

418 where

416 debind (Right (x, y)) = let (vs, x') = depat [] x

419 debind (Right (x, y)) = let (vs, x') = depat [] x

417 (_, y') = depat [] y in

420 (_, y') = depat [] y in

src/Idris/Parser.hs+40−37

@@ -96,40 +96,42 @@ loadSource lidr f

96 mapM_ (addIBC . IBCImport) modules

97 ds' <- parseProg (defaultSyntax {syn_namespace = reverse mname })

98 f rest pos

99+ unless (null ds') $ do

99− let ds = namespaces mname ds'

100+ let ds = namespaces mname ds'

100− logLvl 3 (dumpDecls ds)

101+ logLvl 3 (dumpDecls ds)

101− i <- getIState

102+ i <- getIState

102− logLvl 10 (show (toAlist (idris_implicits i)))

103+ logLvl 10 (show (toAlist (idris_implicits i)))

103− logLvl 3 (show (idris_infixes i))

104+ logLvl 3 (show (idris_infixes i))

104− -- Now add all the declarations to the context

105+ -- Now add all the declarations to the context

105− v <- verbose

106+ v <- verbose

106− when v $ iputStrLn $ "Type checking " ++ f

107+ when v $ iputStrLn $ "Type checking " ++ f

107− elabDecls toplevel ds

108+ elabDecls toplevel ds

108− i <- get

109+ i <- get

109− -- simplify every definition do give the totality checker

110+ -- simplify every definition do give the totality checker

110− -- a better chance

111+ -- a better chance

111− mapM_ (\n -> do logLvl 5 $ "Simplifying " ++ show n

112+ mapM_ (\n -> do logLvl 5 $ "Simplifying " ++ show n

112− updateContext (simplifyCasedef n))

113+ updateContext (simplifyCasedef n))

113− (map snd (idris_totcheck i))

114+ (map snd (idris_totcheck i))

114− -- build size change graph from simplified definitions

115+ -- build size change graph from simplified definitions

115− iLOG "Totality checking"

116+ iLOG "Totality checking"

116− i <- get

117+ i <- get

117−-- mapM_ buildSCG (idris_totcheck i)

118+ -- mapM_ buildSCG (idris_totcheck i)

118− mapM_ checkDeclTotality (idris_totcheck i)

119+ mapM_ checkDeclTotality (idris_totcheck i)

119− iLOG ("Finished " ++ f)

120+ iLOG ("Finished " ++ f)

120− ibcsd <- valIBCSubDir i

121+ ibcsd <- valIBCSubDir i

121− let ibc = ibcPathNoFallback ibcsd f

122+ let ibc = ibcPathNoFallback ibcsd f

122− iLOG "Universe checking"

123+ iLOG "Universe checking"

123− iucheck

124+ iucheck

124− i <- getIState

125+ i <- getIState

125− addHides (hide_list i)

126+ addHides (hide_list i)

126− ok <- noErrors

127+ ok <- noErrors

127− when ok $

128+ when ok $

128− idrisCatch (do writeIBC f ibc; clearIBC)

129+ idrisCatch (do writeIBC f ibc; clearIBC)

129− (\c -> return ()) -- failure is harmless

130+ (\c -> return ()) -- failure is harmless

130− i <- getIState

131+ i <- getIState

131− putIState (i { default_total = def_total,

132+ putIState (i { default_total = def_total,

132− hide_list = [] })

133+ hide_list = [] })

134+ return ()

133 return ()

135 return ()

134 where

136 where

135 namespaces [] ds = ds

137 namespaces [] ds = ds

@@ -279,7 +281,8 @@ parseProg syn fname input pos

279 eof

281 eof

280 i' <- getState

282 i' <- getState

281 return (concat ps, i')) i fname input of

283 return (concat ps, i')) i fname input of

282− Left err -> fail (show err)

284+ Left err -> do iputStrLn (show err)

285+ return []

283 Right (x, i) -> do put i

286 Right (x, i) -> do put i

284 return (collect x)

287 return (collect x)

285

288

@@ -512,8 +515,8 @@ pFixity = do pushIndent

512 })

515 })

513 fc <- pfc

516 fc <- pfc

514 return (PFix fc (f prec) ops)

517 return (PFix fc (f prec) ops)

515− else fail $ concatMap (\(f, (x:xs)) -> "Illegal redeclaration of fixity: \""

518+ else fail $ concatMap (\(f, (x:xs)) -> "Illegal redeclaration of fixity:\n\t\""

516− ++ show f ++ "\" overrides \"" ++ show x ++ "\"\n") ill

519+ ++ show f ++ "\" overrides \"" ++ show x ++ "\"") ill

517 where alreadyDeclared :: [FixDecl] -> FixDecl -> (FixDecl, [FixDecl])

520 where alreadyDeclared :: [FixDecl] -> FixDecl -> (FixDecl, [FixDecl])

518 alreadyDeclared fs f = (f, filter ((extractName f ==) . extractName) fs)

521 alreadyDeclared fs f = (f, filter ((extractName f ==) . extractName) fs)

519

522