{-|
Module      : Idris.IBC
Description : Core representations and code to generate IBC files.

License     : BSD3
Maintainer  : The Idris Community.
-}

{-# LANGUAGE FlexibleInstances, TypeSynonymInstances #-}
{-# OPTIONS_GHC -fwarn-incomplete-patterns #-}
{-# OPTIONS_GHC -fwarn-unused-imports #-}

module Idris.IBC (loadIBC, loadPkgIndex,
                  writeIBC, writePkgIndex,
                  hasValidIBCVersion, IBCPhase(..),
                  getIBCHash, getImportHashes) where

import Idris.AbsSyntax
import Idris.Core.CaseTree
import Idris.Core.Evaluate
import Idris.Core.TT
import Idris.DeepSeq ()
import Idris.Docstrings (Docstring)
import qualified Idris.Docstrings as D
import Idris.Error
import Idris.Imports
import Idris.Options
import Idris.Output
import IRTS.System (getIdrisLibDir)

import qualified Cheapskate.Types as CT
import Codec.Archive.Zip
import Control.DeepSeq
import Control.Monad
import Data.Binary
import Data.ByteString.Lazy as B hiding (elem, length, map)
import Data.List as L
import Data.Maybe (catMaybes)
import qualified Data.Set as S
import System.Directory
import System.FilePath

ibcVersion :: Word16
ibcVersion :: Word16
ibcVersion = Word16
167

-- | When IBC is being loaded - we'll load different things (and omit
-- different structures/definitions) depending on which phase we're in.
data IBCPhase = IBC_Building  -- ^ when building the module tree
              | IBC_REPL Bool -- ^ when loading modules for the REPL Bool = True for top level module
  deriving (Int -> IBCPhase -> ShowS
[IBCPhase] -> ShowS
IBCPhase -> String
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
showList :: [IBCPhase] -> ShowS
$cshowList :: [IBCPhase] -> ShowS
show :: IBCPhase -> String
$cshow :: IBCPhase -> String
showsPrec :: Int -> IBCPhase -> ShowS
$cshowsPrec :: Int -> IBCPhase -> ShowS
Show, IBCPhase -> IBCPhase -> Bool
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
/= :: IBCPhase -> IBCPhase -> Bool
$c/= :: IBCPhase -> IBCPhase -> Bool
== :: IBCPhase -> IBCPhase -> Bool
$c== :: IBCPhase -> IBCPhase -> Bool
Eq)

data IBCFile = IBCFile {
    IBCFile -> Word16
ver                        :: Word16
  , IBCFile -> Int
iface_hash                 :: Int
  , IBCFile -> String
sourcefile                 :: FilePath
  , IBCFile -> [(Bool, String)]
ibc_imports                :: ![(Bool, FilePath)]
  , IBCFile -> [String]
ibc_importdirs             :: ![FilePath]
  , IBCFile -> [String]
ibc_sourcedirs             :: ![FilePath]
  , IBCFile -> [(Name, [PArg])]
ibc_implicits              :: ![(Name, [PArg])]
  , IBCFile -> [FixDecl]
ibc_fixes                  :: ![FixDecl]
  , IBCFile -> [(Name, [Bool])]
ibc_statics                :: ![(Name, [Bool])]
  , IBCFile -> [(Name, InterfaceInfo)]
ibc_interfaces             :: ![(Name, InterfaceInfo)]
  , IBCFile -> [(Name, RecordInfo)]
ibc_records                :: ![(Name, RecordInfo)]
  , IBCFile -> [(Bool, Bool, Name, Name)]
ibc_implementations        :: ![(Bool, Bool, Name, Name)]
  , IBCFile -> [(Name, DSL)]
ibc_dsls                   :: ![(Name, DSL)]
  , IBCFile -> [(Name, TypeInfo)]
ibc_datatypes              :: ![(Name, TypeInfo)]
  , IBCFile -> [(Name, OptInfo)]
ibc_optimise               :: ![(Name, OptInfo)]
  , IBCFile -> [Syntax]
ibc_syntax                 :: ![Syntax]
  , IBCFile -> [String]
ibc_keywords               :: ![String]
  , IBCFile -> [(Codegen, String)]
ibc_objs                   :: ![(Codegen, FilePath)]
  , IBCFile -> [(Codegen, String)]
ibc_libs                   :: ![(Codegen, String)]
  , IBCFile -> [(Codegen, String)]
ibc_cgflags                :: ![(Codegen, String)]
  , IBCFile -> [String]
ibc_dynamic_libs           :: ![String]
  , IBCFile -> [(Codegen, String)]
ibc_hdrs                   :: ![(Codegen, String)]
  , IBCFile -> [(FC, String)]
ibc_totcheckfail           :: ![(FC, String)]
  , IBCFile -> [(Name, FnOpts)]
ibc_flags                  :: ![(Name, [FnOpt])]
  , IBCFile -> [(Name, FnInfo)]
ibc_fninfo                 :: ![(Name, FnInfo)]
  , IBCFile -> [(Name, CGInfo)]
ibc_cg                     :: ![(Name, CGInfo)]
  , IBCFile
-> [(Name, (Docstring DocTerm, [(Name, Docstring DocTerm)]))]
ibc_docstrings             :: ![(Name, (Docstring D.DocTerm, [(Name, Docstring D.DocTerm)]))]
  , IBCFile -> [(Name, Docstring DocTerm)]
ibc_moduledocs             :: ![(Name, Docstring D.DocTerm)]
  , IBCFile -> [(Name, (TT Name, TT Name))]
ibc_transforms             :: ![(Name, (Term, Term))]
  , IBCFile -> [(TT Name, TT Name)]
ibc_errRev                 :: ![(Term, Term)]
  , IBCFile -> [Name]
ibc_errReduce              :: ![Name]
  , IBCFile -> [Name]
ibc_coercions              :: ![Name]
  , IBCFile -> [(String, Int, PTerm)]
ibc_lineapps               :: ![(FilePath, Int, PTerm)]
  , IBCFile -> [(Name, Name)]
ibc_namehints              :: ![(Name, Name)]
  , IBCFile -> [(Name, MetaInformation)]
ibc_metainformation        :: ![(Name, MetaInformation)]
  , IBCFile -> [Name]
ibc_errorhandlers          :: ![Name]
  , IBCFile -> [(Name, Name, Name)]
ibc_function_errorhandlers :: ![(Name, Name, Name)] -- fn, arg, handler
  , IBCFile -> [(Name, (Maybe Name, Int, [Name], Bool, Bool))]
ibc_metavars               :: ![(Name, (Maybe Name, Int, [Name], Bool, Bool))]
  , IBCFile
-> [(Name, ([([(Name, TT Name)], TT Name, TT Name)], [PTerm]))]
ibc_patdefs                :: ![(Name, ([([(Name, Term)], Term, Term)], [PTerm]))]
  , IBCFile -> [Name]
ibc_postulates             :: ![Name]
  , IBCFile -> [(Name, Int)]
ibc_externs                :: ![(Name, Int)]
  , IBCFile -> Maybe FC
ibc_parsedSpan             :: !(Maybe FC)
  , IBCFile -> [(Name, Int)]
ibc_usage                  :: ![(Name, Int)]
  , IBCFile -> [Name]
ibc_exports                :: ![Name]
  , IBCFile -> [(Name, Name)]
ibc_autohints              :: ![(Name, Name)]
  , IBCFile -> [(Name, String)]
ibc_deprecated             :: ![(Name, String)]
  , IBCFile -> [(Name, Def)]
ibc_defs                   :: ![(Name, Def)]
  , IBCFile -> [(Name, Totality)]
ibc_total                  :: ![(Name, Totality)]
  , IBCFile -> [(Name, Bool)]
ibc_injective              :: ![(Name, Injectivity)]
  , IBCFile -> [(Name, Accessibility)]
ibc_access                 :: ![(Name, Accessibility)]
  , IBCFile -> [(Name, String)]
ibc_fragile                :: ![(Name, String)]
  , IBCFile -> [(FC, UConstraint)]
ibc_constraints            :: ![(FC, UConstraint)]
  , IBCFile -> [LanguageExt]
ibc_langexts               :: ![LanguageExt]
  , IBCFile -> [(String, Int)]
ibc_importhashes           :: ![(FilePath, Int)]
  }
  deriving Int -> IBCFile -> ShowS
[IBCFile] -> ShowS
IBCFile -> String
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
showList :: [IBCFile] -> ShowS
$cshowList :: [IBCFile] -> ShowS
show :: IBCFile -> String
$cshow :: IBCFile -> String
showsPrec :: Int -> IBCFile -> ShowS
$cshowsPrec :: Int -> IBCFile -> ShowS
Show
{-!
deriving instance Binary IBCFile
!-}

initIBC :: IBCFile
initIBC :: IBCFile
initIBC = Word16
-> Int
-> String
-> [(Bool, String)]
-> [String]
-> [String]
-> [(Name, [PArg])]
-> [FixDecl]
-> [(Name, [Bool])]
-> [(Name, InterfaceInfo)]
-> [(Name, RecordInfo)]
-> [(Bool, Bool, Name, Name)]
-> [(Name, DSL)]
-> [(Name, TypeInfo)]
-> [(Name, OptInfo)]
-> [Syntax]
-> [String]
-> [(Codegen, String)]
-> [(Codegen, String)]
-> [(Codegen, String)]
-> [String]
-> [(Codegen, String)]
-> [(FC, String)]
-> [(Name, FnOpts)]
-> [(Name, FnInfo)]
-> [(Name, CGInfo)]
-> [(Name, (Docstring DocTerm, [(Name, Docstring DocTerm)]))]
-> [(Name, Docstring DocTerm)]
-> [(Name, (TT Name, TT Name))]
-> [(TT Name, TT Name)]
-> [Name]
-> [Name]
-> [(String, Int, PTerm)]
-> [(Name, Name)]
-> [(Name, MetaInformation)]
-> [Name]
-> [(Name, Name, Name)]
-> [(Name, (Maybe Name, Int, [Name], Bool, Bool))]
-> [(Name, ([([(Name, TT Name)], TT Name, TT Name)], [PTerm]))]
-> [Name]
-> [(Name, Int)]
-> Maybe FC
-> [(Name, Int)]
-> [Name]
-> [(Name, Name)]
-> [(Name, String)]
-> [(Name, Def)]
-> [(Name, Totality)]
-> [(Name, Bool)]
-> [(Name, Accessibility)]
-> [(Name, String)]
-> [(FC, UConstraint)]
-> [LanguageExt]
-> [(String, Int)]
-> IBCFile
IBCFile Word16
ibcVersion Int
0 String
"" [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] forall a. Maybe a
Nothing [] [] [] [] [] [] [] [] [] [] [] []

hasValidIBCVersion :: FilePath -> Idris Bool
hasValidIBCVersion :: String -> Idris Bool
hasValidIBCVersion String
fp = do
  ByteString
archiveFile <- forall a. IO a -> Idris a
runIO forall a b. (a -> b) -> a -> b
$ String -> IO ByteString
B.readFile String
fp
  case ByteString -> Either String Archive
toArchiveOrFail ByteString
archiveFile of
    Left String
_ -> forall (m :: * -> *) a. Monad m => a -> m a
return Bool
False
    Right Archive
archive -> do Word16
ver <- forall b. (Binary b, NFData b) => b -> String -> Archive -> Idris b
getEntry Word16
0 String
"ver" Archive
archive
                        forall (m :: * -> *) a. Monad m => a -> m a
return (Word16
ver forall a. Eq a => a -> a -> Bool
== Word16
ibcVersion)


loadIBC :: Bool -- ^ True = reexport, False = make everything private
        -> IBCPhase
        -> FilePath -> Idris ()
loadIBC :: Bool -> IBCPhase -> String -> Idris ()
loadIBC Bool
reexport IBCPhase
phase String
fp
           = do Int -> String -> Idris ()
logIBC Int
1 forall a b. (a -> b) -> a -> b
$ String
"loadIBC (reexport, phase, fp)" forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> String
show (Bool
reexport, IBCPhase
phase, String
fp)
                [(String, Bool)]
imps <- Idris [(String, Bool)]
getImported
                Int -> String -> Idris ()
logIBC Int
3 forall a b. (a -> b) -> a -> b
$ String
"loadIBC imps" forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> String
show [(String, Bool)]
imps
                case forall a b. Eq a => a -> [(a, b)] -> Maybe b
lookup String
fp [(String, Bool)]
imps of
                    Maybe Bool
Nothing -> Bool -> Idris ()
load Bool
True
                    Just Bool
p -> if (Bool -> Bool
not Bool
p Bool -> Bool -> Bool
&& Bool
reexport) then Bool -> Idris ()
load Bool
False else forall (m :: * -> *) a. Monad m => a -> m a
return ()
        where
            load :: Bool -> Idris ()
load Bool
fullLoad = do
                    Int -> String -> Idris ()
logIBC Int
1 forall a b. (a -> b) -> a -> b
$ String
"Loading ibc " forall a. [a] -> [a] -> [a]
++ String
fp forall a. [a] -> [a] -> [a]
++ String
" " forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> String
show Bool
reexport
                    ByteString
archiveFile <- forall a. IO a -> Idris a
runIO forall a b. (a -> b) -> a -> b
$ String -> IO ByteString
B.readFile String
fp
                    case ByteString -> Either String Archive
toArchiveOrFail ByteString
archiveFile of
                        Left String
_ -> do
                            forall a. String -> Idris a
ifail forall a b. (a -> b) -> a -> b
$ String
fp  forall a. [a] -> [a] -> [a]
++ String
" isn't loadable, it may have an old ibc format.\n"
                                        forall a. [a] -> [a] -> [a]
++ String
"Please clean and rebuild it."
                        Right Archive
archive -> do
                            if Bool
fullLoad
                                then Bool -> IBCPhase -> Archive -> String -> Idris ()
process Bool
reexport IBCPhase
phase Archive
archive String
fp
                                else IBCPhase -> String -> Archive -> Idris ()
unhide IBCPhase
phase String
fp Archive
archive
                            Bool -> String -> Idris ()
addImported Bool
reexport String
fp

getIBCHash :: FilePath -> Idris Int
getIBCHash :: String -> Idris Int
getIBCHash String
fp
    = do ByteString
archiveFile <- forall a. IO a -> Idris a
runIO forall a b. (a -> b) -> a -> b
$ String -> IO ByteString
B.readFile String
fp
         case ByteString -> Either String Archive
toArchiveOrFail ByteString
archiveFile of
              Left String
_ -> forall (m :: * -> *) a. Monad m => a -> m a
return Int
0
              Right Archive
archive -> forall b. (Binary b, NFData b) => b -> String -> Archive -> Idris b
getEntry Int
0 String
"iface_hash" Archive
archive


getImportHashes :: FilePath -> Idris [(FilePath, Int)]
getImportHashes :: String -> Idris [(String, Int)]
getImportHashes String
fp
    = do ByteString
archiveFile <- forall a. IO a -> Idris a
runIO forall a b. (a -> b) -> a -> b
$ String -> IO ByteString
B.readFile String
fp
         case ByteString -> Either String Archive
toArchiveOrFail ByteString
archiveFile of
              Left String
_ -> forall (m :: * -> *) a. Monad m => a -> m a
return []
              Right Archive
archive -> forall b. (Binary b, NFData b) => b -> String -> Archive -> Idris b
getEntry [] String
"ibc_importhashes" Archive
archive

-- | Load an entire package from its index file
loadPkgIndex :: PkgName -> Idris ()
loadPkgIndex :: PkgName -> Idris ()
loadPkgIndex PkgName
pkg = do String
ddir <- forall a. IO a -> Idris a
runIO IO String
getIdrisLibDir
                      String -> Idris ()
addImportDir (String
ddir String -> ShowS
</> PkgName -> String
unPkgName PkgName
pkg)
                      String
fp <- PkgName -> Idris String
findPkgIndex PkgName
pkg
                      Bool -> IBCPhase -> String -> Idris ()
loadIBC Bool
True IBCPhase
IBC_Building String
fp


makeEntry :: (Binary b) => String -> [b] -> Maybe Entry
makeEntry :: forall b. Binary b => String -> [b] -> Maybe Entry
makeEntry String
name [b]
val = if forall (t :: * -> *) a. Foldable t => t a -> Bool
L.null [b]
val
                        then forall a. Maybe a
Nothing
                        else forall a. a -> Maybe a
Just forall a b. (a -> b) -> a -> b
$ String -> Integer -> ByteString -> Entry
toEntry String
name Integer
0 (forall a. Binary a => a -> ByteString
encode [b]
val)


entries :: IBCFile -> [Entry]
entries :: IBCFile -> [Entry]
entries IBCFile
i = forall a. [Maybe a] -> [a]
catMaybes [forall a. a -> Maybe a
Just forall a b. (a -> b) -> a -> b
$ String -> Integer -> ByteString -> Entry
toEntry String
"ver" Integer
0 (forall a. Binary a => a -> ByteString
encode forall a b. (a -> b) -> a -> b
$ IBCFile -> Word16
ver IBCFile
i),
                       forall a. a -> Maybe a
Just forall a b. (a -> b) -> a -> b
$ String -> Integer -> ByteString -> Entry
toEntry String
"iface_hash" Integer
0 (forall a. Binary a => a -> ByteString
encode forall a b. (a -> b) -> a -> b
$ IBCFile -> Int
iface_hash IBCFile
i),
                       forall b. Binary b => String -> [b] -> Maybe Entry
makeEntry String
"sourcefile"  (IBCFile -> String
sourcefile IBCFile
i),
                       forall b. Binary b => String -> [b] -> Maybe Entry
makeEntry String
"ibc_imports"  (IBCFile -> [(Bool, String)]
ibc_imports IBCFile
i),
                       forall b. Binary b => String -> [b] -> Maybe Entry
makeEntry String
"ibc_importdirs"  (IBCFile -> [String]
ibc_importdirs IBCFile
i),
                       forall b. Binary b => String -> [b] -> Maybe Entry
makeEntry String
"ibc_sourcedirs"  (IBCFile -> [String]
ibc_sourcedirs IBCFile
i),
                       forall b. Binary b => String -> [b] -> Maybe Entry
makeEntry String
"ibc_implicits"  (IBCFile -> [(Name, [PArg])]
ibc_implicits IBCFile
i),
                       forall b. Binary b => String -> [b] -> Maybe Entry
makeEntry String
"ibc_fixes"  (IBCFile -> [FixDecl]
ibc_fixes IBCFile
i),
                       forall b. Binary b => String -> [b] -> Maybe Entry
makeEntry String
"ibc_statics"  (IBCFile -> [(Name, [Bool])]
ibc_statics IBCFile
i),
                       forall b. Binary b => String -> [b] -> Maybe Entry
makeEntry String
"ibc_interfaces"  (IBCFile -> [(Name, InterfaceInfo)]
ibc_interfaces IBCFile
i),
                       forall b. Binary b => String -> [b] -> Maybe Entry
makeEntry String
"ibc_records"  (IBCFile -> [(Name, RecordInfo)]
ibc_records IBCFile
i),
                       forall b. Binary b => String -> [b] -> Maybe Entry
makeEntry String
"ibc_implementations"  (IBCFile -> [(Bool, Bool, Name, Name)]
ibc_implementations IBCFile
i),
                       forall b. Binary b => String -> [b] -> Maybe Entry
makeEntry String
"ibc_dsls"  (IBCFile -> [(Name, DSL)]
ibc_dsls IBCFile
i),
                       forall b. Binary b => String -> [b] -> Maybe Entry
makeEntry String
"ibc_datatypes"  (IBCFile -> [(Name, TypeInfo)]
ibc_datatypes IBCFile
i),
                       forall b. Binary b => String -> [b] -> Maybe Entry
makeEntry String
"ibc_optimise"  (IBCFile -> [(Name, OptInfo)]
ibc_optimise IBCFile
i),
                       forall b. Binary b => String -> [b] -> Maybe Entry
makeEntry String
"ibc_syntax"  (IBCFile -> [Syntax]
ibc_syntax IBCFile
i),
                       forall b. Binary b => String -> [b] -> Maybe Entry
makeEntry String
"ibc_keywords"  (IBCFile -> [String]
ibc_keywords IBCFile
i),
                       forall b. Binary b => String -> [b] -> Maybe Entry
makeEntry String
"ibc_objs"  (IBCFile -> [(Codegen, String)]
ibc_objs IBCFile
i),
                       forall b. Binary b => String -> [b] -> Maybe Entry
makeEntry String
"ibc_libs"  (IBCFile -> [(Codegen, String)]
ibc_libs IBCFile
i),
                       forall b. Binary b => String -> [b] -> Maybe Entry
makeEntry String
"ibc_cgflags"  (IBCFile -> [(Codegen, String)]
ibc_cgflags IBCFile
i),
                       forall b. Binary b => String -> [b] -> Maybe Entry
makeEntry String
"ibc_dynamic_libs"  (IBCFile -> [String]
ibc_dynamic_libs IBCFile
i),
                       forall b. Binary b => String -> [b] -> Maybe Entry
makeEntry String
"ibc_hdrs"  (IBCFile -> [(Codegen, String)]
ibc_hdrs IBCFile
i),
                       forall b. Binary b => String -> [b] -> Maybe Entry
makeEntry String
"ibc_totcheckfail"  (IBCFile -> [(FC, String)]
ibc_totcheckfail IBCFile
i),
                       forall b. Binary b => String -> [b] -> Maybe Entry
makeEntry String
"ibc_flags"  (IBCFile -> [(Name, FnOpts)]
ibc_flags IBCFile
i),
                       forall b. Binary b => String -> [b] -> Maybe Entry
makeEntry String
"ibc_fninfo"  (IBCFile -> [(Name, FnInfo)]
ibc_fninfo IBCFile
i),
                       forall b. Binary b => String -> [b] -> Maybe Entry
makeEntry String
"ibc_cg"  (IBCFile -> [(Name, CGInfo)]
ibc_cg IBCFile
i),
                       forall b. Binary b => String -> [b] -> Maybe Entry
makeEntry String
"ibc_docstrings"  (IBCFile
-> [(Name, (Docstring DocTerm, [(Name, Docstring DocTerm)]))]
ibc_docstrings IBCFile
i),
                       forall b. Binary b => String -> [b] -> Maybe Entry
makeEntry String
"ibc_moduledocs"  (IBCFile -> [(Name, Docstring DocTerm)]
ibc_moduledocs IBCFile
i),
                       forall b. Binary b => String -> [b] -> Maybe Entry
makeEntry String
"ibc_transforms"  (IBCFile -> [(Name, (TT Name, TT Name))]
ibc_transforms IBCFile
i),
                       forall b. Binary b => String -> [b] -> Maybe Entry
makeEntry String
"ibc_errRev"  (IBCFile -> [(TT Name, TT Name)]
ibc_errRev IBCFile
i),
                       forall b. Binary b => String -> [b] -> Maybe Entry
makeEntry String
"ibc_errReduce"  (IBCFile -> [Name]
ibc_errReduce IBCFile
i),
                       forall b. Binary b => String -> [b] -> Maybe Entry
makeEntry String
"ibc_coercions"  (IBCFile -> [Name]
ibc_coercions IBCFile
i),
                       forall b. Binary b => String -> [b] -> Maybe Entry
makeEntry String
"ibc_lineapps"  (IBCFile -> [(String, Int, PTerm)]
ibc_lineapps IBCFile
i),
                       forall b. Binary b => String -> [b] -> Maybe Entry
makeEntry String
"ibc_namehints"  (IBCFile -> [(Name, Name)]
ibc_namehints IBCFile
i),
                       forall b. Binary b => String -> [b] -> Maybe Entry
makeEntry String
"ibc_metainformation"  (IBCFile -> [(Name, MetaInformation)]
ibc_metainformation IBCFile
i),
                       forall b. Binary b => String -> [b] -> Maybe Entry
makeEntry String
"ibc_errorhandlers"  (IBCFile -> [Name]
ibc_errorhandlers IBCFile
i),
                       forall b. Binary b => String -> [b] -> Maybe Entry
makeEntry String
"ibc_function_errorhandlers"  (IBCFile -> [(Name, Name, Name)]
ibc_function_errorhandlers IBCFile
i),
                       forall b. Binary b => String -> [b] -> Maybe Entry
makeEntry String
"ibc_metavars"  (IBCFile -> [(Name, (Maybe Name, Int, [Name], Bool, Bool))]
ibc_metavars IBCFile
i),
                       forall b. Binary b => String -> [b] -> Maybe Entry
makeEntry String
"ibc_patdefs"  (IBCFile
-> [(Name, ([([(Name, TT Name)], TT Name, TT Name)], [PTerm]))]
ibc_patdefs IBCFile
i),
                       forall b. Binary b => String -> [b] -> Maybe Entry
makeEntry String
"ibc_postulates"  (IBCFile -> [Name]
ibc_postulates IBCFile
i),
                       forall b. Binary b => String -> [b] -> Maybe Entry
makeEntry String
"ibc_externs"  (IBCFile -> [(Name, Int)]
ibc_externs IBCFile
i),
                       String -> Integer -> ByteString -> Entry
toEntry String
"ibc_parsedSpan" Integer
0 forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a. Binary a => a -> ByteString
encode forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> IBCFile -> Maybe FC
ibc_parsedSpan IBCFile
i,
                       forall b. Binary b => String -> [b] -> Maybe Entry
makeEntry String
"ibc_usage"  (IBCFile -> [(Name, Int)]
ibc_usage IBCFile
i),
                       forall b. Binary b => String -> [b] -> Maybe Entry
makeEntry String
"ibc_exports"  (IBCFile -> [Name]
ibc_exports IBCFile
i),
                       forall b. Binary b => String -> [b] -> Maybe Entry
makeEntry String
"ibc_autohints"  (IBCFile -> [(Name, Name)]
ibc_autohints IBCFile
i),
                       forall b. Binary b => String -> [b] -> Maybe Entry
makeEntry String
"ibc_deprecated"  (IBCFile -> [(Name, String)]
ibc_deprecated IBCFile
i),
                       forall b. Binary b => String -> [b] -> Maybe Entry
makeEntry String
"ibc_defs"  (IBCFile -> [(Name, Def)]
ibc_defs IBCFile
i),
                       forall b. Binary b => String -> [b] -> Maybe Entry
makeEntry String
"ibc_total"  (IBCFile -> [(Name, Totality)]
ibc_total IBCFile
i),
                       forall b. Binary b => String -> [b] -> Maybe Entry
makeEntry String
"ibc_injective"  (IBCFile -> [(Name, Bool)]
ibc_injective IBCFile
i),
                       forall b. Binary b => String -> [b] -> Maybe Entry
makeEntry String
"ibc_access"  (IBCFile -> [(Name, Accessibility)]
ibc_access IBCFile
i),
                       forall b. Binary b => String -> [b] -> Maybe Entry
makeEntry String
"ibc_fragile" (IBCFile -> [(Name, String)]
ibc_fragile IBCFile
i),
                       forall b. Binary b => String -> [b] -> Maybe Entry
makeEntry String
"ibc_langexts" (IBCFile -> [LanguageExt]
ibc_langexts IBCFile
i),
                       forall b. Binary b => String -> [b] -> Maybe Entry
makeEntry String
"ibc_importhashes" (IBCFile -> [(String, Int)]
ibc_importhashes IBCFile
i)]
-- TODO: Put this back in shortly after minimising/pruning constraints
--                        makeEntry "ibc_constraints" (ibc_constraints i)]

writeArchive :: FilePath -> IBCFile -> Idris ()
writeArchive :: String -> IBCFile -> Idris ()
writeArchive String
fp IBCFile
i = do let a :: Archive
a = forall (t :: * -> *) b a.
Foldable t =>
(b -> a -> b) -> b -> t a -> b
L.foldl (\Archive
x Entry
y -> Entry -> Archive -> Archive
addEntryToArchive Entry
y Archive
x) Archive
emptyArchive (IBCFile -> [Entry]
entries IBCFile
i)
                       forall a. IO a -> Idris a
runIO forall a b. (a -> b) -> a -> b
$ String -> ByteString -> IO ()
B.writeFile String
fp (Archive -> ByteString
fromArchive Archive
a)

writeIBC :: FilePath -> FilePath -> Idris ()
writeIBC :: String -> String -> Idris ()
writeIBC String
src String
f
    = do
         Int -> String -> Idris ()
logIBC  Int
2 forall a b. (a -> b) -> a -> b
$ String
"Writing IBC for: " forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> String
show String
f
         Int -> String -> Idris ()
iReport Int
2 forall a b. (a -> b) -> a -> b
$ String
"Writing IBC for: " forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> String
show String
f
         IState
i <- Idris IState
getIState
         Idris ()
resetNameIdx
         IBCFile
ibc_data <- [IBCWrite] -> IBCFile -> Idris IBCFile
mkIBC (IState -> [IBCWrite]
ibc_write IState
i) (IBCFile
initIBC { sourcefile :: String
sourcefile = String
src,
                                                    ibc_langexts :: [LanguageExt]
ibc_langexts = IState -> [LanguageExt]
idris_language_extensions IState
i })
         let ibcf :: IBCFile
ibcf = IBCFile
ibc_data { iface_hash :: Int
iface_hash = IState -> IBCFile -> Int
calculateHash IState
i IBCFile
ibc_data }
         Int -> String -> Idris ()
logIBC Int
5 forall a b. (a -> b) -> a -> b
$ String
"Hash for " forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> String
show String
f forall a. [a] -> [a] -> [a]
++ String
" = " forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> String
show (IBCFile -> Int
iface_hash IBCFile
ibcf)
         forall a. Idris a -> (Err -> Idris a) -> Idris a
idrisCatch (do forall a. IO a -> Idris a
runIO forall a b. (a -> b) -> a -> b
$ Bool -> String -> IO ()
createDirectoryIfMissing Bool
True (ShowS
dropFileName String
f)
                        String -> IBCFile -> Idris ()
writeArchive String
f IBCFile
ibcf
                        Int -> String -> Idris ()
logIBC Int
2 String
"Written")
            (\Err
c -> do Int -> String -> Idris ()
logIBC Int
2 forall a b. (a -> b) -> a -> b
$ String
"Failed " forall a. [a] -> [a] -> [a]
++ IState -> Err -> String
pshow IState
i Err
c)
         forall (m :: * -> *) a. Monad m => a -> m a
return ()

qhash :: Int -> String -> Int
qhash :: Int -> String -> Int
qhash Int
hash [] = forall a. Num a => a -> a
abs Int
hash forall a. Integral a => a -> a -> a
`mod` Int
0xffffffff
qhash Int
hash (Char
x:String
xs) = Int -> String -> Int
qhash (Int
hash forall a. Num a => a -> a -> a
* Int
33 forall a. Num a => a -> a -> a
+ forall a b. (Integral a, Num b) => a -> b
fromIntegral (forall a. Enum a => a -> Int
fromEnum Char
x)) String
xs

hashTerm :: Int -> Term -> Int
hashTerm :: Int -> TT Name -> Int
hashTerm Int
i TT Name
t = Int -> String -> Int
qhash (Int
i forall a. Num a => a -> a -> a
* Int
5381) (forall a. Show a => a -> String
show TT Name
t)

hashName :: Int -> Name -> Int
hashName :: Int -> Name -> Int
hashName Int
i Name
n = Int -> String -> Int
qhash (Int
i forall a. Num a => a -> a -> a
* Int
5381) (forall a. Show a => a -> String
show Name
n)

calculateHash :: IState -> IBCFile -> Int
calculateHash :: IState -> IBCFile -> Int
calculateHash IState
ist IBCFile
f
    = let acc :: [(Name, Accessibility)]
acc = forall a. (a -> Bool) -> [a] -> [a]
L.filter forall {a}. (a, Accessibility) -> Bool
exported (IBCFile -> [(Name, Accessibility)]
ibc_access IBCFile
f)
          inl :: [(Name, FnOpts)]
inl = forall a. (a -> Bool) -> [a] -> [a]
L.filter (forall {a} {t :: * -> *} {t :: * -> *}.
(Eq a, Foldable t, Foldable t) =>
t a -> (a, t FnOpt) -> Bool
inlinable (forall a b. (a -> b) -> [a] -> [b]
map forall a b. (a, b) -> a
fst [(Name, Accessibility)]
acc)) (IBCFile -> [(Name, FnOpts)]
ibc_flags IBCFile
f) in
          [Name] -> [TT Name] -> Int
mkHashFrom (forall a b. (a -> b) -> [a] -> [b]
map forall a b. (a, b) -> a
fst [(Name, Accessibility)]
acc) ([(Name, Accessibility)] -> [TT Name]
getDefs [(Name, Accessibility)]
acc forall a. [a] -> [a] -> [a]
++ forall (t :: * -> *) a b. Foldable t => (a -> [b]) -> t a -> [b]
L.concatMap (Name, FnOpts) -> [TT Name]
getFullDef [(Name, FnOpts)]
inl)
  where
    mkHashFrom :: [Name] -> [Term] -> Int
    mkHashFrom :: [Name] -> [TT Name] -> Int
mkHashFrom [Name]
ns [TT Name]
tms = forall (t :: * -> *) a. (Foldable t, Num a) => t a -> a
sum (forall a b c. (a -> b -> c) -> [a] -> [b] -> [c]
L.zipWith Int -> Name -> Int
hashName [Int
1..] [Name]
ns) forall a. Num a => a -> a -> a
+
                        forall (t :: * -> *) a. (Foldable t, Num a) => t a -> a
sum (forall a b c. (a -> b -> c) -> [a] -> [b] -> [c]
L.zipWith Int -> TT Name -> Int
hashTerm [Int
1..] [TT Name]
tms)

    exported :: (a, Accessibility) -> Bool
exported (a
_, Accessibility
Public) = Bool
True
    exported (a
_, Accessibility
Frozen) = Bool
True
    exported (a, Accessibility)
_ = Bool
False

    inlinable :: t a -> (a, t FnOpt) -> Bool
inlinable t a
acc (a
n, t FnOpt
opts)
        = a
n forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
`elem` t a
acc Bool -> Bool -> Bool
&&
             (FnOpt
Inlinable forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
`elem` t FnOpt
opts Bool -> Bool -> Bool
|| FnOpt
PEGenerated forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
`elem` t FnOpt
opts)

    findTms :: [(a, Term, Term)] -> [Term]
    findTms :: forall a. [(a, TT Name, TT Name)] -> [TT Name]
findTms = forall (t :: * -> *) a b. Foldable t => (a -> [b]) -> t a -> [b]
L.concatMap (\ (a
_, TT Name
x, TT Name
y) -> [TT Name
x, TT Name
y])

    patDef :: Name -> [Term]
    patDef :: Name -> [TT Name]
patDef Name
n
        = case forall a. Name -> Ctxt a -> Maybe a
lookupCtxtExact Name
n (IState -> Ctxt ([([(Name, TT Name)], TT Name, TT Name)], [PTerm])
idris_patdefs IState
ist) of
               Maybe ([([(Name, TT Name)], TT Name, TT Name)], [PTerm])
Nothing -> []
               Just ([([(Name, TT Name)], TT Name, TT Name)]
tms, [PTerm]
_) -> forall a. [(a, TT Name, TT Name)] -> [TT Name]
findTms [([(Name, TT Name)], TT Name, TT Name)]
tms

    getDefs :: [(Name, Accessibility)] -> [Term]
    getDefs :: [(Name, Accessibility)] -> [TT Name]
getDefs [] = []
    getDefs ((Name
n, Accessibility
Public) : [(Name, Accessibility)]
ns)
        = let ts :: [TT Name]
ts = [(Name, Accessibility)] -> [TT Name]
getDefs [(Name, Accessibility)]
ns in
              case Name -> Context -> Maybe (TT Name)
lookupTyExact Name
n (IState -> Context
tt_ctxt IState
ist) of
                   Maybe (TT Name)
Nothing -> [TT Name]
ts
                   Just TT Name
ty -> TT Name
ty forall a. a -> [a] -> [a]
: Name -> [TT Name]
patDef Name
n forall a. [a] -> [a] -> [a]
++ [TT Name]
ts
    getDefs ((Name
n, Accessibility
Frozen) : [(Name, Accessibility)]
ns)
        = let ts :: [TT Name]
ts = [(Name, Accessibility)] -> [TT Name]
getDefs [(Name, Accessibility)]
ns in
              case Name -> Context -> Maybe (TT Name)
lookupTyExact Name
n (IState -> Context
tt_ctxt IState
ist) of
                   Maybe (TT Name)
Nothing -> [TT Name]
ts
                   Just TT Name
ty -> TT Name
ty forall a. a -> [a] -> [a]
: [TT Name]
ts
    getDefs ((Name, Accessibility)
_ : [(Name, Accessibility)]
ns) = [(Name, Accessibility)] -> [TT Name]
getDefs [(Name, Accessibility)]
ns

    getFullDef :: (Name, [FnOpt]) -> [Term]
    getFullDef :: (Name, FnOpts) -> [TT Name]
getFullDef (Name
n, FnOpts
_)
        = case Name -> Context -> Maybe (TT Name)
lookupTyExact Name
n (IState -> Context
tt_ctxt IState
ist) of
               Maybe (TT Name)
Nothing -> []
               Just TT Name
ty -> TT Name
ty forall a. a -> [a] -> [a]
: Name -> [TT Name]
patDef Name
n

-- | Write a package index containing all the imports in the current
-- IState Used for ':search' of an entire package, to ensure
-- everything is loaded.
writePkgIndex :: FilePath -> Idris ()
writePkgIndex :: String -> Idris ()
writePkgIndex String
f
    = do IState
i <- Idris IState
getIState
         let imps :: [(Bool, String)]
imps = forall a b. (a -> b) -> [a] -> [b]
map (\ (String
x, Bool
y) -> (Bool
True, String
x)) forall a b. (a -> b) -> a -> b
$ IState -> [(String, Bool)]
idris_imported IState
i
         Int -> String -> Idris ()
logIBC Int
2 forall a b. (a -> b) -> a -> b
$ String
"Writing package index " forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> String
show String
f forall a. [a] -> [a] -> [a]
++ String
" including\n" forall a. [a] -> [a] -> [a]
++
                forall a. Show a => a -> String
show (forall a b. (a -> b) -> [a] -> [b]
map forall a b. (a, b) -> b
snd [(Bool, String)]
imps)
         Idris ()
resetNameIdx
         let ibcf :: IBCFile
ibcf = IBCFile
initIBC { ibc_imports :: [(Bool, String)]
ibc_imports = [(Bool, String)]
imps,
                              ibc_langexts :: [LanguageExt]
ibc_langexts = IState -> [LanguageExt]
idris_language_extensions IState
i }
         forall a. Idris a -> (Err -> Idris a) -> Idris a
idrisCatch (do forall a. IO a -> Idris a
runIO forall a b. (a -> b) -> a -> b
$ Bool -> String -> IO ()
createDirectoryIfMissing Bool
True (ShowS
dropFileName String
f)
                        String -> IBCFile -> Idris ()
writeArchive String
f IBCFile
ibcf
                        Int -> String -> Idris ()
logIBC Int
2 String
"Written")
            (\Err
c -> do Int -> String -> Idris ()
logIBC Int
2 forall a b. (a -> b) -> a -> b
$ String
"Failed " forall a. [a] -> [a] -> [a]
++ IState -> Err -> String
pshow IState
i Err
c)
         forall (m :: * -> *) a. Monad m => a -> m a
return ()

mkIBC :: [IBCWrite] -> IBCFile -> Idris IBCFile
mkIBC :: [IBCWrite] -> IBCFile -> Idris IBCFile
mkIBC [] IBCFile
f = forall (m :: * -> *) a. Monad m => a -> m a
return IBCFile
f
mkIBC (IBCWrite
i:[IBCWrite]
is) IBCFile
f = do IState
ist <- Idris IState
getIState
                    Int -> String -> Idris ()
logIBC Int
5 forall a b. (a -> b) -> a -> b
$ forall a. Show a => a -> String
show IBCWrite
i forall a. [a] -> [a] -> [a]
++ String
" " forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> String
show (forall (t :: * -> *) a. Foldable t => t a -> Int
L.length [IBCWrite]
is)
                    IBCFile
f' <- IState -> IBCWrite -> IBCFile -> Idris IBCFile
ibc IState
ist IBCWrite
i IBCFile
f
                    [IBCWrite] -> IBCFile -> Idris IBCFile
mkIBC [IBCWrite]
is IBCFile
f'

ibc :: IState -> IBCWrite -> IBCFile -> Idris IBCFile
ibc :: IState -> IBCWrite -> IBCFile -> Idris IBCFile
ibc IState
i (IBCFix FixDecl
d) IBCFile
f = forall (m :: * -> *) a. Monad m => a -> m a
return IBCFile
f { ibc_fixes :: [FixDecl]
ibc_fixes = FixDecl
d forall a. a -> [a] -> [a]
: IBCFile -> [FixDecl]
ibc_fixes IBCFile
f }
ibc IState
i (IBCImp Name
n) IBCFile
f = case forall a. Name -> Ctxt a -> Maybe a
lookupCtxtExact Name
n (IState -> Ctxt [PArg]
idris_implicits IState
i) of
                        Just [PArg]
v -> forall (m :: * -> *) a. Monad m => a -> m a
return IBCFile
f { ibc_implicits :: [(Name, [PArg])]
ibc_implicits = (Name
n,[PArg]
v)forall a. a -> [a] -> [a]
: IBCFile -> [(Name, [PArg])]
ibc_implicits IBCFile
f     }
                        Maybe [PArg]
_ -> forall a. String -> Idris a
ifail String
"IBC write failed"
ibc IState
i (IBCStatic Name
n) IBCFile
f
                   = case forall a. Name -> Ctxt a -> Maybe a
lookupCtxtExact Name
n (IState -> Ctxt [Bool]
idris_statics IState
i) of
                        Just [Bool]
v -> forall (m :: * -> *) a. Monad m => a -> m a
return IBCFile
f { ibc_statics :: [(Name, [Bool])]
ibc_statics = (Name
n,[Bool]
v)forall a. a -> [a] -> [a]
: IBCFile -> [(Name, [Bool])]
ibc_statics IBCFile
f     }
                        Maybe [Bool]
_ -> forall a. String -> Idris a
ifail String
"IBC write failed"
ibc IState
i (IBCInterface Name
n) IBCFile
f
                   = case forall a. Name -> Ctxt a -> Maybe a
lookupCtxtExact Name
n (IState -> Ctxt InterfaceInfo
idris_interfaces IState
i) of
                        Just InterfaceInfo
v -> forall (m :: * -> *) a. Monad m => a -> m a
return IBCFile
f { ibc_interfaces :: [(Name, InterfaceInfo)]
ibc_interfaces = (Name
n,InterfaceInfo
v)forall a. a -> [a] -> [a]
: IBCFile -> [(Name, InterfaceInfo)]
ibc_interfaces IBCFile
f     }
                        Maybe InterfaceInfo
_ -> forall a. String -> Idris a
ifail String
"IBC write failed"
ibc IState
i (IBCRecord Name
n) IBCFile
f
                   = case forall a. Name -> Ctxt a -> Maybe a
lookupCtxtExact Name
n (IState -> Ctxt RecordInfo
idris_records IState
i) of
                        Just RecordInfo
v -> forall (m :: * -> *) a. Monad m => a -> m a
return IBCFile
f { ibc_records :: [(Name, RecordInfo)]
ibc_records = (Name
n,RecordInfo
v)forall a. a -> [a] -> [a]
: IBCFile -> [(Name, RecordInfo)]
ibc_records IBCFile
f     }
                        Maybe RecordInfo
_ -> forall a. String -> Idris a
ifail String
"IBC write failed"
ibc IState
i (IBCImplementation Bool
int Bool
res Name
n Name
ins) IBCFile
f
                   = forall (m :: * -> *) a. Monad m => a -> m a
return IBCFile
f { ibc_implementations :: [(Bool, Bool, Name, Name)]
ibc_implementations = (Bool
int, Bool
res, Name
n, Name
ins) forall a. a -> [a] -> [a]
: IBCFile -> [(Bool, Bool, Name, Name)]
ibc_implementations IBCFile
f }
ibc IState
i (IBCDSL Name
n) IBCFile
f
                   = case forall a. Name -> Ctxt a -> Maybe a
lookupCtxtExact Name
n (IState -> Ctxt DSL
idris_dsls IState
i) of
                        Just DSL
v -> forall (m :: * -> *) a. Monad m => a -> m a
return IBCFile
f { ibc_dsls :: [(Name, DSL)]
ibc_dsls = (Name
n,DSL
v)forall a. a -> [a] -> [a]
: IBCFile -> [(Name, DSL)]
ibc_dsls IBCFile
f     }
                        Maybe DSL
_ -> forall a. String -> Idris a
ifail String
"IBC write failed"
ibc IState
i (IBCData Name
n) IBCFile
f
                   = case forall a. Name -> Ctxt a -> Maybe a
lookupCtxtExact Name
n (IState -> Ctxt TypeInfo
idris_datatypes IState
i) of
                        Just TypeInfo
v -> forall (m :: * -> *) a. Monad m => a -> m a
return IBCFile
f { ibc_datatypes :: [(Name, TypeInfo)]
ibc_datatypes = (Name
n,TypeInfo
v)forall a. a -> [a] -> [a]
: IBCFile -> [(Name, TypeInfo)]
ibc_datatypes IBCFile
f     }
                        Maybe TypeInfo
_ -> forall a. String -> Idris a
ifail String
"IBC write failed"
ibc IState
i (IBCOpt Name
n) IBCFile
f = case forall a. Name -> Ctxt a -> Maybe a
lookupCtxtExact Name
n (IState -> Ctxt OptInfo
idris_optimisation IState
i) of
                        Just OptInfo
v -> forall (m :: * -> *) a. Monad m => a -> m a
return IBCFile
f { ibc_optimise :: [(Name, OptInfo)]
ibc_optimise = (Name
n,OptInfo
v)forall a. a -> [a] -> [a]
: IBCFile -> [(Name, OptInfo)]
ibc_optimise IBCFile
f     }
                        Maybe OptInfo
_ -> forall a. String -> Idris a
ifail String
"IBC write failed"
ibc IState
i (IBCSyntax Syntax
n) IBCFile
f = forall (m :: * -> *) a. Monad m => a -> m a
return IBCFile
f { ibc_syntax :: [Syntax]
ibc_syntax = Syntax
n forall a. a -> [a] -> [a]
: IBCFile -> [Syntax]
ibc_syntax IBCFile
f }
ibc IState
i (IBCKeyword String
n) IBCFile
f = forall (m :: * -> *) a. Monad m => a -> m a
return IBCFile
f { ibc_keywords :: [String]
ibc_keywords = String
n forall a. a -> [a] -> [a]
: IBCFile -> [String]
ibc_keywords IBCFile
f }
ibc IState
i (IBCImport (Bool, String)
n) IBCFile
f = forall (m :: * -> *) a. Monad m => a -> m a
return IBCFile
f { ibc_imports :: [(Bool, String)]
ibc_imports = (Bool, String)
n forall a. a -> [a] -> [a]
: IBCFile -> [(Bool, String)]
ibc_imports IBCFile
f }
ibc IState
i (IBCImportDir String
n) IBCFile
f = forall (m :: * -> *) a. Monad m => a -> m a
return IBCFile
f { ibc_importdirs :: [String]
ibc_importdirs = String
n forall a. a -> [a] -> [a]
: IBCFile -> [String]
ibc_importdirs IBCFile
f }
ibc IState
i (IBCSourceDir String
n) IBCFile
f = forall (m :: * -> *) a. Monad m => a -> m a
return IBCFile
f { ibc_sourcedirs :: [String]
ibc_sourcedirs = String
n forall a. a -> [a] -> [a]
: IBCFile -> [String]
ibc_sourcedirs IBCFile
f }
ibc IState
i (IBCObj Codegen
tgt String
n) IBCFile
f = forall (m :: * -> *) a. Monad m => a -> m a
return IBCFile
f { ibc_objs :: [(Codegen, String)]
ibc_objs = (Codegen
tgt, String
n) forall a. a -> [a] -> [a]
: IBCFile -> [(Codegen, String)]
ibc_objs IBCFile
f }
ibc IState
i (IBCLib Codegen
tgt String
n) IBCFile
f = forall (m :: * -> *) a. Monad m => a -> m a
return IBCFile
f { ibc_libs :: [(Codegen, String)]
ibc_libs = (Codegen
tgt, String
n) forall a. a -> [a] -> [a]
: IBCFile -> [(Codegen, String)]
ibc_libs IBCFile
f }
ibc IState
i (IBCCGFlag Codegen
tgt String
n) IBCFile
f = forall (m :: * -> *) a. Monad m => a -> m a
return IBCFile
f { ibc_cgflags :: [(Codegen, String)]
ibc_cgflags = (Codegen
tgt, String
n) forall a. a -> [a] -> [a]
: IBCFile -> [(Codegen, String)]
ibc_cgflags IBCFile
f }
ibc IState
i (IBCDyLib String
n) IBCFile
f = forall (m :: * -> *) a. Monad m => a -> m a
return IBCFile
f {ibc_dynamic_libs :: [String]
ibc_dynamic_libs = String
n forall a. a -> [a] -> [a]
: IBCFile -> [String]
ibc_dynamic_libs IBCFile
f }
ibc IState
i (IBCHeader Codegen
tgt String
n) IBCFile
f = forall (m :: * -> *) a. Monad m => a -> m a
return IBCFile
f { ibc_hdrs :: [(Codegen, String)]
ibc_hdrs = (Codegen
tgt, String
n) forall a. a -> [a] -> [a]
: IBCFile -> [(Codegen, String)]
ibc_hdrs IBCFile
f }
ibc IState
i (IBCDef Name
n) IBCFile
f
   = do IBCFile
f' <- case Name -> Context -> Maybe Def
lookupDefExact Name
n (IState -> Context
tt_ctxt IState
i) of
                   Just Def
v -> forall (m :: * -> *) a. Monad m => a -> m a
return IBCFile
f { ibc_defs :: [(Name, Def)]
ibc_defs = (Name
n,Def
v) forall a. a -> [a] -> [a]
: IBCFile -> [(Name, Def)]
ibc_defs IBCFile
f }
                   Maybe Def
_ -> forall a. String -> Idris a
ifail String
"IBC write failed"
        case forall a. Name -> Ctxt a -> Maybe a
lookupCtxtExact Name
n (IState -> Ctxt ([([(Name, TT Name)], TT Name, TT Name)], [PTerm])
idris_patdefs IState
i) of
                   Just ([([(Name, TT Name)], TT Name, TT Name)], [PTerm])
v -> forall (m :: * -> *) a. Monad m => a -> m a
return IBCFile
f' { ibc_patdefs :: [(Name, ([([(Name, TT Name)], TT Name, TT Name)], [PTerm]))]
ibc_patdefs = (Name
n,([([(Name, TT Name)], TT Name, TT Name)], [PTerm])
v) forall a. a -> [a] -> [a]
: IBCFile
-> [(Name, ([([(Name, TT Name)], TT Name, TT Name)], [PTerm]))]
ibc_patdefs IBCFile
f }
                   Maybe ([([(Name, TT Name)], TT Name, TT Name)], [PTerm])
