e086ccf · Idris-dev · git.iko.soy

git.iko.soy/Idris-dev

on master help sign in

Check arguments being matched on are matchable

e086ccfEdwin Brady12 years ago

idris.cabal+3

compare with master

unifiedsplit

@@ -273,6 +273,9 @@ Extra-source-files:

273 test/reg053/run

274 test/reg053/*.idr

275 test/reg053/expected

276+ test/reg054/run

277+ test/reg054/*.idr

278+ test/reg054/expected

276

279

277 test/basic001/run

280 test/basic001/run

278 test/basic001/*.idr

281 test/basic001/*.idr

src/Idris/ElabTerm.hs+49−10

@@ -138,12 +138,37 @@ buildTC ist info emode opts fn tm

138 else return (tm, ds, is)

139 where pattern = emode == ELHS

140

141+-- return whether arguments of the given constructor name can be

142+-- matched on. If they're polymorphic and the type doesn't appear in the

143+-- return type, then no, otherwise yes.

144+getUnmatchable :: Context -> Name -> [Bool]

145+getUnmatchable ctxt n | isDConName n ctxt && n /= inferCon

146+ = case lookupTyExact n ctxt of

147+ Nothing -> []

148+ Just ty -> checkArgs [] [] ty

149+ where checkArgs :: [Name] -> [[Name]] -> Type -> [Bool]

150+ checkArgs env ns (Bind n (Pi t _) sc)

151+ = let env' = case t of

152+ TType _ -> n : env

153+ _ -> env in

154+ checkArgs env' (intersect env (refsIn t) : ns)

155+ (instantiate (P Bound n t) sc)

156+ checkArgs env ns t

157+ = map (anyMissing (intersect env (refsIn t))) (reverse ns)

158+

159+ anyMissing tns [] = False

160+ anyMissing tns (x : xs) = not (x `elem` tns) || anyMissing tns xs

161+

162+getUnmatchable ctxt n = []

163+

141data ElabCtxt = ElabCtxt { e_inarg :: Bool,

164data ElabCtxt = ElabCtxt { e_inarg :: Bool,

142 e_guarded :: Bool,

165 e_guarded :: Bool,

143 e_intype :: Bool,

166 e_intype :: Bool,

144− e_qq :: Bool }

167+ e_qq :: Bool,

168+ e_nomatching :: Bool -- ^ can't pattern match

169+ }

145

170

146−initElabCtxt = ElabCtxt False False False False

171+initElabCtxt = ElabCtxt False False False False False

147

172

148-- Returns the set of declarations we need to add to complete the definition

173-- Returns the set of declarations we need to add to complete the definition

149-- (most likely case blocks to elaborate)

174-- (most likely case blocks to elaborate)

@@ -268,6 +293,8 @@ elab ist info emode opts fn tm

268 | pattern && not reflection && not (e_qq ina) && not (e_intype ina)

293 | pattern && not reflection && not (e_qq ina) && not (e_intype ina)

269 && isTypeConst c

294 && isTypeConst c

270 = lift $ tfail $ Msg ("No explicit types on left hand side: " ++ show tm)

295 = lift $ tfail $ Msg ("No explicit types on left hand side: " ++ show tm)

296+ | pattern && e_nomatching ina

297+ = lift $ tfail $ Msg ("Attempting concrete match on polymorphic argument: " ++ show tm)

271 | otherwise = do apply (RConstant c) []; solve

298 | otherwise = do apply (RConstant c) []; solve

272 elab' ina fc (PQuote r) = do fill r; solve

299 elab' ina fc (PQuote r) = do fill r; solve

273 elab' ina _ (PTrue fc _) =

300 elab' ina _ (PTrue fc _) =

@@ -365,10 +392,12 @@ elab ist info emode opts fn tm

365-- elab' (_, _, inty) (PRef fc f)

392-- elab' (_, _, inty) (PRef fc f)

366-- | isTConName f (tt_ctxt ist) && pattern && not reflection && not inty

393-- | isTConName f (tt_ctxt ist) && pattern && not reflection && not inty

367-- = lift $ tfail (Msg "Typecase is not allowed")

394-- = lift $ tfail (Msg "Typecase is not allowed")

368− elab' ec _ (PRef fc n)

395+ elab' ec _ tm@(PRef fc n)

369 | pattern && not reflection && not (e_qq ec) && not (e_intype ec)

396 | pattern && not reflection && not (e_qq ec) && not (e_intype ec)

370 && isTConName n (tt_ctxt ist)

397 && isTConName n (tt_ctxt ist)

371 = lift $ tfail $ Msg ("No explicit types on left hand side: " ++ show tm)

398 = lift $ tfail $ Msg ("No explicit types on left hand side: " ++ show tm)

399+ | pattern && e_nomatching ec

400+ = lift $ tfail $ Msg ("Attempting concrete match on polymorphic argument: " ++ show tm)

372 | (pattern || (bindfree && bindable n)) && not (inparamBlock n) && not (e_qq ec)

401 | (pattern || (bindfree && bindable n)) && not (inparamBlock n) && not (e_qq ec)

373 = do let ina = e_inarg ec

402 = do let ina = e_inarg ec

374 guarded = e_guarded ec

403 guarded = e_guarded ec

@@ -395,6 +424,8 @@ elab ist info emode opts fn tm

395 | pattern && not reflection && not (e_qq ina) && not (e_intype ina)

424 | pattern && not reflection && not (e_qq ina) && not (e_intype ina)

396 && isTConName n (tt_ctxt ist)

425 && isTConName n (tt_ctxt ist)

397 = lift $ tfail $ Msg ("No explicit types on left hand side: " ++ show tm)

426 = lift $ tfail $ Msg ("No explicit types on left hand side: " ++ show tm)

427+ | pattern && e_nomatching ina

428+ = lift $ tfail $ Msg ("Attempting concrete match on polymorphic argument: " ++ show tm)

398 | otherwise = erun fc $ do apply (Var n) []; solve

429 | otherwise = erun fc $ do apply (Var n) []; solve

399 elab' ina fc (PLam n Placeholder sc)

430 elab' ina fc (PLam n Placeholder sc)

400 = do -- if n is a type constructor name, this makes no sense...

431 = do -- if n is a type constructor name, this makes no sense...

@@ -551,8 +582,14 @@ elab ist info emode opts fn tm

551-- = lift $ tfail (Msg "Typecase is not allowed")

582-- = lift $ tfail (Msg "Typecase is not allowed")

552 -- if f is local, just do a simple_app

583 -- if f is local, just do a simple_app

553 elab' ina _ tm@(PApp fc (PRef _ f) args)

584 elab' ina _ tm@(PApp fc (PRef _ f) args)

585+ | pattern && e_nomatching ina

586+ = lift $ tfail $ Msg ("Attempting concrete match on polymorphic argument: " ++ show tm)

587+ | otherwise

554 = do env <- get_env

588 = do env <- get_env

555 ty <- goal

589 ty <- goal

590+ let unmatchableArgs = if pattern

591+ then getUnmatchable (tt_ctxt ist) f

592+ else []

556 when (pattern && not reflection && not (e_qq ina) && not (e_intype ina)

593 when (pattern && not reflection && not (e_qq ina) && not (e_intype ina)

557 && isTConName f (tt_ctxt ist)) $

594 && isTConName f (tt_ctxt ist)) $

558 lift $ tfail $ Msg ("No explicit types on left hand side: " ++ show tm)

595 lift $ tfail $ Msg ("No explicit types on left hand side: " ++ show tm)

@@ -589,7 +626,8 @@ elab ist info emode opts fn tm

589 sortBy cmpArg (zip ns args)

626 sortBy cmpArg (zip ns args)

590 ulog <- getUnifyLog

627 ulog <- getUnifyLog

591 elabArgs ist (ina { e_inarg = e_inarg ina || not isinf })

628 elabArgs ist (ina { e_inarg = e_inarg ina || not isinf })

592− [] fc False f ns'

629+ [] fc False f

630+ (zip ns' (unmatchableArgs ++ repeat False))

593 (f == sUN "Force")

631 (f == sUN "Force")

594 (map (\x -> getTm x) eargs) -- TODO: remove this False arg

632 (map (\x -> getTm x) eargs) -- TODO: remove this False arg

595 solve

633 solve

@@ -1004,21 +1042,21 @@ elab ist info emode opts fn tm

1004 -> FC -- ^ Source location

1042 -> FC -- ^ Source location

1005 -> Bool

1043 -> Bool

1006 -> Name -- ^ Name of the function being applied

1044 -> Name -- ^ Name of the function being applied

1007− -> [(Name, Name)] -- ^ (Argument Name, Hole Name)

1045+ -> [((Name, Name), Bool)] -- ^ (Argument Name, Hole Name, unmatchable)

1008 -> Bool -- ^ under a 'force'

1046 -> Bool -- ^ under a 'force'

1009− -> [PTerm] -- ^ (Laziness, argument)

1047+ -> [PTerm] -- ^ argument

1010 -> ElabD ()

1048 -> ElabD ()

1011 elabArgs ist ina failed fc retry f [] force _ = return ()

1049 elabArgs ist ina failed fc retry f [] force _ = return ()

1012− elabArgs ist ina failed fc r f ((argName, holeName):ns) force (t : args)

1050+ elabArgs ist ina failed fc r f (((argName, holeName), unm):ns) force (t : args)

1013 = do hs <- get_holes

1051 = do hs <- get_holes

1014 if holeName `elem` hs then

1052 if holeName `elem` hs then

1015 do focus holeName

1053 do focus holeName

1016 case t of

1054 case t of

1017 Placeholder -> do movelast holeName

1055 Placeholder -> do movelast holeName

1018 elabArgs ist ina failed fc r f ns force args

1056 elabArgs ist ina failed fc r f ns force args

1019− _ -> elabArg argName holeName t

1057+ _ -> elabArg t

1020 else elabArgs ist ina failed fc r f ns force args

1058 else elabArgs ist ina failed fc r f ns force args

1021− where elabArg argName holeName t =

1059+ where elabArg t =

1022 do -- solveAutos ist fn False

1060 do -- solveAutos ist fn False

1023 now_elaborating fc f argName

1061 now_elaborating fc f argName

1024 wrapErr f argName $ do

1062 wrapErr f argName $ do

@@ -1033,7 +1071,8 @@ elab ist info emode opts fn tm

1033 g <- goal

1071 g <- goal

1034 ulog <- getUnifyLog

1072 ulog <- getUnifyLog

1035 traceWhen ulog ("Elaborating argument " ++ show (argName, holeName, g)) $

1073 traceWhen ulog ("Elaborating argument " ++ show (argName, holeName, g)) $

1074+ elab (ina { e_nomatching = unm }) (Just fc) t

1036− elab ina (Just fc) t; return failed

1075+ return failed

1037 done_elaborating_arg f argName

1076 done_elaborating_arg f argName

1038 elabArgs ist ina failed fc r f ns force args

1077 elabArgs ist ina failed fc r f ns force args

1039 wrapErr f argName action =

1078 wrapErr f argName action =

test/reg054/expectednew file+10

@@ -0,0 +1,10 @@

1+reg054.idr:18:5:When elaborating left hand side of inf:

2+When elaborating an application of constructor [91mMain.MkInfer[0m:

3+ Attempting concrete match on polymorphic argument: 0

4+reg054.idr:34:7:When elaborating left hand side of weird:

5+When elaborating argument [95mx[0m to Main.weird:

6+ No explicit types on left hand side: Char

7+reg054.idr:37:9:Can't convert

8+ [94mMaybe[0m [95ma[0m

9+with

10+ [95ma[0m

test/reg054/reg054.idrnew file+39

@@ -0,0 +1,39 @@

1+-- Catch typecase

3+data Ty = MInt | Str

5+eval : Ty -> Type

6+eval MInt = Maybe Int

7+eval Str = String

9+tcok : (x : Ty) -> eval x -> Int

10+tcok MInt (Just x) = x

11+tcok Str "foo" = 42

12+tcok Str x = 100

13+

14+data Infer : Type where

15+ MkInfer : (a : Type) -> a -> Infer

16+

17+inf : Infer -> Bool

18+inf (MkInfer _ Z) = True

19+inf (MkInfer _ (S k)) = False

20+

21+data InfView : Infer -> Type where

22+ INat : (x : Nat) -> InfView (MkInfer Nat x)

23+

24+foo : (i : Infer) -> InfView i -> Nat

25+foo (MkInfer _ _) (INat Z) = Z

26+foo (MkInfer _ _) (INat (S k)) = k

27+

28+data Weird : Type -> Type where

29+ WInt : Int -> Weird Int

30+ WStr : String -> Weird String

31+ WBot : Weird Void

32+

33+weird : Weird x -> x

34+weird {x = Char} y = '5'

35+

36+tctrick : a -> Int

37+tctrick (Just x) = x

38+tctrick Nothing = 42

39+

test/reg054/runnew file+2

@@ -0,0 +1,2 @@

1+#!/usr/bin/env bash

2+idris $@ reg054.idr --check