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

git.iko.soy/Idris-dev

Merge pull request #958 from david-christiansen/reflection-reflection

Proof automation improvements

commit2d79c852ad9aea1332ff7b4c1fdfd1486f20783f authorEdwin Brady <edwin.brady@gmail.com> dateSun 9 Mar 2014, 22:39 (13 years ago) parentf596a36 423b4c4

9 files changed+30−7

compare with master

unifiedsplit

CHANGELOG+6−4 libs/base/Language/Reflection.idr+2 src/Idris/AbsSyntax.hs+6 src/Idris/AbsSyntaxTree.hs+4−1 src/Idris/Completion.hs+5−1 src/Idris/ElabTerm.hs+2 src/Idris/Prover.hs+2−1 src/Idris/REPL.hs+2 src/Idris/REPLParser.hs+1

CHANGELOG+6−4

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

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

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

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

16−||| Add two natural numbers

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

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

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

16+ ||| Add two natural numbers

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

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

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".

2022

2123New in 0.9.11:

2224--------------

libs/base/Language/Reflection.idr+2

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

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

181181 | Reflect TT

182182 -- ^ turn a value into its reflected representation

183+ | ByReflection TT

184+ -- ^ use a %reflection function

183185 | Fill Raw

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

185187 | Exact TT

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/ElabTerm.hs+2

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

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

12061206reifyApp ist t [t']

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

1208+reifyApp ist t [t']

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

12081210reifyApp _ t [t']

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

12101212reifyApp ist t [t']

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