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