2d79c85 · Idris-dev · git.iko.soy

CHANGELOG+6−4

compare with master

unifiedsplit

@@ -13,10 +13,12 @@ New in 0.9.12:

13* Syntax for dealing with match failure in <- and pattern matching let.

14* New syntax for inline documentation. Documentation starts with |||, and

15 arguments are documented by preceding their name with @. Example:

16−||| Add two natural numbers

16+ ||| Add two natural numbers

17−||| @ n the first number (examined by the function)

17+ ||| @ n the first number (examined by the function)

18−||| @ m the second number (not examined)

18+ ||| @ m the second number (not examined)

19−plus (n, m : Nat) -> Nat

19+ plus (n, m : Nat) -> Nat

20+* Allow the auto-solve behavior in the prover to be disabled, for easier debugging

21+ of proof automation. Use ":set autosolve" and ":unset autosolve".

20

22

21New in 0.9.11:

23New in 0.9.11:

22--------------

24--------------

libs/base/Language/Reflection.idr+2

@@ -180,6 +180,8 @@ data Tactic = Try Tactic Tactic

180 -- ^ invoke the reflected rep. of another tactic

181 | Reflect TT

182 -- ^ turn a value into its reflected representation

183+ | ByReflection TT

184+ -- ^ use a %reflection function

183 | Fill Raw

185 | Fill Raw

184 -- ^ turn a raw value back into a term

186 -- ^ turn a raw value back into a term

185 | Exact TT

187 | Exact TT

src/Idris/AbsSyntax.hs+6

@@ -713,6 +713,12 @@ setShowOrigErr b = do i <- getIState

713 let opt' = opts { opt_origerr = b }

714 putIState $ i { idris_options = opt' }

715

716+setAutoSolve :: Bool -> Idris ()

717+setAutoSolve b = do i <- getIState

718+ let opts = idris_options i

719+ let opt' = opts { opt_autoSolve = b }

720+ putIState $ i { idris_options = opt' }

721+

716setNoBanner :: Bool -> Idris ()

722setNoBanner :: Bool -> Idris ()

717setNoBanner n = do i <- getIState

723setNoBanner n = do i <- getIState

718 let opts = idris_options i

724 let opts = idris_options i

src/Idris/AbsSyntaxTree.hs+4−1

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

53 opt_cpu :: String,

54 opt_optLevel :: Word,

55 opt_cmdline :: [Opt], -- remember whole command line

56− opt_origerr :: Bool

56+ opt_origerr :: Bool,

57+ opt_autoSolve :: Bool -- ^ automatically apply "solve" tactic in prover

57 }

58 }

58 deriving (Show, Eq)

59 deriving (Show, Eq)

59

60

@@ -76,6 +77,7 @@ defaultOpts = IOption { opt_logLevel = 0

76 , opt_optLevel = 2

77 , opt_optLevel = 2

77 , opt_cmdline = []

78 , opt_cmdline = []

78 , opt_origerr = False

79 , opt_origerr = False

80+ , opt_autoSolve = True

79 }

81 }

80

82

81data LanguageExt = TypeProviders | ErrorReflection deriving (Show, Eq, Read, Ord)

83data LanguageExt = TypeProviders | ErrorReflection deriving (Show, Eq, Read, Ord)

@@ -336,6 +338,7 @@ data Opt = Filename String

336 | Client String

338 | Client String

337 | ShowOrigErr

339 | ShowOrigErr

338 | AutoWidth -- ^ Automatically adjust terminal width

340 | AutoWidth -- ^ Automatically adjust terminal width

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

339 deriving (Show, Eq)

342 deriving (Show, Eq)

340

343

341-- Parsed declarations

344-- Parsed declarations

src/Idris/Completion.hs+5−1

@@ -108,7 +108,11 @@ completeMetaVar = completeWord Nothing (" \t(){}:" ++ opChars) completeM

108

109completeOption :: CompletionFunc Idris

110completeOption = completeWord Nothing " \t" completeOpt

