7c71bfa · Idris-dev · git.iko.soy

git.iko.soy/Idris-dev

on master help sign in

Merge branch 'master' of https://github.com/edwinb/Idris-dev into windows

7c71bfaChetan T14 years ago

contribs/tool-support/vim/syntax/idris.vim+1−1

compare with master

unifiedsplit

@@ -10,7 +10,7 @@ syn match idrisModule "\<$module\|namespace$\>"

10syn match idrisImport "\<import\>"

11syn match idrisStructure "\<$class\|\(co$\?data\|instance\|where\|record\)\>"

12syn match idrisVisibility "\<$public\|abstract\|private$\>"

14syn match idrisSyntax "$pattern \+\|term \+$\?syntax"

15syn match idrisConditional "\<$if\|then\|else$\>"

src/Core/TT.hs+1

@@ -59,6 +59,7 @@ data Err = Msg String

59 | UniverseError

60 | ProgramLineComment

61 | Inaccessible Name

62+ | NonCollapsiblePostulate Name

62 | At FC Err

63 | At FC Err

63 deriving Eq

64 deriving Eq

src/Idris/AbsSyntax.hs+9−1

@@ -390,7 +390,7 @@ infP = P (TCon 6 0) inferTy (Set (UVal 0))

390getInferTerm, getInferType :: Term -> Term

391getInferTerm (Bind n b sc) = Bind n b $ getInferTerm sc

392getInferTerm (App (App _ _) tm) = tm

393−getInferTerm tm = error ("getInferTerm " ++ show tm)

393+getInferTerm tm = tm -- error ("getInferTerm " ++ show tm)

394

395getInferType (Bind n b sc) = Bind n b $ getInferType sc

396getInferType (App (App _ ty) _) = ty

@@ -511,6 +511,13 @@ expandParamsD rhsonly ist dec ps ns (PTy doc syn fc o n ty)

511 PTy doc syn fc o (dec n) (piBind ps (expandParams dec ps ns ty))

512 else --trace (show (n, expandParams dec ps ns ty)) $

513 PTy doc syn fc o n (expandParams dec ps ns ty)

514+expandParamsD rhsonly ist dec ps ns (PPostulate doc syn fc o n ty)

515+ = if n `elem` ns && (not rhsonly)

516+ then -- trace (show (n, expandParams dec ps ns ty)) $

517+ PPostulate doc syn fc o (dec n) (piBind ps

518+ (expandParams dec ps ns ty))

519+ else --trace (show (n, expandParams dec ps ns ty)) $

520+ PPostulate doc syn fc o n (expandParams dec ps ns ty)

514expandParamsD rhsonly ist dec ps ns (PClauses fc opts n cs)

521expandParamsD rhsonly ist dec ps ns (PClauses fc opts n cs)

515 = let n' = if n `elem` ns then dec n else n in

522 = let n' = if n `elem` ns then dec n else n in

516 PClauses fc opts n' (map expandParamsC cs)

523 PClauses fc opts n' (map expandParamsC cs)

@@ -1073,3 +1080,4 @@ shadow n n' t = sm t where

1073 sm (PHidden x) = PHidden (sm x)

1080 sm (PHidden x) = PHidden (sm x)

1074 sm x = x

1081 sm x = x

1075

1082

1083+

src/Idris/AbsSyntaxTree.hs+30−25

@@ -289,31 +289,33 @@ type FnOpts = [FnOpt]

289inlinable :: FnOpts -> Bool

290inlinable = elem Inlinable

291

292+data PDecl' t

292−data PDecl' t = PFix FC Fixity [String] -- fixity declaration

293+ = PFix FC Fixity [String] -- fixity declaration

293− | PTy String SyntaxInfo FC FnOpts Name t -- type declaration

294+ | PTy String SyntaxInfo FC FnOpts Name t -- type declaration

295+ | PPostulate String SyntaxInfo FC FnOpts Name t

