bb76c6c · Idris-dev · git.iko.soy

git.iko.soy/Idris-dev

on master help sign in

More aggressive simplification; fix case generation bug

bb76c6cEdwin Brady14 years ago

idris.cabal+2−1

compare with master

unifiedsplit

@@ -73,7 +73,8 @@ Executable idris

73 Pkg.Package, Pkg.PParser,

75 IRTS.Lang, IRTS.LParser, IRTS.Bytecode, IRTS.Simplified,

76− IRTS.CodegenC, IRTS.Defunctionalise, IRTS.Compiler,

76+ IRTS.CodegenC, IRTS.Defunctionalise, IRTS.Inliner,

77+ IRTS.Compiler,

78 Paths_idris

79 Paths_idris

src/Core/CaseTree.hs+21−6

@@ -31,10 +31,19 @@ type CaseTree = SC

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

32type CS = ([Term], Int)

34+instance TermSize SC where

35+ termsize (Case n as) = termsize as

36+ termsize (STerm t) = termsize t

37+ termsize _ = 1

38+

39+instance TermSize CaseAlt where

40+ termsize (ConCase _ _ _ s) = termsize s

41+ termsize (ConstCase _ s) = termsize s

42+ termsize (DefaultCase s) = termsize s

43+

34-- simple terms can be inlined trivially - good for primitives in particular

44-- simple terms can be inlined trivially - good for primitives in particular

35small :: SC -> Bool

45small :: SC -> Bool

36−-- small (STerm t) = True

46+small t = termsize t < 150

37−small _ = False

39namesUsed :: SC -> [Name]

48namesUsed :: SC -> [Name]

40namesUsed sc = nub $ nu' [] sc where

49namesUsed sc = nub $ nu' [] sc where

