on master help sign in
Don't save original TT pattern clauses

They're only used for totality checking and not even viewable, so don't save/reload from IBCs

commite8a41dc081a0d23a4b592cb1d06c27cd45049768 authorEdwin Brady <ecb10@st-andrews.ac.uk> dateWed 27 Jan 2016, 22:35 (11 years ago) parentd3dc418
1 file changed+12−14
src/Idris/IBC.hs+12−14
src/Idris/IBC.hs+12−14
@@ -40,7 +40,7 @@ import System.Directory
4040import Codec.Archive.Zip
4141
4242ibcVersion :: Word16
43−ibcVersion = 129
43+ibcVersion = 130
4444
4545-- When IBC is being loaded - we'll load different things (and omit different
4646-- structures/definitions) depending on which phase we're in
@@ -545,11 +545,9 @@ pDefs reexp ds
545545 return $ Right (l', r')
546546
547547 updateCD (CaseDefs (ts, t) (cs, c) (is, i) (rs, r))
548− = do t' <- updateSC t
549− c' <- updateSC c
550− i' <- updateSC i
548+ = do c' <- updateSC c
551549 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')
553551
554552 updateSC (Case t n alts) = do alts' <- mapM updateAlt alts
555553 return (Case t n alts')
@@ -896,13 +894,13 @@ instance Binary Def where
896894 put x2
897895 -- all primitives just get added at the start, don't write
898896 Operator x1 x2 x3 -> do return ()
899− CaseOp x1 x2 x2a x3 x3a x4 -> do putWord8 3
900− put x1
901− put x2
902− put x2a
903− put x3
904− -- no x3a
905− put x4
897+ -- no need to add/load original patterns, because they're not
898+ -- used again after totality checking
899+ CaseOp x1 x2 x3 _ _ x4 -> do putWord8 3
900+ put x1
901+ put x2
902+ put x3
903+ put x4
906904 get
907905 = do i <- getWord8
908906 case i of
@@ -916,10 +914,10 @@ instance Binary Def where
916914 3 -> do x1 <- get
917915 x2 <- get
918916 x3 <- get
919− x4 <- get
917+-- x4 <- get
920918 -- x3 <- get always []
921919 x5 <- get
922− return (CaseOp x1 x2 x3 x4 [] x5)
920+ return (CaseOp x1 x2 x3 [] [] x5)
923921 _ -> error "Corrupted binary data for Def"
924922
925923instance Binary Accessibility where