@@ -1,4 +1,4 @@
1−{-# LANGUAGE TypeSynonymInstances, TemplateHaskell #-}
1+{-# LANGUAGE TypeSynonymInstances #-}
22
33module Idris.IBC where
44
@@ -7,17 +7,26 @@ import Core.TT
77import Core.CaseTree
88import Idris.Compiler
99import Idris.AbsSyntax
10+import Idris.Imports
1011
1112import Data.Binary
1213import Data.List
13−import Data.DeriveTH
14+import Data.ByteString.Lazy as B hiding (length, elem)
15+-- import Data.DeriveTH
1416import Control.Monad
17+import Control.Monad.State hiding (get, put)
18+import System.FilePath
19+import System.Posix.Files
20+
21+import Paths_idris
1522
1623ibcVersion :: Word8
17−ibcVersion = 1
24+ibcVersion = 3
1825
1926data IBCFile = IBCFile { ver :: Word8,
27+ sourcefile :: FilePath,
2028 ibc_imports :: [FilePath],
29+ ibc_implicits :: [(Name, [PArg])],
2130 ibc_fixes :: [FixDecl],
2231 ibc_statics :: [(Name, [Bool])],
2332 ibc_classes :: [(Name, ClassInfo)],
@@ -27,59 +36,906 @@ data IBCFile = IBCFile { ver :: Word8,
2736 ibc_libs :: [String],
2837 ibc_hdrs :: [String],
2938 ibc_defs :: [(Name, Def)] }
39+{-!
40+deriving instance Binary IBCFile
41+!-}
3042
3143initIBC :: IBCFile
32−initIBC = IBCFile ibcVersion [] [] [] [] [] [] [] [] [] []
44+initIBC = IBCFile ibcVersion "" [] [] [] [] [] [] [] [] [] [] []
3345
3446loadIBC :: FilePath -> Idris ()
35−loadIBC fp = fail "Not implemented"
47+loadIBC fp = do iLOG $ "Loading ibc " ++ fp
48+ ibcf <- lift $ (decodeFile fp :: IO IBCFile)
49+ process ibcf fp
3650
37−writeIBC :: FilePath -> Idris ()
38−writeIBC f
51+writeIBC :: FilePath -> FilePath -> Idris ()
52+writeIBC src f
3953 = do iLOG $ "Writing ibc " ++ show f
4054 i <- getIState
4155 case idris_metavars i \\ primDefs of
4256 (_:_) -> fail "Can't write ibc when there are unsolve metavariables"
4357 [] -> return ()
58+ ibcf <- mkIBC (ibc_write i) (initIBC { sourcefile = src })
59+ lift $ encodeFile f ibcf
60+ iLOG $ "Written"
4461 return ()
4562
46−$( derive makeBinary ''IBCFile )
47−$( derive makeBinary ''PTerm )
48−$( derive makeBinary ''Raw )
49−$( derive makeBinary ''PTactic' )
50−$( derive makeBinary ''PDo' )
51−$( derive makeBinary ''PArg' )
52−$( derive makeBinary ''ClassInfo )
53−$( derive makeBinary ''Plicity )
54−$( derive makeBinary ''FC )
55−$( derive makeBinary ''Syntax )
56−$( derive makeBinary ''SynContext )
57−$( derive makeBinary ''SSymbol )
58−$( derive makeBinary ''Static )
59−$( derive makeBinary ''Fixity )
60−$( derive makeBinary ''FixDecl )
61−
62−$( derive makeBinary ''Def )
63−$( derive makeBinary ''SC )
64−$( derive makeBinary ''CaseAlt )
65−$( derive makeBinary ''NameType )
66−$( derive makeBinary ''Name )
67−$( derive makeBinary ''Binder )
68−$( derive makeBinary ''TT )
69−$( derive makeBinary ''Const )
70−
71−-- We need this for serialising Def. Fortunately, it never gets used because
72−-- we'll never serialise a primitive operator
73−
74−instance Binary (a -> b) where
75− put x = return ()
76− get = undefined
77−
78−-- We assume that universe levels have been checked, so anything external
79−-- can just have the same universe variable and we won't get any new
80−-- cycles.
81−
82−instance Binary UExp where
83− put x = return ()
84− get = return (UVar (-1))
63+mkIBC :: [IBCWrite] -> IBCFile -> Idris IBCFile
64+mkIBC [] f = return f
65+mkIBC (i:is) f = do ist <- getIState
66+ logLvl 5 $ show i ++ " " ++ show (Data.List.length is)
67+ f' <- ibc ist i f
68+ mkIBC is f'
69+
70+ibc i (IBCFix d) f = return f { ibc_fixes = d : ibc_fixes f }
71+ibc i (IBCImp n) f = case lookupCtxt Nothing n (idris_implicits i) of
72+ [v] -> return f { ibc_implicits = (n,v): ibc_implicits f }
73+ _ -> fail "IBC write failed"
74+ibc i (IBCStatic n) f
75+ = case lookupCtxt Nothing n (idris_statics i) of
76+ [v] -> return f { ibc_statics = (n,v): ibc_statics f }
77+ _ -> fail "IBC write failed"
78+ibc i (IBCClass n) f
79+ = case lookupCtxt Nothing n (idris_classes i) of
80+ [v] -> return f { ibc_classes = (n,v): ibc_classes f }
81+ _ -> fail "IBC write failed"
82+ibc i (IBCSyntax n) f = return f { ibc_syntax = n : ibc_syntax f }
83+ibc i (IBCKeyword n) f = return f { ibc_keywords = n : ibc_keywords f }
84+ibc i (IBCImport n) f = return f { ibc_imports = n : ibc_imports f }
85+ibc i (IBCObj n) f = return f { ibc_objs = n : ibc_objs f }
86+ibc i (IBCLib n) f = return f { ibc_libs = n : ibc_libs f }
87+ibc i (IBCHeader n) f = return f { ibc_hdrs = n : ibc_hdrs f }
88+ibc i (IBCDef n) f = case lookupDef Nothing n (tt_ctxt i) of
89+ [v] -> return f { ibc_defs = (n,v): ibc_defs f }
90+ _ -> fail "IBC write failed"
91+
92+process :: IBCFile -> FilePath -> Idris ()
93+process i fn
94+ | ver i /= ibcVersion = do iLOG "ibc out of date"
95+ fail "Incorrect ibc version"
96+ | otherwise =
97+ do lift $ timestampOlder (sourcefile i) fn
98+ pImports (ibc_imports i)
99+ pImps (ibc_implicits i)
100+ pFixes (ibc_fixes i)
101+ pStatics (ibc_statics i)
102+ pClasses (ibc_classes i)
103+ pSyntax (ibc_syntax i)
104+ pKeywords (ibc_keywords i)
105+ pObjs (ibc_objs i)
106+ pLibs (ibc_libs i)
107+ pHdrs (ibc_hdrs i)
108+ pDefs (ibc_defs i)
109+
110+timestampOlder :: FilePath -> FilePath -> IO ()
111+timestampOlder src ibc = do srcs <- getFileStatus src
112+ ibcs <- getFileStatus ibc
113+ if (modificationTime srcs > modificationTime ibcs)
114+ then fail "Needs reloading"
115+ else return ()
116+
117+pImports :: [FilePath] -> Idris ()
118+pImports fs
119+ = do datadir <- lift $ getDataDir
120+ mapM_ (\f -> do fp <- lift $ findImport [".", datadir] f
121+ i <- getIState
122+ if (f `elem` imported i)
123+ then iLOG $ "Already read " ++ f
124+ else do putIState (i { imported = f : imported i })
125+ case fp of
126+ IDR fn -> do iLOG $ "Failed at " ++ fn
127+ fail "Must be an ibc"
128+ IBC fn src -> loadIBC fn)
129+ fs
130+
131+pImps :: [(Name, [PArg])] -> Idris ()
132+pImps imps = mapM_ (\ (n, imp) ->
133+ do i <- getIState
134+ putIState (i { idris_implicits
135+ = addDef n imp (idris_implicits i) }))
136+ imps
137+
138+pFixes :: [FixDecl] -> Idris ()
139+pFixes f = do i <- getIState
140+ putIState (i { idris_infixes = f ++ idris_infixes i })
141+
142+pStatics :: [(Name, [Bool])] -> Idris ()
143+pStatics ss = mapM_ (\ (n, s) ->
144+ do i <- getIState
145+ putIState (i { idris_statics
146+ = addDef n s (idris_statics i) }))
147+ ss
148+
149+pClasses :: [(Name, ClassInfo)] -> Idris ()
150+pClasses cs = mapM_ (\ (n, c) ->
151+ do i <- getIState
152+ putIState (i { idris_classes
153+ = addDef n c (idris_classes i) }))
154+ cs
155+
156+pSyntax :: [Syntax] -> Idris ()
157+pSyntax s = do i <- getIState
158+ putIState (i { syntax_rules = s ++ syntax_rules i })
159+
160+pKeywords :: [String] -> Idris ()
161+pKeywords k = do i <- getIState
162+ putIState (i { syntax_keywords = k ++ syntax_keywords i })
163+
164+pObjs :: [FilePath] -> Idris ()
165+pObjs os = mapM_ addObjectFile os
166+
167+pLibs :: [String] -> Idris ()
168+pLibs ls = mapM_ addLib ls
169+
170+pHdrs :: [String] -> Idris ()
171+pHdrs hs = mapM_ addHdr hs
172+
173+pDefs :: [(Name, Def)] -> Idris ()
174+pDefs ds = mapM_ (\ (n, d) ->
175+ do i <- getIState
176+ putIState (i { tt_ctxt = addCtxtDef n d (tt_ctxt i) }))
177+ ds
178+
179+
180+----- Generated by 'derive'
181+
182+
183+instance Binary FC where
184+ put (FC x1 x2)
185+ = do put x1
186+ put x2
187+ get
188+ = do x1 <- get
189+ x2 <- get
190+ return (FC x1 x2)
191+
192+
193+instance Binary Name where
194+ put x
195+ = case x of
196+ UN x1 -> do putWord8 0
197+ put x1
198+ NS x1 x2 -> do putWord8 1
199+ put x1
200+ put x2
201+ MN x1 x2 -> do putWord8 2
202+ put x1
203+ put x2
204+ get
205+ = do i <- getWord8
206+ case i of
207+ 0 -> do x1 <- get
208+ return (UN x1)
209+ 1 -> do x1 <- get
210+ x2 <- get
211+ return (NS x1 x2)
212+ 2 -> do x1 <- get
213+ x2 <- get
214+ return (MN x1 x2)
215+ _ -> error "Corrupted binary data for Name"
216+
217+
218+instance Binary Const where
219+ put x
220+ = case x of
221+ I x1 -> do putWord8 0
222+ put x1
223+ BI x1 -> do putWord8 1
224+ put x1
225+ Fl x1 -> do putWord8 2
226+ put x1
227+ Ch x1 -> do putWord8 3
228+ put x1
229+ Str x1 -> do putWord8 4
230+ put x1
231+ IType -> putWord8 5
232+ BIType -> putWord8 6
233+ FlType -> putWord8 7
234+ ChType -> putWord8 8
235+ StrType -> putWord8 9
236+ PtrType -> putWord8 10
237+ get
238+ = do i <- getWord8
239+ case i of
240+ 0 -> do x1 <- get
241+ return (I x1)
242+ 1 -> do x1 <- get
243+ return (BI x1)
244+ 2 -> do x1 <- get
245+ return (Fl x1)
246+ 3 -> do x1 <- get
247+ return (Ch x1)
248+ 4 -> do x1 <- get
249+ return (Str x1)
250+ 5 -> return IType
251+ 6 -> return BIType
252+ 7 -> return FlType
253+ 8 -> return ChType
254+ 9 -> return StrType
255+ 10 -> return PtrType
256+ _ -> error "Corrupted binary data for Const"
257+
258+
259+instance Binary Raw where
260+ put x
261+ = case x of
262+ Var x1 -> do putWord8 0
263+ put x1
264+ RBind x1 x2 x3 -> do putWord8 1
265+ put x1
266+ put x2
267+ put x3
268+ RApp x1 x2 -> do putWord8 2
269+ put x1
270+ put x2
271+ RSet -> putWord8 3
272+ RConstant x1 -> do putWord8 4
273+ put x1
274+ get
275+ = do i <- getWord8
276+ case i of
277+ 0 -> do x1 <- get
278+ return (Var x1)
279+ 1 -> do x1 <- get
280+ x2 <- get
281+ x3 <- get
282+ return (RBind x1 x2 x3)
283+ 2 -> do x1 <- get
284+ x2 <- get
285+ return (RApp x1 x2)
286+ 3 -> return RSet
287+ 4 -> do x1 <- get
288+ return (RConstant x1)
289+ _ -> error "Corrupted binary data for Raw"
290+
291+
292+instance (Binary b) => Binary (Binder b) where
293+ put x
294+ = case x of
295+ Lam x1 -> do putWord8 0
296+ put x1
297+ Pi x1 -> do putWord8 1
298+ put x1
299+ Let x1 x2 -> do putWord8 2
300+ put x1
301+ put x2
302+ NLet x1 x2 -> do putWord8 3
303+ put x1
304+ put x2
305+ Hole x1 -> do putWord8 4
306+ put x1
307+ GHole x1 -> do putWord8 5
308+ put x1
309+ Guess x1 x2 -> do putWord8 6
310+ put x1
311+ put x2
312+ PVar x1 -> do putWord8 7
313+ put x1
314+ PVTy x1 -> do putWord8 8
315+ put x1
316+ get
317+ = do i <- getWord8
318+ case i of
319+ 0 -> do x1 <- get
320+ return (Lam x1)
321+ 1 -> do x1 <- get
322+ return (Pi x1)
323+ 2 -> do x1 <- get
324+ x2 <- get
325+ return (Let x1 x2)
326+ 3 -> do x1 <- get
327+ x2 <- get
328+ return (NLet x1 x2)
329+ 4 -> do x1 <- get
330+ return (Hole x1)
331+ 5 -> do x1 <- get
332+ return (GHole x1)
333+ 6 -> do x1 <- get
334+ x2 <- get
335+ return (Guess x1 x2)
336+ 7 -> do x1 <- get
337+ return (PVar x1)
338+ 8 -> do x1 <- get
339+ return (PVTy x1)
340+ _ -> error "Corrupted binary data for Binder"
341+
342+
343+instance Binary NameType where
344+ put x
345+ = case x of
346+ Bound -> putWord8 0
347+ Ref -> putWord8 1
348+ DCon x1 x2 -> do putWord8 2
349+ put x1
350+ put x2
351+ TCon x1 x2 -> do putWord8 3
352+ put x1
353+ put x2
354+ get
355+ = do i <- getWord8
356+ case i of
357+ 0 -> return Bound
358+ 1 -> return Ref
359+ 2 -> do x1 <- get
360+ x2 <- get
361+ return (DCon x1 x2)
362+ 3 -> do x1 <- get
363+ x2 <- get
364+ return (TCon x1 x2)
365+ _ -> error "Corrupted binary data for NameType"
366+
367+
368+instance (Binary n) => Binary (TT n) where
369+ put x
370+ = case x of
371+ P x1 x2 x3 -> do putWord8 0
372+ put x1
373+ put x2
374+ put x3
375+ V x1 -> do putWord8 1
376+ put x1
377+ Bind x1 x2 x3 -> do putWord8 2
378+ put x1
379+ put x2
380+ put x3
381+ App x1 x2 -> do putWord8 3
382+ put x1
383+ put x2
384+ Constant x1 -> do putWord8 4
385+ put x1
386+ Set x1 -> do putWord8 5
387+ put x1
388+ get
389+ = do i <- getWord8
390+ case i of
391+ 0 -> do x1 <- get
392+ x2 <- get
393+ x3 <- get
394+ return (P x1 x2 x3)
395+ 1 -> do x1 <- get
396+ return (V x1)
397+ 2 -> do x1 <- get
398+ x2 <- get
399+ x3 <- get
400+ return (Bind x1 x2 x3)
401+ 3 -> do x1 <- get
402+ x2 <- get
403+ return (App x1 x2)
404+ 4 -> do x1 <- get
405+ return (Constant x1)
406+ 5 -> do x1 <- get
407+ return (Set x1)
408+ _ -> error "Corrupted binary data for TT"
409+
410+
411+instance Binary SC where
412+ put x
413+ = case x of
414+ Case x1 x2 -> do putWord8 0
415+ put x1
416+ put x2
417+ STerm x1 -> do putWord8 1
418+ put x1
419+ UnmatchedCase x1 -> do putWord8 2
420+ put x1
421+ get
422+ = do i <- getWord8
423+ case i of
424+ 0 -> do x1 <- get
425+ x2 <- get
426+ return (Case x1 x2)
427+ 1 -> do x1 <- get
428+ return (STerm x1)
429+ 2 -> do x1 <- get
430+ return (UnmatchedCase x1)
431+ _ -> error "Corrupted binary data for SC"
432+
433+
434+instance Binary CaseAlt where
435+ put x
436+ = case x of
437+ ConCase x1 x2 x3 x4 -> do putWord8 0
438+ put x1
439+ put x2
440+ put x3
441+ put x4
442+ ConstCase x1 x2 -> do putWord8 1
443+ put x1
444+ put x2
445+ DefaultCase x1 -> do putWord8 2
446+ put x1
447+ get
448+ = do i <- getWord8
449+ case i of
450+ 0 -> do x1 <- get
451+ x2 <- get
452+ x3 <- get
453+ x4 <- get
454+ return (ConCase x1 x2 x3 x4)
455+ 1 -> do x1 <- get
456+ x2 <- get
457+ return (ConstCase x1 x2)
458+ 2 -> do x1 <- get
459+ return (DefaultCase x1)
460+ _ -> error "Corrupted binary data for CaseAlt"
461+
462+
463+instance Binary Def where
464+ put x
465+ = case x of
466+ Function x1 x2 -> do putWord8 0
467+ put x1
468+ put x2
469+ TyDecl x1 x2 -> do putWord8 1
470+ put x1
471+ put x2
472+ Operator x1 x2 x3 -> do putWord8 2
473+ put x1
474+ put x2
475+ put x3
476+ CaseOp x1 x2 x3 x4 x5 -> do putWord8 3
477+ put x1
478+ put x2
479+ put x3
480+ put x4
481+ put x5
482+ get
483+ = do i <- getWord8
484+ case i of
485+ 0 -> do x1 <- get
486+ x2 <- get
487+ return (Function x1 x2)
488+ 1 -> do x1 <- get
489+ x2 <- get
490+ return (TyDecl x1 x2)
491+ 2 -> do x1 <- get
492+ x2 <- get
493+ x3 <- get
494+ return (Operator x1 x2 x3)
495+ 3 -> do x1 <- get
496+ x2 <- get
497+ x3 <- get
498+ x4 <- get
499+ x5 <- get
500+ return (CaseOp x1 x2 x3 x4 x5)
501+ _ -> error "Corrupted binary data for Def"
502+
503+
504+instance Binary IBCFile where
505+ put (IBCFile x1 x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13)
506+ = do put x1
507+ put x2
508+ put x3
509+ put x4
510+ put x5
511+ put x6
512+ put x7
513+ put x8
514+ put x9
515+ put x10
516+ put x11
517+ put x12
518+ put x13
519+ get
520+ = do x1 <- get
521+ if x1 == ibcVersion then
522+ do x2 <- get
523+ x3 <- get
524+ x4 <- get
525+ x5 <- get
526+ x6 <- get
527+ x7 <- get
528+ x8 <- get
529+ x9 <- get
530+ x10 <- get
531+ x11 <- get
532+ x12 <- get
533+ x13 <- get
534+ return (IBCFile x1 x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13)
535+ else return (initIBC { ver = x1 })
536+
537+instance Binary Fixity where
538+ put x
539+ = case x of
540+ Infixl x1 -> do putWord8 0
541+ put x1
542+ Infixr x1 -> do putWord8 1
543+ put x1
544+ InfixN x1 -> do putWord8 2
545+ put x1
546+ PrefixN x1 -> do putWord8 3
547+ put x1
548+ get
549+ = do i <- getWord8
550+ case i of
551+ 0 -> do x1 <- get
552+ return (Infixl x1)
553+ 1 -> do x1 <- get
554+ return (Infixr x1)
555+ 2 -> do x1 <- get
556+ return (InfixN x1)
557+ 3 -> do x1 <- get
558+ return (PrefixN x1)
559+ _ -> error "Corrupted binary data for Fixity"
560+
561+
562+instance Binary FixDecl where
563+ put (Fix x1 x2)
564+ = do put x1
565+ put x2
566+ get
567+ = do x1 <- get
568+ x2 <- get
569+ return (Fix x1 x2)
570+
571+
572+instance Binary Static where
573+ put x
574+ = case x of
575+ Static -> putWord8 0
576+ Dynamic -> putWord8 1
577+ get
578+ = do i <- getWord8
579+ case i of
580+ 0 -> return Static
581+ 1 -> return Dynamic
582+ _ -> error "Corrupted binary data for Static"
583+
584+
585+instance Binary Plicity where
586+ put x
587+ = case x of
588+ Imp x1 x2 -> do putWord8 0
589+ put x1
590+ put x2
591+ Exp x1 x2 -> do putWord8 1
592+ put x1
593+ put x2
594+ Constraint x1 x2 -> do putWord8 2
595+ put x1
596+ put x2
597+ get
598+ = do i <- getWord8
599+ case i of
600+ 0 -> do x1 <- get
601+ x2 <- get
602+ return (Imp x1 x2)
603+ 1 -> do x1 <- get
604+ x2 <- get
605+ return (Exp x1 x2)
606+ 2 -> do x1 <- get
607+ x2 <- get
608+ return (Constraint x1 x2)
609+ _ -> error "Corrupted binary data for Plicity"
610+
611+
612+instance Binary PTerm where
613+ put x
614+ = case x of
615+ PQuote x1 -> do putWord8 0
616+ put x1
617+ PRef x1 x2 -> do putWord8 1
618+ put x1
619+ put x2
620+ PLam x1 x2 x3 -> do putWord8 2
621+ put x1
622+ put x2
623+ put x3
624+ PPi x1 x2 x3 x4 -> do putWord8 3
625+ put x1
626+ put x2
627+ put x3
628+ put x4
629+ PLet x1 x2 x3 x4 -> do putWord8 4
630+ put x1
631+ put x2
632+ put x3
633+ put x4
634+ PApp x1 x2 x3 -> do putWord8 5
635+ put x1
636+ put x2
637+ put x3
638+ PTrue x1 -> do putWord8 6
639+ put x1
640+ PFalse x1 -> do putWord8 7
641+ put x1
642+ PRefl x1 -> do putWord8 8
643+ put x1
644+ PResolveTC x1 -> do putWord8 9
645+ put x1
646+ PEq x1 x2 x3 -> do putWord8 10
647+ put x1
648+ put x2
649+ put x3
650+ PPair x1 x2 x3 -> do putWord8 11
651+ put x1
652+ put x2
653+ put x3
654+ PDPair x1 x2 x3 x4 -> do putWord8 12
655+ put x1
656+ put x2
657+ put x3
658+ put x4
659+ PAlternative x1 -> do putWord8 13
660+ put x1
661+ PHidden x1 -> do putWord8 14
662+ put x1
663+ PSet -> putWord8 15
664+ PConstant x1 -> do putWord8 16
665+ put x1
666+ Placeholder -> putWord8 17
667+ PDoBlock x1 -> do putWord8 18
668+ put x1
669+ PReturn x1 -> do putWord8 19
670+ put x1
671+ PMetavar x1 -> do putWord8 20
672+ put x1
673+ PProof x1 -> do putWord8 21
674+ put x1
675+ PTactics x1 -> do putWord8 22
676+ put x1
677+ PElabError x1 -> do putWord8 23
678+ put x1
679+ PImpossible -> putWord8 24
680+ get
681+ = do i <- getWord8
682+ case i of
683+ 0 -> do x1 <- get
684+ return (PQuote x1)
685+ 1 -> do x1 <- get
686+ x2 <- get
687+ return (PRef x1 x2)
688+ 2 -> do x1 <- get
689+ x2 <- get
690+ x3 <- get
691+ return (PLam x1 x2 x3)
692+ 3 -> do x1 <- get
693+ x2 <- get
694+ x3 <- get
695+ x4 <- get
696+ return (PPi x1 x2 x3 x4)
697+ 4 -> do x1 <- get
698+ x2 <- get
699+ x3 <- get
700+ x4 <- get
701+ return (PLet x1 x2 x3 x4)
702+ 5 -> do x1 <- get
703+ x2 <- get
704+ x3 <- get
705+ return (PApp x1 x2 x3)
706+ 6 -> do x1 <- get
707+ return (PTrue x1)
708+ 7 -> do x1 <- get
709+ return (PFalse x1)
710+ 8 -> do x1 <- get
711+ return (PRefl x1)
712+ 9 -> do x1 <- get
713+ return (PResolveTC x1)
714+ 10 -> do x1 <- get
715+ x2 <- get
716+ x3 <- get
717+ return (PEq x1 x2 x3)
718+ 11 -> do x1 <- get
719+ x2 <- get
720+ x3 <- get
721+ return (PPair x1 x2 x3)
722+ 12 -> do x1 <- get
723+ x2 <- get
724+ x3 <- get
725+ x4 <- get
726+ return (PDPair x1 x2 x3 x4)
727+ 13 -> do x1 <- get
728+ return (PAlternative x1)
729+ 14 -> do x1 <- get
730+ return (PHidden x1)
731+ 15 -> return PSet
732+ 16 -> do x1 <- get
733+ return (PConstant x1)
734+ 17 -> return Placeholder
735+ 18 -> do x1 <- get
736+ return (PDoBlock x1)
737+ 19 -> do x1 <- get
738+ return (PReturn x1)
739+ 20 -> do x1 <- get
740+ return (PMetavar x1)
741+ 21 -> do x1 <- get
742+ return (PProof x1)
743+ 22 -> do x1 <- get
744+ return (PTactics x1)
745+ 23 -> do x1 <- get
746+ return (PElabError x1)
747+ 24 -> return PImpossible
748+ _ -> error "Corrupted binary data for PTerm"
749+
750+
751+instance (Binary t) => Binary (PTactic' t) where
752+ put x
753+ = case x of
754+ Intro x1 -> do putWord8 0
755+ put x1
756+ Focus x1 -> do putWord8 1
757+ put x1
758+ Refine x1 x2 -> do putWord8 2
759+ put x1
760+ put x2
761+ Rewrite x1 -> do putWord8 3
762+ put x1
763+ LetTac x1 x2 -> do putWord8 4
764+ put x1
765+ put x2
766+ Exact x1 -> do putWord8 5
767+ put x1
768+ Compute -> putWord8 6
769+ Trivial -> putWord8 7
770+ Solve -> putWord8 8
771+ Attack -> putWord8 9
772+ ProofState -> putWord8 10
773+ ProofTerm -> putWord8 11
774+ Undo -> putWord8 12
775+ Try x1 x2 -> do putWord8 13
776+ put x1
777+ put x2
778+ TSeq x1 x2 -> do putWord8 14
779+ put x1
780+ put x2
781+ Qed -> putWord8 15
782+ get
783+ = do i <- getWord8
784+ case i of
785+ 0 -> do x1 <- get
786+ return (Intro x1)
787+ 1 -> do x1 <- get
788+ return (Focus x1)
789+ 2 -> do x1 <- get
790+ x2 <- get
791+ return (Refine x1 x2)
792+ 3 -> do x1 <- get
793+ return (Rewrite x1)
794+ 4 -> do x1 <- get
795+ x2 <- get
796+ return (LetTac x1 x2)
797+ 5 -> do x1 <- get
798+ return (Exact x1)
799+ 6 -> return Compute
800+ 7 -> return Trivial
801+ 8 -> return Solve
802+ 9 -> return Attack
803+ 10 -> return ProofState
804+ 11 -> return ProofTerm
805+ 12 -> return Undo
806+ 13 -> do x1 <- get
807+ x2 <- get
808+ return (Try x1 x2)
809+ 14 -> do x1 <- get
810+ x2 <- get
811+ return (TSeq x1 x2)
812+ 15 -> return Qed
813+ _ -> error "Corrupted binary data for PTactic'"
814+
815+
816+instance (Binary t) => Binary (PDo' t) where
817+ put x
818+ = case x of
819+ DoExp x1 x2 -> do putWord8 0
820+ put x1
821+ put x2
822+ DoBind x1 x2 x3 -> do putWord8 1
823+ put x1
824+ put x2
825+ put x3
826+ DoLet x1 x2 x3 -> do putWord8 2
827+ put x1
828+ put x2
829+ put x3
830+ get
831+ = do i <- getWord8
832+ case i of
833+ 0 -> do x1 <- get
834+ x2 <- get
835+ return (DoExp x1 x2)
836+ 1 -> do x1 <- get
837+ x2 <- get
838+ x3 <- get
839+ return (DoBind x1 x2 x3)
840+ 2 -> do x1 <- get
841+ x2 <- get
842+ x3 <- get
843+ return (DoLet x1 x2 x3)
844+ _ -> error "Corrupted binary data for PDo'"
845+
846+
847+instance (Binary t) => Binary (PArg' t) where
848+ put x
849+ = case x of
850+ PImp x1 x2 x3 x4 -> do putWord8 0
851+ put x1
852+ put x2
853+ put x3
854+ put x4
855+ PExp x1 x2 x3 -> do putWord8 1
856+ put x1
857+ put x2
858+ put x3
859+ PConstraint x1 x2 x3 -> do putWord8 2
860+ put x1
861+ put x2
862+ put x3
863+ get
864+ = do i <- getWord8
865+ case i of
866+ 0 -> do x1 <- get
867+ x2 <- get
868+ x3 <- get
869+ x4 <- get
870+ return (PImp x1 x2 x3 x4)
871+ 1 -> do x1 <- get
872+ x2 <- get
873+ x3 <- get
874+ return (PExp x1 x2 x3)
875+ 2 -> do x1 <- get
876+ x2 <- get
877+ x3 <- get
878+ return (PConstraint x1 x2 x3)
879+ _ -> error "Corrupted binary data for PArg'"
880+
881+
882+instance Binary ClassInfo where
883+ put (CI x1 x2 x3 x4)
884+ = do put x1
885+ put x2
886+ put x3
887+ put x4
888+ get
889+ = do x1 <- get
890+ x2 <- get
891+ x3 <- get
892+ x4 <- get
893+ return (CI x1 x2 x3 x4)
894+
895+
896+instance Binary SynContext where
897+ put x
898+ = case x of
899+ PatternSyntax -> putWord8 0
900+ TermSyntax -> putWord8 1
901+ AnySyntax -> putWord8 2
902+ get
903+ = do i <- getWord8
904+ case i of
905+ 0 -> return PatternSyntax
906+ 1 -> return TermSyntax
907+ 2 -> return AnySyntax
908+ _ -> error "Corrupted binary data for SynContext"
909+
910+
911+instance Binary Syntax where
912+ put (Rule x1 x2 x3)
913+ = do put x1
914+ put x2
915+ put x3
916+ get
917+ = do x1 <- get
918+ x2 <- get
919+ x3 <- get
920+ return (Rule x1 x2 x3)
85921
922+
923+instance Binary SSymbol where
924+ put x
925+ = case x of
926+ Keyword x1 -> do putWord8 0
927+ put x1
928+ Symbol x1 -> do putWord8 1
929+ put x1
930+ Expr x1 -> do putWord8 2
931+ put x1
932+ get
933+ = do i <- getWord8
934+ case i of
935+ 0 -> do x1 <- get
936+ return (Keyword x1)
937+ 1 -> do x1 <- get
938+ return (Symbol x1)
939+ 2 -> do x1 <- get
940+ return (Expr x1)
941+ _ -> error "Corrupted binary data for SSymbol"