8096500 · Idris-dev · git.iko.soy

git.iko.soy/Idris-dev

on master help sign in

Add %used pragma

8096500Edwin Brady12 years ago

libs/prelude/IO.idr+13−2

compare with master

unifiedsplit

@@ -112,7 +112,12 @@ prim_fwrite h s

112

113--------- The C FFI

114

115+data Raw : Type -> Type where

115−data Raw a = MkRaw a -- code generated can assume it's compiled just as 'a'

116+ -- code generated can assume it's compiled just as 't'

117+ MkRaw : (x : t) -> Raw t

118+

119+-- Tell erasure analysis not to erase the argument

120+%used MkRaw x

116

121

117-- Supported C integer types

122-- Supported C integer types

118data C_IntTypes : Type -> Type where

123data C_IntTypes : Type -> Type where

@@ -163,7 +168,8 @@ forceGC = foreign FFI_C "idris_forceGC" (Ptr -> IO ()) prim__vm

163

168

164-- Supported JS foreign types

169-- Supported JS foreign types

165mutual

170mutual

171+ data JsFn : Type -> Type where

166− data JsFn t = MkJsFn t

172+ MkJsFn : (x : t) -> JsFn t

167

173

168 data JS_IntTypes : Type -> Type where

174 data JS_IntTypes : Type -> Type where

169 JS_IntChar : JS_IntTypes Char

175 JS_IntChar : JS_IntTypes Char

@@ -182,6 +188,11 @@ mutual

182 JS_FnT : JS_FnTypes a -> JS_Types (JsFn a)

188 JS_FnT : JS_FnTypes a -> JS_Types (JsFn a)

183 JS_IntT : JS_IntTypes i -> JS_Types i

189 JS_IntT : JS_IntTypes i -> JS_Types i

184

190

191+-- Tell erasure analysis not to erase the argument. Needs to be outside the

192+-- mutual block, since directives are done on the first pass and in the first

193+-- pass we only have 'JsFn' and not the constructor.

194+%used MkJsFn x

195+

185FFI_JS : FFI

196FFI_JS : FFI

186FFI_JS = MkFFI JS_Types String

197FFI_JS = MkFFI JS_Types String

187

198

src/Idris/AbsSyntax.hs+20

@@ -125,6 +125,26 @@ addErrRev :: (Term, Term) -> Idris ()

125addErrRev t = do i <- getIState

126 putIState $ i { idris_errRev = t : idris_errRev i }

127

128+addErasureUsage :: Name -> Int -> Idris ()

129+addErasureUsage n i = do ist <- getIState

130+ putIState $ ist { idris_erasureUsed = (n, i) : idris_erasureUsed ist }

131+

132+addUsedName :: FC -> Name -> Name -> Idris ()

133+addUsedName fc n arg

134+ = do ist <- getIState

135+ case lookupTyName n (tt_ctxt ist) of

136+ [(_, ty)] -> addUsage 0 ty

137+ [] -> throwError (At fc (NoSuchVariable n))

138+ xs -> throwError (At fc (CantResolveAlts (map fst xs)))

139+ where addUsage i (Bind x _ sc) | x == arg = do addIBC (IBCUsage (n, i))

140+ addErasureUsage n i

141+ | otherwise = addUsage (i + 1) sc

142+ addUsage _ _ = throwError (At fc (Msg ("No such argument name " ++ show arg)))

143+

144+getErasureUsage :: Idris [(Name, Int)]

145+getErasureUsage = do ist <- getIState;

146+ return (idris_erasureUsed ist)

147+

128totcheck :: (FC, Name) -> Idris ()

148totcheck :: (FC, Name) -> Idris ()

129totcheck n = do i <- getIState; putIState $ i { idris_totcheck = idris_totcheck i ++ [n] }

149totcheck n = do i <- getIState; putIState $ i { idris_totcheck = idris_totcheck i ++ [n] }

130

150

src/Idris/AbsSyntaxTree.hs+3−1

