8e7216e · Idris-dev · git.iko.soy

CHANGELOG+11−4

compare with master

unifiedsplit

@@ -9,6 +9,9 @@ Language updates

9 for defining new names. `{n} still quotes n to an existing name in scope.

10* A new primitive operator prim__strSubstr for more efficient extraction of

11 substrings. External code generators should implement this.

12+* The previous syntax for tactic proofs and the previous interactive prover

13+ are now deprecated in favour of reflected elaboration. They will be removed

14+ at some point in the future.

12* Changed scoping rules for unbound implicits: any name which would be a

15* Changed scoping rules for unbound implicits: any name which would be a

13 valid unbound implicit is now *always* an unbound implicit. This is much

16 valid unbound implicit is now *always* an unbound implicit. This is much

14 more resilient to changes in inputs, but does require that function names

17 more resilient to changes in inputs, but does require that function names

@@ -18,13 +21,15 @@ Library updates

18---------------

21---------------

19

22

20* The 'Neg' class now represents numeric types which can be negative. As

23* The 'Neg' class now represents numeric types which can be negative. As

21−such, the (-) operator and 'abs' have been moved there from 'Num'.

24+ such, the (-) operator and 'abs' have been moved there from 'Num'.

22* A special version of (-) on 'Nat' requires that the second argument is

25* A special version of (-) on 'Nat' requires that the second argument is

23−smaller than or equal to the first. 'minus' retains the old behaviour,

26+ smaller than or equal to the first. 'minus' retains the old behaviour,

24−returning Z if there is an underflow.

27+ returning Z if there is an underflow.

25* The (+), (-), and (*) operations on Fin have been removed.

28* The (+), (-), and (*) operations on Fin have been removed.

26* New Logging Effects have been added to facilitate logging of effectful

29* New Logging Effects have been added to facilitate logging of effectful

27 programmes.

30 programmes.

31+* Elaborator reflection is now a part of the prelude. It is no longer

32+ necessary to import Language.Reflection.Elab.

28

33

29Tool updates

34Tool updates

30------------

35------------

@@ -33,8 +38,10 @@ Tool updates

33

38

34Miscellaneous updates

39Miscellaneous updates

35---------------------

40---------------------

41+* Disable the deprecation warnings for %elim and old-style tactic scripts

42+ with the --no-elim-deprecation-warnings and --no-tactic-deprecation-warnings

43+ flags.

36

44

37−[None so far]

38

45

39New in 0.9.19:

46New in 0.9.19:

40--------------

47--------------

docs/reference/elaborator-reflection.rst+9−7

@@ -11,11 +11,6 @@ For details, see Edwin Brady's 2013 paper in the Journal of Functional Programmi

11Elaborator reflection makes the elaboration type as well as a selection of its tactics available to Idris code.

12This means that metaprograms written in Idris can have complete control over the elaboration process, generating arbitrary code, and they have access to all of the facilities available in the elaborator, such as higher-order unification, type checking, and emitting auxiliary definitions.

13

14−WARNING

15−=======

16−

17−Elaborator reflection is a new, **experimental** feature. It **will change**. You've been warned.

18−

19The Elaborator State

14The Elaborator State

20====================

15====================

21

16

@@ -81,8 +76,15 @@ Interactively Building Elab Scripts

81

76

82To build an ``Elab`` script interactively, use the ``:elab`` command at the REPL.

77To build an ``Elab`` script interactively, use the ``:elab`` command at the REPL.

83It takes the name of a hole as an argument.

78It takes the name of a hole as an argument.

84−The interface is largely the same as in Idris's interactive prover, except all meta-commands start with colon.

79+To list all available holes, use the command ``:m``.

85−For example, use ``:qed`` instead of ``qed``, ``:abandon`` instead of ``abandon``, and ``:undo`` instead of ``undo``.

80+

81+In interactive elaboration shell, the following commands are available:

82+- ``:q`` - Quits the elaboration shell (gives up on proving current lemma).

83+- ``:abandon`` - Same as :q

84+- ``:state`` - Displays the current state of the term being constructed.

85+- ``:term`` - Displays the current proof term complete with its yet-to-be-filled holes.

86+- ``:undo`` - Undoes the last tactic.

87+- ``:qed`` - Once the elaboration shell tells you "No more goals," you get to type this in celebration! (Completes the construction and exits the shell)

86

88

87

89

88Failure

90Failure

docs/reference/tactics.rst+10−6

@@ -1,7 +1,11 @@

1***************************

2−Tactics and Theorem Proving

2+DEPRECATED: Tactics and Theorem Proving

3***************************

4

5+.. warning::

6+ The interactive theorem-proving interface documented here has been

7+ deprecated in favor of :ref:`elaborator-reflection`.

8+

5Idris supports interactive theorem proving, and the analyse of context

9Idris supports interactive theorem proving, and the analyse of context

6through holes. To list all unproven holes, use the command ``:m``.

10through holes. To list all unproven holes, use the command ``:m``.

7This will display their qualified names and the expected types. To

11This will display their qualified names and the expected types. To

@@ -15,12 +19,12 @@ Basic commands

15==============

19==============

16

20

17- ``:q`` - Quits the prover (gives up on proving current lemma).

21- ``:q`` - Quits the prover (gives up on proving current lemma).

18−- ``abandon`` - Same as :q

22+- ``:abandon`` - Same as :q

19−- ``state`` - Displays the current state of the proof.

23+- ``:state`` - Displays the current state of the proof.

20−- ``term`` - Displays the current proof term complete with its

24+- ``:term`` - Displays the current proof term complete with its

21 yet-to-be-filled holes (is only really useful for debugging).

25 yet-to-be-filled holes (is only really useful for debugging).

22−- ``undo`` - Undoes the last tactic.

26+- ``:undo`` - Undoes the last tactic.

23−- ``qed`` - Once the interactive theorem prover tells you "No more

27+- ``:qed`` - Once the interactive theorem prover tells you "No more

24 goals," you get to type this in celebration! (Completes the proof and

28 goals," you get to type this in celebration! (Completes the proof and

25 exits the prover)

29 exits the prover)

26

30

libs/base/Debug/Error.idr+1−1

@@ -8,7 +8,7 @@ import System

8||| @ loc The source location to display for the error

9||| @ message The error to print

10partial

11−error : {default tactics {sourceLocation} loc : SourceLocation} ->

11+error : {default (%runElab sourceLocation) loc : SourceLocation} ->

12 (message : String) ->

13 a

14error {loc = FileLoc filename (line, col) _} message =

libs/base/base.ipkg+1−1

@@ -1,6 +1,6 @@

1package base

2

3−opts = "--nobasepkgs --total -i ../prelude"

3+opts = "--nobasepkgs --total --no-elim-deprecation-warnings -i ../prelude"

4modules = System,

5

6 Debug.Error, Debug.Trace,

libs/contrib/Data/Heap.idr+10−19

@@ -133,21 +133,21 @@ instance Ord a => Monoid (MaxiphobicHeap a) where

133-- Properties

134--------------------------------------------------------------------------------

135

136+total

136−total absurdBoolDischarge : False = True -> Void

137+absurdBoolDischarge : False = True -> Void

137−absurdBoolDischarge p = replace {P = disjointTy} p ()

138+absurdBoolDischarge Refl impossible

138− where

139− total disjointTy : Bool -> Type

140− disjointTy False = ()

141− disjointTy True = Void

142

139

140+total

143−total isEmptySizeZero : (h : MaxiphobicHeap a) -> (isEmpty h = True) -> size h = Z

141+isEmptySizeZero : (h : MaxiphobicHeap a) -> (isEmpty h = True) -> size h = Z

144isEmptySizeZero Empty p = Refl

142isEmptySizeZero Empty p = Refl

145−isEmptySizeZero (Node s l e r) p = ?isEmptySizeZeroNodeAbsurd

143+isEmptySizeZero (Node s l e r) Refl impossible

146

144

145+total

147−total emptyHeapValid : Ord a => isValidHeap (empty {a}) = True

146+emptyHeapValid : Ord a => isValidHeap (empty {a}) = True

148emptyHeapValid = Refl

147emptyHeapValid = Refl

149

148

149+total

150−total singletonHeapValid : Ord a => (e : a) -> isValidHeap $ singleton e = True

150+singletonHeapValid : Ord a => (e : a) -> isValidHeap $ singleton e = True

151singletonHeapValid e = Refl

152

153{-

@@ -161,16 +161,7 @@ mergePreservesValidHeaps (Node ls ll le lr) (Node rs rl re rr) lp rp =

161 ?mergePreservesValidHeapsBody

162-}

163

164−--------------------------------------------------------------------------------

165−-- Proofs

166−--------------------------------------------------------------------------------

167

164

168−isEmptySizeZeroNodeAbsurd = proof {

169− intros;

170− refine void;

171− refine absurdBoolDischarge;

172− exact p;

173−}

174

165

175--------------------------------------------------------------------------------

166--------------------------------------------------------------------------------

176-- Debug

167-- Debug

libs/prelude/Language/Reflection/Elab.idr+17

@@ -139,6 +139,7 @@ data Elab : Type -> Type where

139 prim__Compute : Elab ()

140 prim__Normalise : (List (TTName, Binder TT)) -> TT -> Elab TT

141 prim__Whnf : TT -> Elab TT

142+ prim__Converts : (List (TTName, Binder TT)) -> TT -> TT -> Elab ()

142

143

143 prim__DeclareType : TyDecl -> Elab ()

144 prim__DeclareType : TyDecl -> Elab ()

144 prim__DefineFunction : FunDefn -> Elab ()

145 prim__DefineFunction : FunDefn -> Elab ()

@@ -373,6 +374,22 @@ namespace Tactics

373 whnf : (term : TT) -> Elab TT

374 whnf : (term : TT) -> Elab TT

374 whnf term = prim__Whnf term

375 whnf term = prim__Whnf term

375

376

377+ ||| Check that two terms are convertable in the current context and

378+ ||| in some environment.

379+ |||

380+ ||| @ env a lexical environment to compare the terms in (see `getEnv`)

381+ ||| @ term1 the first term to convert

382+ ||| @ term2 the second term to convert

383+ convertsInEnv : (env : List (TTName, Binder TT)) -> (term1, term2 : TT) -> Elab ()

384+ convertsInEnv env term1 term2 = prim__Converts env term1 term2

385+

386+ ||| Check that two terms are convertable in the current context and environment

387+ |||

388+ ||| @ term1 the first term to convert

389+ ||| @ term2 the second term to convert

390+ converts : (term1, term2 : TT) -> Elab ()

391+ converts term1 term2 = convertsInEnv !getEnv term1 term2

392+

376 ||| Find the source context for the elaboration script

393 ||| Find the source context for the elaboration script

377 getSourceLocation : Elab SourceLocation

394 getSourceLocation : Elab SourceLocation

378 getSourceLocation = prim__SourceLocation

395 getSourceLocation = prim__SourceLocation

libs/prelude/Prelude.idr+1

@@ -30,6 +30,7 @@ import public Prelude.File

30import public Prelude.Doubles

31import public Decidable.Equality

32import public Language.Reflection

33+import public Language.Reflection.Elab

33import public Language.Reflection.Errors

34import public Language.Reflection.Errors

34

35

35%access public

36%access public

libs/prelude/prelude.ipkg+1−1

@@ -1,6 +1,6 @@

1package prelude

2

3−opts = "--nobuiltins --total"

3+opts = "--nobuiltins --total --no-elim-deprecation-warnings"

4modules = Builtins, Prelude, IO,

5

6 Prelude.Algebra, Prelude.Basics, Prelude.Bool, Prelude.Cast,

src/Idris/AbsSyntaxTree.hs+3−1

@@ -506,10 +506,12 @@ data Opt = Filename String

506 | Client String

507 | ShowOrigErr

508 | AutoWidth -- ^ Automatically adjust terminal width

509− | AutoSolve -- ^ Automatically issue "solve" tactic in interactive prover

509+ | AutoSolve -- ^ Automatically issue "solve" tactic in old-style interactive prover

510 | UseConsoleWidth ConsoleWidth

511 | DumpHighlights

512 | DesugarNats

513+ | NoElimDeprecationWarnings -- ^ Don't show deprecation warnings for %elim

514+ | NoOldTacticDeprecationWarnings -- ^ Don't show deprecation warnings for old-style tactics

513 deriving (Show, Eq)

515 deriving (Show, Eq)

514

516

515data ElabShellCmd = EQED | EAbandon | EUndo | EProofState | EProofTerm

517data ElabShellCmd = EQED | EAbandon | EUndo | EProofState | EProofTerm

src/Idris/CmdOptions.hs+2

@@ -148,6 +148,8 @@ parseFlags = many $

148

149 <|> (UseConsoleWidth <$> option (str >>= parseConsoleWidth) (long "consolewidth" <> metavar "WIDTH" <> help "Select console width: auto, infinite, nat"))

150 <|> flag' DumpHighlights (long "highlight" <> help "Emit source code highlighting")

151+ <|> flag' NoElimDeprecationWarnings (long "no-elim-deprecation-warnings" <> help "Disable deprecation warnings for %elim")

152+ <|> flag' NoOldTacticDeprecationWarnings (long "no-tactic-deprecation-warnings" <> help "Disable deprecation warnings for the old tactic sublanguage")

151

153

152 where

154 where

153 getExt s = case maybeRead s of

155 getExt s = case maybeRead s of

src/Idris/Core/ProofState.hs+6−6

@@ -621,19 +621,19 @@ introTy ty n ctxt env _ = fail "Can't introduce here."

621

622intro :: Maybe Name -> RunTactic

623intro mn ctxt env (Bind x (Hole t) (P _ x' _)) | x == x' =

624− do let n = case mn of

625− Just name -> name

626− Nothing -> x

627− let t' = case t of

624+ do let t' = case t of

628 x@(Bind y (Pi _ s _) _) -> x

625 x@(Bind y (Pi _ s _) _) -> x

629 _ -> hnf ctxt env t

626 _ -> hnf ctxt env t

630 case t' of

627 case t' of

631 Bind y (Pi _ s _) t ->

628 Bind y (Pi _ s _) t ->

629+ let n = case mn of

630+ Just name -> name

631+ Nothing -> y

632 -- It's important that this be subst and not updsubst,

633 -- because we want to substitute even in portions of

634 -- terms that we know do not contain holes.

635− let t' = subst y (P Bound n s) t in

635+ t' = subst y (P Bound n s) t

636− return $ Bind n (Lam s) (Bind x (Hole t') (P Bound x t'))

636+ in return $ Bind n (Lam s) (Bind x (Hole t') (P Bound x t'))

637 _ -> lift $ tfail $ CantIntroduce t'

638intro n ctxt env _ = fail "Can't introduce here."

639

src/Idris/DeepSeq.hs+3−1

@@ -162,7 +162,9 @@ instance NFData Opt where

162 rnf (AutoWidth) = ()

163 rnf (AutoSolve) = ()

164 rnf (UseConsoleWidth cw) = rnf cw `seq` ()

165− rnf (DumpHighlights) = ()

165+ rnf DumpHighlights = ()

166+ rnf NoElimDeprecationWarnings = ()

167+ rnf NoOldTacticDeprecationWarnings = ()

166

168

167

169

168instance NFData TIData where

170instance NFData TIData where

src/Idris/Elab/Term.hs+7

@@ -1961,6 +1961,13 @@ runElabAction ist fc env tm ns = do tm' <- eval tm

1961 = do tm' <- reifyTT tm

1962 ctxt <- get_context

1963 fmap fst . checkClosed . reflect $ whnf ctxt tm'

1964+ | n == tacN "prim__Converts", [env, tm1, tm2] <- args

1965+ = do env' <- reifyEnv env

1966+ tm1' <- reifyTT tm1

1967+ tm2' <- reifyTT tm2

1968+ ctxt <- get_context

1969+ lift $ converts ctxt env' tm1' tm2'

1970+ returnUnit

1964 | n == tacN "prim__DeclareType", [decl] <- args

1971 | n == tacN "prim__DeclareType", [decl] <- args

1965 = do (RDeclare n args res) <- reifyTyDecl decl

1972 = do (RDeclare n args res) <- reifyTyDecl decl

1966 ctxt <- get_context

1973 ctxt <- get_context

src/Idris/ParseData.hs+12−2

@@ -157,11 +157,21 @@ DefaultEliminator ::= 'noelim'?

157 -}

158dataOpts :: DataOpts -> IdrisParser DataOpts

159dataOpts opts

160+ = do fc <- reservedFC "%elim"

161+ warnElim fc

160− = do reserved "%elim"; dataOpts (DefaultEliminator : DefaultCaseFun : opts)

162+ dataOpts (DefaultEliminator : DefaultCaseFun : opts)

163+ <|> do fc <- reservedFC "%case"

164+ warnElim fc

161− <|> do reserved "%case"; dataOpts (DefaultCaseFun : opts)

165+ dataOpts (DefaultCaseFun : opts)

162 <|> do reserved "%error_reverse"; dataOpts (DataErrRev : opts)

166 <|> do reserved "%error_reverse"; dataOpts (DataErrRev : opts)

163 <|> return opts

167 <|> return opts

164 <?> "data options"

168 <?> "data options"

169+ where warnElim fc =

170+ do ist <- get

171+ let cmdline = opt_cmdline (idris_options ist)

172+ unless (NoElimDeprecationWarnings `elem` cmdline) $

173+ put ist { parserWarnings =

174+ (fc, Msg "Eliminator generation is deprecated. Use an eliminator generator in a library instead.") : parserWarnings ist }

165

175

166{- | Parses a data type declaration

176{- | Parses a data type declaration

167Data ::= DocComment? Accessibility? DataI DefaultEliminator FnName TypeSig ExplicitTypeDataRest?

177Data ::= DocComment? Accessibility? DataI DefaultEliminator FnName TypeSig ExplicitTypeDataRest?

src/Idris/ParseExpr.hs+10

@@ -331,6 +331,14 @@ caseOption syn = do lhs <- expr (syn { inPattern = True })

331 return (lhs, r)

332 <?> "case option"

333

334+warnTacticDeprecation :: FC -> IdrisParser ()

335+warnTacticDeprecation fc =

336+ do ist <- get

337+ let cmdline = opt_cmdline (idris_options ist)

338+ unless (NoOldTacticDeprecationWarnings `elem` cmdline) $

339+ put ist { parserWarnings =

340+ (fc, Msg "This style of tactic proof is deprecated. See %runElab for the replacement.") : parserWarnings ist }

341+

334{- | Parses a proof block

342{- | Parses a proof block

335@

343@

336ProofExpr ::=

344ProofExpr ::=

@@ -342,6 +350,7 @@ proofExpr :: SyntaxInfo -> IdrisParser PTerm

342proofExpr syn = do kw <- reservedFC "proof"

350proofExpr syn = do kw <- reservedFC "proof"

343 ts <- indentedBlock1 (tactic syn)

351 ts <- indentedBlock1 (tactic syn)

344 highlightP kw AnnKeyword

352 highlightP kw AnnKeyword

353+ warnTacticDeprecation kw

345 return $ PProof ts

354 return $ PProof ts

346 <?> "proof block"

355 <?> "proof block"

347

356

@@ -356,6 +365,7 @@ tacticsExpr :: SyntaxInfo -> IdrisParser PTerm

356tacticsExpr syn = do kw <- reservedFC "tactics"

365tacticsExpr syn = do kw <- reservedFC "tactics"

357 ts <- indentedBlock1 (tactic syn)

366 ts <- indentedBlock1 (tactic syn)

358 highlightP kw AnnKeyword

367 highlightP kw AnnKeyword

368+ warnTacticDeprecation kw

359 return $ PTactics ts

369 return $ PTactics ts

360 <?> "tactics block"

370 <?> "tactics block"

361

371

src/Idris/ParseHelpers.hs+2−1

@@ -100,7 +100,8 @@ reportParserWarnings = do ist <- getIState

100 mapM_ (uncurry iWarn)

101 (map (\ (fc, err) -> (fc, pprintErr ist err)) .

102 reverse .

103− nub $

103+ nubBy (\(fc, err) (fc', err') ->

104+ FC' fc == FC' fc' && err == err') $

104 parserWarnings ist)

105 parserWarnings ist)

105 clearParserWarnings

106 clearParserWarnings

106

107

src/Idris/Prover.hs+24−20

@@ -1,3 +1,4 @@

1+

1{-# LANGUAGE PatternGuards #-}

2{-# LANGUAGE PatternGuards #-}

2module Idris.Prover (prover, showProof, showRunElab) where

3module Idris.Prover (prover, showProof, showRunElab) where

3

4

@@ -5,7 +6,7 @@ module Idris.Prover (prover, showProof, showRunElab) where

5-- This exludes (<$>) as fmap, because wl-pprint uses it for newline

6-- This exludes (<$>) as fmap, because wl-pprint uses it for newline

6import Prelude (Eq(..), Show(..),

7import Prelude (Eq(..), Show(..),

7 Bool(..), Either(..), Maybe(..), String,

8 Bool(..), Either(..), Maybe(..), String,

8− (.), ($), (++), (||),

9+ (.), ($), (++), (||), (&&),

9 concatMap, id, elem, error, fst, flip, foldl, foldr, init,

10 concatMap, id, elem, error, fst, flip, foldl, foldr, init,

10 length, lines, map, not, null, repeat, reverse, tail, zip)

11 length, lines, map, not, null, repeat, reverse, tail, zip)

11

12

@@ -89,7 +90,10 @@ prove mode opt ctxt lit n ty

89 (tm, prf) <-

90 (tm, prf) <-

90 if mode

91 if mode

91 then elabloop n True ("-" ++ show n) [] (ES (ps, initEState) "" Nothing) [] Nothing []

92 then elabloop n True ("-" ++ show n) [] (ES (ps, initEState) "" Nothing) [] Nothing []

93+ else do iputStrLn $ "Warning: this interactive prover is deprecated and will be removed " ++

94+ "in a future release. Please see :elab for a similar feature that "++

95+ "will replace it."

92− else ploop n True ("-" ++ show n) [] (ES (ps, initEState) "" Nothing) Nothing

96+ ploop n True ("-" ++ show n) [] (ES (ps, initEState) "" Nothing) Nothing

93 logLvl 1 $ "Adding " ++ show tm

97 logLvl 1 $ "Adding " ++ show tm

94 i <- getIState

98 i <- getIState

95 let shower = if mode

99 let shower = if mode

@@ -145,16 +149,16 @@ elabStep st e =

145 return (res, ctxt)

149 return (res, ctxt)

146 ((_,_,_,_,e,_,_):_) -> lift $ Error e

150 ((_,_,_,_,e,_,_):_) -> lift $ Error e

147

151

148−dumpState :: IState -> [(Name, Type, Term)] -> ProofState -> Idris ()

152+dumpState :: IState -> Bool -> [(Name, Type, Term)] -> ProofState -> Idris ()

149−dumpState ist menv ps | [] <- holes ps =

153+dumpState ist inElab menv ps | [] <- holes ps =

150 do let nm = thname ps

154 do let nm = thname ps

151 rendered <- iRender $ prettyName True False [] nm <> colon <+> text "No more goals."

155 rendered <- iRender $ prettyName True False [] nm <> colon <+> text "No more goals."

152 iputGoal rendered

156 iputGoal rendered

153−dumpState ist menv ps | (h : hs) <- holes ps = do

157+dumpState ist inElab menv ps | (h : hs) <- holes ps = do

154 let OK ty = goalAtFocus ps

158 let OK ty = goalAtFocus ps

155 let OK env = envAtFocus ps

159 let OK env = envAtFocus ps

156 let state = prettyOtherGoals hs <> line <>

160 let state = prettyOtherGoals hs <> line <>

157− prettyAssumptions ty env <> line <>

161+ prettyAssumptions inElab ty env <> line <>

158 prettyMetaValues (reverse menv) <>

162 prettyMetaValues (reverse menv) <>

159 prettyGoal (zip (assumptionNames env) (repeat False)) ty

163 prettyGoal (zip (assumptionNames env) (repeat False)) ty

160 rendered <- iRender state

164 rendered <- iRender state

@@ -172,18 +176,18 @@ dumpState ist menv ps | (h : hs) <- holes ps = do

172 assumptionNames :: Env -> [Name]

176 assumptionNames :: Env -> [Name]

173 assumptionNames = map fst

177 assumptionNames = map fst

174

178

175− prettyPs :: Binder Type -> [(Name, Bool)] -> Env -> Doc OutputAnnotation

179+ prettyPs :: Bool -> Binder Type -> [(Name, Bool)] -> Env -> Doc OutputAnnotation

176− prettyPs g bnd [] = empty

180+ prettyPs all g bnd [] = empty

177− prettyPs g bnd ((n@(MN _ r), _) : bs)

181+ prettyPs all g bnd ((n@(MN _ r), _) : bs)

178− | r == txt "rewrite_rule" = prettyPs g ((n, False):bnd) bs

182+ | not all && r == txt "rewrite_rule" = prettyPs all g ((n, False):bnd) bs

179− prettyPs g bnd ((n@(MN _ _), _) : bs)

183+ prettyPs all g bnd ((n@(MN _ _), _) : bs)

180− | not (n `elem` freeEnvNames bs || n `elem` goalNames g) = prettyPs g bnd bs

184+ | not (all || n `elem` freeEnvNames bs || n `elem` goalNames g) = prettyPs all g bnd bs

181− prettyPs g bnd ((n, Let t v) : bs) =

185+ prettyPs all g bnd ((n, Let t v) : bs) =

182 line <> bindingOf n False <+> text "=" <+> tPretty bnd v <+> colon <+>

186 line <> bindingOf n False <+> text "=" <+> tPretty bnd v <+> colon <+>

183− align (tPretty bnd t) <> prettyPs g ((n, False):bnd) bs

187+ align (tPretty bnd t) <> prettyPs all g ((n, False):bnd) bs

184− prettyPs g bnd ((n, b) : bs) =

188+ prettyPs all g bnd ((n, b) : bs) =

185 line <> bindingOf n False <+> colon <+>

189 line <> bindingOf n False <+> colon <+>

186− align (tPretty bnd (binderTy b)) <> prettyPs g ((n, False):bnd) bs

190+ align (tPretty bnd (binderTy b)) <> prettyPs all g ((n, False):bnd) bs

187

191

188 prettyMetaValues [] = empty

192 prettyMetaValues [] = empty

189 prettyMetaValues mvs =

193 prettyMetaValues mvs =

@@ -210,12 +214,12 @@ dumpState ist menv ps | (h : hs) <- holes ps = do

210 text "---------- Goal: ----------" <$$>

214 text "---------- Goal: ----------" <$$>

211 bindingOf h False <+> colon <+> align (prettyG bnd ty)

215 bindingOf h False <+> colon <+> align (prettyG bnd ty)

212

216

213− prettyAssumptions g env =

217+ prettyAssumptions inElab g env =

214 if length env == 0 then

218 if length env == 0 then

215 empty

219 empty

216 else

220 else

217 text "---------- Assumptions: ----------" <>

221 text "---------- Assumptions: ----------" <>

218− nest nestingSize (prettyPs g [] $ reverse env)

222+ nest nestingSize (prettyPs inElab g [] $ reverse env)

219

223

220 prettyOtherGoals hs =

224 prettyOtherGoals hs =

221 if length hs == 0 then

225 if length hs == 0 then

@@ -273,7 +277,7 @@ undoElab prf env st (h:hs) = do (prf', env', st') <- undoStep prf env st h

273elabloop :: Name -> Bool -> String -> [String] -> ElabState EState -> [ElabShellHistory] -> Maybe History -> [(Name, Type, Term)] -> Idris (Term, [String])

277elabloop :: Name -> Bool -> String -> [String] -> ElabState EState -> [ElabShellHistory] -> Maybe History -> [(Name, Type, Term)] -> Idris (Term, [String])

274elabloop fn d prompt prf e prev h env

278elabloop fn d prompt prf e prev h env

275 = do ist <- getIState

279 = do ist <- getIState

276− when d $ dumpState ist env (proof e)

280+ when d $ dumpState ist True env (proof e)

277 (x, h') <-

281 (x, h') <-

278 case idris_outputmode ist of

282 case idris_outputmode ist of

279 RawOutput _ ->

283 RawOutput _ ->

@@ -390,7 +394,7 @@ ploop :: Name -> Bool -> String -> [String] -> ElabState EState -> Maybe History

390ploop fn d prompt prf e h

394ploop fn d prompt prf e h

391 = do i <- getIState

395 = do i <- getIState

392 let autoSolve = opt_autoSolve (idris_options i)

396 let autoSolve = opt_autoSolve (idris_options i)

393− when d $ dumpState i [] (proof e)

397+ when d $ dumpState i False [] (proof e)

394 (x, h') <-

398 (x, h') <-

395 case idris_outputmode i of

399 case idris_outputmode i of

396 RawOutput _ ->

400 RawOutput _ ->

test/basic002/expected+4

@@ -1 +1,5 @@

1+test006.idr:25:23-28:

2+This style of tactic proof is deprecated. See %runElab for the replacement.

3+test006.idr:32:23-28:

4+This style of tactic proof is deprecated. See %runElab for the replacement.

1[False, True, False, True, False, True]

5[False, True, False, True, False, True]

test/basic002/run+1−1

@@ -1,4 +1,4 @@

1#!/usr/bin/env bash

2−idris $@ test006.idr -o test006

2+idris $@ --nocolour --consolewidth 80 test006.idr -o test006

3./test006

4rm -f test006 test006.ibc

test/docs003/expected+1

@@ -15,6 +15,7 @@ Instances:

15 Functor Stream

16 Functor Provider

17 Functor Binder

18+ Functor Elab

18 Functor PrimIO

19 Functor PrimIO

19 Functor Maybe

20 Functor Maybe

20 Functor (Either e)

21 Functor (Either e)

test/effects003/expected+2

@@ -1,3 +1,5 @@

1+hangman.idr:204:8-13:

2+This style of tactic proof is deprecated. See %runElab for the replacement.

1------------

3------------

2

4

36 guesses left

56 guesses left

test/effects003/hangman.idr+4

@@ -223,3 +223,7 @@ were caught by the type checker:

223

224main : IO ()

225main = run runGame

226+

227+-- Local Variables:

228+-- idris-load-packages: ("effects")

229+-- End:

test/effects003/run+1−1

@@ -1,4 +1,4 @@

1#!/usr/bin/env bash

2−idris $@ hangman.idr -p effects -o hangman

2+idris $@ hangman.idr --consolewidth 80 --nocolour -p effects -o hangman

3./hangman < input

4rm -f hangman *.ibc

test/proof001/expected+4

@@ -0,0 +1,4 @@

1+test029.idr:29:25-30:

2+This style of tactic proof is deprecated. See %runElab for the replacement.

3+test029.idr:36:25-30:

4+This style of tactic proof is deprecated. See %runElab for the replacement.

test/proof001/run+1−1

@@ -1,3 +1,3 @@

1#!/usr/bin/env bash

2−idris $@ test029.idr --check test029

2+idris $@ test029.idr --consolewidth 80 --nocolour --check test029

3rm -f *.ibc

test/proof002/expected+6

@@ -1,3 +1,9 @@

1+Reflect.idr:173:21-26:

2+This style of tactic proof is deprecated. See %runElab for the replacement.

3+Reflect.idr:182:21-26:

4+This style of tactic proof is deprecated. See %runElab for the replacement.

5+Reflect.idr:190:15-20:

6+This style of tactic proof is deprecated. See %runElab for the replacement.

1test030a.idr:12:26-14:1:

7test030a.idr:12:26-14:1:

2When checking right hand side of testReflect1:

8When checking right hand side of testReflect1:

3When checking an application of function Reflect.getJust:

9When checking an application of function Reflect.getJust:

test/proof003/expected+12

@@ -1,3 +1,15 @@

1+Parity.idr:15:18-23:

2+This style of tactic proof is deprecated. See %runElab for the replacement.

3+Parity.idr:22:18-23:

4+This style of tactic proof is deprecated. See %runElab for the replacement.

5+test015.idr:88:15-20:

6+This style of tactic proof is deprecated. See %runElab for the replacement.

7+test015.idr:97:16-21:

8+This style of tactic proof is deprecated. See %runElab for the replacement.

9+test015.idr:108:20-25:

10+This style of tactic proof is deprecated. See %runElab for the replacement.

11+test015.idr:136:20-25:

12+This style of tactic proof is deprecated. See %runElab for the replacement.

100101010

1300101010

201011001

1401011001

3010000011

15010000011

test/proof003/run+1−1

@@ -1,4 +1,4 @@

1#!/usr/bin/env bash

2−idris $@ test015.idr -o test015

2+idris $@ test015.idr --nocolour --consolewidth 80 -o test015

3./test015

4rm -f test015 Parity.ibc test015.ibc

test/proof008/expected+2

@@ -0,0 +1,2 @@

1+ClaimAndUnfocus.idr:8:27-32:

2+This style of tactic proof is deprecated. See %runElab for the replacement.

test/proof008/run+1−1

@@ -1,3 +1,3 @@

1#!/usr/bin/env bash

2−idris --check $@ ClaimAndUnfocus.idr

2+idris --nocolour --consolewidth 80 --check $@ ClaimAndUnfocus.idr

3rm -f *.ibc

test/proof009/expected+1

@@ -1,3 +1,4 @@

1+Warning: this interactive prover is deprecated and will be removed in a future release. Please see :elab for a similar feature that will replace it.

1

2

3

3---------- Goal: ----------

4---------- Goal: ----------

test/quasiquote004/expected+6

@@ -1,3 +1,9 @@

1+Quasiquote004.idr:39:26-31:

2+This style of tactic proof is deprecated. See %runElab for the replacement.

3+Quasiquote004.idr:42:28-33:

4+This style of tactic proof is deprecated. See %runElab for the replacement.

5+Quasiquote004.idr:50:27-32:

6+This style of tactic proof is deprecated. See %runElab for the replacement.

1Quasiquote004.idr:50:25:

7Quasiquote004.idr:50:25:

2When checking right hand side of Quasiquote004.getMeNat':

8When checking right hand side of Quasiquote004.getMeNat':

3Not a Nat goal

9Not a Nat goal

test/reg017/expected+4

@@ -1 +1,5 @@

1+reg017.idr:5:17-24:

2+This style of tactic proof is deprecated. See %runElab for the replacement.

3+reg017.idr:8:17-24:

4+This style of tactic proof is deprecated. See %runElab for the replacement.

14

54

test/reg017/run+1−1

@@ -1,4 +1,4 @@

1#!/usr/bin/env bash

2−idris $@ reg017.idr -o reg017

2+idris $@ --nocolour --consolewidth 80 reg017.idr -o reg017

3./reg017

4rm -f reg017 *.ibc

test/reg028/expected+2

@@ -1,4 +1,6 @@

1reg028.idr:5:1:

2tbad.bad is possibly not total due to: with block in tbad.bad

3+reg028a.idr:17:14-19:

4+This style of tactic proof is deprecated. See %runElab for the replacement.

3reg028a.idr:11:1:

5reg028a.idr:11:1:

4tbad.qsort' is possibly not total due to: with block in tbad.qsort'

6tbad.qsort' is possibly not total due to: with block in tbad.qsort'

test/reg044/expected+2

@@ -1,3 +1,5 @@

1+reg044.idr:4:6-11:

2+This style of tactic proof is deprecated. See %runElab for the replacement.

1reg044.idr:4:4:When checking right hand side of Main.pf:

3reg044.idr:4:4:When checking right hand side of Main.pf:

2Type mismatch between

4Type mismatch between

3 b = b (Type of Refl)

5 b = b (Type of Refl)

test/sourceLocation001/expected+8

@@ -1,3 +1,11 @@

1+SourceLoc.idr:11:19-26:

2+This style of tactic proof is deprecated. See %runElab for the replacement.

3+SourceLoc.idr:20:19-24:

4+This style of tactic proof is deprecated. See %runElab for the replacement.

5+SourceLoc.idr:40:20-27:

6+This style of tactic proof is deprecated. See %runElab for the replacement.

7+SourceLoc.idr:98:18-23:

8+This style of tactic proof is deprecated. See %runElab for the replacement.

1Testing using definition

9Testing using definition

2FileLoc "SourceLoc.idr" (16, 11) (16, 17)

10FileLoc "SourceLoc.idr" (16, 11) (16, 17)

3Testing using inline tactics

11Testing using inline tactics

test/sourceLocation001/run+1−1

@@ -1,4 +1,4 @@

1#!/usr/bin/env bash

2−idris $@ SourceLoc.idr -o sourceLocation001

2+idris $@ --nocolour --consolewidth 80 SourceLoc.idr -o sourceLocation001

3./sourceLocation001

4rm -f sourceLocation001 *.ibc

test/totality002/expected+2

@@ -1,3 +1,5 @@

1+test017.idr:94:26-31:

2+This style of tactic proof is deprecated. See %runElab for the replacement.

1test017a.idr:7:1:

3test017a.idr:7:1:

2scg.vtrans is possibly not total due to recursive path scg.vtrans --> scg.vtrans

4scg.vtrans is possibly not total due to recursive path scg.vtrans --> scg.vtrans

3test017b.idr:4:1:

5test017b.idr:4:1:

test/totality003/run+2−2

@@ -1,4 +1,4 @@

1#!/usr/bin/env bash

2−idris --consolewidth 80 $@ totality003.idr --check

2+idris --nocolour --consolewidth 80 $@ totality003.idr --check

3−idris --consolewidth 80 $@ totality003a.idr --check

3+idris --nocolour --consolewidth 80 $@ totality003a.idr --check

4rm -f *.ibc

test/tutorial002/expected+6

@@ -0,0 +1,6 @@

1+tutorial002.idr:41:25-30:

2+This style of tactic proof is deprecated. See %runElab for the replacement.

3+tutorial002.idr:48:18-23:

4+This style of tactic proof is deprecated. See %runElab for the replacement.

5+tutorial002.idr:54:18-23:

6+This style of tactic proof is deprecated. See %runElab for the replacement.

test/tutorial002/run+1−1

@@ -1,3 +1,3 @@

1#!/usr/bin/env bash

2−idris $@ tutorial002.idr --check

2+idris $@ --nocolour --consolewidth 80 tutorial002.idr --check

3rm -f *.ibc

test/tutorial004/expected+4

@@ -0,0 +1,4 @@

1+tutorial004.idr:46:14-19:

2+This style of tactic proof is deprecated. See %runElab for the replacement.

3+tutorial004.idr:53:14-19:

4+This style of tactic proof is deprecated. See %runElab for the replacement.

test/tutorial004/run+1−1

@@ -1,3 +1,3 @@

1#!/usr/bin/env bash

2−idris $@ tutorial004.idr --check

2+idris $@ tutorial004.idr --check --nocolour --consolewidth 80

3rm -f *.ibc