ad66486 · Idris-dev · git.iko.soy

git.iko.soy/Idris-dev

on master help sign in

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

ad66486Edwin Brady13 years ago

idris.cabal+1−1

compare with master

unifiedsplit

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

258 Idris.Coverage, Idris.IBC, Idris.Unlit,

259 Idris.DataOpts, Idris.Transforms, Idris.DSL,

260 Idris.UnusedArgs, Idris.Docs, Idris.Completion,

261− Idris.Providers,

261+ Idris.PartialEval, Idris.Providers,

262

263 Util.Pretty, Util.System, Util.DynamicLinker,

264 Pkg.Package, Pkg.PParser,

src/Core/Evaluate.hs+80−49

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

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

89specialise 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]

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

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

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

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

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

125unbindEnv [] tm = tm

127unbindEnv [] tm = tm

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

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

127

129

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

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

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

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

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

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

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

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

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

141+ = case lookup n ns of

133− Just 0 -> (False, ns)

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

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

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

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

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

136− else (True, (n, 100) : 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 ()

137

154

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

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

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

156-- 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+

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

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

141 [EvalOpt] -> Eval Value

163 [EvalOpt] -> Eval Value

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

164eval 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

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

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

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

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

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

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

178+ | otherwise

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

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

180+ if u then

157− = do let val = lookupDefAcc n atRepl ctxt

181+ do let val = lookupDefAcc n atRepl ctxt

158− case val of

182+ case val of

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

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

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

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

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

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

162− return $ VP nt n vty

186+ return $ VP nt n vty

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

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

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

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

165− if canSimplify inl inr n stk

189+ if canSimplify inl inr n stk

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

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

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

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

168− case c of

192+ case c of

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

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

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

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

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

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)

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

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

173 ev ntimes stk top env (V i)

199 ev ntimes stk top env (V i)

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

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

175 | otherwise = return $ VV i

201 | otherwise = return $ VV i

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

228 | not top && hnf = case args of

254 | not top && hnf = case args of

229 [] -> return f

255 [] -> return f

230 _ -> return $ unload env f args

256 _ -> return $ unload env f args

257+ | otherwise

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

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

232− = traceWhen traceon (show stk) $

259+ if u then

233− do let val = lookupDefAcc n atRepl ctxt

260+ do let val = lookupDefAcc n atRepl ctxt

234− case val of

261+ case val of

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

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

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

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

237− if canSimplify inl inr n stk

264+ if canSimplify inl inr n stk

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

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

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

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

240− case c of

267+ case c of

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

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

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

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

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

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

244− if (i <= length args)

271+ if (i <= length args)

245− then case op (take i args) of

272+ then case op (take i args) of

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

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

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

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

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

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

249− _ -> case args of

276+ _ -> case args of

250− [] -> return f

277+ [] -> return f

251− _ -> return $ unload env f args

278+ _ -> return $ unload env f args

279+ else case args of

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

281+ [] -> return f

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

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

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

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

254

284

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

264 unload env f [] = f

294 unload env f [] = f

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

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

266

296

267− evCase ntimes stk top env ns args tree

297+ evCase ntimes n stk top env ns args tree

268 | length ns <= length args

298 | length ns <= length args

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

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

270 let rest = drop (length ns) args

300 let rest = drop (length ns) args

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

271 t <- evTree ntimes stk top env

302 t <- evTree ntimes stk top env

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

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

273 return (t, rest)

304 return (t, rest)

src/Idris/AbsSyntaxTree.hs+1−1

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

332 | Coinductive | AssertTotal | TCGen

333 | Implicit -- implicit coercion

334 | 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

336 deriving (Show, Eq)

337{-!

338deriving instance Binary FnOpt

src/Idris/ElabDecls.hs+22−8

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

13import Idris.DataOpts

14import Idris.Providers

15import Idris.Primitives

16+import Idris.PartialEval

16import IRTS.Lang

17import IRTS.Lang

17import Paths_idris

18import Paths_idris

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

482 putIState (ist { idris_optimisation = opts })

483 putIState (ist { idris_optimisation = opts })

483 addIBC (IBCOpt n)

484 addIBC (IBCOpt n)

484 ist <- getIState

485 ist <- getIState

485− let pats = pats_in

486+ let pats = doTransforms ist pats_in

487+

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

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

487 -- show l ++ " = " ++

489 -- show l ++ " = " ++

488 -- show r) pats))

490 -- show r) pats))

489 let tcase = opt_typecase (idris_options ist)

491 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

491

493

492 numArgs <- tclift $ sameLength pdef

494 numArgs <- tclift $ sameLength pdef

493

495

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

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

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

497 else stripCollapsed pats

499 else stripCollapsed pats

498

500

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 ()

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

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

501

506

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

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

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

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

504 simpleCase tcase False CompileTime fc pdef

509 simpleCase tcase False CompileTime fc pdef

505 cov <- coverage

510 cov <- coverage

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

600

605

601 getLHS (_, l, _) = l

606 getLHS (_, l, _) = l

602

607

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

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

604−-- simplify ctxt rt [] y)

609+ simpl ctxt t = t

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

610+

606− simpl rt ctxt t = t

611+ specNames [] = Nothing

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

613+ specNames (_ : xs) = specNames xs

607

614

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

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

609 = do l <- sameLength xs

616 = do l <- sameLength xs

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

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

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

613 sameLength [] = return 0

620 sameLength [] = return 0

614

621

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+

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

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

616elabVal info aspat tm_in

630elabVal info aspat tm_in

617 = do ctxt <- getContext

631 = do ctxt <- getContext

src/Idris/ElabTerm.hs−1

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

470 elab' ina (PMetavar cname')

471 let newdef = PClauses fc [] cname'

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

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

474 -- elaborate case

473 -- elaborate case

475 env <- get_env

474 env <- get_env

476 g <- goal

475 g <- goal

src/Idris/Parser.hs+7−2

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

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

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

713 pFnOpts (CExport c : opts))

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

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

715+ pFnOpts (AssertTotal : opts))

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

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

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

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

717 pFnOpts (Specialise ns : opts)

718 pFnOpts (Specialise ns : opts)

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

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

719 <|> return opts

720 <|> return opts

721+ where nameTimes = do n <- pfName

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

723+ return (Just (fromInteger reds)))

724+ return (n, t)

720

725

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

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

722addAcc n a = do i <- getState

727addAcc 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)