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

git.iko.soy/Idris-dev

on master help sign in

Add skeleton of inliner

81425d2Edwin Brady13 years ago

idris.cabal+1

compare with master

unifiedsplit

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

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

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

261 Idris.PartialEval, Idris.Providers, Idris.Chaser,

262+ Idris.Inliner,

262

263

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

264 Util.Pretty, Util.System, Util.DynamicLinker,

264 Pkg.Package, Pkg.PParser,

265 Pkg.Package, Pkg.PParser,

src/Core/Evaluate.hs+8−1

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

529data CaseDefs = CaseDefs {

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

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

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

532 cases_runtime :: ([Name], SC)

533 cases_runtime :: ([Name], SC)

533 }

534 }

534

535

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

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

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

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

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

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

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

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

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

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

680 Type -> Context -> Context

682 Type -> Context -> Context

681addCasedef n ci@(CaseInfo alwaysInline tcdict)

683addCasedef 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

683 = let ctxt = definitions uctxt

686 = let ctxt = definitions uctxt

684 access = case lookupDefAcc n False uctxt of

687 access = case lookupDefAcc n False uctxt of

685 [(_, acc)] -> acc

688 [(_, acc)] -> acc

686 _ -> Public

689 _ -> Public

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

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

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

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

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

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

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

690 (OK (CaseDef args_tot sc_tot _),

694 (OK (CaseDef args_tot sc_tot _),

691 OK (CaseDef args_ct sc_ct _),

695 OK (CaseDef args_ct sc_ct _),

696+ OK (CaseDef args_inl sc_inl _),

692 OK (CaseDef args_rt sc_rt _)) ->

697 OK (CaseDef args_rt sc_rt _)) ->

693 let inl = alwaysInline -- || tcdict

698 let inl = alwaysInline -- || tcdict

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

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

695 inlr = inl || small n args_rt sc_rt

700 inlr = inl || small n args_rt sc_rt

696 cdef = CaseDefs (args_tot, sc_tot)

701 cdef = CaseDefs (args_tot, sc_tot)

697 (args_ct, sc_ct)

702 (args_ct, sc_ct)

703+ (args_inl, sc_inl)

698 (args_rt, sc_rt) in

704 (args_rt, sc_rt) in

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

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

700 ty ps_in ps_tot cdef,

706 ty ps_in ps_tot cdef,

701 access, Unchecked) ctxt in

707 access, Unchecked) ctxt in

702 uctxt { definitions = ctxt' }

708 uctxt { definitions = ctxt' }

703

709

710+-- simplify a definition for totality checking

704simplifyCasedef :: Name -> Context -> Context

711simplifyCasedef :: Name -> Context -> Context

705simplifyCasedef n uctxt

712simplifyCasedef n uctxt

706 = let ctxt = definitions uctxt

713 = let ctxt = definitions uctxt

src/Core/Execute.hs+4−4

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

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

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

183 [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

185 doExec env ctxt tm

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

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

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

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

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

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

315 execApp' env ctxt r (drop arity args)

316 Nothing -> return (mkEApp f args)

317 else return (mkEApp f args)

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

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

319 do rhs <- doExec env ctxt tm

320 execApp' env ctxt rhs args

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

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

322 do res <- execCase env ctxt ns sc args

323 return $ fromMaybe (mkEApp f args) res

324 thing -> return $ mkEApp f args

src/Idris/ElabDecls.hs+12−4

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

13import Idris.DataOpts

14import Idris.Providers

15import Idris.Primitives

16+import Idris.Inliner

16import Idris.PartialEval

17import Idris.PartialEval

17import IRTS.Lang

18import IRTS.Lang

18import Paths_idris

19import Paths_idris

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

575

576

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

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

577

578

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

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

579− let pdef_inl = pdef

587+ let pdef_inl = inlineDef ist pdef

580

588

581 numArgs <- tclift $ sameLength pdef

589 numArgs <- tclift $ sameLength pdef

582

590

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

616

624

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

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

618 pdef' <- applyOpts optpdef

626 pdef' <- applyOpts optpdef

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

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

620

628

621 ist <- getIState

629 ist <- getIState

622 -- let wf = wellFounded ist n sc

630 -- let wf = wellFounded ist n sc

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

653 reflect

661 reflect

654 (AssertTotal `elem` opts)

662 (AssertTotal `elem` opts)

655 pats

663 pats

656− pdef pdef_inl pdef' ty)

664+ pdef pdef pdef_inl pdef' ty)

657 addIBC (IBCDef n)

665 addIBC (IBCDef n)

658 setTotality n tot

666 setTotality n tot

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

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

src/Idris/IBC.hs+7−6

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

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

693

694instance Binary CaseDefs where

695− put (CaseDefs x1 x2 x3)

695+ put (CaseDefs x1 x2 x3 x4)

696− = do put x1

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

697 put x2

698 put x3

699+ put x4

699 get

700 get

700− = do x1 <- get

701+ = do x2 <- get

701− x2 <- get

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

702− x3 <- get

703+ x4 <- get

703− return (CaseDefs x1 x2 x3)

704+ return (CaseDefs x3 x2 x3 x4)

704

705

705instance Binary CaseInfo where

706instance Binary CaseInfo where

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

707 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

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

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

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

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

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

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

80 solveDeferred n

81 solveDeferred n

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

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