git.iko.soy/Idris-dev
on master help sign in
Initial partial version of REPL error reflection
commitb0e43f07449b79c0d98198573bcb9c9354ed2ef6 authorDavid Raymond Christiansen <david@davidchristiansen.dk> dateThu 9 Jan 2014, 17:18 (13 years ago) parent5361547
6 files changed+72−24
compare with master
unifiedsplit
libs/base/Language/Reflection/Errors.idr+2 src/Idris/Core/Execute.hs−8 src/Idris/Core/TT.hs+8 src/Idris/ElabTerm.hs+33−3 src/Idris/Error.hs+16 src/Idris/REPL.hs+13−13
libs/base/Language/Reflection/Errors.idr+2
@@ -40,3 +40,5 @@ data ErrorReportPart = Message String
4040
4141
4242-- Error reports become functions in List (String, TT) -> Err -> ErrorReport
43+ErrorHandler : Type
44+ErrorHandler = Err -> Maybe (List ErrorReportPart)
src/Idris/Core/Execute.hs−8
@@ -499,14 +499,6 @@ getFTy (EP _ (UN t) _) =
499499 _ -> Nothing
500500getFTy _ = Nothing
501501
502−unList :: Term -> Maybe [Term]
503−unList tm = case unApply tm of
504− (nil, [_]) -> Just []
505− (cons, ([_, x, xs])) ->
506− do rest <- unList xs
507− return $ x:rest
508− (f, args) -> Nothing
509−
510502unEList :: ExecVal -> Maybe [ExecVal]
511503unEList tm = case unApplyV tm of
512504 (nil, [_]) -> Just []
src/Idris/Core/TT.hs+8
@@ -793,6 +793,14 @@ mkApp :: TT n -> [TT n] -> TT n
793793mkApp f [] = f
794794mkApp f (a:as) = mkApp (App f a) as
795795
796+unList :: Term -> Maybe [Term]
797+unList tm = case unApply tm of
798+ (nil, [_]) -> Just []
799+ (cons, ([_, x, xs])) ->
800+ do rest <- unList xs
801+ return $ x:rest
802+ (f, args) -> Nothing
803+
796804forget :: TT Name -> Raw
797805forget tm = fe [] tm
798806 where
src/Idris/ElabTerm.hs+33−3
@@ -5,15 +5,18 @@ module Idris.ElabTerm where
55import Idris.AbsSyntax
66import Idris.DSL
77import Idris.Delaborate
8+import Idris.Error
89import Idris.ProofSearch
910
1011import Idris.Core.Elaborate hiding (Tactic(..))
1112import Idris.Core.TT
1213import Idris.Core.Evaluate
14+import Idris.Core.Typecheck (check)
1315
1416import Control.Monad
1517import Control.Monad.State
1618import Data.List
19+import Data.Maybe (mapMaybe)
1720
1821import Debug.Trace
1922
@@ -1352,9 +1355,36 @@ reflectEnv = foldr consToEnvList emptyEnvList
13521355
13531356-- | Reflect an error into the internal datatype of Idris -- TODO
13541357reflectErr :: Err -> Raw
1355−reflectErr (Msg msg) = raw_apply (Var (NS (UN "Msg") ["Reflection", "Language"])) [reflectConstant (Str msg)]
1356−reflectErr (InternalMsg msg) = raw_apply (Var (NS (UN "InternalMsg") ["Reflection", "Language"])) [reflectConstant (Str msg)]
1357−reflectErr x = trace ("Couldn't reflect error " ++ show x) raw_apply (Var (NS (UN "Msg") ["Reflection", "Language"])) [reflectConstant (Str $ show x)]
1358+reflectErr (Msg msg) = raw_apply (Var (NS (UN "Msg") ["Errors", "Reflection", "Language"])) [RConstant (Str msg)]
1359+reflectErr (InternalMsg msg) = raw_apply (Var (NS (UN "InternalMsg") ["Errors", "Reflection", "Language"])) [RConstant (Str msg)]
1360+reflectErr x = raw_apply (Var (NS (UN "Msg") ["Errors", "Reflection", "Language"])) [RConstant . Str $ "Default reflection: " ++ show x]
1361+
1362+withErrorReflection :: Idris a -> Idris a
1363+withErrorReflection x = idrisCatch x (\ e -> handle e >>= ierror)
1364+ where handle :: Err -> Idris Err
1365+ handle e = do ist <- getIState
1366+ let handlers = idris_errorhandlers ist
1367+ let reports = map (\n -> RApp (Var n) (reflectErr e)) handlers
1368+
1369+ -- Typecheck error handlers - if this fails, then something else was wrong earlier!
1370+ handlers <- case mapM (check (tt_ctxt ist) []) reports of
1371+ Error e -> do formatted <- showErr e
1372+ ierror . InternalMsg $
1373+ "Type error during error reflection: " ++ formatted
1374+ OK hs -> return hs
1375+
1376+ -- Normalize error handler terms to produce the new messages
1377+ ctxt <- getContext
1378+ let results = map (normalise ctxt []) (map fst handlers)
1379+
1380+
1381+ errorparts <- mapM reifyReportPart (concat (mapMaybe unList (mapMaybe fromTTMaybe results)))
1382+ newMsgs <- mapM renderReportPart errorparts
1383+ return . Msg $ concat (intersperse " " newMsgs)
1384+
1385+ fromTTMaybe :: Term -> Maybe Term -- WARNING: Assumes the term has type Maybe a
1386+ fromTTMaybe (App (App (P (DCon _ _) (NS (UN "Just") _) _) ty) tm) = Just tm
1387+ fromTTMaybe x = Nothing
13581388
13591389envTupleType :: Raw
13601390envTupleType
src/Idris/Error.hs+16
@@ -38,6 +38,7 @@ report e
3838idrisCatch :: Idris a -> (Err -> Idris a) -> Idris a
3939idrisCatch = catchError
4040
41+
4142setAndReport :: Err -> Idris ()
4243setAndReport e = do ist <- getIState
4344 let h = idris_outh ist
@@ -71,3 +72,18 @@ getErrLine _ = 0
7172getErrColumn :: Err -> Int
7273getErrColumn (At (FC _ _ c) _) = c
7374getErrColumn _ = 0
75+
76+data ErrorReportPart = Message String
77+ | Name Name
78+ | Term Term
79+ deriving (Show)
80+
81+reifyReportPart :: Term -> Idris ErrorReportPart
82+reifyReportPart (App (P (DCon _ _) (NS (UN "Message") ["Errors", "Reflection", "Language"]) _) (Constant (Str msg))) =
83+ return (Message msg)
84+reifyReportPart x = ierror . Msg $ "could not reify " ++ show x
85+
86+renderReportPart :: ErrorReportPart -> Idris String
87+renderReportPart (Message str) = return str
88+renderReportPart (Name n) = return (show n) -- TODO colouring
89+renderReportPart (Term t) = return (show t) -- TODO pretty-print and colour
src/Idris/REPL.hs+13−13
@@ -442,19 +442,19 @@ process h fn (ChangeDirectory f)
442442 = do runIO $ setCurrentDirectory f
443443 return ()
444444process h fn (Eval t)
445− = do (tm, ty) <- elabVal toplevel False t
446− ctxt <- getContext
447− let tm' = force (normaliseAll ctxt [] tm)
448− let ty' = force (normaliseAll ctxt [] ty)
449− -- Add value to context, call it "it"
450− updateContext (addCtxtDef (UN "it") (Function ty' tm'))
451− ist <- getIState
452− logLvl 3 $ "Raw: " ++ show (tm', ty')
453− logLvl 10 $ "Debug: " ++ showEnvDbg [] tm'
454− imp <- impShow
455− c <- colourise
456− ihPrintResult h (showImp (Just ist) imp c (delab ist tm') ++ " : " ++
457− showImp (Just ist) imp c (delab ist ty'))
445+ = withErrorReflection $ do (tm, ty) <- elabVal toplevel False t
446+ ctxt <- getContext
447+ let tm' = force (normaliseAll ctxt [] tm)
448+ let ty' = force (normaliseAll ctxt [] ty)
449+ -- Add value to context, call it "it"
450+ updateContext (addCtxtDef (UN "it") (Function ty' tm'))
451+ ist <- getIState
452+ logLvl 3 $ "Raw: " ++ show (tm', ty')
453+ logLvl 10 $ "Debug: " ++ showEnvDbg [] tm'
454+ imp <- impShow
455+ c <- colourise
456+ ihPrintResult h (showImp (Just ist) imp c (delab ist tm') ++ " : " ++
457+ showImp (Just ist) imp c (delab ist ty'))
458458process h fn (ExecVal t)
459459 = do ctxt <- getContext
460460 ist <- getIState