{-|
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 -> FilePath
(Int -> IBCPhase -> ShowS)
-> (IBCPhase -> FilePath) -> ([IBCPhase] -> ShowS) -> Show IBCPhase
forall a.
(Int -> a -> ShowS) -> (a -> FilePath) -> ([a] -> ShowS) -> Show a
$cshowsPrec :: Int -> IBCPhase -> ShowS
showsPrec :: Int -> IBCPhase -> ShowS
$cshow :: IBCPhase -> FilePath
show :: IBCPhase -> FilePath
$cshowList :: [IBCPhase] -> ShowS
showList :: [IBCPhase] -> ShowS
Show, IBCPhase -> IBCPhase -> Bool
(IBCPhase -> IBCPhase -> Bool)
-> (IBCPhase -> IBCPhase -> Bool) -> Eq IBCPhase
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
$c== :: IBCPhase -> IBCPhase -> Bool
== :: IBCPhase -> IBCPhase -> Bool
$c/= :: IBCPhase -> IBCPhase -> Bool
/= :: IBCPhase -> IBCPhase -> Bool
Eq)

data IBCFile = IBCFile {
    IBCFile -> Word16
ver                        :: Word16
  , IBCFile -> Int
iface_hash                 :: Int
  , IBCFile -> FilePath
sourcefile                 :: FilePath
  , IBCFile -> [(Bool, FilePath)]
ibc_imports                :: ![(Bool, FilePath)]
  , IBCFile -> [FilePath]
ibc_importdirs             :: ![FilePath]
  , IBCFile -> [FilePath]
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 -> [FilePath]
ibc_keywords               :: ![String]
  , IBCFile -> [(Codegen, FilePath)]
ibc_objs                   :: ![(Codegen, FilePath)]
  , IBCFile -> [(Codegen, FilePath)]
ibc_libs                   :: ![(Codegen, String)]
  , IBCFile -> [(Codegen, FilePath)]
ibc_cgflags                :: ![(Codegen, String)]
  , IBCFile -> [FilePath]
ibc_dynamic_libs           :: ![String]
  , IBCFile -> [(Codegen, FilePath)]
ibc_hdrs                   :: ![(Codegen, String)]
  , IBCFile -> [(FC, FilePath)]
ibc_totcheckfail           :: ![(FC, String)]
  , IBCFile -> [(Name, [FnOpt])]
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, (Term, Term))]
ibc_transforms             :: ![(Name, (Term, Term))]
  , IBCFile -> [(Term, Term)]
ibc_errRev                 :: ![(Term, Term)]
  , IBCFile -> [Name]
ibc_errReduce              :: ![Name]
  , IBCFile -> [Name]
ibc_coercions              :: ![Name]
  , IBCFile -> [(FilePath, 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, Term)], Term, Term)], [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, FilePath)]
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, FilePath)]
ibc_fragile                :: ![(Name, String)]
  , IBCFile -> [(FC, UConstraint)]
ibc_constraints            :: ![(FC, UConstraint)]
  , IBCFile -> [LanguageExt]
ibc_langexts               :: ![LanguageExt]
  , IBCFile -> [(FilePath, Int)]
ibc_importhashes           :: ![(FilePath, Int)]
  }
  deriving Int -> IBCFile -> ShowS
[IBCFile] -> ShowS
IBCFile -> FilePath
(Int -> IBCFile -> ShowS)
-> (IBCFile -> FilePath) -> ([IBCFile] -> ShowS) -> Show IBCFile
forall a.
(Int -> a -> ShowS) -> (a -> FilePath) -> ([a] -> ShowS) -> Show a
$cshowsPrec :: Int -> IBCFile -> ShowS
showsPrec :: Int -> IBCFile -> ShowS
$cshow :: IBCFile -> FilePath
show :: IBCFile -> FilePath
$cshowList :: [IBCFile] -> ShowS
showList :: [IBCFile] -> ShowS
Show
{-!
deriving instance Binary IBCFile
!-}

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

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


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

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


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

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


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


