4bcfa68 · Idris-dev · git.iko.soy

git.iko.soy/Idris-dev

Tinker with specialisation

commit4bcfa68d1d9d5fa99a9ccec927124c8d6170e082 authorEdwin Brady <eb@cs.st-andrews.ac.uk> dateMon 6 Feb 2012, 12:28 (15 years ago) parent09f2abd

8 files changed+177−113

compare with master

unifiedsplit

src/Core/Evaluate.hs+121−97 src/Core/ProofState.hs+1−1 src/Idris/AbsSyntax.hs+2−1 src/Idris/ElabDecls.hs+2−2 src/Idris/ElabTerm.hs+42−11 src/Idris/IBC.hs+4 src/Idris/Parser.hs+4 src/Idris/REPL.hs+1−1

src/Core/Evaluate.hs+121−97

@@ -19,12 +19,15 @@ import Data.Binary hiding (get, put)

1919import Core.TT

2020import Core.CaseTree

2121

22−type EvalState = ()

22+data EvalState = ES { limited :: [(Name, Int)],

23+ steps :: Int }

2324type Eval a = State EvalState a

2425

2526data EvalOpt = Spec | HNF | Simplify | AtREPL

2627 deriving (Show, Eq)

2728

29+initEval = ES [] 0

30+

2831-- VALUES (as HOAS) ---------------------------------------------------------

2932

3033data Value = VP NameType Name Value

@@ -46,7 +49,7 @@ data HNF = HP NameType Name (TT Name)

4649 deriving Show

4750

4851instance Show Value where

49− show x = show $ evalState (quote 100 x) ()

52+ show x = show $ evalState (quote 100 x) initEval

5053

5154instance Show (a -> b) where

5255 show x = "<<fn>>"

@@ -60,36 +63,36 @@ instance Show (a -> b) where

6063

6164normaliseC :: Context -> Env -> TT Name -> TT Name

6265normaliseC ctxt env t

63− = evalState (do val <- eval ctxt emptyContext env t []

64− quote 0 val) ()

66+ = evalState (do val <- eval ctxt [] env t []

67+ quote 0 val) initEval

6568

6669normaliseAll :: Context -> Env -> TT Name -> TT Name

6770normaliseAll ctxt env t

68− = evalState (do val <- eval ctxt emptyContext env t [AtREPL]

69− quote 0 val) ()

71+ = evalState (do val <- eval ctxt [] env t [AtREPL]

72+ quote 0 val) initEval

7073

7174normalise :: Context -> Env -> TT Name -> TT Name

7275normalise ctxt env t

73− = evalState (do val <- eval ctxt emptyContext (map finalEntry env) (finalise t) []

74− quote 0 val) ()

76+ = evalState (do val <- eval ctxt [] (map finalEntry env) (finalise t) []

77+ quote 0 val) initEval

7578

76−specialise :: Context -> Ctxt [Bool] -> TT Name -> TT Name

77−specialise ctxt statics t

78− = evalState (do val <- eval ctxt statics [] (finalise t) [Spec]

79− quote 0 val) ()

79+specialise :: Context -> Env -> [(Name, Int)] -> TT Name -> TT Name

80+specialise ctxt env limits t

81+ = evalState (do val <- eval ctxt limits (map finalEntry env) (finalise t) []

82+ quote 0 val) (initEval { limited = limits })

8083

8184-- Like normalise, but we only reduce functions that are marked as okay to

