git.iko.soy/Idris-dev
on master help sign in
Show error contexts with pretty-printer
b5e97e4David Raymond Christiansen
src/Idris/Core/Unify.hs+7−7
compare with master
unifiedsplit
@@ -76,7 +76,7 @@ match_unify ctxt env topx topy dont holes =
76 | otherwise = do UI s f <- get
76 | otherwise = do UI s f <- get
77 let r = recoverable x y
77 let r = recoverable x y
78 let err = CantUnify r
78 let err = CantUnify r
79− topx topy (CantUnify r x y (Msg "") [] s) (errEnv env) s
79+ topx topy (CantUnify r x y (Msg "") (errEnv env) s) (errEnv env) s
80 if (not r) then lift $ tfail err
80 if (not r) then lift $ tfail err
81 else do put (UI s ((x, y, env, err) : f))
81 else do put (UI s ((x, y, env, err) : f))
82 lift $ tfail err
82 lift $ tfail err
@@ -90,7 +90,7 @@ match_unify ctxt env topx topy dont holes =
90 uB bnames x y = do UI s f <- get
90 uB bnames x y = do UI s f <- get
91 let r = recoverable (binderTy x) (binderTy y)
91 let r = recoverable (binderTy x) (binderTy y)
92 let err = CantUnify r topx topy
92 let err = CantUnify r topx topy
93− (CantUnify r (binderTy x) (binderTy y) (Msg "") [] s)
93+ (CantUnify r (binderTy x) (binderTy y) (Msg "") (errEnv env) s)
94 (errEnv env) s
94 (errEnv env) s
95 put (UI s ((binderTy x, binderTy y, env, err) : f))
95 put (UI s ((binderTy x, binderTy y, env, err) : f))
96 return []
96 return []
@@ -104,7 +104,7 @@ match_unify ctxt env topx topy dont holes =
104 unifyFail x y = do UI s f <- get
104 unifyFail x y = do UI s f <- get
105 let r = recoverable x y
105 let r = recoverable x y
106 let err = CantUnify r
106 let err = CantUnify r
107− topx topy (CantUnify r x y (Msg "") [] s) (errEnv env) s
107+ topx topy (CantUnify r x y (Msg "") (errEnv env) s) (errEnv env) s
108 put (UI s ((x, y, env, err) : f))
108 put (UI s ((x, y, env, err) : f))
109 lift $ tfail err
109 lift $ tfail err
110 combine bnames as [] = return as
110 combine bnames as [] = return as
@@ -309,7 +309,7 @@ unify ctxt env topx topy dont holes =
309 | otherwise = do UI s f <- get
309 | otherwise = do UI s f <- get
310 let r = recoverable x y
310 let r = recoverable x y
311 let err = CantUnify r
311 let err = CantUnify r
312− topx topy (CantUnify r x y (Msg "") [] s) (errEnv env) s
312+ topx topy (CantUnify r x y (Msg "") (errEnv env) s) (errEnv env) s
313 if (not r) then lift $ tfail err
313 if (not r) then lift $ tfail err
314 else do put (UI s ((x, y, env, err) : f))
314 else do put (UI s ((x, y, env, err) : f))
315 return [] -- lift $ tfail err
315 return [] -- lift $ tfail err
@@ -436,7 +436,7 @@ unify ctxt env topx topy dont holes =
436 = do UI s f <- get
436 = do UI s f <- get
437 let r = recoverable x y
437 let r = recoverable x y
438 let err = CantUnify r
438 let err = CantUnify r
439− topx topy (CantUnify r x y (Msg "") [] s) (errEnv env) s
439+ topx topy (CantUnify r x y (Msg "") (errEnv env) s) (errEnv env) s
440 put (UI s ((topx, topy, env, err) : f))
440 put (UI s ((topx, topy, env, err) : f))
441 return []
441 return []
442
442
@@ -444,7 +444,7 @@ unify ctxt env topx topy dont holes =
444 unifyFail x y = do UI s f <- get
444 unifyFail x y = do UI s f <- get
445 let r = recoverable x y
445 let r = recoverable x y
446 let err = CantUnify r
446 let err = CantUnify r
447− topx topy (CantUnify r x y (Msg "") [] s) (errEnv env) s
447+ topx topy (CantUnify r x y (Msg "") (errEnv env) s) (errEnv env) s
448 put (UI s ((topx, topy, env, err) : f))
448 put (UI s ((topx, topy, env, err) : f))
449 lift $ tfail err
449 lift $ tfail err
450
450
@@ -466,7 +466,7 @@ unify ctxt env topx topy dont holes =
466 uB bnames x y = do UI s f <- get
466 uB bnames x y = do UI s f <- get
467 let r = recoverable (binderTy x) (binderTy y)
467 let r = recoverable (binderTy x) (binderTy y)
468 let err = CantUnify r topx topy
468 let err = CantUnify r topx topy
469− (CantUnify r (binderTy x) (binderTy y) (Msg "") [] s)
469+ (CantUnify r (binderTy x) (binderTy y) (Msg "") (errEnv env) s)
470 (errEnv env) s
470 (errEnv env) s
471 put (UI s ((binderTy x, binderTy y, env, err) : f))
471 put (UI s ((binderTy x, binderTy y, env, err) : f))
472 return [] -- lift $ tfail err
472 return [] -- lift $ tfail err
src/Idris/Delaborate.hs+14−8
@@ -153,22 +153,22 @@ pprintErr' i (CantUnify _ x y e sc s) =
153 Msg "" -> empty
153 Msg "" -> empty
154 _ -> line <> line <> text "Specifically:" <>
154 _ -> line <> line <> text "Specifically:" <>
155 indented (pprintErr' i e) <>
155 indented (pprintErr' i e) <>
156− if (opt_errContext (idris_options i)) then text $ showSc i sc else empty
156+ if (opt_errContext (idris_options i)) then showSc i sc else empty
157pprintErr' i (CantConvert x y env) =
157pprintErr' i (CantConvert x y env) =
158 text "Can't convert" <>
158 text "Can't convert" <>
159 indented (pprintTerm' i (map (\ (n, b) -> (n, False)) env) (delab i x)) <$>
159 indented (pprintTerm' i (map (\ (n, b) -> (n, False)) env) (delab i x)) <$>
160 text "with" <>
160 text "with" <>
161 indented (pprintTerm' i (map (\ (n, b) -> (n, False)) env) (delab i y)) <>
161 indented (pprintTerm' i (map (\ (n, b) -> (n, False)) env) (delab i y)) <>
162− if (opt_errContext (idris_options i)) then line <> text (showSc i env) else empty
162+ if (opt_errContext (idris_options i)) then line <> showSc i env else empty
163pprintErr' i (CantSolveGoal x env) =
163pprintErr' i (CantSolveGoal x env) =
164 text "Can't solve goal " <>
164 text "Can't solve goal " <>
165 indented (pprintTerm' i (map (\ (n, b) -> (n, False)) env) (delab i x)) <>
165 indented (pprintTerm' i (map (\ (n, b) -> (n, False)) env) (delab i x)) <>
166− if (opt_errContext (idris_options i)) then line <> text (showSc i env) else empty
166+ if (opt_errContext (idris_options i)) then line <> showSc i env else empty
167pprintErr' i (UnifyScope n out tm env) =
167pprintErr' i (UnifyScope n out tm env) =
168 text "Can't unify" <> indented (annName n) <+>
168 text "Can't unify" <> indented (annName n) <+>
169 text "with" <> indented (pprintTerm' i (map (\ (n, b) -> (n, False)) env) (delab i tm)) <+>
169 text "with" <> indented (pprintTerm' i (map (\ (n, b) -> (n, False)) env) (delab i tm)) <+>
170 text "as" <> indented (annName out) <> text "is not in scope" <>
170 text "as" <> indented (annName out) <> text "is not in scope" <>
171− if (opt_errContext (idris_options i)) then line <> text (showSc i env) else empty
171+ if (opt_errContext (idris_options i)) then line <> showSc i env else empty
172pprintErr' i (CantInferType t) = text "Can't infer type for" <+> text t
172pprintErr' i (CantInferType t) = text "Can't infer type for" <+> text t
173pprintErr' i (NonFunctionType f ty) =
173pprintErr' i (NonFunctionType f ty) =
174 pprintTerm i (delab i f) <+>
174 pprintTerm i (delab i f) <+>
@@ -185,7 +185,7 @@ pprintErr' i (InfiniteUnify x tm env) =
185 text "Unifying" <+> annName' x (showbasic x) <+> text "and" <+>
185 text "Unifying" <+> annName' x (showbasic x) <+> text "and" <+>
186 pprintTerm' i (map (\ (n, b) -> (n, False)) env) (delab i tm) <+>
186 pprintTerm' i (map (\ (n, b) -> (n, False)) env) (delab i tm) <+>
187 text "would lead to infinite value" <>
187 text "would lead to infinite value" <>
188− if (opt_errContext (idris_options i)) then line <> text (showSc i env) else empty
188+ if (opt_errContext (idris_options i)) then line <> showSc i env else empty
189pprintErr' i (NotInjective p x y) =
189pprintErr' i (NotInjective p x y) =
190 text "Can't verify injectivity of" <+> pprintTerm i (delab i p) <+>
190 text "Can't verify injectivity of" <+> pprintTerm i (delab i p) <+>
191 text " when unifying" <+> pprintTerm i (delab i x) <+> text "and" <+>
191 text " when unifying" <+> pprintTerm i (delab i x) <+> text "and" <+>
@@ -233,9 +233,15 @@ annName n = annName' n (show n)
233annName' :: Name -> String -> Doc OutputAnnotation
233annName' :: Name -> String -> Doc OutputAnnotation
234annName' n str = annotate (AnnName n Nothing Nothing) (text str)
234annName' n str = annotate (AnnName n Nothing Nothing) (text str)
235
235
236−showSc i [] = ""
236+showSc :: IState -> [(Name, Term)] -> Doc OutputAnnotation
237+showSc i [] = empty
237−showSc i xs = "\n\nIn context:\n" ++ showSep "\n" (map showVar (reverse xs))
238+showSc i xs = line <> line <> text "In context:" <>
238− where showVar (x, y) = "\t" ++ showbasic x ++ " : " ++ show (delab i y)
239+ indented (vsep (reverse (showSc' [] xs)))
240+ where showSc' bnd [] = []
241+ showSc' bnd ((n, ty):ctxt) =
242+ let this = bindingOf n False <+> colon <+> pprintTerm' i bnd (delab i ty)
243+ in this : showSc' ((n,False):bnd) ctxt
244+
239
245
240showqual :: IState -> Name -> String
246showqual :: IState -> Name -> String
241showqual i n = showName (Just i) [] False False (dens n)
247showqual i n = showName (Just i) [] False False (dens n)