entries :: IBCFile -> [Entry]
entries :: IBCFile -> [Entry]
entries IBCFile
i = [Maybe Entry] -> [Entry]
forall a. [Maybe a] -> [a]
catMaybes [Entry -> Maybe Entry
forall a. a -> Maybe a
Just (Entry -> Maybe Entry) -> Entry -> Maybe Entry
forall a b. (a -> b) -> a -> b
$ FilePath -> Integer -> ByteString -> Entry
toEntry FilePath
"ver" Integer
0 (Word16 -> ByteString
forall a. Binary a => a -> ByteString
encode (Word16 -> ByteString) -> Word16 -> ByteString
forall a b. (a -> b) -> a -> b
$ IBCFile -> Word16
ver IBCFile
i),
                       Entry -> Maybe Entry
forall a. a -> Maybe a
Just (Entry -> Maybe Entry) -> Entry -> Maybe Entry
forall a b. (a -> b) -> a -> b
$ FilePath -> Integer -> ByteString -> Entry
toEntry FilePath
"iface_hash" Integer
0 (Int -> ByteString
forall a. Binary a => a -> ByteString
encode (Int -> ByteString) -> Int -> ByteString
forall a b. (a -> b) -> a -> b
$ IBCFile -> Int
iface_hash IBCFile
i),
                       FilePath -> FilePath -> Maybe Entry
forall b. Binary b => FilePath -> [b] -> Maybe Entry
makeEntry FilePath
"sourcefile"  (IBCFile -> FilePath
sourcefile IBCFile
i),
                       FilePath -> [(Bool, FilePath)] -> Maybe Entry
forall b. Binary b => FilePath -> [b] -> Maybe Entry
makeEntry FilePath
"ibc_imports"  (IBCFile -> [(Bool, FilePath)]
ibc_imports IBCFile
i),
                       FilePath -> [FilePath] -> Maybe Entry
forall b. Binary b => FilePath -> [b] -> Maybe Entry
makeEntry FilePath
"ibc_importdirs"  (IBCFile -> [FilePath]
ibc_importdirs IBCFile
i),
                       FilePath -> [FilePath] -> Maybe Entry
forall b. Binary b => FilePath -> [b] -> Maybe Entry
makeEntry FilePath
"ibc_sourcedirs"  (IBCFile -> [FilePath]
ibc_sourcedirs IBCFile
i),
                       FilePath -> [(Name, [PArg])] -> Maybe Entry
forall b. Binary b => FilePath -> [b] -> Maybe Entry
makeEntry FilePath
"ibc_implicits"  (IBCFile -> [(Name, [PArg])]
ibc_implicits IBCFile
i),
                       FilePath -> [FixDecl] -> Maybe Entry
forall b. Binary b => FilePath -> [b] -> Maybe Entry
makeEntry FilePath
"ibc_fixes"  (IBCFile -> [FixDecl]
ibc_fixes IBCFile
i),
                       FilePath -> [(Name, [Bool])] -> Maybe Entry
forall b. Binary b => FilePath -> [b] -> Maybe Entry
makeEntry FilePath
"ibc_statics"  (IBCFile -> [(Name, [Bool])]
ibc_statics IBCFile
i),
                       FilePath -> [(Name, InterfaceInfo)] -> Maybe Entry
forall b. Binary b => FilePath -> [b] -> Maybe Entry
makeEntry FilePath
"ibc_interfaces"  (IBCFile -> [(Name, InterfaceInfo)]
ibc_interfaces IBCFile
i),
                       FilePath -> [(Name, RecordInfo)] -> Maybe Entry
forall b. Binary b => FilePath -> [b] -> Maybe Entry
makeEntry FilePath
"ibc_records"  (IBCFile -> [(Name, RecordInfo)]
ibc_records IBCFile
i),
                       FilePath -> [(Bool, Bool, Name, Name)] -> Maybe Entry
forall b. Binary b => FilePath -> [b] -> Maybe Entry
makeEntry FilePath
"ibc_implementations"  (IBCFile -> [(Bool, Bool, Name, Name)]
ibc_implementations IBCFile
i),
                       FilePath -> [(Name, DSL)] -> Maybe Entry
forall b. Binary b => FilePath -> [b] -> Maybe Entry
makeEntry FilePath
"ibc_dsls"  (IBCFile -> [(Name, DSL)]
ibc_dsls IBCFile
i),
                       FilePath -> [(Name, TypeInfo)] -> Maybe Entry
forall b. Binary b => FilePath -> [b] -> Maybe Entry
makeEntry FilePath
"ibc_datatypes"  (IBCFile -> [(Name, TypeInfo)]
ibc_datatypes IBCFile
i),
                       FilePath -> [(Name, OptInfo)] -> Maybe Entry
forall b. Binary b => FilePath -> [b] -> Maybe Entry
makeEntry FilePath
"ibc_optimise"  (IBCFile -> [(Name, OptInfo)]
ibc_optimise IBCFile
i),
                       FilePath -> [Syntax] -> Maybe Entry
forall b. Binary b => FilePath -> [b] -> Maybe Entry
makeEntry FilePath
"ibc_syntax"  (IBCFile -> [Syntax]
ibc_syntax IBCFile
i),
                       FilePath -> [FilePath] -> Maybe Entry
forall b. Binary b => FilePath -> [b] -> Maybe Entry
makeEntry FilePath
"ibc_keywords"  (IBCFile -> [FilePath]
ibc_keywords IBCFile
i),
                       FilePath -> [(Codegen, FilePath)] -> Maybe Entry
forall b. Binary b => FilePath -> [b] -> Maybe Entry
makeEntry FilePath
"ibc_objs"  (IBCFile -> [(Codegen, FilePath)]
ibc_objs IBCFile
i),
                       FilePath -> [(Codegen, FilePath)] -> Maybe Entry
forall b. Binary b => FilePath -> [b] -> Maybe Entry
makeEntry FilePath
"ibc_libs"  (IBCFile -> [(Codegen, FilePath)]
ibc_libs IBCFile
i),
                       FilePath -> [(Codegen, FilePath)] -> Maybe Entry
forall b. Binary b => FilePath -> [b] -> Maybe Entry
makeEntry FilePath
"ibc_cgflags"  (IBCFile -> [(Codegen, FilePath)]
ibc_cgflags IBCFile
i),
                       FilePath -> [FilePath] -> Maybe Entry
forall b. Binary b => FilePath -> [b] -> Maybe Entry
makeEntry FilePath
"ibc_dynamic_libs"  (IBCFile -> [FilePath]
ibc_dynamic_libs IBCFile
i),
                       FilePath -> [(Codegen, FilePath)] -> Maybe Entry
forall b. Binary b => FilePath -> [b] -> Maybe Entry
makeEntry FilePath
"ibc_hdrs"  (IBCFile -> [(Codegen, FilePath)]
ibc_hdrs IBCFile
i),
                       FilePath -> [(FC, FilePath)] -> Maybe Entry
forall b. Binary b => FilePath -> [b] -> Maybe Entry
makeEntry FilePath
"ibc_totcheckfail"  (IBCFile -> [(FC, FilePath)]
ibc_totcheckfail IBCFile
i),
                       FilePath -> [(Name, [FnOpt])] -> Maybe Entry
forall b. Binary b => FilePath -> [b] -> Maybe Entry
makeEntry FilePath
"ibc_flags"  (IBCFile -> [(Name, [FnOpt])]
ibc_flags IBCFile
i),
                       FilePath -> [(Name, FnInfo)] -> Maybe Entry
forall b. Binary b => FilePath -> [b] -> Maybe Entry
makeEntry FilePath
"ibc_fninfo"  (IBCFile -> [(Name, FnInfo)]
ibc_fninfo IBCFile
i),
                       FilePath -> [(Name, CGInfo)] -> Maybe Entry
forall b. Binary b => FilePath -> [b] -> Maybe Entry
makeEntry FilePath
"ibc_cg"  (IBCFile -> [(Name, CGInfo)]
ibc_cg IBCFile
i),
                       FilePath
-> [(Name, (Docstring DocTerm, [(Name, Docstring DocTerm)]))]
-> Maybe Entry
forall b. Binary b => FilePath -> [b] -> Maybe Entry
makeEntry FilePath
"ibc_docstrings"  (IBCFile
-> [(Name, (Docstring DocTerm, [(Name, Docstring DocTerm)]))]
ibc_docstrings IBCFile
i),
                       FilePath -> [(Name, Docstring DocTerm)] -> Maybe Entry
forall b. Binary b => FilePath -> [b] -> Maybe Entry
makeEntry FilePath
"ibc_moduledocs"  (IBCFile -> [(Name, Docstring DocTerm)]
ibc_moduledocs IBCFile
i),
                       FilePath -> [(Name, (Term, Term))] -> Maybe Entry
forall b. Binary b => FilePath -> [b] -> Maybe Entry
makeEntry FilePath
"ibc_transforms"  (IBCFile -> [(Name, (Term, Term))]
ibc_transforms IBCFile
i),
                       FilePath -> [(Term, Term)] -> Maybe Entry
forall b. Binary b => FilePath -> [b] -> Maybe Entry
makeEntry FilePath
"ibc_errRev"  (IBCFile -> [(Term, Term)]
ibc_errRev IBCFile
i),
                       FilePath -> [Name] -> Maybe Entry
forall b. Binary b => FilePath -> [b] -> Maybe Entry
makeEntry FilePath
"ibc_errReduce"  (IBCFile -> [Name]
ibc_errReduce IBCFile
i),
                       FilePath -> [Name] -> Maybe Entry
forall b. Binary b => FilePath -> [b] -> Maybe Entry
makeEntry FilePath
"ibc_coercions"  (IBCFile -> [Name]
ibc_coercions IBCFile
i),
                       FilePath -> [(FilePath, Int, PTerm)] -> Maybe Entry
forall b. Binary b => FilePath -> [b] -> Maybe Entry
makeEntry FilePath
"ibc_lineapps"  (IBCFile -> [(FilePath, Int, PTerm)]
ibc_lineapps IBCFile
i),
                       FilePath -> [(Name, Name)] -> Maybe Entry
forall b. Binary b => FilePath -> [b] -> Maybe Entry
makeEntry FilePath
"ibc_namehints"  (IBCFile -> [(Name, Name)]
ibc_namehints IBCFile
i),
                       FilePath -> [(Name, MetaInformation)] -> Maybe Entry
forall b. Binary b => FilePath -> [b] -> Maybe Entry
makeEntry FilePath
"ibc_metainformation"  (IBCFile -> [(Name, MetaInformation)]
ibc_metainformation IBCFile
i),
                       FilePath -> [Name] -> Maybe Entry
forall b. Binary b => FilePath -> [b] -> Maybe Entry
makeEntry FilePath
"ibc_errorhandlers"  (IBCFile -> [Name]
ibc_errorhandlers IBCFile
i),
                       FilePath -> [(Name, Name, Name)] -> Maybe Entry
forall b. Binary b => FilePath -> [b] -> Maybe Entry
makeEntry FilePath
"ibc_function_errorhandlers"  (IBCFile -> [(Name, Name, Name)]
ibc_function_errorhandlers IBCFile
i),
                       FilePath
-> [(Name, (Maybe Name, Int, [Name], Bool, Bool))] -> Maybe Entry
forall b. Binary b => FilePath -> [b] -> Maybe Entry
makeEntry FilePath
"ibc_metavars"  (IBCFile -> [(Name, (Maybe Name, Int, [Name], Bool, Bool))]
ibc_metavars IBCFile
i),
                       FilePath
-> [(Name, ([([(Name, Term)], Term, Term)], [PTerm]))]
-> Maybe Entry
forall b. Binary b => FilePath -> [b] -> Maybe Entry
makeEntry FilePath
"ibc_patdefs"  (IBCFile -> [(Name, ([([(Name, Term)], Term, Term)], [PTerm]))]
ibc_patdefs IBCFile
i),
                       FilePath -> [Name] -> Maybe Entry
forall b. Binary b => FilePath -> [b] -> Maybe Entry
makeEntry FilePath
"ibc_postulates"  (IBCFile -> [Name]
ibc_postulates IBCFile
i),
                       FilePath -> [(Name, Int)] -> Maybe Entry
forall b. Binary b => FilePath -> [b] -> Maybe Entry
makeEntry FilePath
"ibc_externs"  (IBCFile -> [(Name, Int)]
ibc_externs IBCFile
i),
                       FilePath -> Integer -> ByteString -> Entry
toEntry FilePath
"ibc_parsedSpan" Integer
0 (ByteString -> Entry) -> (FC -> ByteString) -> FC -> Entry
forall b c a. (b -> c) -> (a -> b) -> a -> c
. FC -> ByteString
forall a. Binary a => a -> ByteString
encode (FC -> Entry) -> Maybe FC -> Maybe Entry
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> IBCFile -> Maybe FC
ibc_parsedSpan IBCFile
i,
                       FilePath -> [(Name, Int)] -> Maybe Entry
forall b. Binary b => FilePath -> [b] -> Maybe Entry
makeEntry FilePath
"ibc_usage"  (IBCFile -> [(Name, Int)]
ibc_usage IBCFile
i),
                       FilePath -> [Name] -> Maybe Entry
forall b. Binary b => FilePath -> [b] -> Maybe Entry
makeEntry FilePath
"ibc_exports"  (IBCFile -> [Name]
ibc_exports IBCFile
i),
                       FilePath -> [(Name, Name)] -> Maybe Entry
forall b. Binary b => FilePath -> [b] -> Maybe Entry
makeEntry FilePath
"ibc_autohints"  (IBCFile -> [(Name, Name)]
ibc_autohints IBCFile
i),
                       FilePath -> [(Name, FilePath)] -> Maybe Entry
forall b. Binary b => FilePath -> [b] -> Maybe Entry
makeEntry FilePath
"ibc_deprecated"  (IBCFile -> [(Name, FilePath)]
ibc_deprecated IBCFile
i),
                       FilePath -> [(Name, Def)] -> Maybe Entry
forall b. Binary b => FilePath -> [b] -> Maybe Entry
makeEntry FilePath
"ibc_defs"  (IBCFile -> [(Name, Def)]
ibc_defs IBCFile
i),
                       FilePath -> [(Name, Totality)] -> Maybe Entry
forall b. Binary b => FilePath -> [b] -> Maybe Entry
makeEntry FilePath
"ibc_total"  (IBCFile -> [(Name, Totality)]
ibc_total IBCFile
i),
                       FilePath -> [(Name, Bool)] -> Maybe Entry
forall b. Binary b => FilePath -> [b] -> Maybe Entry
makeEntry FilePath
"ibc_injective"  (IBCFile -> [(Name, Bool)]
ibc_injective IBCFile
i),
                       FilePath -> [(Name, Accessibility)] -> Maybe Entry
forall b. Binary b => FilePath -> [b] -> Maybe Entry
makeEntry FilePath
"ibc_access"  (IBCFile -> [(Name, Accessibility)]
ibc_access IBCFile
i),
                       FilePath -> [(Name, FilePath)] -> Maybe Entry
forall b. Binary b => FilePath -> [b] -> Maybe Entry
makeEntry FilePath
"ibc_fragile" (IBCFile -> [(Name, FilePath)]
ibc_fragile IBCFile
i),
                       FilePath -> [LanguageExt] -> Maybe Entry
forall b. Binary b => FilePath -> [b] -> Maybe Entry
makeEntry FilePath
"ibc_langexts" (IBCFile -> [LanguageExt]
ibc_langexts IBCFile
i),
                       FilePath -> [(FilePath, Int)] -> Maybe Entry
forall b. Binary b => FilePath -> [b] -> Maybe Entry
makeEntry FilePath
"ibc_importhashes" (IBCFile -> [(FilePath, 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 :: FilePath -> IBCFile -> Idris ()
writeArchive FilePath
fp IBCFile
i = do let a :: Archive
a = (Archive -> Entry -> Archive) -> Archive -> [Entry] -> Archive
forall b a. (b -> a -> b) -> b -> [a] -> b
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)
                       IO () -> Idris ()
forall a. IO a -> Idris a
runIO (IO () -> Idris ()) -> IO () -> Idris ()
forall a b. (a -> b) -> a -> b
$ FilePath -> ByteString -> IO ()
B.writeFile FilePath
fp (Archive -> ByteString
fromArchive Archive
a)

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

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

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

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

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

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

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

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

    getFullDef :: (Name, [FnOpt]) -> [Term]
    getFullDef :: (Name, [FnOpt]) -> [Term]
getFullDef (Name
n, [FnOpt]
_)
        = case Name -> Context -> Maybe Term
lookupTyExact Name
n (IState -> Context
tt_ctxt IState
ist) of
               Maybe Term
Nothing -> []
               Just Term
ty -> Term
ty Term -> [Term] -> [Term]
forall a. a -> [a] -> [a]
: Name -> [Term]
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 :: FilePath -> Idris ()
writePkgIndex FilePath
f
    = do IState
i <- Idris IState
getIState
         let imps :: [(Bool, FilePath)]
imps = ((FilePath, Bool) -> (Bool, FilePath))
-> [(FilePath, Bool)] -> [(Bool, FilePath)]
forall a b. (a -> b) -> [a] -> [b]
map (\ (FilePath
x, Bool
y) -> (Bool
True, FilePath
x)) ([(FilePath, Bool)] -> [(Bool, FilePath)])
-> [(FilePath, Bool)] -> [(Bool, FilePath)]
forall a b. (a -> b) -> a -> b
$ IState -> [(FilePath, Bool)]
idris_imported IState
i
         Int -> FilePath -> Idris ()
logIBC Int
2 (FilePath -> Idris ()) -> FilePath -> Idris ()
forall a b. (a -> b) -> a -> b
$ FilePath
"Writing package index " FilePath -> ShowS
forall a. [a] -> [a] -> [a]
++ ShowS
forall a. Show a => a -> FilePath
show FilePath
f FilePath -> ShowS
forall a. [a] -> [a] -> [a]
++ FilePath
" including\n" FilePath -> ShowS
forall a. [a] -> [a] -> [a]
++
                [FilePath] -> FilePath
forall a. Show a => a -> FilePath
show (((Bool, FilePath) -> FilePath) -> [(Bool, FilePath)] -> [FilePath]
forall a b. (a -> b) -> [a] -> [b]
map (Bool, FilePath) -> FilePath
forall a b. (a, b) -> b
snd [(Bool, FilePath)]
imps)
         Idris ()
resetNameIdx
         let ibcf :: IBCFile
ibcf = IBCFile
initIBC { ibc_imports = imps,
                              ibc_langexts = idris_language_extensions i }
         Idris () -> (Err -> Idris ()) -> Idris ()
forall a. Idris a -> (Err -> Idris a) -> Idris a
idrisCatch (do IO () -> Idris ()
forall a. IO a -> Idris a
runIO (IO () -> Idris ()) -> IO () -> Idris ()
forall a b. (a -> b) -> a -> b
$ Bool -> FilePath -> IO ()
createDirectoryIfMissing Bool
True (ShowS
dropFileName FilePath
f)
                        FilePath -> IBCFile -> Idris ()
writeArchive FilePath
f IBCFile
ibcf
                        Int -> FilePath -> Idris ()
logIBC Int
2 FilePath
"Written")
            (\Err
c -> do Int -> FilePath -> Idris ()
logIBC Int
2 (FilePath -> Idris ()) -> FilePath -> Idris ()
forall a b. (a -> b) -> a -> b
$ FilePath
"Failed " FilePath -> ShowS
forall a. [a] -> [a] -> [a]
++ IState -> Err -> FilePath
pshow IState
i Err
c)
         () -> Idris ()
forall a. a -> StateT IState (ExceptT Err IO) a
forall (m :: * -> *) a. Monad m => a -> m a
return ()

mkIBC :: [IBCWrite] -> IBCFile -> Idris IBCFile
mkIBC :: [IBCWrite] -> IBCFile -> Idris IBCFile
mkIBC [] IBCFile
f = IBCFile -> Idris IBCFile
forall a. a -> StateT IState (ExceptT Err IO) a
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 -> FilePath -> Idris ()
logIBC Int
5 (FilePath -> Idris ()) -> FilePath -> Idris ()
forall a b. (a -> b) -> a -> b
$ IBCWrite -> FilePath
forall a. Show a => a -> FilePath
show IBCWrite
i FilePath -> ShowS
forall a. [a] -> [a] -> [a]
++ FilePath
" " FilePath -> ShowS
forall a. [a] -> [a] -> [a]
++ Int -> FilePath
forall a. Show a => a -> FilePath
show ([IBCWrite] -> Int
forall a. [a] -> Int
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 = IBCFile -> Idris IBCFile
forall a. a -> StateT IState (ExceptT Err IO) a
forall (m :: * -> *) a. Monad m => a -> m a
return IBCFile
f { ibc_fixes = d : ibc_fixes f }
ibc IState
i (IBCImp Name
n) IBCFile
f = case Name -> Ctxt [PArg] -> Maybe [PArg]
forall a. Name -> Ctxt a -> Maybe a
lookupCtxtExact Name
n (IState -> Ctxt [PArg]
idris_implicits IState
i) of
                        Just [PArg]
v -> IBCFile -> Idris IBCFile
forall a. a -> StateT IState (ExceptT Err IO) a
forall (m :: * -> *) a. Monad m => a -> m a
return IBCFile
f { ibc_implicits = (n,v): ibc_implicits f     }
                        Maybe [PArg]
_ -> FilePath -> Idris IBCFile
forall a. FilePath -> Idris a
ifail FilePath
"IBC write failed"
ibc IState
i (IBCStatic Name
n) IBCFile
f
                   = case Name -> Ctxt [Bool] -> Maybe [Bool]
forall a. Name -> Ctxt a -> Maybe a
lookupCtxtExact Name
n (IState -> Ctxt [Bool]
idris_statics IState
i) of
                        Just [Bool]
v -> IBCFile -> Idris IBCFile
forall a. a -> StateT IState (ExceptT Err IO) a
forall (m :: * -> *) a. Monad m => a -> m a
return IBCFile
f { ibc_statics = (n,v): ibc_statics f     }
                        Maybe [Bool]
_ -> FilePath -> Idris IBCFile
forall a. FilePath -> Idris a
ifail FilePath
"IBC write failed"
ibc IState
i (IBCInterface Name
n) IBCFile
f
                   = case Name -> Ctxt InterfaceInfo -> Maybe InterfaceInfo
forall a. Name -> Ctxt a -> Maybe a
lookupCtxtExact Name
n (IState -> Ctxt InterfaceInfo
idris_interfaces IState
i) of
                        Just InterfaceInfo
v -> IBCFile -> Idris IBCFile
forall a. a -> StateT IState (ExceptT Err IO) a
forall (m :: * -> *) a. Monad m => a -> m a
return IBCFile
f { ibc_interfaces = (n,v): ibc_interfaces f     }
                        Maybe InterfaceInfo
_ -> FilePath -> Idris IBCFile
forall a. FilePath -> Idris a
ifail FilePath
"IBC write failed"
ibc IState
i (IBCRecord Name
n) IBCFile
f
                   = case Name -> Ctxt RecordInfo -> Maybe RecordInfo
forall a. Name -> Ctxt a -> Maybe a
lookupCtxtExact Name
n (IState -> Ctxt RecordInfo
idris_records IState
i) of
                        Just RecordInfo
v -> IBCFile -> Idris IBCFile
forall a. a -> StateT IState (ExceptT Err IO) a
forall (m :: * -> *) a. Monad m => a -> m a
return IBCFile
f { ibc_records = (n,v): ibc_records f     }
                        Maybe RecordInfo
_ -> FilePath -> Idris IBCFile
forall a. FilePath -> Idris a
ifail FilePath
"IBC write failed"
ibc IState
i (IBCImplementation Bool
int Bool
res Name
n Name
ins) IBCFile
f
                   = IBCFile -> Idris IBCFile
forall a. a -> StateT IState (ExceptT Err IO) a
forall (m :: * -> *) a. Monad m => a -> m a
return IBCFile
f { ibc_implementations = (int, res, n, ins) : ibc_implementations f }
ibc IState
i (IBCDSL Name
n) IBCFile
f
                   = case Name -> Ctxt DSL -> Maybe DSL
forall a. Name -> Ctxt a -> Maybe a
lookupCtxtExact Name
n (IState -> Ctxt DSL
idris_dsls IState
i) of
                        Just DSL
v -> IBCFile -> Idris IBCFile
forall a. a -> StateT IState (ExceptT Err IO) a
forall (m :: * -> *) a. Monad m => a -> m a
return IBCFile
f { ibc_dsls = (n,v): ibc_dsls f     }
                        Maybe DSL
_ -> FilePath -> Idris IBCFile
forall a. FilePath -> Idris a
ifail FilePath
"IBC write failed"
ibc IState
i (IBCData Name
n) IBCFile
f
                   = case Name -> Ctxt TypeInfo -> Maybe TypeInfo
forall a. Name -> Ctxt a -> Maybe a
lookupCtxtExact Name
n (IState -> Ctxt TypeInfo
idris_datatypes IState
i) of
                        Just TypeInfo
v -> IBCFile -> Idris IBCFile
forall a. a -> StateT IState (ExceptT Err IO) a
forall (m :: * -> *) a. Monad m => a -> m a
return IBCFile
f { ibc_datatypes = (n,v): ibc_datatypes f     }
                        Maybe TypeInfo
_ -> FilePath -> Idris IBCFile
forall a. FilePath -> Idris a
ifail FilePath
"IBC write failed"
ibc IState
i (IBCOpt Name
n) IBCFile
f = case Name -> Ctxt OptInfo -> Maybe OptInfo
forall a. Name -> Ctxt a -> Maybe a
lookupCtxtExact Name
n (IState -> Ctxt OptInfo
idris_optimisation IState
i) of
                        Just OptInfo
v -> IBCFile -> Idris IBCFile
forall a. a -> StateT IState (ExceptT Err IO) a
forall (m :: * -> *) a. Monad m => a -> m a
return IBCFile
f { ibc_optimise = (n,v): ibc_optimise f     }
                        Maybe OptInfo
_ -> FilePath -> Idris IBCFile
forall a. FilePath -> Idris a
ifail FilePath
"IBC write failed"
ibc IState
i (IBCSyntax Syntax
n) IBCFile
f = IBCFile -> Idris IBCFile
forall a. a -> StateT IState (ExceptT Err IO) a
forall (m :: * -> *) a. Monad m => a -> m a
return IBCFile
f { ibc_syntax = n : ibc_syntax f }
ibc IState
i (IBCKeyword FilePath
n) IBCFile
f = IBCFile -> Idris IBCFile
forall a. a -> StateT IState (ExceptT Err IO) a
forall (m :: * -> *) a. Monad m => a -> m a
return IBCFile
f { ibc_keywords = n : ibc_keywords f }
ibc IState
i (IBCImport (Bool, FilePath)
n) IBCFile
f = IBCFile -> Idris IBCFile
forall a. a -> StateT IState (ExceptT Err IO) a
forall (m :: * -> *) a. Monad m => a -> m a
return IBCFile
f { ibc_imports = n : ibc_imports f }
ibc IState
i (IBCImportDir FilePath
n) IBCFile
f = IBCFile -> Idris IBCFile
forall a. a -> StateT IState (ExceptT Err IO) a
forall (m :: * -> *) a. Monad m => a -> m a
return IBCFile
f { ibc_importdirs = n : ibc_importdirs f }
ibc IState
i (IBCSourceDir FilePath
n) IBCFile
f = IBCFile -> Idris IBCFile
forall a. a -> StateT IState (ExceptT Err IO) a
forall (m :: * -> *) a. Monad m => a -> m a
return IBCFile
f { ibc_sourcedirs = n : ibc_sourcedirs f }
ibc IState
i (IBCObj Codegen
tgt FilePath
n) IBCFile
f = IBCFile -> Idris IBCFile
forall a. a -> StateT IState (ExceptT Err IO) a
forall (m :: * -> *) a. Monad m => a -> m a
return IBCFile
f { ibc_objs = (tgt, n) : ibc_objs f }
ibc IState
i (IBCLib Codegen
tgt FilePath
n) IBCFile
f = IBCFile -> Idris IBCFile
forall a. a -> StateT IState (ExceptT Err IO) a
forall (m :: * -> *) a. Monad m => a -> m a
return IBCFile
f { ibc_libs = (tgt, n) : ibc_libs f }
ibc IState
i (IBCCGFlag Codegen
tgt FilePath
n) IBCFile
f = IBCFile -> Idris IBCFile
forall a. a -> StateT IState (ExceptT Err IO) a
forall (m :: * -> *) a. Monad m => a -> m a
return IBCFile
f { ibc_cgflags = (tgt, n) : ibc_cgflags f }
ibc IState
i (IBCDyLib FilePath
n) IBCFile
f = IBCFile -> Idris IBCFile
forall a. a -> StateT IState (ExceptT Err IO) a
forall (m :: * -> *) a. Monad m => a -> m a
return IBCFile
f {ibc_dynamic_libs = n : ibc_dynamic_libs f }
ibc IState
i (IBCHeader Codegen
tgt FilePath
n) IBCFile
f = IBCFile -> Idris IBCFile
forall a. a -> StateT IState (ExceptT Err IO) a
forall (m :: * -> *) a. Monad m => a -> m a
return IBCFile
f { ibc_hdrs = (tgt, n) : ibc_hdrs 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 -> IBCFile -> Idris IBCFile
forall a. a -> StateT IState (ExceptT Err IO) a
forall (m :: * -> *) a. Monad m => a -> m a
return IBCFile
f { ibc_defs = (n,v) : ibc_defs f }
                   Maybe Def
_ -> FilePath -> Idris IBCFile
forall a. FilePath -> Idris a
ifail FilePath
"IBC write failed"
        case Name
-> Ctxt ([([(Name, Term)], Term, Term)], [PTerm])
-> Maybe ([([(Name, Term)], Term, Term)], [PTerm])
forall a. Name -> Ctxt a -> Maybe a
lookupCtxtExact Name
n (IState -> Ctxt ([([(Name, Term)], Term, Term)], [PTerm])
idris_patdefs IState
i) of
                   Just ([([(Name, Term)], Term, Term)], [PTerm])
v -> IBCFile -> Idris IBCFile
forall a. a -> StateT IState (ExceptT Err IO) a
forall (m :: * -> *) a. Monad m => a -> m a
return IBCFile
f' { ibc_patdefs = (n,v) : ibc_patdefs f }
                   Maybe ([([(Name, Term)], Term, Term)], [PTerm])
_ -> IBCFile -> Idris IBCFile
forall a. a -> StateT IState (ExceptT Err IO) a
forall (m :: * -> *) a. Monad m => a -> m a
return IBCFile
f' -- Not a pattern definition

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

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

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

                                                Just FilePath
ploc -> [FilePath] -> FilePath
unwords [FilePath
"Please reinstall:", [FilePath] -> FilePath
forall a. HasCallStack => [a] -> a
L.head ([FilePath] -> FilePath) -> [FilePath] -> FilePath
forall a b. (a -> b) -> a -> b
$ FilePath -> [FilePath]
splitDirectories FilePath
ploc]
                                    FilePath -> Idris ()
forall a. FilePath -> Idris a
ifail (FilePath -> Idris ()) -> FilePath -> Idris ()
forall a b. (a -> b) -> a -> b
$ [FilePath] -> FilePath
unlines [ [FilePath] -> FilePath
unwords [FilePath
"Incompatible ibc version for:", ShowS
forall a. Show a => a -> FilePath
show FilePath
fn]
                                                    , [FilePath] -> FilePath
unwords [FilePath
start
                                                              , FilePath
"was built with"
                                                              , FilePath
e
                                                              , FilePath
"version of Idris."]
                                                    , FilePath
end
                                                    ]
                FilePath
source <- FilePath -> FilePath -> Archive -> Idris FilePath
forall b.
(Binary b, NFData b) =>
b -> FilePath -> Archive -> Idris b
getEntry FilePath
"" FilePath
"sourcefile" Archive
archive
                Bool
srcok <- IO Bool -> Idris Bool
forall a. IO a -> Idris a
runIO (IO Bool -> Idris Bool) -> IO Bool -> Idris Bool
forall a b. (a -> b) -> a -> b
$ FilePath -> IO Bool
doesFileExist FilePath
source
                Bool -> Idris () -> Idris ()
forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
when Bool
srcok (Idris () -> Idris ()) -> Idris () -> Idris ()
forall a b. (a -> b) -> a -> b
$ FilePath -> FilePath -> Idris ()
timestampOlder FilePath
source FilePath
fn
                Archive -> Idris ()
processImportDirs Archive
archive
                Archive -> Idris ()
processSourceDirs Archive
archive
                Bool -> IBCPhase -> FilePath -> Archive -> Idris ()
processImports Bool
reexp IBCPhase
phase FilePath
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
                FilePath -> Archive -> Idris ()
processObjectFiles FilePath
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 :: FilePath -> FilePath -> Idris ()
timestampOlder FilePath
src FilePath
ibc = do
  UTCTime
srct <- IO UTCTime -> Idris UTCTime
forall a. IO a -> Idris a
runIO (IO UTCTime -> Idris UTCTime) -> IO UTCTime -> Idris UTCTime
forall a b. (a -> b) -> a -> b
$ FilePath -> IO UTCTime
getModificationTime FilePath
src
  UTCTime
ibct <- IO UTCTime -> Idris UTCTime
forall a. IO a -> Idris a
runIO (IO UTCTime -> Idris UTCTime) -> IO UTCTime -> Idris UTCTime
forall a b. (a -> b) -> a -> b
$ FilePath -> IO UTCTime
getModificationTime FilePath
ibc
  if (UTCTime
srct UTCTime -> UTCTime -> Bool
forall a. Ord a => a -> a -> Bool
> UTCTime
ibct)
    then FilePath -> Idris ()
forall a. FilePath -> Idris a
ifail (FilePath -> Idris ()) -> FilePath -> Idris ()
forall a b. (a -> b) -> a -> b
$ [FilePath] -> FilePath
unlines [ FilePath
"Module needs reloading:"
                         , [FilePath] -> FilePath
unwords [FilePath
"\tSRC :", ShowS
forall a. Show a => a -> FilePath
show FilePath
src]
                         , [FilePath] -> FilePath
unwords [FilePath
"\tModified at:", UTCTime -> FilePath
forall a. Show a => a -> FilePath
show UTCTime
srct]
                         , [FilePath] -> FilePath
unwords [FilePath
"\tIBC :", ShowS
forall a. Show a => a -> FilePath
show FilePath
ibc]
                         , [FilePath] -> FilePath
unwords [FilePath
"\tModified at:", UTCTime -> FilePath
forall a. Show a => a -> FilePath
show UTCTime
ibct]
                         ]
    else () -> Idris ()
forall a. a -> StateT IState (ExceptT Err IO) a
forall (m :: * -> *) a. Monad m => a -> m a
return ()

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

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

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

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

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

processAutoHints :: Archive -> Idris ()
processAutoHints :: Archive -> Idris ()
processAutoHints Archive
ar = do
    [(Name, Name)]
ns <- [(Name, Name)] -> FilePath -> Archive -> Idris [(Name, Name)]
forall b.
(Binary b, NFData b) =>
b -> FilePath -> Archive -> Idris b
getEntry [] FilePath
"ibc_autohints" Archive
ar
    ((Name, Name) -> Idris ()) -> [(Name, Name)] -> Idris ()
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, FilePath)]
ns <-  [(Name, FilePath)]
-> FilePath -> Archive -> Idris [(Name, FilePath)]
forall b.
(Binary b, NFData b) =>
b -> FilePath -> Archive -> Idris b
getEntry [] FilePath
"ibc_deprecated" Archive
ar
    ((Name, FilePath) -> Idris ()) -> [(Name, FilePath)] -> Idris ()
forall (t :: * -> *) (m :: * -> *) a b.
(Foldable t, Monad m) =>
(a -> m b) -> t a -> m ()
mapM_ (\(Name
n,FilePath
reason) -> Name -> FilePath -> Idris ()
addDeprecated Name
n FilePath
reason) [(Name, FilePath)]
ns

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

processConstraints :: Archive -> Idris ()
processConstraints :: Archive -> Idris ()
processConstraints Archive
ar = do
    [(FC, UConstraint)]
cs <- [(FC, UConstraint)]
-> FilePath -> Archive -> Idris [(FC, UConstraint)]
forall b.
(Binary b, NFData b) =>
b -> FilePath -> Archive -> Idris b
getEntry [] FilePath
"ibc_constraints" Archive
ar
    ((FC, UConstraint) -> Idris ()) -> [(FC, UConstraint)] -> Idris ()
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
    [FilePath]
fs <- [FilePath] -> FilePath -> Archive -> Idris [FilePath]
forall b.
(Binary b, NFData b) =>
b -> FilePath -> Archive -> Idris b
getEntry [] FilePath
"ibc_importdirs" Archive
ar
    (FilePath -> Idris ()) -> [FilePath] -> Idris ()
forall (t :: * -> *) (m :: * -> *) a b.
(Foldable t, Monad m) =>
(a -> m b) -> t a -> m ()
mapM_ FilePath -> Idris ()
addImportDir [FilePath]
fs

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

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

processImplicits :: Archive -> Idris ()
processImplicits :: Archive -> Idris ()
processImplicits Archive
ar = do
    [(Name, [PArg])]
imps <- [(Name, [PArg])] -> FilePath -> Archive -> Idris [(Name, [PArg])]
forall b.
(Binary b, NFData b) =>
b -> FilePath -> Archive -> Idris b
getEntry [] FilePath
"ibc_implicits" Archive
ar
    ((Name, [PArg]) -> Idris ()) -> [(Name, [PArg])] -> Idris ()
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) -> () -> Idris ()
forall a. a -> StateT IState (ExceptT Err IO) a
forall (m :: * -> *) a. Monad m => a -> m a
return ()
            Just (Def
n, Accessibility
Private) -> () -> Idris ()
forall a. a -> StateT IState (ExceptT Err IO) a
forall (m :: * -> *) a. Monad m => a -> m a
return ()
            Maybe (Def, Accessibility)
_ -> IState -> Idris ()
putIState (IState
i { idris_implicits = addDef n imp (idris_implicits i) })) [(Name, [PArg])]
imps

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

processStatics :: Archive -> Idris ()
processStatics :: Archive -> Idris ()
processStatics Archive
ar = do
    [(Name, [Bool])]
ss <- [(Name, [Bool])] -> FilePath -> Archive -> Idris [(Name, [Bool])]
forall b.
(Binary b, NFData b) =>
b -> FilePath -> Archive -> Idris b
getEntry [] FilePath
"ibc_statics" Archive
ar
    ((Name, [Bool]) -> Idris ()) -> [(Name, [Bool])] -> Idris ()
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 = addDef n s (idris_statics i) })) [(Name, [Bool])]
ss

