d27925c · Idris-dev · git.iko.soy

git.iko.soy/Idris-dev

Merge branch 'master' of https://github.com/raichoo/Idris-dev

Conflicts: contribs/tool-support/vim/syntax/idris.vim

commitd27925c8bca0b037eaf07d9fad4b2d3ad92fed97 authorEdwin Brady <ecb10@st-andrews.ac.uk> dateWed 24 Oct 2012, 20:32 (14 years ago) parentcad5efb dc01a56

9 files changed+50−11

compare with master

unifiedsplit

contribs/tool-support/vim/indent/idris.vim+2−2 contribs/tool-support/vim/syntax/idris.vim+1−1 src/IRTS/Compiler.hs+1−1 src/Idris/AbsSyntaxTree.hs+7 src/Idris/Coverage.hs+14−1 src/Idris/ElabDecls.hs+2−1 src/Idris/IBC.hs+20−2 src/Idris/UnusedArgs.hs+3−3 tutorial/idris-tutorial.pdf

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

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

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

112112 endif

113113

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

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

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

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

116116 endif

117117

118118 return match(prevline, '\S')

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

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

1010syn match idrisImport "\<import\>"

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

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

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

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

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

src/IRTS/Compiler.hs+1−1

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

170170 [oi] -> collapsible oi

171171 _ -> False

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

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

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

174174 _ -> []

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

176176 if collapse then return LNothing

src/Idris/AbsSyntaxTree.hs+7

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

8181 compiled_so :: Maybe String

8282 }

8383

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

85+ deriving Show

86+{-!

87+deriving instance Binary SizeChange

88+!-}

89+

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

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

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

8693 argsused :: [Name],

8794 unusedpos :: [Int] }

8895 deriving Show

src/Idris/Coverage.hs+14−1

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

284284 return (and argsprod)

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

286286 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

288288 prod ok t = return True

289289

290290 cotype ty

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

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

423423 checkTotality [] fc n

424424

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

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

347347 do let calls = findCalls sc' scargs'

348348 let used = findUsedArgs sc' scargs'

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

349+ let scg = buildSCG sc scargs

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

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

351352 addToCG n cg

352353 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

263263

264264----- Generated by 'derive'

265265

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+

266282instance Binary CGInfo where

267− put (CGInfo x1 x2 x3 x4)

283+ put (CGInfo x1 x2 x3 x4 x5)

268284 = do put x1

269285 put x2

270286 put x3

271287 put x4

288+ put x5

272289 get

273290 = do x1 <- get

274291 x2 <- get

275292 x3 <- get

276293 x4 <- get

277− return (CGInfo x1 x2 x3 x4)

294+ x5 <- get

295+ return (CGInfo x1 x2 x3 x4 x5)

278296

279297instance Binary FC where

280298 put (FC x1 x2)

src/Idris/UnusedArgs.hs+3−3

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

1616traceUnused n

1717 = do i <- get

1818 case lookupCtxt Nothing n (idris_callgraph i) of

19− [CGInfo args calls usedns _] ->

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

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

2121 let fargs = concatMap (getFargpos calls) argpos

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

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

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

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

2929 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

3131 _ -> return ()

3232 where

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

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

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

4141 i <- get

4242 case lookupCtxt Nothing g (idris_callgraph i) of

43− [CGInfo args calls usedns unused] ->

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

4444 if (j >= length args)

4545 then -- overapplied, assume used

4646 return True

tutorial/idris-tutorial.pdf

Binary file not shown.