b5e97e4 · Idris-dev · git.iko.soy

git.iko.soy/Idris-dev

Show error contexts with pretty-printer

commitb5e97e42cfde8c6744825afb5e22cc4c1872905f authorDavid Raymond Christiansen <david@davidchristiansen.dk> dateSat 8 Feb 2014, 10:34 (13 years ago) parentf7b466d

2 files changed+21−15

compare with master

unifiedsplit

src/Idris/Core/Unify.hs+7−7 src/Idris/Delaborate.hs+14−8

src/Idris/Core/Unify.hs+7−7

@@ -76,7 +76,7 @@ match_unify ctxt env topx topy dont holes =

7676 | otherwise = do UI s f <- get

7777 let r = recoverable x y

7878 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

8080 if (not r) then lift $ tfail err

8181 else do put (UI s ((x, y, env, err) : f))

8282 lift $ tfail err

@@ -90,7 +90,7 @@ match_unify ctxt env topx topy dont holes =

9090 uB bnames x y = do UI s f <- get

9191 let r = recoverable (binderTy x) (binderTy y)

9292 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)

9494 (errEnv env) s

9595 put (UI s ((binderTy x, binderTy y, env, err) : f))

9696 return []

@@ -104,7 +104,7 @@ match_unify ctxt env topx topy dont holes =

104104 unifyFail x y = do UI s f <- get

105105 let r = recoverable x y

106106 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

108108 put (UI s ((x, y, env, err) : f))

109109 lift $ tfail err

110110 combine bnames as [] = return as

@@ -309,7 +309,7 @@ unify ctxt env topx topy dont holes =

309309 | otherwise = do UI s f <- get

310310 let r = recoverable x y

311311 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

313313 if (not r) then lift $ tfail err

314314 else do put (UI s ((x, y, env, err) : f))

315315 return [] -- lift $ tfail err

@@ -436,7 +436,7 @@ unify ctxt env topx topy dont holes =

436436 = do UI s f <- get

437437 let r = recoverable x y

438438 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

440440 put (UI s ((topx, topy, env, err) : f))

441441 return []

442442

@@ -444,7 +444,7 @@ unify ctxt env topx topy dont holes =

444444 unifyFail x y = do UI s f <- get

445445 let r = recoverable x y

446446 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

448448 put (UI s ((topx, topy, env, err) : f))

449449 lift $ tfail err

450450

@@ -466,7 +466,7 @@ unify ctxt env topx topy dont holes =

466466 uB bnames x y = do UI s f <- get

467467 let r = recoverable (binderTy x) (binderTy y)

468468 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)

470470 (errEnv env) s

471471 put (UI s ((binderTy x, binderTy y, env, err) : f))

472472 return [] -- lift $ tfail err

src/Idris/Delaborate.hs+14−8

@@ -153,22 +153,22 @@ pprintErr' i (CantUnify _ x y e sc s) =

153153 Msg "" -> empty

154154 _ -> line <> line <> text "Specifically:" <>

155155 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

157157pprintErr' i (CantConvert x y env) =

158158 text "Can't convert" <>

159159 indented (pprintTerm' i (map (\ (n, b) -> (n, False)) env) (delab i x)) <$>

160160 text "with" <>

161161 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

163163pprintErr' i (CantSolveGoal x env) =

164164 text "Can't solve goal " <>

165165 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

167167pprintErr' i (UnifyScope n out tm env) =

168168 text "Can't unify" <> indented (annName n) <+>

169169 text "with" <> indented (pprintTerm' i (map (\ (n, b) -> (n, False)) env) (delab i tm)) <+>

170170 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

172172pprintErr' i (CantInferType t) = text "Can't infer type for" <+> text t

173173pprintErr' i (NonFunctionType f ty) =

174174 pprintTerm i (delab i f) <+>

@@ -185,7 +185,7 @@ pprintErr' i (InfiniteUnify x tm env) =

185185 text "Unifying" <+> annName' x (showbasic x) <+> text "and" <+>

186186 pprintTerm' i (map (\ (n, b) -> (n, False)) env) (delab i tm) <+>

187187 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

189189pprintErr' i (NotInjective p x y) =

190190 text "Can't verify injectivity of" <+> pprintTerm i (delab i p) <+>

191191 text " when unifying" <+> pprintTerm i (delab i x) <+> text "and" <+>

@@ -233,9 +233,15 @@ annName n = annName' n (show n)

233233annName' :: Name -> String -> Doc OutputAnnotation

234234annName' n str = annotate (AnnName n Nothing Nothing) (text str)

235235

236−showSc i [] = ""

237−showSc i xs = "\n\nIn context:\n" ++ showSep "\n" (map showVar (reverse xs))

238− where showVar (x, y) = "\t" ++ showbasic x ++ " : " ++ show (delab i y)

236+showSc :: IState -> [(Name, Term)] -> Doc OutputAnnotation

237+showSc i [] = empty

238+showSc i xs = line <> line <> text "In context:" <>

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+

239245

240246showqual :: IState -> Name -> String

241247showqual i n = showName (Just i) [] False False (dens n)