c4e039e · Idris-dev · git.iko.soy

.travis.yml+2−2

@@ -8,8 +8,8 @@ env:

88

99matrix:

1010 include:

11− - env: STYLISH=YES

12− addons: {apt: {packages: [ghc-8.0.1], sources: [hvr-ghc]}}

11+ - env: CABALVER="1.24" GHCVER="8.0.1" STACKVER="7.14" STYLISH=YES

12+ addons: {apt: {packages: [cabal-install-1.24,ghc-8.0.1,hscolour], sources: [hvr-ghc]}}

1313 - os: osx

1414 env: CABALVER="1.24" GHCVER="8.0.1" TESTS="test_c"

1515 compiler: ": #GHC 8.0.1"

main/Main.hs+6−6

@@ -1,10 +1,10 @@

11module Main where

22

3−import System.Exit ( ExitCode(..), exitWith, exitSuccess )

3+import System.Exit (ExitCode(..), exitSuccess, exitWith)

44

5−import Control.Monad ( unless, when, (>=>) )

6−import Data.Maybe ( fromMaybe )

7−import Data.Foldable ( foldrM )

5+import Control.Monad (unless, when, (>=>))

6+import Data.Foldable (foldrM)

7+import Data.Maybe (fromMaybe)

88

99import Idris.AbsSyntax

1010import Idris.CmdOptions

@@ -15,8 +15,8 @@ import Idris.Package

1515

1616import Util.System (setupBundledCC)

1717

18−import Util.System ( setupBundledCC )

19−import System.Exit ( ExitCode(..), exitWith)

18+import System.Exit (ExitCode(..), exitWith)

19+import Util.System (setupBundledCC)

2020

2121processShowOptions :: [Opt] -> Idris ()

2222processShowOptions opts = runIO $ do

src/Idris/AbsSyntaxTree.hs+2−2

@@ -1843,11 +1843,11 @@ pprintPTerm ppo bnd docArgs infixes = prettySe (ppopt_depth ppo) startPrec bnd

18431843 kwd "let" <+> (group . align . hang 2 $ prettyBindingOf n False <+> text "=" <$> prettySe (decD d) startPrec bnd v) </>

18441844 kwd "in" <+> (group . align . hang 2 $ prettySe (decD d) startPrec ((n, False):bnd) sc)

18451845 prettySe d p bnd (PPi (Exp l s _ rig) n _ ty sc)

1846− | Rig0 <- rig =

1846+ | Rig0 <- rig =

18471847 depth d . bracket p startPrec . group $

18481848 enclose lparen rparen (group . align $ text "0" <+> prettyBindingOf n False <+> colon <+> prettySe (decD d) startPrec bnd ty) <+>

18491849 st <> text "->" <$> prettySe (decD d) startPrec ((n, False):bnd) sc

1850− | Rig1 <- rig =

1850+ | Rig1 <- rig =

18511851 depth d . bracket p startPrec . group $

18521852 enclose lparen rparen (group . align $ text "1" <+> prettyBindingOf n False <+> colon <+> prettySe (decD d) startPrec bnd ty) <+>

18531853 st <> text "->" <$> prettySe (decD d) startPrec ((n, False):bnd) sc

src/Idris/Core/CaseTree.hs+5−5

@@ -174,7 +174,7 @@ findCalls' ignoreasserts sc topargs = S.toList $ nu' topargs sc where

174174 then S.empty

175175 else if n `elem` ps

176176 then S.union (nut ps f) (nut ps a)

177− else S.insert (n, map argNames args)

177+ else S.insert (n, map argNames args)

178178 (S.unions $ map (nut ps) args)

179179 | (P (TCon _ _) n _, _) <- unApply fn = S.empty

180180 | otherwise = S.union (nut ps f) (nut ps a)

@@ -245,7 +245,7 @@ runCaseBuilder :: ErasureInfo -> CaseBuilder a -> (CS -> (a, CS))

245245runCaseBuilder ei bld = runState $ runReaderT bld ei

246246

247247data Phase = CoverageCheck [Int] -- list of positions explicitly given

248− | CompileTime

248+ | CompileTime

249249 | RunTime

250250 deriving (Show, Eq)

251251

@@ -253,7 +253,7 @@ data Phase = CoverageCheck [Int] -- list of positions explicitly given

253253-- Work Right to Left

254254

255255simpleCase :: Bool -> SC -> Bool ->

256− Phase -> FC ->

256+ Phase -> FC ->

257257 -- Following two can be empty lists when Phase = CoverageCheck

258258 [Int] -> -- Inaccessible argument positions

259259 [(Type, Bool)] -> -- (Argument type, whether it's canonical)

@@ -444,7 +444,7 @@ order :: Phase -> [(Name, Bool)] -> [Clause] -> [Bool] -> ([Name], [Clause])

444444-- order CompileTime ns cs _ = (map fst ns, cs)

445445order _ [] cs cans = ([], cs)

446446order _ ns' [] cans = (map fst ns', [])

447−order (CoverageCheck pos) ns' cs cans

447+order (CoverageCheck pos) ns' cs cans