294− | PClauses FC FnOpts Name [PClause' t] -- pattern clause

296+ | PClauses FC FnOpts Name [PClause' t] -- pattern clause

295− | PCAF FC Name t -- top level constant

297+ | PCAF FC Name t -- top level constant

296− | PData String SyntaxInfo FC Bool -- codata

298+ | PData String SyntaxInfo FC Bool -- codata

297− (PData' t) -- data declaration

299+ (PData' t) -- data declaration

298− | PParams FC [(Name, t)] [PDecl' t] -- params block

300+ | PParams FC [(Name, t)] [PDecl' t] -- params block

299− | PNamespace String [PDecl' t] -- new namespace

301+ | PNamespace String [PDecl' t] -- new namespace

300− | PRecord String SyntaxInfo FC Name t String Name t -- record declaration

302+ | PRecord String SyntaxInfo FC Name t String Name t -- record declaration

301− | PClass String SyntaxInfo FC

303+ | PClass String SyntaxInfo FC

302− [t] -- constraints

304+ [t] -- constraints

303− Name

305+ Name

304− [(Name, t)] -- parameters

306+ [(Name, t)] -- parameters

305− [PDecl' t] -- declarations

307+ [PDecl' t] -- declarations

306− | PInstance SyntaxInfo FC [t] -- constraints

308+ | PInstance SyntaxInfo FC [t] -- constraints

307− Name -- class

309+ Name -- class

308− [t] -- parameters

310+ [t] -- parameters

309− t -- full instance type

311+ t -- full instance type

310− (Maybe Name) -- explicit name

312+ (Maybe Name) -- explicit name

311− [PDecl' t]

313+ [PDecl' t]

312− | PDSL Name (DSL' t)

314+ | PDSL Name (DSL' t)

313− | PSyntax FC Syntax

315+ | PSyntax FC Syntax

314− | PMutual FC [PDecl' t]

316+ | PMutual FC [PDecl' t]

315− | PDirective (Idris ())

317+ | PDirective (Idris ())

316− deriving Functor

318+ deriving Functor

317{-!

319{-!

318deriving instance Binary PDecl'

320deriving instance Binary PDecl'

319!-}

321!-}

@@ -348,6 +350,7 @@ type PClause = PClause' PTerm

348declared :: PDecl -> [Name]

350declared :: PDecl -> [Name]

349declared (PFix _ _ _) = []

351declared (PFix _ _ _) = []

350declared (PTy _ _ _ _ n t) = [n]

352declared (PTy _ _ _ _ n t) = [n]

353+declared (PPostulate _ _ _ _ n t) = [n]

351declared (PClauses _ _ n _) = [] -- not a declaration

354declared (PClauses _ _ n _) = [] -- not a declaration

352declared (PRecord _ _ _ n _ _ c _) = [n, c]

355declared (PRecord _ _ _ n _ _ c _) = [n, c]

353declared (PData _ _ _ _ (PDatadecl n _ ts)) = n : map fstt ts

356declared (PData _ _ _ _ (PDatadecl n _ ts)) = n : map fstt ts

@@ -360,6 +363,7 @@ declared (PNamespace _ ds) = concatMap declared ds

360defined :: PDecl -> [Name]

363defined :: PDecl -> [Name]

361defined (PFix _ _ _) = []

364defined (PFix _ _ _) = []

362defined (PTy _ _ _ _ n t) = []

365defined (PTy _ _ _ _ n t) = []

366+defined (PPostulate _ _ _ _ n t) = []

363defined (PClauses _ _ n _) = [n] -- not a declaration

367defined (PClauses _ _ n _) = [n] -- not a declaration

364defined (PRecord _ _ _ n _ _ c _) = [n, c]

368defined (PRecord _ _ _ n _ _ c _) = [n, c]

365defined (PData _ _ _ _ (PDatadecl n _ ts)) = n : map fstt ts

369defined (PData _ _ _ _ (PDatadecl n _ ts)) = n : map fstt ts

@@ -657,6 +661,7 @@ instance Show PData where

657

661

658showDeclImp _ (PFix _ f ops) = show f ++ " " ++ showSep ", " ops

662showDeclImp _ (PFix _ f ops) = show f ++ " " ++ showSep ", " ops

659showDeclImp t (PTy _ _ _ _ n ty) = show n ++ " : " ++ showImp t ty

663showDeclImp t (PTy _ _ _ _ n ty) = show n ++ " : " ++ showImp t ty

664+showDeclImp t (PPostulate _ _ _ _ n ty) = show n ++ " : " ++ showImp t ty

660showDeclImp _ (PClauses _ _ n c) = showSep "\n" (map show c)

665showDeclImp _ (PClauses _ _ n c) = showSep "\n" (map show c)

661showDeclImp _ (PData _ _ _ _ d) = show d

666showDeclImp _ (PData _ _ _ _ d) = show d

662showDeclImp _ (PParams f ns ps) = "parameters " ++ show ns ++ "\n" ++

667showDeclImp _ (PParams f ns ps) = "parameters " ++ show ns ++ "\n" ++

src/Idris/Delaborate.hs+2

@@ -102,6 +102,8 @@ pshow i (IncompleteTerm t) = "Incomplete term " ++ showImp True (delab i t)

102pshow i UniverseError = "Universe inconsistency"

103pshow i ProgramLineComment = "Program line next to comment"

104pshow i (Inaccessible n) = show n ++ " is not an accessible pattern variable"

105+pshow i (NonCollapsiblePostulate n)

106+ = "The return type of postulate " ++ show n ++ " is not collapsible"

105pshow i (At f e) = show f ++ ":" ++ pshow i e

107pshow i (At f e) = show f ++ ":" ++ pshow i e

106

108

107showSc i [] = ""

109showSc i [] = ""

src/Idris/ElabDecls.hs+158−118

@@ -80,6 +80,30 @@ elabType info syn doc fc opts n ty' = {- let ty' = piBind (params info) ty_in

80 when corec $ do setAccessibility n Frozen

81 addIBC (IBCAccess n Frozen)

83+elabPostulate :: ElabInfo -> SyntaxInfo -> String ->

84+ FC -> FnOpts -> Name -> PTerm -> Idris ()

85+elabPostulate info syn doc fc opts n ty

86+ = do elabType info syn doc fc opts n ty

87+ -- make sure it's collapsible, so it is never needed at run time

88+ -- start by getting the elaborated type

89+ ctxt <- getContext

90+ fty <- case lookupTy Nothing n ctxt of

91+ [] -> tclift $ tfail $ (At fc (NoTypeDecl n)) -- can't happen!

92+ [ty] -> return ty

93+ ist <- get

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

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

96+ let postOK = case ap of

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

98+ (idris_optimisation ist) of

99+ [oi] -> collapsible oi

100+ _ -> False

101+ _ -> False

102+ when (not postOK)

103+ $ tclift $ tfail (At fc (NonCollapsiblePostulate n))

104+ -- remove it from the deferred definitions list

105+ solveDeferred n

106+

83elabData :: ElabInfo -> SyntaxInfo -> String -> FC -> Bool -> PData -> Idris ()

107elabData :: ElabInfo -> SyntaxInfo -> String -> FC -> Bool -> PData -> Idris ()

84elabData info syn doc fc codata (PLaterdecl n t_in)

108elabData info syn doc fc codata (PLaterdecl n t_in)

85 = do iLOG (show (fc, doc))

109 = do iLOG (show (fc, doc))

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

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

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

275 do ctxt <- getContext

299 do ctxt <- getContext

276 -- Check n actually exists

300 -- Check n actually exists

277− 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

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

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

279− -- question: CAFs in where blocks?

305+ -- question: CAFs in where blocks?

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

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

281− [ty] -> return ty

307+ [ty] -> return ty

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

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

283− (zip [0..] cs)

309+ (zip [0..] cs)

284− -- 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

285− -- just do nothing

311+ -- just do nothing

286− ist <- get

312+ ist <- get

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

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

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

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

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

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

290− let doNothing = case ap of

316+ let doNothing = case ap of

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

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

292− (idris_optimisation ist) of

318+ (idris_optimisation ist) of

293− [oi] -> collapsible oi

319+ [oi] -> collapsible oi

294− _ -> False

320+ _ -> False

295− _ -> False

321+ _ -> False

296− solveDeferred n

322+ solveDeferred n

297− ist <- get

323+ ist <- get

298− when doNothing $

324+ when doNothing $

299− case lookupCtxt Nothing n (idris_optimisation ist) of

325+ case lookupCtxt Nothing n (idris_optimisation ist) of

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

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

301− (idris_optimisation ist)

327+ (idris_optimisation ist)

302− put (ist { idris_optimisation = opts })

328+ put (ist { idris_optimisation = opts })

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

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

304− (idris_optimisation ist)

330+ (idris_optimisation ist)

305− put (ist { idris_optimisation = opts })

331+ put (ist { idris_optimisation = opts })

306− addIBC (IBCOpt n)

332+ addIBC (IBCOpt n)

307− ist <- get

333+ ist <- get

308− let pats = pats_in

334+ let pats = pats_in

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

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

310−-- show l ++ " = " ++

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

311−-- show r) pats))

337+ -- show r) pats))

312− let tcase = opt_typecase (idris_options ist)

338+ let tcase = opt_typecase (idris_options ist)

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

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

314−

340+

315− numArgs <- tclift $ sameLength pdef

341+ numArgs <- tclift $ sameLength pdef

316−

342+

317− optpats <- if doNothing

343+ optpats <- if doNothing

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

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

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

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

320− else stripCollapsed pats

346+ else stripCollapsed pats

321−

347+

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

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

323−

349+

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

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

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

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

326− simpleCase tcase False CompileTime fc pdef

352+ simpleCase tcase False CompileTime fc pdef

327− cov <- coverage

353+ cov <- coverage

328− pmissing <-

354+ pmissing <-

329− if cov

355+ if cov

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

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

331− -- missing <- genMissing n scargs sc

357+ -- missing <- genMissing n scargs sc

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

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

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

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

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

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

335− "\nAgainst: " ++

361+ "\nAgainst: " ++

336− 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))

337− return missing'

363+ return missing'

338− else return []

364+ else return []

339− let pcover = null pmissing

365+ let pcover = null pmissing

340− pdef' <- applyOpts optpdef

366+ pdef' <- applyOpts optpdef

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

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

342− ist <- get

368+ ist <- get

343−-- let wf = wellFounded ist n sc

369+ -- let wf = wellFounded ist n sc

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

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

345− then Unchecked -- finish checking later

371+ then Unchecked -- finish checking later

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

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

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

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

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

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

349−-- then case tot of

375+ -- then case tot of

350−-- Total _ -> return ()

376+ -- Total _ -> return ()

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

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

352−-- else return ()

378+ -- else return ()

353−-- _ -> return ()

379+ -- _ -> return ()

354− case tree of

380+ case tree of

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

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

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

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

357− iputStrLn $ show fc ++

383+ iputStrLn $ show fc ++

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

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

359− show (delab ist x)) xs

385+ show (delab ist x)) xs

360− let knowncovering = pcover && cov

386+ let knowncovering = pcover && cov

361−

387+

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

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

363− logLvl 3 (show tree)

389+ logLvl 3 (show tree)

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

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

365− ctxt <- getContext

391+ ctxt <- getContext

366− ist <- get

392+ ist <- get

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

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

368− case lookupTy (namespace info) n ctxt of

394+ case lookupTy (namespace info) n ctxt of

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

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

370− tcase knowncovering pats

396+ tcase knowncovering pats

371− pdef pdef' ty)

397+ pdef pdef' ty)

372− addIBC (IBCDef n)

398+ addIBC (IBCDef n)

373− setTotality n tot

399+ setTotality n tot

374− totcheck (fc, n)

400+ totcheck (fc, n)

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

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

376− i <- get

402+ i <- get

377− case lookupDef Nothing n (tt_ctxt i) of

403+ case lookupDef Nothing n (tt_ctxt i) of

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

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

379− do let calls = findCalls sc' scargs'

405+ do let calls = findCalls sc' scargs'

380− let used = findUsedArgs sc' scargs'

406+ let used = findUsedArgs sc' scargs'

381− -- let scg = buildSCG i sc scargs

407+ -- let scg = buildSCG i sc scargs

382− -- add SCG later, when checking totality

408+ -- add SCG later, when checking totality

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

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

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

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

385− addToCG n cg

411+ addToCG n cg

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

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

387− addIBC (IBCCG n)

413+ addIBC (IBCCG n)

388− _ -> return ()

414+ _ -> return ()

389−-- addIBC (IBCTotal n tot)

415+ -- addIBC (IBCTotal n tot)

390− [] -> return ()

416+ [] -> return ()

417+ return ()

391 where

418 where

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

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

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

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

@@ -417,8 +444,16 @@ elabVal info aspat tm_in

417 i <- get

444 i <- get

418 let tm = addImpl i tm_in

445 let tm = addImpl i tm_in

419 logLvl 10 (showImp True tm)

446 logLvl 10 (showImp True tm)

447+ -- try:

448+ -- * ordinary elaboration

449+ -- * elaboration as a Set

450+ -- * elaboration as a function a -> b

451+

452+ ((tm', defer, is), _) <-

453+ tctry (elaborate ctxt (MN 0 "val") (Set (UVal 0)) []

454+ (build i info aspat (MN 0 "val") tm))

420− ((tm', defer, is), _) <- tclift $ elaborate ctxt (MN 0 "val") infP []

455+ (elaborate ctxt (MN 0 "val") infP []

421− (build i info aspat (MN 0 "val") (infTerm tm))

456+ (build i info aspat (MN 0 "val") (infTerm tm)))

422 logLvl 3 ("Value: " ++ show tm')

457 logLvl 3 ("Value: " ++ show tm')

423 let vtm = getInferTerm tm'

458 let vtm = getInferTerm tm'

424 logLvl 2 (show vtm)

459 logLvl 2 (show vtm)

@@ -533,8 +568,9 @@ elabClause info tcgen (_, PWith fc fname lhs_in withs wval_in withblock)

533 i <- get

568 i <- get

534 let lhs = addImpl i lhs_in

569 let lhs = addImpl i lhs_in

535 logLvl 5 ("LHS: " ++ showImp True lhs)

570 logLvl 5 ("LHS: " ++ showImp True lhs)

571+ ((lhs', dlhs, []), _) <-

536− ((lhs', dlhs, []), _) <- tclift $ elaborate ctxt (MN 0 "patLHS") infP []

572+ tclift $ elaborate ctxt (MN 0 "patLHS") infP []

537− (erun fc (buildTC i info True tcgen fname (infTerm lhs)))

573+ (erun fc (buildTC i info True tcgen fname (infTerm lhs)))

538 let lhs_tm = orderPats (getInferTerm lhs')

574 let lhs_tm = orderPats (getInferTerm lhs')

539 let lhs_ty = getInferType lhs'

575 let lhs_ty = getInferType lhs'

540 let ret_ty = getRetTy lhs_ty

576 let ret_ty = getRetTy lhs_ty

@@ -990,6 +1026,10 @@ elabDecl' what info (PTy doc s f o n ty)

990 | what /= EDefns

1026 | what /= EDefns

991 = do iLOG $ "Elaborating type decl " ++ show n ++ show o

1027 = do iLOG $ "Elaborating type decl " ++ show n ++ show o

992 elabType info s doc f o n ty

1028 elabType info s doc f o n ty

1029+elabDecl' what info (PPostulate doc s f o n ty)

1030+ | what /= EDefns

1031+ = do iLOG $ "Elaborating postulate " ++ show n ++ show o

1032+ elabPostulate info s doc f o n ty

993elabDecl' what info (PData doc s f co d)

1033elabDecl' what info (PData doc s f co d)

994 | what /= ETypes

1034 | what /= ETypes

995 = do iLOG $ "Elaborating " ++ show (d_name d)

1035 = do iLOG $ "Elaborating " ++ show (d_name d)

src/Idris/ElabTerm.hs+11−3

@@ -318,15 +318,23 @@ elab ist info pattern tcgen fn tm

318 _ -> n

319 elab' ina x = fail $ "Something's gone wrong. Did you miss a semi-colon somewhere?"

320

321− caseBlock :: FC -> Name -> [(Name, Binder Term)] -> [(PTerm, PTerm)] -> [PClause]

321+ caseBlock :: FC -> Name -> [(Name, Binder Term)] ->

322+ [(PTerm, PTerm)] -> [PClause]

322 caseBlock fc n env opts

323 caseBlock fc n env opts

323 = let args = map mkarg (map fst (init env)) in

324 = let args = map mkarg (map fst (init env)) in

324 map (mkClause args) opts

325 map (mkClause args) opts

325 where -- mkarg (MN _ _) = Placeholder

326 where -- mkarg (MN _ _) = Placeholder

326 mkarg n = PRef fc n

327 mkarg n = PRef fc n

328+ -- may be shadowed names in the new pattern - so replace the

329+ -- old ones with an _

327 mkClause args (l, r)

330 mkClause args (l, r)

331+ = let args' = map (shadowed (allNamesIn l)) args

328− = PClause fc n (PApp fc (PRef fc n)

332+ lhs = PApp fc (PRef fc n)

329− (map pexp args ++ [pexp l])) [] r []

333+ (map pexp args' ++ [pexp l]) in

334+ PClause fc n lhs [] r []

335+

336+ shadowed new (PRef _ n) | n `elem` new = Placeholder

337+ shadowed new t = t

330

338

331 elabArgs ina failed retry [] _

339 elabArgs ina failed retry [] _

332-- | retry = let (ns, ts) = unzip (reverse failed) in

340-- | retry = let (ns, ts) = unzip (reverse failed) in

src/Idris/Error.hs+6

@@ -58,6 +58,12 @@ tclift tc = case tc of

58 _ -> return ()

59 throwIO (IErr $ pshow i err)

61+tctry :: TC a -> TC a -> Idris a

62+tctry tc1 tc2

63+ = case tc1 of

64+ OK v -> return v

65+ Error err -> tclift tc2

66+

61getErrLine str

67getErrLine str

62 = case span (/=':') str of

68 = case span (/=':') str of

63 (_, ':':rest) -> case span isDigit rest of

69 (_, ':':rest) -> case span isDigit rest of

src/Idris/IBC.hs+15

@@ -959,6 +959,14 @@ instance (Binary t) => Binary (PDecl' t) where

959 PMutual x1 x2 -> do putWord8 11

960 put x1

961 put x2

962+ PPostulate x1 x2 x3 x4 x5 x6

963+ -> do putWord8 12

964+ put x1

965+ put x2

966+ put x3

967+ put x4

968+ put x5

969+ put x6

962 get

970 get

963 = do i <- getWord8

971 = do i <- getWord8

964 case i of

972 case i of

@@ -1027,6 +1035,13 @@ instance (Binary t) => Binary (PDecl' t) where

1027 11 -> do x1 <- get

1035 11 -> do x1 <- get

1028 x2 <- get

1036 x2 <- get

1029 return (PMutual x1 x2)

1037 return (PMutual x1 x2)

1038+ 12 -> do x1 <- get

1039+ x2 <- get

1040+ x3 <- get

1041+ x4 <- get

1042+ x5 <- get

1043+ x6 <- get

1044+ return (PPostulate x1 x2 x3 x4 x5 x6)

1030 _ -> error "Corrupted binary data for PDecl'"

1045 _ -> error "Corrupted binary data for PDecl'"

1031

1046

1032instance Binary SyntaxInfo where

1047instance Binary SyntaxInfo where

src/Idris/Parser.hs+61−39

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

97 mapM_ (addIBC . IBCImport) modules

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

99 f rest pos

100+ unless (null ds') $ do

100− let ds = namespaces mname ds'

101+ let ds = namespaces mname ds'

101− logLvl 3 (dumpDecls ds)

102+ logLvl 3 (dumpDecls ds)

102− i <- getIState

103+ i <- getIState

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

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

104− logLvl 3 (show (idris_infixes i))

105+ logLvl 3 (show (idris_infixes i))

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

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

106− v <- verbose

107+ v <- verbose

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

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

108− elabDecls toplevel ds

109+ elabDecls toplevel ds

109− i <- get

110+ i <- get

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

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

111− -- a better chance

112+ -- a better chance

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

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

113− updateContext (simplifyCasedef n))

114+ updateContext (simplifyCasedef n))

114− (map snd (idris_totcheck i))

115+ (map snd (idris_totcheck i))

115− -- build size change graph from simplified definitions

116+ -- build size change graph from simplified definitions

116− iLOG "Totality checking"

117+ iLOG "Totality checking"

117− i <- get

118+ i <- get

118−-- mapM_ buildSCG (idris_totcheck i)

119+ -- mapM_ buildSCG (idris_totcheck i)

119− mapM_ checkDeclTotality (idris_totcheck i)

120+ mapM_ checkDeclTotality (idris_totcheck i)

120− iLOG ("Finished " ++ f)

121+ iLOG ("Finished " ++ f)

121− ibcsd <- valIBCSubDir i

122+ ibcsd <- valIBCSubDir i

122− let ibc = ibcPathNoFallback ibcsd f

123+ let ibc = ibcPathNoFallback ibcsd f

123− iLOG "Universe checking"

124+ iLOG "Universe checking"

124− iucheck

125+ iucheck

125− i <- getIState

126+ i <- getIState

126− addHides (hide_list i)

127+ addHides (hide_list i)

127− ok <- noErrors

128+ ok <- noErrors

128− when ok $

129+ when ok $

129− idrisCatch (do writeIBC f ibc; clearIBC)

130+ idrisCatch (do writeIBC f ibc; clearIBC)

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

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

131− i <- getIState

132+ i <- getIState

132− putIState (i { default_total = def_total,

133+ putIState (i { default_total = def_total,

133− hide_list = [] })

134+ hide_list = [] })

135+ return ()

134 return ()

136 return ()

135 where

137 where

136 namespaces [] ds = ds

138 namespaces [] ds = ds

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

277 eof

279 eof

278 i' <- getState

280 i' <- getState

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

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

280− Left err -> fail (show err)

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

283+ return []

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

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

282 return (collect x)

285 return (collect x)

283

286

@@ -415,8 +418,6 @@ pSynSym = try (do lchar '['; n <- pName; lchar ']'

415

418

416pFunDecl' :: SyntaxInfo -> IParser PDecl

419pFunDecl' :: SyntaxInfo -> IParser PDecl

417pFunDecl' syn = try (do doc <- option "" (pDocComment '|')

420pFunDecl' syn = try (do doc <- option "" (pDocComment '|')

418− -- trace ("Doc: " ++ show doc) $

419−-- let doc = ""

420 pushIndent

421 pushIndent

421 ist <- getState

422 ist <- getState

422 let initOpts = if default_total ist

423 let initOpts = if default_total ist

@@ -433,9 +434,30 @@ pFunDecl' syn = try (do doc <- option "" (pDocComment '|')

433-- ty' <- implicit syn n ty

434-- ty' <- implicit syn n ty

434 addAcc n acc

435 addAcc n acc

435 return (PTy doc syn fc opts' n ty))

436 return (PTy doc syn fc opts' n ty))

437+ <|> try (pPostulate syn)

436 <|> try (pPattern syn)

438 <|> try (pPattern syn)

437 <|> try (pCAF syn)

439 <|> try (pCAF syn)

438

440

441+pPostulate :: SyntaxInfo -> IParser PDecl

442+pPostulate syn = do doc <- option "" (pDocComment '|')

443+ pushIndent

444+ reserved "postulate"

445+ ist <- getState

446+ let initOpts = if default_total ist

447+ then [TotalFn]

448+ else []

449+ opts <- pFnOpts initOpts

450+ acc <- pAccessibility

451+ opts' <- pFnOpts opts

452+ n_in <- pfName

453+ let n = expandNS syn n_in

454+ ty <- pTSig (impOK syn)

455+ fc <- pfc

456+ pTerminator

457+ addAcc n acc

458+ return (PPostulate doc syn fc opts' n ty)

459+

460+

439pUsing :: SyntaxInfo -> IParser [PDecl]

461pUsing :: SyntaxInfo -> IParser [PDecl]

440pUsing syn =

462pUsing syn =

441 do reserved "using"; lchar '('; ns <- tyDeclList syn; lchar ')'

463 do reserved "using"; lchar '('; ns <- tyDeclList syn; lchar ')'

@@ -491,8 +513,8 @@ pFixity = do pushIndent

491 })

513 })

492 fc <- pfc

514 fc <- pfc

493 return (PFix fc (f prec) ops)

515 return (PFix fc (f prec) ops)

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

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

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

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

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

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

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

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

498

520