8f77986 · Idris-dev · git.iko.soy

git.iko.soy/Idris-dev

on master help sign in

Added some serialisation

8f77986Edwin Brady15 years ago

idris.cabal+3−3

compare with master

unifiedsplit

@@ -33,15 +33,15 @@ Executable idris

33 Idris.REPLParser, Idris.ElabDecls, Idris.Error,

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

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

36− Idris.Coverage,

36+ Idris.Coverage, Idris.IBC,

38 Paths_idris

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

41 containers, process, transformers, filepath, directory,

42− epic>=0.9.1

42+ binary, derive, epic>=0.9.1

44 Extensions: MultiParamTypeClasses, FunctionalDependencies,

45− FlexibleInstances

45+ FlexibleInstances, TemplateHaskell

46 ghc-prof-options: -auto-all

47 ghc-options: -rtsopts

impl-paper/overview.tex+1−1

@@ -25,8 +25,8 @@ High level view of steps we've taken to implement this new version:

25\end{itemize}

26\item An Elaborator, as an EDSL, which is a language for applying primitive tactics and

27 constructing derived tactics, from a high level syntax withe implicit arguments.

28−\item Advanced elaborations: using declarations, where clauses.

29\item Adding primitive operators and a link to Epic~\cite{epic-tfp}.

28\item Adding primitive operators and a link to Epic~\cite{epic-tfp}.

29+\item Advanced elaborations: using declarations, where clauses, type classes.

30\end{itemize}

32For the high level language: we need nothing more than the core type theory,

lib/prelude/vect.idr+1−1

@@ -22,7 +22,7 @@ lookup : Fin n -> Vect a n -> a;

22lookup fO (x :: xs) = x;

23lookup (fS k) (x :: xs) = lookup k xs;

24lookup fO [] impossible;

25−lookup (fS k) [] impossible;

25+lookup (fS _) [] impossible;

27app : Vect a n -> Vect a m -> Vect a (n + m);

28app [] ys = ys;

src/Core/Evaluate.hs+22−24

@@ -2,7 +2,7 @@

2 PatternGuards #-}

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

5− Fun(..), Def(..),

5+ Def(..),

6 Context, initContext, ctxtAlist, uconstraints, next_tvar,

7 addToCtxt, addTyDecl, addDatatype, addCasedef, addOperator,

8 lookupTy, lookupP, lookupDef, lookupVal, lookupTyEnv,

@@ -10,6 +10,8 @@ module Core.Evaluate(normalise, normaliseC, simplify, specialise, hnf,

11import Debug.Trace

12import Control.Monad.State

13+import qualified Data.Binary as B

14+import Data.Binary hiding (get, put)

14import Core.TT

16import Core.TT

15import Core.CaseTree

17import Core.CaseTree

@@ -106,8 +108,9 @@ eval ctxt statics genv tm opts = ev True [] tm where

106 ev top env (P _ n ty)

108 ev top env (P _ n ty)

107 | Just (Let t v) <- lookup n genv = ev top env v

109 | Just (Let t v) <- lookup n genv = ev top env v

108 ev top env (P Ref n ty) = case lookupDef Nothing n ctxt of

110 ev top env (P Ref n ty) = case lookupDef Nothing n ctxt of

109− [Function (Fun _ _ _ v)] -> return v

111+ [Function _ tm] -> ev True env tm

112+ [TyDecl nt ty] -> do vty <- ev True env ty

110− [TyDecl nt ty hty] -> return $ VP nt n hty

113+ return $ VP nt n vty

111 [CaseOp inl _ _ [] tree] ->

114 [CaseOp inl _ _ [] tree] ->

112 if simpl && (not inl)

115 if simpl && (not inl)

113 then liftM (VP Ref n) (ev top env ty)

116 then liftM (VP Ref n) (ev top env ty)

@@ -293,8 +296,8 @@ eval_hnf ctxt statics genv tm = ev [] tm where

293 ev env (P _ n ty)

296 ev env (P _ n ty)

294 | Just (Let t v) <- lookup n genv = ev env v

297 | Just (Let t v) <- lookup n genv = ev env v

295 ev env (P Ref n ty) = case lookupDef Nothing n ctxt of

298 ev env (P Ref n ty) = case lookupDef Nothing n ctxt of

296− [Function (Fun _ _ t _)] -> ev env t

299+ [Function _ t] -> ev env t

297− [TyDecl nt ty hty] -> return $ HP nt n ty

300+ [TyDecl nt ty] -> return $ HP nt n ty

298 [CaseOp inl _ _ [] tree] ->

301 [CaseOp inl _ _ [] tree] ->

299 do c <- evCase env [] [] tree

302 do c <- evCase env [] [] tree

300 case c of

303 case c of

@@ -416,23 +419,20 @@ spec ctxt statics genv tm = undefined

416

419

417-- CONTEXTS -----------------------------------------------------------------

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

418

421

419−data Fun = Fun Type Value Term Value

420− deriving Show

421−

422{- A definition is either a simple function (just an expression with a type),

423 a constant, which could be a data or type constructor, an axiom or as an

424 yet undefined function, or an Operator.

425 An Operator is a function which explains how to reduce.

426 A CaseOp is a function defined by a simple case tree -}

427

428−data Def = Function Fun

428+data Def = Function Type Term

429− | TyDecl NameType Type Value

429+ | TyDecl NameType Type

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

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

432

433instance Show Def where

434− show (Function f) = "Function: " ++ show f

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

435− show (TyDecl nt ty val) = "TyDecl: " ++ show nt ++ " " ++ show ty

435+ show (TyDecl nt ty) = "TyDecl: " ++ show nt ++ " " ++ show ty

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

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

438 show ns ++ " " ++ show sc

@@ -453,14 +453,13 @@ veval ctxt env t = evalState (eval ctxt emptyContext env t []) ()

453addToCtxt :: Name -> Term -> Type -> Context -> Context

454addToCtxt n tm ty uctxt

455 = let ctxt = definitions uctxt

456− ctxt' = addDef n (Function (Fun ty (veval uctxt [] ty)

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

457− tm (veval uctxt [] tm))) ctxt in

