8096500 · Idris-dev · git.iko.soy

git.iko.soy/Idris-dev

Add %used pragma

%used function_name arg_name -- asserts that arg_name is always used by function_name. This is mostly likely to be useful in FFI things, where erasure doesn't know what is used and you want to assert that something should never be erased because a foreign call will use it.

commit8096500dfc3901b69a7079bc6e0a1d343e9202c6 authorEdwin Brady <ecb10@st-andrews.ac.uk> dateWed 28 Jan 2015, 18:46 (12 years ago) parent0011835

6 files changed+69−20

compare with master

unifiedsplit

libs/prelude/IO.idr+13−2 src/Idris/AbsSyntax.hs+20 src/Idris/AbsSyntaxTree.hs+3−1 src/Idris/Erasure.hs+13−12 src/Idris/IBC.hs+14−5 src/Idris/Parser.hs+6

libs/prelude/IO.idr+13−2

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

112112

113113--------- The C FFI

114114

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

115+data Raw : Type -> Type where

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

116121

117122-- Supported C integer types

118123data C_IntTypes : Type -> Type where

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

163168

164169-- Supported JS foreign types

165170mutual

166− data JsFn t = MkJsFn t

171+ data JsFn : Type -> Type where

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

167173

168174 data JS_IntTypes : Type -> Type where

169175 JS_IntChar : JS_IntTypes Char

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

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

183189 JS_IntT : JS_IntTypes i -> JS_Types i

184190

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+

185196FFI_JS : FFI

186197FFI_JS = MkFFI JS_Types String

187198

src/Idris/AbsSyntax.hs+20

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

125125addErrRev t = do i <- getIState

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

127127

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+

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

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

130150

src/Idris/AbsSyntaxTree.hs+3−1

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

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

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

221221 idris_postulates :: S.Set Name,

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

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

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

224225 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

294295 | IBCTotCheckErr FC String

295296 | IBCParsedRegion FC

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

298+ | IBCUsage (Name, Int)

297299 deriving Show

298300

299301-- | The initial state for the compiler

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

306308 [] [] [] defaultOpts 6 [] [] [] [] emptySyntaxRules [] [] [] [] [] [] []

307309 [] [] Nothing [] Nothing [] [] Nothing Nothing [] Hidden False [] Nothing [] []

308310 (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

310312

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

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

src/Idris/Erasure.hs+13−12

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

7676 ci <- idris_classes <$> getIState

7777 cg <- idris_callgraph <$> getIState

7878 opt <- idris_optimisation <$> getIState

79+ used <- idris_erasureUsed <$> getIState

7980

8081 -- Build the dependency graph.

81− let depMap = buildDepMap ci ctx main

82+ let depMap = buildDepMap ci used ctx main

8283

8384 -- Search for reachable nodes in the graph.

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

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

170171

171172-- Build the dependency graph,

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

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

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

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

175+buildDepMap ci used ctx mainName = addPostulates used $

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

175177 where

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

177− addPostulates :: Deps -> Deps

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

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

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

179181 where

180182 -- mini-DSL for postulates

181183 (==>) 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]

187189 usedNames = allNames deps S.\\ specialPrims

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

189191

190− postulates =

192+ postulates used =

191193 [ [] ==> concat

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

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

194196 [ [(mainName, Result)]

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

196198

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

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

201+

197202 -- MkIO is read by run__IO,

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

199204 , it "MkIO" [2]

200205 , it "prim__IO" [1]

201206

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

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

204− -- in Idris source

205− , it "MkJsFn" [1]

206− , it "MkRaw" [1]

207−

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

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

208209 , [(pairCon, Arg 2),

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

210211

src/Idris/IBC.hs+14−5

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

3535import Util.Zlib (decompressEither)

3636

3737ibcVersion :: Word8

38−ibcVersion = 94

38+ibcVersion = 95

3939

4040data IBCFile = IBCFile { ver :: Word8,

4141 sourcefile :: FilePath,

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

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

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

7979 ibc_postulates :: ![Name],

80− ibc_parsedSpan :: !(Maybe FC)

80+ ibc_parsedSpan :: !(Maybe FC),

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

8182 }

8283 deriving Show

8384{-!

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

8586!-}

8687

8788initIBC :: IBCFile

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

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

8990

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

9192 -> FilePath -> Idris ()

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

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

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

231232 _ -> ifail "IBC write failed"

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

232234

233235process :: Bool -- ^ Reexporting

234236 -> IBCFile -> FilePath -> Idris ()

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

285287 pMetavars $ force (ibc_metavars i)

286288 pPostulates $ force (ibc_postulates i)

287289 pParsedSpan $ force (ibc_parsedSpan i)

290+ pUsage $ force (ibc_usage i)

288291

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

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

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

302305pParsedSpan fc = do ist <- getIState

303306 putIState ist { idris_parsedSpan = fc }

304307

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

309+pUsage ns = do ist <- getIState

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

311+

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

306313pImportDirs fs = mapM_ addImportDir fs

307314

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

907914 return (DataMI x1)

908915

909916instance 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)

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

912919 do put x1

913920 put x2

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

950957 put x39

951958 put x40

952959 put x41

960+ put x42

953961

954962 get

955963 = do x1 <- get

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

9941002 x39 <- get

9951003 x40 <- get

9961004 x41 <- 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)

1005+ x42 <- get

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)

9981007 else return (initIBC { ver = x1 })

9991008

10001009instance Binary DataOpt where

src/Idris/Parser.hs+6

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

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

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

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

10601066 <?> "directive"

10611067 where disambiguate :: Name -> Idris Name

10621068 disambiguate n = do i <- getIState