ad995dc · Idris-dev · git.iko.soy

git.iko.soy/Idris-dev

on master help sign in

Check that case does not overspecialise

ad995dcEdwin Brady13 years ago

src/Idris/Core/CaseTree.hs+95−34

compare with master

unifiedsplit

@@ -67,7 +67,7 @@ instance Show t => Show (SC' t) where

68type CaseTree = SC

69type Clause = ([Pat], (Term, Term))

70−type CS = ([Term], Int)

70+type CS = ([Term], Int, [(Name, Type)])

72instance TermSize SC where

73 termsize n (Case n' as) = termsize n as

@@ -204,13 +204,18 @@ simpleCase tc cover reflect phase fc cs

204 ns = take numargs args

205 (ns', ps') = order ns pats

206 (tree, st) = runState

207− (match ns' ps' (defaultCase cover)) ([], numargs)

207+ (match ns' ps' (defaultCase cover)) ([], numargs, [])

208− t = CaseDef ns (prune proj (depatt ns' tree)) (fst st) in

208+ t = CaseDef ns (prune proj (depatt ns' tree)) (fstT st) in

209− if proj then return (stripLambdas t) else return t

209+ if proj then return (stripLambdas t)

210+ else if checkSameTypes (lstT st) tree

211+ then return t

212+ else Error (At fc (Msg "Typecase is not allowed"))

210 Error err -> Error (At fc err)

213 Error err -> Error (At fc err)

211 where args = map (\i -> MN i "e") [0..]

214 where args = map (\i -> MN i "e") [0..]

212 defaultCase True = STerm Erased

215 defaultCase True = STerm Erased

213 defaultCase False = UnmatchedCase "Error"

216 defaultCase False = UnmatchedCase "Error"

217+ fstT (x, _, _) = x

218+ lstT (_, _, x) = x

214

219

215 chkAccessible (avs, l, c)

220 chkAccessible (avs, l, c)

216 | phase == RunTime || reflect = return (l, c)

221 | phase == RunTime || reflect = return (l, c)

@@ -218,17 +223,61 @@ simpleCase tc cover reflect phase fc cs

218 return (l, c)

223 return (l, c)

219

224

220 acc [] n = Error (Inaccessible n)

225 acc [] n = Error (Inaccessible n)

221− acc (PV x : xs) n | x == n = OK ()

226+ acc (PV x t : xs) n | x == n = OK ()

222 acc (PCon _ _ ps : xs) n = acc (ps ++ xs) n

227 acc (PCon _ _ ps : xs) n = acc (ps ++ xs) n

223 acc (PSuc p : xs) n = acc (p : xs) n

228 acc (PSuc p : xs) n = acc (p : xs) n

224 acc (_ : xs) n = acc xs n

229 acc (_ : xs) n = acc xs n

225

230

231+-- For each 'Case', make sure every choice is in the same type family,

232+-- as directed by the variable type (i.e. there is no implicit type casing

233+-- going on).

234+

235+checkSameTypes :: [(Name, Type)] -> SC -> Bool

236+checkSameTypes tys (Case n alts)

237+ = case lookup n tys of

238+ Just t -> and (map (checkAlts t) alts)

239+ _ -> and (map ((checkSameTypes tys).getSC) alts)

240+ where

241+ checkAlts t (ConCase n _ _ sc) = isType n t && checkSameTypes tys sc

242+ checkAlts (Constant t) (ConstCase c sc) = isConstType c t && checkSameTypes tys sc

243+ checkAlts _ (ConstCase c sc) = False

244+ checkAlts _ _ = True

245+

246+ getSC (ConCase _ _ _ sc) = sc

247+ getSC (FnCase _ _ sc) = sc

248+ getSC (ConstCase _ sc) = sc

249+ getSC (SucCase _ sc) = sc

250+ getSC (DefaultCase sc) = sc

251+checkSameTypes _ _ = True

252+

253+-- FIXME: All we're actually doing here is checking that we haven't arrived

254+-- at a specific constructor for a polymorphic argument. I *think* this

255+-- is sufficient, but if it turns out not to be, fix it!

256+isType n t | (P (TCon _ _) _ _, _) <- unApply t = True

257+isType n t = False

258+

259+isConstType (I _) (AType (ATInt ITNative)) = True

260+isConstType (BI _) (AType (ATInt ITBig)) = True

261+isConstType (Fl _) (AType ATFloat) = True

262+isConstType (Ch _) (AType (ATInt ITChar)) = True

263+isConstType (Str _) StrType = True

264+isConstType (B8 _) (AType (ATInt _)) = True

265+isConstType (B16 _) (AType (ATInt _)) = True

266+isConstType (B32 _) (AType (ATInt _)) = True

267+isConstType (B64 _) (AType (ATInt _)) = True

268+isConstType (B8V _) (AType (ATInt _)) = True

269+isConstType (B16V _) (AType (ATInt _)) = True

270+isConstType (B32V _) (AType (ATInt _)) = True

271+isConstType (B64V _) (AType (ATInt _)) = True

272+isConstType _ _ = False

273+

226data Pat = PCon Name Int [Pat]

274data Pat = PCon Name Int [Pat]

227 | PConst Const

275 | PConst Const

228− | PV Name

276+ | PV Name Type

229 | PSuc Pat -- special case for n+1 on Integer

277 | PSuc Pat -- special case for n+1 on Integer

230 | PReflected Name [Pat]

278 | PReflected Name [Pat]

231 | PAny

279 | PAny

280+ | PTyPat -- typecase, not allowed, inspect last

232 deriving Show

281 deriving Show

233

282

234-- If there are repeated variables, take the *last* one (could be name shadowing

283-- If there are repeated variables, take the *last* one (could be name shadowing

@@ -250,25 +299,30 @@ toPat reflect tc tms = evalState (mapM (\x -> toPat' x []) tms) []

250 = do p' <- toPat' p []

299 = do p' <- toPat' p []

251 return $ PSuc p'

300 return $ PSuc p'

252 -- Typecase

301 -- Typecase

253− toPat' (P (TCon t a) n _) args | tc

302+-- toPat' (P (TCon t a) n _) args | tc

254− = do args' <- mapM (\x -> toPat' x []) args

303+-- = do args' <- mapM (\x -> toPat' x []) args

255− return $ PCon n t args'

304+-- return $ PCon n t args'

256− toPat' (Constant (AType (ATInt ITNative))) []

305+-- toPat' (Constant (AType (ATInt ITNative))) []

257− | tc = return $ PCon (UN "Int") 1 []

306+-- | tc = return $ PCon (UN "Int") 1 []

258− toPat' (Constant (AType ATFloat)) [] | tc = return $ PCon (UN "Float") 2 []

307+-- toPat' (Constant (AType ATFloat)) [] | tc = return $ PCon (UN "Float") 2 []

259− toPat' (Constant (AType (ATInt ITChar))) [] | tc = return $ PCon (UN "Char") 3 []

308+-- toPat' (Constant (AType (ATInt ITChar))) [] | tc = return $ PCon (UN "Char") 3 []

260− toPat' (Constant StrType) [] | tc = return $ PCon (UN "String") 4 []

309+-- toPat' (Constant StrType) [] | tc = return $ PCon (UN "String") 4 []

261− toPat' (Constant PtrType) [] | tc = return $ PCon (UN "Ptr") 5 []

310+-- toPat' (Constant PtrType) [] | tc = return $ PCon (UN "Ptr") 5 []

262− toPat' (Constant (AType (ATInt ITBig))) []

311+-- toPat' (Constant (AType (ATInt ITBig))) []

263− | tc = return $ PCon (UN "Integer") 6 []

312+-- | tc = return $ PCon (UN "Integer") 6 []

264− toPat' (Constant (AType (ATInt (ITFixed n)))) []

313+-- toPat' (Constant (AType (ATInt (ITFixed n)))) []

265− | tc = return $ PCon (UN (fixedN n)) (7 + fromEnum n) [] -- 7-10 inclusive

314+-- | tc = return $ PCon (UN (fixedN n)) (7 + fromEnum n) [] -- 7-10 inclusive

266− toPat' (P Bound n _) [] = do ns <- get

315+ toPat' (P Bound n ty) [] = -- trace (show (n, ty)) $

316+ do ns <- get

267 if n `elem` ns

317 if n `elem` ns

268 then return PAny

318 then return PAny

269 else do put (n : ns)

319 else do put (n : ns)

270− return (PV n)

320+ return (PV n ty)

271 toPat' (App f a) args = toPat' f (a : args)

321 toPat' (App f a) args = toPat' f (a : args)

322+ toPat' (Constant (AType _)) [] = return PTyPat

323+ toPat' (Constant StrType) [] = return PTyPat

324+ toPat' (Constant PtrType) [] = return PTyPat

325+ toPat' (Constant VoidType) [] = return PTyPat

272 toPat' (Constant x) [] = return $ PConst x

326 toPat' (Constant x) [] = return $ PConst x

273 toPat' (Bind n (Pi t) sc) [] | reflect && noOccurrence n sc

327 toPat' (Bind n (Pi t) sc) [] | reflect && noOccurrence n sc

274 = do t' <- toPat' t []

328 = do t' <- toPat' t []

@@ -289,9 +343,10 @@ data Partition = Cons [Clause]

289 | Vars [Clause]

343 | Vars [Clause]

290 deriving Show

344 deriving Show

291

345

292−isVarPat (PV _ : ps , _) = True

346+isVarPat (PV _ _ : ps , _) = True

293−isVarPat (PAny : ps , _) = True

347+isVarPat (PAny : ps , _) = True

348+isVarPat (PTyPat : ps , _) = True

294−isVarPat _ = False

349+isVarPat _ = False

295

350

296isConPat (PCon _ _ _ : ps, _) = True

351isConPat (PCon _ _ _ : ps, _) = True

297isConPat (PReflected _ _ : ps, _) = True

352isConPat (PReflected _ _ : ps, _) = True

@@ -337,8 +392,8 @@ order ns cs = let patnames = transpose (map (zip ns) (map fst cs))

337match :: [Name] -> [Clause] -> SC -- error case

392match :: [Name] -> [Clause] -> SC -- error case

338 -> State CS SC

393 -> State CS SC

339match [] (([], ret) : xs) err

394match [] (([], ret) : xs) err

340− = do (ts, v) <- get

395+ = do (ts, v, ntys) <- get

341− put (ts ++ (map (fst.snd) xs), v)

396+ put (ts ++ (map (fst.snd) xs), v, ntys)

342 case snd ret of

397 case snd ret of

343 Impossible -> return ImpossibleCase

398 Impossible -> return ImpossibleCase

344 tm -> return $ STerm tm -- run out of arguments

399 tm -> return $ STerm tm -- run out of arguments

@@ -408,12 +463,15 @@ argsToAlt rs@((r, m) : rest)

408 return (newArgs, addRs rs)

463 return (newArgs, addRs rs)

409 where

464 where

410 getNewVars [] = return []

465 getNewVars [] = return []

411− getNewVars ((PV n) : ns) = do v <- getVar "e"

466+ getNewVars ((PV n t) : ns) = do v <- getVar "e"

412− nsv <- getNewVars ns

467+ nsv <- getNewVars ns

413− return (v : nsv)

468+ return (v : nsv)

414 getNewVars (PAny : ns) = do v <- getVar "i"

469 getNewVars (PAny : ns) = do v <- getVar "i"

415 nsv <- getNewVars ns

470 nsv <- getNewVars ns

416 return (v : nsv)

471 return (v : nsv)

472+ getNewVars (PTyPat : ns) = do v <- getVar "t"

473+ nsv <- getNewVars ns

474+ return (v : nsv)

417 getNewVars (_ : ns) = do v <- getVar "e"

475 getNewVars (_ : ns) = do v <- getVar "e"

418 nsv <- getNewVars ns

476 nsv <- getNewVars ns

419 return (v : nsv)

477 return (v : nsv)

@@ -424,7 +482,7 @@ argsToAlt rs@((r, m) : rest)

424 uniq i n = n

482 uniq i n = n

425

483

426getVar :: String -> State CS Name

484getVar :: String -> State CS Name

427−getVar b = do (t, v) <- get; put (t, v+1); return (MN v b)

485+getVar b = do (t, v, ntys) <- get; put (t, v+1, ntys); return (MN v b)

428

486

429groupCons :: [Clause] -> State CS [Group]

487groupCons :: [Clause] -> State CS [Group]

430groupCons cs = gc [] cs

488groupCons cs = gc [] cs

@@ -454,12 +512,15 @@ groupCons cs = gc [] cs

454

512

455varRule :: [Name] -> [Clause] -> SC -> State CS SC

513varRule :: [Name] -> [Clause] -> SC -> State CS SC

456varRule (v : vs) alts err =

514varRule (v : vs) alts err =

457− do let alts' = map (repVar v) alts

515+ do alts' <- mapM (repVar v) alts

458 match vs alts' err

516 match vs alts' err

459 where

517 where

460− repVar v (PV p : ps , (lhs, res))

518+ repVar v (PV p ty : ps , (lhs, res))

519+ = do (cs, i, ntys) <- get

520+ put (cs, i, (v, ty) : ntys)

461− = (ps, (lhs, subst p (P Bound v Erased) res))

521+ return (ps, (lhs, subst p (P Bound v ty) res))

462− repVar v (PAny : ps , res) = (ps, res)

522+ repVar v (PAny : ps , res) = return (ps, res)

523+ repVar v (PTyPat : ps , res) = return (ps, res)

463

524

464-- fix: case e of S k -> f (S k) ==> case e of S k -> f e

525-- fix: case e of S k -> f (S k) ==> case e of S k -> f e

465

526