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

git.iko.soy/Idris-dev

Optimise datatypes with one constructor and one argument

No need to pack them up (because we're strict!) so just treat them as a newtype would be in Haskell. No need now to treat prim__IO/prim_io_bind specially in the compiler as the cosntructor is automatically discarded by this optimisation.

commit1d4d226c74518e00a4faff31752cc3342e00e75c authorEdwin Brady <ecb10@st-andrews.ac.uk> dateTue 3 Sep 2013, 19:28 (13 years ago) parent87265a9

6 files changed+43−20

compare with master

unifiedsplit

src/IRTS/Compiler.hs+11−11 src/Idris/AbsSyntaxTree.hs+1 src/Idris/Coverage.hs+1−1 src/Idris/DataOpts.hs+24−4 src/Idris/ElabDecls.hs+1−1 src/Idris/IBC.hs+5−3

src/IRTS/Compiler.hs+11−11

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

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

188188 = do arg' <- ir' env arg

189189 return $ LOp LFork [LLazyExp arg']

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

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

192− return v'

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

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

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

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

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

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

199− k' <- ir' env k

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

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

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

192+-- return v'

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

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

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

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

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

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

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

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

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

202202 = do size' <- ir' env size

203203 t' <- ir' env t

src/Idris/AbsSyntaxTree.hs+1

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

688688!-}

689689

690690data OptInfo = Optimise { collapsible :: Bool,

691+ isnewtype :: Bool,

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

692693 recursive :: [Int] }

693694 deriving Show

src/Idris/Coverage.hs+1−1

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

173173 resugar t = t

174174

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

176− [Optimise _ fs _] -> fs

176+ [o] -> forceable o

177177 _ -> []

178178

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

src/Idris/DataOpts.hs+24−4

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

1818forceArgs n t = do i <- getIState

1919 let fargs = force i 0 t

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

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

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

2222 (op:_) -> return op

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

2424 putIState (i { idris_optimisation = opts })

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

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

6363 allFR <- mapM (forceRec i) cons'

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

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

65+ else checkNewType cons'

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

6781 setCollapsible :: Name -> Idris ()

6882 setCollapsible n

6983 = do i <- getIState

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

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

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

7488 putIState (i { idris_optimisation = opts })

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

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

7690 let opts = addDef n oi (idris_optimisation i)

7791 putIState (i { idris_optimisation = opts })

7892 addIBC (IBCOpt n)

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

256270 doOpts n args _ forced

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

258272 args) in

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

273+ if isnewtype oi

274+ then case args' of

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

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

277+ else

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

279+ (map snd args')

260280

261281 keep (forced, _) = not forced

262282

src/Idris/ElabDecls.hs+1−1

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

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

546546 (idris_optimisation ist)

547547 putIState (ist { idris_optimisation = opts })

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

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

549549 (idris_optimisation ist)

550550 putIState (ist { idris_optimisation = opts })

551551 addIBC (IBCOpt n)

src/Idris/IBC.hs+5−3

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

2323import Paths_idris

2424

2525ibcVersion :: Word8

26−ibcVersion = 34

26+ibcVersion = 35

2727

2828data IBCFile = IBCFile { ver :: Word8,

2929 sourcefile :: FilePath,

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

16391639 return (CI x1 x2 x3 x4 [])

16401640

16411641instance Binary OptInfo where

1642− put (Optimise x1 x2 x3)

1642+ put (Optimise x1 x2 x3 x4)

16431643 = do put x1

16441644 put x2

16451645 put x3

1646+ put x4

16461647 get

16471648 = do x1 <- get

16481649 x2 <- get

16491650 x3 <- get

1650− return (Optimise x1 x2 x3)

1651+ x4 <- get

1652+ return (Optimise x1 x2 x3 x4)

16511653

16521654instance Binary TypeInfo where

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