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

git.iko.soy/Idris-dev

Fix interactive editing and tests

The pretty-printer fix broke parens in interactive editing.

commit77ca4ed4622fa7060cb0e47fb3985b0af2d49d4d authorDavid Raymond Christiansen <david@davidchristiansen.dk> dateFri 2 May 2014, 14:36 (12 years ago) parent7273f3b

5 files changed+13−8

compare with master

unifiedsplit

src/Idris/AbsSyntaxTree.hs+1−1 src/Idris/CaseSplit.hs+4−1 src/Idris/REPL.hs+5−3 test/interactive001/expected+1−1 test/interactive003/expected+2−2

src/Idris/AbsSyntaxTree.hs+1−1

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

12111211 [] -> enclose lparen rparen opName

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

12131213 [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

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

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

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

src/Idris/CaseSplit.hs+4−1

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

2222

2323import Data.Maybe

2424import Data.Char

25+import Data.List (isPrefixOf, isSuffixOf)

2526import Control.Monad

2627import Control.Monad.State.Strict

2728

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

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

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

301302

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

303+ addBrackets tm | ' ' `elem` tm

304+ , not (isPrefixOf "(" tm)

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

303306 | otherwise = tm

304307

305308getUniq nm i

src/Idris/REPL.hs+5−3

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

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

825825 ctxt <- getContext

826826 i <- getIState

827− return $ show (stripNS

828− (dropCtxt envlen

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

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

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

829+ (stripNS

830+ (dropCtxt envlen

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

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

831833 if updatefile then

832834 do let fb = fn ++ "~"

test/interactive001/expected+1−1

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

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

7−f x :: (map f xs)

7+f x :: map f xs

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

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

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

test/interactive003/expected+2−2

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

11Type checking ./interactive003.idr

22ys

3−x :: (app xs ys)

3+x :: app xs ys

44[]

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

5+f x y :: vzipWith f xs ys