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