8285-- inline (and probably shouldn't reduce lets?)

8386

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

8588simplify ctxt env t

86− = evalState (do val <- eval ctxt emptyContext (map finalEntry env) (finalise t) [Simplify]

87− quote 0 val) ()

89+ = evalState (do val <- eval ctxt [] (map finalEntry env) (finalise t) [Simplify]

90+ quote 0 val) initEval

8891

8992hnf :: Context -> Env -> TT Name -> TT Name

9093hnf ctxt env t

91− = evalState (do val <- eval ctxt emptyContext (map finalEntry env) (finalise t) [HNF]

92− quote 0 val) ()

94+ = evalState (do val <- eval ctxt [] (map finalEntry env) (finalise t) [HNF]

95+ quote 0 val) initEval

9396

9497

9598-- unbindEnv env (quote 0 (eval ctxt (bindEnv env t)))

@@ -106,120 +109,141 @@ unbindEnv :: EnvTT n -> TT n -> TT n

106109unbindEnv [] tm = tm

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

108111

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

113+usable n [] = (True, [])

114+usable n ns = case lookup n ns of

115+ Just 0 -> (False, ns)

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

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

118+

119+reduction :: Eval ()

120+reduction = do ES ns s <- get

121+ put (ES ns (s+1))

122+

109123-- Evaluate in a context of locally named things (i.e. not de Bruijn indexed,

110124-- such as we might have during construction of a proof)

111125

112−eval :: Context -> Ctxt [Bool] -> Env -> TT Name -> [EvalOpt] -> Eval Value

113−eval ctxt statics genv tm opts = ev [] True [] tm where

126+eval :: Context -> [(Name, Int)] -> Env -> TT Name -> [EvalOpt] -> Eval Value

127+eval ctxt ntimes genv tm opts = ev ntimes [] True [] tm where

114128 spec = Spec `elem` opts

115129 simpl = Simplify `elem` opts

116130 atRepl = AtREPL `elem` opts

117131

118− ev stk top env (P _ n ty)

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

120− ev stk top env (P Ref n ty) = case lookupDefAcc Nothing n atRepl ctxt of

121− [(Function _ tm, Public)] ->

122− ev (n:stk) True env tm

123− [(TyDecl nt ty, _)] -> do vty <- ev stk True env ty

124− return $ VP nt n vty

125− [(CaseOp inl _ _ [] tree _ _, Public)] -> -- unoptimised version

126− if simpl && (not inl || elem n stk)

127− then liftM (VP Ref n) (ev stk top env ty)

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

129− case c of

130− (Nothing, _) -> liftM (VP Ref n) (ev stk top env ty)

131− (Just v, _) -> return v

132− _ -> liftM (VP Ref n) (ev stk top env ty)

133− ev stk top env (P nt n ty) = liftM (VP nt n) (ev stk top env ty)

134− ev stk top env (V i) | i < length env = return $ env !! i

132+ ev ntimes stk top env (P _ n ty)

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

134+ ev ntimes_in stk top env (P Ref n ty)

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

136+ = do let val = lookupDefAcc Nothing n atRepl ctxt

137+ case val of

138+ [(Function _ tm, Public)] ->

139+ ev ntimes (n:stk) True env tm

140+ [(TyDecl nt ty, _)] -> do vty <- ev ntimes stk True env ty

141+ return $ VP nt n vty

142+ [(CaseOp inl _ _ [] tree _ _, Public)] -> -- unoptimised version

143+ if simpl && (not inl || elem n stk)

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

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

146+ case c of

147+ (Nothing, _) -> liftM (VP Ref n) (ev ntimes stk top env ty)

148+ (Just v, _) -> return v

149+ _ -> liftM (VP Ref n) (ev ntimes stk top env ty)

150+ ev ntimes stk top env (P nt n ty) = liftM (VP nt n) (ev ntimes stk top env ty)

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

135152 | otherwise = return $ VV i

136− ev stk top env (Bind n (Let t v) sc)

137− = do v' <- ev stk top env v --(finalise v)

138− sc' <- ev stk top (v' : env) sc

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

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

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

139156 wknV (-1) sc'

140− ev stk top env (Bind n (NLet t v) sc)

141− = do t' <- ev stk top env (finalise t)

142− v' <- ev stk top env (finalise v)

143− sc' <- ev stk top (v' : env) sc

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

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

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

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

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

145− ev stk top env (Bind n b sc)

162+ ev ntimes stk top env (Bind n b sc)

146163 = do b' <- vbind env b

147− return $ VBind n b' (\x -> ev stk top (x:env) sc)

148− where vbind env t = fmapMB (\tm -> ev stk top env (finalise tm)) t

