49fae22 · Idris-dev · git.iko.soy

git.iko.soy/Idris-dev

Add option to desugar nats in REPL output

Added option 'desugarnats' to REPL's ':set' and ':unset' commands. Setting this option prevents the pretty-printer from resugaring terms of type Nat, as resugaring may obscure unification performed by an implicit search. The 'desugarnats' option is set to 'false' by default. Resolves: #2507

commit49fae22e4bcdfac37099ed7eadd5a644d12ab9d6 authorben-schulz <benjamin.john.schulz@gmail.com> dateTue 15 Sep 2015, 22:07 (11 years ago) parent3a32759

6 files changed+51−16

compare with master

unifiedsplit

src/Idris/AbsSyntax.hs+12 src/Idris/AbsSyntaxTree.hs+25−13 src/Idris/DeepSeq.hs+4−1 src/Idris/Delaborate.hs+5−1 src/Idris/REPL.hs+4−1 src/Idris/REPLParser.hs+1

src/Idris/AbsSyntax.hs+12

@@ -800,6 +800,18 @@ setEvalTypes n = do i <- getIState

800800 let opt' = opts { opt_evaltypes = n }

801801 putIState $ i { idris_options = opt' }

802802

803+getDesugarNats :: Idris Bool

804+getDesugarNats = do i <- getIState

805+ let opts = idris_options i

806+ return (opt_desugarnats opts)

807+

808+

809+setDesugarNats :: Bool -> Idris ()

810+setDesugarNats n = do i <- getIState

811+ let opts = idris_options i

812+ let opt' = opts { opt_desugarnats = n }

813+ putIState $ i { idris_options = opt' }

814+

803815setQuiet :: Bool -> Idris ()

804816setQuiet q = do i <- getIState

805817 let opts = idris_options i

src/Idris/AbsSyntaxTree.hs+25−13

@@ -90,8 +90,9 @@ data IOption = IOption { opt_logLevel :: Int,

9090 opt_autoImport :: [FilePath], -- ^ e.g. Builtins+Prelude

9191 opt_optimise :: [Optimisation],

9292 opt_printdepth :: Maybe Int,

93− opt_evaltypes :: Bool -- ^ normalise types in :t

94− }

93+ opt_evaltypes :: Bool, -- ^ normalise types in :t

94+ opt_desugarnats :: Bool

95+ }

9596 deriving (Show, Eq)

9697

9798defaultOpts = IOption { opt_logLevel = 0

@@ -117,10 +118,12 @@ defaultOpts = IOption { opt_logLevel = 0

117118 , opt_optimise = defaultOptimise

118119 , opt_printdepth = Just 5000

119120 , opt_evaltypes = True

121+ , opt_desugarnats = False

120122 }

121123

122124data PPOption = PPOption {

123125 ppopt_impl :: Bool -- ^^ whether to show implicits

126+ , ppopt_desugarnats :: Bool

124127 , ppopt_pinames :: Bool -- ^^ whether to show names in pi bindings

125128 , ppopt_depth :: Maybe Int

126129} deriving (Show)

@@ -133,12 +136,14 @@ defaultOptimise = [PETransform]

133136-- | Pretty printing options with default verbosity.

134137defaultPPOption :: PPOption

135138defaultPPOption = PPOption { ppopt_impl = False,

139+ ppopt_desugarnats = False,

136140 ppopt_pinames = False,

137141 ppopt_depth = Just 200 }

138142

139143-- | Pretty printing options with the most verbosity.

140144verbosePPOption :: PPOption

141145verbosePPOption = PPOption { ppopt_impl = True,

146+ ppopt_desugarnats = True,

142147 ppopt_pinames = True,

143148 ppopt_depth = Just 200 }

144149

@@ -147,7 +152,8 @@ ppOption :: IOption -> PPOption

147152ppOption opt = PPOption {

148153 ppopt_impl = opt_showimp opt,

149154 ppopt_pinames = False,

150− ppopt_depth = opt_printdepth opt

155+ ppopt_depth = opt_printdepth opt,

156+ ppopt_desugarnats = opt_desugarnats opt

151157}

152158

153159-- | Get pretty printing options from an idris state record.

@@ -503,6 +509,7 @@ data Opt = Filename String

503509 | AutoSolve -- ^ Automatically issue "solve" tactic in interactive prover

504510 | UseConsoleWidth ConsoleWidth

505511 | DumpHighlights

512+ | DesugarNats

506513 deriving (Show, Eq)

507514

508515data ElabShellCmd = EQED | EAbandon | EUndo | EProofState | EProofTerm

@@ -1653,7 +1660,7 @@ pprintPTerm ppo bnd docArgs infixes = prettySe (ppopt_depth ppo) startPrec bnd

16531660 prettySe d p bnd (PPatvar fc n) = pretty n

16541661 prettySe d p bnd e

16551662 | Just str <- slist d p bnd e = depth d $ str

1656− | Just n <- snat d p e = depth d $ annotate (AnnData "Nat" "") (text (show n))

1663+ | Just n <- snat ppo d p e = depth d $ annotate (AnnData "Nat" "") (text (show n))

16571664 prettySe d p bnd (PRef fc _ n) = prettyName True (ppopt_impl ppo) bnd n

16581665 prettySe d p bnd (PLam fc n nfc ty sc) =

16591666 depth d . bracket p startPrec . group . align . hang 2 $

@@ -1944,15 +1951,20 @@ pprintPTerm ppo bnd docArgs infixes = prettySe (ppopt_depth ppo) startPrec bnd

19441951

19451952 natns = "Prelude.Nat."

19461953

1947− snat :: Maybe Int -> Int -> PTerm -> Maybe Integer

1948− snat (Just x) _ _ | x <= 0 = Nothing

1949− snat d p (PRef _ _ z)

1950− | show z == (natns++"Z") || show z == "Z" = Just 0

1951− snat d p (PApp _ s [PExp {getTm=n}])

1952− | show s == (natns++"S") || show s == "S",

1953− Just n' <- snat (decD d) p n

1954− = Just $ 1 + n'

1955− snat _ _ _ = Nothing

1954+ snat :: PPOption -> Maybe Int -> Int -> PTerm -> Maybe Integer

1955+ snat ppo d p e

1956+ | ppopt_desugarnats ppo = Nothing

1957+ | otherwise = snat' d p e

1958+ where

1959+ snat' :: Maybe Int -> Int -> PTerm -> Maybe Integer

1960+ snat' (Just x) _ _ | x <= 0 = Nothing

1961+ snat' d p (PRef _ _ z)

1962+ | show z == (natns++"Z") || show z == "Z" = Just 0

1963+ snat' d p (PApp _ s [PExp {getTm=n}])

1964+ | show s == (natns++"S") || show s == "S",

1965+ Just n' <- snat' (decD d) p n

1966+ = Just $ 1 + n'

1967+ snat' _ _ _ = Nothing

19561968

19571969 bracket outer inner doc

19581970 | outer > inner = lparen <> doc <> rparen

src/Idris/DeepSeq.hs+4−1

@@ -125,6 +125,7 @@ instance NFData Opt where

125125 rnf (WarnPartial) = ()

126126 rnf (WarnReach) = ()

127127 rnf (EvalTypes) = ()

128+ rnf (DesugarNats) = ()

128129 rnf (NoCoverage) = ()

129130 rnf (ErrContext) = ()

130131 rnf (ShowImpl) = ()

@@ -192,7 +193,8 @@ instance NFData IOption where

192193 opt_autoImport

193194 opt_optimise

194195 opt_printdepth

195− opt_evaltypes) =

196+ opt_evaltypes

197+ opt_desugarnats) =