458 uctxt { definitions = ctxt' }

457 uctxt { definitions = ctxt' }

459

458

460addTyDecl :: Name -> Type -> Context -> Context

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

461addTyDecl n ty uctxt

460addTyDecl n ty uctxt

462 = let ctxt = definitions uctxt

461 = let ctxt = definitions uctxt

463− ctxt' = addDef n (TyDecl Ref ty (veval uctxt [] ty)) ctxt in

462+ ctxt' = addDef n (TyDecl Ref ty) ctxt in

464 uctxt { definitions = ctxt' }

463 uctxt { definitions = ctxt' }

465

464

466addDatatype :: Datatype Name -> Context -> Context

465addDatatype :: Datatype Name -> Context -> Context

@@ -468,14 +467,14 @@ addDatatype (Data n tag ty cons) uctxt

468 = let ctxt = definitions uctxt

467 = let ctxt = definitions uctxt

469 ty' = normalise uctxt [] ty

468 ty' = normalise uctxt [] ty

470 ctxt' = addCons 0 cons (addDef n

469 ctxt' = addCons 0 cons (addDef n

471− (TyDecl (TCon tag (arity ty')) ty (veval uctxt [] ty)) ctxt) in

470+ (TyDecl (TCon tag (arity ty')) ty) ctxt) in

472 uctxt { definitions = ctxt' }

471 uctxt { definitions = ctxt' }

473 where

472 where

474 addCons tag [] ctxt = ctxt

473 addCons tag [] ctxt = ctxt

475 addCons tag ((n, ty) : cons) ctxt

474 addCons tag ((n, ty) : cons) ctxt

476 = let ty' = normalise uctxt [] ty in

475 = let ty' = normalise uctxt [] ty in

477 addCons (tag+1) cons (addDef n

476 addCons (tag+1) cons (addDef n

478− (TyDecl (DCon tag (arity ty')) ty (veval uctxt [] ty)) ctxt)

477+ (TyDecl (DCon tag (arity ty')) ty) ctxt)

479

478

480addCasedef :: Name -> Bool -> Bool -> [(Term, Term)] -> Type -> Context -> Context

479addCasedef :: Name -> Bool -> Bool -> [(Term, Term)] -> Type -> Context -> Context

481addCasedef n alwaysInline tcase ps ty uctxt

480addCasedef n alwaysInline tcase ps ty uctxt

@@ -498,8 +497,8 @@ lookupTy :: Maybe [String] -> Name -> Context -> [Type]

498lookupTy root n ctxt

497lookupTy root n ctxt

499 = do def <- lookupCtxt root n (definitions ctxt)

498 = do def <- lookupCtxt root n (definitions ctxt)

500 case def of

499 case def of

501− (Function (Fun ty _ _ _)) -> return ty

500+ (Function ty _) -> return ty

502− (TyDecl _ ty _) -> return ty

501+ (TyDecl _ ty) -> return ty

503 (Operator ty _ _) -> return ty

502 (Operator ty _ _) -> return ty

504 (CaseOp _ ty _ _ _) -> return ty

503 (CaseOp _ ty _ _ _) -> return ty

505

504

@@ -507,8 +506,8 @@ lookupP :: Maybe [String] -> Name -> Context -> [Term]

507lookupP root n ctxt

506lookupP root n ctxt

508 = do def <- lookupCtxt root n (definitions ctxt)

507 = do def <- lookupCtxt root n (definitions ctxt)

509 case def of

508 case def of

510− (Function (Fun ty _ tm _)) -> return (P Ref n ty)

509+ (Function ty tm) -> return (P Ref n ty)

511− (TyDecl nt ty hty) -> return (P nt n ty)

510+ (TyDecl nt ty) -> return (P nt n ty)

512 (CaseOp _ ty _ _ _) -> return (P Ref n ty)

511 (CaseOp _ ty _ _ _) -> return (P Ref n ty)

513 (Operator ty _ _) -> return (P Ref n ty)

512 (Operator ty _ _) -> return (P Ref n ty)

514

513

@@ -519,8 +518,8 @@ lookupVal :: Maybe [String] -> Name -> Context -> [Value]

519lookupVal root n ctxt

518lookupVal root n ctxt

520 = do def <- lookupCtxt root n (definitions ctxt)

519 = do def <- lookupCtxt root n (definitions ctxt)

521 case def of

520 case def of

522− (Function (Fun _ _ _ htm)) -> return htm

521+ (Function _ htm) -> return (veval ctxt [] htm)

523− (TyDecl nt ty hty) -> return (VP nt n hty)

522+ (TyDecl nt ty) -> return (VP nt n (veval ctxt [] ty))

524

523

525lookupTyEnv :: Name -> Env -> Maybe (Int, Type)

524lookupTyEnv :: Name -> Env -> Maybe (Int, Type)

526lookupTyEnv n env = li n 0 env where

525lookupTyEnv n env = li n 0 env where

@@ -528,4 +527,3 @@ lookupTyEnv n env = li n 0 env where

528 li n i ((x, b): xs)

527 li n i ((x, b): xs)

529 | n == x = Just (i, binderTy b)

528 | n == x = Just (i, binderTy b)

530 | otherwise = li n (i+1) xs

529 | otherwise = li n (i+1) xs

531−

src/Core/TT.hs+2

@@ -7,6 +7,8 @@ import Debug.Trace

7import qualified Data.Map as Map

8import Data.Char

9import Data.List

10+import qualified Data.Binary as B

11+import Data.Binary hiding (get, put)

11{- The language has:

13{- The language has:

12 * Full dependent types

14 * Full dependent types

src/Idris/AbsSyntax.hs+27−3

@@ -47,11 +47,27 @@ data IState = IState { tt_ctxt :: Context,

47 idris_libs :: [String],

48 idris_hdrs :: [String],

49 last_proof :: Maybe (Name, [String]),

50− errLine :: Maybe Int

50+ errLine :: Maybe Int,

51+ ibc_write :: [IBCWrite]

51 }

52 }

52−

53+

54+-- information that needs writing for the current module's .ibc file

55+data IBCWrite = IBCFix FixDecl

56+ | IBCImp Name

57+ | IBCStatic Name

58+ | IBCClass Name

59+ | IBCMeta Name

60+ | IBCSyntax Syntax

61+ | IBCKeyword String

62+ | IBCImport FilePath

63+ | IBCObj FilePath

64+ | IBCLib String

65+ | IBCHeader String

66+ | IBCDef Name -- i.e. main context

67+ deriving Show

68+

53idrisInit = IState initContext [] [] emptyContext emptyContext emptyContext

69idrisInit = IState initContext [] [] emptyContext emptyContext emptyContext

54− "" defaultOpts 6 [] [] [] [] [] [] [] [] Nothing Nothing

70+ "" defaultOpts 6 [] [] [] [] [] [] [] [] Nothing Nothing []

56-- The monad for the main REPL - reading and processing files and updating

72-- The monad for the main REPL - reading and processing files and updating

57-- global state (hence the IO inner monad).

73-- global state (hence the IO inner monad).

@@ -75,6 +91,12 @@ addLib f = do i <- get; put (i { idris_libs = f : idris_libs i })

75addHdr :: String -> Idris ()

91addHdr :: String -> Idris ()

76addHdr f = do i <- get; put (i { idris_hdrs = f : idris_hdrs i })

92addHdr f = do i <- get; put (i { idris_hdrs = f : idris_hdrs i })

94+addIBC :: IBCWrite -> Idris ()

95+addIBC ibc = do i <- get; put (i { ibc_write = ibc : ibc_write i })

96+

97+clearIBC :: Idris ()

98+clearIBC = do i <- get; put (i { ibc_write = [] })

99+

78getHdrs :: Idris [String]

100getHdrs :: Idris [String]

79getHdrs = do i <- get; return (idris_hdrs i)

101getHdrs = do i <- get; return (idris_hdrs i)

102

@@ -768,9 +790,11 @@ implicit syn n ptm

768 let (tm', impdata) = implicitise syn i ptm

790 let (tm', impdata) = implicitise syn i ptm

769 let (tm'', spos) = findStatics i tm'

791 let (tm'', spos) = findStatics i tm'

770 put (i { idris_implicits = addDef n impdata (idris_implicits i) })

792 put (i { idris_implicits = addDef n impdata (idris_implicits i) })

793+ addIBC (IBCImp n)

771 logLvl 5 ("Implicit " ++ show n ++ " " ++ show impdata)

794 logLvl 5 ("Implicit " ++ show n ++ " " ++ show impdata)

772 i <- get

795 i <- get

773 put (i { idris_statics = addDef n spos (idris_statics i) })

796 put (i { idris_statics = addDef n spos (idris_statics i) })

797+ addIBC (IBCStatic n)

774 return tm''

798 return tm''

775

799

776implicitise :: SyntaxInfo -> IState -> PTerm -> (PTerm, [PArg])

800implicitise :: SyntaxInfo -> IState -> PTerm -> (PTerm, [PArg])

src/Idris/Compiler.hs+1−1

@@ -49,7 +49,7 @@ build (n, d) = do i <- getIState

49impossible = int 42424242

51instance ToEpic Def where

52− epic (Function (Fun _ _ tm _)) = epic tm

52+ epic (Function tm _) = epic tm

53 epic (CaseOp _ _ pats args sc) = epic (args, sc) -- TODO: redo case comp after optimising

54 epic _ = return impossible

src/Idris/ElabDecls.hs+7−2

@@ -47,6 +47,7 @@ elabType info syn fc n ty' = {- let ty' = piBind (params info) ty_in

47 logLvl 2 $ "---> " ++ show cty

48 let nty = normalise ctxt [] cty

49 ds <- checkDef fc ((n, nty):defer)

50+ addIBC (IBCDef n)

50 addDeferred ds

51 addDeferred ds

52elabData :: ElabInfo -> SyntaxInfo -> FC -> PData -> Idris ()

53elabData :: ElabInfo -> SyntaxInfo -> FC -> PData -> Idris ()

@@ -66,6 +67,7 @@ elabData info syn fc (PDatadecl n t_in dcons)

66 updateContext (addTyDecl n cty) -- temporary, to check cons

67 updateContext (addTyDecl n cty) -- temporary, to check cons

67 cons <- mapM (elabCon info syn) dcons

68 cons <- mapM (elabCon info syn) dcons

68 ttag <- getName

69 ttag <- getName

70+ addIBC (IBCDef n)

69 updateContext (addDatatype (Data n ttag cty cons))

71 updateContext (addDatatype (Data n ttag cty cons))

71elabCon :: ElabInfo -> SyntaxInfo -> (Name, PTerm, FC) -> Idris (Name, Type)

73elabCon :: ElabInfo -> SyntaxInfo -> (Name, PTerm, FC) -> Idris (Name, Type)

@@ -84,6 +86,7 @@ elabCon info syn (n, t_in, fc)

84 ctxt <- getContext

86 ctxt <- getContext

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

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

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

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

89+ addIBC (IBCDef n)

87 return (n, cty)

90 return (n, cty)

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

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

@@ -103,8 +106,9 @@ elabClauses info fc opts n_in cs_in = let n = liftname info n_in in

103 logLvl 3 (show tree)

106 logLvl 3 (show tree)

104 ctxt <- getContext

107 ctxt <- getContext

105 case lookupTy (namespace info) n ctxt of

108 case lookupTy (namespace info) n ctxt of

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

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

107− tcase pdef ty)

110+ tcase pdef ty)

111+ addIBC (IBCDef n)

108 [] -> return ()

112 [] -> return ()

109 where

113 where

110 debind (x, y) = (depat x, depat y)

114 debind (x, y) = (depat x, depat y)

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

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

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

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

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

337 (idris_classes i) })

341 (idris_classes i) })

342+ addIBC (IBCClass cn)

338 where

343 where

339 pibind [] x = x

344 pibind [] x = x

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

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

src/Idris/IBC.hsnew file+85

@@ -0,0 +1,85 @@

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

3+module Idris.IBC where

5+import Core.Evaluate

6+import Core.TT

7+import Core.CaseTree

8+import Idris.Compiler

9+import Idris.AbsSyntax

10+

11+import Data.Binary

12+import Data.List

13+import Data.DeriveTH

14+import Control.Monad

15+

16+ibcVersion :: Word8

17+ibcVersion = 1

18+

19+data IBCFile = IBCFile { ver :: Word8,

20+ ibc_imports :: [FilePath],

21+ ibc_fixes :: [FixDecl],

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

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

24+ ibc_syntax :: [Syntax],

25+ ibc_keywords :: [String],

26+ ibc_objs :: [FilePath],

27+ ibc_libs :: [String],

28+ ibc_hdrs :: [String],

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

30+

31+initIBC :: IBCFile

32+initIBC = IBCFile ibcVersion [] [] [] [] [] [] [] [] [] []

33+

34+loadIBC :: FilePath -> Idris ()

35+loadIBC fp = fail "Not implemented"

36+

37+writeIBC :: FilePath -> Idris ()

38+writeIBC f

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

40+ i <- getIState

41+ case idris_metavars i \\ primDefs of

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

43+ [] -> return ()

44+ return ()

45+

46+$( derive makeBinary ''IBCFile )

47+$( derive makeBinary ''PTerm )

48+$( derive makeBinary ''Raw )

49+$( derive makeBinary ''PTactic' )

50+$( derive makeBinary ''PDo' )

51+$( derive makeBinary ''PArg' )

52+$( derive makeBinary ''ClassInfo )

53+$( derive makeBinary ''Plicity )

54+$( derive makeBinary ''FC )

55+$( derive makeBinary ''Syntax )

56+$( derive makeBinary ''SynContext )

57+$( derive makeBinary ''SSymbol )

58+$( derive makeBinary ''Static )

59+$( derive makeBinary ''Fixity )

60+$( derive makeBinary ''FixDecl )

61+

62+$( derive makeBinary ''Def )

63+$( derive makeBinary ''SC )

64+$( derive makeBinary ''CaseAlt )

65+$( derive makeBinary ''NameType )

66+$( derive makeBinary ''Name )

67+$( derive makeBinary ''Binder )

68+$( derive makeBinary ''TT )

69+$( derive makeBinary ''Const )

70+

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

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

73+

74+instance Binary (a -> b) where

75+ put x = return ()

76+ get = undefined

77+

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

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

80+-- cycles.

81+

82+instance Binary UExp where

83+ put x = return ()

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

85+

src/Idris/Imports.hs+2−2

@@ -9,7 +9,7 @@ import System.FilePath

9import System.Directory

10import Control.Monad.State

12−data IFileType = IDR FilePath | IBC FilePath

12+data IFileType = IDR FilePath | IBC FilePath FilePath

13 deriving Eq

15srcPath :: FilePath -> FilePath

@@ -30,7 +30,7 @@ findImport (d:ds) fp = do let ibcp = ibcPath (d ++ "/" ++ fp)

30 ibc <- doesFileExist (ibcPath ibcp)

31 idr <- doesFileExist (srcPath idrp)

32 if ibc

33− then return (IBC ibcp)

33+ then return (IBC ibcp idrp)

34 else if idr

35 then return (IDR idrp)

36 else findImport ds fp

src/Idris/Parser.hs+19−5

@@ -5,6 +5,7 @@ import Idris.Imports

5import Idris.Error

6import Idris.ElabDecls

7import Idris.ElabTerm

8+import Idris.IBC

8import Paths_idris

9import Paths_idris

10import Core.CoreParser

11import Core.CoreParser

@@ -59,7 +60,8 @@ loadModule f

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

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

60 case fp of

61 case fp of

61 IDR fn -> loadSource fn

62 IDR fn -> loadSource fn

62− IBC fn -> error "Not implemented"

63+ IBC fn src -> idrisCatch (loadIBC fn)

64+ (\c -> loadSource src)

63 let (dir, fh) = splitFileName f

65 let (dir, fh) = splitFileName f

64 return (dropExtension fh))

66 return (dropExtension fh))

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

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

@@ -72,6 +74,8 @@ loadSource f = do iLOG ("Reading " ++ f)

72 file <- lift $ readFile f

74 file <- lift $ readFile f

73 (mname, modules, rest, pos) <- parseImports f file

75 (mname, modules, rest, pos) <- parseImports f file

74 mapM_ loadModule modules

76 mapM_ loadModule modules

77+ clearIBC -- start a new .ibc file

78+ mapM_ (\m -> addIBC (IBCImport m)) modules

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

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

76 f rest pos

80 f rest pos

77 let ds = namespaces mname ds'

81 let ds = namespaces mname ds'

@@ -82,6 +86,9 @@ loadSource f = do iLOG ("Reading " ++ f)

82 -- Now add all the declarations to the context

86 -- Now add all the declarations to the context

83 mapM_ (elabDecl toplevel) ds

87 mapM_ (elabDecl toplevel) ds

84 iLOG ("Finished " ++ f)

88 iLOG ("Finished " ++ f)

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

90+ idrisCatch (do writeIBC ibc; clearIBC)

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

85 return ()

92 return ()

86 where

93 where

87 namespaces [] ds = ds

94 namespaces [] ds = ds

@@ -216,9 +223,12 @@ pSyntaxDecl syn

216 i <- getState

223 i <- getState

217 let rs = syntax_rules i

224 let rs = syntax_rules i

218 let ns = syntax_keywords i

225 let ns = syntax_keywords i

226+ let ibc = ibc_write i

219 let ks = map show (names s)

227 let ks = map show (names s)

220 setState (i { syntax_rules = s : rs,

228 setState (i { syntax_rules = s : rs,

221− syntax_keywords = ks ++ ns })

229+ syntax_keywords = ks ++ ns,

230+ ibc_write = IBCSyntax s : map IBCKeyword ks ++ ibc

231+ })

222 fc <- pfc

232 fc <- pfc

223 return (PSyntax fc s)

233 return (PSyntax fc s)

224 where

234 where

@@ -312,7 +322,8 @@ pFixity = do f <- fixity; i <- natural; ops <- sepBy1 operator (lchar ',')

312 istate <- getState

322 istate <- getState

313 let fs = map (Fix (f prec)) ops

323 let fs = map (Fix (f prec)) ops

314 setState (istate {

324 setState (istate {

315− idris_infixes = sort (fs ++ idris_infixes istate) })

325+ idris_infixes = sort (fs ++ idris_infixes istate),

326+ ibc_write = map IBCFix fs ++ ibc_write istate })

316 fc <- pfc

327 fc <- pfc

317 return (PFix fc (f prec) ops)

328 return (PFix fc (f prec) ops)

318

329

@@ -785,13 +796,16 @@ pWhereblock n syn

785

796

786pDirective :: IParser [PDecl]

797pDirective :: IParser [PDecl]

787pDirective = try (do lchar '%'; reserved "lib"; lib <- strlit;

798pDirective = try (do lchar '%'; reserved "lib"; lib <- strlit;

788− return [PDirective (addLib lib)])

799+ return [PDirective (do addLib lib

800+ addIBC (IBCLib lib))])

789 <|> try (do lchar '%'; reserved "link"; obj <- strlit;

801 <|> try (do lchar '%'; reserved "link"; obj <- strlit;

790 return [PDirective (do datadir <- lift $ getDataDir

802 return [PDirective (do datadir <- lift $ getDataDir

791 o <- lift $ findInPath [".", datadir] obj

803 o <- lift $ findInPath [".", datadir] obj

804+ addIBC (IBCObj o)

792 addObjectFile o)])

805 addObjectFile o)])

793 <|> try (do lchar '%'; reserved "include"; hdr <- strlit;

806 <|> try (do lchar '%'; reserved "include"; hdr <- strlit;

794− return [PDirective (addHdr hdr)])

807+ return [PDirective (do addHdr hdr

808+ addIBC (IBCHeader hdr))])

795 <|> do lchar '%'; reserved "logging"; i <- natural;

809 <|> do lchar '%'; reserved "logging"; i <- natural;

796 return [PDirective (setLogLevel (fromInteger i))]

810 return [PDirective (setLogLevel (fromInteger i))]

797

811