git.iko.soy/Idris-dev
on bc8da8d help sign in
Idris-dev/src/Idris/Core/Binary.hs
374 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 (NoEliminator s t) = do putWord8 37
137 put s
138 put t
139 put (InvalidTCArg n t) = do putWord8 38
140 put n
141 put t
142 put (ElabScriptStuck x1) = do putWord8 39
143 put x1
144 put (UnknownImplicit n f) = do putWord8 40
145 put n
146 put f
147 put (NoValidAlts ns) = do putWord8 41
148 put ns
149 put (RunningElabScript e) = do putWord8 42
150 put e
151 put (ElabScriptStaging n) = do putWord8 43
152 put n
153 put (FancyMsg xs) = do putWord8 44
154 put xs
155 get = do i <- getWord8
156 case i of
157 0 -> fmap Msg get
158 1 -> fmap InternalMsg get
159 2 -> do x <- get ; y <- get ; z <- get ; e <- get ; ctxt <- get ; i <- get
160 return $ CantUnify x y z e ctxt i
161 3 -> do x <- get ; y <- get ; z <- get
162 return $ InfiniteUnify x y z
163 4 -> do x <- get ; y <- get ; z <- get
164 return $ CantConvert x y z
165 5 -> do x <- get ; y <- get
166 return $ CantSolveGoal x y
167 6 -> do w <- get ; x <- get ; y <- get ; z <- get
168 return $ UnifyScope w x y z
169 7 -> fmap CantInferType get
170 8 -> do x <- get ; y <- get
171 return $ NonFunctionType x y
172 9 -> do x <- get ; y <- get
173 return $ NotEquality x y
174 10 -> fmap TooManyArguments get
175 11 -> fmap CantIntroduce get
176 12 -> fmap NoSuchVariable get
177 13 -> fmap NoTypeDecl get
178 14 -> do x <- get ; y <- get ; z <- get
179 return $ NotInjective x y z
180 15 -> CantResolve False <$> get <*> get
181 16 -> fmap CantResolveAlts get
182 17 -> fmap IncompleteTerm get
183 18 -> UniverseError <$> get <*> get <*> get <*> get <*> get
184 19 -> do x <- get ; y <- get
185 return $ UniqueError x y
186 20 -> do x <- get ; y <- get
187 return $ UniqueKindError x y
188 21 -> return ProgramLineComment
189 22 -> fmap Inaccessible get
190 23 -> fmap NonCollapsiblePostulate get
191 24 -> fmap AlreadyDefined get
192 25 -> fmap ProofSearchFail get
193 26 -> do l <- get; r <- get; t <- get
194 return $ NoRewriting l r t
195 27 -> do x <- get ; y <- get
196 return $ At x y
197 28 -> do w <- get; x <- get ; y <- get ; z <- get
198 return $ Elaborating w 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 (ElabScriptDebug 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 39 -> do x1 <- get
221 return (ElabScriptStuck x1)
222 40 -> do x <- get ; y <- get
223 return $ UnknownImplicit x y
224 41 -> fmap NoValidAlts get
225 42 -> fmap RunningElabScript get
226 43 -> fmap ElabScriptStaging get
227 44 -> fmap FancyMsg get
228 _ -> error "Corrupted binary data for Err'"
229----- Generated by 'derive'
231instance Binary FC
232instance Binary FC'
233instance Binary Name
234instance Binary SpecialName
235instance Binary Const where
236 put x
237 = case x of
238 I x1 -> do putWord8 0
239 put x1
240 BI x1 -> do putWord8 1
241 put x1
242 Fl x1 -> do putWord8 2
243 putDoublele x1
244 Ch x1 -> do putWord8 3
245 put x1
246 Str x1 -> do putWord8 4
247 put x1
248 B8 x1 -> putWord8 5 >> put x1
249 B16 x1 -> putWord8 6 >> put x1
250 B32 x1 -> putWord8 7 >> put x1
251 B64 x1 -> putWord8 8 >> put x1
253 (AType (ATInt ITNative)) -> putWord8 9
254 (AType (ATInt ITBig)) -> putWord8 10
255 (AType ATFloat) -> putWord8 11
256 (AType (ATInt ITChar)) -> putWord8 12
257 StrType -> putWord8 13
258 Forgot -> putWord8 15
259 (AType (ATInt (ITFixed ity))) -> putWord8 (fromIntegral (16 + fromEnum ity)) -- 16-19 inclusive
260 VoidType -> putWord8 27
261 WorldType -> putWord8 28
262 TheWorld -> putWord8 29
263 get
264 = do i <- getWord8
265 case i of
266 0 -> do x1 <- get
267 return (I x1)
268 1 -> do x1 <- get
269 return (BI x1)
270 2 -> do x1 <- getDoublele
271 return (Fl x1)
272 3 -> do x1 <- get
273 return (Ch x1)
274 4 -> do x1 <- get
275 return (Str x1)
276 5 -> fmap B8 get
277 6 -> fmap B16 get
278 7 -> fmap B32 get
279 8 -> fmap B64 get
281 9 -> return (AType (ATInt ITNative))
282 10 -> return (AType (ATInt ITBig))
283 11 -> return (AType ATFloat)
284 12 -> return (AType (ATInt ITChar))
285 13 -> return StrType
286 15 -> return Forgot
288 16 -> return (AType (ATInt (ITFixed IT8)))
289 17 -> return (AType (ATInt (ITFixed IT16)))
290 18 -> return (AType (ATInt (ITFixed IT32)))
291 19 -> return (AType (ATInt (ITFixed IT64)))
293 27 -> return VoidType
294 28 -> return WorldType
295 29 -> return TheWorld
296 _ -> error "Corrupted binary data for Const"
298instance Binary Raw
299instance Binary RigCount
300instance Binary ImplicitInfo where
301 put x
302 = case x of
303 Impl x1 x2 x3 -> do put x1; put x2
304 get
305 = do x1 <- get
306 x2 <- get
307 return (Impl x1 x2 False)
309instance (Binary b) => Binary (Binder b)
310instance Binary Universe
311instance Binary NameType
312instance Binary UExp
313instance Binary (TT Name) where
314 put x
315 = {-# SCC "putTT" #-}
316 case x of
317 P x1 x2 x3 -> do putWord8 0
318 put x1
319 put x2
320-- put x3
321 V x1 -> if (x1 >= 0 && x1 < 256)
322 then do putWord8 1
323 putWord8 (toEnum (x1 + 1))
324 else do putWord8 9
325 put x1
326 Bind x1 x2 x3 -> do putWord8 2
327 put x1
328 put x2
329 put x3
330 App _ x1 x2 -> do putWord8 3
331 put x1
332 put x2
333 Constant x1 -> do putWord8 4
334 put x1
335 Proj x1 x2 -> do putWord8 5
336 put x1
337 putWord8 (toEnum (x2 + 1))
338 Erased -> putWord8 6
339 TType x1 -> do putWord8 7
340 put x1
341 Impossible -> putWord8 8
342 Inferred x1 -> put x1 -- drop the 'Inferred'
343 UType x1 -> do putWord8 10
344 put x1
345 get
346 = do i <- getWord8
347 case i of
348 0 -> do x1 <- get
349 x2 <- get
350-- x3 <- get
351 return (P x1 x2 Erased)
352 1 -> do x1 <- getWord8
353 return (V ((fromEnum x1) - 1))
354 2 -> do x1 <- get
355 x2 <- get
356 x3 <- get
357 return (Bind x1 x2 x3)
358 3 -> do x1 <- get
359 x2 <- get
360 return (App Complete x1 x2)
361 4 -> do x1 <- get
362 return (Constant x1)
363 5 -> do x1 <- get
364 x2 <- getWord8
365 return (Proj x1 ((fromEnum x2)-1))
366 6 -> return Erased
367 7 -> do x1 <- get
368 return (TType x1)
369 8 -> return Impossible
370 9 -> do x1 <- get
371 return (V x1)
372 10 -> do x1 <- get
373 return (UType x1)
374 _ -> error "Corrupted binary data for TT"