81425d2 · Idris-dev · git.iko.soy

git.iko.soy/Idris-dev

Add skeleton of inliner

commit81425d257ae17a11c52720620c84d58286ea6eac authorEdwin Brady <ecb10@st-andrews.ac.uk> dateThu 5 Sep 2013, 13:36 (13 years ago) parent1931074

7 files changed+50−15

compare with master

unifiedsplit

idris.cabal+1 src/Core/Evaluate.hs+8−1 src/Core/Execute.hs+4−4 src/Idris/ElabDecls.hs+12−4 src/Idris/IBC.hs+7−6 src/Idris/Inliner.hs+17 src/Idris/Prover.hs+1

idris.cabal+1

@@ -259,6 +259,7 @@ Executable idris

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

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

261261 Idris.PartialEval, Idris.Providers, Idris.Chaser,

262+ Idris.Inliner,

262263

263264 Util.Pretty, Util.System, Util.DynamicLinker,

264265 Pkg.Package, Pkg.PParser,

src/Core/Evaluate.hs+8−1

@@ -529,6 +529,7 @@ data Def = Function Type Term

529529data CaseDefs = CaseDefs {

530530 cases_totcheck :: ([Name], SC),

531531 cases_compiletime :: ([Name], SC),

532+ cases_inlined :: ([Name], SC),

532533 cases_runtime :: ([Name], SC)

533534 }

534535

@@ -676,31 +677,37 @@ addCasedef :: Name -> CaseInfo -> Bool -> Bool -> Bool -> Bool ->

676677 [Either Term (Term, Term)] ->

677678 [([Name], Term, Term)] -> -- totality

678679 [([Name], Term, Term)] -> -- compile time

680+ [([Name], Term, Term)] -> -- inlined

679681 [([Name], Term, Term)] -> -- run time

680682 Type -> Context -> Context

681683addCasedef n ci@(CaseInfo alwaysInline tcdict)

682− tcase covering reflect asserted ps_in ps_tot ps_ct ps_rt ty uctxt

684+ tcase covering reflect asserted ps_in

685+ ps_tot ps_inl ps_ct ps_rt ty uctxt

683686 = let ctxt = definitions uctxt

684687 access = case lookupDefAcc n False uctxt of

685688 [(_, acc)] -> acc

686689 _ -> Public

687690 ctxt' = case (simpleCase tcase covering reflect CompileTime (FC "" 0) ps_tot,

688691 simpleCase tcase covering reflect CompileTime (FC "" 0) ps_ct,

692+ simpleCase tcase covering reflect CompileTime (FC "" 0) ps_inl,

689693 simpleCase tcase covering reflect RunTime (FC "" 0) ps_rt) of

690694 (OK (CaseDef args_tot sc_tot _),

691695 OK (CaseDef args_ct sc_ct _),

696+ OK (CaseDef args_inl sc_inl _),

692697 OK (CaseDef args_rt sc_rt _)) ->

693698 let inl = alwaysInline -- || tcdict

694699 inlc = (inl || small n args_ct sc_ct) && (not asserted)

695700 inlr = inl || small n args_rt sc_rt

696701 cdef = CaseDefs (args_tot, sc_tot)

697702 (args_ct, sc_ct)

703+ (args_inl, sc_inl)

698704 (args_rt, sc_rt) in

699705 addDef n (CaseOp (ci { case_inlinable = inlc })

700706 ty ps_in ps_tot cdef,

701707 access, Unchecked) ctxt in

