git.iko.soy/Idris-dev
on 13ebfcf help sign in
Idris-dev/src/Idris/Core/Binary.hs
599 lines 23 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
150 get = do i <- getWord8
151 case i of
152 0 -> fmap Msg get
153 1 -> fmap InternalMsg get
154 2 -> do x <- get ; y <- get ; z <- get ; e <- get ; ctxt <- get ; i <- get
155 return $ CantUnify x y z e ctxt i
156 3 -> do x <- get ; y <- get ; z <- get
157 return $ InfiniteUnify x y z
158 4 -> do x <- get ; y <- get ; z <- get
159 return $ CantConvert x y z
160 5 -> do x <- get ; y <- get
161 return $ CantSolveGoal x y
162 6 -> do w <- get ; x <- get ; y <- get ; z <- get
163 return $ UnifyScope w x y z
164 7 -> fmap CantInferType get
165 8 -> do x <- get ; y <- get
166 return $ NonFunctionType x y
167 9 -> do x <- get ; y <- get
168 return $ NotEquality x y
169 10 -> fmap TooManyArguments get
170 11 -> fmap CantIntroduce get
171 12 -> fmap NoSuchVariable get
172 13 -> fmap NoTypeDecl get
173 14 -> do x <- get ; y <- get ; z <- get
174 return $ NotInjective x y z
175 15 -> fmap CantResolve get
176 16 -> fmap CantResolveAlts get
177 17 -> fmap IncompleteTerm get
178 18 -> return UniverseError
179 19 -> do x <- get ; y <- get
180 return $ UniqueError x y
181 20 -> do x <- get ; y <- get
182 return $ UniqueKindError x y
183 21 -> return ProgramLineComment
184 22 -> fmap Inaccessible get
185 23 -> fmap NonCollapsiblePostulate get
186 24 -> fmap AlreadyDefined get
187 25 -> fmap ProofSearchFail get
188 26 -> fmap NoRewriting get
189 27 -> do x <- get ; y <- get
190 return $ At x y
191 28 -> do x <- get ; y <- get ; z <- get
192 return $ Elaborating x y z
193 29 -> do w <- get ; x <- get ; y <- get ; z <- get
194 return $ ElaboratingArg w x y z
195 30 -> fmap ProviderError get
196 31 -> do x <- get ; y <- get
197 return $ LoadingFailed x y
198 32 -> do x <- get ; y <- get
199 return $ ReflectionError x y
200 33 -> do x <- get ; y <- get
201 return $ ReflectionFailed x y
202 34 -> fmap WithFnType get
203 35 -> fmap CantMatch get
204 36 -> do x1 <- get
205 x2 <- get
206 x3 <- get
207 return (ElabDebug x1 x2 x3)
208 _ -> error "Corrupted binary data for Err'"
209----- Generated by 'derive'
211instance Binary FC where
212 put (FC x1 (x2, x3) (x4, x5))
213 = do put x1
214 put (x2 * 65536 + x3)
215 put (x4 * 65536 + x5)
216 get
217 = do x1 <- get
218 x2x3 <- get
219 x4x5 <- get
220 return (FC x1 (x2x3 `div` 65536, x2x3 `mod` 65536) (x4x5 `div` 65536, x4x5 `mod` 65536))
223instance Binary Name where
224 put x
225 = case x of
226 UN x1 -> do putWord8 0
227 put x1
228 NS x1 x2 -> do putWord8 1
229 put x1
230 put x2
231 MN x1 x2 -> do putWord8 2
232 put x1
233 put x2
234 NErased -> putWord8 3
235 SN x1 -> do putWord8 4
236 put x1
237 SymRef x1 -> do putWord8 5
238 put x1
239 get
240 = do i <- getWord8
241 case i of
242 0 -> do x1 <- get
243 return (UN x1)
244 1 -> do x1 <- get
245 x2 <- get
246 return (NS x1 x2)
247 2 -> do x1 <- get
248 x2 <- get
249 return (MN x1 x2)
250 3 -> return NErased
251 4 -> do x1 <- get
252 return (SN x1)
253 5 -> do x1 <- get
254 return (SymRef x1)
255 _ -> error "Corrupted binary data for Name"
257instance Binary T.Text where
258 put x = put (str x)
259 get = do x <- get
260 return (txt x)
262instance Binary SpecialName where
263 put x
264 = case x of
265 WhereN x1 x2 x3 -> do putWord8 0
266 put x1
267 put x2
268 put x3
269 InstanceN x1 x2 -> do putWord8 1
270 put x1
271 put x2
272 ParentN x1 x2 -> do putWord8 2
273 put x1
274 put x2
275 MethodN x1 -> do putWord8 3
276 put x1
277 CaseN x1 -> do putWord8 4; put x1
278 ElimN x1 -> do putWord8 5; put x1
279 InstanceCtorN x1 -> do putWord8 6; put x1
280 WithN x1 x2 -> do putWord8 7
281 put x1
282 put x2
283 get
284 = do i <- getWord8
285 case i of
286 0 -> do x1 <- get
287 x2 <- get
288 x3 <- get
289 return (WhereN x1 x2 x3)
290 1 -> do x1 <- get
291 x2 <- get
292 return (InstanceN x1 x2)
293 2 -> do x1 <- get
294 x2 <- get
295 return (ParentN x1 x2)
296 3 -> do x1 <- get
297 return (MethodN x1)
298 4 -> do x1 <- get
299 return (CaseN x1)
300 5 -> do x1 <- get
301 return (ElimN x1)
302 6 -> do x1 <- get
303 return (InstanceCtorN x1)
304 7 -> do x1 <- get
305 x2 <- get
306 return (WithN x1 x2)
307 _ -> error "Corrupted binary data for SpecialName"
310instance Binary Const where
311 put x
312 = case x of
313 I x1 -> do putWord8 0
314 put x1
315 BI x1 -> do putWord8 1
316 put x1
317 Fl x1 -> do putWord8 2
318 put x1
319 Ch x1 -> do putWord8 3
320 put x1
321 Str x1 -> do putWord8 4
322 put x1
323 B8 x1 -> putWord8 5 >> put x1
324 B16 x1 -> putWord8 6 >> put x1
325 B32 x1 -> putWord8 7 >> put x1
326 B64 x1 -> putWord8 8 >> put x1
328 (AType (ATInt ITNative)) -> putWord8 9
329 (AType (ATInt ITBig)) -> putWord8 10
330 (AType ATFloat) -> putWord8 11
331 (AType (ATInt ITChar)) -> putWord8 12
332 StrType -> putWord8 13
333 PtrType -> putWord8 14
334 Forgot -> putWord8 15
335 (AType (ATInt (ITFixed ity))) -> putWord8 (fromIntegral (16 + fromEnum ity)) -- 16-19 inclusive
336 (AType (ATInt (ITVec ity count))) -> do
337 putWord8 20
338 putWord8 (fromIntegral . fromEnum $ ity)
339 putWord8 (fromIntegral count)
341 B8V x1 -> putWord8 21 >> put x1
342 B16V x1 -> putWord8 22 >> put x1
343 B32V x1 -> putWord8 23 >> put x1
344 B64V x1 -> putWord8 24 >> put x1
345 BufferType -> putWord8 25
346 ManagedPtrType -> putWord8 26
347 VoidType -> putWord8 27
348 WorldType -> putWord8 28
349 TheWorld -> putWord8 29
350 get
351 = do i <- getWord8
352 case i of
353 0 -> do x1 <- get
354 return (I x1)
355 1 -> do x1 <- get
356 return (BI x1)
357 2 -> do x1 <- get
358 return (Fl x1)
359 3 -> do x1 <- get
360 return (Ch x1)
361 4 -> do x1 <- get
362 return (Str x1)
363 5 -> fmap B8 get
364 6 -> fmap B16 get
365 7 -> fmap B32 get
366 8 -> fmap B64 get
368 9 -> return (AType (ATInt ITNative))
369 10 -> return (AType (ATInt ITBig))
370 11 -> return (AType ATFloat)
371 12 -> return (AType (ATInt ITChar))
372 13 -> return StrType
373 14 -> return PtrType
374 15 -> return Forgot
376 16 -> return (AType (ATInt (ITFixed IT8)))
377 17 -> return (AType (ATInt (ITFixed IT16)))
378 18 -> return (AType (ATInt (ITFixed IT32)))
379 19 -> return (AType (ATInt (ITFixed IT64)))
381 20 -> do
382 e <- getWord8
383 c <- getWord8
384 return (AType (ATInt (ITVec (toEnum . fromIntegral $ e) (fromIntegral c))))
386 21 -> fmap B8V get
387 22 -> fmap B16V get
388 23 -> fmap B32V get
389 24 -> fmap B64V get
390 25 -> return BufferType
391 26 -> return ManagedPtrType
392 27 -> return VoidType
393 28 -> return WorldType
394 29 -> return TheWorld
395 _ -> error "Corrupted binary data for Const"
398instance Binary Raw where
399 put x
400 = case x of
401 Var x1 -> do putWord8 0
402 put x1
403 RBind x1 x2 x3 -> do putWord8 1
404 put x1
405 put x2
406 put x3
407 RApp x1 x2 -> do putWord8 2
408 put x1
409 put x2
410 RType -> putWord8 3
411 RConstant x1 -> do putWord8 4
412 put x1
413 RForce x1 -> do putWord8 5
414 put x1
415 RUType x1 -> do putWord8 6
416 put x1
417 get
418 = do i <- getWord8
419 case i of
420 0 -> do x1 <- get
421 return (Var x1)
422 1 -> do x1 <- get
423 x2 <- get
424 x3 <- get
425 return (RBind x1 x2 x3)
426 2 -> do x1 <- get
427 x2 <- get
428 return (RApp x1 x2)
429 3 -> return RType
430 4 -> do x1 <- get
431 return (RConstant x1)
432 5 -> do x1 <- get
433 return (RForce x1)
434 6 -> do x1 <- get
435 return (RUType x1)
436 _ -> error "Corrupted binary data for Raw"
438instance Binary ImplicitInfo where
439 put x
440 = case x of
441 Impl x1 -> put x1
442 get
443 = do x1 <- get
444 return (Impl x1)
446instance (Binary b) => Binary (Binder b) where
447 put x
448 = case x of
449 Lam x1 -> do putWord8 0
450 put x1
451 Pi x1 x2 x3 -> do putWord8 1
452 put x1
453 put x2
454 put x3
455 Let x1 x2 -> do putWord8 2
456 put x1
457 put x2
458 NLet x1 x2 -> do putWord8 3
459 put x1
460 put x2
461 Hole x1 -> do putWord8 4
462 put x1
463 GHole x1 x2 -> do putWord8 5
464 put x1
465 put x2
466 Guess x1 x2 -> do putWord8 6
467 put x1
468 put x2
469 PVar x1 -> do putWord8 7
470 put x1
471 PVTy x1 -> do putWord8 8
472 put x1
473 get
474 = do i <- getWord8
475 case i of
476 0 -> do x1 <- get
477 return (Lam x1)
478 1 -> do x1 <- get
479 x2 <- get
480 x3 <- get
481 return (Pi x1 x2 x3)
482 2 -> do x1 <- get
483 x2 <- get
484 return (Let x1 x2)
485 3 -> do x1 <- get
486 x2 <- get
487 return (NLet x1 x2)
488 4 -> do x1 <- get
489 return (Hole x1)
490 5 -> do x1 <- get
491 x2 <- get
492 return (GHole x1 x2)
493 6 -> do x1 <- get
494 x2 <- get
495 return (Guess x1 x2)
496 7 -> do x1 <- get
497 return (PVar x1)
498 8 -> do x1 <- get
499 return (PVTy x1)
500 _ -> error "Corrupted binary data for Binder"
503instance Binary Universe where
504 put x = case x of
505 UniqueType -> putWord8 0
506 AllTypes -> putWord8 1
507 NullType -> putWord8 2
508 get = do i <- getWord8
509 case i of
510 0 -> return UniqueType
511 1 -> return AllTypes
512 2 -> return NullType
513 _ -> error "Corrupted binary data for Universe"
515instance Binary NameType where
516 put x
517 = case x of
518 Bound -> putWord8 0
519 Ref -> putWord8 1
520 DCon x1 x2 x3 -> do putWord8 2
521 put (x1 * 65536 + x2)
522 put x3
523 TCon x1 x2 -> do putWord8 3
524 put (x1 * 65536 + x2)
525 get
526 = do i <- getWord8
527 case i of
528 0 -> return Bound
529 1 -> return Ref
530 2 -> do x1x2 <- get
531 x3 <- get
532 return (DCon (x1x2 `div` 65536) (x1x2 `mod` 65536) x3)
533 3 -> do x1x2 <- get
534 return (TCon (x1x2 `div` 65536) (x1x2 `mod` 65536))
535 _ -> error "Corrupted binary data for NameType"
538instance {- (Binary n) => -} Binary (TT Name) where
539 put x
540 = {-# SCC "putTT" #-}
541 case x of
542 P x1 x2 x3 -> do putWord8 0
543 put x1
544 put x2
545-- put x3
546 V x1 -> if (x1 >= 0 && x1 < 256)
547 then do putWord8 1
548 putWord8 (toEnum (x1 + 1))
549 else do putWord8 9
550 put x1
551 Bind x1 x2 x3 -> do putWord8 2
552 put x1
553 put x2
554 put x3
555 App x1 x2 -> do putWord8 3
556 put x1
557 put x2
558 Constant x1 -> do putWord8 4
559 put x1
560 Proj x1 x2 -> do putWord8 5
561 put x1
562 putWord8 (toEnum (x2 + 1))
563 Erased -> putWord8 6
564 TType x1 -> do putWord8 7
565 put x1
566 Impossible -> putWord8 8
567 UType x1 -> do putWord8 10
568 put x1
569 get
570 = do i <- getWord8
571 case i of
572 0 -> do x1 <- get
573 x2 <- get
574-- x3 <- get
575 return (P x1 x2 Erased)
576 1 -> do x1 <- getWord8
577 return (V ((fromEnum x1) - 1))
578 2 -> do x1 <- get
579 x2 <- get
580 x3 <- get
581 return (Bind x1 x2 x3)
582 3 -> do x1 <- get
583 x2 <- get
584 return (App x1 x2)
585 4 -> do x1 <- get
586 return (Constant x1)
587 5 -> do x1 <- get
588 x2 <- getWord8
589 return (Proj x1 ((fromEnum x2)-1))
590 6 -> return Erased
591 7 -> do x1 <- get
592 return (TType x1)
593 8 -> return Impossible
594 9 -> do x1 <- get
595 return (V x1)
596 10 -> do x1 <- get
597 return (UType x1)
598 _ -> error "Corrupted binary data for TT"