f6bcfb6 · Idris-dev · git.iko.soy

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

compare with master

unifiedsplit

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

86 return (map (renameBinders env) v')

87 _ -> tfail e

88 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 :)

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

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

94 StateT UInfo

90 StateT UInfo

95 TC [(Name, TT Name)]

91 TC [(Name, TT Name)]

96

92

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)

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

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

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

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

99 holeIn env f || f `elem` holes

109 holeIn env f || f `elem` holes

src/Idris/Delaborate.hs+2

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

57 _ -> PRef un n

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

59 = 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)

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

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

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

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

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

64 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

1065 addLam ty' t

1066 where

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

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

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

1069 t' <- addLam sc t

1070 return (PLam emptyFC impn Placeholder t')

1071 addLam _ t = return t

src/Idris/ParseExpr.hs+1−5

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

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

883 symbol "->"

884 sc <- expr syn

885− if implicitAllowed syn

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

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

890 <|> (do x <- opExpr syn

886 <|> (do x <- opExpr syn

891 (do symbol "->"

887 (do symbol "->"

892 sc <- expr syn

888 sc <- expr syn