196198 rnf opt_logLevel

197199 `seq` rnf opt_typecase

198200 `seq` rnf opt_typeintype

@@ -216,6 +218,7 @@ instance NFData IOption where

216218 `seq` rnf opt_optimise

217219 `seq` rnf opt_printdepth

218220 `seq` rnf opt_evaltypes

221+ `seq` rnf opt_desugarnats

219222 `seq` ()

220223

221224instance NFData LanguageExt where

src/Idris/Delaborate.hs+5−1

@@ -1,6 +1,6 @@

11{-# LANGUAGE PatternGuards #-}

22{-# OPTIONS_GHC -fwarn-incomplete-patterns #-}

3−module Idris.Delaborate (annName, bugaddr, delab, delab', delabMV, delabSugared, delabTy, delabTy', fancifyAnnots, pprintDelab, pprintDelabTy, pprintErr, resugar) where

3+module Idris.Delaborate (annName, bugaddr, delab, delab', delabMV, delabSugared, delabTy, delabTy', fancifyAnnots, pprintDelab, pprintNoDelab, pprintDelabTy, pprintErr, resugar) where

55-- Convert core TT back into high level syntax, primarily for display

66-- purposes.

@@ -226,6 +226,10 @@ pprintDelab :: IState -> Term -> Doc OutputAnnotation

226226pprintDelab ist tm = annotate (AnnTerm [] tm)

227227 (prettyIst ist (delabSugared ist tm))

228228

229+pprintNoDelab :: IState -> Term -> Doc OutputAnnotation

230+pprintNoDelab ist tm = annotate (AnnTerm [] tm)

231+ (prettyIst ist (delab ist tm))

232+

229233-- | Pretty-print the type of some name

230234pprintDelabTy :: IState -> Name -> Doc OutputAnnotation

231235pprintDelabTy i n

src/Idris/REPL.hs+4−1

@@ -808,7 +808,7 @@ process fn (Eval t)

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

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

810810 let tmDoc = pprintDelab ist tm'

811− tyDoc = pprintDelab ist ty'

811+ tyDoc = pprintDelab ist ty'

812812 iPrintTermWithType tmDoc tyDoc

813813 where perhapsForce tm | termSmallerThan 100 tm = force tm

814814 | otherwise = tm

@@ -1266,6 +1266,9 @@ process fn (UnsetOpt WarnReach) = fmodifyState opts_idrisCmdline $ delete Warn

12661266process fn (SetOpt EvalTypes) = setEvalTypes True

12671267process fn (UnsetOpt EvalTypes) = setEvalTypes False

12681268

1269+process fn (SetOpt DesugarNats) = setDesugarNats True

1270+process fn (UnsetOpt DesugarNats) = setDesugarNats False

1271+

12691272process fn (SetOpt _) = iPrintError "Not a valid option"

12701273process fn (UnsetOpt _) = iPrintError "Not a valid option"

12711274process fn (SetColour ty c) = setColour ty c

src/Idris/REPLParser.hs+1

@@ -260,6 +260,7 @@ optArg cmd name = do

260260 <|> do discard (P.symbol "nobanner") ; return NoBanner

261261 <|> do discard (P.symbol "warnreach"); return WarnReach

262262 <|> do discard (P.symbol "evaltypes"); return EvalTypes

263+ <|> do discard (P.symbol "desugarnats"); return DesugarNats

263264

264265proofArg :: (Bool -> Int -> Name -> Command) -> String -> P.IdrisParser (Either String Command)

265266proofArg cmd name = do