@@ -331,67 +331,67 @@ getEntry alt f a = case findEntryByPath f a of
332unhide :: IBCPhase -> Archive -> Idris ()
332unhide :: IBCPhase -> Archive -> Idris ()
333unhide phase ar = do
333unhide phase ar = do
334− pImports True phase =<< getEntry [] "ibc_imports" ar
334+ processImports True phase ar
335− pAccess True phase =<< getEntry [] "ibc_access" ar
335+ processAccess True phase ar
337process :: Bool -- ^ Reexporting
337process :: Bool -- ^ Reexporting
338 -> IBCPhase
338 -> IBCPhase
339 -> Archive -> FilePath -> Idris ()
339 -> Archive -> FilePath -> Idris ()
340−process reexp phase i fn = do
340+process reexp phase archive fn = do
341− ver <- getEntry 0 "ver" i
341+ ver <- getEntry 0 "ver" archive
342 when (ver /= ibcVersion) $ do
342 when (ver /= ibcVersion) $ do
343 logIBC 1 "ibc out of date"
343 logIBC 1 "ibc out of date"
344 let e = if ver < ibcVersion
344 let e = if ver < ibcVersion
345 then " an earlier " else " a later "
345 then " an earlier " else " a later "
346 ifail $ "Incompatible ibc version.\nThis library was built with"
346 ifail $ "Incompatible ibc version.\nThis library was built with"
347 ++ e ++ "version of Idris.\n" ++ "Please clean and rebuild."
347 ++ e ++ "version of Idris.\n" ++ "Please clean and rebuild."
348− source <- getEntry "" "sourcefile" i
348+ source <- getEntry "" "sourcefile" archive
349 srcok <- runIO $ doesFileExist source
349 srcok <- runIO $ doesFileExist source
350 when srcok $ timestampOlder source fn
350 when srcok $ timestampOlder source fn
351− pImportDirs =<< getEntry [] "ibc_importdirs" i
351+ processImportDirs archive
352− pImports reexp phase =<< getEntry [] "ibc_imports" i
352+ processImports reexp phase archive
353− pImps =<< getEntry [] "ibc_implicits" i
353+ processImplicits archive
354− pFixes =<< getEntry [] "ibc_fixes" i
354+ processInfix archive
355− pStatics =<< getEntry [] "ibc_statics" i
355+ processStatics archive
356− pClasses =<< getEntry [] "ibc_classes" i
356+ processClasses archive
357− pRecords =<< getEntry [] "ibc_records" i
357+ processRecords archive
358− pInstances =<< getEntry [] "ibc_instances" i
358+ processInstances archive
359− pDSLs =<< getEntry [] "ibc_dsls" i
359+ processDSLs archive
360− pDatatypes =<< getEntry [] "ibc_datatypes" i
360+ processDatatypes archive
361− pOptimise =<< getEntry [] "ibc_optimise" i
361+ processOptimise archive
362− pSyntax =<< getEntry [] "ibc_syntax" i
362+ processSyntax archive
363− pKeywords =<< getEntry [] "ibc_keywords" i
363+ processKeywords archive
364− pObjs =<< getEntry [] "ibc_objs" i
364+ processObjectFiles archive
365− pLibs =<< getEntry [] "ibc_libs" i
365+ processLibs archive
366− pCGFlags =<< getEntry [] "ibc_cgflags" i
366+ processCodegenFlags archive
367− pDyLibs =<< getEntry [] "ibc_dynamic_libs" i
367+ processDynamicLibs archive
368− pHdrs =<< getEntry [] "ibc_hdrs" i
368+ processHeaders archive
369− pPatdefs =<< getEntry [] "ibc_patdefs" i
369+ processPatternDefs archive
370− pFlags =<< getEntry [] "ibc_flags" i
370+ processFlags archive
371− pFnInfo =<< getEntry [] "ibc_fninfo" i
371+ processFnInfo archive
372− pTotCheckErr =<< getEntry [] "ibc_totcheckfail" i
372+ processTotalityCheckError archive
373− pCG =<< getEntry [] "ibc_cg" i
373+ processCallgraph archive
374− pDocs =<< getEntry [] "ibc_docstrings" i
374+ processDocs archive
375− pMDocs =<< getEntry [] "ibc_moduledocs" i
375+ processModuleDocs archive
376− pCoercions =<< getEntry [] "ibc_coercions" i
376+ processCoercions archive
377− pTrans =<< getEntry [] "ibc_transforms" i
377+ processTransforms archive
378− pErrRev =<< getEntry [] "ibc_errRev" i
378+ processErrRev archive
379− pLineApps =<< getEntry [] "ibc_lineapps" i
379+ processLineApps archive
380− pNameHints =<< getEntry [] "ibc_namehints" i
380+ processNameHints archive
381− pMetaInformation =<< getEntry [] "ibc_metainformation" i
381+ processMetaInformation archive
382− pErrorHandlers =<< getEntry [] "ibc_errorhandlers" i
382+ processErrorHandlers archive
383− pFunctionErrorHandlers =<< getEntry [] "ibc_function_errorhandlers" i
383+ processFunctionErrorHandlers archive
384− pMetavars =<< getEntry [] "ibc_metavars" i
384+ processMetaVars archive
385− pPostulates =<< getEntry [] "ibc_postulates" i
385+ processPostulates archive
386− pExterns =<< getEntry [] "ibc_externs" i
386+ processExterns archive
387− pParsedSpan =<< getEntry Nothing "ibc_parsedSpan" i
387+ processParsedSpan archive
388− pUsage =<< getEntry [] "ibc_usage" i
388+ processUsage archive
389− pExports =<< getEntry [] "ibc_exports" i
389+ processExports archive
390− pAutoHints =<< getEntry [] "ibc_autohints" i
390+ processAutoHints archive
391− pDeprecate =<< getEntry [] "ibc_deprecated" i
391+ processDeprecate archive
392− pDefs reexp =<< getEntry [] "ibc_defs" i
392+ processDefs archive
393− pTotal =<< getEntry [] "ibc_total" i
393+ processTotal archive
394− pAccess reexp phase =<< getEntry [] "ibc_access" i
394+ processAccess reexp phase archive
396timestampOlder :: FilePath -> FilePath -> Idris ()
396timestampOlder :: FilePath -> FilePath -> Idris ()
397timestampOlder src ibc = do srct <- runIO $ getModificationTime src
397timestampOlder src ibc = do srct <- runIO $ getModificationTime src
@@ -400,280 +400,364 @@ timestampOlder src ibc = do srct <- runIO $ getModificationTime src
400 then ifail $ "Needs reloading " ++ show (srct, ibct)
400 then ifail $ "Needs reloading " ++ show (srct, ibct)
401 else return ()
401 else return ()
403−pPostulates :: [Name] -> Idris ()
403+processPostulates :: Archive -> Idris ()
404−pPostulates ns = updateIState
404+processPostulates ar = do
405+ ns <- getEntry [] "ibc_postulates" ar
405− (\i -> i { idris_postulates = idris_postulates i `S.union` S.fromList ns })
406+ updateIState (\i -> i { idris_postulates = idris_postulates i `S.union` S.fromList ns })
407−pExterns :: [(Name, Int)] -> Idris ()
408+processExterns :: Archive -> Idris ()
409+processExterns ar = do
410+ ns <- getEntry [] "ibc_externs" ar
408−pExterns ns = updateIState (\i -> i{ idris_externs = idris_externs i `S.union` S.fromList ns })
411+ updateIState (\i -> i{ idris_externs = idris_externs i `S.union` S.fromList ns })
410−pParsedSpan :: Maybe FC -> Idris ()
413+processParsedSpan :: Archive -> Idris ()
414+processParsedSpan ar = do
415+ fc <- getEntry Nothing "ibc_parsedSpan" ar
411−pParsedSpan fc = updateIState (\i -> i { idris_parsedSpan = fc })
416+ updateIState (\i -> i { idris_parsedSpan = fc })
413−pUsage :: [(Name, Int)] -> Idris ()
418+processUsage :: Archive -> Idris ()
420+ ns <- getEntry [] "ibc_usage" ar
414−pUsage ns = updateIState (\i -> i { idris_erasureUsed = ns ++ idris_erasureUsed i })
421+ updateIState (\i -> i { idris_erasureUsed = ns ++ idris_erasureUsed i })
416−pExports :: [Name] -> Idris ()
423+processExports :: Archive -> Idris ()
424+processExports ar = do
425+ ns <- getEntry [] "ibc_exports" ar
417−pExports ns = updateIState (\i -> i { idris_exports = ns ++ idris_exports i })
426+ updateIState (\i -> i { idris_exports = ns ++ idris_exports i })
419−pAutoHints :: [(Name, Name)] -> Idris ()
428+processAutoHints :: Archive -> Idris ()
429+processAutoHints ar = do
430+ ns <- getEntry [] "ibc_autohints" ar
420−pAutoHints ns = mapM_ (\(n,h) -> addAutoHint n h) ns
431+ mapM_ (\(n,h) -> addAutoHint n h) ns
422−pDeprecate :: [(Name, String)] -> Idris ()
433+processDeprecate :: Archive -> Idris ()
434+processDeprecate ar = do
435+ ns <- getEntry [] "ibc_deprecated" ar
423−pDeprecate ns = mapM_ (\(n,reason) -> addDeprecated n reason) ns
436+ mapM_ (\(n,reason) -> addDeprecated n reason) ns
425−pImportDirs :: [FilePath] -> Idris ()
438+processImportDirs :: Archive -> Idris ()
439+processImportDirs ar = do
440+ fs <- getEntry [] "ibc_importdirs" ar
426−pImportDirs fs = mapM_ addImportDir fs
441+ mapM_ addImportDir fs
428−pImports :: Bool -> IBCPhase -> [(Bool, FilePath)] -> Idris ()
443+processImports :: Bool -> IBCPhase -> Archive -> Idris ()
429−pImports reexp phase fs
444+processImports reexp phase ar = do
445+ fs <- getEntry [] "ibc_imports" ar
430− = do mapM_ (\(re, f) ->
446+ mapM_ (\(re, f) -> do
431− do i <- getIState
447+ i <- getIState
432− ibcsd <- valIBCSubDir i
448+ ibcsd <- valIBCSubDir i
433− ids <- allImportDirs
449+ ids <- allImportDirs
434− fp <- findImport ids ibcsd f
450+ fp <- findImport ids ibcsd f
435-- if (f `elem` imported i)
451-- if (f `elem` imported i)
436-- then logLvl 1 $ "Already read " ++ f
452-- then logLvl 1 $ "Already read " ++ f
437− putIState (i { imported = f : imported i })
453+ putIState (i { imported = f : imported i })
438− let phase' = case phase of
454+ let phase' = case phase of
439− IBC_REPL _ -> IBC_REPL False
455+ IBC_REPL _ -> IBC_REPL False
441− case fp of
457+ case fp of
442− LIDR fn -> do
458+ LIDR fn -> do
443− logIBC 1 $ "Failed at " ++ fn
459+ logIBC 1 $ "Failed at " ++ fn
444− ifail "Must be an ibc"
460+ ifail "Must be an ibc"
445− IDR fn -> do
461+ IDR fn -> do
446− logIBC 1 $ "Failed at " ++ fn
462+ logIBC 1 $ "Failed at " ++ fn
447− ifail "Must be an ibc"
463+ ifail "Must be an ibc"
448− IBC fn src -> loadIBC (reexp && re) phase' fn)
464+ IBC fn src -> loadIBC (reexp && re) phase' fn) fs
450−
466+processImplicits :: Archive -> Idris ()
451−pImps :: [(Name, [PArg])] -> Idris ()
467+processImplicits ar = do
468+ imps <- getEntry [] "ibc_implicits" ar
452−pImps imps = mapM_ (\ (n, imp) ->
469+ mapM_ (\ (n, imp) -> do
453− do i <- getIState
470+ i <- getIState
454− case lookupDefAccExact n False (tt_ctxt i) of
471+ case lookupDefAccExact n False (tt_ctxt i) of
455− Just (n, Hidden) -> return ()
472+ Just (n, Hidden) -> return ()
456− Just (n, Private) -> return ()
473+ Just (n, Private) -> return ()
457− _ -> putIState (i { idris_implicits
474+ _ -> putIState (i { idris_implicits = addDef n imp (idris_implicits i) })) imps
458− = addDef n imp (idris_implicits i) }))
475+
459− imps
476+processInfix :: Archive -> Idris ()
460−
477+processInfix ar = do
461−pFixes :: [FixDecl] -> Idris ()
478+ f <- getEntry [] "ibc_fixes" ar
462−pFixes f = do i <- getIState
463− putIState (i { idris_infixes = sort $ f ++ idris_infixes i })
479+ updateIState (\i -> i { idris_infixes = sort $ f ++ idris_infixes i })
465−pStatics :: [(Name, [Bool])] -> Idris ()
481+processStatics :: Archive -> Idris ()
482+processStatics ar = do
483+ ss <- getEntry [] "ibc_statics" ar
466−pStatics ss = mapM_ (\ (n, s) ->
484+ mapM_ (\ (n, s) ->
468− putIState (i { idris_statics
469− = addDef n s (idris_statics i) }))
485+ updateIState (\i -> i { idris_statics = addDef n s (idris_statics i) })) ss
471−
487+processClasses :: Archive -> Idris ()
472−pClasses :: [(Name, ClassInfo)] -> Idris ()
488+processClasses ar = do
489+ cs <- getEntry [] "ibc_classes" ar
473−pClasses cs = mapM_ (\ (n, c) ->
490+ mapM_ (\ (n, c) -> do
474− do i <- getIState
491+ i <- getIState
475− -- Don't lose instances from previous IBCs, which
492+ -- Don't lose instances from previous IBCs, which
476− -- could have loaded in any order
493+ -- could have loaded in any order
477− let is = case lookupCtxtExact n (idris_classes i) of
494+ let is = case lookupCtxtExact n (idris_classes i) of
478− Just (CI _ _ _ _ _ ins _) -> ins
495+ Just (CI _ _ _ _ _ ins _) -> ins
480− let c' = c { class_instances =
497+ let c' = c { class_instances = class_instances c ++ is }
481− class_instances c ++ is }
482− putIState (i { idris_classes
498+ putIState (i { idris_classes = addDef n c' (idris_classes i) })) cs
483− = addDef n c' (idris_classes i) }))
499+
484− cs
500+processRecords :: Archive -> Idris ()
485−
501+processRecords ar = do
486−pRecords :: [(Name, RecordInfo)] -> Idris ()
502+ rs <- getEntry [] "ibc_records" ar
487−pRecords rs = mapM_ (\ (n, r) ->
503+ mapM_ (\ (n, r) ->
489− putIState (i { idris_records
490− = addDef n r (idris_records i) }))
504+ updateIState (\i -> i { idris_records = addDef n r (idris_records i) })) rs
492−
506+processInstances :: Archive -> Idris ()
493−pInstances :: [(Bool, Bool, Name, Name)] -> Idris ()
507+processInstances ar = do
508+ cs <- getEntry [] "ibc_instances" ar
494−pInstances cs = mapM_ (\ (i, res, n, ins) -> addInstance i res n ins) cs
509+ mapM_ (\ (i, res, n, ins) -> addInstance i res n ins) cs
496−pDSLs :: [(Name, DSL)] -> Idris ()
511+processDSLs :: Archive -> Idris ()
513+ cs <- getEntry [] "ibc_dsls" ar
497−pDSLs cs = mapM_ (\ (n, c) -> updateIState (\i ->
514+ mapM_ (\ (n, c) -> updateIState (\i ->
498 i { idris_dsls = addDef n c (idris_dsls i) })) cs
515 i { idris_dsls = addDef n c (idris_dsls i) })) cs
500−pDatatypes :: [(Name, TypeInfo)] -> Idris ()
517+processDatatypes :: Archive -> Idris ()
518+processDatatypes ar = do
519+ cs <- getEntry [] "ibc_datatypes" ar
501−pDatatypes cs = mapM_ (\ (n, c) -> updateIState (\i ->
520+ mapM_ (\ (n, c) -> updateIState (\i ->
502 i { idris_datatypes = addDef n c (idris_datatypes i) })) cs
521 i { idris_datatypes = addDef n c (idris_datatypes i) })) cs
504−pOptimise :: [(Name, OptInfo)] -> Idris ()
523+processOptimise :: Archive -> Idris ()
524+processOptimise ar = do
525+ cs <- getEntry [] "ibc_optimise" ar
505−pOptimise cs = mapM_ (\ (n, c) -> updateIState (\i ->
526+ mapM_ (\ (n, c) -> updateIState (\i ->
506 i { idris_optimisation = addDef n c (idris_optimisation i) })) cs
527 i { idris_optimisation = addDef n c (idris_optimisation i) })) cs
508−pSyntax :: [Syntax] -> Idris ()
529+processSyntax :: Archive -> Idris ()
530+processSyntax ar = do
531+ s <- getEntry [] "ibc_syntax" ar
509−pSyntax s = updateIState (\i -> i { syntax_rules = updateSyntaxRules s (syntax_rules i) })
532+ updateIState (\i -> i { syntax_rules = updateSyntaxRules s (syntax_rules i) })
511−pKeywords :: [String] -> Idris ()
534+processKeywords :: Archive -> Idris ()
535+processKeywords ar = do
536+ k <- getEntry [] "ibc_keywords" ar
512−pKeywords k = updateIState (\i -> i { syntax_keywords = k ++ syntax_keywords i })
537+ updateIState (\i -> i { syntax_keywords = k ++ syntax_keywords i })
514−pObjs :: [(Codegen, FilePath)] -> Idris ()
539+processObjectFiles :: Archive -> Idris ()
540+processObjectFiles ar = do
541+ os <- getEntry [] "ibc_objs" ar
542+ mapM_ (\ (cg, obj) -> do
515−pObjs os = mapM_ (\ (cg, obj) -> do dirs <- allImportDirs
543+ dirs <- allImportDirs
516− o <- runIO $ findInPath dirs obj
544+ o <- runIO $ findInPath dirs obj
517− addObjectFile cg o) os
545+ addObjectFile cg o) os
519−pLibs :: [(Codegen, String)] -> Idris ()
547+processLibs :: Archive -> Idris ()
549+ ls <- getEntry [] "ibc_libs" ar
520−pLibs ls = mapM_ (uncurry addLib) ls
550+ mapM_ (uncurry addLib) ls
522−pCGFlags :: [(Codegen, String)] -> Idris ()
552+processCodegenFlags :: Archive -> Idris ()
553+processCodegenFlags ar = do
554+ ls <- getEntry [] "ibc_cgflags" ar
523−pCGFlags ls = mapM_ (uncurry addFlag) ls
555+ mapM_ (uncurry addFlag) ls
525−pDyLibs :: [String] -> Idris ()
557+processDynamicLibs :: Archive -> Idris ()
558+processDynamicLibs ar = do
559+ ls <- getEntry [] "ibc_dynamic_libs" ar
526−pDyLibs ls = do res <- mapM (addDyLib . return) ls
560+ res <- mapM (addDyLib . return) ls
527− mapM_ checkLoad res
561+ mapM_ checkLoad res
529− where checkLoad (Left _) = return ()
563+ checkLoad (Left _) = return ()
530− checkLoad (Right err) = ifail err
564+ checkLoad (Right err) = ifail err
532−pHdrs :: [(Codegen, String)] -> Idris ()
566+processHeaders :: Archive -> Idris ()
567+processHeaders ar = do
568+ hs <- getEntry [] "ibc_hdrs" ar
533−pHdrs hs = mapM_ (uncurry addHdr) hs
569+ mapM_ (uncurry addHdr) hs
535−pPatdefs :: [(Name, ([([(Name, Term)], Term, Term)], [PTerm]))] -> Idris ()
571+processPatternDefs :: Archive -> Idris ()
572+processPatternDefs ar = do
573+ ds <- getEntry [] "ibc_patdefs" ar
536−pPatdefs ds = mapM_ (\ (n, d) -> updateIState (\i ->
574+ mapM_ (\ (n, d) -> updateIState (\i ->
537 i { idris_patdefs = addDef n (force d) (idris_patdefs i) })) ds
575 i { idris_patdefs = addDef n (force d) (idris_patdefs i) })) ds
539−pDefs :: Bool -> [(Name, Def)] -> Idris ()
577+processDefs :: Archive -> Idris ()
540−pDefs reexp ds
578+processDefs ar = do
579+ ds <- getEntry [] "ibc_defs" ar
541− = mapM_ (\ (n, d) ->
580+ mapM_ (\ (n, d) -> do
542− do d' <- updateDef d
581+ d' <- updateDef d
543− case d' of
582+ case d' of
544− TyDecl _ _ -> return ()
583+ TyDecl _ _ -> return ()
545− _ -> do logIBC 1 $ "SOLVING " ++ show n
585+ logIBC 1 $ "SOLVING " ++ show n
546− solveDeferred emptyFC n
586+ solveDeferred emptyFC n
547− updateIState (\i -> i { tt_ctxt = addCtxtDef n d' (tt_ctxt i) })
587+ updateIState (\i -> i { tt_ctxt = addCtxtDef n d' (tt_ctxt i) })) ds
550− updateDef (CaseOp c t args o s cd)
589+ updateDef (CaseOp c t args o s cd) = do
551− = do o' <- mapM updateOrig o
590+ o' <- mapM updateOrig o
552− cd' <- updateCD cd
591+ cd' <- updateCD cd
553− return $ CaseOp c t args o' s cd'
592+ return $ CaseOp c t args o' s cd'
554− updateDef t = return t
593+ updateDef t = return t
556− updateOrig (Left t) = liftM Left (update t)
595+ updateOrig (Left t) = liftM Left (update t)
557− updateOrig (Right (l, r)) = do l' <- update l
596+ updateOrig (Right (l, r)) = do
558− r' <- update r
598+ r' <- update r
559− return $ Right (l', r')
599+ return $ Right (l', r')
561− updateCD (CaseDefs (ts, t) (cs, c) (is, i) (rs, r))
601+ updateCD (CaseDefs (ts, t) (cs, c) (is, i) (rs, r)) = do
562− = do c' <- updateSC c
602+ c' <- updateSC c
563− r' <- updateSC r
603+ r' <- updateSC r
564− return $ CaseDefs (cs, c') (cs, c') (cs, c') (rs, r')
604+ return $ CaseDefs (cs, c') (cs, c') (cs, c') (rs, r')
606+ updateSC (Case t n alts) = do
566− updateSC (Case t n alts) = do alts' <- mapM updateAlt alts
607+ alts' <- mapM updateAlt alts
567− return (Case t n alts')
608+ return (Case t n alts')
568− updateSC (ProjCase t alts) = do alts' <- mapM updateAlt alts
609+ updateSC (ProjCase t alts) = do
610+ alts' <- mapM updateAlt alts
569− return (ProjCase t alts')
611+ return (ProjCase t alts')
570− updateSC (STerm t) = do t' <- update t
612+ updateSC (STerm t) = do
571− return (STerm t')
614+ return (STerm t')
572− updateSC c = return c
615+ updateSC c = return c
574− updateAlt (ConCase n i ns t) = do t' <- updateSC t
617+ updateAlt (ConCase n i ns t) = do
575− return (ConCase n i ns t')
619+ return (ConCase n i ns t')
576− updateAlt (FnCase n ns t) = do t' <- updateSC t
620+ updateAlt (FnCase n ns t) = do
577− return (FnCase n ns t')
622+ return (FnCase n ns t')
578− updateAlt (ConstCase c t) = do t' <- updateSC t
623+ updateAlt (ConstCase c t) = do
579− return (ConstCase c t')
625+ return (ConstCase c t')
580− updateAlt (SucCase n t) = do t' <- updateSC t
626+ updateAlt (SucCase n t) = do
581− return (SucCase n t')
628+ return (SucCase n t')
582− updateAlt (DefaultCase t) = do t' <- updateSC t
629+ updateAlt (DefaultCase t) = do
583− return (DefaultCase t')
631+ return (DefaultCase t')
585− -- We get a lot of repetition in sub terms and can save a fair chunk
633+ -- We get a lot of repetition in sub terms and can save a fair chunk
586− -- of memory if we make sure they're shared. addTT looks for a term
634+ -- of memory if we make sure they're shared. addTT looks for a term
587− -- and returns it if it exists already, while also keeping stats of
635+ -- and returns it if it exists already, while also keeping stats of
588− -- how many times a subterm is repeated.
636+ -- how many times a subterm is repeated.
589− update t = do tm <- addTT t
637+ update t = do
590− case tm of
639+ case tm of
591− Nothing -> update' t
640+ Nothing -> update' t
592− Just t' -> return t'
641+ Just t' -> return t'
594− update' (P t n ty) = do n' <- getSymbol n
643+ update' (P t n ty) = do
595− return $ P t n' ty
645+ return $ P t n' ty
596− update' (App s f a) = liftM2 (App s) (update' f) (update' a)
646+ update' (App s f a) = liftM2 (App s) (update' f) (update' a)
597− update' (Bind n b sc) = do b' <- updateB b
647+ update' (Bind n b sc) = do
598− sc' <- update sc
649+ sc' <- update sc
599− return $ Bind n b' sc'
650+ return $ Bind n b' sc'
601− updateB (Let t v) = liftM2 Let (update' t) (update' v)
652+ updateB (Let t v) = liftM2 Let (update' t) (update' v)
602− updateB b = do ty' <- update' (binderTy b)
654+ ty' <- update' (binderTy b)
603− return (b { binderTy = ty' })
655+ return (b { binderTy = ty' })
604− update' (Proj t i) = do t' <- update' t
656+ update' (Proj t i) = do
605− return $ Proj t' i
658+ return $ Proj t' i
606− update' t = return t
659+ update' t = return t
608−pDocs :: [(Name, (Docstring D.DocTerm, [(Name, Docstring D.DocTerm)]))] -> Idris ()
661+processDocs :: Archive -> Idris ()
663+ ds <- getEntry [] "ibc_docstrings" ar
609−pDocs ds = mapM_ (\(n, a) -> addDocStr n (fst a) (snd a)) ds
664+ mapM_ (\(n, a) -> addDocStr n (fst a) (snd a)) ds
611−pMDocs :: [(Name, Docstring D.DocTerm)] -> Idris ()
666+processModuleDocs :: Archive -> Idris ()
667+processModuleDocs ar = do
668+ ds <- getEntry [] "ibc_moduledocs" ar
612−pMDocs ds = mapM_ (\ (n, d) -> updateIState (\i ->
669+ mapM_ (\ (n, d) -> updateIState (\i ->
613 i { idris_moduledocs = addDef n d (idris_moduledocs i) })) ds
670 i { idris_moduledocs = addDef n d (idris_moduledocs i) })) ds
615−pAccess :: Bool -- ^ Reexporting?
672+processAccess :: Bool -- ^ Reexporting?
616 -> IBCPhase
673 -> IBCPhase
617− -> [(Name, Accessibility)] -> Idris ()
674+ -> Archive -> Idris ()
618−pAccess reexp phase ds
675+processAccess reexp phase ar = do
676+ ds <- getEntry [] "ibc_access" ar
619− = mapM_ (\ (n, a_in) ->
677+ mapM_ (\ (n, a_in) -> do
620− do let a = if reexp then a_in else Hidden
678+ let a = if reexp then a_in else Hidden
621− logIBC 3 $ "Setting " ++ show (a, n) ++ " to " ++ show a
679+ logIBC 3 $ "Setting " ++ show (a, n) ++ " to " ++ show a
622− updateIState (\i -> i { tt_ctxt = setAccess n a (tt_ctxt i) })
680+ updateIState (\i -> i { tt_ctxt = setAccess n a (tt_ctxt i) })
624− if (not reexp) then do logIBC 1 $ "Not exporting " ++ show n
684+ logIBC 1 $ "Not exporting " ++ show n
625− setAccessibility n Hidden
685+ setAccessibility n Hidden
626− else logIBC 1 $ "Exporting " ++ show n
686+ else logIBC 1 $ "Exporting " ++ show n
627− -- Everything should be available at the REPL from
687+ -- Everything should be available at the REPL from
628− -- things imported publicly
688+ -- things imported publicly
629− when (phase == IBC_REPL True) $
630− setAccessibility n Public
689+ when (phase == IBC_REPL True) $ setAccessibility n Public) ds
632−
691+processFlags :: Archive -> Idris ()
633−pFlags :: [(Name, [FnOpt])] -> Idris ()
692+processFlags ar = do
693+ ds <- getEntry [] "ibc_flags" ar
634−pFlags ds = mapM_ (\ (n, a) -> setFlags n a) ds
694+ mapM_ (\ (n, a) -> setFlags n a) ds
636−pFnInfo :: [(Name, FnInfo)] -> Idris ()
696+processFnInfo :: Archive -> Idris ()
697+processFnInfo ar = do
698+ ds <- getEntry [] "ibc_fninfo" ar
637−pFnInfo ds = mapM_ (\ (n, a) -> setFnInfo n a) ds
699+ mapM_ (\ (n, a) -> setFnInfo n a) ds
639−pTotal :: [(Name, Totality)] -> Idris ()
701+processTotal :: Archive -> Idris ()
703+ ds <- getEntry [] "ibc_total" ar
640−pTotal ds = mapM_ (\ (n, a) -> updateIState (\i -> i { tt_ctxt = setTotal n a (tt_ctxt i) })) ds
704+ mapM_ (\ (n, a) -> updateIState (\i -> i { tt_ctxt = setTotal n a (tt_ctxt i) })) ds
642−pTotCheckErr :: [(FC, String)] -> Idris ()
706+processTotalityCheckError :: Archive -> Idris ()
707+processTotalityCheckError ar = do
708+ es <- getEntry [] "ibc_totcheckfail" ar
643−pTotCheckErr es = updateIState (\i -> i { idris_totcheckfail = idris_totcheckfail i ++ es })
709+ updateIState (\i -> i { idris_totcheckfail = idris_totcheckfail i ++ es })
645−pCG :: [(Name, CGInfo)] -> Idris ()
711+processCallgraph :: Archive -> Idris ()
712+processCallgraph ar = do
713+ ds <- getEntry [] "ibc_cg" ar
646−pCG ds = mapM_ (\ (n, a) -> addToCG n a) ds
714+ mapM_ (\ (n, a) -> addToCG n a) ds
648−pCoercions :: [Name] -> Idris ()
716+processCoercions :: Archive -> Idris ()
717+processCoercions ar = do
718+ ns <- getEntry [] "ibc_coercions" ar
649−pCoercions ns = mapM_ (\ n -> addCoercion n) ns
719+ mapM_ (\ n -> addCoercion n) ns
651−pTrans :: [(Name, (Term, Term))] -> Idris ()
721+processTransforms :: Archive -> Idris ()
722+processTransforms ar = do
723+ ts <- getEntry [] "ibc_transforms" ar
652−pTrans ts = mapM_ (\ (n, t) -> addTrans n t) ts
724+ mapM_ (\ (n, t) -> addTrans n t) ts
654−pErrRev :: [(Term, Term)] -> Idris ()
726+processErrRev :: Archive -> Idris ()
727+processErrRev ar = do
728+ ts <- getEntry [] "ibc_errRev" ar
655−pErrRev ts = mapM_ addErrRev ts
729+ mapM_ addErrRev ts
657−pLineApps :: [(FilePath, Int, PTerm)] -> Idris ()
731+processLineApps :: Archive -> Idris ()
732+processLineApps ar = do
733+ ls <- getEntry [] "ibc_lineapps" ar
658−pLineApps ls = mapM_ (\ (f, i, t) -> addInternalApp f i t) ls
734+ mapM_ (\ (f, i, t) -> addInternalApp f i t) ls
660−pNameHints :: [(Name, Name)] -> Idris ()
736+processNameHints :: Archive -> Idris ()
737+processNameHints ar = do
738+ ns <- getEntry [] "ibc_namehints" ar
661−pNameHints ns = mapM_ (\ (n, ty) -> addNameHint n ty) ns
739+ mapM_ (\ (n, ty) -> addNameHint n ty) ns
663−pMetaInformation :: [(Name, MetaInformation)] -> Idris ()
741+processMetaInformation :: Archive -> Idris ()
742+processMetaInformation ar = do
743+ ds <- getEntry [] "ibc_metainformation" ar
664−pMetaInformation ds = mapM_ (\ (n, m) -> updateIState (\i ->
744+ mapM_ (\ (n, m) -> updateIState (\i ->
665 i { tt_ctxt = setMetaInformation n m (tt_ctxt i) })) ds
745 i { tt_ctxt = setMetaInformation n m (tt_ctxt i) })) ds
667−pErrorHandlers :: [Name] -> Idris ()
747+processErrorHandlers :: Archive -> Idris ()
668−pErrorHandlers ns = updateIState (\i ->
748+processErrorHandlers ar = do
749+ ns <- getEntry [] "ibc_errorhandlers" ar
669− i { idris_errorhandlers = idris_errorhandlers i ++ ns })
750+ updateIState (\i -> i { idris_errorhandlers = idris_errorhandlers i ++ ns })
671−pFunctionErrorHandlers :: [(Name, Name, Name)] -> Idris ()
752+processFunctionErrorHandlers :: Archive -> Idris ()
672−pFunctionErrorHandlers ns = mapM_ (\ (fn,arg,handler) ->
753+processFunctionErrorHandlers ar = do
754+ ns <- getEntry [] "ibc_function_errorhandlers" ar
673− addFunctionErrorHandlers fn arg [handler]) ns
755+ mapM_ (\ (fn,arg,handler) -> addFunctionErrorHandlers fn arg [handler]) ns
675−pMetavars :: [(Name, (Maybe Name, Int, [Name], Bool, Bool))] -> Idris ()
757+processMetaVars :: Archive -> Idris ()
758+processMetaVars ar = do
759+ ns <- getEntry [] "ibc_metavars" ar
676−pMetavars ns = updateIState (\i -> i { idris_metavars = L.reverse ns ++ idris_metavars i })
760+ updateIState (\i -> i { idris_metavars = L.reverse ns ++ idris_metavars i })
678----- For Cheapskate and docstrings
762----- For Cheapskate and docstrings