0175376 · Idris-dev · git.iko.soy

git.iko.soy/Idris-dev

Remove some unnecessary fields

commit017537684153d6dd0b3821ce6ad674b3b542a3b2 authorEdwin Brady <ecb10@st-andrews.ac.uk> dateTue 26 Jan 2016, 22:28 (11 years ago) parentd579139

8 files changed+38−45

compare with master

unifiedsplit

src/Idris/ASTUtils.hs+1−4 src/Idris/AbsSyntax.hs+9−6 src/Idris/AbsSyntaxTree.hs+4−6 src/Idris/Coverage.hs+1−1 src/Idris/DeepSeq.hs+3−3 src/Idris/Elab/Clause.hs+4−8 src/Idris/Elab/Term.hs+3−7 src/Idris/IBC.hs+13−10

src/Idris/ASTUtils.hs+1−4

@@ -118,17 +118,14 @@ opt_detaggable = Field detaggable (\v opt -> opt{ detaggable = v })

118118ist_callgraph :: Name -> Field IState CGInfo

119119ist_callgraph n =

120120 maybe_default CGInfo

121− { argsdef = [], calls = [], scg = []

122− , argsused = [], usedpos = []

121+ { calls = [], scg = [], usedpos = []

123122 }

124123 . ctxt_lookup n

125124 . Field idris_callgraph (\v ist -> ist{ idris_callgraph = v })

126125

127−-- some fields of the CGInfo record

128126cg_usedpos :: Field CGInfo [(Int, [UsageReason])]

129127cg_usedpos = Field usedpos (\v cg -> cg{ usedpos = v })

130128

131−

132129-- Commandline flags

133130--------------------

134131

src/Idris/AbsSyntax.hs+9−6

@@ -232,6 +232,14 @@ addToCG n cg

232232 = do i <- getIState

233233 putIState $ i { idris_callgraph = addDef n cg (idris_callgraph i) }

234234

235+addCalls :: Name -> [Name] -> Idris ()

236+addCalls n calls

237+ = do i <- getIState

238+ case lookupCtxtExact n (idris_callgraph i) of

239+ Nothing -> addToCG n (CGInfo calls [] [])

240+ Just (CGInfo cs scg used) ->

241+ addToCG n (CGInfo (nub (calls ++ cs)) scg used)

242+

235243addTyInferred :: Name -> Idris ()

236244addTyInferred n

237245 = do i <- getIState

@@ -328,7 +336,7 @@ allNames :: [Name] -> Name -> Idris [Name]

328336allNames ns n | n `elem` ns = return []

329337allNames ns n = do i <- getIState

330338 case lookupCtxtExact n (idris_callgraph i) of

331− Just ns' -> do more <- mapM (allNames (n:ns)) (map fst (calls ns'))

339+ Just ns' -> do more <- mapM (allNames (n:ns)) (calls ns')

332340 return (nub (n : concat more))

333341 _ -> return [n]

334342

@@ -360,11 +368,6 @@ getNameHints i n =

360368 [ns] -> ns

361369 _ -> []

362370

363−-- Issue #1737 in the Issue Tracker.

364−-- https://github.com/idris-lang/Idris-dev/issues/1737

365−addToCalledG :: Name -> [Name] -> Idris ()

366−addToCalledG n ns = return () -- TODO

367−

368371addDeprecated :: Name -> String -> Idris ()

369372addDeprecated n reason = do i <- getIState

370373 putIState $ i { idris_deprecated = addDef n reason (idris_deprecated i) }

src/Idris/AbsSyntaxTree.hs+4−6

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

194194 -- ^ list of lhs/rhs, and a list of missing clauses

195195 idris_flags :: Ctxt [FnOpt],

196196 idris_callgraph :: Ctxt CGInfo, -- name, args used in each pos

197− idris_calledgraph :: Ctxt [Name],

198197 idris_docstrings :: Ctxt (Docstring DocTerm, [(Name, Docstring DocTerm)]),

199198 idris_moduledocs :: Ctxt (Docstring DocTerm),

200199 -- ^ module documentation is saved in a special MN so the context

@@ -280,11 +279,10 @@ deriving instance NFData SizeChange

280279type SCGEntry = (Name, [Maybe (Int, SizeChange)])

