77701e1 · Idris-dev · git.iko.soy

git.iko.soy/Idris-dev

on master help sign in

Save pattern definitions/missing cases

77701e1Edwin Brady13 years ago

src/Idris/IBC.hs+24−10

compare with master

unifiedsplit

@@ -28,8 +28,7 @@ import Codec.Compression.Zlib (compress)

28import Util.Zlib (decompressEither)

30ibcVersion :: Word8

31−ibcVersion = 64

31+ibcVersion = 65

32−

34data IBCFile = IBCFile { ver :: Word8,

33data IBCFile = IBCFile { ver :: Word8,

35 sourcefile :: FilePath,

34 sourcefile :: FilePath,

@@ -64,7 +63,8 @@ data IBCFile = IBCFile { ver :: Word8,

64 ibc_metainformation :: [(Name, MetaInformation)],

63 ibc_metainformation :: [(Name, MetaInformation)],

65 ibc_errorhandlers :: [Name],

64 ibc_errorhandlers :: [Name],

66 ibc_function_errorhandlers :: [(Name, Name, Name)], -- fn, arg, handler

65 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]))]

68 }

69 deriving Show

70{-!

@@ -72,7 +72,7 @@ deriving instance Binary IBCFile

72!-}

74initIBC :: IBCFile

75−initIBC = IBCFile ibcVersion "" [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] []

75+initIBC = IBCFile ibcVersion "" [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] []

77loadIBC :: FilePath -> Idris ()

78loadIBC 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 }

145ibc i (IBCCGFlag tgt n) f = return f { ibc_cgflags = (tgt, n) : ibc_cgflags f }

146ibc i (IBCDyLib n) f = return f {ibc_dynamic_libs = n : ibc_dynamic_libs f }

147ibc i (IBCHeader tgt n) f = return f { ibc_hdrs = (tgt, n) : ibc_hdrs f }

148+ibc i (IBCDef n) f

148−ibc i (IBCDef n) f = case lookupDef n (tt_ctxt i) of

149+ = do f' <- case lookupDef n (tt_ctxt i) of

149− [v] -> do (v', (f', _)) <- runStateT (updateDef v) (f, length (symbols f))

150+ [v] -> do (v', (f', _)) <- runStateT (updateDef v) (f, length (symbols f))

150− return f' { ibc_defs = (n,v) : ibc_defs f' }

151+ return f' { ibc_defs = (n,v) : ibc_defs f' }

151− _ -> ifail "IBC write failed"

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

152 where

156 where

153 updateDef :: Def -> StateT (IBCFile, Int) Idris Def

157 updateDef :: Def -> StateT (IBCFile, Int) Idris Def

154 updateDef (CaseOp c t args o s cd)

158 updateDef (CaseOp c t args o s cd)

@@ -256,6 +260,7 @@ process i fn

256 pDyLibs (ibc_dynamic_libs i)

260 pDyLibs (ibc_dynamic_libs i)

257 pHdrs (ibc_hdrs i)

261 pHdrs (ibc_hdrs i)

258 pDefs (symbols i) (ibc_defs i)

262 pDefs (symbols i) (ibc_defs i)

263+ pPatdefs (ibc_patdefs i)

259 pAccess (ibc_access i)

264 pAccess (ibc_access i)

260 pTotal (ibc_total i)

265 pTotal (ibc_total i)

261 pCG (ibc_cg i)

266 pCG (ibc_cg i)

@@ -381,6 +386,13 @@ pDyLibs ls = do res <- mapM (addDyLib . return) ls

381pHdrs :: [(Codegen, String)] -> Idris ()

386pHdrs :: [(Codegen, String)] -> Idris ()

382pHdrs hs = mapM_ (uncurry addHdr) hs

387pHdrs hs = mapM_ (uncurry addHdr) hs

383

388

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+

384pDefs :: [Name] -> [(Name, Def)] -> Idris ()

396pDefs :: [Name] -> [(Name, Def)] -> Idris ()

385pDefs syms ds

397pDefs syms ds

386 = mapM_ (\ (n, d) ->

398 = mapM_ (\ (n, d) ->

@@ -1137,7 +1149,7 @@ instance Binary MetaInformation where

1137 return (DataMI x1)

1149 return (DataMI x1)

1138

1150

1139instance Binary IBCFile where

1151instance 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)

1141 = {-# SCC "putIBCFile" #-}

1153 = {-# SCC "putIBCFile" #-}

1142 do put x1

1154 do put x1

1143 put x2

1155 put x2

@@ -1173,6 +1185,7 @@ instance Binary IBCFile where

1173 put x32

1185 put x32

1174 put x33

1186 put x33

1175 put x34

1187 put x34

1188+ put x35

1176

1189

1177 get

1190 get

1178 = do x1 <- get

1191 = do x1 <- get

@@ -1210,7 +1223,8 @@ instance Binary IBCFile where

1210 x32 <- get

1223 x32 <- get

1211 x33 <- get

1224 x33 <- get

1212 x34 <- get

1225 x34 <- get

1226+ x35 <- 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)

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)

1214 else return (initIBC { ver = x1 })

1228 else return (initIBC { ver = x1 })

1215

1229

1216instance Binary DataOpt where

1230instance Binary DataOpt where