git.iko.soy/Idris-dev
on master help sign in
Require postulate unreachability instead of collapsibility.
commit644f093c751374eeb06a1f50d3482ce31da7005f authorMatus Tejiscak <ziman@functor.sk> dateMon 10 Mar 2014, 18:46 (13 years ago) parent2604c1d
3 files changed+21−6
compare with master
unifiedsplit
src/Idris/AbsSyntaxTree.hs+3−2 src/Idris/ElabDecls.hs+13−4 src/Idris/Erasure.hs+5
src/Idris/AbsSyntaxTree.hs+3−2
@@ -165,7 +165,8 @@ data IState = IState {
165165 idris_nameIdx :: (Int, Ctxt (Int, Name)),
166166 idris_function_errorhandlers :: Ctxt (M.Map Name (S.Set Name)), -- ^ Specific error handlers
167167 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
169170 }
170171
171172data SizeChange = Smaller | Same | Bigger | Unknown
@@ -236,7 +237,7 @@ idrisInit = IState initContext [] [] emptyContext emptyContext emptyContext
236237 [] [] defaultOpts 6 [] [] [] [] [] [] [] [] [] [] [] [] []
237238 [] [] Nothing [] Nothing [] [] Nothing [] Hidden False [] Nothing [] [] RawOutput
238239 True defaultTheme stdout [] (0, emptyContext) emptyContext M.empty
239− AutomaticWidth
240+ AutomaticWidth S.empty
240241
241242-- | The monad for the main REPL - reading and processing files and updating
242243-- global state (hence the IO inner monad).
src/Idris/ElabDecls.hs+13−4
@@ -37,6 +37,7 @@ import Data.Maybe
3737import Debug.Trace
3838
3939import qualified Data.Map as Map
40+import qualified Data.Set as S
4041import qualified Data.Text as T
4142import Data.Char(isLetter, toLower)
4243import Data.List.Split (splitOn)
@@ -204,8 +205,15 @@ inaccessibleArgs _ _ = []
204205
205206elabPostulate :: ElabInfo -> SyntaxInfo -> Docstring ->
206207 FC -> FnOpts -> Name -> PTerm -> Idris ()
207−elabPostulate info syn doc fc opts n ty
208− = do elabType info syn doc [] fc opts n ty
208+elabPostulate info syn doc fc opts n ty = do
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+ -
209217 -- make sure it's collapsible, so it is never needed at run time
210218 -- start by getting the elaborated type
211219 ctxt <- getContext
@@ -214,6 +222,7 @@ elabPostulate info syn doc fc opts n ty
214222 [ty] -> return ty
215223 ist <- getIState
216224 let (ap, _) = unApply (getRetTy (normalise ctxt [] fty))
225+
217226 logLvl 5 $ "Checking collapsibility of " ++ show (ap, fty)
218227 let postOK = case ap of
219228 P _ tn _ -> case lookupCtxt tn
@@ -223,8 +232,8 @@ elabPostulate info syn doc fc opts n ty
223232 _ -> False
224233 when (not postOK)
225234 $ tclift $ tfail (At fc (NonCollapsiblePostulate n))
226− -- remove it from the deferred definitions list
227− solveDeferred n
235+-}
236+
228237
229238elabData :: ElabInfo -> SyntaxInfo -> Docstring -> [(Name, Docstring)] -> FC -> DataOpts -> PData -> Idris ()
230239elabData info syn doc argDocs fc opts (PLaterdecl n t_in)
src/Idris/Erasure.hs+5
@@ -90,6 +90,11 @@ performUsageAnalysis = do
9090 when checkEnabled $
9191 mapM_ (checkAccessibility opt) usage
9292
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+
9398 -- Store the usage info in the internal state.
9499 mapM_ (storeUsage cg) usage
95100