@@ -121,6 +130,7 @@ toPat tc tms = evalState (mapM (\x -> toPat' x []) tms) []

121

130

122data Partition = Cons [Clause]

131data Partition = Cons [Clause]

123 | Vars [Clause]

132 | Vars [Clause]

133+ deriving Show

124

134

125isVarPat (PV _ : ps , _) = True

135isVarPat (PV _ : ps , _) = True

126isVarPat (PAny : ps , _) = True

136isVarPat (PAny : ps , _) = True

@@ -145,7 +155,8 @@ match [] (([], ret) : xs) err

145 = do (ts, v) <- get

155 = do (ts, v) <- get

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

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

147 return $ STerm (snd ret) -- run out of arguments

157 return $ STerm (snd ret) -- run out of arguments

158+match vs cs err = do let ps = partition cs

148−match vs cs err = do cs <- mixture vs (partition cs) err

159+ cs <- mixture vs ps err

149 return cs

160 return cs

150

161

151mixture :: [Name] -> [Partition] -> SC -> State CS SC

162mixture :: [Name] -> [Partition] -> SC -> State CS SC

@@ -188,19 +199,23 @@ caseGroups (v:vs) gs err = do g <- altGroups gs

188

199

189argsToAlt :: [([Pat], Clause)] -> State CS ([Name], [Clause])

200argsToAlt :: [([Pat], Clause)] -> State CS ([Name], [Clause])

190argsToAlt [] = return ([], [])

201argsToAlt [] = return ([], [])

191−argsToAlt rs@((r, m) : _)

202+argsToAlt rs@((r, m) : rest)

192 = do newArgs <- getNewVars r

203 = do newArgs <- getNewVars r

193 return (newArgs, addRs rs)

204 return (newArgs, addRs rs)

194 where

205 where

195 getNewVars [] = return []

206 getNewVars [] = return []

207+ getNewVars ((PV n) : ns) = do v <- getVar

196− getNewVars ((PV n) : ns) = do nsv <- getNewVars ns

208+ nsv <- getNewVars ns

197− return (n : nsv)

209+ return (v : nsv)

198 getNewVars (_ : ns) = do v <- getVar

210 getNewVars (_ : ns) = do v <- getVar

199 nsv <- getNewVars ns

211 nsv <- getNewVars ns

200 return (v : nsv)

212 return (v : nsv)

201 addRs [] = []

213 addRs [] = []

202 addRs ((r, (ps, res)) : rs) = ((r++ps, res) : addRs rs)

214 addRs ((r, (ps, res)) : rs) = ((r++ps, res) : addRs rs)

203

215

216+ uniq i (UN n) = MN i n

217+ uniq i n = n

218+

204getVar :: State CS Name

219getVar :: State CS Name

205getVar = do (t, v) <- get; put (t, v+1); return (MN v "e")

220getVar = do (t, v) <- get; put (t, v+1); return (MN v "e")

206

221

src/Core/Evaluate.hs+19−14

@@ -109,7 +109,7 @@ specialise ctxt env limits t

109

110simplify :: Context -> Env -> TT Name -> TT Name

111simplify ctxt env t

112− = evalState (do val <- eval False ctxt threshold []

112+ = evalState (do val <- eval False ctxt threshold [(UN "lazy", 0)]

113 (map finalEntry env) (finalise t) [Simplify]

114 quote 0 val) initEval

115

@@ -133,12 +133,13 @@ unbindEnv :: EnvTT n -> TT n -> TT n

133unbindEnv [] tm = tm

134unbindEnv (_:bs) (Bind n b sc) = unbindEnv bs sc

135

136−usable :: Name -> [(Name, Int)] -> (Bool, [(Name, Int)])

136+usable :: Bool -> Name -> [(Name, Int)] -> (Bool, [(Name, Int)])

137−usable n [] = (True, [])

137+usable s n [] = (True, [])

138−usable n ns = case lookup n ns of

138+usable s n ns = case lookup n ns of

139− Just 0 -> (False, ns)

139+ Just 0 -> (False, ns)

140− Just i -> (True, (n, abs (i-1)) : filter (\ (n', _) -> n/=n') ns)

140+ Just i -> (True, (n, abs (i-1)) : filter (\ (n', _) -> n/=n') ns)

141+ _ -> if s then (True, (n, 0) : filter (\ (n', _) -> n/=n') ns)

141− _ -> (True, (n, 100) : filter (\ (n', _) -> n/=n') ns)

142+ else (True, (n, 100) : filter (\ (n', _) -> n/=n') ns)

142

143

143reduction :: Eval ()

144reduction :: Eval ()

144reduction = do ES ns s <- get

145reduction = do ES ns s <- get

@@ -158,7 +159,7 @@ eval traceon ctxt maxred ntimes genv tm opts = ev ntimes [] True [] tm where

158 | Just (Let t v) <- lookup n genv = do when (not atRepl) $ step maxred

159 | Just (Let t v) <- lookup n genv = do when (not atRepl) $ step maxred

159 ev ntimes stk top env v

160 ev ntimes stk top env v

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

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

161− | (True, ntimes) <- usable n ntimes_in

162+ | (True, ntimes) <- usable simpl n ntimes_in

162 = do let val = lookupDefAcc Nothing n atRepl ctxt

163 = do let val = lookupDefAcc Nothing n atRepl ctxt

163 when (not atRepl) $ step maxred

164 when (not atRepl) $ step maxred

164 case val of

165 case val of

@@ -178,10 +179,17 @@ eval traceon ctxt maxred ntimes genv tm opts = ev ntimes [] True [] tm where

178 ev ntimes stk top env (V i) | i < length env = return $ env !! i

179 ev ntimes stk top env (V i) | i < length env = return $ env !! i

179 | otherwise = return $ VV i

180 | otherwise = return $ VV i

180 ev ntimes stk top env (Bind n (Let t v) sc)

181 ev ntimes stk top env (Bind n (Let t v) sc)

182+ | not simpl || vinstances 0 sc < 2

181 = do v' <- ev ntimes stk top env v --(finalise v)

183 = do v' <- ev ntimes stk top env v --(finalise v)

182 when (not atRepl) $ step maxred

184 when (not atRepl) $ step maxred

183 sc' <- ev ntimes stk top (v' : env) sc

185 sc' <- ev ntimes stk top (v' : env) sc

184 wknV (-1) sc'

186 wknV (-1) sc'

187+ | otherwise

188+ = do t' <- ev ntimes stk top env t

189+ v' <- ev ntimes stk top env v --(finalise v)

190+ when (not atRepl) $ step maxred

191+ sc' <- ev ntimes stk top (v' : env) sc

192+ return $ VBind n (Let t' v') (\x -> return sc')

185 ev ntimes stk top env (Bind n (NLet t v) sc)

193 ev ntimes stk top env (Bind n (NLet t v) sc)

186 = do t' <- ev ntimes stk top env (finalise t)

194 = do t' <- ev ntimes stk top env (finalise t)

187 v' <- ev ntimes stk top env (finalise v)

195 v' <- ev ntimes stk top env (finalise v)

@@ -219,7 +227,7 @@ eval traceon ctxt maxred ntimes genv tm opts = ev ntimes [] True [] tm where

219-- apply ntimes stk False env f args

227-- apply ntimes stk False env f args

220-- | spec = specApply ntimes stk env f args

228-- | spec = specApply ntimes stk env f args

221 apply ntimes_in stk top env f@(VP Ref n ty) args

229 apply ntimes_in stk top env f@(VP Ref n ty) args

222− | (True, ntimes) <- usable n ntimes_in

230+ | (True, ntimes) <- usable simpl n ntimes_in

223 = traceWhen traceon (show stk) $

231 = traceWhen traceon (show stk) $

224 do let val = lookupDefAcc Nothing n atRepl ctxt

232 do let val = lookupDefAcc Nothing n atRepl ctxt

225 case val of

233 case val of

@@ -683,16 +691,13 @@ addCasedef :: Name -> Bool -> Bool -> Bool ->

683 Type -> Context -> Context

691 Type -> Context -> Context

684addCasedef n alwaysInline tcase covering ps psrt ty uctxt

692addCasedef n alwaysInline tcase covering ps psrt ty uctxt

685 = let ctxt = definitions uctxt

693 = let ctxt = definitions uctxt

686− ps' = ps -- simpl ps in

687− ctxt' = case (simpleCase tcase covering (FC "" 0) ps',

694+ ctxt' = case (simpleCase tcase covering (FC "" 0) ps,

688 simpleCase tcase covering (FC "" 0) psrt) of

695 simpleCase tcase covering (FC "" 0) psrt) of

689 (OK (CaseDef args sc _), OK (CaseDef args' sc' _)) ->

696 (OK (CaseDef args sc _), OK (CaseDef args' sc' _)) ->

690− let inl = alwaysInline in

697+ let inl = alwaysInline || small sc' in

691 addDef n (CaseOp inl ty ps args sc args' sc',

698 addDef n (CaseOp inl ty ps args sc args' sc',

692 Public, Unchecked) ctxt in

699 Public, Unchecked) ctxt in

693 uctxt { definitions = ctxt' }

700 uctxt { definitions = ctxt' }

694− where simpl [] = []

695− simpl ((l,r) : xs) = (l, simplify uctxt [] r) : simpl xs

696

701

697addOperator :: Name -> Type -> Int -> ([Value] -> Maybe Value) -> Context -> Context

702addOperator :: Name -> Type -> Int -> ([Value] -> Maybe Value) -> Context -> Context

698addOperator n ty a op uctxt

703addOperator n ty a op uctxt

src/Core/TT.hs+23

@@ -417,6 +417,20 @@ data TT n = P NameType n (TT n) -- embed type

417deriving instance Binary TT

418!-}

419

420+class TermSize a where

421+ termsize :: a -> Int

422+

423+instance TermSize a => TermSize [a] where

424+ termsize [] = 0

425+ termsize (x : xs) = termsize x + termsize xs

426+

427+instance TermSize (TT a) where

428+ termsize (P _ _ _) = 1

429+ termsize (V _) = 1

430+ termsize (Bind n (Let t v) sc) = termsize v + termsize sc

431+ termsize (App f a) = termsize f + termsize a

432+ termsize _ = 1

433+

420instance Sized a => Sized (TT a) where

434instance Sized a => Sized (TT a) where

421 size (P name n trm) = 1 + size name + size n + size trm

435 size (P name n trm) = 1 + size name + size n + size trm

422 size (V v) = 1

436 size (V v) = 1

@@ -459,6 +473,15 @@ isInjective (Bind _ (Pi _) sc) = True

459isInjective (App f a) = isInjective f

473isInjective (App f a) = isInjective f

460isInjective _ = False

474isInjective _ = False

461

475

476+-- Count the number of instances of a de Bruijn index in a term

477+vinstances :: Int -> TT n -> Int

478+vinstances i (V x) | i == x = 1

479+vinstances i (App f a) = vinstances i f + vinstances i a

480+vinstances i (Bind x b sc) = instancesB b + vinstances (i + 1) sc

481+ where instancesB (Let t v) = vinstances i v

482+ instancesB _ = 0

483+vinstances i t = 0

484+

462instantiate :: TT n -> TT n -> TT n

485instantiate :: TT n -> TT n -> TT n

463instantiate e = subst 0 where

486instantiate e = subst 0 where

464 subst i (V x) | i == x = e

487 subst i (V x) | i == x = e

src/IRTS/Compiler.hs+24−15

@@ -7,6 +7,7 @@ import IRTS.Defunctionalise

7import IRTS.Simplified

8import IRTS.CodegenC

9import IRTS.CodegenJava

10+import IRTS.Inliner

11import Idris.AbsSyntax

12import Idris.AbsSyntax

12import Core.TT

13import Core.TT

@@ -36,7 +37,13 @@ compile target f tm

36 -- iputStrLn $ showSep "\n" (map show defs)

37 -- iputStrLn $ showSep "\n" (map show defs)

37 let (nexttag, tagged) = addTags 65536 (liftAll defs)

38 let (nexttag, tagged) = addTags 65536 (liftAll defs)

38 let ctxtIn = addAlist tagged emptyContext

39 let ctxtIn = addAlist tagged emptyContext

40+ iLOG "Defunctionalising"

39− let defuns = defunctionalise nexttag ctxtIn

41+ let defuns_in = defunctionalise nexttag ctxtIn

42+ logLvl 5 $ show defuns_in

43+ iLOG "Inlining"

44+ let defuns = inline defuns_in

45+ logLvl 5 $ show defuns

46+

40 -- iputStrLn $ showSep "\n" (map show (toAlist defuns))

47 -- iputStrLn $ showSep "\n" (map show (toAlist defuns))

41 let checked = checkDefs defuns (toAlist defuns)

48 let checked = checkDefs defuns (toAlist defuns)

42 case checked of

49 case checked of

@@ -108,7 +115,7 @@ instance ToIR (TT Name) where

108 ir tm = ir' [] tm where

115 ir tm = ir' [] tm where

109 ir' env tm@(App f a)

116 ir' env tm@(App f a)

110 | (P _ (UN "mkForeign") _, args) <- unApply tm

117 | (P _ (UN "mkForeign") _, args) <- unApply tm

111− = doForeign args

118+ = doForeign env args

112 | (P _ (UN "unsafePerformIO") _, [_, arg]) <- unApply tm

119 | (P _ (UN "unsafePerformIO") _, [_, arg]) <- unApply tm

113 = ir' env arg

120 = ir' env arg

114 | (P _ (UN "lazy") _, [_, arg]) <- unApply tm

121 | (P _ (UN "lazy") _, [_, arg]) <- unApply tm

@@ -138,10 +145,12 @@ instance ToIR (TT Name) where

138 args' <- mapM (ir' env) args

145 args' <- mapM (ir' env) args

139 return (LApp False f' args')

146 return (LApp False f' args')

140 ir' env (P _ n _) = return $ LV (Glob n)

147 ir' env (P _ n _) = return $ LV (Glob n)

141− ir' env (V i) = return $ LV (Glob (env!!i))

148+ ir' env (V i) | i < length env = return $ LV (Glob (env!!i))

149+ | otherwise = error $ "IR fail " ++ show i ++ " " ++ show tm

142 ir' env (Bind n (Lam _) sc)

150 ir' env (Bind n (Lam _) sc)

151+ = do let n' = uniqueName n env

143− = do sc' <- ir' (n : env) sc

152+ sc' <- ir' (n' : env) sc

144− return $ LLam [n] sc'

153+ return $ LLam [n'] sc'

145 ir' env (Bind n (Let _ v) sc)

154 ir' env (Bind n (Let _ v) sc)

146 = do sc' <- ir' (n : env) sc

155 = do sc' <- ir' (n : env) sc

147 v' <- ir' env v

156 v' <- ir' env v

@@ -163,16 +172,16 @@ instance ToIR (TT Name) where

163 buildApp env e xs = do xs' <- mapM (ir' env) xs

172 buildApp env e xs = do xs' <- mapM (ir' env) xs

164 return $ LApp False e xs'

173 return $ LApp False e xs'

165

174

166−doForeign :: [TT Name] -> Idris LExp

175+ doForeign :: [Name] -> [TT Name] -> Idris LExp

167−doForeign (_ : fgn : args)

176+ doForeign env (_ : fgn : args)

168− | (_, (Constant (Str fgnName) : fgnArgTys : ret : [])) <- unApply fgn

177+ | (_, (Constant (Str fgnName) : fgnArgTys : ret : [])) <- unApply fgn

169− = let tys = getFTypes fgnArgTys

178+ = let tys = getFTypes fgnArgTys

170− rty = mkIty' ret in

179+ rty = mkIty' ret in

171− do args' <- mapM ir args

180+ do args' <- mapM (ir' env) args

172− -- wrap it in a prim__IO

181+ -- wrap it in a prim__IO

173− -- return $ con_ 0 @@ impossible @@

182+ -- return $ con_ 0 @@ impossible @@

174− return $ LLazyExp $ LForeign LANG_C rty fgnName (zip tys args')

183+ return $ LLazyExp $ LForeign LANG_C rty fgnName (zip tys args')

175− | otherwise = fail "Badly formed foreign function call"

184+ | otherwise = fail "Badly formed foreign function call"

176

185

177getFTypes :: TT Name -> [FType]

186getFTypes :: TT Name -> [FType]

178getFTypes tm = case unApply tm of

187getFTypes tm = case unApply tm of

src/IRTS/Defunctionalise.hs+48−3

@@ -1,4 +1,5 @@

1−module IRTS.Defunctionalise where

1+module IRTS.Defunctionalise(module IRTS.Defunctionalise,

2+ module IRTS.Lang) where

3import IRTS.Lang

4import IRTS.Lang

4import Core.TT

5import Core.TT

@@ -137,7 +138,7 @@ mkApplyCase fname n ar

137

138

138mkEval :: [(Name, Int, EvalApply DAlt)] -> (Name, DDecl)

139mkEval :: [(Name, Int, EvalApply DAlt)] -> (Name, DDecl)

139mkEval xs = (MN 0 "EVAL", DFun (MN 0 "EVAL") [MN 0 "arg"]

140mkEval xs = (MN 0 "EVAL", DFun (MN 0 "EVAL") [MN 0 "arg"]

140− (DCase (DV (Glob (MN 0 "arg")))

141+ (mkBigCase (MN 0 "EVAL") 256 (DV (Glob (MN 0 "arg")))

141 (mapMaybe evalCase xs ++

142 (mapMaybe evalCase xs ++

142 [DDefaultCase (DV (Glob (MN 0 "arg")))])))

143 [DDefaultCase (DV (Glob (MN 0 "arg")))])))

143 where

144 where

@@ -146,13 +147,15 @@ mkEval xs = (MN 0 "EVAL", DFun (MN 0 "EVAL") [MN 0 "arg"]

146

147

147mkApply :: [(Name, Int, EvalApply DAlt)] -> (Name, DDecl)

148mkApply :: [(Name, Int, EvalApply DAlt)] -> (Name, DDecl)

148mkApply xs = (MN 0 "APPLY", DFun (MN 0 "APPLY") [MN 0 "fn", MN 0 "arg"]

149mkApply xs = (MN 0 "APPLY", DFun (MN 0 "APPLY") [MN 0 "fn", MN 0 "arg"]

150+ (mkBigCase (MN 0 "APPLY")

149− (DCase (DApp False (MN 0 "EVAL")

151+ 256 (DApp False (MN 0 "EVAL")

150 [DV (Glob (MN 0 "fn"))])

152 [DV (Glob (MN 0 "fn"))])

151 (mapMaybe applyCase xs)))

153 (mapMaybe applyCase xs)))

152 where

154 where

153 applyCase (n, t, ApplyCase x) = Just x

155 applyCase (n, t, ApplyCase x) = Just x

154 applyCase _ = Nothing

156 applyCase _ = Nothing

155

157

158+

156declare :: Int -> [(Name, Int, EvalApply DAlt)] -> [(Name, DDecl)]

159declare :: Int -> [(Name, Int, EvalApply DAlt)] -> [(Name, DDecl)]

157declare t xs = dec' t xs [] where

160declare t xs = dec' t xs [] where

158 dec' t [] acc = reverse acc

161 dec' t [] acc = reverse acc

@@ -189,3 +192,45 @@ instance Show DExp where

189 ++ show' env e

192 ++ show' env e

190 showAlt env (DConstCase c e) = show c ++ " => " ++ show' env e

193 showAlt env (DConstCase c e) = show c ++ " => " ++ show' env e

191 showAlt env (DDefaultCase e) = "_ => " ++ show' env e

194 showAlt env (DDefaultCase e) = "_ => " ++ show' env e

195+

196+-- Divide up a large case expression so that each has a maximum of

197+-- 'max' branches

198+

199+mkBigCase cn max arg branches

200+ | length branches <= max = DCase arg branches

201+ | otherwise = -- DCase arg branches -- until I think of something...

202+ -- divide the branches into groups of at most max (by tag),

203+ -- generate a new case and shrink, recursively

204+ let bs = sortBy tagOrd branches

205+ (all, def) = case (last bs) of

206+ DDefaultCase t -> (init all, Just (DDefaultCase t))

207+ _ -> (all, Nothing)

208+ bss = groupsOf max all

209+ cs = map mkCase bss in

210+ DCase arg branches

211+

212+ where mkCase bs = DCase arg bs

213+

214+ tagOrd (DConCase t _ _ _) (DConCase t' _ _ _) = compare t t'

215+ tagOrd (DConstCase c _) (DConstCase c' _) = compare c c'

216+ tagOrd (DDefaultCase _) (DDefaultCase _) = EQ

217+ tagOrd (DConCase _ _ _ _) (DDefaultCase _) = LT

218+ tagOrd (DConCase _ _ _ _) (DConstCase _ _) = LT

219+ tagOrd (DConstCase _ _) (DDefaultCase _) = LT

220+ tagOrd (DDefaultCase _) (DConCase _ _ _ _) = GT

221+ tagOrd (DConstCase _ _) (DConCase _ _ _ _) = GT

222+ tagOrd (DDefaultCase _) (DConstCase _ _) = GT

223+

224+

225+groupsOf :: Int -> [DAlt] -> [[DAlt]]

226+groupsOf x [] = []

227+groupsOf x xs = let (batch, rest) = span (tagLT (x + tagHead xs)) xs in

228+ batch : groupsOf x rest

229+ where tagHead (DConstCase (I i) _ : _) = i

230+ tagHead (DConCase t _ _ _ : _) = t

231+ tagHead (DDefaultCase _ : _) = -1 -- must be the end

232+

233+ tagLT i (DConstCase (I j) _) = i < j

234+ tagLT i (DConCase j _ _ _) = i < j

235+ tagLT i (DDefaultCase _) = False

236+

src/IRTS/Inliner.hsnew file+9

@@ -0,0 +1,9 @@

1+module IRTS.Inliner where

3+import Core.TT

5+import IRTS.Defunctionalise

7+inline :: DDefs -> DDefs

8+inline xs = xs

src/IRTS/Lang.hs+1−1

@@ -52,7 +52,7 @@ data LAlt = LConCase Int Name [Name] LExp

52 | LDefaultCase LExp

53 deriving (Show, Eq)

55−data LDecl = LFun Name [Name] LExp -- name, arg names, definition

55+data LDecl = LFun Name [Name] LExp -- name, arg names, definition, inlinable

56 | LConstructor Name Int Int -- constructor name, tag, arity

57 deriving (Show, Eq)

src/IRTS/Simplified.hs−1

@@ -1,6 +1,5 @@

1module IRTS.Simplified where

3−import IRTS.Lang

4import IRTS.Defunctionalise

3import IRTS.Defunctionalise

5import Core.TT

4import Core.TT

6import Data.Maybe

5import Data.Maybe

src/Idris/REPL.hs+1−1

@@ -226,7 +226,7 @@ process fn (Search t) = iputStrLn "Not implemented"

226process fn (Spec t) = do (tm, ty) <- elabVal toplevel False t

227 ctxt <- getContext

228 ist <- get

229− let tm' = specialise ctxt [] [] {- (idris_statics ist) -} tm

229+ let tm' = simplify ctxt [] {- (idris_statics ist) -} tm

230 iputStrLn (show (delab ist tm'))

231

232process fn (RmProof n')