dccbc43 · Idris-dev · git.iko.soy

git.iko.soy/Idris-dev

on master help sign in

Generate bytecode so that files don't need to be rechecked every time they're loaded

dccbc43Edwin Brady15 years ago

Makefile+1−1

compare with master

unifiedsplit

@@ -1,6 +1,6 @@

1install: .PHONY

2 cabal install

3− make -C lib check

3+ make -C lib recheck

5pinstall: .PHONY

6 cabal configure --enable-executable-profiling

idris.cabal+2−2

@@ -18,7 +18,7 @@ Description: Idris is an experimental language with full dependent types.

18Cabal-Version: >= 1.6

19Build-type: Simple

21−Data-files: *.idr prelude/*.idr

21+Data-files: *.idr prelude/*.idr *.ibc prelude/*.ibc

22Data-dir: lib

24Executable idris

@@ -39,7 +39,7 @@ Executable idris

40 Build-depends: base>=4 && <5, parsec, mtl, Cabal, readline,

41 containers, process, transformers, filepath, directory,

42− binary, derive, epic>=0.9.1

42+ binary, bytestring, unix, epic>=0.9.1

44 Extensions: MultiParamTypeClasses, FunctionalDependencies,

45 FlexibleInstances, TemplateHaskell

lib/Makefile+6

@@ -5,4 +5,10 @@ check: .PHONY

5 idris --noprelude --check $$x; \

6 done

8+recheck: clean check

10+clean: .PHONY

11+ rm -f *.ibc

12+ rm -f prelude/*.ibc

13+

8.PHONY:

14.PHONY:

src/Core/CaseTree.hs+7−1

@@ -13,11 +13,17 @@ data SC = Case Name [CaseAlt]

13 | STerm Term

14 | UnmatchedCase String -- error message

15 deriving Show

16+{-!

17+deriving instance Binary SC

18+!-}

17data CaseAlt = ConCase Name Int [Name] SC

20data CaseAlt = ConCase Name Int [Name] SC

18 | ConstCase Const SC

21 | ConstCase Const SC

19 | DefaultCase SC

22 | DefaultCase SC

20 deriving Show

23 deriving Show

24+{-!

25+deriving instance Binary CaseAlt

26+!-}

22type CaseTree = SC

28type CaseTree = SC

23type Clause = ([Pat], Term)

29type Clause = ([Pat], Term)

@@ -191,7 +197,7 @@ varRule (v : vs) alts err =

191 do let alts' = map (repVar v) alts

197 do let alts' = map (repVar v) alts

192 match vs alts' err

198 match vs alts' err

193 where

199 where

194− repVar v (PV p : ps , res) = (ps, subst p (P Bound v undefined) res)

200+ repVar v (PV p : ps , res) = (ps, subst p (P Bound v (V 0)) res)

195 repVar v (PAny : ps , res) = (ps, res)

201 repVar v (PAny : ps , res) = (ps, res)

196

202

197{-

203{-

src/Core/Constraints.hs+1

@@ -40,6 +40,7 @@ acyclic r cvs = checkCycle (FC "root" 0) r [] 0 cvs

40 let r' = M.insert c [] r

41 checkCycle fc r' path inc cs

43+ check fc path inc (UVar x) | x < 0 = return ()

43 check fc path inc cv

44 check fc path inc cv

44 | inc > 0 && cv `elem` path = Error $ At fc UniverseError

45 | inc > 0 && cv `elem` path = Error $ At fc UniverseError

45 | otherwise = case M.lookup cv r of

46 | otherwise = case M.lookup cv r of

src/Core/Evaluate.hs+17−2

@@ -4,7 +4,8 @@

4module Core.Evaluate(normalise, normaliseC, simplify, specialise, hnf,

5 Def(..),

6 Context, initContext, ctxtAlist, uconstraints, next_tvar,

7− addToCtxt, addTyDecl, addDatatype, addCasedef, addOperator,

7+ addToCtxt, addCtxtDef, addTyDecl, addDatatype,

8+ addCasedef, addOperator,

8 lookupTy, lookupP, lookupDef, lookupVal, lookupTyEnv,

9 lookupTy, lookupP, lookupDef, lookupVal, lookupTyEnv,

9 Value(..)) where

10 Value(..)) where

@@ -415,7 +416,7 @@ eval_hnf ctxt statics genv tm = ev [] tm where

415-- evaluator

416-- evaluator

416

417

417spec :: Context -> Ctxt [Bool] -> Env -> TT Name -> Eval (TT Name)

418spec :: Context -> Ctxt [Bool] -> Env -> TT Name -> Eval (TT Name)

418−spec ctxt statics genv tm = undefined

419+spec ctxt statics genv tm = error "spec undefined"

419

420

420-- CONTEXTS -----------------------------------------------------------------

421-- CONTEXTS -----------------------------------------------------------------

421

422

@@ -429,6 +430,9 @@ data Def = Function Type Term

429 | TyDecl NameType Type

430 | TyDecl NameType Type

430 | Operator Type Int ([Value] -> Maybe Value)

431 | Operator Type Int ([Value] -> Maybe Value)

431 | CaseOp Bool Type [(Term, Term)] [Name] SC -- Bool for inlineable

432 | CaseOp Bool Type [(Term, Term)] [Name] SC -- Bool for inlineable

433+{-!

434+deriving instance Binary Def

435+!-}

432

436

433instance Show Def where

437instance Show Def where

434 show (Function ty tm) = "Function: " ++ show (ty, tm)

438 show (Function ty tm) = "Function: " ++ show (ty, tm)

@@ -436,6 +440,12 @@ instance Show Def where

436 show (Operator ty _ _) = "Operator: " ++ show ty

440 show (Operator ty _ _) = "Operator: " ++ show ty

437 show (CaseOp _ ty ps ns sc) = "Case: " ++ show ps ++ "\n" ++

441 show (CaseOp _ ty ps ns sc) = "Case: " ++ show ps ++ "\n" ++

438 show ns ++ " " ++ show sc

442 show ns ++ " " ++ show sc

443+-- We need this for serialising Def. Fortunately, it never gets used because

444+-- we'll never serialise a primitive operator

445+

446+instance Binary (a -> b) where

447+ put x = return ()

448+ get = error "Getting a function"

439

449

440-------

450-------

441

451

@@ -456,6 +466,11 @@ addToCtxt n tm ty uctxt

456 ctxt' = addDef n (Function ty tm) ctxt in

466 ctxt' = addDef n (Function ty tm) ctxt in

457 uctxt { definitions = ctxt' }

467 uctxt { definitions = ctxt' }

458

468

469+addCtxtDef :: Name -> Def -> Context -> Context

470+addCtxtDef n d c = let ctxt = definitions c

471+ ctxt' = addDef n d ctxt in

472+ c { definitions = ctxt' }

473+

459addTyDecl :: Name -> Type -> Context -> Context

474addTyDecl :: Name -> Type -> Context -> Context

460addTyDecl n ty uctxt

475addTyDecl n ty uctxt

461 = let ctxt = definitions uctxt

476 = let ctxt = definitions uctxt

src/Core/TT.hs+29

@@ -30,6 +30,9 @@ data Option = SetInSet

30data FC = FC { fc_fname :: String,

31 fc_line :: Int }

32 deriving Eq

33+{-!

34+deriving instance Binary FC

35+!-}

34instance Show FC where

37instance Show FC where

35 show (FC f l) = f ++ ":" ++ show l

38 show (FC f l) = f ++ ":" ++ show l

@@ -96,6 +99,9 @@ data Name = UN String

96 | NS Name [String] -- root, namespaces

99 | NS Name [String] -- root, namespaces

97 | MN Int String

100 | MN Int String

98 deriving (Eq, Ord)

101 deriving (Eq, Ord)

102+{-!

103+deriving instance Binary Name

104+!-}

105

100instance Show Name where

106instance Show Name where

101 show (UN n) = n

107 show (UN n) = n

@@ -160,6 +166,9 @@ data Const = I Int | BI Integer | Fl Double | Ch Char | Str String

161 | PtrType

167 | PtrType

162 deriving Eq

168 deriving Eq

169+{-!

170+deriving instance Binary Const

171+!-}

163

172

164data Raw = Var Name

173data Raw = Var Name

165 | RBind Name (Binder Raw) Raw

174 | RBind Name (Binder Raw) Raw

@@ -167,6 +176,9 @@ data Raw = Var Name

167 | RSet

176 | RSet

168 | RConstant Const

177 | RConstant Const

169 deriving (Show, Eq)

178 deriving (Show, Eq)

179+{-!

180+deriving instance Binary Raw

181+!-}

170

182

171data Binder b = Lam { binderTy :: b }

183data Binder b = Lam { binderTy :: b }

172 | Pi { binderTy :: b }

184 | Pi { binderTy :: b }

@@ -181,6 +193,9 @@ data Binder b = Lam { binderTy :: b }

181 | PVar { binderTy :: b }

193 | PVar { binderTy :: b }

182 | PVTy { binderTy :: b }

194 | PVTy { binderTy :: b }

183 deriving (Show, Eq, Functor)

195 deriving (Show, Eq, Functor)

196+{-!

197+deriving instance Binary Binder

198+!-}

184

199

185fmapMB :: Monad m => (a -> m b) -> Binder a -> m (Binder b)

200fmapMB :: Monad m => (a -> m b) -> Binder a -> m (Binder b)

186fmapMB f (Let t v) = liftM2 Let (f t) (f v)

201fmapMB f (Let t v) = liftM2 Let (f t) (f v)

@@ -218,6 +233,14 @@ data UExp = UVar Int -- universe variable

218 | UVal Int -- explicit universe level

233 | UVal Int -- explicit universe level

219 deriving (Eq, Ord)

234 deriving (Eq, Ord)

220

235

236+-- We assume that universe levels have been checked, so anything external

237+-- can just have the same universe variable and we won't get any new

238+-- cycles.

239+

240+instance Binary UExp where

241+ put x = return ()

242+ get = return (UVar (-1))

243+

221instance Show UExp where

244instance Show UExp where

222 show (UVar x) | x < 26 = [toEnum (x + fromEnum 'a')]

245 show (UVar x) | x < 26 = [toEnum (x + fromEnum 'a')]

223 | otherwise = toEnum ((x `mod` 26) + fromEnum 'a') : show (x `div` 26)

246 | otherwise = toEnum ((x `mod` 26) + fromEnum 'a') : show (x `div` 26)

@@ -236,6 +259,9 @@ type UCs = (Int, [UConstraint])

236

259

237data NameType = Bound | Ref | DCon Int Int | TCon Int Int

260data NameType = Bound | Ref | DCon Int Int | TCon Int Int

238 deriving (Show, Eq)

261 deriving (Show, Eq)

262+{-!

263+deriving instance Binary NameType

264+!-}

239

265

240data TT n = P NameType n (TT n) -- embed type

266data TT n = P NameType n (TT n) -- embed type

241 | V Int

267 | V Int

@@ -244,6 +270,9 @@ data TT n = P NameType n (TT n) -- embed type

244 | Constant Const

270 | Constant Const

245 | Set UExp

271 | Set UExp

246 deriving Functor

272 deriving Functor

273+{-!

274+deriving instance Binary TT

275+!-}

247

276

248type EnvTT n = [(n, Binder (TT n))]

277type EnvTT n = [(n, Binder (TT n))]

249

278

src/Idris/AbsSyntax.hs+37−1

@@ -56,7 +56,6 @@ data IBCWrite = IBCFix FixDecl

56 | IBCImp Name

57 | IBCStatic Name

58 | IBCClass Name

59− | IBCMeta Name

60 | IBCSyntax Syntax

59 | IBCSyntax Syntax

61 | IBCKeyword String

60 | IBCKeyword String

62 | IBCImport FilePath

61 | IBCImport FilePath

@@ -235,6 +234,9 @@ data Fixity = Infixl { prec :: Int }

235 | InfixN { prec :: Int }

234 | InfixN { prec :: Int }

236 | PrefixN { prec :: Int }

235 | PrefixN { prec :: Int }

237 deriving Eq

236 deriving Eq

237+{-!

238+deriving instance Binary Fixity

239+!-}

238

240

239instance Show Fixity where

241instance Show Fixity where

240 show (Infixl i) = "infixl " ++ show i

242 show (Infixl i) = "infixl " ++ show i

@@ -244,6 +246,9 @@ instance Show Fixity where

244

246

245data FixDecl = Fix Fixity String

247data FixDecl = Fix Fixity String

246 deriving (Show, Eq)

248 deriving (Show, Eq)

249+{-!

250+deriving instance Binary FixDecl

251+!-}

247

252

248instance Ord FixDecl where

253instance Ord FixDecl where

249 compare (Fix x _) (Fix y _) = compare (prec x) (prec y)

254 compare (Fix x _) (Fix y _) = compare (prec x) (prec y)

@@ -251,6 +256,9 @@ instance Ord FixDecl where

251

256

252data Static = Static | Dynamic

257data Static = Static | Dynamic

253 deriving (Show, Eq)

258 deriving (Show, Eq)

259+{-!

260+deriving instance Binary Static

261+!-}

254

262

255-- Mark bindings with their explicitness, and laziness

263-- Mark bindings with their explicitness, and laziness

256data Plicity = Imp { plazy :: Bool,

264data Plicity = Imp { plazy :: Bool,

@@ -261,6 +269,10 @@ data Plicity = Imp { plazy :: Bool,

261 pstatic :: Static }

269 pstatic :: Static }

262 deriving (Show, Eq)

270 deriving (Show, Eq)

263

271

272+{-!

273+deriving instance Binary Plicity

274+!-}

275+

264impl = Imp False Dynamic

276impl = Imp False Dynamic

265expl = Exp False Dynamic

277expl = Exp False Dynamic

266constraint = Constraint False Static

278constraint = Constraint False Static

@@ -370,6 +382,9 @@ data PTerm = PQuote Raw

370 | PElabError String -- error to report on elaboration

382 | PElabError String -- error to report on elaboration

371 | PImpossible -- special case for declaring when an LHS can't typecheck

383 | PImpossible -- special case for declaring when an LHS can't typecheck

372 deriving Eq

384 deriving Eq

385+{-!

386+deriving instance Binary PTerm

387+!-}

373

388

374mapPT :: (PTerm -> PTerm) -> PTerm -> PTerm

389mapPT :: (PTerm -> PTerm) -> PTerm -> PTerm

375mapPT f t = f (mpt t) where

390mapPT f t = f (mpt t) where

@@ -398,6 +413,9 @@ data PTactic' t = Intro [Name] | Focus Name

398 | TSeq (PTactic' t) (PTactic' t)

413 | TSeq (PTactic' t) (PTactic' t)

399 | Qed

414 | Qed

400 deriving (Show, Eq, Functor)

415 deriving (Show, Eq, Functor)

416+{-!

417+deriving instance Binary PTactic'

418+!-}

401

419

402type PTactic = PTactic' PTerm

420type PTactic = PTactic' PTerm

403

421

@@ -405,6 +423,9 @@ data PDo' t = DoExp FC t

405 | DoBind FC Name t

423 | DoBind FC Name t

406 | DoLet FC Name t

424 | DoLet FC Name t

407 deriving (Eq, Functor)

425 deriving (Eq, Functor)

426+{-!

427+deriving instance Binary PDo'

428+!-}

408

429

409type PDo = PDo' PTerm

430type PDo = PDo' PTerm

410

431

@@ -419,6 +440,9 @@ data PArg' t = PImp { priority :: Int,

419 | PConstraint { priority :: Int,

440 | PConstraint { priority :: Int,

420 lazyarg :: Bool, getTm :: t }

441 lazyarg :: Bool, getTm :: t }

421 deriving (Show, Eq, Functor)

442 deriving (Show, Eq, Functor)

443+{-!

444+deriving instance Binary PArg'

445+!-}

422

446

423pimp = PImp 0 False

447pimp = PImp 0 False

424pexp = PExp 0 False

448pexp = PExp 0 False

@@ -433,6 +457,9 @@ data ClassInfo = CI { instanceName :: Name,

433 class_defaults :: [(Name, Name)], -- method name -> default impl

457 class_defaults :: [(Name, Name)], -- method name -> default impl

434 class_params :: [Name] }

458 class_params :: [Name] }

435 deriving Show

459 deriving Show

460+{-!

461+deriving instance Binary ClassInfo

462+!-}

436

463

437-- Syntactic sugar info

464-- Syntactic sugar info

438

465

@@ -442,14 +469,23 @@ data DSL = DSL { dsl_bind :: Name,

442

469

443data SynContext = PatternSyntax | TermSyntax | AnySyntax

470data SynContext = PatternSyntax | TermSyntax | AnySyntax

444 deriving Show

471 deriving Show

472+{-!

473+deriving instance Binary SynContext

474+!-}

445

475

446data Syntax = Rule [SSymbol] PTerm SynContext

476data Syntax = Rule [SSymbol] PTerm SynContext

447 deriving Show

477 deriving Show

478+{-!

479+deriving instance Binary Syntax

480+!-}

448

481

449data SSymbol = Keyword Name

482data SSymbol = Keyword Name

450 | Symbol String

483 | Symbol String

451 | Expr Name

484 | Expr Name

452 deriving Show

485 deriving Show

486+{-!

487+deriving instance Binary SSymbol

488+!-}

453

489

454initDSL = DSL (UN ">>=") (UN "return")

490initDSL = DSL (UN ">>=") (UN "return")

455

491

src/Idris/ElabDecls.hs+1−1

@@ -339,7 +339,7 @@ elabClass info syn fc constraints tn ps ds

339 let defaults = map (\ (x, (y, z)) -> (x,y)) defs

340 put (i { idris_classes = addDef tn (CI cn imethods defaults (map fst ps))

341 (idris_classes i) })

342− addIBC (IBCClass cn)

342+ addIBC (IBCClass tn)

343 where

344 pibind [] x = x

345 pibind ((n, ty): ns) x = PPi expl n ty (pibind ns x)

src/Idris/IBC.hs+902−46

@@ -1,4 +1,4 @@

1−{-# LANGUAGE TypeSynonymInstances, TemplateHaskell #-}

1+{-# LANGUAGE TypeSynonymInstances #-}

3module Idris.IBC where

@@ -7,17 +7,26 @@ import Core.TT

7import Core.CaseTree

8import Idris.Compiler

9import Idris.AbsSyntax

10+import Idris.Imports

11import Data.Binary

12import Data.Binary

12import Data.List

13import Data.List

14+import Data.ByteString.Lazy as B hiding (length, elem)

13−import Data.DeriveTH

15+-- import Data.DeriveTH

14import Control.Monad

16import Control.Monad

17+import Control.Monad.State hiding (get, put)

18+import System.FilePath

19+import System.Posix.Files

20+

21+import Paths_idris

16ibcVersion :: Word8

23ibcVersion :: Word8

17−ibcVersion = 1

24+ibcVersion = 3

19data IBCFile = IBCFile { ver :: Word8,

26data IBCFile = IBCFile { ver :: Word8,

27+ sourcefile :: FilePath,

20 ibc_imports :: [FilePath],

28 ibc_imports :: [FilePath],

29+ ibc_implicits :: [(Name, [PArg])],

21 ibc_fixes :: [FixDecl],

30 ibc_fixes :: [FixDecl],

22 ibc_statics :: [(Name, [Bool])],

31 ibc_statics :: [(Name, [Bool])],

23 ibc_classes :: [(Name, ClassInfo)],

32 ibc_classes :: [(Name, ClassInfo)],

@@ -27,59 +36,906 @@ data IBCFile = IBCFile { ver :: Word8,

27 ibc_libs :: [String],

36 ibc_libs :: [String],

28 ibc_hdrs :: [String],

37 ibc_hdrs :: [String],

29 ibc_defs :: [(Name, Def)] }

38 ibc_defs :: [(Name, Def)] }

39+{-!

40+deriving instance Binary IBCFile

41+!-}

31initIBC :: IBCFile

43initIBC :: IBCFile

32−initIBC = IBCFile ibcVersion [] [] [] [] [] [] [] [] [] []

44+initIBC = IBCFile ibcVersion "" [] [] [] [] [] [] [] [] [] [] []

34loadIBC :: FilePath -> Idris ()

46loadIBC :: FilePath -> Idris ()

35−loadIBC fp = fail "Not implemented"

47+loadIBC fp = do iLOG $ "Loading ibc " ++ fp

48+ ibcf <- lift $ (decodeFile fp :: IO IBCFile)

49+ process ibcf fp

37−writeIBC :: FilePath -> Idris ()

51+writeIBC :: FilePath -> FilePath -> Idris ()

38−writeIBC f

52+writeIBC src f

39 = do iLOG $ "Writing ibc " ++ show f

53 = do iLOG $ "Writing ibc " ++ show f

40 i <- getIState

54 i <- getIState

41 case idris_metavars i \\ primDefs of

55 case idris_metavars i \\ primDefs of

42 (_:_) -> fail "Can't write ibc when there are unsolve metavariables"

56 (_:_) -> fail "Can't write ibc when there are unsolve metavariables"

43 [] -> return ()

57 [] -> return ()

58+ ibcf <- mkIBC (ibc_write i) (initIBC { sourcefile = src })

59+ lift $ encodeFile f ibcf

60+ iLOG $ "Written"

44 return ()

61 return ()

46−$( derive makeBinary ''IBCFile )

63+mkIBC :: [IBCWrite] -> IBCFile -> Idris IBCFile

47−$( derive makeBinary ''PTerm )

64+mkIBC [] f = return f

48−$( derive makeBinary ''Raw )

65+mkIBC (i:is) f = do ist <- getIState

49−$( derive makeBinary ''PTactic' )

66+ logLvl 5 $ show i ++ " " ++ show (Data.List.length is)

50−$( derive makeBinary ''PDo' )

67+ f' <- ibc ist i f

51−$( derive makeBinary ''PArg' )

68+ mkIBC is f'

52−$( derive makeBinary ''ClassInfo )

69+

53−$( derive makeBinary ''Plicity )

70+ibc i (IBCFix d) f = return f { ibc_fixes = d : ibc_fixes f }

54−$( derive makeBinary ''FC )

71+ibc i (IBCImp n) f = case lookupCtxt Nothing n (idris_implicits i) of

55−$( derive makeBinary ''Syntax )

72+ [v] -> return f { ibc_implicits = (n,v): ibc_implicits f }

56−$( derive makeBinary ''SynContext )

73+ _ -> fail "IBC write failed"

57−$( derive makeBinary ''SSymbol )

74+ibc i (IBCStatic n) f

58−$( derive makeBinary ''Static )

75+ = case lookupCtxt Nothing n (idris_statics i) of

59−$( derive makeBinary ''Fixity )

76+ [v] -> return f { ibc_statics = (n,v): ibc_statics f }

60−$( derive makeBinary ''FixDecl )

77+ _ -> fail "IBC write failed"

61−

78+ibc i (IBCClass n) f

62−$( derive makeBinary ''Def )

79+ = case lookupCtxt Nothing n (idris_classes i) of

63−$( derive makeBinary ''SC )

80+ [v] -> return f { ibc_classes = (n,v): ibc_classes f }

64−$( derive makeBinary ''CaseAlt )

81+ _ -> fail "IBC write failed"

65−$( derive makeBinary ''NameType )

82+ibc i (IBCSyntax n) f = return f { ibc_syntax = n : ibc_syntax f }

66−$( derive makeBinary ''Name )

83+ibc i (IBCKeyword n) f = return f { ibc_keywords = n : ibc_keywords f }

67−$( derive makeBinary ''Binder )

84+ibc i (IBCImport n) f = return f { ibc_imports = n : ibc_imports f }

68−$( derive makeBinary ''TT )

85+ibc i (IBCObj n) f = return f { ibc_objs = n : ibc_objs f }

69−$( derive makeBinary ''Const )

86+ibc i (IBCLib n) f = return f { ibc_libs = n : ibc_libs f }

70−

87+ibc i (IBCHeader n) f = return f { ibc_hdrs = n : ibc_hdrs f }

71−-- We need this for serialising Def. Fortunately, it never gets used because

88+ibc i (IBCDef n) f = case lookupDef Nothing n (tt_ctxt i) of

72−-- we'll never serialise a primitive operator

89+ [v] -> return f { ibc_defs = (n,v): ibc_defs f }

73−

90+ _ -> fail "IBC write failed"

74−instance Binary (a -> b) where

91+

75− put x = return ()

92+process :: IBCFile -> FilePath -> Idris ()

76− get = undefined

93+process i fn

77−

94+ | ver i /= ibcVersion = do iLOG "ibc out of date"

78−-- We assume that universe levels have been checked, so anything external

95+ fail "Incorrect ibc version"

79−-- can just have the same universe variable and we won't get any new

96+ | otherwise =

80−-- cycles.

97+ do lift $ timestampOlder (sourcefile i) fn

81−

98+ pImports (ibc_imports i)

82−instance Binary UExp where

99+ pImps (ibc_implicits i)

83− put x = return ()

100+ pFixes (ibc_fixes i)

84− get = return (UVar (-1))

101+ pStatics (ibc_statics i)

102+ pClasses (ibc_classes i)

103+ pSyntax (ibc_syntax i)

104+ pKeywords (ibc_keywords i)

105+ pObjs (ibc_objs i)

106+ pLibs (ibc_libs i)

107+ pHdrs (ibc_hdrs i)

108+ pDefs (ibc_defs i)

109+

110+timestampOlder :: FilePath -> FilePath -> IO ()

111+timestampOlder src ibc = do srcs <- getFileStatus src

112+ ibcs <- getFileStatus ibc

113+ if (modificationTime srcs > modificationTime ibcs)

114+ then fail "Needs reloading"

115+ else return ()

116+

117+pImports :: [FilePath] -> Idris ()

118+pImports fs

119+ = do datadir <- lift $ getDataDir

120+ mapM_ (\f -> do fp <- lift $ findImport [".", datadir] f

121+ i <- getIState

122+ if (f `elem` imported i)

123+ then iLOG $ "Already read " ++ f

124+ else do putIState (i { imported = f : imported i })

125+ case fp of

126+ IDR fn -> do iLOG $ "Failed at " ++ fn

127+ fail "Must be an ibc"

128+ IBC fn src -> loadIBC fn)

129+ fs

130+

131+pImps :: [(Name, [PArg])] -> Idris ()

132+pImps imps = mapM_ (\ (n, imp) ->

133+ do i <- getIState

134+ putIState (i { idris_implicits

135+ = addDef n imp (idris_implicits i) }))

136+ imps

137+

138+pFixes :: [FixDecl] -> Idris ()

139+pFixes f = do i <- getIState

140+ putIState (i { idris_infixes = f ++ idris_infixes i })

141+

142+pStatics :: [(Name, [Bool])] -> Idris ()

143+pStatics ss = mapM_ (\ (n, s) ->

144+ do i <- getIState

145+ putIState (i { idris_statics

146+ = addDef n s (idris_statics i) }))

147+ ss

148+

149+pClasses :: [(Name, ClassInfo)] -> Idris ()

150+pClasses cs = mapM_ (\ (n, c) ->

151+ do i <- getIState

152+ putIState (i { idris_classes

153+ = addDef n c (idris_classes i) }))

154+ cs

155+

156+pSyntax :: [Syntax] -> Idris ()

157+pSyntax s = do i <- getIState

158+ putIState (i { syntax_rules = s ++ syntax_rules i })

159+

160+pKeywords :: [String] -> Idris ()

161+pKeywords k = do i <- getIState

162+ putIState (i { syntax_keywords = k ++ syntax_keywords i })

163+

164+pObjs :: [FilePath] -> Idris ()

165+pObjs os = mapM_ addObjectFile os

166+

167+pLibs :: [String] -> Idris ()

168+pLibs ls = mapM_ addLib ls

169+

170+pHdrs :: [String] -> Idris ()

171+pHdrs hs = mapM_ addHdr hs

172+

173+pDefs :: [(Name, Def)] -> Idris ()

174+pDefs ds = mapM_ (\ (n, d) ->

175+ do i <- getIState

176+ putIState (i { tt_ctxt = addCtxtDef n d (tt_ctxt i) }))

177+ ds

178+

179+

180+----- Generated by 'derive'

181+

182+

183+instance Binary FC where

184+ put (FC x1 x2)

185+ = do put x1

186+ put x2

187+ get

188+ = do x1 <- get

189+ x2 <- get

190+ return (FC x1 x2)

191+

192+

193+instance Binary Name where

194+ put x

195+ = case x of

196+ UN x1 -> do putWord8 0

197+ put x1

198+ NS x1 x2 -> do putWord8 1

199+ put x1

200+ put x2

201+ MN x1 x2 -> do putWord8 2

202+ put x1

203+ put x2

204+ get

205+ = do i <- getWord8

206+ case i of

207+ 0 -> do x1 <- get

208+ return (UN x1)

209+ 1 -> do x1 <- get

210+ x2 <- get

211+ return (NS x1 x2)

212+ 2 -> do x1 <- get

213+ x2 <- get

214+ return (MN x1 x2)

215+ _ -> error "Corrupted binary data for Name"

216+

217+

218+instance Binary Const where

219+ put x

220+ = case x of

221+ I x1 -> do putWord8 0

222+ put x1

223+ BI x1 -> do putWord8 1

224+ put x1

225+ Fl x1 -> do putWord8 2

226+ put x1

227+ Ch x1 -> do putWord8 3

228+ put x1

229+ Str x1 -> do putWord8 4

230+ put x1

231+ IType -> putWord8 5

232+ BIType -> putWord8 6

233+ FlType -> putWord8 7

234+ ChType -> putWord8 8

235+ StrType -> putWord8 9

236+ PtrType -> putWord8 10

237+ get

238+ = do i <- getWord8

239+ case i of

240+ 0 -> do x1 <- get

241+ return (I x1)

242+ 1 -> do x1 <- get

243+ return (BI x1)

244+ 2 -> do x1 <- get

245+ return (Fl x1)

246+ 3 -> do x1 <- get

247+ return (Ch x1)

248+ 4 -> do x1 <- get

249+ return (Str x1)

250+ 5 -> return IType

251+ 6 -> return BIType

252+ 7 -> return FlType

253+ 8 -> return ChType

254+ 9 -> return StrType

255+ 10 -> return PtrType

256+ _ -> error "Corrupted binary data for Const"

257+

258+

259+instance Binary Raw where

260+ put x

261+ = case x of

262+ Var x1 -> do putWord8 0

263+ put x1

264+ RBind x1 x2 x3 -> do putWord8 1

265+ put x1

266+ put x2

267+ put x3

268+ RApp x1 x2 -> do putWord8 2

269+ put x1

270+ put x2

271+ RSet -> putWord8 3

272+ RConstant x1 -> do putWord8 4

273+ put x1

274+ get

275+ = do i <- getWord8

276+ case i of

277+ 0 -> do x1 <- get

278+ return (Var x1)

279+ 1 -> do x1 <- get

280+ x2 <- get

281+ x3 <- get

282+ return (RBind x1 x2 x3)

283+ 2 -> do x1 <- get

284+ x2 <- get

285+ return (RApp x1 x2)

286+ 3 -> return RSet

287+ 4 -> do x1 <- get

288+ return (RConstant x1)

289+ _ -> error "Corrupted binary data for Raw"

290+

291+

292+instance (Binary b) => Binary (Binder b) where

293+ put x

294+ = case x of

295+ Lam x1 -> do putWord8 0

296+ put x1

297+ Pi x1 -> do putWord8 1

298+ put x1

299+ Let x1 x2 -> do putWord8 2

300+ put x1

301+ put x2

302+ NLet x1 x2 -> do putWord8 3

303+ put x1

304+ put x2

305+ Hole x1 -> do putWord8 4

306+ put x1

307+ GHole x1 -> do putWord8 5

308+ put x1

309+ Guess x1 x2 -> do putWord8 6

310+ put x1

311+ put x2

312+ PVar x1 -> do putWord8 7

313+ put x1

314+ PVTy x1 -> do putWord8 8

315+ put x1

316+ get

317+ = do i <- getWord8

318+ case i of

319+ 0 -> do x1 <- get

320+ return (Lam x1)

321+ 1 -> do x1 <- get

322+ return (Pi x1)

323+ 2 -> do x1 <- get

324+ x2 <- get

325+ return (Let x1 x2)

326+ 3 -> do x1 <- get

327+ x2 <- get

328+ return (NLet x1 x2)

329+ 4 -> do x1 <- get

330+ return (Hole x1)

331+ 5 -> do x1 <- get

332+ return (GHole x1)

333+ 6 -> do x1 <- get

334+ x2 <- get

335+ return (Guess x1 x2)

336+ 7 -> do x1 <- get

337+ return (PVar x1)

338+ 8 -> do x1 <- get

339+ return (PVTy x1)

340+ _ -> error "Corrupted binary data for Binder"

341+

342+

343+instance Binary NameType where

344+ put x

345+ = case x of

346+ Bound -> putWord8 0

347+ Ref -> putWord8 1

348+ DCon x1 x2 -> do putWord8 2

349+ put x1

350+ put x2

351+ TCon x1 x2 -> do putWord8 3

352+ put x1

353+ put x2

354+ get

355+ = do i <- getWord8

356+ case i of

357+ 0 -> return Bound

358+ 1 -> return Ref

359+ 2 -> do x1 <- get

360+ x2 <- get

361+ return (DCon x1 x2)

362+ 3 -> do x1 <- get

363+ x2 <- get

364+ return (TCon x1 x2)

365+ _ -> error "Corrupted binary data for NameType"

366+

367+

368+instance (Binary n) => Binary (TT n) where

369+ put x

370+ = case x of

371+ P x1 x2 x3 -> do putWord8 0

372+ put x1

373+ put x2

374+ put x3

375+ V x1 -> do putWord8 1

376+ put x1

377+ Bind x1 x2 x3 -> do putWord8 2

378+ put x1

379+ put x2

380+ put x3

381+ App x1 x2 -> do putWord8 3

382+ put x1

383+ put x2

384+ Constant x1 -> do putWord8 4

385+ put x1

386+ Set x1 -> do putWord8 5

387+ put x1

388+ get

389+ = do i <- getWord8

390+ case i of

391+ 0 -> do x1 <- get

392+ x2 <- get

393+ x3 <- get

394+ return (P x1 x2 x3)

395+ 1 -> do x1 <- get

396+ return (V x1)

397+ 2 -> do x1 <- get

398+ x2 <- get

399+ x3 <- get

400+ return (Bind x1 x2 x3)

401+ 3 -> do x1 <- get

402+ x2 <- get

403+ return (App x1 x2)

404+ 4 -> do x1 <- get

405+ return (Constant x1)

406+ 5 -> do x1 <- get

407+ return (Set x1)

408+ _ -> error "Corrupted binary data for TT"

409+

410+

411+instance Binary SC where

412+ put x

413+ = case x of

414+ Case x1 x2 -> do putWord8 0

415+ put x1

416+ put x2

417+ STerm x1 -> do putWord8 1

418+ put x1

419+ UnmatchedCase x1 -> do putWord8 2

420+ put x1

421+ get

422+ = do i <- getWord8

423+ case i of

424+ 0 -> do x1 <- get

425+ x2 <- get

426+ return (Case x1 x2)

427+ 1 -> do x1 <- get

428+ return (STerm x1)

429+ 2 -> do x1 <- get

430+ return (UnmatchedCase x1)

431+ _ -> error "Corrupted binary data for SC"

432+

433+

434+instance Binary CaseAlt where

435+ put x

436+ = case x of

437+ ConCase x1 x2 x3 x4 -> do putWord8 0

438+ put x1

439+ put x2

440+ put x3

441+ put x4

442+ ConstCase x1 x2 -> do putWord8 1

443+ put x1

444+ put x2

445+ DefaultCase x1 -> do putWord8 2

446+ put x1

447+ get

448+ = do i <- getWord8

449+ case i of

450+ 0 -> do x1 <- get

451+ x2 <- get

452+ x3 <- get

453+ x4 <- get

454+ return (ConCase x1 x2 x3 x4)

455+ 1 -> do x1 <- get

456+ x2 <- get

457+ return (ConstCase x1 x2)

458+ 2 -> do x1 <- get

459+ return (DefaultCase x1)

460+ _ -> error "Corrupted binary data for CaseAlt"

461+

462+

463+instance Binary Def where

464+ put x

465+ = case x of

466+ Function x1 x2 -> do putWord8 0

467+ put x1

468+ put x2

469+ TyDecl x1 x2 -> do putWord8 1

470+ put x1

471+ put x2

472+ Operator x1 x2 x3 -> do putWord8 2

473+ put x1

474+ put x2

475+ put x3

476+ CaseOp x1 x2 x3 x4 x5 -> do putWord8 3

477+ put x1

478+ put x2

479+ put x3

480+ put x4

481+ put x5

482+ get

483+ = do i <- getWord8

484+ case i of

485+ 0 -> do x1 <- get

486+ x2 <- get

487+ return (Function x1 x2)

488+ 1 -> do x1 <- get

489+ x2 <- get

490+ return (TyDecl x1 x2)

491+ 2 -> do x1 <- get

492+ x2 <- get

493+ x3 <- get

494+ return (Operator x1 x2 x3)

495+ 3 -> do x1 <- get

496+ x2 <- get

497+ x3 <- get

498+ x4 <- get

499+ x5 <- get

500+ return (CaseOp x1 x2 x3 x4 x5)

501+ _ -> error "Corrupted binary data for Def"

502+

503+

504+instance Binary IBCFile where

505+ put (IBCFile x1 x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13)

506+ = do put x1

507+ put x2

508+ put x3

509+ put x4

510+ put x5

511+ put x6

512+ put x7

513+ put x8

514+ put x9

515+ put x10

516+ put x11

517+ put x12

518+ put x13

519+ get

520+ = do x1 <- get

521+ if x1 == ibcVersion then

522+ do x2 <- get

523+ x3 <- get

524+ x4 <- get

525+ x5 <- get

526+ x6 <- get

527+ x7 <- get

528+ x8 <- get

529+ x9 <- get

530+ x10 <- get

531+ x11 <- get

532+ x12 <- get

533+ x13 <- get

534+ return (IBCFile x1 x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13)

535+ else return (initIBC { ver = x1 })

536+

537+instance Binary Fixity where

538+ put x

539+ = case x of

540+ Infixl x1 -> do putWord8 0

541+ put x1

542+ Infixr x1 -> do putWord8 1

543+ put x1

544+ InfixN x1 -> do putWord8 2

545+ put x1

546+ PrefixN x1 -> do putWord8 3

547+ put x1

548+ get

549+ = do i <- getWord8

550+ case i of

551+ 0 -> do x1 <- get

552+ return (Infixl x1)

553+ 1 -> do x1 <- get

554+ return (Infixr x1)

555+ 2 -> do x1 <- get

556+ return (InfixN x1)

557+ 3 -> do x1 <- get

558+ return (PrefixN x1)

559+ _ -> error "Corrupted binary data for Fixity"

560+

561+

562+instance Binary FixDecl where

563+ put (Fix x1 x2)

564+ = do put x1

565+ put x2

566+ get

567+ = do x1 <- get

568+ x2 <- get

569+ return (Fix x1 x2)

570+

571+

572+instance Binary Static where

573+ put x

574+ = case x of

575+ Static -> putWord8 0

576+ Dynamic -> putWord8 1

577+ get

578+ = do i <- getWord8

579+ case i of

580+ 0 -> return Static

581+ 1 -> return Dynamic

582+ _ -> error "Corrupted binary data for Static"

583+

584+

585+instance Binary Plicity where

586+ put x

587+ = case x of

588+ Imp x1 x2 -> do putWord8 0

589+ put x1

590+ put x2

591+ Exp x1 x2 -> do putWord8 1

592+ put x1

593+ put x2

594+ Constraint x1 x2 -> do putWord8 2

595+ put x1

596+ put x2

597+ get

598+ = do i <- getWord8

599+ case i of

600+ 0 -> do x1 <- get

601+ x2 <- get

602+ return (Imp x1 x2)

603+ 1 -> do x1 <- get

604+ x2 <- get

605+ return (Exp x1 x2)

606+ 2 -> do x1 <- get

607+ x2 <- get

608+ return (Constraint x1 x2)

609+ _ -> error "Corrupted binary data for Plicity"

610+

611+

612+instance Binary PTerm where

613+ put x

614+ = case x of

615+ PQuote x1 -> do putWord8 0

616+ put x1

617+ PRef x1 x2 -> do putWord8 1

618+ put x1

619+ put x2

620+ PLam x1 x2 x3 -> do putWord8 2

621+ put x1

622+ put x2

623+ put x3

624+ PPi x1 x2 x3 x4 -> do putWord8 3

625+ put x1

626+ put x2

627+ put x3

628+ put x4

629+ PLet x1 x2 x3 x4 -> do putWord8 4

630+ put x1

631+ put x2

632+ put x3

633+ put x4

634+ PApp x1 x2 x3 -> do putWord8 5

635+ put x1

636+ put x2

637+ put x3

638+ PTrue x1 -> do putWord8 6

639+ put x1

640+ PFalse x1 -> do putWord8 7

641+ put x1

642+ PRefl x1 -> do putWord8 8

643+ put x1

644+ PResolveTC x1 -> do putWord8 9

645+ put x1

646+ PEq x1 x2 x3 -> do putWord8 10

647+ put x1

648+ put x2

649+ put x3

650+ PPair x1 x2 x3 -> do putWord8 11

651+ put x1

652+ put x2

653+ put x3

654+ PDPair x1 x2 x3 x4 -> do putWord8 12

655+ put x1

656+ put x2

657+ put x3

658+ put x4

659+ PAlternative x1 -> do putWord8 13

660+ put x1

661+ PHidden x1 -> do putWord8 14

662+ put x1

663+ PSet -> putWord8 15

664+ PConstant x1 -> do putWord8 16

665+ put x1

666+ Placeholder -> putWord8 17

667+ PDoBlock x1 -> do putWord8 18

668+ put x1

669+ PReturn x1 -> do putWord8 19

670+ put x1

671+ PMetavar x1 -> do putWord8 20

672+ put x1

673+ PProof x1 -> do putWord8 21

674+ put x1

675+ PTactics x1 -> do putWord8 22

676+ put x1

677+ PElabError x1 -> do putWord8 23

678+ put x1

679+ PImpossible -> putWord8 24

680+ get

681+ = do i <- getWord8

682+ case i of

683+ 0 -> do x1 <- get

684+ return (PQuote x1)

685+ 1 -> do x1 <- get

686+ x2 <- get

687+ return (PRef x1 x2)

688+ 2 -> do x1 <- get

689+ x2 <- get

690+ x3 <- get

691+ return (PLam x1 x2 x3)

692+ 3 -> do x1 <- get

693+ x2 <- get

694+ x3 <- get

695+ x4 <- get

696+ return (PPi x1 x2 x3 x4)

697+ 4 -> do x1 <- get

698+ x2 <- get

699+ x3 <- get

700+ x4 <- get

701+ return (PLet x1 x2 x3 x4)

702+ 5 -> do x1 <- get

703+ x2 <- get

704+ x3 <- get

705+ return (PApp x1 x2 x3)

706+ 6 -> do x1 <- get

707+ return (PTrue x1)

708+ 7 -> do x1 <- get

709+ return (PFalse x1)

710+ 8 -> do x1 <- get

711+ return (PRefl x1)

712+ 9 -> do x1 <- get

713+ return (PResolveTC x1)

714+ 10 -> do x1 <- get

715+ x2 <- get

716+ x3 <- get

717+ return (PEq x1 x2 x3)

718+ 11 -> do x1 <- get

719+ x2 <- get

720+ x3 <- get

721+ return (PPair x1 x2 x3)

722+ 12 -> do x1 <- get

723+ x2 <- get

724+ x3 <- get

725+ x4 <- get

726+ return (PDPair x1 x2 x3 x4)

727+ 13 -> do x1 <- get

728+ return (PAlternative x1)

729+ 14 -> do x1 <- get

730+ return (PHidden x1)

731+ 15 -> return PSet

732+ 16 -> do x1 <- get

733+ return (PConstant x1)

734+ 17 -> return Placeholder

735+ 18 -> do x1 <- get

736+ return (PDoBlock x1)

737+ 19 -> do x1 <- get

738+ return (PReturn x1)

739+ 20 -> do x1 <- get

740+ return (PMetavar x1)

741+ 21 -> do x1 <- get

742+ return (PProof x1)

743+ 22 -> do x1 <- get

744+ return (PTactics x1)

745+ 23 -> do x1 <- get

746+ return (PElabError x1)

747+ 24 -> return PImpossible

748+ _ -> error "Corrupted binary data for PTerm"

749+

750+

751+instance (Binary t) => Binary (PTactic' t) where

752+ put x

753+ = case x of

754+ Intro x1 -> do putWord8 0

755+ put x1

756+ Focus x1 -> do putWord8 1

757+ put x1

758+ Refine x1 x2 -> do putWord8 2

759+ put x1

760+ put x2

761+ Rewrite x1 -> do putWord8 3

762+ put x1

763+ LetTac x1 x2 -> do putWord8 4

764+ put x1

765+ put x2

766+ Exact x1 -> do putWord8 5

767+ put x1

768+ Compute -> putWord8 6

769+ Trivial -> putWord8 7

770+ Solve -> putWord8 8

771+ Attack -> putWord8 9

772+ ProofState -> putWord8 10

773+ ProofTerm -> putWord8 11

774+ Undo -> putWord8 12

775+ Try x1 x2 -> do putWord8 13

776+ put x1

777+ put x2

778+ TSeq x1 x2 -> do putWord8 14

779+ put x1

780+ put x2

781+ Qed -> putWord8 15

782+ get

783+ = do i <- getWord8

784+ case i of

785+ 0 -> do x1 <- get

786+ return (Intro x1)

787+ 1 -> do x1 <- get

788+ return (Focus x1)

789+ 2 -> do x1 <- get

790+ x2 <- get

791+ return (Refine x1 x2)

792+ 3 -> do x1 <- get

793+ return (Rewrite x1)

794+ 4 -> do x1 <- get

795+ x2 <- get

796+ return (LetTac x1 x2)

797+ 5 -> do x1 <- get

798+ return (Exact x1)

799+ 6 -> return Compute

800+ 7 -> return Trivial

801+ 8 -> return Solve

802+ 9 -> return Attack

803+ 10 -> return ProofState

804+ 11 -> return ProofTerm

805+ 12 -> return Undo

806+ 13 -> do x1 <- get

807+ x2 <- get

808+ return (Try x1 x2)

809+ 14 -> do x1 <- get

810+ x2 <- get

811+ return (TSeq x1 x2)

812+ 15 -> return Qed

813+ _ -> error "Corrupted binary data for PTactic'"

814+

815+

816+instance (Binary t) => Binary (PDo' t) where

817+ put x

818+ = case x of

819+ DoExp x1 x2 -> do putWord8 0

820+ put x1

821+ put x2

822+ DoBind x1 x2 x3 -> do putWord8 1

823+ put x1

824+ put x2

825+ put x3

826+ DoLet x1 x2 x3 -> do putWord8 2

827+ put x1

828+ put x2

829+ put x3

830+ get

831+ = do i <- getWord8

832+ case i of

833+ 0 -> do x1 <- get

834+ x2 <- get

835+ return (DoExp x1 x2)

836+ 1 -> do x1 <- get

837+ x2 <- get

838+ x3 <- get

839+ return (DoBind x1 x2 x3)

840+ 2 -> do x1 <- get

841+ x2 <- get

842+ x3 <- get

843+ return (DoLet x1 x2 x3)

844+ _ -> error "Corrupted binary data for PDo'"

845+

846+

847+instance (Binary t) => Binary (PArg' t) where

848+ put x

849+ = case x of

850+ PImp x1 x2 x3 x4 -> do putWord8 0

851+ put x1

852+ put x2

853+ put x3

854+ put x4

855+ PExp x1 x2 x3 -> do putWord8 1

856+ put x1

857+ put x2

858+ put x3

859+ PConstraint x1 x2 x3 -> do putWord8 2

860+ put x1

861+ put x2

862+ put x3

863+ get

864+ = do i <- getWord8

865+ case i of

866+ 0 -> do x1 <- get

867+ x2 <- get

868+ x3 <- get

869+ x4 <- get

870+ return (PImp x1 x2 x3 x4)

871+ 1 -> do x1 <- get

872+ x2 <- get

873+ x3 <- get

874+ return (PExp x1 x2 x3)

875+ 2 -> do x1 <- get

876+ x2 <- get

877+ x3 <- get

878+ return (PConstraint x1 x2 x3)

879+ _ -> error "Corrupted binary data for PArg'"

880+

881+

882+instance Binary ClassInfo where

883+ put (CI x1 x2 x3 x4)

884+ = do put x1

885+ put x2

886+ put x3

887+ put x4

888+ get

889+ = do x1 <- get

890+ x2 <- get

891+ x3 <- get

892+ x4 <- get

893+ return (CI x1 x2 x3 x4)

894+

895+

896+instance Binary SynContext where

897+ put x

898+ = case x of

899+ PatternSyntax -> putWord8 0

900+ TermSyntax -> putWord8 1

901+ AnySyntax -> putWord8 2

902+ get

903+ = do i <- getWord8

904+ case i of

905+ 0 -> return PatternSyntax

906+ 1 -> return TermSyntax

907+ 2 -> return AnySyntax

908+ _ -> error "Corrupted binary data for SynContext"

909+

910+

911+instance Binary Syntax where

912+ put (Rule x1 x2 x3)

913+ = do put x1

914+ put x2

915+ put x3

916+ get

917+ = do x1 <- get

918+ x2 <- get

919+ x3 <- get

920+ return (Rule x1 x2 x3)

921

922+

923+instance Binary SSymbol where

924+ put x

925+ = case x of

926+ Keyword x1 -> do putWord8 0

927+ put x1

928+ Symbol x1 -> do putWord8 1

929+ put x1

930+ Expr x1 -> do putWord8 2

931+ put x1

932+ get

933+ = do i <- getWord8

934+ case i of

935+ 0 -> do x1 <- get

936+ return (Keyword x1)

937+ 1 -> do x1 <- get

938+ return (Symbol x1)

939+ 2 -> do x1 <- get

940+ return (Expr x1)

941+ _ -> error "Corrupted binary data for SSymbol"

src/Idris/Parser.hs+3−2

@@ -61,7 +61,8 @@ loadModule f

61 case fp of

62 IDR fn -> loadSource fn

63 IBC fn src -> idrisCatch (loadIBC fn)

64+ (\c -> do iLOG $ fn ++ " failed"

64− (\c -> loadSource src)

65+ loadSource src)

65 let (dir, fh) = splitFileName f

66 let (dir, fh) = splitFileName f

66 return (dropExtension fh))

67 return (dropExtension fh))

67 (\e -> do let msg = report e

68 (\e -> do let msg = report e

@@ -87,7 +88,7 @@ loadSource f = do iLOG ("Reading " ++ f)

87 mapM_ (elabDecl toplevel) ds

88 mapM_ (elabDecl toplevel) ds

88 iLOG ("Finished " ++ f)

89 iLOG ("Finished " ++ f)

89 let ibc = dropExtension f ++ ".ibc"

90 let ibc = dropExtension f ++ ".ibc"

90− idrisCatch (do writeIBC ibc; clearIBC)

91+ idrisCatch (do writeIBC f ibc; clearIBC)

91 (\c -> return ()) -- failure is harmless

92 (\c -> return ()) -- failure is harmless

92 return ()

93 return ()

93 where

94 where

test/mktest.pl+1−1

@@ -14,7 +14,7 @@ open(FOO,">run");

15print FOO "#!/bin/bash\n";

16print FOO "idris $test.idr -o $test\n";

17−print FOO "./$test\n";print FOO "rm -f $test\n";

17+print FOO "./$test\n";print FOO "rm -f $test $test.ibc\n";

19close(FOO);

test/test001/run+1−1

@@ -1,4 +1,4 @@

1#!/bin/bash

2idris test001.idr -o test001

3./test001

4−rm -f test001

4+rm -f test001 test001.ibc