a88053b · Idris-dev · git.iko.soy

git.iko.soy/Idris-dev

Add idris_postulates to IBC.

commita88053b835d9fc70b514ff28139159faffcac527 authorMatus Tejiscak <ziman@functor.sk> dateThu 27 Mar 2014, 17:08 (13 years ago) parentba81129

4 files changed+19−4

compare with master

unifiedsplit

src/Idris/AbsSyntaxTree.hs+1 src/Idris/ElabDecls.hs+2 src/Idris/Erasure.hs+1 src/Idris/IBC.hs+15−4

src/Idris/AbsSyntaxTree.hs+1

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

226226 | IBCLineApp FilePath Int PTerm

227227 | IBCErrorHandler Name

228228 | IBCFunctionErrorHandler Name Name Name

229+ | IBCPostulate Name

229230 deriving Show

230231

231232-- | The initial state for the compiler

src/Idris/ElabDecls.hs+2

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

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

208208elabPostulate info syn doc fc opts n ty = do

209209 elabType info syn doc [] fc opts n ty

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

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

212+ addIBC (IBCPostulate n)

211213

212214 -- remove it from the deferred definitions list

213215 solveDeferred n

src/Idris/Erasure.hs+1

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

9292

9393 -- Check that no postulates are reachable.

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

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

9596 when (not . S.null $ reachablePostulates)

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

9798

src/Idris/IBC.hs+15−4

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

1919import Data.List

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

2121import qualified Data.Text as T

22+import qualified Data.Set as S

2223

2324import Control.Monad

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

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

6566 ibc_errorhandlers :: [Name],

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

6768 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]

6971 }

7072 deriving Show

7173{-!

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

7375!-}

7476

7577initIBC :: IBCFile

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

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

7779

7880loadIBC :: FilePath -> Idris ()

7981loadIBC fp = do imps <- getImported

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

236238 case lookup n (idris_metavars i) of

237239 Nothing -> return f

238240 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 }

239242

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

241244process i fn

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

278281 pErrorHandlers (ibc_errorhandlers i)

279282 pFunctionErrorHandlers (ibc_function_errorhandlers i)

280283 pMetavars (ibc_metavars i)

284+ pPostulates (ibc_postulates i)

281285

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

283287timestampOlder src ibc = do srct <- getModificationTime src

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

286290 then fail "Needs reloading"

287291 else return ()

288292

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+

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

290299pImports fs

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

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

11521161 return (DataMI x1)

11531162

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

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

11571166 do put x1

11581167 put x2

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

11891198 put x33

11901199 put x34

11911200 put x35

1201+ put x36

11921202

11931203 get

11941204 = do x1 <- get

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

12271237 x33 <- get

12281238 x34 <- get

12291239 x35 <- 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)

1240+ x36 <- get

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)

12311242 else return (initIBC { ver = x1 })

12321243

12331244instance Binary DataOpt where