423b4c4 · Idris-dev · git.iko.soy

git.iko.soy/Idris-dev

Allow users to disable the auto-solve in the prover

Use :set autosolve and :unset autosolve to do this.

commit423b4c4076fb033c470278b79aa3e24433761856 authorDavid Raymond Christiansen <david@davidchristiansen.dk> dateFri 7 Mar 2014, 09:16 (13 years ago) parentd0edb70

7 files changed+26−7

compare with master

unifiedsplit

CHANGELOG+6−4 src/Idris/AbsSyntax.hs+6 src/Idris/AbsSyntaxTree.hs+4−1 src/Idris/Completion.hs+5−1 src/Idris/Prover.hs+2−1 src/Idris/REPL.hs+2 src/Idris/REPLParser.hs+1

CHANGELOG+6−4

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

1212* Allow type providers to return postulates in addition to terms

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

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

15−||| Add two natural numbers

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

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

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

15+ ||| Add two natural numbers

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

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

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

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

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

1921

2022New in 0.9.11:

2123--------------

src/Idris/AbsSyntax.hs+6

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

713713 let opt' = opts { opt_origerr = b }

714714 putIState $ i { idris_options = opt' }

715715

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+

716722setNoBanner :: Bool -> Idris ()

717723setNoBanner n = do i <- getIState

718724 let opts = idris_options i

src/Idris/AbsSyntaxTree.hs+4−1

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

5353 opt_cpu :: String,

5454 opt_optLevel :: Word,

5555 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

5758 }

5859 deriving (Show, Eq)

5960

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

7677 , opt_optLevel = 2

7778 , opt_cmdline = []

7879 , opt_origerr = False

80+ , opt_autoSolve = True

7981 }

8082

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

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

336338 | Client String

337339 | ShowOrigErr

338340 | AutoWidth -- ^ Automatically adjust terminal width

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

339342 deriving (Show, Eq)

340343

341344-- Parsed declarations

src/Idris/Completion.hs+5−1

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

108108

109109completeOption :: CompletionFunc Idris

110110completeOption = 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+ ]

112116

113117completeConsoleWidth :: CompletionFunc Idris

114118completeConsoleWidth = completeWord Nothing " \t" completeW

src/Idris/Prover.hs+2−1

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

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

165165ploop fn d prompt prf e h

166166 = do i <- getIState

167+ let autoSolve = opt_autoSolve (idris_options i)

167168 when d $ dumpState i (proof e)

168169 (x, h') <-

169170 case idris_outputmode i of

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

260261 return (False, e, False, prf))

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

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

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

265266 iPrintResult ""

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

src/Idris/REPL.hs+2

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

932932process h fn (UnsetOpt ShowImpl) = setImpShow False

933933process h fn (SetOpt ShowOrigErr) = setShowOrigErr True

934934process h fn (UnsetOpt ShowOrigErr) = setShowOrigErr False

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

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

935937

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

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

src/Idris/REPLParser.hs+1

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

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

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

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

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

110111

111112pConsoleWidth :: P.IdrisParser ConsoleWidth

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