ad66486 · Idris-dev · git.iko.soy

git.iko.soy/Idris-dev

Add %specialise annotation for functions (Part 1 of partial evaluation)

%specialise [n1 t1, n2 t2 ...] as an annotation before a function type means that the r.h.s. of all the clauses will be evaluated, but with the name n1 reduced at most t1 times, etc. The t1 part is optional, and means unlimited (which is the default for all names at the minute anyway) e.g. %specialise [interp, fact 1] i_factorial : Int -> Int i_factorial x = interp [] fact x will run the interpreter on fact, ensuring that fact is only unfolded once to avoid infinite evalution. The UK specific spelling is intentional :).

commitad664863679c3a76d460b7a41d6ec212a5e66022 authorEdwin Brady <ecb10@st-andrews.ac.uk> dateThu 25 Jul 2013, 16:56 (13 years ago) parent10c9385

7 files changed+131−62

compare with master

unifiedsplit

idris.cabal+1−1 src/Core/Evaluate.hs+80−49 src/Idris/AbsSyntaxTree.hs+1−1 src/Idris/ElabDecls.hs+22−8 src/Idris/ElabTerm.hs−1 src/Idris/Parser.hs+7−2 src/Idris/PartialEval.hs+20

idris.cabal+1−1

@@ -258,7 +258,7 @@ Executable idris

258258 Idris.Coverage, Idris.IBC, Idris.Unlit,

259259 Idris.DataOpts, Idris.Transforms, Idris.DSL,

260260 Idris.UnusedArgs, Idris.Docs, Idris.Completion,

261− Idris.Providers,

261+ Idris.PartialEval, Idris.Providers,

262262

263263 Util.Pretty, Util.System, Util.DynamicLinker,

264264 Pkg.Package, Pkg.PParser,

src/Core/Evaluate.hs+80−49

@@ -87,7 +87,9 @@ normaliseTrace tr ctxt env t

8787

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

8989specialise ctxt env limits t

