{-# LANGUAGE TypeSynonymInstances #-}
{-# OPTIONS_GHC -fwarn-incomplete-patterns #-}

module Idris.IBC where

import Idris.Core.Evaluate
import Idris.Core.TT
import Idris.Core.Binary
import Idris.Core.CaseTree
import Idris.AbsSyntax
import Idris.Imports
import Idris.Error
import Idris.DeepSeq
import Idris.Delaborate
import qualified Idris.Docstrings as D
import Idris.Docstrings (Docstring)
import Idris.Output
import IRTS.System (getIdrisLibDir)
import Paths_idris

import qualified Cheapskate.Types as CT

import Data.Binary
import Data.Vector.Binary
import Data.List
import Data.ByteString.Lazy as B hiding (length, elem, map)
import qualified Data.Text as T
import qualified Data.Set as S

import Control.Monad
import Control.DeepSeq
import Control.Monad.State.Strict hiding (get, put)
import qualified Control.Monad.State.Strict as ST
import System.FilePath
import System.Directory
import Codec.Compression.Zlib (compress)
import Util.Zlib (decompressEither)

ibcVersion :: Word8
ibcVersion = 100

data IBCFile = IBCFile { ver :: Word8,
                         sourcefile :: FilePath,
                         symbols :: ![Name],
                         ibc_imports :: ![(Bool, FilePath)],
                         ibc_importdirs :: ![FilePath],
                         ibc_implicits :: ![(Name, [PArg])],
                         ibc_fixes :: ![FixDecl],
                         ibc_statics :: ![(Name, [Bool])],
                         ibc_classes :: ![(Name, ClassInfo)],
                         ibc_instances :: ![(Bool, Name, Name)],
                         ibc_dsls :: ![(Name, DSL)],
                         ibc_datatypes :: ![(Name, TypeInfo)],
                         ibc_optimise :: ![(Name, OptInfo)],
                         ibc_syntax :: ![Syntax],
                         ibc_keywords :: ![String],
                         ibc_objs :: ![(Codegen, FilePath)],
                         ibc_libs :: ![(Codegen, String)],
                         ibc_cgflags :: ![(Codegen, String)],
                         ibc_dynamic_libs :: ![String],
                         ibc_hdrs :: ![(Codegen, String)],
                         ibc_access :: ![(Name, Accessibility)],
                         ibc_total :: ![(Name, Totality)],
                         ibc_totcheckfail :: ![(FC, String)],
                         ibc_flags :: ![(Name, [FnOpt])],
                         ibc_fninfo :: ![(Name, FnInfo)],
                         ibc_cg :: ![(Name, CGInfo)],
                         ibc_defs :: ![(Name, Def)],
                         ibc_docstrings :: ![(Name, (Docstring D.DocTerm, [(Name, Docstring D.DocTerm)]))],
                         ibc_moduledocs :: ![(Name, Docstring D.DocTerm)],
                         ibc_transforms :: ![(Name, (Term, Term))],
                         ibc_errRev :: ![(Term, Term)],
                         ibc_coercions :: ![Name],
                         ibc_lineapps :: ![(FilePath, Int, PTerm)],
                         ibc_namehints :: ![(Name, Name)],
                         ibc_metainformation :: ![(Name, MetaInformation)],
                         ibc_errorhandlers :: ![Name],
                         ibc_function_errorhandlers :: ![(Name, Name, Name)], -- fn, arg, handler
                         ibc_metavars :: ![(Name, (Maybe Name, Int, Bool))],
                         ibc_patdefs :: ![(Name, ([([Name], Term, Term)], [PTerm]))],
                         ibc_postulates :: ![Name],
                         ibc_parsedSpan :: !(Maybe FC),
                         ibc_usage :: ![(Name, Int)],
                         ibc_exports :: ![Name]
                       }
   deriving Show
{-!
deriving instance Binary IBCFile
!-}

initIBC :: IBCFile
initIBC = IBCFile ibcVersion "" [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] Nothing [] []

loadIBC :: Bool -- ^ True = reexport, False = make everything private
        -> FilePath -> Idris ()
loadIBC reexport fp
           = do imps <- getImported
                let redo = case lookup fp imps of
                                Nothing -> True
                                Just p -> not p && reexport
                when redo $
                  do iLOG $ "Loading ibc " ++ fp ++ " " ++ show reexport
                     ibcf <- runIO $ (bdecode fp :: IO IBCFile)
                     process reexport ibcf fp
                     addImported reexport fp

-- | Load an entire package from its index file
loadPkgIndex :: String -> Idris ()
loadPkgIndex pkg = do ddir <- runIO $ getIdrisLibDir
                      addImportDir (ddir </> pkg)
                      fp <- findPkgIndex pkg
                      loadIBC True fp

bencode :: Binary a => FilePath -> a -> IO ()
bencode f d = B.writeFile f (compress (encode d))

bdecode :: Binary b => FilePath -> IO b
bdecode f = do d' <- B.readFile f
               either
                 (\(_, e) -> error $ "Invalid / corrupted zip format on " ++ show f ++ ": " ++ e)
                 (return . decode)
                 (decompressEither d')

writeIBC :: FilePath -> FilePath -> Idris ()
writeIBC src f
    = do iLOG $ "Writing ibc " ++ show f
         i <- getIState
--          case (Data.List.map fst (idris_metavars i)) \\ primDefs of
--                 (_:_) -> ifail "Can't write ibc when there are unsolved metavariables"
--                 [] -> return ()
         resetNameIdx
         ibcf <- mkIBC (ibc_write i) (initIBC { sourcefile = src })
         idrisCatch (do runIO $ createDirectoryIfMissing True (dropFileName f)
                        runIO $ bencode f ibcf
                        iLOG "Written")
            (\c -> do iLOG $ "Failed " ++ pshow i c)
         return ()

-- Write a package index containing all the imports in the current IState
-- Used for ':search' of an entire package, to ensure everything is loaded.
writePkgIndex :: FilePath -> Idris ()
writePkgIndex f
    = do i <- getIState
         let imps = map (\ (x, y) -> (True, x)) $ idris_imported i
         iLOG $ "Writing package index " ++ show f ++ " including\n" ++
                show (map snd imps)
         resetNameIdx
         let ibcf = initIBC { ibc_imports = imps }
         idrisCatch (do runIO $ createDirectoryIfMissing True (dropFileName f)
                        runIO $ bencode f ibcf
                        iLOG "Written")
            (\c -> do iLOG $ "Failed " ++ pshow i c)
         return ()

mkIBC :: [IBCWrite] -> IBCFile -> Idris IBCFile
mkIBC [] f = return f
mkIBC (i:is) f = do ist <- getIState
                    logLvl 5 $ show i ++ " " ++ show (Data.List.length is)
                    f' <- ibc ist i f
                    mkIBC is f'

ibc :: IState -> IBCWrite -> IBCFile -> Idris IBCFile
ibc i (IBCFix d) f = return f { ibc_fixes = d : ibc_fixes f }
ibc i (IBCImp n) f = case lookupCtxtExact n (idris_implicits i) of
                        Just v -> return f { ibc_implicits = (n,v): ibc_implicits f     }
                        _ -> ifail "IBC write failed"
ibc i (IBCStatic n) f
                   = case lookupCtxtExact n (idris_statics i) of
                        Just v -> return f { ibc_statics = (n,v): ibc_statics f     }
                        _ -> ifail "IBC write failed"
ibc i (IBCClass n) f
                   = case lookupCtxtExact n (idris_classes i) of
                        Just v -> return f { ibc_classes = (n,v): ibc_classes f     }
                        _ -> ifail "IBC write failed"
ibc i (IBCInstance int n ins) f
                   = return f { ibc_instances = (int,n,ins): ibc_instances f     }
ibc i (IBCDSL n) f
                   = case lookupCtxtExact n (idris_dsls i) of
                        Just v -> return f { ibc_dsls = (n,v): ibc_dsls f     }
                        _ -> ifail "IBC write failed"
ibc i (IBCData n) f
                   = case lookupCtxtExact n (idris_datatypes i) of
                        Just v -> return f { ibc_datatypes = (n,v): ibc_datatypes f     }
                        _ -> ifail "IBC write failed"
ibc i (IBCOpt n) f = case lookupCtxtExact n (idris_optimisation i) of
                        Just v -> return f { ibc_optimise = (n,v): ibc_optimise f     }
                        _ -> ifail "IBC write failed"
ibc i (IBCSyntax n) f = return f { ibc_syntax = n : ibc_syntax f }
ibc i (IBCKeyword n) f = return f { ibc_keywords = n : ibc_keywords f }
ibc i (IBCImport n) f = return f { ibc_imports = n : ibc_imports f }
ibc i (IBCImportDir n) f = return f { ibc_importdirs = n : ibc_importdirs f }
ibc i (IBCObj tgt n) f = return f { ibc_objs = (tgt, n) : ibc_objs f }
ibc i (IBCLib tgt n) f = return f { ibc_libs = (tgt, n) : ibc_libs f }
ibc i (IBCCGFlag tgt n) f = return f { ibc_cgflags = (tgt, n) : ibc_cgflags f }
ibc i (IBCDyLib n) f = return f {ibc_dynamic_libs = n : ibc_dynamic_libs f }
ibc i (IBCHeader tgt n) f = return f { ibc_hdrs = (tgt, n) : ibc_hdrs f }
ibc i (IBCDef n) f
   = do f' <- case lookupDefExact n (tt_ctxt i) of
                   Just v -> return f { ibc_defs = (n,v) : ibc_defs f }
                   _ -> ifail "IBC write failed"
        case lookupCtxtExact n (idris_patdefs i) of
                   Just v -> return f' { ibc_patdefs = (n,v) : ibc_patdefs f }
                   _ -> return f' -- Not a pattern definition

ibc i (IBCDoc n) f = case lookupCtxtExact n (idris_docstrings i) of
                        Just v -> return f { ibc_docstrings = (n,v) : ibc_docstrings f }
                        _ -> ifail "IBC write failed"
ibc i (IBCCG n) f = case lookupCtxtExact n (idris_callgraph i) of
                        Just v -> return f { ibc_cg = (n,v) : ibc_cg f     }
                        _ -> ifail "IBC write failed"
ibc i (IBCCoercion n) f = return f { ibc_coercions = n : ibc_coercions f }
ibc i (IBCAccess n a) f = return f { ibc_access = (n,a) : ibc_access f }
ibc i (IBCFlags n a) f = return f { ibc_flags = (n,a) : ibc_flags f }
ibc i (IBCFnInfo n a) f = return f { ibc_fninfo = (n,a) : ibc_fninfo f }
ibc i (IBCTotal n a) f = return f { ibc_total = (n,a) : ibc_total f }
ibc i (IBCTrans n t) f = return f { ibc_transforms = (n, t) : ibc_transforms f }
ibc i (IBCErrRev t) f = return f { ibc_errRev = t : ibc_errRev f }
ibc i (IBCLineApp fp l t) f
     = return f { ibc_lineapps = (fp,l,t) : ibc_lineapps f }
ibc i (IBCNameHint (n, ty)) f
     = return f { ibc_namehints = (n, ty) : ibc_namehints f }
ibc i (IBCMetaInformation n m) f = return f { ibc_metainformation = (n,m) : ibc_metainformation f }
ibc i (IBCErrorHandler n) f = return f { ibc_errorhandlers = n : ibc_errorhandlers f }
ibc i (IBCFunctionErrorHandler fn a n) f =
  return f { ibc_function_errorhandlers = (fn, a, n) : ibc_function_errorhandlers f }
ibc i (IBCMetavar n) f =
     case lookup n (idris_metavars i) of
          Nothing -> return f
          Just t -> return f { ibc_metavars = (n, t) : ibc_metavars f }
ibc i (IBCPostulate n) f = return f { ibc_postulates = n : ibc_postulates f }
ibc i (IBCTotCheckErr fc err) f = return f { ibc_totcheckfail = (fc, err) : ibc_totcheckfail f }
ibc i (IBCParsedRegion fc) f = return f { ibc_parsedSpan = Just fc }
ibc i (IBCModDocs n) f = case lookupCtxtExact n (idris_moduledocs i) of
                           Just v -> return f { ibc_moduledocs = (n,v) : ibc_moduledocs f }
                           _ -> ifail "IBC write failed"
ibc i (IBCUsage n) f = return f { ibc_usage = n : ibc_usage f }
ibc i (IBCExport n) f = return f { ibc_exports = n : ibc_exports f }

process :: Bool -- ^ Reexporting
           -> IBCFile -> FilePath -> Idris ()
process reexp i fn
   | ver i /= ibcVersion
       = do iLOG "ibc out of date"
            let e = if ver i < ibcVersion then " an earlier " else " a later "
            ifail $ "Incompatible ibc version.\nThis library was built with"
                    ++ e ++ "version of Idris.\n" ++
                    "Please clean and rebuild."

                              --- please rebuild"
   | otherwise =
            do srcok <- runIO $ doesFileExist (sourcefile i)
               when srcok $ timestampOlder (sourcefile i) fn
               v <- verbose
               quiet <- getQuiet
--                when (v && srcok && not quiet) $ iputStrLn $ "Skipping " ++ sourcefile i
               pImportDirs $ force (ibc_importdirs i)
               pImports $ force (ibc_imports i)
               pImps $ force (ibc_implicits i)
               pFixes $ force (ibc_fixes i)
               pStatics $ force (ibc_statics i)
               pClasses $ force (ibc_classes i)
               pInstances $ force (ibc_instances i)
               pDSLs $ force (ibc_dsls i)
               pDatatypes $ force (ibc_datatypes i)
               pOptimise $ force (ibc_optimise i)
               pSyntax $ force (ibc_syntax i)
               pKeywords $ force (ibc_keywords i)
               pObjs $ force (ibc_objs i)
               pLibs $ force (ibc_libs i)
               pCGFlags $ force (ibc_cgflags i)
               pDyLibs $ force (ibc_dynamic_libs i)
               pHdrs $ force (ibc_hdrs i)
               pDefs reexp (symbols i) $ force (ibc_defs i)
               pPatdefs $ force (ibc_patdefs i)
               pAccess reexp $ force (ibc_access i)
               pFlags $ force (ibc_flags i)
               pFnInfo $ force (ibc_fninfo i)
               pTotal $ force (ibc_total i)
               pTotCheckErr $ force (ibc_totcheckfail i)
               pCG $ force (ibc_cg i)
               pDocs $ force (ibc_docstrings i)
               pMDocs $ force (ibc_moduledocs i)
               pCoercions $ force (ibc_coercions i)
               pTrans $ force (ibc_transforms i)
               pErrRev $ force (ibc_errRev i)
               pLineApps $ force (ibc_lineapps i)
               pNameHints $ force (ibc_namehints i)
               pMetaInformation $ force (ibc_metainformation i)
               pErrorHandlers $ force (ibc_errorhandlers i)
               pFunctionErrorHandlers $ force (ibc_function_errorhandlers i)
               pMetavars $ force (ibc_metavars i)
               pPostulates $ force (ibc_postulates i)
               pParsedSpan $ force (ibc_parsedSpan i)
               pUsage $ force (ibc_usage i)
               pExports $ force (ibc_exports i)

timestampOlder :: FilePath -> FilePath -> Idris ()
timestampOlder src ibc = do srct <- runIO $ getModificationTime src
                            ibct <- runIO $ getModificationTime ibc
                            if (srct > ibct)
                               then ifail "Needs reloading"
                               else return ()

pPostulates :: [Name] -> Idris ()
pPostulates ns = do
    i <- getIState
    putIState i{ idris_postulates = idris_postulates i `S.union` S.fromList ns }

pParsedSpan :: Maybe FC -> Idris ()
pParsedSpan fc = do ist <- getIState
                    putIState ist { idris_parsedSpan = fc }

pUsage :: [(Name, Int)] -> Idris ()
pUsage ns = do ist <- getIState
               putIState ist { idris_erasureUsed = ns ++ idris_erasureUsed ist }

pExports :: [Name] -> Idris ()
pExports ns = do ist <- getIState
                 putIState ist { idris_exports = ns ++ idris_exports ist }

pImportDirs :: [FilePath] -> Idris ()
pImportDirs fs = mapM_ addImportDir fs

pImports :: [(Bool, FilePath)] -> Idris ()
pImports fs
  = do mapM_ (\(re, f) ->
                    do i <- getIState
                       ibcsd <- valIBCSubDir i
                       ids <- allImportDirs
                       fp <- findImport ids ibcsd f
--                        if (f `elem` imported i)
--                         then iLOG $ "Already read " ++ f
                       putIState (i { imported = f : imported i })
                       case fp of
                            LIDR fn -> do iLOG $ "Failed at " ++ fn
                                          ifail "Must be an ibc"
                            IDR fn -> do iLOG $ "Failed at " ++ fn
                                         ifail "Must be an ibc"
                            IBC fn src -> loadIBC re fn)
             fs

pImps :: [(Name, [PArg])] -> Idris ()
pImps imps = mapM_ (\ (n, imp) ->
                        do i <- getIState
                           case lookupDefAccExact n False (tt_ctxt i) of
                              Just (n, Hidden) -> return ()
                              _ -> putIState (i { idris_implicits
                                            = addDef n imp (idris_implicits i) }))
                   imps

pFixes :: [FixDecl] -> Idris ()
pFixes f = do i <- getIState
              putIState (i { idris_infixes = sort $ f ++ idris_infixes i })

pStatics :: [(Name, [Bool])] -> Idris ()
pStatics ss = mapM_ (\ (n, s) ->
                        do i <- getIState
                           putIState (i { idris_statics
                                           = addDef n s (idris_statics i) }))
                    ss

pClasses :: [(Name, ClassInfo)] -> Idris ()
pClasses cs = mapM_ (\ (n, c) ->
                        do i <- getIState
                           -- Don't lose instances from previous IBCs, which
                           -- could have loaded in any order
                           let is = case lookupCtxtExact n (idris_classes i) of
                                      Just (CI _ _ _ _ _ ins _) -> ins
                                      _ -> []
                           let c' = c { class_instances =
                                          class_instances c ++ is }
                           putIState (i { idris_classes
                                           = addDef n c' (idris_classes i) }))
                    cs

pInstances :: [(Bool, Name, Name)] -> Idris ()
pInstances cs = mapM_ (\ (i, n, ins) -> addInstance i n ins) cs

pDSLs :: [(Name, DSL)] -> Idris ()
pDSLs cs = mapM_ (\ (n, c) ->
                        do i <- getIState
                           putIState (i { idris_dsls
                                           = addDef n c (idris_dsls i) }))
                    cs

pDatatypes :: [(Name, TypeInfo)] -> Idris ()
pDatatypes cs = mapM_ (\ (n, c) ->
                        do i <- getIState
                           putIState (i { idris_datatypes
                                           = addDef n c (idris_datatypes i) }))
                    cs

pOptimise :: [(Name, OptInfo)] -> Idris ()
pOptimise cs = mapM_ (\ (n, c) ->
                        do i <- getIState
                           putIState (i { idris_optimisation
                                           = addDef n c (idris_optimisation i) }))
                    cs

pSyntax :: [Syntax] -> Idris ()
pSyntax s = do i <- getIState
               putIState (i { syntax_rules = updateSyntaxRules s (syntax_rules i) })

pKeywords :: [String] -> Idris ()
pKeywords k = do i <- getIState
                 putIState (i { syntax_keywords = k ++ syntax_keywords i })

pObjs :: [(Codegen, FilePath)] -> Idris ()
pObjs os = mapM_ (\ (cg, obj) -> do dirs <- allImportDirs
                                    o <- runIO $ findInPath dirs obj
                                    addObjectFile cg o) os

pLibs :: [(Codegen, String)] -> Idris ()
pLibs ls = mapM_ (uncurry addLib) ls

pCGFlags :: [(Codegen, String)] -> Idris ()
pCGFlags ls = mapM_ (uncurry addFlag) ls

pDyLibs :: [String] -> Idris ()
pDyLibs ls = do res <- mapM (addDyLib . return) ls
                mapM_ checkLoad res
                return ()
    where checkLoad (Left _) = return ()
          checkLoad (Right err) = ifail err

pHdrs :: [(Codegen, String)] -> Idris ()
pHdrs hs = mapM_ (uncurry addHdr) hs

pPatdefs :: [(Name, ([([Name], Term, Term)], [PTerm]))] -> Idris ()
pPatdefs ds
   = mapM_ (\ (n, d) ->
                do i <- getIState
                   putIState (i { idris_patdefs = addDef n (force d) (idris_patdefs i) }))
           ds

pDefs :: Bool -> [Name] -> [(Name, Def)] -> Idris ()
pDefs reexp syms ds
   = mapM_ (\ (n, d) ->
               do d' <- updateDef d
                  case d' of
                       TyDecl _ _ -> return ()
                       _ -> do iLOG $ "SOLVING " ++ show n
                               solveDeferred n
                  i <- getIState
--                   logLvl 1 $ "Added " ++ show (n, d')
                  putIState (i { tt_ctxt = addCtxtDef n d' (tt_ctxt i) })
                  if (not reexp) then do iLOG $ "Not exporting " ++ show n
                                         setAccessibility n Hidden
                                 else iLOG $ "Exporting " ++ show n) ds
  where
    updateDef (CaseOp c t args o s cd)
      = do o' <- mapM updateOrig o
           cd' <- updateCD cd
           return $ CaseOp c t args o' s cd'
    updateDef t = return t

    updateOrig (Left t) = liftM Left (update t)
    updateOrig (Right (l, r)) = do l' <- update l
                                   r' <- update r
                                   return $ Right (l', r')

    updateCD (CaseDefs (ts, t) (cs, c) (is, i) (rs, r))
        = do t' <- updateSC t
             c' <- updateSC c
             i' <- updateSC i
             r' <- updateSC r
             return $ CaseDefs (ts, t') (cs, c') (is, i') (rs, r')

    updateSC (Case t n alts) = do alts' <- mapM updateAlt alts
                                  return (Case t n alts')
    updateSC (ProjCase t alts) = do alts' <- mapM updateAlt alts
                                    return (ProjCase t alts')
    updateSC (STerm t) = do t' <- update t
                            return (STerm t')
    updateSC c = return c

    updateAlt (ConCase n i ns t) = do t' <- updateSC t
                                      return (ConCase n i ns t')
    updateAlt (FnCase n ns t) = do t' <- updateSC t
                                   return (FnCase n ns t')
    updateAlt (ConstCase c t) = do t' <- updateSC t
                                   return (ConstCase c t')
    updateAlt (SucCase n t) = do t' <- updateSC t
                                 return (SucCase n t')
    updateAlt (DefaultCase t) = do t' <- updateSC t
                                   return (DefaultCase t')

    update (P t n ty) = do n' <- getSymbol n
                           return $ P t n' ty
    update (App f a) = liftM2 App (update f) (update a)
    update (Bind n b sc) = do b' <- updateB b
                              sc' <- update sc
                              return $ Bind n b' sc'
      where
        updateB (Let t v) = liftM2 Let (update t) (update v)
        updateB b = do ty' <- update (binderTy b)
                       return (b { binderTy = ty' })
    update (Proj t i) = do t' <- update t
                           return $ Proj t' i
    update t = return t

pDocs :: [(Name, (Docstring D.DocTerm, [(Name, Docstring D.DocTerm)]))] -> Idris ()
pDocs ds = mapM_ (\(n, a) -> addDocStr n (fst a) (snd a)) ds

pMDocs :: [(Name, Docstring D.DocTerm)] -> Idris ()
pMDocs ds = mapM_ addMDocStr ds
  where addMDocStr (n, d) = do ist <- getIState
                               putIState ist { idris_moduledocs = addDef n d (idris_moduledocs ist) }

pAccess :: Bool -- ^ Reexporting?
           -> [(Name, Accessibility)] -> Idris ()
pAccess reexp ds
        = mapM_ (\ (n, a_in) ->
                      do let a = if reexp then a_in else Hidden
                         logLvl 3 $ "Setting " ++ show (a, n) ++ " to " ++ show a
                         i <- getIState
                         putIState (i { tt_ctxt = setAccess n a (tt_ctxt i) }))
                   ds

pFlags :: [(Name, [FnOpt])] -> Idris ()
pFlags ds = mapM_ (\ (n, a) -> setFlags n a) ds

pFnInfo :: [(Name, FnInfo)] -> Idris ()
pFnInfo ds = mapM_ (\ (n, a) -> setFnInfo n a) ds

pTotal :: [(Name, Totality)] -> Idris ()
pTotal ds = mapM_ (\ (n, a) ->
                      do i <- getIState
                         putIState (i { tt_ctxt = setTotal n a (tt_ctxt i) }))
                   ds

pTotCheckErr :: [(FC, String)] -> Idris ()
pTotCheckErr es = do ist <- getIState
                     putIState ist { idris_totcheckfail = idris_totcheckfail ist ++ es }

pCG :: [(Name, CGInfo)] -> Idris ()
pCG ds = mapM_ (\ (n, a) -> addToCG n a) ds

pCoercions :: [Name] -> Idris ()
pCoercions ns = mapM_ (\ n -> addCoercion n) ns

pTrans :: [(Name, (Term, Term))] -> Idris ()
pTrans ts = mapM_ (\ (n, t) -> addTrans n t) ts

pErrRev :: [(Term, Term)] -> Idris ()
pErrRev ts = mapM_ addErrRev ts

pLineApps :: [(FilePath, Int, PTerm)] -> Idris ()
pLineApps ls = mapM_ (\ (f, i, t) -> addInternalApp f i t) ls

pNameHints :: [(Name, Name)] -> Idris ()
pNameHints ns = mapM_ (\ (n, ty) -> addNameHint n ty) ns

pMetaInformation :: [(Name, MetaInformation)] -> Idris ()
pMetaInformation ds = mapM_ (\ (n, m) ->
                            do i <- getIState
                               putIState (i { tt_ctxt = setMetaInformation n m (tt_ctxt i) }))
                         ds

pErrorHandlers :: [Name] -> Idris ()
pErrorHandlers ns = do i <- getIState
                       putIState $ i { idris_errorhandlers = idris_errorhandlers i ++ ns }

pFunctionErrorHandlers :: [(Name, Name, Name)] -> Idris ()
pFunctionErrorHandlers [] = return ()
pFunctionErrorHandlers ((fn, arg, handler):ns) = do addFunctionErrorHandlers fn arg [handler]
                                                    pFunctionErrorHandlers ns

pMetavars :: [(Name, (Maybe Name, Int, Bool))] -> Idris ()
pMetavars ns = do i <- getIState
                  putIState $ i { idris_metavars = Data.List.reverse ns
                                                     ++ idris_metavars i }

----- For Cheapskate and docstrings

instance Binary a => Binary (D.Docstring a) where
  put (D.DocString opts lines) = do put opts ; put lines
  get = do opts <- get
           lines <- get
           return (D.DocString opts lines)

instance Binary CT.Options where
  put (CT.Options x1 x2 x3 x4) = do put x1 ; put x2 ; put x3 ; put x4
  get = do x1 <- get
           x2 <- get
           x3 <- get
           x4 <- get
           return (CT.Options x1 x2 x3 x4)

instance Binary D.DocTerm where
  put D.Unchecked = putWord8 0
  put (D.Checked t) = putWord8 1 >> put t
  put (D.Example t) = putWord8 2 >> put t
  put (D.Failing e) = putWord8 3 >> put e

  get = do i <- getWord8
           case i of
             0 -> return D.Unchecked
             1 -> fmap D.Checked get
             2 -> fmap D.Example get
             3 -> fmap D.Failing get
             _ -> error "Corrupted binary data for DocTerm"

instance Binary a => Binary (D.Block a) where
  put (D.Para lines) = do putWord8 0 ; put lines
  put (D.Header i lines) = do putWord8 1 ; put i ; put lines
  put (D.Blockquote bs) = do putWord8 2 ; put bs
  put (D.List b t xs) = do putWord8 3 ; put b ; put t ; put xs
  put (D.CodeBlock attr txt src) = do putWord8 4 ; put attr ; put txt ; put src
  put (D.HtmlBlock txt) = do putWord8 5 ; put txt
  put D.HRule = putWord8 6
  get = do i <- getWord8
           case i of
             0 -> fmap D.Para get
             1 -> liftM2 D.Header get get
             2 -> fmap D.Blockquote get
             3 -> liftM3 D.List get get get
             4 -> liftM3 D.CodeBlock get get get
             5 -> liftM D.HtmlBlock get
             6 -> return D.HRule
             _ -> error "Corrupted binary data for Block"

instance Binary a => Binary (D.Inline a) where
  put (D.Str txt) = do putWord8 0 ; put txt
  put D.Space = putWord8 1
  put D.SoftBreak = putWord8 2
  put D.LineBreak = putWord8 3
  put (D.Emph xs) = putWord8 4 >> put xs
  put (D.Strong xs) = putWord8 5 >> put xs
  put (D.Code xs tm) = putWord8 6 >> put xs >> put tm
  put (D.Link a b c) = putWord8 7 >> put a >> put b >> put c
  put (D.Image a b c) = putWord8 8 >> put a >> put b >> put c
  put (D.Entity a) = putWord8 9 >> put a
  put (D.RawHtml x) = putWord8 10 >> put x
  get = do i <- getWord8
           case i of
             0 -> liftM D.Str get
             1 -> return D.Space
             2 -> return D.SoftBreak
             3 -> return D.LineBreak
             4 -> liftM D.Emph get
             5 -> liftM D.Strong get
             6 -> liftM2 D.Code get get
             7 -> liftM3 D.Link get get get
             8 -> liftM3 D.Image get get get
             9 -> liftM D.Entity get
             10 -> liftM D.RawHtml get
             _ -> error "Corrupted binary data for Inline"

instance Binary CT.ListType where
  put (CT.Bullet c) = putWord8 0 >> put c
  put (CT.Numbered nw i) = putWord8 1 >> put nw >> put i
  get = do i <- getWord8
           case i of
             0 -> liftM CT.Bullet get
             1 -> liftM2 CT.Numbered get get
             _ -> error "Corrupted binary data for ListType"

instance Binary CT.CodeAttr where
  put (CT.CodeAttr a b) = put a >> put b
  get = liftM2 CT.CodeAttr get get

instance Binary CT.NumWrapper where
  put (CT.PeriodFollowing) = putWord8 0
  put (CT.ParenFollowing) = putWord8 1
  get = do i <- getWord8
           case i of
             0 -> return CT.PeriodFollowing
             1 -> return CT.ParenFollowing
             _ -> error "Corrupted binary data for NumWrapper"

----- Generated by 'derive'

instance Binary SizeChange where
        put x
          = case x of
                Smaller -> putWord8 0
                Same -> putWord8 1
                Bigger -> putWord8 2
                Unknown -> putWord8 3
        get
          = do i <- getWord8
               case i of
                   0 -> return Smaller
                   1 -> return Same
                   2 -> return Bigger
                   3 -> return Unknown
                   _ -> error "Corrupted binary data for SizeChange"

instance Binary CGInfo where
        put (CGInfo x1 x2 x3 x4 x5)
          = do put x1
               put x2
--                put x3 -- Already used SCG info for totality check
               put x4
               put x5
        get
          = do x1 <- get
               x2 <- get
               x4 <- get
               x5 <- get
               return (CGInfo x1 x2 [] x4 x5)

instance Binary CaseType where
        put x = case x of
                     Updatable -> putWord8 0
                     Shared -> putWord8 1
        get = do i <- getWord8
                 case i of
                     0 -> return Updatable
                     1 -> return Shared
                     _ -> error "Corrupted binary data for CaseType"

instance Binary SC where
        put x
          = case x of
                Case x1 x2 x3 -> do putWord8 0
                                    put x1
                                    put x2
                                    put x3
                ProjCase x1 x2 -> do putWord8 1
                                     put x1
                                     put x2
                STerm x1 -> do putWord8 2
                               put x1
                UnmatchedCase x1 -> do putWord8 3
                                       put x1
                ImpossibleCase -> do putWord8 4
        get
          = do i <- getWord8
               case i of
                   0 -> do x1 <- get
                           x2 <- get
                           x3 <- get
                           return (Case x1 x2 x3)
                   1 -> do x1 <- get
                           x2 <- get
                           return (ProjCase x1 x2)
                   2 -> do x1 <- get
                           return (STerm x1)
                   3 -> do x1 <- get
                           return (UnmatchedCase x1)
                   4 -> return ImpossibleCase
                   _ -> error "Corrupted binary data for SC"


instance Binary CaseAlt where
        put x
          = {-# SCC "putCaseAlt" #-}
            case x of
                ConCase x1 x2 x3 x4 -> do putWord8 0
                                          put x1
                                          put x2
                                          put x3
                                          put x4
                ConstCase x1 x2 -> do putWord8 1
                                      put x1
                                      put x2
                DefaultCase x1 -> do putWord8 2
                                     put x1
                FnCase x1 x2 x3 -> do putWord8 3
                                      put x1
                                      put x2
                                      put x3
                SucCase x1 x2 -> do putWord8 4
                                    put x1
                                    put x2
        get
          = do i <- getWord8
               case i of
                   0 -> do x1 <- get
                           x2 <- get
                           x3 <- get
                           x4 <- get
                           return (ConCase x1 x2 x3 x4)
                   1 -> do x1 <- get
                           x2 <- get
                           return (ConstCase x1 x2)
                   2 -> do x1 <- get
                           return (DefaultCase x1)
                   3 -> do x1 <- get
                           x2 <- get
                           x3 <- get
                           return (FnCase x1 x2 x3)
                   4 -> do x1 <- get
                           x2 <- get
                           return (SucCase x1 x2)
                   _ -> error "Corrupted binary data for CaseAlt"

instance Binary CaseDefs where
        put (CaseDefs x1 x2 x3 x4)
          = do -- don't need totality checked or inlined versions
               put x2
               put x4
        get
          = do x2 <- get
               x4 <- get
               return (CaseDefs x2 x2 x2 x4)

instance Binary CaseInfo where
        put x@(CaseInfo x1 x2 x3) = do put x1
                                       put x2
                                       put x3
        get = do x1 <- get
                 x2 <- get
                 x3 <- get
                 return (CaseInfo x1 x2 x3)

instance Binary Def where
        put x
          = {-# SCC "putDef" #-}
            case x of
                Function x1 x2 -> do putWord8 0
                                     put x1
                                     put x2
                TyDecl x1 x2 -> do putWord8 1
                                   put x1
                                   put x2
                -- all primitives just get added at the start, don't write
                Operator x1 x2 x3 -> do return ()
                CaseOp x1 x2 x2a x3 x3a x4 -> do putWord8 3
                                                 put x1
                                                 put x2
                                                 put x2a
                                                 put x3
                                                 -- no x3a
                                                 put x4
        get
          = do i <- getWord8
               case i of
                   0 -> do x1 <- get
                           x2 <- get
                           return (Function x1 x2)
                   1 -> do x1 <- get
                           x2 <- get
                           return (TyDecl x1 x2)
                   -- Operator isn't written, don't read
                   3 -> do x1 <- get
                           x2 <- get
                           x3 <- get
                           x4 <- get
                           -- x3 <- get always []
                           x5 <- get
                           return (CaseOp x1 x2 x3 x4 [] x5)
                   _ -> error "Corrupted binary data for Def"

instance Binary Accessibility where
        put x
          = case x of
                Public -> putWord8 0
                Frozen -> putWord8 1
                Hidden -> putWord8 2
        get
          = do i <- getWord8
               case i of
                   0 -> return Public
                   1 -> return Frozen
                   2 -> return Hidden
                   _ -> error "Corrupted binary data for Accessibility"

safeToEnum :: (Enum a, Bounded a, Integral int) => String -> int -> a
safeToEnum label x' = result
  where
    x = fromIntegral x'
    result
        |  x < fromEnum (minBound `asTypeOf` result)
        || x > fromEnum (maxBound `asTypeOf` result)
            = error $ label ++ ": corrupted binary representation in IBC"
        | otherwise = toEnum x

instance Binary PReason where
        put x
          = case x of
                Other x1 -> do putWord8 0
                               put x1
                Itself -> putWord8 1
                NotCovering -> putWord8 2
                NotPositive -> putWord8 3
                Mutual x1 -> do putWord8 4
                                put x1
                NotProductive -> putWord8 5
                BelieveMe -> putWord8 6
                UseUndef x1 -> do putWord8 7
                                  put x1
                ExternalIO -> putWord8 8
        get
          = do i <- getWord8
               case i of
                   0 -> do x1 <- get
                           return (Other x1)
                   1 -> return Itself
                   2 -> return NotCovering
                   3 -> return NotPositive
                   4 -> do x1 <- get
                           return (Mutual x1)
                   5 -> return NotProductive
                   6 -> return BelieveMe
                   7 -> do x1 <- get
                           return (UseUndef x1)
                   8 -> return ExternalIO
                   _ -> error "Corrupted binary data for PReason"

instance Binary Totality where
        put x
          = case x of
                Total x1 -> do putWord8 0
                               put x1
                Partial x1 -> do putWord8 1
                                 put x1
                Unchecked -> do putWord8 2
                Productive -> do putWord8 3
        get
          = do i <- getWord8
               case i of
                   0 -> do x1 <- get
                           return (Total x1)
                   1 -> do x1 <- get
                           return (Partial x1)
                   2 -> return Unchecked
                   3 -> return Productive
                   _ -> error "Corrupted binary data for Totality"

instance Binary MetaInformation where
  put x
    = case x of
      EmptyMI   -> do putWord8 0
      DataMI x1 -> do putWord8 1
                      put x1
  get = do i <- getWord8
           case i of
             0 -> return EmptyMI
             1 -> do x1 <- get
                     return (DataMI x1)
             _ -> error "Corrupted binary data for MetaInformation"

instance Binary IBCFile where
        put x@(IBCFile x1 x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 x15 x16 x17 x18 x19 x20 x21 x22 x23 x24 x25 x26 x27 x28 x29 x30 x31 x32 x33 x34 x35 x36 x37 x38 x39 x40 x41 x42 x43)
         = {-# SCC "putIBCFile" #-}
            do put x1
               put x2
               put x3
               put x4
               put x5
               put x6
               put x7
               put x8
               put x9
               put x10
               put x11
               put x12
               put x13
               put x14
               put x15
               put x16
               put x17
               put x18
               put x19
               put x20
               put x21
               put x22
               put x23
               put x24
               put x25
               put x26
               put x27
               put x28
               put x29
               put x30
               put x31
               put x32
               put x33
               put x34
               put x35
               put x36
               put x37
               put x38
               put x39
               put x40
               put x41
               put x42
               put x43

        get
          = do x1 <- get
               if x1 == ibcVersion then
                 do x2 <- get
                    x3 <- get
                    x4 <- get
                    x5 <- get
                    x6 <- get
                    x7 <- get
                    x8 <- get
                    x9 <- get
                    x10 <- get
                    x11 <- get
                    x12 <- get
                    x13 <- get
                    x14 <- get
                    x15 <- get
                    x16 <- get
                    x17 <- get
                    x18 <- get
                    x19 <- get
                    x20 <- get
                    x21 <- get
                    x22 <- get
                    x23 <- get
                    x24 <- get
                    x25 <- get
                    x26 <- get
                    x27 <- get
                    x28 <- get
                    x29 <- get
                    x30 <- get
                    x31 <- get
                    x32 <- get
                    x33 <- get
                    x34 <- get
                    x35 <- get
                    x36 <- get
                    x37 <- get
                    x38 <- get
                    x39 <- get
                    x40 <- get
                    x41 <- get
                    x42 <- get
                    x43 <- get
                    return (IBCFile x1 x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 x15 x16 x17 x18 x19 x20 x21 x22 x23 x24 x25 x26 x27 x28 x29 x30 x31 x32 x33 x34 x35 x36 x37 x38 x39 x40 x41 x42 x43)
                  else return (initIBC { ver = x1 })

instance Binary DataOpt where
  put x = case x of
    Codata -> putWord8 0
    DefaultEliminator -> putWord8 1
    DataErrRev -> putWord8 2
    DefaultCaseFun -> putWord8 3
  get = do i <- getWord8
           case i of
            0 -> return Codata
            1 -> return DefaultEliminator
            2 -> return DataErrRev
            3 -> return DefaultCaseFun
            _ -> error "Corrupted binary data for DataOpt"

instance Binary FnOpt where
        put x
          = case x of
                Inlinable -> putWord8 0
                TotalFn -> putWord8 1
                Dictionary -> putWord8 2
                AssertTotal -> putWord8 3
                Specialise x -> do putWord8 4
                                   put x
                Coinductive -> putWord8 5
                PartialFn -> putWord8 6
                Implicit -> putWord8 7
                Reflection -> putWord8 8
                ErrorHandler -> putWord8 9
                ErrorReverse -> putWord8 10
                CoveringFn -> putWord8 11
                NoImplicit -> putWord8 12
                Constructor -> putWord8 13
                CExport x1 -> do putWord8 14
                                 put x1
        get
          = do i <- getWord8
               case i of
                   0 -> return Inlinable
                   1 -> return TotalFn
                   2 -> return Dictionary
                   3 -> return AssertTotal
                   4 -> do x <- get
                           return (Specialise x)
                   5 -> return Coinductive
                   6 -> return PartialFn
                   7 -> return Implicit
                   8 -> return Reflection
                   9 -> return ErrorHandler
                   10 -> return ErrorReverse
                   11 -> return CoveringFn
                   12 -> return NoImplicit
                   13 -> return Constructor
                   14 -> do x1 <- get
                            return $ CExport x1
                   _ -> error "Corrupted binary data for FnOpt"

instance Binary Fixity where
        put x
          = case x of
                Infixl x1 -> do putWord8 0
                                put x1
                Infixr x1 -> do putWord8 1
                                put x1
                InfixN x1 -> do putWord8 2
                                put x1
                PrefixN x1 -> do putWord8 3
                                 put x1
        get
          = do i <- getWord8
               case i of
                   0 -> do x1 <- get
                           return (Infixl x1)
                   1 -> do x1 <- get
                           return (Infixr x1)
                   2 -> do x1 <- get
                           return (InfixN x1)
                   3 -> do x1 <- get
                           return (PrefixN x1)
                   _ -> error "Corrupted binary data for Fixity"


instance Binary FixDecl where
        put (Fix x1 x2)
          = do put x1
               put x2
        get
          = do x1 <- get
               x2 <- get
               return (Fix x1 x2)


instance Binary ArgOpt where
        put x
          = case x of
                HideDisplay -> putWord8 0
                InaccessibleArg -> putWord8 1
                AlwaysShow -> putWord8 2
        get
          = do i <- getWord8
               case i of
                   0 -> return HideDisplay
                   1 -> return InaccessibleArg
                   2 -> return AlwaysShow
                   _ -> error "Corrupted binary data for Static"

instance Binary Static where
        put x
          = case x of
                Static -> putWord8 0
                Dynamic -> putWord8 1
        get
          = do i <- getWord8
               case i of
                   0 -> return Static
                   1 -> return Dynamic
                   _ -> error "Corrupted binary data for Static"


instance Binary Plicity where
        put x
          = case x of
                Imp x1 x2 x3 x4 ->
                             do putWord8 0
                                put x1
                                put x2
                                put x3
                                put x4
                Exp x1 x2 x3 ->
                             do putWord8 1
                                put x1
                                put x2
                                put x3
                Constraint x1 x2 ->
                                    do putWord8 2
                                       put x1
                                       put x2
                TacImp x1 x2 x3 ->
                                   do putWord8 3
                                      put x1
                                      put x2
                                      put x3
        get
          = do i <- getWord8
               case i of
                   0 -> do x1 <- get
                           x2 <- get
                           x3 <- get
                           x4 <- get
                           return (Imp x1 x2 x3 x4)
                   1 -> do x1 <- get
                           x2 <- get
                           x3 <- get
                           return (Exp x1 x2 x3)
                   2 -> do x1 <- get
                           x2 <- get
                           return (Constraint x1 x2)
                   3 -> do x1 <- get
                           x2 <- get
                           x3 <- get
                           return (TacImp x1 x2 x3)
                   _ -> error "Corrupted binary data for Plicity"


instance (Binary t) => Binary (PDecl' t) where
        put x
          = case x of
                PFix x1 x2 x3 -> do putWord8 0
                                    put x1
                                    put x2
                                    put x3
                PTy x1 x2 x3 x4 x5 x6 x7
                                   -> do putWord8 1
                                         put x1
                                         put x2
                                         put x3
                                         put x4
                                         put x5
                                         put x6
                                         put x7
                PClauses x1 x2 x3 x4 -> do putWord8 2
                                           put x1
                                           put x2
                                           put x3
                                           put x4
                PData x1 x2 x3 x4 x5 x6 ->
                                     do putWord8 3
                                        put x1
                                        put x2
                                        put x3
                                        put x4
                                        put x5
                                        put x6
                PParams x1 x2 x3 -> do putWord8 4
                                       put x1
                                       put x2
                                       put x3
                PNamespace x1 x2 -> do putWord8 5
                                       put x1
                                       put x2
                PRecord x1 x2 x3 x4 x5 x6 x7 x8 x9 ->
                                             do putWord8 6
                                                put x1
                                                put x2
                                                put x3
                                                put x4
                                                put x5
                                                put x6
                                                put x7
                                                put x8
                                                put x9
                PClass x1 x2 x3 x4 x5 x6 x7 x8 x9
                                         -> do putWord8 7
                                               put x1
                                               put x2
                                               put x3
                                               put x4
                                               put x5
                                               put x6
                                               put x7
                                               put x8
                                               put x9
                PInstance x1 x2 x3 x4 x5 x6 x7 x8 x9 x10 ->
                  do putWord8 8
                     put x1
                     put x2
                     put x3
                     put x4
                     put x5
                     put x6
                     put x7
                     put x8
                     put x9
                     put x10
                PDSL x1 x2 -> do putWord8 9
                                 put x1
                                 put x2
                PCAF x1 x2 x3 -> do putWord8 10
                                    put x1
                                    put x2
                                    put x3
                PMutual x1 x2  -> do putWord8 11
                                     put x1
                                     put x2
                PPostulate x1 x2 x3 x4 x5 x6
                                   -> do putWord8 12
                                         put x1
                                         put x2
                                         put x3
                                         put x4
                                         put x5
                                         put x6
                PSyntax x1 x2 -> do putWord8 13
                                    put x1
                                    put x2
                PDirective x1 -> error "Cannot serialize PDirective"
                PProvider x1 x2 x3 x4 x5 ->
                  do putWord8 15
                     put x1
                     put x2
                     put x3
                     put x4
                     put x5
                PTransform x1 x2 x3 x4 -> do putWord8 16
                                             put x1
                                             put x2
                                             put x3
                                             put x4
        get
          = do i <- getWord8
               case i of
                   0 -> do x1 <- get
                           x2 <- get
                           x3 <- get
                           return (PFix x1 x2 x3)
                   1 -> do x1 <- get
                           x2 <- get
                           x3 <- get
                           x4 <- get
                           x5 <- get
                           x6 <- get
                           x7 <- get
                           return (PTy x1 x2 x3 x4 x5 x6 x7)
                   2 -> do x1 <- get
                           x2 <- get
                           x3 <- get
                           x4 <- get
                           return (PClauses x1 x2 x3 x4)
                   3 -> do x1 <- get
                           x2 <- get
                           x3 <- get
                           x4 <- get
                           x5 <- get
                           x6 <- get
                           return (PData x1 x2 x3 x4 x5 x6)
                   4 -> do x1 <- get
                           x2 <- get
                           x3 <- get
                           return (PParams x1 x2 x3)
                   5 -> do x1 <- get
                           x2 <- get
                           return (PNamespace x1 x2)
                   6 -> do x1 <- get
                           x2 <- get
                           x3 <- get
                           x4 <- get
                           x5 <- get
                           x6 <- get
                           x7 <- get
                           x8 <- get
                           x9 <- get
                           return (PRecord x1 x2 x3 x4 x5 x6 x7 x8 x9)
                   7 -> do x1 <- get
                           x2 <- get
                           x3 <- get
                           x4 <- get
                           x5 <- get
                           x6 <- get
                           x7 <- get
                           x8 <- get
                           x9 <- get
                           return (PClass x1 x2 x3 x4 x5 x6 x7 x8 x9)
                   8 -> do x1 <- get
                           x2 <- get
                           x3 <- get
                           x4 <- get
                           x5 <- get
                           x6 <- get
                           x7 <- get
                           x8 <- get
                           x9 <- get
                           x10 <- get
                           return (PInstance x1 x2 x3 x4 x5 x6 x7 x8 x9 x10)
                   9 -> do x1 <- get
                           x2 <- get
                           return (PDSL x1 x2)
                   10 -> do x1 <- get
                            x2 <- get
                            x3 <- get
                            return (PCAF x1 x2 x3)
                   11 -> do x1 <- get
                            x2 <- get
                            return (PMutual x1 x2)
                   12 -> do x1 <- get
                            x2 <- get
                            x3 <- get
                            x4 <- get
                            x5 <- get
                            x6 <- get
                            return (PPostulate x1 x2 x3 x4 x5 x6)
                   13 -> do x1 <- get
                            x2 <- get
                            return (PSyntax x1 x2)
                   14 -> do error "Cannot deserialize PDirective"
                   15 -> do x1 <- get
                            x2 <- get
                            x3 <- get
                            x4 <- get
                            x5 <- get
                            return (PProvider x1 x2 x3 x4 x5)
                   16 -> do x1 <- get
                            x2 <- get
                            x3 <- get
                            x4 <- get
                            return (PTransform x1 x2 x3 x4)
                   _ -> error "Corrupted binary data for PDecl'"

instance Binary t => Binary (ProvideWhat' t) where
  put (ProvTerm x1 x2) = do putWord8 0
                            put x1
                            put x2
  put (ProvPostulate x1) = do putWord8 1
                              put x1
  get = do y <- getWord8
           case y of
             0 -> do x1 <- get
                     x2 <- get
                     return (ProvTerm x1 x2)
             1 -> do x1 <- get
                     return (ProvPostulate x1)
             _ -> error "Corrupted binary data for ProvideWhat"

instance Binary Using where
        put (UImplicit x1 x2) = do putWord8 0; put x1; put x2
        put (UConstraint x1 x2) = do putWord8 1; put x1; put x2

        get = do i <- getWord8
                 case i of
                    0 -> do x1 <- get; x2 <- get; return (UImplicit x1 x2)
                    1 -> do x1 <- get; x2 <- get; return (UConstraint x1 x2)
                    _ -> error "Corrupted binary data for Using"

instance Binary SyntaxInfo where
        put (Syn x1 x2 x3 x4 _ _ x5 x6 _ _ x7 _)
          = do put x1
               put x2
               put x3
               put x4
               put x5
               put x6
               put x7
        get
          = do x1 <- get
               x2 <- get
               x3 <- get
               x4 <- get
               x5 <- get
               x6 <- get
               x7 <- get
               return (Syn x1 x2 x3 x4 [] id x5 x6 Nothing 0 x7 0)

instance (Binary t) => Binary (PClause' t) where
        put x
          = case x of
                PClause x1 x2 x3 x4 x5 x6 -> do putWord8 0
                                                put x1
                                                put x2
                                                put x3
                                                put x4
                                                put x5
                                                put x6
                PWith x1 x2 x3 x4 x5 x6 x7 -> do putWord8 1
                                                 put x1
                                                 put x2
                                                 put x3
                                                 put x4
                                                 put x5
                                                 put x6
                                                 put x7
                PClauseR x1 x2 x3 x4 -> do putWord8 2
                                           put x1
                                           put x2
                                           put x3
                                           put x4
                PWithR x1 x2 x3 x4 x5 -> do putWord8 3
                                            put x1
                                            put x2
                                            put x3
                                            put x4
                                            put x5
        get
          = do i <- getWord8
               case i of
                   0 -> do x1 <- get
                           x2 <- get
                           x3 <- get
                           x4 <- get
                           x5 <- get
                           x6 <- get
                           return (PClause x1 x2 x3 x4 x5 x6)
                   1 -> do x1 <- get
                           x2 <- get
                           x3 <- get
                           x4 <- get
                           x5 <- get
                           x6 <- get
                           x7 <- get
                           return (PWith x1 x2 x3 x4 x5 x6 x7)
                   2 -> do x1 <- get
                           x2 <- get
                           x3 <- get
                           x4 <- get
                           return (PClauseR x1 x2 x3 x4)
                   3 -> do x1 <- get
                           x2 <- get
                           x3 <- get
                           x4 <- get
                           x5 <- get
                           return (PWithR x1 x2 x3 x4 x5)
                   _ -> error "Corrupted binary data for PClause'"

instance (Binary t) => Binary (PData' t) where
        put x
          = case x of
                PDatadecl x1 x2 x3 -> do putWord8 0
                                         put x1
                                         put x2
                                         put x3
                PLaterdecl x1 x2 -> do putWord8 1
                                       put x1
                                       put x2
        get
          = do i <- getWord8
               case i of
                   0 -> do x1 <- get
                           x2 <- get
                           x3 <- get
                           return (PDatadecl x1 x2 x3)
                   1 -> do x1 <- get
                           x2 <- get
                           return (PLaterdecl x1 x2)
                   _ -> error "Corrupted binary data for PData'"

instance Binary PunInfo where
        put x
          = case x of
              TypeOrTerm -> putWord8 0
              IsType     -> putWord8 1
              IsTerm     -> putWord8 2
        get
          = do i <- getWord8
               case i of
                 0 -> return TypeOrTerm
                 1 -> return IsType
                 2 -> return IsTerm
                 _ -> error "Corrupted binary data for PunInfo"

instance Binary PTerm where
        put x
          = case x of
                PQuote x1 -> do putWord8 0
                                put x1
                PRef x1 x2 -> do putWord8 1
                                 put x1
                                 put x2
                PInferRef x1 x2 -> do putWord8 2
                                      put x1
                                      put x2
                PPatvar x1 x2 -> do putWord8 3
                                    put x1
                                    put x2
                PLam x1 x2 x3 x4 -> do putWord8 4
                                       put x1
                                       put x2
                                       put x3
                                       put x4
                PPi x1 x2 x3 x4 -> do putWord8 5
                                      put x1
                                      put x2
                                      put x3
                                      put x4
                PLet x1 x2 x3 x4 x5 -> do putWord8 6
                                          put x1
                                          put x2
                                          put x3
                                          put x4
                                          put x5
                PTyped x1 x2 -> do putWord8 7
                                   put x1
                                   put x2
                PAppImpl x1 x2 -> error "PAppImpl in final term"
                PApp x1 x2 x3 -> do putWord8 8
                                    put x1
                                    put x2
                                    put x3
                PAppBind x1 x2 x3 -> do putWord8 9
                                        put x1
                                        put x2
                                        put x3
                PMatchApp x1 x2 -> do putWord8 10
                                      put x1
                                      put x2
                PCase x1 x2 x3 -> do putWord8 11
                                     put x1
                                     put x2
                                     put x3
                PTrue x1 x2 -> do putWord8 12
                                  put x1
                                  put x2
                PRefl x1 x2 -> do putWord8 14
                                  put x1
                                  put x2
                PResolveTC x1 -> do putWord8 15
                                    put x1
                PEq x1 x2 x3 x4 x5 -> do putWord8 16
                                         put x1
                                         put x2
                                         put x3
                                         put x4
                                         put x5
                PRewrite x1 x2 x3 x4 -> do putWord8 17
                                           put x1
                                           put x2
                                           put x3
                                           put x4
                PPair x1 x2 x3 x4 -> do putWord8 18
                                        put x1
                                        put x2
                                        put x3
                                        put x4
                PDPair x1 x2 x3 x4 x5 -> do putWord8 19
                                            put x1
                                            put x2
                                            put x3
                                            put x4
                                            put x5
                PAlternative x1 x2 -> do putWord8 20
                                         put x1
                                         put x2
                PHidden x1 -> do putWord8 21
                                 put x1
                PType -> putWord8 22
                PGoal x1 x2 x3 x4 -> do putWord8 23
                                        put x1
                                        put x2
                                        put x3
                                        put x4
                PConstant x1 -> do putWord8 24
                                   put x1
                Placeholder -> putWord8 25
                PDoBlock x1 -> do putWord8 26
                                  put x1
                PIdiom x1 x2 -> do putWord8 27
                                   put x1
                                   put x2
                PReturn x1 -> do putWord8 28
                                 put x1
                PMetavar x1 -> do putWord8 29
                                  put x1
                PProof x1 -> do putWord8 30
                                put x1
                PTactics x1 -> do putWord8 31
                                  put x1
                PImpossible -> putWord8 33
                PCoerced x1 -> do putWord8 34
                                  put x1
                PUnifyLog x1 -> do putWord8 35
                                   put x1
                PNoImplicits x1 -> do putWord8 36
                                      put x1
                PDisamb x1 x2 -> do putWord8 37
                                    put x1
                                    put x2
                PUniverse x1 -> do putWord8 38
                                   put x1
                PRunTactics x1 x2 -> do putWord8 39
                                        put x1
                                        put x2
                PAs x1 x2 x3 -> do putWord8 40
                                   put x1
                                   put x2
                                   put x3
                PElabError x1 -> do putWord8 41
                                    put x1
                PQuasiquote x1 x2 -> do putWord8 42
                                        put x1
                                        put x2
                PUnquote x1 -> do putWord8 43
                                  put x1


        get
          = do i <- getWord8
               case i of
                   0 -> do x1 <- get
                           return (PQuote x1)
                   1 -> do x1 <- get
                           x2 <- get
                           return (PRef x1 x2)
                   2 -> do x1 <- get
                           x2 <- get
                           return (PInferRef x1 x2)
                   3 -> do x1 <- get
                           x2 <- get
                           return (PPatvar x1 x2)
                   4 -> do x1 <- get
                           x2 <- get
                           x3 <- get
                           x4 <- get
                           return (PLam x1 x2 x3 x4)
                   5 -> do x1 <- get
                           x2 <- get
                           x3 <- get
                           x4 <- get
                           return (PPi x1 x2 x3 x4)
                   6 -> do x1 <- get
                           x2 <- get
                           x3 <- get
                           x4 <- get
                           x5 <- get
                           return (PLet x1 x2 x3 x4 x5)
                   7 -> do x1 <- get
                           x2 <- get
                           return (PTyped x1 x2)
                   8 -> do x1 <- get
                           x2 <- get
                           x3 <- get
                           return (PApp x1 x2 x3)
                   9 -> do x1 <- get
                           x2 <- get
                           x3 <- get
                           return (PAppBind x1 x2 x3)
                   10 -> do x1 <- get
                            x2 <- get
                            return (PMatchApp x1 x2)
                   11 -> do x1 <- get
                            x2 <- get
                            x3 <- get
                            return (PCase x1 x2 x3)
                   12 -> do x1 <- get
                            x2 <- get
                            return (PTrue x1 x2)
                   14 -> do x1 <- get
                            x2 <- get
                            return (PRefl x1 x2)
                   15 -> do x1 <- get
                            return (PResolveTC x1)
                   16 -> do x1 <- get
                            x2 <- get
                            x3 <- get
                            x4 <- get
                            x5 <- get
                            return (PEq x1 x2 x3 x4 x5)
                   17 -> do x1 <- get
                            x2 <- get
                            x3 <- get
                            x4 <- get
                            return (PRewrite x1 x2 x3 x4)
                   18 -> do x1 <- get
                            x2 <- get
                            x3 <- get
                            x4 <- get
                            return (PPair x1 x2 x3 x4)
                   19 -> do x1 <- get
                            x2 <- get
                            x3 <- get
                            x4 <- get
                            x5 <- get
                            return (PDPair x1 x2 x3 x4 x5)
                   20 -> do x1 <- get
                            x2 <- get
                            return (PAlternative x1 x2)
                   21 -> do x1 <- get
                            return (PHidden x1)
                   22 -> return PType
                   23 -> do x1 <- get
                            x2 <- get
                            x3 <- get
                            x4 <- get
                            return (PGoal x1 x2 x3 x4)
                   24 -> do x1 <- get
                            return (PConstant x1)
                   25 -> return Placeholder
                   26 -> do x1 <- get
                            return (PDoBlock x1)
                   27 -> do x1 <- get
                            x2 <- get
                            return (PIdiom x1 x2)
                   28 -> do x1 <- get
                            return (PReturn x1)
                   29 -> do x1 <- get
                            return (PMetavar x1)
                   30 -> do x1 <- get
                            return (PProof x1)
                   31 -> do x1 <- get
                            return (PTactics x1)
                   33 -> return PImpossible
                   34 -> do x1 <- get
                            return (PCoerced x1)
                   35 -> do x1 <- get
                            return (PUnifyLog x1)
                   36 -> do x1 <- get
                            return (PNoImplicits x1)
                   37 -> do x1 <- get
                            x2 <- get
                            return (PDisamb x1 x2)
                   38 -> do x1 <- get
                            return (PUniverse x1)
                   39 -> do x1 <- get
                            x2 <- get
                            return (PRunTactics x1 x2)
                   40 -> do x1 <- get
                            x2 <- get
                            x3 <- get
                            return (PAs x1 x2 x3)
                   41 -> do x1 <- get
                            return (PElabError x1)
                   42 -> do x1 <- get
                            x2 <- get
                            return (PQuasiquote x1 x2)
                   43 -> do x1 <- get
                            return (PUnquote x1)
                   _ -> error "Corrupted binary data for PTerm"

instance (Binary t) => Binary (PTactic' t) where
        put x
          = case x of
                Intro x1 -> do putWord8 0
                               put x1
                Focus x1 -> do putWord8 1
                               put x1
                Refine x1 x2 -> do putWord8 2
                                   put x1
                                   put x2
                Rewrite x1 -> do putWord8 3
                                 put x1
                LetTac x1 x2 -> do putWord8 4
                                   put x1
                                   put x2
                Exact x1 -> do putWord8 5
                               put x1
                Compute -> putWord8 6
                Trivial -> putWord8 7
                Solve -> putWord8 8
                Attack -> putWord8 9
                ProofState -> putWord8 10
                ProofTerm -> putWord8 11
                Undo -> putWord8 12
                Try x1 x2 -> do putWord8 13
                                put x1
                                put x2
                TSeq x1 x2 -> do putWord8 14
                                 put x1
                                 put x2
                Qed -> putWord8 15
                ApplyTactic x1 -> do putWord8 16
                                     put x1
                Reflect x1 -> do putWord8 17
                                 put x1
                Fill x1 -> do putWord8 18
                              put x1
                Induction x1 -> do putWord8 19
                                   put x1
                ByReflection x1 -> do putWord8 20
                                      put x1
                ProofSearch x1 x2 x3 x4 x5 -> do putWord8 21
                                                 put x1
                                                 put x2
                                                 put x3
                                                 put x4
                                                 put x5
                DoUnify -> putWord8 22
                CaseTac x1 -> do putWord8 23
                                 put x1
                SourceFC -> putWord8 24
                Intros -> putWord8 25
                Equiv x1 -> do putWord8 26
                               put x1
                Claim x1 x2 -> do putWord8 27
                                  put x1
                                  put x2
                Unfocus -> putWord8 28
                MatchRefine x1 -> do putWord8 29
                                     put x1
                LetTacTy x1 x2 x3 -> do putWord8 30
                                        put x1
                                        put x2
                                        put x3
                TCInstance -> putWord8 31
                GoalType x1 x2 -> do putWord8 32
                                     put x1
                                     put x2
                TCheck x1 -> do putWord8 33
                                put x1
                TEval x1 -> do putWord8 34
                               put x1
                TDocStr x1 -> do putWord8 35
                                 put x1
                TSearch x1 -> do putWord8 36
                                 put x1
                Skip -> putWord8 37
                TFail x1 -> do putWord8 38
                               put x1
                Abandon -> putWord8 39
        get
          = do i <- getWord8
               case i of
                   0 -> do x1 <- get
                           return (Intro x1)
                   1 -> do x1 <- get
                           return (Focus x1)
                   2 -> do x1 <- get
                           x2 <- get
                           return (Refine x1 x2)
                   3 -> do x1 <- get
                           return (Rewrite x1)
                   4 -> do x1 <- get
                           x2 <- get
                           return (LetTac x1 x2)
                   5 -> do x1 <- get
                           return (Exact x1)
                   6 -> return Compute
                   7 -> return Trivial
                   8 -> return Solve
                   9 -> return Attack
                   10 -> return ProofState
                   11 -> return ProofTerm
                   12 -> return Undo
                   13 -> do x1 <- get
                            x2 <- get
                            return (Try x1 x2)
                   14 -> do x1 <- get
                            x2 <- get
                            return (TSeq x1 x2)
                   15 -> return Qed
                   16 -> do x1 <- get
                            return (ApplyTactic x1)
                   17 -> do x1 <- get
                            return (Reflect x1)
                   18 -> do x1 <- get
                            return (Fill x1)
                   19 -> do x1 <- get
                            return (Induction x1)
                   20 -> do x1 <- get
                            return (ByReflection x1)
                   21 -> do x1 <- get
                            x2 <- get
                            x3 <- get
                            x4 <- get
                            x5 <- get
                            return (ProofSearch x1 x2 x3 x4 x5)
                   22 -> return DoUnify
                   23 -> do x1 <- get
                            return (CaseTac x1)
                   24 -> return SourceFC
                   25 -> return Intros
                   26 -> do x1 <- get
                            return (Equiv x1)
                   27 -> do x1 <- get
                            x2 <- get
                            return (Claim x1 x2)
                   28 -> return Unfocus
                   29 -> do x1 <- get
                            return (MatchRefine x1)
                   30 -> do x1 <- get
                            x2 <- get
                            x3 <- get
                            return (LetTacTy x1 x2 x3)
                   31 -> return TCInstance
                   32 -> do x1 <- get
                            x2 <- get
                            return (GoalType x1 x2)
                   33 -> do x1 <- get
                            return (TCheck x1)
                   34 -> do x1 <- get
                            return (TEval x1)
                   35 -> do x1 <- get
                            return (TDocStr x1)
                   36 -> do x1 <- get
                            return (TSearch x1)
                   37 -> return Skip
                   38 -> do x1 <- get
                            return (TFail x1)
                   39 -> return Abandon
                   _ -> error "Corrupted binary data for PTactic'"


instance (Binary t) => Binary (PDo' t) where
        put x
          = case x of
                DoExp x1 x2 -> do putWord8 0
                                  put x1
                                  put x2
                DoBind x1 x2 x3 -> do putWord8 1
                                      put x1
                                      put x2
                                      put x3
                DoBindP x1 x2 x3 x4 -> do putWord8 2
                                          put x1
                                          put x2
                                          put x3
                                          put x4
                DoLet x1 x2 x3 x4 -> do putWord8 3
                                        put x1
                                        put x2
                                        put x3
                                        put x4
                DoLetP x1 x2 x3 -> do putWord8 4
                                      put x1
                                      put x2
                                      put x3
        get
          = do i <- getWord8
               case i of
                   0 -> do x1 <- get
                           x2 <- get
                           return (DoExp x1 x2)
                   1 -> do x1 <- get
                           x2 <- get
                           x3 <- get
                           return (DoBind x1 x2 x3)
                   2 -> do x1 <- get
                           x2 <- get
                           x3 <- get
                           x4 <- get
                           return (DoBindP x1 x2 x3 x4)
                   3 -> do x1 <- get
                           x2 <- get
                           x3 <- get
                           x4 <- get
                           return (DoLet x1 x2 x3 x4)
                   4 -> do x1 <- get
                           x2 <- get
                           x3 <- get
                           return (DoLetP x1 x2 x3)
                   _ -> error "Corrupted binary data for PDo'"


instance (Binary t) => Binary (PArg' t) where
        put x
          = case x of
                PImp x1 x2 x3 x4 x5 ->
                                    do putWord8 0
                                       put x1
                                       put x2
                                       put x3
                                       put x4
                                       put x5
                PExp x1 x2 x3 x4 ->
                                 do putWord8 1
                                    put x1
                                    put x2
                                    put x3
                                    put x4
                PConstraint x1 x2 x3 x4 ->
                                        do putWord8 2
                                           put x1
                                           put x2
                                           put x3
                                           put x4
                PTacImplicit x1 x2 x3 x4 x5 ->
                                               do putWord8 3
                                                  put x1
                                                  put x2
                                                  put x3
                                                  put x4
                                                  put x5
        get
          = do i <- getWord8
               case i of
                   0 -> do x1 <- get
                           x2 <- get
                           x3 <- get
                           x4 <- get
                           x5 <- get
                           return (PImp x1 x2 x3 x4 x5)
                   1 -> do x1 <- get
                           x2 <- get
                           x3 <- get
                           x4 <- get
                           return (PExp x1 x2 x3 x4)
                   2 -> do x1 <- get
                           x2 <- get
                           x3 <- get
                           x4 <- get
                           return (PConstraint x1 x2 x3 x4)
                   3 -> do x1 <- get
                           x2 <- get
                           x3 <- get
                           x4 <- get
                           x5 <- get
                           return (PTacImplicit x1 x2 x3 x4 x5)
                   _ -> error "Corrupted binary data for PArg'"


instance Binary ClassInfo where
        put (CI x1 x2 x3 x4 x5 _ x6)
          = do put x1
               put x2
               put x3
               put x4
               put x5
               put x6
        get
          = do x1 <- get
               x2 <- get
               x3 <- get
               x4 <- get
               x5 <- get
               x6 <- get
               return (CI x1 x2 x3 x4 x5 [] x6)

instance Binary OptInfo where
        put (Optimise x1 x2)
          = do put x1
               put x2
        get
          = do x1 <- get
               x2 <- get
               return (Optimise x1 x2)

instance Binary FnInfo where
        put (FnInfo x1)
          = put x1
        get
          = do x1 <- get
               return (FnInfo x1)

instance Binary TypeInfo where
        put (TI x1 x2 x3 x4 x5) = do put x1
                                     put x2
                                     put x3
                                     put x4
                                     put x5
        get = do x1 <- get
                 x2 <- get
                 x3 <- get
                 x4 <- get
                 x5 <- get
                 return (TI x1 x2 x3 x4 x5)

instance Binary SynContext where
        put x
          = case x of
                PatternSyntax -> putWord8 0
                TermSyntax -> putWord8 1
                AnySyntax -> putWord8 2
        get
          = do i <- getWord8
               case i of
                   0 -> return PatternSyntax
                   1 -> return TermSyntax
                   2 -> return AnySyntax
                   _ -> error "Corrupted binary data for SynContext"


instance Binary Syntax where
        put (Rule x1 x2 x3)
          = do put x1
               put x2
               put x3
        get
          = do x1 <- get
               x2 <- get
               x3 <- get
               return (Rule x1 x2 x3)

instance (Binary t) => Binary (DSL' t) where
        put (DSL x1 x2 x3 x4 x5 x6 x7 x8 x9 x10)
          = do put x1
               put x2
               put x3
               put x4
               put x5
               put x6
               put x7
               put x8
               put x9
               put x10
        get
          = do x1 <- get
               x2 <- get
               x3 <- get
               x4 <- get
               x5 <- get
               x6 <- get
               x7 <- get
               x8 <- get
               x9 <- get
               x10 <- get
               return (DSL x1 x2 x3 x4 x5 x6 x7 x8 x9 x10)

instance Binary SSymbol where
        put x
          = case x of
                Keyword x1 -> do putWord8 0
                                 put x1
                Symbol x1 -> do putWord8 1
                                put x1
                Expr x1 -> do putWord8 2
                              put x1
                SimpleExpr x1 -> do putWord8 3
                                    put x1
                Binding x1 -> do putWord8 4
                                 put x1
        get
          = do i <- getWord8
               case i of
                   0 -> do x1 <- get
                           return (Keyword x1)
                   1 -> do x1 <- get
                           return (Symbol x1)
                   2 -> do x1 <- get
                           return (Expr x1)
                   3 -> do x1 <- get
                           return (SimpleExpr x1)
                   4 -> do x1 <- get
                           return (Binding x1)
                   _ -> error "Corrupted binary data for SSymbol"

instance Binary Codegen where
        put x
          = case x of
                Via str -> do putWord8 0
                              put str
                Bytecode -> putWord8 1
        get
          = do i <- getWord8
               case i of
                  0 -> do x1 <- get
                          return (Via x1)
                  1 -> return Bytecode
                  _ -> error  "Corrupted binary data for Codegen"