740d82d · Idris-dev · git.iko.soy

git.iko.soy/Idris-dev

Display normalised types on :t for expressions

Behaviour of :t on names remains the same (showing the non-normalised type). Added evaltypes option (on by default) so the old behaviour can be regained with :unset evaltypes. This means partially applied things with interesting types will be displayed more helpfully, e.g.: *printf> :t printf "%s %d" printf "%s %d" : String -> Int -> String

commit740d82d7da51b3e2b4d69b9a8480dae255439649 authorEdwin Brady <ecb10@st-andrews.ac.uk> dateSat 25 Jul 2015, 20:15 (11 years ago) parentbf52728

5 files changed+18−4

compare with master

unifiedsplit

src/Idris/AbsSyntax.hs+6 src/Idris/AbsSyntaxTree.hs+4−1 src/Idris/IBC.hs+1−1 src/Idris/REPL.hs+6−2 src/Idris/REPLParser.hs+1

src/Idris/AbsSyntax.hs+6

@@ -790,6 +790,12 @@ getNoBanner = do i <- getIState

790790 let opts = idris_options i

791791 return (opt_nobanner opts)

792792

793+setEvalTypes :: Bool -> Idris ()

794+setEvalTypes n = do i <- getIState

795+ let opts = idris_options i

796+ let opt' = opts { opt_evaltypes = n }

797+ putIState $ i { idris_options = opt' }

798+

793799setQuiet :: Bool -> Idris ()

794800setQuiet q = do i <- getIState

795801 let opts = idris_options i

src/Idris/AbsSyntaxTree.hs+4−1

@@ -89,7 +89,8 @@ data IOption = IOption { opt_logLevel :: Int,

8989 opt_autoSolve :: Bool, -- ^ automatically apply "solve" tactic in prover

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

9191 opt_optimise :: [Optimisation],

92− opt_printdepth :: Maybe Int

92+ opt_printdepth :: Maybe Int,

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

9394 }

9495 deriving (Show, Eq)

9596

@@ -115,6 +116,7 @@ defaultOpts = IOption { opt_logLevel = 0

115116 , opt_autoImport = []

116117 , opt_optimise = defaultOptimise

117118 , opt_printdepth = Just 5000

119+ , opt_evaltypes = True

118120 }

119121

120122data PPOption = PPOption {

@@ -451,6 +453,7 @@ data Opt = Filename String

451453 | DefaultPartial

452454 | WarnPartial

453455 | WarnReach

456+ | EvalTypes

454457 | NoCoverage

455458 | ErrContext

456459 | ShowImpl

src/Idris/IBC.hs+1−1

@@ -365,7 +365,7 @@ timestampOlder :: FilePath -> FilePath -> Idris ()

365365timestampOlder src ibc = do srct <- runIO $ getModificationTime src

366366 ibct <- runIO $ getModificationTime ibc

367367 if (srct > ibct)

368− then ifail "Needs reloading"

368+ then ifail $ "Needs reloading " ++ show (srct, ibct)

369369 else return ()

370370

371371pPostulates :: [Name] -> Idris ()

src/Idris/REPL.hs+6−2

@@ -934,12 +934,14 @@ process fn (Check t)

934934 ctxt <- getContext

935935 ist <- getIState

936936 let ppo = ppOptionIst ist

937− ty' = normaliseC ctxt [] ty

937+ ty' = if opt_evaltypes (idris_options ist)

938+ then normaliseC ctxt [] ty

939+ else ty

938940 case tm of

939941 TType _ ->

940942 iPrintTermWithType (prettyIst ist (PType emptyFC)) type1Doc

941943 _ -> iPrintTermWithType (pprintDelab ist tm)

942− (pprintDelab ist ty)

944+ (pprintDelab ist ty')

943945

944946process fn (Core t)

945947 = do (tm, ty) <- elabREPL recinfo ERHS t

@@ -1234,6 +1236,8 @@ process fn (SetOpt NoBanner) = setNoBanner True

12341236process fn (UnsetOpt NoBanner) = setNoBanner False

12351237process fn (SetOpt WarnReach) = fmodifyState opts_idrisCmdline $ nub . (WarnReach:)

12361238process fn (UnsetOpt WarnReach) = fmodifyState opts_idrisCmdline $ delete WarnReach

1239+process fn (SetOpt EvalTypes) = setEvalTypes True

1240+process fn (UnsetOpt EvalTypes) = setEvalTypes False

12371241

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

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

src/Idris/REPLParser.hs+1

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

257257 <|> do discard (P.symbol "autosolve"); return AutoSolve

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

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

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

260261

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

262263proofArg cmd name = do