e8a41dc · Idris-dev · git.iko.soy

40import Codec.Archive.Zip

41

42ibcVersion :: Word16

43−ibcVersion = 129

43+ibcVersion = 130

44

45-- When IBC is being loaded - we'll load different things (and omit different

46-- structures/definitions) depending on which phase we're in

545 return $ Right (l', r')

546

547 updateCD (CaseDefs (ts, t) (cs, c) (is, i) (rs, r))

548− = do t' <- updateSC t

549− c' <- updateSC c

548+ = do c' <- updateSC c

550− i' <- updateSC i

551 r' <- updateSC r

549 r' <- updateSC r

552− return $ CaseDefs (ts, t') (cs, c') (is, i') (rs, r')

550+ return $ CaseDefs (cs, c') (cs, c') (cs, c') (rs, r')

553

551

554 updateSC (Case t n alts) = do alts' <- mapM updateAlt alts

552 updateSC (Case t n alts) = do alts' <- mapM updateAlt alts

555 return (Case t n alts')

553 return (Case t n alts')

896 put x2

894 put x2

897 -- all primitives just get added at the start, don't write

895 -- all primitives just get added at the start, don't write

898 Operator x1 x2 x3 -> do return ()

896 Operator x1 x2 x3 -> do return ()

897+ -- no need to add/load original patterns, because they're not

898+ -- used again after totality checking

899− CaseOp x1 x2 x2a x3 x3a x4 -> do putWord8 3

899+ CaseOp x1 x2 x3 _ _ x4 -> do putWord8 3

900− put x1

900+ put x1

901− put x2

901+ put x2

902− put x2a

903− put x3

902+ put x3

904− -- no x3a

905− put x4

903+ put x4

906 get

904 get

907 = do i <- getWord8

905 = do i <- getWord8

908 case i of

906 case i of

916 3 -> do x1 <- get

914 3 -> do x1 <- get

917 x2 <- get

915 x2 <- get

918 x3 <- get

916 x3 <- get

919− x4 <- get

917+-- x4 <- get

920 -- x3 <- get always []

918 -- x3 <- get always []

921 x5 <- get

919 x5 <- get

922− return (CaseOp x1 x2 x3 x4 [] x5)

920+ return (CaseOp x1 x2 x3 [] [] x5)

923 _ -> error "Corrupted binary data for Def"

921 _ -> error "Corrupted binary data for Def"

924

922

925instance Binary Accessibility where

923instance Binary Accessibility where