7922bb6 · Idris-dev · git.iko.soy

git.iko.soy/Idris-dev

Merge pull request #1175 from david-christiansen/pprint-assoc

Fix associativity in pretty-printer

commit7922bb6d79ea9fced9df788703cd76bba995d291 authorDavid Christiansen <david@davidchristiansen.dk> dateFri 2 May 2014, 15:14 (12 years ago) parentba19708 77ca4ed

10 files changed+108−71

compare with master

unifiedsplit

src/Idris/AbsSyntaxTree.hs+32−6 src/Idris/CaseSplit.hs+4−1 src/Idris/Delaborate.hs+1−1 src/Idris/Docs.hs+22−17 src/Idris/IdrisDoc.hs+2−2 src/Idris/Output.hs+6−4 src/Idris/Prover.hs+13−11 src/Idris/REPL.hs+25−26 test/interactive001/expected+1−1 test/interactive003/expected+2−2

src/Idris/AbsSyntaxTree.hs+32−6

@@ -31,6 +31,7 @@ import qualified Data.Map as M

3131import Data.Either

3232import qualified Data.Set as S

3333import Data.Word (Word)

34+import Data.Maybe (fromMaybe)

3435

3536import Debug.Trace

3637

@@ -1127,19 +1128,24 @@ consoleDecorate ist (AnnTextFmt fmt) = Idris.Colours.colourise (colour fmt)

11271128 colour UnderlineText = IdrisColour Nothing True True False False

11281129 colour ItalicText = IdrisColour Nothing True False False True

11291130

1130−-- | Pretty-print a high-level closed Idris term

1131+-- | Pretty-print a high-level closed Idris term with no information about precedence/associativity

11311132prettyImp :: Bool -- ^^ whether to show implicits

11321133 -> PTerm -- ^^ the term to pretty-print

11331134 -> Doc OutputAnnotation

1134−prettyImp impl = pprintPTerm impl [] []

1135+prettyImp impl = pprintPTerm impl [] [] []

11351136

1136−-- | Pretty-print a high-level Idris term in some bindings context

1137+-- | Do the right thing for rendering a term in an IState

1138+prettyIst :: IState -> PTerm -> Doc OutputAnnotation

1139+prettyIst ist = pprintPTerm (opt_showimp (idris_options ist)) [] [] (idris_infixes ist)

1140+

1141+-- | Pretty-print a high-level Idris term in some bindings context with infix info

11371142pprintPTerm :: Bool -- ^^ whether to show implicits

11381143 -> [(Name, Bool)] -- ^^ the currently-bound names and whether they are implicit

11391144 -> [Name] -- ^^ names to always show in pi, even if not used

1145+ -> [FixDecl] -- ^^ Fixity declarations

11401146 -> PTerm -- ^^ the term to pretty-print

11411147 -> Doc OutputAnnotation

1142−pprintPTerm impl bnd docArgs = prettySe 10 bnd

1148+pprintPTerm impl bnd docArgs infixes = prettySe 10 bnd

11431149 where

11441150 prettySe :: Int -> [(Name, Bool)] -> PTerm -> Doc OutputAnnotation

11451151 prettySe p bnd (PQuote r) =

@@ -1204,13 +1210,23 @@ pprintPTerm impl bnd docArgs = prettySe 10 bnd

12041210 case getExps args of

12051211 [] -> enclose lparen rparen opName

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

1207− [l,r] -> bracket p 1 $ inFix l r

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

1214+ in bracket p precedence $ inFix l r

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

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

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

12111218 where opName = prettyName impl bnd op

1219+ f = getFixity (opStr op)

1220+ left l = case f of

1221+ Nothing -> prettySe (-1) bnd l

1222+ Just (Infixl p') -> prettySe p' bnd l

1223+ Just f' -> prettySe (prec f'-1) bnd l

1224+ right r = case f of

1225+ Nothing -> prettySe (-1) bnd r

1226+ Just (Infixr p') -> prettySe p' bnd r

1227+ Just f' -> prettySe (prec f'-1) bnd r

