git.iko.soy/Idris-dev
on master help sign in
Merge pull request #2345 from david-christiansen/issue/2333
763af04David Christiansen
CHANGELOG+4
compare with master
unifiedsplit
@@ -5,6 +5,10 @@ New in 0.9.19:
5* The Show class has been moved into Prelude.Show and augmented with the method
5* The Show class has been moved into Prelude.Show and augmented with the method
6 showPrec, which allows correct parenthesization of showed terms. This comes
6 showPrec, which allows correct parenthesization of showed terms. This comes
7 with the type Prec of precedences and a few helper functions.
7 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.
8* Compiler output shows applications of >>= in do-notation
12* Compiler output shows applications of >>= in do-notation
9* fromInteger i where i is an integer constant is now shown just as i in
13* fromInteger i where i is an integer constant is now shown just as i in
10 compiler output
14 compiler output
docs/reference/repl.rst+2
@@ -136,6 +136,8 @@ The current set of supported commands are:
136+----------------+------------------------------+----------------------------------------------------------------------------------------------------------+
136+----------------+------------------------------+----------------------------------------------------------------------------------------------------------+
137|:consolewidth | auto|infinite|<number> | Set the width of the console |
137|:consolewidth | auto|infinite|<number> | Set the width of the console |
138+----------------+------------------------------+----------------------------------------------------------------------------------------------------------+
138+----------------+------------------------------+----------------------------------------------------------------------------------------------------------+
139+|:printerdepth | <number-or-blank> | Set the maximum pretty-printing depth, or infinite if nothing specified |
140++----------------+------------------------------+----------------------------------------------------------------------------------------------------------+
139|:q :quit | | Exit the Idris system |
141|:q :quit | | Exit the Idris system |
140+----------------+------------------------------+----------------------------------------------------------------------------------------------------------+
142+----------------+------------------------------+----------------------------------------------------------------------------------------------------------+
141|:w :warranty | | Displays warranty information |
143|:w :warranty | | Displays warranty information |
idris.cabal+3
@@ -526,6 +526,9 @@ Extra-source-files:
526 test/interactive007/run
526 test/interactive007/run
527 test/interactive007/input
527 test/interactive007/input
528 test/interactive007/expected
528 test/interactive007/expected
529+ test/interactive008/run
530+ test/interactive008/input
531+ test/interactive008/expected
529
532
530 test/io001/run
533 test/io001/run
531 test/io001/*.idr
534 test/io001/*.idr
src/Idris/AbsSyntax.hs+5
@@ -637,9 +637,14 @@ setWidth :: ConsoleWidth -> Idris ()
637setWidth w = do ist <- getIState
637setWidth w = do ist <- getIState
638 put ist { idris_consolewidth = w }
638 put ist { idris_consolewidth = w }
639
639
640+setDepth :: Maybe Int -> Idris ()
641+setDepth d = do ist <- getIState
642+ put ist { idris_options = (idris_options ist) { opt_printdepth = d } }
643+
640typeDescription :: String
644typeDescription :: String
641typeDescription = "The type of types"
645typeDescription = "The type of types"
642
646
647+
643type1Doc :: Doc OutputAnnotation
648type1Doc :: Doc OutputAnnotation
644type1Doc = (annotate (AnnType "Type" "The type of types, one level up") $ text "Type 1")
649type1Doc = (annotate (AnnType "Type" "The type of types, one level up") $ text "Type 1")
645
650
src/Idris/AbsSyntaxTree.hs+158−141
@@ -88,7 +88,8 @@ data IOption = IOption { opt_logLevel :: Int,
88 opt_origerr :: Bool,
88 opt_origerr :: Bool,
89 opt_autoSolve :: Bool, -- ^ automatically apply "solve" tactic in prover
89 opt_autoSolve :: Bool, -- ^ automatically apply "solve" tactic in prover
90 opt_autoImport :: [FilePath], -- ^ e.g. Builtins+Prelude
90 opt_autoImport :: [FilePath], -- ^ e.g. Builtins+Prelude
91− opt_optimise :: [Optimisation]
91+ opt_optimise :: [Optimisation],
92+ opt_printdepth :: Maybe Int
92 }
93 }
93 deriving (Show, Eq)
94 deriving (Show, Eq)
94
95
@@ -113,10 +114,12 @@ defaultOpts = IOption { opt_logLevel = 0
113 , opt_autoSolve = True
114 , opt_autoSolve = True
114 , opt_autoImport = []
115 , opt_autoImport = []
115 , opt_optimise = defaultOptimise
116 , opt_optimise = defaultOptimise
117+ , opt_printdepth = Just 5000
116 }
118 }
117
119
118data PPOption = PPOption {
120data PPOption = PPOption {
119 ppopt_impl :: Bool -- ^^ whether to show implicits
121 ppopt_impl :: Bool -- ^^ whether to show implicits
122+ , ppopt_depth :: Maybe Int
120} deriving (Show)
123} deriving (Show)
121
124
122data Optimisation = PETransform -- partial eval and associated transforms
125data Optimisation = PETransform -- partial eval and associated transforms
@@ -126,16 +129,17 @@ defaultOptimise = [PETransform]
126
129
127-- | Pretty printing options with default verbosity.
130-- | Pretty printing options with default verbosity.
128defaultPPOption :: PPOption
131defaultPPOption :: PPOption
129−defaultPPOption = PPOption { ppopt_impl = False }
132+defaultPPOption = PPOption { ppopt_impl = False , ppopt_depth = Just 200 }
130
133
131-- | Pretty printing options with the most verbosity.
134-- | Pretty printing options with the most verbosity.
132verbosePPOption :: PPOption
135verbosePPOption :: PPOption
133−verbosePPOption = PPOption { ppopt_impl = True }
136+verbosePPOption = PPOption { ppopt_impl = True, ppopt_depth = Just 200 }
134
137
135-- | Get pretty printing options from the big options record.
138-- | Get pretty printing options from the big options record.
136ppOption :: IOption -> PPOption
139ppOption :: IOption -> PPOption
137ppOption opt = PPOption {
140ppOption opt = PPOption {
138− ppopt_impl = opt_showimp opt
141+ ppopt_impl = opt_showimp opt,
142+ ppopt_depth = opt_printdepth opt
139}
143}
140
144
141-- | Get pretty printing options from an idris state record.
145-- | Get pretty printing options from an idris state record.
@@ -406,6 +410,7 @@ data Command = Quit
406 | ColourOff
410 | ColourOff
407 | ListErrorHandlers
411 | ListErrorHandlers
408 | SetConsoleWidth ConsoleWidth
412 | SetConsoleWidth ConsoleWidth
413+ | SetPrinterDepth (Maybe Int)
409 | Apropos [String] String
414 | Apropos [String] String
410 | WhoCalls Name
415 | WhoCalls Name
411 | CallsWho Name
416 | CallsWho Name
@@ -1441,96 +1446,97 @@ pprintPTerm :: PPOption -- ^^ pretty printing options
1441 -> [FixDecl] -- ^^ Fixity declarations
1446 -> [FixDecl] -- ^^ Fixity declarations
1442 -> PTerm -- ^^ the term to pretty-print
1447 -> PTerm -- ^^ the term to pretty-print
1443 -> Doc OutputAnnotation
1448 -> Doc OutputAnnotation
1444−pprintPTerm ppo bnd docArgs infixes = prettySe startPrec bnd
1449+pprintPTerm ppo bnd docArgs infixes = prettySe (ppopt_depth ppo) startPrec bnd
1445 where
1450 where
1446 startPrec = 0
1451 startPrec = 0
1447 funcAppPrec = 10
1452 funcAppPrec = 10
1448
1453
1449− prettySe :: Int -> [(Name, Bool)] -> PTerm -> Doc OutputAnnotation
1454+ prettySe :: Maybe Int -> Int -> [(Name, Bool)] -> PTerm -> Doc OutputAnnotation
1450− prettySe p bnd (PQuote r) =
1455+ prettySe d p bnd (PQuote r) =
1451 text "![" <> pretty r <> text "]"
1456 text "![" <> pretty r <> text "]"
1452− prettySe p bnd (PPatvar fc n) = pretty n
1457+ prettySe d p bnd (PPatvar fc n) = pretty n
1453− prettySe p bnd e
1458+ prettySe d p bnd e
1454− | Just str <- slist p bnd e = str
1459+ | Just str <- slist d p bnd e = depth d $ str
1455− | Just n <- snat p e = annotate (AnnData "Nat" "") (text (show n))
1460+ | Just n <- snat d p e = depth d $ annotate (AnnData "Nat" "") (text (show n))
1456− prettySe p bnd (PRef fc n) = prettyName True (ppopt_impl ppo) bnd n
1461+ prettySe d p bnd (PRef fc n) = prettyName True (ppopt_impl ppo) bnd n
1457− prettySe p bnd (PLam fc n nfc ty sc) =
1462+ prettySe d p bnd (PLam fc n nfc ty sc) =
1458− bracket p startPrec . group . align . hang 2 $
1463+ depth d . bracket p startPrec . group . align . hang 2 $
1459 text "\\" <> prettyBindingOf n False <+> text "=>" <$>
1464 text "\\" <> prettyBindingOf n False <+> text "=>" <$>
1460− prettySe startPrec ((n, False):bnd) sc
1465+ prettySe (decD d) startPrec ((n, False):bnd) sc
1461− prettySe p bnd (PLet fc n nfc ty v sc) =
1466+ prettySe d p bnd (PLet fc n nfc ty v sc) =
1462− bracket p startPrec . group . align $
1467+ depth d . bracket p startPrec . group . align $
1463− kwd "let" <+> (group . align . hang 2 $ prettyBindingOf n False <+> text "=" <$> prettySe startPrec bnd v) </>
1468+ kwd "let" <+> (group . align . hang 2 $ prettyBindingOf n False <+> text "=" <$> prettySe (decD d) startPrec bnd v) </>
1464− kwd "in" <+> (group . align . hang 2 $ prettySe startPrec ((n, False):bnd) sc)
1469+ kwd "in" <+> (group . align . hang 2 $ prettySe (decD d) startPrec ((n, False):bnd) sc)
1465− prettySe p bnd (PPi (Exp l s _) n _ ty sc)
1470+ prettySe d p bnd (PPi (Exp l s _) n _ ty sc)
1466 | n `elem` allNamesIn sc || ppopt_impl ppo || n `elem` docArgs =
1471 | n `elem` allNamesIn sc || ppopt_impl ppo || n `elem` docArgs =
1467− bracket p startPrec . group $
1472+ depth d . bracket p startPrec . group $
1468− enclose lparen rparen (group . align $ prettyBindingOf n False <+> colon <+> prettySe startPrec bnd ty) <+>
1473+ enclose lparen rparen (group . align $ prettyBindingOf n False <+> colon <+> prettySe (decD d) startPrec bnd ty) <+>
1469− st <> text "->" <$> prettySe startPrec ((n, False):bnd) sc
1474+ st <> text "->" <$> prettySe (decD d) startPrec ((n, False):bnd) sc
1470 | otherwise =
1475 | otherwise =
1471− bracket p startPrec . group $
1476+ depth d . bracket p startPrec . group $
1472− group (prettySe (startPrec + 1) bnd ty <+> st) <> text "->" <$> group (prettySe startPrec ((n, False):bnd) sc)
1477+ group (prettySe (decD d) (startPrec + 1) bnd ty <+> st) <> text "->" <$>
1478+ group (prettySe (decD d) startPrec ((n, False):bnd) sc)
1473 where
1479 where
1474 st =
1480 st =
1475 case s of
1481 case s of
1476 Static -> text "[static]" <> space
1482 Static -> text "[static]" <> space
1477 _ -> empty
1483 _ -> 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)
1479 | ppopt_impl ppo =
1485 | ppopt_impl ppo =
1480− bracket p startPrec $
1486+ depth d . bracket p startPrec $
1481− lbrace <> prettyBindingOf n True <+> colon <+> prettySe startPrec bnd ty <> rbrace <+>
1487+ lbrace <> prettyBindingOf n True <+> colon <+> prettySe (decD d) startPrec bnd ty <> rbrace <+>
1482− st <> text "->" </> prettySe startPrec ((n, True):bnd) sc
1488+ st <> text "->" </> prettySe (decD d) startPrec ((n, True):bnd) sc
1483− | otherwise = prettySe startPrec ((n, True):bnd) sc
1489+ | otherwise = depth d $ prettySe (decD d) startPrec ((n, True):bnd) sc
1484 where
1490 where
1485 st =
1491 st =
1486 case s of
1492 case s of
1487 Static -> text "[static]" <> space
1493 Static -> text "[static]" <> space
1488 _ -> empty
1494 _ -> empty
1489− prettySe p bnd (PPi (Constraint _ _) n _ ty sc) =
1495+ prettySe d p bnd (PPi (Constraint _ _) n _ ty sc) =
1490− bracket p startPrec $
1496+ depth d . bracket p startPrec $
1491− prettySe (startPrec + 1) bnd ty <+> text "=>" </> prettySe startPrec ((n, True):bnd) sc
1497+ prettySe (decD d) (startPrec + 1) bnd ty <+> text "=>" </> prettySe (decD d) startPrec ((n, True):bnd) sc
1492− prettySe p bnd (PPi (TacImp _ _ (PTactics [ProofSearch _ _ _ _ _])) n _ ty sc) =
1498+ prettySe d p bnd (PPi (TacImp _ _ (PTactics [ProofSearch _ _ _ _ _])) n _ ty sc) =
1493− lbrace <> kwd "auto" <+> pretty n <+> colon <+> prettySe startPrec bnd ty <>
1499+ lbrace <> kwd "auto" <+> pretty n <+> colon <+> prettySe (decD d) startPrec bnd ty <>
1494− rbrace <+> text "->" </> prettySe startPrec ((n, True):bnd) sc
1500+ rbrace <+> text "->" </> prettySe (decD d) startPrec ((n, True):bnd) sc
1495− prettySe p bnd (PPi (TacImp _ _ s) n _ ty sc) =
1501+ prettySe d p bnd (PPi (TacImp _ _ s) n _ ty sc) =
1496− bracket p startPrec $
1502+ depth d . bracket p startPrec $
1497− lbrace <> kwd "default" <+> prettySe (funcAppPrec + 1) bnd s <+> pretty n <+> colon <+> prettySe startPrec bnd ty <>
1503+ lbrace <> kwd "default" <+> prettySe (decD d) (funcAppPrec + 1) bnd s <+> pretty n <+> colon <+> prettySe (decD d) startPrec bnd ty <>
1498− rbrace <+> text "->" </> prettySe startPrec ((n, True):bnd) sc
1504+ rbrace <+> text "->" </> prettySe (decD d) startPrec ((n, True):bnd) sc
1499 -- This case preserves the behavior of the former constructor PEq.
1505 -- This case preserves the behavior of the former constructor PEq.
1500 -- It should be removed if feasible when the pretty-printing of infix
1506 -- It should be removed if feasible when the pretty-printing of infix
1501 -- operators in general is improved.
1507 -- 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])
1503 | n == eqTy, ppopt_impl ppo =
1509 | n == eqTy, ppopt_impl ppo =
1504− bracket p eqPrec $
1510+ depth d . bracket p eqPrec $
1505 enclose lparen rparen eq <+>
1511 enclose lparen rparen eq <+>
1506− align (group (vsep (map (prettyArgS bnd)
1512+ align (group (vsep (map (prettyArgS (decD d) bnd)
1507 [lt, rt, l, r])))
1513 [lt, rt, l, r])))
1508 | n == eqTy =
1514 | n == eqTy =
1509− bracket p eqPrec . align . group $
1515+ depth d . bracket p eqPrec . align . group $
1510 prettyTerm (getTm l) <+> eq <$> group (prettyTerm (getTm r))
1516 prettyTerm (getTm l) <+> eq <$> group (prettyTerm (getTm r))
1511 where eq = annName eqTy (text "=")
1517 where eq = annName eqTy (text "=")
1512 eqPrec = startPrec
1518 eqPrec = startPrec
1513− prettyTerm = prettySe (eqPrec + 1) bnd
1519+ prettyTerm = prettySe (decD d) (eqPrec + 1) bnd
1514− prettySe p bnd (PApp _ (PRef _ f) args) -- normal names, no explicit args
1520+ prettySe d p bnd (PApp _ (PRef _ f) args) -- normal names, no explicit args
1515 | UN nm <- basename f
1521 | UN nm <- basename f
1516 , not (ppopt_impl ppo) && null (getShowArgs args) =
1522 , not (ppopt_impl ppo) && null (getShowArgs args) =
1517 prettyName True (ppopt_impl ppo) bnd f
1523 prettyName True (ppopt_impl ppo) bnd f
1518− prettySe p bnd (PAppBind _ (PRef _ f) [])
1524+ prettySe d p bnd (PAppBind _ (PRef _ f) [])
1519 | not (ppopt_impl ppo) = text "!" <> prettyName True (ppopt_impl ppo) bnd f
1525 | 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
1521 | UN nm <- basename op
1527 | UN nm <- basename op
1522 , not (tnull nm) &&
1528 , not (tnull nm) &&
1523 (not (ppopt_impl ppo)) && (not $ isAlpha (thead nm)) =
1529 (not (ppopt_impl ppo)) && (not $ isAlpha (thead nm)) =
1524 case getShowArgs args of
1530 case getShowArgs args of
1525 [] -> opName True
1531 [] -> 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)))
1527 [l,r] -> let precedence = maybe (startPrec - 1) prec f
1533 [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)
1529 (l@(PExp _ _ _ _) : r@(PExp _ _ _ _) : rest) ->
1535 (l@(PExp _ _ _ _) : r@(PExp _ _ _ _) : rest) ->
1530− bracket p funcAppPrec $
1536+ depth d . bracket p funcAppPrec $
1531 enclose lparen rparen (inFix (getTm l) (getTm r)) <+>
1537 enclose lparen rparen (inFix (getTm l) (getTm r)) <+>
1532− align (group (vsep (map (prettyArgS bnd) rest)))
1538+ align (group (vsep (map (prettyArgS d bnd) rest)))
1533− as -> opName True <+> align (vsep (map (prettyArgS bnd) as))
1539+ as -> opName True <+> align (vsep (map (prettyArgS d bnd) as))
1534 where opName isPrefix = prettyName isPrefix (ppopt_impl ppo) bnd op
1540 where opName isPrefix = prettyName isPrefix (ppopt_impl ppo) bnd op
1535 f = getFixity (opStr op)
1541 f = getFixity (opStr op)
1536 left = case f of
1542 left = case f of
@@ -1542,26 +1548,26 @@ pprintPTerm ppo bnd docArgs infixes = prettySe startPrec bnd
1542 Just (Infixr p') -> p'
1548 Just (Infixr p') -> p'
1543 Just f' -> prec f' + 1
1549 Just f' -> prec f' + 1
1544 inFix l r = align . group $
1550 inFix l r = align . group $
1545− (prettySe left bnd l <+> opName False) <$>
1551+ (prettySe (decD d) left bnd l <+> opName False) <$>
1546− group (prettySe right bnd r)
1552+ group (prettySe (decD d) right bnd r)
1547− prettySe p bnd (PApp _ hd@(PRef fc f) [tm]) -- symbols, like 'foo
1553+ prettySe d p bnd (PApp _ hd@(PRef fc f) [tm]) -- symbols, like 'foo
1548 | PConstant NoFC (Idris.Core.TT.Str str) <- getTm tm,
1554 | PConstant NoFC (Idris.Core.TT.Str str) <- getTm tm,
1549 f == sUN "Symbol_" = annotate (AnnType ("'" ++ str) ("The symbol " ++ str)) $
1555 f == sUN "Symbol_" = annotate (AnnType ("'" ++ str) ("The symbol " ++ str)) $
1550− char '\'' <> prettySe startPrec bnd (PRef fc (sUN str))
1556+ char '\'' <> prettySe (decD d) startPrec bnd (PRef fc (sUN str))
1551− prettySe p bnd (PApp _ f as) = -- Normal prefix applications
1557+ prettySe d p bnd (PApp _ f as) = -- Normal prefix applications
1552 let args = getShowArgs as
1558 let args = getShowArgs as
1553− fp = prettySe (startPrec + 1) bnd f
1559+ fp = prettySe (decD d) (startPrec + 1) bnd f
1554 shownArgs = if ppopt_impl ppo then as else args
1560 shownArgs = if ppopt_impl ppo then as else args
1555 in
1561 in
1556− bracket p funcAppPrec . group $
1562+ depth d . bracket p funcAppPrec . group $
1557 if null shownArgs
1563 if null shownArgs
1558 then fp
1564 then fp
1559− else fp <+> align (vsep (map (prettyArgS bnd) shownArgs))
1565+ else fp <+> align (vsep (map (prettyArgS d bnd) shownArgs))
1560− prettySe p bnd (PCase _ scr cases) =
1566+ prettySe d p bnd (PCase _ scr cases) =
1561− align $ kwd "case" <+> prettySe startPrec bnd scr <+> kwd "of" <$>
1567+ align $ kwd "case" <+> prettySe (decD d) startPrec bnd scr <+> kwd "of" <$>
1562− indent 2 (vsep (map ppcase cases))
1568+ depth d (indent 2 (vsep (map ppcase cases)))
1563 where
1569 where
1564− ppcase (l, r) = let prettyCase = prettySe startPrec
1570+ ppcase (l, r) = let prettyCase = prettySe (decD d) startPrec
1565 ([(n, False) | n <- vars l] ++ bnd)
1571 ([(n, False) | n <- vars l] ++ bnd)
1566 in nest nestingSize $
1572 in nest nestingSize $
1567 prettyCase l <+> text "=>" <+> prettyCase r
1573 prettyCase l <+> text "=>" <+> prettyCase r
@@ -1579,67 +1585,68 @@ pprintPTerm ppo bnd docArgs infixes = prettySe startPrec bnd
1579 noNS (NS _ _) = False
1585 noNS (NS _ _) = False
1580 noNS _ = True
1586 noNS _ = True
1581
1587
1582− prettySe p bnd (PIfThenElse _ c t f) =
1588+ prettySe d p bnd (PIfThenElse _ c t f) =
1583− bracket p funcAppPrec . group . align . hang 2 . vsep $
1589+ depth d . bracket p funcAppPrec . group . align . hang 2 . vsep $
1584− [ kwd "if" <+> prettySe startPrec bnd c
1590+ [ kwd "if" <+> prettySe (decD d) startPrec bnd c
1585− , kwd "then" <+> prettySe startPrec bnd t
1591+ , kwd "then" <+> prettySe (decD d) startPrec bnd t
1586− , kwd "else" <+> prettySe startPrec bnd f
1592+ , kwd "else" <+> prettySe (decD d) startPrec bnd f
1587 ]
1593 ]
1588− prettySe p bnd (PHidden tm) = text "." <> prettySe funcAppPrec bnd tm
1594+ prettySe d p bnd (PHidden tm) = text "." <> prettySe (decD d) funcAppPrec bnd tm
1589− prettySe p bnd (PResolveTC _) = kwd "%instance"
1595+ prettySe d p bnd (PResolveTC _) = kwd "%instance"
1590− prettySe p bnd (PTrue _ IsType) = annName unitTy $ text "()"
1596+ prettySe d p bnd (PTrue _ IsType) = annName unitTy $ text "()"
1591− prettySe p bnd (PTrue _ IsTerm) = annName unitCon $ text "()"
1597+ prettySe d p bnd (PTrue _ IsTerm) = annName unitCon $ text "()"
1592− prettySe p bnd (PTrue _ TypeOrTerm) = text "()"
1598+ prettySe d p bnd (PTrue _ TypeOrTerm) = text "()"
1593− prettySe p bnd (PRewrite _ l r _) =
1599+ prettySe d p bnd (PRewrite _ l r _) =
1594− bracket p startPrec $
1600+ depth d . bracket p startPrec $
1595− text "rewrite" <+> prettySe (startPrec + 1) bnd l <+> text "in" <+> prettySe startPrec bnd r
1601+ text "rewrite" <+> prettySe (decD d) (startPrec + 1) bnd l <+> text "in" <+> prettySe (decD d) startPrec bnd r
1596− prettySe p bnd (PTyped l r) =
1602+ prettySe d p bnd (PTyped l r) =
1597− lparen <> prettySe startPrec bnd l <+> colon <+> prettySe startPrec bnd r <> rparen
1603+ lparen <> prettySe (decD d) startPrec bnd l <+> colon <+> prettySe (decD d) startPrec bnd r <> rparen
1598− prettySe p bnd pair@(PPair _ pun _ _) -- flatten tuples to the right, like parser
1604+ prettySe d p bnd pair@(PPair _ pun _ _) -- flatten tuples to the right, like parser
1599− | Just elts <- pairElts pair = enclose (ann lparen) (ann rparen) .
1605+ | Just elts <- pairElts pair = depth d . enclose (ann lparen) (ann rparen) .
1600 align . group . vsep . punctuate (ann comma) $
1606 align . group . vsep . punctuate (ann comma) $
1601− map (prettySe startPrec bnd) elts
1607+ map (prettySe (decD d) startPrec bnd) elts
1602 where ann = case pun of
1608 where ann = case pun of
1603 TypeOrTerm -> id
1609 TypeOrTerm -> id
1604 IsType -> annName pairTy
1610 IsType -> annName pairTy
1605 IsTerm -> annName pairCon
1611 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 $
1607 annotated lparen <>
1614 annotated lparen <>
1608 left <+>
1615 left <+>
1609 annotated (text "**") <+>
1616 annotated (text "**") <+>
1610− prettySe startPrec (addBinding bnd) r <>
1617+ prettySe (decD d) startPrec (addBinding bnd) r <>
1611 annotated rparen
1618 annotated rparen
1612 where annotated = case pun of
1619 where annotated = case pun of
1613 IsType -> annName sigmaTy
1620 IsType -> annName sigmaTy
1614 IsTerm -> annName sigmaCon
1621 IsTerm -> annName sigmaCon
1615 TypeOrTerm -> id
1622 TypeOrTerm -> id
1616 (left, addBinding) = case (l, pun) of
1623 (left, addBinding) = case (l, pun) of
1617− (PRef _ n, IsType) -> (bindingOf n False <+> text ":" <+> prettySe startPrec bnd t, ((n, False) :))
1624+ (PRef _ n, IsType) -> (bindingOf n False <+> text ":" <+> prettySe (decD d) startPrec bnd t, ((n, False) :))
1618− _ -> (prettySe startPrec bnd l, id )
1625+ _ -> (prettySe (decD d) startPrec bnd l, id )
1619− prettySe p bnd (PAlternative a as) =
1626+ prettySe d p bnd (PAlternative a as) =
1620 lparen <> text "|" <> prettyAs <> text "|" <> rparen
1627 lparen <> text "|" <> prettyAs <> text "|" <> rparen
1621 where
1628 where
1622 prettyAs =
1629 prettyAs =
1623− foldr (\l -> \r -> l <+> text "," <+> r) empty $ map (prettySe startPrec bnd) as
1630+ foldr (\l -> \r -> l <+> text "," <+> r) empty $ map (depth d . prettySe (decD d) startPrec bnd) as
1624− prettySe p bnd (PType _) = annotate (AnnType "Type" "The type of types") $ text "Type"
1631+ prettySe d 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)
1632+ prettySe d 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))
1633+ prettySe d p bnd (PConstant _ c) = annotate (AnnConst c) (text (show c))
1627 -- XXX: add pretty for tactics
1634 -- XXX: add pretty for tactics
1628− prettySe p bnd (PProof ts) =
1635+ prettySe d p bnd (PProof ts) =
1629− kwd "proof" <+> lbrace <> text "..." <> rbrace
1636+ kwd "proof" <+> lbrace <> ellipsis <> rbrace
1630− prettySe p bnd (PTactics ts) =
1637+ prettySe d p bnd (PTactics ts) =
1631− kwd "tactics" <+> lbrace <> text "..." <> rbrace
1638+ kwd "tactics" <+> lbrace <> ellipsis <> rbrace
1632− prettySe p bnd (PMetavar _ n) = annotate (AnnName n (Just MetavarOutput) Nothing Nothing) $ text "?" <> pretty n
1639+ prettySe d p bnd (PMetavar _ n) = annotate (AnnName n (Just MetavarOutput) Nothing Nothing) $ text "?" <> pretty n
1633− prettySe p bnd (PReturn f) = kwd "return"
1640+ prettySe d p bnd (PReturn f) = kwd "return"
1634− prettySe p bnd PImpossible = kwd "impossible"
1641+ prettySe d p bnd PImpossible = kwd "impossible"
1635− prettySe p bnd Placeholder = text "_"
1642+ prettySe d p bnd Placeholder = text "_"
1636− prettySe p bnd (PDoBlock dos) =
1643+ prettySe d p bnd (PDoBlock dos) =
1637 bracket p startPrec $
1644 bracket p startPrec $
1638 kwd "do" <+> align (vsep (map (group . align . hang 2) (ppdo bnd dos)))
1645 kwd "do" <+> align (vsep (map (group . align . hang 2) (ppdo bnd dos)))
1639− where ppdo bnd (DoExp _ tm:dos) = prettySe startPrec bnd tm : ppdo bnd dos
1646+ where ppdo bnd (DoExp _ tm:dos) = prettySe (decD d) startPrec bnd tm : ppdo bnd dos
1640 ppdo bnd (DoBind _ bn _ tm : dos) =
1647 ppdo bnd (DoBind _ bn _ tm : dos) =
1641 (prettyBindingOf bn False <+> text "<-" <+>
1648 (prettyBindingOf bn False <+> text "<-" <+>
1642− group (align (hang 2 (prettySe startPrec bnd tm)))) :
1649+ group (align (hang 2 (prettySe (decD d) startPrec bnd tm)))) :
1643 ppdo ((bn, False):bnd) dos
1650 ppdo ((bn, False):bnd) dos
1644 ppdo bnd (DoBindP _ _ _ _ : dos) = -- ok because never made by delab
1651 ppdo bnd (DoBindP _ _ _ _ : dos) = -- ok because never made by delab
1645 text "no pretty printer for pattern-matching do binding" :
1652 text "no pretty printer for pattern-matching do binding" :
@@ -1647,23 +1654,23 @@ pprintPTerm ppo bnd docArgs infixes = prettySe startPrec bnd
1647 ppdo bnd (DoLet _ ln _ ty v : dos) =
1654 ppdo bnd (DoLet _ ln _ ty v : dos) =
1648 (kwd "let" <+> prettyBindingOf ln False <+>
1655 (kwd "let" <+> prettyBindingOf ln False <+>
1649 (if ty /= Placeholder
1656 (if ty /= Placeholder
1650− then colon <+> prettySe startPrec bnd ty <+> text "="
1657+ then colon <+> prettySe (decD d) startPrec bnd ty <+> text "="
1651 else text "=") <+>
1658 else text "=") <+>
1652− group (align (hang 2 (prettySe startPrec bnd v)))) :
1659+ group (align (hang 2 (prettySe (decD d) startPrec bnd v)))) :
1653 ppdo ((ln, False):bnd) dos
1660 ppdo ((ln, False):bnd) dos
1654 ppdo bnd (DoLetP _ _ _ : dos) = -- ok because never made by delab
1661 ppdo bnd (DoLetP _ _ _ : dos) = -- ok because never made by delab
1655 text "no pretty printer for pattern-matching do binding" :
1662 text "no pretty printer for pattern-matching do binding" :
1656 ppdo bnd dos
1663 ppdo bnd dos
1657 ppdo _ [] = []
1664 ppdo _ [] = []
1658− prettySe p bnd (PCoerced t) = prettySe p bnd t
1665+ prettySe d p bnd (PCoerced t) = prettySe d p bnd t
1659− prettySe p bnd (PElabError s) = pretty s
1666+ prettySe d p bnd (PElabError s) = pretty s
1660 -- Quasiquote pprinting ignores bound vars
1667 -- Quasiquote pprinting ignores bound vars
1661− prettySe p bnd (PQuasiquote t Nothing) = text "`(" <> prettySe p [] t <> text ")"
1668+ prettySe d p bnd (PQuasiquote t Nothing) = text "`(" <> prettySe (decD d) p [] t <> text ")"
1662− prettySe p bnd (PQuasiquote t (Just g)) = text "`(" <> prettySe p [] t <+> colon <+> prettySe p [] g <> text ")"
1669+ prettySe d p bnd (PQuasiquote t (Just g)) = text "`(" <> prettySe (decD d) p [] t <+> colon <+> prettySe (decD d) p [] g <> text ")"
1663− prettySe p bnd (PUnquote t) = text "~" <> prettySe p bnd t
1670+ prettySe d p bnd (PUnquote t) = text "~" <> prettySe (decD d) p bnd t
1664− prettySe p bnd (PQuoteName n) = text "`{" <> prettyName True (ppopt_impl ppo) bnd n <> text "}"
1671+ prettySe d p bnd (PQuoteName n) = text "`{" <> prettyName True (ppopt_impl ppo) bnd n <> text "}"
1665
1672
1666− prettySe p bnd _ = text "missing pretty-printer for term"
1673+ prettySe d p bnd _ = text "missing pretty-printer for term"
1667
1674
1668 prettyBindingOf :: Name -> Bool -> Doc OutputAnnotation
1675 prettyBindingOf :: Name -> Bool -> Doc OutputAnnotation
1669 prettyBindingOf n imp = annotate (AnnBoundName n imp) (text (display n))
1676 prettyBindingOf n imp = annotate (AnnBoundName n imp) (text (display n))
@@ -1673,15 +1680,15 @@ pprintPTerm ppo bnd docArgs infixes = prettySe startPrec bnd
1673 display (NS n ns) = (concat . intersperse "." . map T.unpack . reverse) ns ++ "." ++ display n
1680 display (NS n ns) = (concat . intersperse "." . map T.unpack . reverse) ns ++ "." ++ display n
1674 display n = show n
1681 display n = show n
1675
1682
1676− prettyArgS bnd (PImp _ _ _ n tm) = prettyArgSi bnd (n, tm)
1683+ prettyArgS d bnd (PImp _ _ _ n tm) = prettyArgSi d bnd (n, tm)
1677− prettyArgS bnd (PExp _ _ _ tm) = prettyArgSe bnd tm
1684+ prettyArgS d bnd (PExp _ _ _ tm) = prettyArgSe d bnd tm
1678− prettyArgS bnd (PConstraint _ _ _ tm) = prettyArgSc bnd tm
1685+ prettyArgS d bnd (PConstraint _ _ _ tm) = prettyArgSc d bnd tm
1679− prettyArgS bnd (PTacImplicit _ _ n _ tm) = prettyArgSti bnd (n, tm)
1686+ prettyArgS d bnd (PTacImplicit _ _ n _ tm) = prettyArgSti d bnd (n, tm)
1680
1687
1681− prettyArgSe bnd arg = prettySe (funcAppPrec + 1) bnd arg
1688+ prettyArgSe d bnd arg = prettySe d (funcAppPrec + 1) bnd arg
1682− prettyArgSi bnd (n, val) = lbrace <> pretty n <+> text "=" <+> prettySe startPrec bnd val <> rbrace
1689+ prettyArgSi d bnd (n, val) = lbrace <> pretty n <+> text "=" <+> prettySe (decD d) startPrec bnd val <> rbrace
1683− prettyArgSc bnd val = lbrace <> lbrace <> prettySe startPrec bnd val <> rbrace <> rbrace
1690+ prettyArgSc d bnd val = lbrace <> lbrace <> prettySe (decD d) startPrec bnd val <> rbrace <> rbrace
1684− prettyArgSti bnd (n, val) = lbrace <> kwd "auto" <+> pretty n <+> text "=" <+> prettySe startPrec bnd val <> rbrace
1691+ prettyArgSti d bnd (n, val) = lbrace <> kwd "auto" <+> pretty n <+> text "=" <+> prettySe (decD d) startPrec bnd val <> rbrace
1685
1692
1686 annName :: Name -> Doc OutputAnnotation -> Doc OutputAnnotation
1693 annName :: Name -> Doc OutputAnnotation -> Doc OutputAnnotation
1687 annName n = annotate (AnnName n Nothing Nothing Nothing)
1694 annName n = annotate (AnnName n Nothing Nothing Nothing)
@@ -1690,35 +1697,36 @@ pprintPTerm ppo bnd docArgs infixes = prettySe startPrec bnd
1690 opStr (NS n _) = opStr n
1697 opStr (NS n _) = opStr n
1691 opStr (UN n) = T.unpack n
1698 opStr (UN n) = T.unpack n
1692
1699
1693− slist' _ _ e
1700+ slist' :: Maybe Int -> Int -> [(Name, Bool)] -> PTerm -> Maybe [Doc OutputAnnotation]
1701+ slist' (Just d) _ _ _ | d <= 0 = Nothing
1702+ slist' d _ _ e
1694 | containsHole e = Nothing
1703 | containsHole e = Nothing
1695− slist' p bnd (PApp _ (PRef _ nil) _)
1704+ slist' d p bnd (PApp _ (PRef _ nil) _)
1696 | not (ppopt_impl ppo) && nsroot nil == sUN "Nil" = Just []
1705 | not (ppopt_impl ppo) && nsroot nil == sUN "Nil" = Just []
1697− slist' p bnd (PRef _ nil)
1706+ slist' d p bnd (PRef _ nil)
1698 | not (ppopt_impl ppo) && nsroot nil == sUN "Nil" = Just []
1707 | not (ppopt_impl ppo) && nsroot nil == sUN "Nil" = Just []
1699− slist' p bnd (PApp _ (PRef _ cons) args)
1708+ slist' d p bnd (PApp _ (PRef _ cons) args)
1700 | nsroot cons == sUN "::",
1709 | nsroot cons == sUN "::",
1701 (PExp {getTm=tl}):(PExp {getTm=hd}):imps <- reverse args,
1710 (PExp {getTm=tl}):(PExp {getTm=hd}):imps <- reverse args,
1702 all isImp imps,
1711 all isImp imps,
1703− Just tl' <- slist' p bnd tl
1712+ Just tl' <- slist' (decD d) p bnd tl
1704− = Just (hd:tl')
1713+ = Just (prettySe d startPrec bnd hd : tl')
1705 where
1714 where
1706 isImp (PImp {}) = True
1715 isImp (PImp {}) = True
1707 isImp _ = False
1716 isImp _ = False
1708− slist' _ _ tm = Nothing
1717+ slist' _ _ _ tm = Nothing
1709−
1718+
1710− slist p bnd e | Just es <- slist' p bnd e = Just $
1719+ slist d p bnd e | Just es <- slist' d p bnd e = Just $
1720+ case es of
1711− case es of [] -> annotate (AnnData "" "") $ text "[]"
1721+ [] -> annotate (AnnData "" "") $ text "[]"
1712− [x] -> enclose left right . group $
1722+ [x] -> enclose left right . group $ x
1713− prettySe p bnd x
1714− xs -> (enclose left right .
1723+ xs -> enclose left right .
1715− align . group . vsep .
1724+ align . group . vsep .
1716− punctuate comma .
1725+ punctuate comma $ xs
1717− map (prettySe p bnd)) xs
1718 where left = (annotate (AnnData "" "") (text "["))
1726 where left = (annotate (AnnData "" "") (text "["))
1719 right = (annotate (AnnData "" "") (text "]"))
1727 right = (annotate (AnnData "" "") (text "]"))
1720 comma = (annotate (AnnData "" "") (text ","))
1728 comma = (annotate (AnnData "" "") (text ","))
1721− slist _ _ _ = Nothing
1729+ slist _ _ _ _ = Nothing
1722
1730
1723 pairElts :: PTerm -> Maybe [PTerm]
1731 pairElts :: PTerm -> Maybe [PTerm]
1724 pairElts (PPair _ _ x y) | Just elts <- pairElts y = Just (x:elts)
1732 pairElts (PPair _ _ x y) | Just elts <- pairElts y = Just (x:elts)
@@ -1727,18 +1735,27 @@ pprintPTerm ppo bnd docArgs infixes = prettySe startPrec bnd
1727
1735
1728 natns = "Prelude.Nat."
1736 natns = "Prelude.Nat."
1729
1737
1738+ snat :: Maybe Int -> Int -> PTerm -> Maybe Integer
1739+ snat (Just x) _ _ | x <= 0 = Nothing
1730− snat p (PRef _ z)
1740+ snat d p (PRef _ z)
1731 | show z == (natns++"Z") || show z == "Z" = Just 0
1741 | show z == (natns++"Z") || show z == "Z" = Just 0
1732− snat p (PApp _ s [PExp {getTm=n}])
1742+ snat d p (PApp _ s [PExp {getTm=n}])
1733 | show s == (natns++"S") || show s == "S",
1743 | show s == (natns++"S") || show s == "S",
1734− Just n' <- snat p n
1744+ Just n' <- snat (decD d) p n
1735 = Just $ 1 + n'
1745 = Just $ 1 + n'
1736− snat _ _ = Nothing
1746+ snat _ _ _ = Nothing
1737
1747
1738 bracket outer inner doc
1748 bracket outer inner doc
1739 | outer > inner = lparen <> doc <> rparen
1749 | outer > inner = lparen <> doc <> rparen
1740 | otherwise = doc
1750 | otherwise = doc
1741
1751
1752+ ellipsis = text "..."
1753+
1754+ depth Nothing = id
1755+ depth (Just d) = if d <= 0 then const (ellipsis) else id
1756+
1757+ decD = fmap (\x -> x - 1)
1758+
1742 kwd = annotate AnnKeyword . text
1759 kwd = annotate AnnKeyword . text
1743
1760
1744 fixities :: M.Map String Fixity
1761 fixities :: M.Map String Fixity
src/Idris/Core/TT.hs+16
@@ -1249,6 +1249,22 @@ unList tm = case unApply tm of
1249 return $ x:rest
1249 return $ x:rest
1250 (f, args) -> Nothing
1250 (f, args) -> Nothing
1251
1251
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+
1252-- | Cast a 'TT' term to a 'Raw' value, discarding universe information and
1268-- | Cast a 'TT' term to a 'Raw' value, discarding universe information and
1253-- the types of named references and replacing all de Bruijn indices
1269-- the types of named references and replacing all de Bruijn indices
1254-- with the corresponding name. It is an error if there are free de
1270-- 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
148 BoldText -> "bold"
148 BoldText -> "bold"
149 ItalicText -> "italic"
149 ItalicText -> "italic"
150 UnderlineText -> "underline"
150 UnderlineText -> "underline"
151+ toSExp (AnnTerm bnd tm)
151− toSExp (AnnTerm bnd tm) = toSExp [(SymbolAtom "tt-term", StringAtom (encodeTerm bnd tm))]
152+ | termSmallerThan 1000 tm = toSExp [(SymbolAtom "tt-term", StringAtom (encodeTerm bnd tm))]
153+ | otherwise = SexpList []
152 toSExp (AnnSearchResult ordr) = toSExp [(SymbolAtom "doc-overview",
154 toSExp (AnnSearchResult ordr) = toSExp [(SymbolAtom "doc-overview",
153 StringAtom ("Result type is " ++ descr))]
155 StringAtom ("Result type is " ++ descr))]
154 where descr = case ordr of
156 where descr = case ordr of
src/Idris/REPL.hs+21−17
@@ -496,7 +496,7 @@ runIdeModeCommand h id orig fn modes (IdeMode.BrowseNS ns) =
496runIdeModeCommand h id orig fn modes (IdeMode.TermNormalise bnd tm) =
496runIdeModeCommand h id orig fn modes (IdeMode.TermNormalise bnd tm) =
497 do ctxt <- getContext
497 do ctxt <- getContext
498 ist <- getIState
498 ist <- getIState
499− let tm' = force (normaliseAll ctxt [] tm)
499+ let tm' = normaliseAll ctxt [] tm
500 ptm = annotate (AnnTerm bnd tm')
500 ptm = annotate (AnnTerm bnd tm')
501 (pprintPTerm (ppOptionIst ist)
501 (pprintPTerm (ppOptionIst ist)
502 bnd
502 bnd
@@ -634,6 +634,8 @@ idemodeProcess fn (MakeWith False pos str) = process fn (MakeWith False pos str)
634idemodeProcess fn (DoProofSearch False r pos str xs) = process fn (DoProofSearch False r pos str xs)
634idemodeProcess fn (DoProofSearch False r pos str xs) = process fn (DoProofSearch False r pos str xs)
635idemodeProcess fn (SetConsoleWidth w) = do process fn (SetConsoleWidth w)
635idemodeProcess fn (SetConsoleWidth w) = do process fn (SetConsoleWidth w)
636 iPrintResult ""
636 iPrintResult ""
637+idemodeProcess fn (SetPrinterDepth d) = do process fn (SetPrinterDepth d)
638+ iPrintResult ""
637idemodeProcess fn (Apropos pkg a) = do process fn (Apropos pkg a)
639idemodeProcess fn (Apropos pkg a) = do process fn (Apropos pkg a)
638 iPrintResult ""
640 iPrintResult ""
639idemodeProcess fn (WhoCalls n) = process fn (WhoCalls n)
641idemodeProcess fn (WhoCalls n) = process fn (WhoCalls n)
@@ -767,21 +769,23 @@ process fn (ModImport f) = do fmod <- loadModule f
767 Just pr -> isetPrompt pr
769 Just pr -> isetPrompt pr
768 Nothing -> iPrintError $ "Can't find import " ++ f
770 Nothing -> iPrintError $ "Can't find import " ++ f
769process fn (Eval t)
771process fn (Eval t)
770− = withErrorReflection $ do logLvl 5 $ show t
772+ = withErrorReflection $
773+ do logLvl 5 $ show t
771− getIState >>= flip warnDisamb t
774+ getIState >>= flip warnDisamb t
772− (tm, ty) <- elabVal recinfo ERHS t
775+ (tm, ty) <- elabVal recinfo ERHS t
773− ctxt <- getContext
776+ ctxt <- getContext
774− let tm' = force (normaliseAll ctxt [] tm)
777+ let tm' = perhapsForce $ normaliseAll ctxt [] tm
775− let ty' = force (normaliseAll ctxt [] ty)
778+ let ty' = perhapsForce $ normaliseAll ctxt [] ty
776− -- Add value to context, call it "it"
779+ -- Add value to context, call it "it"
777− updateContext (addCtxtDef (sUN "it") (Function ty' tm'))
780+ updateContext (addCtxtDef (sUN "it") (Function ty' tm'))
778− ist <- getIState
781+ ist <- getIState
779− logLvl 3 $ "Raw: " ++ show (tm', ty')
782+ logLvl 3 $ "Raw: " ++ show (tm', ty')
780− logLvl 10 $ "Debug: " ++ showEnvDbg [] tm'
783+ logLvl 10 $ "Debug: " ++ showEnvDbg [] tm'
781− let tmDoc = pprintDelab ist tm'
784+ let tmDoc = pprintDelab ist tm'
782− tyDoc = pprintDelab ist ty'
785+ tyDoc = pprintDelab ist ty'
783− iPrintTermWithType tmDoc tyDoc
786+ iPrintTermWithType tmDoc tyDoc
784−
787+ where perhapsForce tm | termSmallerThan 100 tm = force tm
788+ | otherwise = tm
785
789
786process fn (NewDefn decls) = do
790process fn (NewDefn decls) = do
787 logLvl 3 ("Defining names using these decls: " ++ show (showDecls verbosePPOption decls))
791 logLvl 3 ("Defining names using these decls: " ++ show (showDecls verbosePPOption decls))
@@ -1239,7 +1243,7 @@ process fn ListErrorHandlers =
1239 [] -> "No registered error handlers"
1243 [] -> "No registered error handlers"
1240 handlers -> "Registered error handlers: " ++ (concat . intersperse ", " . map show) handlers
1244 handlers -> "Registered error handlers: " ++ (concat . intersperse ", " . map show) handlers
1241process fn (SetConsoleWidth w) = setWidth w
1245process fn (SetConsoleWidth w) = setWidth w
1242−
1246+process fn (SetPrinterDepth d) = setDepth d
1243process fn (Apropos pkgs a) =
1247process fn (Apropos pkgs a) =
1244 do orig <- getIState
1248 do orig <- getIState
1245 when (not (null pkgs)) $
1249 when (not (null pkgs)) $
src/Idris/REPLParser.hs+7−2
@@ -39,7 +39,7 @@ allHelp = [ (map (':' :) names, args, text)
39 | (names, args, text, _) <- parserCommandsForHelp ++ parserCommands ]
39 | (names, args, text, _) <- parserCommandsForHelp ++ parserCommands ]
40
40
41parserCommandsForHelp :: CommandTable
41parserCommandsForHelp :: CommandTable
42−parserCommandsForHelp =
42+parserCommandsForHelp =
43 [ exprArgCmd ["t", "type"] Check "Check the type of an expression"
43 [ exprArgCmd ["t", "type"] Check "Check the type of an expression"
44 , exprArgCmd ["core"] Core "View the core language representation of a term"
44 , exprArgCmd ["core"] Core "View the core language representation of a term"
45 , nameArgCmd ["miss", "missing"] Missing "Show missing clauses"
45 , nameArgCmd ["miss", "missing"] Missing "Show missing clauses"
@@ -82,6 +82,7 @@ parserCommandsForHelp =
82 , "Turn REPL colours on or off; set a specific colour"
82 , "Turn REPL colours on or off; set a specific colour"
83 , cmd_colour)
83 , cmd_colour)
84 , (["consolewidth"], ConsoleWidthArg, "Set the width of the console", cmd_consolewidth)
84 , (["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)
85 , noArgCmd ["q", "quit"] Quit "Exit the Idris system"
86 , noArgCmd ["q", "quit"] Quit "Exit the Idris system"
86 , noArgCmd ["w", "warranty"] Warranty "Displays warranty information"
87 , noArgCmd ["w", "warranty"] Warranty "Displays warranty information"
87 , (["let"], ManyArgs DeclArg
88 , (["let"], ManyArgs DeclArg
@@ -96,7 +97,7 @@ parserCommandsForHelp =
96 , cmd_pprint)
97 , cmd_pprint)
97 ]
98 ]
98
99
99−parserCommands =
100+parserCommands =
100 [ noArgCmd ["u", "universes"] Universes "Display universe constraints"
101 [ noArgCmd ["u", "universes"] Universes "Display universe constraints"
101 , noArgCmd ["errorhandlers"] ListErrorHandlers "List registered error handlers"
102 , noArgCmd ["errorhandlers"] ListErrorHandlers "List registered error handlers"
102
103
@@ -290,6 +291,10 @@ cmd_consolewidth name = do
290 <|> do n <- fmap (fromInteger . fst) P.natural
291 <|> do n <- fmap (fromInteger . fst) P.natural
291 return (ColsWide n)
292 return (ColsWide n)
292
293
294+cmd_printdepth :: String -> P.IdrisParser (Either String Command)
295+cmd_printdepth _ = do d <- optional (fmap (fromInteger . fst) P.natural)
296+ return (Right $ SetPrinterDepth d)
297+
293cmd_execute :: String -> P.IdrisParser (Either String Command)
298cmd_execute :: String -> P.IdrisParser (Either String Command)
294cmd_execute name = do
299cmd_execute name = do
295 tm <- option maintm (P.fullExpr defaultSyntax)
300 tm <- option maintm (P.fullExpr defaultSyntax)
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