_ -> forall (m :: * -> *) a. Monad m => a -> m a
return IBCFile
f' -- Not a pattern definition

ibc IState
i (IBCDoc Name
n) IBCFile
f = case forall a. Name -> Ctxt a -> Maybe a
lookupCtxtExact Name
n (IState -> Ctxt (Docstring DocTerm, [(Name, Docstring DocTerm)])
idris_docstrings IState
i) of
                        Just (Docstring DocTerm, [(Name, Docstring DocTerm)])
v -> forall (m :: * -> *) a. Monad m => a -> m a
return IBCFile
f { ibc_docstrings :: [(Name, (Docstring DocTerm, [(Name, Docstring DocTerm)]))]
ibc_docstrings = (Name
n,(Docstring DocTerm, [(Name, Docstring DocTerm)])
v) forall a. a -> [a] -> [a]
: IBCFile
-> [(Name, (Docstring DocTerm, [(Name, Docstring DocTerm)]))]
ibc_docstrings IBCFile
f }
                        Maybe (Docstring DocTerm, [(Name, Docstring DocTerm)])
_ -> forall a. String -> Idris a
ifail String
"IBC write failed"
ibc IState
i (IBCCG Name
n) IBCFile
f = case forall a. Name -> Ctxt a -> Maybe a
lookupCtxtExact Name
n (IState -> Ctxt CGInfo
idris_callgraph IState
i) of
                        Just CGInfo
