d27925c · Idris-dev · git.iko.soy

contribs/tool-support/vim/indent/idris.vim+2−2

compare with master

unifiedsplit

@@ -111,8 +111,8 @@ function! GetIdrisIndent()

111 return match(prevline, '$namespace\|\(co$\?data\)') + &shiftwidth

112 endif

113

114− if prevline =~ '^\s*using\s\+([^(]*)\s*$'

114+ if prevline =~ '^\s*$using\|parameters$\s*([^(]*)\s*$'

115− return match(prevline, 'using') + &shiftwidth

115+ return match(prevline, '$using\|parameters$') + &shiftwidth

116 endif

117

118 return match(prevline, '\S')

contribs/tool-support/vim/syntax/idris.vim+1−1

@@ -10,7 +10,7 @@ syn match idrisModule "\<$module\|namespace$\>"

10syn match idrisImport "\<import\>"

11syn match idrisStructure "\<$class\|\(co$\?data\|instance\|where\|record\)\>"

12syn match idrisVisibility "\<$public\|abstract\|private$\>"

13−syn match idrisStatement "\<$do\|case\|of\|let\|in\|with\|total\|\|partial\|dsl\|auto\|using$\>"

14syn match idrisSyntax "$pattern \+\|term \+$\?syntax"

15syn match idrisConditional "\<$if\|then\|else$\>"

src/IRTS/Compiler.hs+1−1

@@ -170,7 +170,7 @@ instance ToIR (TT Name) where

170 [oi] -> collapsible oi

171 _ -> False

172 let unused = case lookupCtxt Nothing n (idris_callgraph i) of

173− [CGInfo _ _ _ unusedpos] -> unusedpos

173+ [CGInfo _ _ _ _ unusedpos] -> unusedpos

174 _ -> []

175 args' <- mapM (ir' env) args

176 if collapse then return LNothing

src/Idris/AbsSyntaxTree.hs+7

@@ -81,8 +81,15 @@ data IState = IState {

81 compiled_so :: Maybe String

82 }

83

84+data SizeChange = Smaller | Same | Bigger | Unknown

85+ deriving Show

86+{-!

87+deriving instance Binary SizeChange

88+!-}

89+

84data CGInfo = CGInfo { argsdef :: [Name],

90data CGInfo = CGInfo { argsdef :: [Name],

85 calls :: [(Name, [[Name]])],

91 calls :: [(Name, [[Name]])],

92+ scg :: [(Name, [[Maybe (Name, SizeChange)]])],

86 argsused :: [Name],

93 argsused :: [Name],

87 unusedpos :: [Int] }

94 unusedpos :: [Int] }

88 deriving Show

95 deriving Show

src/Idris/Coverage.hs+14−1

@@ -284,7 +284,7 @@ calcProd i fc n pats = do patsprod <- mapM prodRec pats

284 return (and argsprod)

285 prod ok (App f a) = liftM2 (&&) (prod False f) (prod False a)

286 prod ok (Bind _ (Let t v) sc) = liftM2 (&&) (prod False v) (prod False v)

287− prod ok (Bind _ b sc) = prod False sc

287+ prod ok (Bind _ b sc) = prod ok sc

288 prod ok t = return True

289

290 cotype ty

@@ -422,3 +422,16 @@ checkDeclTotality (fc, n)

422 = do logLvl 2 $ "Checking " ++ show n ++ " for totality"

423 checkTotality [] fc n

424

425+-- Calculate the size change graph for this definition

426+

427+-- SCG for a function f consists of a list of:

428+-- (g, [(a1, sizechange1), (a2, sizechange2), ..., (an, sizechangen)])

429+

430+-- where g is a function called

431+-- a1 ... an are the arguments of f in positions 1..n of g

432+-- sizechange1 ... sizechange2 is how their size has changed wrt the input to f

433+-- Nothing, if the argument is unrelated to the input

434+

435+buildSCG :: SC -> [Name] -> [(Name, [[Maybe (Name, SizeChange)]])]

436+buildSCG _ _ = []

437+

src/Idris/ElabDecls.hs+2−1

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

346 (CaseOp _ _ _ scargs sc scargs' sc' : _) ->

347 do let calls = findCalls sc' scargs'

348 let used = findUsedArgs sc' scargs'

349+ let scg = buildSCG sc scargs

349− let cg = CGInfo scargs' calls used []

350+ let cg = CGInfo scargs' calls scg used []

350 logLvl 2 $ "Called names: " ++ show cg

351 logLvl 2 $ "Called names: " ++ show cg

351 addToCG n cg

352 addToCG n cg

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

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

src/Idris/IBC.hs+20−2

@@ -263,18 +263,36 @@ pCG ds = mapM_ (\ (n, a) -> addToCG n a) ds

263

264----- Generated by 'derive'

265

266+instance Binary SizeChange where

267+ put x

268+ = case x of

269+ Smaller -> putWord8 0

270+ Same -> putWord8 1

271+ Bigger -> putWord8 2

272+ Unknown -> putWord8 3

273+ get

274+ = do i <- getWord8

275+ case i of

276+ 0 -> return Smaller

277+ 1 -> return Same

278+ 2 -> return Bigger

279+ 3 -> return Unknown

280+ _ -> error "Corrupted binary data for SizeChange"

281+

266instance Binary CGInfo where

282instance Binary CGInfo where

267− put (CGInfo x1 x2 x3 x4)

283+ put (CGInfo x1 x2 x3 x4 x5)

268 = do put x1

284 = do put x1

269 put x2

285 put x2

270 put x3

286 put x3

271 put x4

287 put x4

288+ put x5

272 get

289 get

273 = do x1 <- get

290 = do x1 <- get

274 x2 <- get

291 x2 <- get

275 x3 <- get

292 x3 <- get

276 x4 <- get

293 x4 <- get

294+ x5 <- get

277− return (CGInfo x1 x2 x3 x4)

295+ return (CGInfo x1 x2 x3 x4 x5)

278

296

279instance Binary FC where

297instance Binary FC where

280 put (FC x1 x2)

298 put (FC x1 x2)

src/Idris/UnusedArgs.hs+3−3

@@ -16,7 +16,7 @@ traceUnused :: Name -> Idris ()

16traceUnused n

17 = do i <- get

18 case lookupCtxt Nothing n (idris_callgraph i) of

19− [CGInfo args calls usedns _] ->

19+ [CGInfo args calls scg usedns _] ->

20 do let argpos = zip args [0..]

21 let fargs = concatMap (getFargpos calls) argpos

22 logLvl 3 $ show n ++ " used TRACE: " ++ show fargs

@@ -27,7 +27,7 @@ traceUnused n

27 logLvl 1 $ show n ++ " used args: " ++ show fused

28 let unusedpos = mapMaybe (getUnused fused) (zip [0..] args)

29 logLvl 1 $ show n ++ " unused args: " ++ show (args, unusedpos)

30− addToCG n (CGInfo args calls usedns unusedpos) -- updates

30+ addToCG n (CGInfo args calls scg usedns unusedpos) -- updates

31 _ -> return ()

32 where

33 getUnused fused (i,n) | n `elem` fused = Nothing

@@ -40,7 +40,7 @@ used path g j

40 = do logLvl 5 $ (show ((g, j) : path))

41 i <- get

42 case lookupCtxt Nothing g (idris_callgraph i) of

43− [CGInfo args calls usedns unused] ->

43+ [CGInfo args calls scg usedns unused] ->

44 if (j >= length args)

45 then -- overapplied, assume used

46 return True

tutorial/idris-tutorial.pdf

Binary file not shown.