git.iko.soy/Idris-dev
on master help sign in
Merge pull request #483 from yfyf/indent_errors
7e1005aEdwin Brady
src/Idris/Delaborate.hs+16−9
compare with master
unifiedsplit
@@ -93,6 +93,12 @@ delabTy' ist imps tm fullname = de [] imps tm
93 imp (PConstraint p l _ d) arg = PConstraint p l arg d
93 imp (PConstraint p l _ d) arg = PConstraint p l arg d
94 imp (PTacImplicit p l n sc _ d) arg = PTacImplicit p l n sc arg d
94 imp (PTacImplicit p l n sc _ d) arg = PTacImplicit p l n sc arg d
95
95
96+
97+indented text = boxIt '\n' $ unlines $ map ('\t':) $ lines text where
98+ boxIt c text = (c:text) ++ if last text == c
99+ then ""
100+ else [c]
101+
96pshow :: IState -> Err -> String
102pshow :: IState -> Err -> String
97pshow i (Msg s) = s
103pshow i (Msg s) = s
98pshow i (InternalMsg s) = "INTERNAL ERROR: " ++ show s ++
104pshow i (InternalMsg s) = "INTERNAL ERROR: " ++ show s ++
@@ -101,25 +107,26 @@ pshow i (InternalMsg s) = "INTERNAL ERROR: " ++ show s ++
101pshow i (CantUnify _ x y e sc s)
107pshow i (CantUnify _ x y e sc s)
102 = let imps = opt_showimp (idris_options i) in
108 = let imps = opt_showimp (idris_options i) in
103 let colour = idris_colourRepl i in
109 let colour = idris_colourRepl i in
104− "Can't unify " ++ showImp (Just i) imps colour (delab i x)
110+ "Can't unify" ++ indented (showImp (Just i) imps colour (delab i x))
105− ++ " with " ++ showImp (Just i) imps colour (delab i y) ++
111+ ++ "with" ++ indented (showImp (Just i) imps colour (delab i y)) ++
106-- " (" ++ show x ++ " and " ++ show y ++ ") " ++
112-- " (" ++ show x ++ " and " ++ show y ++ ") " ++
107 case e of
113 case e of
108 Msg "" -> ""
114 Msg "" -> ""
109− _ -> "\n\nSpecifically:\n\t" ++ pshow i e ++
115+ _ -> "\nSpecifically:" ++
116+ indented (pshow i e) ++
110− if (opt_errContext (idris_options i)) then showSc i sc else ""
117+ if (opt_errContext (idris_options i)) then showSc i sc else ""
111pshow i (CantConvert x y env)
118pshow i (CantConvert x y env)
112 = let imps = opt_showimp (idris_options i) in
119 = let imps = opt_showimp (idris_options i) in
113 let colour = idris_colourRepl i in
120 let colour = idris_colourRepl i in
114− "Can't convert " ++ showImp (Just i) imps colour (delab i x) ++ " with "
121+ "Can't convert" ++ indented (showImp (Just i) imps colour (delab i x)) ++ "with"
115− ++ showImp (Just i) imps colour (delab i y) ++
122+ ++ indented (showImp (Just i) imps colour (delab i y)) ++
116 if (opt_errContext (idris_options i)) then showSc i env else ""
123 if (opt_errContext (idris_options i)) then showSc i env else ""
117pshow i (UnifyScope n out tm env)
124pshow i (UnifyScope n out tm env)
118 = let imps = opt_showimp (idris_options i) in
125 = let imps = opt_showimp (idris_options i) in
119 let colour = idris_colourRepl i in
126 let colour = idris_colourRepl i in
120− "Can't unify " ++ show n ++ " with "
127+ "Can't unify" ++ indented (show n) ++ "with"
121− ++ showImp (Just i) imps colour (delab i tm) ++ " as " ++ show out ++
128+ ++ indented (showImp (Just i) imps colour (delab i tm)) ++ "as" ++
122− " is not in scope" ++
129+ indented (show out) ++ "is not in scope" ++
123 if (opt_errContext (idris_options i)) then showSc i env else ""
130 if (opt_errContext (idris_options i)) then showSc i env else ""
124pshow i (CantInferType t)
131pshow i (CantInferType t)
125 = "Can't infer type for " ++ t
132 = "Can't infer type for " ++ t
test/reg010/expected+9−2
@@ -1,5 +1,12 @@
1reg010.idr:5:When elaborating right hand side of usubst.unsafeSubst:
1reg010.idr:5:When elaborating right hand side of usubst.unsafeSubst:
2−Can't unify P x with P y
2+Can't unify
3+ P x
4+with
5+ P y
3
6
4Specifically:
7Specifically:
5− Can't unify P x with P y
8+ Can't unify
9+ P x
10+ with
11+ P y
12+
test/test020/expected+9−2
@@ -1,7 +1,14 @@
1When elaborating right hand side of foo:
1When elaborating right hand side of foo:
2−test020a.idr:16:Can't unify Vect n a with List a
2+test020a.idr:16:Can't unify
3+ Vect n a
4+with
5+ List a
3
6
4Specifically:
7Specifically:
5− Can't unify Vect n a with List a
8+ Can't unify
9+ Vect n a
10+ with
11+ List a
12+
6[3, 2, 1]
13[3, 2, 1]
7Number 42
14Number 42
test/test030/expected+9−2
@@ -1,5 +1,12 @@
1test030a.idr:12:When elaborating right hand side of testReflect1:
1test030a.idr:12:When elaborating right hand side of testReflect1:
2+Can't unify
3+ IsJust (Just x)
4+with
2−Can't unify IsJust (Just x) with IsJust (prove (getProof x))
5+ IsJust (prove (getProof x))
3
6
4Specifically:
7Specifically:
5− Can't unify Just x with Nothing
8+ Can't unify
9+ Just x
10+ with
11+ Nothing
12+