281280type UsageReason = (Name, Int) -- fn_name, its_arg_number

282281

283−data CGInfo = CGInfo { argsdef :: [Name],

284− calls :: [(Name, [[Name]])],

282+data CGInfo = CGInfo { calls :: [Name],

285283 scg :: [SCGEntry],

286− argsused :: [Name],

287− usedpos :: [(Int, [UsageReason])] }

284+ usedpos :: [(Int, [UsageReason])]

285+ }

288286 deriving Show

289287{-!

290288deriving instance Binary CGInfo

@@ -349,7 +347,7 @@ idrisInit = IState initContext S.empty []

349347 emptyContext emptyContext emptyContext emptyContext

350348 emptyContext emptyContext emptyContext emptyContext

351349 emptyContext emptyContext emptyContext emptyContext

352− emptyContext emptyContext

350+ emptyContext

353351 [] [] [] defaultOpts 6 [] [] [] [] emptySyntaxRules [] [] [] [] [] [] []

354352 [] [] Nothing [] Nothing [] [] Nothing Nothing [] Hidden False [] Nothing [] []

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

src/Idris/Coverage.hs+1−1

@@ -313,7 +313,7 @@ checkAllCovering fc done top n | not (n `elem` done)

313313 [Partial _] ->

314314 case lookupCtxt n (idris_callgraph i) of

315315 [cg] -> mapM_ (checkAllCovering fc (n : done) top)

316− (map fst (calls cg))

316+ (calls cg)

317317 _ -> return ()

318318 x -> return () -- stop if total

319319checkAllCovering _ _ _ _ = return ()

src/Idris/DeepSeq.hs+3−3

@@ -365,9 +365,9 @@ instance NFData LogCat where

365365 rnf _ = ()

366366

367367instance NFData CGInfo where

368− rnf (CGInfo x1 x2 x3 x4 x5)

368+ rnf (CGInfo x1 x2 x3)

369369 = rnf x1 `seq`

370− rnf x2 `seq` rnf x3 `seq` rnf x4 `seq` rnf x5 `seq` ()

370+ rnf x2 `seq` rnf x3 `seq` ()

371371

372372instance NFData Fixity where

373373 rnf (Infixl x1) = rnf x1 `seq` ()

@@ -696,7 +696,7 @@ instance NFData IState where

696696 rnf (IState x1 x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 x15 x16 x17 x18 x19 x20

697697 x21 x22 x23 x24 x25 x26 x27 x28 x29 x30 x31 x32 x33 x34 x35 x36 x37 x38 x39 x40

698698 x41 x42 x43 x44 x45 x46 x47 x48 x49 x50 x51 x52 x53 x54 x55 x56 x57 x58 x59 x60

699− x61 x62 x63 x64 x65 x66 x67 x68 x69 x70 x71 x72 x73 x74 x75)

699+ x61 x62 x63 x64 x65 x66 x67 x68 x69 x70 x71 x72 x73 x74)

700700 = rnf x1 `seq` rnf x2 `seq` rnf x3 `seq` rnf x4 `seq` rnf x5 `seq` rnf x6 `seq` rnf x7 `seq` rnf x8 `seq` rnf x9 `seq` rnf x10 `seq` () `seq` rnf x11 `seq` rnf x12 `seq` rnf x13 `seq` rnf x14 `seq` rnf x15 `seq` rnf x16 `seq` rnf x17 `seq` rnf x18 `seq` rnf x19 `seq` rnf x20 `seq`

701701 rnf x21 `seq` rnf x22 `seq` rnf x23 `seq` rnf x24 `seq` rnf x25 `seq` rnf x26 `seq` rnf x27 `seq` rnf x28 `seq` rnf x29 `seq` rnf x30 `seq` rnf x31 `seq` rnf x32 `seq` rnf x33 `seq` rnf x34 `seq` rnf x35 `seq` rnf x36 `seq` rnf x37 `seq` rnf x38 `seq` rnf x39 `seq` rnf x40 `seq`

702702 rnf x41 `seq` rnf x42 `seq` rnf x43 `seq` rnf x44 `seq` rnf x45 `seq` rnf x46 `seq` rnf x47 `seq` rnf x48 `seq` rnf x49 `seq` rnf x50 `seq` rnf x51 `seq` rnf x52 `seq` rnf x53 `seq` rnf x54 `seq` rnf x55 `seq` rnf x56 `seq` rnf x57 `seq` rnf x58 `seq` rnf x59 `seq` rnf x60 `seq`