@@ -219,6 +219,7 @@ data IState = IState {

219 module_aliases :: M.Map [T.Text] [T.Text],

220 idris_consolewidth :: ConsoleWidth, -- ^ How many chars wide is the console?

221 idris_postulates :: S.Set Name,

222+ idris_erasureUsed :: [(Name, Int)], -- ^ Function/constructor name, argument position is used

222 idris_whocalls :: Maybe (M.Map Name [Name]),

223 idris_whocalls :: Maybe (M.Map Name [Name]),

223 idris_callswho :: Maybe (M.Map Name [Name]),

224 idris_callswho :: Maybe (M.Map Name [Name]),

224 idris_repl_defs :: [Name], -- ^ List of names that were defined in the repl, and can be re-/un-defined

225 idris_repl_defs :: [Name], -- ^ List of names that were defined in the repl, and can be re-/un-defined

@@ -294,6 +295,7 @@ data IBCWrite = IBCFix FixDecl

294 | IBCTotCheckErr FC String

295 | IBCTotCheckErr FC String

295 | IBCParsedRegion FC

296 | IBCParsedRegion FC

296 | IBCModDocs Name -- ^ The name is the special name used to track module docs

297 | IBCModDocs Name -- ^ The name is the special name used to track module docs

298+ | IBCUsage (Name, Int)

297 deriving Show

299 deriving Show

298

300

299-- | The initial state for the compiler

301-- | The initial state for the compiler

@@ -306,7 +308,7 @@ idrisInit = IState initContext [] []

306 [] [] [] defaultOpts 6 [] [] [] [] emptySyntaxRules [] [] [] [] [] [] []

308 [] [] [] defaultOpts 6 [] [] [] [] emptySyntaxRules [] [] [] [] [] [] []

307 [] [] Nothing [] Nothing [] [] Nothing Nothing [] Hidden False [] Nothing [] []

309 [] [] Nothing [] Nothing [] [] Nothing Nothing [] Hidden False [] Nothing [] []

308 (RawOutput stdout) True defaultTheme [] (0, emptyContext) emptyContext M.empty

310 (RawOutput stdout) True defaultTheme [] (0, emptyContext) emptyContext M.empty

309− AutomaticWidth S.empty Nothing Nothing [] [] M.empty

311+ AutomaticWidth S.empty [] Nothing Nothing [] [] M.empty

310

312

311-- | The monad for the main REPL - reading and processing files and updating

313-- | The monad for the main REPL - reading and processing files and updating

312-- global state (hence the IO inner monad).

314-- global state (hence the IO inner monad).

src/Idris/Erasure.hs+13−12

@@ -76,9 +76,10 @@ performUsageAnalysis = do

76 ci <- idris_classes <$> getIState

77 cg <- idris_callgraph <$> getIState

78 opt <- idris_optimisation <$> getIState

79+ used <- idris_erasureUsed <$> getIState

80 -- Build the dependency graph.

81 -- Build the dependency graph.

81− let depMap = buildDepMap ci ctx main

82+ let depMap = buildDepMap ci used ctx main

83 -- Search for reachable nodes in the graph.

84 -- Search for reachable nodes in the graph.

84 let (residDeps, (reachableNames, minUse)) = minimalUsage depMap

85 let (residDeps, (reachableNames, minUse)) = minimalUsage depMap

@@ -170,12 +171,13 @@ forwardChain deps

170

171

171-- Build the dependency graph,

172-- Build the dependency graph,

172-- starting the depth-first search from a list of Names.

173-- starting the depth-first search from a list of Names.

173−buildDepMap :: Ctxt ClassInfo -> Context -> Name -> Deps

174+buildDepMap :: Ctxt ClassInfo -> [(Name, Int)] -> Context -> Name -> Deps

174−buildDepMap ci ctx mainName = addPostulates $ dfs S.empty M.empty [mainName]

175+buildDepMap ci used ctx mainName = addPostulates used $

176+ dfs S.empty M.empty [mainName]

175 where

177 where

176 -- mark the result of Main.main as used with the empty assumption

178 -- mark the result of Main.main as used with the empty assumption

177− addPostulates :: Deps -> Deps

179+ addPostulates :: [(Name, Int)] -> Deps -> Deps

178− addPostulates deps = foldr (\(ds, rs) -> M.insertWith (M.unionWith S.union) ds rs) deps postulates

180+ addPostulates used deps = foldr (\(ds, rs) -> M.insertWith (M.unionWith S.union) ds rs) deps (postulates used)

179 where

181 where

180 -- mini-DSL for postulates

182 -- mini-DSL for postulates

181 (==>) ds rs = (S.fromList ds, M.fromList [(r, S.empty) | r <- rs])

183 (==>) ds rs = (S.fromList ds, M.fromList [(r, S.empty) | r <- rs])

@@ -187,24 +189,23 @@ buildDepMap ci ctx mainName = addPostulates $ dfs S.empty M.empty [mainName]

187 usedNames = allNames deps S.\\ specialPrims

189 usedNames = allNames deps S.\\ specialPrims

188 usedPrims = [(p_name p, p_arity p) | p <- primitives, p_name p `S.member` usedNames]

190 usedPrims = [(p_name p, p_arity p) | p <- primitives, p_name p `S.member` usedNames]

189

191

190− postulates =

192+ postulates used =

191 [ [] ==> concat

193 [ [] ==> concat

192 -- These two, Main.main and run__IO, are always evaluated

194 -- These two, Main.main and run__IO, are always evaluated

193 -- but they elude analysis since they come from the seed term.

195 -- but they elude analysis since they come from the seed term.

194 [ [(mainName, Result)]

196 [ [(mainName, Result)]

195 , [(sUN "run__IO", Result), (sUN "run__IO", Arg 1)]

197 , [(sUN "run__IO", Result), (sUN "run__IO", Arg 1)]

196

198

199+ -- Explicit usage declarations from a %used pragma

200+ , map (\(n, i) -> (n, Arg i)) used

201+

197 -- MkIO is read by run__IO,

202 -- MkIO is read by run__IO,

198 -- but this cannot be observed in the source code of programs.

203 -- but this cannot be observed in the source code of programs.

199 , it "MkIO" [2]

204 , it "MkIO" [2]

200 , it "prim__IO" [1]

205 , it "prim__IO" [1]

201

206

202− -- temporary hacks for preventing erasure of these in foreign

207+ -- Foreign calls are built with pairs, but mkForeign doesn't

203− -- calls. TODO: make this not a hack, and possible to set

208+ -- have an implementation so analysis won't see them

204− -- in Idris source

205− , it "MkJsFn" [1]

206− , it "MkRaw" [1]

207−

208 , [(pairCon, Arg 2),

209 , [(pairCon, Arg 2),

209 (pairCon, Arg 3)] -- Used in foreign calls

210 (pairCon, Arg 3)] -- Used in foreign calls

210

211

src/Idris/IBC.hs+14−5

@@ -35,7 +35,7 @@ import Codec.Compression.Zlib (compress)

35import Util.Zlib (decompressEither)

37ibcVersion :: Word8

38−ibcVersion = 94

38+ibcVersion = 95

40data IBCFile = IBCFile { ver :: Word8,

41 sourcefile :: FilePath,

@@ -77,7 +77,8 @@ data IBCFile = IBCFile { ver :: Word8,

77 ibc_metavars :: ![(Name, (Maybe Name, Int, Bool))],

78 ibc_patdefs :: ![(Name, ([([Name], Term, Term)], [PTerm]))],

79 ibc_postulates :: ![Name],

80− ibc_parsedSpan :: !(Maybe FC)

80+ ibc_parsedSpan :: !(Maybe FC),

81+ ibc_usage :: ![(Name, Int)]

81 }

82 }

82 deriving Show

83 deriving Show

83{-!

84{-!

@@ -85,7 +86,7 @@ deriving instance Binary IBCFile

85!-}

86!-}

87initIBC :: IBCFile

88initIBC :: IBCFile

88−initIBC = IBCFile ibcVersion "" [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] Nothing

89+initIBC = IBCFile ibcVersion "" [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] Nothing []

90loadIBC :: Bool -- ^ True = reexport, False = make everything private

91loadIBC :: Bool -- ^ True = reexport, False = make everything private

91 -> FilePath -> Idris ()

92 -> FilePath -> Idris ()

@@ -229,6 +230,7 @@ ibc i (IBCParsedRegion fc) f = return f { ibc_parsedSpan = Just fc }

229ibc i (IBCModDocs n) f = case lookupCtxtExact n (idris_moduledocs i) of

230ibc i (IBCModDocs n) f = case lookupCtxtExact n (idris_moduledocs i) of

230 Just v -> return f { ibc_moduledocs = (n,v) : ibc_moduledocs f }

231 Just v -> return f { ibc_moduledocs = (n,v) : ibc_moduledocs f }

231 _ -> ifail "IBC write failed"

232 _ -> ifail "IBC write failed"

233+ibc i (IBCUsage n) f = return f { ibc_usage = n : ibc_usage f }

232

234

233process :: Bool -- ^ Reexporting

235process :: Bool -- ^ Reexporting

234 -> IBCFile -> FilePath -> Idris ()

236 -> IBCFile -> FilePath -> Idris ()

@@ -285,6 +287,7 @@ process reexp i fn

285 pMetavars $ force (ibc_metavars i)

287 pMetavars $ force (ibc_metavars i)

286 pPostulates $ force (ibc_postulates i)

288 pPostulates $ force (ibc_postulates i)

287 pParsedSpan $ force (ibc_parsedSpan i)

289 pParsedSpan $ force (ibc_parsedSpan i)

290+ pUsage $ force (ibc_usage i)

288

291

289timestampOlder :: FilePath -> FilePath -> Idris ()

292timestampOlder :: FilePath -> FilePath -> Idris ()

290timestampOlder src ibc = do srct <- runIO $ getModificationTime src

293timestampOlder src ibc = do srct <- runIO $ getModificationTime src

@@ -302,6 +305,10 @@ pParsedSpan :: Maybe FC -> Idris ()

302pParsedSpan fc = do ist <- getIState

305pParsedSpan fc = do ist <- getIState

303 putIState ist { idris_parsedSpan = fc }

306 putIState ist { idris_parsedSpan = fc }

304

307

308+pUsage :: [(Name, Int)] -> Idris ()

309+pUsage ns = do ist <- getIState

310+ putIState ist { idris_erasureUsed = ns ++ idris_erasureUsed ist }

311+

305pImportDirs :: [FilePath] -> Idris ()

312pImportDirs :: [FilePath] -> Idris ()

306pImportDirs fs = mapM_ addImportDir fs

313pImportDirs fs = mapM_ addImportDir fs

307

314

@@ -907,7 +914,7 @@ instance Binary MetaInformation where

907 return (DataMI x1)

914 return (DataMI x1)

908

915

909instance Binary IBCFile where

916instance Binary IBCFile where

910− put x@(IBCFile x1 x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 x15 x16 x17 x18 x19 x20 x21 x22 x23 x24 x25 x26 x27 x28 x29 x30 x31 x32 x33 x34 x35 x36 x37 x38 x39 x40 x41)

917+ put x@(IBCFile x1 x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 x15 x16 x17 x18 x19 x20 x21 x22 x23 x24 x25 x26 x27 x28 x29 x30 x31 x32 x33 x34 x35 x36 x37 x38 x39 x40 x41 x42)

911 = {-# SCC "putIBCFile" #-}

918 = {-# SCC "putIBCFile" #-}

912 do put x1

919 do put x1

913 put x2

920 put x2

@@ -950,6 +957,7 @@ instance Binary IBCFile where

950 put x39

957 put x39

951 put x40

958 put x40

952 put x41

959 put x41

960+ put x42

953

961

954 get

962 get

955 = do x1 <- get

963 = do x1 <- get

@@ -994,7 +1002,8 @@ instance Binary IBCFile where

994 x39 <- get

1002 x39 <- get

995 x40 <- get

1003 x40 <- get

996 x41 <- get

1004 x41 <- get

1005+ x42 <- get

997− return (IBCFile x1 x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 x15 x16 x17 x18 x19 x20 x21 x22 x23 x24 x25 x26 x27 x28 x29 x30 x31 x32 x33 x34 x35 x36 x37 x38 x39 x40 x41)

1006+ return (IBCFile x1 x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 x15 x16 x17 x18 x19 x20 x21 x22 x23 x24 x25 x26 x27 x28 x29 x30 x31 x32 x33 x34 x35 x36 x37 x38 x39 x40 x41 x42)

998 else return (initIBC { ver = x1 })

1007 else return (initIBC { ver = x1 })

999

1008

1000instance Binary DataOpt where

1009instance Binary DataOpt where

src/Idris/Parser.hs+6

@@ -1057,6 +1057,12 @@ directive syn = do try (lchar '%' *> reserved "lib"); cgn <- codegen_; lib <- st

1057 mapM_ (addIBC . IBCFunctionErrorHandler fn' arg) ns')]

1058 <|> do try (lchar '%' *> reserved "language"); ext <- pLangExt;

1059 return [PDirective (addLangExt ext)]

1060+ <|> do fc <- getFC

1061+ try (lchar '%' *> reserved "used")

1062+ fn <- fnName

1063+ arg <- iName []

1064+ return [PDirective (addUsedName fc fn arg)]

1065+

1060 <?> "directive"

1066 <?> "directive"

1061 where disambiguate :: Name -> Idris Name

1067 where disambiguate :: Name -> Idris Name

1062 disambiguate n = do i <- getIState

1068 disambiguate n = do i <- getIState