bcd2db1 · Idris-dev · git.iko.soy

libs/base/Language/Reflection/Errors.idr+1

compare with master

unifiedsplit

@@ -19,6 +19,7 @@ data Err = Msg String

19 | TooManyArguments TTName

20 | CantIntroduce TT

21 | NoSuchVariable TTName

22+ | WithFnType TT

22 | NoTypeDecl TTName

23 | NoTypeDecl TTName

23 | NotInjective TT TT TT

24 | NotInjective TT TT TT

24 | CantResolve TT

25 | CantResolve TT

libs/base/Language/Reflection/Utils.idr+1

@@ -261,6 +261,7 @@ instance Show Err where

261 show (TooManyArguments n) = "TooManyArguments " ++ show n

262 show (CantIntroduce tm) = "CantIntroduce " ++ show tm

263 show (NoSuchVariable n) = "NoSuchVariable " ++ show n

264+ show (WithFnType tm) = "WithFnType " ++ show tm

264 show (NoTypeDecl n) = "NoTypeDecl " ++ show n

265 show (NoTypeDecl n) = "NoTypeDecl " ++ show n

265 show (NotInjective tm tm' x) = "NotInjective " ++ show tm ++ " " ++ show tm'

266 show (NotInjective tm tm' x) = "NotInjective " ++ show tm ++ " " ++ show tm'

266 show (CantResolve tm) = "CantResolve " ++ show tm

267 show (CantResolve tm) = "CantResolve " ++ show tm

src/Idris/Core/Binary.hs+3

@@ -118,6 +118,8 @@ instance Binary a => Binary (Err' a) where

118 put (ReflectionFailed str e) = do putWord8 33

119 put str

120 put e

121+ put (WithFnType t) = do putWord8 34

122+ put t

121

123

122 get = do i <- getWord8

124 get = do i <- getWord8

123 case i of

125 case i of

@@ -171,6 +173,7 @@ instance Binary a => Binary (Err' a) where

171 return $ ReflectionError x y

173 return $ ReflectionError x y

172 33 -> do x <- get ; y <- get

174 33 -> do x <- get ; y <- get

173 return $ ReflectionFailed x y

175 return $ ReflectionFailed x y

176+ 34 -> fmap WithFnType get

174 _ -> error "Corrupted binary data for Err'"

177 _ -> error "Corrupted binary data for Err'"

175----- Generated by 'derive'

178----- Generated by 'derive'

176

179

src/Idris/Core/TT.hs+3

@@ -136,6 +136,7 @@ data Err' t

136 | TooManyArguments Name

137 | CantIntroduce t

138 | NoSuchVariable Name

139+ | WithFnType t

139 | NoTypeDecl Name

140 | NoTypeDecl Name

140 | NotInjective t t t

141 | NotInjective t t t

141 | CantResolve t

142 | CantResolve t

@@ -1119,6 +1120,8 @@ bindTyArgs b xs = bindAll (map (\ (n, ty) -> (n, b ty)) xs)

1119-- | Return a list of pairs of the names of the outermost 'Pi'-bound

1120-- | Return a list of pairs of the names of the outermost 'Pi'-bound

1120-- variables in the given term, together with their types.

1121-- variables in the given term, together with their types.

1121getArgTys :: TT n -> [(n, TT n)]

1122getArgTys :: TT n -> [(n, TT n)]

1123+getArgTys (Bind n (PVar _) sc) = getArgTys sc

1124+getArgTys (Bind n (PVTy _) sc) = getArgTys sc

1122getArgTys (Bind n (Pi t _) sc) = (n, t) : getArgTys sc

1125getArgTys (Bind n (Pi t _) sc) = (n, t) : getArgTys sc

1123getArgTys _ = []

1126getArgTys _ = []

1124

1127

src/Idris/Delaborate.hs+2

@@ -260,6 +260,8 @@ pprintErr' i (CantResolveAlts as) = text "Can't disambiguate name:" <+>

260 align (cat (punctuate (comma <> space) (map (fmap (fancifyAnnots i) . annName) as)))

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

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

263+pprintErr' i (WithFnType ty) =

264+ text "Can't match on a function: type is" <+> annTm ty (pprintTerm i (delab i ty))

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

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

264pprintErr' i UniverseError = text "Universe inconsistency"

266pprintErr' i UniverseError = text "Universe inconsistency"

265pprintErr' i (UniqueError NullType n)

267pprintErr' i (UniqueError NullType n)

src/Idris/Elab/Clause.hs+7

@@ -828,6 +828,13 @@ elabClause info opts (_, PWith fc fname lhs_in withs wval_in withblock)

828 let cwvaltyN = explicitNames (normalise ctxt [] cwvalty)

829 let cwvalN = explicitNames (normalise ctxt [] cwval)

830 logLvl 3 ("With type " ++ show cwvalty ++ "\nRet type " ++ show ret_ty)

831+ -- We're going to assume the with type is not a function shortly,

832+ -- so report an error if it is (you can't match on a function anyway

833+ -- so this doesn't lose anything)

834+ case getArgTys cwvaltyN of

835+ [] -> return ()

836+ (_:_) -> ierror $ At fc (WithFnType cwvalty)

837+

831 let pvars = map fst (getPBtys cwvalty)

838 let pvars = map fst (getPBtys cwvalty)

832 -- we need the unelaborated term to get the names it depends on

839 -- we need the unelaborated term to get the names it depends on

833 -- rather than a de Bruijn index.

840 -- rather than a de Bruijn index.

src/Idris/ElabTerm.hs+1

@@ -2118,6 +2118,7 @@ reflectErr (NotEquality t t') =

2118reflectErr (TooManyArguments n) = raw_apply (Var $ reflErrName "TooManyArguments") [reflectName n]

2119reflectErr (CantIntroduce t) = raw_apply (Var $ reflErrName "CantIntroduce") [reflect t]

2120reflectErr (NoSuchVariable n) = raw_apply (Var $ reflErrName "NoSuchVariable") [reflectName n]

2121+reflectErr (WithFnType t) = raw_apply (Var $ reflErrName "WithFnType") [reflect t]

2121reflectErr (NoTypeDecl n) = raw_apply (Var $ reflErrName "NoTypeDecl") [reflectName n]

2122reflectErr (NoTypeDecl n) = raw_apply (Var $ reflErrName "NoTypeDecl") [reflectName n]

2122reflectErr (NotInjective t1 t2 t3) =

2123reflectErr (NotInjective t1 t2 t3) =

2123 raw_apply (Var $ reflErrName "NotInjective")

2124 raw_apply (Var $ reflErrName "NotInjective")