12121228 inFix l r = align . group $

1213− (prettySe 1 bnd l <+> opName) <$> group (prettySe 0 bnd r)

1229+ (left l <+> opName) <$> group (right r)

12141230 prettySe p bnd (PApp _ hd@(PRef fc f) [tm])

12151231 | PConstant (Idris.Core.TT.Str str) <- getTm tm,

12161232 f == sUN "Symbol_" = char '\'' <> prettySe 10 bnd (PRef fc (sUN str))

@@ -1315,6 +1331,10 @@ pprintPTerm impl bnd docArgs = prettySe 10 bnd

13151331 annName :: Name -> Doc OutputAnnotation -> Doc OutputAnnotation

13161332 annName n = annotate (AnnName n Nothing Nothing Nothing)

13171333

1334+ opStr :: Name -> String

1335+ opStr (NS n _) = opStr n

1336+ opStr (UN n) = T.unpack n

1337+

13181338 basename :: Name -> Name

13191339 basename (NS n _) = basename n

13201340 basename n = n

@@ -1368,6 +1388,12 @@ pprintPTerm impl bnd docArgs = prettySe 10 bnd

13681388

13691389 kwd = annotate AnnKeyword . text

13701390

1391+ fixities :: M.Map String Fixity

1392+ fixities = M.fromList [(s, f) | (Fix f s) <- infixes]

1393+

1394+ getFixity :: String -> Maybe Fixity

1395+ getFixity = flip M.lookup fixities

1396+

13711397-- | Pretty-printer helper for the binding site of a name

13721398bindingOf :: Name -- ^^ the bound name

13731399 -> Bool -- ^^ whether the name is implicit

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/Delaborate.hs+1−1

@@ -138,7 +138,7 @@ pprintTerm :: IState -> PTerm -> Doc OutputAnnotation

138138pprintTerm ist = pprintTerm' ist []

139139

140140pprintTerm' :: IState -> [(Name, Bool)] -> PTerm -> Doc OutputAnnotation

141−pprintTerm' ist bnd tm = pprintPTerm (opt_showimp (idris_options ist)) bnd [] tm

141+pprintTerm' ist bnd = pprintPTerm (opt_showimp (idris_options ist)) bnd [] (idris_infixes ist)

142142

143143pprintErr :: IState -> Err -> Doc OutputAnnotation

144144pprintErr i err = pprintErr' i (fmap (errReverse i) err)

src/Idris/Docs.hs+22−17

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

