455ae60 · Idris-dev · git.iko.soy

src/Idris/AbsSyntax.hs+3−1

@@ -995,7 +995,9 @@ showImp impl tm = se 10 tm where

995 where showbasic n@(UN _) = show n

996 showbasic (MN _ s) = s

997 showbasic (NS n s) = showSep "." (reverse s) ++ "." ++ showbasic n

998− se p (PLam n ty sc) = bracket p 2 $ "\\ " ++ show n ++ " => " ++ show sc

998+ se p (PLam n ty sc) = bracket p 2 $ "\\ " ++ show n ++

999+ (if impl then " : " ++ se 10 ty else "") ++ " => "

1000+ ++ se 10 sc

999 se p (PLet n ty v sc) = bracket p 2 $ "let " ++ show n ++ " = " ++ se 10 v ++

1001 se p (PLet n ty v sc) = bracket p 2 $ "let " ++ show n ++ " = " ++ se 10 v ++

1000 " in " ++ se 10 sc

1002 " in " ++ se 10 sc

1001 se p (PPi (Exp l s) n ty sc)

1003 se p (PPi (Exp l s) n ty sc)

src/Idris/Delaborate.hs+1

@@ -71,6 +71,7 @@ pshow i (Msg s) = s

71pshow i (CantUnify x y e s)

72 = "Can't unify " ++ show (delab i x)

73 ++ " with " ++ show (delab i y) ++

74+-- " (" ++ show x ++ " and " ++ show y ++ ") " ++

74 case e of

75 case e of

75 Msg "" -> ""

76 Msg "" -> ""

76 _ -> "\n\nSpecifically:\n\t " ++ pshow i e

77 _ -> "\n\nSpecifically:\n\t " ++ pshow i e

src/Idris/ElabTerm.hs+6−2

@@ -102,8 +102,12 @@ elab ist info pattern tcgen fn tm

102 elab' ina (PFalse fc) = elab' ina (PRef fc falseTy)

103 elab' ina (PResolveTC (FC "HACK" _)) -- for chasing parent classes

104 = resolveTC 5 fn ist

105− elab' ina (PResolveTC fc) = do c <- unique_hole (MN 0 "c")

105+ elab' ina (PResolveTC fc)

106+ | pattern = do c <- unique_hole (MN 0 "c")

106− instanceArg c

107+ instanceArg c

108+ | otherwise = try (resolveTC 2 fn ist)

109+ (do c <- unique_hole (MN 0 "c")

110+ instanceArg c)

107 elab' ina (PRefl fc) = elab' ina (PApp fc (PRef fc eqCon) [pimp (MN 0 "a") Placeholder,

111 elab' ina (PRefl fc) = elab' ina (PApp fc (PRef fc eqCon) [pimp (MN 0 "a") Placeholder,

108 pimp (MN 0 "x") Placeholder])

112 pimp (MN 0 "x") Placeholder])

109 elab' ina (PEq fc l r) = elab' ina (PApp fc (PRef fc eqTy) [pimp (MN 0 "a") Placeholder,

113 elab' ina (PEq fc l r) = elab' ina (PApp fc (PRef fc eqTy) [pimp (MN 0 "a") Placeholder,