v -> forall (m :: * -> *) a. Monad m => a -> m a
return IBCFile
f { ibc_cg :: [(Name, CGInfo)]
ibc_cg = (Name
n,CGInfo
v) forall a. a -> [a] -> [a]
: IBCFile -> [(Name, CGInfo)]
ibc_cg IBCFile
f     }
                        Maybe CGInfo
_ -> forall a. String -> Idris a
ifail String
"IBC write failed"
ibc IState
i (IBCCoercion Name
n) IBCFile
f = forall (m :: * -> *) a. Monad m => a -> m a
return IBCFile
f { ibc_coercions :: [Name]
ibc_coercions = Name
n forall a. a -> [a] -> [a]
: IBCFile -> [Name]
ibc_coercions IBCFile
f }
ibc IState
i (IBCAccess Name
n Accessibility
a) IBCFile
f = forall (m :: * -> *) a. Monad m => a -> m a
return IBCFile
f { ibc_access :: [(Name, Accessibility)]
ibc_access = (Name
n,Accessibility
a) forall a. a -> [a] -> [a]
: IBCFile -> [(Name, Accessibility)]
ibc_access IBCFile
f }
ibc IState
i (IBCFlags Name
n) IBCFile
f
    = case forall a. Name -> Ctxt a -> Maybe a
