c4e039e · Idris-dev · git.iko.soy

git.iko.soy/Idris-dev

on master help sign in

Merge pull request #3618 from ahmadsalim/hotfix/travis-stylishness-config

c4e039eAhmad Salim Al-Sibahi10 years ago

.travis.yml+2−2

compare with master

unifiedsplit

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

9matrix:

10 include:

11− - env: STYLISH=YES

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

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

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

13 - os: osx

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

15 compiler: ": #GHC 8.0.1"

main/Main.hs+6−6

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

1module Main where

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

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

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

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

6−import Data.Maybe ( fromMaybe )

7−import Data.Foldable ( foldrM )

6+import Data.Foldable (foldrM)

7+import Data.Maybe (fromMaybe)

9import Idris.AbsSyntax

10import Idris.CmdOptions

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

16import Util.System (setupBundledCC)

18−import Util.System ( setupBundledCC )

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

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

19+import Util.System (setupBundledCC)

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

22processShowOptions opts = runIO $ do

src/Idris/AbsSyntaxTree.hs+2−2

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

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

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

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

1846− | Rig0 <- rig =

1846+ | Rig0 <- rig =

1847 depth d . bracket p startPrec . group $

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

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

1850− | Rig1 <- rig =

1850+ | Rig1 <- rig =

1851 depth d . bracket p startPrec . group $

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

1853 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

174 then S.empty

175 else if n `elem` ps

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

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

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

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

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

245runCaseBuilder ei bld = runState $ runReaderT bld ei

246

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

248− | CompileTime

248+ | CompileTime

249 | RunTime

250 deriving (Show, Eq)

251

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

253-- Work Right to Left

254

255simpleCase :: Bool -> SC -> Bool ->

256− Phase -> FC ->

256+ Phase -> FC ->

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

258 [Int] -> -- Inaccessible argument positions

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

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

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

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

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

447−order (CoverageCheck pos) ns' cs cans

447+order (CoverageCheck pos) ns' cs cans

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

449 cs_out = map pickClause cs in

450 (ns_out, cs_out)

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

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

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

456 pick i skipped [] = reverse skipped

457− pick i skipped (x : xs)

457+ pick i skipped (x : xs)

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

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

460

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

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

144 (tm, limited st)

145

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

147−-- inline, and lets

147+-- inline, and lets

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

149simplify ctxt env t

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

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

160 quote 0 val) initEval

161

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

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

165inlineSmall ctxt env t

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

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

229 = case lookup n ns of

230 Just 0 -> return (False, ns)

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

232− _ -> return $ if uf

232+ _ -> return $ if uf

233 then (False, ns)

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

235

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

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

1182 = do linearCheckArg ctxt ty

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

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

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

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

1186 checkArgs _ = return ()

1187

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

1189linearCheckArg ctxt ty = mapM_ checkNameOK (allTTNames ty)

1190 where

1191− checkNameOK f

1191+ checkNameOK f

1192 = case lookupRigCountExact f ctxt of

1193 Just Rig1 ->

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

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

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

1198 = do mapM_ checkNameOK (allTTNames ty)

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

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

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

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

1202 checkArgs _ = return ()

1203

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

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

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

1004

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

1006−orderUpdateSolved ns tm = update [] ns tm

1006+orderUpdateSolved ns tm = update [] ns tm

1007 where

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

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

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

1011 (map (updateMatch n) ns)

1012 (updateSolved [n] t)

1013−

1013+

1014 -- Update the later solutions too

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

1016

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

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

1095 previous = Just ps, plog = "",

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

1097− recents = recents ps ++ dropped,

1097+ recents = recents ps ++ dropped,

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

1099processTactic t ps

1100 = case holes ps of

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

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

12module Idris.Core.Typecheck where

14import Idris.Core.Evaluate

15−import Idris.Core.WHNF

16import Idris.Core.TT

15import Idris.Core.TT

16+import Idris.Core.WHNF

18import Control.Monad.State

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

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

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

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

90−check' holes tcns ctxt env top

90+check' holes tcns ctxt env top

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

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

92 return (tm, ty)

93 where

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

106 Maybe UExp -> -- universe for kind

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

108 chk rigc u lvl env (Var n)

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

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

110 = case rigSafe holes erig rigc n of

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

112 Just msg -> lift $ tfail $ Msg msg

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

151 t -> lift $ tfail $ NonFunctionType fv fty

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

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

