@@ -28,8 +28,7 @@ import Codec.Compression.Zlib (compress)
2828import Util.Zlib (decompressEither)
2929
3030ibcVersion :: Word8
31−ibcVersion = 64
32−
31+ibcVersion = 65
3332
3433data IBCFile = IBCFile { ver :: Word8,
3534 sourcefile :: FilePath,
@@ -64,7 +63,8 @@ data IBCFile = IBCFile { ver :: Word8,
6463 ibc_metainformation :: [(Name, MetaInformation)],
6564 ibc_errorhandlers :: [Name],
6665 ibc_function_errorhandlers :: [(Name, Name, Name)], -- fn, arg, handler
67− ibc_metavars :: [(Name, (Maybe Name, Int, Bool))]
66+ ibc_metavars :: [(Name, (Maybe Name, Int, Bool))],
67+ ibc_patdefs :: [(Name, ([([Name], Term, Term)], [PTerm]))]
6868 }
6969 deriving Show
7070{-!
@@ -72,7 +72,7 @@ deriving instance Binary IBCFile
7272!-}
7373
7474initIBC :: IBCFile
75−initIBC = IBCFile ibcVersion "" [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] []
75+initIBC = IBCFile ibcVersion "" [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] []
7676
7777loadIBC :: FilePath -> Idris ()
7878loadIBC fp = do iLOG $ "Loading ibc " ++ fp
@@ -145,10 +145,14 @@ ibc i (IBCLib tgt n) f = return f { ibc_libs = (tgt, n) : ibc_libs f }
145145ibc i (IBCCGFlag tgt n) f = return f { ibc_cgflags = (tgt, n) : ibc_cgflags f }
146146ibc i (IBCDyLib n) f = return f {ibc_dynamic_libs = n : ibc_dynamic_libs f }
147147ibc i (IBCHeader tgt n) f = return f { ibc_hdrs = (tgt, n) : ibc_hdrs f }
148−ibc i (IBCDef n) f = case lookupDef n (tt_ctxt i) of
149− [v] -> do (v', (f', _)) <- runStateT (updateDef v) (f, length (symbols f))
150− return f' { ibc_defs = (n,v) : ibc_defs f' }
151− _ -> ifail "IBC write failed"
148+ibc i (IBCDef n) f
149+ = do f' <- case lookupDef n (tt_ctxt i) of
150+ [v] -> do (v', (f', _)) <- runStateT (updateDef v) (f, length (symbols f))
151+ return f' { ibc_defs = (n,v) : ibc_defs f' }
152+ _ -> ifail "IBC write failed"
153+ case lookupCtxt n (idris_patdefs i) of
154+ [v] -> return f' { ibc_patdefs = (n,v) : ibc_patdefs f' }
155+ _ -> return f' -- Not a pattern definition
152156 where
153157 updateDef :: Def -> StateT (IBCFile, Int) Idris Def
154158 updateDef (CaseOp c t args o s cd)
@@ -256,6 +260,7 @@ process i fn
256260 pDyLibs (ibc_dynamic_libs i)
257261 pHdrs (ibc_hdrs i)
258262 pDefs (symbols i) (ibc_defs i)
263+ pPatdefs (ibc_patdefs i)
259264 pAccess (ibc_access i)
260265 pTotal (ibc_total i)
261266 pCG (ibc_cg i)
@@ -381,6 +386,13 @@ pDyLibs ls = do res <- mapM (addDyLib . return) ls
381386pHdrs :: [(Codegen, String)] -> Idris ()
382387pHdrs hs = mapM_ (uncurry addHdr) hs
383388
389+pPatdefs :: [(Name, ([([Name], Term, Term)], [PTerm]))] -> Idris ()
390+pPatdefs ds
391+ = mapM_ (\ (n, d) ->
392+ do i <- getIState
393+ putIState (i { idris_patdefs = addDef n d (idris_patdefs i) }))
394+ ds
395+
384396pDefs :: [Name] -> [(Name, Def)] -> Idris ()
385397pDefs syms ds
386398 = mapM_ (\ (n, d) ->
@@ -1137,7 +1149,7 @@ instance Binary MetaInformation where
11371149 return (DataMI x1)
11381150
11391151instance Binary IBCFile where
1140− 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)
1152+ 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)
11411153 = {-# SCC "putIBCFile" #-}
11421154 do put x1
11431155 put x2
@@ -1173,6 +1185,7 @@ instance Binary IBCFile where
11731185 put x32
11741186 put x33
11751187 put x34
1188+ put x35
11761189
11771190 get
11781191 = do x1 <- get
@@ -1210,7 +1223,8 @@ instance Binary IBCFile where
12101223 x32 <- get
12111224 x33 <- get
12121225 x34 <- get
1213− return (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)
1226+ x35 <- get
1227+ return (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)
12141228 else return (initIBC { ver = x1 })
12151229
12161230instance Binary DataOpt where