{-# LANGUAGE FlexibleInstances, TypeSynonymInstances #-}
{-# OPTIONS_GHC -fwarn-incomplete-patterns #-}
{-# OPTIONS_GHC -fwarn-unused-imports #-}
module Idris.IBC (loadIBC, loadPkgIndex,
writeIBC, writePkgIndex,
hasValidIBCVersion, IBCPhase(..),
getIBCHash, getImportHashes) where
import Idris.AbsSyntax
import Idris.Core.CaseTree
import Idris.Core.Evaluate
import Idris.Core.TT
import Idris.DeepSeq ()
import Idris.Docstrings (Docstring)
import qualified Idris.Docstrings as D
import Idris.Error
import Idris.Imports
import Idris.Options
import Idris.Output
import IRTS.System (getIdrisLibDir)
import qualified Cheapskate.Types as CT
import Codec.Archive.Zip
import Control.DeepSeq
import Control.Monad
import Data.Binary
import Data.ByteString.Lazy as B hiding (elem, length, map)
import Data.List as L
import Data.Maybe (catMaybes)
import qualified Data.Set as S
import System.Directory
import System.FilePath
ibcVersion :: Word16
ibcVersion :: Word16
ibcVersion = Word16
167
data IBCPhase = IBC_Building
| IBC_REPL Bool
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)]
, 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
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 Int
0 String
"" [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] Maybe FC
forall a. Maybe a
Nothing [] [] [] [] [] [] [] [] [] [] [] []
hasValidIBCVersion :: FilePath -> Idris Bool
hasValidIBCVersion :: String -> Idris Bool
hasValidIBCVersion 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
_ -> Bool -> Idris Bool
forall (m :: * -> *) a. Monad m => a -> m a
return Bool
False
Right Archive
archive -> do Word16
ver <- Word16 -> String -> Archive -> Idris Word16
forall b. (Binary b, NFData b) => b -> String -> Archive -> Idris b
getEntry Word16
0 String
"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
-> IBCPhase
-> FilePath -> Idris ()
loadIBC :: Bool -> IBCPhase -> String -> Idris ()
loadIBC Bool
reexport IBCPhase
phase String
fp
= do Int -> String -> Idris ()
logIBC Int
1 (String -> Idris ()) -> String -> Idris ()
forall a b. (a -> b) -> a -> b
$ String
"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 Int
3 (String -> Idris ()) -> String -> Idris ()
forall a b. (a -> b) -> a -> b
$ String
"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
Maybe Bool
Nothing -> Bool -> Idris ()
load Bool
True
Just Bool
p -> if (Bool -> Bool
not Bool
p Bool -> Bool -> Bool
&& Bool
reexport) then Bool -> Idris ()
load Bool
False else () -> Idris ()
forall (m :: * -> *) a. Monad m => a -> m a
return ()
where
load :: Bool -> Idris ()
load Bool
fullLoad = do
Int -> String -> Idris ()
logIBC Int
1 (String -> Idris ()) -> String -> Idris ()
forall a b. (a -> b) -> a -> b
$ String
"Loading ibc " String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
fp String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
" " 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 String
_ -> 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]
++ String
" isn't loadable, it may have an old ibc format.\n"
String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
"Please clean and rebuild it."
Right Archive
archive -> do
if Bool
fullLoad
then Bool -> IBCPhase -> Archive -> String -> Idris ()
process Bool
reexport IBCPhase
phase Archive
archive String
fp
else IBCPhase -> String -> Archive -> Idris ()
unhide IBCPhase
phase String
fp Archive
archive
Bool -> String -> Idris ()
addImported Bool
reexport String
fp
getIBCHash :: FilePath -> Idris Int
getIBCHash :: String -> Idris Int
getIBCHash String
fp
= do ByteString
archiveFile <- 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 Int
forall (m :: * -> *) a. Monad m => a -> m a
return Int
0
Right Archive
archive -> Int -> String -> Archive -> Idris Int
forall b. (Binary b, NFData b) => b -> String -> Archive -> Idris b
getEntry Int
0 String
"iface_hash" Archive
archive
getImportHashes :: FilePath -> Idris [(FilePath, Int)]
getImportHashes :: String -> Idris [(String, Int)]
getImportHashes String
fp
= do ByteString
archiveFile <- 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
_ -> [(String, Int)] -> Idris [(String, Int)]
forall (m :: * -> *) a. Monad m => a -> m a
return []
Right Archive
archive -> [(String, Int)] -> String -> Archive -> Idris [(String, Int)]
forall b. (Binary b, NFData b) => b -> String -> Archive -> Idris b
getEntry [] String
"ibc_importhashes" Archive
archive
loadPkgIndex :: PkgName -> Idris ()
loadPkgIndex :: PkgName -> Idris ()
loadPkgIndex 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 String
name [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 Integer
0 ([b] -> ByteString
forall a. Binary a => a -> ByteString
encode [b]
val)
entries :: IBCFile -> [Entry]
entries :: IBCFile -> [Entry]
entries IBCFile
i = [Maybe Entry] -> [Entry]
forall a. [Maybe a] -> [a]
catMaybes [Entry -> Maybe Entry
forall a. a -> Maybe a
Just (Entry -> Maybe Entry) -> Entry -> Maybe Entry
forall a b. (a -> b) -> a -> b
$ String -> Integer -> ByteString -> Entry
toEntry String
"ver" Integer
0 (Word16 -> ByteString
forall a. Binary a => a -> ByteString
encode (Word16 -> ByteString) -> Word16 -> ByteString
forall a b. (a -> b) -> a -> b
$ IBCFile -> Word16
ver IBCFile
i),
Entry -> Maybe Entry
forall a. a -> Maybe a
Just (Entry -> Maybe Entry) -> Entry -> Maybe Entry
forall a b. (a -> b) -> a -> b
$ String -> Integer -> ByteString -> Entry
toEntry String
"iface_hash" Integer
0 (Int -> ByteString
forall a. Binary a => a -> ByteString
encode (Int -> ByteString) -> Int -> ByteString
forall a b. (a -> b) -> a -> b
$ IBCFile -> Int
iface_hash IBCFile
i),
String -> String -> Maybe Entry
forall b. Binary b => String -> [b] -> Maybe Entry
makeEntry String
"sourcefile" (IBCFile -> String
sourcefile IBCFile
i),
String -> [(Bool, String)] -> Maybe Entry
forall b. Binary b => String -> [b] -> Maybe Entry
makeEntry String
"ibc_imports" (IBCFile -> [(Bool, String)]
ibc_imports IBCFile
i),
String -> [String] -> Maybe Entry
forall b. Binary b => String -> [b] -> Maybe Entry
makeEntry String
"ibc_importdirs" (IBCFile -> [String]
ibc_importdirs IBCFile
i),
String -> [String] -> Maybe Entry
forall b. Binary b => String -> [b] -> Maybe Entry
makeEntry String
"ibc_sourcedirs" (IBCFile -> [String]
ibc_sourcedirs IBCFile
i),
String -> [(Name, [PArg])] -> Maybe Entry
forall b. Binary b => String -> [b] -> Maybe Entry
makeEntry String
"ibc_implicits" (IBCFile -> [(Name, [PArg])]
ibc_implicits IBCFile
i),
String -> [FixDecl] -> Maybe Entry
forall b. Binary b => String -> [b] -> Maybe Entry
makeEntry String
"ibc_fixes" (IBCFile -> [FixDecl]
ibc_fixes IBCFile
i),
String -> [(Name, [Bool])] -> Maybe Entry
forall b. Binary b => String -> [b] -> Maybe Entry
makeEntry String
"ibc_statics" (IBCFile -> [(Name, [Bool])]
ibc_statics IBCFile
i),
String -> [(Name, InterfaceInfo)] -> Maybe Entry
forall b. Binary b => String -> [b] -> Maybe Entry
makeEntry String
"ibc_interfaces" (IBCFile -> [(Name, InterfaceInfo)]
ibc_interfaces IBCFile
i),
String -> [(Name, RecordInfo)] -> Maybe Entry
forall b. Binary b => String -> [b] -> Maybe Entry
makeEntry String
"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 String
"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 String
"ibc_dsls" (IBCFile -> [(Name, DSL)]
ibc_dsls IBCFile
i),
String -> [(Name, TypeInfo)] -> Maybe Entry
forall b. Binary b => String -> [b] -> Maybe Entry
makeEntry String
"ibc_datatypes" (IBCFile -> [(Name, TypeInfo)]
ibc_datatypes IBCFile
i),
String -> [(Name, OptInfo)] -> Maybe Entry
forall b. Binary b => String -> [b] -> Maybe Entry
makeEntry String
"ibc_optimise" (IBCFile -> [(Name, OptInfo)]
ibc_optimise IBCFile
i),
String -> [Syntax] -> Maybe Entry
forall b. Binary b => String -> [b] -> Maybe Entry
makeEntry String
"ibc_syntax" (IBCFile -> [Syntax]
ibc_syntax IBCFile
i),
String -> [String] -> Maybe Entry
forall b. Binary b => String -> [b] -> Maybe Entry
makeEntry String
"ibc_keywords" (IBCFile -> [String]
ibc_keywords IBCFile
i),
String -> [(Codegen, String)] -> Maybe Entry
forall b. Binary b => String -> [b] -> Maybe Entry
makeEntry String
"ibc_objs" (IBCFile -> [(Codegen, String)]
ibc_objs IBCFile
i),
String -> [(Codegen, String)] -> Maybe Entry
forall b. Binary b => String -> [b] -> Maybe Entry
makeEntry String
"ibc_libs" (IBCFile -> [(Codegen, String)]
ibc_libs IBCFile
i),
String -> [(Codegen, String)] -> Maybe Entry
forall b. Binary b => String -> [b] -> Maybe Entry
makeEntry String
"ibc_cgflags" (IBCFile -> [(Codegen, String)]
ibc_cgflags IBCFile
i),
String -> [String] -> Maybe Entry
forall b. Binary b => String -> [b] -> Maybe Entry
makeEntry String
"ibc_dynamic_libs" (IBCFile -> [String]
ibc_dynamic_libs IBCFile
i),
String -> [(Codegen, String)] -> Maybe Entry
forall b. Binary b => String -> [b] -> Maybe Entry
makeEntry String
"ibc_hdrs" (IBCFile -> [(Codegen, String)]
ibc_hdrs IBCFile
i),
String -> [(FC, String)] -> Maybe Entry
forall b. Binary b => String -> [b] -> Maybe Entry
makeEntry String
"ibc_totcheckfail" (IBCFile -> [(FC, String)]
ibc_totcheckfail IBCFile
i),
String -> [(Name, [FnOpt])] -> Maybe Entry
forall b. Binary b => String -> [b] -> Maybe Entry
makeEntry String
"ibc_flags" (IBCFile -> [(Name, [FnOpt])]
ibc_flags IBCFile
i),
String -> [(Name, FnInfo)] -> Maybe Entry
forall b. Binary b => String -> [b] -> Maybe Entry
makeEntry String
"ibc_fninfo" (IBCFile -> [(Name, FnInfo)]
ibc_fninfo IBCFile
i),
String -> [(Name, CGInfo)] -> Maybe Entry
forall b. Binary b => String -> [b] -> Maybe Entry
makeEntry String
"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 String
"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 String
"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 String
"ibc_transforms" (IBCFile -> [(Name, (Term, Term))]
ibc_transforms IBCFile
i),
String -> [(Term, Term)] -> Maybe Entry
forall b. Binary b => String -> [b] -> Maybe Entry
makeEntry String
"ibc_errRev" (IBCFile -> [(Term, Term)]
ibc_errRev IBCFile
i),
String -> [Name] -> Maybe Entry
forall b. Binary b => String -> [b] -> Maybe Entry
makeEntry String
"ibc_errReduce" (IBCFile -> [Name]
ibc_errReduce IBCFile
i),
String -> [Name] -> Maybe Entry
forall b. Binary b => String -> [b] -> Maybe Entry
makeEntry String
"ibc_coercions" (IBCFile -> [Name]
ibc_coercions IBCFile
i),
String -> [(String, Int, PTerm)] -> Maybe Entry
forall b. Binary b => String -> [b] -> Maybe Entry
makeEntry String
"ibc_lineapps" (IBCFile -> [(String, Int, PTerm)]
ibc_lineapps IBCFile
i),
String -> [(Name, Name)] -> Maybe Entry
forall b. Binary b => String -> [b] -> Maybe Entry
makeEntry String
"ibc_namehints" (IBCFile -> [(Name, Name)]
ibc_namehints IBCFile
i),
String -> [(Name, MetaInformation)] -> Maybe Entry
forall b. Binary b => String -> [b] -> Maybe Entry
makeEntry String
"ibc_metainformation" (IBCFile -> [(Name, MetaInformation)]
ibc_metainformation IBCFile
i),
String -> [Name] -> Maybe Entry
forall b. Binary b => String -> [b] -> Maybe Entry
makeEntry String
"ibc_errorhandlers" (IBCFile -> [Name]
ibc_errorhandlers IBCFile
i),
String -> [(Name, Name, Name)] -> Maybe Entry
forall b. Binary b => String -> [b] -> Maybe Entry
makeEntry String
"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 String
"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 String
"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 String
"ibc_postulates" (IBCFile -> [Name]
ibc_postulates IBCFile
i),
String -> [(Name, Int)] -> Maybe Entry
forall b. Binary b => String -> [b] -> Maybe Entry
makeEntry String
"ibc_externs" (IBCFile -> [(Name, Int)]
ibc_externs IBCFile
i),
String -> Integer -> ByteString -> Entry
toEntry String
"ibc_parsedSpan" Integer
0 (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 String
"ibc_usage" (IBCFile -> [(Name, Int)]
ibc_usage IBCFile
i),
String -> [Name] -> Maybe Entry
forall b. Binary b => String -> [b] -> Maybe Entry
makeEntry String
"ibc_exports" (IBCFile -> [Name]
ibc_exports IBCFile
i),
String -> [(Name, Name)] -> Maybe Entry
forall b. Binary b => String -> [b] -> Maybe Entry
makeEntry String
"ibc_autohints" (IBCFile -> [(Name, Name)]
ibc_autohints IBCFile
i),
String -> [(Name, String)] -> Maybe Entry
forall b. Binary b => String -> [b] -> Maybe Entry
makeEntry String
"ibc_deprecated" (IBCFile -> [(Name, String)]
ibc_deprecated IBCFile
i),
String -> [(Name, Def)] -> Maybe Entry
forall b. Binary b => String -> [b] -> Maybe Entry
makeEntry String
"ibc_defs" (IBCFile -> [(Name, Def)]
ibc_defs IBCFile
i),
String -> [(Name, Totality)] -> Maybe Entry
forall b. Binary b => String -> [b] -> Maybe Entry
makeEntry String
"ibc_total" (IBCFile -> [(Name, Totality)]
ibc_total IBCFile
i),
String -> [(Name, Bool)] -> Maybe Entry
forall b. Binary b => String -> [b] -> Maybe Entry
makeEntry String
"ibc_injective" (IBCFile -> [(Name, Bool)]
ibc_injective IBCFile
i),
String -> [(Name, Accessibility)] -> Maybe Entry
forall b. Binary b => String -> [b] -> Maybe Entry
makeEntry String
"ibc_access" (IBCFile -> [(Name, Accessibility)]
ibc_access IBCFile
i),
String -> [(Name, String)] -> Maybe Entry
forall b. Binary b => String -> [b] -> Maybe Entry
makeEntry String
"ibc_fragile" (IBCFile -> [(Name, String)]
ibc_fragile IBCFile
i),
String -> [LanguageExt] -> Maybe Entry
forall b. Binary b => String -> [b] -> Maybe Entry
makeEntry String
"ibc_langexts" (IBCFile -> [LanguageExt]
ibc_langexts IBCFile
i),
String -> [(String, Int)] -> Maybe Entry
forall b. Binary b => String -> [b] -> Maybe Entry
makeEntry String
"ibc_importhashes" (IBCFile -> [(String, Int)]
ibc_importhashes IBCFile
i)]
writeArchive :: FilePath -> IBCFile -> Idris ()
writeArchive :: String -> IBCFile -> Idris ()
writeArchive String
fp 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 (\Archive
x Entry
y -> Entry -> Archive -> Archive
addEntryToArchive Entry
y Archive
x) Archive
emptyArchive (IBCFile -> [Entry]
entries IBCFile
i)
IO () -> Idris ()
forall a. IO a -> Idris a
runIO (IO () -> Idris ()) -> IO () -> Idris ()
forall a b. (a -> b) -> a -> b
$ String -> ByteString -> IO ()
B.writeFile String
fp (Archive -> ByteString
fromArchive Archive
a)
writeIBC :: FilePath -> FilePath -> Idris ()
writeIBC :: String -> String -> Idris ()
writeIBC String
src String
f
= do
Int -> String -> Idris ()
logIBC Int
2 (String -> Idris ()) -> String -> Idris ()
forall a b. (a -> b) -> a -> b
$ String
"Writing IBC for: " String -> ShowS
forall a. [a] -> [a] -> [a]
++ ShowS
forall a. Show a => a -> String
show String
f
Int -> String -> Idris ()
iReport Int
2 (String -> Idris ()) -> String -> Idris ()
forall a b. (a -> b) -> a -> b
$ String
"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 Int
5 (String -> Idris ()) -> String -> Idris ()
forall a b. (a -> b) -> a -> b
$ String
"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
" = " 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 Int
2 String
"Written")
(\Err
c -> do Int -> String -> Idris ()
logIBC Int
2 (String -> Idris ()) -> String -> Idris ()
forall a b. (a -> b) -> a -> b
$ String
"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 Int
hash [] = Int -> Int
forall a. Num a => a -> a
abs Int
hash Int -> Int -> Int
forall a. Integral a => a -> a -> a
`mod` Int
0xffffffff
qhash Int
hash (Char
x:String
xs) = Int -> String -> Int
qhash (Int
hash Int -> Int -> Int
forall a. Num a => a -> a -> a
* Int
33 Int -> Int -> Int
forall a. Num a => a -> a -> a
+ Int -> Int
forall a b. (Integral a, Num b) => a -> b
fromIntegral (Char -> Int
forall a. Enum a => a -> Int
fromEnum Char
x)) String
xs
hashTerm :: Int -> Term -> Int
hashTerm :: Int -> Term -> Int
hashTerm Int
i Term
t = Int -> String -> Int
qhash (Int
i Int -> Int -> Int
forall a. Num a => a -> a -> a
* Int
5381) (Term -> String
forall a. Show a => a -> String
show Term
t)
hashName :: Int -> Name -> Int
hashName :: Int -> Name -> Int
hashName Int
i Name
n = Int -> String -> Int
qhash (Int
i Int -> Int -> Int
forall a. Num a => a -> a -> a
* Int
5381) (Name -> String
forall a. Show a => a -> String
show Name
n)
calculateHash :: IState -> IBCFile -> Int
calculateHash :: IState -> IBCFile -> Int
calculateHash IState
ist IBCFile
f
= let acc :: [(Name, Accessibility)]
acc = ((Name, Accessibility) -> Bool)
-> [(Name, Accessibility)] -> [(Name, Accessibility)]
forall a. (a -> Bool) -> [a] -> [a]
L.filter (Name, Accessibility) -> Bool
forall a. (a, Accessibility) -> Bool
exported (IBCFile -> [(Name, Accessibility)]
ibc_access IBCFile
f)
inl :: [(Name, [FnOpt])]
inl = ((Name, [FnOpt]) -> Bool) -> [(Name, [FnOpt])] -> [(Name, [FnOpt])]
forall a. (a -> Bool) -> [a] -> [a]
L.filter ([Name] -> (Name, [FnOpt]) -> Bool
forall a (t :: * -> *) (t :: * -> *).
(Eq a, Foldable t, Foldable t) =>
t a -> (a, t FnOpt) -> Bool
inlinable (((Name, Accessibility) -> Name)
-> [(Name, Accessibility)] -> [Name]
forall a b. (a -> b) -> [a] -> [b]
map (Name, Accessibility) -> Name
forall a b. (a, b) -> a
fst [(Name, Accessibility)]
acc)) (IBCFile -> [(Name, [FnOpt])]
ibc_flags IBCFile
f) in
[Name] -> [Term] -> Int
mkHashFrom (((Name, Accessibility) -> Name)
-> [(Name, Accessibility)] -> [Name]
forall a b. (a -> b) -> [a] -> [b]
map (Name, Accessibility) -> Name
forall a b. (a, b) -> a
fst [(Name, Accessibility)]
acc) ([(Name, Accessibility)] -> [Term]
getDefs [(Name, Accessibility)]
acc [Term] -> [Term] -> [Term]
forall a. [a] -> [a] -> [a]
++ ((Name, [FnOpt]) -> [Term]) -> [(Name, [FnOpt])] -> [Term]
forall (t :: * -> *) a b. Foldable t => (a -> [b]) -> t a -> [b]
L.concatMap (Name, [FnOpt]) -> [Term]
getFullDef [(Name, [FnOpt])]
inl)
where
mkHashFrom :: [Name] -> [Term] -> Int
mkHashFrom :: [Name] -> [Term] -> Int
mkHashFrom [Name]
ns [Term]
tms = [Int] -> Int
forall (t :: * -> *) a. (Foldable t, Num a) => t a -> a
sum ((Int -> Name -> Int) -> [Int] -> [Name] -> [Int]
forall a b c. (a -> b -> c) -> [a] -> [b] -> [c]
L.zipWith Int -> Name -> Int
hashName [Int
1..] [Name]
ns) Int -> Int -> Int
forall a. Num a => a -> a -> a
+
[Int] -> Int
forall (t :: * -> *) a. (Foldable t, Num a) => t a -> a
sum ((Int -> Term -> Int) -> [Int] -> [Term] -> [Int]
forall a b c. (a -> b -> c) -> [a] -> [b] -> [c]
L.zipWith Int -> Term -> Int
hashTerm [Int
1..] [Term]
tms)
exported :: (a, Accessibility) -> Bool
exported (a
_, Accessibility
Public) = Bool
True
exported (a
_, Accessibility
Frozen) = Bool
True
exported (a, Accessibility)
_ = Bool
False
inlinable :: t a -> (a, t FnOpt) -> Bool
inlinable t a
acc (a
n, t FnOpt
opts)
= a
n a -> t a -> Bool
forall (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 (\ (a
_, Term
x, Term
y) -> [Term
x, Term
y])
patDef :: Name -> [Term]
patDef :: Name -> [Term]
patDef Name
n
= case Name
-> Ctxt ([([(Name, Term)], Term, Term)], [PTerm])
-> Maybe ([([(Name, Term)], Term, Term)], [PTerm])
forall a. Name -> Ctxt a -> Maybe a
lookupCtxtExact Name
n (IState -> Ctxt ([([(Name, Term)], Term, Term)], [PTerm])
idris_patdefs IState
ist) of
Maybe ([([(Name, Term)], Term, Term)], [PTerm])
Nothing -> []
Just ([([(Name, Term)], Term, Term)]
tms, [PTerm]
_) -> [([(Name, Term)], Term, Term)] -> [Term]
forall a. [(a, Term, Term)] -> [Term]
findTms [([(Name, Term)], Term, Term)]
tms
getDefs :: [(Name, Accessibility)] -> [Term]
getDefs :: [(Name, Accessibility)] -> [Term]
getDefs [] = []
getDefs ((Name
n, Accessibility
Public) : [(Name, Accessibility)]
ns)
= let ts :: [Term]
ts = [(Name, Accessibility)] -> [Term]
getDefs [(Name, Accessibility)]
ns in
case Name -> Context -> Maybe Term
lookupTyExact Name
n (IState -> Context
tt_ctxt IState
ist) of
Maybe Term
Nothing -> [Term]
ts
Just Term
ty -> Term
ty Term -> [Term] -> [Term]
forall a. a -> [a] -> [a]
: Name -> [Term]
patDef Name
n [Term] -> [Term] -> [Term]
forall a. [a] -> [a] -> [a]
++ [Term]
ts
getDefs ((Name
n, Accessibility
Frozen) : [(Name, Accessibility)]
ns)
= let ts :: [Term]
ts = [(Name, Accessibility)] -> [Term]
getDefs [(Name, Accessibility)]
ns in
case Name -> Context -> Maybe Term
lookupTyExact Name
n (IState -> Context
tt_ctxt IState
ist) of
Maybe Term
Nothing -> [Term]
ts
Just Term
ty -> Term
ty Term -> [Term] -> [Term]
forall a. a -> [a] -> [a]
: [Term]
ts
getDefs ((Name, Accessibility)
_ : [(Name, Accessibility)]
ns) = [(Name, Accessibility)] -> [Term]
getDefs [(Name, Accessibility)]
ns
getFullDef :: (Name, [FnOpt]) -> [Term]
getFullDef :: (Name, [FnOpt]) -> [Term]
getFullDef (Name
n, [FnOpt]
_)
= case Name -> Context -> Maybe Term
lookupTyExact Name
n (IState -> Context
tt_ctxt IState
ist) of
Maybe Term
Nothing -> []
Just Term
ty -> Term
ty Term -> [Term] -> [Term]
forall a. a -> [a] -> [a]
: Name -> [Term]
patDef Name
n
writePkgIndex :: FilePath -> Idris ()
writePkgIndex :: String -> Idris ()
writePkgIndex 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 (\ (String
x, 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 Int
2 (String -> Idris ()) -> String -> Idris ()
forall a b. (a -> b) -> a -> b
$ String
"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]
++ String
" 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 Int
2 String
"Written")
(\Err
c -> do Int -> String -> Idris ()
logIBC Int
2 (String -> Idris ()) -> String -> Idris ()
forall a b. (a -> b) -> a -> b
$ String
"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 [] IBCFile
f = IBCFile -> Idris IBCFile
forall (m :: * -> *) a. Monad m => a -> m a
return IBCFile
f
mkIBC (IBCWrite
i:[IBCWrite]
is) IBCFile
f = do IState
ist <- Idris IState
getIState
Int -> String -> Idris ()
logIBC Int
5 (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
" " 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 IState
i (IBCFix FixDecl
d) 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 IState
i (IBCImp Name
n) IBCFile
f = case Name -> Ctxt [PArg] -> Maybe [PArg]
forall a. Name -> Ctxt a -> Maybe a
lookupCtxtExact Name
n (IState -> Ctxt [PArg]
idris_implicits IState
i) of
Just [PArg]
v -> IBCFile -> Idris IBCFile
forall (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 }
Maybe [PArg]
_ -> String -> Idris IBCFile
forall a. String -> Idris a
ifail String
"IBC write failed"
ibc IState
i (IBCStatic Name
n) IBCFile
f
= case Name -> Ctxt [Bool] -> Maybe [Bool]
forall a. Name -> Ctxt a -> Maybe a
lookupCtxtExact Name
n (IState -> Ctxt [Bool]
idris_statics IState
i) of
Just [Bool]
v -> IBCFile -> Idris IBCFile
forall (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 }
Maybe [Bool]
_ -> String -> Idris IBCFile
forall a. String -> Idris a
ifail String
"IBC write failed"
ibc IState
i (IBCInterface Name
n) IBCFile
f
= case Name -> Ctxt InterfaceInfo -> Maybe InterfaceInfo
forall a. Name -> Ctxt a -> Maybe a
lookupCtxtExact Name
n (IState -> Ctxt InterfaceInfo
idris_interfaces IState
i) of
Just InterfaceInfo
v -> IBCFile -> Idris IBCFile
forall (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 }
Maybe InterfaceInfo
_ -> String -> Idris IBCFile
forall a. String -> Idris a
ifail String
"IBC write failed"
ibc IState
i (IBCRecord Name
n) IBCFile
f
= case Name -> Ctxt RecordInfo -> Maybe RecordInfo
forall a. Name -> Ctxt a -> Maybe a
lookupCtxtExact Name
n (IState -> Ctxt RecordInfo
idris_records IState
i) of
Just RecordInfo
v -> IBCFile -> Idris IBCFile
forall (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 }
Maybe RecordInfo
_ -> String -> Idris IBCFile
forall a. String -> Idris a
ifail String
"IBC write failed"
ibc IState
i (IBCImplementation Bool
int Bool
res Name
n Name
ins) 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 IState
i (IBCDSL Name
n) IBCFile
f
= case Name -> Ctxt DSL -> Maybe DSL
forall a. Name -> Ctxt a -> Maybe a
lookupCtxtExact Name
n (IState -> Ctxt DSL
idris_dsls IState
i) of
Just DSL
v -> IBCFile -> Idris IBCFile
forall (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 }
Maybe DSL
_ -> String -> Idris IBCFile
forall a. String -> Idris a
ifail String
"IBC write failed"
ibc IState
i (IBCData Name
n) IBCFile
f
= case Name -> Ctxt TypeInfo -> Maybe TypeInfo
forall a. Name -> Ctxt a -> Maybe a
lookupCtxtExact Name
n (IState -> Ctxt TypeInfo
idris_datatypes IState
i) of
Just TypeInfo
v -> IBCFile -> Idris IBCFile
forall (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 }
Maybe TypeInfo
_ -> String -> Idris IBCFile
forall a. String -> Idris a
ifail String
"IBC write failed"
ibc IState
i (IBCOpt Name
n) IBCFile
f = case Name -> Ctxt OptInfo -> Maybe OptInfo
forall a. Name -> Ctxt a -> Maybe a
lookupCtxtExact Name
n (IState -> Ctxt OptInfo
idris_optimisation IState
i) of
Just OptInfo
v -> IBCFile -> Idris IBCFile
forall (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 }
Maybe OptInfo
_ -> String -> Idris IBCFile
forall a. String -> Idris a
ifail String
"IBC write failed"
ibc IState
i (IBCSyntax Syntax
n) 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 IState
i (IBCKeyword String
n) 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 IState
i (IBCImport (Bool, String)
n) 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 IState
i (IBCImportDir String
n) 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 IState
i (IBCSourceDir String
n) 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 IState
i (IBCObj Codegen
tgt String
n) 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 IState
i (IBCLib Codegen
tgt String
n) 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 IState
i (IBCCGFlag Codegen
tgt String
n) 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 IState
i (IBCDyLib String
n) 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 IState
i (IBCHeader Codegen
tgt String
n) 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 IState
i (IBCDef Name
n) IBCFile
f
= do IBCFile
f' <- case Name -> Context -> Maybe Def
lookupDefExact Name
n (IState -> Context
tt_ctxt IState
i) of
Just Def
v -> IBCFile -> Idris IBCFile
forall (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 }
Maybe Def
_ -> String -> Idris IBCFile
forall a. String -> Idris a
ifail String
"IBC write failed"
case Name
-> Ctxt ([([(Name, Term)], Term, Term)], [PTerm])
-> Maybe ([([(Name, Term)], Term, Term)], [PTerm])
forall a. Name -> Ctxt a -> Maybe a
lookupCtxtExact Name
n (IState -> Ctxt ([([(Name, Term)], Term, Term)], [PTerm])
idris_patdefs IState
i) of
Just ([([(Name, Term)], Term, Term)], [PTerm])
v -> IBCFile -> Idris IBCFile
forall (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 }
Maybe ([([(Name, Term)], Term, Term)], [PTerm])
_ -> IBCFile -> Idris IBCFile
forall (m :: * -> *) a. Monad m => a -> m a
return IBCFile
f'
ibc IState
i (IBCDoc Name
n) IBCFile
f = case Name
-> Ctxt (Docstring DocTerm, [(Name, Docstring DocTerm)])
-> Maybe (Docstring DocTerm, [(Name, Docstring DocTerm)])
forall a. Name -> Ctxt a -> Maybe a
lookupCtxtExact Name
n (IState -> Ctxt (Docstring DocTerm, [(Name, Docstring DocTerm)])
idris_docstrings IState
i) of
Just (Docstring DocTerm, [(Name, Docstring DocTerm)])
v -> IBCFile -> Idris IBCFile
forall (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 }
Maybe (Docstring DocTerm, [(Name, Docstring DocTerm)])
_ -> String -> Idris IBCFile
forall a. String -> Idris a
ifail String
"IBC write failed"
ibc IState
i (IBCCG Name
n) IBCFile
f = case Name -> Ctxt CGInfo -> Maybe CGInfo
forall a. Name -> Ctxt a -> Maybe a
lookupCtxtExact Name
n (IState -> Ctxt CGInfo
idris_callgraph IState
i) of
Just CGInfo
v -> IBCFile -> Idris IBCFile
forall (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 }
Maybe CGInfo
_ -> String -> Idris IBCFile
forall a. String -> Idris a
ifail String
"IBC write failed"
ibc IState
i (IBCCoercion Name
n) 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 IState
i (IBCAccess Name
n Accessibility
a) 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 IState
i (IBCFlags Name
n) IBCFile
f
= case Name -> Ctxt [FnOpt] -> Maybe [FnOpt]
forall a. Name -> Ctxt a -> Maybe a
lookupCtxtExact Name
n (IState -> Ctxt [FnOpt]
idris_flags IState
i) of
Just [FnOpt]
a -> IBCFile -> Idris IBCFile
forall (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 }
Maybe [FnOpt]
_ -> String -> Idris IBCFile
forall a. String -> Idris a
ifail String
"IBC write failed"
ibc IState
i (IBCFnInfo Name
n FnInfo
a) 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 IState
i (IBCTotal Name
n Totality
a) 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 IState
i (IBCInjective Name
n Bool
a) 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 IState
i (IBCTrans Name
n (Term, Term)
t) 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 IState
i (IBCErrRev (Term, Term)
t) 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 IState
i (IBCErrReduce Name
t) 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 IState
i (IBCLineApp String
fp Int
l PTerm
t) 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 IState
i (IBCNameHint (Name
n, Name
ty)) 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 IState
i (IBCMetaInformation Name
n MetaInformation
m) 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 IState
i (IBCErrorHandler Name
n) 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 IState
i (IBCFunctionErrorHandler Name
fn Name
a Name
n) 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 IState
i (IBCMetavar Name
n) IBCFile
f =
case Name
-> [(Name, (Maybe Name, Int, [Name], Bool, Bool))]
-> Maybe (Maybe Name, Int, [Name], Bool, Bool)
forall a b. Eq a => a -> [(a, b)] -> Maybe b
lookup Name
n (IState -> [(Name, (Maybe Name, Int, [Name], Bool, Bool))]
idris_metavars IState
i) of
Maybe (Maybe Name, Int, [Name], Bool, Bool)
Nothing -> IBCFile -> Idris IBCFile
forall (m :: * -> *) a. Monad m => a -> m a
return IBCFile
f
Just (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 IState
i (IBCPostulate Name
n) 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 IState
i (IBCExtern (Name, Int)
n) 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 IState
i (IBCTotCheckErr FC
fc String
err) 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 IState
i (IBCParsedRegion FC
fc) 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 IState
i (IBCModDocs Name
n) IBCFile
f = case Name -> Ctxt (Docstring DocTerm) -> Maybe (Docstring DocTerm)
forall a. Name -> Ctxt a -> Maybe a
lookupCtxtExact Name
n (IState -> Ctxt (Docstring DocTerm)
idris_moduledocs IState
i) of
Just Docstring DocTerm
v -> IBCFile -> Idris IBCFile
forall (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 }
Maybe (Docstring DocTerm)
_ -> String -> Idris IBCFile
forall a. String -> Idris a
ifail String
"IBC write failed"
ibc IState
i (IBCUsage (Name, Int)
n) 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 IState
i (IBCExport Name
n) 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 IState
i (IBCAutoHint Name
n Name
h) 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 IState
i (IBCDeprecate Name
n String
r) 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 IState
i (IBCFragile Name
n String
r) 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 IState
i (IBCConstraint FC
fc UConstraint
u) 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 IState
i (IBCImportHash String
fn Int
h) 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 b
alt String
f Archive
a = case String -> Archive -> Maybe Entry
findEntryByPath String
f Archive
a of
Maybe Entry
Nothing -> b -> Idris b
forall (m :: * -> *) a. Monad m => a -> m a
return b
alt
Just 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 IBCPhase
phase String
fp Archive
ar = do
Bool -> IBCPhase -> String -> Archive -> Idris ()
processImports Bool
True IBCPhase
phase String
fp Archive
ar
Bool -> IBCPhase -> Archive -> Idris ()
processAccess Bool
True IBCPhase
phase Archive
ar
process :: Bool
-> IBCPhase
-> Archive -> FilePath -> Idris ()
process :: Bool -> IBCPhase -> Archive -> String -> Idris ()
process Bool
reexp IBCPhase
phase Archive
archive String
fn = do
Word16
ver <- Word16 -> String -> Archive -> Idris Word16
forall b. (Binary b, NFData b) => b -> String -> Archive -> Idris b
getEntry Word16
0 String
"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 Int
2 String
"ibc out of date"
let e :: String
e = if Word16
ver Word16 -> Word16 -> Bool
forall a. Ord a => a -> a -> Bool
< Word16
ibcVersion
then String
"an earlier" else String
"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 String
"This external module"
else String
"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
Maybe String
Nothing -> String
"Please clean and rebuild."
Just String
ploc -> [String] -> String
unwords [String
"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 [String
"Incompatible ibc version for:", ShowS
forall a. Show a => a -> String
show String
fn]
, [String] -> String
unwords [String
start
, String
"was built with"
, String
e
, String
"version of Idris."]
, String
end
]
String
source <- String -> String -> Archive -> Idris String
forall b. (Binary b, NFData b) => b -> String -> Archive -> Idris b
getEntry String
"" String
"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 String
src 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 [ String
"Module needs reloading:"
, [String] -> String
unwords [String
"\tSRC :", ShowS
forall a. Show a => a -> String
show String
src]
, [String] -> String
unwords [String
"\tModified at:", UTCTime -> String
forall a. Show a => a -> String
show UTCTime
srct]
, [String] -> String
unwords [String
"\tIBC :", ShowS
forall a. Show a => a -> String
show String
ibc]
, [String] -> String
unwords [String
"\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 Archive
ar = do
[Name]
ns <- [Name] -> String -> Archive -> Idris [Name]
forall b. (Binary b, NFData b) => b -> String -> Archive -> Idris b
getEntry [] String
"ibc_postulates" Archive
ar
(IState -> IState) -> Idris ()
updateIState (\IState
i -> IState
i { idris_postulates :: Set Name
idris_postulates = IState -> Set Name
idris_postulates IState
i 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 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 [] String
"ibc_externs" Archive
ar
(IState -> IState) -> Idris ()
updateIState (\IState
i -> IState
i{ idris_externs :: Set (Name, Int)
idris_externs = IState -> Set (Name, Int)
idris_externs IState
i 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 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 String
"ibc_parsedSpan" Archive
ar
(IState -> IState) -> Idris ()
updateIState (\IState
i -> IState
i { idris_parsedSpan :: Maybe FC
idris_parsedSpan = Maybe FC
fc })
processUsage :: Archive -> Idris ()
processUsage :: Archive -> Idris ()
processUsage Archive
ar = do
[(Name, Int)]
ns <- [(Name, Int)] -> String -> Archive -> Idris [(Name, Int)]
forall b. (Binary b, NFData b) => b -> String -> Archive -> Idris b
getEntry [] String
"ibc_usage" Archive
ar
(IState -> IState) -> Idris ()
updateIState (\IState
i -> IState
i { idris_erasureUsed :: [(Name, Int)]
idris_erasureUsed = [(Name, Int)]
ns [(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 Archive
ar = do
[Name]
ns <- [Name] -> String -> Archive -> Idris [Name]
forall b. (Binary b, NFData b) => b -> String -> Archive -> Idris b
getEntry [] String
"ibc_exports" Archive
ar
(IState -> IState) -> Idris ()
updateIState (\IState
i -> IState
i { idris_exports :: [Name]
idris_exports = [Name]
ns [Name] -> [Name] -> [Name]
forall a. [a] -> [a] -> [a]
++ IState -> [Name]
idris_exports IState
i })
processAutoHints :: Archive -> Idris ()
processAutoHints :: Archive -> Idris ()
processAutoHints 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 [] String
"ibc_autohints" Archive
ar
((Name, Name) -> Idris ()) -> [(Name, Name)] -> Idris ()
forall (t :: * -> *) (m :: * -> *) a b.
(Foldable t, Monad m) =>
(a -> m b) -> t a -> m ()
mapM_ (\(Name
n,Name
h) -> Name -> Name -> Idris ()
addAutoHint Name
n Name
h) [(Name, Name)]
ns
processDeprecate :: Archive -> Idris ()
processDeprecate :: Archive -> Idris ()
processDeprecate Archive
ar = do
[(Name, String)]
ns <- [(Name, String)] -> String -> Archive -> Idris [(Name, String)]
forall b. (Binary b, NFData b) => b -> String -> Archive -> Idris b
getEntry [] String
"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_ (\(Name
n,String
reason) -> Name -> String -> Idris ()
addDeprecated Name
n String
reason) [(Name, String)]
ns
processFragile :: Archive -> Idris ()
processFragile :: Archive -> Idris ()
processFragile Archive
ar = do
[(Name, String)]
ns <- [(Name, String)] -> String -> Archive -> Idris [(Name, String)]
forall b. (Binary b, NFData b) => b -> String -> Archive -> Idris b
getEntry [] String
"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_ (\(Name
n,String
reason) -> Name -> String -> Idris ()
addFragile Name
n String
reason) [(Name, String)]
ns
processConstraints :: Archive -> Idris ()
processConstraints :: Archive -> Idris ()
processConstraints Archive
ar = do
[(FC, UConstraint)]
cs <- [(FC, UConstraint)]
-> String -> Archive -> Idris [(FC, UConstraint)]
forall b. (Binary b, NFData b) => b -> String -> Archive -> Idris b
getEntry [] String
"ibc_constraints" Archive
ar
((FC, UConstraint) -> Idris ()) -> [(FC, UConstraint)] -> Idris ()
forall (t :: * -> *) (m :: * -> *) a b.
(Foldable t, Monad m) =>
(a -> m b) -> t a -> m ()
mapM_ (\ (FC
fc, UConstraint
c) -> FC -> (Int, [UConstraint]) -> Idris ()
addConstraints FC
fc (Int
0, [UConstraint
c])) [(FC, UConstraint)]
cs
processImportDirs :: Archive -> Idris ()
processImportDirs :: Archive -> Idris ()
processImportDirs Archive
ar = do
[String]
fs <- [String] -> String -> Archive -> Idris [String]
forall b. (Binary b, NFData b) => b -> String -> Archive -> Idris b
getEntry [] String
"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 Archive
ar = do
[String]
fs <- [String] -> String -> Archive -> Idris [String]
forall b. (Binary b, NFData b) => b -> String -> Archive -> Idris b
getEntry [] String
"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 Bool
reexp IBCPhase
phase String
fname 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 [] String
"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_ (\(Bool
re, String
f) -> do
IState
i <- Idris IState
getIState
String
ibcsd <- IState -> Idris String
valIBCSubDir IState
i
[String]
ids <- String -> Idris [String]
rankedImportDirs String
fname
IState -> Idris ()
putIState (IState
i { imported :: [String]
imported = String
f String -> [String] -> [String]
forall a. a -> [a] -> [a]
: IState -> [String]
imported IState
i })
let (IBCPhase
phase', Bool
reexp') =
case IBCPhase
phase of
IBC_REPL Bool
True -> (Bool -> IBCPhase
IBC_REPL Bool
False, Bool
reexp)
IBC_REPL Bool
False -> (IBCPhase
IBC_Building, Bool
reexp Bool -> Bool -> Bool
&& Bool
re)
IBCPhase
p -> (IBCPhase
p, Bool
reexp Bool -> Bool -> Bool
&& Bool
re)
Maybe String
fp <- [String] -> String -> String -> Idris (Maybe String)
findIBC [String]
ids String
ibcsd String
f
Int -> String -> Idris ()
logIBC Int
4 (String -> Idris ()) -> String -> Idris ()
forall a b. (a -> b) -> a -> b
$ String
"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
Maybe String
Nothing -> do Int -> String -> Idris ()
logIBC Int
2 (String -> Idris ()) -> String -> Idris ()
forall a b. (a -> b) -> a -> b
$ String
"Failed to load ibc " String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
f
Just String
fn -> do Bool -> IBCPhase -> String -> Idris ()
loadIBC Bool
reexp' IBCPhase
phase' String
fn) [(Bool, String)]
fs
processImplicits :: Archive -> Idris ()
processImplicits :: Archive -> Idris ()
processImplicits Archive
ar = do
[(Name, [PArg])]
imps <- [(Name, [PArg])] -> String -> Archive -> Idris [(Name, [PArg])]
forall b. (Binary b, NFData b) => b -> String -> Archive -> Idris b
getEntry [] String
"ibc_implicits" Archive
ar
((Name, [PArg]) -> Idris ()) -> [(Name, [PArg])] -> Idris ()
forall (t :: * -> *) (m :: * -> *) a b.
(Foldable t, Monad m) =>
(a -> m b) -> t a -> m ()
mapM_ (\ (Name
n, [PArg]
imp) -> do
IState
i <- Idris IState
getIState
case Name -> Bool -> Context -> Maybe (Def, Accessibility)
lookupDefAccExact Name
n Bool
False (IState -> Context
tt_ctxt IState
i) of
Just (Def
n, Accessibility
Hidden) -> () -> Idris ()
forall (m :: * -> *) a. Monad m => a -> m a
return ()
Just (Def
n, Accessibility
Private) -> () -> Idris ()
forall (m :: * -> *) a. Monad m => a -> m a
return ()
Maybe (Def, Accessibility)
_ -> 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 Archive
ar = do
[FixDecl]
f <- [FixDecl] -> String -> Archive -> Idris [FixDecl]
forall b. (Binary b, NFData b) => b -> String -> Archive -> Idris b
getEntry [] String
"ibc_fixes" Archive
ar
(IState -> IState) -> Idris ()
updateIState (\IState
i -> IState
i { idris_infixes :: [FixDecl]
idris_infixes = [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 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 [] String
"ibc_statics" Archive
ar
((Name, [Bool]) -> Idris ()) -> [(Name, [Bool])] -> Idris ()
forall (t :: * -> *) (m :: * -> *) a b.
(Foldable t, Monad m) =>
(a -> m b) -> t a -> m ()
mapM_ (\ (Name
n, [Bool]
s) ->
(IState -> IState) -> Idris ()
updateIState (\IState
i -> IState
i { idris_statics :: 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 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 [] String
"ibc_interfaces" Archive
ar
((Name, InterfaceInfo) -> Idris ())
-> [(Name, InterfaceInfo)] -> Idris ()
forall (t :: * -> *) (m :: * -> *) a b.
(Foldable t, Monad m) =>
(a -> m b) -> t a -> m ()
mapM_ (\ (Name
n, InterfaceInfo
c) -> do
IState
i <- Idris IState
getIState
let is :: [(Name, Bool)]
is = case Name -> Ctxt InterfaceInfo -> Maybe InterfaceInfo
forall a. Name -> Ctxt a -> Maybe a
lookupCtxtExact Name
n (IState -> Ctxt InterfaceInfo
idris_interfaces IState
i) of
Just InterfaceInfo
ci -> InterfaceInfo -> [(Name, Bool)]
interface_implementations InterfaceInfo
ci
Maybe InterfaceInfo
_ -> []
let c' :: InterfaceInfo
c' = InterfaceInfo
c { interface_implementations :: [(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 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 [] String
"ibc_records" Archive
ar
((Name, RecordInfo) -> Idris ())
-> [(Name, RecordInfo)] -> Idris ()
forall (t :: * -> *) (m :: * -> *) a b.
(Foldable t, Monad m) =>
(a -> m b) -> t a -> m ()
mapM_ (\ (Name
n, RecordInfo
r) ->
(IState -> IState) -> Idris ()
updateIState (\IState
i -> IState
i { idris_records :: 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 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 [] String
"ibc_implementations" Archive
ar
((Bool, Bool, Name, Name) -> Idris ())
-> [(Bool, Bool, Name, Name)] -> Idris ()
forall (t :: * -> *) (m :: * -> *) a b.
(Foldable t, Monad m) =>
(a -> m b) -> t a -> m ()
mapM_ (\ (Bool
i, Bool
res, Name
n, Name
ins) -> Bool -> Bool -> Name -> Name -> Idris ()
addImplementation Bool
i Bool
res Name
n Name
ins) [(Bool, Bool, Name, Name)]
cs
processDSLs :: Archive -> Idris ()
processDSLs :: Archive -> Idris ()
processDSLs Archive
ar = do
[(Name, DSL)]
cs <- [(Name, DSL)] -> String -> Archive -> Idris [(Name, DSL)]
forall b. (Binary b, NFData b) => b -> String -> Archive -> Idris b
getEntry [] String
"ibc_dsls" Archive
ar
((Name, DSL) -> Idris ()) -> [(Name, DSL)] -> Idris ()
forall (t :: * -> *) (m :: * -> *) a b.
(Foldable t, Monad m) =>
(a -> m b) -> t a -> m ()
mapM_ (\ (Name
n, DSL
c) -> (IState -> IState) -> Idris ()
updateIState (\IState
i ->
IState
i { idris_dsls :: 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 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 [] String
"ibc_datatypes" Archive
ar
((Name, TypeInfo) -> Idris ()) -> [(Name, TypeInfo)] -> Idris ()
forall (t :: * -> *) (m :: * -> *) a b.
(Foldable t, Monad m) =>
(a -> m b) -> t a -> m ()
mapM_ (\ (Name
n, TypeInfo
c) -> (IState -> IState) -> Idris ()
updateIState (\IState
i ->
IState
i { idris_datatypes :: 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 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 [] String
"ibc_optimise" Archive
ar
((Name, OptInfo) -> Idris ()) -> [(Name, OptInfo)] -> Idris ()
forall (t :: * -> *) (m :: * -> *) a b.
(Foldable t, Monad m) =>
(a -> m b) -> t a -> m ()
mapM_ (\ (Name
n, OptInfo
c) -> (IState -> IState) -> Idris ()
updateIState (\IState
i ->
IState
i { idris_optimisation :: 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 Archive
ar = do
[Syntax]
s <- [Syntax] -> String -> Archive -> Idris [Syntax]
forall b. (Binary b, NFData b) => b -> String -> Archive -> Idris b
getEntry [] String
"ibc_syntax" Archive
ar
(IState -> IState) -> Idris ()
updateIState (\IState
i -> IState
i { syntax_rules :: SyntaxRules
syntax_rules = [Syntax] -> SyntaxRules -> SyntaxRules
updateSyntaxRules [Syntax]
s (IState -> SyntaxRules
syntax_rules IState
i) })
processKeywords :: Archive -> Idris ()
processKeywords :: Archive -> Idris ()
processKeywords Archive
ar = do
[String]
k <- [String] -> String -> Archive -> Idris [String]
forall b. (Binary b, NFData b) => b -> String -> Archive -> Idris b
getEntry [] String
"ibc_keywords" Archive
ar
(IState -> IState) -> Idris ()
updateIState (\IState
i -> IState
i { syntax_keywords :: [String]
syntax_keywords = [String]
k [String] -> [String] -> [String]
forall a. [a] -> [a] -> [a]
++ IState -> [String]
syntax_keywords IState
i })
processObjectFiles :: FilePath -> Archive -> Idris ()
processObjectFiles :: String -> Archive -> Idris ()
processObjectFiles String
fn Archive
ar = do
[(Codegen, String)]
os <- [(Codegen, String)]
-> String -> Archive -> Idris [(Codegen, String)]
forall b. (Binary b, NFData b) => b -> String -> Archive -> Idris b
getEntry [] String
"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_ (\ (Codegen
cg, 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 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 [] String
"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 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 [] String
"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 Archive
ar = do
[String]
ls <- [String] -> String -> Archive -> Idris [String]
forall b. (Binary b, NFData b) => b -> String -> Archive -> Idris b
getEntry [] String
"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 a
_) = () -> Idris ()
forall (m :: * -> *) a. Monad m => a -> m a
return ()
checkLoad (Right String
err) = String -> Idris ()
forall a. String -> Idris a
ifail String
err
processHeaders :: Archive -> Idris ()
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 [] String
"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 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 [] String
"ibc_patdefs" Archive
ar
((Name, ([([(Name, Term)], Term, Term)], [PTerm])) -> Idris ())
-> [(Name, ([([(Name, Term)], Term, Term)], [PTerm]))] -> Idris ()
forall (t :: * -> *) (m :: * -> *) a b.
(Foldable t, Monad m) =>
(a -> m b) -> t a -> m ()
mapM_ (\ (Name
n, ([([(Name, Term)], Term, Term)], [PTerm])
d) -> (IState -> IState) -> Idris ()
updateIState (\IState
i ->
IState
i { idris_patdefs :: 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 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 [] String
"ibc_defs" Archive
ar
Int -> String -> Idris ()
logIBC Int
4 (String -> Idris ()) -> String -> Idris ()
forall a b. (a -> b) -> a -> b
$ String
"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_ (\ (Name
n, Def
d) -> do
Def
d' <- Def -> StateT IState (ExceptT Err IO) Def
updateDef Def
d
case Def
d' of
TyDecl NameType
_ Term
_ -> () -> Idris ()
forall (m :: * -> *) a. Monad m => a -> m a
return ()
Def
_ -> do
Int -> String -> Idris ()
logIBC Int
2 (String -> Idris ()) -> String -> Idris ()
forall a b. (a -> b) -> a -> b
$ String
"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 (\IState
i -> IState
i { tt_ctxt :: Context
tt_ctxt = Name -> Def -> Context -> Context
addCtxtDef Name
n Def
d' (IState -> Context
tt_ctxt IState
i) })) [(Name, Def)]
ds
where
updateDef :: Def -> StateT IState (ExceptT Err IO) Def
updateDef (CaseOp CaseInfo
c Term
t [(Term, Bool)]
args [Either Term (Term, Term)]
o [([Name], Term, Term)]
s CaseDefs
cd) = do
[Either Term (Term, Term)]
o' <- (Either Term (Term, Term)
-> StateT IState (ExceptT Err IO) (Either Term (Term, Term)))
-> [Either Term (Term, Term)]
-> StateT IState (ExceptT Err IO) [Either Term (Term, Term)]
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
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 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 Term
t) = (Term -> Either Term (Term, Term))
-> StateT IState (ExceptT Err IO) Term
-> StateT IState (ExceptT Err IO) (Either Term (Term, Term))
forall (m :: * -> *) a1 r. Monad m => (a1 -> r) -> m a1 -> m r
liftM Term -> Either Term (Term, Term)
forall a b. a -> Either a b
Left (Term -> StateT IState (ExceptT Err IO) Term
update Term
t)
updateOrig (Right (Term
l, Term
r)) = do
Term
l' <- Term -> StateT IState (ExceptT Err IO) Term
update Term
l
Term
r' <- Term -> StateT IState (ExceptT Err IO) Term
update Term
r
Either Term (Term, Term)
-> StateT IState (ExceptT Err IO) (Either Term (Term, Term))
forall (m :: * -> *) a. Monad m => a -> m a
return (Either Term (Term, Term)
-> StateT IState (ExceptT Err IO) (Either Term (Term, Term)))
-> Either Term (Term, Term)
-> StateT IState (ExceptT Err IO) (Either Term (Term, Term))
forall a b. (a -> b) -> a -> b
$ (Term, Term) -> Either Term (Term, Term)
forall a b. b -> Either a b
Right (Term
l', Term
r')
updateCD :: CaseDefs -> StateT IState (ExceptT Err IO) CaseDefs
updateCD (CaseDefs ([Name]
cs, SC
c) ([Name]
rs, SC
r)) = do
SC
c' <- SC -> StateT IState (ExceptT Err IO) SC
updateSC SC
c
SC
r' <- SC -> StateT IState (ExceptT Err IO) SC
updateSC SC
r
CaseDefs -> StateT IState (ExceptT Err IO) CaseDefs
forall (m :: * -> *) a. Monad m => a -> m a
return (CaseDefs -> StateT IState (ExceptT Err IO) CaseDefs)
-> CaseDefs -> StateT IState (ExceptT Err IO) CaseDefs
forall a b. (a -> b) -> a -> b
$ ([Name], SC) -> ([Name], SC) -> CaseDefs
CaseDefs ([Name]
cs, SC
c') ([Name]
rs, SC
r')
updateSC :: SC -> StateT IState (ExceptT Err IO) SC
updateSC (Case CaseType
t Name
n [CaseAlt' Term]
alts) = do
[CaseAlt' Term]
alts' <- (CaseAlt' Term -> StateT IState (ExceptT Err IO) (CaseAlt' Term))
-> [CaseAlt' Term]
-> StateT IState (ExceptT Err IO) [CaseAlt' Term]
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
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 Term
t [CaseAlt' Term]
alts) = do
[CaseAlt' Term]
alts' <- (CaseAlt' Term -> StateT IState (ExceptT Err IO) (CaseAlt' Term))
-> [CaseAlt' Term]
-> StateT IState (ExceptT Err IO) [CaseAlt' Term]
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
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 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 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 Name
n Int
i [Name]
ns SC
t) = do
SC
t' <- SC -> StateT IState (ExceptT Err IO) SC
updateSC SC
t
CaseAlt' Term -> StateT IState (ExceptT Err IO) (CaseAlt' Term)
forall (m :: * -> *) a. Monad m => a -> m a
return (Name -> Int -> [Name] -> SC -> CaseAlt' Term
forall t. Name -> Int -> [Name] -> SC' t -> CaseAlt' t
ConCase Name
n Int
i [Name]
ns SC
t')
updateAlt (FnCase Name
n [Name]
ns SC
t) = do
SC
t' <- SC -> StateT IState (ExceptT Err IO) SC
updateSC SC
t
CaseAlt' Term -> StateT IState (ExceptT Err IO) (CaseAlt' Term)
forall (m :: * -> *) a. Monad m => a -> m a
return (Name -> [Name] -> SC -> CaseAlt' Term
forall t. Name -> [Name] -> SC' t -> CaseAlt' t
FnCase Name
n [Name]
ns SC
t')
updateAlt (ConstCase Const
c SC
t) = do
SC
t' <- SC -> StateT IState (ExceptT Err IO) SC
updateSC SC
t
CaseAlt' Term -> StateT IState (ExceptT Err IO) (CaseAlt' Term)
forall (m :: * -> *) a. Monad m => a -> m a
return (Const -> SC -> CaseAlt' Term
forall t. Const -> SC' t -> CaseAlt' t
ConstCase Const
c SC
t')
updateAlt (SucCase Name
n SC
t) = do
SC
t' <- SC -> StateT IState (ExceptT Err IO) SC
updateSC SC
t
CaseAlt' Term -> StateT IState (ExceptT Err IO) (CaseAlt' Term)
forall (m :: * -> *) a. Monad m => a -> m a
return (Name -> SC -> CaseAlt' Term
forall t. Name -> SC' t -> CaseAlt' t
SucCase Name
n SC
t')
updateAlt (DefaultCase SC
t) = do
SC
t' <- SC -> StateT IState (ExceptT Err IO) SC
updateSC SC
t
CaseAlt' Term -> StateT IState (ExceptT Err IO) (CaseAlt' Term)
forall (m :: * -> *) a. Monad m => a -> m a
return (SC -> CaseAlt' Term
forall t. SC' t -> CaseAlt' t
DefaultCase SC
t')
update :: Term -> StateT IState (ExceptT Err IO) Term
update Term
t = do
Maybe Term
tm <- Term -> Idris (Maybe Term)
addTT Term
t
case Maybe Term
tm of
Maybe Term
Nothing -> Term -> StateT IState (ExceptT Err IO) Term
update' Term
t
Just Term
t' -> Term -> StateT IState (ExceptT Err IO) Term
forall (m :: * -> *) a. Monad m => a -> m a
return Term
t'
update' :: Term -> StateT IState (ExceptT Err IO) Term
update' (P NameType
t Name
n Term
ty) = do
Name
n' <- Name -> Idris Name
getSymbol Name
n
Term -> StateT IState (ExceptT Err IO) Term
forall (m :: * -> *) a. Monad m => a -> m a
return (Term -> StateT IState (ExceptT Err IO) Term)
-> Term -> StateT IState (ExceptT Err IO) Term
forall a b. (a -> b) -> a -> b
$ NameType -> Name -> Term -> Term
forall n. NameType -> n -> TT n -> TT n
P NameType
t Name
n' Term
ty
update' (App AppStatus Name
s Term
f Term
a) = (Term -> Term -> Term)
-> StateT IState (ExceptT Err IO) Term
-> StateT IState (ExceptT Err IO) Term
-> StateT IState (ExceptT Err IO) Term
forall (m :: * -> *) a1 a2 r.
Monad m =>
(a1 -> a2 -> r) -> m a1 -> m a2 -> m r
liftM2 (AppStatus Name -> Term -> Term -> Term
forall n. AppStatus n -> TT n -> TT n -> TT n
App AppStatus Name
s) (Term -> StateT IState (ExceptT Err IO) Term
update' Term
f) (Term -> StateT IState (ExceptT Err IO) Term
update' Term
a)
update' (Bind Name
n Binder Term
b Term
sc) = do
Binder Term
b' <- Binder Term -> StateT IState (ExceptT Err IO) (Binder Term)
updateB Binder Term
b
Term
sc' <- Term -> StateT IState (ExceptT Err IO) Term
update Term
sc
Term -> StateT IState (ExceptT Err IO) Term
forall (m :: * -> *) a. Monad m => a -> m a
return (Term -> StateT IState (ExceptT Err IO) Term)
-> Term -> StateT IState (ExceptT Err IO) Term
forall a b. (a -> b) -> a -> b
$ Name -> Binder Term -> Term -> Term
forall n. n -> Binder (TT n) -> TT n -> TT n
Bind Name
n Binder Term
b' Term
sc'
where
updateB :: Binder Term -> StateT IState (ExceptT Err IO) (Binder Term)
updateB (Let RigCount
rig Term
t Term
v) = (Term -> Term -> Binder Term)
-> StateT IState (ExceptT Err IO) Term
-> StateT IState (ExceptT Err IO) Term
-> StateT IState (ExceptT Err IO) (Binder Term)
forall (m :: * -> *) a1 a2 r.
Monad m =>
(a1 -> a2 -> r) -> m a1 -> m a2 -> m r
liftM2 (RigCount -> Term -> Term -> Binder Term
forall b. RigCount -> b -> b -> Binder b
Let RigCount
rig) (Term -> StateT IState (ExceptT Err IO) Term
update' Term
t) (Term -> StateT IState (ExceptT Err IO) Term
update' Term
v)
updateB Binder Term
b = do
Term
ty' <- Term -> StateT IState (ExceptT Err IO) Term
update' (Binder Term -> Term
forall b. Binder b -> b
binderTy Binder Term
b)
Binder Term -> StateT IState (ExceptT Err IO) (Binder Term)
forall (m :: * -> *) a. Monad m => a -> m a
return (Binder Term
b { binderTy :: Term
binderTy = Term
ty' })
update' (Proj Term
t Int
i) = do
Term
t' <- Term -> StateT IState (ExceptT Err IO) Term
update' Term
t
Term -> StateT IState (ExceptT Err IO) Term
forall (m :: * -> *) a. Monad m => a -> m a
return (Term -> StateT IState (ExceptT Err IO) Term)
-> Term -> StateT IState (ExceptT Err IO) Term
forall a b. (a -> b) -> a -> b
$ Term -> Int -> Term
forall n. TT n -> Int -> TT n
Proj Term
t' Int
i
update' Term
t = Term -> StateT IState (ExceptT Err IO) Term
forall (m :: * -> *) a. Monad m => a -> m a
return Term
t
processDocs :: Archive -> Idris ()
processDocs :: Archive -> Idris ()
processDocs Archive
ar = do
[(Name, (Docstring DocTerm, [(Name, Docstring DocTerm)]))]
ds <- [(Name, (Docstring DocTerm, [(Name, Docstring DocTerm)]))]
-> String
-> Archive
-> Idris [(Name, (Docstring DocTerm, [(Name, Docstring DocTerm)]))]
forall b. (Binary b, NFData b) => b -> String -> Archive -> Idris b
getEntry [] String
"ibc_docstrings" Archive
ar
((Name, (Docstring DocTerm, [(Name, Docstring DocTerm)]))
-> Idris ())
-> [(Name, (Docstring DocTerm, [(Name, Docstring DocTerm)]))]
-> Idris ()
forall (t :: * -> *) (m :: * -> *) a b.
(Foldable t, Monad m) =>
(a -> m b) -> t a -> m ()
mapM_ (\(Name
n, (Docstring DocTerm, [(Name, Docstring DocTerm)])
a) -> Name
-> Docstring DocTerm -> [(Name, Docstring DocTerm)] -> Idris ()
addDocStr Name
n ((Docstring DocTerm, [(Name, Docstring DocTerm)])
-> Docstring DocTerm
forall a b. (a, b) -> a
fst (Docstring DocTerm, [(Name, Docstring DocTerm)])
a) ((Docstring DocTerm, [(Name, Docstring DocTerm)])
-> [(Name, Docstring DocTerm)]
forall a b. (a, b) -> b
snd (Docstring DocTerm, [(Name, Docstring DocTerm)])
a)) [(Name, (Docstring DocTerm, [(Name, Docstring DocTerm)]))]
ds
processModuleDocs :: Archive -> Idris ()
processModuleDocs :: Archive -> Idris ()
processModuleDocs Archive
ar = do
[(Name, Docstring DocTerm)]
ds <- [(Name, Docstring DocTerm)]
-> String -> Archive -> Idris [(Name, Docstring DocTerm)]
forall b. (Binary b, NFData b) => b -> String -> Archive -> Idris b
getEntry [] String
"ibc_moduledocs" Archive
ar
((Name, Docstring DocTerm) -> Idris ())
-> [(Name, Docstring DocTerm)] -> Idris ()
forall (t :: * -> *) (m :: * -> *) a b.
(Foldable t, Monad m) =>
(a -> m b) -> t a -> m ()
mapM_ (\ (Name
n, Docstring DocTerm
d) -> (IState -> IState) -> Idris ()
updateIState (\IState
i ->
IState
i { idris_moduledocs :: 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
-> IBCPhase
-> Archive -> Idris ()
processAccess :: Bool -> IBCPhase -> Archive -> Idris ()
processAccess Bool
reexp IBCPhase
phase Archive
ar = do
Int -> String -> Idris ()
logIBC Int
3 (String -> Idris ()) -> String -> Idris ()
forall a b. (a -> b) -> a -> b
$ String
"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 [] String
"ibc_access" Archive
ar
Int -> String -> Idris ()
logIBC Int
3 (String -> Idris ()) -> String -> Idris ()
forall a b. (a -> b) -> a -> b
$ String
"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_ (\ (Name
n, Accessibility
a_in) -> do
let a :: Accessibility
a = if Bool
reexp then Accessibility
a_in else Accessibility
Hidden
Int -> String -> Idris ()
logIBC Int
3 (String -> Idris ()) -> String -> Idris ()
forall a b. (a -> b) -> a -> b
$ String
"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]
++ String
" to " String -> ShowS
forall a. [a] -> [a] -> [a]
++ Accessibility -> String
forall a. Show a => a -> String
show Accessibility
a
(IState -> IState) -> Idris ()
updateIState (\IState
i -> IState
i { tt_ctxt :: Context
tt_ctxt = Name -> Accessibility -> Context -> Context
setAccess Name
n Accessibility
a (IState -> Context
tt_ctxt IState
i) })
if (Bool -> Bool
not Bool
reexp)
then do
Int -> String -> Idris ()
logIBC Int
2 (String -> Idris ()) -> String -> Idris ()
forall a b. (a -> b) -> a -> b
$ String
"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 Int
2 (String -> Idris ()) -> String -> Idris ()
forall a b. (a -> b) -> a -> b
$ String
"Exporting " String -> ShowS
forall a. [a] -> [a] -> [a]
++ Name -> String
forall a. Show a => a -> String
show Name
n
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 Int
2 (String -> Idris ()) -> String -> Idris ()
forall a b. (a -> b) -> a -> b
$ String
"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 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 [] String
"ibc_flags" Archive
ar
((Name, [FnOpt]) -> Idris ()) -> [(Name, [FnOpt])] -> Idris ()
forall (t :: * -> *) (m :: * -> *) a b.
(Foldable t, Monad m) =>
(a -> m b) -> t a -> m ()
mapM_ (\ (Name
n, [FnOpt]
a) -> Name -> [FnOpt] -> Idris ()
setFlags Name
n [FnOpt]
a) [(Name, [FnOpt])]
ds
processFnInfo :: Archive -> Idris ()
processFnInfo :: Archive -> Idris ()
processFnInfo Archive
ar = do
[(Name, FnInfo)]
ds <- [(Name, FnInfo)] -> String -> Archive -> Idris [(Name, FnInfo)]
forall b. (Binary b, NFData b) => b -> String -> Archive -> Idris b
getEntry [] String
"ibc_fninfo" Archive
ar
((Name, FnInfo) -> Idris ()) -> [(Name, FnInfo)] -> Idris ()
forall (t :: * -> *) (m :: * -> *) a b.
(Foldable t, Monad m) =>
(a -> m b) -> t a -> m ()
mapM_ (\ (Name
n, FnInfo
a) -> Name -> FnInfo -> Idris ()
setFnInfo Name
n FnInfo
a) [(Name, FnInfo)]
ds
processTotal :: Archive -> Idris ()
processTotal :: Archive -> Idris ()
processTotal Archive
ar = do
[(Name, Totality)]
ds <- [(Name, Totality)] -> String -> Archive -> Idris [(Name, Totality)]
forall b. (Binary b, NFData b) => b -> String -> Archive -> Idris b
getEntry [] String
"ibc_total" Archive
ar
((Name, Totality) -> Idris ()) -> [(Name, Totality)] -> Idris ()
forall (t :: * -> *) (m :: * -> *) a b.
(Foldable t, Monad m) =>
(a -> m b) -> t a -> m ()
mapM_ (\ (Name
n, Totality
a) -> (IState -> IState) -> Idris ()
updateIState (\IState
i -> IState
i { tt_ctxt :: Context
tt_ctxt = Name -> Totality -> Context -> Context
setTotal Name
n Totality
a (IState -> Context
tt_ctxt IState
i) })) [(Name, Totality)]
ds
processInjective :: Archive -> Idris ()
processInjective :: Archive -> Idris ()
processInjective Archive
ar = do
[(Name, Bool)]
ds <- [(Name, Bool)] -> String -> Archive -> Idris [(Name, Bool)]
forall b. (Binary b, NFData b) => b -> String -> Archive -> Idris b
getEntry [] String
"ibc_injective" Archive
ar
((Name, Bool) -> Idris ()) -> [(Name, Bool)] -> Idris ()
forall (t :: * -> *) (m :: * -> *) a b.
(Foldable t, Monad m) =>
(a -> m b) -> t a -> m ()
mapM_ (\ (Name
n, Bool
a) -> (IState -> IState) -> Idris ()
updateIState (\IState
i -> IState
i { tt_ctxt :: Context
tt_ctxt = Name -> Bool -> Context -> Context
setInjective Name
n Bool
a (IState -> Context
tt_ctxt IState
i) })) [(Name, Bool)]
ds
processTotalityCheckError :: Archive -> Idris ()
processTotalityCheckError :: Archive -> Idris ()
processTotalityCheckError Archive
ar = do
[(FC, String)]
es <- [(FC, String)] -> String -> Archive -> Idris [(FC, String)]
forall b. (Binary b, NFData b) => b -> String -> Archive -> Idris b
getEntry [] String
"ibc_totcheckfail" Archive
ar
(IState -> IState) -> Idris ()
updateIState (\IState
i -> IState
i { idris_totcheckfail :: [(FC, String)]
idris_totcheckfail = IState -> [(FC, String)]
idris_totcheckfail IState
i [(FC, String)] -> [(FC, String)] -> [(FC, String)]
forall a. [a] -> [a] -> [a]
++ [(FC, String)]
es })
processCallgraph :: Archive -> Idris ()
processCallgraph :: Archive -> Idris ()
processCallgraph 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 [] String
"ibc_cg" Archive
ar
((Name, CGInfo) -> Idris ()) -> [(Name, CGInfo)] -> Idris ()
forall (t :: * -> *) (m :: * -> *) a b.
(Foldable t, Monad m) =>
(a -> m b) -> t a -> m ()
mapM_ (\ (Name
n, CGInfo
a) -> Name -> CGInfo -> Idris ()
addToCG Name
n CGInfo
a) [(Name, CGInfo)]
ds
processCoercions :: Archive -> Idris ()
processCoercions :: Archive -> Idris ()
processCoercions Archive
ar = do
[Name]
ns <- [Name] -> String -> Archive -> Idris [Name]
forall b. (Binary b, NFData b) => b -> String -> Archive -> Idris b
getEntry [] String
"ibc_coercions" Archive
ar
(Name -> Idris ()) -> [Name] -> Idris ()
forall (t :: * -> *) (m :: * -> *) a b.
(Foldable t, Monad m) =>
(a -> m b) -> t a -> m ()
mapM_ (\ Name
n -> Name -> Idris ()
addCoercion Name
n) [Name]
ns
processTransforms :: Archive -> Idris ()
processTransforms :: Archive -> Idris ()
processTransforms Archive
ar = do
[(Name, (Term, Term))]
ts <- [(Name, (Term, Term))]
-> String -> Archive -> Idris [(Name, (Term, Term))]
forall b. (Binary b, NFData b) => b -> String -> Archive -> Idris b
getEntry [] String
"ibc_transforms" Archive
ar
((Name, (Term, Term)) -> Idris ())
-> [(Name, (Term, Term))] -> Idris ()
forall (t :: * -> *) (m :: * -> *) a b.
(Foldable t, Monad m) =>
(a -> m b) -> t a -> m ()
mapM_ (\ (Name
n, (Term, Term)
t) -> Name -> (Term, Term) -> Idris ()
addTrans Name
n (Term, Term)
t) [(Name, (Term, Term))]
ts
processErrRev :: Archive -> Idris ()
processErrRev :: Archive -> Idris ()
processErrRev Archive
ar = do
[(Term, Term)]
ts <- [(Term, Term)] -> String -> Archive -> Idris [(Term, Term)]
forall b. (Binary b, NFData b) => b -> String -> Archive -> Idris b
getEntry [] String
"ibc_errRev" Archive
ar
((Term, Term) -> Idris ()) -> [(Term, Term)] -> Idris ()
forall (t :: * -> *) (m :: * -> *) a b.
(Foldable t, Monad m) =>
(a -> m b) -> t a -> m ()
mapM_ (Term, Term) -> Idris ()
addErrRev [(Term, Term)]
ts
processErrReduce :: Archive -> Idris ()
processErrReduce :: Archive -> Idris ()
processErrReduce Archive
ar = do
[Name]
ts <- [Name] -> String -> Archive -> Idris [Name]
forall b. (Binary b, NFData b) => b -> String -> Archive -> Idris b
getEntry [] String
"ibc_errReduce" Archive
ar
(Name -> Idris ()) -> [Name] -> Idris ()
forall (t :: * -> *) (m :: * -> *) a b.
(Foldable t, Monad m) =>
(a -> m b) -> t a -> m ()
mapM_ Name -> Idris ()
addErrReduce [Name]
ts
processLineApps :: Archive -> Idris ()
processLineApps :: Archive -> Idris ()
processLineApps Archive
ar = do
[(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 [] String
"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_ (\ (String
f, Int
i, PTerm
t) -> String -> Int -> PTerm -> Idris ()
addInternalApp String
f Int
i PTerm
t) [(String, Int, PTerm)]
ls
processNameHints :: Archive -> Idris ()
processNameHints :: Archive -> Idris ()
processNameHints Archive
ar = do
[(Name, Name)]
ns <- [(Name, Name)] -> String -> Archive -> Idris [(Name, Name)]
forall b. (Binary b, NFData b) => b -> String -> Archive -> Idris b
getEntry [] String
"ibc_namehints" Archive
ar
((Name, Name) -> Idris ()) -> [(Name, Name)] -> Idris ()
forall (t :: * -> *) (m :: * -> *) a b.
(Foldable t, Monad m) =>
(a -> m b) -> t a -> m ()
mapM_ (\ (Name
n, Name
ty) -> Name -> Name -> Idris ()
addNameHint Name
n Name
ty) [(Name, Name)]
ns
processMetaInformation :: Archive -> Idris ()
processMetaInformation :: Archive -> Idris ()
processMetaInformation Archive
ar = do
[(Name, MetaInformation)]
ds <- [(Name, MetaInformation)]
-> String -> Archive -> Idris [(Name, MetaInformation)]
forall b. (Binary b, NFData b) => b -> String -> Archive -> Idris b
getEntry [] String
"ibc_metainformation" Archive
ar
((Name, MetaInformation) -> Idris ())
-> [(Name, MetaInformation)] -> Idris ()
forall (t :: * -> *) (m :: * -> *) a b.
(Foldable t, Monad m) =>
(a -> m b) -> t a -> m ()
mapM_ (\ (Name
n, MetaInformation
m) -> (IState -> IState) -> Idris ()
updateIState (\IState
i ->
IState
i { tt_ctxt :: Context
tt_ctxt = Name -> MetaInformation -> Context -> Context
setMetaInformation Name
n MetaInformation
m (IState -> Context
tt_ctxt IState
i) })) [(Name, MetaInformation)]
ds
processErrorHandlers :: Archive -> Idris ()
processErrorHandlers :: Archive -> Idris ()
processErrorHandlers Archive
ar = do
[Name]
ns <- [Name] -> String -> Archive -> Idris [Name]
forall b. (Binary b, NFData b) => b -> String -> Archive -> Idris b
getEntry [] String
"ibc_errorhandlers" Archive
ar
(IState -> IState) -> Idris ()
updateIState (\IState
i -> IState
i { idris_errorhandlers :: [Name]
idris_errorhandlers = IState -> [Name]
idris_errorhandlers IState
i [Name] -> [Name] -> [Name]
forall a. [a] -> [a] -> [a]
++ [Name]
ns })
processFunctionErrorHandlers :: Archive -> Idris ()
processFunctionErrorHandlers :: Archive -> Idris ()
processFunctionErrorHandlers 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 [] String
"ibc_function_errorhandlers" Archive
ar
((Name, Name, Name) -> Idris ())
-> [(Name, Name, Name)] -> Idris ()
forall (t :: * -> *) (m :: * -> *) a b.
(Foldable t, Monad m) =>
(a -> m b) -> t a -> m ()
mapM_ (\ (Name
fn,Name
arg,Name
handler) -> Name -> Name -> [Name] -> Idris ()
addFunctionErrorHandlers Name
fn Name
arg [Name
handler]) [(Name, Name, Name)]
ns
processMetaVars :: Archive -> Idris ()
processMetaVars :: Archive -> Idris ()
processMetaVars Archive
ar = do
[(Name, (Maybe Name, Int, [Name], Bool, Bool))]
ns <- [(Name, (Maybe Name, Int, [Name], Bool, Bool))]
-> String
-> Archive
-> Idris [(Name, (Maybe Name, Int, [Name], Bool, Bool))]
forall b. (Binary b, NFData b) => b -> String -> Archive -> Idris b
getEntry [] String
"ibc_metavars" Archive
ar
(IState -> IState) -> Idris ()
updateIState (\IState
i -> IState
i { idris_metavars :: [(Name, (Maybe Name, Int, [Name], Bool, Bool))]
idris_metavars = [(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 })
processLangExts :: IBCPhase -> Archive -> Idris ()
processLangExts :: IBCPhase -> Archive -> Idris ()
processLangExts (IBC_REPL Bool
True) Archive
ar
= do [LanguageExt]
ds <- [LanguageExt] -> String -> Archive -> Idris [LanguageExt]
forall b. (Binary b, NFData b) => b -> String -> Archive -> Idris b
getEntry [] String
"ibc_langexts" Archive
ar
(LanguageExt -> Idris ()) -> [LanguageExt] -> Idris ()
forall (t :: * -> *) (m :: * -> *) a b.
(Foldable t, Monad m) =>
(a -> m b) -> t a -> m ()
mapM_ LanguageExt -> Idris ()
addLangExt [LanguageExt]
ds
processLangExts IBCPhase
_ Archive
_ = () -> Idris ()
forall (m :: * -> *) a. Monad m => a -> m a
return ()
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
instance Binary SizeChange
instance Binary CGInfo where
put :: CGInfo -> Put
put (CGInfo [Name]
x1 Maybe [Name]
x2 [SCGEntry]
x3 [(Int, [(Name, Int)])]
x4)
= do [Name] -> Put
forall t. Binary t => t -> Put
put [Name]
x1
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 Def
x
= {-# SCC "putDef" #-}
case Def
x of
Function Term
x1 Term
x2 -> do Word8 -> Put
putWord8 Word8
0
Term -> Put
forall t. Binary t => t -> Put
put Term
x1
Term -> Put
forall t. Binary t => t -> Put
put Term
x2
TyDecl NameType
x1 Term
x2 -> do Word8 -> Put
putWord8 Word8
1
NameType -> Put
forall t. Binary t => t -> Put
put NameType
x1
Term -> Put
forall t. Binary t => t -> Put
put Term
x2
Operator Term
x1 Int
x2 [Value] -> Maybe Value
x3 -> do () -> Put
forall (m :: * -> *) a. Monad m => a -> m a
return ()
CaseOp CaseInfo
x1 Term
x2 [(Term, Bool)]
x3 [Either Term (Term, Term)]
_ [([Name], Term, Term)]
_ CaseDefs
x4 -> do Word8 -> Put
putWord8 Word8
3
CaseInfo -> Put
forall t. Binary t => t -> Put
put CaseInfo
x1
Term -> Put
forall t. Binary t => t -> Put
put Term
x2
[(Term, Bool)] -> Put
forall t. Binary t => t -> Put
put [(Term, Bool)]
x3
CaseDefs -> Put
forall t. Binary t => t -> Put
put CaseDefs
x4
get :: Get Def
get
= do Word8
i <- Get Word8
getWord8
case Word8
i of
Word8
0 -> do Term
x1 <- Get Term
forall t. Binary t => Get t
get
Term
x2 <- Get Term
forall t. Binary t => Get t
get
Def -> Get Def
forall (m :: * -> *) a. Monad m => a -> m a
return (Term -> Term -> Def
Function Term
x1 Term
x2)
Word8
1 -> do NameType
x1 <- Get NameType
forall t. Binary t => Get t
get
Term
x2 <- Get Term
forall t. Binary t => Get t
get
Def -> Get Def
forall (m :: * -> *) a. Monad m => a -> m a
return (NameType -> Term -> Def
TyDecl NameType
x1 Term
x2)
Word8
3 -> do CaseInfo
x1 <- Get CaseInfo
forall t. Binary t => Get t
get
Term
x2 <- Get Term
forall t. Binary t => Get t
get
[(Term, Bool)]
x3 <- Get [(Term, Bool)]
forall t. Binary t => Get t
get
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)
Word8
_ -> String -> Get Def
forall a. HasCallStack => String -> a
error String
"Corrupted binary data for Def"
instance Binary Accessibility
instance Binary PReason
instance Binary Totality
instance Binary MetaInformation
instance Binary DataOpt
instance Binary FnOpt
instance Binary Fixity
instance Binary FixDecl
instance Binary ArgOpt
instance Binary Static
instance Binary Plicity where
put :: Plicity -> Put
put Plicity
x
= case Plicity
x of
Imp [ArgOpt]
x1 Static
x2 Bool
x3 Maybe ImplicitInfo
x4 Bool
_ RigCount
x5 ->
do Word8 -> Put
putWord8 Word8
0
[ArgOpt] -> Put
forall t. Binary t => t -> Put
put [ArgOpt]
x1
Static -> Put
forall t. Binary t => t -> Put
put Static
x2
Bool -> Put
forall t. Binary t => t -> Put
put Bool
x3
Maybe ImplicitInfo -> Put
forall t. Binary t => t -> Put
put Maybe ImplicitInfo
x4
RigCount -> Put
forall t. Binary t => t -> Put
put RigCount
x5
Exp [ArgOpt]
x1 Static
x2 Bool
x3 RigCount
x4 ->
do Word8 -> Put
putWord8 Word8
1
[ArgOpt] -> Put
forall t. Binary t => t -> Put
put [ArgOpt]
x1
Static -> Put
forall t. Binary t => t -> Put
put Static
x2
Bool -> Put
forall t. Binary t => t -> Put
put Bool
x3
RigCount -> Put
forall t. Binary t => t -> Put
put RigCount
x4
Constraint [ArgOpt]
x1 Static
x2 RigCount
x3 ->
do Word8 -> Put
putWord8 Word8
2
[ArgOpt] -> Put
forall t. Binary t => t -> Put
put [ArgOpt]
x1
Static -> Put
forall t. Binary t => t -> Put
put Static
x2
RigCount -> Put
forall t. Binary t => t -> Put
put RigCount
x3
TacImp [ArgOpt]
x1 Static
x2 PTerm
x3 RigCount
x4 ->
do Word8 -> Put
putWord8 Word8
3
[ArgOpt] -> Put
forall t. Binary t => t -> Put
put [ArgOpt]
x1
Static -> Put
forall t. Binary t => t -> Put
put Static
x2
PTerm -> Put
forall t. Binary t => t -> Put
put PTerm
x3
RigCount -> Put
forall t. Binary t => t -> Put
put RigCount
x4
get :: Get Plicity
get
= do Word8
i <- Get Word8
getWord8
case Word8
i of
Word8
0 -> do [ArgOpt]
x1 <- Get [ArgOpt]
forall t. Binary t => Get t
get
Static
x2 <- Get Static
forall t. Binary t => Get t
get
Bool
x3 <- Get Bool
forall t. Binary t => Get t
get
Maybe ImplicitInfo
x4 <- Get (Maybe ImplicitInfo)
forall t. Binary t => Get t
get
RigCount
x5 <- Get RigCount
forall t. Binary t => Get t
get
Plicity -> Get Plicity
forall (m :: * -> *) a. Monad m => a -> m a
return ([ArgOpt]
-> Static
-> Bool
-> Maybe ImplicitInfo
-> Bool
-> RigCount
-> Plicity
Imp [ArgOpt]
x1 Static
x2 Bool
x3 Maybe ImplicitInfo
x4 Bool
False RigCount
x5)
Word8
1 -> do [ArgOpt]
x1 <- Get [ArgOpt]
forall t. Binary t => Get t
get
Static
x2 <- Get Static
forall t. Binary t => Get t
get
Bool
x3 <- Get Bool
forall t. Binary t => Get t
get
RigCount
x4 <- Get RigCount
forall t. Binary t => Get t
get
Plicity -> Get Plicity
forall (m :: * -> *) a. Monad m => a -> m a
return ([ArgOpt] -> Static -> Bool -> RigCount -> Plicity
Exp [ArgOpt]
x1 Static
x2 Bool
x3 RigCount
x4)
Word8
2 -> do [ArgOpt]
x1 <- Get [ArgOpt]
forall t. Binary t => Get t
get
Static
x2 <- Get Static
forall t. Binary t => Get t
get
RigCount
x3 <- Get RigCount
forall t. Binary t => Get t
get
Plicity -> Get Plicity
forall (m :: * -> *) a. Monad m => a -> m a
return ([ArgOpt] -> Static -> RigCount -> Plicity
Constraint [ArgOpt]
x1 Static
x2 RigCount
x3)
Word8
3 -> do [ArgOpt]
x1 <- Get [ArgOpt]
forall t. Binary t => Get t
get
Static
x2 <- Get Static
forall t. Binary t => Get t
get
PTerm
x3 <- Get PTerm
forall t. Binary t => Get t
get
RigCount
x4 <- Get RigCount
forall t. Binary t => Get t
get
Plicity -> Get Plicity
forall (m :: * -> *) a. Monad m => a -> m a
return ([ArgOpt] -> Static -> PTerm -> RigCount -> Plicity
TacImp [ArgOpt]
x1 Static
x2 PTerm
x3 RigCount
x4)
Word8
_ -> String -> Get Plicity
forall a. HasCallStack => String -> a
error String
"Corrupted binary data for Plicity"
instance Binary DefaultTotality
instance Binary LanguageExt
instance Binary Directive
instance (Binary t) => Binary (PDecl' t)
instance Binary t => Binary (ProvideWhat' t)
instance Binary Using
instance Binary SyntaxInfo where
put :: SyntaxInfo -> Put
put (Syn [Using]
x1 [(Name, PTerm)]
x2 [String]
x3 [Name]
x4 [Name]
_ Name -> Name
_ Bool
x5 Bool
x6 Bool
x7 Maybe Int
_ Int
_ DSL
x8 Int
_ Bool
_ Bool
_)
= do [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 Int
0 DSL
x8 Int
0 Bool
True Bool
True)
instance (Binary t) => Binary (PClause' t)
instance (Binary t) => Binary (PData' t)
instance Binary PunInfo
instance Binary PTerm
instance Binary PAltType
instance (Binary t) => Binary (PTactic' t)
instance (Binary t) => Binary (PDo' t)
instance (Binary t) => Binary (PArg' t)
instance Binary InterfaceInfo where
put :: InterfaceInfo -> Put
put (CI Name
x1 [(Name, (Bool, [FnOpt], PTerm))]
x2 [(Name, (Name, PDecl))]
x3 [PDecl]
x4 [Name]
x5 [Name]
x6 [PTerm]
x7 [(Name, Bool)]
_ [Int]
x8)
= do Name -> Put
forall t. Binary t => t -> Put
put Name
x1
[(Name, (Bool, [FnOpt], PTerm))] -> Put
forall t. Binary t => t -> Put
put [(Name, (Bool, [FnOpt], PTerm))]
x2
[(Name, (Name, PDecl))] -> Put
forall t. Binary t => t -> Put
put [(Name, (Name, PDecl))]
x3
[PDecl] -> Put
forall t. Binary t => t -> Put
put [PDecl]
x4
[Name] -> Put
forall t. Binary t => t -> Put
put [Name]
x5
[Name] -> Put
forall t. Binary t => t -> Put
put [Name]
x6
[PTerm] -> Put
forall t. Binary t => t -> Put
put [PTerm]
x7
[Int] -> Put
forall t. Binary t => t -> Put
put [Int]
x8
get :: Get InterfaceInfo
get
= do Name
x1 <- Get Name
forall t. Binary t => Get t
get
[(Name, (Bool, [FnOpt], PTerm))]
x2 <- Get [(Name, (Bool, [FnOpt], PTerm))]
forall t. Binary t => Get t
get
[(Name, (Name, PDecl))]
x3 <- Get [(Name, (Name, PDecl))]
forall t. Binary t => Get t
get
[PDecl]
x4 <- Get [PDecl]
forall t. Binary t => Get t
get
[Name]
x5 <- Get [Name]
forall t. Binary t => Get t
get
[Name]
x6 <- Get [Name]
forall t. Binary t => Get t
get
[PTerm]
x7 <- Get [PTerm]
forall t. Binary t => Get t
get
[Int]
x8 <- Get [Int]
forall t. Binary t => Get t
get
InterfaceInfo -> Get InterfaceInfo
forall (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