521dc75 · Idris-dev · git.iko.soy

git.iko.soy/Idris-dev

on master help sign in

Prune case trees properly on optimised Nat

521dc75Edwin Brady13 years ago

src/Core/CaseTree.hs+11−1

compare with master

unifiedsplit

@@ -502,6 +502,9 @@ prune proj (Case n alts)

502 [] -> ImpossibleCase

503 as@[ConCase cn i args sc] -> if proj then mkProj n 0 args sc

504 else Case n as

505+ as@[SucCase cn sc] -> if proj then mkProj n (-1) [cn] sc

506+ else Case n as

507+ as@[ConstCase _ sc] -> prune proj sc

505 -- Bit of a hack here! The default case will always be 0, make sure

508 -- Bit of a hack here! The default case will always be 0, make sure

506 -- it gets caught first.

509 -- it gets caught first.

507 [s@(SucCase _ _), DefaultCase dc]

510 [s@(SucCase _ _), DefaultCase dc]

@@ -517,9 +520,16 @@ prune proj (Case n alts)

517 notErased (DefaultCase ImpossibleCase) = False

520 notErased (DefaultCase ImpossibleCase) = False

518 notErased _ = True

521 notErased _ = True

519

522

520− mkProj n i [] sc = sc

523+ mkProj n i [] sc = prune proj sc

521 mkProj n i (x : xs) sc = mkProj n (i + 1) xs (projRep x n i sc)

524 mkProj n i (x : xs) sc = mkProj n (i + 1) xs (projRep x n i sc)

522

525

526+ -- Change every 'n' in sc to 'n-1'

527+-- mkProjS n cn sc = prune proj (fmap projn sc) where

528+-- projn pn@(P _ n' _)

529+-- | cn == n' = App (App (P Ref (UN "prim__subBigInt") Erased)

530+-- (P Bound n Erased)) (Constant (BI 1))

531+-- projn t = t

532+

523 projRep :: Name -> Name -> Int -> SC -> SC

533 projRep :: Name -> Name -> Int -> SC -> SC

524 projRep arg n i (Case x alts)

534 projRep arg n i (Case x alts)

525 | x == arg = ProjCase (Proj (P Bound n Erased) i)

535 | x == arg = ProjCase (Proj (P Bound n Erased) i)

src/Core/Evaluate.hs+8−4

@@ -29,6 +29,7 @@ data EvalOpt = Spec

29 | HNF

30 | Simplify

31 | AtREPL

32+ | RunTT

32 deriving (Show, Eq)

33 deriving (Show, Eq)

34initEval = ES [] 0

35initEval = ES [] 0

@@ -162,6 +163,7 @@ eval :: Bool -> Context -> [(Name, Int)] -> Env -> TT Name ->

162eval traceon ctxt ntimes genv tm opts = ev ntimes [] True [] tm where

163eval traceon ctxt ntimes genv tm opts = ev ntimes [] True [] tm where

163 spec = Spec `elem` opts

164 spec = Spec `elem` opts

164 simpl = Simplify `elem` opts

165 simpl = Simplify `elem` opts

166+ runtime = RunTT `elem` opts

165 atRepl = AtREPL `elem` opts

167 atRepl = AtREPL `elem` opts

166 hnf = HNF `elem` opts

168 hnf = HNF `elem` opts

167

169

@@ -173,6 +175,10 @@ eval traceon ctxt ntimes genv tm opts = ev ntimes [] True [] tm where

173 || (n == UN "prim__syntactic_eq")

175 || (n == UN "prim__syntactic_eq")

174 | otherwise = False

176 | otherwise = False

175

177

178+ getCases cd | simpl = cases_totcheck cd

179+ | runtime = cases_runtime cd

180+ | otherwise = cases_compiletime cd

181+

176 ev ntimes stk top env (P _ n ty)

182 ev ntimes stk top env (P _ n ty)

177 | Just (Let t v) <- lookup n genv = ev ntimes stk top env v