448448 = let ns_out = pick 0 [] (map fst ns')

449449 cs_out = map pickClause cs in

450450 (ns_out, cs_out)

@@ -454,7 +454,7 @@ order (CoverageCheck pos) ns' cs cans

454454 -- Order the list so that things in a position in 'pos' are in the first

455455 -- part, then all the other things later. Otherwise preserve order.

456456 pick i skipped [] = reverse skipped

457− pick i skipped (x : xs)

457+ pick i skipped (x : xs)

458458 | i `elem` pos = x : pick (i + 1) skipped xs

459459 | otherwise = pick (i + 1) (x : skipped) xs

460460

src/Idris/Core/Evaluate.hs+6−6

@@ -144,7 +144,7 @@ specialise ctxt env limits t

144144 (tm, limited st)

145145

146146-- | Like normalise, but we only reduce functions that are marked as okay to

147−-- inline, and lets

147+-- inline, and lets

148148simplify :: Context -> Env -> TT Name -> TT Name

149149simplify ctxt env t

150150 = evalState (do val <- eval False ctxt [(sUN "lazy", 0),

@@ -160,7 +160,7 @@ simplify ctxt env t

160160 quote 0 val) initEval

161161

162162-- | Like simplify, but we only reduce functions that are marked as okay to

163−-- inline, and don't reduce lets

163+-- inline, and don't reduce lets

164164inlineSmall :: Context -> Env -> TT Name -> TT Name

165165inlineSmall ctxt env t

166166 = evalState (do val <- eval False ctxt []

@@ -229,7 +229,7 @@ usable False uf depthlimit n ns

229229 = case lookup n ns of

230230 Just 0 -> return (False, ns)

231231 Just i -> return $ (True, (n, abs (i-1)) : filter (\ (n', _) -> n/=n') ns)

232− _ -> return $ if uf

232+ _ -> return $ if uf

233233 then (False, ns)

234234 else (True, (n, depthlimit) : filter (\ (n', _) -> n/=n') ns)

235235

@@ -1181,14 +1181,14 @@ linearCheck ctxt t = checkArgs t

11811181 checkArgs (Bind n (Pi RigW _ ty _) sc)

11821182 = do linearCheckArg ctxt ty

11831183 checkArgs (substV (P Bound n Erased) sc)

1184− checkArgs (Bind n (Pi _ _ _ _) sc)

1184+ checkArgs (Bind n (Pi _ _ _ _) sc)

11851185 = checkArgs (substV (P Bound n Erased) sc)

11861186 checkArgs _ = return ()

11871187

11881188linearCheckArg :: Context -> Type -> TC ()

11891189linearCheckArg ctxt ty = mapM_ checkNameOK (allTTNames ty)

11901190 where

1191− checkNameOK f

1191+ checkNameOK f

11921192 = case lookupRigCountExact f ctxt of

11931193 Just Rig1 ->

11941194 tfail $ Msg $ show f ++ " can only appear in a linear binding"

@@ -1197,7 +1197,7 @@ linearCheckArg ctxt ty = mapM_ checkNameOK (allTTNames ty)

11971197 checkArgs (Bind n (Pi RigW _ ty _) sc)

11981198 = do mapM_ checkNameOK (allTTNames ty)

11991199 checkArgs (substV (P Bound n Erased) sc)

1200− checkArgs (Bind n (Pi _ _ _ _) sc)

1200+ checkArgs (Bind n (Pi _ _ _ _) sc)

12011201 = checkArgs (substV (P Bound n Erased) sc)

12021202 checkArgs _ = return ()

12031203

src/Idris/Core/ProofState.hs+3−3

@@ -1003,14 +1003,14 @@ updateProblems ps updates probs = rec 10 updates probs

10031003 updateEnv ns env, updateError ns err, fc, fa)

10041004

10051005orderUpdateSolved :: [(Name, Term)] -> ProofTerm -> (ProofTerm, [Name])

1006−orderUpdateSolved ns tm = update [] ns tm

1006+orderUpdateSolved ns tm = update [] ns tm

10071007 where

10081008 update done [] t = (t, done)

10091009 update done ((n, P _ n' _) : ns) t | n == n' = update done ns t

10101010 update done (n : ns) t = update (fst n : done)

10111011 (map (updateMatch n) ns)

10121012 (updateSolved [n] t)

1013−

1013+

10141014 -- Update the later solutions too

10151015 updateMatch n (x, tm) = (x, updateSolvedTerm [n] tm)

10161016

@@ -1094,7 +1094,7 @@ processTactic (MatchProblems all) ps

10941094 return (ps { pterm = pterm', solved = Nothing, problems = probs'',

10951095 previous = Just ps, plog = "",

10961096 notunified = updateNotunified ns'' (notunified ps),

1097− recents = recents ps ++ dropped,

1097+ recents = recents ps ++ dropped,

10981098 holes = holes ps \\ dropped }, plog ps)

10991099processTactic t ps

11001100 = case holes ps of

src/Idris/Core/Typecheck.hs+11−11

@@ -12,8 +12,8 @@ Maintainer : The Idris Community.

1212module Idris.Core.Typecheck where

1313

1414import Idris.Core.Evaluate

15−import Idris.Core.WHNF

1615import Idris.Core.TT

16+import Idris.Core.WHNF

1717

1818import Control.Monad.State

1919import qualified Data.Vector.Unboxed as V (length)

@@ -87,8 +87,8 @@ check ctxt env tm

8787 = evalStateT (check' True [] ctxt env tm) (0, [])

8888

8989check' :: Bool -> String -> Context -> Env -> Raw -> StateT UCs TC (Term, Type)

90−check' holes tcns ctxt env top

91− = do (tm, ty, _) <- chk Rig1 (TType (UVar tcns (-5))) Nothing env top

90+check' holes tcns ctxt env top

91+ = do (tm, ty, _) <- chk Rig1 (TType (UVar tcns (-5))) Nothing env top

9292 return (tm, ty)

9393 where

9494

@@ -106,7 +106,7 @@ check' holes tcns ctxt env top

106106 Maybe UExp -> -- universe for kind

107107 Env -> Raw -> StateT UCs TC (Term, Type, [Name])

108108 chk rigc u lvl env (Var n)

109− | Just (i, erig, ty) <- lookupTyEnv n env

109+ | Just (i, erig, ty) <- lookupTyEnv n env

110110 = case rigSafe holes erig rigc n of

111111 Nothing -> return (P Bound n ty, ty, used rigc n)

112112 Just msg -> lift $ tfail $ Msg msg

@@ -151,13 +151,13 @@ check' holes tcns ctxt env top

151151 t -> lift $ tfail $ NonFunctionType fv fty

152152 chk rigc u lvl env ap@(RApp f a)

153153 = do (fv, fty, fns) <- chk rigc u Nothing env f

154− let (rigf, fty') =

154+ let (rigf, fty') =

155155 case uniqueBinders (map fstEnv env) (finalise fty) of

156156 ty@(Bind x (Pi rig i s k) t) -> (rig, ty)

157157 _ -> case normalise ctxt env fty of

158− ty@(Bind x (Pi rig i s k) t) ->

158+ ty@(Bind x (Pi rig i s k) t) ->

159159 (rig, uniqueBinders (map fstEnv env) ty)

160− _ -> (RigW, uniqueBinders (map fstEnv env)

160+ _ -> (RigW, uniqueBinders (map fstEnv env)

161161 (normalise ctxt env fty)) -- This is an error, caught below...

162162 (av, aty, ans) <- chk (rigMult rigc rigf) u Nothing env a

163163 case fty' of

@@ -198,7 +198,7 @@ check' holes tcns ctxt env top

198198 constType _ = TType (UVal 0)

199199 chk rigc u lvl env (RBind n (Pi rig i s k) t)

200200 = do (sv, st, sns) <- chk Rig0 u Nothing (envZero env) s

201− when (rig == RigW) $

201+ when (rig == RigW) $

202202 lift $ linearCheckArg ctxt (normalise ctxt env sv)

203203 (v, cs) <- get

204204 (kv, kt, _) <- chk Rig0 u Nothing (envZero env) k -- no need to validate these constraints, they are independent

@@ -256,10 +256,10 @@ check' holes tcns ctxt env top

256256

257257 checkUsageOK Rig0 _ = return ()

258258 checkUsageOK RigW _ = return ()

259− checkUsageOK Rig1 ns

259+ checkUsageOK Rig1 ns

260260 = let used = length (filter (==n) ns) in

261261 if used == 1 then return ()

262− else lift $ tfail $ Msg $ "There are " ++ (show used) ++

262+ else lift $ tfail $ Msg $ "There are " ++ (show used) ++

263263 " uses of linear name " ++ show n

264264

265265 checkBinder (Lam rig t)

@@ -269,7 +269,7 @@ check' holes tcns ctxt env top

269269 return (Lam rig tv, tt, [])

270270 checkBinder (Let t v)

271271 = do (tv, tt, _) <- chk Rig0 u Nothing (envZero env) t

272− -- May have multiple uses, check at RigW

272+ -- May have multiple uses, check at RigW

273273 -- (or rather, like an application of a lambda, multiply)

274274 -- (Consider: adding a single use let?)

275275 (vv, vt, vns) <- chk (rigMult rigc RigW) u Nothing env v

src/Idris/Core/WHNF.hs+8−8

@@ -55,13 +55,13 @@ data WHNF = WDCon Int Int Bool Name (Term, WEnv) -- ^ data constructor

5555whnf :: Context -> Env -> Term -> Term

5656-- whnf ctxt env tm = let res = whnf' ctxt env tm in

5757-- trace (show tm ++ "\n==>\n" ++ show res ++ "\n") res

58−whnf ctxt env tm =

58+whnf ctxt env tm =

5959 inlineSmall ctxt env $ -- reduce small things in body. This is primarily

6060 -- to get rid of any noisy "assert_smaller/assert_total"

6161 -- and evaluate any simple operators, which makes things

6262 -- easier to read.

6363 whnf' ctxt env tm

64−whnf' ctxt env tm =

64+whnf' ctxt env tm =

6565 quote (do_whnf ctxt (map finalEntry env) (finalise tm))

6666

6767-- | Reduce a type so that all arguments are expanded

@@ -72,8 +72,8 @@ whnfArgs' ctxt env tm

7272 -- The assumption is that de Bruijn indices refer to local things

7373 -- (so not in the external environment) so we need to instantiate

7474 -- the name

75− Bind n b@(Pi rig _ ty _) sc ->

76− Bind n b (whnfArgs' ctxt ((n, rig, b):env)

75+ Bind n b@(Pi rig _ ty _) sc ->

76+ Bind n b (whnfArgs' ctxt ((n, rig, b):env)

7777 (subst n (P Bound n ty) sc))

7878 res -> tm

7979

@@ -96,7 +96,7 @@ do_whnf ctxt genv tm = eval (WEnv 0 []) [] tm

9696 =let n' = uniqueName n (map fstEnv genv) in

9797 WBind n' (fmap (\t -> (t, wenv)) b) (sc, WEnv (d + 1) env)

9898

99− eval env stk (P nt n ty)

99+ eval env stk (P nt n ty)

100100 | Just (Let t v) <- lookupBinder n genv = eval env stk v

101101 eval env stk (P nt n ty) = apply env nt n ty stk

102102 eval env stk (App _ f a) = eval env ((a, env) : stk) f

@@ -112,7 +112,7 @@ do_whnf ctxt genv tm = eval (WEnv 0 []) [] tm

112112 eval env stk (UType u) = unload (WUType u) stk

113113

114114 apply :: WEnv -> NameType -> Name -> Type -> Stack -> WHNF

115− apply env nt n ty stk

115+ apply env nt n ty stk

116116 = let wp = case nt of

117117 DCon t a u -> WDCon t a u n (ty, env)

118118 TCon t a -> WTCon t a n (ty, env)

@@ -122,7 +122,7 @@ do_whnf ctxt genv tm = eval (WEnv 0 []) [] tm

122122 if not (tcReducible n ctxt)

123123 then unload wp stk

124124 else case lookupDefAccExact n False ctxt of

125− Just (CaseOp ci _ _ _ _ cd, acc)

125+ Just (CaseOp ci _ _ _ _ cd, acc)

126126 | acc == Public || acc == Hidden ->

127127 let (ns, tree) = cases_compiletime cd in

128128 case evalCase env ns tree stk of

@@ -230,7 +230,7 @@ quote (WDCon t a u n (ty, env)) = P (DCon t a u) n (quoteEnv env ty)

230230quote (WTCon t a n (ty, env)) = P (TCon t a) n (quoteEnv env ty)

231231quote (WPRef n (ty, env)) = P Ref n (quoteEnv env ty)

232232quote (WV i) = V i

233−quote (WBind n b (sc, env)) = Bind n (fmap (\ (t, env) -> quoteEnv env t) b)

233+quote (WBind n b (sc, env)) = Bind n (fmap (\ (t, env) -> quoteEnv env t) b)

234234 (quoteEnv env sc)

235235quote (WApp f (a, env)) = App Complete (quote f) (quoteEnv env a)

236236quote (WConstant c) = Constant c

src/Idris/Coverage.hs+31−31

@@ -62,30 +62,30 @@ mkPatTm t = do i <- getIState

6262--

6363-- This will only work after the given clauses have been typechecked and the

6464-- names are fully explicit!

65−genClauses :: FC -> Name -> [([Name], Term)] -> -- (Argument names, LHS)

65+genClauses :: FC -> Name -> [([Name], Term)] -> -- (Argument names, LHS)

6666 [PTerm] -> Idris [PTerm]

6767-- No clauses (only valid via elab reflection). We should probably still do

6868-- a check here somehow, e.g. that one of the arguments is an obviously

6969-- empty type. In practice, this should only really be used for Void elimination.

70−genClauses fc n lhs_tms [] = return []

70+genClauses fc n lhs_tms [] = return []

7171genClauses fc n lhs_tms given

7272 = do i <- getIState

73−

74− let lhs_given = zipWith removePlaceholders lhs_tms

73+

74+ let lhs_given = zipWith removePlaceholders lhs_tms

7575 (map (stripUnmatchable i) (map flattenArgs given))

76−

76+

7777 logCoverage 5 $ "Building coverage tree for:\n" ++ showSep "\n" (map show (lhs_given))

7878 let givenpos = mergePos (map getGivenPos given)

7979

80− (cns, ctree_in) <-

80+ (cns, ctree_in) <-

8181 case simpleCase False (UnmatchedCase "Undefined") False

8282 (CoverageCheck givenpos) emptyFC [] []

83− lhs_given

83+ lhs_given

8484 (const []) of

8585 OK (CaseDef cns ctree_in _) ->

8686 return (cns, ctree_in)

8787 Error e -> tclift $ tfail $ At fc e

88−

88+

8989 let ctree = trimOverlapping (addMissingCons i ctree_in)

9090 let (coveredas, missingas) = mkNewClauses (tt_ctxt i) n cns ctree

9191 let covered = map (\t -> delab' i t True True) coveredas

@@ -94,9 +94,9 @@ genClauses fc n lhs_tms given

9494

9595 logCoverage 5 $ "Coverage from case tree for " ++ show n ++ ": " ++ show ctree

9696 logCoverage 2 $ show (length missing) ++ " missing clauses for " ++ show n

97− logCoverage 3 $ "Missing clauses:\n" ++ showSep "\n"

97+ logCoverage 3 $ "Missing clauses:\n" ++ showSep "\n"

9898 (map showTmImpls missing)

99− logCoverage 10 $ "Covered clauses:\n" ++ showSep "\n"

99+ logCoverage 10 $ "Covered clauses:\n" ++ showSep "\n"

100100 (map showTmImpls covered)

101101 return missing

102102 where

@@ -132,16 +132,16 @@ removePlaceholders (ns, tm) ptm = (ns, rp tm ptm, Erased)

132132 | (tf, [tyl, tyr, tl, tr]) <- unApply tm

133133 = let tl' = rp tl pl

134134 tr' = rp tr pr in

135− mkApp tf [Erased, Erased, tl', tr']

135+ mkApp tf [Erased, Erased, tl', tr']

136136 rp tm (PDPair _ _ _ pl pt pr)

137137 | (tf, [tyl, tyr, tl, tr]) <- unApply tm

138138 = let tl' = rp tl pl

139139 tr' = rp tr pr in

140− mkApp tf [Erased, Erased, tl', tr']

140+ mkApp tf [Erased, Erased, tl', tr']

141141 rp tm _ = tm

142142

143143mkNewClauses :: Context -> Name -> [Name] -> SC -> ([Term], [Term])

144−mkNewClauses ctxt fn ns sc

144+mkNewClauses ctxt fn ns sc

145145 = (map (mkPlApp (P Ref fn Erased)) $

146146 mkFromSC True (map (\n -> P Ref n Erased) ns) sc,

147147 map (mkPlApp (P Ref fn Erased)) $

@@ -149,7 +149,7 @@ mkNewClauses ctxt fn ns sc

149149 where

150150 mkPlApp f args = mkApp f (map erasePs args)

151151

152− erasePs ap@(App t f a)

152+ erasePs ap@(App t f a)

153153 | (f, args) <- unApply ap = mkApp f (map erasePs args)

154154 erasePs (P _ n _) | not (isConName n ctxt) = Erased

155155 erasePs tm = tm

@@ -157,16 +157,16 @@ mkNewClauses ctxt fn ns sc

157157 mkFromSC cov args sc = evalState (mkFromSC' cov args sc) []

158158

159159 mkFromSC' :: Bool -> [Term] -> SC -> State [[Term]] [[Term]]

160− mkFromSC' cov args (STerm _)

160+ mkFromSC' cov args (STerm _)

161161 = if cov then return [args] else return [] -- leaf of provided case

162− mkFromSC' cov args (UnmatchedCase _)

162+ mkFromSC' cov args (UnmatchedCase _)

163163 = if cov then return [] else return [args] -- leaf of missing case

164164 mkFromSC' cov args ImpossibleCase = return []

165165 mkFromSC' cov args (Case _ x alts)

166166 = do done <- get

167167 if (args `elem` done)

168168 then return []

169− else do alts' <- mapM (mkFromAlt cov args x) alts

169+ else do alts' <- mapM (mkFromAlt cov args x) alts

170170 put (args : done)

171171 return (concat alts')

172172 mkFromSC' cov args _ = return [] -- Should never happen

@@ -178,7 +178,7 @@ mkNewClauses ctxt fn ns sc

178178 args' = map (subst x argrep) args in

179179 mkFromSC' cov args' sc

180180 mkFromAlt cov args x (ConstCase c sc)

181− = let argrep = Constant c

181+ = let argrep = Constant c

182182 args' = map (subst x argrep) args in

183183 mkFromSC' cov args' sc

184184 mkFromAlt cov args x (DefaultCase sc)

@@ -195,18 +195,18 @@ addMissingConsSt :: IState -> SC -> State Int SC

195195addMissingConsSt ist (Case t n alts) = liftM (Case t n) (addMissingAlts n alts)

196196 where

197197 addMissingAlt :: CaseAlt -> State Int CaseAlt

198− addMissingAlt (ConCase n i ns sc)

198+ addMissingAlt (ConCase n i ns sc)

199199 = liftM (ConCase n i ns) (addMissingConsSt ist sc)

200− addMissingAlt (FnCase n ns sc)

200+ addMissingAlt (FnCase n ns sc)

201201 = liftM (FnCase n ns) (addMissingConsSt ist sc)

202− addMissingAlt (ConstCase c sc)

202+ addMissingAlt (ConstCase c sc)

203203 = liftM (ConstCase c) (addMissingConsSt ist sc)

204− addMissingAlt (SucCase n sc)

204+ addMissingAlt (SucCase n sc)

205205 = liftM (SucCase n) (addMissingConsSt ist sc)

206− addMissingAlt (DefaultCase sc)

206+ addMissingAlt (DefaultCase sc)

207207 = liftM DefaultCase (addMissingConsSt ist sc)

208208

209− addMissingAlts argn as

209+ addMissingAlts argn as

210210-- | any hasDefault as = map addMissingAlt as

211211 | cons@(n:_) <- mapMaybe collectCons as,

212212 Just tyn <- getConType n,

@@ -226,7 +226,7 @@ addMissingConsSt ist (Case t n alts) = liftM (Case t n) (addMissingAlts n alts)

226226 addCases missing (DefaultCase rhs : rest)

227227 = do missing' <- mapM (genMissingAlt rhs) missing

228228 return (mapMaybe id missing' ++ rest)

229− addCases missing (c : rest)

229+ addCases missing (c : rest)

230230 = liftM (c :) $ addCases missing rest

231231

232232 addCons missing [] = []

@@ -258,7 +258,7 @@ addMissingConsSt ist (Case t n alts) = liftM (Case t n) (addMissingAlts n alts)

258258 case unApply (getRetTy (normalise (tt_ctxt ist) [] ty)) of

259259 (P _ tyn _, _) -> Just tyn

260260 _ -> Nothing

261−

261+

262262 -- for every constant in a term (at any level) take next one to make sure

263263 -- that constants which are not explicitly handled are covered

264264 nextConst (I c) = I (c + 1)

@@ -312,7 +312,7 @@ trimOverlapping sc = trim [] [] sc

312312 substMatch ca (_:cs) = substMatch ca cs

313313

314314 substNames [] sc = sc

315− substNames ((n, n') : ns) sc

315+ substNames ((n, n') : ns) sc

316316 = substNames ns (substSC n n' sc)

317317

318318 notConMatch cs (ConCase cn t args sc) = cn `notElem` cs

@@ -358,14 +358,14 @@ recoverableCoverage ctxt (CantUnify r (topx, _) (topy, _) e _ _)

358358 -- The state is a mapping of name to what it has failed to unify

359359 -- with

360360 checkRec :: Term -> Term -> State [(Name, Term)] Bool

361− checkRec (P Bound x _) tm

361+ checkRec (P Bound x _) tm

362362 | (P yt _ _, _) <- unApply tm,

363363 conType yt = do nmap <- get

364364 case lookup x nmap of

365365 Nothing -> do put ((x, tm) : nmap)

366366 return True

367367 Just y' -> checkRec tm y'

368− checkRec tm (P Bound y _)

368+ checkRec tm (P Bound y _)

369369 | (P xt _ _, _) <- unApply tm,

370370 conType xt = do nmap <- get

371371 case lookup y nmap of

@@ -379,13 +379,13 @@ recoverableCoverage ctxt (CantUnify r (topx, _) (topy, _) e _ _)

379379 (f', as') <- unApply fa'

380380 = if (length as /= length as')

381381 then checkRec f f'

382− else checkRecs (f : as) (f' : as')

382+ else checkRecs (f : as) (f' : as')

383383 where

384384 checkRecs [] [] = return True

385385 checkRecs (a : as) (b : bs) = do aok <- checkRec a b

386386 asok <- checkRecs as bs

387387 return (aok && asok)

388− checkRec (P xt x _) (P yt y _)

388+ checkRec (P xt x _) (P yt y _)

389389 | x == y = return True

390390 | ntRec xt yt = return True

391391 checkRec _ _ = return False

src/Idris/Elab/Clause.hs+28−28

@@ -14,9 +14,9 @@ import Idris.Core.CaseTree

1414import Idris.Core.Elaborate hiding (Tactic(..))

1515import Idris.Core.Evaluate

1616import Idris.Core.Execute

17−import Idris.Core.WHNF

1817import Idris.Core.TT

1918import Idris.Core.Typecheck

19+import Idris.Core.WHNF

2020import Idris.Coverage

2121import Idris.DataOpts

2222import Idris.DeepSeq

@@ -150,13 +150,13 @@ elabClauses info' fc opts n_in cs =

150150

151151 -- pdef is the compile-time pattern definition, after forcing

152152 -- optimisation applied to LHS

153− let pdef = map (\(ns, lhs, rhs) -> (map fst ns, lhs, rhs)) $

153+ let pdef = map (\(ns, lhs, rhs) -> (map fst ns, lhs, rhs)) $

154154 map debind pats_forced

155155 -- pdef_cov is the pattern definition without forcing, which

156156 -- we feed to the coverage checker (we need to know what the

157157 -- programmer wrote before forcing erasure)

158158 let pdef_cov

159− = map (\(ns, lhs, rhs) -> (map fst ns, lhs, rhs)) $

159+ = map (\(ns, lhs, rhs) -> (map fst ns, lhs, rhs)) $

160160 map debind pats_raw

161161 -- pdef_pe is the one which will get further optimised

162162 -- for run-time, with no forcing optimisation of the LHS because

@@ -189,7 +189,7 @@ elabClauses info' fc opts n_in cs =

189189 pmissing <-

190190 if cov && not (hasDefault pats_raw)

191191 then do -- Generate clauses from the given possible cases

192− missing <- genClauses fc n

192+ missing <- genClauses fc n

193193 (map (\ (ns,tm,_) -> (ns, tm)) pdef)

194194 cs_full

195195 -- missing <- genMissing n scargs sc

@@ -287,8 +287,8 @@ elabClauses info' fc opts n_in cs =

287287 Just Public -> mapM_ (checkVisibility fc n Public Public) calls

288288 _ -> return ()

289289 addCalls n calls

290− let rig = if linearArg (whnfArgs ctxt [] ty)

291− then Rig1

290+ let rig = if linearArg (whnfArgs ctxt [] ty)

291+ then Rig1

292292 else RigW

293293 updateContext (setRigCount n (minRig ctxt rig calls))

294294 addIBC (IBCCG n)

@@ -354,7 +354,7 @@ elabClauses info' fc opts n_in cs =

354354

355355 -- Simplify the left hand side of a definition, to remove any lets

356356 -- that may have arisen during elaboration

357− simple_lhs ctxt (Right (x, y))

357+ simple_lhs ctxt (Right (x, y))

358358 = Right (Idris.Core.Evaluate.simplify ctxt [] x, y)

359359 simple_lhs ctxt t = t

360360

@@ -598,12 +598,12 @@ checkPossible info fc tcgen fname lhs_in

598598 updateIState $ \i -> i { idris_name = newGName }

599599 let lhs_tm = normalise ctxt [] (orderPats (getInferTerm lhs'))

600600 let emptyPat = hasEmptyPat ctxt (idris_datatypes i) lhs_tm

601− if emptyPat then

601+ if emptyPat then

602602 do logElab 10 $ "Empty type in pattern "

603603 return Nothing

604604 else

605605 case recheck (constraintNS info) ctxt' [] (forget lhs_tm) lhs_tm of

606− OK (tm, _, _) ->

606+ OK (tm, _, _) ->

607607 do logElab 10 $ "Valid " ++ show tm ++ "\n"

608608 ++ " from " ++ show lhs

609609 return (Just (delab' i tm True True))

@@ -618,7 +618,7 @@ checkPossible info fc tcgen fname lhs_in

618618 if tcgen then returnTm i err (recoverableCoverage ctxt err)

619619 else returnTm i err (validCoverageCase ctxt err ||

620620 recoverableCoverage ctxt err)

621− where returnTm i err True = do logLvl 10 $ "Possibly resolvable error on " ++

621+ where returnTm i err True = do logLvl 10 $ "Possibly resolvable error on " ++

622622 pshow i (fmap (normalise (tt_ctxt i) []) err)

623623 ++ " on " ++ showTmImpls lhs_in

624624 return $ Just lhs_in

@@ -637,8 +637,8 @@ checkPossibles info fc tcgen fname (lhs : rest)

637637 -- check, just remove from the next batch

638638 let rest' = filter (\x -> not (qmatch x lhs)) (take 200 rest) ++ drop 200 rest

639639 restpos <- checkPossibles info fc tcgen fname rest'

640− case ok of

641− Nothing -> return restpos

640+ case ok of

641+ Nothing -> return restpos

642642 Just lhstm -> return (lhstm : restpos)

643643 where

644644 qmatch _ Placeholder = True

@@ -647,9 +647,9 @@ checkPossibles info fc tcgen fname (lhs : rest)

647647 = qmatch f f' && and (zipWith qmatch (map getTm args)

648648 (map getTm args'))

649649 qmatch (PRef _ _ n) (PRef _ _ n') = n == n'

650− qmatch (PPair _ _ _ l r) (PPair _ _ _ l' r') = qmatch l l' && qmatch r r'

651− qmatch (PDPair _ _ _ l t r) (PDPair _ _ _ l' t' r')

652− = qmatch l l' && qmatch t t' && qmatch r r'

650+ qmatch (PPair _ _ _ l r) (PPair _ _ _ l' r') = qmatch l l' && qmatch r r'

651+ qmatch (PDPair _ _ _ l t r) (PDPair _ _ _ l' t' r')

652+ = qmatch l l' && qmatch t t' && qmatch r r'

653653 qmatch x y = x == y

654654checkPossibles _ _ _ _ [] = return []

655655

@@ -680,12 +680,12 @@ getNamesToUnfold iname ms tm = nub $ iname : getNames Nothing tm ++ ms

680680 | (f, args) <- unApply fn

681681 = let under' = case f of

682682 P _ fn _ -> Just fn

683− _ -> Nothing

683+ _ -> Nothing

684684 in

685685 getNames under f ++ concatMap (getNames under') args

686686 getNames (Just under) (P _ ref _)

687687 = if ref == iname then [under] else []

688− getNames under (Bind n (Let t v) sc)

688+ getNames under (Bind n (Let t v) sc)

689689 = getNames Nothing t ++

690690 getNames Nothing v ++

691691 getNames Nothing sc

@@ -862,13 +862,13 @@ elabClause info opts (cnum, PClause fc fname lhs_in_as withs rhs_in_as wherebloc

862862 logElab 3 "DONE CHECK"

863863 logElab 3 $ "---> " ++ show rhsElab

864864 ctxt <- getContext

865−

865+

866866 let rhs' = case getUnfolds opts of

867− Just (n, ms) ->

867+ Just (n, ms) ->

868868 let ns = getNamesToUnfold n ms rhsElab in

869869 unfold ctxt [] (map (\n -> (n, 1)) ns) rhsElab

870870 _ -> rhsElab

871−

871+

872872 logElab 5 $ "----- " ++ show (getUnfolds opts) ++

873873 "\nUnfolded " ++ show rhsElab ++ "\n" ++

874874 "to " ++ show rhs'

@@ -1042,7 +1042,7 @@ elabClause info opts (_, PWith fc fname lhs_in withs wval_in pn_in withblock)

10421042 Placeholder -> ierror $ At fc $

10431043 Msg "No expression for the with block to inspect.\nYou need to replace the _ with an expression."

10441044 _ -> return $

1045− rhs_trans info $

1045+ rhs_trans info $

10461046 addImplBound i (map fst bargs) wval_in

10471047 logElab 5 ("Checking " ++ showTmImpls wval)

10481048 -- Elaborate wval in this context

@@ -1070,11 +1070,11 @@ elabClause info opts (_, PWith fc fname lhs_in withs wval_in pn_in withblock)

10701070 mapM_ (elabCaseBlock info opts) is

10711071

10721072 let wval' = case getUnfolds opts of

1073− Just (n, ms) ->

1073+ Just (n, ms) ->

10741074 let ns = getNamesToUnfold n ms wvalElab in

10751075 unfold ctxt [] (map (\n -> (n, 1)) ns) wvalElab

10761076 _ -> wvalElab

1077−

1077+

10781078 logElab 5 ("Checked wval " ++ show wval')

10791079 logElab 5 $ "----- " ++ show (getUnfolds opts) ++

10801080 "\nUnfolded wval " ++ show wvalElab ++ "\n" ++

@@ -1155,7 +1155,7 @@ elabClause info opts (_, PWith fc fname lhs_in withs wval_in pn_in withblock)

11551155 Just (n, ns) -> [UnfoldIface n ns]

11561156 _ -> []

11571157 setFlags wname ([Inlinable] ++ uflags)

1158− when (AssertTotal `elem` opts) $

1158+ when (AssertTotal `elem` opts) $

11591159 setFlags wname ([Inlinable, AssertTotal] ++ uflags)

11601160 i <- getIState

11611161 let rhstrans' = updateWithTerm i mpn wname lhs (map fst bargs_pre) (map fst (bargs_post))

@@ -1186,18 +1186,18 @@ elabClause info opts (_, PWith fc fname lhs_in withs wval_in pn_in withblock)

11861186 tt <- get_term

11871187 return (tt, d, is, ctxt', newDecls, highlights, newGName))

11881188 setContext ctxt'

1189−

1189+

11901190 processTacticDecls info newDecls

11911191 sendHighlighting highlights

11921192 updateIState $ \i -> i { idris_name = newGName }

1193−

1193+

11941194 ctxt <- getContext

11951195 let rhs' = case getUnfolds opts of

1196− Just (n, ms) ->

1196+ Just (n, ms) ->

11971197 let ns = getNamesToUnfold n ms rhsElab in

11981198 unfold ctxt [] (map (\n -> (n, 1)) ns) rhsElab

11991199 _ -> rhsElab

1200−

1200+

12011201 logElab 5 $ "----- " ++ show (getUnfolds opts) ++

12021202 "\nUnfolded with RHS " ++ show rhsElab ++ "\n" ++

12031203 "to " ++ show rhs'

src/Idris/Elab/Data.hs+4−4

@@ -193,7 +193,7 @@ elabCon info syn tn codata expkind dkind (doc, argDocs, n, nfc, t_in, fc, forcen

193193

194194 -- Check that the constructor type is, in fact, a part of the family being defined

195195 tyIs n cty'

196− let force = if tn == sUN "Delayed"

196+ let force = if tn == sUN "Delayed"

197197 then [] -- TMP HACK! Totality checker needs this info

198198 else forceArgs ctxt cty'

199199

@@ -273,7 +273,7 @@ forceArgs ctxt ty = forceFrom 0 ty

273273 forceFrom :: Int -> Type -> [Int]

274274 forceFrom i (Bind n (Pi _ _ _ _) sc)

275275 = forceFrom (i + 1) (substV (P Ref (sMN i "FF") Erased) sc)

276− forceFrom i sc

276+ forceFrom i sc

277277 -- Go under the top level type application

278278 -- We risk affecting erasure of more complex indices, so we'll only

279279 -- mark something forced if *everything* which appears in an index

@@ -292,14 +292,14 @@ forceArgs ctxt ty = forceFrom 0 ty

292292 -- Only look under constructors in applications

293293 findForcePos ap@(App _ f a)

294294 | (P _ con _, args) <- unApply ap,

295− isDConName con ctxt

295+ isDConName con ctxt

296296 = nub $ concatMap findForcePos args

297297 findForcePos _ = []

298298

299299 findNonForcePos fok (P _ (MN i ff) _)

300300 | ff == txt "FF" = if fok then [] else [i]

301301 -- Look under non-constructors in applications for things which can't

302− -- be forced

302+ -- be forced

303303 findNonForcePos fok ap@(App _ f a)

304304 | (P _ con _, args) <- unApply ap

305305 = nub $ concatMap (findNonForcePos (fok && isConName con ctxt)) args

src/Idris/Elab/Term.hs+4−4

@@ -18,7 +18,7 @@ import Idris.Core.ProofTerm (getProofTerm)

1818import Idris.Core.TT

1919import Idris.Core.Typecheck (check, converts, isType, recheck)

2020import Idris.Core.Unify

21−import Idris.Core.WHNF (whnf,whnfArgs)

21+import Idris.Core.WHNF (whnf, whnfArgs)

2222import Idris.Coverage (genClauses, recoverableCoverage, validCoverageCase)

2323import Idris.Delaborate

2424import Idris.DSL

@@ -30,7 +30,7 @@ import Idris.ErrReverse (errReverse)

3030import Idris.Output (pshow)

3131import Idris.ProofSearch

3232import Idris.Reflection

33−import Idris.Termination(buildSCG, checkDeclTotality, checkPositive)

33+import Idris.Termination (buildSCG, checkDeclTotality, checkPositive)

3434

3535import qualified Util.Pretty as U

3636

@@ -710,7 +710,7 @@ elab ist info emode opts fn tm

710710 solve

711711 highlightSource nfc (AnnBoundName n False)

712712 elab' ina fc (PPi p n nfc Placeholder sc)

713− = do attack;

713+ = do attack;

714714 case pcount p of

715715 RigW -> return ()

716716 _ -> unless (LinearTypes `elem` idris_language_extensions ist

@@ -1754,7 +1754,7 @@ pruneByType imp env (P _ n _) goalty ist as

17541754 | (P _ fl _, argsl) <- unApply apl,

17551755 (P _ fr _, argsr) <- unApply apr,

17561756 isConName fl ctxt && isConName fr ctxt

1757− = fl == fr

1757+ = fl == fr

17581758 matchingHead _ _ = True

17591759

17601760 -- Return whether there is a possible coercion between the return type

src/Idris/Elab/Type.hs+2−2

@@ -16,10 +16,10 @@ import Idris.ASTUtils

1616import Idris.Core.CaseTree

1717import Idris.Core.Elaborate hiding (Tactic(..))

1818import Idris.Core.Evaluate

19−import Idris.Core.WHNF

2019import Idris.Core.Execute

2120import Idris.Core.TT

2221import Idris.Core.Typecheck

22+import Idris.Core.WHNF

2323import Idris.Coverage

2424import Idris.DataOpts

2525import Idris.DeepSeq

@@ -133,7 +133,7 @@ buildType info syn fc opts n ty' = do

133133 let fninfo = FnInfo (param_pos 0 pnames cty)

134134 setFnInfo n fninfo

135135 addIBC (IBCFnInfo n fninfo)

136−

136+

137137 -- If we use any types with linear constructor arguments, we'd better

138138 -- make sure they are use-once

139139 tcliftAt fc $ linearCheck ctxt (whnfArgs ctxt [] cty)

src/Idris/Elab/Utils.hs+6−6

@@ -11,9 +11,9 @@ module Idris.Elab.Utils where

1111import Idris.AbsSyntax

1212import Idris.Core.Elaborate hiding (Tactic(..))

1313import Idris.Core.Evaluate

14−import Idris.Core.WHNF

1514import Idris.Core.TT

1615import Idris.Core.Typecheck

16+import Idris.Core.WHNF

1717import Idris.DeepSeq

1818import Idris.Delaborate

1919import Idris.Docstrings

@@ -561,7 +561,7 @@ isEmpty ctxt tyctxt ty

561561 findClash l r

562562 | (P _ n _, _) <- unApply l,

563563 (P _ n' _, _) <- unApply r,

564− isConName n ctxt && isConName n' ctxt, n /= n'

564+ isConName n ctxt && isConName n' ctxt, n /= n'

565565 = True

566566 findClash (App _ f a) (App _ f' a') = findClash f f' || findClash a a'

567567 findClash l r = False

@@ -584,16 +584,16 @@ findLinear ist env tm | (P _ f _, args) <- unApply tm,

584584 findLinArg (Bind n (Pi c _ _ _) sc) (P _ a _ : as)

585585 | Rig0 <- c = (a, c) : findLinArg sc as

586586 | Rig1 <- c = (a, c) : findLinArg sc as

587− findLinArg (Bind n (Pi _ _ _ _) sc) (a : as)

587+ findLinArg (Bind n (Pi _ _ _ _) sc) (a : as)

588588 = findLinArg (whnf (tt_ctxt ist) [] (substV a sc)) as

589589 findLinArg _ _ = []

590−findLinear ist env (App _ f a)

591− = nub $ findLinear ist env f ++ findLinear ist env a

590+findLinear ist env (App _ f a)

591+ = nub $ findLinear ist env f ++ findLinear ist env a

592592findLinear ist env (Bind n b sc) = findLinear ist (n : env) sc

593593findLinear ist _ _ = []

594594

595595setLinear :: [(Name, RigCount)] -> Term -> Term

596−setLinear ns (Bind n b@(PVar r t) sc)

596+setLinear ns (Bind n b@(PVar r t) sc)

597597 | Just r <- lookup n ns = Bind n (PVar r t) (setLinear ns sc)

598598 | otherwise = Bind n b (setLinear ns sc)

599599setLinear ns tm = tm

src/Idris/Termination.hs+5−5

@@ -48,7 +48,7 @@ checkAllCovering _ _ _ _ = return ()

4848--

4949-- If so, set the 'AllGuarded' flag which can be used by the productivity check

5050checkIfGuarded :: Name -> Idris ()

51−checkIfGuarded n

51+checkIfGuarded n

5252 = do i <- get

5353 let ctxt = tt_ctxt i

5454 case lookupDefExact n ctxt of

@@ -65,9 +65,9 @@ checkIfGuarded n

6565 Nothing -> False

6666 Just fs -> AllGuarded `elem` fs

6767

68− -- Top level thing always needs to be a constructor application if

68+ -- Top level thing always needs to be a constructor application if

6969 -- the delayed things are going to be definitely guarded by this definition

70− allGuarded names i (STerm t)

70+ allGuarded names i (STerm t)

7171 | (P _ fn _, args) <- unApply t,

7272 guard fn i

7373 = and (map (guardedTerm names i) args)

@@ -86,7 +86,7 @@ checkIfGuarded n

8686 = and (map (guardedTerm names i) args)

8787 guardedTerm names i (App _ f a) = False

8888 guardedTerm names i tm = True

89−

89+

9090 guardedAlt names i (ConCase _ _ _ t) = allGuarded names i t

9191 guardedAlt names i (FnCase _ _ t) = allGuarded names i t

9292 guardedAlt names i (ConstCase _ t) = allGuarded names i t

@@ -369,7 +369,7 @@ buildSCG' ist topfn pats args = nub $ concatMap scgPat pats where

369369 = findCalls cases Unguarded f pvs pargs ++ findCalls cases Unguarded a pvs pargs

370370 findCalls cases guarded (Bind n (Let t v) e) pvs pargs

371371 = findCalls cases Unguarded t pvs pargs ++

372− findCalls cases Unguarded v pvs pargs ++

372+ findCalls cases Unguarded v pvs pargs ++

373373 -- Substitute in the scope since this might reveal some useful

374374 -- structure

375375 findCalls cases guarded (substV v e) pvs pargs

stylize.sh+4−3

@@ -5,13 +5,14 @@ set -e

55if [ -n "$TRAVIS" ];

66then

77 mkdir -p ~/.local/bin

8− export PATH=$HOME/.local/bin:/opt/ghc/8.0.1/bin:$PATH

8+ export PATH=$HOME/.local/bin:/opt/ghc/$GHCVER/bin:$PATH

99 curl --retry 3 -L https://www.stackage.org/stack/linux-x86_64 | tar xz --wildcards --strip-components=1 -C ~/.local/bin '*/stack'

10− stack install --resolver lts-7.2 stylish-haskell --no-terminal

10+ stack config set system-ghc --global true

11+ stack install --resolver "lts-$STACKVER" stylish-haskell --no-terminal

1112fi

1213

1314

14−find . -name \*.hs -and $ -not \( -name Setup.hs -or -path ./dist/\* $ \) | xargs stylish-haskell -i > stylish-out 2>&1

15+find . -name \*.hs -and $ -not \( -name Setup.hs -or -path ./.cabal-sandbox/\* -or -path ./dist/\* $ \) | xargs stylish-haskell -i > stylish-out 2>&1

1516

1617# It doesn't do exit codes properly, so we just check if it outputted anything.

1718if [ -s stylish-out ];