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

git.iko.soy/Idris-dev

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

commit7c71bfa547496e27f3c2b03c4620e614d2b4416e authorChetan T <chetant@gmail.com> dateMon 26 Nov 2012, 21:35 (14 years ago) parentbb9a3ad 51f3340

10 files changed+294−187

compare with master

unifiedsplit

contribs/tool-support/vim/syntax/idris.vim+1−1 src/Core/TT.hs+1 src/Idris/AbsSyntax.hs+9−1 src/Idris/AbsSyntaxTree.hs+30−25 src/Idris/Delaborate.hs+2 src/Idris/ElabDecls.hs+158−118 src/Idris/ElabTerm.hs+11−3 src/Idris/Error.hs+6 src/Idris/IBC.hs+15 src/Idris/Parser.hs+61−39

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

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

1010syn match idrisImport "\<import\>"

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

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

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

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

src/Core/TT.hs+1

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

5959 | UniverseError

6060 | ProgramLineComment

6161 | Inaccessible Name

62+ | NonCollapsiblePostulate Name

6263 | At FC Err

6364 deriving Eq

6465

src/Idris/AbsSyntax.hs+9−1

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

390390getInferTerm, getInferType :: Term -> Term

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

392392getInferTerm (App (App _ _) tm) = tm

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

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

394394

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

396396getInferType (App (App _ ty) _) = ty

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

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

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

513513 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)

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

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

516523 PClauses fc opts n' (map expandParamsC cs)

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

10731080 sm (PHidden x) = PHidden (sm x)

10741081 sm x = x

10751082

1083+

src/Idris/AbsSyntaxTree.hs+30−25

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

289289inlinable :: FnOpts -> Bool

290290inlinable = elem Inlinable

291291

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

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

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

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

296− | PData String SyntaxInfo FC Bool -- codata

