git.iko.soy/Idris-dev
on be22ac6 help sign in
Idris-dev/src/Idris/Core/Binary.hs
602 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
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 Forgot -> putWord8 15
346 (AType (ATInt (ITFixed ity))) -> putWord8 (fromIntegral (16 + fromEnum ity)) -- 16-19 inclusive
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 15 -> return Forgot
375 16 -> return (AType (ATInt (ITFixed IT8)))
376 17 -> return (AType (ATInt (ITFixed IT16)))
377 18 -> return (AType (ATInt (ITFixed IT32)))
378 19 -> return (AType (ATInt (ITFixed IT64)))
380 27 -> return VoidType
381 28 -> return WorldType
382 29 -> return TheWorld
383 _ -> error "Corrupted binary data for Const"
386instance Binary Raw where
387 put x
388 = case x of
389 Var x1 -> do putWord8 0
390 put x1
391 RBind x1 x2 x3 -> do putWord8 1
392 put x1
393 put x2
394 put x3
395 RApp x1 x2 -> do putWord8 2
396 put x1
397 put x2
398 RType -> putWord8 3
399 RConstant x1 -> do putWord8 4
400 put x1
401 RForce x1 -> do putWord8 5
402 put x1
403 RUType x1 -> do putWord8 6
404 put x1
405 get
406 = do i <- getWord8
407 case i of
408 0 -> do x1 <- get
409 return (Var x1)
410 1 -> do x1 <- get
411 x2 <- get
412 x3 <- get
413 return (RBind x1 x2 x3)
414 2 -> do x1 <- get
415 x2 <- get
416 return (RApp x1 x2)
417 3 -> return RType
418 4 -> do x1 <- get
419 return (RConstant x1)
420 5 -> do x1 <- get
421 return (RForce x1)
422 6 -> do x1 <- get
423 return (RUType x1)
424 _ -> error "Corrupted binary data for Raw"
426instance Binary ImplicitInfo where
427 put x
428 = case x of
429 Impl x1 -> put x1
430 get
431 = do x1 <- get
432 return (Impl x1)
434instance (Binary b) => Binary (Binder b) where
435 put x
436 = case x of
437 Lam x1 -> do putWord8 0
438 put x1
439 Pi x1 x2 x3 -> do putWord8 1
440 put x1
441 put x2
442 put x3
443 Let x1 x2 -> do putWord8 2
444 put x1
445 put x2
446 NLet x1 x2 -> do putWord8 3
447 put x1
448 put x2
449 Hole x1 -> do putWord8 4
450 put x1
451 GHole x1 x2 -> do putWord8 5
452 put x1
453 put x2
454 Guess x1 x2 -> do putWord8 6
455 put x1
456 put x2
457 PVar x1 -> do putWord8 7
458 put x1
459 PVTy x1 -> do putWord8 8
460 put x1
461 get
462 = do i <- getWord8
463 case i of
464 0 -> do x1 <- get
465 return (Lam x1)
466 1 -> do x1 <- get
467 x2 <- get
468 x3 <- get
469 return (Pi x1 x2 x3)
470 2 -> do x1 <- get
471 x2 <- get
472 return (Let x1 x2)
473 3 -> do x1 <- get
474 x2 <- get
475 return (NLet x1 x2)
476 4 -> do x1 <- get
477 return (Hole x1)
478 5 -> do x1 <- get
479 x2 <- get
480 return (GHole x1 x2)
481 6 -> do x1 <- get
482 x2 <- get
483 return (Guess x1 x2)
484 7 -> do x1 <- get
485 return (PVar x1)
486 8 -> do x1 <- get
487 return (PVTy x1)
488 _ -> error "Corrupted binary data for Binder"
491instance Binary Universe where
492 put x = case x of
493 UniqueType -> putWord8 0
494 AllTypes -> putWord8 1
495 NullType -> putWord8 2
496 get = do i <- getWord8
497 case i of
498 0 -> return UniqueType
499 1 -> return AllTypes
500 2 -> return NullType
501 _ -> error "Corrupted binary data for Universe"
503instance Binary NameType where
504 put x
505 = case x of
506 Bound -> putWord8 0
507 Ref -> putWord8 1
508 DCon x1 x2 x3 -> do putWord8 2
509 put (x1 * 65536 + x2)
510 put x3
511 TCon x1 x2 -> do putWord8 3
512 put (x1 * 65536 + x2)
513 get
514 = do i <- getWord8
515 case i of
516 0 -> return Bound
517 1 -> return Ref
518 2 -> do x1x2 <- get
519 x3 <- get
520 return (DCon (x1x2 `div` 65536) (x1x2 `mod` 65536) x3)
521 3 -> do x1x2 <- get
522 return (TCon (x1x2 `div` 65536) (x1x2 `mod` 65536))
523 _ -> error "Corrupted binary data for NameType"
525-- record concrete levels only, for now
526instance Binary UExp where
527 put x = case x of
528 UVar t -> do putWord8 0
529 put ((-1) :: Int) -- TMP HACK!
530 UVal t -> do putWord8 1
531 put t
533 get = do i <- getWord8
534 case i of
535 0 -> do x1 <- get
536 return (UVar x1)
537 1 -> do x1 <- get
538 return (UVal x1)
539 _ -> error "Corrupted binary data for UExp"
541instance {- (Binary n) => -} Binary (TT Name) where
542 put x
543 = {-# SCC "putTT" #-}
544 case x of
545 P x1 x2 x3 -> do putWord8 0
546 put x1
547 put x2
548-- put x3
549 V x1 -> if (x1 >= 0 && x1 < 256)
550 then do putWord8 1
551 putWord8 (toEnum (x1 + 1))
552 else do putWord8 9
553 put x1
554 Bind x1 x2 x3 -> do putWord8 2
555 put x1
556 put x2
557 put x3
558 App x1 x2 -> do putWord8 3
559 put x1
560 put x2
561 Constant x1 -> do putWord8 4
562 put x1
563 Proj x1 x2 -> do putWord8 5
564 put x1
565 putWord8 (toEnum (x2 + 1))
566 Erased -> putWord8 6
567 TType x1 -> do putWord8 7
568 put x1
569 Impossible -> putWord8 8
570 UType x1 -> do putWord8 10
571 put x1
572 get
573 = do i <- getWord8
574 case i of
575 0 -> do x1 <- get
576 x2 <- get
577-- x3 <- get
578 return (P x1 x2 Erased)
579 1 -> do x1 <- getWord8
580 return (V ((fromEnum x1) - 1))
581 2 -> do x1 <- get
582 x2 <- get
583 x3 <- get
584 return (Bind x1 x2 x3)
585 3 -> do x1 <- get
586 x2 <- get
587 return (App x1 x2)
588 4 -> do x1 <- get
589 return (Constant x1)
590 5 -> do x1 <- get
591 x2 <- getWord8
592 return (Proj x1 ((fromEnum x2)-1))
593 6 -> return Erased
594 7 -> do x1 <- get
595 return (TType x1)
596 8 -> return Impossible
597 9 -> do x1 <- get
598 return (V x1)
599 10 -> do x1 <- get
600 return (UType x1)
601 _ -> error "Corrupted binary data for TT"