@@ -13,63 +13,14 @@ module Idris.Core.Binary where
1313import Idris.Core.TT
1414
1515import Control.Applicative ((<$>), (<*>))
16−import Control.Monad (liftM2)
1716import Data.Binary
1817import Data.Binary.Get
1918import Data.Binary.Put
2019
21−instance Binary ErrorReportPart where
22− put (TextPart msg) = do putWord8 0 ; put msg
23− put (NamePart n) = do putWord8 1 ; put n
24− put (TermPart t) = do putWord8 2 ; put t
25− put (SubReport ps) = do putWord8 3 ; put ps
26− put (RawPart r) = do putWord8 4 ; put r
27−
28− get = do i <- getWord8
29− case i of
30− 0 -> fmap TextPart get
31− 1 -> fmap NamePart get
32− 2 -> fmap TermPart get
33− 3 -> fmap SubReport get
34− 4 -> fmap RawPart get
35− _ -> error "Corrupted binary data for ErrorReportPart"
36−
37−instance Binary Provenance where
38− put ExpectedType = putWord8 0
39− put (SourceTerm t) = do putWord8 1
40− put t
41− put InferredVal = putWord8 2
42− put GivenVal = putWord8 3
43− put (TooManyArgs t) = do putWord8 4
44− put t
45−
46− get = do i <- getWord8
47− case i of
48− 0 -> return ExpectedType
49− 1 -> do x1 <- get
50− return (SourceTerm x1)
51− 2 -> return InferredVal
52− 3 -> return GivenVal
53− 4 -> do x1 <- get
54− return (TooManyArgs x1)
55− _ -> error "Corrupted binary data for Provenance"
56−
57−instance Binary UConstraint where
58− put (ULT x1 x2) = putWord8 0 >> put x1 >> put x2
59− put (ULE x1 x2) = putWord8 1 >> put x1 >> put x2
60− get = do i <- getWord8
61− case i of
62− 0 -> ULT <$> get <*> get
63− 1 -> ULE <$> get <*> get
64− _ -> error "Corrupted binary data for UConstraint"
65−
66−instance Binary ConstraintFC where
67− put (ConstraintFC x1 x2) = putWord8 0 >> put x1 >> put x2
68− get = do i <- getWord8
69− case i of
70− 0 -> liftM2 ConstraintFC get get
71− _ -> error "Corrupted binary data for ConstraintFC"
72−
20+instance Binary ErrorReportPart
21+instance Binary Provenance
22+instance Binary UConstraint
23+instance Binary ConstraintFC
7324instance Binary a => Binary (Err' a) where
7425 put (Msg str) = do putWord8 0
7526 put str
@@ -277,119 +228,10 @@ instance Binary a => Binary (Err' a) where
277228 _ -> error "Corrupted binary data for Err'"
278229----- Generated by 'derive'
279230
280−instance Binary FC where
281− put x =
282− case x of
283− (FC x1 (x2, x3) (x4, x5)) -> do putWord8 0
284− put x1
285− put (x2 * 65536 + x3)
286− put (x4 * 65536 + x5)
287− NoFC -> putWord8 1
288− FileFC x1 -> do putWord8 2
289− put x1
290− get
291− = do i <- getWord8
292− case i of
293− 0 -> do x1 <- get
294− x2x3 <- get
295− x4x5 <- get
296− return (FC x1 (x2x3 `div` 65536, x2x3 `mod` 65536) (x4x5 `div` 65536, x4x5 `mod` 65536))
297− 1 -> return NoFC
298− 2 -> do x1 <- get
299− return (FileFC x1)
300− _ -> error "Corrupted binary data for FC"
301−
302−instance Binary FC' where
303− put (FC' fc) = put fc
304− get = fmap FC' get
305−
306−instance Binary Name where
307− put x
308− = case x of
309− UN x1 -> do putWord8 0
310− put x1
311− NS x1 x2 -> do putWord8 1
312− put x1
313− put x2
314− MN x1 x2 -> do putWord8 2
315− put x1
316− put x2
317− SN x1 -> do putWord8 3
318− put x1
319− SymRef x1 -> do putWord8 4
320− put x1
321− get
322− = do i <- getWord8
323− case i of
324− 0 -> do x1 <- get
325− return (UN x1)
326− 1 -> do x1 <- get
327− x2 <- get
328− return (NS x1 x2)
329− 2 -> do x1 <- get
330− x2 <- get
331− return (MN x1 x2)
332− 3 -> do x1 <- get
333− return (SN x1)
334− 4 -> do x1 <- get
335− return (SymRef x1)
336− _ -> error "Corrupted binary data for Name"
337−
338−instance Binary SpecialName where
339− put x
340− = case x of
341− WhereN x1 x2 x3 -> do putWord8 0
342− put x1
343− put x2
344− put x3
345− ImplementationN x1 x2 -> do putWord8 1
346− put x1
347− put x2
348− ParentN x1 x2 -> do putWord8 2
349− put x1
350− put x2
351− MethodN x1 -> do putWord8 3
352− put x1
353− CaseN x1 x2 -> do putWord8 4; put x1; put x2
354− ElimN x1 -> do putWord8 5; put x1
355− ImplementationCtorN x1 -> do putWord8 6; put x1
356− WithN x1 x2 -> do putWord8 7
357− put x1
358− put x2
359− MetaN x1 x2 -> do putWord8 8
360− put x1
361− put x2
362− get
363− = do i <- getWord8
364− case i of
365− 0 -> do x1 <- get
366− x2 <- get
367− x3 <- get
368− return (WhereN x1 x2 x3)
369− 1 -> do x1 <- get
370− x2 <- get
371− return (ImplementationN x1 x2)
372− 2 -> do x1 <- get
373− x2 <- get
374− return (ParentN x1 x2)
375− 3 -> do x1 <- get
376− return (MethodN x1)
377− 4 -> do x1 <- get
378− x2 <- get
379− return (CaseN x1 x2)
380− 5 -> do x1 <- get
381− return (ElimN x1)
382− 6 -> do x1 <- get
383− return (ImplementationCtorN x1)
384− 7 -> do x1 <- get
385− x2 <- get
386− return (WithN x1 x2)
387− 8 -> do x1 <- get
388− x2 <- get
389− return (MetaN x1 x2)
390− _ -> error "Corrupted binary data for SpecialName"
391−
392−
231+instance Binary FC
232+instance Binary FC'
233+instance Binary Name
234+instance Binary SpecialName
393235instance Binary Const where
394236 put x
395237 = case x of
@@ -453,56 +295,8 @@ instance Binary Const where
453295 29 -> return TheWorld
454296 _ -> error "Corrupted binary data for Const"
455297
456−
457−instance Binary Raw where
458− put x
459− = case x of
460− Var x1 -> do putWord8 0
461− put x1
462− RBind x1 x2 x3 -> do putWord8 1
463− put x1
464− put x2
465− put x3
466− RApp x1 x2 -> do putWord8 2
467− put x1
468− put x2
469− RType -> putWord8 3
470− RConstant x1 -> do putWord8 4
471− put x1
472− RUType x1 -> do putWord8 5
473− put x1
474− get
475− = do i <- getWord8
476− case i of
477− 0 -> do x1 <- get
478− return (Var x1)
479− 1 -> do x1 <- get
480− x2 <- get
481− x3 <- get
482− return (RBind x1 x2 x3)
483− 2 -> do x1 <- get
484− x2 <- get
485− return (RApp x1 x2)
486− 3 -> return RType
487− 4 -> do x1 <- get
488− return (RConstant x1)
489− 5 -> do x1 <- get
490− return (RUType x1)
491− _ -> error "Corrupted binary data for Raw"
492−
493−instance Binary RigCount where
494− put x = case x of
495− Rig0 -> putWord8 0
496− Rig1 -> putWord8 1
497− RigW -> putWord8 2
498− get = do i <- getWord8
499− case i of
500− 0 -> return Rig0
501− 1 -> return Rig1
502− 2 -> return RigW
503− _ -> error "Corrupted binary data for RigCount"
504−
505−
298+instance Binary Raw
299+instance Binary RigCount
506300instance Binary ImplicitInfo where
507301 put x
508302 = case x of
@@ -512,124 +306,11 @@ instance Binary ImplicitInfo where
512306 x2 <- get
513307 return (Impl x1 x2 False)
514308
515−instance (Binary b) => Binary (Binder b) where
516− put x
517− = case x of
518− Lam x1 x2 -> do putWord8 0
519− put x1
520− put x2
521− Pi x1 x2 x3 x4 -> do putWord8 1
522− put x1
523− put x2
524− put x3
525− put x4
526− Let x1 x2 -> do putWord8 2
527− put x1
528− put x2
529− NLet x1 x2 -> do putWord8 3
530− put x1
531− put x2
532− Hole x1 -> do putWord8 4
533− put x1
534− GHole x1 x2 x3 -> do putWord8 5
535− put x1
536− put x2
537− put x3
538− Guess x1 x2 -> do putWord8 6
539− put x1
540− put x2
541− PVar x1 x2 -> do putWord8 7
542− put x1
543− put x2
544− PVTy x1 -> do putWord8 8
545− put x1
546− get
547− = do i <- getWord8
548− case i of
549− 0 -> do x1 <- get
550− x2 <- get
551− return (Lam x1 x2)
552− 1 -> do x1 <- get
553− x2 <- get
554− x3 <- get
555− x4 <- get
556− return (Pi x1 x2 x3 x4)
557− 2 -> do x1 <- get
558− x2 <- get
559− return (Let x1 x2)
560− 3 -> do x1 <- get
561− x2 <- get
562− return (NLet x1 x2)
563− 4 -> do x1 <- get
564− return (Hole x1)
565− 5 -> do x1 <- get
566− x2 <- get
567− x3 <- get
568− return (GHole x1 x2 x3)
569− 6 -> do x1 <- get
570− x2 <- get
571− return (Guess x1 x2)
572− 7 -> do x1 <- get
573− x2 <- get
574− return (PVar x1 x2)
575− 8 -> do x1 <- get
576− return (PVTy x1)
577− _ -> error "Corrupted binary data for Binder"
578−
579−
580−instance Binary Universe where
581− put x = case x of
582− UniqueType -> putWord8 0
583− AllTypes -> putWord8 1
584− NullType -> putWord8 2
585− get = do i <- getWord8
586− case i of
587− 0 -> return UniqueType
588− 1 -> return AllTypes
589− 2 -> return NullType
590− _ -> error "Corrupted binary data for Universe"
591−
592−instance Binary NameType where
593− put x
594− = case x of
595− Bound -> putWord8 0
596− Ref -> putWord8 1
597− DCon x1 x2 x3 -> do putWord8 2
598− put (x1 * 65536 + x2)
599− put x3
600− TCon x1 x2 -> do putWord8 3
601− put (x1 * 65536 + x2)
602− get
603− = do i <- getWord8
604− case i of
605− 0 -> return Bound
606− 1 -> return Ref
607− 2 -> do x1x2 <- get
608− x3 <- get
609− return (DCon (x1x2 `div` 65536) (x1x2 `mod` 65536) x3)
610− 3 -> do x1x2 <- get
611− return (TCon (x1x2 `div` 65536) (x1x2 `mod` 65536))
612− _ -> error "Corrupted binary data for NameType"
613−
614−-- record concrete levels only, for now
615−instance Binary UExp where
616− put x = case x of
617− UVar ns t -> do putWord8 0
618− put ns
619− put t
620− UVal t -> do putWord8 1
621− put t
622−
623− get = do i <- getWord8
624− case i of
625− 0 -> do x1 <- get
626− x2 <- get
627− return (UVar x1 x2)
628− 1 -> do x1 <- get
629− return (UVal x1)
630− _ -> error "Corrupted binary data for UExp"
631−
632−instance {- (Binary n) => -} Binary (TT Name) where
309+instance (Binary b) => Binary (Binder b)
310+instance Binary Universe
311+instance Binary NameType
312+instance Binary UExp
313+instance Binary (TT Name) where
633314 put x
634315 = {-# SCC "putTT" #-}
635316 case x of