lookupCtxtExact Name
n (IState -> Ctxt FnOpts
idris_flags IState
i) of
           Just FnOpts
a -> forall (m :: * -> *) a. Monad m => a -> m a
return IBCFile
f { ibc_flags :: [(Name, FnOpts)]
ibc_flags = (Name
n,FnOpts
a)forall a. a -> [a] -> [a]
: IBCFile -> [(Name, FnOpts)]
ibc_flags IBCFile
f }
           Maybe FnOpts
_ -> forall a. String -> Idris a
ifail String
"IBC write failed"
ibc IState
i (IBCFnInfo Name
n FnInfo
a) IBCFile
f = forall (m :: * -> *) a. Monad m => a -> m a
return IBCFile
f { ibc_fninfo :: [(Name, FnInfo)]
ibc_fninfo = (Name
n,FnInfo
a) forall a. a -> [a] -> [a]
: IBCFile -> [(Name, FnInfo)]
ibc_fninfo IBCFile
f }
ibc IState
i (IBCTotal Name
n Totality
a) IBCFile
f = forall (m :: * -> *) a. Monad m => a -> m a
return IBCFile
f { ibc_total :: [(Name, Totality)]
ibc_total = (Name
n,Totality
a) forall a. a -> [a] -> [a]
: IBCFile -> [(Name, Totality)]
ibc_total IBCFile
f }
ibc IState
i (IBCInjective Name
n Bool
a) IBCFile
f = forall (m :: * -> *) a. Monad m => a -> m a
return IBCFile
f { ibc_injective :: [(Name, Bool)]
ibc_injective = (Name
n,Bool
a) forall a. a -> [a] -> [a]
: IBCFile -> [(Name, Bool)]
ibc_injective IBCFile
f }
ibc IState
i (IBCTrans Name
n (TT Name, TT Name)
t) IBCFile
f = forall (m :: * -> *) a. Monad m => a -> m a
return IBCFile
f { ibc_transforms :: [(Name, (TT Name, TT Name))]
ibc_transforms = (Name
n, (TT Name, TT Name)
t) forall a. a -> [a] -> [a]
: IBCFile -> [(Name, (TT Name, TT Name))]
ibc_transforms IBCFile
f }
ibc IState
i (IBCErrRev (TT Name, TT Name)
t) IBCFile
f = forall (m :: * -> *) a. Monad m => a -> m a
return IBCFile
f { ibc_errRev :: [(TT Name, TT Name)]
ibc_errRev = (TT Name, TT Name)
t forall a. a -> [a] -> [a]
: IBCFile -> [(TT Name, TT Name)]
ibc_errRev IBCFile
f }
ibc IState
i (IBCErrReduce Name
t) IBCFile
f = forall (m :: * -> *) a. Monad m => a -> m a
return IBCFile
f { ibc_errReduce :: [Name]
ibc_errReduce = Name
t forall a. a -> [a] -> [a]
: IBCFile -> [Name]
ibc_errReduce IBCFile
f }
ibc IState
i (IBCLineApp String
fp Int
l PTerm
t) IBCFile
f
     = forall (m :: * -> *) a. Monad m => a -> m a
return IBCFile
f { ibc_lineapps :: [(String, Int, PTerm)]
ibc_lineapps = (String
fp,Int
l,PTerm
t) forall a. a -> [a] -> [a]
: IBCFile -> [(String, Int, PTerm)]
ibc_lineapps IBCFile
f }
ibc IState
i (IBCNameHint (Name
n, Name
ty)) IBCFile
f
     = forall (m :: * -> *) a. Monad m => a -> m a
return IBCFile
f { ibc_namehints :: [(Name, Name)]
ibc_namehints = (Name
n, Name
ty) forall a. a -> [a] -> [a]
: IBCFile -> [(Name, Name)]
ibc_namehints IBCFile
f }
ibc IState
i (IBCMetaInformation Name
n MetaInformation
m) IBCFile
f = forall (m :: * -> *) a. Monad m => a -> m a
return IBCFile
f { ibc_metainformation :: [(Name, MetaInformation)]
ibc_metainformation = (Name
n,MetaInformation
m) forall a. a -> [a] -> [a]
: IBCFile -> [(Name, MetaInformation)]
ibc_metainformation IBCFile
f }
ibc IState
i (IBCErrorHandler Name
n) IBCFile
f = forall (m :: * -> *) a. Monad m => a -> m a
return IBCFile
f { ibc_errorhandlers :: [Name]
ibc_errorhandlers = Name
n forall a. a -> [a] -> [a]
: IBCFile -> [Name]
ibc_errorhandlers IBCFile
f }
ibc IState
i (IBCFunctionErrorHandler Name
fn Name
a Name
n) IBCFile
f =
  forall (m :: * -> *) a. Monad m => a -> m a
return IBCFile
f { ibc_function_errorhandlers :: [(Name, Name, Name)]
ibc_function_errorhandlers = (Name
fn, Name
a, Name
n) forall a. a -> [a] -> [a]
: IBCFile -> [(Name, Name, Name)]
ibc_function_errorhandlers IBCFile
f }
ibc IState
i (IBCMetavar Name
n) IBCFile
f =
     case forall a b. Eq a => a -> [(a, b)] -> Maybe b
lookup Name
n (IState -> [(Name, (Maybe Name, Int, [Name], Bool, Bool))]
idris_metavars IState
i) of
          Maybe (Maybe Name, Int, [Name], Bool, Bool)
Nothing -> forall (m :: * -> *) a. Monad m => a -> m a
return IBCFile
f
          Just (Maybe Name, Int, [Name], Bool, Bool)
t -> forall (m :: * -> *) a. Monad m => a -> m a
return IBCFile
f { ibc_metavars :: [(Name, (Maybe Name, Int, [Name], Bool, Bool))]
ibc_metavars = (Name
n, (Maybe Name, Int, [Name], Bool, Bool)
t) forall a. a -> [a] -> [a]
: IBCFile -> [(Name, (Maybe Name, Int, [Name], Bool, Bool))]
ibc_metavars IBCFile
f }
ibc IState
i (IBCPostulate Name
n) IBCFile
f = forall (m :: * -> *) a. Monad m => a -> m a
return IBCFile
f { ibc_postulates :: [Name]
ibc_postulates = Name
n forall a. a -> [a] -> [a]
: IBCFile -> [Name]
ibc_postulates IBCFile
f }
ibc IState
i (IBCExtern (Name, Int)
n) IBCFile
f = forall (m :: * -> *) a. Monad m => a -> m a
return IBCFile
f { ibc_externs :: [(Name, Int)]
ibc_externs = (Name, Int)
n forall a. a -> [a] -> [a]
: IBCFile -> [(Name, Int)]
ibc_externs IBCFile
f }
ibc IState
i (IBCTotCheckErr FC
fc String
err) IBCFile
f = forall (m :: * -> *) a. Monad m => a -> m a
return IBCFile
f { ibc_totcheckfail :: [(FC, String)]
ibc_totcheckfail = (FC
fc, String
err) forall a. a -> [a] -> [a]
: IBCFile -> [(FC, String)]
ibc_totcheckfail IBCFile
f }
ibc IState
i (IBCParsedRegion FC
fc) IBCFile
f = forall (m :: * -> *) a. Monad m => a -> m a
return IBCFile
f { ibc_parsedSpan :: Maybe FC
ibc_parsedSpan = forall a. a -> Maybe a
Just FC
fc }
ibc IState
i (IBCModDocs Name
n) IBCFile
f = case forall a. Name -> Ctxt a -> Maybe a
lookupCtxtExact Name
n (IState -> Ctxt (Docstring DocTerm)
idris_moduledocs IState
i) of
                           Just Docstring DocTerm
v -> forall (m :: * -> *) a. Monad m => a -> m a
return IBCFile
f { ibc_moduledocs :: [(Name, Docstring DocTerm)]
ibc_moduledocs = (Name
n,Docstring DocTerm
v) forall a. a -> [a] -> [a]
: IBCFile -> [(Name, Docstring DocTerm)]
ibc_moduledocs IBCFile
f }
                           Maybe (Docstring DocTerm)
_ -> forall a. String -> Idris a
ifail String
"IBC write failed"
ibc IState
i (IBCUsage (Name, Int)
n) IBCFile
f = forall (m :: * -> *) a. Monad m => a -> m a
return IBCFile
f { ibc_usage :: [(Name, Int)]
ibc_usage = (Name, Int)
n forall a. a -> [a] -> [a]
: IBCFile -> [(Name, Int)]
ibc_usage IBCFile
f }
ibc IState
i (IBCExport Name
n) IBCFile
f = forall (m :: * -> *) a. Monad m => a -> m a
return IBCFile
f { ibc_exports :: [Name]
ibc_exports = Name
n forall a. a -> [a] -> [a]
: IBCFile -> [Name]
ibc_exports IBCFile
f }
ibc IState
i (IBCAutoHint Name
n Name
h) IBCFile
f = forall (m :: * -> *) a. Monad m => a -> m a
return IBCFile
f { ibc_autohints :: [(Name, Name)]
ibc_autohints = (Name
n, Name
h) forall a. a -> [a] -> [a]
: IBCFile -> [(Name, Name)]
ibc_autohints IBCFile
f }
ibc IState
i (IBCDeprecate Name
n String
r) IBCFile
f = forall (m :: * -> *) a. Monad m => a -> m a
return IBCFile
f { ibc_deprecated :: [(Name, String)]
ibc_deprecated = (Name
n, String
r) forall a. a -> [a] -> [a]
: IBCFile -> [(Name, String)]
ibc_deprecated IBCFile
f }
ibc IState
i (IBCFragile Name
n String
r)   IBCFile
f = forall (m :: * -> *) a. Monad m => a -> m a
return IBCFile
f { ibc_fragile :: [(Name, String)]
ibc_fragile    = (Name
n,String
r)  forall a. a -> [a] -> [a]
: IBCFile -> [(Name, String)]
ibc_fragile IBCFile
f }
ibc IState
i (IBCConstraint FC
fc UConstraint
u)  IBCFile
f = forall (m :: * -> *) a. Monad m => a -> m a
return IBCFile
f { ibc_constraints :: [(FC, UConstraint)]
ibc_constraints = (FC
fc, UConstraint
u) forall a. a -> [a] -> [a]
: IBCFile -> [(FC, UConstraint)]
ibc_constraints IBCFile
f }
ibc IState
i (IBCImportHash String
fn Int
h) IBCFile
f = forall (m :: * -> *) a. Monad m => a -> m a
return IBCFile
f { ibc_importhashes :: [(String, Int)]
ibc_importhashes = (String
fn, Int
h) forall a. a -> [a] -> [a]
: IBCFile -> [(String, Int)]
ibc_importhashes IBCFile
f }

getEntry :: (Binary b, NFData b) => b -> FilePath -> Archive -> Idris b
getEntry :: forall b. (Binary b, NFData b) => b -> String -> Archive -> Idris b
getEntry b
alt String
f Archive
a = case String -> Archive -> Maybe Entry
findEntryByPath String
f Archive
a of
                Maybe Entry
Nothing -> forall (m :: * -> *) a. Monad m => a -> m a
return b
alt
                Just Entry
e -> forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$! (forall a. NFData a => a -> a
force forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a. Binary a => ByteString -> a
decode forall b c a. (b -> c) -> (a -> b) -> a -> c
. Entry -> ByteString
fromEntry) Entry
e

unhide :: IBCPhase -> FilePath -> Archive -> Idris ()
unhide :: IBCPhase -> String -> Archive -> Idris ()
unhide IBCPhase
phase String
fp Archive
ar = do
    Bool -> IBCPhase -> String -> Archive -> Idris ()
processImports Bool
True IBCPhase
phase String
fp Archive
ar
    Bool -> IBCPhase -> Archive -> Idris ()
processAccess Bool
True IBCPhase
phase Archive
ar

process :: Bool -- ^ Reexporting
           -> IBCPhase
           -> Archive -> FilePath -> Idris ()
process :: Bool -> IBCPhase -> Archive -> String -> Idris ()
process Bool
reexp IBCPhase
phase Archive
archive String
fn = do
                Word16
ver <- forall b. (Binary b, NFData b) => b -> String -> Archive -> Idris b
getEntry Word16
0 String
"ver" Archive
archive
                forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
when (Word16
ver forall a. Eq a => a -> a -> Bool
/= Word16
ibcVersion) forall a b. (a -> b) -> a -> b
$ do
                                    Int -> String -> Idris ()
logIBC Int
2 String
"ibc out of date"
                                    let e :: String
e = if Word16
ver forall a. Ord a => a -> a -> Bool
< Word16
ibcVersion
                                            then String
"an earlier" else String
"a later"
                                    String
ldir <- forall a. IO a -> Idris a
runIO forall a b. (a -> b) -> a -> b
$ IO String
getIdrisLibDir
                                    let start :: String
start = if String
ldir forall a. Eq a => [a] -> [a] -> Bool
`L.isPrefixOf` String
fn
                                                  then String
"This external module"
                                                  else String
"This module"
                                    let end :: String
end = case forall a. Eq a => [a] -> [a] -> Maybe [a]
L.stripPrefix String
ldir String
fn of
                                                Maybe String
Nothing -> String
"Please clean and rebuild."

                                                Just String
ploc -> [String] -> String
unwords [String
"Please reinstall:", forall a. [a] -> a
L.head forall a b. (a -> b) -> a -> b
$ String -> [String]
splitDirectories String
ploc]
                                    forall a. String -> Idris a
ifail forall a b. (a -> b) -> a -> b
$ [String] -> String
unlines [ [String] -> String
unwords [String
"Incompatible ibc version for:", forall a. Show a => a -> String
show String
fn]
                                                    , [String] -> String
unwords [String
start
                                                              , String
"was built with"
                                                              , String
e
                                                              , String
"version of Idris."]
                                                    , String
end
                                                    ]
                String
source <- forall b. (Binary b, NFData b) => b -> String -> Archive -> Idris b
getEntry String
"" String
"sourcefile" Archive
archive
                Bool
srcok <- forall a. IO a -> Idris a
runIO forall a b. (a -> b) -> a -> b
$ String -> IO Bool
doesFileExist String
source
                forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
when Bool
srcok forall a b. (a -> b) -> a -> b
$ String -> String -> Idris ()
timestampOlder String
source String
fn
                Archive -> Idris ()
processImportDirs Archive
archive
                Archive -> Idris ()