149− ev stk top env (App f a) = do f' <- ev stk top env f

150− a' <- ev stk False env a

151− evApply stk top env [a'] f'

152− ev stk top env (Constant c) = return $ VConstant c

153− ev stk top env Erased = return VErased

154− ev stk top env (Set i) = return $ VSet i

164+ return $ VBind n b' (\x -> ev ntimes stk top (x:env) sc)

165+ where vbind env t = fmapMB (\tm -> ev ntimes stk top env (finalise tm)) t

166+ ev ntimes stk top env (App f a)

167+ = do f' <- ev ntimes stk top env f

168+ a' <- ev ntimes stk False env a

169+ evApply ntimes stk top env [a'] f'

170+ ev ntimes stk top env (Constant c) = return $ VConstant c

171+ ev ntimes stk top env Erased = return VErased

172+ ev ntimes stk top env (Set i) = return $ VSet i

155173

156− evApply stk top env args (VApp f a) =

157− evApply stk top env (a:args) f

158− evApply stk top env args f = apply stk top env f args

174+ evApply ntimes stk top env args (VApp f a) =

175+ evApply ntimes stk top env (a:args) f

176+ evApply ntimes stk top env args f = apply ntimes stk top env f args

159177

160− apply stk top env (VBind n (Lam t) sc) (a:as)

178+ apply ntimes stk top env (VBind n (Lam t) sc) (a:as)

161179 = do a' <- sc a

162− app <- apply stk top env a' as

180+ app <- apply ntimes stk top env a' as

163181 wknV (-1) app

164− apply stk False env f args

165− | spec = specApply stk env f args

166− apply stk top env (VP Ref n ty) args

167− | [(CaseOp inl _ _ ns tree _ _, Public)] <- lookupDefAcc Nothing n atRepl ctxt

168− = -- traceWhen (n == UN ["interp"]) (show (n, args)) $

169− if simpl && (not inl || elem n stk)

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

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

172− case c of

173− (Nothing, _) -> return $ unload env (VP Ref n ty) args

174− (Just v, rest) -> evApply stk top env rest v

175− | [Operator _ i op] <- lookupDef Nothing n ctxt

176− = if (i <= length args)

177− then case op (take i args) of

178− Nothing -> return $ unload env (VP Ref n ty) args

179− Just v -> evApply stk top env (drop i args) v

180− else return $ unload env (VP Ref n ty) args

181− apply stk top env f (a:as) = return $ unload env f (a:as)

182− apply stk top env f [] = return f

183−

184− specApply stk env f@(VP Ref n ty) args

185− = case lookupCtxt Nothing n statics of

186− [as] -> if or as

187− then trace (show (n, map fst (filter (\ (_, s) -> s) (zip args as)))) $

188− return $ unload env f args

189− else return $ unload env f args

190− _ -> return $ unload env f args

191− specApply stk env f args = return $ unload env f args

182+-- apply ntimes stk False env f args

183+-- | spec = specApply ntimes stk env f args

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

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

186+ = do let val = lookupDefAcc Nothing n atRepl ctxt

187+ case val of

188+ [(CaseOp inl _ _ ns tree _ _, Public)] ->

189+ if simpl && (not inl || elem n stk)

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

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

192+ case c of

193+ (Nothing, _) -> return $ unload env (VP Ref n ty) args

194+ (Just v, rest) -> evApply ntimes stk top env rest v

195+ [(Operator _ i op, _)] ->

196+ if (i <= length args)

197+ then case op (take i args) of

198+ Nothing -> return $ unload env (VP Ref n ty) args

199+ Just v -> evApply ntimes stk top env (drop i args) v

200+ else return $ unload env (VP Ref n ty) args

201+ _ -> case args of

202+ [] -> return f

203+ _ -> return $ unload env f args

204+ apply ntimes stk top env f (a:as) = return $ unload env f (a:as)

205+ apply ntimes stk top env f [] = return f

206+

207+-- specApply stk env f@(VP Ref n ty) args

208+-- = case lookupCtxt Nothing n statics of

209+-- [as] -> if or as

210+-- then trace (show (n, map fst (filter (\ (_, s) -> s) (zip args as)))) $

211+-- return $ unload env f args

212+-- else return $ unload env f args

213+-- _ -> return $ unload env f args

214+-- specApply stk env f args = return $ unload env f args

192215

193216 unload env f [] = f

194217 unload env f (a:as) = unload env (VApp f a) as

195218

196− evCase stk top env ns args tree

219+ evCase ntimes stk top env ns args tree

197220 | length ns <= length args

198221 = do let args' = take (length ns) args

199222 let rest = drop (length ns) args

200− t <- evTree stk top env (zipWith (\n t -> (n, t)) ns args') tree

223+ t <- evTree ntimes stk top env (zipWith (\n t -> (n, t)) ns args') tree

201224 return (t, rest)

202225 | otherwise = return (Nothing, args)

203226

204− evTree :: [Name] -> Bool -> [Value] -> [(Name, Value)] -> SC -> Eval (Maybe Value)

205− evTree stk top env amap (UnmatchedCase str) = return Nothing

206− evTree stk top env amap (STerm tm)

227+ evTree :: [(Name, Int)] -> [Name] -> Bool ->

228+ [Value] -> [(Name, Value)] -> SC -> Eval (Maybe Value)

229+ evTree ntimes stk top env amap (UnmatchedCase str) = return Nothing

230+ evTree ntimes stk top env amap (STerm tm)

207231 = do let etm = pToVs (map fst amap) tm

208− etm' <- ev stk top (map snd amap ++ env) etm

232+ etm' <- ev ntimes stk top (map snd amap ++ env) etm

209233 return $ Just etm'

210− evTree stk top env amap (Case n alts)

234+ evTree ntimes stk top env amap (Case n alts)

211235 = case lookup n amap of

212236 Just v -> do c <- chooseAlt env v (getValArgs v) alts amap

213237 case c of

214− Just (altmap, sc) -> evTree stk top env altmap sc

215− _ -> do c' <- chooseAlt' stk env v (getValArgs v) alts amap

238+ Just (altmap, sc) -> evTree ntimes stk top env altmap sc

239+ _ -> do c' <- chooseAlt' ntimes stk env v (getValArgs v) alts amap

216240 case c' of

217− Just (altmap, sc) -> evTree stk top env altmap sc

241+ Just (altmap, sc) -> evTree ntimes stk top env altmap sc

218242 _ -> return Nothing

219243 _ -> return Nothing

220244

221− chooseAlt' stk env _ (f, args) alts amap

222− = do f' <- apply stk True env f args

245+ chooseAlt' ntimes stk env _ (f, args) alts amap

246+ = do f' <- apply ntimes stk True env f args

223247 chooseAlt env f' (getValArgs f') alts amap

224248

225249 chooseAlt :: [Value] -> Value -> (Value, [Value]) -> [CaseAlt] -> [(Name, Value)] ->

@@ -571,7 +595,7 @@ initContext = MkContext [] 0 emptyContext

571595ctxtAlist :: Context -> [(Name, Def)]

572596ctxtAlist ctxt = map (\(n, (d, a, t)) -> (n, d)) $ toAlist (definitions ctxt)

573597

574−veval ctxt env t = evalState (eval ctxt emptyContext env t []) ()

598+veval ctxt env t = evalState (eval ctxt [] env t []) initEval

575599

576600addToCtxt :: Name -> Term -> Type -> Context -> Context

577601addToCtxt n tm ty uctxt

src/Core/ProofState.hs+1−1

@@ -284,7 +284,7 @@ fill _ _ _ _ = fail "Can't fill here."

284284

285285prep_fill :: Name -> [Name] -> RunTactic

286286prep_fill f as ctxt env (Bind x (Hole ty) sc) =

287− do let val = mkApp (P Ref f undefined) (map (\n -> P Ref n undefined) as)

287+ do let val = mkApp (P Ref f Erased) (map (\n -> P Ref n Erased) as)

288288 return $ Bind x (Guess ty val) sc

289289prep_fill f as ctxt env t = fail $ "Can't prepare fill at " ++ show t

290290

src/Idris/AbsSyntax.hs+2−1

@@ -404,6 +404,7 @@ constraint = Constraint False Dynamic

404404tacimpl = TacImp False Dynamic

405405

406406data FnOpt = Inlinable | TotalFn | AssertTotal | TCGen

407+ | Specialise [Name] -- specialise it, freeze these names

407408 deriving (Show, Eq)

408409{-!

409410deriving instance Binary FnOpt

@@ -752,7 +753,7 @@ getAll = map getTm

752753showImp :: Bool -> PTerm -> String

753754showImp impl tm = se 10 tm where

754755 se p (PQuote r) = "![" ++ show r ++ "]"

755− se p (PRef fc n) = if impl then show n ++ "[" ++ show fc ++ "]"

756+ se p (PRef fc n) = if impl then show n -- ++ "[" ++ show fc ++ "]"

756757 else showbasic n

757758 where showbasic n@(UN _) = show n

758759 showbasic (MN _ s) = s

src/Idris/ElabDecls.hs+2−2

@@ -293,8 +293,8 @@ elabClauses info fc opts n_in cs = let n = liftname info n_in in

293293 when (tot /= Unchecked) $ addIBC (IBCTotal n tot)

294294 i <- get

295295 case lookupDef Nothing n (tt_ctxt i) of

296− (CaseOp _ _ _ _ sc _ _ : _) ->

297− do let ns = namesUsed sc

296+ (CaseOp _ _ _ scargs sc _ _ : _) ->

297+ do let ns = namesUsed sc \\ scargs

298298 logLvl 2 $ "Called names: " ++ show ns

299299 addToCG n ns

300300 addIBC (IBCCG n)

src/Idris/ElabTerm.hs+42−11

@@ -210,11 +210,11 @@ elab ist info pattern tcgen fn tm

210210-- | [d] <- lookupCtxt Nothing dsl (idris_dsls ist)

211211-- = let dsl' = expandDo d (getTm arg) in

212212-- trace (show dsl') $ elab' ina dsl'

213− elab' (ina, g) (PApp fc (PRef _ f) args')

213+ elab' (ina, g) tm@(PApp fc (PRef _ f) args')

214214 = do let args = {- case lookupCtxt f (inblock info) of

215215 Just ps -> (map (pexp . (PRef fc)) ps ++ args')

216216 _ ->-} args'

217− mkSpecialised ist fc f (map getTm args')

217+-- newtm <- mkSpecialised ist fc f (map getTm args') tm

218218 ivs <- get_instances

219219 -- HACK: we shouldn't resolve type classes if we're defining an instance

220220 -- function or default definition.

@@ -222,7 +222,6 @@ elab ist info pattern tcgen fn tm

222222 ctxt <- get_context

223223 let guarded = isConName Nothing f ctxt

224224 try (do ns <- apply (Var f) (map isph args)

225− solve

226225 let (ns', eargs)

227226 = unzip $

228227 sortBy (\(_,x) (_,y) -> compare (priority x) (priority y))

@@ -231,8 +230,11 @@ elab ist info pattern tcgen fn tm

231230 [] False ns' (map (\x -> (lazyarg x, getTm x)) eargs))

232231 (elabArgs (ina || not isinf, guarded)

233232 [] False (reverse ns')

234− (map (\x -> (lazyarg x, getTm x)) (reverse eargs))))

233+ (map (\x -> (lazyarg x, getTm x)) (reverse eargs)))

234+ mkSpecialised ist fc f (map getTm args') tm

235+ solve)

235236 (do apply_elab f (map (toElab (ina || not isinf, guarded)) args)

237+ mkSpecialised ist fc f (map getTm args') tm

236238 solve)

237239 ivs' <- get_instances

238240 when (not pattern || (ina && not tcgen)) $

@@ -503,11 +505,40 @@ solveAll = try (do solve; solveAll) (return ())

503505-- top level function by normalising the application

504506-- and elaborating the new expression.

505507

506−mkSpecialised :: IState -> FC -> Name -> [PTerm] -> ElabD ()

507−mkSpecialised i fc n args

508− = case lookupCtxt Nothing n (idris_statics i) of

509− [] -> return ()

510− [as] -> if (not (or as)) then return () else

511− do return () -- trace (show (n, args)) $ return ()

512−

508+mkSpecialised :: IState -> FC -> Name -> [PTerm] -> PTerm -> ElabD PTerm

509+mkSpecialised i fc n args def

510+ = do let tm' = def

511+ case lookupCtxt Nothing n (idris_statics i) of

512+ [] -> return tm'

513+ [as] -> if (not (or as)) then return tm' else

514+ mkSpecDecl i n (zip args as) tm'

515+

516+mkSpecDecl :: IState -> Name -> [(PTerm, Bool)] -> PTerm -> ElabD PTerm

517+mkSpecDecl i n pargs tm'

518+ = do t <- goal

519+ g <- get_guess

520+ let (f, args) = unApply g

521+ let sargs = zip args (map snd pargs)

522+ let staticArgs = map fst (filter (\ (_,x) -> x) sargs)

523+ let ns = group (sort (concatMap staticFnNames staticArgs))

524+ let ntimes = map (\xs -> (head xs, length xs - 1)) ns

525+ if (not (null ns)) then

526+ do env <- get_env

527+ let g' = g -- specialise ctxt env ntimes g

528+ return tm'

529+-- trace (show t ++ "\n" ++

530+-- show ntimes ++ "\n" ++

531+-- show (delab i g) ++ "\n" ++ show (delab i g')) $ return tm' -- TODO

532+ else return tm'

533+ where

534+ ctxt = tt_ctxt i

535+ cg = idris_callgraph i

536+

537+ staticFnNames tm | (P _ f _, as) <- unApply tm

538+ = if not (isFnName Nothing f ctxt) then []

539+ else case lookupCtxt Nothing f cg of

540+ [ns] -> f : f : [] --(ns \\ [f])

541+ [] -> [f,f]

542+ _ -> []

543+ staticFnNames _ = []

513544

src/Idris/IBC.hs+4

@@ -704,6 +704,8 @@ instance Binary FnOpt where

704704 TotalFn -> putWord8 1

705705 TCGen -> putWord8 2

706706 AssertTotal -> putWord8 3

707+ Specialise x -> do putWord8 4

708+ put x

707709 get

708710 = do i <- getWord8

709711 case i of

@@ -711,6 +713,8 @@ instance Binary FnOpt where

711713 1 -> return TotalFn

712714 2 -> return TCGen

713715 3 -> return AssertTotal

716+ 4 -> do x <- get

717+ return (Specialise x)

714718 _ -> error "Corrupted binary data for FnOpt"

715719

716720instance Binary Fixity where

src/Idris/Parser.hs+4

@@ -615,6 +615,10 @@ pAccessibility

615615pFnOpts :: IParser [FnOpt]

616616pFnOpts = do reserved "total"; xs <- pFnOpts; return (TotalFn : xs)

617617 <|> do lchar '%'; reserved "assert_total"; xs <- pFnOpts; return (AssertTotal : xs)

618+ <|> do lchar '%'; reserved "specialise";

619+ lchar '['; ns <- sepBy pfName (lchar ','); lchar ']'

620+ xs <- pFnOpts

621+ return (Specialise ns : xs)

618622 <|> return []

619623

620624addAcc :: Name -> Maybe Accessibility -> IParser ()

src/Idris/REPL.hs+1−1

@@ -195,7 +195,7 @@ process fn (Info n) = do i <- get

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

196196 ctxt <- getContext

197197 ist <- get

198− let tm' = specialise ctxt (idris_statics ist) tm

198+ let tm' = specialise ctxt [] [] {- (idris_statics ist) -} tm

199199 iputStrLn (show (delab ist tm'))

200200process fn (Prove n) = do prover (lit fn) n

201201 -- recheck totality