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

idris.cabal+2

compare with master

unifiedsplit

@@ -63,6 +63,8 @@ Executable idris

63 Idris.Coverage, Idris.IBC, Idris.Unlit,

64 Idris.DataOpts, Idris.Transforms, Idris.DSL,

65

66+ Util.Pretty,

67+

66 Paths_idris

68 Paths_idris

67

69

68 Build-depends: base>=4 && <5, parsec, mtl, Cabal, haskeline,

70 Build-depends: base>=4 && <5, parsec, mtl, Cabal, haskeline,

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+5−2

@@ -47,8 +47,10 @@ delab' ist tm fullname = de [] tm

47 deFn env (P _ n _) [l,r] | n == pairTy = PPair un (de env l) (de env r)

48 | n == eqCon = PRefl un

49 | n == UN "lazy" = de env r

50+ deFn env (P _ n _) [ty, Bind x (Lam _) r]

51+ | n == UN "Exists"

50− | n == UN "Exists" = PDPair un (de env l) Placeholder

52+ = PDPair un (PRef un x) (de env ty)

51− (de env r)

53+ (de env (instantiate (P Bound x ty) r))

52 deFn env (P _ n _) [_,_,l,r] | n == pairCon = PPair un (de env l) (de env r)

54 deFn env (P _ n _) [_,_,l,r] | n == pairCon = PPair un (de env l) (de env r)

53 | n == eqTy = PEq un (de env l) (de env r)

55 | n == eqTy = PEq un (de env l) (de env r)

54 | n == UN "Ex_intro" = PDPair un (de env l) Placeholder

56 | n == UN "Ex_intro" = PDPair un (de env l) Placeholder

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

71pshow i (CantUnify x y e s)

73pshow i (CantUnify x y e s)

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

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

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

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

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

74 case e of

77 case e of

75 Msg "" -> ""

78 Msg "" -> ""

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

79 _ -> "\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,