154− let (rigf, fty') =

154+ let (rigf, fty') =

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

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

157 _ -> 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) ->

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

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

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

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

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

163 case fty' of

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

198 constType _ = TType (UVal 0)

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

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

201− when (rig == RigW) $

201+ when (rig == RigW) $

202 lift $ linearCheckArg ctxt (normalise ctxt env sv)

203 (v, cs) <- get

204 (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

256

257 checkUsageOK Rig0 _ = return ()

258 checkUsageOK RigW _ = return ()

259− checkUsageOK Rig1 ns

259+ checkUsageOK Rig1 ns

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

261 if used == 1 then return ()

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

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

263 " uses of linear name " ++ show n

264

265 checkBinder (Lam rig t)

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

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

270 checkBinder (Let t v)

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

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

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

275 (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

55whnf :: Context -> Env -> Term -> Term

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

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

58−whnf ctxt env tm =

58+whnf ctxt env tm =

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

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

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

62 -- easier to read.

63 whnf' ctxt env tm

64−whnf' ctxt env tm =

64+whnf' ctxt env tm =

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

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

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

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

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

74 -- the name

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

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

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

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

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

78 res -> tm

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

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

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

99− eval env stk (P nt n ty)

99+ eval env stk (P nt n ty)

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

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

102 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

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

113

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

115− apply env nt n ty stk

115+ apply env nt n ty stk

116 = let wp = case nt of

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

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

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

122 if not (tcReducible n ctxt)

123 then unload wp stk

124 else case lookupDefAccExact n False ctxt of

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

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

126 | acc == Public || acc == Hidden ->

127 let (ns, tree) = cases_compiletime cd in

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

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

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

232quote (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)

234 (quoteEnv env sc)

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

236quote (WConstant c) = Constant c

src/Idris/Coverage.hs+31−31

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

62--

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

64-- names are fully explicit!

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

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

66 [PTerm] -> Idris [PTerm]

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

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

69-- 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 []

71genClauses fc n lhs_tms given

72 = do i <- getIState

73−

73+

74− let lhs_given = zipWith removePlaceholders lhs_tms

74+ let lhs_given = zipWith removePlaceholders lhs_tms

75 (map (stripUnmatchable i) (map flattenArgs given))

76−

76+

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

78 let givenpos = mergePos (map getGivenPos given)

80− (cns, ctree_in) <-

80+ (cns, ctree_in) <-

81 case simpleCase False (UnmatchedCase "Undefined") False

82 (CoverageCheck givenpos) emptyFC [] []

83− lhs_given

83+ lhs_given

84 (const []) of

85 OK (CaseDef cns ctree_in _) ->

86 return (cns, ctree_in)

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

88−

88+

89 let ctree = trimOverlapping (addMissingCons i ctree_in)

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

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

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

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

96 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"

98 (map showTmImpls missing)

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

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

100 (map showTmImpls covered)

101 return missing

102 where

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

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

133 = let tl' = rp tl pl

134 tr' = rp tr pr in

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

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

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

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

138 = let tl' = rp tl pl

139 tr' = rp tr pr in

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

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

141 rp tm _ = tm

142

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

144−mkNewClauses ctxt fn ns sc

144+mkNewClauses ctxt fn ns sc

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

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

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

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

149 where

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

151

152− erasePs ap@(App t f a)

152+ erasePs ap@(App t f a)

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

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

155 erasePs tm = tm

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

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

158

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

160− mkFromSC' cov args (STerm _)

160+ mkFromSC' cov args (STerm _)

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

162− mkFromSC' cov args (UnmatchedCase _)

162+ mkFromSC' cov args (UnmatchedCase _)

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

164 mkFromSC' cov args ImpossibleCase = return []

165 mkFromSC' cov args (Case _ x alts)

166 = do done <- get

167 if (args `elem` done)

168 then return []

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

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

170 put (args : done)

171 return (concat alts')

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

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

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

179 mkFromSC' cov args' sc

180 mkFromAlt cov args x (ConstCase c sc)

181− = let argrep = Constant c

181+ = let argrep = Constant c

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

183 mkFromSC' cov args' sc

184 mkFromAlt cov args x (DefaultCase sc)

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

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

196 where

197 addMissingAlt :: CaseAlt -> State Int CaseAlt

198− addMissingAlt (ConCase n i ns sc)

198+ addMissingAlt (ConCase n i ns sc)

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

200− addMissingAlt (FnCase n ns sc)

200+ addMissingAlt (FnCase n ns sc)

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

202− addMissingAlt (ConstCase c sc)

202+ addMissingAlt (ConstCase c sc)

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

204− addMissingAlt (SucCase n sc)

204+ addMissingAlt (SucCase n sc)

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

206− addMissingAlt (DefaultCase sc)

206+ addMissingAlt (DefaultCase sc)

207 = liftM DefaultCase (addMissingConsSt ist sc)

208

209− addMissingAlts argn as

209+ addMissingAlts argn as

210-- | any hasDefault as = map addMissingAlt as

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

212 Just tyn <- getConType n,

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

226 addCases missing (DefaultCase rhs : rest)

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

228 return (mapMaybe id missing' ++ rest)

229− addCases missing (c : rest)

229+ addCases missing (c : rest)

230 = liftM (c :) $ addCases missing rest

231

232 addCons missing [] = []

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

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

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

260 _ -> Nothing

261−

261+

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

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

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

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

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

313

314 substNames [] sc = sc

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

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

316 = substNames ns (substSC n n' sc)

317

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

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

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

359 -- with

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

361− checkRec (P Bound x _) tm

361+ checkRec (P Bound x _) tm

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

363 conType yt = do nmap <- get

364 case lookup x nmap of

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

366 return True

367 Just y' -> checkRec tm y'

368− checkRec tm (P Bound y _)

368+ checkRec tm (P Bound y _)

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

370 conType xt = do nmap <- get

371 case lookup y nmap of

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

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

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

381 then checkRec f f'

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

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

383 where

384 checkRecs [] [] = return True

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

386 asok <- checkRecs as bs

387 return (aok && asok)

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

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

389 | x == y = return True

390 | ntRec xt yt = return True

391 checkRec _ _ = return False

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

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

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

15import Idris.Core.Evaluate

16import Idris.Core.Execute

17−import Idris.Core.WHNF

18import Idris.Core.TT

17import Idris.Core.TT

19import Idris.Core.Typecheck

18import Idris.Core.Typecheck

19+import Idris.Core.WHNF

20import Idris.Coverage

21import Idris.DataOpts

22import Idris.DeepSeq

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

150

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

152 -- 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)) $

154 map debind pats_forced

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

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

157 -- programmer wrote before forcing erasure)

158 let pdef_cov

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

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

160 map debind pats_raw

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

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

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

189 pmissing <-

190 if cov && not (hasDefault pats_raw)

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

192− missing <- genClauses fc n

192+ missing <- genClauses fc n

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

194 cs_full

195 -- missing <- genMissing n scargs sc

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

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

288 _ -> return ()

289 addCalls n calls

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

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

291− then Rig1

291+ then Rig1

292 else RigW

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

294 addIBC (IBCCG n)

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

354

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

356 -- that may have arisen during elaboration

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

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

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

359 simple_lhs ctxt t = t

360

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

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

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

600 let emptyPat = hasEmptyPat ctxt (idris_datatypes i) lhs_tm

601− if emptyPat then

601+ if emptyPat then

602 do logElab 10 $ "Empty type in pattern "

603 return Nothing

604 else

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

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

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

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

608 ++ " from " ++ show lhs

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

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

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

619 else returnTm i err (validCoverageCase ctxt err ||

620 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 " ++

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

623 ++ " on " ++ showTmImpls lhs_in

624 return $ Just lhs_in

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

637 -- check, just remove from the next batch

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

639 restpos <- checkPossibles info fc tcgen fname rest'

640− case ok of

640+ case ok of

641− Nothing -> return restpos

641+ Nothing -> return restpos

642 Just lhstm -> return (lhstm : restpos)

643 where

644 qmatch _ Placeholder = True

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

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

648 (map getTm args'))

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

650− qmatch (PPair _ _ _ l r) (PPair _ _ _ l' r') = qmatch l l' && 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')

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

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

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

653 qmatch x y = x == y

654checkPossibles _ _ _ _ [] = return []

655

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

680 | (f, args) <- unApply fn

681 = let under' = case f of

682 P _ fn _ -> Just fn

683− _ -> Nothing

683+ _ -> Nothing

684 in

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

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

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

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

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

689 = getNames Nothing t ++

690 getNames Nothing v ++

691 getNames Nothing sc

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

862 logElab 3 "DONE CHECK"

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

864 ctxt <- getContext

865−

865+

866 let rhs' = case getUnfolds opts of

867− Just (n, ms) ->

867+ Just (n, ms) ->

868 let ns = getNamesToUnfold n ms rhsElab in

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

870 _ -> rhsElab

871−

871+

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

873 "\nUnfolded " ++ show rhsElab ++ "\n" ++

874 "to " ++ show rhs'

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

1042 Placeholder -> ierror $ At fc $

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

1044 _ -> return $

1045− rhs_trans info $

1045+ rhs_trans info $

1046 addImplBound i (map fst bargs) wval_in

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

1048 -- Elaborate wval in this context

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

1070 mapM_ (elabCaseBlock info opts) is

1071

1072 let wval' = case getUnfolds opts of

1073− Just (n, ms) ->

1073+ Just (n, ms) ->

1074 let ns = getNamesToUnfold n ms wvalElab in

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

1076 _ -> wvalElab

1077−

1077+

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

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

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

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

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

1156 _ -> []

1157 setFlags wname ([Inlinable] ++ uflags)

1158− when (AssertTotal `elem` opts) $

1158+ when (AssertTotal `elem` opts) $

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

1160 i <- getIState

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

1186 tt <- get_term

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

1188 setContext ctxt'

1189−

1189+

1190 processTacticDecls info newDecls

1191 sendHighlighting highlights

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

1193−

1193+

1194 ctxt <- getContext

1195 let rhs' = case getUnfolds opts of

1196− Just (n, ms) ->

1196+ Just (n, ms) ->

1197 let ns = getNamesToUnfold n ms rhsElab in

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

1199 _ -> rhsElab

1200−

1200+

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

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

1203 "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

193

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

195 tyIs n cty'

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

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

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

198 else forceArgs ctxt cty'

199

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

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

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

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

276− forceFrom i sc

276+ forceFrom i sc

277 -- Go under the top level type application

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

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

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

292 -- Only look under constructors in applications

293 findForcePos ap@(App _ f a)

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

295− isDConName con ctxt

295+ isDConName con ctxt

296 = nub $ concatMap findForcePos args

297 findForcePos _ = []

298

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

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

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

302− -- be forced

302+ -- be forced

303 findNonForcePos fok ap@(App _ f a)

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

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

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

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

18import Idris.Core.TT

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

20import Idris.Core.Unify

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

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

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

23import Idris.Delaborate

24import Idris.DSL

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

30import Idris.Output (pshow)

31import Idris.ProofSearch

32import Idris.Reflection

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

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

35import qualified Util.Pretty as U

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

710 solve

711 highlightSource nfc (AnnBoundName n False)

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

713− = do attack;

713+ = do attack;

714 case pcount p of

715 RigW -> return ()

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

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

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

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

1756 isConName fl ctxt && isConName fr ctxt

1757− = fl == fr

1757+ = fl == fr

1758 matchingHead _ _ = True

1759

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

16import Idris.Core.CaseTree

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

18import Idris.Core.Evaluate

19−import Idris.Core.WHNF

20import Idris.Core.Execute

19import Idris.Core.Execute

21import Idris.Core.TT

20import Idris.Core.TT

22import Idris.Core.Typecheck

21import Idris.Core.Typecheck

22+import Idris.Core.WHNF

23import Idris.Coverage

24import Idris.DataOpts

25import Idris.DeepSeq

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

133 let fninfo = FnInfo (param_pos 0 pnames cty)

134 setFnInfo n fninfo

135 addIBC (IBCFnInfo n fninfo)

136−

136+

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

138 -- make sure they are use-once

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

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

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

11import Idris.AbsSyntax

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

13import Idris.Core.Evaluate

14−import Idris.Core.WHNF

15import Idris.Core.TT

14import Idris.Core.TT

16import Idris.Core.Typecheck

15import Idris.Core.Typecheck

16+import Idris.Core.WHNF

17import Idris.DeepSeq

18import Idris.Delaborate

19import Idris.Docstrings

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

561 findClash l r

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

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

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

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

565 = True

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

567 findClash l r = False

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

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

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

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

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

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

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

589 findLinArg _ _ = []

590−findLinear ist env (App _ f a)

590+findLinear ist env (App _ f a)

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

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

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

593findLinear ist _ _ = []

594

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

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

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

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

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

599setLinear ns tm = tm

src/Idris/Termination.hs+5−5

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

48--

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

50checkIfGuarded :: Name -> Idris ()

51−checkIfGuarded n

51+checkIfGuarded n

52 = do i <- get

53 let ctxt = tt_ctxt i

54 case lookupDefExact n ctxt of

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

65 Nothing -> False

66 Just fs -> AllGuarded `elem` fs

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

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

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

70− allGuarded names i (STerm t)

70+ allGuarded names i (STerm t)

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

72 guard fn i

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

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

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

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

88 guardedTerm names i tm = True

89−

89+

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

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

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

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

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

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

371 = findCalls cases Unguarded t pvs pargs ++

372− findCalls cases Unguarded v pvs pargs ++

372+ findCalls cases Unguarded v pvs pargs ++

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

374 -- structure

375 findCalls cases guarded (substV v e) pvs pargs

stylize.sh+4−3

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

5if [ -n "$TRAVIS" ];

6then

7 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

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

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

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

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

11fi

12fi

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

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

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

17if [ -s stylish-out ];

18if [ -s stylish-out ];