processSourceDirs Archive
archive
                Bool -> IBCPhase -> String -> Archive -> Idris ()
processImports Bool
reexp IBCPhase
phase String
fn Archive
archive
                Archive -> Idris ()
processImplicits Archive
archive
                Archive -> Idris ()
processInfix Archive
archive
                Archive -> Idris ()
processStatics Archive
archive
                Archive -> Idris ()
processInterfaces Archive
archive
                Archive -> Idris ()
processRecords Archive
archive
                Archive -> Idris ()
processImplementations Archive
archive
                Archive -> Idris ()
processDSLs Archive
archive
                Archive -> Idris ()
processDatatypes  Archive
archive
                Archive -> Idris ()
processOptimise  Archive
archive
                Archive -> Idris ()
processSyntax Archive
archive
                Archive -> Idris ()
processKeywords Archive
archive
                String -> Archive -> Idris ()
processObjectFiles String
fn Archive
archive
                Archive -> Idris ()
processLibs Archive
archive
                Archive -> Idris ()
processCodegenFlags Archive
archive
                Archive -> Idris ()
processDynamicLibs Archive
archive
                Archive -> Idris ()
processHeaders Archive
archive
                Archive -> Idris ()
processPatternDefs Archive
archive
                Archive -> Idris ()
processFlags Archive
archive
                Archive -> Idris ()
processFnInfo Archive
archive
                Archive -> Idris ()
processTotalityCheckError Archive
archive
                Archive -> Idris ()
processCallgraph Archive
archive
                Archive -> Idris ()
processDocs Archive
archive
                Archive -> Idris ()
processModuleDocs Archive
archive
                Archive -> Idris ()
processCoercions Archive
archive
                Archive -> Idris ()
processTransforms Archive
archive
                Archive -> Idris ()
processErrRev Archive
archive
                Archive -> Idris ()
processErrReduce Archive
archive
                Archive -> Idris ()
processLineApps Archive
archive
                Archive -> Idris ()
processNameHints Archive
archive
                Archive -> Idris ()
processMetaInformation Archive
archive
                Archive -> Idris ()
processErrorHandlers Archive
archive
                Archive -> Idris ()
processFunctionErrorHandlers Archive
archive
                Archive -> Idris ()
processMetaVars Archive
archive
                Archive -> Idris ()
processPostulates Archive
archive
                Archive -> Idris ()
processExterns Archive
archive
                Archive -> Idris ()
processParsedSpan Archive
archive
                Archive -> Idris ()
processUsage Archive
archive
                Archive -> Idris ()
processExports Archive
archive
                Archive -> Idris ()
processAutoHints Archive
archive
                Archive -> Idris ()
processDeprecate Archive
archive
                Archive -> Idris ()
processDefs Archive
archive
                Archive -> Idris ()
processTotal Archive
archive
                Archive -> Idris ()
processInjective Archive
archive
                Bool -> IBCPhase -> Archive -> Idris ()
processAccess Bool
reexp IBCPhase
phase Archive
archive
                Archive -> Idris ()
processFragile Archive
archive
                Archive -> Idris ()
processConstraints Archive
archive
                IBCPhase -> Archive -> Idris ()
processLangExts IBCPhase
phase Archive
archive

timestampOlder :: FilePath -> FilePath -> Idris ()
timestampOlder :: String -> String -> Idris ()
timestampOlder String
src String
ibc = do
  UTCTime
srct <- forall a. IO a -> Idris a
runIO forall a b. (a -> b) -> a -> b
$ String -> IO UTCTime
getModificationTime String
src
  UTCTime
ibct <- forall a. IO a -> Idris a
runIO forall a b. (a -> b) -> a -> b
$ String -> IO UTCTime
getModificationTime String
ibc
  if (UTCTime
srct forall a. Ord a => a -> a -> Bool
> UTCTime
ibct)
    then forall a. String -> Idris a
ifail forall a b. (a -> b) -> a -> b
$ [String] -> String
unlines [ String
"Module needs reloading:"
                         , [String] -> String
unwords [String
"\tSRC :", forall a. Show a => a -> String
show String
src]
                         , [String] -> String
unwords [String
"\tModified at:", forall a. Show a => a -> String
show UTCTime
srct]
                         , [String] -> String
unwords [String
"\tIBC :", forall a. Show a => a -> String
show String
ibc]
                         , [String] -> String
unwords [String
"\tModified at:", forall a. Show a => a -> String
show UTCTime
ibct]
                         ]
    else forall (m :: * -> *) a. Monad m => a -> m a
return ()

processPostulates :: Archive -> Idris ()
processPostulates :: Archive -> Idris ()
processPostulates Archive
ar = do
    [Name]
ns <- forall b. (Binary b, NFData b) => b -> String -> Archive -> Idris b
getEntry [] String
"ibc_postulates" Archive
ar
    (IState -> IState) -> Idris ()
updateIState (\IState
i -> IState
i { idris_postulates :: Set Name
idris_postulates = IState -> Set Name
idris_postulates IState
i forall a. Ord a => Set a -> Set a -> Set a
`S.union` forall a. Ord a => [a] -> Set a
S.fromList [Name]
ns })

processExterns :: Archive -> Idris ()
processExterns :: Archive -> Idris ()
processExterns Archive
ar = do
    [(Name, Int)]
ns <-  forall b. (Binary b, NFData b) => b -> String -> Archive -> Idris b
getEntry [] String
"ibc_externs" Archive
ar
    (IState -> IState) -> Idris ()
updateIState (\IState
i -> IState
i{ idris_externs :: Set (Name, Int)
idris_externs = IState -> Set (Name, Int)
idris_externs IState
i forall a. Ord a => Set a -> Set a -> Set a
`S.union` forall a. Ord a => [a] -> Set a
S.fromList [(Name, Int)]
ns })

processParsedSpan :: Archive -> Idris ()
processParsedSpan :: Archive -> Idris ()
processParsedSpan Archive
ar = do
    Maybe FC
fc <- forall b. (Binary b, NFData b) => b -> String -> Archive -> Idris b
getEntry forall a. Maybe a
Nothing String
"ibc_parsedSpan" Archive
ar
    (IState -> IState) -> Idris ()
updateIState (\IState
i -> IState
i { idris_parsedSpan :: Maybe FC
idris_parsedSpan = Maybe FC
fc })

processUsage :: Archive -> Idris ()
processUsage :: Archive -> Idris ()
processUsage Archive
ar = do
    [(Name, Int)]
ns <- forall b. (Binary b, NFData b) => b -> String -> Archive -> Idris b
getEntry [] String
"ibc_usage" Archive
ar
    (IState -> IState) -> Idris ()
updateIState (\IState
i -> IState
i { idris_erasureUsed :: [(Name, Int)]
idris_erasureUsed = [(Name, Int)]
ns forall a. [a] -> [a] -> [a]
++ IState -> [(Name, Int)]
idris_erasureUsed IState
i })

processExports :: Archive -> Idris ()
processExports :: Archive -> Idris ()
processExports Archive
ar = do
    [Name]
ns <- forall b. (Binary b, NFData b) => b -> String -> Archive -> Idris b
getEntry [] String
"ibc_exports" Archive
ar
    (IState -> IState) -> Idris ()
updateIState (\IState
i -> IState
i { idris_exports :: [Name]
idris_exports = [Name]
ns forall a. [a] -> [a] -> [a]
++ IState -> [Name]
idris_exports IState
i })

processAutoHints :: Archive -> Idris ()
processAutoHints :: Archive -> Idris ()
processAutoHints Archive
ar = do
    [(Name, Name)]
ns <- forall b. (Binary b, NFData b) => b -> String -> Archive -> Idris b
getEntry [] String
"ibc_autohints" Archive
ar
    forall (t :: * -> *) (m :: * -> *) a b.
(Foldable t, Monad m) =>
(a -> m b) -> t a -> m ()
mapM_ (\(Name
n,Name
h) -> Name -> Name -> Idris ()
addAutoHint Name
n Name
h) [(Name, Name)]
ns

processDeprecate :: Archive -> Idris ()
processDeprecate :: Archive -> Idris ()
processDeprecate Archive
ar = do
    [(Name, String)]
ns <-  forall b. (Binary b, NFData b) => b -> String -> Archive -> Idris b
getEntry [] String
"ibc_deprecated" Archive
ar
    forall (t :: * -> *) (m :: * -> *) a b.
(Foldable t, Monad m) =>
(a -> m b) -> t a -> m ()
mapM_ (\(Name
n,String
reason) -> Name -> String -> Idris ()
addDeprecated Name
n String
reason) [(Name, String)]
ns

processFragile :: Archive -> Idris ()
processFragile :: Archive -> Idris ()
processFragile Archive
ar = do
    [(Name, String)]
ns <- forall b. (Binary b, NFData b) => b -> String -> Archive -> Idris b
getEntry [] String
"ibc_fragile" Archive
ar
    forall (t :: * -> *) (m :: * -> *) a b.
(Foldable t, Monad m) =>
(a -> m b) -> t a -> m ()
mapM_ (\(Name
n,String
reason) -> Name -> String -> Idris ()
addFragile Name
n String
reason) [(Name, String)]
ns

processConstraints :: Archive -> Idris ()
processConstraints :: Archive -> Idris ()
processConstraints Archive
ar = do
    [(FC, UConstraint)]
cs <- forall b. (Binary b, NFData b) => b -> String -> Archive -> Idris b
getEntry [] String
"ibc_constraints" Archive
ar
    forall (t :: * -> *) (m :: * -> *) a b.
(Foldable t, Monad m) =>
(a -> m b) -> t a -> m ()
mapM_ (\ (FC
fc, UConstraint
c) -> FC -> (Int, [UConstraint]) -> Idris ()
addConstraints FC
fc (Int
0, [UConstraint
c])) [(FC, UConstraint)]
cs

processImportDirs :: Archive -> Idris ()
processImportDirs :: Archive -> Idris ()
processImportDirs Archive
ar = do
    [String]
fs <- forall b. (Binary b, NFData b) => b -> String -> Archive -> Idris b
getEntry [] String
"ibc_importdirs" Archive
ar
    forall (t :: * -> *) (m :: * -> *) a b.
(Foldable t, Monad m) =>
(a -> m b) -> t a -> m ()
mapM_ String -> Idris ()
addImportDir [String]
fs

processSourceDirs :: Archive -> Idris ()
processSourceDirs :: Archive -> Idris ()
processSourceDirs Archive
ar = do
    [String]
fs <- forall b. (Binary b, NFData b) => b -> String -> Archive -> Idris b
getEntry [] String
"ibc_sourcedirs" Archive
ar
    forall (t :: * -> *) (m :: * -> *) a b.
(Foldable t, Monad m) =>
(a -> m b) -> t a -> m ()
mapM_ String -> Idris ()
addSourceDir [String]
fs

processImports :: Bool -> IBCPhase -> FilePath -> Archive -> Idris ()
processImports :: Bool -> IBCPhase -> String -> Archive -> Idris ()
processImports Bool
reexp IBCPhase
phase String
fname Archive
ar = do
    [(Bool, String)]
fs <- forall b. (Binary b, NFData b) => b -> String -> Archive -> Idris b
getEntry [] String
"ibc_imports" Archive
ar
    forall (t :: * -> *) (m :: * -> *) a b.