702708 uctxt { definitions = ctxt' }

703709

710+-- simplify a definition for totality checking

704711simplifyCasedef :: Name -> Context -> Context

705712simplifyCasedef n uctxt

706713 = let ctxt = definitions uctxt

src/Core/Execute.hs+4−4

@@ -181,9 +181,9 @@ doExec env ctxt p@(P Ref n ty) =

181181 [Function _ tm] -> doExec env ctxt tm

182182 [TyDecl _ _] -> return (EP Ref n EErased) -- abstract def

183183 [Operator tp arity op] -> return (EP Ref n EErased) -- will be special-cased later

184− [CaseOp _ _ _ _ (CaseDefs _ ([], STerm tm) _)] -> -- nullary fun

184+ [CaseOp _ _ _ _ (CaseDefs _ ([], STerm tm) _ _)] -> -- nullary fun

185185 doExec env ctxt tm

186− [CaseOp _ _ _ _ (CaseDefs _ (ns, sc) _)] -> return (EP Ref n EErased)

186+ [CaseOp _ _ _ _ (CaseDefs _ (ns, sc) _ _)] -> return (EP Ref n EErased)

187187 [] -> execFail $ "Could not find " ++ show n ++ " in definitions."

188188 thing -> trace (take 200 $ "got to " ++ show thing ++ " lookup up " ++ show n) $ undefined

189189doExec env ctxt p@(P Bound n ty) =

@@ -315,10 +315,10 @@ execApp' env ctxt f@(EP _ n _) args =

315315 execApp' env ctxt r (drop arity args)

316316 Nothing -> return (mkEApp f args)

317317 else return (mkEApp f args)

318− [CaseOp _ _ _ _ (CaseDefs _ ([], STerm tm) _)] -> -- nullary fun

318+ [CaseOp _ _ _ _ (CaseDefs _ ([], STerm tm) _ _)] -> -- nullary fun

319319 do rhs <- doExec env ctxt tm

320320 execApp' env ctxt rhs args

321− [CaseOp _ _ _ _ (CaseDefs _ (ns, sc) _)] ->

321+ [CaseOp _ _ _ _ (CaseDefs _ (ns, sc) _ _)] ->

322322 do res <- execCase env ctxt ns sc args

323323 return $ fromMaybe (mkEApp f args) res

324324 thing -> return $ mkEApp f args

src/Idris/ElabDecls.hs+12−4

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

1313import Idris.DataOpts

1414import Idris.Providers

1515import Idris.Primitives

16+import Idris.Inliner

1617import Idris.PartialEval

1718import IRTS.Lang

1819import Paths_idris

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

575576

576577 logLvl 5 $ "Initial typechecked patterns:\n" ++ show pdef

577578

578− -- TODO: Inlining on initial definition happens here

579− let pdef_inl = pdef

579+ -- TODO: Inlining on initial definition happens here.

580+

581+ -- NOTE: Need to store original definition so that proofs which

582+ -- rely on its structure aren't affected by any changes to the

583+ -- inliner. Just use the inlined version to generate pdef' and to

584+ -- help with later inlinings.

585+

586+ ist <- getIState

587+ let pdef_inl = inlineDef ist pdef

580588

581589 numArgs <- tclift $ sameLength pdef

582590

@@ -616,7 +624,7 @@ elabClauses info fc opts n_in cs = let n = liftname info n_in in

616624

617625 -- pdef' is the version that gets compiled for run-time

618626 pdef' <- applyOpts optpdef

619− logLvl 5 $ "After data structure transofmrations:\n" ++ show pdef'

627+ logLvl 5 $ "After data structure transformations:\n" ++ show pdef'

620628

621629 ist <- getIState

622630 -- let wf = wellFounded ist n sc

@@ -653,7 +661,7 @@ elabClauses info fc opts n_in cs = let n = liftname info n_in in

653661 reflect

654662 (AssertTotal `elem` opts)

655663 pats

656− pdef pdef_inl pdef' ty)

664+ pdef pdef pdef_inl pdef' ty)

657665 addIBC (IBCDef n)

658666 setTotality n tot

659667 when (not reflect) $ totcheck (fc, n)

src/Idris/IBC.hs+7−6

@@ -692,15 +692,16 @@ instance Binary CaseAlt where

692692 _ -> error "Corrupted binary data for CaseAlt"

693693

694694instance Binary CaseDefs where

695− put (CaseDefs x1 x2 x3)

696− = do put x1

695+ put (CaseDefs x1 x2 x3 x4)

696+ = do -- don't need totality checked version

697697 put x2

698698 put x3

699+ put x4

699700 get

700− = do x1 <- get

701− x2 <- get

702− x3 <- get

703− return (CaseDefs x1 x2 x3)

701+ = do x2 <- get

702+ x3 <- get -- use for totality checked version

703+ x4 <- get

704+ return (CaseDefs x3 x2 x3 x4)

704705

705706instance Binary CaseInfo where

706707 put x@(CaseInfo x1 x2) = do put x1

src/Idris/Inliner.hsnew file+17

@@ -0,0 +1,17 @@

1+module Idris.Inliner where

3+import Core.TT

4+import Idris.AbsSyntax

6+inlineDef :: IState -> [([Name], Term, Term)] -> [([Name], Term, Term)]

7+inlineDef ist d = d

9+-- Inlining is either top level (i.e. not in a function arg) or argument level

10+

11+-- For each application in a term:

12+-- * Check if the function is inlinable

13+-- (Dictionaries are inlinable in an argument, not otherwise)

14+-- - If so, try inlining without reducing its arguments

15+-- + If successful, then continue on the result (top level)

16+-- + If not, reduce the arguments (argument level) and try again

17+-- - If not, inline all the arguments (top level)

src/Idris/Prover.hs+1

@@ -76,6 +76,7 @@ prove ctxt lit n ty

7676 [Right (P Ref n ty, ptm)]

7777 [([], P Ref n ty, ptm)]

7878 [([], P Ref n ty, ptm)]

79+ [([], P Ref n ty, ptm)]

7980 [([], P Ref n ty, ptm')] ty)

8081 solveDeferred n

8182elabStep :: ElabState [PDecl] -> ElabD a -> Idris (a, ElabState [PDecl])