111− where completeOpt = return . completeWith ["errorcontext", "showimplicits", "originalerrors"]

111+ where completeOpt = return . completeWith [ "errorcontext"

112+ , "showimplicits"

113+ , "originalerrors"

114+ , "autosolve"

115+ ]

112

116

113completeConsoleWidth :: CompletionFunc Idris

117completeConsoleWidth :: CompletionFunc Idris

114completeConsoleWidth = completeWord Nothing " \t" completeW

118completeConsoleWidth = completeWord Nothing " \t" completeW

src/Idris/ElabTerm.hs+2

@@ -1205,6 +1205,8 @@ reifyApp ist t [t']

1205 | t == reflm "ApplyTactic" = liftM (ApplyTactic . delab ist) (reifyTT t')

1206reifyApp ist t [t']

1207 | t == reflm "Reflect" = liftM (Reflect . delab ist) (reifyTT t')

1208+reifyApp ist t [t']

1209+ | t == reflm "ByReflection" = liftM (ByReflection . delab ist) (reifyTT t')

1208reifyApp _ t [t']

1210reifyApp _ t [t']

1209 | t == reflm "Fill" = liftM (Fill . PQuote) (reifyRaw t')

1211 | t == reflm "Fill" = liftM (Fill . PQuote) (reifyRaw t')

1210reifyApp ist t [t']

1212reifyApp ist t [t']

src/Idris/Prover.hs+2−1

@@ -164,6 +164,7 @@ receiveInput e =

164ploop :: Name -> Bool -> String -> [String] -> ElabState [PDecl] -> Maybe History -> Idris (Term, [String])

165ploop fn d prompt prf e h

166 = do i <- getIState

167+ let autoSolve = opt_autoSolve (idris_options i)

167 when d $ dumpState i (proof e)

168 when d $ dumpState i (proof e)

168 (x, h') <-

169 (x, h') <-

169 case idris_outputmode i of

170 case idris_outputmode i of

@@ -260,7 +261,7 @@ ploop fn d prompt prf e h

260 return (False, e, False, prf))

261 return (False, e, False, prf))

261 (\err -> do putIState ist ; ierror err)

262 (\err -> do putIState ist ; ierror err)

262 Success tac -> do (_, e) <- elabStep e saveState

263 Success tac -> do (_, e) <- elabStep e saveState

263− (_, st) <- elabStep e (runTac True i fn tac)

264+ (_, st) <- elabStep e (runTac autoSolve i fn tac)

264-- trace (show (problems (proof st))) $

265-- trace (show (problems (proof st))) $

265 iPrintResult ""

266 iPrintResult ""

266 return (True, st, False, prf ++ [step]))

267 return (True, st, False, prf ++ [step]))

src/Idris/REPL.hs+2

@@ -932,6 +932,8 @@ process h fn (SetOpt ShowImpl) = setImpShow True

932process h fn (UnsetOpt ShowImpl) = setImpShow False

933process h fn (SetOpt ShowOrigErr) = setShowOrigErr True

934process h fn (UnsetOpt ShowOrigErr) = setShowOrigErr False

935+process h fn (SetOpt AutoSolve) = setAutoSolve True

936+process h fn (UnsetOpt AutoSolve) = setAutoSolve False

935

937

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

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

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

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

src/Idris/REPLParser.hs+1

@@ -107,6 +107,7 @@ pOption :: P.IdrisParser Opt

107pOption = do discard (P.symbol "errorcontext"); return ErrContext

108 <|> do discard (P.symbol "showimplicits"); return ShowImpl

109 <|> do discard (P.symbol "originalerrors"); return ShowOrigErr

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

110

111

111pConsoleWidth :: P.IdrisParser ConsoleWidth

112pConsoleWidth :: P.IdrisParser ConsoleWidth

112pConsoleWidth = do discard (P.symbol "auto"); return AutomaticWidth

113pConsoleWidth = do discard (P.symbol "auto"); return AutomaticWidth