@@ -1,3 +1,5 @@
1+{-# OPTIONS_GHC -fwarn-incomplete-patterns -Werror #-}
2+
13{-| Binary instances for the core datatypes -}
24module Idris.Core.Binary where
35
@@ -7,6 +9,169 @@ import qualified Data.Text as T
79
810import Idris.Core.TT
911
12+instance 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
17+
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"
25+
26+instance 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+
122+ get = do i <- getWord8
123+ case i of
124+ 0 -> fmap Msg get
125+ 1 -> fmap InternalMsg get
126+ 2 -> do x <- get ; y <- get ; z <- get ; e <- get ; ctxt <- get ; i <- get
127+ return $ CantUnify x y z e ctxt i
128+ 3 -> do x <- get ; y <- get ; z <- get
129+ return $ InfiniteUnify x y z
130+ 4 -> do x <- get ; y <- get ; z <- get
131+ return $ CantConvert x y z
132+ 5 -> do x <- get ; y <- get
133+ return $ CantSolveGoal x y
134+ 6 -> do w <- get ; x <- get ; y <- get ; z <- get
135+ return $ UnifyScope w x y z
136+ 7 -> fmap CantInferType get
137+ 8 -> do x <- get ; y <- get
138+ return $ NonFunctionType x y
139+ 9 -> do x <- get ; y <- get
140+ return $ NotEquality x y
141+ 10 -> fmap TooManyArguments get
142+ 11 -> fmap CantIntroduce get
143+ 12 -> fmap NoSuchVariable get
144+ 13 -> fmap NoTypeDecl get
145+ 14 -> do x <- get ; y <- get ; z <- get
146+ return $ NotInjective x y z
147+ 15 -> fmap CantResolve get
148+ 16 -> fmap CantResolveAlts get
149+ 17 -> fmap IncompleteTerm get
150+ 18 -> return UniverseError
151+ 19 -> do x <- get ; y <- get
152+ return $ UniqueError x y
153+ 20 -> do x <- get ; y <- get
154+ return $ UniqueKindError x y
155+ 21 -> return ProgramLineComment
156+ 22 -> fmap Inaccessible get
157+ 23 -> fmap NonCollapsiblePostulate get
158+ 24 -> fmap AlreadyDefined get
159+ 25 -> fmap ProofSearchFail get
160+ 26 -> fmap NoRewriting get
161+ 27 -> do x <- get ; y <- get
162+ return $ At x y
163+ 28 -> do x <- get ; y <- get ; z <- get
164+ return $ Elaborating x y z
165+ 29 -> do w <- get ; x <- get ; y <- get ; z <- get
166+ return $ ElaboratingArg w x y z
167+ 30 -> fmap ProviderError get
168+ 31 -> do x <- get ; y <- get
169+ return $ LoadingFailed x y
170+ 32 -> do x <- get ; y <- get
171+ return $ ReflectionError x y
172+ 33 -> do x <- get ; y <- get
173+ return $ ReflectionFailed x y
174+ _ -> error "Corrupted binary data for Err'"
10175----- Generated by 'derive'
11176
12177instance Binary FC where
@@ -145,6 +310,7 @@ instance Binary Const where
145310 B64V x1 -> putWord8 24 >> put x1
146311 BufferType -> putWord8 25
147312 ManagedPtrType -> putWord8 26
313+ VoidType -> putWord8 27
148314 get
149315 = do i <- getWord8
150316 case i of
@@ -187,7 +353,7 @@ instance Binary Const where
187353 24 -> fmap B64V get
188354 25 -> return BufferType
189355 26 -> return ManagedPtrType
190−
356+ 27 -> return VoidType
191357 _ -> error "Corrupted binary data for Const"
192358
193359
@@ -208,6 +374,8 @@ instance Binary Raw where
208374 put x1
209375 RForce x1 -> do putWord8 5
210376 put x1
377+ RUType x1 -> do putWord8 6
378+ put x1
211379 get
212380 = do i <- getWord8
213381 case i of
@@ -225,6 +393,8 @@ instance Binary Raw where
225393 return (RConstant x1)
226394 5 -> do x1 <- get
227395 return (RForce x1)
396+ 6 -> do x1 <- get
397+ return (RUType x1)
228398 _ -> error "Corrupted binary data for Raw"
229399
230400