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