git.iko.soy/Idris-dev
on master help sign in
Variable names in makelemma types
96e9b1aEdwin Brady
CHANGELOG+2
compare with master
unifiedsplit
@@ -24,6 +24,8 @@ New in 0.9.19:
24* More flexible 'case' construct, allowing each branch to target different
24* More flexible 'case' construct, allowing each branch to target different
25 types, provided that the case analysis does not affect the form of any
25 types, provided that the case analysis does not affect the form of any
26 variable used in the right hand side of the case.
26 variable used in the right hand side of the case.
27+* Some improvements in interactive editing, particularly in lifting out
28+ definitions and proof search.
27
29
28New in 0.9.18:
30New in 0.9.18:
29--------------
31--------------
src/Idris/AbsSyntaxTree.hs+16−3
@@ -121,6 +121,7 @@ defaultOpts = IOption { opt_logLevel = 0
121
121
122data PPOption = PPOption {
122data PPOption = PPOption {
123 ppopt_impl :: Bool -- ^^ whether to show implicits
123 ppopt_impl :: Bool -- ^^ whether to show implicits
124+ , ppopt_pinames :: Bool -- ^^ whether to show names in pi bindings
124 , ppopt_depth :: Maybe Int
125 , ppopt_depth :: Maybe Int
125} deriving (Show)
126} deriving (Show)
126
127
@@ -131,16 +132,21 @@ defaultOptimise = [PETransform]
131
132
132-- | Pretty printing options with default verbosity.
133-- | Pretty printing options with default verbosity.
133defaultPPOption :: PPOption
134defaultPPOption :: PPOption
134−defaultPPOption = PPOption { ppopt_impl = False , ppopt_depth = Just 200 }
135+defaultPPOption = PPOption { ppopt_impl = False,
136+ ppopt_pinames = False,
137+ ppopt_depth = Just 200 }
135
138
136-- | Pretty printing options with the most verbosity.
139-- | Pretty printing options with the most verbosity.
137verbosePPOption :: PPOption
140verbosePPOption :: PPOption
138−verbosePPOption = PPOption { ppopt_impl = True, ppopt_depth = Just 200 }
141+verbosePPOption = PPOption { ppopt_impl = True,
142+ ppopt_pinames = True,
143+ ppopt_depth = Just 200 }
139
144
140-- | Get pretty printing options from the big options record.
145-- | Get pretty printing options from the big options record.
141ppOption :: IOption -> PPOption
146ppOption :: IOption -> PPOption
142ppOption opt = PPOption {
147ppOption opt = PPOption {
143 ppopt_impl = opt_showimp opt,
148 ppopt_impl = opt_showimp opt,
149+ ppopt_pinames = False,
144 ppopt_depth = opt_printdepth opt
150 ppopt_depth = opt_printdepth opt
145}
151}
146
152
@@ -1558,7 +1564,8 @@ pprintPTerm ppo bnd docArgs infixes = prettySe (ppopt_depth ppo) startPrec bnd
1558 kwd "let" <+> (group . align . hang 2 $ prettyBindingOf n False <+> text "=" <$> prettySe (decD d) startPrec bnd v) </>
1564 kwd "let" <+> (group . align . hang 2 $ prettyBindingOf n False <+> text "=" <$> prettySe (decD d) startPrec bnd v) </>
1559 kwd "in" <+> (group . align . hang 2 $ prettySe (decD d) startPrec ((n, False):bnd) sc)
1565 kwd "in" <+> (group . align . hang 2 $ prettySe (decD d) startPrec ((n, False):bnd) sc)
1560 prettySe d p bnd (PPi (Exp l s _) n _ ty sc)
1566 prettySe d p bnd (PPi (Exp l s _) n _ ty sc)
1561− | n `elem` allNamesIn sc || ppopt_impl ppo || n `elem` docArgs =
1567+ | n `elem` allNamesIn sc || ppopt_impl ppo || n `elem` docArgs
1568+ || ppopt_pinames ppo && uname n =
1562 depth d . bracket p startPrec . group $
1569 depth d . bracket p startPrec . group $
1563 enclose lparen rparen (group . align $ prettyBindingOf n False <+> colon <+> prettySe (decD d) startPrec bnd ty) <+>
1570 enclose lparen rparen (group . align $ prettyBindingOf n False <+> colon <+> prettySe (decD d) startPrec bnd ty) <+>
1564 st <> text "->" <$> prettySe (decD d) startPrec ((n, False):bnd) sc
1571 st <> text "->" <$> prettySe (decD d) startPrec ((n, False):bnd) sc
@@ -1567,6 +1574,9 @@ pprintPTerm ppo bnd docArgs infixes = prettySe (ppopt_depth ppo) startPrec bnd
1567 group (prettySe (decD d) (startPrec + 1) bnd ty <+> st) <> text "->" <$>
1574 group (prettySe (decD d) (startPrec + 1) bnd ty <+> st) <> text "->" <$>
1568 group (prettySe (decD d) startPrec ((n, False):bnd) sc)
1575 group (prettySe (decD d) startPrec ((n, False):bnd) sc)
1569 where
1576 where
1577+ uname (UN _) = True
1578+ uname _ = False
1579+
1570 st =
1580 st =
1571 case s of
1581 case s of
1572 Static -> text "[static]" <> space
1582 Static -> text "[static]" <> space
@@ -2005,6 +2015,9 @@ showTm ist = displayDecorated (consoleDecorate ist) .
2005showTmImpls :: PTerm -> String
2015showTmImpls :: PTerm -> String
2006showTmImpls = flip (displayS . renderCompact . prettyImp verbosePPOption) ""
2016showTmImpls = flip (displayS . renderCompact . prettyImp verbosePPOption) ""
2007
2017
2018+-- | Show a term with specific options
2019+showTmOpts :: PPOption -> PTerm -> String
2020+showTmOpts opt = flip (displayS . renderPretty 1.0 10000000 . prettyImp opt) ""
2008
2021
2009
2022
2010instance Sized PTerm where
2023instance Sized PTerm where
src/Idris/Interactive.hs+2−1
@@ -307,7 +307,8 @@ makeLemma fn updatefile l n
307
307
308 let lem = show n ++ " : " ++
308 let lem = show n ++ " : " ++
309 constraints i classes mty ++
309 constraints i classes mty ++
310+ showTmOpts (defaultPPOption { ppopt_pinames = True })
310− show (stripMNBind skip (delab i mty))
311+ (stripMNBind skip (delab i mty))
311 let lem_app = show n ++ appArgs skip margs mty
312 let lem_app = show n ++ appArgs skip margs mty
312
313
313 if updatefile then
314 if updatefile then