{-|
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
  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 toArchiveOrFail 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 ver <- Word16 -> FilePath -> Archive -> Idris Word16
forall b.
(Binary b, NFData b) =>
b -> FilePath -> Archive -> Idris b
getEntry Word16
0 FilePath
"ver" Archive
archive
                        return (ver == 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)
                imps <- Idris [(FilePath, Bool)]
getImported
                logIBC 3 $ "loadIBC imps" ++ show imps
                case lookup fp 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
                    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 toArchiveOrFail 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 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 toArchiveOrFail 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 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 toArchiveOrFail 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 ddir <- IO FilePath -> Idris FilePath
forall a. IO a -> Idris a
runIO IO FilePath
getIdrisLibDir
                      addImportDir (ddir </> unPkgName pkg)
                      fp <- findPkgIndex pkg
                      loadIBC True IBC_Building 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
         i <- Idris IState
getIState
         resetNameIdx
         ibc_data <- mkIBC (ibc_write i) (initIBC { sourcefile = src,
                                                    ibc_langexts = idris_language_extensions i })
         let ibcf = IBCFile
ibc_data { iface_hash = calculateHash i ibc_data }
         logIBC 5 $ "Hash for " ++ show f ++ " = " ++ show (iface_hash ibcf)
         idrisCatch (do runIO $ createDirectoryIfMissing True (dropFileName f)
                        writeArchive f ibcf
                        logIBC 2 "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)
         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 i <- Idris IState
getIState
         let 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
         logIBC 2 $ "Writing package index " ++ show f ++ " including\n" ++
                show (map snd imps)
         resetNameIdx
         let ibcf = IBCFile
initIBC { ibc_imports = imps,
                              ibc_langexts = idris_language_extensions i }
         idrisCatch (do runIO $ createDirectoryIfMissing True (dropFileName f)
                        writeArchive f ibcf
                        logIBC 2 "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)
         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 ist <- Idris IState
getIState
                    logIBC 5 $ show i ++ " " ++ show (L.length is)
                    f' <- ibc ist i f
                    mkIBC is 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 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 lookupCtxtExact n (idris_patdefs 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
                ver <- Word16 -> FilePath -> Archive -> Idris Word16
forall b.
(Binary b, NFData b) =>
b -> FilePath -> Archive -> Idris b
getEntry Word16
0 FilePath
"ver" Archive
archive
                when (ver /= ibcVersion) $ do
                                    logIBC 2 "ibc out of date"
                                    let e = if Word16
ver Word16 -> Word16 -> Bool
forall a. Ord a => a -> a -> Bool
< Word16
ibcVersion
                                            then FilePath
"an earlier" else FilePath
"a later"
                                    ldir <- runIO $ getIdrisLibDir
                                    let 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 = 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]
                                    ifail $ unlines [ unwords ["Incompatible ibc version for:", show fn]
                                                    , unwords [start
                                                              , "was built with"
                                                              , e
                                                              , "version of Idris."]
                                                    , end
                                                    ]
                source <- getEntry "" "sourcefile" archive
                srcok <- runIO $ doesFileExist source
                when srcok $ timestampOlder source fn
                processImportDirs archive
                processSourceDirs archive
                processImports reexp phase fn archive
                processImplicits archive
                processInfix archive
                processStatics archive
                processInterfaces archive
                processRecords archive
                processImplementations archive
                processDSLs archive
                processDatatypes  archive
                processOptimise  archive
                processSyntax archive
                processKeywords archive
                processObjectFiles fn archive
                processLibs archive
                processCodegenFlags archive
                processDynamicLibs archive
                processHeaders archive
                processPatternDefs archive
                processFlags archive
                processFnInfo archive
                processTotalityCheckError archive
                processCallgraph archive
                processDocs archive
                processModuleDocs archive
                processCoercions archive
                processTransforms archive
                processErrRev archive
                processErrReduce archive
                processLineApps archive
                processNameHints archive
                processMetaInformation archive
                processErrorHandlers archive
                processFunctionErrorHandlers archive
                processMetaVars archive
                processPostulates archive
                processExterns archive
                processParsedSpan archive
                processUsage archive
                processExports archive
                processAutoHints archive
                processDeprecate archive
                processDefs archive
                processTotal archive
                processInjective archive
                processAccess reexp phase archive
                processFragile archive
                processConstraints archive
                processLangExts phase archive

timestampOlder :: FilePath -> FilePath -> Idris ()
timestampOlder :: FilePath -> FilePath -> Idris ()
timestampOlder FilePath
src FilePath
ibc = do
  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
  ibct <- runIO $ getModificationTime ibc
  if (srct > ibct)
    then ifail $ unlines [ "Module needs reloading:"
                         , unwords ["\tSRC :", show src]
                         , unwords ["\tModified at:", show srct]
                         , unwords ["\tIBC :", show ibc]
                         , unwords ["\tModified at:", show ibct]
                         ]
    else return ()

processPostulates :: Archive -> Idris ()
processPostulates :: Archive -> Idris ()
processPostulates Archive
ar = do
    ns <- [Name] -> FilePath -> Archive -> Idris [Name]
forall b.
(Binary b, NFData b) =>
b -> FilePath -> Archive -> Idris b
getEntry [] FilePath
"ibc_postulates" Archive
ar
    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
    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
    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
    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
    updateIState (\IState
i -> IState
i { idris_parsedSpan = fc })

processUsage :: Archive -> Idris ()
processUsage :: Archive -> Idris ()
processUsage Archive
ar = do
    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
    updateIState (\IState
i -> IState
i { idris_erasureUsed = ns ++ idris_erasureUsed i })

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

processAutoHints :: Archive -> Idris ()
processAutoHints :: Archive -> Idris ()
processAutoHints Archive
ar = do
    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
    mapM_ (\(Name
n,Name
h) -> Name -> Name -> Idris ()
addAutoHint Name
n Name
h) ns

processDeprecate :: Archive -> Idris ()
processDeprecate :: Archive -> Idris ()
processDeprecate Archive
ar = do
    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
    mapM_ (\(Name
n,FilePath
reason) -> Name -> FilePath -> Idris ()
addDeprecated Name
n FilePath
reason) ns

processFragile :: Archive -> Idris ()
processFragile :: Archive -> Idris ()
processFragile Archive
ar = do
    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
    mapM_ (\(Name
n,FilePath
reason) -> Name -> FilePath -> Idris ()
addFragile Name
n FilePath
reason) ns

processConstraints :: Archive -> Idris ()
processConstraints :: Archive -> Idris ()
processConstraints Archive
ar = do
    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
    mapM_ (\ (FC
fc, UConstraint
c) -> FC -> (Int, [UConstraint]) -> Idris ()
addConstraints FC
fc (Int
0, [UConstraint
c])) cs

processImportDirs :: Archive -> Idris ()
processImportDirs :: Archive -> Idris ()
processImportDirs Archive
ar = do
    fs <- [FilePath] -> FilePath -> Archive -> Idris [FilePath]
forall b.
(Binary b, NFData b) =>
b -> FilePath -> Archive -> Idris b
getEntry [] FilePath
"ibc_importdirs" Archive
ar
    mapM_ addImportDir fs

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

processImports :: Bool -> IBCPhase -> FilePath -> Archive -> Idris ()
processImports :: Bool -> IBCPhase -> FilePath -> Archive -> Idris ()
processImports Bool
reexp IBCPhase
phase FilePath
fname Archive
ar = do
    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
    mapM_ (\(Bool
re, FilePath
f) -> do
        i <- Idris IState
getIState
        ibcsd <- valIBCSubDir i
        ids <- rankedImportDirs fname
        putIState (i { imported = f : imported i })
        let (phase', reexp') =
              case 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)
        fp <- findIBC ids ibcsd f
        logIBC 4 $ "processImports (fp, phase')" ++ show (fp, phase')
        case 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) fs

processImplicits :: Archive -> Idris ()
processImplicits :: Archive -> Idris ()
processImplicits Archive
ar = do
    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
    mapM_ (\ (Name
n, [PArg]
imp) -> do
        i <- Idris IState
getIState
        case lookupDefAccExact n False (tt_ctxt 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) })) imps

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

processStatics :: Archive -> Idris ()
processStatics :: Archive -> Idris ()
processStatics Archive
ar = do
    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
    mapM_ (\ (Name
n, [Bool]
s) ->
        (IState -> IState) -> Idris ()
updateIState (\IState
i -> IState
i { idris_statics = addDef n s (idris_statics i) })) ss

processInterfaces :: Archive -> Idris ()
processInterfaces :: Archive -> Idris ()
processInterfaces Archive
ar = do
    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
    mapM_ (\ (Name
n, InterfaceInfo
c) -> do
        i <- Idris IState
getIState
        -- Don't lose implementations from previous IBCs, which
        -- could have loaded in any order
        let 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 { interface_implementations = interface_implementations c ++ is }
        putIState (i { idris_interfaces = addDef n c' (idris_interfaces i) })) cs

processRecords :: Archive -> Idris ()
processRecords :: Archive -> Idris ()
processRecords Archive
ar = do
    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
    mapM_ (\ (Name
n, RecordInfo
r) ->
        (IState -> IState) -> Idris ()
updateIState (\IState
i -> IState
i { idris_records = addDef n r (idris_records i) })) rs

processImplementations :: Archive -> Idris ()
processImplementations :: Archive -> Idris ()
processImplementations Archive
ar = do
    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
    mapM_ (\ (Bool
i, Bool
res, Name
n, Name
ins) -> Bool -> Bool -> Name -> Name -> Idris ()
addImplementation Bool
i Bool
res Name
n Name
ins) cs

processDSLs :: Archive -> Idris ()
processDSLs :: Archive -> Idris ()
processDSLs Archive
ar = do
    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
    mapM_ (\ (Name
n, DSL
c) -> (IState -> IState) -> Idris ()
updateIState (\IState
i ->
                        IState
i { idris_dsls = addDef n c (idris_dsls i) })) cs

processDatatypes :: Archive -> Idris ()
processDatatypes :: Archive -> Idris ()
processDatatypes Archive
ar = do
    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
    mapM_ (\ (Name
n, TypeInfo
c) -> (IState -> IState) -> Idris ()
updateIState (\IState
i ->
                        IState
i { idris_datatypes = addDef n c (idris_datatypes i) })) cs

processOptimise :: Archive -> Idris ()
processOptimise :: Archive -> Idris ()
processOptimise Archive
ar = do
    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
    mapM_ (\ (Name
n, OptInfo
c) -> (IState -> IState) -> Idris ()
updateIState (\IState
i ->
                        IState
i { idris_optimisation = addDef n c (idris_optimisation i) })) cs

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

processKeywords :: Archive -> Idris ()
processKeywords :: Archive -> Idris ()
processKeywords Archive
ar = do
    k <- [FilePath] -> FilePath -> Archive -> Idris [FilePath]
forall b.
(Binary b, NFData b) =>
b -> FilePath -> Archive -> Idris b
getEntry [] FilePath
"ibc_keywords" Archive
ar
    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
    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
    mapM_ (\ (Codegen
cg, FilePath
obj) -> do
        dirs <- FilePath -> Idris [FilePath]
rankedImportDirs FilePath
fn
        o <- runIO $ findInPath dirs obj
        addObjectFile cg o) os

processLibs :: Archive -> Idris ()
processLibs :: Archive -> Idris ()
processLibs Archive
ar = do
    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
    mapM_ (uncurry addLib) ls

processCodegenFlags :: Archive -> Idris ()
processCodegenFlags :: Archive -> Idris ()
processCodegenFlags Archive
ar = do
    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
    mapM_ (uncurry addFlag) ls

processDynamicLibs :: Archive -> Idris ()
processDynamicLibs :: Archive -> Idris ()
processDynamicLibs Archive
ar = do
        ls <- [FilePath] -> FilePath -> Archive -> Idris [FilePath]
forall b.
(Binary b, NFData b) =>
b -> FilePath -> Archive -> Idris b
getEntry [] FilePath
"ibc_dynamic_libs" Archive
ar
        res <- mapM (addDyLib . return) ls
        mapM_ checkLoad 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
    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
    mapM_ (uncurry addHdr) hs

processPatternDefs :: Archive -> Idris ()
processPatternDefs :: Archive -> Idris ()
processPatternDefs Archive
ar = do
    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
    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) })) ds