src/Idris/Elab/Clause.hs+4−8

@@ -249,16 +249,12 @@ elabClauses info' fc opts n_in cs =

249249 i <- getIState

250250 case lookupDef n (tt_ctxt i) of

251251 (CaseOp _ _ _ _ _ cd : _) ->

252− let (scargs, sc) = cases_compiletime cd

253− (scargs', sc') = cases_runtime cd in

254− do let calls = findCalls sc' scargs'

255− let used = findUsedArgs sc' scargs'

252+ let (scargs, sc) = cases_compiletime cd in

253+ do let calls = map fst $ findCalls sc scargs

256254 -- let scg = buildSCG i sc scargs

257255 -- add SCG later, when checking totality

258− let cg = CGInfo scargs' calls [] used [] -- TODO: remove this, not needed anymore

259− logElab 2 $ "Called names: " ++ show cg

260− addToCG n cg

261− addToCalledG n (nub (map fst calls)) -- plus names in type!

256+ logElab 2 $ "Called names: " ++ show calls

257+ addCalls n calls

262258 addIBC (IBCCG n)

263259 _ -> return ()

264260 return ()

src/Idris/Elab/Term.hs+3−7

@@ -2549,13 +2549,9 @@ processTacticDecls info steps =

25492549 -- we refer to, so that if they aren't total, the whole

25502550 -- thing won't be.

25512551 let (scargs, sc) = cases_compiletime cd

2552− (scargs', sc') = cases_runtime cd

2553− calls = findCalls sc' scargs

2554− used = findUsedArgs sc' scargs'

2555− cg = CGInfo scargs' calls [] used []

2556− in do logElab 2 $ "Called names in reflected elab: " ++ show cg

2557− addToCG n cg

2558− addToCalledG n (nub (map fst calls))

2552+ calls = map fst $ findCalls sc scargs

2553+ in do logElab 2 $ "Called names in reflected elab: " ++ show calls

2554+ addCalls n calls

25592555 addIBC $ IBCCG n

25602556 Just _ -> return () -- TODO throw internal error

25612557 Nothing -> return ()

src/Idris/IBC.hs+13−10

@@ -40,10 +40,17 @@ import System.Directory

4040import Codec.Archive.Zip

4141

4242ibcVersion :: Word16

43−ibcVersion = 128

43+ibcVersion = 129

44+

45+-- When IBC is being loaded - we'll load different things (and omit different

46+-- structures/definitions) depending on which phase we're in

47+data IBCPhase = IBC_Building -- ^ when building the module tree

48+ | IBC_REPL -- ^ when loading modules for the REPL

49+ | IBC_IDE -- ^ when running in IDE mode

4450

4551data IBCFile = IBCFile { ver :: Word16,

4652 sourcefile :: FilePath,

53+ ibc_reachablenames :: ![Name],

4754 ibc_imports :: ![(Bool, FilePath)],

4855 ibc_importdirs :: ![FilePath],

4956 ibc_implicits :: ![(Name, [PArg])],

@@ -95,7 +102,7 @@ deriving instance Binary IBCFile

95102!-}

96103

97104initIBC :: IBCFile

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

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

99106

100107hasValidIBCVersion :: FilePath -> Idris Bool

101108hasValidIBCVersion fp = do

@@ -763,18 +770,14 @@ instance Binary SizeChange where

763770 _ -> error "Corrupted binary data for SizeChange"

764771

765772instance Binary CGInfo where

766− put (CGInfo x1 x2 x3 x4 x5)

773+ put (CGInfo x1 x2 x3)

767774 = do put x1

768− put x2

769775-- put x3 -- Already used SCG info for totality check

770− put x4

771− put x5

776+ put x3

772777 get

773778 = do x1 <- get

774− x2 <- get

775− x4 <- get

776− x5 <- get

777− return (CGInfo x1 x2 [] x4 x5)

779+ x3 <- get

780+ return (CGInfo x1 [] x3)

778781

779782instance Binary CaseType where

780783 put x = case x of