(Foldable t, Monad m) =>
(a -> m b) -> t a -> m ()
mapM_ (\(Bool
re, String
f) -> do
        IState
i <- Idris IState
getIState
        String
ibcsd <- IState -> Idris String
valIBCSubDir IState
i
        [String]
ids <- String -> Idris [String]
rankedImportDirs String
fname
        IState -> Idris ()
putIState (IState
i { imported :: [String]
imported = String
f forall a. a -> [a] -> [a]
: IState -> [String]
imported IState
i })
        let (IBCPhase
phase', Bool
reexp') =
              case IBCPhase
phase of
                IBC_REPL Bool
True -> (Bool -> IBCPhase
IBC_REPL Bool
False, Bool
reexp)
                IBC_REPL Bool
False -> (IBCPhase
IBC_Building, Bool
reexp Bool -> Bool -> Bool
&& Bool
re)
                IBCPhase
p -> (IBCPhase
p, Bool
reexp Bool -> Bool -> Bool
&& Bool
re)
        Maybe String
fp <- [String] -> String -> String -> Idris (Maybe String)
findIBC [String]
ids String
ibcsd String
f
        Int -> String -> Idris ()
logIBC Int
4 forall a b. (a -> b) -> a -> b
$ String
"processImports (fp, phase')" forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> String
show (Maybe String
fp, IBCPhase
phase')
        case Maybe String
fp of
            Maybe String
Nothing -> do Int -> String -> Idris ()
logIBC Int
2 forall a b. (a -> b) -> a -> b
$ String
"Failed to load ibc " forall a. [a] -> [a] -> [a]
++ String
f
            Just String
fn -> do Bool -> IBCPhase -> String -> Idris ()
loadIBC Bool
reexp' IBCPhase
phase' String
fn) [(Bool, String)]
fs

processImplicits :: Archive -> Idris ()
processImplicits :: Archive -> Idris ()
processImplicits Archive
ar = do
    [(Name, [PArg])]
imps <- forall b. (Binary b, NFData b) => b -> String -> Archive -> Idris b
getEntry [] String
"ibc_implicits" Archive
ar
    forall (t :: * -> *) (m :: * -> *) a b.
(Foldable t, Monad m) =>
(a -> m b) -> t a -> m ()
mapM_ (\ (Name
n, [PArg]
imp) -> do
        IState
i <- Idris IState
getIState
        case Name -> Bool -> Context -> Maybe (Def, Accessibility)
lookupDefAccExact Name
n Bool
False (IState -> Context
tt_ctxt IState
i) of
            Just (Def
n, Accessibility
Hidden) -> forall (m :: * -> *) a. Monad m => a -> m a
return ()
            Just (Def
n, Accessibility
Private) -> forall (m :: * -> *) a. Monad m => a -> m a
return ()
            Maybe (Def, Accessibility)
_ -> IState -> Idris ()
putIState (IState
i { idris_implicits :: Ctxt [PArg]
idris_implicits = forall a. Name -> a -> Ctxt a -> Ctxt a
addDef Name
n [PArg]
imp (IState -> Ctxt [PArg]
idris_implicits IState
i) })) [(Name, [PArg])]
imps

processInfix :: Archive -> Idris ()
processInfix :: Archive -> Idris ()
processInfix Archive
ar = do
    [FixDecl]
f <- forall b. (Binary b, NFData b) => b -> String -> Archive -> Idris b
getEntry [] String
"ibc_fixes" Archive
ar
    (IState -> IState) -> Idris ()
updateIState (\IState
i -> IState
i { idris_infixes :: [FixDecl]
idris_infixes = forall a. Ord a => [a] -> [a]
sort forall a b. (a -> b) -> a -> b
$ [FixDecl]
f forall a. [a] -> [a] -> [a]
++ IState -> [FixDecl]
idris_infixes IState
i })

processStatics :: Archive -> Idris ()
processStatics :: Archive -> Idris ()
processStatics Archive
ar = do
    [(Name, [Bool])]
ss <- forall b. (Binary b, NFData b) => b -> String -> Archive -> Idris b
getEntry [] String
"ibc_statics" Archive
ar
    forall (t :: * -> *) (m :: * -> *) a b.
(Foldable t, Monad m) =>
(a -> m b) -> t a -> m ()
mapM_ (\ (Name
n, [Bool]
s) ->
        (IState -> IState) -> Idris ()
updateIState (\IState
i -> IState
i { idris_statics :: Ctxt [Bool]
idris_statics = forall a. Name -> a -> Ctxt a -> Ctxt a
addDef Name
n [Bool]
s (IState -> Ctxt [Bool]
idris_statics IState
i) })) [(Name, [Bool])]
ss

processInterfaces :: Archive -> Idris ()
processInterfaces :: Archive -> Idris ()
processInterfaces Archive
ar = do
    [(Name, InterfaceInfo)]
cs <- forall b. (Binary b, NFData b) => b -> String -> Archive -> Idris b
getEntry [] String
"ibc_interfaces" Archive
ar
    forall (t :: * -> *) (m :: * -> *) a b.
(Foldable t, Monad m) =>
(a -> m b) -> t a -> m ()
mapM_ (\ (Name
n, InterfaceInfo
c) -> do
        IState
i <- Idris IState
getIState
        -- Don't lose implementations from previous IBCs, which
        -- could have loaded in any order
        let is :: [(Name, Bool)]
is = case forall a. Name -> Ctxt a -> Maybe a
lookupCtxtExact Name
n (IState -> Ctxt InterfaceInfo
idris_interfaces IState
i) of
                    Just InterfaceInfo
ci -> InterfaceInfo -> [(Name, Bool)]
interface_implementations InterfaceInfo
ci
                    Maybe InterfaceInfo
_ -> []
        let c' :: InterfaceInfo
c' = InterfaceInfo
c { interface_implementations :: [(Name, Bool)]
interface_implementations = InterfaceInfo -> [(Name, Bool)]
interface_implementations InterfaceInfo
c forall a. [a] -> [a] -> [a]
++ [(Name, Bool)]
is }
        IState -> Idris ()
putIState (IState
i { idris_interfaces :: Ctxt InterfaceInfo
idris_interfaces = forall a. Name -> a -> Ctxt a -> Ctxt a
addDef Name
n InterfaceInfo
c' (IState -> Ctxt InterfaceInfo
idris_interfaces IState
i) })) [(Name, InterfaceInfo)]
cs

processRecords :: Archive -> Idris ()
processRecords :: Archive -> Idris ()
processRecords Archive
ar = do
    [(Name, RecordInfo)]
rs <- forall b. (Binary b, NFData b) => b -> String -> Archive -> Idris b
getEntry [] String
"ibc_records" Archive
ar
    forall (t :: * -> *) (m :: * -> *) a b.
(Foldable t, Monad m) =>
(a -> m b) -> t a -> m ()
mapM_ (\ (Name
n, RecordInfo
r) ->
        (IState -> IState) -> Idris ()
updateIState (\IState
i -> IState
i { idris_records :: Ctxt RecordInfo
idris_records = forall a. Name -> a -> Ctxt a -> Ctxt a
addDef Name
n RecordInfo
r (IState -> Ctxt RecordInfo
idris_records IState
i) })) [(Name, RecordInfo)]
rs

processImplementations :: Archive -> Idris ()
processImplementations :: Archive -> Idris ()
processImplementations Archive
ar = do
    [(Bool, Bool, Name, Name)]
cs <- forall b. (Binary b, NFData b) => b -> String -> Archive -> Idris b
getEntry [] String
"ibc_implementations" Archive
ar
    forall (t :: * -> *) (m :: * -> *) a b.
(Foldable t, Monad m) =>
(a -> m b) -> t a -> m ()
mapM_ (\ (Bool
i, Bool
res, Name
n, Name
ins) -> Bool -> Bool -> Name -> Name -> Idris ()
addImplementation Bool
i Bool
res Name
n Name
ins) [(Bool, Bool, Name, Name)]
cs

processDSLs :: Archive -> Idris ()
processDSLs :: Archive -> Idris ()
processDSLs Archive
ar = do
    [(Name, DSL)]
cs <- forall b. (Binary b, NFData b) => b -> String -> Archive -> Idris b
getEntry [] String
"ibc_dsls" Archive
ar
    forall (t :: * -> *) (m :: * -> *) a b.
(Foldable t, Monad m) =>
(a -> m b) -> t a -> m ()
mapM_ (\ (Name
n, DSL
c) -> (IState -> IState) -> Idris ()
updateIState (\IState
i ->
                        IState
i { idris_dsls :: Ctxt DSL
idris_dsls = forall a. Name -> a -> Ctxt a -> Ctxt a
addDef Name
n DSL
c (IState -> Ctxt DSL
idris_dsls IState
i) })) [(Name, DSL)]
cs

processDatatypes :: Archive -> Idris ()
processDatatypes :: Archive -> Idris ()
processDatatypes Archive
ar = do
    [(Name, TypeInfo)]
cs <- forall b. (Binary b, NFData b) => b -> String -> Archive -> Idris b
getEntry [] String
"ibc_datatypes" Archive
ar
    forall (t :: * -> *) (m :: * -> *) a b.
(Foldable t, Monad m) =>
(a -> m b) -> t a -> m ()
mapM_ (\ (Name
n, TypeInfo
c) -> (IState -> IState) -> Idris ()
updateIState (\IState
i ->
                        IState
i { idris_datatypes :: Ctxt TypeInfo
idris_datatypes = forall a. Name -> a -> Ctxt a -> Ctxt a
addDef Name
n TypeInfo
c (IState -> Ctxt TypeInfo
idris_datatypes IState
i) })) [(Name, TypeInfo)]
cs

processOptimise :: Archive -> Idris ()
processOptimise :: Archive -> Idris ()
processOptimise Archive
ar = do
    [(Name, OptInfo)]
cs <- forall b. (Binary b, NFData b) => b -> String -> Archive -> Idris b
getEntry [] String
"ibc_optimise" Archive
ar
    forall (t :: * -> *) (m :: * -> *) a b.
(Foldable t, Monad m) =>
(a -> m b) -> t a -> m ()
mapM_ (\ (Name
n, OptInfo
c) -> (IState -> IState) -> Idris ()
updateIState (\IState
i ->
                        IState
i { idris_optimisation :: Ctxt OptInfo
idris_optimisation = forall a. Name -> a -> Ctxt a -> Ctxt a
addDef Name
n OptInfo
c (IState -> Ctxt OptInfo
idris_optimisation IState
i) })) [(Name, OptInfo)]
cs

processSyntax :: Archive -> Idris ()
processSyntax :: Archive -> Idris ()
processSyntax Archive
ar = do
    [Syntax]
s <- forall b. (Binary b, NFData b) => b -> String -> Archive -> Idris b
getEntry [] String
"ibc_syntax" Archive
ar
    (IState -> IState) -> Idris ()
updateIState (\IState
i -> IState
i { syntax_rules :: SyntaxRules
syntax_rules = [Syntax] -> SyntaxRules -> SyntaxRules
updateSyntaxRules [Syntax]
s (IState -> SyntaxRules
syntax_rules IState
i) })

processKeywords :: Archive -> Idris ()
processKeywords :: Archive -> Idris ()
processKeywords Archive
ar = do
    [String]
k <- forall b. (Binary b, NFData b) => b -> String -> Archive -> Idris b
getEntry [] String
"ibc_keywords" Archive
ar
    (IState -> IState) -> Idris ()
updateIState (\IState
i -> IState
i { syntax_keywords :: [String]
syntax_keywords = [String]
k forall a. [a] -> [a] -> [a]
++ IState -> [String]
syntax_keywords IState
i })

processObjectFiles :: FilePath -> Archive -> Idris ()
processObjectFiles :: String -> Archive -> Idris ()
processObjectFiles String
fn Archive
ar = do
    [(Codegen, String)]
os <- forall b. (Binary b, NFData b) => b -> String -> Archive -> Idris b
getEntry [] String
"ibc_objs" Archive
ar
    forall (t :: * -> *) (m :: * -> *) a b.
(Foldable t, Monad m) =>
(a -> m b) -> t a -> m ()
mapM_ (\ (Codegen
cg, String
obj) -> do
        [String]
dirs <- String -> Idris [String]
rankedImportDirs String
fn
        String
o <- forall a. IO a -> Idris a
runIO forall a b. (a -> b) -> a -> b
$ [String] -> String -> IO String
findInPath [String]
dirs String
obj
        Codegen -> String -> Idris ()
addObjectFile Codegen
cg String
o) [(Codegen, String)]
os

processLibs :: Archive -> Idris ()
processLibs :: Archive -> Idris ()
processLibs Archive
ar = do
    [(Codegen, String)]
ls <- forall b. (Binary b, NFData b) => b -> String -> Archive -> Idris b
getEntry [] String
"ibc_libs" Archive
ar
    forall (t :: * -> *) (m :: * -> *) a b.
(Foldable t, Monad m) =>
(a -> m b) -> t a -> m ()
mapM_ (forall a b c. (a -> b -> c) -> (a, b) -> c
uncurry Codegen -> String -> Idris ()
addLib) [(Codegen, String)]
ls

processCodegenFlags :: Archive -> Idris ()
processCodegenFlags :: Archive -> Idris ()
processCodegenFlags Archive
ar = do
    [(Codegen, String)]
ls <- forall b. (Binary b, NFData b) => b -> String -> Archive -> Idris b
getEntry [] String
"ibc_cgflags" Archive
ar
    forall (t :: * -> *) (m :: * -> *) a b.
(Foldable t, Monad m) =>
(a -> m b) -> t a -> m ()
mapM_ (forall a b c. (a -> b -> c) -> (a, b) -> c
uncurry Codegen -> String -> Idris ()
addFlag) [(Codegen, String)]
ls

processDynamicLibs :: Archive -> Idris ()
processDynamicLibs :: Archive -> Idris ()
processDynamicLibs Archive
ar = do
        [String]
ls <- forall b. (Binary b, NFData b) => b -> String -> Archive -> Idris b
getEntry [] String
"ibc_dynamic_libs" Archive
ar
        [Either DynamicLib String]
res <- forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
mapM ([String]
-> StateT IState (ExceptT Err IO) (Either DynamicLib String)
addDyLib forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall (m :: * -> *) a. Monad m => a -> m a
return) [String]
ls
        forall (t :: * -> *) (m :: * -> *) a b.
(Foldable t, Monad m) =>
(a -> m b) -> t a -> m ()
mapM_ forall {a}. Either a String -> Idris ()
checkLoad [Either DynamicLib String]
res
    where
        checkLoad :: Either a String -> Idris ()
checkLoad (Left a
_) = forall (m :: * -> *) a. Monad m => a -> m a
return ()
        checkLoad (Right String
err) = forall a. String -> Idris a
ifail String
err

processHeaders :: Archive -> Idris ()
processHeaders :: Archive -> Idris ()
processHeaders Archive
ar = do
    [(Codegen, String)]
hs <- forall b. (Binary b, NFData b) => b -> String -> Archive -> Idris b
getEntry [] String
"ibc_hdrs" Archive
ar
    forall (t :: * -> *) (m :: * -> *) a b.
(Foldable t, Monad m) =>
(a -> m b) -> t a -> m ()
mapM_ (forall a b c. (a -> b -> c) -> (a, b) -> c
uncurry Codegen -> String -> Idris ()
addHdr) [(Codegen, String)]
hs

processPatternDefs :: Archive -> Idris ()
processPatternDefs :: Archive -> Idris ()
processPatternDefs Archive
ar = do
    [(Name, ([([(Name, TT Name)], TT Name, TT Name)], [PTerm]))]
ds <- forall b. (Binary b, NFData b) => b -> String -> Archive -> Idris b
getEntry [] String
"ibc_patdefs" Archive
ar
    forall (t :: * -> *) (m :: * -> *) a b.
(Foldable t, Monad m) =>
(a -> m b) -> t a -> m ()
mapM_ (\ (Name
n, ([([(Name, TT Name)], TT Name, TT Name)], [PTerm])
d) -> (IState -> IState) -> Idris ()
updateIState (\IState
i ->
            IState
i { idris_patdefs :: Ctxt ([([(Name, TT Name)], TT Name, TT Name)], [PTerm])
idris_patdefs = forall a. Name -> a -> Ctxt a -> Ctxt a
addDef Name
n (forall a. NFData a => a -> a
force ([([(Name, TT Name)], TT Name, TT Name)], [PTerm])
d) (IState -> Ctxt ([([(Name, TT Name)], TT Name, TT Name)], [PTerm])
idris_patdefs IState
i) })) [(Name, ([([(Name, TT Name)], TT Name, TT Name)], [PTerm]))]
ds

processDefs :: Archive -> Idris ()
processDefs :: Archive -> Idris ()
processDefs Archive
ar = do
        [(Name, Def)]
ds <- forall b. (Binary b, NFData b) => b -> String -> Archive -> Idris b
getEntry [] String
"ibc_defs" Archive
ar
        Int -> String -> Idris ()
logIBC Int
4 forall a b. (a -> b) -> a -> b
$ String
"processDefs ds" forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> String
show [(Name, Def)]
ds
        forall (t :: * -> *) (m :: * -> *) a b.
(Foldable t, Monad m) =>
(a -> m b) -> t a -> m ()
mapM_ (\ (Name
n, Def
d) -> do
            Def
d' <- Def -> StateT IState (ExceptT Err IO) Def
updateDef Def
d
            case Def
d' of
                TyDecl NameType
_ TT Name
_ -> forall (m :: * -> *) a. Monad m => a -> m a
return ()
                Def
_ -> do
                    Int -> String -> Idris ()
logIBC Int
2 forall a b. (a -> b) -> a -> b
$ String
"SOLVING " forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> String
show Name
n
                    FC -> Name -> Idris ()
solveDeferred FC
emptyFC Name
n
            (IState -> IState) -> Idris ()
updateIState (\IState
i -> IState
i { tt_ctxt :: Context
tt_ctxt = Name -> Def -> Context -> Context
addCtxtDef Name
n Def
d' (IState -> Context
tt_ctxt IState
i) })) [(Name, Def)]
ds
    where
        updateDef :: Def -> StateT IState (ExceptT Err IO) Def
updateDef (CaseOp CaseInfo
c TT Name
t [(TT Name, Bool)]
args [Either (TT Name) (TT Name, TT Name)]
o [([Name], TT Name, TT Name)]
s CaseDefs
cd) = do
            [Either (TT Name) (TT Name, TT Name)]
o' <- forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
mapM Either (TT Name) (TT Name, TT Name)
-> StateT
     IState (ExceptT Err IO) (Either (TT Name) (TT Name, TT Name))
updateOrig [Either (TT Name) (TT Name, TT Name)]
o
            CaseDefs
cd' <- CaseDefs -> StateT IState (ExceptT Err IO) CaseDefs
updateCD CaseDefs
cd
            forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ CaseInfo
-> TT Name
-> [(TT Name, Bool)]
-> [Either (TT Name) (TT Name, TT Name)]
-> [([Name], TT Name, TT Name)]
-> CaseDefs
-> Def
CaseOp CaseInfo
c TT Name
t [(TT Name, Bool)]
args [Either (TT Name) (TT Name, TT Name)]
o' [([Name], TT Name, TT Name)]
s CaseDefs
cd'
        updateDef Def
t = forall (m :: * -> *) a. Monad m => a -> m a
return Def
t

        updateOrig :: Either (TT Name) (TT Name, TT Name)
-> StateT
     IState (ExceptT Err IO) (Either (TT Name) (TT Name, TT Name))
updateOrig (Left TT Name
t) = forall (m :: * -> *) a1 r. Monad m => (a1 -> r) -> m a1 -> m r
liftM forall a b. a -> Either a b
Left (TT Name -> StateT IState (ExceptT Err IO) (TT Name)
update TT Name
t)
        updateOrig (Right (TT Name
l, TT Name
r)) = do
            TT Name
l' <- TT Name -> StateT IState (ExceptT Err IO) (TT Name)
update TT Name
l
            TT Name
r' <- TT Name -> StateT IState (ExceptT Err IO) (TT Name)
update TT Name
r
            forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ forall a b. b -> Either a b