11{-# LANGUAGE PatternGuards #-}

2−module Idris.Docs where

2+module Idris.Docs (pprintDocs, getDocs, FunDoc(..), Docs (..)) where

44import Idris.AbsSyntax

55import Idris.AbsSyntaxTree

@@ -34,11 +34,11 @@ data Docs = FunDoc FunDoc

3434showDoc d | nullDocstring d = empty

3535 | otherwise = text " -- " <> renderDocstring d

3636

37−pprintFD :: Bool -> FunDoc -> Doc OutputAnnotation

38−pprintFD imp (FD n doc args ty f)

37+pprintFD :: IState -> FunDoc -> Doc OutputAnnotation

38+pprintFD ist (FD n doc args ty f)

3939 = nest 4 (prettyName imp [] n <+> colon <+>

4040 pprintPTerm imp [] [ n | (n@(UN n'),_,_,_) <- args

41− , not (T.isPrefixOf (T.pack "__") n') ] ty <$>

41+ , not (T.isPrefixOf (T.pack "__") n') ] infixes ty <$>

4242 renderDocstring doc <$>

4343 maybe empty (\f -> text (show f) <> line) f <>

4444 let argshow = showArgs args [] in

@@ -46,21 +46,23 @@ pprintFD imp (FD n doc args ty f)

4646 then nest 4 $ text "Arguments:" <$> vsep argshow

4747 else empty)

4848

49− where showArgs ((n, ty, Exp {}, Just d):args) bnd

49+ where imp = opt_showimp (idris_options ist)

50+ infixes = idris_infixes ist

51+ showArgs ((n, ty, Exp {}, Just d):args) bnd

5052 = bindingOf n False <+> colon <+>

51− pprintPTerm imp bnd [] ty <>

53+ pprintPTerm imp bnd [] infixes ty <>

5254 showDoc d <> line

5355 :

5456 showArgs args ((n, False):bnd)

5557 showArgs ((n, ty, Constraint {}, Just d):args) bnd

5658 = text "Class constraint" <+>

57− pprintPTerm imp bnd [] ty <> showDoc d <> line

59+ pprintPTerm imp bnd [] infixes ty <> showDoc d <> line

5860 :

5961 showArgs args ((n, True):bnd)

6062 showArgs ((n, ty, Imp {}, Just d):args) bnd

6163 = text "(implicit)" <+>

6264 bindingOf n True <+> colon <+>

63− pprintPTerm imp bnd [] ty <>

65+ pprintPTerm imp bnd [] infixes ty <>

6466 showDoc d <> line

6567 :

6668 showArgs args ((n, True):bnd)

@@ -68,20 +70,20 @@ pprintFD imp (FD n doc args ty f)

6870 showArgs [] _ = []

6971

7072

71−pprintDocs :: Bool -> Docs -> Doc OutputAnnotation

72−pprintDocs imp (FunDoc d) = pprintFD imp d

73−pprintDocs imp (DataDoc t args)

74− = text "Data type" <+> pprintFD imp t <$>

73+pprintDocs :: IState -> Docs -> Doc OutputAnnotation

74+pprintDocs ist (FunDoc d) = pprintFD ist d

75+pprintDocs ist (DataDoc t args)

76+ = text "Data type" <+> pprintFD ist t <$>

7577 nest 4 (text "Constructors:" <> line <>

76− vsep (map (pprintFD imp) args))

77−pprintDocs imp (ClassDoc n doc meths params instances)

78+ vsep (map (pprintFD ist) args))

79+pprintDocs ist (ClassDoc n doc meths params instances)

7880 = nest 4 (text "Type class" <+> prettyName imp [] n <>

7981 if nullDocstring doc then empty else line <> renderDocstring doc)

8082 <> line <$>

8183 nest 4 (text "Parameters:" <$> prettyParameters)

8284 <> line <$>

8385 nest 4 (text "Methods:" <$>

84− vsep (map (pprintFD imp) meths))

86+ vsep (map (pprintFD ist) meths))

8587 <$>

8688 nest 4 (text "Instances:" <$>

8789 vsep (if null instances' then [text "<no instances>"]

@@ -94,9 +96,12 @@ pprintDocs imp (ClassDoc n doc meths params instances)

9496 params' = zip pNames (repeat False)

9597

9698 pNames = map fst params

97−

99+

100+ imp = opt_showimp (idris_options ist)

101+ infixes = idris_infixes ist

102+

98103 dumpInstance :: PTerm -> Doc OutputAnnotation

99− dumpInstance = pprintPTerm imp params' []

104+ dumpInstance = pprintPTerm imp params' [] infixes

100105

101106 prettifySubclasses (PPi (Constraint _ _) _ tm _) = prettifySubclasses tm

102107 prettifySubclasses (PPi plcity nm t1 t2) = PPi plcity (safeHead nm pNames) (prettifySubclasses t1) (prettifySubclasses t2)

src/Idris/IdrisDoc.hs+2−2

@@ -457,7 +457,7 @@ genTypeHeader ist (FD n _ args ftype _) = do

457457

458458 where

459459 htmlSignature = displayDecorated decorator $ renderCompact signature

460− signature = pprintPTerm False [] names ftype

460+ signature = pprintPTerm False [] names (idris_infixes ist) ftype

461461 names = [ n | (n@(UN n'), _, _, _) <- args,

462462 not (T.isPrefixOf (txt "__") n') ]

463463

@@ -656,4 +656,4 @@ copyDependencies :: FilePath -- ^ The base directory to which

656656 -> IO ()

657657copyDependencies dir =

658658 do styles <- getDataFileName $ "idrisdoc" </> "styles.css"

659− copyFile styles (dir </> "styles.css")

659+ copyFile styles (dir </> "styles.css")

src/Idris/Output.hs+6−4

@@ -78,7 +78,7 @@ ideSlaveReturnAnnotated n h out = do ist <- getIState

7878

7979ihPrintTermWithType :: Handle -> Doc OutputAnnotation -> Doc OutputAnnotation -> Idris ()

8080ihPrintTermWithType h tm ty = do ist <- getIState

81− let output = tm <+> colon <+> ty

81+ let output = tm <+> colon <+> align ty

8282 case idris_outputmode ist of

8383 RawOutput -> consoleDisplayAnnotated h output

8484 IdeSlave n -> ideSlaveReturnAnnotated n h output

@@ -88,12 +88,14 @@ ihPrintFunTypes :: Handle -> [(Name, Bool)] -> Name -> [(Name, PTerm)] -> Idris

8888ihPrintFunTypes h bnd n [] = ihPrintError h $ "No such variable " ++ show n

8989ihPrintFunTypes h bnd n overloads = do imp <- impShow

9090 ist <- getIState

91− let output = vsep (map (uncurry (ppOverload imp)) overloads)

91+ let infixes = idris_infixes ist

92+ let output = vsep (map (uncurry (ppOverload imp infixes)) overloads)

9293 case idris_outputmode ist of

9394 RawOutput -> consoleDisplayAnnotated h output

9495 IdeSlave n -> ideSlaveReturnAnnotated n h output

9596 where fullName n = prettyName True bnd n

96− ppOverload imp n tm = fullName n <+> colon <+> align (pprintPTerm imp bnd [] tm)

97+ ppOverload imp infixes n tm =

98+ fullName n <+> colon <+> align (pprintPTerm imp bnd [] infixes tm)

9799

98100ihRenderResult :: Handle -> Doc OutputAnnotation -> Idris ()

99101ihRenderResult h d = do ist <- getIState

@@ -119,7 +121,7 @@ fancifyAnnots ist annot@(AnnName n _ _ _) =

119121 out = displayS . renderPretty 1.0 50 $ renderDocstring o

120122 return (out "")

121123 getTy :: IState -> Name -> String -- fails if name not already extant!

122− getTy ist n = let theTy = pprintPTerm (opt_showimp (idris_options ist)) [] [] $

124+ getTy ist n = let theTy = pprintPTerm (opt_showimp (idris_options ist)) [] [] (idris_infixes ist) $

123125 delabTy ist n

124126 in (displayS . renderPretty 1.0 50 $ theTy) ""

125127fancifyAnnots _ annot = annot

src/Idris/Prover.hs+13−11

@@ -112,7 +112,7 @@ dumpState ist ps@(PS nm (h:hs) _ _ tm _ _ _ _ _ _ problems i _ _ ctxy _ _ _ _) =

112112 where

113113 showImplicits = opt_showimp (idris_options ist)

114114

115− tPretty bnd t = pprintPTerm showImplicits bnd [] $ delab ist t

115+ tPretty bnd t = pprintPTerm showImplicits bnd [] (idris_infixes ist) $ delab ist t

116116

117117 assumptionNames :: Env -> [Name]

118118 assumptionNames = map fst

@@ -237,15 +237,16 @@ ploop fn d prompt prf e h

237237 ctxt' = envCtxt env ctxt

238238 putIState ist { tt_ctxt = ctxt' }

239239 (tm, ty) <- elabVal toplevel False t

240− let imp = opt_showimp (idris_options ist)

241− ty' = normaliseC ctxt [] ty

242− h = idris_outh ist

240+ let imp = opt_showimp (idris_options ist)

241+ ty' = normaliseC ctxt [] ty

242+ h = idris_outh ist

243+ infixes = idris_infixes ist

243244 case tm of

244245 TType _ ->

245246 ihPrintTermWithType h (prettyImp imp PType) type1Doc

246247 _ -> let bnd = map (\x -> (fst x, False)) env in

247− ihPrintTermWithType h (pprintPTerm imp bnd [] (delab ist tm))

248− (pprintPTerm imp bnd [] (delab ist ty))

248+ ihPrintTermWithType h (pprintPTerm imp bnd [] infixes (delab ist tm))

249+ (pprintPTerm imp bnd [] infixes (delab ist ty))

249250 putIState ist

250251 return (False, e, False, prf))

251252 (\err -> do putIState ist { tt_ctxt = ctxt } ; ierror err)

@@ -259,11 +260,12 @@ ploop fn d prompt prf e h

259260 bnd = map (\x -> (fst x, False)) env

260261 putIState ist'

261262 (tm, ty) <- elabVal toplevel False t

262− let tm' = force (normaliseAll ctxt' env tm)

263− ty' = force (normaliseAll ctxt' env ty)

264− imp = opt_showimp (idris_options ist')

265− tmDoc = pprintPTerm imp bnd [] (delab ist' tm')

266− tyDoc = pprintPTerm imp bnd [] (delab ist' ty')

263+ let tm' = force (normaliseAll ctxt' env tm)

264+ ty' = force (normaliseAll ctxt' env ty)

265+ imp = opt_showimp (idris_options ist')

266+ infixes = idris_infixes ist

267+ tmDoc = pprintPTerm imp bnd [] infixes (delab ist' tm')

268+ tyDoc = pprintPTerm imp bnd [] infixes (delab ist' ty')

267269 ihPrintTermWithType (idris_outh ist') tmDoc tyDoc

268270 putIState ist

269271 return (False, e, False, prf))

src/Idris/REPL.hs+25−26

@@ -327,8 +327,9 @@ runIdeSlaveCommand id orig fn mods (IdeSlave.Metavariables cols) =

327327 -> ([(String, String, SpanList OutputAnnotation)],

328328 (String, SpanList OutputAnnotation))

329329 sexpGoal ist cols imp ns ([], concl) =

330− let concl' = displaySpans . renderPretty 0.9 cols . fmap (fancifyAnnots ist) $

331− pprintPTerm imp (zip ns (repeat False)) [] concl

330+ let infixes = idris_infixes ist

331+ concl' = displaySpans . renderPretty 0.9 cols . fmap (fancifyAnnots ist) $

332+ pprintPTerm imp (zip ns (repeat False)) [] infixes concl

332333 in ([], concl')

333334 sexpGoal ist cols imp ns ((n, t):ps, concl) =

334335 let n' = case n of

@@ -337,7 +338,7 @@ runIdeSlaveCommand id orig fn mods (IdeSlave.Metavariables cols) =

337338 | otherwise -> str nm

338339 _ -> "_"

339340 (t', spans) = displaySpans . renderPretty 0.9 cols . fmap (fancifyAnnots ist) $

340− pprintPTerm imp (zip ns (repeat False)) [] t

341+ pprintPTerm imp (zip ns (repeat False)) [] (idris_infixes ist) t

341342 rest = sexpGoal ist cols imp (n:ns) (ps, concl)

342343 in ((n', t', spans) : fst rest, snd rest)

343344runIdeSlaveCommand id orig fn mods (IdeSlave.WhoCalls n) =

@@ -562,21 +563,19 @@ process h fn (Eval t)

562563 ist <- getIState

563564 logLvl 3 $ "Raw: " ++ show (tm', ty')

564565 logLvl 10 $ "Debug: " ++ showEnvDbg [] tm'

565− let imp = opt_showimp (idris_options ist)

566− tmDoc = prettyImp imp (delab ist tm')

567− tyDoc = prettyImp imp (delab ist ty')

566+ let tmDoc = prettyIst ist (delab ist tm')

567+ tyDoc = prettyIst ist (delab ist ty')

568568 ihPrintTermWithType h tmDoc tyDoc

569569

570570process h fn (ExecVal t)

571571 = do ctxt <- getContext

572572 ist <- getIState

573− let imp = opt_showimp (idris_options ist)

574573 (tm, ty) <- elabVal toplevel False t

575574-- let tm' = normaliseAll ctxt [] tm

576575 let ty' = normaliseAll ctxt [] ty

577576 res <- execute tm

578− let (resOut, tyOut) = (prettyImp imp (delab ist res),

579− prettyImp imp (delab ist ty'))

577+ let (resOut, tyOut) = (prettyIst ist (delab ist res),

578+ prettyIst ist (delab ist ty'))

580579 ihPrintTermWithType h resOut tyOut

581580

582581process h fn (Check (PRef _ n))

@@ -611,7 +610,7 @@ process h fn (Check (PRef _ n))

611610 annotate (AnnName n Nothing Nothing Nothing) (text $ show n) <+> colon <+>

612611 align (tPretty bnd ist g)

613612

614− tPretty bnd ist t = pprintPTerm (opt_showimp (idris_options ist)) bnd [] t

613+ tPretty bnd ist t = pprintPTerm (opt_showimp (idris_options ist)) bnd [] (idris_infixes ist) t

615614

616615

617616process h fn (Check t)

@@ -622,19 +621,18 @@ process h fn (Check t)

622621 ty' = normaliseC ctxt [] ty

623622 case tm of

624623 TType _ ->

625− ihPrintTermWithType h (prettyImp imp PType) type1Doc

626− _ -> ihPrintTermWithType h (prettyImp imp (delab ist tm))

627− (prettyImp imp (delab ist ty))

624+ ihPrintTermWithType h (prettyIst ist PType) type1Doc

625+ _ -> ihPrintTermWithType h (prettyIst ist (delab ist tm))

626+ (prettyIst ist (delab ist ty))

628627

629628process h fn (DocStr n)

630− = do i <- getIState

631− let imp = opt_showimp (idris_options i)

632− case lookupCtxtName n (idris_docstrings i) of

629+ = do ist <- getIState

630+ case lookupCtxtName n (idris_docstrings ist) of

633631 [] -> iPrintError $ "No documentation for " ++ show n

634− ns -> do toShow <- mapM (showDoc imp) ns

632+ ns -> do toShow <- mapM (showDoc ist) ns

635633 ihRenderResult h (vsep toShow)

636− where showDoc imp (n, d) = do doc <- getDocs n

637− return $ pprintDocs imp doc

634+ where showDoc ist (n, d) = do doc <- getDocs n

635+ return $ pprintDocs ist doc

638636process h fn Universes

639637 = do i <- getIState

640638 let cs = idris_constraints i

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

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

827825 ctxt <- getContext

828826 i <- getIState

829− return $ show (stripNS

830− (dropCtxt envlen

831− (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)))))

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

833833 if updatefile then

834834 do let fb = fn ++ "~"

@@ -1051,15 +1051,14 @@ process h fn (SetConsoleWidth w) = setWidth w

10511051

10521052process h fn (Apropos a) =

10531053 do ist <- getIState

1054− let impl = opt_showimp (idris_options ist)

10551054 let names = apropos ist (T.pack a)

10561055 let aproposInfo = [ (n,

10571056 delabTy ist n,

10581057 fmap (overview . fst) (lookupCtxtExact n (idris_docstrings ist)))

10591058 | n <- sort names, isUN n ]

1060− ihRenderResult h $ vsep (map (renderApropos impl) aproposInfo)

1061− where renderApropos impl (name, ty, docs) =

1062− prettyName True [] name <+> colon <+> align (prettyImp impl ty) <$>

1059+ ihRenderResult h $ vsep (map (renderApropos ist) aproposInfo)

1060+ where renderApropos ist (name, ty, docs) =

1061+ prettyName True [] name <+> colon <+> align (prettyIst ist ty) <$>

10631062 fromMaybe empty (fmap (\d -> renderDocstring d <> line) docs)

10641063 isUN (UN _) = True

10651064 isUN (NS n _) = isUN n

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