297− (PData' t) -- data declaration

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

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

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

301− | PClass String SyntaxInfo FC

302− [t] -- constraints

303− Name

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

305− [PDecl' t] -- declarations

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

307− Name -- class

308− [t] -- parameters

309− t -- full instance type

310− (Maybe Name) -- explicit name

311− [PDecl' t]

312− | PDSL Name (DSL' t)

313− | PSyntax FC Syntax

314− | PMutual FC [PDecl' t]

315− | PDirective (Idris ())

316− deriving Functor

292+data PDecl' t

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

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

295+ | PPostulate String SyntaxInfo FC FnOpts Name t

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

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

298+ | PData String SyntaxInfo FC Bool -- codata

299+ (PData' t) -- data declaration

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

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

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

303+ | PClass String SyntaxInfo FC

304+ [t] -- constraints

305+ Name

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

307+ [PDecl' t] -- declarations

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

309+ Name -- class

310+ [t] -- parameters

311+ t -- full instance type

312+ (Maybe Name) -- explicit name

313+ [PDecl' t]

314+ | PDSL Name (DSL' t)

315+ | PSyntax FC Syntax

316+ | PMutual FC [PDecl' t]

317+ | PDirective (Idris ())

318+ deriving Functor

317319{-!

318320deriving instance Binary PDecl'

319321!-}

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

348350declared :: PDecl -> [Name]

349351declared (PFix _ _ _) = []

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

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

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

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

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

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

360363defined :: PDecl -> [Name]

361364defined (PFix _ _ _) = []

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

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

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

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

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

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

657661

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

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

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

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

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

662667showDeclImp _ (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)

102102pshow i UniverseError = "Universe inconsistency"

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

104104pshow 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"

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

106108

107109showSc 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

8080 when corec $ do setAccessibility n Frozen

8181 addIBC (IBCAccess n Frozen)

8282

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+

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

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

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

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

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

275299 do ctxt <- getContext

276300 -- 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 ()

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 ()

391418 where

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

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

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

417444 i <- get

418445 let tm = addImpl i tm_in

419446 logLvl 10 (showImp True tm)

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

421− (build i info aspat (MN 0 "val") (infTerm 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))

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

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

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

423458 let vtm = getInferTerm tm'

424459 logLvl 2 (show vtm)

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

533568 i <- get

534569 let lhs = addImpl i lhs_in

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

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

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

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

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

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

538574 let lhs_tm = orderPats (getInferTerm lhs')

539575 let lhs_ty = getInferType lhs'

540576 let ret_ty = getRetTy lhs_ty

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

9901026 | what /= EDefns

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

9921028 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

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

9941034 | what /= ETypes

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

src/Idris/ElabTerm.hs+11−3

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

318318 _ -> n

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

320320

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

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

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

322323 caseBlock fc n env opts

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

324325 map (mkClause args) opts

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

326327 mkarg n = PRef fc n

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

329+ -- old ones with an _

327330 mkClause args (l, r)

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

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

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

332+ lhs = PApp fc (PRef fc n)

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

330338

331339 elabArgs ina failed retry [] _

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

src/Idris/Error.hs+6

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

5858 _ -> return ()

5959 throwIO (IErr $ pshow i err)

6060

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+

6167getErrLine str

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

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

src/Idris/IBC.hs+15

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

959959 PMutual x1 x2 -> do putWord8 11

960960 put x1

961961 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

962970 get

963971 = do i <- getWord8

964972 case i of

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

10271035 11 -> do x1 <- get

10281036 x2 <- get

10291037 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)

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

10311046

10321047instance Binary SyntaxInfo where

src/Idris/Parser.hs+61−39

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

9797 mapM_ (addIBC . IBCImport) modules

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

9999 f rest pos

100− let ds = namespaces mname ds'

101− logLvl 3 (dumpDecls ds)

102− i <- getIState

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

104− logLvl 3 (show (idris_infixes i))

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

106− v <- verbose

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

108− elabDecls toplevel ds

109− i <- get

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

111− -- a better chance

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

113− updateContext (simplifyCasedef n))

114− (map snd (idris_totcheck i))

115− -- build size change graph from simplified definitions

116− iLOG "Totality checking"

117− i <- get

118−-- mapM_ buildSCG (idris_totcheck i)

119− mapM_ checkDeclTotality (idris_totcheck i)

120− iLOG ("Finished " ++ f)

121− ibcsd <- valIBCSubDir i

122− let ibc = ibcPathNoFallback ibcsd f

123− iLOG "Universe checking"

124− iucheck

125− i <- getIState

126− addHides (hide_list i)

127− ok <- noErrors

128− when ok $

129− idrisCatch (do writeIBC f ibc; clearIBC)

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

131− i <- getIState

132− putIState (i { default_total = def_total,

133− hide_list = [] })

100+ unless (null ds') $ do

101+ let ds = namespaces mname ds'

102+ logLvl 3 (dumpDecls ds)

103+ i <- getIState

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

105+ logLvl 3 (show (idris_infixes i))

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

107+ v <- verbose

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

109+ elabDecls toplevel ds

110+ i <- get

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

112+ -- a better chance

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

114+ updateContext (simplifyCasedef n))

115+ (map snd (idris_totcheck i))

116+ -- build size change graph from simplified definitions

117+ iLOG "Totality checking"

118+ i <- get

119+ -- mapM_ buildSCG (idris_totcheck i)

120+ mapM_ checkDeclTotality (idris_totcheck i)

121+ iLOG ("Finished " ++ f)

122+ ibcsd <- valIBCSubDir i

123+ let ibc = ibcPathNoFallback ibcsd f

124+ iLOG "Universe checking"

125+ iucheck

126+ i <- getIState

127+ addHides (hide_list i)

128+ ok <- noErrors

129+ when ok $

130+ idrisCatch (do writeIBC f ibc; clearIBC)

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

132+ i <- getIState

133+ putIState (i { default_total = def_total,

134+ hide_list = [] })

135+ return ()

134136 return ()

135137 where

136138 namespaces [] ds = ds

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

277279 eof

278280 i' <- getState

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

280− Left err -> fail (show err)

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

283+ return []

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

282285 return (collect x)

283286

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

415418

416419pFunDecl' :: SyntaxInfo -> IParser PDecl

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

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

419−-- let doc = ""

420421 pushIndent

421422 ist <- getState

422423 let initOpts = if default_total ist

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

433434-- ty' <- implicit syn n ty

434435 addAcc n acc

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

437+ <|> try (pPostulate syn)

436438 <|> try (pPattern syn)

437439 <|> try (pCAF syn)

438440

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+

439461pUsing :: SyntaxInfo -> IParser [PDecl]

440462pUsing syn =

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

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

491513 })

492514 fc <- pfc

493515 return (PFix fc (f prec) ops)

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

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

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

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

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

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

498520