644f093 · Idris-dev · git.iko.soy

git.iko.soy/Idris-dev

on master help sign in

Require postulate unreachability instead of collapsibility.

644f093Matus Tejiscak13 years ago

src/Idris/AbsSyntaxTree.hs+3−2

compare with master

unifiedsplit

@@ -165,7 +165,8 @@ data IState = IState {

165 idris_nameIdx :: (Int, Ctxt (Int, Name)),

166 idris_function_errorhandlers :: Ctxt (M.Map Name (S.Set Name)), -- ^ Specific error handlers

167 module_aliases :: M.Map [T.Text] [T.Text],

168− idris_consolewidth :: ConsoleWidth -- ^ How many chars wide is the console?

168+ idris_consolewidth :: ConsoleWidth, -- ^ How many chars wide is the console?

169+ idris_postulates :: S.Set Name

169 }

170 }

170

171

171data SizeChange = Smaller | Same | Bigger | Unknown

172data SizeChange = Smaller | Same | Bigger | Unknown

@@ -236,7 +237,7 @@ idrisInit = IState initContext [] [] emptyContext emptyContext emptyContext

236 [] [] defaultOpts 6 [] [] [] [] [] [] [] [] [] [] [] [] []

237 [] [] defaultOpts 6 [] [] [] [] [] [] [] [] [] [] [] [] []

237 [] [] Nothing [] Nothing [] [] Nothing [] Hidden False [] Nothing [] [] RawOutput

238 [] [] Nothing [] Nothing [] [] Nothing [] Hidden False [] Nothing [] [] RawOutput

238 True defaultTheme stdout [] (0, emptyContext) emptyContext M.empty

239 True defaultTheme stdout [] (0, emptyContext) emptyContext M.empty

239− AutomaticWidth

240+ AutomaticWidth S.empty

240

241

241-- | The monad for the main REPL - reading and processing files and updating

242-- | The monad for the main REPL - reading and processing files and updating

242-- global state (hence the IO inner monad).

243-- global state (hence the IO inner monad).

src/Idris/ElabDecls.hs+13−4

@@ -37,6 +37,7 @@ import Data.Maybe

37import Debug.Trace

39import qualified Data.Map as Map

40+import qualified Data.Set as S

40import qualified Data.Text as T

41import qualified Data.Text as T

41import Data.Char(isLetter, toLower)

42import Data.Char(isLetter, toLower)

42import Data.List.Split (splitOn)

43import Data.List.Split (splitOn)

@@ -204,8 +205,15 @@ inaccessibleArgs _ _ = []

204

205

205elabPostulate :: ElabInfo -> SyntaxInfo -> Docstring ->

206elabPostulate :: ElabInfo -> SyntaxInfo -> Docstring ->

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

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

207−elabPostulate info syn doc fc opts n ty

208+elabPostulate info syn doc fc opts n ty = do

208− = do elabType info syn doc [] fc opts n ty

209+ elabType info syn doc [] fc opts n ty

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

211+

212+ -- remove it from the deferred definitions list

213+ solveDeferred n

214+

215+{- NB. this check has been superseded by usage analysis

216+ -

209 -- make sure it's collapsible, so it is never needed at run time

217 -- make sure it's collapsible, so it is never needed at run time

210 -- start by getting the elaborated type

218 -- start by getting the elaborated type

211 ctxt <- getContext

219 ctxt <- getContext

@@ -214,6 +222,7 @@ elabPostulate info syn doc fc opts n ty

214 [ty] -> return ty

222 [ty] -> return ty

215 ist <- getIState

223 ist <- getIState

216 let (ap, _) = unApply (getRetTy (normalise ctxt [] fty))

224 let (ap, _) = unApply (getRetTy (normalise ctxt [] fty))

225+

217 logLvl 5 $ "Checking collapsibility of " ++ show (ap, fty)

226 logLvl 5 $ "Checking collapsibility of " ++ show (ap, fty)

218 let postOK = case ap of

227 let postOK = case ap of

219 P _ tn _ -> case lookupCtxt tn

228 P _ tn _ -> case lookupCtxt tn

@@ -223,8 +232,8 @@ elabPostulate info syn doc fc opts n ty

223 _ -> False

232 _ -> False

224 when (not postOK)

233 when (not postOK)

225 $ tclift $ tfail (At fc (NonCollapsiblePostulate n))

234 $ tclift $ tfail (At fc (NonCollapsiblePostulate n))

226− -- remove it from the deferred definitions list

235+-}

227− solveDeferred n

236+

228

237

229elabData :: ElabInfo -> SyntaxInfo -> Docstring -> [(Name, Docstring)] -> FC -> DataOpts -> PData -> Idris ()

238elabData :: ElabInfo -> SyntaxInfo -> Docstring -> [(Name, Docstring)] -> FC -> DataOpts -> PData -> Idris ()

230elabData info syn doc argDocs fc opts (PLaterdecl n t_in)

239elabData info syn doc argDocs fc opts (PLaterdecl n t_in)

src/Idris/Erasure.hs+5

@@ -90,6 +90,11 @@ performUsageAnalysis = do

90 when checkEnabled $

91 mapM_ (checkAccessibility opt) usage

93+ -- Check that no postulates are reachable.

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

95+ when (not . S.null $ reachablePostulates)

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

97+

93 -- Store the usage info in the internal state.

98 -- Store the usage info in the internal state.

94 mapM_ (storeUsage cg) usage

99 mapM_ (storeUsage cg) usage

100