git.iko.soy/Idris-dev
on master help sign in
Stylish changes since this PR was originally submitted
7ac40afEcho Nolan
src/Idris/Core/TT.hs+1−1
compare with master
unifiedsplit
@@ -1455,7 +1455,7 @@ substRetTy (Bind n (PVar ty) sc) = substRetTy (substV (P Ref n ty) sc)
1455substRetTy (Bind n (PVTy ty) sc) = substRetTy (substV (P Ref n ty) sc)
1455substRetTy (Bind n (PVTy ty) sc) = substRetTy (substV (P Ref n ty) sc)
1456substRetTy (Bind n (Pi _ ty _) sc) = substRetTy (substV (P Ref n ty) sc)
1456substRetTy (Bind n (Pi _ ty _) sc) = substRetTy (substV (P Ref n ty) sc)
1457substRetTy sc = sc
1457substRetTy sc = sc
1458−
1458+
1459
1459
1460uniqueNameFrom :: [Name] -> [Name] -> Name
1460uniqueNameFrom :: [Name] -> [Name] -> Name
1461uniqueNameFrom [] hs = uniqueName (nextName (sUN "x")) hs
1461uniqueNameFrom [] hs = uniqueName (nextName (sUN "x")) hs
src/Idris/Elab/Clause.hs+1−1
@@ -441,7 +441,7 @@ elabPE info fc caller r =
441 | (P Ref n _, _) <- unApply tm = Just (n, Just (if simpl then 1 else 0))
441 | (P Ref n _, _) <- unApply tm = Just (n, Just (if simpl then 1 else 0))
442 specName simpl (ExplicitS, tm)
442 specName simpl (ExplicitS, tm)
443 | (P Ref n _, _) <- unApply tm = Just (n, Just (if simpl then 1 else 0))
443 | (P Ref n _, _) <- unApply tm = Just (n, Just (if simpl then 1 else 0))
444− specName simpl (ConstraintS, tm)
444+ specName simpl (ConstraintS, tm)
445 | (P Ref n _, _) <- unApply tm = Just (n, Just (if simpl then 1 else 0))
445 | (P Ref n _, _) <- unApply tm = Just (n, Just (if simpl then 1 else 0))
446 specName simpl _ = Nothing
446 specName simpl _ = Nothing
447
447
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
93 -- if the implementation type matches any of the implementations we have already,
93 -- if the implementation type matches any of the implementations we have already,
94 -- and it's not a named implementation, then it's overlapping, so report an error
94 -- and it's not a named implementation, then it's overlapping, so report an error
95 case expn of
95 case expn of
96− Nothing
96+ Nothing
97 | OverlappingDictionary `notElem` opts ->
97 | OverlappingDictionary `notElem` opts ->
98 do mapM_ (maybe (return ()) overlapping . findOverlapping ist (interface_determiners ci) (delab ist nty))
98 do mapM_ (maybe (return ()) overlapping . findOverlapping ist (interface_determiners ci) (delab ist nty))
99 (map fst $ interface_implementations ci)
99 (map fst $ interface_implementations ci)
@@ -130,7 +130,7 @@ elabImplementation info syn doc argDocs what fc cs parents acc opts n nfc ps pex
130 Just ty -> (map (\n -> (n, getTypeIn ist n ty)) headVars, ty)
130 Just ty -> (map (\n -> (n, getTypeIn ist n ty)) headVars, ty)
131 _ -> (zip headVars (repeat Placeholder), Erased)
131 _ -> (zip headVars (repeat Placeholder), Erased)
132
132
133− let impps = getImpParams ist (interface_impparams ci)
133+ let impps = getImpParams ist (interface_impparams ci)
134 (snd (unApply (substRetTy ty)))
134 (snd (unApply (substRetTy ty)))
135 let iimpps = zip (interface_impparams ci) impps
135 let iimpps = zip (interface_impparams ci) impps
136
136
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
81 syn_in { using = addToUsing (using syn_in)
81 syn_in { using = addToUsing (using syn_in)
82 [(pn, pt) | (pn, _, pt) <- ps]
82 [(pn, pt) | (pn, _, pt) <- ps]
83 }
83 }
84−
84+
85 -- Calculate implicit parameters
85 -- Calculate implicit parameters
86 ist <- getIState
86 ist <- getIState
87 let impps_ns = nub $ map (\n -> (n, emptyFC, Placeholder)) $
87 let impps_ns = nub $ map (\n -> (n, emptyFC, Placeholder)) $
88− concatMap (implicitNamesIn [] ist)
88+ concatMap (implicitNamesIn [] ist)
89 (map (\ (_,_,x) -> x) ps)
89 (map (\ (_,_,x) -> x) ps)
90− let impps = filter (\ (n, _, _) ->
90+ let impps = filter (\ (n, _, _) ->
91 n `notElem` (map (\ (n, _, _) -> n) ps)) impps_ns
91 n `notElem` (map (\ (n, _, _) -> n) ps)) impps_ns
92
92
93− let tty = impbind (map (\(n, _, ty) -> (n, ty)) impps) $
93+ let tty = impbind (map (\(n, _, ty) -> (n, ty)) impps) $
94 pibind (map (\(n, _, ty) -> (n, ty)) ps) (PType fc)
94 pibind (map (\(n, _, ty) -> (n, ty)) ps) (PType fc)
95
95
96 logElab 5 $ "Implicit parameters are " ++ show impps
96 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
129 elabData info (syn { no_imp = no_imp syn ++ mnames,
129 elabData info (syn { no_imp = no_imp syn ++ mnames,
130 imp_methods = mnames }) doc pDocs fc [] ddecl
130 imp_methods = mnames }) doc pDocs fc [] ddecl
131 dets <- findDets cn (map fst fds)
131 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
133 (map (\(n, _, _) -> n) impps)
133 (map (\(n, _, _) -> n) impps)
134− (map (\(n, _, _) -> n) ps)
134+ (map (\(n, _, _) -> n) ps)
135 [] dets)
135 [] dets)
136
136
137 -- for each constraint, build a top level function to chase it
137 -- for each constraint, build a top level function to chase it
src/Idris/PartialEval.hs+5−5
@@ -276,7 +276,7 @@ mkPE_TermDecl :: IState
276 -> [(PEArgType, Term)]
276 -> [(PEArgType, Term)]
277 -> PEDecl
277 -> PEDecl
278mkPE_TermDecl ist newname sname specty ns
278mkPE_TermDecl ist newname sname specty ns
279− {- We need to erase the *dynamic* arguments
279+ {- We need to erase the *dynamic* arguments
280 where their *name* appears in the *type* of a later argument
280 where their *name* appears in the *type* of a later argument
281 in specty.
281 in specty.
282 i.e. if a later dynamic argument depends on an earlier dynamic
282 i.e. if a later dynamic argument depends on an earlier dynamic
@@ -285,12 +285,12 @@ mkPE_TermDecl ist newname sname specty ns
285 on the RHS.
285 on the RHS.
286 -}
286 -}
287 = let deps = getDepNames (eraseRet specty)
287 = let deps = getDepNames (eraseRet specty)
288− lhs = eraseDeps deps $
288+ lhs = eraseDeps deps $
289 PApp emptyFC (PRef emptyFC [] newname) (mkp ns)
289 PApp emptyFC (PRef emptyFC [] newname) (mkp ns)
290 rhs = eraseDeps deps $
290 rhs = eraseDeps deps $
291 delab ist (mkApp (P Ref sname Erased) (map snd ns))
291 delab ist (mkApp (P Ref sname Erased) (map snd ns))
292 patdef = -- trace (showTmImpls specty ++ "\n" ++ showTmImpls lhs ++ "\n"
292 patdef = -- trace (showTmImpls specty ++ "\n" ++ showTmImpls lhs ++ "\n"
293− -- ++ showTmImpls rhs) $
293+ -- ++ showTmImpls rhs) $
294 lookupCtxtExact sname (idris_patdefs ist)
294 lookupCtxtExact sname (idris_patdefs ist)
295 newpats = case patdef of
295 newpats = case patdef of
296 Nothing -> PEDecl lhs rhs [(lhs, rhs)] True
296 Nothing -> PEDecl lhs rhs [(lhs, rhs)] True
@@ -305,7 +305,7 @@ mkPE_TermDecl ist newname sname specty ns
305
305
306 -- Get names used in later arguments; assume we've called eraseRet so there's
306 -- Get names used in later arguments; assume we've called eraseRet so there's
307 -- no names going to appear in return type
307 -- no names going to appear in return type
308− getDepNames (PPi _ n _ _ sc)
308+ getDepNames (PPi _ n _ _ sc)
309 | n `elem` allNamesIn sc = n : getDepNames sc
309 | n `elem` allNamesIn sc = n : getDepNames sc
310 | otherwise = getDepNames sc
310 | otherwise = getDepNames sc
311 getDepNames tm = []
311 getDepNames tm = []
@@ -337,7 +337,7 @@ getSpecApps ist env tm = ga env (explicitNames tm) where
337 | Just n <- imparg imp = (ImplicitS n, tm)
337 | Just n <- imparg imp = (ImplicitS n, tm)
338 | constrarg imp = (ConstraintS, tm)
338 | constrarg imp = (ConstraintS, tm)
339 | otherwise = (ExplicitS, tm)
339 | otherwise = (ExplicitS, tm)
340−
340+
341 staticArg env False imp tm n
341 staticArg env False imp tm n
342 | Just nm <- imparg imp = (ImplicitD nm, (P Ref (sUN (show n ++ "arg")) Erased))
342 | Just nm <- imparg imp = (ImplicitD nm, (P Ref (sUN (show n ++ "arg")) Erased))
343 | constrarg imp = (ConstraintD, tm)
343 | constrarg imp = (ConstraintD, tm)