git.iko.soy/Idris-dev
on bf4e535 help sign in
Idris-dev/src/Idris/IBC.hs
2234 lines 89 kB history raw
1{-# LANGUAGE TypeSynonymInstances #-}
2{-# OPTIONS_GHC -fwarn-incomplete-patterns #-}
4module Idris.IBC where
6import Idris.Core.Evaluate
7import Idris.Core.TT
8import Idris.Core.Binary
9import Idris.Core.CaseTree
10import Idris.AbsSyntax
11import Idris.Imports
12import Idris.Error
13import Idris.DeepSeq
14import Idris.Delaborate
15import qualified Idris.Docstrings as D
16import Idris.Docstrings (Docstring)
17import Idris.Output
18import IRTS.System (getIdrisLibDir)
19import Paths_idris
21import qualified Cheapskate.Types as CT
23import Data.Binary
24import Data.Vector.Binary
25import Data.List
26import Data.ByteString.Lazy as B hiding (length, elem, map)
27import qualified Data.Text as T
28import qualified Data.Set as S
30import Control.Monad
31import Control.DeepSeq
32import Control.Monad.State.Strict hiding (get, put)
33import qualified Control.Monad.State.Strict as ST
34import System.FilePath
35import System.Directory
36import Codec.Compression.Zlib (compress)
37import Util.Zlib (decompressEither)
39ibcVersion :: Word8
40ibcVersion = 104
42data IBCFile = IBCFile { ver :: Word8,
43 sourcefile :: FilePath,
44 symbols :: ![Name],
45 ibc_imports :: ![(Bool, FilePath)],
46 ibc_importdirs :: ![FilePath],
47 ibc_implicits :: ![(Name, [PArg])],
48 ibc_fixes :: ![FixDecl],
49 ibc_statics :: ![(Name, [Bool])],
50 ibc_classes :: ![(Name, ClassInfo)],
51 ibc_instances :: ![(Bool, Name, Name)],
52 ibc_dsls :: ![(Name, DSL)],
53 ibc_datatypes :: ![(Name, TypeInfo)],
54 ibc_optimise :: ![(Name, OptInfo)],
55 ibc_syntax :: ![Syntax],
56 ibc_keywords :: ![String],
57 ibc_objs :: ![(Codegen, FilePath)],
58 ibc_libs :: ![(Codegen, String)],
59 ibc_cgflags :: ![(Codegen, String)],
60 ibc_dynamic_libs :: ![String],
61 ibc_hdrs :: ![(Codegen, String)],
62 ibc_access :: ![(Name, Accessibility)],
63 ibc_total :: ![(Name, Totality)],
64 ibc_totcheckfail :: ![(FC, String)],
65 ibc_flags :: ![(Name, [FnOpt])],
66 ibc_fninfo :: ![(Name, FnInfo)],
67 ibc_cg :: ![(Name, CGInfo)],
68 ibc_defs :: ![(Name, Def)],
69 ibc_docstrings :: ![(Name, (Docstring D.DocTerm, [(Name, Docstring D.DocTerm)]))],
70 ibc_moduledocs :: ![(Name, Docstring D.DocTerm)],
71 ibc_transforms :: ![(Name, (Term, Term))],
72 ibc_errRev :: ![(Term, Term)],
73 ibc_coercions :: ![Name],
74 ibc_lineapps :: ![(FilePath, Int, PTerm)],
75 ibc_namehints :: ![(Name, Name)],
76 ibc_metainformation :: ![(Name, MetaInformation)],
77 ibc_errorhandlers :: ![Name],
78 ibc_function_errorhandlers :: ![(Name, Name, Name)], -- fn, arg, handler
79 ibc_metavars :: ![(Name, (Maybe Name, Int, Bool))],
80 ibc_patdefs :: ![(Name, ([([Name], Term, Term)], [PTerm]))],
81 ibc_postulates :: ![Name],
82 ibc_externs :: ![(Name, Int)],
83 ibc_parsedSpan :: !(Maybe FC),
84 ibc_usage :: ![(Name, Int)],
85 ibc_exports :: ![Name],
86 ibc_autohints :: ![(Name, Name)]
87 }
88 deriving Show
89{-!
90deriving instance Binary IBCFile
91!-}
93initIBC :: IBCFile
94initIBC = IBCFile ibcVersion "" [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] Nothing [] [] []
96loadIBC :: Bool -- ^ True = reexport, False = make everything private
97 -> FilePath -> Idris ()
98loadIBC reexport fp
99 = do imps <- getImported
100 let redo = case lookup fp imps of
101 Nothing -> True
102 Just p -> not p && reexport
103 when redo $
104 do iLOG $ "Loading ibc " ++ fp ++ " " ++ show reexport
105 ibcf <- runIO $ (bdecode fp :: IO IBCFile)
106 process reexport ibcf fp
107 addImported reexport fp
109-- | Load an entire package from its index file
110loadPkgIndex :: String -> Idris ()
111loadPkgIndex pkg = do ddir <- runIO $ getIdrisLibDir
112 addImportDir (ddir </> pkg)
113 fp <- findPkgIndex pkg
114 loadIBC True fp
116bencode :: Binary a => FilePath -> a -> IO ()
117bencode f d = B.writeFile f (compress (encode d))
119bdecode :: Binary b => FilePath -> IO b
120bdecode f = do d' <- B.readFile f
121 either
122 (\(_, e) -> error $ "Invalid / corrupted zip format on " ++ show f ++ ": " ++ e)
123 (return . decode)
124 (decompressEither d')
126writeIBC :: FilePath -> FilePath -> Idris ()
127writeIBC src f
128 = do iLOG $ "Writing ibc " ++ show f
129 i <- getIState
130-- case (Data.List.map fst (idris_metavars i)) \\ primDefs of
131-- (_:_) -> ifail "Can't write ibc when there are unsolved metavariables"
132-- [] -> return ()
133 resetNameIdx
134 ibcf <- mkIBC (ibc_write i) (initIBC { sourcefile = src })
135 idrisCatch (do runIO $ createDirectoryIfMissing True (dropFileName f)
136 runIO $ bencode f ibcf
137 iLOG "Written")
138 (\c -> do iLOG $ "Failed " ++ pshow i c)
139 return ()
141-- Write a package index containing all the imports in the current IState
142-- Used for ':search' of an entire package, to ensure everything is loaded.
143writePkgIndex :: FilePath -> Idris ()
144writePkgIndex f
145 = do i <- getIState
146 let imps = map (\ (x, y) -> (True, x)) $ idris_imported i
147 iLOG $ "Writing package index " ++ show f ++ " including\n" ++
148 show (map snd imps)
149 resetNameIdx
150 let ibcf = initIBC { ibc_imports = imps }
151 idrisCatch (do runIO $ createDirectoryIfMissing True (dropFileName f)
152 runIO $ bencode f ibcf
153 iLOG "Written")
154 (\c -> do iLOG $ "Failed " ++ pshow i c)
155 return ()
157mkIBC :: [IBCWrite] -> IBCFile -> Idris IBCFile
158mkIBC [] f = return f
159mkIBC (i:is) f = do ist <- getIState
160 logLvl 5 $ show i ++ " " ++ show (Data.List.length is)
161 f' <- ibc ist i f
162 mkIBC is f'
164ibc :: IState -> IBCWrite -> IBCFile -> Idris IBCFile
165ibc i (IBCFix d) f = return f { ibc_fixes = d : ibc_fixes f }
166ibc i (IBCImp n) f = case lookupCtxtExact n (idris_implicits i) of
167 Just v -> return f { ibc_implicits = (n,v): ibc_implicits f }
168 _ -> ifail "IBC write failed"
169ibc i (IBCStatic n) f
170 = case lookupCtxtExact n (idris_statics i) of
171 Just v -> return f { ibc_statics = (n,v): ibc_statics f }
172 _ -> ifail "IBC write failed"
173ibc i (IBCClass n) f
174 = case lookupCtxtExact n (idris_classes i) of
175 Just v -> return f { ibc_classes = (n,v): ibc_classes f }
176 _ -> ifail "IBC write failed"
177ibc i (IBCInstance int n ins) f
178 = return f { ibc_instances = (int,n,ins): ibc_instances f }
179ibc i (IBCDSL n) f
180 = case lookupCtxtExact n (idris_dsls i) of
181 Just v -> return f { ibc_dsls = (n,v): ibc_dsls f }
182 _ -> ifail "IBC write failed"
183ibc i (IBCData n) f
184 = case lookupCtxtExact n (idris_datatypes i) of
185 Just v -> return f { ibc_datatypes = (n,v): ibc_datatypes f }
186 _ -> ifail "IBC write failed"
187ibc i (IBCOpt n) f = case lookupCtxtExact n (idris_optimisation i) of
188 Just v -> return f { ibc_optimise = (n,v): ibc_optimise f }
189 _ -> ifail "IBC write failed"
190ibc i (IBCSyntax n) f = return f { ibc_syntax = n : ibc_syntax f }
191ibc i (IBCKeyword n) f = return f { ibc_keywords = n : ibc_keywords f }
192ibc i (IBCImport n) f = return f { ibc_imports = n : ibc_imports f }
193ibc i (IBCImportDir n) f = return f { ibc_importdirs = n : ibc_importdirs f }
194ibc i (IBCObj tgt n) f = return f { ibc_objs = (tgt, n) : ibc_objs f }
195ibc i (IBCLib tgt n) f = return f { ibc_libs = (tgt, n) : ibc_libs f }
196ibc i (IBCCGFlag tgt n) f = return f { ibc_cgflags = (tgt, n) : ibc_cgflags f }
197ibc i (IBCDyLib n) f = return f {ibc_dynamic_libs = n : ibc_dynamic_libs f }
198ibc i (IBCHeader tgt n) f = return f { ibc_hdrs = (tgt, n) : ibc_hdrs f }
199ibc i (IBCDef n) f
200 = do f' <- case lookupDefExact n (tt_ctxt i) of
201 Just v -> return f { ibc_defs = (n,v) : ibc_defs f }
202 _ -> ifail "IBC write failed"
203 case lookupCtxtExact n (idris_patdefs i) of
204 Just v -> return f' { ibc_patdefs = (n,v) : ibc_patdefs f }
205 _ -> return f' -- Not a pattern definition
207ibc i (IBCDoc n) f = case lookupCtxtExact n (idris_docstrings i) of
208 Just v -> return f { ibc_docstrings = (n,v) : ibc_docstrings f }
209 _ -> ifail "IBC write failed"
210ibc i (IBCCG n) f = case lookupCtxtExact n (idris_callgraph i) of
211 Just v -> return f { ibc_cg = (n,v) : ibc_cg f }
212 _ -> ifail "IBC write failed"
213ibc i (IBCCoercion n) f = return f { ibc_coercions = n : ibc_coercions f }
214ibc i (IBCAccess n a) f = return f { ibc_access = (n,a) : ibc_access f }
215ibc i (IBCFlags n a) f = return f { ibc_flags = (n,a) : ibc_flags f }
216ibc i (IBCFnInfo n a) f = return f { ibc_fninfo = (n,a) : ibc_fninfo f }
217ibc i (IBCTotal n a) f = return f { ibc_total = (n,a) : ibc_total f }
218ibc i (IBCTrans n t) f = return f { ibc_transforms = (n, t) : ibc_transforms f }
219ibc i (IBCErrRev t) f = return f { ibc_errRev = t : ibc_errRev f }
220ibc i (IBCLineApp fp l t) f
221 = return f { ibc_lineapps = (fp,l,t) : ibc_lineapps f }
222ibc i (IBCNameHint (n, ty)) f
223 = return f { ibc_namehints = (n, ty) : ibc_namehints f }
224ibc i (IBCMetaInformation n m) f = return f { ibc_metainformation = (n,m) : ibc_metainformation f }
225ibc i (IBCErrorHandler n) f = return f { ibc_errorhandlers = n : ibc_errorhandlers f }
226ibc i (IBCFunctionErrorHandler fn a n) f =
227 return f { ibc_function_errorhandlers = (fn, a, n) : ibc_function_errorhandlers f }
228ibc i (IBCMetavar n) f =
229 case lookup n (idris_metavars i) of
230 Nothing -> return f
231 Just t -> return f { ibc_metavars = (n, t) : ibc_metavars f }
232ibc i (IBCPostulate n) f = return f { ibc_postulates = n : ibc_postulates f }
233ibc i (IBCExtern n) f = return f { ibc_externs = n : ibc_externs f }
234ibc i (IBCTotCheckErr fc err) f = return f { ibc_totcheckfail = (fc, err) : ibc_totcheckfail f }
235ibc i (IBCParsedRegion fc) f = return f { ibc_parsedSpan = Just fc }
236ibc i (IBCModDocs n) f = case lookupCtxtExact n (idris_moduledocs i) of
237 Just v -> return f { ibc_moduledocs = (n,v) : ibc_moduledocs f }
238 _ -> ifail "IBC write failed"
239ibc i (IBCUsage n) f = return f { ibc_usage = n : ibc_usage f }
240ibc i (IBCExport n) f = return f { ibc_exports = n : ibc_exports f }
241ibc i (IBCAutoHint n h) f = return f { ibc_autohints = (n, h) : ibc_autohints f }
243process :: Bool -- ^ Reexporting
244 -> IBCFile -> FilePath -> Idris ()
245process reexp i fn
246 | ver i /= ibcVersion
247 = do iLOG "ibc out of date"
248 let e = if ver i < ibcVersion then " an earlier " else " a later "
249 ifail $ "Incompatible ibc version.\nThis library was built with"
250 ++ e ++ "version of Idris.\n" ++
251 "Please clean and rebuild."
253 --- please rebuild"
254 | otherwise =
255 do srcok <- runIO $ doesFileExist (sourcefile i)
256 when srcok $ timestampOlder (sourcefile i) fn
257 v <- verbose
258 quiet <- getQuiet
259-- when (v && srcok && not quiet) $ iputStrLn $ "Skipping " ++ sourcefile i
260 pImportDirs $ force (ibc_importdirs i)
261 pImports $ force (ibc_imports i)
262 pImps $ force (ibc_implicits i)
263 pFixes $ force (ibc_fixes i)
264 pStatics $ force (ibc_statics i)
265 pClasses $ force (ibc_classes i)
266 pInstances $ force (ibc_instances i)
267 pDSLs $ force (ibc_dsls i)
268 pDatatypes $ force (ibc_datatypes i)
269 pOptimise $ force (ibc_optimise i)
270 pSyntax $ force (ibc_syntax i)
271 pKeywords $ force (ibc_keywords i)
272 pObjs $ force (ibc_objs i)
273 pLibs $ force (ibc_libs i)
274 pCGFlags $ force (ibc_cgflags i)
275 pDyLibs $ force (ibc_dynamic_libs i)
276 pHdrs $ force (ibc_hdrs i)
277 pDefs reexp (symbols i) $ force (ibc_defs i)
278 pPatdefs $ force (ibc_patdefs i)
279 pAccess reexp $ force (ibc_access i)
280 pFlags $ force (ibc_flags i)
281 pFnInfo $ force (ibc_fninfo i)
282 pTotal $ force (ibc_total i)
283 pTotCheckErr $ force (ibc_totcheckfail i)
284 pCG $ force (ibc_cg i)
285 pDocs $ force (ibc_docstrings i)
286 pMDocs $ force (ibc_moduledocs i)
287 pCoercions $ force (ibc_coercions i)
288 pTrans $ force (ibc_transforms i)
289 pErrRev $ force (ibc_errRev i)
290 pLineApps $ force (ibc_lineapps i)
291 pNameHints $ force (ibc_namehints i)
292 pMetaInformation $ force (ibc_metainformation i)
293 pErrorHandlers $ force (ibc_errorhandlers i)
294 pFunctionErrorHandlers $ force (ibc_function_errorhandlers i)
295 pMetavars $ force (ibc_metavars i)
296 pPostulates $ force (ibc_postulates i)
297 pExterns $ force (ibc_externs i)
298 pParsedSpan $ force (ibc_parsedSpan i)
299 pUsage $ force (ibc_usage i)
300 pExports $ force (ibc_exports i)
301 pAutoHints $ force (ibc_autohints i)
303timestampOlder :: FilePath -> FilePath -> Idris ()
304timestampOlder src ibc = do srct <- runIO $ getModificationTime src
305 ibct <- runIO $ getModificationTime ibc
306 if (srct > ibct)
307 then ifail "Needs reloading"
308 else return ()
310pPostulates :: [Name] -> Idris ()
311pPostulates ns = do
312 i <- getIState
313 putIState i{ idris_postulates = idris_postulates i `S.union` S.fromList ns }
315pExterns :: [(Name, Int)] -> Idris ()
316pExterns ns = do
317 i <- getIState
318 putIState i{ idris_externs = idris_externs i `S.union` S.fromList ns }
320pParsedSpan :: Maybe FC -> Idris ()
321pParsedSpan fc = do ist <- getIState
322 putIState ist { idris_parsedSpan = fc }
324pUsage :: [(Name, Int)] -> Idris ()
325pUsage ns = do ist <- getIState
326 putIState ist { idris_erasureUsed = ns ++ idris_erasureUsed ist }
328pExports :: [Name] -> Idris ()
329pExports ns = do ist <- getIState
330 putIState ist { idris_exports = ns ++ idris_exports ist }
332pAutoHints :: [(Name, Name)] -> Idris ()
333pAutoHints ns = mapM_ (\(n,h) -> addAutoHint n h) ns
335pImportDirs :: [FilePath] -> Idris ()
336pImportDirs fs = mapM_ addImportDir fs
338pImports :: [(Bool, FilePath)] -> Idris ()
339pImports fs
340 = do mapM_ (\(re, f) ->
341 do i <- getIState
342 ibcsd <- valIBCSubDir i
343 ids <- allImportDirs
344 fp <- findImport ids ibcsd f
345-- if (f `elem` imported i)
346-- then iLOG $ "Already read " ++ f
347 putIState (i { imported = f : imported i })
348 case fp of
349 LIDR fn -> do iLOG $ "Failed at " ++ fn
350 ifail "Must be an ibc"
351 IDR fn -> do iLOG $ "Failed at " ++ fn
352 ifail "Must be an ibc"
353 IBC fn src -> loadIBC re fn)
354 fs
356pImps :: [(Name, [PArg])] -> Idris ()
357pImps imps = mapM_ (\ (n, imp) ->
358 do i <- getIState
359 case lookupDefAccExact n False (tt_ctxt i) of
360 Just (n, Hidden) -> return ()
361 _ -> putIState (i { idris_implicits
362 = addDef n imp (idris_implicits i) }))
363 imps
365pFixes :: [FixDecl] -> Idris ()
366pFixes f = do i <- getIState
367 putIState (i { idris_infixes = sort $ f ++ idris_infixes i })
369pStatics :: [(Name, [Bool])] -> Idris ()
370pStatics ss = mapM_ (\ (n, s) ->
371 do i <- getIState
372 putIState (i { idris_statics
373 = addDef n s (idris_statics i) }))
374 ss
376pClasses :: [(Name, ClassInfo)] -> Idris ()
377pClasses cs = mapM_ (\ (n, c) ->
378 do i <- getIState
379 -- Don't lose instances from previous IBCs, which
380 -- could have loaded in any order
381 let is = case lookupCtxtExact n (idris_classes i) of
382 Just (CI _ _ _ _ _ ins _) -> ins
383 _ -> []
384 let c' = c { class_instances =
385 class_instances c ++ is }
386 putIState (i { idris_classes
387 = addDef n c' (idris_classes i) }))
388 cs
390pInstances :: [(Bool, Name, Name)] -> Idris ()
391pInstances cs = mapM_ (\ (i, n, ins) -> addInstance i n ins) cs
393pDSLs :: [(Name, DSL)] -> Idris ()
394pDSLs cs = mapM_ (\ (n, c) ->
395 do i <- getIState
396 putIState (i { idris_dsls
397 = addDef n c (idris_dsls i) }))
398 cs
400pDatatypes :: [(Name, TypeInfo)] -> Idris ()
401pDatatypes cs = mapM_ (\ (n, c) ->
402 do i <- getIState
403 putIState (i { idris_datatypes
404 = addDef n c (idris_datatypes i) }))
405 cs
407pOptimise :: [(Name, OptInfo)] -> Idris ()
408pOptimise cs = mapM_ (\ (n, c) ->
409 do i <- getIState
410 putIState (i { idris_optimisation
411 = addDef n c (idris_optimisation i) }))
412 cs
414pSyntax :: [Syntax] -> Idris ()
415pSyntax s = do i <- getIState
416 putIState (i { syntax_rules = updateSyntaxRules s (syntax_rules i) })
418pKeywords :: [String] -> Idris ()
419pKeywords k = do i <- getIState
420 putIState (i { syntax_keywords = k ++ syntax_keywords i })
422pObjs :: [(Codegen, FilePath)] -> Idris ()
423pObjs os = mapM_ (\ (cg, obj) -> do dirs <- allImportDirs
424 o <- runIO $ findInPath dirs obj
425 addObjectFile cg o) os
427pLibs :: [(Codegen, String)] -> Idris ()
428pLibs ls = mapM_ (uncurry addLib) ls
430pCGFlags :: [(Codegen, String)] -> Idris ()
431pCGFlags ls = mapM_ (uncurry addFlag) ls
433pDyLibs :: [String] -> Idris ()
434pDyLibs ls = do res <- mapM (addDyLib . return) ls
435 mapM_ checkLoad res
436 return ()
437 where checkLoad (Left _) = return ()
438 checkLoad (Right err) = ifail err
440pHdrs :: [(Codegen, String)] -> Idris ()
441pHdrs hs = mapM_ (uncurry addHdr) hs
443pPatdefs :: [(Name, ([([Name], Term, Term)], [PTerm]))] -> Idris ()
444pPatdefs ds
445 = mapM_ (\ (n, d) ->
446 do i <- getIState
447 putIState (i { idris_patdefs = addDef n (force d) (idris_patdefs i) }))
448 ds
450pDefs :: Bool -> [Name] -> [(Name, Def)] -> Idris ()
451pDefs reexp syms ds
452 = mapM_ (\ (n, d) ->
453 do d' <- updateDef d
454 case d' of
455 TyDecl _ _ -> return ()
456 _ -> do iLOG $ "SOLVING " ++ show n
457 solveDeferred n
458 i <- getIState
459-- logLvl 1 $ "Added " ++ show (n, d')
460 putIState (i { tt_ctxt = addCtxtDef n d' (tt_ctxt i) })
461 if (not reexp) then do iLOG $ "Not exporting " ++ show n
462 setAccessibility n Hidden
463 else iLOG $ "Exporting " ++ show n) ds
464 where
465 updateDef (CaseOp c t args o s cd)
466 = do o' <- mapM updateOrig o
467 cd' <- updateCD cd
468 return $ CaseOp c t args o' s cd'
469 updateDef t = return t
471 updateOrig (Left t) = liftM Left (update t)
472 updateOrig (Right (l, r)) = do l' <- update l
473 r' <- update r
474 return $ Right (l', r')
476 updateCD (CaseDefs (ts, t) (cs, c) (is, i) (rs, r))
477 = do t' <- updateSC t
478 c' <- updateSC c
479 i' <- updateSC i
480 r' <- updateSC r
481 return $ CaseDefs (ts, t') (cs, c') (is, i') (rs, r')
483 updateSC (Case t n alts) = do alts' <- mapM updateAlt alts
484 return (Case t n alts')
485 updateSC (ProjCase t alts) = do alts' <- mapM updateAlt alts
486 return (ProjCase t alts')
487 updateSC (STerm t) = do t' <- update t
488 return (STerm t')
489 updateSC c = return c
491 updateAlt (ConCase n i ns t) = do t' <- updateSC t
492 return (ConCase n i ns t')
493 updateAlt (FnCase n ns t) = do t' <- updateSC t
494 return (FnCase n ns t')
495 updateAlt (ConstCase c t) = do t' <- updateSC t
496 return (ConstCase c t')
497 updateAlt (SucCase n t) = do t' <- updateSC t
498 return (SucCase n t')
499 updateAlt (DefaultCase t) = do t' <- updateSC t
500 return (DefaultCase t')
502 update (P t n ty) = do n' <- getSymbol n
503 return $ P t n' ty
504 update (App f a) = liftM2 App (update f) (update a)
505 update (Bind n b sc) = do b' <- updateB b
506 sc' <- update sc
507 return $ Bind n b' sc'
508 where
509 updateB (Let t v) = liftM2 Let (update t) (update v)
510 updateB b = do ty' <- update (binderTy b)
511 return (b { binderTy = ty' })
512 update (Proj t i) = do t' <- update t
513 return $ Proj t' i
514 update t = return t
516pDocs :: [(Name, (Docstring D.DocTerm, [(Name, Docstring D.DocTerm)]))] -> Idris ()
517pDocs ds = mapM_ (\(n, a) -> addDocStr n (fst a) (snd a)) ds
519pMDocs :: [(Name, Docstring D.DocTerm)] -> Idris ()
520pMDocs ds = mapM_ addMDocStr ds
521 where addMDocStr (n, d) = do ist <- getIState
522 putIState ist { idris_moduledocs = addDef n d (idris_moduledocs ist) }
524pAccess :: Bool -- ^ Reexporting?
525 -> [(Name, Accessibility)] -> Idris ()
526pAccess reexp ds
527 = mapM_ (\ (n, a_in) ->
528 do let a = if reexp then a_in else Hidden
529 logLvl 3 $ "Setting " ++ show (a, n) ++ " to " ++ show a
530 i <- getIState
531 putIState (i { tt_ctxt = setAccess n a (tt_ctxt i) }))
532 ds
534pFlags :: [(Name, [FnOpt])] -> Idris ()
535pFlags ds = mapM_ (\ (n, a) -> setFlags n a) ds
537pFnInfo :: [(Name, FnInfo)] -> Idris ()
538pFnInfo ds = mapM_ (\ (n, a) -> setFnInfo n a) ds
540pTotal :: [(Name, Totality)] -> Idris ()
541pTotal ds = mapM_ (\ (n, a) ->
542 do i <- getIState
543 putIState (i { tt_ctxt = setTotal n a (tt_ctxt i) }))
544 ds
546pTotCheckErr :: [(FC, String)] -> Idris ()
547pTotCheckErr es = do ist <- getIState
548 putIState ist { idris_totcheckfail = idris_totcheckfail ist ++ es }
550pCG :: [(Name, CGInfo)] -> Idris ()
551pCG ds = mapM_ (\ (n, a) -> addToCG n a) ds
553pCoercions :: [Name] -> Idris ()
554pCoercions ns = mapM_ (\ n -> addCoercion n) ns
556pTrans :: [(Name, (Term, Term))] -> Idris ()
557pTrans ts = mapM_ (\ (n, t) -> addTrans n t) ts
559pErrRev :: [(Term, Term)] -> Idris ()
560pErrRev ts = mapM_ addErrRev ts
562pLineApps :: [(FilePath, Int, PTerm)] -> Idris ()
563pLineApps ls = mapM_ (\ (f, i, t) -> addInternalApp f i t) ls
565pNameHints :: [(Name, Name)] -> Idris ()
566pNameHints ns = mapM_ (\ (n, ty) -> addNameHint n ty) ns
568pMetaInformation :: [(Name, MetaInformation)] -> Idris ()
569pMetaInformation ds = mapM_ (\ (n, m) ->
570 do i <- getIState
571 putIState (i { tt_ctxt = setMetaInformation n m (tt_ctxt i) }))
572 ds
574pErrorHandlers :: [Name] -> Idris ()
575pErrorHandlers ns = do i <- getIState
576 putIState $ i { idris_errorhandlers = idris_errorhandlers i ++ ns }
578pFunctionErrorHandlers :: [(Name, Name, Name)] -> Idris ()
579pFunctionErrorHandlers [] = return ()
580pFunctionErrorHandlers ((fn, arg, handler):ns) = do addFunctionErrorHandlers fn arg [handler]
581 pFunctionErrorHandlers ns
583pMetavars :: [(Name, (Maybe Name, Int, Bool))] -> Idris ()
584pMetavars ns = do i <- getIState
585 putIState $ i { idris_metavars = Data.List.reverse ns
586 ++ idris_metavars i }
588----- For Cheapskate and docstrings
590instance Binary a => Binary (D.Docstring a) where
591 put (D.DocString opts lines) = do put opts ; put lines
592 get = do opts <- get
593 lines <- get
594 return (D.DocString opts lines)
596instance Binary CT.Options where
597 put (CT.Options x1 x2 x3 x4) = do put x1 ; put x2 ; put x3 ; put x4
598 get = do x1 <- get
599 x2 <- get
600 x3 <- get
601 x4 <- get
602 return (CT.Options x1 x2 x3 x4)
604instance Binary D.DocTerm where
605 put D.Unchecked = putWord8 0
606 put (D.Checked t) = putWord8 1 >> put t
607 put (D.Example t) = putWord8 2 >> put t
608 put (D.Failing e) = putWord8 3 >> put e
610 get = do i <- getWord8
611 case i of
612 0 -> return D.Unchecked
613 1 -> fmap D.Checked get
614 2 -> fmap D.Example get
615 3 -> fmap D.Failing get
616 _ -> error "Corrupted binary data for DocTerm"
618instance Binary a => Binary (D.Block a) where
619 put (D.Para lines) = do putWord8 0 ; put lines
620 put (D.Header i lines) = do putWord8 1 ; put i ; put lines
621 put (D.Blockquote bs) = do putWord8 2 ; put bs
622 put (D.List b t xs) = do putWord8 3 ; put b ; put t ; put xs
623 put (D.CodeBlock attr txt src) = do putWord8 4 ; put attr ; put txt ; put src
624 put (D.HtmlBlock txt) = do putWord8 5 ; put txt
625 put D.HRule = putWord8 6
626 get = do i <- getWord8
627 case i of
628 0 -> fmap D.Para get
629 1 -> liftM2 D.Header get get
630 2 -> fmap D.Blockquote get
631 3 -> liftM3 D.List get get get
632 4 -> liftM3 D.CodeBlock get get get
633 5 -> liftM D.HtmlBlock get
634 6 -> return D.HRule
635 _ -> error "Corrupted binary data for Block"
637instance Binary a => Binary (D.Inline a) where
638 put (D.Str txt) = do putWord8 0 ; put txt
639 put D.Space = putWord8 1
640 put D.SoftBreak = putWord8 2
641 put D.LineBreak = putWord8 3
642 put (D.Emph xs) = putWord8 4 >> put xs
643 put (D.Strong xs) = putWord8 5 >> put xs
644 put (D.Code xs tm) = putWord8 6 >> put xs >> put tm
645 put (D.Link a b c) = putWord8 7 >> put a >> put b >> put c
646 put (D.Image a b c) = putWord8 8 >> put a >> put b >> put c
647 put (D.Entity a) = putWord8 9 >> put a
648 put (D.RawHtml x) = putWord8 10 >> put x
649 get = do i <- getWord8
650 case i of
651 0 -> liftM D.Str get
652 1 -> return D.Space
653 2 -> return D.SoftBreak
654 3 -> return D.LineBreak
655 4 -> liftM D.Emph get
656 5 -> liftM D.Strong get
657 6 -> liftM2 D.Code get get
658 7 -> liftM3 D.Link get get get
659 8 -> liftM3 D.Image get get get
660 9 -> liftM D.Entity get
661 10 -> liftM D.RawHtml get
662 _ -> error "Corrupted binary data for Inline"
664instance Binary CT.ListType where
665 put (CT.Bullet c) = putWord8 0 >> put c
666 put (CT.Numbered nw i) = putWord8 1 >> put nw >> put i
667 get = do i <- getWord8
668 case i of
669 0 -> liftM CT.Bullet get
670 1 -> liftM2 CT.Numbered get get
671 _ -> error "Corrupted binary data for ListType"
673instance Binary CT.CodeAttr where
674 put (CT.CodeAttr a b) = put a >> put b
675 get = liftM2 CT.CodeAttr get get
677instance Binary CT.NumWrapper where
678 put (CT.PeriodFollowing) = putWord8 0
679 put (CT.ParenFollowing) = putWord8 1
680 get = do i <- getWord8
681 case i of
682 0 -> return CT.PeriodFollowing
683 1 -> return CT.ParenFollowing
684 _ -> error "Corrupted binary data for NumWrapper"
686----- Generated by 'derive'
688instance Binary SizeChange where
689 put x
690 = case x of
691 Smaller -> putWord8 0
692 Same -> putWord8 1
693 Bigger -> putWord8 2
694 Unknown -> putWord8 3
695 get
696 = do i <- getWord8
697 case i of
698 0 -> return Smaller
699 1 -> return Same
700 2 -> return Bigger
701 3 -> return Unknown
702 _ -> error "Corrupted binary data for SizeChange"
704instance Binary CGInfo where
705 put (CGInfo x1 x2 x3 x4 x5)
706 = do put x1
707 put x2
708-- put x3 -- Already used SCG info for totality check
709 put x4
710 put x5
711 get
712 = do x1 <- get
713 x2 <- get
714 x4 <- get
715 x5 <- get
716 return (CGInfo x1 x2 [] x4 x5)
718instance Binary CaseType where
719 put x = case x of
720 Updatable -> putWord8 0
721 Shared -> putWord8 1
722 get = do i <- getWord8
723 case i of
724 0 -> return Updatable
725 1 -> return Shared
726 _ -> error "Corrupted binary data for CaseType"
728instance Binary SC where
729 put x
730 = case x of
731 Case x1 x2 x3 -> do putWord8 0
732 put x1
733 put x2
734 put x3
735 ProjCase x1 x2 -> do putWord8 1
736 put x1
737 put x2
738 STerm x1 -> do putWord8 2
739 put x1
740 UnmatchedCase x1 -> do putWord8 3
741 put x1
742 ImpossibleCase -> do putWord8 4
743 get
744 = do i <- getWord8
745 case i of
746 0 -> do x1 <- get
747 x2 <- get
748 x3 <- get
749 return (Case x1 x2 x3)
750 1 -> do x1 <- get
751 x2 <- get
752 return (ProjCase x1 x2)
753 2 -> do x1 <- get
754 return (STerm x1)
755 3 -> do x1 <- get
756 return (UnmatchedCase x1)
757 4 -> return ImpossibleCase
758 _ -> error "Corrupted binary data for SC"
761instance Binary CaseAlt where
762 put x
763 = {-# SCC "putCaseAlt" #-}
764 case x of
765 ConCase x1 x2 x3 x4 -> do putWord8 0
766 put x1
767 put x2
768 put x3
769 put x4
770 ConstCase x1 x2 -> do putWord8 1
771 put x1
772 put x2
773 DefaultCase x1 -> do putWord8 2
774 put x1
775 FnCase x1 x2 x3 -> do putWord8 3
776 put x1
777 put x2
778 put x3
779 SucCase x1 x2 -> do putWord8 4
780 put x1
781 put x2
782 get
783 = do i <- getWord8
784 case i of
785 0 -> do x1 <- get
786 x2 <- get
787 x3 <- get
788 x4 <- get
789 return (ConCase x1 x2 x3 x4)
790 1 -> do x1 <- get
791 x2 <- get
792 return (ConstCase x1 x2)
793 2 -> do x1 <- get
794 return (DefaultCase x1)
795 3 -> do x1 <- get
796 x2 <- get
797 x3 <- get
798 return (FnCase x1 x2 x3)
799 4 -> do x1 <- get
800 x2 <- get
801 return (SucCase x1 x2)
802 _ -> error "Corrupted binary data for CaseAlt"
804instance Binary CaseDefs where
805 put (CaseDefs x1 x2 x3 x4)
806 = do -- don't need totality checked or inlined versions
807 put x2
808 put x4
809 get
810 = do x2 <- get
811 x4 <- get
812 return (CaseDefs x2 x2 x2 x4)
814instance Binary CaseInfo where
815 put x@(CaseInfo x1 x2 x3) = do put x1
816 put x2
817 put x3
818 get = do x1 <- get
819 x2 <- get
820 x3 <- get
821 return (CaseInfo x1 x2 x3)
823instance Binary Def where
824 put x
825 = {-# SCC "putDef" #-}
826 case x of
827 Function x1 x2 -> do putWord8 0
828 put x1
829 put x2
830 TyDecl x1 x2 -> do putWord8 1
831 put x1
832 put x2
833 -- all primitives just get added at the start, don't write
834 Operator x1 x2 x3 -> do return ()
835 CaseOp x1 x2 x2a x3 x3a x4 -> do putWord8 3
836 put x1
837 put x2
838 put x2a
839 put x3
840 -- no x3a
841 put x4
842 get
843 = do i <- getWord8
844 case i of
845 0 -> do x1 <- get
846 x2 <- get
847 return (Function x1 x2)
848 1 -> do x1 <- get
849 x2 <- get
850 return (TyDecl x1 x2)
851 -- Operator isn't written, don't read
852 3 -> do x1 <- get
853 x2 <- get
854 x3 <- get
855 x4 <- get
856 -- x3 <- get always []
857 x5 <- get
858 return (CaseOp x1 x2 x3 x4 [] x5)
859 _ -> error "Corrupted binary data for Def"
861instance Binary Accessibility where
862 put x
863 = case x of
864 Public -> putWord8 0
865 Frozen -> putWord8 1
866 Hidden -> putWord8 2
867 get
868 = do i <- getWord8
869 case i of
870 0 -> return Public
871 1 -> return Frozen
872 2 -> return Hidden
873 _ -> error "Corrupted binary data for Accessibility"
875safeToEnum :: (Enum a, Bounded a, Integral int) => String -> int -> a
876safeToEnum label x' = result
877 where
878 x = fromIntegral x'
879 result
880 | x < fromEnum (minBound `asTypeOf` result)
881 || x > fromEnum (maxBound `asTypeOf` result)
882 = error $ label ++ ": corrupted binary representation in IBC"
883 | otherwise = toEnum x
885instance Binary PReason where
886 put x
887 = case x of
888 Other x1 -> do putWord8 0
889 put x1
890 Itself -> putWord8 1
891 NotCovering -> putWord8 2
892 NotPositive -> putWord8 3
893 Mutual x1 -> do putWord8 4
894 put x1
895 NotProductive -> putWord8 5
896 BelieveMe -> putWord8 6
897 UseUndef x1 -> do putWord8 7
898 put x1
899 ExternalIO -> putWord8 8
900 get
901 = do i <- getWord8
902 case i of
903 0 -> do x1 <- get
904 return (Other x1)
905 1 -> return Itself
906 2 -> return NotCovering
907 3 -> return NotPositive
908 4 -> do x1 <- get
909 return (Mutual x1)
910 5 -> return NotProductive
911 6 -> return BelieveMe
912 7 -> do x1 <- get
913 return (UseUndef x1)
914 8 -> return ExternalIO
915 _ -> error "Corrupted binary data for PReason"
917instance Binary Totality where
918 put x
919 = case x of
920 Total x1 -> do putWord8 0
921 put x1
922 Partial x1 -> do putWord8 1
923 put x1
924 Unchecked -> do putWord8 2
925 Productive -> do putWord8 3
926 get
927 = do i <- getWord8
928 case i of
929 0 -> do x1 <- get
930 return (Total x1)
931 1 -> do x1 <- get
932 return (Partial x1)
933 2 -> return Unchecked
934 3 -> return Productive
935 _ -> error "Corrupted binary data for Totality"
937instance Binary MetaInformation where
938 put x
939 = case x of
940 EmptyMI -> do putWord8 0
941 DataMI x1 -> do putWord8 1
942 put x1
943 get = do i <- getWord8
944 case i of
945 0 -> return EmptyMI
946 1 -> do x1 <- get
947 return (DataMI x1)
948 _ -> error "Corrupted binary data for MetaInformation"
950instance Binary IBCFile where
951 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 x44 x45)
952 = {-# SCC "putIBCFile" #-}
953 do put x1
954 put x2
955 put x3
956 put x4
957 put x5
958 put x6
959 put x7
960 put x8
961 put x9
962 put x10
963 put x11
964 put x12
965 put x13
966 put x14
967 put x15
968 put x16
969 put x17
970 put x18
971 put x19
972 put x20
973 put x21
974 put x22
975 put x23
976 put x24
977 put x25
978 put x26
979 put x27
980 put x28
981 put x29
982 put x30
983 put x31
984 put x32
985 put x33
986 put x34
987 put x35
988 put x36
989 put x37
990 put x38
991 put x39
992 put x40
993 put x41
994 put x42
995 put x43
996 put x44
997 put x45
999 get
1000 = do x1 <- get
1001 if x1 == ibcVersion then
1002 do x2 <- get
1003 x3 <- get
1004 x4 <- get
1005 x5 <- get
1006 x6 <- get
1007 x7 <- get
1008 x8 <- get
1009 x9 <- get
1010 x10 <- get
1011 x11 <- get
1012 x12 <- get
1013 x13 <- get
1014 x14 <- get
1015 x15 <- get
1016 x16 <- get
1017 x17 <- get
1018 x18 <- get
1019 x19 <- get
1020 x20 <- get
1021 x21 <- get
1022 x22 <- get
1023 x23 <- get
1024 x24 <- get
1025 x25 <- get
1026 x26 <- get
1027 x27 <- get
1028 x28 <- get
1029 x29 <- get
1030 x30 <- get
1031 x31 <- get
1032 x32 <- get
1033 x33 <- get
1034 x34 <- get
1035 x35 <- get
1036 x36 <- get
1037 x37 <- get
1038 x38 <- get
1039 x39 <- get
1040 x40 <- get
1041 x41 <- get
1042 x42 <- get
1043 x43 <- get
1044 x44 <- get
1045 x45 <- get
1046 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 x44 x45)
1047 else return (initIBC { ver = x1 })
1049instance Binary DataOpt where
1050 put x = case x of
1051 Codata -> putWord8 0
1052 DefaultEliminator -> putWord8 1
1053 DataErrRev -> putWord8 2
1054 DefaultCaseFun -> putWord8 3
1055 get = do i <- getWord8
1056 case i of
1057 0 -> return Codata
1058 1 -> return DefaultEliminator
1059 2 -> return DataErrRev
1060 3 -> return DefaultCaseFun
1061 _ -> error "Corrupted binary data for DataOpt"
1063instance Binary FnOpt where
1064 put x
1065 = case x of
1066 Inlinable -> putWord8 0
1067 TotalFn -> putWord8 1
1068 Dictionary -> putWord8 2
1069 AssertTotal -> putWord8 3
1070 Specialise x -> do putWord8 4
1071 put x
1072 Coinductive -> putWord8 5
1073 PartialFn -> putWord8 6
1074 Implicit -> putWord8 7
1075 Reflection -> putWord8 8
1076 ErrorHandler -> putWord8 9
1077 ErrorReverse -> putWord8 10
1078 CoveringFn -> putWord8 11
1079 NoImplicit -> putWord8 12
1080 Constructor -> putWord8 13
1081 CExport x1 -> do putWord8 14
1082 put x1
1083 AutoHint -> putWord8 15
1084 get
1085 = do i <- getWord8
1086 case i of
1087 0 -> return Inlinable
1088 1 -> return TotalFn
1089 2 -> return Dictionary
1090 3 -> return AssertTotal
1091 4 -> do x <- get
1092 return (Specialise x)
1093 5 -> return Coinductive
1094 6 -> return PartialFn
1095 7 -> return Implicit
1096 8 -> return Reflection
1097 9 -> return ErrorHandler
1098 10 -> return ErrorReverse
1099 11 -> return CoveringFn
1100 12 -> return NoImplicit
1101 13 -> return Constructor
1102 14 -> do x1 <- get
1103 return $ CExport x1
1104 15 -> return AutoHint
1105 _ -> error "Corrupted binary data for FnOpt"
1107instance Binary Fixity where
1108 put x
1109 = case x of
1110 Infixl x1 -> do putWord8 0
1111 put x1
1112 Infixr x1 -> do putWord8 1
1113 put x1
1114 InfixN x1 -> do putWord8 2
1115 put x1
1116 PrefixN x1 -> do putWord8 3
1117 put x1
1118 get
1119 = do i <- getWord8
1120 case i of
1121 0 -> do x1 <- get
1122 return (Infixl x1)
1123 1 -> do x1 <- get
1124 return (Infixr x1)
1125 2 -> do x1 <- get
1126 return (InfixN x1)
1127 3 -> do x1 <- get
1128 return (PrefixN x1)
1129 _ -> error "Corrupted binary data for Fixity"
1132instance Binary FixDecl where
1133 put (Fix x1 x2)
1134 = do put x1
1135 put x2
1136 get
1137 = do x1 <- get
1138 x2 <- get
1139 return (Fix x1 x2)
1142instance Binary ArgOpt where
1143 put x
1144 = case x of
1145 HideDisplay -> putWord8 0
1146 InaccessibleArg -> putWord8 1
1147 AlwaysShow -> putWord8 2
1148 get
1149 = do i <- getWord8
1150 case i of
1151 0 -> return HideDisplay
1152 1 -> return InaccessibleArg
1153 2 -> return AlwaysShow
1154 _ -> error "Corrupted binary data for Static"
1156instance Binary Static where
1157 put x
1158 = case x of
1159 Static -> putWord8 0
1160 Dynamic -> putWord8 1
1161 get
1162 = do i <- getWord8
1163 case i of
1164 0 -> return Static
1165 1 -> return Dynamic
1166 _ -> error "Corrupted binary data for Static"
1169instance Binary Plicity where
1170 put x
1171 = case x of
1172 Imp x1 x2 x3 x4 ->
1173 do putWord8 0
1174 put x1
1175 put x2
1176 put x3
1177 put x4
1178 Exp x1 x2 x3 ->
1179 do putWord8 1
1180 put x1
1181 put x2
1182 put x3
1183 Constraint x1 x2 ->
1184 do putWord8 2
1185 put x1
1186 put x2
1187 TacImp x1 x2 x3 ->
1188 do putWord8 3
1189 put x1
1190 put x2
1191 put x3
1192 get
1193 = do i <- getWord8
1194 case i of
1195 0 -> do x1 <- get
1196 x2 <- get
1197 x3 <- get
1198 x4 <- get
1199 return (Imp x1 x2 x3 x4)
1200 1 -> do x1 <- get
1201 x2 <- get
1202 x3 <- get
1203 return (Exp x1 x2 x3)
1204 2 -> do x1 <- get
1205 x2 <- get
1206 return (Constraint x1 x2)
1207 3 -> do x1 <- get
1208 x2 <- get
1209 x3 <- get
1210 return (TacImp x1 x2 x3)
1211 _ -> error "Corrupted binary data for Plicity"
1214instance (Binary t) => Binary (PDecl' t) where
1215 put x
1216 = case x of
1217 PFix x1 x2 x3 -> do putWord8 0
1218 put x1
1219 put x2
1220 put x3
1221 PTy x1 x2 x3 x4 x5 x6 x7
1222 -> do putWord8 1
1223 put x1
1224 put x2
1225 put x3
1226 put x4
1227 put x5
1228 put x6
1229 put x7
1230 PClauses x1 x2 x3 x4 -> do putWord8 2
1231 put x1
1232 put x2
1233 put x3
1234 put x4
1235 PData x1 x2 x3 x4 x5 x6 ->
1236 do putWord8 3
1237 put x1
1238 put x2
1239 put x3
1240 put x4
1241 put x5
1242 put x6
1243 PParams x1 x2 x3 -> do putWord8 4
1244 put x1
1245 put x2
1246 put x3
1247 PNamespace x1 x2 -> do putWord8 5
1248 put x1
1249 put x2
1250 PRecord x1 x2 x3 x4 x5 x6 x7 x8 x9 ->
1251 do putWord8 6
1252 put x1
1253 put x2
1254 put x3
1255 put x4
1256 put x5
1257 put x6
1258 put x7
1259 put x8
1260 put x9
1261 PClass x1 x2 x3 x4 x5 x6 x7 x8 x9
1262 -> do putWord8 7
1263 put x1
1264 put x2
1265 put x3
1266 put x4
1267 put x5
1268 put x6
1269 put x7
1270 put x8
1271 put x9
1272 PInstance x1 x2 x3 x4 x5 x6 x7 x8 x9 x10 ->
1273 do putWord8 8
1274 put x1
1275 put x2
1276 put x3
1277 put x4
1278 put x5
1279 put x6
1280 put x7
1281 put x8
1282 put x9
1283 put x10
1284 PDSL x1 x2 -> do putWord8 9
1285 put x1
1286 put x2
1287 PCAF x1 x2 x3 -> do putWord8 10
1288 put x1
1289 put x2
1290 put x3
1291 PMutual x1 x2 -> do putWord8 11
1292 put x1
1293 put x2
1294 PPostulate x1 x2 x3 x4 x5 x6 x7
1295 -> do putWord8 12
1296 put x1
1297 put x2
1298 put x3
1299 put x4
1300 put x5
1301 put x6
1302 put x7
1303 PSyntax x1 x2 -> do putWord8 13
1304 put x1
1305 put x2
1306 PDirective x1 -> error "Cannot serialize PDirective"
1307 PProvider x1 x2 x3 x4 x5 ->
1308 do putWord8 15
1309 put x1
1310 put x2
1311 put x3
1312 put x4
1313 put x5
1314 PTransform x1 x2 x3 x4 -> do putWord8 16
1315 put x1
1316 put x2
1317 put x3
1318 put x4
1319 get
1320 = do i <- getWord8
1321 case i of
1322 0 -> do x1 <- get
1323 x2 <- get
1324 x3 <- get
1325 return (PFix x1 x2 x3)
1326 1 -> do x1 <- get
1327 x2 <- get
1328 x3 <- get
1329 x4 <- get
1330 x5 <- get
1331 x6 <- get
1332 x7 <- get
1333 return (PTy x1 x2 x3 x4 x5 x6 x7)
1334 2 -> do x1 <- get
1335 x2 <- get
1336 x3 <- get
1337 x4 <- get
1338 return (PClauses x1 x2 x3 x4)
1339 3 -> do x1 <- get
1340 x2 <- get
1341 x3 <- get
1342 x4 <- get
1343 x5 <- get
1344 x6 <- get
1345 return (PData x1 x2 x3 x4 x5 x6)
1346 4 -> do x1 <- get
1347 x2 <- get
1348 x3 <- get
1349 return (PParams x1 x2 x3)
1350 5 -> do x1 <- get
1351 x2 <- get
1352 return (PNamespace x1 x2)
1353 6 -> do x1 <- get
1354 x2 <- get
1355 x3 <- get
1356 x4 <- get
1357 x5 <- get
1358 x6 <- get
1359 x7 <- get
1360 x8 <- get
1361 x9 <- get
1362 return (PRecord x1 x2 x3 x4 x5 x6 x7 x8 x9)
1363 7 -> do x1 <- get
1364 x2 <- get
1365 x3 <- get
1366 x4 <- get
1367 x5 <- get
1368 x6 <- get
1369 x7 <- get
1370 x8 <- get
1371 x9 <- get
1372 return (PClass x1 x2 x3 x4 x5 x6 x7 x8 x9)
1373 8 -> do x1 <- get
1374 x2 <- get
1375 x3 <- get
1376 x4 <- get
1377 x5 <- get
1378 x6 <- get
1379 x7 <- get
1380 x8 <- get
1381 x9 <- get
1382 x10 <- get
1383 return (PInstance x1 x2 x3 x4 x5 x6 x7 x8 x9 x10)
1384 9 -> do x1 <- get
1385 x2 <- get
1386 return (PDSL x1 x2)
1387 10 -> do x1 <- get
1388 x2 <- get
1389 x3 <- get
1390 return (PCAF x1 x2 x3)
1391 11 -> do x1 <- get
1392 x2 <- get
1393 return (PMutual x1 x2)
1394 12 -> do x1 <- get
1395 x2 <- get
1396 x3 <- get
1397 x4 <- get
1398 x5 <- get
1399 x6 <- get
1400 x7 <- get
1401 return (PPostulate x1 x2 x3 x4 x5 x6 x7)
1402 13 -> do x1 <- get
1403 x2 <- get
1404 return (PSyntax x1 x2)
1405 14 -> do error "Cannot deserialize PDirective"
1406 15 -> do x1 <- get
1407 x2 <- get
1408 x3 <- get
1409 x4 <- get
1410 x5 <- get
1411 return (PProvider x1 x2 x3 x4 x5)
1412 16 -> do x1 <- get
1413 x2 <- get
1414 x3 <- get
1415 x4 <- get
1416 return (PTransform x1 x2 x3 x4)
1417 _ -> error "Corrupted binary data for PDecl'"
1419instance Binary t => Binary (ProvideWhat' t) where
1420 put (ProvTerm x1 x2) = do putWord8 0
1421 put x1
1422 put x2
1423 put (ProvPostulate x1) = do putWord8 1
1424 put x1
1425 get = do y <- getWord8
1426 case y of
1427 0 -> do x1 <- get
1428 x2 <- get
1429 return (ProvTerm x1 x2)
1430 1 -> do x1 <- get
1431 return (ProvPostulate x1)
1432 _ -> error "Corrupted binary data for ProvideWhat"
1434instance Binary Using where
1435 put (UImplicit x1 x2) = do putWord8 0; put x1; put x2
1436 put (UConstraint x1 x2) = do putWord8 1; put x1; put x2
1438 get = do i <- getWord8
1439 case i of
1440 0 -> do x1 <- get; x2 <- get; return (UImplicit x1 x2)
1441 1 -> do x1 <- get; x2 <- get; return (UConstraint x1 x2)
1442 _ -> error "Corrupted binary data for Using"
1444instance Binary SyntaxInfo where
1445 put (Syn x1 x2 x3 x4 _ _ x5 x6 _ _ x7 _)
1446 = do put x1
1447 put x2
1448 put x3
1449 put x4
1450 put x5
1451 put x6
1452 put x7
1453 get
1454 = do x1 <- get
1455 x2 <- get
1456 x3 <- get
1457 x4 <- get
1458 x5 <- get
1459 x6 <- get
1460 x7 <- get
1461 return (Syn x1 x2 x3 x4 [] id x5 x6 Nothing 0 x7 0)
1463instance (Binary t) => Binary (PClause' t) where
1464 put x
1465 = case x of
1466 PClause x1 x2 x3 x4 x5 x6 -> do putWord8 0
1467 put x1
1468 put x2
1469 put x3
1470 put x4
1471 put x5
1472 put x6
1473 PWith x1 x2 x3 x4 x5 x6 x7 -> do putWord8 1
1474 put x1
1475 put x2
1476 put x3
1477 put x4
1478 put x5
1479 put x6
1480 put x7
1481 PClauseR x1 x2 x3 x4 -> do putWord8 2
1482 put x1
1483 put x2
1484 put x3
1485 put x4
1486 PWithR x1 x2 x3 x4 x5 -> do putWord8 3
1487 put x1
1488 put x2
1489 put x3
1490 put x4
1491 put x5
1492 get
1493 = do i <- getWord8
1494 case i of
1495 0 -> do x1 <- get
1496 x2 <- get
1497 x3 <- get
1498 x4 <- get
1499 x5 <- get
1500 x6 <- get
1501 return (PClause x1 x2 x3 x4 x5 x6)
1502 1 -> do x1 <- get
1503 x2 <- get
1504 x3 <- get
1505 x4 <- get
1506 x5 <- get
1507 x6 <- get
1508 x7 <- get
1509 return (PWith x1 x2 x3 x4 x5 x6 x7)
1510 2 -> do x1 <- get
1511 x2 <- get
1512 x3 <- get
1513 x4 <- get
1514 return (PClauseR x1 x2 x3 x4)
1515 3 -> do x1 <- get
1516 x2 <- get
1517 x3 <- get
1518 x4 <- get
1519 x5 <- get
1520 return (PWithR x1 x2 x3 x4 x5)
1521 _ -> error "Corrupted binary data for PClause'"
1523instance (Binary t) => Binary (PData' t) where
1524 put x
1525 = case x of
1526 PDatadecl x1 x2 x3 -> do putWord8 0
1527 put x1
1528 put x2
1529 put x3
1530 PLaterdecl x1 x2 -> do putWord8 1
1531 put x1
1532 put x2
1533 get
1534 = do i <- getWord8
1535 case i of
1536 0 -> do x1 <- get
1537 x2 <- get
1538 x3 <- get
1539 return (PDatadecl x1 x2 x3)
1540 1 -> do x1 <- get
1541 x2 <- get
1542 return (PLaterdecl x1 x2)
1543 _ -> error "Corrupted binary data for PData'"
1545instance Binary PunInfo where
1546 put x
1547 = case x of
1548 TypeOrTerm -> putWord8 0
1549 IsType -> putWord8 1
1550 IsTerm -> putWord8 2
1551 get
1552 = do i <- getWord8
1553 case i of
1554 0 -> return TypeOrTerm
1555 1 -> return IsType
1556 2 -> return IsTerm
1557 _ -> error "Corrupted binary data for PunInfo"
1559instance Binary PTerm where
1560 put x
1561 = case x of
1562 PQuote x1 -> do putWord8 0
1563 put x1
1564 PRef x1 x2 -> do putWord8 1
1565 put x1
1566 put x2
1567 PInferRef x1 x2 -> do putWord8 2
1568 put x1
1569 put x2
1570 PPatvar x1 x2 -> do putWord8 3
1571 put x1
1572 put x2
1573 PLam x1 x2 x3 x4 -> do putWord8 4
1574 put x1
1575 put x2
1576 put x3
1577 put x4
1578 PPi x1 x2 x3 x4 -> do putWord8 5
1579 put x1
1580 put x2
1581 put x3
1582 put x4
1583 PLet x1 x2 x3 x4 x5 -> do putWord8 6
1584 put x1
1585 put x2
1586 put x3
1587 put x4
1588 put x5
1589 PTyped x1 x2 -> do putWord8 7
1590 put x1
1591 put x2
1592 PAppImpl x1 x2 -> error "PAppImpl in final term"
1593 PApp x1 x2 x3 -> do putWord8 8
1594 put x1
1595 put x2
1596 put x3
1597 PAppBind x1 x2 x3 -> do putWord8 9
1598 put x1
1599 put x2
1600 put x3
1601 PMatchApp x1 x2 -> do putWord8 10
1602 put x1
1603 put x2
1604 PCase x1 x2 x3 -> do putWord8 11
1605 put x1
1606 put x2
1607 put x3
1608 PTrue x1 x2 -> do putWord8 12
1609 put x1
1610 put x2
1611 PRefl x1 x2 -> do putWord8 14
1612 put x1
1613 put x2
1614 PResolveTC x1 -> do putWord8 15
1615 put x1
1616 PEq x1 x2 x3 x4 x5 -> do putWord8 16
1617 put x1
1618 put x2
1619 put x3
1620 put x4
1621 put x5
1622 PRewrite x1 x2 x3 x4 -> do putWord8 17
1623 put x1
1624 put x2
1625 put x3
1626 put x4
1627 PPair x1 x2 x3 x4 -> do putWord8 18
1628 put x1
1629 put x2
1630 put x3
1631 put x4
1632 PDPair x1 x2 x3 x4 x5 -> do putWord8 19
1633 put x1
1634 put x2
1635 put x3
1636 put x4
1637 put x5
1638 PAlternative x1 x2 -> do putWord8 20
1639 put x1
1640 put x2
1641 PHidden x1 -> do putWord8 21
1642 put x1
1643 PType -> putWord8 22
1644 PGoal x1 x2 x3 x4 -> do putWord8 23
1645 put x1
1646 put x2
1647 put x3
1648 put x4
1649 PConstant x1 -> do putWord8 24
1650 put x1
1651 Placeholder -> putWord8 25
1652 PDoBlock x1 -> do putWord8 26
1653 put x1
1654 PIdiom x1 x2 -> do putWord8 27
1655 put x1
1656 put x2
1657 PReturn x1 -> do putWord8 28
1658 put x1
1659 PMetavar x1 -> do putWord8 29
1660 put x1
1661 PProof x1 -> do putWord8 30
1662 put x1
1663 PTactics x1 -> do putWord8 31
1664 put x1
1665 PImpossible -> putWord8 33
1666 PCoerced x1 -> do putWord8 34
1667 put x1
1668 PUnifyLog x1 -> do putWord8 35
1669 put x1
1670 PNoImplicits x1 -> do putWord8 36
1671 put x1
1672 PDisamb x1 x2 -> do putWord8 37
1673 put x1
1674 put x2
1675 PUniverse x1 -> do putWord8 38
1676 put x1
1677 PRunTactics x1 x2 -> do putWord8 39
1678 put x1
1679 put x2
1680 PAs x1 x2 x3 -> do putWord8 40
1681 put x1
1682 put x2
1683 put x3
1684 PElabError x1 -> do putWord8 41
1685 put x1
1686 PQuasiquote x1 x2 -> do putWord8 42
1687 put x1
1688 put x2
1689 PUnquote x1 -> do putWord8 43
1690 put x1
1693 get
1694 = do i <- getWord8
1695 case i of
1696 0 -> do x1 <- get
1697 return (PQuote x1)
1698 1 -> do x1 <- get
1699 x2 <- get
1700 return (PRef x1 x2)
1701 2 -> do x1 <- get
1702 x2 <- get
1703 return (PInferRef x1 x2)
1704 3 -> do x1 <- get
1705 x2 <- get
1706 return (PPatvar x1 x2)
1707 4 -> do x1 <- get
1708 x2 <- get
1709 x3 <- get
1710 x4 <- get
1711 return (PLam x1 x2 x3 x4)
1712 5 -> do x1 <- get
1713 x2 <- get
1714 x3 <- get
1715 x4 <- get
1716 return (PPi x1 x2 x3 x4)
1717 6 -> do x1 <- get
1718 x2 <- get
1719 x3 <- get
1720 x4 <- get
1721 x5 <- get
1722 return (PLet x1 x2 x3 x4 x5)
1723 7 -> do x1 <- get
1724 x2 <- get
1725 return (PTyped x1 x2)
1726 8 -> do x1 <- get
1727 x2 <- get
1728 x3 <- get
1729 return (PApp x1 x2 x3)
1730 9 -> do x1 <- get
1731 x2 <- get
1732 x3 <- get
1733 return (PAppBind x1 x2 x3)
1734 10 -> do x1 <- get
1735 x2 <- get
1736 return (PMatchApp x1 x2)
1737 11 -> do x1 <- get
1738 x2 <- get
1739 x3 <- get
1740 return (PCase x1 x2 x3)
1741 12 -> do x1 <- get
1742 x2 <- get
1743 return (PTrue x1 x2)
1744 14 -> do x1 <- get
1745 x2 <- get
1746 return (PRefl x1 x2)
1747 15 -> do x1 <- get
1748 return (PResolveTC x1)
1749 16 -> do x1 <- get
1750 x2 <- get
1751 x3 <- get
1752 x4 <- get
1753 x5 <- get
1754 return (PEq x1 x2 x3 x4 x5)
1755 17 -> do x1 <- get
1756 x2 <- get
1757 x3 <- get
1758 x4 <- get
1759 return (PRewrite x1 x2 x3 x4)
1760 18 -> do x1 <- get
1761 x2 <- get
1762 x3 <- get
1763 x4 <- get
1764 return (PPair x1 x2 x3 x4)
1765 19 -> do x1 <- get
1766 x2 <- get
1767 x3 <- get
1768 x4 <- get
1769 x5 <- get
1770 return (PDPair x1 x2 x3 x4 x5)
1771 20 -> do x1 <- get
1772 x2 <- get
1773 return (PAlternative x1 x2)
1774 21 -> do x1 <- get
1775 return (PHidden x1)
1776 22 -> return PType
1777 23 -> do x1 <- get
1778 x2 <- get
1779 x3 <- get
1780 x4 <- get
1781 return (PGoal x1 x2 x3 x4)
1782 24 -> do x1 <- get
1783 return (PConstant x1)
1784 25 -> return Placeholder
1785 26 -> do x1 <- get
1786 return (PDoBlock x1)
1787 27 -> do x1 <- get
1788 x2 <- get
1789 return (PIdiom x1 x2)
1790 28 -> do x1 <- get
1791 return (PReturn x1)
1792 29 -> do x1 <- get
1793 return (PMetavar x1)
1794 30 -> do x1 <- get
1795 return (PProof x1)
1796 31 -> do x1 <- get
1797 return (PTactics x1)
1798 33 -> return PImpossible
1799 34 -> do x1 <- get
1800 return (PCoerced x1)
1801 35 -> do x1 <- get
1802 return (PUnifyLog x1)
1803 36 -> do x1 <- get
1804 return (PNoImplicits x1)
1805 37 -> do x1 <- get
1806 x2 <- get
1807 return (PDisamb x1 x2)
1808 38 -> do x1 <- get
1809 return (PUniverse x1)
1810 39 -> do x1 <- get
1811 x2 <- get
1812 return (PRunTactics x1 x2)
1813 40 -> do x1 <- get
1814 x2 <- get
1815 x3 <- get
1816 return (PAs x1 x2 x3)
1817 41 -> do x1 <- get
1818 return (PElabError x1)
1819 42 -> do x1 <- get
1820 x2 <- get
1821 return (PQuasiquote x1 x2)
1822 43 -> do x1 <- get
1823 return (PUnquote x1)
1824 _ -> error "Corrupted binary data for PTerm"
1826instance (Binary t) => Binary (PTactic' t) where
1827 put x
1828 = case x of
1829 Intro x1 -> do putWord8 0
1830 put x1
1831 Focus x1 -> do putWord8 1
1832 put x1
1833 Refine x1 x2 -> do putWord8 2
1834 put x1
1835 put x2
1836 Rewrite x1 -> do putWord8 3
1837 put x1
1838 LetTac x1 x2 -> do putWord8 4
1839 put x1
1840 put x2
1841 Exact x1 -> do putWord8 5
1842 put x1
1843 Compute -> putWord8 6
1844 Trivial -> putWord8 7
1845 Solve -> putWord8 8
1846 Attack -> putWord8 9
1847 ProofState -> putWord8 10
1848 ProofTerm -> putWord8 11
1849 Undo -> putWord8 12
1850 Try x1 x2 -> do putWord8 13
1851 put x1
1852 put x2
1853 TSeq x1 x2 -> do putWord8 14
1854 put x1
1855 put x2
1856 Qed -> putWord8 15
1857 ApplyTactic x1 -> do putWord8 16
1858 put x1
1859 Reflect x1 -> do putWord8 17
1860 put x1
1861 Fill x1 -> do putWord8 18
1862 put x1
1863 Induction x1 -> do putWord8 19
1864 put x1
1865 ByReflection x1 -> do putWord8 20
1866 put x1
1867 ProofSearch x1 x2 x3 x4 x5 -> do putWord8 21
1868 put x1
1869 put x2
1870 put x3
1871 put x4
1872 put x5
1873 DoUnify -> putWord8 22
1874 CaseTac x1 -> do putWord8 23
1875 put x1
1876 SourceFC -> putWord8 24
1877 Intros -> putWord8 25
1878 Equiv x1 -> do putWord8 26
1879 put x1
1880 Claim x1 x2 -> do putWord8 27
1881 put x1
1882 put x2
1883 Unfocus -> putWord8 28
1884 MatchRefine x1 -> do putWord8 29
1885 put x1
1886 LetTacTy x1 x2 x3 -> do putWord8 30
1887 put x1
1888 put x2
1889 put x3
1890 TCInstance -> putWord8 31
1891 GoalType x1 x2 -> do putWord8 32
1892 put x1
1893 put x2
1894 TCheck x1 -> do putWord8 33
1895 put x1
1896 TEval x1 -> do putWord8 34
1897 put x1
1898 TDocStr x1 -> do putWord8 35
1899 put x1
1900 TSearch x1 -> do putWord8 36
1901 put x1
1902 Skip -> putWord8 37
1903 TFail x1 -> do putWord8 38
1904 put x1
1905 Abandon -> putWord8 39
1906 get
1907 = do i <- getWord8
1908 case i of
1909 0 -> do x1 <- get
1910 return (Intro x1)
1911 1 -> do x1 <- get
1912 return (Focus x1)
1913 2 -> do x1 <- get
1914 x2 <- get
1915 return (Refine x1 x2)
1916 3 -> do x1 <- get
1917 return (Rewrite x1)
1918 4 -> do x1 <- get
1919 x2 <- get
1920 return (LetTac x1 x2)
1921 5 -> do x1 <- get
1922 return (Exact x1)
1923 6 -> return Compute
1924 7 -> return Trivial
1925 8 -> return Solve
1926 9 -> return Attack
1927 10 -> return ProofState
1928 11 -> return ProofTerm
1929 12 -> return Undo
1930 13 -> do x1 <- get
1931 x2 <- get
1932 return (Try x1 x2)
1933 14 -> do x1 <- get
1934 x2 <- get
1935 return (TSeq x1 x2)
1936 15 -> return Qed
1937 16 -> do x1 <- get
1938 return (ApplyTactic x1)
1939 17 -> do x1 <- get
1940 return (Reflect x1)
1941 18 -> do x1 <- get
1942 return (Fill x1)
1943 19 -> do x1 <- get
1944 return (Induction x1)
1945 20 -> do x1 <- get
1946 return (ByReflection x1)
1947 21 -> do x1 <- get
1948 x2 <- get
1949 x3 <- get
1950 x4 <- get
1951 x5 <- get
1952 return (ProofSearch x1 x2 x3 x4 x5)
1953 22 -> return DoUnify
1954 23 -> do x1 <- get
1955 return (CaseTac x1)
1956 24 -> return SourceFC
1957 25 -> return Intros
1958 26 -> do x1 <- get
1959 return (Equiv x1)
1960 27 -> do x1 <- get
1961 x2 <- get
1962 return (Claim x1 x2)
1963 28 -> return Unfocus
1964 29 -> do x1 <- get
1965 return (MatchRefine x1)
1966 30 -> do x1 <- get
1967 x2 <- get
1968 x3 <- get
1969 return (LetTacTy x1 x2 x3)
1970 31 -> return TCInstance
1971 32 -> do x1 <- get
1972 x2 <- get
1973 return (GoalType x1 x2)
1974 33 -> do x1 <- get
1975 return (TCheck x1)
1976 34 -> do x1 <- get
1977 return (TEval x1)
1978 35 -> do x1 <- get
1979 return (TDocStr x1)
1980 36 -> do x1 <- get
1981 return (TSearch x1)
1982 37 -> return Skip
1983 38 -> do x1 <- get
1984 return (TFail x1)
1985 39 -> return Abandon
1986 _ -> error "Corrupted binary data for PTactic'"
1989instance (Binary t) => Binary (PDo' t) where
1990 put x
1991 = case x of
1992 DoExp x1 x2 -> do putWord8 0
1993 put x1
1994 put x2
1995 DoBind x1 x2 x3 -> do putWord8 1
1996 put x1
1997 put x2
1998 put x3
1999 DoBindP x1 x2 x3 x4 -> do putWord8 2
2000 put x1
2001 put x2
2002 put x3
2003 put x4
2004 DoLet x1 x2 x3 x4 -> do putWord8 3
2005 put x1
2006 put x2
2007 put x3
2008 put x4
2009 DoLetP x1 x2 x3 -> do putWord8 4
2010 put x1
2011 put x2
2012 put x3
2013 get
2014 = do i <- getWord8
2015 case i of
2016 0 -> do x1 <- get
2017 x2 <- get
2018 return (DoExp x1 x2)
2019 1 -> do x1 <- get
2020 x2 <- get
2021 x3 <- get
2022 return (DoBind x1 x2 x3)
2023 2 -> do x1 <- get
2024 x2 <- get
2025 x3 <- get
2026 x4 <- get
2027 return (DoBindP x1 x2 x3 x4)
2028 3 -> do x1 <- get
2029 x2 <- get
2030 x3 <- get
2031 x4 <- get
2032 return (DoLet x1 x2 x3 x4)
2033 4 -> do x1 <- get
2034 x2 <- get
2035 x3 <- get
2036 return (DoLetP x1 x2 x3)
2037 _ -> error "Corrupted binary data for PDo'"
2040instance (Binary t) => Binary (PArg' t) where
2041 put x
2042 = case x of
2043 PImp x1 x2 x3 x4 x5 ->
2044 do putWord8 0
2045 put x1
2046 put x2
2047 put x3
2048 put x4
2049 put x5
2050 PExp x1 x2 x3 x4 ->
2051 do putWord8 1
2052 put x1
2053 put x2
2054 put x3
2055 put x4
2056 PConstraint x1 x2 x3 x4 ->
2057 do putWord8 2
2058 put x1
2059 put x2
2060 put x3
2061 put x4
2062 PTacImplicit x1 x2 x3 x4 x5 ->
2063 do putWord8 3
2064 put x1
2065 put x2
2066 put x3
2067 put x4
2068 put x5
2069 get
2070 = do i <- getWord8
2071 case i of
2072 0 -> do x1 <- get
2073 x2 <- get
2074 x3 <- get
2075 x4 <- get
2076 x5 <- get
2077 return (PImp x1 x2 x3 x4 x5)
2078 1 -> do x1 <- get
2079 x2 <- get
2080 x3 <- get
2081 x4 <- get
2082 return (PExp x1 x2 x3 x4)
2083 2 -> do x1 <- get
2084 x2 <- get
2085 x3 <- get
2086 x4 <- get
2087 return (PConstraint x1 x2 x3 x4)
2088 3 -> do x1 <- get
2089 x2 <- get
2090 x3 <- get
2091 x4 <- get
2092 x5 <- get
2093 return (PTacImplicit x1 x2 x3 x4 x5)
2094 _ -> error "Corrupted binary data for PArg'"
2097instance Binary ClassInfo where
2098 put (CI x1 x2 x3 x4 x5 _ x6)
2099 = do put x1
2100 put x2
2101 put x3
2102 put x4
2103 put x5
2104 put x6
2105 get
2106 = do x1 <- get
2107 x2 <- get
2108 x3 <- get
2109 x4 <- get
2110 x5 <- get
2111 x6 <- get
2112 return (CI x1 x2 x3 x4 x5 [] x6)
2114instance Binary OptInfo where
2115 put (Optimise x1 x2)
2116 = do put x1
2117 put x2
2118 get
2119 = do x1 <- get
2120 x2 <- get
2121 return (Optimise x1 x2)
2123instance Binary FnInfo where
2124 put (FnInfo x1)
2125 = put x1
2126 get
2127 = do x1 <- get
2128 return (FnInfo x1)
2130instance Binary TypeInfo where
2131 put (TI x1 x2 x3 x4 x5) = do put x1
2132 put x2
2133 put x3
2134 put x4
2135 put x5
2136 get = do x1 <- get
2137 x2 <- get
2138 x3 <- get
2139 x4 <- get
2140 x5 <- get
2141 return (TI x1 x2 x3 x4 x5)
2143instance Binary SynContext where
2144 put x
2145 = case x of
2146 PatternSyntax -> putWord8 0
2147 TermSyntax -> putWord8 1
2148 AnySyntax -> putWord8 2
2149 get
2150 = do i <- getWord8
2151 case i of
2152 0 -> return PatternSyntax
2153 1 -> return TermSyntax
2154 2 -> return AnySyntax
2155 _ -> error "Corrupted binary data for SynContext"
2158instance Binary Syntax where
2159 put (Rule x1 x2 x3)
2160 = do put x1
2161 put x2
2162 put x3
2163 get
2164 = do x1 <- get
2165 x2 <- get
2166 x3 <- get
2167 return (Rule x1 x2 x3)
2169instance (Binary t) => Binary (DSL' t) where
2170 put (DSL x1 x2 x3 x4 x5 x6 x7 x8 x9 x10)
2171 = do put x1
2172 put x2
2173 put x3
2174 put x4
2175 put x5
2176 put x6
2177 put x7
2178 put x8
2179 put x9
2180 put x10
2181 get
2182 = do x1 <- get
2183 x2 <- get
2184 x3 <- get
2185 x4 <- get
2186 x5 <- get
2187 x6 <- get
2188 x7 <- get
2189 x8 <- get
2190 x9 <- get
2191 x10 <- get
2192 return (DSL x1 x2 x3 x4 x5 x6 x7 x8 x9 x10)
2194instance Binary SSymbol where
2195 put x
2196 = case x of
2197 Keyword x1 -> do putWord8 0
2198 put x1
2199 Symbol x1 -> do putWord8 1
2200 put x1
2201 Expr x1 -> do putWord8 2
2202 put x1
2203 SimpleExpr x1 -> do putWord8 3
2204 put x1
2205 Binding x1 -> do putWord8 4
2206 put x1
2207 get
2208 = do i <- getWord8
2209 case i of
2210 0 -> do x1 <- get
2211 return (Keyword x1)
2212 1 -> do x1 <- get
2213 return (Symbol x1)
2214 2 -> do x1 <- get
2215 return (Expr x1)
2216 3 -> do x1 <- get
2217 return (SimpleExpr x1)
2218 4 -> do x1 <- get
2219 return (Binding x1)
2220 _ -> error "Corrupted binary data for SSymbol"
2222instance Binary Codegen where
2223 put x
2224 = case x of
2225 Via str -> do putWord8 0
2226 put str
2227 Bytecode -> putWord8 1
2228 get
2229 = do i <- getWord8
2230 case i of
2231 0 -> do x1 <- get
2232 return (Via x1)
2233 1 -> return Bytecode
2234 _ -> error "Corrupted binary data for Codegen"