processInterfaces :: Archive -> Idris ()
processInterfaces :: Archive -> Idris ()
processInterfaces Archive
ar = do
    [(Name, InterfaceInfo)]
cs <- [(Name, InterfaceInfo)]
-> FilePath -> Archive -> Idris [(Name, InterfaceInfo)]
forall b.
(Binary b, NFData b) =>
b -> FilePath -> Archive -> Idris b
getEntry [] FilePath
"ibc_interfaces" Archive
ar
    ((Name, InterfaceInfo) -> Idris ())
-> [(Name, InterfaceInfo)] -> Idris ()
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 Name -> Ctxt InterfaceInfo -> Maybe InterfaceInfo
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 = interface_implementations c ++ is }
        IState -> Idris ()
putIState (IState
i { idris_interfaces = addDef n c' (idris_interfaces i) })) [(Name, InterfaceInfo)]
cs

processRecords :: Archive -> Idris ()
processRecords :: Archive -> Idris ()
processRecords Archive
ar = do
    [(Name, RecordInfo)]
rs <- [(Name, RecordInfo)]
-> FilePath -> Archive -> Idris [(Name, RecordInfo)]
forall b.
(Binary b, NFData b) =>
b -> FilePath -> Archive -> Idris b
getEntry [] FilePath
"ibc_records" Archive
ar
    ((Name, RecordInfo) -> Idris ())
-> [(Name, RecordInfo)] -> Idris ()
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 = addDef n r (idris_records i) })) [(Name, RecordInfo)]
rs

