git.iko.soy/Idris-dev
on 1b71663 help sign in
Idris-dev/src/Idris/Core/Binary.hs
368 lines 15 kB history raw
1{-|
2Module : Idris.Core.Binary
3Description : Binary instances for the core datatypes
5License : BSD3
6Maintainer : The Idris Community.
7-}
8{-# LANGUAGE FlexibleInstances #-}
10{-# OPTIONS_GHC -fwarn-incomplete-patterns #-}
11module Idris.Core.Binary where
13import Idris.Core.TT
15import Control.Applicative ((<$>), (<*>))
16import Data.Binary
17import Data.Binary.Get
18import Data.Binary.Put
20instance Binary ErrorReportPart
21instance Binary Provenance
22instance Binary UConstraint
23instance Binary ConstraintFC
24instance Binary a => Binary (Err' a) where
25 put (Msg str) = do putWord8 0
26 put str
27 put (InternalMsg str) = do putWord8 1
28 put str
29 put (CantUnify x y z e ctxt i) = do putWord8 2
30 put x
31 put y
32 put z
33 put e
34 put ctxt
35 put i
36 put (InfiniteUnify n t ctxt) = do putWord8 3
37 put n
38 put t
39 put ctxt
40 put (CantConvert x y ctxt) = do putWord8 4
41 put x
42 put y
43 put ctxt
44 put (CantSolveGoal x ctxt) = do putWord8 5
45 put x
46 put ctxt
47 put (UnifyScope n1 n2 x ctxt) = do putWord8 6
48 put n1
49 put n2
50 put x
51 put ctxt
52 put (CantInferType str) = do putWord8 7
53 put str
54 put (NonFunctionType t1 t2) = do putWord8 8
55 put t1
56 put t2
57 put (NotEquality t1 t2) = do putWord8 9
58 put t1
59 put t2
60 put (TooManyArguments n) = do putWord8 10
61 put n
62 put (CantIntroduce t) = do putWord8 11
63 put t
64 put (NoSuchVariable n) = do putWord8 12
65 put n
66 put (NoTypeDecl n) = do putWord8 13
67 put n
68 put (NotInjective x y z) = do putWord8 14
69 put x
70 put y
71 put z
72 put (CantResolve _ t u) = do putWord8 15
73 put t
74 put u
75 put (CantResolveAlts ns) = do putWord8 16
76 put ns
77 put (IncompleteTerm t) = do putWord8 17
78 put t
79 put (UniverseError x1 x2 x3 x4 x5) = do putWord8 18
80 put x1
81 put x2
82 put x3
83 put x4
84 put x5
85 put (UniqueError u n) = do putWord8 19
86 put u
87 put n
88 put (UniqueKindError u n) = do putWord8 20
89 put u
90 put n
91 put ProgramLineComment = putWord8 21
92 put (Inaccessible n) = do putWord8 22
93 put n
94 put (NonCollapsiblePostulate n) = do putWord8 23
95 put n
96 put (AlreadyDefined n) = do putWord8 24
97 put n
98 put (ProofSearchFail e) = do putWord8 25
99 put e
100 put (NoRewriting l r t) = do putWord8 26
101 put l
102 put r
103 put t
104 put (At fc e) = do putWord8 27
105 put fc
106 put e
107 put (Elaborating str n ty e) = do putWord8 28
108 put str
109 put n
110 put ty
111 put e
112 put (ElaboratingArg n1 n2 ns e) = do putWord8 29
113 put n1
114 put n2
115 put ns
116 put e
117 put (ProviderError str) = do putWord8 30
118 put str
119 put (LoadingFailed str e) = do putWord8 31
120 put str
121 put e
122 put (ReflectionError parts e) = do putWord8 32
123 put parts
124 put e
125 put (ReflectionFailed str e) = do putWord8 33
126 put str
127 put e
128 put (WithFnType t) = do putWord8 34
129 put t
130 put (CantMatch t) = do putWord8 35
131 put t
132 put (ElabScriptDebug x1 x2 x3) = do putWord8 36
133 put x1
134 put x2
135 put x3
136 put (InvalidTCArg n t) = do putWord8 38
137 put n
138 put t
139 put (ElabScriptStuck x1) = do putWord8 39
140 put x1
141 put (UnknownImplicit n f) = do putWord8 40
142 put n
143 put f
144 put (NoValidAlts ns) = do putWord8 41
145 put ns
146 put (RunningElabScript e) = do putWord8 42
147 put e
148 put (ElabScriptStaging n) = do putWord8 43
149 put n
150 put (FancyMsg xs) = do putWord8 44
151 put xs
152 get = do i <- getWord8
153 case i of
154 0 -> fmap Msg get
155 1 -> fmap InternalMsg get
156 2 -> do x <- get ; y <- get ; z <- get ; e <- get ; ctxt <- get ; i <- get
157 return $ CantUnify x y z e ctxt i
158 3 -> do x <- get ; y <- get ; z <- get
159 return $ InfiniteUnify x y z
160 4 -> do x <- get ; y <- get ; z <- get
161 return $ CantConvert x y z
162 5 -> do x <- get ; y <- get
163 return $ CantSolveGoal x y
164 6 -> do w <- get ; x <- get ; y <- get ; z <- get
165 return $ UnifyScope w x y z
166 7 -> fmap CantInferType get
167 8 -> do x <- get ; y <- get
168 return $ NonFunctionType x y
169 9 -> do x <- get ; y <- get
170 return $ NotEquality x y
171 10 -> fmap TooManyArguments get
172 11 -> fmap CantIntroduce get
173 12 -> fmap NoSuchVariable get
174 13 -> fmap NoTypeDecl get
175 14 -> do x <- get ; y <- get ; z <- get
176 return $ NotInjective x y z
177 15 -> CantResolve False <$> get <*> get
178 16 -> fmap CantResolveAlts get
179 17 -> fmap IncompleteTerm get
180 18 -> UniverseError <$> get <*> get <*> get <*> get <*> get
181 19 -> do x <- get ; y <- get
182 return $ UniqueError x y
183 20 -> do x <- get ; y <- get
184 return $ UniqueKindError x y
185 21 -> return ProgramLineComment
186 22 -> fmap Inaccessible get
187 23 -> fmap NonCollapsiblePostulate get
188 24 -> fmap AlreadyDefined get
189 25 -> fmap ProofSearchFail get
190 26 -> do l <- get; r <- get; t <- get
191 return $ NoRewriting l r t
192 27 -> do x <- get ; y <- get
193 return $ At x y
194 28 -> do w <- get; x <- get ; y <- get ; z <- get
195 return $ Elaborating w x y z
196 29 -> do w <- get ; x <- get ; y <- get ; z <- get
197 return $ ElaboratingArg w x y z
198 30 -> fmap ProviderError get
199 31 -> do x <- get ; y <- get
200 return $ LoadingFailed x y
201 32 -> do x <- get ; y <- get
202 return $ ReflectionError x y
203 33 -> do x <- get ; y <- get
204 return $ ReflectionFailed x y
205 34 -> fmap WithFnType get
206 35 -> fmap CantMatch get
207 36 -> do x1 <- get
208 x2 <- get
209 x3 <- get
210 return (ElabScriptDebug x1 x2 x3)
211 38 -> do x1 <- get
212 x2 <- get
213 return (InvalidTCArg x1 x2)
214 39 -> do x1 <- get
215 return (ElabScriptStuck x1)
216 40 -> do x <- get ; y <- get
217 return $ UnknownImplicit x y
218 41 -> fmap NoValidAlts get
219 42 -> fmap RunningElabScript get
220 43 -> fmap ElabScriptStaging get
221 44 -> fmap FancyMsg get
222 _ -> error "Corrupted binary data for Err'"
223----- Generated by 'derive'
225instance Binary FC
226instance Binary FC'
227instance Binary Name
228instance Binary SpecialName
229instance Binary Const where
230 put x
231 = case x of
232 I x1 -> do putWord8 0
233 put x1
234 BI x1 -> do putWord8 1
235 put x1
236 Fl x1 -> do putWord8 2
237 putDoublele x1
238 Ch x1 -> do putWord8 3
239 put x1
240 Str x1 -> do putWord8 4
241 put x1
242 B8 x1 -> putWord8 5 >> put x1
243 B16 x1 -> putWord8 6 >> put x1
244 B32 x1 -> putWord8 7 >> put x1
245 B64 x1 -> putWord8 8 >> put x1
247 (AType (ATInt ITNative)) -> putWord8 9
248 (AType (ATInt ITBig)) -> putWord8 10
249 (AType ATFloat) -> putWord8 11
250 (AType (ATInt ITChar)) -> putWord8 12
251 StrType -> putWord8 13
252 Forgot -> putWord8 15
253 (AType (ATInt (ITFixed ity))) -> putWord8 (fromIntegral (16 + fromEnum ity)) -- 16-19 inclusive
254 VoidType -> putWord8 27
255 WorldType -> putWord8 28
256 TheWorld -> putWord8 29
257 get
258 = do i <- getWord8
259 case i of
260 0 -> do x1 <- get
261 return (I x1)
262 1 -> do x1 <- get
263 return (BI x1)
264 2 -> do x1 <- getDoublele
265 return (Fl x1)
266 3 -> do x1 <- get
267 return (Ch x1)
268 4 -> do x1 <- get
269 return (Str x1)
270 5 -> fmap B8 get
271 6 -> fmap B16 get
272 7 -> fmap B32 get
273 8 -> fmap B64 get
275 9 -> return (AType (ATInt ITNative))
276 10 -> return (AType (ATInt ITBig))
277 11 -> return (AType ATFloat)
278 12 -> return (AType (ATInt ITChar))
279 13 -> return StrType
280 15 -> return Forgot
282 16 -> return (AType (ATInt (ITFixed IT8)))
283 17 -> return (AType (ATInt (ITFixed IT16)))
284 18 -> return (AType (ATInt (ITFixed IT32)))
285 19 -> return (AType (ATInt (ITFixed IT64)))
287 27 -> return VoidType
288 28 -> return WorldType
289 29 -> return TheWorld
290 _ -> error "Corrupted binary data for Const"
292instance Binary Raw
293instance Binary RigCount
294instance Binary ImplicitInfo where
295 put x
296 = case x of
297 Impl x1 x2 x3 -> do put x1; put x2
298 get
299 = do x1 <- get
300 x2 <- get
301 return (Impl x1 x2 False)
303instance (Binary b) => Binary (Binder b)
304instance Binary Universe
305instance Binary NameType
306instance Binary UExp
307instance Binary (TT Name) where
308 put x
309 = {-# SCC "putTT" #-}
310 case x of
311 P x1 x2 x3 -> do putWord8 0
312 put x1
313 put x2
314-- put x3
315 V x1 -> if (x1 >= 0 && x1 < 256)
316 then do putWord8 1
317 putWord8 (toEnum (x1 + 1))
318 else do putWord8 9
319 put x1
320 Bind x1 x2 x3 -> do putWord8 2
321 put x1
322 put x2
323 put x3
324 App _ x1 x2 -> do putWord8 3
325 put x1
326 put x2
327 Constant x1 -> do putWord8 4
328 put x1
329 Proj x1 x2 -> do putWord8 5
330 put x1
331 putWord8 (toEnum (x2 + 1))
332 Erased -> putWord8 6
333 TType x1 -> do putWord8 7
334 put x1
335 Impossible -> putWord8 8
336 Inferred x1 -> put x1 -- drop the 'Inferred'
337 UType x1 -> do putWord8 10
338 put x1
339 get
340 = do i <- getWord8
341 case i of
342 0 -> do x1 <- get
343 x2 <- get
344-- x3 <- get
345 return (P x1 x2 Erased)
346 1 -> do x1 <- getWord8
347 return (V ((fromEnum x1) - 1))
348 2 -> do x1 <- get
349 x2 <- get
350 x3 <- get
351 return (Bind x1 x2 x3)
352 3 -> do x1 <- get
353 x2 <- get
354 return (App Complete x1 x2)
355 4 -> do x1 <- get
356 return (Constant x1)
357 5 -> do x1 <- get
358 x2 <- getWord8
359 return (Proj x1 ((fromEnum x2)-1))
360 6 -> return Erased
361 7 -> do x1 <- get
362 return (TType x1)
363 8 -> return Impossible
364 9 -> do x1 <- get
365 return (V x1)
366 10 -> do x1 <- get
367 return (UType x1)
368 _ -> error "Corrupted binary data for TT"