02881b1 · Idris-dev · git.iko.soy

git.iko.soy/Idris-dev

on master help sign in

Implemented forcing optimisation

02881b1Edwin Brady15 years ago

idris.cabal+1

compare with master

unifiedsplit

@@ -34,6 +34,7 @@ Executable idris

34 Idris.Delaborate, Idris.Primitives, Idris.Imports,

35 Idris.Compiler, Idris.Prover, Idris.ElabTerm,

36 Idris.Coverage, Idris.IBC, Idris.Unlit,

37+ Idris.DataOpts

38 Paths_idris

39 Paths_idris

src/Core/Evaluate.hs+3

@@ -31,6 +31,7 @@ data Value = VP NameType Name Value

31 | VBind Name (Binder Value) (Value -> Eval Value)

32 | VApp Value Value

33 | VSet UExp

34+ | VErased

34 | VConstant Const

35 | VConstant Const

35 | VTmp Int

36 | VTmp Int

@@ -147,6 +148,7 @@ eval ctxt statics genv tm opts = ev True [] tm where

147 a' <- ev False env a

148 a' <- ev False env a

148 evApply top env [a'] f'

149 evApply top env [a'] f'

149 ev top env (Constant c) = return $ VConstant c

150 ev top env (Constant c) = return $ VConstant c

151+ ev top env Erased = return VErased

150 ev top env (Set i) = return $ VSet i

152 ev top env (Set i) = return $ VSet i

151

153

152 evApply top env args (VApp f a) =

154 evApply top env args (VApp f a) =

@@ -259,6 +261,7 @@ instance Quote Value where

259 where quoteB t = fmapMB (quote i) t

261 where quoteB t = fmapMB (quote i) t

260 quote i (VApp f a) = liftM2 App (quote i f) (quote i a)

262 quote i (VApp f a) = liftM2 App (quote i f) (quote i a)

261 quote i (VSet u) = return $ Set u

263 quote i (VSet u) = return $ Set u

264+ quote i VErased = return $ Erased

262 quote i (VConstant c) = return $ Constant c

265 quote i (VConstant c) = return $ Constant c

263 quote i (VTmp x) = return $ V (i - x - 1)

266 quote i (VTmp x) = return $ V (i - x - 1)

264

267

src/Core/ProofState.hs+1−1

@@ -436,7 +436,7 @@ updateSolved xs t = t

436processTactic :: Tactic -> ProofState -> TC (ProofState, String)

437processTactic QED ps = case holes ps of

438 [] -> do let tm = {- normalise (context ps) [] -} (pterm ps)

439− (tm', ty', _) <- recheck (context ps) [] tm

439+ (tm', ty', _) <- recheck (context ps) [] (forget tm) tm

440 return (ps { done = True, pterm = tm' },

441 "Proof complete: " ++ showEnv [] tm')

442 _ -> fail "Still holes to fill."

src/Core/TT.hs+15−2

@@ -173,7 +173,7 @@ addAlist ((n, tm) : ds) ctxt = addDef n tm (addAlist ds ctxt)

173

174data Const = I Int | BI Integer | Fl Double | Ch Char | Str String

176− | PtrType

176+ | PtrType | Forgot

177 deriving Eq

178{-!

179deriving instance Binary Const

@@ -183,6 +183,7 @@ data Raw = Var Name

183 | RBind Name (Binder Raw) Raw

184 | RApp Raw Raw

185 | RSet

186+ | RForce Raw

186 | RConstant Const

187 | RConstant Const

187 deriving (Show, Eq)

188 deriving (Show, Eq)

188{-!

189{-!

@@ -221,6 +222,11 @@ raw_apply :: Raw -> [Raw] -> Raw

221raw_apply f [] = f

222raw_apply f [] = f

222raw_apply f (a : as) = raw_apply (RApp f a) as

223raw_apply f (a : as) = raw_apply (RApp f a) as

223

224

225+raw_unapply :: Raw -> (Raw, [Raw])

226+raw_unapply t = ua [] t where

227+ ua args (RApp f a) = ua (a:args) f

228+ ua args t = (t, args)

229+

224data RawFun = RawFun { rtype :: Raw,

230data RawFun = RawFun { rtype :: Raw,

225 rval :: Raw

231 rval :: Raw

226 }

232 }

@@ -284,6 +290,7 @@ data TT n = P NameType n (TT n) -- embed type

284 | Bind n (Binder (TT n)) (TT n)

290 | Bind n (Binder (TT n)) (TT n)

285 | App (TT n) (TT n) -- function, function type, arg

291 | App (TT n) (TT n) -- function, function type, arg

286 | Constant Const

292 | Constant Const

293+ | Erased

287 | Set UExp

294 | Set UExp

288 deriving Functor

295 deriving Functor

289{-!

296{-!

@@ -305,6 +312,8 @@ instance Eq n => Eq (TT n) where

305 (==) (App fx ax) (App fy ay) = fx == fy && ax == ay

312 (==) (App fx ax) (App fy ay) = fx == fy && ax == ay

306 (==) (Set _) (Set _) = True -- deal with constraints later

313 (==) (Set _) (Set _) = True -- deal with constraints later

307 (==) (Constant x) (Constant y) = x == y

314 (==) (Constant x) (Constant y) = x == y

315+ (==) Erased _ = True

316+ (==) _ Erased = True

308 (==) _ _ = False

317 (==) _ _ = False

309

318

310convEq :: Eq n => TT n -> TT n -> StateT UCs TC Bool

319convEq :: Eq n => TT n -> TT n -> StateT UCs TC Bool

@@ -320,6 +329,8 @@ convEq (Constant x) (Constant y) = return (x == y)

320convEq (Set x) (Set y) = do (v, cs) <- get

329convEq (Set x) (Set y) = do (v, cs) <- get

321 put (v, ULE x y : cs)

330 put (v, ULE x y : cs)

322 return True

331 return True

332+convEq Erased _ = return True

333+convEq _ Erased = return True

323convEq _ _ = return False

334convEq _ _ = return False

324

335

325-- A few handy operations on well typed terms:

336-- A few handy operations on well typed terms:

@@ -418,7 +429,8 @@ forget tm = fe [] tm

418 fe env (Constant c)

429 fe env (Constant c)

419 = RConstant c

430 = RConstant c

420 fe env (Set i) = RSet

431 fe env (Set i) = RSet

421−

432+ fe env Erased = RConstant Forgot

433+

422bindAll :: [(n, Binder (TT n))] -> TT n -> TT n

434bindAll :: [(n, Binder (TT n))] -> TT n -> TT n

423bindAll [] t =t

435bindAll [] t =t

424bindAll ((n, b) : bs) t = Bind n b (bindAll bs t)

436bindAll ((n, b) : bs) t = Bind n b (bindAll bs t)

@@ -485,6 +497,7 @@ showEnv' env t dbg = se 10 env t where

485 se p env (Bind n b sc) = bracket p 2 $ sb env n b ++ se 10 ((n,b):env) sc

497 se p env (Bind n b sc) = bracket p 2 $ sb env n b ++ se 10 ((n,b):env) sc

486 se p env (App f a) = bracket p 1 $ se 1 env f ++ " " ++ se 0 env a

498 se p env (App f a) = bracket p 1 $ se 1 env f ++ " " ++ se 0 env a

487 se p env (Constant c) = show c

499 se p env (Constant c) = show c

500+ se p env Erased = "[__]"

488 se p env (Set i) = "Set " ++ show i

501 se p env (Set i) = "Set " ++ show i

489

502

490 sb env n (Lam t) = showb env "\\ " " => " n t

503 sb env n (Lam t) = showb env "\\ " " => " n t

src/Core/Typecheck.hs+8−4

@@ -36,11 +36,11 @@ isSet ctxt env tm = isSet' (normalise ctxt env tm)

36 where isSet' (Set _) = return ()

37 isSet' tm = fail (showEnv env tm ++ " is not a Set")

39−recheck :: Context -> Env -> Term -> TC (Term, Type, UCs)

39+recheck :: Context -> Env -> Raw -> Term -> TC (Term, Type, UCs)

40−recheck ctxt env tm

40+recheck ctxt env tm orig

41 = let v = next_tvar ctxt in

42− case runStateT (check' False ctxt env (forget tm)) (v, []) of -- holes banned

42+ case runStateT (check' False ctxt env tm) (v, []) of -- holes banned

43− Error (IncompleteTerm _) -> Error $ IncompleteTerm tm

43+ Error (IncompleteTerm _) -> Error $ IncompleteTerm orig

44 Error e -> Error e

45 OK ((tm, ty), constraints) ->

46 return (tm, ty, constraints)

@@ -77,13 +77,17 @@ check' holes ctxt env top = chk env top where

77 let c = ULT (UVar v) (UVar (v+1))

78 put (v+2, (c:cs))

79 return (Set (UVar v), Set (UVar (v+1)))

80+ chk env (RConstant Forgot) = return (Erased, Erased)

80 chk env (RConstant c) = return (Constant c, constType c)

81 chk env (RConstant c) = return (Constant c, constType c)

81 where constType (I _) = Constant IType

82 where constType (I _) = Constant IType

82 constType (BI _) = Constant BIType

83 constType (BI _) = Constant BIType

83 constType (Fl _) = Constant FlType

84 constType (Fl _) = Constant FlType

84 constType (Ch _) = Constant ChType

85 constType (Ch _) = Constant ChType

85 constType (Str _) = Constant StrType

86 constType (Str _) = Constant StrType

87+ constType Forgot = Erased

86 constType _ = Set (UVal 0)

88 constType _ = Set (UVal 0)

89+ chk env (RForce t) = do (_, ty) <- chk env t

90+ return (Erased, ty)

87 chk env (RBind n (Pi s) t)

91 chk env (RBind n (Pi s) t)

88 = do (sv, st) <- chk env s

92 = do (sv, st) <- chk env s

89 (tv, tt) <- chk ((n, Pi sv) : env) t

93 (tv, tt) <- chk ((n, Pi sv) : env) t

src/Idris/AbsSyntax.hs+12

@@ -39,6 +39,7 @@ data IState = IState { tt_ctxt :: Context,

39 idris_implicits :: Ctxt [PArg],

40 idris_statics :: Ctxt [Bool],

41 idris_classes :: Ctxt ClassInfo,

42+ idris_optimisation :: Ctxt OptInfo,

42 idris_log :: String,

43 idris_log :: String,

43 idris_options :: IOption,

44 idris_options :: IOption,

44 idris_name :: Int,

45 idris_name :: Int,

@@ -66,6 +67,7 @@ data IBCWrite = IBCFix FixDecl

66 | IBCImp Name

67 | IBCImp Name

67 | IBCStatic Name

68 | IBCStatic Name

68 | IBCClass Name

69 | IBCClass Name

70+ | IBCOpt Name

69 | IBCSyntax Syntax

71 | IBCSyntax Syntax

70 | IBCKeyword String

72 | IBCKeyword String

71 | IBCImport FilePath

73 | IBCImport FilePath

@@ -77,6 +79,7 @@ data IBCWrite = IBCFix FixDecl

77 deriving Show

79 deriving Show

79idrisInit = IState initContext [] [] emptyContext emptyContext emptyContext

81idrisInit = IState initContext [] [] emptyContext emptyContext emptyContext

82+ emptyContext

80 "" defaultOpts 6 [] [] [] [] [] [] [] []

83 "" defaultOpts 6 [] [] [] [] [] [] [] []

81 Nothing Nothing Nothing [] [] [] Hidden [] Nothing

84 Nothing Nothing Nothing [] [] [] Hidden [] Nothing

@@ -521,6 +524,15 @@ data ClassInfo = CI { instanceName :: Name,

521deriving instance Binary ClassInfo

524deriving instance Binary ClassInfo

522!-}

525!-}

523

526

527+data OptInfo = Optimise { collapsible :: Bool,

528+ forceable :: [Int], -- argument positions

529+ recursive :: [Int] }

530+ deriving Show

531+{-!

532+deriving instance Binary OptInfo

533+!-}

534+

535+

524-- Syntactic sugar info

536-- Syntactic sugar info

525

537

526data DSL = DSL { dsl_bind :: PTerm,

538data DSL = DSL { dsl_bind :: PTerm,

src/Idris/Compiler.hs+1

@@ -107,6 +107,7 @@ instance ToEpic (TT Name) where

107 a' <- epic' env a

108 return (f' @@ a')

109 epic' env (Constant c) = epic c

110+ epic' env Erased = return impossible

110 epic' env (Set _) = return impossible

111 epic' env (Set _) = return impossible

111

112

112 epicCon env t arity n args

113 epicCon env t arity n args

src/Idris/DataOpts.hsnew file+88

@@ -0,0 +1,88 @@

1+{-# LANGUAGE PatternGuards #-}

3+module Idris.DataOpts where

5+-- Forcing, detagging and collapsing

7+import Idris.AbsSyntax

8+import Core.TT

10+import Data.List

11+import Data.Maybe

12+import Debug.Trace

13+

14+-- Calculate the forceable arguments to a constructor and update the set of

15+-- optimisations

16+

17+forceArgs :: Name -> Type -> Idris ()

18+-- forceArgs n t = return ()

19+forceArgs n t = do let fargs = force 0 t

20+ i <- getIState

21+ copt <- case lookupCtxt Nothing n (idris_optimisation i) of

22+ [] -> return $ Optimise False [] []

23+ (op:_) -> return op

24+ let opts = addDef n (copt { forceable = fargs }) (idris_optimisation i)

25+ putIState (i { idris_optimisation = opts })

26+ addIBC (IBCOpt n)

27+ iLOG $ "Forced: " ++ show n ++ " " ++ show fargs

28+ where

29+ force :: Int -> Term -> [Int]

30+ force i (Bind _ (Pi _) sc)

31+ = force (i + 1) $ instantiate (P Bound (MN i "F?") Erased) sc

32+ force _ sc@(App f a)

33+ | (_, args) <- unApply sc

34+ = nub $ concatMap guarded args

35+ force _ _ = []

36+

37+ isF (P _ (MN force "F?") _) = Just force

38+ isF _ = Nothing

39+

40+ guarded :: Term -> [Int]

41+ guarded t@(App f a)

42+ | (P (TCon _ _) _ _, args) <- unApply t

43+ = mapMaybe isF args ++ concatMap guarded args

44+ | (P (DCon _ _) _ _, args) <- unApply t

45+ = mapMaybe isF args ++ concatMap guarded args

46+ guarded t = mapMaybe isF [t]

47+

48+class Optimisable term where

49+ applyOpts :: term -> Idris term

50+

51+-- Raw is for compile time optimisation (before type checking)

52+-- Term is for run time optimisation (after type checking, collapsing allowed)

53+

54+instance Optimisable Raw where

55+ applyOpts t@(RApp f a)

56+ | (Var n, args) <- raw_unapply t -- MAGIC HERE

57+ = do i <- getIState

58+ case lookupCtxt Nothing n (idris_optimisation i) of

59+ (oi:_) -> return $ applyDataOpt oi n args

60+ _ -> do args' <- mapM applyOpts args

61+ return (raw_apply (Var n) args')

62+ | otherwise = do f' <- applyOpts f

63+ a' <- applyOpts a

64+ return (RApp f' a')

65+ applyOpts (RBind n b t) = do b' <- applyOpts b

66+ t' <- applyOpts t

67+ return (RBind n b' t')

68+ applyOpts (RForce t) = applyOpts t

69+ applyOpts t = return t

70+

71+instance Optimisable t => Optimisable (Binder t) where

72+ applyOpts (Let t v) = do t' <- applyOpts t

73+ v' <- applyOpts v

74+ return (Let t' v')

75+ applyOpts b = do t' <- applyOpts (binderTy b)

76+ return (b { binderTy = t' })

77+

78+-- Compile time: no collapsing

79+

80+applyDataOpt :: OptInfo -> Name -> [Raw] -> Raw

81+applyDataOpt oi n args

82+ = let args' = zipWith doForce (map (\x -> x `elem` (forceable oi)) [0..])

83+ args in

84+ raw_apply (Var n) args'

85+ where

86+ doForce True a = RForce a

87+ doForce False a = a

88+

src/Idris/ElabDecls.hs+4−1

@@ -8,6 +8,7 @@ import Idris.Delaborate

8import Idris.Imports

9import Idris.ElabTerm

10import Idris.Coverage

11+import Idris.DataOpts

11import Paths_idris

12import Paths_idris

13import Core.TT

14import Core.TT

@@ -24,7 +25,8 @@ import Debug.Trace

26recheckC ctxt fc env t

27recheckC ctxt fc env t

28+ = do t' <- applyOpts (forget t)

27− = do (tm, ty, cs) <- tclift $ recheck ctxt env t

29+ (tm, ty, cs) <- tclift $ recheck ctxt env t' t

28 addConstraints fc cs

30 addConstraints fc cs

29 return (tm, ty)

31 return (tm, ty)

@@ -90,6 +92,7 @@ elabCon info syn (n, t_in, fc)

90 (cty, _) <- recheckC ctxt fc [] t'

92 (cty, _) <- recheckC ctxt fc [] t'

91 logLvl 2 $ "---> " ++ show n ++ " : " ++ show cty

93 logLvl 2 $ "---> " ++ show n ++ " : " ++ show cty

92 addIBC (IBCDef n)

94 addIBC (IBCDef n)

95+ forceArgs n cty

93 return (n, cty)

96 return (n, cty)

95elabClauses :: ElabInfo -> FC -> FnOpts -> Name -> [PClause] -> Idris ()

98elabClauses :: ElabInfo -> FC -> FnOpts -> Name -> [PClause] -> Idris ()

src/Idris/IBC.hs+40−7

@@ -22,7 +22,7 @@ import System.Directory

22import Paths_idris

24ibcVersion :: Word8

25−ibcVersion = 4

25+ibcVersion = 5

27data IBCFile = IBCFile { ver :: Word8,

28 sourcefile :: FilePath,

@@ -31,6 +31,7 @@ data IBCFile = IBCFile { ver :: Word8,

31 ibc_fixes :: [FixDecl],

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

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

34+ ibc_optimise :: [(Name, OptInfo)],

34 ibc_syntax :: [Syntax],

35 ibc_syntax :: [Syntax],

35 ibc_keywords :: [String],

36 ibc_keywords :: [String],

36 ibc_objs :: [FilePath],

37 ibc_objs :: [FilePath],

@@ -43,7 +44,7 @@ deriving instance Binary IBCFile

43!-}

44!-}

45initIBC :: IBCFile

46initIBC :: IBCFile

46−initIBC = IBCFile ibcVersion "" [] [] [] [] [] [] [] [] [] [] [] []

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

48loadIBC :: FilePath -> Idris ()

49loadIBC :: FilePath -> Idris ()

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

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

@@ -58,8 +59,9 @@ writeIBC src f

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

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

59 [] -> return ()

60 [] -> return ()

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

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

61− liftIO $ encodeFile f ibcf

62+ idrisCatch (do liftIO $ encodeFile f ibcf

62− iLOG $ "Written"

63+ iLOG "Written")

64+ (\c -> do iLOG $ "Failed " ++ show c)

63 return ()

65 return ()

65mkIBC :: [IBCWrite] -> IBCFile -> Idris IBCFile

67mkIBC :: [IBCWrite] -> IBCFile -> Idris IBCFile

@@ -81,6 +83,9 @@ ibc i (IBCClass n) f

81 = case lookupCtxt Nothing n (idris_classes i) of

83 = case lookupCtxt Nothing n (idris_classes i) of

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

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

83 _ -> fail "IBC write failed"

85 _ -> fail "IBC write failed"

86+ibc i (IBCOpt n) f = case lookupCtxt Nothing n (idris_optimisation i) of

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

88+ _ -> fail "IBC write failed"

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

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

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

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

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

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

@@ -106,6 +111,7 @@ process i fn

106 pFixes (ibc_fixes i)

111 pFixes (ibc_fixes i)

107 pStatics (ibc_statics i)

112 pStatics (ibc_statics i)

108 pClasses (ibc_classes i)

113 pClasses (ibc_classes i)

114+ pOptimise (ibc_optimise i)

109 pSyntax (ibc_syntax i)

115 pSyntax (ibc_syntax i)

110 pKeywords (ibc_keywords i)

116 pKeywords (ibc_keywords i)

111 pObjs (ibc_objs i)

117 pObjs (ibc_objs i)

@@ -162,6 +168,13 @@ pClasses cs = mapM_ (\ (n, c) ->

162 = addDef n c (idris_classes i) }))

168 = addDef n c (idris_classes i) }))

163 cs

169 cs

164

170

171+pOptimise :: [(Name, OptInfo)] -> Idris ()

172+pOptimise cs = mapM_ (\ (n, c) ->

173+ do i <- getIState

174+ putIState (i { idris_optimisation

175+ = addDef n c (idris_optimisation i) }))

176+ cs

177+

165pSyntax :: [Syntax] -> Idris ()

178pSyntax :: [Syntax] -> Idris ()

166pSyntax s = do i <- getIState

179pSyntax s = do i <- getIState

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

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

@@ -249,6 +262,7 @@ instance Binary Const where

249 ChType -> putWord8 8

262 ChType -> putWord8 8

250 StrType -> putWord8 9

263 StrType -> putWord8 9

251 PtrType -> putWord8 10

264 PtrType -> putWord8 10

265+ Forgot -> putWord8 11

252 get

266 get

253 = do i <- getWord8

267 = do i <- getWord8

254 case i of

268 case i of

@@ -268,6 +282,7 @@ instance Binary Const where

268 8 -> return ChType

282 8 -> return ChType

269 9 -> return StrType

283 9 -> return StrType

270 10 -> return PtrType

284 10 -> return PtrType

285+ 11 -> return Forgot

271 _ -> error "Corrupted binary data for Const"

286 _ -> error "Corrupted binary data for Const"

272

287

273

288

@@ -286,6 +301,8 @@ instance Binary Raw where

286 RSet -> putWord8 3

301 RSet -> putWord8 3

287 RConstant x1 -> do putWord8 4

302 RConstant x1 -> do putWord8 4

288 put x1

303 put x1

304+ RForce x1 -> do putWord8 5

305+ put x1

289 get

306 get

290 = do i <- getWord8

307 = do i <- getWord8

291 case i of

308 case i of

@@ -301,6 +318,8 @@ instance Binary Raw where

301 3 -> return RSet

318 3 -> return RSet

302 4 -> do x1 <- get

319 4 -> do x1 <- get

303 return (RConstant x1)

320 return (RConstant x1)

321+ 5 -> do x1 <- get

322+ return (RForce x1)

304 _ -> error "Corrupted binary data for Raw"

323 _ -> error "Corrupted binary data for Raw"

305

324

306

325

@@ -400,6 +419,7 @@ instance (Binary n) => Binary (TT n) where

400 put x1

419 put x1

401 Set x1 -> do putWord8 5

420 Set x1 -> do putWord8 5

402 put x1

421 put x1

422+ Erased -> do putWord8 6

403 get

423 get

404 = do i <- getWord8

424 = do i <- getWord8

405 case i of

425 case i of

@@ -420,6 +440,7 @@ instance (Binary n) => Binary (TT n) where

420 return (Constant x1)

440 return (Constant x1)

421 5 -> do x1 <- get

441 5 -> do x1 <- get

422 return (Set x1)

442 return (Set x1)

443+ 6 -> return Erased

423 _ -> error "Corrupted binary data for TT"

444 _ -> error "Corrupted binary data for TT"

424

445

425

446

@@ -530,7 +551,7 @@ instance Binary Accessibility where

530 _ -> error "Corrupted binary data for Accessibility"

551 _ -> error "Corrupted binary data for Accessibility"

531

552

532instance Binary IBCFile where

553instance Binary IBCFile where

533− put (IBCFile x1 x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14)

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

534 = do put x1

555 = do put x1

535 put x2

556 put x2

536 put x3

557 put x3

@@ -545,6 +566,7 @@ instance Binary IBCFile where

545 put x12

566 put x12

546 put x13

567 put x13

547 put x14

568 put x14

569+ put x15

548 get

570 get

549 = do x1 <- get

571 = do x1 <- get

550 if x1 == ibcVersion then

572 if x1 == ibcVersion then

@@ -561,7 +583,8 @@ instance Binary IBCFile where

561 x12 <- get

583 x12 <- get

562 x13 <- get

584 x13 <- get

563 x14 <- get

585 x14 <- get

586+ x15 <- get

564− return (IBCFile x1 x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14)

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

565 else return (initIBC { ver = x1 })

588 else return (initIBC { ver = x1 })

566

589

567instance Binary Fixity where

590instance Binary Fixity where

@@ -940,7 +963,17 @@ instance Binary ClassInfo where

940 x4 <- get

963 x4 <- get

941 return (CI x1 x2 x3 x4)

964 return (CI x1 x2 x3 x4)

942

965

943−

966+instance Binary OptInfo where

967+ put (Optimise x1 x2 x3)

968+ = do put x1

969+ put x2

970+ put x3

971+ get

972+ = do x1 <- get

973+ x2 <- get

974+ x3 <- get

975+ return (Optimise x1 x2 x3)

976+

944instance Binary SynContext where

977instance Binary SynContext where

945 put x

978 put x

946 = case x of

979 = case x of

src/Idris/Parser.hs+1−1

@@ -64,7 +64,7 @@ loadModule f

64 LIDR fn -> loadSource True fn

65 IBC fn src ->

66 idrisCatch (loadIBC fn)

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

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

68 case src of

69 IDR sfn -> loadSource False sfn

70 LIDR sfn -> loadSource True sfn)