processImplementations :: Archive -> Idris ()
processImplementations :: Archive -> Idris ()
processImplementations Archive
ar = do
    [(Bool, Bool, Name, Name)]
cs <- [(Bool, Bool, Name, Name)]
-> FilePath -> Archive -> Idris [(Bool, Bool, Name, Name)]
forall b.
(Binary b, NFData b) =>
b -> FilePath -> Archive -> Idris b
getEntry [] FilePath
"ibc_implementations" Archive
ar
    ((Bool, Bool, Name, Name) -> Idris ())
-> [(Bool, Bool, Name, Name)] -> Idris ()
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 <- [(Name, DSL)] -> FilePath -> Archive -> Idris [(Name, DSL)]
forall b.
(Binary b, NFData b) =>
b -> FilePath -> Archive -> Idris b
getEntry [] FilePath
"ibc_dsls" Archive
ar
    ((Name, DSL) -> Idris ()) -> [(Name, DSL)] -> Idris ()
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 = addDef n c (idris_dsls i) })) [(Name, DSL)]
cs

processDatatypes :: Archive -> Idris ()
processDatatypes :: Archive -> Idris ()
processDatatypes Archive
ar = do
    [(Name, TypeInfo)]
cs <- [(Name, TypeInfo)]
-> FilePath -> Archive -> Idris [(Name, TypeInfo)]
forall b.
(Binary b, NFData b) =>
b -> FilePath -> Archive -> Idris b
getEntry [] FilePath
"ibc_datatypes" Archive
ar
    ((Name, TypeInfo) -> Idris ()) -> [(Name, TypeInfo)] -> Idris ()
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 = addDef n c (idris_datatypes i) })) [(Name, TypeInfo)]
cs

