7ac40af · Idris-dev · git.iko.soy

git.iko.soy/Idris-dev

Stylish changes since this PR was originally submitted

These changes are from stylish-haskell and reflect changes since PR #3475 - integrating stylish-haskell into the Travis checks - was first submitted.

commit7ac40af7bc09b4e6e6c7fc396272bd77e8f7aca0 authorEcho Nolan <echo@echonolan.net> dateThu 13 Oct 2016, 15:44 (10 years ago) parenta6f2eb7

5 files changed+15−15

compare with master

unifiedsplit

src/Idris/Core/TT.hs+1−1 src/Idris/Elab/Clause.hs+1−1 src/Idris/Elab/Implementation.hs+2−2 src/Idris/Elab/Interface.hs+6−6 src/Idris/PartialEval.hs+5−5

src/Idris/Core/TT.hs+1−1

@@ -1455,7 +1455,7 @@ substRetTy (Bind n (PVar ty) sc) = substRetTy (substV (P Ref n ty) sc)

14551455substRetTy (Bind n (PVTy ty) sc) = substRetTy (substV (P Ref n ty) sc)

14561456substRetTy (Bind n (Pi _ ty _) sc) = substRetTy (substV (P Ref n ty) sc)

14571457substRetTy sc = sc

1458−

1458+

14591459

14601460uniqueNameFrom :: [Name] -> [Name] -> Name

14611461uniqueNameFrom [] hs = uniqueName (nextName (sUN "x")) hs

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

@@ -441,7 +441,7 @@ elabPE info fc caller r =

441441 | (P Ref n _, _) <- unApply tm = Just (n, Just (if simpl then 1 else 0))

442442 specName simpl (ExplicitS, tm)

443443 | (P Ref n _, _) <- unApply tm = Just (n, Just (if simpl then 1 else 0))

444− specName simpl (ConstraintS, tm)

444+ specName simpl (ConstraintS, tm)

445445 | (P Ref n _, _) <- unApply tm = Just (n, Just (if simpl then 1 else 0))

446446 specName simpl _ = Nothing

447447

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

@@ -93,7 +93,7 @@ elabImplementation info syn doc argDocs what fc cs parents acc opts n nfc ps pex

9393 -- if the implementation type matches any of the implementations we have already,

9494 -- and it's not a named implementation, then it's overlapping, so report an error

9595 case expn of

96− Nothing

96+ Nothing

9797 | OverlappingDictionary `notElem` opts ->

9898 do mapM_ (maybe (return ()) overlapping . findOverlapping ist (interface_determiners ci) (delab ist nty))

9999 (map fst $ interface_implementations ci)

@@ -130,7 +130,7 @@ elabImplementation info syn doc argDocs what fc cs parents acc opts n nfc ps pex

130130 Just ty -> (map (\n -> (n, getTypeIn ist n ty)) headVars, ty)

131131 _ -> (zip headVars (repeat Placeholder), Erased)

132132

133− let impps = getImpParams ist (interface_impparams ci)

133+ let impps = getImpParams ist (interface_impparams ci)

134134 (snd (unApply (substRetTy ty)))

135135 let iimpps = zip (interface_impparams ci) impps

136136

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

@@ -81,16 +81,16 @@ elabInterface info syn_in doc fc constraints tn tnfc ps pDocs fds ds mcn cd

8181 syn_in { using = addToUsing (using syn_in)

8282 [(pn, pt) | (pn, _, pt) <- ps]

8383 }

84−

84+

8585 -- Calculate implicit parameters

8686 ist <- getIState

8787 let impps_ns = nub $ map (\n -> (n, emptyFC, Placeholder)) $

88− concatMap (implicitNamesIn [] ist)

88+ concatMap (implicitNamesIn [] ist)

8989 (map (\ (_,_,x) -> x) ps)

90− let impps = filter (\ (n, _, _) ->

90+ let impps = filter (\ (n, _, _) ->

9191 n `notElem` (map (\ (n, _, _) -> n) ps)) impps_ns

9292

93− let tty = impbind (map (\(n, _, ty) -> (n, ty)) impps) $

93+ let tty = impbind (map (\(n, _, ty) -> (n, ty)) impps) $

9494 pibind (map (\(n, _, ty) -> (n, ty)) ps) (PType fc)

9595

9696 logElab 5 $ "Implicit parameters are " ++ show impps

@@ -129,9 +129,9 @@ elabInterface info syn_in doc fc constraints tn tnfc ps pDocs fds ds mcn cd

129129 elabData info (syn { no_imp = no_imp syn ++ mnames,

130130 imp_methods = mnames }) doc pDocs fc [] ddecl

131131 dets <- findDets cn (map fst fds)

132− addInterface tn (CI cn (map nodoc imethods) defaults idecls

132+ addInterface tn (CI cn (map nodoc imethods) defaults idecls

133133 (map (\(n, _, _) -> n) impps)

134− (map (\(n, _, _) -> n) ps)

134+ (map (\(n, _, _) -> n) ps)

135135 [] dets)

136136

137137 -- for each constraint, build a top level function to chase it

src/Idris/PartialEval.hs+5−5

@@ -276,7 +276,7 @@ mkPE_TermDecl :: IState

276276 -> [(PEArgType, Term)]

277277 -> PEDecl

278278mkPE_TermDecl ist newname sname specty ns

279− {- We need to erase the *dynamic* arguments

279+ {- We need to erase the *dynamic* arguments

280280 where their *name* appears in the *type* of a later argument

281281 in specty.

282282 i.e. if a later dynamic argument depends on an earlier dynamic

@@ -285,12 +285,12 @@ mkPE_TermDecl ist newname sname specty ns

285285 on the RHS.

286286 -}

287287 = let deps = getDepNames (eraseRet specty)

288− lhs = eraseDeps deps $

288+ lhs = eraseDeps deps $

289289 PApp emptyFC (PRef emptyFC [] newname) (mkp ns)

290290 rhs = eraseDeps deps $

291291 delab ist (mkApp (P Ref sname Erased) (map snd ns))

292292 patdef = -- trace (showTmImpls specty ++ "\n" ++ showTmImpls lhs ++ "\n"

293− -- ++ showTmImpls rhs) $

293+ -- ++ showTmImpls rhs) $

294294 lookupCtxtExact sname (idris_patdefs ist)

295295 newpats = case patdef of

296296 Nothing -> PEDecl lhs rhs [(lhs, rhs)] True

@@ -305,7 +305,7 @@ mkPE_TermDecl ist newname sname specty ns

305305

306306 -- Get names used in later arguments; assume we've called eraseRet so there's

307307 -- no names going to appear in return type

308− getDepNames (PPi _ n _ _ sc)

308+ getDepNames (PPi _ n _ _ sc)

309309 | n `elem` allNamesIn sc = n : getDepNames sc

310310 | otherwise = getDepNames sc

311311 getDepNames tm = []

@@ -337,7 +337,7 @@ getSpecApps ist env tm = ga env (explicitNames tm) where

337337 | Just n <- imparg imp = (ImplicitS n, tm)

338338 | constrarg imp = (ConstraintS, tm)

339339 | otherwise = (ExplicitS, tm)

340−

340+

341341 staticArg env False imp tm n

342342 | Just nm <- imparg imp = (ImplicitD nm, (P Ref (sUN (show n ++ "arg")) Erased))

343343 | constrarg imp = (ConstraintD, tm)