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