git.iko.soy/Idris-dev
on master help sign in
Tinkering with error reporting
commitf9fb3634e91d0c9c3aa37c51461f67b056f3b0a2 authorEdwin Brady <eb@cs.st-andrews.ac.uk> dateMon 10 Oct 2011, 18:43 (15 years ago) parent59c1eb1
5 files changed+48−29
compare with master
unifiedsplit
src/Core/ProofState.hs+4−4 src/Core/TT.hs+14−4 src/Core/Unify.hs+4−7 src/Idris/AbsSyntax.hs−14 src/Idris/Error.hs+26
src/Core/ProofState.hs+4−4
@@ -133,7 +133,7 @@ goal h tm = g [] tm where
133133 | otherwise
134134 = gb env b `mplus` g ((n, b):env) sc
135135 g env (App f a) = g env f `mplus` g env a
136− g env t = Error "Can't find hole"
136+ g env t = fail "Can't find hole"
137137
138138 gb env (Let t v) = g env t `mplus` g env v
139139 gb env (Guess t v) = g env t `mplus` g env v
@@ -323,10 +323,10 @@ processTactic QED ps = case holes ps of
323323 (tm', ty') <- recheck (context ps) [] tm
324324 return (ps { done = True, pterm = tm' },
325325 "Proof complete: " ++ showEnv [] tm')
326− _ -> Error "Still holes to fill."
326+ _ -> fail "Still holes to fill."
327327processTactic ProofState ps = return (ps, showEnv [] (pterm ps))
328328processTactic Undo ps = case previous ps of
329− Nothing -> Error "Nothing to undo."
329+ Nothing -> fail "Nothing to undo."
330330 Just pold -> return (pold, "")
331331processTactic EndUnify ps = let (h, ns) = unified ps
332332 tm' = updateSolved ns (pterm ps) in
@@ -344,7 +344,7 @@ processTactic EndUnify ps = let (h, ns) = unified ps
344344 updateSolved xs t = t
345345processTactic t ps
346346 = case holes ps of
347− [] -> Error "Nothing to fill in."
347+ [] -> fail "Nothing to fill in."
348348 (h:_) -> do let n = nextname ps
349349 ps' <- execStateT (process t h) ps
350350 return (ps' { previous = Just ps, plog = "" }, plog ps')
src/Core/TT.hs+14−4
@@ -23,13 +23,20 @@ data Option = SetInSet
2323 | CheckConv
2424 deriving Eq
2525
26+data Err = Msg String
27+ | CantUnify Term Term
28+ deriving Eq
29+
30+instance Show Err where
31+ show (Msg s) = s
32+
2633data TC a = OK a
27− | Error String -- TMP! Make this an informative data structure
34+ | Error Err
2835 deriving (Eq, Functor)
2936
3037instance Show a => Show (TC a) where
3138 show (OK x) = show x
32− show (Error str) = "Error: " ++ str
39+ show (Error str) = "Error: " ++ (show str)
3340
3441-- at some point, this instance should also carry type checking options
3542-- (e.g. Set:Set)
@@ -39,10 +46,13 @@ instance Monad TC where
3946 x >>= k = case x of
4047 OK v -> k v
4148 Error e -> Error e
42− fail = Error
49+ fail e = Error (Msg e)
50+
51+tfail :: Err -> TC a
52+tfail e = Error e
4353
4454instance MonadPlus TC where
45− mzero = Error "Unknown error"
55+ mzero = fail "Unknown error"
4656 (OK x) `mplus` _ = OK x
4757 _ `mplus` (OK y) = OK y
4858 err `mplus` _ = err
src/Core/Unify.hs+4−7
@@ -14,13 +14,10 @@ import Debug.Trace
1414-- to help the rest of the unification
1515
1616unify :: Context -> Env -> TT Name -> TT Name -> TC [(Name, TT Name)]
17−unify ctxt env x y
18− = --case un' [] x y of -- try without normalising first, for speed
19− -- OK v -> return v
20− -- _ ->
21− case un' [] (normalise ctxt env x) (normalise ctxt env y) of
22− OK v -> return v
23− _ -> fail $ "Can't unify " ++ showEnv env x ++ " and " ++ showEnv env y
17+unify ctxt env topx topy
18+ = case un' [] (normalise ctxt env topx) (normalise ctxt env topy) of
19+ OK v -> return v
20+ _ -> tfail $ CantUnify topx topy
2421 where
2522 un' bnames (P Bound x _) (P Bound y _)
2623 | (x,y) `elem` bnames = return []
src/Idris/AbsSyntax.hs−14
@@ -45,11 +45,6 @@ updateContext f = do i <- get; put (i { tt_ctxt = f (tt_ctxt i) } )
4545iputStrLn :: String -> Idris ()
4646iputStrLn = lift.putStrLn
4747
48−tclift :: Show a => TC a -> Idris a
49−tclift tc = case tc of
50− OK v -> return v
51− err -> fail (show err)
52−
5348setLogLevel :: Int -> Idris ()
5449setLogLevel l = do i <- get
5550 let opts = idris_options i
@@ -70,15 +65,6 @@ logLvl l str = do i <- get
7065iLOG :: String -> Idris ()
7166iLOG = logLvl 1
7267
73−-- Taken from the library source code - for ghc 6.12/7 compatibility
74−liftCatch :: (m (a,s) -> (e -> m (a,s)) -> m (a,s)) ->
75− StateT s m a -> (e -> StateT s m a) -> StateT s m a
76−liftCatch catchError m h =
77− StateT $ \s -> runStateT m s `catchError` \e -> runStateT (h e) s
78−
79−idrisCatch :: Idris a -> (IOError -> Idris a) -> Idris a
80−idrisCatch op handler = liftCatch catch op handler
81−
8268-- Commands in the REPL
8369
8470data Command = Quit | Help | Eval PTerm
src/Idris/Error.hs+26
@@ -1,6 +1,12 @@
11module Idris.Error where
22
33import Idris.AbsSyntax
4+import Idris.Delaborate
5+
6+import Core.TT
7+import Core.Typecheck
8+
9+import Control.Monad.State
410import System.IO.Error
511
612report :: IOError -> String
@@ -8,3 +14,23 @@ report e
814 | isUserError e = ioeGetErrorString e
915 | otherwise = show e
1016
17+-- Taken from the library source code - for ghc 6.12/7 compatibility
18+liftCatch :: (m (a,s) -> (e -> m (a,s)) -> m (a,s)) ->
19+ StateT s m a -> (e -> StateT s m a) -> StateT s m a
20+liftCatch catchError m h =
21+ StateT $ \s -> runStateT m s `catchError` \e -> runStateT (h e) s
22+
23+idrisCatch :: Idris a -> (IOError -> Idris a) -> Idris a
24+idrisCatch op handler = liftCatch catch op handler
25+
26+pshow :: IState -> Err -> String
27+pshow i (Msg s) = s
28+pshow i (CantUnify x y) = "Can't unify " ++ show (delab i x) ++
29+ " with " ++ show (delab i y)
30+
31+tclift :: Show a => TC a -> Idris a
32+tclift tc = case tc of
33+ OK v -> return v
34+ Error err -> do i <- get
35+ fail (pshow i err)
36+