f6bcfb6 · Idris-dev · git.iko.soy

git.iko.soy/Idris-dev

Some tidying of scoped implicits

commitf6bcfb6c6be23b233eb551940943331b287b9bd3 authorEdwin Brady <ecb10@st-andrews.ac.uk> dateSun 11 Jan 2015, 21:00 (12 years ago) parente0cab49

4 files changed+18−10

compare with master

unifiedsplit

src/Idris/Core/Unify.hs+14−4 src/Idris/Delaborate.hs+2 src/Idris/ElabTerm.hs+1−1 src/Idris/ParseExpr.hs+1−5

src/Idris/Core/Unify.hs+14−4

@@ -86,14 +86,24 @@ match_unify ctxt env topx topy inj holes from =

8686 return (map (renameBinders env) v')

8787 _ -> tfail e

8888 where

89− -- This rule is highly dubious... it certainly produces a valid answer

90− -- but it scares me. However, matching is never guaranteed to give a unique

91− -- answer, merely a valid one, so perhaps we're okay.

92− -- In other words: it may vanish without warning some day :)

9389 un :: [((Name, Name), TT Name)] -> TT Name -> TT Name ->

9490 StateT UInfo

9591 TC [(Name, TT Name)]

9692

93+ -- This rule is highly dubious... it certainly produces a valid answer

94+ -- but it scares me. However, matching is never guaranteed to give a unique

95+ -- answer, merely a valid one, so perhaps we're okay.

96+ -- In other words: it may vanish without warning some day :)

97+ un names x tm@(App (P _ f (Bind fn (Pi _ t _) sc)) a)

98+ | (P (TCon _ _) _ _, _) <- unApply x,

99+ holeIn env f || f `elem` holes

100+ = let n' = uniqueName (sMN 0 "mv") (map fst env) in

101+ checkCycle names (f, Bind n' (Lam t) x)

102+ un names tm@(App (P _ f (Bind fn (Pi _ t _) sc)) a) x

103+ | (P (TCon _ _) _ _, _) <- unApply x,

104+ holeIn env f || f `elem` holes

105+ = let n' = uniqueName fn (map fst env) in

106+ checkCycle names (f, Bind n' (Lam t) x)

97107 un names x tm@(App (P _ f (Bind fn (Pi _ t _) sc)) a)

98108 | (P (DCon _ _ _) _ _, _) <- unApply x,

99109 holeIn env f || f `elem` holes

src/Idris/Delaborate.hs+2

@@ -57,6 +57,8 @@ delabTy' ist imps tm fullname mvs = de [] imps tm

5757 _ -> PRef un n

5858 de env _ (Bind n (Lam ty) sc)

5959 = PLam un n (de env [] ty) (de ((n,n):env) [] sc)

60+ de env is (Bind n (Pi True ty _) sc)

61+ = PPi (Imp [] Dynamic False True) n (de env [] ty) (de ((n,n):env) is sc)

6062 de env ((PImp { argopts = opts }):is) (Bind n (Pi _ ty _) sc)

6163 = PPi (Imp opts Dynamic False False) n (de env [] ty) (de ((n,n):env) is sc)

6264 de env (PConstraint _ _ _ _:is) (Bind n (Pi _ ty _) sc)

src/Idris/ElabTerm.hs+1−1

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

10651065 addLam ty' t

10661066 where

10671067 addLam (Bind n (Pi True _ _) sc) t

1068− = do impn <- unique_hole (sUN "imp")

1068+ = do impn <- unique_hole (sMN 0 "imp")

10691069 t' <- addLam sc t

10701070 return (PLam emptyFC impn Placeholder t')

10711071 addLam _ t = return t

src/Idris/ParseExpr.hs+1−5

@@ -882,11 +882,7 @@ pi syn =

882882 <|> (do xt <- try (lchar '{' *> typeDeclList syn <* lchar '}')

883883 symbol "->"

884884 sc <- expr syn

885− if implicitAllowed syn

886− then return (bindList (PPi (Imp opts st False False)) xt sc)

887− -- TODO: TIDY BEFORE COMMITTING!

888− else return (bindList (PPi (Imp opts st False True)) xt sc)))

889− -- fail "no implicit arguments allowed here"))

885+ return (bindList (PPi (Imp opts st False (not (implicitAllowed syn)))) xt sc)))

890886 <|> (do x <- opExpr syn

891887 (do symbol "->"

892888 sc <- expr syn