@@ -1,4 +1,5 @@
11{-# LANGUAGE TypeSynonymInstances #-}
2+{-# OPTIONS_GHC -fwarn-incomplete-patterns #-}
23
34module Idris.IBC where
45
@@ -610,6 +611,7 @@ instance Binary a => Binary (D.Block a) where
610611 4 -> liftM3 D.CodeBlock get get get
611612 5 -> liftM D.HtmlBlock get
612613 6 -> return D.HRule
614+ _ -> error "Corrupted binary data for Block"
613615
614616instance Binary a => Binary (D.Inline a) where
615617 put (D.Str txt) = do putWord8 0 ; put txt
@@ -636,6 +638,7 @@ instance Binary a => Binary (D.Inline a) where
636638 8 -> liftM3 D.Image get get get
637639 9 -> liftM D.Entity get
638640 10 -> liftM D.RawHtml get
641+ _ -> error "Corrupted binary data for Inline"
639642
640643instance Binary CT.ListType where
641644 put (CT.Bullet c) = putWord8 0 >> put c
@@ -644,6 +647,7 @@ instance Binary CT.ListType where
644647 case i of
645648 0 -> liftM CT.Bullet get
646649 1 -> liftM2 CT.Numbered get get
650+ _ -> error "Corrupted binary data for ListType"
647651
648652instance Binary CT.CodeAttr where
649653 put (CT.CodeAttr a b) = put a >> put b
@@ -656,6 +660,7 @@ instance Binary CT.NumWrapper where
656660 case i of
657661 0 -> return CT.PeriodFollowing
658662 1 -> return CT.ParenFollowing
663+ _ -> error "Corrupted binary data for NumWrapper"
659664
660665----- Generated by 'derive'
661666
@@ -868,6 +873,9 @@ instance Binary PReason where
868873 put x1
869874 NotProductive -> putWord8 5
870875 BelieveMe -> putWord8 6
876+ UseUndef x1 -> do putWord8 7
877+ put x1
878+ ExternalIO -> putWord8 8
871879 get
872880 = do i <- getWord8
873881 case i of
@@ -880,6 +888,9 @@ instance Binary PReason where
880888 return (Mutual x1)
881889 5 -> return NotProductive
882890 6 -> return BelieveMe
891+ 7 -> do x1 <- get
892+ return (UseUndef x1)
893+ 8 -> return ExternalIO
883894 _ -> error "Corrupted binary data for PReason"
884895
885896instance Binary Totality where
@@ -913,6 +924,7 @@ instance Binary MetaInformation where
913924 0 -> return EmptyMI
914925 1 -> do x1 <- get
915926 return (DataMI x1)
927+ _ -> error "Corrupted binary data for MetaInformation"
916928
917929instance Binary IBCFile where
918930 put x@(IBCFile x1 x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 x15 x16 x17 x18 x19 x20 x21 x22 x23 x24 x25 x26 x27 x28 x29 x30 x31 x32 x33 x34 x35 x36 x37 x38 x39 x40 x41 x42)
@@ -1019,6 +1031,7 @@ instance Binary DataOpt where
10191031 1 -> return DefaultEliminator
10201032 2 -> return DataErrRev
10211033 3 -> return DefaultCaseFun
1034+ _ -> error "Corrupted binary data for DataOpt"
10221035
10231036instance Binary FnOpt where
10241037 put x
@@ -1038,6 +1051,8 @@ instance Binary FnOpt where
10381051 CoveringFn -> putWord8 11
10391052 NoImplicit -> putWord8 12
10401053 Constructor -> putWord8 13
1054+ CExport x1 -> do putWord8 14
1055+ put x1
10411056 get
10421057 = do i <- getWord8
10431058 case i of
@@ -1056,6 +1071,8 @@ instance Binary FnOpt where
10561071 11 -> return CoveringFn
10571072 12 -> return NoImplicit
10581073 13 -> return Constructor
1074+ 14 -> do x1 <- get
1075+ return $ CExport x1
10591076 _ -> error "Corrupted binary data for FnOpt"
10601077
10611078instance Binary Fixity where
@@ -1249,6 +1266,20 @@ instance (Binary t) => Binary (PDecl' t) where
12491266 put x4
12501267 put x5
12511268 put x6
1269+ PSyntax x1 x2 -> do putWord8 13
1270+ put x1
1271+ put x2
1272+ PDirective x1 -> error "Cannot serialize PDirective"
1273+ PProvider x1 x2 x3 x4 -> do putWord8 15
1274+ put x1
1275+ put x2
1276+ put x3
1277+ put x4
1278+ PTransform x1 x2 x3 x4 -> do putWord8 16
1279+ put x1
1280+ put x2
1281+ put x3
1282+ put x4
12521283 get
12531284 = do i <- getWord8
12541285 case i of
@@ -1328,8 +1359,37 @@ instance (Binary t) => Binary (PDecl' t) where
13281359 x5 <- get
13291360 x6 <- get
13301361 return (PPostulate x1 x2 x3 x4 x5 x6)
1362+ 13 -> do x1 <- get
1363+ x2 <- get
1364+ return (PSyntax x1 x2)
1365+ 14 -> do error "Cannot deserialize PDirective"
1366+ 15 -> do x1 <- get
1367+ x2 <- get
1368+ x3 <- get
1369+ x4 <- get
1370+ return (PProvider x1 x2 x3 x4)
1371+ 16 -> do x1 <- get
1372+ x2 <- get
1373+ x3 <- get
1374+ x4 <- get
1375+ return (PTransform x1 x2 x3 x4)
13311376 _ -> error "Corrupted binary data for PDecl'"
13321377
1378+instance Binary t => Binary (ProvideWhat' t) where
1379+ put (ProvTerm x1 x2) = do putWord8 0
1380+ put x1
1381+ put x2
1382+ put (ProvPostulate x1) = do putWord8 1
1383+ put x1
1384+ get = do y <- getWord8
1385+ case y of
1386+ 0 -> do x1 <- get
1387+ x2 <- get
1388+ return (ProvTerm x1 x2)
1389+ 1 -> do x1 <- get
1390+ return (ProvPostulate x1)
1391+ _ -> error "Corrupted binary data for ProvideWhat"
1392+
13331393instance Binary Using where
13341394 put (UImplicit x1 x2) = do putWord8 0; put x1; put x2
13351395 put (UConstraint x1 x2) = do putWord8 1; put x1; put x2
@@ -1338,6 +1398,7 @@ instance Binary Using where
13381398 case i of
13391399 0 -> do x1 <- get; x2 <- get; return (UImplicit x1 x2)
13401400 1 -> do x1 <- get; x2 <- get; return (UConstraint x1 x2)
1401+ _ -> error "Corrupted binary data for Using"
13411402
13421403instance Binary SyntaxInfo where
13431404 put (Syn x1 x2 x3 x4 _ x5 x6 _ _ x7 _)
@@ -1452,6 +1513,7 @@ instance Binary PunInfo where
14521513 0 -> return TypeOrTerm
14531514 1 -> return IsType
14541515 2 -> return IsTerm
1516+ _ -> error "Corrupted binary data for PunInfo"
14551517
14561518instance Binary PTerm where
14571519 put x
@@ -1574,6 +1636,18 @@ instance Binary PTerm where
15741636 PRunTactics x1 x2 -> do putWord8 39
15751637 put x1
15761638 put x2
1639+ PAs x1 x2 x3 -> do putWord8 40
1640+ put x1
1641+ put x2
1642+ put x3
1643+ PElabError x1 -> do putWord8 41
1644+ put x1
1645+ PQuasiquote x1 x2 -> do putWord8 42
1646+ put x1
1647+ put x2
1648+ PUnquote x1 -> do putWord8 43
1649+ put x1
1650+
15771651
15781652 get
15791653 = do i <- getWord8
@@ -1695,6 +1769,17 @@ instance Binary PTerm where
16951769 39 -> do x1 <- get
16961770 x2 <- get
16971771 return (PRunTactics x1 x2)
1772+ 40 -> do x1 <- get
1773+ x2 <- get
1774+ x3 <- get
1775+ return (PAs x1 x2 x3)
1776+ 41 -> do x1 <- get
1777+ return (PElabError x1)
1778+ 42 -> do x1 <- get
1779+ x2 <- get
1780+ return (PQuasiquote x1 x2)
1781+ 43 -> do x1 <- get
1782+ return (PUnquote x1)
16981783 _ -> error "Corrupted binary data for PTerm"
16991784
17001785instance (Binary t) => Binary (PTactic' t) where
@@ -1748,6 +1833,35 @@ instance (Binary t) => Binary (PTactic' t) where
17481833 CaseTac x1 -> do putWord8 23
17491834 put x1
17501835 SourceFC -> putWord8 24
1836+ Intros -> putWord8 25
1837+ Equiv x1 -> do putWord8 26
1838+ put x1
1839+ Claim x1 x2 -> do putWord8 27
1840+ put x1
1841+ put x2
1842+ Unfocus -> putWord8 28
1843+ MatchRefine x1 -> do putWord8 29
1844+ put x1
1845+ LetTacTy x1 x2 x3 -> do putWord8 30
1846+ put x1
1847+ put x2
1848+ put x3
1849+ TCInstance -> putWord8 31
1850+ GoalType x1 x2 -> do putWord8 32
1851+ put x1
1852+ put x2
1853+ TCheck x1 -> do putWord8 33
1854+ put x1
1855+ TEval x1 -> do putWord8 34
1856+ put x1
1857+ TDocStr x1 -> do putWord8 35
1858+ put x1
1859+ TSearch x1 -> do putWord8 36
1860+ put x1
1861+ Skip -> putWord8 37
1862+ TFail x1 -> do putWord8 38
1863+ put x1
1864+ Abandon -> putWord8 39
17511865 get
17521866 = do i <- getWord8
17531867 case i of
@@ -1799,6 +1913,35 @@ instance (Binary t) => Binary (PTactic' t) where
17991913 23 -> do x1 <- get
18001914 return (CaseTac x1)
18011915 24 -> return SourceFC
1916+ 25 -> return Intros
1917+ 26 -> do x1 <- get
1918+ return (Equiv x1)
1919+ 27 -> do x1 <- get
1920+ x2 <- get
1921+ return (Claim x1 x2)
1922+ 28 -> return Unfocus
1923+ 29 -> do x1 <- get
1924+ return (MatchRefine x1)
1925+ 30 -> do x1 <- get
1926+ x2 <- get
1927+ x3 <- get
1928+ return (LetTacTy x1 x2 x3)
1929+ 31 -> return TCInstance
1930+ 32 -> do x1 <- get
1931+ x2 <- get
1932+ return (GoalType x1 x2)
1933+ 33 -> do x1 <- get
1934+ return (TCheck x1)
1935+ 34 -> do x1 <- get
1936+ return (TEval x1)
1937+ 35 -> do x1 <- get
1938+ return (TDocStr x1)
1939+ 36 -> do x1 <- get
1940+ return (TSearch x1)
1941+ 37 -> return Skip
1942+ 38 -> do x1 <- get
1943+ return (TFail x1)
1944+ 39 -> return Abandon
18021945 _ -> error "Corrupted binary data for PTactic'"
18031946
18041947