{-|
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 = 166

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

data IBCFile = IBCFile {
    IBCFile -> Word16
ver                        :: Word16
  , IBCFile -> Int
iface_hash                 :: Int
  , IBCFile -> String
sourcefile                 :: FilePath
  , IBCFile -> [(Bool, String)]
ibc_imports                :: ![(Bool, FilePath)]
  , IBCFile -> [String]
ibc_importdirs             :: ![FilePath]
  , IBCFile -> [String]
ibc_sourcedirs             :: ![FilePath]
  , IBCFile -> [(Name, [PArg])]
ibc_implicits              :: ![(Name, [PArg])]
  , IBCFile -> [FixDecl]
ibc_fixes                  :: ![FixDecl]
  , IBCFile -> [(Name, [Bool])]
ibc_statics                :: ![(Name, [Bool])]
  , IBCFile -> [(Name, InterfaceInfo)]
ibc_interfaces             :: ![(Name, InterfaceInfo)]
  , IBCFile -> [(Name, RecordInfo)]
ibc_records                :: ![(Name, RecordInfo)]
  , IBCFile -> [(Bool, Bool, Name, Name)]
ibc_implementations        :: ![(Bool, Bool, Name, Name)]
  , IBCFile -> [(Name, DSL)]
ibc_dsls                   :: ![(Name, DSL)]
  , IBCFile -> [(Name, TypeInfo)]
ibc_datatypes              :: ![(Name, TypeInfo)]
  , IBCFile -> [(Name, OptInfo)]
ibc_optimise               :: ![(Name, OptInfo)]
  , IBCFile -> [Syntax]
ibc_syntax                 :: ![Syntax]
  , IBCFile -> [String]
ibc_keywords               :: ![String]
  , IBCFile -> [(Codegen, String)]
ibc_objs                   :: ![(Codegen, FilePath)]
  , IBCFile -> [(Codegen, String)]
ibc_libs                   :: ![(Codegen, String)]
  , IBCFile -> [(Codegen, String)]
ibc_cgflags                :: ![(Codegen, String)]
  , IBCFile -> [String]
ibc_dynamic_libs           :: ![String]
  , IBCFile -> [(Codegen, String)]
ibc_hdrs                   :: ![(Codegen, String)]
  , IBCFile -> [(FC, String)]
ibc_totcheckfail           :: ![(FC, String)]
  , IBCFile -> [(Name, [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 -> [(String, Int, PTerm)]
ibc_lineapps               :: ![(FilePath, Int, PTerm)]
  , IBCFile -> [(Name, Name)]
ibc_namehints              :: ![(Name, Name)]
  , IBCFile -> [(Name, MetaInformation)]
ibc_metainformation        :: ![(Name, MetaInformation)]
  , IBCFile -> [Name]
ibc_errorhandlers          :: ![Name]
  , IBCFile -> [(Name, Name, Name)]
ibc_function_errorhandlers :: ![(Name, Name, Name)] -- fn, arg, handler
  , IBCFile -> [(Name, (Maybe Name, Int, [Name], Bool, Bool))]
ibc_metavars               :: ![(Name, (Maybe Name, Int, [Name], Bool, Bool))]
  , IBCFile -> [(Name, ([([(Name, 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, String)]
ibc_deprecated             :: ![(Name, String)]
  , IBCFile -> [(Name, Def)]
ibc_defs                   :: ![(Name, Def)]
  , IBCFile -> [(Name, Totality)]
ibc_total                  :: ![(Name, Totality)]
  , IBCFile -> [(Name, Bool)]
ibc_injective              :: ![(Name, Injectivity)]
  , IBCFile -> [(Name, Accessibility)]
ibc_access                 :: ![(Name, Accessibility)]
  , IBCFile -> [(Name, String)]
ibc_fragile                :: ![(Name, String)]
  , IBCFile -> [(FC, UConstraint)]
ibc_constraints            :: ![(FC, UConstraint)]
  , IBCFile -> [LanguageExt]
ibc_langexts               :: ![LanguageExt]
  , IBCFile -> [(String, Int)]
ibc_importhashes           :: ![(FilePath, Int)]
  }
  deriving Int -> IBCFile -> ShowS
[IBCFile] -> ShowS
IBCFile -> String
(Int -> IBCFile -> ShowS)
-> (IBCFile -> String) -> ([IBCFile] -> ShowS) -> Show IBCFile
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
showList :: [IBCFile] -> ShowS
$cshowList :: [IBCFile] -> ShowS
show :: IBCFile -> String
$cshow :: IBCFile -> String
showsPrec :: Int -> IBCFile -> ShowS
$cshowsPrec :: Int -> IBCFile -> ShowS
Show
{-!
deriving instance Binary IBCFile
!-}

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

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


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

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


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

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


makeEntry :: (Binary b) => String -> [b] -> Maybe Entry
makeEntry :: String -> [b] -> Maybe Entry
makeEntry name :: String
name val :: [b]
val = if [b] -> 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
$ String -> Integer -> ByteString -> Entry
toEntry String
name 0 ([b] -> ByteString
forall a. Binary a => a -> ByteString
encode [b]
val)


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

writeArchive :: FilePath -> IBCFile -> Idris ()
writeArchive :: String -> IBCFile -> Idris ()
writeArchive fp :: String
fp i :: IBCFile
i = do let a :: Archive
a = (Archive -> Entry -> Archive) -> Archive -> [Entry] -> Archive
forall (t :: * -> *) b a.
Foldable t =>
(b -> a -> b) -> b -> t a -> b
L.foldl (\x :: Archive
x y :: 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
$ String -> ByteString -> IO ()
B.writeFile String
fp (Archive -> ByteString
fromArchive Archive
a)

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

qhash :: Int -> String -> Int
qhash :: Int -> String -> Int
qhash hash :: Int
hash [] = Int -> Int
forall a. Num a => a -> a
abs Int
hash Int -> Int -> Int
forall a. Integral a => a -> a -> a
`mod` 0xffffffff
qhash hash :: Int
hash (x :: Char
x:xs :: String
xs) = Int -> String -> Int
qhash (Int
hash Int -> Int -> Int
forall a. Num a => a -> a -> a
* 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)) String
xs

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

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

calculateHash :: IState -> IBCFile -> Int
calculateHash :: IState -> IBCFile -> Int
calculateHash ist :: IState
ist f :: 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 ns :: [Name]
ns tms :: [Term]
tms = [Int] -> Int
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 [1..] [Name]
ns) Int -> Int -> Int
forall a. Num a => a -> a -> a
+
                        [Int] -> Int
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 [1..] [Term]
tms)

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

    inlinable :: t a -> (a, t FnOpt) -> Bool
inlinable acc :: t a
acc (n :: a
n, opts :: t FnOpt
opts)
        = a
n 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 (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
`elem` t FnOpt
opts Bool -> Bool -> Bool
|| FnOpt
PEGenerated FnOpt -> t FnOpt -> Bool
forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
`elem` t FnOpt
opts)

    findTms :: [(a, Term, Term)] -> [Term]
    findTms :: [(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 (\ (_, x :: Term
x, y :: Term
y) -> [Term
x, Term
y])

    patDef :: Name -> [Term]
    patDef :: Name -> [Term]
patDef n :: 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
               Nothing -> []
               Just (tms :: [([(Name, Term)], Term, Term)]
tms, _) -> [([(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 ((n :: Name
n, Public) : ns :: [(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
                   Nothing -> [Term]
ts
                   Just ty :: 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 ((n :: Name
n, Frozen) : ns :: [(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
                   Nothing -> [Term]
ts
                   Just ty :: Term
ty -> Term
ty Term -> [Term] -> [Term]
forall a. a -> [a] -> [a]
: [Term]
ts
    getDefs (_ : ns :: [(Name, Accessibility)]
ns) = [(Name, Accessibility)] -> [Term]
getDefs [(Name, Accessibility)]
ns

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

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

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

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

getEntry :: (Binary b, NFData b) => b -> FilePath -> Archive -> Idris b
getEntry :: b -> String -> Archive -> Idris b
getEntry alt :: b
alt f :: String
f a :: Archive
a = case String -> Archive -> Maybe Entry
findEntryByPath String
f Archive
a of
                Nothing -> b -> Idris b
forall (m :: * -> *) a. Monad m => a -> m a
return b
alt
                Just e :: Entry
e -> b -> Idris b
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 -> String -> Archive -> Idris ()
unhide phase :: IBCPhase
phase fp :: String
fp ar :: Archive
ar = do
    Bool -> IBCPhase -> String -> Archive -> Idris ()
processImports Bool
True IBCPhase
phase String
fp Archive
ar
    Bool -> IBCPhase -> Archive -> Idris ()
processAccess Bool
True IBCPhase
phase Archive
ar

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

        if (Bool -> Bool
not Bool
reexp)
            then do
                Int -> String -> Idris ()
logIBC 2 (String -> Idris ()) -> String -> Idris ()
forall a b. (a -> b) -> a -> b
$ "Not exporting " String -> ShowS
forall a. [a] -> [a] -> [a]
++ Name -> String
forall a. Show a => a -> String
show Name
n
                Name -> Accessibility -> Idris ()
setAccessibility Name
n Accessibility
Hidden
            else
                Int -> String -> Idris ()
logIBC 2 (String -> Idris ()) -> String -> Idris ()
forall a b. (a -> b) -> a -> b
$ "Exporting " String -> ShowS
forall a. [a] -> [a] -> [a]
++ Name -> String
forall a. Show a => a -> String
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 -> String -> Idris ()
logIBC 2 (String -> Idris ()) -> String -> Idris ()
forall a b. (a -> b) -> a -> b
$ "Top level, exporting " String -> ShowS
forall a. [a] -> [a] -> [a]
++ Name -> String
forall a. Show a => a -> String
show Name
n
            Name -> Accessibility -> Idris ()
setAccessibility Name
n Accessibility
Public
      ) [(Name, Accessibility)]
ds

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

-- We only want the language extensions when reading the top level thing
processLangExts :: IBCPhase -> Archive -> Idris ()
processLangExts :: IBCPhase -> Archive -> Idris ()
processLangExts (IBC_REPL True) ar :: Archive
ar
    = do [LanguageExt]
ds <- [LanguageExt] -> String -> Archive -> Idris [LanguageExt]
forall b. (Binary b, NFData b) => b -> String -> Archive -> Idris b
getEntry [] "ibc_langexts" Archive
ar
         (LanguageExt -> Idris ()) -> [LanguageExt] -> Idris ()
forall (t :: * -> *) (m :: * -> *) a b.
(Foldable t, Monad m) =>
(a -> m b) -> t a -> m ()
mapM_ LanguageExt -> Idris ()
addLangExt [LanguageExt]
ds
processLangExts _ _ = () -> Idris ()
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 x1 :: [Name]
x1 x2 :: Maybe [Name]
x2 x3 :: [SCGEntry]
x3 x4 :: [(Int, [(Name, Int)])]
x4)
          = do [Name] -> Put
forall t. Binary t => t -> Put
put [Name]
x1
--                put x3 -- Already used SCG info for totality check
               Maybe [Name] -> Put
forall t. Binary t => t -> Put
put Maybe [Name]
x2
               [(Int, [(Name, Int)])] -> Put
forall t. Binary t => t -> Put
put [(Int, [(Name, Int)])]
x4
        get :: Get CGInfo
get
          = do [Name]
x1 <- Get [Name]
forall t. Binary t => Get t
get
               Maybe [Name]
x2 <- Get (Maybe [Name])
forall t. Binary t => Get t
get
               [(Int, [(Name, Int)])]
x3 <- Get [(Int, [(Name, Int)])]
forall t. Binary t => Get t
get
               CGInfo -> Get CGInfo
forall (m :: * -> *) a. Monad m => a -> m a
return ([Name]
-> Maybe [Name] -> [SCGEntry] -> [(Int, [(Name, Int)])] -> CGInfo
CGInfo [Name]
x1 Maybe [Name]
x2 [] [(Int, [(Name, Int)])]
x3)

instance Binary CaseType
instance Binary SC
instance Binary CaseAlt
instance Binary CaseDefs
instance Binary CaseInfo
instance Binary Def where
        put :: Def -> Put
put x :: Def
x
          = {-# SCC "putDef" #-}
            case Def
x of
                Function x1 :: Term
x1 x2 :: Term
x2 -> do Word8 -> Put
putWord8 0
                                     Term -> Put
forall t. Binary t => t -> Put
put Term
x1
                                     Term -> Put
forall t. Binary t => t -> Put
put Term
x2
                TyDecl x1 :: NameType
x1 x2 :: Term
x2 -> do Word8 -> Put
putWord8 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 x1 :: Term
x1 x2 :: Int
x2 x3 :: [Value] -> Maybe Value
x3 -> do () -> Put
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 x1 :: CaseInfo
x1 x2 :: Term
x2 x3 :: [(Term, Bool)]
x3 _ _ x4 :: CaseDefs
x4 -> do Word8 -> Put
putWord8 3
                                             CaseInfo -> Put
forall t. Binary t => t -> Put
put CaseInfo
x1
                                             Term -> Put
forall t. Binary t => t -> Put
put Term
x2
                                             [(Term, Bool)] -> Put
forall t. Binary t => t -> Put
put [(Term, Bool)]
x3
                                             CaseDefs -> Put
forall t. Binary t => t -> Put
put CaseDefs
x4
        get :: Get Def
get
          = do Word8
i <- Get Word8
getWord8
               case Word8
i of
                   0 -> do Term
x1 <- Get Term
forall t. Binary t => Get t
get
                           Term
x2 <- Get Term
forall t. Binary t => Get t
get
                           Def -> Get Def
forall (m :: * -> *) a. Monad m => a -> m a
return (Term -> Term -> Def
Function Term
x1 Term
x2)
                   1 -> do NameType
x1 <- Get NameType
forall t. Binary t => Get t
get
                           Term
x2 <- Get Term
forall t. Binary t => Get t
get
                           Def -> Get Def
forall (m :: * -> *) a. Monad m => a -> m a
return (NameType -> Term -> Def
TyDecl NameType
x1 Term
x2)
                   -- Operator isn't written, don't read
                   3 -> do CaseInfo
x1 <- Get CaseInfo
forall t. Binary t => Get t
get
                           Term
x2 <- Get Term
forall t. Binary t => Get t
get
                           [(Term, Bool)]
x3 <- Get [(Term, Bool)]
forall t. Binary t => Get t
get
--                            x4 <- get
                           -- x3 <- get always []
                           CaseDefs
x5 <- Get CaseDefs
forall t. Binary t => Get t
get
                           Def -> Get Def
forall (m :: * -> *) a. Monad m => a -> m a
return (CaseInfo
-> Term
-> [(Term, Bool)]
-> [Either Term (Term, Term)]
-> [([Name], Term, Term)]
-> CaseDefs
-> Def
CaseOp CaseInfo
x1 Term
x2 [(Term, Bool)]
x3 [] [] CaseDefs
x5)
                   _ -> String -> Get Def
forall a. HasCallStack => String -> a
error "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 x :: Plicity
x
          = case Plicity
x of
                Imp x1 :: [ArgOpt]
x1 x2 :: Static
x2 x3 :: Bool
x3 x4 :: Maybe ImplicitInfo
x4 _ x5 :: RigCount
x5 ->
                             do Word8 -> Put
putWord8 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 x1 :: [ArgOpt]
x1 x2 :: Static
x2 x3 :: Bool
x3 x4 :: RigCount
x4 ->
                             do Word8 -> Put
putWord8 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 x1 :: [ArgOpt]
x1 x2 :: Static
x2 x3 :: RigCount
x3 ->
                                    do Word8 -> Put
putWord8 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 x1 :: [ArgOpt]
x1 x2 :: Static
x2 x3 :: PTerm
x3 x4 :: RigCount
x4 ->
                                   do Word8 -> Put
putWord8 3
                                      [ArgOpt] -> Put
forall t. Binary t => t -> Put
put [ArgOpt]
x1
                                      Static -> Put
forall t. Binary t => t -> Put
put Static
x2
                                      PTerm -> Put
forall t. Binary t => t -> Put
put PTerm
x3
                                      RigCount -> Put
forall t. Binary t => t -> Put
put RigCount
x4
        get :: Get Plicity
get
          = do Word8
i <- Get Word8
getWord8
               case Word8
i of
                   0 -> do [ArgOpt]
x1 <- Get [ArgOpt]
forall t. Binary t => Get t
get
                           Static
x2 <- Get Static
forall t. Binary t => Get t
get
                           Bool
x3 <- Get Bool
forall t. Binary t => Get t
get
                           Maybe ImplicitInfo
x4 <- Get (Maybe ImplicitInfo)
forall t. Binary t => Get t
get
                           RigCount
x5 <- Get RigCount
forall t. Binary t => Get t
get
                           Plicity -> Get Plicity
forall (m :: * -> *) a. Monad m => a -> m a
return ([ArgOpt]
-> Static
-> Bool
-> Maybe ImplicitInfo
-> Bool
-> RigCount
-> Plicity
Imp [ArgOpt]
x1 Static
x2 Bool
x3 Maybe ImplicitInfo
x4 Bool
False RigCount
x5)
                   1 -> do [ArgOpt]
x1 <- Get [ArgOpt]
forall t. Binary t => Get t
get
                           Static
x2 <- Get Static
forall t. Binary t => Get t
get
                           Bool
x3 <- Get Bool
forall t. Binary t => Get t
get
                           RigCount
x4 <- Get RigCount
forall t. Binary t => Get t
get
                           Plicity -> Get Plicity
forall (m :: * -> *) a. Monad m => a -> m a
return ([ArgOpt] -> Static -> Bool -> RigCount -> Plicity
Exp [ArgOpt]
x1 Static
x2 Bool
x3 RigCount
x4)
                   2 -> do [ArgOpt]
x1 <- Get [ArgOpt]
forall t. Binary t => Get t
get
                           Static
x2 <- Get Static
forall t. Binary t => Get t
get
                           RigCount
x3 <- Get RigCount
forall t. Binary t => Get t
get
                           Plicity -> Get Plicity
forall (m :: * -> *) a. Monad m => a -> m a
return ([ArgOpt] -> Static -> RigCount -> Plicity
Constraint [ArgOpt]
x1 Static
x2 RigCount
x3)
                   3 -> do [ArgOpt]
x1 <- Get [ArgOpt]
forall t. Binary t => Get t
get
                           Static
x2 <- Get Static
forall t. Binary t => Get t
get
                           PTerm
x3 <- Get PTerm
forall t. Binary t => Get t
get
                           RigCount
x4 <- Get RigCount
forall t. Binary t => Get t
get
                           Plicity -> Get Plicity
forall (m :: * -> *) a. Monad m => a -> m a
return ([ArgOpt] -> Static -> PTerm -> RigCount -> Plicity
TacImp [ArgOpt]
x1 Static
x2 PTerm
x3 RigCount
x4)
                   _ -> String -> Get Plicity
forall a. HasCallStack => String -> a
error "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 x1 :: [Using]
x1 x2 :: [(Name, PTerm)]
x2 x3 :: [String]
x3 x4 :: [Name]
x4 _ _ x5 :: Bool
x5 x6 :: Bool
x6 x7 :: Bool
x7 _ _ x8 :: DSL
x8 _ _ _)
          = 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
               [String] -> Put
forall t. Binary t => t -> Put
put [String]
x3
               [Name] -> Put
forall t. Binary t => t -> Put
put [Name]
x4
               Bool -> Put
forall t. Binary t => t -> Put
put Bool
x5
               Bool -> Put
forall t. Binary t => t -> Put
put Bool
x6
               Bool -> Put
forall t. Binary t => t -> Put
put Bool
x7
               DSL -> Put
forall t. Binary t => t -> Put
put DSL
x8
        get :: Get SyntaxInfo
get
          = do [Using]
x1 <- Get [Using]
forall t. Binary t => Get t
get
               [(Name, PTerm)]
x2 <- Get [(Name, PTerm)]
forall t. Binary t => Get t
get
               [String]
x3 <- Get [String]
forall t. Binary t => Get t
get
               [Name]
x4 <- Get [Name]
forall t. Binary t => Get t
get
               Bool
x5 <- Get Bool
forall t. Binary t => Get t
get
               Bool
x6 <- Get Bool
forall t. Binary t => Get t
get
               Bool
x7 <- Get Bool
forall t. Binary t => Get t
get
               DSL
x8 <- Get DSL
forall t. Binary t => Get t
get
               SyntaxInfo -> Get SyntaxInfo
forall (m :: * -> *) a. Monad m => a -> m a
return ([Using]
-> [(Name, PTerm)]
-> [String]
-> [Name]
-> [Name]
-> (Name -> Name)
-> Bool
-> Bool
-> Bool
-> Maybe Int
-> Int
-> DSL
-> Int
-> Bool
-> Bool
-> SyntaxInfo
Syn [Using]
x1 [(Name, PTerm)]
x2 [String]
x3 [Name]
x4 [] Name -> Name
forall a. a -> a
id Bool
x5 Bool
x6 Bool
x7 Maybe Int
forall a. Maybe a
Nothing 0 DSL
x8 0 Bool
True Bool
True)

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

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