90− = evalState (do val <- eval False ctxt limits (map finalEntry env) (finalise t) []

90+ = evalState (do val <- eval False ctxt []

91+ (map finalEntry env) (finalise t)

92+ [Spec]

9193 quote 0 val) (initEval { limited = limits })

9294

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

@@ -125,18 +127,38 @@ unbindEnv :: EnvTT n -> TT n -> TT n

125127unbindEnv [] tm = tm

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

127129

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

129−usable _ _ ns@((MN 0 "STOP", _) : _) = (False, ns)

130−usable True (UN "io_bind") ns = (False, ns)

131−usable s n [] = (True, [])

132−usable s n ns = case lookup n ns of

133− Just 0 -> (False, ns)

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

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

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

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

131+usable _ _ _ ns@((MN 0 "STOP", _) : _) = return (False, ns)

132+usable True _ (UN "io_bind") ns = return (False, ns)

133+usable simpl False n [] = return (True, [])

134+usable simpl True n ns

135+ = do ES ls num <- get

136+ case lookup n ls of

137+ Just 0 -> return (False, ns)

138+ Just i -> return (True, ns)

139+ _ -> return (True, ns)

140+usable simpl False n ns

141+ = case lookup n ns of

142+ Just 0 -> return (False, ns)

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

144+ _ -> if simpl then return $ (True, (n, 0) : filter (\ (n', _) -> n/=n') ns)

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

146+

147+

148+deduct :: Name -> Eval ()

149+deduct n = do ES ls num <- get

150+ case lookup n ls of

151+ Just i -> do put $ ES ((n, (i-1)) :

152+ filter (\ (n', _) -> n/=n') ls) num

153+ _ -> return ()

137154

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

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

157+

158+-- The (Name, Int) pair in the arguments is the maximum depth of unfolding of

159+-- a name. The corresponding pair in the state is the maximum number of

160+-- unfoldings overall.

161+

140162eval :: Bool -> Context -> [(Name, Int)] -> Env -> TT Name ->

141163 [EvalOpt] -> Eval Value

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

@@ -153,23 +175,27 @@ eval traceon ctxt ntimes genv tm opts = ev ntimes [] True [] tm where

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

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

155177 | not top && hnf = liftM (VP Ref n) (ev ntimes stk top env ty)

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

157− = do let val = lookupDefAcc n atRepl ctxt

158− case val of

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

160− ev ntimes (n:stk) True env tm

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

162− return $ VP nt n vty

163− [(CaseOp inl inr _ _ _ [] tree _ _, acc)]

164− | acc == Public || simpl -> -- unoptimised version

165− if canSimplify inl inr n stk

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

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

168− case c of

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

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

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

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

178+ | otherwise

179+ = do (u, ntimes) <- usable simpl spec n ntimes_in

180+ if u then

181+ do let val = lookupDefAcc n atRepl ctxt

182+ case val of

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

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

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

186+ return $ VP nt n vty

187+ [(CaseOp inl inr _ _ _ [] tree _ _, acc)]

188+ | acc == Public || simpl -> -- unoptimised version

189+ if canSimplify inl inr n stk

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

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

192+ case c of

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

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

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

196+ else liftM (VP Ref n) (ev ntimes stk top env ty)

197+ ev ntimes stk top env (P nt n ty)

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

173199 ev ntimes stk top env (V i)

174200 | i < length env && i >= 0 = return $ env !! i

175201 | otherwise = return $ VV i

@@ -228,27 +254,31 @@ eval traceon ctxt ntimes genv tm opts = ev ntimes [] True [] tm where

228254 | not top && hnf = case args of

229255 [] -> return f

230256 _ -> return $ unload env f args

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

232− = traceWhen traceon (show stk) $

233− do let val = lookupDefAcc n atRepl ctxt

234− case val of

235− [(CaseOp inl inr _ _ _ ns tree _ _, acc)]

236− | acc == Public -> -- unoptimised version

237− if canSimplify inl inr n stk

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

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

240− case c of

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

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

243− [(Operator _ i op, _)] ->

244− if (i <= length args)

245− then case op (take i args) of

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

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

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

249− _ -> case args of

250− [] -> return f

251− _ -> return $ unload env f args

257+ | otherwise

258+ = do (u, ntimes) <- usable simpl spec n ntimes_in

259+ if u then

260+ do let val = lookupDefAcc n atRepl ctxt

261+ case val of

262+ [(CaseOp inl inr _ _ _ ns tree _ _, acc)]

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

264+ if canSimplify inl inr n stk

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

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

267+ case c of

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

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

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

271+ if (i <= length args)

272+ then case op (take i args) of

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

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

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

276+ _ -> case args of

277+ [] -> return f

278+ _ -> return $ unload env f args

279+ else case args of

280+ (a : as) -> return $ unload env f (a:as)

281+ [] -> return f

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

253283 apply ntimes stk top env f [] = return f

254284

@@ -264,10 +294,11 @@ eval traceon ctxt ntimes genv tm opts = ev ntimes [] True [] tm where

264294 unload env f [] = f

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

266296

267− evCase ntimes stk top env ns args tree

297+ evCase ntimes n stk top env ns args tree

268298 | length ns <= length args

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

270300 let rest = drop (length ns) args

301+ when spec $ deduct n -- successful, so deduct usages

271302 t <- evTree ntimes stk top env

272303 (zipWith (\n t -> (n, t)) ns args') tree

273304 return (t, rest)

src/Idris/AbsSyntaxTree.hs+1−1

@@ -332,7 +332,7 @@ data FnOpt = Inlinable | TotalFn | PartialFn

332332 | Coinductive | AssertTotal | TCGen

333333 | Implicit -- implicit coercion

334334 | CExport String -- export, with a C name

335− | Specialise [Name] -- specialise it, freeze these names

335+ | Specialise [(Name, Maybe Int)] -- specialise it, freeze these names

336336 deriving (Show, Eq)

337337{-!

338338deriving instance Binary FnOpt

src/Idris/ElabDecls.hs+22−8

@@ -13,6 +13,7 @@ import Idris.Coverage

1313import Idris.DataOpts

1414import Idris.Providers

1515import Idris.Primitives

16+import Idris.PartialEval

1617import IRTS.Lang

1718import Paths_idris

1819

@@ -482,12 +483,13 @@ elabClauses info fc opts n_in cs = let n = liftname info n_in in

482483 putIState (ist { idris_optimisation = opts })

483484 addIBC (IBCOpt n)

484485 ist <- getIState

485− let pats = pats_in

486+ let pats = doTransforms ist pats_in

487+

486488 -- logLvl 3 (showSep "\n" (map (\ (l,r) ->

487489 -- show l ++ " = " ++

488490 -- show r) pats))

489491 let tcase = opt_typecase (idris_options ist)

490− let pdef = map debind $ map (simpl False (tt_ctxt ist)) pats

492+ let pdef = map debind $ map (simpl (tt_ctxt ist)) pats

491493

492494 numArgs <- tclift $ sameLength pdef

493495

@@ -496,10 +498,13 @@ elabClauses info fc opts n_in cs = let n = liftname info n_in in

496498 (take numArgs (repeat Erased)), Erased)]

497499 else stripCollapsed pats

498500

499− logLvl 5 $ "Patterns:\n" ++ show pats

501+ logLvl 5 $ "Patterns:\n" ++ show pats_in

502+ case specNames opts of

503+ Just _ -> logLvl 5 $ "Partially evaluated:\n" ++ show pats

504+ _ -> return ()

500505 logLvl 3 $ "SIMPLIFIED: \n" ++ show pdef

501506

502− let optpdef = map debind $ map (simpl True (tt_ctxt ist)) optpats

507+ let optpdef = map debind $ map (simpl (tt_ctxt ist)) optpats

503508 tree@(CaseDef scargs sc _) <- tclift $

504509 simpleCase tcase False CompileTime fc pdef

505510 cov <- coverage

@@ -600,10 +605,12 @@ elabClauses info fc opts n_in cs = let n = liftname info n_in in

600605

601606 getLHS (_, l, _) = l

602607

603−-- simpl rt ctxt (Right (x, y)) = Right (normalise ctxt [] x,

604−-- simplify ctxt rt [] y)

605− simpl rt ctxt (Right (x, y)) = Right (normalise ctxt [] x, y)

606− simpl rt ctxt t = t

608+ simpl ctxt (Right (x, y)) = Right (normalise ctxt [] x, y)

609+ simpl ctxt t = t

610+

611+ specNames [] = Nothing

612+ specNames (Specialise ns : _) = Just ns

613+ specNames (_ : xs) = specNames xs

607614

608615 sameLength ((_, x, _) : xs)

609616 = do l <- sameLength xs

@@ -612,6 +619,13 @@ elabClauses info fc opts n_in cs = let n = liftname info n_in in

612619 else tfail (At fc (Msg "Clauses have differing numbers of arguments "))

613620 sameLength [] = return 0

614621

622+ -- apply all transformations (just specialisation for now, add

623+ -- user defined transformation rules later)

624+ doTransforms ist pats =

625+ case specNames opts of

626+ Nothing -> pats

627+ Just ns -> partial_eval (tt_ctxt ist) ns pats

628+

615629elabVal :: ElabInfo -> Bool -> PTerm -> Idris (Term, Type)

616630elabVal info aspat tm_in

617631 = do ctxt <- getContext

src/Idris/ElabTerm.hs−1

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

470470 elab' ina (PMetavar cname')

471471 let newdef = PClauses fc [] cname'

472472 (caseBlock fc cname' (reverse args) opts)

473− -- fail $ "Not implemented " ++ show c ++ "\n" ++ show args

474473 -- elaborate case

475474 env <- get_env

476475 g <- goal

src/Idris/Parser.hs+7−2

@@ -711,12 +711,17 @@ pFnOpts opts

711711 <|> do reserved "partial"; pFnOpts (PartialFn : (opts \\ [TotalFn]))

712712 <|> try (do lchar '%'; reserved "export"; c <- strlit;

713713 pFnOpts (CExport c : opts))

714− <|> do lchar '%'; reserved "assert_total"; pFnOpts (AssertTotal : opts)

714+ <|> try (do lchar '%'; reserved "assert_total";

715+ pFnOpts (AssertTotal : opts))

715716 <|> do lchar '%'; reserved "specialise";

716− lchar '['; ns <- sepBy pfName (lchar ','); lchar ']'

717+ lchar '['; ns <- sepBy nameTimes (lchar ','); lchar ']'

717718 pFnOpts (Specialise ns : opts)

718719 <|> do reserved "implicit"; pFnOpts (Implicit : opts)

719720 <|> return opts

721+ where nameTimes = do n <- pfName

722+ t <- option Nothing (do reds <- natural

723+ return (Just (fromInteger reds)))

724+ return (n, t)

720725

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

722727addAcc n a = do i <- getState

src/Idris/PartialEval.hsnew file+20

@@ -0,0 +1,20 @@

1+module Idris.PartialEval(partial_eval) where

3+import Idris.AbsSyntax

5+import Core.TT

6+import Core.Evaluate

8+import Debug.Trace

10+partial_eval :: Context -> [(Name, Maybe Int)] ->

11+ [Either Term (Term, Term)] ->

12+ [Either Term (Term, Term)]

13+partial_eval ctxt ns tms = map peClause tms where

14+ peClause (Left t) = Left t

15+ peClause (Right (lhs, rhs))

16+ = let rhs' = specialise ctxt [] (map toLimit ns) rhs in

17+ Right (lhs, rhs')

18+

19+ toLimit (n, Nothing) = (n, 65536) -- somewhat arbitrary reduction limit

20+ toLimit (n, Just l) = (n, l)