git.iko.soy/Idris-dev
on master help sign in
Merge pull request #483 from yfyf/indent_errors

Indent terms printed in typechecking errors

commit7e1005a706201ee857a6eab90a5ff2fb841f2e0c authorEdwin Brady <edwin.brady@gmail.com> dateSat 14 Sep 2013, 15:01 (13 years ago) parent5203e1bccee056
4 files changed+43−15
compare with master
unifiedsplit
src/Idris/Delaborate.hs+16−9 test/reg010/expected+9−2 test/test020/expected+9−2 test/test030/expected+9−2
src/Idris/Delaborate.hs+16−9
@@ -93,6 +93,12 @@ delabTy' ist imps tm fullname = de [] imps tm
9393 imp (PConstraint p l _ d) arg = PConstraint p l arg d
9494 imp (PTacImplicit p l n sc _ d) arg = PTacImplicit p l n sc arg d
9595
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+
96102pshow :: IState -> Err -> String
97103pshow i (Msg s) = s
98104pshow i (InternalMsg s) = "INTERNAL ERROR: " ++ show s ++
@@ -101,25 +107,26 @@ pshow i (InternalMsg s) = "INTERNAL ERROR: " ++ show s ++
101107pshow i (CantUnify _ x y e sc s)
102108 = let imps = opt_showimp (idris_options i) in
103109 let colour = idris_colourRepl i in
104− "Can't unify " ++ showImp (Just i) imps colour (delab i x)
105− ++ " with " ++ showImp (Just i) imps colour (delab i y) ++
110+ "Can't unify" ++ indented (showImp (Just i) imps colour (delab i x))
111+ ++ "with" ++ indented (showImp (Just i) imps colour (delab i y)) ++
106112-- " (" ++ show x ++ " and " ++ show y ++ ") " ++
107113 case e of
108114 Msg "" -> ""
109− _ -> "\n\nSpecifically:\n\t" ++ pshow i e ++
110− if (opt_errContext (idris_options i)) then showSc i sc else ""
115+ _ -> "\nSpecifically:" ++
116+ indented (pshow i e) ++
117+ if (opt_errContext (idris_options i)) then showSc i sc else ""
111118pshow i (CantConvert x y env)
112119 = let imps = opt_showimp (idris_options i) in
113120 let colour = idris_colourRepl i in
114− "Can't convert " ++ showImp (Just i) imps colour (delab i x) ++ " with "
115− ++ showImp (Just i) imps colour (delab i y) ++
121+ "Can't convert" ++ indented (showImp (Just i) imps colour (delab i x)) ++ "with"
122+ ++ indented (showImp (Just i) imps colour (delab i y)) ++
116123 if (opt_errContext (idris_options i)) then showSc i env else ""
117124pshow i (UnifyScope n out tm env)
118125 = let imps = opt_showimp (idris_options i) in
119126 let colour = idris_colourRepl i in
120− "Can't unify " ++ show n ++ " with "
121− ++ showImp (Just i) imps colour (delab i tm) ++ " as " ++ show out ++
122− " is not in scope" ++
127+ "Can't unify" ++ indented (show n) ++ "with"
128+ ++ indented (showImp (Just i) imps colour (delab i tm)) ++ "as" ++
129+ indented (show out) ++ "is not in scope" ++
123130 if (opt_errContext (idris_options i)) then showSc i env else ""
124131pshow i (CantInferType t)
125132 = "Can't infer type for " ++ t
test/reg010/expected+9−2
@@ -1,5 +1,12 @@
11reg010.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
36
47Specifically:
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 @@
11When 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
36
47Specifically:
5− Can't unify Vect n a with List a
8+ Can't unify
9+ Vect n a
10+ with
11+ List a
12+
613[3, 2, 1]
714Number 42
test/test030/expected+9−2
@@ -1,5 +1,12 @@
11test030a.idr:12:When elaborating right hand side of testReflect1:
2−Can't unify IsJust (Just x) with IsJust (prove (getProof x))
2+Can't unify
3+ IsJust (Just x)
4+with
5+ IsJust (prove (getProof x))
36
47Specifically:
5− Can't unify Just x with Nothing
8+ Can't unify
9+ Just x
10+ with
11+ Nothing
12+