a88053b · Idris-dev · git.iko.soy

git.iko.soy/Idris-dev

on master help sign in

Add idris_postulates to IBC.

a88053bMatus Tejiscak13 years ago

src/Idris/AbsSyntaxTree.hs+1

compare with master

unifiedsplit

@@ -226,6 +226,7 @@ data IBCWrite = IBCFix FixDecl

226 | IBCLineApp FilePath Int PTerm

227 | IBCErrorHandler Name

228 | IBCFunctionErrorHandler Name Name Name

229+ | IBCPostulate Name

229 deriving Show

230 deriving Show

230

231

231-- | The initial state for the compiler

232-- | The initial state for the compiler

src/Idris/ElabDecls.hs+2

@@ -207,7 +207,9 @@ elabPostulate :: ElabInfo -> SyntaxInfo -> Docstring ->

207 FC -> FnOpts -> Name -> PTerm -> Idris ()

208elabPostulate info syn doc fc opts n ty = do

209 elabType info syn doc [] fc opts n ty

210+ logLvl (-10) $ "adding postulate " ++ show n

210 putIState . (\ist -> ist{ idris_postulates = S.insert n (idris_postulates ist) }) =<< getIState

211 putIState . (\ist -> ist{ idris_postulates = S.insert n (idris_postulates ist) }) =<< getIState

212+ addIBC (IBCPostulate n)

211

213

212 -- remove it from the deferred definitions list

214 -- remove it from the deferred definitions list

213 solveDeferred n

215 solveDeferred n

src/Idris/Erasure.hs+1

@@ -92,6 +92,7 @@ performUsageAnalysis = do

93 -- Check that no postulates are reachable.

94 reachablePostulates <- S.intersection reachableNames . idris_postulates <$> getIState

95+ logLvl (-10) . show . idris_postulates =<< getIState

95 when (not . S.null $ reachablePostulates)

96 when (not . S.null $ reachablePostulates)

96 $ ifail ("reachable postulates: " ++ (show $ S.toList reachablePostulates))

97 $ ifail ("reachable postulates: " ++ (show $ S.toList reachablePostulates))

src/Idris/IBC.hs+15−4

@@ -19,6 +19,7 @@ import Data.Vector.Binary

19import Data.List

20import Data.ByteString.Lazy as B hiding (length, elem, map)

21import qualified Data.Text as T

22+import qualified Data.Set as S

23import Control.Monad

24import Control.Monad

24import Control.Monad.State.Strict hiding (get, put)

25import Control.Monad.State.Strict hiding (get, put)

@@ -65,7 +66,8 @@ data IBCFile = IBCFile { ver :: Word8,

65 ibc_errorhandlers :: [Name],

66 ibc_errorhandlers :: [Name],

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

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

67 ibc_metavars :: [(Name, (Maybe Name, Int, Bool))],

68 ibc_metavars :: [(Name, (Maybe Name, Int, Bool))],

68− ibc_patdefs :: [(Name, ([([Name], Term, Term)], [PTerm]))]

69+ ibc_patdefs :: [(Name, ([([Name], Term, Term)], [PTerm]))],

70+ ibc_postulates :: [Name]

69 }

71 }

70 deriving Show

72 deriving Show

71{-!

73{-!

@@ -73,7 +75,7 @@ deriving instance Binary IBCFile

73!-}

75!-}

75initIBC :: IBCFile

77initIBC :: IBCFile

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

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

78loadIBC :: FilePath -> Idris ()

80loadIBC :: FilePath -> Idris ()

79loadIBC fp = do imps <- getImported

81loadIBC fp = do imps <- getImported

@@ -236,6 +238,7 @@ ibc i (IBCMetavar n) f =

236 case lookup n (idris_metavars i) of

238 case lookup n (idris_metavars i) of

237 Nothing -> return f

239 Nothing -> return f

238 Just t -> return f { ibc_metavars = (n, t) : ibc_metavars f }

240 Just t -> return f { ibc_metavars = (n, t) : ibc_metavars f }

241+ibc i (IBCPostulate n) f = return f { ibc_postulates = n : ibc_postulates f }

239

242

240process :: IBCFile -> FilePath -> Idris ()

243process :: IBCFile -> FilePath -> Idris ()

241process i fn

244process i fn

@@ -278,6 +281,7 @@ process i fn

278 pErrorHandlers (ibc_errorhandlers i)

281 pErrorHandlers (ibc_errorhandlers i)

279 pFunctionErrorHandlers (ibc_function_errorhandlers i)

282 pFunctionErrorHandlers (ibc_function_errorhandlers i)

280 pMetavars (ibc_metavars i)

283 pMetavars (ibc_metavars i)

284+ pPostulates (ibc_postulates i)

281

285

282timestampOlder :: FilePath -> FilePath -> IO ()

286timestampOlder :: FilePath -> FilePath -> IO ()

283timestampOlder src ibc = do srct <- getModificationTime src

287timestampOlder src ibc = do srct <- getModificationTime src

@@ -286,6 +290,11 @@ timestampOlder src ibc = do srct <- getModificationTime src

286 then fail "Needs reloading"

290 then fail "Needs reloading"

287 else return ()

291 else return ()

288

292

293+pPostulates :: [Name] -> Idris ()

294+pPostulates ns = do

295+ i <- getIState

296+ putIState i{ idris_postulates = idris_postulates i `S.union` S.fromList ns }

297+

289pImports :: [FilePath] -> Idris ()

298pImports :: [FilePath] -> Idris ()

290pImports fs

299pImports fs

291 = do mapM_ (\f -> do i <- getIState

300 = do mapM_ (\f -> do i <- getIState

@@ -1152,7 +1161,7 @@ instance Binary MetaInformation where

1152 return (DataMI x1)

1161 return (DataMI x1)

1153

1162

1154instance Binary IBCFile where

1163instance Binary IBCFile where

1155− 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)

1164+ 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 x36)

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

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

1157 do put x1

1166 do put x1

1158 put x2

1167 put x2

@@ -1189,6 +1198,7 @@ instance Binary IBCFile where

1189 put x33

1198 put x33

1190 put x34

1199 put x34

1191 put x35

1200 put x35

1201+ put x36

1192

1202

1193 get

1203 get

1194 = do x1 <- get

1204 = do x1 <- get

@@ -1227,7 +1237,8 @@ instance Binary IBCFile where

1227 x33 <- get

1237 x33 <- get

1228 x34 <- get

1238 x34 <- get

1229 x35 <- get

1239 x35 <- get

1240+ x36 <- get

1230− 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)

1241+ 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 x36)

1231 else return (initIBC { ver = x1 })

1242 else return (initIBC { ver = x1 })

1232

1243

1233instance Binary DataOpt where

1244instance Binary DataOpt where