9249aae · Idris-dev · git.iko.soy

git.iko.soy/Idris-dev

on master help sign in

IBC generation pattern match completeness

9249aaeDavid Raymond Christiansen12 years ago

src/Idris/IBC.hs+143

compare with master

unifiedsplit

@@ -1,4 +1,5 @@

1{-# LANGUAGE TypeSynonymInstances #-}

2+{-# OPTIONS_GHC -fwarn-incomplete-patterns #-}

3module Idris.IBC where

4module Idris.IBC where

@@ -610,6 +611,7 @@ instance Binary a => Binary (D.Block a) where

610 4 -> liftM3 D.CodeBlock get get get

611 4 -> liftM3 D.CodeBlock get get get

611 5 -> liftM D.HtmlBlock get

612 5 -> liftM D.HtmlBlock get

612 6 -> return D.HRule

613 6 -> return D.HRule

614+ _ -> error "Corrupted binary data for Block"

613

615

614instance Binary a => Binary (D.Inline a) where

616instance Binary a => Binary (D.Inline a) where

615 put (D.Str txt) = do putWord8 0 ; put txt

617 put (D.Str txt) = do putWord8 0 ; put txt

@@ -636,6 +638,7 @@ instance Binary a => Binary (D.Inline a) where

636 8 -> liftM3 D.Image get get get

638 8 -> liftM3 D.Image get get get

637 9 -> liftM D.Entity get

639 9 -> liftM D.Entity get

638 10 -> liftM D.RawHtml get

640 10 -> liftM D.RawHtml get

641+ _ -> error "Corrupted binary data for Inline"

639

642

640instance Binary CT.ListType where

643instance Binary CT.ListType where

641 put (CT.Bullet c) = putWord8 0 >> put c

644 put (CT.Bullet c) = putWord8 0 >> put c

@@ -644,6 +647,7 @@ instance Binary CT.ListType where

644 case i of

647 case i of

645 0 -> liftM CT.Bullet get

648 0 -> liftM CT.Bullet get

646 1 -> liftM2 CT.Numbered get get

649 1 -> liftM2 CT.Numbered get get

650+ _ -> error "Corrupted binary data for ListType"

647

651

648instance Binary CT.CodeAttr where

652instance Binary CT.CodeAttr where

649 put (CT.CodeAttr a b) = put a >> put b

653 put (CT.CodeAttr a b) = put a >> put b

@@ -656,6 +660,7 @@ instance Binary CT.NumWrapper where

656 case i of

660 case i of

657 0 -> return CT.PeriodFollowing

661 0 -> return CT.PeriodFollowing

658 1 -> return CT.ParenFollowing

662 1 -> return CT.ParenFollowing

663+ _ -> error "Corrupted binary data for NumWrapper"

659

664

660----- Generated by 'derive'

665----- Generated by 'derive'

661

666

@@ -868,6 +873,9 @@ instance Binary PReason where

868 put x1

873 put x1

869 NotProductive -> putWord8 5

874 NotProductive -> putWord8 5

870 BelieveMe -> putWord8 6

875 BelieveMe -> putWord8 6

876+ UseUndef x1 -> do putWord8 7

877+ put x1

878+ ExternalIO -> putWord8 8

871 get

879 get

872 = do i <- getWord8

880 = do i <- getWord8

873 case i of

881 case i of

@@ -880,6 +888,9 @@ instance Binary PReason where

880 return (Mutual x1)

888 return (Mutual x1)

881 5 -> return NotProductive

889 5 -> return NotProductive

882 6 -> return BelieveMe

890 6 -> return BelieveMe

891+ 7 -> do x1 <- get

892+ return (UseUndef x1)

893+ 8 -> return ExternalIO

883 _ -> error "Corrupted binary data for PReason"

894 _ -> error "Corrupted binary data for PReason"

884

895

885instance Binary Totality where

896instance Binary Totality where

@@ -913,6 +924,7 @@ instance Binary MetaInformation where

913 0 -> return EmptyMI

924 0 -> return EmptyMI

914 1 -> do x1 <- get

925 1 -> do x1 <- get

915 return (DataMI x1)

926 return (DataMI x1)

927+ _ -> error "Corrupted binary data for MetaInformation"

916

928

917instance Binary IBCFile where

929instance Binary IBCFile where

918 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)

930 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

1019 1 -> return DefaultEliminator

1031 1 -> return DefaultEliminator

1020 2 -> return DataErrRev

1032 2 -> return DataErrRev

1021 3 -> return DefaultCaseFun

1033 3 -> return DefaultCaseFun

1034+ _ -> error "Corrupted binary data for DataOpt"

1022

1035

1023instance Binary FnOpt where

1036instance Binary FnOpt where

1024 put x

1037 put x

@@ -1038,6 +1051,8 @@ instance Binary FnOpt where

1038 CoveringFn -> putWord8 11

1051 CoveringFn -> putWord8 11

1039 NoImplicit -> putWord8 12

1052 NoImplicit -> putWord8 12

1040 Constructor -> putWord8 13

1053 Constructor -> putWord8 13

1054+ CExport x1 -> do putWord8 14

1055+ put x1

1041 get

1056 get

1042 = do i <- getWord8

1057 = do i <- getWord8

1043 case i of

1058 case i of

@@ -1056,6 +1071,8 @@ instance Binary FnOpt where

1056 11 -> return CoveringFn

1071 11 -> return CoveringFn

1057 12 -> return NoImplicit

1072 12 -> return NoImplicit

1058 13 -> return Constructor

1073 13 -> return Constructor

1074+ 14 -> do x1 <- get

1075+ return $ CExport x1

1059 _ -> error "Corrupted binary data for FnOpt"

1076 _ -> error "Corrupted binary data for FnOpt"

1060

1077

1061instance Binary Fixity where

1078instance Binary Fixity where

@@ -1249,6 +1266,20 @@ instance (Binary t) => Binary (PDecl' t) where

1249 put x4

1266 put x4

1250 put x5

1267 put x5

1251 put x6

1268 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

1252 get

1283 get

1253 = do i <- getWord8

1284 = do i <- getWord8

1254 case i of

1285 case i of

@@ -1328,8 +1359,37 @@ instance (Binary t) => Binary (PDecl' t) where

1328 x5 <- get

1359 x5 <- get

1329 x6 <- get

1360 x6 <- get

1330 return (PPostulate x1 x2 x3 x4 x5 x6)

1361 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)

1331 _ -> error "Corrupted binary data for PDecl'"

1376 _ -> error "Corrupted binary data for PDecl'"

1332

1377

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+

1333instance Binary Using where

1393instance Binary Using where

1334 put (UImplicit x1 x2) = do putWord8 0; put x1; put x2

1394 put (UImplicit x1 x2) = do putWord8 0; put x1; put x2

1335 put (UConstraint x1 x2) = do putWord8 1; put x1; put x2

1395 put (UConstraint x1 x2) = do putWord8 1; put x1; put x2

@@ -1338,6 +1398,7 @@ instance Binary Using where

1338 case i of

1398 case i of

1339 0 -> do x1 <- get; x2 <- get; return (UImplicit x1 x2)

1399 0 -> do x1 <- get; x2 <- get; return (UImplicit x1 x2)

1340 1 -> do x1 <- get; x2 <- get; return (UConstraint x1 x2)

1400 1 -> do x1 <- get; x2 <- get; return (UConstraint x1 x2)

1401+ _ -> error "Corrupted binary data for Using"

1341

1402

1342instance Binary SyntaxInfo where

1403instance Binary SyntaxInfo where

1343 put (Syn x1 x2 x3 x4 _ x5 x6 _ _ x7 _)

1404 put (Syn x1 x2 x3 x4 _ x5 x6 _ _ x7 _)

@@ -1452,6 +1513,7 @@ instance Binary PunInfo where

1452 0 -> return TypeOrTerm

1513 0 -> return TypeOrTerm

1453 1 -> return IsType

1514 1 -> return IsType

1454 2 -> return IsTerm

1515 2 -> return IsTerm

1516+ _ -> error "Corrupted binary data for PunInfo"

1455

1517

1456instance Binary PTerm where

1518instance Binary PTerm where

1457 put x

1519 put x

@@ -1574,6 +1636,18 @@ instance Binary PTerm where

1574 PRunTactics x1 x2 -> do putWord8 39

1636 PRunTactics x1 x2 -> do putWord8 39

1575 put x1

1637 put x1

1576 put x2

1638 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+

1577

1651

1578 get

1652 get

1579 = do i <- getWord8

1653 = do i <- getWord8

@@ -1695,6 +1769,17 @@ instance Binary PTerm where

1695 39 -> do x1 <- get

1769 39 -> do x1 <- get

1696 x2 <- get

1770 x2 <- get

1697 return (PRunTactics x1 x2)

1771 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)

1698 _ -> error "Corrupted binary data for PTerm"

1783 _ -> error "Corrupted binary data for PTerm"

1699

1784

1700instance (Binary t) => Binary (PTactic' t) where

1785instance (Binary t) => Binary (PTactic' t) where

@@ -1748,6 +1833,35 @@ instance (Binary t) => Binary (PTactic' t) where

1748 CaseTac x1 -> do putWord8 23

1833 CaseTac x1 -> do putWord8 23

1749 put x1

1834 put x1

1750 SourceFC -> putWord8 24

1835 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

1751 get

1865 get

1752 = do i <- getWord8

1866 = do i <- getWord8

1753 case i of

1867 case i of

@@ -1799,6 +1913,35 @@ instance (Binary t) => Binary (PTactic' t) where

1799 23 -> do x1 <- get

1913 23 -> do x1 <- get

1800 return (CaseTac x1)

1914 return (CaseTac x1)

1801 24 -> return SourceFC

1915 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

1802 _ -> error "Corrupted binary data for PTactic'"

1945 _ -> error "Corrupted binary data for PTactic'"

1803

1946

1804

1947