processOptimise :: Archive -> Idris ()
processOptimise :: Archive -> Idris ()
processOptimise Archive
ar = do
    [(Name, OptInfo)]
cs <- [(Name, OptInfo)] -> FilePath -> Archive -> Idris [(Name, OptInfo)]
forall b.
(Binary b, NFData b) =>
b -> FilePath -> Archive -> Idris b
getEntry [] FilePath
"ibc_optimise" Archive
ar
    ((Name, OptInfo) -> Idris ()) -> [(Name, OptInfo)] -> Idris ()
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 = addDef n c (idris_optimisation i) })) [(Name, OptInfo)]
cs

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

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

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

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

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

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

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

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

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

        updateOrig :: Either Term (Term, Term)
-> StateT IState (ExceptT Err IO) (Either Term (Term, Term))
updateOrig (Left Term
t) = (Term -> Either Term (Term, Term))
-> StateT IState (ExceptT Err IO) Term
-> StateT IState (ExceptT Err IO) (Either Term (Term, Term))
forall (m :: * -> *) a1 r. Monad m => (a1 -> r) -> m a1 -> m r
liftM Term -> Either Term (Term, Term)
forall a b. a -> Either a b
Left (Term -> StateT IState (ExceptT Err IO) Term
update Term
t)
        updateOrig (Right (Term
l, Term
r)) = do
            Term
l' <- Term -> StateT IState (ExceptT Err IO) Term
update Term
l
            Term
r' <- Term -> StateT IState (ExceptT Err IO) Term
update Term
r
            Either Term (Term, Term)
-> StateT IState (ExceptT Err IO) (Either Term (Term, Term))
forall a. a -> StateT IState (ExceptT Err IO) a
forall (m :: * -> *) a. Monad m => a -> m a
return (Either Term (Term, Term)
 -> StateT IState (ExceptT Err IO) (Either Term (Term, Term)))
