77ca4ed · Idris-dev · git.iko.soy

src/Idris/AbsSyntaxTree.hs+1−1

compare with master

unifiedsplit

@@ -1211,7 +1211,7 @@ pprintPTerm impl bnd docArgs infixes = prettySe 10 bnd

1211 [] -> enclose lparen rparen opName

1212 [x] -> group (enclose lparen rparen opName <$> group (prettySe 0 bnd x))

1213 [l,r] -> let precedence = fromMaybe 20 (fmap prec f)

1214− in trace ("p=" ++ show p++",prec="++show precedence) (bracket p precedence $ inFix l r)

1214+ in bracket p precedence $ inFix l r

1215 (l:r:rest) -> bracket p 1 $

1216 enclose lparen rparen (inFix l r) <+>

1217 align (group (vsep (map (prettyArgSe bnd) rest)))

src/Idris/CaseSplit.hs+4−1

@@ -22,6 +22,7 @@ import Idris.Core.Evaluate

22

23import Data.Maybe

24import Data.Char

25+import Data.List (isPrefixOf, isSuffixOf)

25import Control.Monad

26import Control.Monad

26import Control.Monad.State.Strict

27import Control.Monad.State.Strict

27

28

@@ -299,7 +300,9 @@ replaceSplits l ups = updateRHSs 1 (map (rep (expandBraces l)) ups)

299 else c : updatePat (not (isAlphaNum c)) n tm rest

300 else c : updatePat (not (isAlphaNum c)) n tm rest

300 updatePat start n tm (c:rest) = c : updatePat (not (isAlpha c)) n tm rest

301 updatePat start n tm (c:rest) = c : updatePat (not (isAlpha c)) n tm rest

301

302

302− addBrackets tm | ' ' `elem` tm = "(" ++ tm ++ ")"

303+ addBrackets tm | ' ' `elem` tm

304+ , not (isPrefixOf "(" tm)

305+ , not (isSuffixOf ")" tm) = "(" ++ tm ++ ")"

303 | otherwise = tm

306 | otherwise = tm

304

307

305getUniq nm i

308getUniq nm i

src/Idris/REPL.hs+5−3

@@ -824,9 +824,11 @@ process h fn (DoProofSearch updatefile rec l n hints)

824 (tm, ty) <- elabVal toplevel False (PRef fc mn)

825 ctxt <- getContext

826 i <- getIState

827+ return . flip displayS "" . renderPretty 1.0 80 $

828+ pprintPTerm False [] [] (idris_infixes i)

827− return $ show (stripNS

829+ (stripNS

828− (dropCtxt envlen

830+ (dropCtxt envlen

829− (delab i (specialise ctxt [] [(mn, 1)] tm)))))

831+ (delab i (specialise ctxt [] [(mn, 1)] tm)))))

830 (\e -> return ("?" ++ show n))

832 (\e -> return ("?" ++ show n))

831 if updatefile then

833 if updatefile then

832 do let fb = fn ++ "~"

834 do let fb = fn ++ "~"

test/interactive001/expected+1−1

@@ -4,7 +4,7 @@ isElem x (y :: xs) = ?isElem_rhs_3

4

5 localZipWith f (_ :: _) (x :: ys) = ?localZipWith_rhs_1

6

7−f x :: (map f xs)

7+f x :: map f xs

8isElem2 x (y :: ys) with (_)

9 isElem2 x (y :: ys) | with_pat = ?isElem2_rhs

10 isElem3 x (x :: ys) | (Yes refl) = ?isElem3_rhs_3

test/interactive003/expected+2−2

@@ -1,5 +1,5 @@

1Type checking ./interactive003.idr

2ys

3−x :: (app xs ys)

3+x :: app xs ys

4[]

5−f x y :: (vzipWith f xs ys)

5+f x y :: vzipWith f xs ys