git.iko.soy/Idris-dev
on master help sign in
Better tracking of FC in implicit coercions / DSL

Now, implicit coercion-related type errors give their source location when its available from a subterm. Also, index_first variables in DSL blocks give the source location of their use site rather than the DSL's definition site.

commit3c187ce04be5446212034dc763851f53cfb84667 authorDavid Raymond Christiansen <david@davidchristiansen.dk> dateSun 18 Jan 2015, 02:52 (12 years ago) parent43ba516
3 files changed+66−2
compare with master
unifiedsplit
src/Idris/AbsSyntaxTree.hs+59 src/Idris/DSL.hs+6−1 src/Idris/ElabTerm.hs+1−1
src/Idris/AbsSyntaxTree.hs+59
@@ -18,6 +18,8 @@ import Idris.Colours
1818import System.Console.Haskeline
1919import System.IO
2020
21+import Control.Applicative ((<|>))
22+
2123import Control.Monad.Trans.State.Strict
2224import Control.Monad.Trans.Except
2325import qualified Control.Monad.Trans.Class as Trans (lift)
@@ -945,6 +947,63 @@ ptacimp n s t = PTacImplicit 2 [] n s t
945947
946948type PArg = PArg' PTerm
947949
950+-- | Get the highest FC in a term, if one exists
951+highestFC :: PTerm -> Maybe FC
952+highestFC (PQuote _) = Nothing
953+highestFC (PRef fc _) = Just fc
954+highestFC (PInferRef fc _) = Just fc
955+highestFC (PPatvar fc _) = Just fc
956+highestFC (PLam fc _ _ _) = Just fc
957+highestFC (PPi _ _ _ _) = Nothing
958+highestFC (PLet fc _ _ _ _) = Just fc
959+highestFC (PTyped tm ty) = highestFC tm <|> highestFC ty
960+highestFC (PApp fc _ _) = Just fc
961+highestFC (PAppBind fc _ _) = Just fc
962+highestFC (PMatchApp fc _) = Just fc
963+highestFC (PCase fc _ _) = Just fc
964+highestFC (PTrue fc _) = Just fc
965+highestFC (PRefl fc _) = Just fc
966+highestFC (PResolveTC fc) = Just fc
967+highestFC (PEq fc _ _ _ _) = Just fc
968+highestFC (PRewrite fc _ _ _) = Just fc
969+highestFC (PPair fc _ _ _) = Just fc
970+highestFC (PDPair fc _ _ _ _) = Just fc
971+highestFC (PAs fc _ _) = Just fc
972+highestFC (PAlternative _ args) =
973+ case mapMaybe highestFC args of
974+ [] -> Nothing
975+ (fc:_) -> Just fc
976+highestFC (PHidden _) = Nothing
977+highestFC PType = Nothing
978+highestFC (PUniverse _) = Nothing
979+highestFC (PGoal fc _ _ _) = Just fc
980+highestFC (PConstant _) = Nothing
981+highestFC Placeholder = Nothing
982+highestFC (PDoBlock lines) =
983+ case map getDoFC lines of
984+ [] -> Nothing
985+ (fc:_) -> Just fc
986+ where
987+ getDoFC (DoExp fc t) = fc
988+ getDoFC (DoBind fc nm t) = fc
989+ getDoFC (DoBindP fc l r alts) = fc
990+ getDoFC (DoLet fc nm l r) = fc
991+ getDoFC (DoLetP fc l r) = fc
992+
993+highestFC (PIdiom fc _) = Just fc
994+highestFC (PReturn fc) = Just fc
995+highestFC (PMetavar _) = Nothing
996+highestFC (PProof _) = Nothing
997+highestFC (PTactics _) = Nothing
998+highestFC (PElabError _) = Nothing
999+highestFC PImpossible = Nothing
1000+highestFC (PCoerced tm) = highestFC tm
1001+highestFC (PDisamb _ opts) = highestFC opts
1002+highestFC (PUnifyLog tm) = highestFC tm
1003+highestFC (PNoImplicits tm) = highestFC tm
1004+highestFC (PQuasiquote _ _) = Nothing
1005+highestFC (PUnquote tm) = highestFC tm
1006+
9481007-- Type class data
9491008
9501009data ClassInfo = CI { instanceName :: Name,
src/Idris/DSL.hs+6−1
@@ -78,6 +78,7 @@ expandDo dsl (PDoBlock ds)
7878expandDo dsl (PIdiom fc e) = expandDo dsl $ unIdiom (dsl_apply dsl) (dsl_pure dsl) fc e
7979expandDo dsl t = t
8080
81+-- | Replace DSL-bound variable in a term
8182var :: DSL -> Name -> PTerm -> Int -> PTerm
8283var dsl n t i = v' i t where
8384 v' i (PRef fc x) | x == n =
@@ -111,11 +112,15 @@ var dsl n t i = v' i t where
111112
112113 mkVar fc 0 = case index_first dsl of
113114 Nothing -> PElabError (Msg "No index_first defined")
114− Just f -> f
115+ Just f -> setFC fc f
115116 mkVar fc n = case index_next dsl of
116117 Nothing -> PElabError (Msg "No index_next defined")
117118 Just f -> PApp fc f [pexp (mkVar fc (n-1))]
118119
120+ setFC fc (PRef _ n) = PRef fc n
121+ setFC fc (PApp _ f xs) = PApp fc (setFC fc f) (map (fmap (setFC fc)) xs)
122+ setFC fc t = t
123+
119124unIdiom :: PTerm -> PTerm -> FC -> PTerm -> PTerm
120125unIdiom ap pure fc e@(PApp _ _ _) = let f = getFn e in
121126 mkap (getFn e)
src/Idris/ElabTerm.hs+1−1
@@ -1096,7 +1096,7 @@ elab ist info emode opts fn tm
10961096 PAlternative True (map (mkCoerce env t) cs)]
10971097 return t'
10981098 where
1099− mkCoerce env t n = let fc = fileFC "Coercion" in -- line never appears!
1099+ mkCoerce env t n = let fc = maybe (fileFC "Coercion") id (highestFC t) in
11001100 addImplBound ist (map fst env)
11011101 (PApp fc (PRef fc n) [pexp (PCoerced t)])
11021102