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

git.iko.soy/Idris-dev

Prune case trees properly on optimised Nat

x!-1 is treated as a special case in argument projection, where x is assumed to be a Big Integer and has 1 subtracted from it. Case trees where only a single constant or successor are left are now collapsed.

commit521dc75c20a774e368ffd8b6d3dfc993ab14beac authorEdwin Brady <ecb10@st-andrews.ac.uk> dateWed 6 Nov 2013, 20:15 (13 years ago) parent86fc1a1

4 files changed+25−6

compare with master

unifiedsplit

src/Core/CaseTree.hs+11−1 src/Core/Evaluate.hs+8−4 src/Core/TT.hs+1 src/IRTS/Compiler.hs+5−1

src/Core/CaseTree.hs+11−1

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

502502 [] -> ImpossibleCase

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

504504 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

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

506509 -- it gets caught first.

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

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

517520 notErased (DefaultCase ImpossibleCase) = False

518521 notErased _ = True

519522

520− mkProj n i [] sc = sc

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

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

522525

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+

523533 projRep :: Name -> Name -> Int -> SC -> SC

524534 projRep arg n i (Case x alts)

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

src/Core/Evaluate.hs+8−4

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

2929 | HNF

3030 | Simplify

3131 | AtREPL

32+ | RunTT

3233 deriving (Show, Eq)

3334

3435initEval = ES [] 0

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

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

163164 spec = Spec `elem` opts

164165 simpl = Simplify `elem` opts

166+ runtime = RunTT `elem` opts

165167 atRepl = AtREPL `elem` opts

166168 hnf = HNF `elem` opts

167169

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

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

174176 | otherwise = False

175177

178+ getCases cd | simpl = cases_totcheck cd

179+ | runtime = cases_runtime cd

180+ | otherwise = cases_compiletime cd

181+

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

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

178184 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

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

190196 | acc == Public &&

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

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

193− else cases_compiletime cd in

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

194199 if blockSimplify ci n stk

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

196201 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

261266 case val of

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

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

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

265− else cases_compiletime cd in

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

266270 if blockSimplify ci n stk

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

268272 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

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

573573 | Constant Const -- ^ constant

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

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

575576 | Erased -- ^ an erased term

576577 | Impossible -- ^ special case for totality checking

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

src/IRTS/Compiler.hs+5−1

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

6767 dumpDefun <- getDumpDefun

6868 case dumpCases of

6969 Nothing -> return ()

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

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

7171 case dumpDefun of

7272 Nothing -> return ()

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

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

259259 v' <- ir' env v

260260 return $ LLet n v' sc'

261261 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)]

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

263267 return $ LProj t' i

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