bcd2db1 · Idris-dev · git.iko.soy

git.iko.soy/Idris-dev

Check target of 'with' is a value (not a function)

commitbcd2db1b8189ed1503b777b7b4ca58fddcc1588d authorEdwin Brady <ecb10@st-andrews.ac.uk> dateThu 4 Dec 2014, 21:51 (12 years ago) parentec17e6a

7 files changed+18

compare with master

unifiedsplit

libs/base/Language/Reflection/Errors.idr+1 libs/base/Language/Reflection/Utils.idr+1 src/Idris/Core/Binary.hs+3 src/Idris/Core/TT.hs+3 src/Idris/Delaborate.hs+2 src/Idris/Elab/Clause.hs+7 src/Idris/ElabTerm.hs+1

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

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

1919 | TooManyArguments TTName

2020 | CantIntroduce TT

2121 | NoSuchVariable TTName

22+ | WithFnType TT

2223 | NoTypeDecl TTName

2324 | NotInjective TT TT TT

2425 | CantResolve TT

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

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

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

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

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

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

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

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

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

src/Idris/Core/Binary.hs+3

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

118118 put (ReflectionFailed str e) = do putWord8 33

119119 put str

120120 put e

121+ put (WithFnType t) = do putWord8 34

122+ put t

121123

122124 get = do i <- getWord8

123125 case i of

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

171173 return $ ReflectionError x y

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

173175 return $ ReflectionFailed x y

176+ 34 -> fmap WithFnType get

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

175178----- Generated by 'derive'

176179

src/Idris/Core/TT.hs+3

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

136136 | TooManyArguments Name

137137 | CantIntroduce t

138138 | NoSuchVariable Name

139+ | WithFnType t

139140 | NoTypeDecl Name

140141 | NotInjective t t t

141142 | CantResolve t

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

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

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

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

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

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

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

11231126getArgTys _ = []

11241127

src/Idris/Delaborate.hs+2

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

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

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

262262pprintErr' 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))

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

264266pprintErr' i UniverseError = text "Universe inconsistency"

265267pprintErr' 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)

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

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

830830 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+

831838 let pvars = map fst (getPBtys cwvalty)

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

833840 -- rather than a de Bruijn index.

src/Idris/ElabTerm.hs+1

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

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

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

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

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

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

21222123reflectErr (NotInjective t1 t2 t3) =

21232124 raw_apply (Var $ reflErrName "NotInjective")