baaba44 · Idris-dev · git.iko.soy

git.iko.soy/Idris-dev

on master help sign in

Run-time forcing optimisation

baaba44Edwin Brady15 years ago

samples/interp.idr+2−3

compare with master

unifiedsplit

@@ -77,7 +77,6 @@ testFac : Int

77testFac = interp [] eFac 4

79main : IO ()

80−main = do { print testFac

81− print test }

80+main = do print test

82−

81+ print testFac

src/Core/Elaborate.hs+6−3

@@ -406,13 +406,16 @@ try t1 t2 = do s <- get

406tryAll :: [(Elab' aux a, String)] -> Elab' aux a

407tryAll xs = tryAll' [] (fail "Nothing to try") (map fst xs)

408 where

409+ cantResolve :: Elab' aux a

410+ cantResolve = fail $ "Couldn't resolve alternative: "

411+ ++ showSep ", " (map snd xs)

412+

409 tryAll' :: [Elab' aux a] -> -- successes

413 tryAll' :: [Elab' aux a] -> -- successes

410 Elab' aux a -> -- last failure

414 Elab' aux a -> -- last failure

411 [Elab' aux a] -> -- still to try

415 [Elab' aux a] -> -- still to try

412 Elab' aux a

416 Elab' aux a

413− tryAll' [res] _ [] = res

417+ tryAll' [res] _ [] = res

414− tryAll' (_:_) _ [] = fail $ "Couldn't resolve alternative: "

418+ tryAll' (_:_) _ [] = cantResolve

415− ++ showSep ", " (map snd xs)

416 tryAll' [] f [] = f

419 tryAll' [] f [] = f

417 tryAll' cs f (x:xs) = do s <- get

420 tryAll' cs f (x:xs) = do s <- get

418 case runStateT x s of

421 case runStateT x s of

src/Core/Evaluate.hs+20−14

@@ -120,7 +120,7 @@ eval ctxt statics genv tm opts = ev True [] tm where

120 [(Function _ tm, Public)] -> ev True env tm

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

122 return $ VP nt n vty

123− [(CaseOp inl _ _ [] tree, Public)] ->

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

124 if simpl && (not inl)

125 then liftM (VP Ref n) (ev top env ty)

126 else do c <- evCase top env [] [] tree

@@ -162,7 +162,7 @@ eval ctxt statics genv tm opts = ev True [] tm where

162 apply False env f args

163 | spec = return $ unload env f args

164 apply top env (VP Ref n ty) args

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

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

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

167 if simpl && (not inl) then return $ unload env (VP Ref n ty) args

168 else do c <- evCase top env ns args tree

@@ -309,7 +309,7 @@ eval_hnf ctxt statics genv tm = ev [] tm where

309 ev env (P Ref n ty) = case lookupDef Nothing n ctxt of

310 [Function _ t] -> ev env t

311 [TyDecl nt ty] -> return $ HP nt n ty

312− [CaseOp inl _ _ [] tree] ->

312+ [CaseOp inl _ _ [] tree _ _] ->

313 do c <- evCase env [] [] tree

314 case c of

315 (Nothing, _, _) -> return $ HP Ref n ty

@@ -339,7 +339,7 @@ eval_hnf ctxt statics genv tm = ev [] tm where

339 app <- apply env sc' as

340 wknH (-1) app

341 apply env (HP Ref n ty) args

342− | [CaseOp _ _ _ ns tree] <- lookupDef Nothing n ctxt

342+ | [CaseOp _ _ _ ns tree _ _] <- lookupDef Nothing n ctxt

343 = do c <- evCase env ns args tree

344 case c of

345 (Nothing, _, env') -> return $ unload env' (HP Ref n ty) args

@@ -439,7 +439,9 @@ spec ctxt statics genv tm = error "spec undefined"

439data Def = Function Type Term

440 | TyDecl NameType Type

441 | Operator Type Int ([Value] -> Maybe Value)

442− | CaseOp Bool Type [(Term, Term)] [Name] SC -- Bool for inlineable

442+ | CaseOp Bool Type [(Term, Term)] -- Bool for inlineable

443+ [Name] SC -- Compile time case definition

444+ [Name] SC -- Run time cae definitions

443{-!

445{-!

444deriving instance Binary Def

446deriving instance Binary Def

445!-}

447!-}

@@ -448,8 +450,10 @@ instance Show Def where

448 show (Function ty tm) = "Function: " ++ show (ty, tm)

450 show (Function ty tm) = "Function: " ++ show (ty, tm)

449 show (TyDecl nt ty) = "TyDecl: " ++ show nt ++ " " ++ show ty

451 show (TyDecl nt ty) = "TyDecl: " ++ show nt ++ " " ++ show ty

450 show (Operator ty _ _) = "Operator: " ++ show ty

452 show (Operator ty _ _) = "Operator: " ++ show ty

451− show (CaseOp _ ty ps ns sc) = "Case: " ++ show ty ++ " " ++ show ps ++ "\n" ++

453+ show (CaseOp _ ty ps ns sc ns' sc')

454+ = "Case: " ++ show ty ++ " " ++ show ps ++ "\n" ++

455+ show ns ++ " " ++ show sc ++ "\n" ++

452− show ns ++ " " ++ show sc

456+ show ns' ++ " " ++ show sc'

453-- We need this for serialising Def. Fortunately, it never gets used because

457-- We need this for serialising Def. Fortunately, it never gets used because

454-- we'll never serialise a primitive operator

458-- we'll never serialise a primitive operator

455

459

@@ -516,13 +520,15 @@ addDatatype (Data n tag ty cons) uctxt

516 addCons (tag+1) cons (addDef n

520 addCons (tag+1) cons (addDef n

517 (TyDecl (DCon tag (arity ty')) ty, Public) ctxt)

521 (TyDecl (DCon tag (arity ty')) ty, Public) ctxt)

518

522

519−addCasedef :: Name -> Bool -> Bool -> [(Term, Term)] -> Type -> Context -> Context

523+addCasedef :: Name -> Bool -> Bool -> [(Term, Term)] -> [(Term, Term)] ->

524+ Type -> Context -> Context

520−addCasedef n alwaysInline tcase ps ty uctxt

525+addCasedef n alwaysInline tcase ps psrt ty uctxt

521 = let ctxt = definitions uctxt

526 = let ctxt = definitions uctxt

522 ps' = ps -- simpl ps in

527 ps' = ps -- simpl ps in

523− ctxt' = case simpleCase tcase ps' of

528+ ctxt' = case (simpleCase tcase ps', simpleCase tcase psrt) of

529+ (CaseDef args sc, CaseDef args' sc') ->

524− CaseDef args sc -> let inl = alwaysInline in

530+ let inl = alwaysInline in

525− addDef n (CaseOp inl ty ps args sc,

531+ addDef n (CaseOp inl ty ps args sc args' sc',

526 Public) ctxt in

532 Public) ctxt in

527 uctxt { definitions = ctxt' }

533 uctxt { definitions = ctxt' }

528 where simpl [] = []

534 where simpl [] = []

@@ -541,7 +547,7 @@ lookupTy root n ctxt

541 (Function ty _) -> return ty

547 (Function ty _) -> return ty

542 (TyDecl _ ty) -> return ty

548 (TyDecl _ ty) -> return ty

543 (Operator ty _ _) -> return ty

549 (Operator ty _ _) -> return ty

544− (CaseOp _ ty _ _ _) -> return ty

550+ (CaseOp _ ty _ _ _ _ _) -> return ty

545

551

546isConName :: Maybe [String] -> Name -> Context -> Bool

552isConName :: Maybe [String] -> Name -> Context -> Bool

547isConName root n ctxt

553isConName root n ctxt

@@ -557,7 +563,7 @@ lookupP root n ctxt

557 p <- case def of

563 p <- case def of

558 (Function ty tm, a) -> return (P Ref n ty, a)

564 (Function ty tm, a) -> return (P Ref n ty, a)

559 (TyDecl nt ty, a) -> return (P nt n ty, a)

565 (TyDecl nt ty, a) -> return (P nt n ty, a)

560− (CaseOp _ ty _ _ _, a) -> return (P Ref n ty, a)

566+ (CaseOp _ ty _ _ _ _ _, a) -> return (P Ref n ty, a)

561 (Operator ty _ _, a) -> return (P Ref n ty, a)

567 (Operator ty _ _, a) -> return (P Ref n ty, a)

562 case snd p of

568 case snd p of

563 Hidden -> []

569 Hidden -> []

src/Idris/AbsSyntax.hs+1−1

280 | Compile String | Execute | ExecVal PTerm

281 | Metavars | Prove Name | AddProof | Universes

282 | TTShell

283− | LogLvl Int | Spec PTerm | HNF PTerm | Defn Name

284 | NOP

285

286-- Parsed declarations

src/Idris/Compiler.hs+5−5

@@ -72,7 +72,7 @@ impossible = int 42424242

73instance ToEpic Def where

74 epic (Function tm _) = epic tm

75− epic (CaseOp _ _ pats args sc) = epic (args, sc) -- TODO: redo case comp after optimising

75+ epic (CaseOp _ _ pats _ _ args sc) = epic (args, sc) -- optimised version

76 epic _ = return impossible

78instance ToEpic (TT Name) where

@@ -80,10 +80,10 @@ instance ToEpic (TT Name) where

80 epic' env tm@(App f a)

81 | (P _ (UN "mkForeign") _, args) <- unApply tm

82 = doForeign args

83− | (P _ (UN "lazy") _, [_, arg]) <- unApply tm

83+ | (P _ (UN "lazy") _, [_,arg]) <- unApply tm

84 = do arg' <- epic' env arg

85 return $ lazy_ arg'

86− | (P _ (UN "prim__IO") _, [_, v]) <- unApply tm

86+ | (P _ (UN "prim__IO") _, [v]) <- unApply tm

87 = epic' env v

88 | (P _ (UN "io_bind") _, [_,_,v,k]) <- unApply tm

89 = do v' <- epic' env v

@@ -137,8 +137,8 @@ doForeign (_ : fgn : args)

137

138getFTypes :: TT Name -> [E.Type]

139getFTypes tm = case unApply tm of

140− (nil, [arg]) -> []

140+ (nil, []) -> []

141− (cons, [a, (P _ (UN ty) _), xs]) ->

141+ (cons, [(P _ (UN ty) _), xs]) ->

142 let rest = getFTypes xs in

143 mkEty ty : rest

144

src/Idris/DataOpts.hs+59−9

@@ -15,7 +15,6 @@ import Debug.Trace

15-- optimisations

17forceArgs :: Name -> Type -> Idris ()

18−-- forceArgs n t = return ()

19forceArgs n t = do let fargs = force 0 t

18forceArgs n t = do let fargs = force 0 t

20 i <- getIState

19 i <- getIState

21 copt <- case lookupCtxt Nothing n (idris_optimisation i) of

20 copt <- case lookupCtxt Nothing n (idris_optimisation i) of

@@ -24,17 +23,18 @@ forceArgs n t = do let fargs = force 0 t

24 let opts = addDef n (copt { forceable = fargs }) (idris_optimisation i)

23 let opts = addDef n (copt { forceable = fargs }) (idris_optimisation i)

25 putIState (i { idris_optimisation = opts })

24 putIState (i { idris_optimisation = opts })

26 addIBC (IBCOpt n)

25 addIBC (IBCOpt n)

27− iLOG $ "Forced: " ++ show n ++ " " ++ show fargs

26+ iLOG $ "Forced: " ++ show n ++ " " ++ show fargs ++ "\n from " ++

27+ show t

28 where

29 force :: Int -> Term -> [Int]

30 force i (Bind _ (Pi _) sc)

31− = force (i + 1) $ instantiate (P Bound (MN i "F?") Erased) sc

31+ = force (i + 1) $ instantiate (P Bound (MN i "?") Erased) sc

32 force _ sc@(App f a)

33 | (_, args) <- unApply sc

34 = nub $ concatMap guarded args

35 force _ _ = []

37− isF (P _ (MN force "F?") _) = Just force

37+ isF (P _ (MN force "?") _) = Just force

38 isF _ = Nothing

40 guarded :: Term -> [Int]

@@ -48,17 +48,27 @@ forceArgs n t = do let fargs = force 0 t

48class Optimisable term where

49 applyOpts :: term -> Idris term

51+instance (Optimisable a, Optimisable b) => Optimisable (a, b) where

52+ applyOpts (x, y) = do x' <- applyOpts x

53+ y' <- applyOpts y

54+ return (x', y')

55+

56+instance Optimisable a => Optimisable [a] where

57+ applyOpts = mapM applyOpts

58+

51-- Raw is for compile time optimisation (before type checking)

59-- Raw is for compile time optimisation (before type checking)

52-- Term is for run time optimisation (after type checking, collapsing allowed)

60-- Term is for run time optimisation (after type checking, collapsing allowed)

62+-- Compile time: no collapsing

63+

54instance Optimisable Raw where

64instance Optimisable Raw where

55 applyOpts t@(RApp f a)

65 applyOpts t@(RApp f a)

56 | (Var n, args) <- raw_unapply t -- MAGIC HERE

66 | (Var n, args) <- raw_unapply t -- MAGIC HERE

67+ = do args' <- mapM applyOpts args

57− = do i <- getIState

68+ i <- getIState

58 case lookupCtxt Nothing n (idris_optimisation i) of

69 case lookupCtxt Nothing n (idris_optimisation i) of

59− (oi:_) -> return $ applyDataOpt oi n args

70+ (oi:_) -> return $ applyDataOpt oi n args'

60− _ -> do args' <- mapM applyOpts args

61− return (raw_apply (Var n) args')

71+ _ -> return (raw_apply (Var n) args')

62 | otherwise = do f' <- applyOpts f

72 | otherwise = do f' <- applyOpts f

63 a' <- applyOpts a

73 a' <- applyOpts a

64 return (RApp f' a')

74 return (RApp f' a')

@@ -75,7 +85,6 @@ instance Optimisable t => Optimisable (Binder t) where

75 applyOpts b = do t' <- applyOpts (binderTy b)

85 applyOpts b = do t' <- applyOpts (binderTy b)

76 return (b { binderTy = t' })

86 return (b { binderTy = t' })

78−-- Compile time: no collapsing

80applyDataOpt :: OptInfo -> Name -> [Raw] -> Raw

89applyDataOpt :: OptInfo -> Name -> [Raw] -> Raw

81applyDataOpt oi n args

90applyDataOpt oi n args

@@ -86,3 +95,44 @@ applyDataOpt oi n args

86 doForce True a = RForce a

95 doForce True a = RForce a

87 doForce False a = a

96 doForce False a = a

98+-- Run-time: do everything

99+

100+instance Optimisable (TT Name) where

101+ applyOpts t@(App f a)

102+ | (c@(P (DCon t arity) n _), args) <- unApply t -- MAGIC HERE

103+ = do args' <- mapM applyOpts args

104+ i <- getIState

105+ case lookupCtxt Nothing n (idris_optimisation i) of

106+ (oi:_) -> do return $ applyDataOptRT oi n t arity args'

107+ _ -> return (mkApp c args')

108+ | otherwise = do f' <- applyOpts f

109+ a' <- applyOpts a

110+ return (App f' a')

111+ applyOpts (Bind n b t) = do b' <- applyOpts b

112+ t' <- applyOpts t

113+ return (Bind n b' t')

114+ applyOpts t = return t

115+

116+-- Need to saturate arguments first to ensure that erasure happens uniformly

117+

118+applyDataOptRT :: OptInfo -> Name -> Int -> Int -> [Term] -> Term

119+applyDataOptRT oi n tag arity args

120+ | length args == arity = doOpts n args (collapsible oi) (forceable oi)

121+ | otherwise = let extra = satArgs (arity - length args)

122+ tm = doOpts n (args ++ map (\n -> P Bound n Erased) extra)

123+ (collapsible oi) (forceable oi) in

124+ bind extra tm

125+ where

126+ satArgs n = map (\i -> MN i "sat") [1..n]

127+

128+ bind [] tm = tm

129+ bind (n:ns) tm = Bind n (Lam Erased) (pToV n (bind ns tm))

130+

131+ doOpts n args True f = Erased

132+ doOpts n args _ forced

133+ = let args' = filter keep (zip (map (\x -> x `elem` forced) [0..])

134+ args) in

135+ mkApp (P (DCon tag (arity - length forced)) n Erased) (map snd args')

136+

137+ keep (forced, _) = not forced

138+

src/Idris/Delaborate.hs+1

@@ -31,6 +31,7 @@ delab' ist tm fullname = de [] tm

31 = PLet n (de env ty) (de env val) (de (n:env) sc)

32 de env (Bind n _ sc) = de (n:env) sc

33 de env (Constant i) = PConstant i

34+ de env Erased = Placeholder

34 de env (Set i) = PSet

35 de env (Set i) = PSet

36 dens x | fullname = x

37 dens x | fullname = x

src/Idris/ElabDecls.hs+7−4

@@ -25,8 +25,8 @@ import Debug.Trace

27recheckC ctxt fc env t

28− = do t' <- applyOpts (forget t)

28+ = do -- t' <- applyOpts (forget t) (doesn't work, or speed things up...)

29− (tm, ty, cs) <- tclift $ recheck ctxt env t' t

29+ (tm, ty, cs) <- tclift $ recheck ctxt env (forget t) t

30 addConstraints fc cs

31 return (tm, ty)

@@ -107,13 +107,16 @@ elabClauses info fc opts n_in cs_in = let n = liftname info n_in in

107 ist <- get

108 let tcase = opt_typecase (idris_options ist)

109 let pdef = map debind pats

110+ pdef' <- applyOpts pdef

110− let tree = simpleCase tcase pdef

111+ let tree = simpleCase tcase pdef

112+ let tree' = simpleCase tcase pdef'

111 tclift $ sameLength pdef

113 tclift $ sameLength pdef

112 logLvl 3 (show tree)

114 logLvl 3 (show tree)

115+ logLvl 3 $ "Optimised: " ++ show tree'

113 ctxt <- getContext

116 ctxt <- getContext

114 case lookupTy (namespace info) n ctxt of

117 case lookupTy (namespace info) n ctxt of

115 [ty] -> do updateContext (addCasedef n (inlinable opts)

118 [ty] -> do updateContext (addCasedef n (inlinable opts)

116− tcase pdef ty)

119+ tcase pdef pdef' ty)

117 addIBC (IBCDef n)

120 addIBC (IBCDef n)

118 [] -> return ()

121 [] -> return ()

119 where

122 where

src/Idris/IBC.hs+12−8

@@ -22,7 +22,7 @@ import System.Directory

22import Paths_idris

24ibcVersion :: Word8

25−ibcVersion = 5

25+ibcVersion = 6

27data IBCFile = IBCFile { ver :: Word8,

28 sourcefile :: FilePath,

@@ -509,12 +509,14 @@ instance Binary Def where

509 put x1

510 put x2

511 put x3

512− CaseOp x1 x2 x3 x4 x5 -> do putWord8 3

512+ CaseOp x1 x2 x3 x4 x5 x6 x7 -> do putWord8 3

513− put x1

513+ put x1

514− put x2

514+ put x2

515− put x3

515+ put x3

516− put x4

516+ put x4

517− put x5

517+ put x5

518+ put x6

519+ put x7

518 get

520 get

519 = do i <- getWord8

521 = do i <- getWord8

520 case i of

522 case i of

@@ -533,7 +535,9 @@ instance Binary Def where

533 x3 <- get

535 x3 <- get

534 x4 <- get

536 x4 <- get

535 x5 <- get

537 x5 <- get

538+ x6 <- get

539+ x7 <- get

536− return (CaseOp x1 x2 x3 x4 x5)

540+ return (CaseOp x1 x2 x3 x4 x5 x6 x7)

537 _ -> error "Corrupted binary data for Def"

541 _ -> error "Corrupted binary data for Def"

538

542

539instance Binary Accessibility where

543instance Binary Accessibility where

src/Idris/Prover.hs+4−1

@@ -12,6 +12,7 @@ import Idris.ElabDecls

12import Idris.ElabTerm

13import Idris.Parser

14import Idris.Error

15+import Idris.DataOpts

16import System.Console.Haskeline

17import System.Console.Haskeline

17import Control.Monad.State

18import Control.Monad.State

@@ -41,7 +42,9 @@ prove ctxt n ty

41 let tree = simpleCase False [(P Ref n ty, tm)]

42 let tree = simpleCase False [(P Ref n ty, tm)]

42 logLvl 3 (show tree)

43 logLvl 3 (show tree)

43 (ptm, pty) <- recheckC ctxt (FC "proof" 0) [] tm

44 (ptm, pty) <- recheckC ctxt (FC "proof" 0) [] tm

45+ ptm' <- applyOpts ptm

44− updateContext (addCasedef n True False [(P Ref n ty, ptm)] ty)

46+ updateContext (addCasedef n True False [(P Ref n ty, ptm)]

47+ [(P Ref n ty, ptm')] ty)

45 solveDeferred n

48 solveDeferred n

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

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

src/Idris/REPL.hs+3

@@ -165,6 +165,9 @@ process Universes = do i <- get

165 OK _ -> iputStrLn "Universes OK"

166process (Defn n) = do ctxt <- getContext

167 liftIO $ print (lookupDef Nothing n ctxt)

168+process (Info n) = do i <- get

169+ let oi = lookupCtxt Nothing n (idris_optimisation i)

170+ liftIO $ print oi

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

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

169 ctxt <- getContext

172 ctxt <- getContext

170 ist <- get

173 ist <- get

src/Idris/REPLParser.hs+1

@@ -36,6 +36,7 @@ pCmd = try (do cmd ["q", "quit"]; eof; return Quit)

36 <|> try (do cmd ["d", "def"]; n <- pName; eof; return (Defn n))

37 <|> try (do cmd ["t", "type"]; do t <- pFullExpr defaultSyntax; return (Check t))

38 <|> try (do cmd ["u", "universes"]; eof; return Universes)

39+ <|> try (do cmd ["i", "info"]; n <- pfName; eof; return (Info n))

39 <|> try (do cmd ["x"]; t <- pFullExpr defaultSyntax; return (ExecVal t))

40 <|> try (do cmd ["x"]; t <- pFullExpr defaultSyntax; return (ExecVal t))

40 <|> do t <- pFullExpr defaultSyntax; return (Eval t)

41 <|> do t <- pFullExpr defaultSyntax; return (Eval t)

41 <|> do eof; return NOP

42 <|> do eof; return NOP