git.iko.soy/Idris-dev
on 385dcbf help sign in
Idris-dev/src/Idris/Core/Binary.hs
693 lines 27 kB history raw
1{-|
2Module : Idris.Core.Binary
3Description : Binary instances for the core datatypes
4Copyright :
5License : BSD3
6Maintainer : The Idris Community.
7-}
8{-# OPTIONS_GHC -fwarn-incomplete-patterns #-}
9module Idris.Core.Binary where
11import Idris.Core.TT
13import Control.Applicative ((<$>), (<*>))
14import Control.DeepSeq (($!!))
15import Control.Monad (liftM2)
16import Data.Binary
17import qualified Data.Text as T
18import qualified Data.Text.Encoding as E
19import Data.Vector.Binary
21instance Binary ErrorReportPart where
22 put (TextPart msg) = do putWord8 0 ; put msg
23 put (NamePart n) = do putWord8 1 ; put n
24 put (TermPart t) = do putWord8 2 ; put t
25 put (SubReport ps) = do putWord8 3 ; put ps
26 put (RawPart r) = do putWord8 4 ; put r
28 get = do i <- getWord8
29 case i of
30 0 -> fmap TextPart get
31 1 -> fmap NamePart get
32 2 -> fmap TermPart get
33 3 -> fmap SubReport get
34 4 -> fmap RawPart get
35 _ -> error "Corrupted binary data for ErrorReportPart"
37instance Binary Provenance where
38 put ExpectedType = putWord8 0
39 put (SourceTerm t) = do putWord8 1
40 put t
41 put InferredVal = putWord8 2
42 put GivenVal = putWord8 3
43 put (TooManyArgs t) = do putWord8 4
44 put t
46 get = do i <- getWord8
47 case i of
48 0 -> return ExpectedType
49 1 -> do x1 <- get
50 return (SourceTerm x1)
51 2 -> return InferredVal
52 3 -> return GivenVal
53 4 -> do x1 <- get
54 return (TooManyArgs x1)
55 _ -> error "Corrupted binary data for Provenance"
57instance Binary UConstraint where
58 put (ULT x1 x2) = putWord8 0 >> put x1 >> put x2
59 put (ULE x1 x2) = putWord8 1 >> put x1 >> put x2
60 get = do i <- getWord8
61 case i of
62 0 -> ULT <$> get <*> get
63 1 -> ULE <$> get <*> get
64 _ -> error "Corrupted binary data for UConstraint"
66instance Binary ConstraintFC where
67 put (ConstraintFC x1 x2) = putWord8 0 >> put x1 >> put x2
68 get = do i <- getWord8
69 case i of
70 0 -> liftM2 ConstraintFC get get
71 _ -> error "Corrupted binary data for ConstraintFC"
73instance Binary a => Binary (Err' a) where
74 put (Msg str) = do putWord8 0
75 put str
76 put (InternalMsg str) = do putWord8 1
77 put str
78 put (CantUnify x y z e ctxt i) = do putWord8 2
79 put x
80 put y
81 put z
82 put e
83 put ctxt
84 put i
85 put (InfiniteUnify n t ctxt) = do putWord8 3
86 put n
87 put t
88 put ctxt
89 put (CantConvert x y ctxt) = do putWord8 4
90 put x
91 put y
92 put ctxt
93 put (CantSolveGoal x ctxt) = do putWord8 5
94 put x
95 put ctxt
96 put (UnifyScope n1 n2 x ctxt) = do putWord8 6
97 put n1
98 put n2
99 put x
100 put ctxt
101 put (CantInferType str) = do putWord8 7
102 put str
103 put (NonFunctionType t1 t2) = do putWord8 8
104 put t1
105 put t2
106 put (NotEquality t1 t2) = do putWord8 9
107 put t1
108 put t2
109 put (TooManyArguments n) = do putWord8 10
110 put n
111 put (CantIntroduce t) = do putWord8 11
112 put t
113 put (NoSuchVariable n) = do putWord8 12
114 put n
115 put (NoTypeDecl n) = do putWord8 13
116 put n
117 put (NotInjective x y z) = do putWord8 14
118 put x
119 put y
120 put z
121 put (CantResolve _ t u) = do putWord8 15
122 put t
123 put u
124 put (CantResolveAlts ns) = do putWord8 16
125 put ns
126 put (IncompleteTerm t) = do putWord8 17
127 put t
128 put (UniverseError x1 x2 x3 x4 x5) = do putWord8 18
129 put x1
130 put x2
131 put x3
132 put x4
133 put x5
134 put (UniqueError u n) = do putWord8 19
135 put u
136 put n
137 put (UniqueKindError u n) = do putWord8 20
138 put u
139 put n
140 put ProgramLineComment = putWord8 21
141 put (Inaccessible n) = do putWord8 22
142 put n
143 put (NonCollapsiblePostulate n) = do putWord8 23
144 put n
145 put (AlreadyDefined n) = do putWord8 24
146 put n
147 put (ProofSearchFail e) = do putWord8 25
148 put e
149 put (NoRewriting l r t) = do putWord8 26
150 put l
151 put r
152 put t
153 put (At fc e) = do putWord8 27
154 put fc
155 put e
156 put (Elaborating str n ty e) = do putWord8 28
157 put str
158 put n
159 put ty
160 put e
161 put (ElaboratingArg n1 n2 ns e) = do putWord8 29
162 put n1
163 put n2
164 put ns
165 put e
166 put (ProviderError str) = do putWord8 30
167 put str
168 put (LoadingFailed str e) = do putWord8 31
169 put str
170 put e
171 put (ReflectionError parts e) = do putWord8 32
172 put parts
173 put e
174 put (ReflectionFailed str e) = do putWord8 33
175 put str
176 put e
177 put (WithFnType t) = do putWord8 34
178 put t
179 put (CantMatch t) = do putWord8 35
180 put t
181 put (ElabScriptDebug x1 x2 x3) = do putWord8 36
182 put x1
183 put x2
184 put x3
185 put (NoEliminator s t) = do putWord8 37
186 put s
187 put t
188 put (InvalidTCArg n t) = do putWord8 38
189 put n
190 put t
191 put (ElabScriptStuck x1) = do putWord8 39
192 put x1
193 put (UnknownImplicit n f) = do putWord8 40
194 put n
195 put f
196 put (NoValidAlts ns) = do putWord8 41
197 put ns
198 put (RunningElabScript e) = do putWord8 42
199 put e
200 put (ElabScriptStaging n) = do putWord8 43
201 put n
202 put (FancyMsg xs) = do putWord8 44
203 put xs
204 get = do i <- getWord8
205 case i of
206 0 -> fmap Msg get
207 1 -> fmap InternalMsg get
208 2 -> do x <- get ; y <- get ; z <- get ; e <- get ; ctxt <- get ; i <- get
209 return $ CantUnify x y z e ctxt i
210 3 -> do x <- get ; y <- get ; z <- get
211 return $ InfiniteUnify x y z
212 4 -> do x <- get ; y <- get ; z <- get
213 return $ CantConvert x y z
214 5 -> do x <- get ; y <- get
215 return $ CantSolveGoal x y
216 6 -> do w <- get ; x <- get ; y <- get ; z <- get
217 return $ UnifyScope w x y z
218 7 -> fmap CantInferType get
219 8 -> do x <- get ; y <- get
220 return $ NonFunctionType x y
221 9 -> do x <- get ; y <- get
222 return $ NotEquality x y
223 10 -> fmap TooManyArguments get
224 11 -> fmap CantIntroduce get
225 12 -> fmap NoSuchVariable get
226 13 -> fmap NoTypeDecl get
227 14 -> do x <- get ; y <- get ; z <- get
228 return $ NotInjective x y z
229 15 -> CantResolve False <$> get <*> get
230 16 -> fmap CantResolveAlts get
231 17 -> fmap IncompleteTerm get
232 18 -> UniverseError <$> get <*> get <*> get <*> get <*> get
233 19 -> do x <- get ; y <- get
234 return $ UniqueError x y
235 20 -> do x <- get ; y <- get
236 return $ UniqueKindError x y
237 21 -> return ProgramLineComment
238 22 -> fmap Inaccessible get
239 23 -> fmap NonCollapsiblePostulate get
240 24 -> fmap AlreadyDefined get
241 25 -> fmap ProofSearchFail get
242 26 -> do l <- get; r <- get; t <- get
243 return $ NoRewriting l r t
244 27 -> do x <- get ; y <- get
245 return $ At x y
246 28 -> do w <- get; x <- get ; y <- get ; z <- get
247 return $ Elaborating w x y z
248 29 -> do w <- get ; x <- get ; y <- get ; z <- get
249 return $ ElaboratingArg w x y z
250 30 -> fmap ProviderError get
251 31 -> do x <- get ; y <- get
252 return $ LoadingFailed x y
253 32 -> do x <- get ; y <- get
254 return $ ReflectionError x y
255 33 -> do x <- get ; y <- get
256 return $ ReflectionFailed x y
257 34 -> fmap WithFnType get
258 35 -> fmap CantMatch get
259 36 -> do x1 <- get
260 x2 <- get
261 x3 <- get
262 return (ElabScriptDebug x1 x2 x3)
263 37 -> do x1 <- get
264 x2 <- get
265 return (NoEliminator x1 x2)
266 38 -> do x1 <- get
267 x2 <- get
268 return (InvalidTCArg x1 x2)
269 39 -> do x1 <- get
270 return (ElabScriptStuck x1)
271 40 -> do x <- get ; y <- get
272 return $ UnknownImplicit x y
273 41 -> fmap NoValidAlts get
274 42 -> fmap RunningElabScript get
275 43 -> fmap ElabScriptStaging get
276 44 -> fmap FancyMsg get
277 _ -> error "Corrupted binary data for Err'"
278----- Generated by 'derive'
280instance Binary FC where
281 put x =
282 case x of
283 (FC x1 (x2, x3) (x4, x5)) -> do putWord8 0
284 put x1
285 put (x2 * 65536 + x3)
286 put (x4 * 65536 + x5)
287 NoFC -> putWord8 1
288 FileFC x1 -> do putWord8 2
289 put x1
290 get
291 = do i <- getWord8
292 case i of
293 0 -> do x1 <- get
294 x2x3 <- get
295 x4x5 <- get
296 return (FC x1 (x2x3 `div` 65536, x2x3 `mod` 65536) (x4x5 `div` 65536, x4x5 `mod` 65536))
297 1 -> return NoFC
298 2 -> do x1 <- get
299 return (FileFC x1)
300 _ -> error "Corrupted binary data for FC"
302instance Binary FC' where
303 put (FC' fc) = put fc
304 get = fmap FC' get
306instance Binary Name where
307 put x
308 = case x of
309 UN x1 -> do putWord8 0
310 put x1
311 NS x1 x2 -> do putWord8 1
312 put x1
313 put x2
314 MN x1 x2 -> do putWord8 2
315 put x1
316 put x2
317 SN x1 -> do putWord8 3
318 put x1
319 SymRef x1 -> do putWord8 4
320 put x1
321 get
322 = do i <- getWord8
323 case i of
324 0 -> do x1 <- get
325 return (UN x1)
326 1 -> do x1 <- get
327 x2 <- get
328 return (NS x1 x2)
329 2 -> do x1 <- get
330 x2 <- get
331 return (MN x1 x2)
332 3 -> do x1 <- get
333 return (SN x1)
334 4 -> do x1 <- get
335 return (SymRef x1)
336 _ -> error "Corrupted binary data for Name"
338instance Binary SpecialName where
339 put x
340 = case x of
341 WhereN x1 x2 x3 -> do putWord8 0
342 put x1
343 put x2
344 put x3
345 ImplementationN x1 x2 -> do putWord8 1
346 put x1
347 put x2
348 ParentN x1 x2 -> do putWord8 2
349 put x1
350 put x2
351 MethodN x1 -> do putWord8 3
352 put x1
353 CaseN x1 x2 -> do putWord8 4; put x1; put x2
354 ElimN x1 -> do putWord8 5; put x1
355 ImplementationCtorN x1 -> do putWord8 6; put x1
356 WithN x1 x2 -> do putWord8 7
357 put x1
358 put x2
359 MetaN x1 x2 -> do putWord8 8
360 put x1
361 put x2
362 get
363 = do i <- getWord8
364 case i of
365 0 -> do x1 <- get
366 x2 <- get
367 x3 <- get
368 return (WhereN x1 x2 x3)
369 1 -> do x1 <- get
370 x2 <- get
371 return (ImplementationN x1 x2)
372 2 -> do x1 <- get
373 x2 <- get
374 return (ParentN x1 x2)
375 3 -> do x1 <- get
376 return (MethodN x1)
377 4 -> do x1 <- get
378 x2 <- get
379 return (CaseN x1 x2)
380 5 -> do x1 <- get
381 return (ElimN x1)
382 6 -> do x1 <- get
383 return (ImplementationCtorN x1)
384 7 -> do x1 <- get
385 x2 <- get
386 return (WithN x1 x2)
387 8 -> do x1 <- get
388 x2 <- get
389 return (MetaN x1 x2)
390 _ -> error "Corrupted binary data for SpecialName"
393instance Binary Const where
394 put x
395 = case x of
396 I x1 -> do putWord8 0
397 put x1
398 BI x1 -> do putWord8 1
399 put x1
400 Fl x1 -> do putWord8 2
401 put x1
402 Ch x1 -> do putWord8 3
403 put x1
404 Str x1 -> do putWord8 4
405 put x1
406 B8 x1 -> putWord8 5 >> put x1
407 B16 x1 -> putWord8 6 >> put x1
408 B32 x1 -> putWord8 7 >> put x1
409 B64 x1 -> putWord8 8 >> put x1
411 (AType (ATInt ITNative)) -> putWord8 9
412 (AType (ATInt ITBig)) -> putWord8 10
413 (AType ATFloat) -> putWord8 11
414 (AType (ATInt ITChar)) -> putWord8 12
415 StrType -> putWord8 13
416 Forgot -> putWord8 15
417 (AType (ATInt (ITFixed ity))) -> putWord8 (fromIntegral (16 + fromEnum ity)) -- 16-19 inclusive
418 VoidType -> putWord8 27
419 WorldType -> putWord8 28
420 TheWorld -> putWord8 29
421 get
422 = do i <- getWord8
423 case i of
424 0 -> do x1 <- get
425 return (I x1)
426 1 -> do x1 <- get
427 return (BI x1)
428 2 -> do x1 <- get
429 return (Fl x1)
430 3 -> do x1 <- get
431 return (Ch x1)
432 4 -> do x1 <- get
433 return (Str x1)
434 5 -> fmap B8 get
435 6 -> fmap B16 get
436 7 -> fmap B32 get
437 8 -> fmap B64 get
439 9 -> return (AType (ATInt ITNative))
440 10 -> return (AType (ATInt ITBig))
441 11 -> return (AType ATFloat)
442 12 -> return (AType (ATInt ITChar))
443 13 -> return StrType
444 15 -> return Forgot
446 16 -> return (AType (ATInt (ITFixed IT8)))
447 17 -> return (AType (ATInt (ITFixed IT16)))
448 18 -> return (AType (ATInt (ITFixed IT32)))
449 19 -> return (AType (ATInt (ITFixed IT64)))
451 27 -> return VoidType
452 28 -> return WorldType
453 29 -> return TheWorld
454 _ -> error "Corrupted binary data for Const"
457instance Binary Raw where
458 put x
459 = case x of
460 Var x1 -> do putWord8 0
461 put x1
462 RBind x1 x2 x3 -> do putWord8 1
463 put x1
464 put x2
465 put x3
466 RApp x1 x2 -> do putWord8 2
467 put x1
468 put x2
469 RType -> putWord8 3
470 RConstant x1 -> do putWord8 4
471 put x1
472 RUType x1 -> do putWord8 5
473 put x1
474 get
475 = do i <- getWord8
476 case i of
477 0 -> do x1 <- get
478 return (Var x1)
479 1 -> do x1 <- get
480 x2 <- get
481 x3 <- get
482 return (RBind x1 x2 x3)
483 2 -> do x1 <- get
484 x2 <- get
485 return (RApp x1 x2)
486 3 -> return RType
487 4 -> do x1 <- get
488 return (RConstant x1)
489 5 -> do x1 <- get
490 return (RUType x1)
491 _ -> error "Corrupted binary data for Raw"
493instance Binary RigCount where
494 put x = case x of
495 Rig0 -> putWord8 0
496 Rig1 -> putWord8 1
497 RigW -> putWord8 2
498 get = do i <- getWord8
499 case i of
500 0 -> return Rig0
501 1 -> return Rig1
502 2 -> return RigW
503 _ -> error "Corrupted binary data for RigCount"
506instance Binary ImplicitInfo where
507 put x
508 = case x of
509 Impl x1 x2 x3 -> do put x1; put x2
510 get
511 = do x1 <- get
512 x2 <- get
513 return (Impl x1 x2 False)
515instance (Binary b) => Binary (Binder b) where
516 put x
517 = case x of
518 Lam x1 x2 -> do putWord8 0
519 put x1
520 put x2
521 Pi x1 x2 x3 x4 -> do putWord8 1
522 put x1
523 put x2
524 put x3
525 put x4
526 Let x1 x2 -> do putWord8 2
527 put x1
528 put x2
529 NLet x1 x2 -> do putWord8 3
530 put x1
531 put x2
532 Hole x1 -> do putWord8 4
533 put x1
534 GHole x1 x2 x3 -> do putWord8 5
535 put x1
536 put x2
537 put x3
538 Guess x1 x2 -> do putWord8 6
539 put x1
540 put x2
541 PVar x1 x2 -> do putWord8 7
542 put x1
543 put x2
544 PVTy x1 -> do putWord8 8
545 put x1
546 get
547 = do i <- getWord8
548 case i of
549 0 -> do x1 <- get
550 x2 <- get
551 return (Lam x1 x2)
552 1 -> do x1 <- get
553 x2 <- get
554 x3 <- get
555 x4 <- get
556 return (Pi x1 x2 x3 x4)
557 2 -> do x1 <- get
558 x2 <- get
559 return (Let x1 x2)
560 3 -> do x1 <- get
561 x2 <- get
562 return (NLet x1 x2)
563 4 -> do x1 <- get
564 return (Hole x1)
565 5 -> do x1 <- get
566 x2 <- get
567 x3 <- get
568 return (GHole x1 x2 x3)
569 6 -> do x1 <- get
570 x2 <- get
571 return (Guess x1 x2)
572 7 -> do x1 <- get
573 x2 <- get
574 return (PVar x1 x2)
575 8 -> do x1 <- get
576 return (PVTy x1)
577 _ -> error "Corrupted binary data for Binder"
580instance Binary Universe where
581 put x = case x of
582 UniqueType -> putWord8 0
583 AllTypes -> putWord8 1
584 NullType -> putWord8 2
585 get = do i <- getWord8
586 case i of
587 0 -> return UniqueType
588 1 -> return AllTypes
589 2 -> return NullType
590 _ -> error "Corrupted binary data for Universe"
592instance Binary NameType where
593 put x
594 = case x of
595 Bound -> putWord8 0
596 Ref -> putWord8 1
597 DCon x1 x2 x3 -> do putWord8 2
598 put (x1 * 65536 + x2)
599 put x3
600 TCon x1 x2 -> do putWord8 3
601 put (x1 * 65536 + x2)
602 get
603 = do i <- getWord8
604 case i of
605 0 -> return Bound
606 1 -> return Ref
607 2 -> do x1x2 <- get
608 x3 <- get
609 return (DCon (x1x2 `div` 65536) (x1x2 `mod` 65536) x3)
610 3 -> do x1x2 <- get
611 return (TCon (x1x2 `div` 65536) (x1x2 `mod` 65536))
612 _ -> error "Corrupted binary data for NameType"
614-- record concrete levels only, for now
615instance Binary UExp where
616 put x = case x of
617 UVar ns t -> do putWord8 0
618 put ns
619 put t
620 UVal t -> do putWord8 1
621 put t
623 get = do i <- getWord8
624 case i of
625 0 -> do x1 <- get
626 x2 <- get
627 return (UVar x1 x2)
628 1 -> do x1 <- get
629 return (UVal x1)
630 _ -> error "Corrupted binary data for UExp"
632instance {- (Binary n) => -} Binary (TT Name) where
633 put x
634 = {-# SCC "putTT" #-}
635 case x of
636 P x1 x2 x3 -> do putWord8 0
637 put x1
638 put x2
639-- put x3
640 V x1 -> if (x1 >= 0 && x1 < 256)
641 then do putWord8 1
642 putWord8 (toEnum (x1 + 1))
643 else do putWord8 9
644 put x1
645 Bind x1 x2 x3 -> do putWord8 2
646 put x1
647 put x2
648 put x3
649 App _ x1 x2 -> do putWord8 3
650 put x1
651 put x2
652 Constant x1 -> do putWord8 4
653 put x1
654 Proj x1 x2 -> do putWord8 5
655 put x1
656 putWord8 (toEnum (x2 + 1))
657 Erased -> putWord8 6
658 TType x1 -> do putWord8 7
659 put x1
660 Impossible -> putWord8 8
661 Inferred x1 -> put x1 -- drop the 'Inferred'
662 UType x1 -> do putWord8 10
663 put x1
664 get
665 = do i <- getWord8
666 case i of
667 0 -> do x1 <- get
668 x2 <- get
669-- x3 <- get
670 return (P x1 x2 Erased)
671 1 -> do x1 <- getWord8
672 return (V ((fromEnum x1) - 1))
673 2 -> do x1 <- get
674 x2 <- get
675 x3 <- get
676 return (Bind x1 x2 x3)
677 3 -> do x1 <- get
678 x2 <- get
679 return (App Complete x1 x2)
680 4 -> do x1 <- get
681 return (Constant x1)
682 5 -> do x1 <- get
683 x2 <- getWord8
684 return (Proj x1 ((fromEnum x2)-1))
685 6 -> return Erased
686 7 -> do x1 <- get
687 return (TType x1)
688 8 -> return Impossible
689 9 -> do x1 <- get
690 return (V x1)
691 10 -> do x1 <- get
692 return (UType x1)
693 _ -> error "Corrupted binary data for TT"