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

src/Idris/AbsSyntax.hs+6

compare with master

unifiedsplit

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

790 let opts = idris_options i

791 return (opt_nobanner opts)

792

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+

793setQuiet :: Bool -> Idris ()

799setQuiet :: Bool -> Idris ()

794setQuiet q = do i <- getIState

800setQuiet q = do i <- getIState

795 let opts = idris_options i

801 let opts = idris_options i

src/Idris/AbsSyntaxTree.hs+4−1

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

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

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

91 opt_optimise :: [Optimisation],

92− opt_printdepth :: Maybe Int

92+ opt_printdepth :: Maybe Int,

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

93 }

94 }

94 deriving (Show, Eq)

95 deriving (Show, Eq)

95

96

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

115 , opt_autoImport = []

116 , opt_autoImport = []

116 , opt_optimise = defaultOptimise

117 , opt_optimise = defaultOptimise

117 , opt_printdepth = Just 5000

118 , opt_printdepth = Just 5000

119+ , opt_evaltypes = True

118 }

120 }

119

121

120data PPOption = PPOption {

122data PPOption = PPOption {

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

451 | DefaultPartial

453 | DefaultPartial

452 | WarnPartial

454 | WarnPartial

453 | WarnReach

455 | WarnReach

456+ | EvalTypes

454 | NoCoverage

457 | NoCoverage

455 | ErrContext

458 | ErrContext

456 | ShowImpl

459 | ShowImpl

src/Idris/IBC.hs+1−1

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

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

366 ibct <- runIO $ getModificationTime ibc

367 if (srct > ibct)

368− then ifail "Needs reloading"

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

369 else return ()

370

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

src/Idris/REPL.hs+6−2

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

934 ctxt <- getContext

935 ist <- getIState

936 let ppo = ppOptionIst ist

937+ ty' = if opt_evaltypes (idris_options ist)

937− ty' = normaliseC ctxt [] ty

938+ then normaliseC ctxt [] ty

939+ else ty

938 case tm of

940 case tm of

939 TType _ ->

941 TType _ ->

940 iPrintTermWithType (prettyIst ist (PType emptyFC)) type1Doc

942 iPrintTermWithType (prettyIst ist (PType emptyFC)) type1Doc

941 _ -> iPrintTermWithType (pprintDelab ist tm)

943 _ -> iPrintTermWithType (pprintDelab ist tm)

942− (pprintDelab ist ty)

944+ (pprintDelab ist ty')

943

945

944process fn (Core t)

946process fn (Core t)

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

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

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

1234process fn (UnsetOpt NoBanner) = setNoBanner False

1236process fn (UnsetOpt NoBanner) = setNoBanner False

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

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

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

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

1239+process fn (SetOpt EvalTypes) = setEvalTypes True

1240+process fn (UnsetOpt EvalTypes) = setEvalTypes False

1237

1241

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

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

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

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

src/Idris/REPLParser.hs+1

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

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

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

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

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

260

261

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

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

262proofArg cmd name = do

263proofArg cmd name = do