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

git.iko.soy/Idris-dev

Merge branch 'master' of github.com:edwinb/Idris-dev

commit7e248ef6d1e109071f9d318e57fa2e56694574e0 authorEdwin Brady <eb@cs.st-andrews.ac.uk> dateThu 29 Mar 2012, 14:56 (15 years ago) parent9bb92a5 067f4fa

4 files changed+16−5

compare with master

unifiedsplit

idris.cabal+2 src/Idris/AbsSyntax.hs+3−1 src/Idris/Delaborate.hs+5−2 src/Idris/ElabTerm.hs+6−2

idris.cabal+2

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

6363 Idris.Coverage, Idris.IBC, Idris.Unlit,

6464 Idris.DataOpts, Idris.Transforms, Idris.DSL,

6565

66+ Util.Pretty,

67+

6668 Paths_idris

6769

6870 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

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

996996 showbasic (MN _ s) = s

997997 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

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

10001002 " in " ++ se 10 sc

10011003 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

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

4848 | n == eqCon = PRefl un

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

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

51− (de env r)

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

51+ | n == UN "Exists"

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

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

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

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

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

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

7173pshow i (CantUnify x y e s)

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

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

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

7477 case e of

7578 Msg "" -> ""

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

src/Idris/ElabTerm.hs+6−2

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

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

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

104104 = resolveTC 5 fn ist

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

106− instanceArg c

105+ elab' ina (PResolveTC fc)

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

107+ instanceArg c

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

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

110+ instanceArg c)

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

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

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