git.iko.soy/Idris-dev
on 7afa310 help sign in
Idris-dev/src/Idris/Core/Binary.hs
382 lines 14 kB history raw
1{-| Binary instances for the core datatypes -}
2module Idris.Core.Binary where
4import Data.Binary
5import Data.Vector.Binary
6import qualified Data.Text as T
8import Idris.Core.TT
10----- Generated by 'derive'
12instance Binary FC where
13 put (FC x1 (x2, x3) (x4, x5))
14 = do put x1
15 put (x2 * 65536 + x3)
16 put (x4 * 65536 + x5)
17 get
18 = do x1 <- get
19 x2x3 <- get
20 x4x5 <- get
21 return (FC x1 (x2x3 `div` 65536, x2x3 `mod` 65536) (x4x5 `div` 65536, x4x5 `mod` 65536))
24instance Binary Name where
25 put x
26 = case x of
27 UN x1 -> do putWord8 0
28 put x1
29 NS x1 x2 -> do putWord8 1
30 put x1
31 put x2
32 MN x1 x2 -> do putWord8 2
33 put x1
34 put x2
35 NErased -> putWord8 3
36 SN x1 -> do putWord8 4
37 put x1
38 SymRef x1 -> do putWord8 5
39 put x1
40 get
41 = do i <- getWord8
42 case i of
43 0 -> do x1 <- get
44 return (UN x1)
45 1 -> do x1 <- get
46 x2 <- get
47 return (NS x1 x2)
48 2 -> do x1 <- get
49 x2 <- get
50 return (MN x1 x2)
51 3 -> return NErased
52 4 -> do x1 <- get
53 return (SN x1)
54 5 -> do x1 <- get
55 return (SymRef x1)
56 _ -> error "Corrupted binary data for Name"
58instance Binary T.Text where
59 put x = put (str x)
60 get = do x <- get
61 return (txt x)
63instance Binary SpecialName where
64 put x
65 = case x of
66 WhereN x1 x2 x3 -> do putWord8 0
67 put x1
68 put x2
69 put x3
70 InstanceN x1 x2 -> do putWord8 1
71 put x1
72 put x2
73 ParentN x1 x2 -> do putWord8 2
74 put x1
75 put x2
76 MethodN x1 -> do putWord8 3
77 put x1
78 CaseN x1 -> do putWord8 4; put x1
79 ElimN x1 -> do putWord8 5; put x1
80 InstanceCtorN x1 -> do putWord8 6; put x1
81 WithN x1 x2 -> do putWord8 7
82 put x1
83 put x2
84 get
85 = do i <- getWord8
86 case i of
87 0 -> do x1 <- get
88 x2 <- get
89 x3 <- get
90 return (WhereN x1 x2 x3)
91 1 -> do x1 <- get
92 x2 <- get
93 return (InstanceN x1 x2)
94 2 -> do x1 <- get
95 x2 <- get
96 return (ParentN x1 x2)
97 3 -> do x1 <- get
98 return (MethodN x1)
99 4 -> do x1 <- get
100 return (CaseN x1)
101 5 -> do x1 <- get
102 return (ElimN x1)
103 6 -> do x1 <- get
104 return (InstanceCtorN x1)
105 7 -> do x1 <- get
106 x2 <- get
107 return (WithN x1 x2)
108 _ -> error "Corrupted binary data for SpecialName"
111instance Binary Const where
112 put x
113 = case x of
114 I x1 -> do putWord8 0
115 put x1
116 BI x1 -> do putWord8 1
117 put x1
118 Fl x1 -> do putWord8 2
119 put x1
120 Ch x1 -> do putWord8 3
121 put x1
122 Str x1 -> do putWord8 4
123 put x1
124 B8 x1 -> putWord8 5 >> put x1
125 B16 x1 -> putWord8 6 >> put x1
126 B32 x1 -> putWord8 7 >> put x1
127 B64 x1 -> putWord8 8 >> put x1
129 (AType (ATInt ITNative)) -> putWord8 9
130 (AType (ATInt ITBig)) -> putWord8 10
131 (AType ATFloat) -> putWord8 11
132 (AType (ATInt ITChar)) -> putWord8 12
133 StrType -> putWord8 13
134 PtrType -> putWord8 14
135 Forgot -> putWord8 15
136 (AType (ATInt (ITFixed ity))) -> putWord8 (fromIntegral (16 + fromEnum ity)) -- 16-19 inclusive
137 (AType (ATInt (ITVec ity count))) -> do
138 putWord8 20
139 putWord8 (fromIntegral . fromEnum $ ity)
140 putWord8 (fromIntegral count)
142 B8V x1 -> putWord8 21 >> put x1
143 B16V x1 -> putWord8 22 >> put x1
144 B32V x1 -> putWord8 23 >> put x1
145 B64V x1 -> putWord8 24 >> put x1
146 BufferType -> putWord8 25
147 ManagedPtrType -> putWord8 26
148 get
149 = do i <- getWord8
150 case i of
151 0 -> do x1 <- get
152 return (I x1)
153 1 -> do x1 <- get
154 return (BI x1)
155 2 -> do x1 <- get
156 return (Fl x1)
157 3 -> do x1 <- get
158 return (Ch x1)
159 4 -> do x1 <- get
160 return (Str x1)
161 5 -> fmap B8 get
162 6 -> fmap B16 get
163 7 -> fmap B32 get
164 8 -> fmap B64 get
166 9 -> return (AType (ATInt ITNative))
167 10 -> return (AType (ATInt ITBig))
168 11 -> return (AType ATFloat)
169 12 -> return (AType (ATInt ITChar))
170 13 -> return StrType
171 14 -> return PtrType
172 15 -> return Forgot
174 16 -> return (AType (ATInt (ITFixed IT8)))
175 17 -> return (AType (ATInt (ITFixed IT16)))
176 18 -> return (AType (ATInt (ITFixed IT32)))
177 19 -> return (AType (ATInt (ITFixed IT64)))
179 20 -> do
180 e <- getWord8
181 c <- getWord8
182 return (AType (ATInt (ITVec (toEnum . fromIntegral $ e) (fromIntegral c))))
184 21 -> fmap B8V get
185 22 -> fmap B16V get
186 23 -> fmap B32V get
187 24 -> fmap B64V get
188 25 -> return BufferType
189 26 -> return ManagedPtrType
191 _ -> error "Corrupted binary data for Const"
194instance Binary Raw where
195 put x
196 = case x of
197 Var x1 -> do putWord8 0
198 put x1
199 RBind x1 x2 x3 -> do putWord8 1
200 put x1
201 put x2
202 put x3
203 RApp x1 x2 -> do putWord8 2
204 put x1
205 put x2
206 RType -> putWord8 3
207 RConstant x1 -> do putWord8 4
208 put x1
209 RForce x1 -> do putWord8 5
210 put x1
211 get
212 = do i <- getWord8
213 case i of
214 0 -> do x1 <- get
215 return (Var x1)
216 1 -> do x1 <- get
217 x2 <- get
218 x3 <- get
219 return (RBind x1 x2 x3)
220 2 -> do x1 <- get
221 x2 <- get
222 return (RApp x1 x2)
223 3 -> return RType
224 4 -> do x1 <- get
225 return (RConstant x1)
226 5 -> do x1 <- get
227 return (RForce x1)
228 _ -> error "Corrupted binary data for Raw"
231instance (Binary b) => Binary (Binder b) where
232 put x
233 = case x of
234 Lam x1 -> do putWord8 0
235 put x1
236 Pi x1 x2 -> do putWord8 1
237 put x1
238 put x2
239 Let x1 x2 -> do putWord8 2
240 put x1
241 put x2
242 NLet x1 x2 -> do putWord8 3
243 put x1
244 put x2
245 Hole x1 -> do putWord8 4
246 put x1
247 GHole x1 x2 -> do putWord8 5
248 put x1
249 put x2
250 Guess x1 x2 -> do putWord8 6
251 put x1
252 put x2
253 PVar x1 -> do putWord8 7
254 put x1
255 PVTy x1 -> do putWord8 8
256 put x1
257 get
258 = do i <- getWord8
259 case i of
260 0 -> do x1 <- get
261 return (Lam x1)
262 1 -> do x1 <- get
263 x2 <- get
264 return (Pi x1 x2)
265 2 -> do x1 <- get
266 x2 <- get
267 return (Let x1 x2)
268 3 -> do x1 <- get
269 x2 <- get
270 return (NLet x1 x2)
271 4 -> do x1 <- get
272 return (Hole x1)
273 5 -> do x1 <- get
274 x2 <- get
275 return (GHole x1 x2)
276 6 -> do x1 <- get
277 x2 <- get
278 return (Guess x1 x2)
279 7 -> do x1 <- get
280 return (PVar x1)
281 8 -> do x1 <- get
282 return (PVTy x1)
283 _ -> error "Corrupted binary data for Binder"
286instance Binary Universe where
287 put x = case x of
288 UniqueType -> putWord8 0
289 AllTypes -> putWord8 1
290 NullType -> putWord8 2
291 get = do i <- getWord8
292 case i of
293 0 -> return UniqueType
294 1 -> return AllTypes
295 2 -> return NullType
296 _ -> error "Corrupted binary data for Universe"
298instance Binary NameType where
299 put x
300 = case x of
301 Bound -> putWord8 0
302 Ref -> putWord8 1
303 DCon x1 x2 x3 -> do putWord8 2
304 put (x1 * 65536 + x2)
305 put x3
306 TCon x1 x2 -> do putWord8 3
307 put (x1 * 65536 + x2)
308 get
309 = do i <- getWord8
310 case i of
311 0 -> return Bound
312 1 -> return Ref
313 2 -> do x1x2 <- get
314 x3 <- get
315 return (DCon (x1x2 `div` 65536) (x1x2 `mod` 65536) x3)
316 3 -> do x1x2 <- get
317 return (TCon (x1x2 `div` 65536) (x1x2 `mod` 65536))
318 _ -> error "Corrupted binary data for NameType"
321instance {- (Binary n) => -} Binary (TT Name) where
322 put x
323 = {-# SCC "putTT" #-}
324 case x of
325 P x1 x2 x3 -> do putWord8 0
326 put x1
327 put x2
328-- put x3
329 V x1 -> if (x1 >= 0 && x1 < 256)
330 then do putWord8 1
331 putWord8 (toEnum (x1 + 1))
332 else do putWord8 9
333 put x1
334 Bind x1 x2 x3 -> do putWord8 2
335 put x1
336 put x2
337 put x3
338 App x1 x2 -> do putWord8 3
339 put x1
340 put x2
341 Constant x1 -> do putWord8 4
342 put x1
343 Proj x1 x2 -> do putWord8 5
344 put x1
345 putWord8 (toEnum (x2 + 1))
346 Erased -> putWord8 6
347 TType x1 -> do putWord8 7
348 put x1
349 Impossible -> putWord8 8
350 UType x1 -> do putWord8 10
351 put x1
352 get
353 = do i <- getWord8
354 case i of
355 0 -> do x1 <- get
356 x2 <- get
357-- x3 <- get
358 return (P x1 x2 Erased)
359 1 -> do x1 <- getWord8
360 return (V ((fromEnum x1) - 1))
361 2 -> do x1 <- get
362 x2 <- get
363 x3 <- get
364 return (Bind x1 x2 x3)
365 3 -> do x1 <- get
366 x2 <- get
367 return (App x1 x2)
368 4 -> do x1 <- get
369 return (Constant x1)
370 5 -> do x1 <- get
371 x2 <- getWord8
372 return (Proj x1 ((fromEnum x2)-1))
373 6 -> return Erased
374 7 -> do x1 <- get
375 return (TType x1)
376 8 -> return Impossible
377 9 -> do x1 <- get
378 return (V x1)
379 10 -> do x1 <- get
380 return (UType x1)
381 _ -> error "Corrupted binary data for TT"