aed179c · Idris-dev · git.iko.soy

git.iko.soy/Idris-dev

on master help sign in

Track the providence of unification errors

aed179cDavid Raymond Christiansen13 years ago

src/Idris/Core/Elaborate.hs+1

compare with master

unifiedsplit

@@ -687,6 +687,7 @@ try' t1 t2 proofSearch

687 r || proofSearch

688 recoverableErr (CantSolveGoal _ _) = False

689 recoverableErr (ProofSearchFail _) = False

690+ recoverableErr (ElaboratingArg _ _ _ e) = recoverableErr e

690 recoverableErr _ = True

691 recoverableErr _ = True

691

692

692tryWhen :: Bool -> Elab' aux a -> Elab' aux a -> Elab' aux a

693tryWhen :: Bool -> Elab' aux a -> Elab' aux a -> Elab' aux a

src/Idris/Core/TT.hs+4−1

@@ -140,7 +140,7 @@ data Err' t

140 | NoRewriting t

141 | At FC (Err' t)

142 | Elaborating String Name (Err' t)

143− | ElaboratingArg Name Name (Err' t)

143+ | ElaboratingArg FC Name Name (Err' t)

144 | ProviderError String

145 | LoadingFailed String (Err' t)

146 | ReflectionError [[ErrorReportPart]] (Err' t)

@@ -171,6 +171,7 @@ instance Sized Err where

171 size ProgramLineComment = 1

172 size (At fc err) = size fc + size err

173 size (Elaborating _ n err) = size err

174+ size (ElaboratingArg _ _ _ err) = size err

174 size (ProviderError msg) = length msg

175 size (ProviderError msg) = length msg

175 size (LoadingFailed fn e) = 1 + length fn + size e

176 size (LoadingFailed fn e) = 1 + length fn + size e

176 size _ = 1

177 size _ = 1

@@ -195,6 +196,8 @@ instance Show Err where

195 show (LoadingFailed fn e) = "Loading " ++ fn ++ " failed: (TT) " ++ show e

196 show (LoadingFailed fn e) = "Loading " ++ fn ++ " failed: (TT) " ++ show e

196 show ProgramLineComment = "Program line next to comment"

197 show ProgramLineComment = "Program line next to comment"

197 show (At f e) = show f ++ ":" ++ show e

198 show (At f e) = show f ++ ":" ++ show e

199+ show (ElaboratingArg fc f x e) = show fc ++ ": Elaborating " ++ show f ++ " arg " ++

200+ show x ++ ": " ++ show e

198 show _ = "Error"

201 show _ = "Error"

199

202

200instance Pretty Err OutputAnnotation where

203instance Pretty Err OutputAnnotation where

src/Idris/Core/Unify.hs+17−11

@@ -37,6 +37,12 @@ data UResult a = UOK a

37 | UPartOK a

38 | UFail Err

40+-- | Smart constructor for unification errors that takes into account the FailContext

41+cantUnify :: [FailContext] -> Bool -> t -> t -> (Err' t) -> [(Name, t)] -> Int -> Err' t

42+cantUnify [] r t1 t2 e ctxt i = CantUnify r t1 t2 e ctxt i

43+cantUnify (FailContext fc f x : _) r t1 t2 e ctxt i =

44+ ElaboratingArg fc f x (CantUnify r t1 t2 e ctxt i)

45+

40-- Solve metavariables by matching terms against each other

46-- Solve metavariables by matching terms against each other

41-- Not really unification, of course!

47-- Not really unification, of course!

@@ -89,7 +95,7 @@ match_unify ctxt env topx topy inj holes from =

89 | OK True <- convEq' ctxt holes x y = do sc 1; return []

95 | OK True <- convEq' ctxt holes x y = do sc 1; return []

90 | otherwise = do UI s f <- get

96 | otherwise = do UI s f <- get

91 let r = recoverable x y

97 let r = recoverable x y

92− let err = CantUnify r

98+ let err = cantUnify from r

93 topx topy (CantUnify r x y (Msg "") (errEnv env) s) (errEnv env) s

99 topx topy (CantUnify r x y (Msg "") (errEnv env) s) (errEnv env) s

94 if (not r) then lift $ tfail err

100 if (not r) then lift $ tfail err

95 else do put (UI s ((x, y, env, err, from, Match) : f))

101 else do put (UI s ((x, y, env, err, from, Match) : f))

@@ -103,9 +109,9 @@ match_unify ctxt env topx topy inj holes from =

103 uB bnames (Pi tx) (Pi ty) = un bnames tx ty

109 uB bnames (Pi tx) (Pi ty) = un bnames tx ty

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

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

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

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

106− let err = CantUnify r topx topy

112+ let err = cantUnify from r topx topy

107− (CantUnify r (binderTy x) (binderTy y) (Msg "") (errEnv env) s)

113+ (CantUnify r (binderTy x) (binderTy y) (Msg "") (errEnv env) s)

108− (errEnv env) s

114+ (errEnv env) s

109 put (UI s ((binderTy x, binderTy y, env, err, from, Match) : f))

115 put (UI s ((binderTy x, binderTy y, env, err, from, Match) : f))

110 return []

116 return []

111

117

@@ -117,7 +123,7 @@ match_unify ctxt env topx topy inj holes from =

117

123

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

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

119 let r = recoverable x y

125 let r = recoverable x y

120− let err = CantUnify r

126+ let err = cantUnify from r

121 topx topy (CantUnify r x y (Msg "") (errEnv env) s) (errEnv env) s

127 topx topy (CantUnify r x y (Msg "") (errEnv env) s) (errEnv env) s

122 put (UI s ((x, y, env, err, from, Match) : f))

128 put (UI s ((x, y, env, err, from, Match) : f))

123 lift $ tfail err

129 lift $ tfail err

@@ -370,7 +376,7 @@ unify ctxt env topx topy inj holes from =

370 | OK True <- convEq' ctxt holes x y = do sc 1; return []

376 | OK True <- convEq' ctxt holes x y = do sc 1; return []

371 | otherwise = do UI s f <- get

377 | otherwise = do UI s f <- get

372 let r = recoverable x y

378 let r = recoverable x y

373− let err = CantUnify r

379+ let err = cantUnify from r

374 topx topy (CantUnify r x y (Msg "") (errEnv env) s) (errEnv env) s

380 topx topy (CantUnify r x y (Msg "") (errEnv env) s) (errEnv env) s

375 if (not r) then lift $ tfail err

381 if (not r) then lift $ tfail err

376 else do put (UI s ((x, y, env, err, from, Unify) : f))

382 else do put (UI s ((x, y, env, err, from, Unify) : f))

@@ -470,7 +476,7 @@ unify ctxt env topx topy inj holes from =

470 unifyTmpFail x y

476 unifyTmpFail x y

471 = do UI s f <- get

477 = do UI s f <- get

472 let r = recoverable x y

478 let r = recoverable x y

473− let err = CantUnify r

479+ let err = cantUnify from r

474 topx topy (CantUnify r x y (Msg "") (errEnv env) s) (errEnv env) s

480 topx topy (CantUnify r x y (Msg "") (errEnv env) s) (errEnv env) s

475 put (UI s ((topx, topy, env, err, from, Unify) : f))

481 put (UI s ((topx, topy, env, err, from, Unify) : f))

476 return []

482 return []

@@ -478,7 +484,7 @@ unify ctxt env topx topy inj holes from =

478 -- shortcut failure, if we *know* nothing can fix it

484 -- shortcut failure, if we *know* nothing can fix it

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

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

480 let r = recoverable x y

486 let r = recoverable x y

481− let err = CantUnify r

487+ let err = cantUnify from r

482 topx topy (CantUnify r x y (Msg "") (errEnv env) s) (errEnv env) s

488 topx topy (CantUnify r x y (Msg "") (errEnv env) s) (errEnv env) s

483 put (UI s ((topx, topy, env, err, from, Unify) : f))

489 put (UI s ((topx, topy, env, err, from, Unify) : f))

484 lift $ tfail err

490 lift $ tfail err

@@ -500,9 +506,9 @@ unify ctxt env topx topy inj holes from =

500 uB bnames (PVar tx) (PVar ty) = un' False bnames tx ty

506 uB bnames (PVar tx) (PVar ty) = un' False bnames tx ty

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

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

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

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

503− let err = CantUnify r topx topy

509+ let err = cantUnify from r topx topy

504− (CantUnify r (binderTy x) (binderTy y) (Msg "") (errEnv env) s)

510+ (CantUnify r (binderTy x) (binderTy y) (Msg "") (errEnv env) s)

505− (errEnv env) s

511+ (errEnv env) s

506 put (UI s ((binderTy x, binderTy y, env, err, from, Unify) : f))

512 put (UI s ((binderTy x, binderTy y, env, err, from, Unify) : f))

507 return [] -- lift $ tfail err

513 return [] -- lift $ tfail err

508

514

src/Idris/Delaborate.hs+19−2

@@ -1,5 +1,4 @@

1{-# LANGUAGE PatternGuards #-}

2−

3module Idris.Delaborate (bugaddr, delab, delab', delabMV, delabTy, delabTy', pshow, pprintErr) where

2module Idris.Delaborate (bugaddr, delab, delab', delabMV, delabTy, delabTy', pshow, pprintErr) where

5-- Convert core TT back into high level syntax, primarily for display

4-- Convert core TT back into high level syntax, primarily for display

@@ -13,6 +12,7 @@ import Idris.Core.Evaluate

13import Idris.ErrReverse

12import Idris.ErrReverse

15import Data.List (intersperse)

14import Data.List (intersperse)

15+import qualified Data.Text as T

17import Debug.Trace

@@ -200,7 +200,7 @@ pprintErr' i (NotInjective p x y) =

200 pprintTerm i (delab i y)

201pprintErr' i (CantResolve c) = text "Can't resolve type class" <+> pprintTerm i (delab i c)

202pprintErr' i (CantResolveAlts as) = text "Can't disambiguate name:" <+>

203− cat (punctuate (comma <> space) (map text as))

203+ align (cat (punctuate (comma <> space) (map text as)))

204pprintErr' i (NoTypeDecl n) = text "No type declaration for" <+> annName n

205pprintErr' i (NoSuchVariable n) = text "No such variable" <+> annName n

206pprintErr' i (IncompleteTerm t) = text "Incomplete term" <+> pprintTerm i (delab i t)

@@ -217,6 +217,17 @@ pprintErr' i (At f e) = annotate (AnnFC f) (text (show f)) <> colon <> pprintErr

217pprintErr' i (Elaborating s n e) = text "When elaborating" <+> text s <>

218 annName' n (showqual i n) <> colon <$>

219 pprintErr' i e

220+pprintErr' i (ElaboratingArg fc f x e)

221+ | isUN x =

222+ annotate (AnnFC fc) (text (show fc)) <> colon <+>

223+ text "When elaborating argument" <+>

224+ annotate (AnnBoundName x False) (text (showbasic x)) <+> --TODO check plicity

225+ text "to function" <+> annName f <> colon <>

226+ indented (pprintErr' i e)

227+ | otherwise =

228+ annotate (AnnFC fc) (text (show fc)) <> colon <+>

229+ text "When elaborating an application of function" <+>

230+ annName f <> colon <> indented (pprintErr' i e)

220pprintErr' i (ProviderError msg) = text ("Type provider error: " ++ msg)

231pprintErr' i (ProviderError msg) = text ("Type provider error: " ++ msg)

221pprintErr' i (LoadingFailed fn e) = text "Loading" <+> text fn <+> text "failed:" <+> pprintErr' i e

232pprintErr' i (LoadingFailed fn e) = text "Loading" <+> text fn <+> text "failed:" <+> pprintErr' i e

222pprintErr' i (ReflectionError parts orig) =

233pprintErr' i (ReflectionError parts orig) =

@@ -235,6 +246,11 @@ pprintErr' i (ReflectionFailed msg err) =

235 indented (pprintErr' i err) <>

246 indented (pprintErr' i err) <>

236 text ("This is probably a bug. Please consider reporting it at " ++ bugaddr)

247 text ("This is probably a bug. Please consider reporting it at " ++ bugaddr)

237

248

249+isUN :: Name -> Bool

250+isUN (UN n) = not $ T.isPrefixOf (T.pack "__") n -- TODO figure out why MNs are getting rewritte to UNs for top-level pattern-matching functions

251+isUN (NS n _) = isUN n

252+isUN _ = False

253+

238annName :: Name -> Doc OutputAnnotation

254annName :: Name -> Doc OutputAnnotation

239annName n = annName' n (showbasic n)

255annName n = annName' n (showbasic n)

240

256

@@ -259,6 +275,7 @@ showqual i n = showName (Just i) [] False False (dens n)

259 _ -> ns

275 _ -> ns

260 dens n = n

276 dens n = n

261

277

278+showbasic :: Name -> String

262showbasic n@(UN _) = show n

279showbasic n@(UN _) = show n

263showbasic (MN _ s) = str s

280showbasic (MN _ s) = str s

264showbasic (NS n s) = showSep "." (map str (reverse s)) ++ "." ++ showbasic n

281showbasic (NS n s) = showSep "." (map str (reverse s)) ++ "." ++ showbasic n

src/Idris/ElabDecls.hs+1−1

@@ -693,7 +693,6 @@ elabProvider info syn fc what n ty tm

693 , prov == txt "Provider" && provs == txt "Providers" = True

694 isProviderOf _ _ = False

695

696−-- | Elaborate a type provider

697elabTransform :: ElabInfo -> FC -> Bool -> PTerm -> PTerm -> Idris ()

696elabTransform :: ElabInfo -> FC -> Bool -> PTerm -> PTerm -> Idris ()

698elabTransform info fc safe lhs_in rhs_in

697elabTransform info fc safe lhs_in rhs_in

699 = do ctxt <- getContext

698 = do ctxt <- getContext

@@ -1280,6 +1279,7 @@ checkPossible info fc tcgen fname lhs_in

1280 impossibleError (CantConvert _ _ _) = False

1279 impossibleError (CantConvert _ _ _) = False

1281 impossibleError (At _ e) = impossibleError e

1280 impossibleError (At _ e) = impossibleError e

1282 impossibleError (Elaborating _ _ e) = impossibleError e

1281 impossibleError (Elaborating _ _ e) = impossibleError e

1282+ impossibleError (ElaboratingArg _ _ _ e) = impossibleError e

1283 impossibleError _ = True

1284

1285 sameFam topx topy

src/Idris/ElabTerm.hs+5−2

@@ -189,6 +189,7 @@ elab ist info pattern opts fn tm

189 | (P _ (UN ht) _, _) <- unApply t,

190 ht == txt "Lazy" = True

191 forceErr (Elaborating _ _ t) = forceErr t

192+ forceErr (ElaboratingArg _ _ _ t) = forceErr t

192 forceErr (At _ t) = forceErr t

193 forceErr (At _ t) = forceErr t

193 forceErr t = False

194 forceErr t = False

194

195

@@ -802,6 +803,7 @@ pruneAlt xs = map prune xs

802 case fs of

803 case fs of

803 [a] -> a

804 [a] -> a

804 _ -> PAlternative a as'

805 _ -> PAlternative a as'

806+

805 choose f (PApp fc f' as) = PApp fc (choose f f') (fmap (fmap (choose f)) as)

807 choose f (PApp fc f' as) = PApp fc (choose f f') (fmap (fmap (choose f)) as)

806 choose f t = t

808 choose f t = t

807

809

@@ -1113,9 +1115,9 @@ runTac autoSolve ist fn tac

1113 runReflected tactic

1115 runReflected tactic

1114 where tacticTy = Var (reflm "Tactic")

1116 where tacticTy = Var (reflm "Tactic")

1115 listTy = Var (sNS (sUN "List") ["List", "Prelude"])

1117 listTy = Var (sNS (sUN "List") ["List", "Prelude"])

1116− scriptTy = (RBind (sUN "__pi_arg")

1118+ scriptTy = (RBind (sMN 0 "__pi_arg")

1117 (Pi (RApp listTy envTupleType))

1119 (Pi (RApp listTy envTupleType))

1118− (RBind (sUN "__pi_arg1")

1120+ (RBind (sMN 1 "__pi_arg")

1119 (Pi (Var $ reflm "TT")) tacticTy))

1121 (Pi (Var $ reflm "TT")) tacticTy))

1120 runT (ByReflection tm) -- run the reflection function 'tm' on the

1122 runT (ByReflection tm) -- run the reflection function 'tm' on the

1121 -- goal, then apply the resulting reflected Tactic

1123 -- goal, then apply the resulting reflected Tactic

@@ -1641,6 +1643,7 @@ withErrorReflection x = idrisCatch x (\ e -> handle e >>= ierror)

1641 handle e@(Elaborating what n err) = do logLvl 3 "Reflecting body of Elaborating"

1643 handle e@(Elaborating what n err) = do logLvl 3 "Reflecting body of Elaborating"

1642 err' <- handle err

1644 err' <- handle err

1643 return (Elaborating what n err')

1645 return (Elaborating what n err')

1646+ -- TODO: argument-specific error handlers go here for ElaboratingArg

1644 handle e = do ist <- getIState

1647 handle e = do ist <- getIState

1645 let err = fmap (errReverse ist) e

1648 let err = fmap (errReverse ist) e

1646 logLvl 2 "Starting error reflection"

1649 logLvl 2 "Starting error reflection"

src/Idris/Error.hs+3

@@ -57,6 +57,8 @@ ierror = throwError

57tclift :: TC a -> Idris a

58tclift (OK v) = return v

59tclift (Error err@(At fc e)) = do setErrSpan fc; throwError err

60+tclift (Error err@(ElaboratingArg fc _ _ e)) = do setErrSpan fc

61+ throwError err

60tclift (Error err) = throwError err

62tclift (Error err) = throwError err

62tctry :: TC a -> TC a -> Idris a

64tctry :: TC a -> TC a -> Idris a

@@ -67,4 +69,5 @@ tctry tc1 tc2

68getErrSpan :: Err -> FC

70getErrSpan :: Err -> FC

69getErrSpan (At fc _) = fc

71getErrSpan (At fc _) = fc

72+getErrSpan (ElaboratingArg fc _ _ e) = fc

70getErrSpan _ = emptyFC

73getErrSpan _ = emptyFC

src/Idris/ParseOps.hs+1−1

@@ -39,7 +39,7 @@ table fixes

39 [[backtick],

40 [binary "$" (\fc x y -> PApp fc x [pexp y]) AssocRight],

41 [binary "=" PEq AssocLeft],

42− [binary "->" (\fc x y -> PPi expl (sUN "__pi_arg") x y) AssocRight]]

42+ [binary "->" (\fc x y -> PPi expl (sMN 0 "__pi_arg") x y) AssocRight]]

44-- | Calculates table for fixtiy declarations

45toTable :: [FixDecl] -> OperatorTable IdrisParser PTerm