183 | Just (Let t v) <- lookup n genv = ev ntimes stk top env v

178 ev ntimes_in stk top env (P Ref n ty)

184 ev ntimes_in stk top env (P Ref n ty)

@@ -189,8 +195,7 @@ eval traceon ctxt ntimes genv tm opts = ev ntimes [] True [] tm where

189 [(CaseOp ci _ _ _ cd, acc)]

195 [(CaseOp ci _ _ _ cd, acc)]

190 | acc == Public &&

196 | acc == Public &&

191 null (fst (cases_totcheck cd)) -> -- unoptimised version

197 null (fst (cases_totcheck cd)) -> -- unoptimised version

192− let (_, tree) = if simpl then cases_totcheck cd

198+ let (_, tree) = getCases cd in

193− else cases_compiletime cd in

194 if blockSimplify ci n stk

199 if blockSimplify ci n stk

195 then liftM (VP Ref n) (ev ntimes stk top env ty)

200 then liftM (VP Ref n) (ev ntimes stk top env ty)

196 else do c <- evCase ntimes n (n:stk) top env [] [] tree

201 else do c <- evCase ntimes n (n:stk) top env [] [] tree

@@ -261,8 +266,7 @@ eval traceon ctxt ntimes genv tm opts = ev ntimes [] True [] tm where

261 case val of

266 case val of

262 [(CaseOp ci _ _ _ cd, acc)]

267 [(CaseOp ci _ _ _ cd, acc)]

263 | acc == Public -> -- unoptimised version

268 | acc == Public -> -- unoptimised version

264− let (ns, tree) = if simpl then cases_totcheck cd

269+ let (ns, tree) = getCases cd in

265− else cases_compiletime cd in

266 if blockSimplify ci n stk

270 if blockSimplify ci n stk

267 then return $ unload env (VP Ref n ty) args

271 then return $ unload env (VP Ref n ty) args

268 else do c <- evCase ntimes n (n:stk) top env ns args tree

272 else do c <- evCase ntimes n (n:stk) top env ns args tree

src/Core/TT.hs+1

@@ -572,6 +572,7 @@ data TT n = P NameType n (TT n) -- ^ named references

572 | App (TT n) (TT n) -- ^ function, function type, arg

573 | Constant Const -- ^ constant

574 | Proj (TT n) Int -- ^ argument projection; runtime only

575+ -- (-1) is a special case for 'subtract one from BI'

575 | Erased -- ^ an erased term

576 | Erased -- ^ an erased term

576 | Impossible -- ^ special case for totality checking

577 | Impossible -- ^ special case for totality checking

577 | TType UExp -- ^ the type of types at some level

578 | TType UExp -- ^ the type of types at some level

src/IRTS/Compiler.hs+5−1

@@ -67,7 +67,7 @@ compile codegen f tm

67 dumpDefun <- getDumpDefun

68 case dumpCases of

69 Nothing -> return ()

70− Just f -> runIO $ writeFile f (showCaseTrees tagged)

70+ Just f -> runIO $ writeFile f (showCaseTrees defs)

71 case dumpDefun of

72 Nothing -> return ()

73 Just f -> runIO $ writeFile f (dumpDefuns defuns)

@@ -259,6 +259,10 @@ instance ToIR (TT Name) where

259 v' <- ir' env v

260 return $ LLet n v' sc'

261 ir' env (Bind _ _ _) = return $ LNothing

262+ ir' env (Proj t i) | i == -1

263+ = do t' <- ir' env t

264+ return $ LOp (LMinus (ATInt ITBig))

265+ [t', LConst (BI 1)]

262 ir' env (Proj t i) = do t' <- ir' env t

266 ir' env (Proj t i) = do t' <- ir' env t

263 return $ LProj t' i

267 return $ LProj t' i

264 ir' env (Constant c) = return $ LConst c

268 ir' env (Constant c) = return $ LConst c