b0e43f0 · Idris-dev · git.iko.soy

libs/base/Language/Reflection/Errors.idr+2

compare with master

unifiedsplit

@@ -40,3 +40,5 @@ data ErrorReportPart = Message String

40

41

42-- 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) _) =

499 _ -> Nothing

500getFTy _ = Nothing

501

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−

510unEList :: ExecVal -> Maybe [ExecVal]

502unEList :: ExecVal -> Maybe [ExecVal]

511unEList tm = case unApplyV tm of

503unEList tm = case unApplyV tm of

512 (nil, [_]) -> Just []

504 (nil, [_]) -> Just []

src/Idris/Core/TT.hs+8

@@ -793,6 +793,14 @@ mkApp :: TT n -> [TT n] -> TT n

793mkApp f [] = f

794mkApp f (a:as) = mkApp (App f a) as

795

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+

796forget :: TT Name -> Raw

804forget :: TT Name -> Raw

797forget tm = fe [] tm

805forget tm = fe [] tm

798 where

806 where

src/Idris/ElabTerm.hs+33−3

@@ -5,15 +5,18 @@ module Idris.ElabTerm where

5import Idris.AbsSyntax

6import Idris.DSL

7import Idris.Delaborate

8+import Idris.Error

8import Idris.ProofSearch

9import Idris.ProofSearch

9

10

10import Idris.Core.Elaborate hiding (Tactic(..))

11import Idris.Core.Elaborate hiding (Tactic(..))

11import Idris.Core.TT

12import Idris.Core.TT

12import Idris.Core.Evaluate

13import Idris.Core.Evaluate

14+import Idris.Core.Typecheck (check)

13

15

14import Control.Monad

16import Control.Monad

15import Control.Monad.State

17import Control.Monad.State

16import Data.List

18import Data.List

19+import Data.Maybe (mapMaybe)

17

20

18import Debug.Trace

21import Debug.Trace

19

22

@@ -1352,9 +1355,36 @@ reflectEnv = foldr consToEnvList emptyEnvList

1352

1355

1353-- | Reflect an error into the internal datatype of Idris -- TODO

1356-- | Reflect an error into the internal datatype of Idris -- TODO

1354reflectErr :: Err -> Raw

1357reflectErr :: Err -> Raw

1355−reflectErr (Msg msg) = raw_apply (Var (NS (UN "Msg") ["Reflection", "Language"])) [reflectConstant (Str msg)]

1358+reflectErr (Msg msg) = raw_apply (Var (NS (UN "Msg") ["Errors", "Reflection", "Language"])) [RConstant (Str msg)]

1356−reflectErr (InternalMsg msg) = raw_apply (Var (NS (UN "InternalMsg") ["Reflection", "Language"])) [reflectConstant (Str msg)]

1359+reflectErr (InternalMsg msg) = raw_apply (Var (NS (UN "InternalMsg") ["Errors", "Reflection", "Language"])) [RConstant (Str msg)]

1357−reflectErr x = trace ("Couldn't reflect error " ++ show x) raw_apply (Var (NS (UN "Msg") ["Reflection", "Language"])) [reflectConstant (Str $ show x)]

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

1358

1388

1359envTupleType :: Raw

1389envTupleType :: Raw

1360envTupleType

1390envTupleType

src/Idris/Error.hs+16

@@ -38,6 +38,7 @@ report e

38idrisCatch :: Idris a -> (Err -> Idris a) -> Idris a

39idrisCatch = catchError

40

41+

41setAndReport :: Err -> Idris ()

42setAndReport :: Err -> Idris ()

42setAndReport e = do ist <- getIState

43setAndReport e = do ist <- getIState

43 let h = idris_outh ist

44 let h = idris_outh ist

@@ -71,3 +72,18 @@ getErrLine _ = 0

71getErrColumn :: Err -> Int

72getErrColumn :: Err -> Int

72getErrColumn (At (FC _ _ c) _) = c

73getErrColumn (At (FC _ _ c) _) = c

73getErrColumn _ = 0

74getErrColumn _ = 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)

442 = do runIO $ setCurrentDirectory f

443 return ()

444process h fn (Eval t)

445− = do (tm, ty) <- elabVal toplevel False t

445+ = withErrorReflection $ do (tm, ty) <- elabVal toplevel False t

446− ctxt <- getContext

446+ ctxt <- getContext

447− let tm' = force (normaliseAll ctxt [] tm)

447+ let tm' = force (normaliseAll ctxt [] tm)

448− let ty' = force (normaliseAll ctxt [] ty)

448+ let ty' = force (normaliseAll ctxt [] ty)

449− -- Add value to context, call it "it"

449+ -- Add value to context, call it "it"

450− updateContext (addCtxtDef (UN "it") (Function ty' tm'))

450+ updateContext (addCtxtDef (UN "it") (Function ty' tm'))

451− ist <- getIState

451+ ist <- getIState

452− logLvl 3 $ "Raw: " ++ show (tm', ty')

452+ logLvl 3 $ "Raw: " ++ show (tm', ty')

453− logLvl 10 $ "Debug: " ++ showEnvDbg [] tm'

453+ logLvl 10 $ "Debug: " ++ showEnvDbg [] tm'

454− imp <- impShow

454+ imp <- impShow

455− c <- colourise

455+ c <- colourise

456− ihPrintResult h (showImp (Just ist) imp c (delab ist tm') ++ " : " ++

456+ ihPrintResult h (showImp (Just ist) imp c (delab ist tm') ++ " : " ++

457− showImp (Just ist) imp c (delab ist ty'))

457+ showImp (Just ist) imp c (delab ist ty'))

458process h fn (ExecVal t)

459 = do ctxt <- getContext

460 ist <- getIState