Right (TT Name
l', TT Name
r')

        updateCD :: CaseDefs -> StateT IState (ExceptT Err IO) CaseDefs
updateCD (CaseDefs ([Name]
cs, SC
c) ([Name]
rs, SC
r)) = do
            SC
c' <- SC -> StateT IState (ExceptT Err IO) SC
updateSC SC
c
            SC
r' <- SC -> StateT IState (ExceptT Err IO) SC
updateSC SC
r
            forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ ([Name], SC) -> ([Name], SC) -> CaseDefs
CaseDefs ([Name]
cs, SC
c') ([Name]
rs, SC
r')

        updateSC :: SC -> StateT IState (ExceptT Err IO) SC
updateSC (Case CaseType
t Name
n [CaseAlt]
alts) = do
            [CaseAlt]
alts' <- forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
mapM CaseAlt -> StateT IState (ExceptT Err IO) CaseAlt
updateAlt [CaseAlt]
alts
            forall (m :: * -> *) a. Monad m => a -> m a
return (forall t. CaseType -> Name -> [CaseAlt' t] -> SC' t
Case CaseType
t Name
n [CaseAlt]
alts')
        updateSC (ProjCase TT Name
t [CaseAlt]
alts) = do
            [CaseAlt]
alts' <- forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
mapM CaseAlt -> StateT IState (ExceptT Err IO) CaseAlt
updateAlt [CaseAlt]
alts
            forall (m :: * -> *) a. Monad m => a -> m a
return (forall t. t -> [CaseAlt' t] -> SC' t
ProjCase TT Name
t [CaseAlt]
alts')
        updateSC (STerm TT Name
t) = do
            TT Name
t' <- TT Name -> StateT IState (ExceptT Err IO) (TT Name)
update TT Name
t
            forall (m :: * -> *) a. Monad m => a -> m a
return (forall t. t -> SC' t
STerm TT Name
t')
        updateSC SC
c = forall (m :: * -> *) a. Monad m => a -> m a
return SC
c

        updateAlt :: CaseAlt -> StateT IState (ExceptT Err IO) CaseAlt
updateAlt (ConCase Name
n Int
i [Name]
ns SC
t) = do
            SC
t' <- SC -> StateT IState (ExceptT Err IO) SC
updateSC SC
t
            forall (m :: * -> *) a. Monad m => a -> m a
return (forall t. Name -> Int -> [Name] -> SC' t -> CaseAlt' t
ConCase Name
n Int
i [Name]
ns SC
t')
        updateAlt (FnCase Name
n [Name]
ns SC
t) = do
            SC
t' <- SC -> StateT IState (ExceptT Err IO) SC
updateSC SC
t
            forall (m :: * -> *) a. Monad m => a -> m a
return (forall t. Name -> [Name] -> SC' t -> CaseAlt' t
FnCase Name
n [Name]
ns SC
t')
        updateAlt (ConstCase Const
c SC
t) = do
            SC
t' <- SC -> StateT IState (ExceptT Err IO) SC
updateSC SC
t
            forall (m :: * -> *) a. Monad m => a -> m a
return (forall t. Const -> SC' t -> CaseAlt' t
ConstCase Const
c SC
t')
        updateAlt (SucCase Name
n SC
t) = do
            SC
t' <- SC -> StateT IState (ExceptT Err IO) SC
updateSC SC
t
            forall (m :: * -> *) a. Monad m => a -> m a
return (forall t. Name -> SC' t -> CaseAlt' t
SucCase Name
n SC
t')
        updateAlt (DefaultCase SC
t) = do
            SC
t' <- SC -> StateT IState (ExceptT Err IO) SC
updateSC SC
t
            forall (m :: * -> *) a. Monad m => a -> m a
return (forall t. SC' t -> CaseAlt' t
DefaultCase SC
t')

        -- We get a lot of repetition in sub terms and can save a fair chunk
        -- of memory if we make sure they're shared. addTT looks for a term
        -- and returns it if it exists already, while also keeping stats of
        -- how many times a subterm is repeated.
        update :: TT Name -> StateT IState (ExceptT Err IO) (TT Name)
update TT Name
t = do
            Maybe (TT Name)
tm <- TT Name -> Idris (Maybe (TT Name))
addTT TT Name
t
            case Maybe (TT Name)
tm of
                Maybe (TT Name)
Nothing -> TT Name -> StateT IState (ExceptT Err IO) (TT Name)
update' TT Name
t
                Just TT Name
t' -> forall (m :: * -> *) a. Monad m => a -> m a
return TT Name
t'

        update' :: TT Name -> StateT IState (ExceptT Err IO) (TT Name)
update' (P NameType
t Name
n TT Name
ty) = do
            Name
n' <- Name -> Idris Name
getSymbol Name
n
            forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ forall n. NameType -> n -> TT n -> TT n
P NameType
t Name
n' TT Name
ty
        update' (App AppStatus Name
s TT Name
f TT Name
a) = forall (m :: * -> *) a1 a2 r.
Monad m =>
(a1 -> a2 -> r) -> m a1 -> m a2 -> m r
liftM2 (forall n. AppStatus n -> TT n -> TT n -> TT n
App AppStatus Name
s) (TT Name -> StateT IState (ExceptT Err IO) (TT Name)
update' TT Name
f) (TT Name -> StateT IState (ExceptT Err IO) (TT Name)
update' TT Name
a)
        update' (Bind Name
n Binder (TT Name)
b TT Name
sc) = do
            Binder (TT Name)
b' <- Binder (TT Name)
-> StateT IState (ExceptT Err IO) (Binder (TT Name))
updateB Binder (TT Name)
b
            TT Name
sc' <- TT Name -> StateT IState (ExceptT Err IO) (TT Name)
update TT Name
sc
            forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ forall n. n -> Binder (TT n) -> TT n -> TT n
Bind Name
n Binder (TT Name)
b' TT Name
sc'
                where
                    updateB :: Binder (TT Name)
-> StateT IState (ExceptT Err IO) (Binder (TT Name))
updateB (Let RigCount
rig TT Name
t TT Name
v) = forall (m :: * -> *) a1 a2 r.
Monad m =>
(a1 -> a2 -> r) -> m a1 -> m a2 -> m r
liftM2 (forall b. RigCount -> b -> b -> Binder b
Let RigCount
rig) (TT Name -> StateT IState (ExceptT Err IO) (TT Name)
update' TT Name
t) (TT Name -> StateT IState (ExceptT Err IO) (TT Name)
update' TT Name
v)
                    updateB Binder (TT Name)
b = do
                        TT Name
ty' <- TT Name -> StateT IState (ExceptT Err IO) (TT Name)
update' (forall b. Binder b -> b
binderTy Binder (TT Name)
b)
                        forall (m :: * -> *) a. Monad m => a -> m a
return (Binder (TT Name)
b { binderTy :: TT Name
binderTy = TT Name
ty' })
        update' (Proj TT Name
t Int
i) = do
                  TT Name
t' <- TT Name -> StateT IState (ExceptT Err IO) (TT Name)
update' TT Name
t
                  forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ forall n. TT n -> Int -> TT n
Proj TT Name
t' Int
i
        update' TT Name
t = forall (m :: * -> *) a. Monad m => a -> m a
return TT Name
t

processDocs :: Archive -> Idris ()
processDocs :: Archive -> Idris ()
processDocs Archive
ar = do
    [(Name, (Docstring DocTerm, [(Name, Docstring DocTerm)]))]
ds <- forall b. (Binary b, NFData b) => b -> String -> Archive -> Idris b
getEntry [] String
"ibc_docstrings" Archive
ar
    forall (t :: * -> *) (m :: * -> *) a b.
(Foldable t, Monad m) =>
(a -> m b) -> t a -> m ()
mapM_ (\(Name
n, (Docstring DocTerm, [(Name, Docstring DocTerm)])
a) -> Name
-> Docstring DocTerm -> [(Name, Docstring DocTerm)] -> Idris ()
addDocStr Name
n (forall a b. (a, b) -> a
fst (Docstring DocTerm, [(Name, Docstring DocTerm)])
a) (forall a b. (a, b) -> b
snd (Docstring DocTerm, [(Name, Docstring DocTerm)])
a)) [(Name, (Docstring DocTerm, [(Name, Docstring DocTerm)]))]
ds

processModuleDocs :: Archive -> Idris ()
processModuleDocs :: Archive -> Idris ()
processModuleDocs Archive
ar = do
    [(Name, Docstring DocTerm)]
ds <- forall b. (Binary b, NFData b) => b -> String -> Archive -> Idris b
getEntry [] String
"ibc_moduledocs" Archive
ar
    forall (t :: * -> *) (m :: * -> *) a b.
(Foldable t, Monad m) =>
(a -> m b) -> t a -> m ()
mapM_  (\ (Name
n, Docstring DocTerm
d) -> (IState -> IState) -> Idris ()
updateIState (\IState
i ->
            IState
i { idris_moduledocs :: Ctxt (Docstring DocTerm)
idris_moduledocs = forall a. Name -> a -> Ctxt a -> Ctxt a
addDef Name
n Docstring DocTerm
d (IState -> Ctxt (Docstring DocTerm)
idris_moduledocs IState
i) })) [(Name, Docstring DocTerm)]
ds

processAccess :: Bool -- ^ Reexporting?
           -> IBCPhase
           -> Archive -> Idris ()
processAccess :: Bool -> IBCPhase -> Archive -> Idris ()
processAccess Bool
reexp IBCPhase
phase Archive
ar = do
    Int -> String -> Idris ()
logIBC Int
3 forall a b. (a -> b) -> a -> b
$ String
"processAccess (reexp, phase)" forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> String
show (Bool
reexp, IBCPhase
phase)
    [(Name, Accessibility)]
ds <- forall b. (Binary b, NFData b) => b -> String -> Archive -> Idris b
getEntry [] String
"ibc_access" Archive
ar
    Int -> String -> Idris ()
logIBC Int
3 forall a b. (a -> b) -> a -> b
$ String
"processAccess ds" forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> String
show [(Name, Accessibility)]
ds
    forall (t :: * -> *) (m :: * -> *) a b.
(Foldable t, Monad m) =>
(a -> m b) -> t a -> m ()
mapM_ (\ (Name
n, Accessibility
a_in) -> do

        let a :: Accessibility
a = if Bool
reexp then Accessibility
a_in else Accessibility
Hidden
        Int -> String -> Idris ()
logIBC Int
3 forall a b. (a -> b) -> a -> b
$ String
"Setting " forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> String
show (Accessibility
a, Name
n) forall a. [a] -> [a] -> [a]
++ String
" to " forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> String
show Accessibility
a
        (IState -> IState) -> Idris ()
updateIState (\IState
i -> IState
i { tt_ctxt :: Context
tt_ctxt = Name -> Accessibility -> Context -> Context
setAccess Name
n Accessibility
a (IState -> Context
tt_ctxt IState
i) })

        if (Bool -> Bool
not Bool
reexp)
            then do
                Int -> String -> Idris ()
logIBC Int
2 forall a b. (a -> b) -> a -> b
$ String
"Not exporting " forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> String
show Name
n
                Name -> Accessibility -> Idris ()
setAccessibility Name
n Accessibility
Hidden
            else
                Int -> String -> Idris ()
logIBC Int
2 forall a b. (a -> b) -> a -> b
$ String
"Exporting " forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> String
show Name
n

        -- Everything should be available at the REPL from
        -- things imported publicly.
        forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
when (IBCPhase
phase forall a. Eq a => a -> a -> Bool
== Bool -> IBCPhase
IBC_REPL Bool
True) forall a b. (a -> b) -> a -> b
$ do
            Int -> String -> Idris ()
logIBC Int
2 forall a b. (a -> b) -> a -> b
$ String
"Top level, exporting " forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> String
show Name
n
            Name -> Accessibility -> Idris ()
setAccessibility Name
n Accessibility
Public
      ) [(Name, Accessibility)]
ds

processFlags :: Archive -> Idris ()
processFlags :: Archive -> Idris ()
processFlags Archive
ar = do
    [(Name, FnOpts)]
ds <- forall b. (Binary b, NFData b) => b -> String -> Archive -> Idris b
getEntry [] String
"ibc_flags" Archive
ar
    forall (t :: * -> *) (m :: * -> *) a b.
(Foldable t, Monad m) =>
(a -> m b) -> t a -> m ()
mapM_ (\ (Name
n, FnOpts
a) -> Name -> FnOpts -> Idris ()
setFlags Name
n FnOpts
a) [(Name, FnOpts)]
ds

processFnInfo :: Archive -> Idris ()
processFnInfo :: Archive -> Idris ()
processFnInfo Archive
ar = do
    [(Name, FnInfo)]
ds <- forall b. (Binary b, NFData b) => b -> String -> Archive -> Idris b
getEntry [] String
"ibc_fninfo" Archive
ar
    forall (t :: * -> *) (m :: * -> *) a b.
(Foldable t, Monad m) =>
(a -> m b) -> t a -> m ()
mapM_ (\ (Name
n, FnInfo
a) -> Name -> FnInfo -> Idris ()
setFnInfo Name
n FnInfo
a) [(Name, FnInfo)]
ds

processTotal :: Archive -> Idris ()
processTotal :: Archive -> Idris ()
processTotal Archive
ar = do
    [(Name, Totality)]
ds <- forall b. (Binary b, NFData b) => b -> String -> Archive -> Idris b
getEntry [] String
"ibc_total" Archive
ar
    forall (t :: * -> *) (m :: * -> *) a b.
(Foldable t, Monad m) =>
(a -> m b) -> t a -> m ()
mapM_ (\ (Name
n, Totality
a) -> (IState -> IState) -> Idris ()
updateIState (\IState
i -> IState
i { tt_ctxt :: Context
tt_ctxt = Name -> Totality -> Context -> Context
setTotal Name
n Totality
a (IState -> Context
tt_ctxt IState
i) })) [(Name, Totality)]
ds

processInjective :: Archive -> Idris ()
processInjective :: Archive -> Idris ()
processInjective Archive
ar = do
    [(Name, Bool)]
ds <- forall b. (Binary b, NFData b) => b -> String -> Archive -> Idris b
getEntry [] String
"ibc_injective" Archive
ar
    forall (t :: * -> *) (m :: * -> *) a b.
(Foldable t, Monad m) =>
(a -> m b) -> t a -> m ()
mapM_ (\ (Name
n, Bool
a) -> (IState -> IState) -> Idris ()
updateIState (\IState
i -> IState
i { tt_ctxt :: Context
tt_ctxt = Name -> Bool -> Context -> Context
setInjective Name
n Bool
a (IState -> Context
tt_ctxt IState
i) })) [(Name, Bool)]
ds

processTotalityCheckError :: Archive -> Idris ()
processTotalityCheckError :: Archive -> Idris ()
processTotalityCheckError Archive
ar = do
    [(FC, String)]
es <- forall b. (Binary b, NFData b) => b -> String -> Archive -> Idris b
getEntry [] String
"ibc_totcheckfail" Archive
ar
    (IState -> IState) -> Idris ()
updateIState (\IState
i -> IState
i { idris_totcheckfail :: [(FC, String)]
idris_totcheckfail = IState -> [(FC, String)]
idris_totcheckfail IState
i forall a. [a] -> [a] -> [a]
++ [(FC, String)]
es })

processCallgraph :: Archive -> Idris ()
processCallgraph :: Archive -> Idris ()
processCallgraph Archive
ar = do
    [(Name, CGInfo)]
ds <- forall b. (Binary b, NFData b) => b -> String -> Archive -> Idris b
getEntry [] String
"ibc_cg" Archive
ar
    forall (t :: * -> *) (m :: * -> *) a b.
(Foldable t, Monad m) =>
(a -> m b) -> t a -> m ()
mapM_ (\ (Name
n, CGInfo
a) -> Name -> CGInfo -> Idris ()
addToCG Name
n CGInfo
a) [(Name, CGInfo)]
ds

processCoercions :: Archive -> Idris ()
processCoercions :: Archive -> Idris ()
processCoercions Archive
ar = do
    [Name]
ns <- forall b. (Binary b, NFData b) => b -> String -> Archive -> Idris b
getEntry [] String
"ibc_coercions" Archive
ar
    forall (t :: * -> *) (m :: * -> *) a b.
(Foldable t, Monad m) =>
(a -> m b) -> t a -> m ()
mapM_ (\ Name
n -> Name -> Idris ()
addCoercion Name
n) [Name]
ns

processTransforms :: Archive -> Idris ()
processTransforms :: Archive -> Idris ()
processTransforms Archive
ar = do
    [(Name, (TT Name, TT Name))]
ts <- forall b. (Binary b, NFData b) => b -> String -> Archive -> Idris b
getEntry [] String
"ibc_transforms" Archive
ar
    forall (t :: * -> *) (m :: * -> *) a b.
(Foldable t, Monad m) =>
(a -> m b) -> t a -> m ()
mapM_ (\ (Name
n, (TT Name, TT Name)
t) -> Name -> (TT Name, TT Name) -> Idris ()
addTrans Name
n (TT Name, TT Name)
t) [(Name, (TT Name, TT Name))]
ts

processErrRev :: Archive -> Idris ()
processErrRev :: Archive -> Idris ()
processErrRev Archive
ar = do
    [(TT Name, TT Name)]
ts <- forall b. (Binary b, NFData b) => b -> String -> Archive -> Idris b
getEntry [] String
"ibc_errRev" Archive
ar
    forall (t :: * -> *) (m :: * -> *) a b.
(Foldable t, Monad m) =>
(a -> m b) -> t a -> m ()
mapM_ (TT Name, TT Name) -> Idris ()
addErrRev [(TT Name, TT Name)]
ts

processErrReduce :: Archive -> Idris ()
processErrReduce :: Archive -> Idris ()
processErrReduce Archive
ar = do
    [Name]
ts <- forall b. (Binary b, NFData b) => b -> String -> Archive -> Idris b
getEntry [] String
"ibc_errReduce" Archive
ar
    forall (t :: * -> *) (m :: * -> *) a b.
(Foldable t, Monad m) =>
(a -> m b) -> t a -> m ()
mapM_ Name -> Idris ()
addErrReduce [Name]
ts

processLineApps :: Archive -> Idris ()
processLineApps :: Archive -> Idris ()
processLineApps Archive
ar = do
    [(String, Int, PTerm)]
ls <- forall b. (Binary b, NFData b) => b -> String -> Archive -> Idris b
getEntry [] String
"ibc_lineapps" Archive
ar
    forall (t :: * -> *) (m :: * -> *) a b.
(Foldable t, Monad m) =>
(a -> m b) -> t a -> m ()
mapM_ (\ (String
f, Int
i, PTerm
t) -> String -> Int -> PTerm -> Idris ()
addInternalApp String
f Int
i PTerm
t) [(String, Int, PTerm)]
ls

processNameHints :: Archive -> Idris ()
processNameHints :: Archive -> Idris ()
processNameHints Archive
ar = do
    [(Name, Name)]
ns <- forall b. (Binary b, NFData b) => b -> String -> Archive -> Idris b
getEntry [] String
"ibc_namehints" Archive
ar
    forall (t :: * -> *) (m :: * -> *) a b.
(Foldable t, Monad m) =>
(a -> m b) -> t a -> m ()
mapM_ (\ (Name
n, Name
ty) -> Name -> Name -> Idris ()
addNameHint Name
n Name
ty) [(Name, Name)]
ns

processMetaInformation :: Archive -> Idris ()
processMetaInformation :: Archive -> Idris ()
processMetaInformation Archive
ar = do
    [(Name, MetaInformation)]
ds <- forall b. (Binary b, NFData b) => b -> String -> Archive -> Idris b
getEntry [] String
"ibc_metainformation" Archive
ar
    forall (t :: * -> *) (m :: * -> *) a b.
(Foldable t, Monad m) =>
(a -> m b) -> t a -> m ()
mapM_ (\ (Name
n, MetaInformation
m) -> (IState -> IState) -> Idris ()
updateIState (\IState
i ->
                               IState
i { tt_ctxt :: Context
tt_ctxt = Name -> MetaInformation -> Context -> Context
setMetaInformation Name
n MetaInformation
m (IState -> Context
tt_ctxt IState
i) })) [(Name, MetaInformation)]
ds

processErrorHandlers :: Archive -> Idris ()
processErrorHandlers :: Archive -> Idris ()
processErrorHandlers Archive
ar = do
    [Name]
ns <- forall b. (Binary b, NFData b) => b -> String -> Archive -> Idris b
getEntry [] String
"ibc_errorhandlers" Archive
ar
    (IState -> IState) -> Idris ()
updateIState (\IState
i -> IState
i { idris_errorhandlers :: [Name]
idris_errorhandlers = IState -> [Name]
idris_errorhandlers IState
i forall a. [a] -> [a] -> [a]
++ [Name]
ns })

processFunctionErrorHandlers :: Archive -> Idris ()
processFunctionErrorHandlers :: Archive -> Idris ()
processFunctionErrorHandlers Archive
ar = do
    [(Name, Name, Name)]
ns <- forall b. (Binary b, NFData b) => b -> String -> Archive -> Idris b
getEntry [] String
"ibc_function_errorhandlers" Archive
ar
    forall (t :: * -> *) (m :: * -> *) a b.
(Foldable t, Monad m) =>
(a -> m b) -> t a -> m ()
mapM_ (\ (Name
fn,Name
arg,Name
handler) -> Name -> Name -> [Name] -> Idris ()
addFunctionErrorHandlers Name
fn Name
arg [Name
handler]) [(Name, Name, Name)]
ns

processMetaVars :: Archive -> Idris ()
processMetaVars :: Archive -> Idris ()
processMetaVars Archive
ar = do
    [(Name, (Maybe Name, Int, [Name], Bool, Bool))]
ns <- forall b. (Binary b, NFData b) => b -> String -> Archive -> Idris b
getEntry [] String
"ibc_metavars" Archive
ar
    (IState -> IState) -> Idris ()
updateIState (\IState
i -> IState
i { idris_metavars :: [(Name, (Maybe Name, Int, [Name], Bool, Bool))]
idris_metavars = forall a. [a] -> [a]
L.reverse [(Name, (Maybe Name, Int, [Name], Bool, Bool))]
ns forall a. [a] -> [a] -> [a]
++ IState -> [(Name, (Maybe Name, Int, [Name], Bool, Bool))]
idris_metavars IState
i })

-- We only want the language extensions when reading the top level thing
processLangExts :: IBCPhase -> Archive -> Idris ()
processLangExts :: IBCPhase -> Archive -> Idris ()
processLangExts (IBC_REPL Bool
True) Archive
ar
    = do [LanguageExt]
ds <- forall b. (Binary b, NFData b) => b -> String -> Archive -> Idris b
getEntry [] String
"ibc_langexts" Archive
ar
         forall (t :: * -> *) (m :: * -> *) a b.
(Foldable t, Monad m) =>
(a -> m b) -> t a -> m ()
mapM_ LanguageExt -> Idris ()
addLangExt [LanguageExt]
ds
processLangExts IBCPhase
_ Archive
_ = forall (m :: * -> *) a. Monad m => a -> m a
return ()

----- For Cheapskate and docstrings

instance Binary a => Binary (D.Docstring a)
instance Binary CT.Options
instance Binary D.DocTerm
instance Binary a => Binary (D.Block a)
instance Binary a => Binary (D.Inline a)
instance Binary CT.ListType
instance Binary CT.CodeAttr
instance Binary CT.NumWrapper

----- Generated by 'derive'

instance Binary SizeChange
instance Binary CGInfo where
        put :: CGInfo -> Put
put (CGInfo [Name]
x1 Maybe [Name]
x2 [SCGEntry]
x3 [(Int, [(Name, Int)])]
x4)
          = do forall t. Binary t => t -> Put
put [Name]
x1
--                put x3 -- Already used SCG info for totality check
               forall t. Binary t => t -> Put
put Maybe [Name]
x2
               forall t. Binary t => t -> Put
put [(Int, [(Name, Int)])]
x4
        get :: Get CGInfo
get
          = do [Name]
x1 <- forall t. Binary t => Get t
get
               Maybe [Name]
x2 <- forall t. Binary t => Get t
get
               [(Int, [(Name, Int)])]
x3 <- forall t. Binary t => Get t
get
               forall (m :: * -> *) a. Monad m => a -> m a
return ([Name]
-> Maybe [Name] -> [SCGEntry] -> [(Int, [(Name, Int)])] -> CGInfo
CGInfo [Name]
x1 Maybe [Name]
x2 [] [(Int, [(Name, Int)])]
x3)

instance Binary CaseType
instance Binary SC
instance Binary CaseAlt
instance Binary CaseDefs
instance Binary CaseInfo
instance Binary Def where
        put :: Def -> Put
put Def
x
          = {-# SCC "putDef" #-}
            case Def
x of
                Function TT Name
x1 TT Name
x2 -> do Word8 -> Put
putWord8 Word8
0
                                     forall t. Binary t => t -> Put
put TT Name
x1
                                     forall t. Binary t => t -> Put
put TT Name
x2
                TyDecl NameType
x1 TT Name
x2 -> do Word8 -> Put
putWord8 Word8
1
                                   forall t. Binary t => t -> Put
put NameType
x1
                                   forall t. Binary t => t -> Put
put TT Name
x2
                -- all primitives just get added at the start, don't write
                Operator TT Name
x1 Int
x2 [Value] -> Maybe Value
x3 -> do forall (m :: * -> *) a. Monad m => a -> m a
return ()
                -- no need to add/load original patterns, because they're not
                -- used again after totality checking
                CaseOp CaseInfo
x1 TT Name
x2 [(TT Name, Bool)]
x3 [Either (TT Name) (TT Name, TT Name)]
_ [([Name], TT Name, TT Name)]
_ CaseDefs
x4 -> do Word8 -> Put
putWord8 Word8
3
                                             forall t. Binary t => t -> Put
put CaseInfo
x1
                                             forall t. Binary t => t -> Put
put TT Name
x2
                                             forall t. Binary t => t -> Put
put [(TT Name, Bool)]
x3
                                             forall t. Binary t => t -> Put
put CaseDefs
x4
        get :: Get Def
get
          = do Word8
i <- Get Word8
getWord8
               case Word8
i of
                   Word8
0 -> do TT Name
x1 <- forall t. Binary t => Get t
get
                           TT Name
x2 <- forall t. Binary t => Get t
get
                           forall (m :: * -> *) a. Monad m => a -> m a
return (TT Name -> TT Name -> Def
Function TT Name
x1 TT Name
x2)
                   Word8
1 -> do NameType
x1 <- forall t. Binary t => Get t
get
                           TT Name
x2 <- forall t. Binary t => Get t
get
                           forall (m :: * -> *) a. Monad m => a -> m a
return (NameType -> TT Name -> Def
TyDecl NameType
x1 TT Name
x2)
                   -- Operator isn't written, don't read
                   Word8
3 -> do CaseInfo
x1 <- forall t. Binary t => Get t
get
                           TT Name
x2 <- forall t. Binary t => Get t
get
                           [(TT Name, Bool)]
x3 <- forall t. Binary t => Get t
get
--                            x4 <- get
                           -- x3 <- get always []
                           CaseDefs
x5 <- forall t. Binary t => Get t
get
                           forall (m :: * -> *) a. Monad m => a -> m a
return (CaseInfo
-> TT Name
-> [(TT Name, Bool)]
-> [Either (TT Name) (TT Name, TT Name)]
-> [([Name], TT Name, TT Name)]
-> CaseDefs
-> Def
CaseOp CaseInfo
x1 TT Name
x2 [(TT Name, Bool)]
x3 [] [] CaseDefs
x5)
                   Word8
_ -> forall a. HasCallStack => String -> a
error String
"Corrupted binary data for Def"

instance Binary Accessibility
instance Binary PReason
instance Binary Totality
instance Binary MetaInformation
instance Binary DataOpt
instance Binary FnOpt
instance Binary Fixity
instance Binary FixDecl
instance Binary ArgOpt
instance Binary Static
instance Binary Plicity where
        put :: Plicity -> Put
put Plicity
x
          = case Plicity
x of
                Imp [ArgOpt]
x1 Static
x2 Bool
x3 Maybe ImplicitInfo
x4 Bool
_ RigCount
x5 ->
                             do Word8 -> Put
putWord8 Word8
0
                                forall t. Binary t => t -> Put
put [ArgOpt]
x1
                                forall t. Binary t => t -> Put
put Static
x2
                                forall t. Binary t => t -> Put
put Bool
x3
                                forall t. Binary t => t -> Put
put Maybe ImplicitInfo
x4
                                forall t. Binary t => t -> Put
put RigCount
x5
                Exp [ArgOpt]
x1 Static
x2 Bool
x3 RigCount
x4 ->
                             do Word8 -> Put
putWord8 Word8
1
                                forall t. Binary t => t -> Put
put [ArgOpt]
x1
                                forall t. Binary t => t -> Put
put Static
x2
                                forall t. Binary t => t -> Put
put Bool
x3
                                forall t. Binary t => t -> Put
put RigCount
x4
                Constraint [ArgOpt]
x1 Static
x2 RigCount
x3 ->
                                    do Word8 -> Put
putWord8 Word8
2
                                       forall t. Binary t => t -> Put
put [ArgOpt]
x1
                                       forall t. Binary t => t -> Put
put Static
x2
                                       forall t. Binary t => t -> Put
put RigCount
x3
                TacImp [ArgOpt]
x1 Static
x2 PTerm
x3 RigCount
x4 ->
                                   do Word8 -> Put
putWord8 Word8
3
                                      forall t. Binary t => t -> Put
put [ArgOpt]
x1
                                      forall t. Binary t => t -> Put
put Static
x2
                                      forall t. Binary t => t -> Put
put PTerm
x3
                                      forall t. Binary t => t -> Put
put RigCount
x4
        get :: Get Plicity
get
          = do Word8
i <- Get Word8
getWord8
               case Word8
i of
                   Word8
0 -> do [ArgOpt]
x1 <- forall t. Binary t => Get t
get
                           Static
x2 <- forall t. Binary t => Get t
get
                           Bool
x3 <- forall t. Binary t => Get t
get
                           Maybe ImplicitInfo
x4 <- forall t. Binary t => Get t
get
                           RigCount
x5 <- forall t. Binary t => Get t
get
                           forall (m :: * -> *) a. Monad m => a -> m a
return ([ArgOpt]
-> Static
-> Bool
-> Maybe ImplicitInfo
-> Bool
-> RigCount
-> Plicity
Imp [ArgOpt]
x1 Static
x2 Bool
x3 Maybe ImplicitInfo
x4 Bool
False RigCount
x5)
                   Word8
1 -> do [ArgOpt]
x1 <- forall t. Binary t => Get t
get
                           Static
x2 <- forall t. Binary t => Get t
get
                           Bool
x3 <- forall t. Binary t => Get t
get
                           RigCount
x4 <- forall t. Binary t => Get t
get
                           forall (m :: * -> *) a. Monad m => a -> m a
return ([ArgOpt] -> Static -> Bool -> RigCount -> Plicity
Exp [ArgOpt]
x1 Static
x2 Bool
x3 RigCount
x4)
                   Word8
2 -> do [ArgOpt]
x1 <- forall t. Binary t => Get t
get
                           Static
x2 <- forall t. Binary t => Get t
get
                           RigCount
x3 <- forall t. Binary t => Get t
get
                           forall (m :: * -> *) a. Monad m => a -> m a
return ([ArgOpt] -> Static -> RigCount -> Plicity
Constraint [ArgOpt]
x1 Static
x2 RigCount
x3)
                   Word8
3 -> do [ArgOpt]
x1 <- forall t. Binary t => Get t
get
                           Static
x2 <- forall t. Binary t => Get t
get
                           PTerm
x3 <- forall t. Binary t => Get t
get
                           RigCount
x4 <- forall t. Binary t => Get t
get
                           forall (m :: * -> *) a. Monad m => a -> m a
return ([ArgOpt] -> Static -> PTerm -> RigCount -> Plicity
TacImp [ArgOpt]
x1 Static
x2 PTerm
x3 RigCount
x4)
                   Word8
_ -> forall a. HasCallStack => String -> a
error String
"Corrupted binary data for Plicity"

instance Binary DefaultTotality
instance Binary LanguageExt
instance Binary Directive
instance (Binary t) => Binary (PDecl' t)
instance Binary t => Binary (ProvideWhat' t)
instance Binary Using
instance Binary SyntaxInfo where
        put :: SyntaxInfo -> Put
put (Syn [Using]
x1 [(Name, PTerm)]
x2 [String]
x3 [Name]
x4 [Name]
_ Name -> Name
_ Bool
x5 Bool
x6 Bool
x7 Maybe Int
_ Int
_ DSL
x8 Int
_ Bool
_ Bool
_)
          = do forall t. Binary t => t -> Put
put [Using]
x1
               forall t. Binary t => t -> Put
put [(Name, PTerm)]
x2
               forall t. Binary t => t -> Put
put [String]
x3
               forall t. Binary t => t -> Put
put [Name]
x4
               forall t. Binary t => t -> Put
put Bool
x5
               forall t. Binary t => t -> Put
put Bool
x6
               forall t. Binary t => t -> Put
put Bool
x7
               forall t. Binary t => t -> Put
put DSL
x8
        get :: Get SyntaxInfo
get
          = do [Using]
x1 <- forall t. Binary t => Get t
get
               [(Name, PTerm)]
x2 <- forall t. Binary t => Get t
get
               [String]
x3 <- forall t. Binary t => Get t
get
               [Name]
x4 <- forall t. Binary t => Get t
get
               Bool
x5 <- forall t. Binary t => Get t
get
               Bool
x6 <- forall t. Binary t => Get t
get
               Bool
x7 <- forall t. Binary t => Get t
get
               DSL
x8 <- forall t. Binary t => Get t
get
               forall (m :: * -> *) a. Monad m => a -> m a
return ([Using]
-> [(Name, PTerm)]
-> [String]
-> [Name]
-> [Name]
-> (Name -> Name)
-> Bool
-> Bool
-> Bool
-> Maybe Int
-> Int
-> DSL
-> Int
-> Bool
-> Bool
-> SyntaxInfo
Syn [Using]
x1 [(Name, PTerm)]
x2 [String]
x3 [Name]
x4 [] forall a. a -> a
id Bool
x5 Bool
x6 Bool
x7 forall a. Maybe a
Nothing Int
0 DSL
x8 Int
0 Bool
True Bool
True)

instance (Binary t) => Binary (PClause' t)
instance (Binary t) => Binary (PData' t)
instance Binary PunInfo
instance Binary PTerm
instance Binary PAltType
instance (Binary t) => Binary (PTactic' t)
instance (Binary t) => Binary (PDo' t)
instance (Binary t) => Binary (PArg' t)
instance Binary InterfaceInfo where
        put :: InterfaceInfo -> Put
put (CI Name
x1 [(Name, (Bool, FnOpts, PTerm))]
x2 [(Name, (Name, PDecl))]
x3 [PDecl]
x4 [Name]
x5 [Name]
x6 [PTerm]
x7 [(Name, Bool)]
_ [Int]
x8)
          = do forall t. Binary t => t -> Put
put Name
x1
               forall t. Binary t => t -> Put
put [(Name, (Bool, FnOpts, PTerm))]
x2
               forall t. Binary t => t -> Put
put [(Name, (Name, PDecl))]
x3
               forall t. Binary t => t -> Put
put [PDecl]
x4
               forall t. Binary t => t -> Put
put [Name]
x5
               forall t. Binary t => t -> Put
put [Name]
x6
               forall t. Binary t => t -> Put
put [PTerm]
x7
               forall t. Binary t => t -> Put
put [Int]
x8
        get :: Get InterfaceInfo
get
          = do Name
x1 <- forall t. Binary t => Get t
get
               [(Name, (Bool, FnOpts, PTerm))]
x2 <- forall t. Binary t => Get t
get
               [(Name, (Name, PDecl))]
x3 <- forall t. Binary t => Get t
get
               [PDecl]
x4 <- forall t. Binary t => Get t
get
               [Name]
x5 <- forall t. Binary t => Get t
get
               [Name]
x6 <- forall t. Binary t => Get t
get
               [PTerm]
x7 <- forall t. Binary t => Get t
get
               [Int]
x8 <- forall t. Binary t => Get t
get
               forall (m :: * -> *) a. Monad m => a -> m a
return (Name
-> [(Name, (Bool, FnOpts, PTerm))]
-> [(Name, (Name, PDecl))]
-> [PDecl]
-> [Name]
-> [Name]
-> [PTerm]
-> [(Name, Bool)]
-> [Int]
-> InterfaceInfo
CI Name
x1 [(Name, (Bool, FnOpts, PTerm))]
x2 [(Name, (Name, PDecl))]
x3 [PDecl]
x4 [Name]
x5 [Name]
x6 [PTerm]
x7 [] [Int]
x8)

instance Binary RecordInfo
instance Binary OptInfo
instance Binary FnInfo
instance Binary TypeInfo
instance Binary SynContext
instance Binary Syntax
instance (Binary t) => Binary (DSL' t)
instance Binary SSymbol
instance Binary Codegen
instance Binary IRFormat