git.iko.soy/Idris-dev
on master help sign in
Add maximum pretty-printer depth option.

The default is set to a high but finite number, so that accidentally evaluating infinite things doesn't cause Idris to hang. Fixes #2333.

commit5542d1cfc5f4c486973795150a0392638e0ba996 authorDavid Raymond Christiansen <david@davidchristiansen.dk> dateWed 3 Jun 2015, 14:40 (11 years ago) parentfe4c09d
13 files changed+429−159
compare with master
unifiedsplit
CHANGELOG+4 docs/reference/repl.rst+2 idris.cabal+3 src/Idris/AbsSyntax.hs+3−1 src/Idris/AbsSyntaxTree.hs+154−137 src/Idris/Core/TT.hs+16 src/Idris/IdeMode.hs+3−1 src/Idris/REPL.hs+21−17 src/Idris/REPLParser.hs+7−2 test/error004/expected+1−1 test/interactive008/expected+204 test/interactive008/input+9 test/interactive008/run+2
CHANGELOG+4
@@ -5,6 +5,10 @@ New in 0.9.19:
55* The Show class has been moved into Prelude.Show and augmented with the method
66 showPrec, which allows correct parenthesization of showed terms. This comes
77 with the type Prec of precedences and a few helper functions.
8+* New REPL command :printerdepth that sets the pretty-printer to only descend to
9+ some particular depth when printing. The default is set to a high number to
10+ make it less dangerous to experiment with infinite structures. Infinite depth
11+ can be set by calling :printerdepth with no argument.
812
913New in 0.9.18:
1014--------------
docs/reference/repl.rst+2
@@ -136,6 +136,8 @@ The current set of supported commands are:
136136+----------------+------------------------------+----------------------------------------------------------------------------------------------------------+
137137|:consolewidth | auto|infinite|<number> | Set the width of the console |
138138+----------------+------------------------------+----------------------------------------------------------------------------------------------------------+
139+|:printerdepth | <number-or-blank> | Set the maximum pretty-printing depth, or infinite if nothing specified |
140++----------------+------------------------------+----------------------------------------------------------------------------------------------------------+
139141|:q :quit | | Exit the Idris system |
140142+----------------+------------------------------+----------------------------------------------------------------------------------------------------------+
141143|:w :warranty | | Displays warranty information |
idris.cabal+3
@@ -526,6 +526,9 @@ Extra-source-files:
526526 test/interactive007/run
527527 test/interactive007/input
528528 test/interactive007/expected
529+ test/interactive008/run
530+ test/interactive008/input
531+ test/interactive008/expected
529532
530533 test/io001/run
531534 test/io001/*.idr
src/Idris/AbsSyntax.hs+3−1
@@ -637,7 +637,9 @@ setWidth :: ConsoleWidth -> Idris ()
637637setWidth w = do ist <- getIState
638638 put ist { idris_consolewidth = w }
639639
640−
640+setDepth :: Maybe Int -> Idris ()
641+setDepth d = do ist <- getIState
642+ put ist { idris_options = (idris_options ist) { opt_printdepth = d } }
641643
642644
643645type1Doc :: Doc OutputAnnotation
src/Idris/AbsSyntaxTree.hs+154−137
@@ -88,7 +88,8 @@ data IOption = IOption { opt_logLevel :: Int,
8888 opt_origerr :: Bool,
8989 opt_autoSolve :: Bool, -- ^ automatically apply "solve" tactic in prover
9090 opt_autoImport :: [FilePath], -- ^ e.g. Builtins+Prelude
91− opt_optimise :: [Optimisation]
91+ opt_optimise :: [Optimisation],
92+ opt_printdepth :: Maybe Int
9293 }
9394 deriving (Show, Eq)
9495
@@ -113,10 +114,12 @@ defaultOpts = IOption { opt_logLevel = 0
113114 , opt_autoSolve = True
114115 , opt_autoImport = []
115116 , opt_optimise = defaultOptimise
117+ , opt_printdepth = Just 5000
116118 }
117119
118120data PPOption = PPOption {
119121 ppopt_impl :: Bool -- ^^ whether to show implicits
122+ , ppopt_depth :: Maybe Int
120123} deriving (Show)
121124
122125data Optimisation = PETransform -- partial eval and associated transforms
@@ -126,16 +129,17 @@ defaultOptimise = [PETransform]
126129
127130-- | Pretty printing options with default verbosity.
128131defaultPPOption :: PPOption
129−defaultPPOption = PPOption { ppopt_impl = False }
132+defaultPPOption = PPOption { ppopt_impl = False , ppopt_depth = Just 200 }
130133
131134-- | Pretty printing options with the most verbosity.
132135verbosePPOption :: PPOption
133−verbosePPOption = PPOption { ppopt_impl = True }
136+verbosePPOption = PPOption { ppopt_impl = True, ppopt_depth = Just 200 }
134137
135138-- | Get pretty printing options from the big options record.
136139ppOption :: IOption -> PPOption
137140ppOption opt = PPOption {
138− ppopt_impl = opt_showimp opt
141+ ppopt_impl = opt_showimp opt,
142+ ppopt_depth = opt_printdepth opt
139143}
140144
141145-- | Get pretty printing options from an idris state record.
@@ -406,6 +410,7 @@ data Command = Quit
406410 | ColourOff
407411 | ListErrorHandlers
408412 | SetConsoleWidth ConsoleWidth
413+ | SetPrinterDepth (Maybe Int)
409414 | Apropos [String] String
410415 | WhoCalls Name
411416 | CallsWho Name
@@ -1441,96 +1446,97 @@ pprintPTerm :: PPOption -- ^^ pretty printing options
14411446 -> [FixDecl] -- ^^ Fixity declarations
14421447 -> PTerm -- ^^ the term to pretty-print
14431448 -> Doc OutputAnnotation
1444−pprintPTerm ppo bnd docArgs infixes = prettySe startPrec bnd
1449+pprintPTerm ppo bnd docArgs infixes = prettySe (ppopt_depth ppo) startPrec bnd
14451450 where
14461451 startPrec = 0
14471452 funcAppPrec = 10
14481453
1449− prettySe :: Int -> [(Name, Bool)] -> PTerm -> Doc OutputAnnotation
1450− prettySe p bnd (PQuote r) =
1454+ prettySe :: Maybe Int -> Int -> [(Name, Bool)] -> PTerm -> Doc OutputAnnotation
1455+ prettySe d p bnd (PQuote r) =
14511456 text "![" <> pretty r <> text "]"
1452− prettySe p bnd (PPatvar fc n) = pretty n
1453− prettySe p bnd e
1454− | Just str <- slist p bnd e = str
1455− | Just n <- snat p e = annotate (AnnData "Nat" "") (text (show n))
1456− prettySe p bnd (PRef fc n) = prettyName True (ppopt_impl ppo) bnd n
1457− prettySe p bnd (PLam fc n nfc ty sc) =
1458− bracket p startPrec . group . align . hang 2 $
1457+ prettySe d p bnd (PPatvar fc n) = pretty n
1458+ prettySe d p bnd e
1459+ | Just str <- slist d p bnd e = depth d $ str
1460+ | Just n <- snat d p e = depth d $ annotate (AnnData "Nat" "") (text (show n))
1461+ prettySe d p bnd (PRef fc n) = prettyName True (ppopt_impl ppo) bnd n
1462+ prettySe d p bnd (PLam fc n nfc ty sc) =
1463+ depth d . bracket p startPrec . group . align . hang 2 $
14591464 text "\\" <> prettyBindingOf n False <+> text "=>" <$>
1460− prettySe startPrec ((n, False):bnd) sc
1461− prettySe p bnd (PLet fc n nfc ty v sc) =
1462− bracket p startPrec . group . align $
1463− kwd "let" <+> (group . align . hang 2 $ prettyBindingOf n False <+> text "=" <$> prettySe startPrec bnd v) </>
1464− kwd "in" <+> (group . align . hang 2 $ prettySe startPrec ((n, False):bnd) sc)
1465− prettySe p bnd (PPi (Exp l s _) n _ ty sc)
1465+ prettySe (decD d) startPrec ((n, False):bnd) sc
1466+ prettySe d p bnd (PLet fc n nfc ty v sc) =
1467+ depth d . bracket p startPrec . group . align $
1468+ kwd "let" <+> (group . align . hang 2 $ prettyBindingOf n False <+> text "=" <$> prettySe (decD d) startPrec bnd v) </>
1469+ kwd "in" <+> (group . align . hang 2 $ prettySe (decD d) startPrec ((n, False):bnd) sc)
1470+ prettySe d p bnd (PPi (Exp l s _) n _ ty sc)
14661471 | n `elem` allNamesIn sc || ppopt_impl ppo || n `elem` docArgs =
1467− bracket p startPrec . group $
1468− enclose lparen rparen (group . align $ prettyBindingOf n False <+> colon <+> prettySe startPrec bnd ty) <+>
1469− st <> text "->" <$> prettySe startPrec ((n, False):bnd) sc
1472+ depth d . bracket p startPrec . group $
1473+ enclose lparen rparen (group . align $ prettyBindingOf n False <+> colon <+> prettySe (decD d) startPrec bnd ty) <+>
1474+ st <> text "->" <$> prettySe (decD d) startPrec ((n, False):bnd) sc
14701475 | otherwise =
1471− bracket p startPrec . group $
1472− group (prettySe (startPrec + 1) bnd ty <+> st) <> text "->" <$> group (prettySe startPrec ((n, False):bnd) sc)
1476+ depth d . bracket p startPrec . group $
1477+ group (prettySe (decD d) (startPrec + 1) bnd ty <+> st) <> text "->" <$>
1478+ group (prettySe (decD d) startPrec ((n, False):bnd) sc)
14731479 where
14741480 st =
14751481 case s of
14761482 Static -> text "[static]" <> space
14771483 _ -> empty
1478− prettySe p bnd (PPi (Imp l s _ fa) n _ ty sc)
1484+ prettySe d p bnd (PPi (Imp l s _ fa) n _ ty sc)
14791485 | ppopt_impl ppo =
1480− bracket p startPrec $
1481− lbrace <> prettyBindingOf n True <+> colon <+> prettySe startPrec bnd ty <> rbrace <+>
1482− st <> text "->" </> prettySe startPrec ((n, True):bnd) sc
1483− | otherwise = prettySe startPrec ((n, True):bnd) sc
1486+ depth d . bracket p startPrec $
1487+ lbrace <> prettyBindingOf n True <+> colon <+> prettySe (decD d) startPrec bnd ty <> rbrace <+>
1488+ st <> text "->" </> prettySe (decD d) startPrec ((n, True):bnd) sc
1489+ | otherwise = depth d $ prettySe (decD d) startPrec ((n, True):bnd) sc
14841490 where
14851491 st =
14861492 case s of
14871493 Static -> text "[static]" <> space
14881494 _ -> empty
1489− prettySe p bnd (PPi (Constraint _ _) n _ ty sc) =
1490− bracket p startPrec $
1491− prettySe (startPrec + 1) bnd ty <+> text "=>" </> prettySe startPrec ((n, True):bnd) sc
1492− prettySe p bnd (PPi (TacImp _ _ (PTactics [ProofSearch _ _ _ _ _])) n _ ty sc) =
1493− lbrace <> kwd "auto" <+> pretty n <+> colon <+> prettySe startPrec bnd ty <>
1494− rbrace <+> text "->" </> prettySe startPrec ((n, True):bnd) sc
1495− prettySe p bnd (PPi (TacImp _ _ s) n _ ty sc) =
1496− bracket p startPrec $
1497− lbrace <> kwd "default" <+> prettySe (funcAppPrec + 1) bnd s <+> pretty n <+> colon <+> prettySe startPrec bnd ty <>
1498− rbrace <+> text "->" </> prettySe startPrec ((n, True):bnd) sc
1495+ prettySe d p bnd (PPi (Constraint _ _) n _ ty sc) =
1496+ depth d . bracket p startPrec $
1497+ prettySe (decD d) (startPrec + 1) bnd ty <+> text "=>" </> prettySe (decD d) startPrec ((n, True):bnd) sc
1498+ prettySe d p bnd (PPi (TacImp _ _ (PTactics [ProofSearch _ _ _ _ _])) n _ ty sc) =
1499+ lbrace <> kwd "auto" <+> pretty n <+> colon <+> prettySe (decD d) startPrec bnd ty <>
1500+ rbrace <+> text "->" </> prettySe (decD d) startPrec ((n, True):bnd) sc
1501+ prettySe d p bnd (PPi (TacImp _ _ s) n _ ty sc) =
1502+ depth d . bracket p startPrec $
1503+ lbrace <> kwd "default" <+> prettySe (decD d) (funcAppPrec + 1) bnd s <+> pretty n <+> colon <+> prettySe (decD d) startPrec bnd ty <>
1504+ rbrace <+> text "->" </> prettySe (decD d) startPrec ((n, True):bnd) sc
14991505 -- This case preserves the behavior of the former constructor PEq.
15001506 -- It should be removed if feasible when the pretty-printing of infix
15011507 -- operators in general is improved.
1502− prettySe p bnd (PApp _ (PRef _ n) [lt, rt, l, r])
1508+ prettySe d p bnd (PApp _ (PRef _ n) [lt, rt, l, r])
15031509 | n == eqTy, ppopt_impl ppo =
1504− bracket p eqPrec $
1510+ depth d . bracket p eqPrec $
15051511 enclose lparen rparen eq <+>
1506− align (group (vsep (map (prettyArgS bnd)
1512+ align (group (vsep (map (prettyArgS (decD d) bnd)
15071513 [lt, rt, l, r])))
15081514 | n == eqTy =
1509− bracket p eqPrec . align . group $
1515+ depth d . bracket p eqPrec . align . group $
15101516 prettyTerm (getTm l) <+> eq <$> group (prettyTerm (getTm r))
15111517 where eq = annName eqTy (text "=")
15121518 eqPrec = startPrec
1513− prettyTerm = prettySe (eqPrec + 1) bnd
1514− prettySe p bnd (PApp _ (PRef _ f) args) -- normal names, no explicit args
1519+ prettyTerm = prettySe (decD d) (eqPrec + 1) bnd
1520+ prettySe d p bnd (PApp _ (PRef _ f) args) -- normal names, no explicit args
15151521 | UN nm <- basename f
15161522 , not (ppopt_impl ppo) && null (getShowArgs args) =
15171523 prettyName True (ppopt_impl ppo) bnd f
1518− prettySe p bnd (PAppBind _ (PRef _ f) [])
1524+ prettySe d p bnd (PAppBind _ (PRef _ f) [])
15191525 | not (ppopt_impl ppo) = text "!" <> prettyName True (ppopt_impl ppo) bnd f
1520− prettySe p bnd (PApp _ (PRef _ op) args) -- infix operators
1526+ prettySe d p bnd (PApp _ (PRef _ op) args) -- infix operators
15211527 | UN nm <- basename op
15221528 , not (tnull nm) &&
15231529 (not (ppopt_impl ppo)) && (not $ isAlpha (thead nm)) =
15241530 case getShowArgs args of
15251531 [] -> opName True
1526− [x] -> group (opName True <$> group (prettySe startPrec bnd (getTm x)))
1532+ [x] -> group (opName True <$> group (prettySe (decD d) startPrec bnd (getTm x)))
15271533 [l,r] -> let precedence = maybe (startPrec - 1) prec f
1528− in bracket p precedence $ inFix (getTm l) (getTm r)
1534+ in depth d . bracket p precedence $ inFix (getTm l) (getTm r)
15291535 (l@(PExp _ _ _ _) : r@(PExp _ _ _ _) : rest) ->
1530− bracket p funcAppPrec $
1536+ depth d . bracket p funcAppPrec $
15311537 enclose lparen rparen (inFix (getTm l) (getTm r)) <+>
1532− align (group (vsep (map (prettyArgS bnd) rest)))
1533− as -> opName True <+> align (vsep (map (prettyArgS bnd) as))
1538+ align (group (vsep (map (prettyArgS d bnd) rest)))
1539+ as -> opName True <+> align (vsep (map (prettyArgS d bnd) as))
15341540 where opName isPrefix = prettyName isPrefix (ppopt_impl ppo) bnd op
15351541 f = getFixity (opStr op)
15361542 left = case f of
@@ -1542,26 +1548,26 @@ pprintPTerm ppo bnd docArgs infixes = prettySe startPrec bnd
15421548 Just (Infixr p') -> p'
15431549 Just f' -> prec f' + 1
15441550 inFix l r = align . group $
1545− (prettySe left bnd l <+> opName False) <$>
1546− group (prettySe right bnd r)
1547− prettySe p bnd (PApp _ hd@(PRef fc f) [tm]) -- symbols, like 'foo
1551+ (prettySe (decD d) left bnd l <+> opName False) <$>
1552+ group (prettySe (decD d) right bnd r)
1553+ prettySe d p bnd (PApp _ hd@(PRef fc f) [tm]) -- symbols, like 'foo
15481554 | PConstant NoFC (Idris.Core.TT.Str str) <- getTm tm,
15491555 f == sUN "Symbol_" = annotate (AnnType ("'" ++ str) ("The symbol " ++ str)) $
1550− char '\'' <> prettySe startPrec bnd (PRef fc (sUN str))
1551− prettySe p bnd (PApp _ f as) = -- Normal prefix applications
1556+ char '\'' <> prettySe (decD d) startPrec bnd (PRef fc (sUN str))
1557+ prettySe d p bnd (PApp _ f as) = -- Normal prefix applications
15521558 let args = getShowArgs as
1553− fp = prettySe (startPrec + 1) bnd f
1559+ fp = prettySe (decD d) (startPrec + 1) bnd f
15541560 shownArgs = if ppopt_impl ppo then as else args
15551561 in
1556− bracket p funcAppPrec . group $
1562+ depth d . bracket p funcAppPrec . group $
15571563 if null shownArgs
15581564 then fp
1559− else fp <+> align (vsep (map (prettyArgS bnd) shownArgs))
1560− prettySe p bnd (PCase _ scr cases) =
1561− align $ kwd "case" <+> prettySe startPrec bnd scr <+> kwd "of" <$>
1562− indent 2 (vsep (map ppcase cases))
1565+ else fp <+> align (vsep (map (prettyArgS d bnd) shownArgs))
1566+ prettySe d p bnd (PCase _ scr cases) =
1567+ align $ kwd "case" <+> prettySe (decD d) startPrec bnd scr <+> kwd "of" <$>
1568+ depth d (indent 2 (vsep (map ppcase cases)))
15631569 where
1564− ppcase (l, r) = let prettyCase = prettySe startPrec
1570+ ppcase (l, r) = let prettyCase = prettySe (decD d) startPrec
15651571 ([(n, False) | n <- vars l] ++ bnd)
15661572 in nest nestingSize $
15671573 prettyCase l <+> text "=>" <+> prettyCase r
@@ -1579,70 +1585,71 @@ pprintPTerm ppo bnd docArgs infixes = prettySe startPrec bnd
15791585 noNS (NS _ _) = False
15801586 noNS _ = True
15811587
1582− prettySe p bnd (PIfThenElse _ c t f) =
1583− group . align . hang 2 . vsep $
1584− [ kwd "if" <+> prettySe startPrec bnd c
1585− , kwd "then" <+> prettySe startPrec bnd t
1586− , kwd "else" <+> prettySe startPrec bnd f
1588+ prettySe d p bnd (PIfThenElse _ c t f) =
1589+ depth d . group . align . hang 2 . vsep $
1590+ [ kwd "if" <+> prettySe (decD d) startPrec bnd c
1591+ , kwd "then" <+> prettySe (decD d) startPrec bnd t
1592+ , kwd "else" <+> prettySe (decD d) startPrec bnd f
15871593 ]
1588− prettySe p bnd (PHidden tm) = text "." <> prettySe funcAppPrec bnd tm
1589− prettySe p bnd (PResolveTC _) = kwd "%instance"
1590− prettySe p bnd (PTrue _ IsType) = annName unitTy $ text "()"
1591− prettySe p bnd (PTrue _ IsTerm) = annName unitCon $ text "()"
1592− prettySe p bnd (PTrue _ TypeOrTerm) = text "()"
1593− prettySe p bnd (PRewrite _ l r _) =
1594− bracket p startPrec $
1595− text "rewrite" <+> prettySe (startPrec + 1) bnd l <+> text "in" <+> prettySe startPrec bnd r
1596− prettySe p bnd (PTyped l r) =
1597− lparen <> prettySe startPrec bnd l <+> colon <+> prettySe startPrec bnd r <> rparen
1598− prettySe p bnd pair@(PPair _ pun _ _) -- flatten tuples to the right, like parser
1599− | Just elts <- pairElts pair = enclose (ann lparen) (ann rparen) .
1594+ prettySe d p bnd (PHidden tm) = text "." <> prettySe (decD d) funcAppPrec bnd tm
1595+ prettySe d p bnd (PResolveTC _) = kwd "%instance"
1596+ prettySe d p bnd (PTrue _ IsType) = annName unitTy $ text "()"
1597+ prettySe d p bnd (PTrue _ IsTerm) = annName unitCon $ text "()"
1598+ prettySe d p bnd (PTrue _ TypeOrTerm) = text "()"
1599+ prettySe d p bnd (PRewrite _ l r _) =
1600+ depth d . bracket p startPrec $
1601+ text "rewrite" <+> prettySe (decD d) (startPrec + 1) bnd l <+> text "in" <+> prettySe (decD d) startPrec bnd r
1602+ prettySe d p bnd (PTyped l r) =
1603+ lparen <> prettySe (decD d) startPrec bnd l <+> colon <+> prettySe (decD d) startPrec bnd r <> rparen
1604+ prettySe d p bnd pair@(PPair _ pun _ _) -- flatten tuples to the right, like parser
1605+ | Just elts <- pairElts pair = depth d . enclose (ann lparen) (ann rparen) .
16001606 align . group . vsep . punctuate (ann comma) $
1601− map (prettySe startPrec bnd) elts
1607+ map (prettySe (decD d) startPrec bnd) elts
16021608 where ann = case pun of
16031609 TypeOrTerm -> id
16041610 IsType -> annName pairTy
16051611 IsTerm -> annName pairCon
1606− prettySe p bnd (PDPair _ pun l t r) =
1612+ prettySe d p bnd (PDPair _ pun l t r) =
1613+ depth d $
16071614 annotated lparen <>
16081615 left <+>
16091616 annotated (text "**") <+>
1610− prettySe startPrec (addBinding bnd) r <>
1617+ prettySe (decD d) startPrec (addBinding bnd) r <>
16111618 annotated rparen
16121619 where annotated = case pun of
16131620 IsType -> annName sigmaTy
16141621 IsTerm -> annName sigmaCon
16151622 TypeOrTerm -> id
16161623 (left, addBinding) = case (l, pun) of
1617− (PRef _ n, IsType) -> (bindingOf n False <+> text ":" <+> prettySe startPrec bnd t, ((n, False) :))
1618− _ -> (prettySe startPrec bnd l, id )
1619− prettySe p bnd (PAlternative a as) =
1624+ (PRef _ n, IsType) -> (bindingOf n False <+> text ":" <+> prettySe (decD d) startPrec bnd t, ((n, False) :))
1625+ _ -> (prettySe (decD d) startPrec bnd l, id )
1626+ prettySe d p bnd (PAlternative a as) =
16201627 lparen <> text "|" <> prettyAs <> text "|" <> rparen
16211628 where
16221629 prettyAs =
1623− foldr (\l -> \r -> l <+> text "," <+> r) empty $ map (prettySe startPrec bnd) as
1624− prettySe p bnd (PType _) = annotate (AnnType "Type" "The type of types") $ text "Type"
1625− prettySe p bnd (PUniverse u) = annotate (AnnType (show u) "The type of unique types") $ text (show u)
1626− prettySe p bnd (PConstant _ c) = annotate (AnnConst c) (text (show c))
1630+ foldr (\l -> \r -> l <+> text "," <+> r) empty $ map (depth d . prettySe (decD d) startPrec bnd) as
1631+ prettySe d p bnd (PType _) = annotate (AnnType "Type" "The type of types") $ text "Type"
1632+ prettySe d p bnd (PUniverse u) = annotate (AnnType (show u) "The type of unique types") $ text (show u)
1633+ prettySe d p bnd (PConstant _ c) = annotate (AnnConst c) (text (show c))
16271634 -- XXX: add pretty for tactics
1628− prettySe p bnd (PProof ts) =
1629− kwd "proof" <+> lbrace <> text "..." <> rbrace
1630− prettySe p bnd (PTactics ts) =
1631− kwd "tactics" <+> lbrace <> text "..." <> rbrace
1632− prettySe p bnd (PMetavar _ n) = annotate (AnnName n (Just MetavarOutput) Nothing Nothing) $ text "?" <> pretty n
1633− prettySe p bnd (PReturn f) = kwd "return"
1634− prettySe p bnd PImpossible = kwd "impossible"
1635− prettySe p bnd Placeholder = text "_"
1636− prettySe p bnd (PDoBlock _) = text "do block pretty not implemented"
1637− prettySe p bnd (PCoerced t) = prettySe p bnd t
1638− prettySe p bnd (PElabError s) = pretty s
1635+ prettySe d p bnd (PProof ts) =
1636+ kwd "proof" <+> lbrace <> ellipsis <> rbrace
1637+ prettySe d p bnd (PTactics ts) =
1638+ kwd "tactics" <+> lbrace <> ellipsis <> rbrace
1639+ prettySe d p bnd (PMetavar _ n) = annotate (AnnName n (Just MetavarOutput) Nothing Nothing) $ text "?" <> pretty n
1640+ prettySe d p bnd (PReturn f) = kwd "return"
1641+ prettySe d p bnd PImpossible = kwd "impossible"
1642+ prettySe d p bnd Placeholder = text "_"
1643+ prettySe d p bnd (PDoBlock _) = text "do block pretty not implemented"
1644+ prettySe d p bnd (PCoerced t) = prettySe d p bnd t
1645+ prettySe d p bnd (PElabError s) = pretty s
16391646 -- Quasiquote pprinting ignores bound vars
1640− prettySe p bnd (PQuasiquote t Nothing) = text "`(" <> prettySe p [] t <> text ")"
1641− prettySe p bnd (PQuasiquote t (Just g)) = text "`(" <> prettySe p [] t <+> colon <+> prettySe p [] g <> text ")"
1642− prettySe p bnd (PUnquote t) = text "~" <> prettySe p bnd t
1643− prettySe p bnd (PQuoteName n) = text "`{" <> prettyName True (ppopt_impl ppo) bnd n <> text "}"
1647+ prettySe d p bnd (PQuasiquote t Nothing) = text "`(" <> prettySe (decD d) p [] t <> text ")"
1648+ prettySe d p bnd (PQuasiquote t (Just g)) = text "`(" <> prettySe (decD d) p [] t <+> colon <+> prettySe (decD d) p [] g <> text ")"
1649+ prettySe d p bnd (PUnquote t) = text "~" <> prettySe (decD d) p bnd t
1650+ prettySe d p bnd (PQuoteName n) = text "`{" <> prettyName True (ppopt_impl ppo) bnd n <> text "}"
16441651
1645− prettySe p bnd _ = text "missing pretty-printer for term"
1652+ prettySe d p bnd _ = text "missing pretty-printer for term"
16461653
16471654 prettyBindingOf :: Name -> Bool -> Doc OutputAnnotation
16481655 prettyBindingOf n imp = annotate (AnnBoundName n imp) (text (display n))
@@ -1652,15 +1659,15 @@ pprintPTerm ppo bnd docArgs infixes = prettySe startPrec bnd
16521659 display (NS n ns) = (concat . intersperse "." . map T.unpack . reverse) ns ++ "." ++ display n
16531660 display n = show n
16541661
1655− prettyArgS bnd (PImp _ _ _ n tm) = prettyArgSi bnd (n, tm)
1656− prettyArgS bnd (PExp _ _ _ tm) = prettyArgSe bnd tm
1657− prettyArgS bnd (PConstraint _ _ _ tm) = prettyArgSc bnd tm
1658− prettyArgS bnd (PTacImplicit _ _ n _ tm) = prettyArgSti bnd (n, tm)
1662+ prettyArgS d bnd (PImp _ _ _ n tm) = prettyArgSi d bnd (n, tm)
1663+ prettyArgS d bnd (PExp _ _ _ tm) = prettyArgSe d bnd tm
1664+ prettyArgS d bnd (PConstraint _ _ _ tm) = prettyArgSc d bnd tm
1665+ prettyArgS d bnd (PTacImplicit _ _ n _ tm) = prettyArgSti d bnd (n, tm)
16591666
1660− prettyArgSe bnd arg = prettySe (funcAppPrec + 1) bnd arg
1661− prettyArgSi bnd (n, val) = lbrace <> pretty n <+> text "=" <+> prettySe startPrec bnd val <> rbrace
1662− prettyArgSc bnd val = lbrace <> lbrace <> prettySe startPrec bnd val <> rbrace <> rbrace
1663− prettyArgSti bnd (n, val) = lbrace <> kwd "auto" <+> pretty n <+> text "=" <+> prettySe startPrec bnd val <> rbrace
1667+ prettyArgSe d bnd arg = prettySe d (funcAppPrec + 1) bnd arg
1668+ prettyArgSi d bnd (n, val) = lbrace <> pretty n <+> text "=" <+> prettySe (decD d) startPrec bnd val <> rbrace
1669+ prettyArgSc d bnd val = lbrace <> lbrace <> prettySe (decD d) startPrec bnd val <> rbrace <> rbrace
1670+ prettyArgSti d bnd (n, val) = lbrace <> kwd "auto" <+> pretty n <+> text "=" <+> prettySe (decD d) startPrec bnd val <> rbrace
16641671
16651672 annName :: Name -> Doc OutputAnnotation -> Doc OutputAnnotation
16661673 annName n = annotate (AnnName n Nothing Nothing Nothing)
@@ -1669,35 +1676,36 @@ pprintPTerm ppo bnd docArgs infixes = prettySe startPrec bnd
16691676 opStr (NS n _) = opStr n
16701677 opStr (UN n) = T.unpack n
16711678
1672− slist' _ _ e
1679+ slist' :: Maybe Int -> Int -> [(Name, Bool)] -> PTerm -> Maybe [Doc OutputAnnotation]
1680+ slist' (Just d) _ _ _ | d <= 0 = Nothing
1681+ slist' d _ _ e
16731682 | containsHole e = Nothing
1674− slist' p bnd (PApp _ (PRef _ nil) _)
1683+ slist' d p bnd (PApp _ (PRef _ nil) _)
16751684 | not (ppopt_impl ppo) && nsroot nil == sUN "Nil" = Just []
1676− slist' p bnd (PRef _ nil)
1685+ slist' d p bnd (PRef _ nil)
16771686 | not (ppopt_impl ppo) && nsroot nil == sUN "Nil" = Just []
1678− slist' p bnd (PApp _ (PRef _ cons) args)
1687+ slist' d p bnd (PApp _ (PRef _ cons) args)
16791688 | nsroot cons == sUN "::",
16801689 (PExp {getTm=tl}):(PExp {getTm=hd}):imps <- reverse args,
16811690 all isImp imps,
1682− Just tl' <- slist' p bnd tl
1683− = Just (hd:tl')
1691+ Just tl' <- slist' (decD d) p bnd tl
1692+ = Just (prettySe d startPrec bnd hd : tl')
16841693 where
16851694 isImp (PImp {}) = True
16861695 isImp _ = False
1687− slist' _ _ tm = Nothing
1688−
1689− slist p bnd e | Just es <- slist' p bnd e = Just $
1690− case es of [] -> annotate (AnnData "" "") $ text "[]"
1691− [x] -> enclose left right . group $
1692− prettySe p bnd x
1693− xs -> (enclose left right .
1694− align . group . vsep .
1695− punctuate comma .
1696− map (prettySe p bnd)) xs
1696+ slist' _ _ _ tm = Nothing
1697+
1698+ slist d p bnd e | Just es <- slist' d p bnd e = Just $
1699+ case es of
1700+ [] -> annotate (AnnData "" "") $ text "[]"
1701+ [x] -> enclose left right . group $ x
1702+ xs -> enclose left right .
1703+ align . group . vsep .
1704+ punctuate comma $ xs
16971705 where left = (annotate (AnnData "" "") (text "["))
16981706 right = (annotate (AnnData "" "") (text "]"))
16991707 comma = (annotate (AnnData "" "") (text ","))
1700− slist _ _ _ = Nothing
1708+ slist _ _ _ _ = Nothing
17011709
17021710 pairElts :: PTerm -> Maybe [PTerm]
17031711 pairElts (PPair _ _ x y) | Just elts <- pairElts y = Just (x:elts)
@@ -1706,18 +1714,27 @@ pprintPTerm ppo bnd docArgs infixes = prettySe startPrec bnd
17061714
17071715 natns = "Prelude.Nat."
17081716
1709− snat p (PRef _ z)
1717+ snat :: Maybe Int -> Int -> PTerm -> Maybe Integer
1718+ snat (Just x) _ _ | x <= 0 = Nothing
1719+ snat d p (PRef _ z)
17101720 | show z == (natns++"Z") || show z == "Z" = Just 0
1711− snat p (PApp _ s [PExp {getTm=n}])
1721+ snat d p (PApp _ s [PExp {getTm=n}])
17121722 | show s == (natns++"S") || show s == "S",
1713− Just n' <- snat p n
1723+ Just n' <- snat (decD d) p n
17141724 = Just $ 1 + n'
1715− snat _ _ = Nothing
1725+ snat _ _ _ = Nothing
17161726
17171727 bracket outer inner doc
17181728 | outer > inner = lparen <> doc <> rparen
17191729 | otherwise = doc
17201730
1731+ ellipsis = text "..."
1732+
1733+ depth Nothing = id
1734+ depth (Just d) = if d <= 0 then const (ellipsis) else id
1735+
1736+ decD = fmap (\x -> x - 1)
1737+
17211738 kwd = annotate AnnKeyword . text
17221739
17231740 fixities :: M.Map String Fixity
src/Idris/Core/TT.hs+16
@@ -1249,6 +1249,22 @@ unList tm = case unApply tm of
12491249 return $ x:rest
12501250 (f, args) -> Nothing
12511251
1252+-- | Hard-code a heuristic maximum term size, to prevent attempts to
1253+-- serialize or force infinite or just gigantic terms
1254+termSmallerThan :: Int -> Term -> Bool
1255+termSmallerThan x tm | x <= 0 = False
1256+termSmallerThan x (P _ _ ty) = termSmallerThan (x-1) ty
1257+termSmallerThan x (Bind _ _ tm) = termSmallerThan (x-1) tm
1258+termSmallerThan x (App _ f a) = termSmallerThan (x-1) f && termSmallerThan (x-1) a
1259+termSmallerThan x (Proj tm _) = termSmallerThan (x-1) tm
1260+termSmallerThan x (V i) = True
1261+termSmallerThan x (Constant c) = True
1262+termSmallerThan x Erased = True
1263+termSmallerThan x Impossible = True
1264+termSmallerThan x (TType u) = True
1265+termSmallerThan x (UType u) = True
1266+
1267+
12521268-- | Cast a 'TT' term to a 'Raw' value, discarding universe information and
12531269-- the types of named references and replacing all de Bruijn indices
12541270-- with the corresponding name. It is an error if there are free de
src/Idris/IdeMode.hs+3−1
@@ -148,7 +148,9 @@ instance SExpable OutputAnnotation where
148148 BoldText -> "bold"
149149 ItalicText -> "italic"
150150 UnderlineText -> "underline"
151− toSExp (AnnTerm bnd tm) = toSExp [(SymbolAtom "tt-term", StringAtom (encodeTerm bnd tm))]
151+ toSExp (AnnTerm bnd tm)
152+ | termSmallerThan 1000 tm = toSExp [(SymbolAtom "tt-term", StringAtom (encodeTerm bnd tm))]
153+ | otherwise = SexpList []
152154 toSExp (AnnSearchResult ordr) = toSExp [(SymbolAtom "doc-overview",
153155 StringAtom ("Result type is " ++ descr))]
154156 where descr = case ordr of
src/Idris/REPL.hs+21−17
@@ -496,7 +496,7 @@ runIdeModeCommand h id orig fn modes (IdeMode.BrowseNS ns) =
496496runIdeModeCommand h id orig fn modes (IdeMode.TermNormalise bnd tm) =
497497 do ctxt <- getContext
498498 ist <- getIState
499− let tm' = force (normaliseAll ctxt [] tm)
499+ let tm' = normaliseAll ctxt [] tm
500500 ptm = annotate (AnnTerm bnd tm')
501501 (pprintPTerm (ppOptionIst ist)
502502 bnd
@@ -634,6 +634,8 @@ idemodeProcess fn (MakeWith False pos str) = process fn (MakeWith False pos str)
634634idemodeProcess fn (DoProofSearch False r pos str xs) = process fn (DoProofSearch False r pos str xs)
635635idemodeProcess fn (SetConsoleWidth w) = do process fn (SetConsoleWidth w)
636636 iPrintResult ""
637+idemodeProcess fn (SetPrinterDepth d) = do process fn (SetPrinterDepth d)
638+ iPrintResult ""
637639idemodeProcess fn (Apropos pkg a) = do process fn (Apropos pkg a)
638640 iPrintResult ""
639641idemodeProcess fn (WhoCalls n) = process fn (WhoCalls n)
@@ -767,21 +769,23 @@ process fn (ModImport f) = do fmod <- loadModule f
767769 Just pr -> isetPrompt pr
768770 Nothing -> iPrintError $ "Can't find import " ++ f
769771process fn (Eval t)
770− = withErrorReflection $ do logLvl 5 $ show t
771− getIState >>= flip warnDisamb t
772− (tm, ty) <- elabVal recinfo ERHS t
773− ctxt <- getContext
774− let tm' = force (normaliseAll ctxt [] tm)
775− let ty' = force (normaliseAll ctxt [] ty)
776− -- Add value to context, call it "it"
777− updateContext (addCtxtDef (sUN "it") (Function ty' tm'))
778− ist <- getIState
779− logLvl 3 $ "Raw: " ++ show (tm', ty')
780− logLvl 10 $ "Debug: " ++ showEnvDbg [] tm'
781− let tmDoc = pprintDelab ist tm'
782− tyDoc = pprintDelab ist ty'
783− iPrintTermWithType tmDoc tyDoc
784−
772+ = withErrorReflection $
773+ do logLvl 5 $ show t
774+ getIState >>= flip warnDisamb t
775+ (tm, ty) <- elabVal recinfo ERHS t
776+ ctxt <- getContext
777+ let tm' = perhapsForce $ normaliseAll ctxt [] tm
778+ let ty' = perhapsForce $ normaliseAll ctxt [] ty
779+ -- Add value to context, call it "it"
780+ updateContext (addCtxtDef (sUN "it") (Function ty' tm'))
781+ ist <- getIState
782+ logLvl 3 $ "Raw: " ++ show (tm', ty')
783+ logLvl 10 $ "Debug: " ++ showEnvDbg [] tm'
784+ let tmDoc = pprintDelab ist tm'
785+ tyDoc = pprintDelab ist ty'
786+ iPrintTermWithType tmDoc tyDoc
787+ where perhapsForce tm | termSmallerThan 100 tm = force tm
788+ | otherwise = tm
785789
786790process fn (NewDefn decls) = do
787791 logLvl 3 ("Defining names using these decls: " ++ show (showDecls verbosePPOption decls))
@@ -1237,7 +1241,7 @@ process fn ListErrorHandlers =
12371241 [] -> "No registered error handlers"
12381242 handlers -> "Registered error handlers: " ++ (concat . intersperse ", " . map show) handlers
12391243process fn (SetConsoleWidth w) = setWidth w
1240−
1244+process fn (SetPrinterDepth d) = setDepth d
12411245process fn (Apropos pkgs a) =
12421246 do orig <- getIState
12431247 when (not (null pkgs)) $
src/Idris/REPLParser.hs+7−2
@@ -39,7 +39,7 @@ allHelp = [ (map (':' :) names, args, text)
3939 | (names, args, text, _) <- parserCommandsForHelp ++ parserCommands ]
4040
4141parserCommandsForHelp :: CommandTable
42−parserCommandsForHelp =
42+parserCommandsForHelp =
4343 [ exprArgCmd ["t", "type"] Check "Check the type of an expression"
4444 , exprArgCmd ["core"] Core "View the core language representation of a term"
4545 , nameArgCmd ["miss", "missing"] Missing "Show missing clauses"
@@ -82,6 +82,7 @@ parserCommandsForHelp =
8282 , "Turn REPL colours on or off; set a specific colour"
8383 , cmd_colour)
8484 , (["consolewidth"], ConsoleWidthArg, "Set the width of the console", cmd_consolewidth)
85+ , (["printerdepth"], OptionalArg NumberArg, "Set the maximum pretty-printer depth (no arg for infinite)", cmd_printdepth)
8586 , noArgCmd ["q", "quit"] Quit "Exit the Idris system"
8687 , noArgCmd ["w", "warranty"] Warranty "Displays warranty information"
8788 , (["let"], ManyArgs DeclArg
@@ -96,7 +97,7 @@ parserCommandsForHelp =
9697 , cmd_pprint)
9798 ]
9899
99−parserCommands =
100+parserCommands =
100101 [ noArgCmd ["u", "universes"] Universes "Display universe constraints"
101102 , noArgCmd ["errorhandlers"] ListErrorHandlers "List registered error handlers"
102103
@@ -285,6 +286,10 @@ cmd_consolewidth name = do
285286 <|> do n <- fmap (fromInteger . fst) P.natural
286287 return (ColsWide n)
287288
289+cmd_printdepth :: String -> P.IdrisParser (Either String Command)
290+cmd_printdepth _ = do d <- optional (fmap (fromInteger . fst) P.natural)
291+ return (Right $ SetPrinterDepth d)
292+
288293cmd_execute :: String -> P.IdrisParser (Either String Command)
289294cmd_execute name = do
290295 tm <- option maintm (P.fullExpr defaultSyntax)
test/error004/expected+1−1
@@ -3,5 +3,5 @@ When checking argument cons1 to function FunErrTest.cadr:
33 Could not prove that [] has at least two elements.
44FunErrTest.idr:38:10:When checking right hand side of badCadr2:
55When checking argument cons2 to function FunErrTest.cadr:
6− Could not prove that tail [(fromInteger 1)] has at least two
6+ Could not prove that tail [fromInteger 1] has at least two
77 elements.
test/interactive008/expectednew file+204
@@ -0,0 +1,204 @@
1+Idris> Idris> Idris> 1 ::
2+2 :: 3 :: 4 :: 5 :: ... : List Integer
3+Idris> Idris> [1,
4+ 2,
5+ 3,
6+ 4,
7+ 5,
8+ 6,
9+ 7,
10+ 8,
11+ 9,
12+ 10,
13+ 11,
14+ 12,
15+ 13,
16+ 14,
17+ 15,
18+ 16,
19+ 17,
20+ 18,
21+ 19,
22+ 20,
23+ 21,
24+ 22,
25+ 23,
26+ 24,
27+ 25,
28+ 26,
29+ 27,
30+ 28,
31+ 29,
32+ 30,
33+ 31,
34+ 32,
35+ 33,
36+ 34,
37+ 35,
38+ 36,
39+ 37,
40+ 38,
41+ 39,
42+ 40,
43+ 41,
44+ 42,
45+ 43,
46+ 44,
47+ 45,
48+ 46,
49+ 47,
50+ 48,
51+ 49,
52+ 50,
53+ 51,
54+ 52,
55+ 53,
56+ 54,
57+ 55,
58+ 56,
59+ 57,
60+ 58,
61+ 59,
62+ 60,
63+ 61,
64+ 62,
65+ 63,
66+ 64,
67+ 65,
68+ 66,
69+ 67,
70+ 68,
71+ 69,
72+ 70,
73+ 71,
74+ 72,
75+ 73,
76+ 74,
77+ 75,
78+ 76,
79+ 77,
80+ 78,
81+ 79,
82+ 80,
83+ 81,
84+ 82,
85+ 83,
86+ 84,
87+ 85,
88+ 86,
89+ 87,
90+ 88,
91+ 89,
92+ 90,
93+ 91,
94+ 92,
95+ 93,
96+ 94,
97+ 95,
98+ 96,
99+ 97,
100+ 98,
101+ 99,
102+ 100] : List Integer
103+Idris> Idris> ... : ...
104+Idris> Idris> [1,
105+ 2,
106+ 3,
107+ 4,
108+ 5,
109+ 6,
110+ 7,
111+ 8,
112+ 9,
113+ 10,
114+ 11,
115+ 12,
116+ 13,
117+ 14,
118+ 15,
119+ 16,
120+ 17,
121+ 18,
122+ 19,
123+ 20,
124+ 21,
125+ 22,
126+ 23,
127+ 24,
128+ 25,
129+ 26,
130+ 27,
131+ 28,
132+ 29,
133+ 30,
134+ 31,
135+ 32,
136+ 33,
137+ 34,
138+ 35,
139+ 36,
140+ 37,
141+ 38,
142+ 39,
143+ 40,
144+ 41,
145+ 42,
146+ 43,
147+ 44,
148+ 45,
149+ 46,
150+ 47,
151+ 48,
152+ 49,
153+ 50,
154+ 51,
155+ 52,
156+ 53,
157+ 54,
158+ 55,
159+ 56,
160+ 57,
161+ 58,
162+ 59,
163+ 60,
164+ 61,
165+ 62,
166+ 63,
167+ 64,
168+ 65,
169+ 66,
170+ 67,
171+ 68,
172+ 69,
173+ 70,
174+ 71,
175+ 72,
176+ 73,
177+ 74,
178+ 75,
179+ 76,
180+ 77,
181+ 78,
182+ 79,
183+ 80,
184+ 81,
185+ 82,
186+ 83,
187+ 84,
188+ 85,
189+ 86,
190+ 87,
191+ 88,
192+ 89,
193+ 90,
194+ 91,
195+ 92,
196+ 93,
197+ 94,
198+ 95,
199+ 96,
200+ 97,
201+ 98,
202+ 99,
203+ 100] : List Integer
204+Idris> Bye bye
test/interactive008/inputnew file+9
@@ -0,0 +1,9 @@
1+:consolewidth 50
2+:printerdepth 5
3+the (List Integer) [1..20]
4+:printerdepth 1000
5+the (List Integer) [1..100]
6+:printerdepth 0
7+the (List Integer) [1..100]
8+:printerdepth
9+the (List Integer) [1..100]
test/interactive008/runnew file+2
@@ -0,0 +1,2 @@
1+#!/usr/bin/env bash
2+idris --nobanner --nocolor < input