1d4d226 · Idris-dev · git.iko.soy

git.iko.soy/Idris-dev

on master help sign in

Optimise datatypes with one constructor and one argument

1d4d226Edwin Brady13 years ago

src/IRTS/Compiler.hs+11−11

compare with master

unifiedsplit

@@ -187,17 +187,17 @@ instance ToIR (TT Name) where

187 | (P _ (UN "prim_fork") _, [arg]) <- unApply tm

188 = do arg' <- ir' env arg

189 return $ LOp LFork [LLazyExp arg']

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

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

191− = do v' <- ir' env v

191+-- = do v' <- ir' env v

192− return v'

192+-- return v'

193− | (P _ (UN "prim_io_bind") _, [_,_,v,Bind n (Lam _) sc]) <- unApply tm

193+-- | (P _ (UN "prim_io_bind") _, [_,_,v,Bind n (Lam _) sc]) <- unApply tm

194− = do v' <- ir' env v

194+-- = do v' <- ir' env v

195− sc' <- ir' (n:env) sc

195+-- sc' <- ir' (n:env) sc

196− return (LLet n (LForce v') sc')

196+-- return (LLet n (LForce v') sc')

197− | (P _ (UN "prim_io_bind") _, [_,_,v,k]) <- unApply tm

197+-- | (P _ (UN "prim_io_bind") _, [_,_,v,k]) <- unApply tm

198− = do v' <- ir' env v

198+-- = do v' <- ir' env v

199− k' <- ir' env k

199+-- k' <- ir' env k

200− return (LApp False k' [LForce v'])

200+-- return (LApp False k' [LForce v'])

201 | (P _ (UN "malloc") _, [_,size,t]) <- unApply tm

202 = do size' <- ir' env size

203 t' <- ir' env t

src/Idris/AbsSyntaxTree.hs+1

@@ -688,6 +688,7 @@ deriving instance Binary ClassInfo

688!-}

689

690data OptInfo = Optimise { collapsible :: Bool,

691+ isnewtype :: Bool,

691 forceable :: [Int], -- argument positions

692 forceable :: [Int], -- argument positions

692 recursive :: [Int] }

693 recursive :: [Int] }

693 deriving Show

694 deriving Show

src/Idris/Coverage.hs+1−1

@@ -173,7 +173,7 @@ genAll i args

173 resugar t = t

174

175 getForceable i n = case lookupCtxt n (idris_optimisation i) of

176− [Optimise _ fs _] -> fs

176+ [o] -> forceable o

177 _ -> []

178

179 dropForce force (x : xs) i | i `elem` force

src/Idris/DataOpts.hs+24−4

@@ -18,7 +18,7 @@ forceArgs :: Name -> Type -> Idris ()

18forceArgs n t = do i <- getIState

19 let fargs = force i 0 t

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

21− [] -> return $ Optimise False [] []

21+ [] -> return $ Optimise False False [] []

22 (op:_) -> return op

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

24 putIState (i { idris_optimisation = opts })

@@ -62,8 +62,22 @@ collapseCons ty cons =

62 let cons' = map (\ (n, t) -> (n, map snd (getArgTys t))) cons

63 allFR <- mapM (forceRec i) cons'

64 if and allFR then detaggable (map getRetTy (map snd cons))

65− else return () -- not collapsible as not detaggable

65+ else checkNewType cons'

66 where

67+ -- one constructor; if one remaining argument, treat as newtype

68+ checkNewType [(n, ts)] = do

69+ i <- getIState

70+ case lookupCtxt n (idris_optimisation i) of

71+ (oi:_) -> do let remaining = length ts - length (forceable oi)

72+ if remaining == 1 then

73+ do let oi' = oi { isnewtype = True }

74+ let opts = addDef n oi' (idris_optimisation i)

75+ putIState (i { idris_optimisation = opts })

76+ else return ()

77+ _ -> return ()

78+

79+ checkNewType _ = return ()

80+

67 setCollapsible :: Name -> Idris ()

81 setCollapsible :: Name -> Idris ()

68 setCollapsible n

82 setCollapsible n

69 = do i <- getIState

83 = do i <- getIState

@@ -72,7 +86,7 @@ collapseCons ty cons =

72 (oi:_) -> do let oi' = oi { collapsible = True }

86 (oi:_) -> do let oi' = oi { collapsible = True }

73 let opts = addDef n oi' (idris_optimisation i)

87 let opts = addDef n oi' (idris_optimisation i)

74 putIState (i { idris_optimisation = opts })

88 putIState (i { idris_optimisation = opts })

75− [] -> do let oi = Optimise True [] []

89+ [] -> do let oi = Optimise True False [] []

76 let opts = addDef n oi (idris_optimisation i)

90 let opts = addDef n oi (idris_optimisation i)

77 putIState (i { idris_optimisation = opts })

91 putIState (i { idris_optimisation = opts })

78 addIBC (IBCOpt n)

92 addIBC (IBCOpt n)

@@ -256,7 +270,13 @@ applyDataOptRT oi n tag arity args

256 doOpts n args _ forced

270 doOpts n args _ forced

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

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

258 args) in

272 args) in

273+ if isnewtype oi

274+ then case args' of

275+ [(_, val)] -> val

276+ _ -> error "Can't happen (not isnewtype)"

277+ else

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

278+ mkApp (P (DCon tag (arity - length forced)) n Erased)

279+ (map snd args')

260

280

261 keep (forced, _) = not forced

281 keep (forced, _) = not forced

262

282

src/Idris/ElabDecls.hs+1−1

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

545 [oi] -> do let opts = addDef n (oi { collapsible = True })

546 (idris_optimisation ist)

547 putIState (ist { idris_optimisation = opts })

548− _ -> do let opts = addDef n (Optimise True [] [])

548+ _ -> do let opts = addDef n (Optimise True False [] [])

549 (idris_optimisation ist)

550 putIState (ist { idris_optimisation = opts })

551 addIBC (IBCOpt n)

src/Idris/IBC.hs+5−3

@@ -23,7 +23,7 @@ import Debug.Trace

23import Paths_idris

25ibcVersion :: Word8

26−ibcVersion = 34

26+ibcVersion = 35

28data IBCFile = IBCFile { ver :: Word8,

29 sourcefile :: FilePath,

@@ -1639,15 +1639,17 @@ instance Binary ClassInfo where

1639 return (CI x1 x2 x3 x4 [])

1640

1641instance Binary OptInfo where

1642− put (Optimise x1 x2 x3)

1642+ put (Optimise x1 x2 x3 x4)

1643 = do put x1

1644 put x2

1645 put x3

1646+ put x4

1646 get

1647 get

1647 = do x1 <- get

1648 = do x1 <- get

1648 x2 <- get

1649 x2 <- get

1649 x3 <- get

1650 x3 <- get

1651+ x4 <- get

1650− return (Optimise x1 x2 x3)

1652+ return (Optimise x1 x2 x3 x4)

1651

1653

1652instance Binary TypeInfo where

1654instance Binary TypeInfo where

1653 put (TI x1 x2 x3) = do put x1

1655 put (TI x1 x2 x3) = do put x1