0175376 · Idris-dev · git.iko.soy

src/Idris/ASTUtils.hs+1−4

compare with master

unifiedsplit

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

118ist_callgraph :: Name -> Field IState CGInfo

119ist_callgraph n =

120 maybe_default CGInfo

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

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

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

123 }

122 }

124 . ctxt_lookup n

123 . ctxt_lookup n

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

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

126

125

127−-- some fields of the CGInfo record

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

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

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

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

130

128

131−

132-- Commandline flags

129-- Commandline flags

133--------------------

130--------------------

134

131

src/Idris/AbsSyntax.hs+9−6

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

232 = do i <- getIState

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

234

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+

235addTyInferred :: Name -> Idris ()

243addTyInferred :: Name -> Idris ()

236addTyInferred n

244addTyInferred n

237 = do i <- getIState

245 = do i <- getIState

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

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

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

329allNames ns n = do i <- getIState

337allNames ns n = do i <- getIState

330 case lookupCtxtExact n (idris_callgraph i) of

338 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')

332 return (nub (n : concat more))

340 return (nub (n : concat more))

333 _ -> return [n]

341 _ -> return [n]

334

342

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

360 [ns] -> ns

368 [ns] -> ns

361 _ -> []

369 _ -> []

362

370

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−

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

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

369addDeprecated n reason = do i <- getIState

372addDeprecated n reason = do i <- getIState

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

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

src/Idris/AbsSyntaxTree.hs+4−6

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

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

195 idris_flags :: Ctxt [FnOpt],

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

197− idris_calledgraph :: Ctxt [Name],

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

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

199 idris_moduledocs :: Ctxt (Docstring DocTerm),

198 idris_moduledocs :: Ctxt (Docstring DocTerm),

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

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

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

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

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

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

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

282

281

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

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

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

285 scg :: [SCGEntry],

283 scg :: [SCGEntry],

286− argsused :: [Name],

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

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

285+ }

288 deriving Show

286 deriving Show

289{-!

287{-!

290deriving instance Binary CGInfo

288deriving instance Binary CGInfo

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

349 emptyContext emptyContext emptyContext emptyContext

347 emptyContext emptyContext emptyContext emptyContext

350 emptyContext emptyContext emptyContext emptyContext

348 emptyContext emptyContext emptyContext emptyContext

351 emptyContext emptyContext emptyContext emptyContext

349 emptyContext emptyContext emptyContext emptyContext

352− emptyContext emptyContext

350+ emptyContext

353 [] [] [] defaultOpts 6 [] [] [] [] emptySyntaxRules [] [] [] [] [] [] []

351 [] [] [] defaultOpts 6 [] [] [] [] emptySyntaxRules [] [] [] [] [] [] []

354 [] [] Nothing [] Nothing [] [] Nothing Nothing [] Hidden False [] Nothing [] []

352 [] [] Nothing [] Nothing [] [] Nothing Nothing [] Hidden False [] Nothing [] []

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

353 (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)

313 [Partial _] ->

314 case lookupCtxt n (idris_callgraph i) of

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

316− (map fst (calls cg))

316+ (calls cg)

317 _ -> return ()

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

319checkAllCovering _ _ _ _ = return ()

src/Idris/DeepSeq.hs+3−3

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

365 rnf _ = ()

366

367instance NFData CGInfo where

368− rnf (CGInfo x1 x2 x3 x4 x5)

368+ rnf (CGInfo x1 x2 x3)

369 = rnf x1 `seq`

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

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

371

372instance NFData Fixity where

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

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

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

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

698 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)

700 = 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`

701 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`

702 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 =

249 i <- getIState

250 case lookupDef n (tt_ctxt i) of

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

252− let (scargs, sc) = cases_compiletime cd

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

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

254− do let calls = findCalls sc' scargs'

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

255− let used = findUsedArgs sc' scargs'

256 -- let scg = buildSCG i sc scargs

254 -- let scg = buildSCG i sc scargs

257 -- add SCG later, when checking totality

255 -- 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

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

260− addToCG n cg

257+ addCalls n calls

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

262 addIBC (IBCCG n)

258 addIBC (IBCCG n)

263 _ -> return ()

259 _ -> return ()

264 return ()

260 return ()

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

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

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

2550 -- thing won't be.

2551 let (scargs, sc) = cases_compiletime cd

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

2553− calls = findCalls sc' scargs

2552+ calls = map fst $ 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

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

2557− addToCG n cg

2554+ addCalls n calls

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

2559 addIBC $ IBCCG n

2555 addIBC $ IBCCG n

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

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

2561 Nothing -> return ()

2557 Nothing -> return ()

src/Idris/IBC.hs+13−10

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

40import Codec.Archive.Zip

41

42ibcVersion :: 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

44

50

45data IBCFile = IBCFile { ver :: Word16,

51data IBCFile = IBCFile { ver :: Word16,

46 sourcefile :: FilePath,

52 sourcefile :: FilePath,

53+ ibc_reachablenames :: ![Name],

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

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

48 ibc_importdirs :: ![FilePath],

55 ibc_importdirs :: ![FilePath],

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

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

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

95!-}

102!-}

96

103

97initIBC :: IBCFile

104initIBC :: IBCFile

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

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

99

106

100hasValidIBCVersion :: FilePath -> Idris Bool

107hasValidIBCVersion :: FilePath -> Idris Bool

101hasValidIBCVersion fp = do

108hasValidIBCVersion fp = do

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

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

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

764

771

765instance Binary CGInfo where

772instance Binary CGInfo where

766− put (CGInfo x1 x2 x3 x4 x5)

773+ put (CGInfo x1 x2 x3)

767 = do put x1

774 = do put x1

768− put x2

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

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

770− put x4

776+ put x3

771− put x5

772 get

777 get

773 = do x1 <- get

778 = do x1 <- get

774− x2 <- get

775− x4 <- get

776− x5 <- get

779+ x3 <- get

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

780+ return (CGInfo x1 [] x3)

778

781

779instance Binary CaseType where

782instance Binary CaseType where

780 put x = case x of

783 put x = case x of