processDefs :: Archive -> Idris ()
processDefs :: Archive -> Idris ()
processDefs Archive
ar = do
        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
        logIBC 4 $ "processDefs ds" ++ show ds
        mapM_ (\ (Name
n, Def
d) -> do
            d' <- Def -> StateT IState (ExceptT Err IO) Def
updateDef Def
d
            case 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
            updateIState (\IState
i -> IState
i { tt_ctxt = addCtxtDef n d' (tt_ctxt i) })) 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
            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
            cd' <- updateCD cd
            return $ CaseOp c t args o' s 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
            l' <- Term -> StateT IState (ExceptT Err IO) Term
update Term
l
            r' <- update r
            return $ Right (l', r')

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

        updateSC :: SC -> StateT IState (ExceptT Err IO) SC
updateSC (Case CaseType
t Name
n [CaseAlt' Term]
alts) = do
            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
            return (Case t n alts')
        updateSC (ProjCase Term
t [CaseAlt' Term]
alts) = do
            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
            return (ProjCase t alts')
        updateSC (STerm Term
t) = do
            t' <- Term -> StateT IState (ExceptT Err IO) Term
update Term
t
            return (STerm 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
            t' <- SC -> StateT IState (ExceptT Err IO) SC
updateSC SC
t
            return (ConCase n i ns t')
        updateAlt (FnCase Name
n [Name]
ns SC
t) = do
            t' <- SC -> StateT IState (ExceptT Err IO) SC
updateSC SC
t
            return (FnCase n ns t')
        updateAlt (ConstCase Const
c SC
t) = do
            t' <- SC -> StateT IState (ExceptT Err IO) SC
updateSC SC
t
            return (ConstCase c t')
        updateAlt (SucCase Name
n SC
t) = do
            t' <- SC -> StateT IState (ExceptT Err IO) SC
updateSC SC
t
            return (SucCase n t')
        updateAlt (DefaultCase SC
t) = do
            t' <- SC -> StateT IState (ExceptT Err IO) SC
updateSC SC
t
            return (DefaultCase 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
            tm <- Term -> Idris (Maybe Term)
addTT Term
t
            case 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
            n' <- Name -> Idris Name
getSymbol Name
n
            return $ P t n' 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
            b' <- Binder Term -> StateT IState (ExceptT Err IO) (Binder Term)
updateB Binder Term
b
            sc' <- update sc
            return $ Bind n b' 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
                        ty' <- Term -> StateT IState (ExceptT Err IO) Term
update' (Binder Term -> Term
forall b. Binder b -> b
binderTy Binder Term
b)
                        return (b { binderTy = ty' })
        update' (Proj Term
t Int
i) = do
                  t' <- Term -> StateT IState (ExceptT Err IO) Term
update' Term
t
                  return $ Proj t' 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
    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
    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)) ds

processModuleDocs :: Archive -> Idris ()
processModuleDocs :: Archive -> Idris ()
processModuleDocs Archive
ar = do
    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
    mapM_  (\ (Name
n, Docstring DocTerm
d) -> (IState -> IState) -> Idris ()
updateIState (\IState
i ->
            IState
i { idris_moduledocs = addDef n d (idris_moduledocs i) })) 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)
    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
    logIBC 3 $ "processAccess ds" ++ show ds
    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
      ) ds

processFlags :: Archive -> Idris ()
processFlags :: Archive -> Idris ()
processFlags Archive
ar = do
    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
    mapM_ (\ (Name
n, [FnOpt]
a) -> Name -> [FnOpt] -> Idris ()
setFlags Name
n [FnOpt]
a) ds

processFnInfo :: Archive -> Idris ()
processFnInfo :: Archive -> Idris ()
processFnInfo Archive
ar = do
    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
    mapM_ (\ (Name
n, FnInfo
a) -> Name -> FnInfo -> Idris ()
setFnInfo Name
n FnInfo
a) ds

processTotal :: Archive -> Idris ()
processTotal :: Archive -> Idris ()
processTotal Archive
ar = do
    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
    mapM_ (\ (Name
n, Totality
a) -> (IState -> IState) -> Idris ()
updateIState (\IState
i -> IState
i { tt_ctxt = setTotal n a (tt_ctxt i) })) ds

processInjective :: Archive -> Idris ()
processInjective :: Archive -> Idris ()
processInjective Archive
ar = do
    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
    mapM_ (\ (Name
n, Bool
a) -> (IState -> IState) -> Idris ()
updateIState (\IState
i -> IState
i { tt_ctxt = setInjective n a (tt_ctxt i) })) ds

processTotalityCheckError :: Archive -> Idris ()
processTotalityCheckError :: Archive -> Idris ()
processTotalityCheckError Archive
ar = do
    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
    updateIState (\IState
i -> IState
i { idris_totcheckfail = idris_totcheckfail i ++ es })

processCallgraph :: Archive -> Idris ()
processCallgraph :: Archive -> Idris ()
processCallgraph Archive
ar = do
    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
    mapM_ (\ (Name
n, CGInfo
a) -> Name -> CGInfo -> Idris ()
addToCG Name
n CGInfo
a) ds

processCoercions :: Archive -> Idris ()
processCoercions :: Archive -> Idris ()
processCoercions Archive
ar = do
    ns <- [Name] -> FilePath -> Archive -> Idris [Name]
forall b.
(Binary b, NFData b) =>
b -> FilePath -> Archive -> Idris b
getEntry [] FilePath
"ibc_coercions" Archive
ar
    mapM_ (\ Name
n -> Name -> Idris ()
addCoercion Name
n) ns

processTransforms :: Archive -> Idris ()
processTransforms :: Archive -> Idris ()
processTransforms Archive
ar = do
    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
    mapM_ (\ (Name
n, (Term, Term)
t) -> Name -> (Term, Term) -> Idris ()
addTrans Name
n (Term, Term)
t) ts

processErrRev :: Archive -> Idris ()
processErrRev :: Archive -> Idris ()
processErrRev Archive
ar = do
    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
    mapM_ addErrRev ts

processErrReduce :: Archive -> Idris ()
processErrReduce :: Archive -> Idris ()
processErrReduce Archive
ar = do
    ts <- [Name] -> FilePath -> Archive -> Idris [Name]
forall b.
(Binary b, NFData b) =>
b -> FilePath -> Archive -> Idris b
getEntry [] FilePath
"ibc_errReduce" Archive
ar
    mapM_ addErrReduce ts

processLineApps :: Archive -> Idris ()
processLineApps :: Archive -> Idris ()
processLineApps Archive
ar = do
    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
    mapM_ (\ (FilePath
f, Int
i, PTerm
t) -> FilePath -> Int -> PTerm -> Idris ()
addInternalApp FilePath
f Int
i PTerm
t) ls

processNameHints :: Archive -> Idris ()
processNameHints :: Archive -> Idris ()
processNameHints Archive
ar = do
    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
    mapM_ (\ (Name
n, Name
ty) -> Name -> Name -> Idris ()
addNameHint Name
n Name
ty) ns

processMetaInformation :: Archive -> Idris ()
processMetaInformation :: Archive -> Idris ()
processMetaInformation Archive
ar = do
    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
    mapM_ (\ (Name
n, MetaInformation
m) -> (IState -> IState) -> Idris ()
updateIState (\IState
i ->
                               IState
i { tt_ctxt = setMetaInformation n m (tt_ctxt i) })) ds

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

processFunctionErrorHandlers :: Archive -> Idris ()
processFunctionErrorHandlers :: Archive -> Idris ()
processFunctionErrorHandlers Archive
ar = do
    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
    mapM_ (\ (Name
fn,Name
arg,Name
handler) -> Name -> Name -> [Name] -> Idris ()
addFunctionErrorHandlers Name
fn Name
arg [Name
handler]) ns

processMetaVars :: Archive -> Idris ()
processMetaVars :: Archive -> Idris ()
processMetaVars Archive
ar = do
    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
    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 ds <- [LanguageExt] -> FilePath -> Archive -> Idris [LanguageExt]
forall b.
(Binary b, NFData b) =>
b -> FilePath -> Archive -> Idris b
getEntry [] FilePath
"ibc_langexts" Archive
ar
         mapM_ addLangExt 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 x1 <- Get [Name]
forall t. Binary t => Get t
get
               x2 <- get
               x3 <- get
               return (CGInfo x1 x2 [] 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 i <- Get Word8
getWord8
               case i of
                   Word8
0 -> do x1 <- Get Term
forall t. Binary t => Get t
get
                           x2 <- get
                           return (Function x1 x2)
                   Word8
1 -> do x1 <- Get NameType
forall t. Binary t => Get t
get
                           x2 <- get
                           return (TyDecl x1 x2)
                   -- Operator isn't written, don't read
                   Word8
3 -> do x1 <- Get CaseInfo
forall t. Binary t => Get t
get
                           x2 <- get
                           x3 <- get
--                            x4 <- get
                           -- x3 <- get always []
                           x5 <- get
                           return (CaseOp x1 x2 x3 [] [] 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 i <- Get Word8
getWord8
               case i of
                   Word8
0 -> do x1 <- Get [ArgOpt]
forall t. Binary t => Get t
get
                           x2 <- get
                           x3 <- get
                           x4 <- get
                           x5 <- get
                           return (Imp x1 x2 x3 x4 False x5)
                   Word8
1 -> do x1 <- Get [ArgOpt]
forall t. Binary t => Get t
get
                           x2 <- get
                           x3 <- get
                           x4 <- get
                           return (Exp x1 x2 x3 x4)
                   Word8
2 -> do x1 <- Get [ArgOpt]
forall t. Binary t => Get t
get
                           x2 <- get
                           x3 <- get
                           return (Constraint x1 x2 x3)
                   Word8
3 -> do x1 <- Get [ArgOpt]
forall t. Binary t => Get t
get
                           x2 <- get
                           x3 <- get
                           x4 <- get
                           return (TacImp x1 x2 x3 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 x1 <- Get [Using]
forall t. Binary t => Get t
get
               x2 <- get
               x3 <- get
               x4 <- get
               x5 <- get
               x6 <- get
               x7 <- get
               x8 <- get
               return (Syn x1 x2 x3 x4 [] id x5 x6 x7 Nothing 0 x8 0 True 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 x1 <- Get Name
forall t. Binary t => Get t
get
               x2 <- get
               x3 <- get
               x4 <- get
               x5 <- get
               x6 <- get
               x7 <- get
               x8 <- get
               return (CI x1 x2 x3 x4 x5 x6 x7 [] 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