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

git.iko.soy/Idris-dev

on master help sign in

Add option to desugar nats in REPL output

49fae22ben-schulz11 years ago

src/Idris/AbsSyntax.hs+12

compare with master

unifiedsplit

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

800 let opt' = opts { opt_evaltypes = n }

801 putIState $ i { idris_options = opt' }

802

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+

803setQuiet :: Bool -> Idris ()

815setQuiet :: Bool -> Idris ()

804setQuiet q = do i <- getIState

816setQuiet q = do i <- getIState

805 let opts = idris_options i

817 let opts = idris_options i

src/Idris/AbsSyntaxTree.hs+25−13

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

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

91 opt_optimise :: [Optimisation],

92 opt_printdepth :: Maybe Int,

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

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

94+ opt_desugarnats :: Bool

94− }

95+ }

95 deriving (Show, Eq)

96 deriving (Show, Eq)

97defaultOpts = IOption { opt_logLevel = 0

98defaultOpts = IOption { opt_logLevel = 0

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

117 , opt_optimise = defaultOptimise

118 , opt_optimise = defaultOptimise

118 , opt_printdepth = Just 5000

119 , opt_printdepth = Just 5000

119 , opt_evaltypes = True

120 , opt_evaltypes = True

121+ , opt_desugarnats = False

120 }

122 }

121

123

122data PPOption = PPOption {

124data PPOption = PPOption {

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

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

126+ , ppopt_desugarnats :: Bool

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

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

125 , ppopt_depth :: Maybe Int

128 , ppopt_depth :: Maybe Int

126} deriving (Show)

129} deriving (Show)

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

133-- | Pretty printing options with default verbosity.

136-- | Pretty printing options with default verbosity.

134defaultPPOption :: PPOption

137defaultPPOption :: PPOption

135defaultPPOption = PPOption { ppopt_impl = False,

138defaultPPOption = PPOption { ppopt_impl = False,

139+ ppopt_desugarnats = False,

136 ppopt_pinames = False,

140 ppopt_pinames = False,

137 ppopt_depth = Just 200 }

141 ppopt_depth = Just 200 }

138

142

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

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

140verbosePPOption :: PPOption

144verbosePPOption :: PPOption

141verbosePPOption = PPOption { ppopt_impl = True,

145verbosePPOption = PPOption { ppopt_impl = True,

146+ ppopt_desugarnats = True,

142 ppopt_pinames = True,

147 ppopt_pinames = True,

143 ppopt_depth = Just 200 }

148 ppopt_depth = Just 200 }

144

149

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

147ppOption opt = PPOption {

152ppOption opt = PPOption {

148 ppopt_impl = opt_showimp opt,

153 ppopt_impl = opt_showimp opt,

149 ppopt_pinames = False,

154 ppopt_pinames = False,

150− ppopt_depth = opt_printdepth opt

155+ ppopt_depth = opt_printdepth opt,

156+ ppopt_desugarnats = opt_desugarnats opt

151}

157}

152

158

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

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

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

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

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

504 | UseConsoleWidth ConsoleWidth

510 | UseConsoleWidth ConsoleWidth

505 | DumpHighlights

511 | DumpHighlights

512+ | DesugarNats

506 deriving (Show, Eq)

513 deriving (Show, Eq)

507

514

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

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

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

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

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

1654 prettySe d p bnd e

1661 prettySe d p bnd e

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

1662 | 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))

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

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

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

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

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

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

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

1944

1951

1945 natns = "Prelude.Nat."

1952 natns = "Prelude.Nat."

1946

1953

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

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

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

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

1949− snat d p (PRef _ _ z)

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

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

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

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

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

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

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

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

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

1954− = Just $ 1 + n'

1966+ = Just $ 1 + n'

1955− snat _ _ _ = Nothing

1967+ snat' _ _ _ = Nothing

1956

1968

1957 bracket outer inner doc

1969 bracket outer inner doc

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

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

src/Idris/DeepSeq.hs+4−1

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

125 rnf (WarnPartial) = ()

126 rnf (WarnReach) = ()

127 rnf (EvalTypes) = ()

128+ rnf (DesugarNats) = ()

128 rnf (NoCoverage) = ()

129 rnf (NoCoverage) = ()

129 rnf (ErrContext) = ()

130 rnf (ErrContext) = ()

130 rnf (ShowImpl) = ()

131 rnf (ShowImpl) = ()

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

192 opt_autoImport

193 opt_autoImport

193 opt_optimise

194 opt_optimise

194 opt_printdepth

195 opt_printdepth

195− opt_evaltypes) =

196+ opt_evaltypes

197+ opt_desugarnats) =

196 rnf opt_logLevel

198 rnf opt_logLevel

197 `seq` rnf opt_typecase

199 `seq` rnf opt_typecase

198 `seq` rnf opt_typeintype

200 `seq` rnf opt_typeintype

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

216 `seq` rnf opt_optimise

218 `seq` rnf opt_optimise

217 `seq` rnf opt_printdepth

219 `seq` rnf opt_printdepth

218 `seq` rnf opt_evaltypes

220 `seq` rnf opt_evaltypes

221+ `seq` rnf opt_desugarnats

219 `seq` ()

222 `seq` ()

220

223

221instance NFData LanguageExt where

224instance NFData LanguageExt where

src/Idris/Delaborate.hs+5−1

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

1{-# LANGUAGE PatternGuards #-}

2{-# 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

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

6-- purposes.

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

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

227 (prettyIst ist (delabSugared ist tm))

228

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

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

231+ (prettyIst ist (delab ist tm))

232+

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

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

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

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

231pprintDelabTy i n

235pprintDelabTy i n

src/Idris/REPL.hs+4−1

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

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

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

810 let tmDoc = pprintDelab ist tm'

811− tyDoc = pprintDelab ist ty'

811+ tyDoc = pprintDelab ist ty'

812 iPrintTermWithType tmDoc tyDoc

813 where perhapsForce tm | termSmallerThan 100 tm = force tm

814 | otherwise = tm

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

1266process fn (SetOpt EvalTypes) = setEvalTypes True

1267process fn (UnsetOpt EvalTypes) = setEvalTypes False

1268

1269+process fn (SetOpt DesugarNats) = setDesugarNats True

1270+process fn (UnsetOpt DesugarNats) = setDesugarNats False

1271+

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

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

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

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

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

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

src/Idris/REPLParser.hs+1

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

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

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

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

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

263

264

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

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

265proofArg cmd name = do

266proofArg cmd name = do