fab7083 · Idris-dev · git.iko.soy

git.iko.soy/Idris-dev

Decorate type provider errors with source location

commitfab7083f913d17521fc1a61b1f076714e8b19585 authorDavid Raymond Christiansen <david@davidchristiansen.dk> dateMon 3 Feb 2014, 10:46 (13 years ago) parentadadee1

2 files changed+14−14

compare with master

unifiedsplit

src/Idris/ElabDecls.hs+1−1 src/Idris/Providers.hs+13−13

src/Idris/ElabDecls.hs+1−1

@@ -646,7 +646,7 @@ elabProvider info syn fc n ty tm

646646 logLvl 1 $ "Normalised " ++ show n ++ "'s RHS to " ++ show rhs

647647

648648 -- Extract the provided term from the type provider

649− tm <- getProvided rhs'

649+ tm <- getProvided fc rhs'

650650

651651 -- Finally add a top-level definition of the provided term

652652 elabClauses info fc [] n [PClause fc n (PRef fc n) [] (delab i tm) []]

src/Idris/Providers.hs+13−13

@@ -18,17 +18,17 @@ ermod = sNS (sUN "Error") ["Providers"]

1818prmod = sNS (sUN "Provide") ["Providers"]

1919

2020-- | Handle an error, if the type provider returned an error. Otherwise return the provided term.

21−getProvided :: TT Name -> Idris (TT Name)

22−getProvided tm | (P _ pioret _, [tp, result]) <- unApply tm

23− , (P _ nm _, [_, err]) <- unApply result

24− , pioret == ioret && nm == ermod

25− = case err of

26− Constant (Str msg) -> ierror . ProviderError $ msg

27− _ -> ifail "Internal error in type provider, non-normalised error"

28− | (P _ pioret _, [tp, result]) <- unApply tm

29− , (P _ nm _, [_, res]) <- unApply result

30− , pioret == ioret && nm == prmod

31− = return res

32− | otherwise = ifail $ "Internal type provider error: result was not " ++

33− "IO (Provider a), or perhaps missing normalisation."

21+getProvided :: FC -> TT Name -> Idris (TT Name)

22+getProvided fc tm | (P _ pioret _, [tp, result]) <- unApply tm

23+ , (P _ nm _, [_, err]) <- unApply result

24+ , pioret == ioret && nm == ermod

25+ = case err of

26+ Constant (Str msg) -> ierror . At fc . ProviderError $ msg

27+ _ -> ifail "Internal error in type provider, non-normalised error"

28+ | (P _ pioret _, [tp, result]) <- unApply tm

29+ , (P _ nm _, [_, res]) <- unApply result

30+ , pioret == ioret && nm == prmod

31+ = return res

32+ | otherwise = ifail $ "Internal type provider error: result was not " ++

33+ "IO (Provider a), or perhaps missing normalisation."

3434