Skip to content

Commit

Permalink
Add with expressions to IBC files
Browse files Browse the repository at this point in the history
This prevents the following error:

idris: src/Idris/IBC.hs:(1546,13)-(1652,44): Non-exhaustive patterns in case
  • Loading branch information
david-christiansen committed Feb 5, 2014
1 parent a83671e commit 649b340
Showing 1 changed file with 8 additions and 1 deletion.
9 changes: 8 additions & 1 deletion src/Idris/IBC.hs
Original file line number Diff line number Diff line change
Expand Up @@ -26,7 +26,7 @@ import Util.Zlib (decompressEither)


ibcVersion :: Word8
ibcVersion = 58
ibcVersion = 59


data IBCFile = IBCFile { ver :: Word8,
Expand Down Expand Up @@ -1650,6 +1650,10 @@ instance Binary PTerm where
put x1
PNoImplicits x1 -> do putWord8 36
put x1
PDisamb x1 x2 -> do putWord8 37
put x1
put x2

get
= do i <- getWord8
case i of
Expand Down Expand Up @@ -1759,6 +1763,9 @@ instance Binary PTerm where
return (PUnifyLog x1)
36 -> do x1 <- get
return (PNoImplicits x1)
37 -> do x1 <- get
x2 <- get
return (PDisamb x1 x2)
_ -> error "Corrupted binary data for PTerm"

instance (Binary t) => Binary (PTactic' t) where
Expand Down

0 comments on commit 649b340

Please sign in to comment.