-> Either Term (Term, Term)
-> StateT IState (ExceptT Err IO) (Either Term (Term, Term))
forall a b. (a -> b) -> a -> b
$ (Term, Term) -> Either Term (Term, Term)
forall a b. b -> Either a b
Right (Term
l', Term
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
            CaseDefs -> StateT IState (ExceptT Err IO) CaseDefs
forall a. a -> StateT IState (ExceptT Err IO) a
forall (m :: * -> *) a. Monad m => a -> m a
return (CaseDefs -> StateT IState (ExceptT Err IO) CaseDefs)
-> CaseDefs -> StateT IState (ExceptT Err IO) CaseDefs
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' Term]
alts) = do
            [CaseAlt' Term]
alts' <- (CaseAlt' Term -> StateT IState (ExceptT Err IO) (CaseAlt' Term))
-> [CaseAlt' Term]
-> StateT IState (ExceptT Err IO) [CaseAlt' Term]
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
forall (m :: * -> *) a b. Monad m => (a -> m b) -> [a] -> m [b]
mapM CaseAlt' Term -> StateT IState (ExceptT Err IO) (CaseAlt' Term)
updateAlt [CaseAlt' Term]
alts
            SC -> StateT IState (ExceptT Err IO) SC
forall a. a -> StateT IState (ExceptT Err IO) a
forall (m :: * -> *) a. Monad m => a -> m a
return (CaseType -> Name -> [CaseAlt' Term] -> SC
forall t. CaseType -> Name -> [CaseAlt' t] -> SC' t
Case CaseType
t Name
n [CaseAlt' Term]
alts')
        updateSC (ProjCase Term
t [CaseAlt' Term]
alts) = do
            [CaseAlt' Term]
alts' <- (CaseAlt' Term -> StateT IState (ExceptT Err IO) (CaseAlt' Term))
-> [CaseAlt' Term]
-> StateT IState (ExceptT Err IO) [CaseAlt' Term]
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
forall (m :: * -> *) a b. Monad m => (a -> m b) -> [a] -> m [b]
mapM CaseAlt' Term -> StateT IState (ExceptT Err IO) (CaseAlt' Term)
updateAlt [CaseAlt' Term]
alts
            SC -> StateT IState (ExceptT Err IO) SC
forall a. a -> StateT IState (ExceptT Err IO) a
forall (m :: * -> *) a. Monad m => a -> m a
return (Term -> [CaseAlt' Term] -> SC
forall t. t -> [CaseAlt' t] -> SC' t
ProjCase Term
t [CaseAlt' Term]
alts')
        updateSC (STerm Term
t) = do
            Term
t' <- Term -> StateT IState (ExceptT Err IO) Term
update Term
t
            SC -> StateT IState (ExceptT Err IO) SC
forall a. a -> StateT IState (ExceptT Err IO) a
forall (m :: * -> *) a. Monad m => a -> m a
return (Term -> SC
forall t. t -> SC' t
STerm Term
t')
        updateSC SC
c = SC -> StateT IState (ExceptT Err IO) SC
forall a. a -> StateT IState (ExceptT Err IO) a
forall (m :: * -> *) a. Monad m => a -> m a
return SC
c

        updateAlt :: CaseAlt' Term -> StateT IState (ExceptT Err IO) (CaseAlt' Term)
updateAlt (ConCase Name
n Int
i [Name]
ns SC
t) = do
            SC
t' <- SC -> StateT IState (ExceptT Err IO) SC
updateSC SC
t
            CaseAlt' Term -> StateT IState (ExceptT Err IO) (CaseAlt' Term)
forall a. a -> StateT IState (ExceptT Err IO) a
forall (m :: * -> *) a. Monad m => a -> m a
return (Name -> Int -> [Name] -> SC -> CaseAlt' Term
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
            CaseAlt' Term -> StateT IState (ExceptT Err IO) (CaseAlt' Term)
forall a. a -> StateT IState (ExceptT Err IO) a
forall (m :: * -> *) a. Monad m => a -> m a
return (Name -> [Name] -> SC -> CaseAlt' Term
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
            CaseAlt' Term -> StateT IState (ExceptT Err IO) (CaseAlt' Term)
forall a. a -> StateT IState (ExceptT Err IO) a
forall (m :: * -> *) a. Monad m => a -> m a
return (Const -> SC -> CaseAlt' Term
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
            CaseAlt' Term -> StateT IState (ExceptT Err IO) (CaseAlt' Term)
forall a. a -> StateT IState (ExceptT Err IO) a
forall (m :: * -> *) a. Monad m => a -> m a
return (Name -> SC -> CaseAlt' Term
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
            CaseAlt' Term -> StateT IState (ExceptT Err IO) (CaseAlt' Term)
forall a. a -> StateT IState (ExceptT Err IO) a
forall (m :: * -> *) a. Monad m => a -> m a
return (SC -> CaseAlt' Term
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 :: Term -> StateT IState (ExceptT Err IO) Term
update Term
t = do
            Maybe Term
tm <- Term -> Idris (Maybe Term)
addTT Term
t
            case Maybe Term
tm of
                Maybe Term
Nothing -> Term -> StateT IState (ExceptT Err IO) Term
update' Term
t
                Just Term
t' -> Term -> StateT IState (ExceptT Err IO) Term
forall a. a -> StateT IState (ExceptT Err IO) a
forall (m :: * -> *) a. Monad m => a -> m a
return Term
t'

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

processDocs :: Archive -> Idris ()
processDocs :: Archive -> Idris ()
processDocs Archive
ar = do
    [(Name, (Docstring DocTerm, [(Name, Docstring DocTerm)]))]
ds <- [(Name, (Docstring DocTerm, [(Name, Docstring DocTerm)]))]
-> FilePath
-> Archive
-> Idris [(Name, (Docstring DocTerm, [(Name, Docstring DocTerm)]))]
forall b.
(Binary b, NFData b) =>
b -> FilePath -> Archive -> Idris b
getEntry [] FilePath
"ibc_docstrings" Archive
ar
    ((Name, (Docstring DocTerm, [(Name, Docstring DocTerm)]))
 -> Idris ())
-> [(Name, (Docstring DocTerm, [(Name, Docstring DocTerm)]))]
-> Idris ()
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 ((Docstring DocTerm, [(Name, Docstring DocTerm)])
-> Docstring DocTerm
forall a b. (a, b) -> a
fst (Docstring DocTerm, [(Name, Docstring DocTerm)])
a) ((Docstring DocTerm, [(Name, Docstring DocTerm)])
-> [(Name, Docstring DocTerm)]
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 <- [(Name, Docstring DocTerm)]
-> FilePath -> Archive -> Idris [(Name, Docstring DocTerm)]
forall b.
(Binary b, NFData b) =>
b -> FilePath -> Archive -> Idris b
getEntry [] FilePath
"ibc_moduledocs" Archive
ar
    ((Name, Docstring DocTerm) -> Idris ())
-> [(Name, Docstring DocTerm)] -> Idris ()
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 = addDef n d (idris_moduledocs 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 -> FilePath -> Idris ()
logIBC Int
3 (FilePath -> Idris ()) -> FilePath -> Idris ()
forall a b. (a -> b) -> a -> b
$ FilePath
"processAccess (reexp, phase)" FilePath -> ShowS
forall a. [a] -> [a] -> [a]
++ (Bool, IBCPhase) -> FilePath
forall a. Show a => a -> FilePath
show (Bool
reexp, IBCPhase
phase)
    [(Name, Accessibility)]
ds <- [(Name, Accessibility)]
-> FilePath -> Archive -> Idris [(Name, Accessibility)]
forall b.
(Binary b, NFData b) =>
b -> FilePath -> Archive -> Idris b
getEntry [] FilePath
"ibc_access" Archive
ar
    Int -> FilePath -> Idris ()
logIBC Int
3 (FilePath -> Idris ()) -> FilePath -> Idris ()
forall a b. (a -> b) -> a -> b
$ FilePath
"processAccess ds" FilePath -> ShowS
forall a. [a] -> [a] -> [a]
++ [(Name, Accessibility)] -> FilePath
forall a. Show a => a -> FilePath
show [(Name, Accessibility)]
ds
    ((Name, Accessibility) -> Idris ())
-> [(Name, Accessibility)] -> Idris ()
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 -> FilePath -> Idris ()
logIBC Int
3 (FilePath -> Idris ()) -> FilePath -> Idris ()
forall a b. (a -> b) -> a -> b
$ FilePath
"Setting " FilePath -> ShowS
forall a. [a] -> [a] -> [a]
++ (Accessibility, Name) -> FilePath
forall a. Show a => a -> FilePath
show (Accessibility
a, Name
n) FilePath -> ShowS
forall a. [a] -> [a] -> [a]
++ FilePath
" to " FilePath -> ShowS
forall a. [a] -> [a] -> [a]
++ Accessibility -> FilePath
forall a. Show a => a -> FilePath
show Accessibility
a
        (IState -> IState) -> Idris ()
updateIState (\IState
i -> IState
i { tt_ctxt = setAccess n a (tt_ctxt i) })

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

        -- Everything should be available at the REPL from
        -- things imported publicly.
        Bool -> Idris () -> Idris ()
forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
when (IBCPhase
phase IBCPhase -> IBCPhase -> Bool
forall a. Eq a => a -> a -> Bool
== Bool -> IBCPhase
IBC_REPL Bool
True) (Idris () -> Idris ()) -> Idris () -> Idris ()
forall a b. (a -> b) -> a -> b
$ do
            Int -> FilePath -> Idris ()
logIBC Int
2 (FilePath -> Idris ()) -> FilePath -> Idris ()
forall a b. (a -> b) -> a -> b
$ FilePath
"Top level, exporting " FilePath -> ShowS
forall a. [a] -> [a] -> [a]
++ Name -> FilePath
forall a. Show a => a -> FilePath
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, [FnOpt])]
ds <- [(Name, [FnOpt])] -> FilePath -> Archive -> Idris [(Name, [FnOpt])]
forall b.
(Binary b, NFData b) =>
b -> FilePath -> Archive -> Idris b
getEntry [] FilePath
"ibc_flags" Archive
ar
    ((Name, [FnOpt]) -> Idris ()) -> [(Name, [FnOpt])] -> Idris ()
forall (t :: * -> *) (m :: * -> *) a b.
(Foldable t, Monad m) =>
(a -> m b) -> t a -> m ()
mapM_ (\ (Name
n, [FnOpt]
a) -> Name -> [FnOpt] -> Idris ()
setFlags Name
n [FnOpt]
a) [(Name, [FnOpt])]
ds

processFnInfo :: Archive -> Idris ()
processFnInfo :: Archive -> Idris ()
processFnInfo Archive
ar = do
    [(Name, FnInfo)]
ds <- [(Name, FnInfo)] -> FilePath -> Archive -> Idris [(Name, FnInfo)]
forall b.
(Binary b, NFData b) =>
b -> FilePath -> Archive -> Idris b
getEntry [] FilePath
"ibc_fninfo" Archive
ar
    ((Name, FnInfo) -> Idris ()) -> [(Name, FnInfo)] -> Idris ()
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 <- [(Name, Totality)]
-> FilePath -> Archive -> Idris [(Name, Totality)]
forall b.
(Binary b, NFData b) =>
b -> FilePath -> Archive -> Idris b
getEntry [] FilePath
"ibc_total" Archive
ar
    ((Name, Totality) -> Idris ()) -> [(Name, Totality)] -> Idris ()
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 = setTotal n a (tt_ctxt i) })) [(Name, Totality)]
ds

processInjective :: Archive -> Idris ()
processInjective :: Archive -> Idris ()
processInjective Archive
ar = do
    [(Name, Bool)]
ds <- [(Name, Bool)] -> FilePath -> Archive -> Idris [(Name, Bool)]
forall b.
(Binary b, NFData b) =>
b -> FilePath -> Archive -> Idris b
getEntry [] FilePath
"ibc_injective" Archive
ar
    ((Name, Bool) -> Idris ()) -> [(Name, Bool)] -> Idris ()
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 = setInjective n a (tt_ctxt i) })) [(Name, Bool)]
ds

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

processCallgraph :: Archive -> Idris ()
processCallgraph :: Archive -> Idris ()
processCallgraph Archive
ar = do
    [(Name, CGInfo)]
ds <- [(Name, CGInfo)] -> FilePath -> Archive -> Idris [(Name, CGInfo)]
forall b.
(Binary b, NFData b) =>
b -> FilePath -> Archive -> Idris b
getEntry [] FilePath
"ibc_cg" Archive
ar
    ((Name, CGInfo) -> Idris ()) -> [(Name, CGInfo)] -> Idris ()
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 <- [Name] -> FilePath -> Archive -> Idris [Name]
forall b.
(Binary b, NFData b) =>
b -> FilePath -> Archive -> Idris b
getEntry [] FilePath
"ibc_coercions" Archive
ar
    (Name -> Idris ()) -> [Name] -> Idris ()
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, (Term, Term))]
ts <- [(Name, (Term, Term))]
-> FilePath -> Archive -> Idris [(Name, (Term, Term))]
forall b.
(Binary b, NFData b) =>
b -> FilePath -> Archive -> Idris b
getEntry [] FilePath
"ibc_transforms" Archive
ar
    ((Name, (Term, Term)) -> Idris ())
-> [(Name, (Term, Term))] -> Idris ()
forall (t :: * -> *) (m :: * -> *) a b.
(Foldable t, Monad m) =>
(a -> m b) -> t a -> m ()
mapM_ (\ (Name
n, (Term, Term)
t) -> Name -> (Term, Term) -> Idris ()
addTrans Name
n (Term, Term)
t) [(Name, (Term, Term))]
ts

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

processErrReduce :: Archive -> Idris ()
processErrReduce :: Archive -> Idris ()
processErrReduce Archive
ar = do
    [Name]
ts <- [Name] -> FilePath -> Archive -> Idris [Name]
forall b.
(Binary b, NFData b) =>
b -> FilePath -> Archive -> Idris b
getEntry [] FilePath
"ibc_errReduce" Archive
ar
    (Name -> Idris ()) -> [Name] -> Idris ()
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
    [(FilePath, Int, PTerm)]
ls <- [(FilePath, Int, PTerm)]
-> FilePath -> Archive -> Idris [(FilePath, Int, PTerm)]
forall b.
(Binary b, NFData b) =>
b -> FilePath -> Archive -> Idris b
getEntry [] FilePath
"ibc_lineapps" Archive
ar
    ((FilePath, Int, PTerm) -> Idris ())
-> [(FilePath, Int, PTerm)] -> Idris ()
forall (t :: * -> *) (m :: * -> *) a b.
(Foldable t, Monad m) =>
(a -> m b) -> t a -> m ()
mapM_ (\ (FilePath
f, Int
i, PTerm
t) -> FilePath -> Int -> PTerm -> Idris ()
addInternalApp FilePath
f Int
i PTerm
t) [(FilePath, Int, PTerm)]
ls

processNameHints :: Archive -> Idris ()
processNameHints :: Archive -> Idris ()
processNameHints Archive
ar = do
    [(Name, Name)]
ns <- [(Name, Name)] -> FilePath -> Archive -> Idris [(Name, Name)]
forall b.
(Binary b, NFData b) =>
b -> FilePath -> Archive -> Idris b
getEntry [] FilePath
"ibc_namehints" Archive
ar
    ((Name, Name) -> Idris ()) -> [(Name, Name)] -> Idris ()
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 <- [(Name, MetaInformation)]
-> FilePath -> Archive -> Idris [(Name, MetaInformation)]
forall b.
(Binary b, NFData b) =>
b -> FilePath -> Archive -> Idris b
getEntry [] FilePath
"ibc_metainformation" Archive
ar
    ((Name, MetaInformation) -> Idris ())
-> [(Name, MetaInformation)] -> Idris ()
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 = setMetaInformation n m (tt_ctxt i) })) [(Name, MetaInformation)]
ds

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

processFunctionErrorHandlers :: Archive -> Idris ()
processFunctionErrorHandlers :: Archive -> Idris ()
processFunctionErrorHandlers Archive
ar = do
    [(Name, Name, Name)]
ns <- [(Name, Name, Name)]
-> FilePath -> Archive -> Idris [(Name, Name, Name)]
forall b.
(Binary b, NFData b) =>
b -> FilePath -> Archive -> Idris b
getEntry [] FilePath
"ibc_function_errorhandlers" Archive
ar
    ((Name, Name, Name) -> Idris ())
-> [(Name, Name, Name)] -> Idris ()
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 <- [(Name, (Maybe Name, Int, [Name], Bool, Bool))]
-> FilePath
-> Archive
-> Idris [(Name, (Maybe Name, Int, [Name], Bool, Bool))]
forall b.
(Binary b, NFData b) =>
b -> FilePath -> Archive -> Idris b
getEntry [] FilePath
"ibc_metavars" Archive
ar
    (IState -> IState) -> Idris ()
updateIState (\IState
i -> IState
i { idris_metavars = L.reverse ns ++ idris_metavars 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 <- [LanguageExt] -> FilePath -> Archive -> Idris [LanguageExt]
forall b.
(Binary b, NFData b) =>
b -> FilePath -> Archive -> Idris b
getEntry [] FilePath
"ibc_langexts" Archive
ar
         (LanguageExt -> Idris ()) -> [LanguageExt] -> Idris ()
forall (t :: * -> *) (m :: * -> *) a b.
(Foldable t, Monad m) =>
(a -> m b) -> t a -> m ()
mapM_ LanguageExt -> Idris ()
addLangExt [LanguageExt]
ds
processLangExts IBCPhase
_ Archive
_ = () -> Idris ()
forall a. a -> StateT IState (ExceptT Err IO) a
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 [Name] -> Put
forall t. Binary t => t -> Put
put [Name]
x1
--                put x3 -- Already used SCG info for totality check
               Maybe [Name] -> Put
forall t. Binary t => t -> Put
put Maybe [Name]
x2
               [(Int, [(Name, Int)])] -> Put
forall t. Binary t => t -> Put
put [(Int, [(Name, Int)])]
x4
        get :: Get CGInfo
get
          = do [Name]
x1 <- Get [Name]
forall t. Binary t => Get t
get
               Maybe [Name]
x2 <- Get (Maybe [Name])
forall t. Binary t => Get t
get
               [(Int, [(Name, Int)])]
x3 <- Get [(Int, [(Name, Int)])]
forall t. Binary t => Get t
get
               CGInfo -> Get CGInfo
forall a. a -> Get a
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 Term
x1 Term
x2 -> do Word8 -> Put
putWord8 Word8
0
                                     Term -> Put
forall t. Binary t => t -> Put
put Term
x1
                                     Term -> Put
forall t. Binary t => t -> Put
put Term
x2
                TyDecl NameType
x1 Term
x2 -> do Word8 -> Put
putWord8 Word8
1
                                   NameType -> Put
forall t. Binary t => t -> Put
put NameType
x1
                                   Term -> Put
forall t. Binary t => t -> Put
put Term
x2
                -- all primitives just get added at the start, don't write
                Operator Term
x1 Int
x2 [Value] -> Maybe Value
x3 -> do () -> Put
forall a. a -> PutM a
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 Term
x2 [(Term, Bool)]
x3 [Either Term (Term, Term)]
_ [([Name], Term, Term)]
_ CaseDefs
x4 -> do Word8 -> Put
putWord8 Word8
3
                                             CaseInfo -> Put
forall t. Binary t => t -> Put
put CaseInfo
x1
                                             Term -> Put
forall t. Binary t => t -> Put
put Term
x2
                                             [(Term, Bool)] -> Put
forall t. Binary t => t -> Put
put [(Term, Bool)]
x3
                                             CaseDefs -> Put
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 Term
x1 <- Get Term
forall t. Binary t => Get t
get
                           Term
x2 <- Get Term
forall t. Binary t => Get t
get
                           Def -> Get Def
forall a. a -> Get a
forall (m :: * -> *) a. Monad m => a -> m a
return (Term -> Term -> Def
Function Term
x1 Term
x2)
                   Word8
1 -> do NameType
x1 <- Get NameType
forall t. Binary t => Get t
get
                           Term
x2 <- Get Term
forall t. Binary t => Get t
get
                           Def -> Get Def
forall a. a -> Get a
forall (m :: * -> *) a. Monad m => a -> m a
return (NameType -> Term -> Def
TyDecl NameType
x1 Term
x2)
                   -- Operator isn't written, don't read
                   Word8
3 -> do CaseInfo
x1 <- Get CaseInfo
forall t. Binary t => Get t
get
                           Term
x2 <- Get Term
forall t. Binary t => Get t
get
                           [(Term, Bool)]
x3 <- Get [(Term, Bool)]
forall t. Binary t => Get t
get
--                            x4 <- get
                           -- x3 <- get always []
                           CaseDefs
x5 <- Get CaseDefs
forall t. Binary t => Get t
get
                           Def -> Get Def
forall a. a -> Get a
forall (m :: * -> *) a. Monad m => a -> m a
return (CaseInfo
-> Term
-> [(Term, Bool)]
-> [Either Term (Term, Term)]
-> [([Name], Term, Term)]
-> CaseDefs
-> Def
CaseOp CaseInfo
x1 Term
x2 [(Term, Bool)]
x3 [] [] CaseDefs
x5)
                   Word8
_ -> FilePath -> Get Def
forall a. HasCallStack => FilePath -> a
error FilePath
"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
                                [ArgOpt] -> Put
forall t. Binary t => t -> Put
put [ArgOpt]
x1
                                Static -> Put
forall t. Binary t => t -> Put
put Static
x2
                                Bool -> Put
forall t. Binary t => t -> Put
put Bool
x3
                                Maybe ImplicitInfo -> Put
forall t. Binary t => t -> Put
put Maybe ImplicitInfo
x4
                                RigCount -> Put
forall t. Binary t => t -> Put
put RigCount
x5
                Exp [ArgOpt]
x1 Static
x2 Bool
x3 RigCount
x4 ->
                             do Word8 -> Put
putWord8 Word8
1
                                [ArgOpt] -> Put
forall t. Binary t => t -> Put
put [ArgOpt]
x1
                                Static -> Put
forall t. Binary t => t -> Put
put Static
x2
                                Bool -> Put
forall t. Binary t => t -> Put
put Bool
x3
                                RigCount -> Put
forall t. Binary t => t -> Put
put RigCount
x4
                Constraint [ArgOpt]
x1 Static
x2 RigCount
x3 ->
                                    do Word8 -> Put
putWord8 Word8
2
                                       [ArgOpt] -> Put
forall t. Binary t => t -> Put
put [ArgOpt]
x1
                                       Static -> Put
forall t. Binary t => t -> Put
put Static
x2
                                       RigCount -> Put
forall t. Binary t => t -> Put
put RigCount
x3
                TacImp [ArgOpt]
x1 Static
x2 PTerm
x3 RigCount
x4 ->
                                   do Word8 -> Put
putWord8 Word8
3
                                      [ArgOpt] -> Put
forall t. Binary t => t -> Put
put [ArgOpt]
x1
                                      Static -> Put
forall t. Binary t => t -> Put
put Static
x2
                                      PTerm -> Put
forall t. Binary t => t -> Put
put PTerm
x3
                                      RigCount -> Put
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 <- Get [ArgOpt]
forall t. Binary t => Get t
get
                           Static
x2 <- Get Static
forall t. Binary t => Get t
get
                           Bool
x3 <- Get Bool
forall t. Binary t => Get t
get
                           Maybe ImplicitInfo
x4 <- Get (Maybe ImplicitInfo)
forall t. Binary t => Get t
get
                           RigCount
x5 <- Get RigCount
forall t. Binary t => Get t
get
                           Plicity -> Get Plicity
forall a. a -> Get a
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 <- Get [ArgOpt]
forall t. Binary t => Get t
get
                           Static
x2 <- Get Static
forall t. Binary t => Get t
get
                           Bool
x3 <- Get Bool
forall t. Binary t => Get t
get
                           RigCount
x4 <- Get RigCount
forall t. Binary t => Get t
get
                           Plicity -> Get Plicity
forall a. a -> Get a
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 <- Get [ArgOpt]
forall t. Binary t => Get t
get
                           Static
x2 <- Get Static
forall t. Binary t => Get t
get
                           RigCount
x3 <- Get RigCount
forall t. Binary t => Get t
get
                           Plicity -> Get Plicity
forall a. a -> Get a
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 <- Get [ArgOpt]
forall t. Binary t => Get t
get
                           Static
x2 <- Get Static
forall t. Binary t => Get t
get
                           PTerm
x3 <- Get PTerm
forall t. Binary t => Get t
get
                           RigCount
x4 <- Get RigCount
forall t. Binary t => Get t
get
                           Plicity -> Get Plicity
forall a. a -> Get a
forall (m :: * -> *) a. Monad m => a -> m a
return ([ArgOpt] -> Static -> PTerm -> RigCount -> Plicity
TacImp [ArgOpt]
x1 Static
x2 PTerm
x3 RigCount
x4)
                   Word8
_ -> FilePath -> Get Plicity
forall a. HasCallStack => FilePath -> a
error FilePath
"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 [FilePath]
x3 [Name]
x4 [Name]
_ Name -> Name
_ Bool
x5 Bool
x6 Bool
x7 Maybe Int
_ Int
_ DSL
x8 Int
_ Bool
_ Bool
_)
          = do [Using] -> Put
forall t. Binary t => t -> Put
put [Using]
x1
               [(Name, PTerm)] -> Put
forall t. Binary t => t -> Put
put [(Name, PTerm)]
x2
               [FilePath] -> Put
forall t. Binary t => t -> Put
put [FilePath]
x3
               [Name] -> Put
forall t. Binary t => t -> Put
put [Name]
x4
               Bool -> Put
forall t. Binary t => t -> Put
put Bool
x5
               Bool -> Put
forall t. Binary t => t -> Put
put Bool
x6
               Bool -> Put
forall t. Binary t => t -> Put
put Bool
x7
               DSL -> Put
forall t. Binary t => t -> Put
put DSL
x8
        get :: Get SyntaxInfo
get
          = do [Using]
x1 <- Get [Using]
forall t. Binary t => Get t
get
               [(Name, PTerm)]
x2 <- Get [(Name, PTerm)]
forall t. Binary t => Get t
get
               [FilePath]
x3 <- Get [FilePath]
forall t. Binary t => Get t
get
               [Name]
x4 <- Get [Name]
forall t. Binary t => Get t
get
               Bool
x5 <- Get Bool
forall t. Binary t => Get t
get
               Bool
x6 <- Get Bool
forall t. Binary t => Get t
get
               Bool
x7 <- Get Bool
forall t. Binary t => Get t
get
               DSL
x8 <- Get DSL
forall t. Binary t => Get t
get
               SyntaxInfo -> Get SyntaxInfo
forall a. a -> Get a
forall (m :: * -> *) a. Monad m => a -> m a
return ([Using]
-> [(Name, PTerm)]
-> [FilePath]
-> [Name]
-> [Name]
-> (Name -> Name)
-> Bool
-> Bool
-> Bool
-> Maybe Int
-> Int
-> DSL
-> Int
-> Bool
-> Bool
-> SyntaxInfo
Syn [Using]
x1 [(Name, PTerm)]
x2 [FilePath]
x3 [Name]
x4 [] Name -> Name
forall a. a -> a
id Bool
x5 Bool
x6 Bool
x7 Maybe Int
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, [FnOpt], PTerm))]
x2 [(Name, (Name, PDecl))]
x3 [PDecl]
x4 [Name]
x5 [Name]
x6 [PTerm]
x7 [(Name, Bool)]
_ [Int]
x8)
          = do Name -> Put
forall t. Binary t => t -> Put
put Name
x1
               [(Name, (Bool, [FnOpt], PTerm))] -> Put
forall t. Binary t => t -> Put
put [(Name, (Bool, [FnOpt], PTerm))]
x2
               [(Name, (Name, PDecl))] -> Put
forall t. Binary t => t -> Put
put [(Name, (Name, PDecl))]
x3
               [PDecl] -> Put
forall t. Binary t => t -> Put
put [PDecl]
x4
               [Name] -> Put
forall t. Binary t => t -> Put
put [Name]
x5
               [Name] -> Put
forall t. Binary t => t -> Put
put [Name]
x6
               [PTerm] -> Put
forall t. Binary t => t -> Put
put [PTerm]
x7
               [Int] -> Put
forall t. Binary t => t -> Put
put [Int]
x8
        get :: Get InterfaceInfo
get
          = do Name
x1 <- Get Name
forall t. Binary t => Get t
get
               [(Name, (Bool, [FnOpt], PTerm))]
x2 <- Get [(Name, (Bool, [FnOpt], PTerm))]
forall t. Binary t => Get t
get
               [(Name, (Name, PDecl))]
x3 <- Get [(Name, (Name, PDecl))]
forall t. Binary t => Get t
get
               [PDecl]
x4 <- Get [PDecl]
forall t. Binary t => Get t
get
               [Name]
x5 <- Get [Name]
forall t. Binary t => Get t
get
               [Name]
x6 <- Get [Name]
forall t. Binary t => Get t
get
               [PTerm]
x7 <- Get [PTerm]
forall t. Binary t => Get t
get
               [Int]
x8 <- Get [Int]
forall t. Binary t => Get t
get
               InterfaceInfo -> Get InterfaceInfo
forall a. a -> Get a
forall (m :: * -> *) a. Monad m => a -> m a
return (Name
-> [(Name, (Bool, [FnOpt], PTerm))]
-> [(Name, (Name, PDecl))]
-> [PDecl]
-> [Name]
-> [Name]
-> [PTerm]
-> [(Name, Bool)]
-> [Int]
-> InterfaceInfo
CI Name
x1 [(Name, (Bool, [FnOpt], 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