5f3e853 · Idris-dev · git.iko.soy

git.iko.soy/Idris-dev

on master help sign in

Merge branch 'master' of github.com:idris-lang/Idris-dev

5f3e853Edwin Brady12 years ago

.gitignore+2

compare with master

unifiedsplit

@@ -14,6 +14,8 @@ cabal.sandbox.config

14.DS_Store

15.hpc

16*.tix

17+.projectile

18+.dir-locals.el

17custom.mk

19custom.mk

18libs/base/base_doc/

20libs/base/base_doc/

19libs/effects/effects_doc/

21libs/effects/effects_doc/

CHANGELOG+3

@@ -2,6 +2,9 @@ New in 0.9.17:

2--------------

3* The --ideslave command line option has been replaced with a --ide-mode

4 command line option with the same semantics.

5+* A new tactic "claim N TY" that introduces a new hole named N with type TY

6+* A new tactic "unfocus" that moves the current hole to the bottom of the

7+ hole stack

6New in 0.9.16:

9New in 0.9.16:

7--------------

10--------------

Setup.hs+1−1

@@ -106,7 +106,7 @@ generateVersionModule verbosity dir release = do

106 "gitHash :: String\n" ++

107 if release

108 then "gitHash = \"\"\n"

109− else "gitHash = \"-git:" ++ h ++ "\"\n"

109+ else "gitHash = \"git:" ++ h ++ "\"\n"

110

111-- Generate a module that contains the lib path for a freestanding Idris

112generateTargetModule verbosity dir targetDir = do

idris.cabal+3

@@ -497,6 +497,9 @@ Extra-source-files:

497 test/proof004/run

498 test/proof004/*.idr

499 test/proof004/expected

500+ test/proof008/run

501+ test/proof008/*.idr

502+ test/proof008/expected

500

503

501 test/quasiquote001/run

504 test/quasiquote001/run

502 test/quasiquote001/*.idr

505 test/quasiquote001/*.idr

libs/prelude/Language/Reflection.idr+7

@@ -213,6 +213,10 @@ data Tactic =

213 Refine TTName |

214 ||| Apply both tactics in sequence

215 Seq Tactic Tactic |

216+ ||| Introduce a new hole with a particular type

217+ Claim TTName TT |

218+ ||| Move the current hole to the end

219+ Unfocus |

216 ||| Intelligently construct the proof target from the context

220 ||| Intelligently construct the proof target from the context

217 Trivial |

221 Trivial |

218 ||| Build a proof by applying contructors up to a maximum depth

222 ||| Build a proof by applying contructors up to a maximum depth

@@ -472,6 +476,8 @@ instance Quotable Tactic where

472 quote (Try tac tac') = `(Try ~(quote tac) ~(quote tac'))

476 quote (Try tac tac') = `(Try ~(quote tac) ~(quote tac'))

473 quote (GoalType x tac) = `(GoalType ~(quote x) ~(quote tac))

477 quote (GoalType x tac) = `(GoalType ~(quote x) ~(quote tac))

474 quote (Refine n) = `(Refine ~(quote n))

478 quote (Refine n) = `(Refine ~(quote n))

479+ quote (Claim n ty) = `(Claim ~(quote n) ~(quote ty))

480+ quote Unfocus = `(Unfocus)

475 quote (Seq tac tac') = `(Seq ~(quote tac) ~(quote tac'))

481 quote (Seq tac tac') = `(Seq ~(quote tac) ~(quote tac'))

476 quote Trivial = `(Trivial)

482 quote Trivial = `(Trivial)

477 quote (Search x) = `(Search ~(quote x))

483 quote (Search x) = `(Search ~(quote x))

@@ -494,3 +500,4 @@ instance Quotable Tactic where

494 quote Skip = `(Skip)

500 quote Skip = `(Skip)

495 quote (Fail xs) = `(Fail ~(quote xs))

501 quote (Fail xs) = `(Fail ~(quote xs))

496 quote SourceFC = `(SourceFC)

502 quote SourceFC = `(SourceFC)

503+

libs/prelude/Prelude/Strings.idr+88−59

@@ -17,8 +17,9 @@ import Decidable.Equality

18||| Appends two strings together.

19|||

20+||| ```idris example

20−||| Idris> "AB" ++ "C"

21+||| "AB" ++ "C"

21−||| "ABC" : String

22+||| ```

22(++) : String -> String -> String

23(++) : String -> String -> String

23(++) = prim__concat

24(++) = prim__concat

@@ -26,8 +27,9 @@ import Decidable.Equality

26|||

27|||

27||| Doesn't work for empty strings.

28||| Doesn't work for empty strings.

28|||

29|||

30+||| ```idris example

29−||| Idris> strHead "A"

31+||| strHead "A"

30−||| 'A' : Char

32+||| ```

31partial

33partial

32strHead : String -> Char

34strHead : String -> Char

33strHead = prim__strHead

35strHead = prim__strHead

@@ -36,20 +38,24 @@ strHead = prim__strHead

36|||

38|||

37||| Doesn't work for empty strings.

39||| Doesn't work for empty strings.

38|||

40|||

41+||| ```idris example

39−||| Idris> strTail "AB"

42+||| strTail "AB"

40−||| "B" : String

43+||| ```

44+||| ```idris example

41−||| Idris> strTail "A"

45+||| strTail "A"

42−||| "" : String

46+||| ```

43partial

47partial

44strTail : String -> String

48strTail : String -> String

45strTail = prim__strTail

49strTail = prim__strTail

47||| Adds a character to the front of the specified string.

51||| Adds a character to the front of the specified string.

48|||

52|||

53+||| ```idris example

49−||| Idris> strCons 'A' "B"

54+||| strCons 'A' "B"

50−||| "AB" : String

55+||| ```

56+||| ```idris example

51−||| Idris> strCons 'A' ""

57+||| strCons 'A' ""

52−||| "A" : String

58+||| ```

53strCons : Char -> String -> String

59strCons : Char -> String -> String

54strCons = prim__strCons

60strCons = prim__strCons

@@ -57,18 +63,21 @@ strCons = prim__strCons

57|||

63|||

58||| Precondition: '0 < i < length s' for 'strIndex s i'.

64||| Precondition: '0 < i < length s' for 'strIndex s i'.

59|||

65|||

66+||| ```idris example

60−||| Idris> strIndex "AB" 1

67+||| strIndex "AB" 1

61−||| 'B' : Char

68+||| ```

62partial

69partial

63strIndex : String -> Int -> Char

70strIndex : String -> Int -> Char

64strIndex = prim__strIndex

71strIndex = prim__strIndex

66||| Reverses the elements within a String.

73||| Reverses the elements within a String.

67|||

74|||

75+||| ```idris example

68−||| Idris> reverse "ABC"

76+||| reverse "ABC"

69−||| "CBA" : String

77+||| ```

78+||| ```idris example

70−||| Idris> reverse ""

79+||| reverse ""

71−||| "" : String

80+||| ```

72reverse : String -> String

81reverse : String -> String

73reverse = prim__strRev

82reverse = prim__strRev

@@ -103,8 +112,9 @@ strM x with (decEq (not (x == "")) True)

103

112

104||| Turns a string into a list of characters.

113||| Turns a string into a list of characters.

105|||

114|||

115+||| ```idris example

106−||| Idris> unpack "ABC"

116+||| unpack "ABC"

107−||| ['A', 'B', 'C'] : List Char

117+||| ```

108unpack : String -> List Char

118unpack : String -> List Char

109unpack s with (strM s)

119unpack s with (strM s)

110 unpack "" | StrNil = []

120 unpack "" | StrNil = []

@@ -116,8 +126,9 @@ pack = foldr strCons ""

116

126

117||| Creates a string of a single character.

127||| Creates a string of a single character.

118|||

128|||

129+||| ```idris example

119−||| Idris> singleton 'A'

130+||| singleton 'A'

120−||| "A" : String

131+||| ```

121singleton : Char -> String

132singleton : Char -> String

122singleton c = strCons c ""

133singleton c = strCons c ""

123

134

@@ -139,10 +150,12 @@ instance Monoid String where

139||| Splits the string into a part before the predicate

150||| Splits the string into a part before the predicate

140||| returns False and the rest of the string.

151||| returns False and the rest of the string.

141|||

152|||

153+||| ```idris example

142−||| Idris> span (/= 'C') "ABCD"

154+||| span (/= 'C') "ABCD"

143−||| ("AB", "CD") : (String, String)

155+||| ```

156+||| ```idris example

144−||| Idris> span (/= 'C') "EFGH"

157+||| span (/= 'C') "EFGH"

145−||| ("EFGH", "") : (String, String)

158+||| ```

146span : (Char -> Bool) -> String -> (String, String)

159span : (Char -> Bool) -> String -> (String, String)

147span p xs with (strM xs)

160span p xs with (strM xs)

148 span p "" | StrNil = ("", "")

161 span p "" | StrNil = ("", "")

@@ -154,28 +167,33 @@ span p xs with (strM xs)

154||| Splits the string into a part before the predicate

167||| Splits the string into a part before the predicate

155||| returns True and the rest of the string.

168||| returns True and the rest of the string.

156|||

169|||

170+||| ```idris example

157−||| Idris> break (== 'C') "ABCD"

171+||| break (== 'C') "ABCD"

158−||| ("AB", "CD") : (String, String)

172+||| ```

173+||| ```idris example

159−||| Idris> break (== 'C') "EFGH"

174+||| break (== 'C') "EFGH"

160−||| ("EFGH", "") : (String, String)

175+||| ```

161break : (Char -> Bool) -> String -> (String, String)

176break : (Char -> Bool) -> String -> (String, String)

162break p = span (not . p)

177break p = span (not . p)

163

178

164||| Splits the string into parts with the predicate

179||| Splits the string into parts with the predicate

165||| indicating separator characters.

180||| indicating separator characters.

166|||

181|||

182+||| ```idris example

167−||| Idris> split (== '.') ".AB.C..D"

183+||| split (== '.') ".AB.C..D"

168−||| ["", "AB", "C", "", "D"] : List String

184+||| ```

169split : (Char -> Bool) -> String -> List String

185split : (Char -> Bool) -> String -> List String

170split p xs = map pack (split p (unpack xs))

186split p xs = map pack (split p (unpack xs))

171

187

172||| Removes whitespace (determined with 'isSpace') from

188||| Removes whitespace (determined with 'isSpace') from

173||| the start of the string.

189||| the start of the string.

174|||

190|||

191+||| ```idris example

175−||| Idris> ltrim " A\nB"

192+||| ltrim " A\nB"

176−||| "A\nB" : String

193+||| ```

194+||| ```idris example

177−||| Idris> ltrim " \nAB"

195+||| ltrim " \nAB"

178−||| "AB" : String

196+||| ```

179ltrim : String -> String

197ltrim : String -> String

180ltrim xs with (strM xs)

198ltrim xs with (strM xs)

181 ltrim "" | StrNil = ""

199 ltrim "" | StrNil = ""

@@ -185,15 +203,17 @@ ltrim xs with (strM xs)

185||| Removes whitespace (determined with 'isSpace') from

203||| Removes whitespace (determined with 'isSpace') from

186||| the start and end of the string.

204||| the start and end of the string.

187|||

205|||

206+||| ```idris example

188−||| Idris> trim " A\nB C "

207+||| trim " A\nB C "

189−||| "A\nB C" : String

208+||| ```

190trim : String -> String

209trim : String -> String

191trim xs = ltrim (reverse (ltrim (reverse xs)))

210trim xs = ltrim (reverse (ltrim (reverse xs)))

192

211

193||| Splits a character list into a list of whitespace separated character lists.

212||| Splits a character list into a list of whitespace separated character lists.

194|||

213|||

214+||| ```idris example

195−||| Idris> words' (unpack " A B C D E ")

215+||| words' (unpack " A B C D E ")

196−||| [['A'], ['B'], ['C'], ['D'], ['E']] : List (List Char)

216+||| ```

197words' : List Char -> List (List Char)

217words' : List Char -> List (List Char)

198words' s = case dropWhile isSpace s of

218words' s = case dropWhile isSpace s of

199 [] => []

219 [] => []

@@ -202,15 +222,17 @@ words' s = case dropWhile isSpace s of

202

222

203||| Splits a string into a list of whitespace separated strings.

223||| Splits a string into a list of whitespace separated strings.

204|||

224|||

225+||| ```idris example

205−||| Idris> words " A B C D E "

226+||| words " A B C D E "

206−||| ["A", "B", "C", "D", "E"] : List String

227+||| ```

207words : String -> List String

228words : String -> List String

208words s = map pack $ words' $ unpack s

229words s = map pack $ words' $ unpack s

209

230

210||| Splits a character list into a list of newline separated character lists.

231||| Splits a character list into a list of newline separated character lists.

211|||

232|||

233+||| ```idris example

212−||| Idris> lines' (unpack "\rA BC\nD\r\nE\n")

234+||| lines' (unpack "\rA BC\nD\r\nE\n")

213−||| [['A', ' ', 'B', 'C'], ['D'], ['E']] : List (List Char)

235+||| ```

214lines' : List Char -> List (List Char)

236lines' : List Char -> List (List Char)

215lines' s = case dropWhile isNL s of

237lines' s = case dropWhile isNL s of

216 [] => []

238 [] => []

@@ -219,8 +241,9 @@ lines' s = case dropWhile isNL s of

219

241

220||| Splits a string into a list of newline separated strings.

242||| Splits a string into a list of newline separated strings.

221|||

243|||

244+||| ```idris example

222−||| Idris> lines "\rA BC\nD\r\nE\n"

245+||| lines "\rA BC\nD\r\nE\n"

223−||| ["A BC", "D", "E"] : List String

246+||| ```

224lines : String -> List String

247lines : String -> List String

225lines s = map pack $ lines' $ unpack s

248lines s = map pack $ lines' $ unpack s

226

249

@@ -235,8 +258,9 @@ foldl1 f (x::xs) = foldl f x xs

235

258

236||| Joins the character lists by spaces into a single character list.

259||| Joins the character lists by spaces into a single character list.

237|||

260|||

261+||| ```idris example

238−||| Idris> unwords' [['A'], ['B', 'C'], ['D'], ['E']]

262+||| unwords' [['A'], ['B', 'C'], ['D'], ['E']]

239−||| ['A', ' ', 'B', 'C', ' ', 'D', ' ', 'E'] : List Char

263+||| ```

240unwords' : List (List Char) -> List Char

264unwords' : List (List Char) -> List Char

241unwords' [] = []

265unwords' [] = []

242unwords' ws = assert_total (foldr1 addSpace ws)

266unwords' ws = assert_total (foldr1 addSpace ws)

@@ -246,24 +270,28 @@ unwords' ws = assert_total (foldr1 addSpace ws)

246

270

247||| Joins the strings by spaces into a single string.

271||| Joins the strings by spaces into a single string.

248|||

272|||

273+||| ```idris example

249−||| Idris> unwords ["A", "BC", "D", "E"]

274+||| unwords ["A", "BC", "D", "E"]

250−||| "A BC D E" : String

275+||| ```

251unwords : List String -> String

276unwords : List String -> String

252unwords = pack . unwords' . map unpack

277unwords = pack . unwords' . map unpack

253

278

254||| Returns the length of the string.

279||| Returns the length of the string.

255|||

280|||

281+||| ```idris example

256−||| Idris> length ""

282+||| length ""

257−||| 0 : Nat

283+||| ```

284+||| ```idris example

258−||| Idris> length "ABC"

285+||| length "ABC"

259−||| 3 : Nat

286+||| ```

260length : String -> Nat

287length : String -> Nat

261length = fromInteger . prim__zextInt_BigInt . prim_lenString

288length = fromInteger . prim__zextInt_BigInt . prim_lenString

262

289

263||| Lowercases all characters in the string.

290||| Lowercases all characters in the string.

264|||

291|||

292+||| ```idris example

265−||| Idris> toLower "aBc12!"

293+||| toLower "aBc12!"

266−||| "abc12!" : String

294+||| ```

267toLower : String -> String

295toLower : String -> String

268toLower x with (strM x)

296toLower x with (strM x)

269 strToLower "" | StrNil = ""

297 strToLower "" | StrNil = ""

@@ -272,14 +300,15 @@ toLower x with (strM x)

272

300

273||| Uppercases all characters in the string.

301||| Uppercases all characters in the string.

274|||

302|||

303+||| ```idris example

275−||| Idris> toLower "aBc12!"

304+||| toLower "aBc12!"

276−||| "ABC12!" : String

305+||| ```

277toUpper : String -> String

306toUpper : String -> String

278toUpper x with (strM x)

307toUpper x with (strM x)

279 strToLower "" | StrNil = ""

308 strToLower "" | StrNil = ""

280 strToLower (strCons c cs) | (StrCons c cs) =

309 strToLower (strCons c cs) | (StrCons c cs) =

281 strCons (toUpper c) (toUpper (assert_smaller (strCons c cs) cs ))

310 strCons (toUpper c) (toUpper (assert_smaller (strCons c cs) cs ))

282−

311+

283--------------------------------------------------------------------------------

312--------------------------------------------------------------------------------

284-- Predicates

313-- Predicates

285--------------------------------------------------------------------------------

314--------------------------------------------------------------------------------

src/Idris/AbsSyntaxTree.hs+2

@@ -830,6 +830,8 @@ data PTactic' t = Intro [Name] | Intros | Focus Name

830 | Induction t

831 | CaseTac t

832 | Equiv t

833+ | Claim Name t

834+ | Unfocus

833 | MatchRefine Name

835 | MatchRefine Name

834 | LetTac Name t | LetTacTy Name t t

836 | LetTac Name t | LetTacTy Name t t

835 | Exact t | Compute | Trivial | TCInstance

837 | Exact t | Compute | Trivial | TCInstance

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

@@ -23,23 +23,23 @@ import Debug.Trace

23import Util.Pretty hiding (fill)

25data ProofState = PS { thname :: Name,

26− holes :: [Name], -- holes still to be solved

26+ holes :: [Name], -- ^ holes still to be solved

27− usedns :: [Name], -- used names, don't use again

27+ usedns :: [Name], -- ^ used names, don't use again

28− nextname :: Int, -- name supply

28+ nextname :: Int, -- ^ name supply

29− pterm :: ProofTerm, -- current proof term

29+ pterm :: ProofTerm, -- ^ current proof term

30− ptype :: Type, -- original goal

30+ ptype :: Type, -- ^ original goal

31− dontunify :: [Name], -- explicitly given by programmer, leave it

31+ dontunify :: [Name], -- ^ explicitly given by programmer, leave it

32 unified :: (Name, [(Name, Term)]),

33 notunified :: [(Name, Term)],

34− dotted :: [(Name, [Name])], -- dot pattern holes + environment

34+ dotted :: [(Name, [Name])], -- ^ dot pattern holes + environment

35− -- either hole or something in env must turn up in the 'notunified' list during elaboration

35+ -- either hole or something in env must turn up in the 'notunified' list during elaboration

36 solved :: Maybe (Name, Term),

37 problems :: Fails,

38 injective :: [Name],

39− deferred :: [Name], -- names we'll need to define

39+ deferred :: [Name], -- ^ names we'll need to define

40− instances :: [Name], -- instance arguments (for type classes)

40+ instances :: [Name], -- ^ instance arguments (for type classes)

41− autos :: [(Name, [Name])], -- unsolved 'auto' implicits with their holes

41+ autos :: [(Name, [Name])], -- ^ unsolved 'auto' implicits with their holes

42− previous :: Maybe ProofState, -- for undo

42+ previous :: Maybe ProofState, -- ^ for undo

43 context :: Context,

44 plog :: String,

45 unifylog :: Bool,

@@ -290,12 +290,12 @@ addLog str = action (\ps -> ps { plog = plog ps ++ str ++ "\n" })

290

291newProof :: Name -> Context -> Type -> ProofState

292newProof n ctxt ty = let h = holeName 0

293− ty' = vToP ty in

293+ ty' = vToP ty

294− PS n [h] [] 1 (mkProofTerm (Bind h (Hole ty')

294+ in PS n [h] [] 1 (mkProofTerm (Bind h (Hole ty')

295− (P Bound h ty'))) ty [] (h, []) [] []

295+ (P Bound h ty'))) ty [] (h, []) [] []

296− Nothing [] []

296+ Nothing [] []

297− [] [] []

297+ [] [] []

298− Nothing ctxt "" False False [] []

298+ Nothing ctxt "" False False [] []

299

300type TState = ProofState -- [TacticAction])

301type RunTactic = RunTactic' TState

src/Idris/Core/ProofTerm.hs+37−14

@@ -1,8 +1,9 @@

1{-# LANGUAGE MultiParamTypeClasses, FlexibleInstances, PatternGuards #-}

3−{- Implements a proof state, some primitive tactics for manipulating

3+{- | Implements a proof state, some primitive tactics for manipulating

4− proofs, and some high level commands for introducing new theorems,

4+proofs, and some high level commands for introducing new theorems,

5− evaluation/checking inside the proof system, etc. --}

5+evaluation/checking inside the proof system, etc.

6+-}

7module Idris.Core.ProofTerm(ProofTerm, Goal(..), mkProofTerm, getProofTerm,

8module Idris.Core.ProofTerm(ProofTerm, Goal(..), mkProofTerm, getProofTerm,

8 updateSolved, updateSolvedTerm, updateSolvedTerm',

9 updateSolved, updateSolvedTerm, updateSolvedTerm',

@@ -18,6 +19,7 @@ import Control.Monad.State.Strict

18import Data.List

19import Data.List

19import Debug.Trace

20import Debug.Trace

22+-- | A zipper over terms, in order to efficiently update proof terms.

21data TermPath = Top

23data TermPath = Top

22 | AppL TermPath Term

24 | AppL TermPath Term

23 | AppR Term TermPath

25 | AppR Term TermPath

@@ -25,6 +27,7 @@ data TermPath = Top

25 | InScope Name (Binder Term) TermPath

27 | InScope Name (Binder Term) TermPath

26 deriving Show

28 deriving Show

30+-- | A zipper over binders, because terms and binders are mutually defined.

28data BinderPath = Binder (Binder TermPath)

31data BinderPath = Binder (Binder TermPath)

29 | LetT TermPath Term

32 | LetT TermPath Term

30 | LetV Term TermPath

33 | LetV Term TermPath

@@ -32,6 +35,8 @@ data BinderPath = Binder (Binder TermPath)

32 | GuessV Term TermPath

35 | GuessV Term TermPath

33 deriving Show

36 deriving Show

38+-- | Replace the top of a term path with another term path. In other

39+-- words, "graft" one term path into another.

35replaceTop :: TermPath -> TermPath -> TermPath

40replaceTop :: TermPath -> TermPath -> TermPath

36replaceTop p Top = p

41replaceTop p Top = p

37replaceTop p (AppL l t) = AppL (replaceTop p l) t

42replaceTop p (AppL l t) = AppL (replaceTop p l) t

@@ -45,6 +50,7 @@ replaceTop p (InBind n bp sc) = InBind n (replaceTopB p bp) sc

45 replaceTopB p (GuessV t v) = GuessV t (replaceTop p v)

50 replaceTopB p (GuessV t v) = GuessV t (replaceTop p v)

46replaceTop p (InScope n b sc) = InScope n b (replaceTop p sc)

51replaceTop p (InScope n b sc) = InScope n b (replaceTop p sc)

53+-- | Build a term from a zipper, given something to put in the hole.

48rebuildTerm :: Term -> TermPath -> Term

54rebuildTerm :: Term -> TermPath -> Term

49rebuildTerm tm Top = tm

55rebuildTerm tm Top = tm

50rebuildTerm tm (AppL p a) = App (rebuildTerm tm p) a

56rebuildTerm tm (AppL p a) = App (rebuildTerm tm p) a

@@ -52,6 +58,7 @@ rebuildTerm tm (AppR f p) = App f (rebuildTerm tm p)

52rebuildTerm tm (InScope n b p) = Bind n b (rebuildTerm tm p)

58rebuildTerm tm (InScope n b p) = Bind n b (rebuildTerm tm p)

53rebuildTerm tm (InBind n bp sc) = Bind n (rebuildBinder tm bp) sc

59rebuildTerm tm (InBind n bp sc) = Bind n (rebuildBinder tm bp) sc

61+-- | Build a binder from a zipper, given something to put in the hole.

55rebuildBinder :: Term -> BinderPath -> Binder Term

62rebuildBinder :: Term -> BinderPath -> Binder Term

56rebuildBinder tm (Binder p) = fmap (rebuildTerm tm) p

63rebuildBinder tm (Binder p) = fmap (rebuildTerm tm) p

57rebuildBinder tm (LetT p t) = Let (rebuildTerm tm p) t

64rebuildBinder tm (LetT p t) = Let (rebuildTerm tm p) t

@@ -59,6 +66,9 @@ rebuildBinder tm (LetV v p) = Let v (rebuildTerm tm p)

59rebuildBinder tm (GuessT p t) = Guess (rebuildTerm tm p) t

66rebuildBinder tm (GuessT p t) = Guess (rebuildTerm tm p) t

60rebuildBinder tm (GuessV v p) = Guess v (rebuildTerm tm p)

67rebuildBinder tm (GuessV v p) = Guess v (rebuildTerm tm p)

69+-- | Find the binding of a hole in a term. If present, return the path

70+-- to the hole's binding, the environment extended by the binders that

71+-- are crossed, and the actual binding term.

62findHole :: Name -> Env -> Term -> Maybe (TermPath, Env, Term)

72findHole :: Name -> Env -> Term -> Maybe (TermPath, Env, Term)

63findHole n env t = fh' env Top t where

73findHole n env t = fh' env Top t where

64 fh' env path tm@(Bind x h sc)

74 fh' env path tm@(Bind x h sc)

@@ -80,7 +90,7 @@ findHole n env t = fh' env Top t where

80 fhB env path b

90 fhB env path b

81 | Just (p, env', tm) <- fh' env path (binderTy b)

91 | Just (p, env', tm) <- fh' env path (binderTy b)

82 = Just (Binder (fmap (\_ -> p) b), env', tm)

92 = Just (Binder (fmap (\_ -> p) b), env', tm)

83− fhB _ _ _ = Nothing

93+ fhB _ _ _ = Nothing

85data ProofTerm = PT { -- wholeterm :: Term,

95data ProofTerm = PT { -- wholeterm :: Term,

86 path :: TermPath,

96 path :: TermPath,

@@ -92,13 +102,17 @@ data ProofTerm = PT { -- wholeterm :: Term,

92type RunTactic' a = Context -> Env -> Term -> StateT a TC Term

102type RunTactic' a = Context -> Env -> Term -> StateT a TC Term

93type Hole = Maybe Name -- Nothing = default hole, first in list in proof state

103type Hole = Maybe Name -- Nothing = default hole, first in list in proof state

104

105+-- | Refocus the proof term zipper on a particular hole, if it

106+-- exists. If not, return the original proof term.

95refocus :: Hole -> ProofTerm -> ProofTerm

107refocus :: Hole -> ProofTerm -> ProofTerm

96refocus h t = let res = refocus' h t in res

108refocus h t = let res = refocus' h t in res

97-- trace ("OLD: " ++ show t ++ "\n" ++

109-- trace ("OLD: " ++ show t ++ "\n" ++

98-- "REFOCUSSED " ++ show h ++ ": " ++ show res) res

110-- "REFOCUSSED " ++ show h ++ ": " ++ show res) res

99refocus' (Just n) pt@(PT path env tm ups)

111refocus' (Just n) pt@(PT path env tm ups)

112+ -- First look for the hole in the proof term as-is

100 | Just (p', env', tm') <- findHole n env tm

113 | Just (p', env', tm') <- findHole n env tm

101 = PT (replaceTop p' path) env' tm' ups

114 = PT (replaceTop p' path) env' tm' ups

115+ -- Next apply the updates, and look for the hole in the resulting term

102 | Just (p', env', tm') <- findHole n [] (rebuildTerm tm (updateSolvedPath ups path))

116 | Just (p', env', tm') <- findHole n [] (rebuildTerm tm (updateSolvedPath ups path))

103 = PT p' env' tm' []

117 = PT p' env' tm' []

104 | otherwise = pt

118 | otherwise = pt

@@ -118,27 +132,32 @@ same :: Eq a => Maybe a -> a -> Bool

118same Nothing n = True

132same Nothing n = True

119same (Just x) n = x == n

133same (Just x) n = x == n

120

134

135+-- | Is a particular binder a hole or a guess?

121hole :: Binder b -> Bool

136hole :: Binder b -> Bool

122hole (Hole _) = True

137hole (Hole _) = True

123hole (Guess _ _) = True

138hole (Guess _ _) = True

124hole _ = False

139hole _ = False

125

140

141+-- | Given a list of solved holes, fill out the solutions in a term

126−updateSolvedTerm :: [(Name, Term)] -> Term -> Term

142+updateSolvedTerm :: [(Name, Term)] -> Term -> Term

127updateSolvedTerm xs x = fst $ updateSolvedTerm' xs x

143updateSolvedTerm xs x = fst $ updateSolvedTerm' xs x

128

144

145+-- | Given a list of solved holes, fill out the solutions in a

146+-- term. Return whether updates were performed, to facilitate sharing

147+-- when there are no updates.

148+updateSolvedTerm' :: [(Name, Term)] -> Term -> (Term, Bool)

129updateSolvedTerm' [] x = (x, False)

149updateSolvedTerm' [] x = (x, False)

130−updateSolvedTerm' xs x = -- updateSolved' xs x where

150+updateSolvedTerm' xs x = updateSolved' xs x where

131−-- This version below saves allocations, because it doesn't need to reallocate

151+ -- This version below saves allocations, because it doesn't need to reallocate

132−-- the term if there are no updates to do.

152+ -- the term if there are no updates to do.

133−-- The Bool is ugly, and probably 'Maybe' would be less ugly, but >>= is

153+ -- The Bool is ugly, and probably 'Maybe' would be less ugly, but >>= is

134−-- the wrong combinator. Feel free to tidy up as long as it's still as cheap :).

154+ -- the wrong combinator. Feel free to tidy up as long as it's still as cheap :).

135− updateSolved' xs x where

136 updateSolved' [] x = (x, False)

155 updateSolved' [] x = (x, False)

137 updateSolved' xs (Bind n (Hole ty) t)

156 updateSolved' xs (Bind n (Hole ty) t)

138− | Just v <- lookup n xs

157+ | Just v <- lookup n xs

139 = case xs of

158 = case xs of

140 [_] -> (subst n v t, True) -- some may be Vs! Can't assume

159 [_] -> (subst n v t, True) -- some may be Vs! Can't assume

141− -- explicit names

160+ -- explicit names

142 _ -> let (t', _) = updateSolved' xs t in

161 _ -> let (t', _) = updateSolved' xs t in

143 (subst n v t', True)

162 (subst n v t', True)

144 updateSolved' xs tm@(Bind n b t)

163 updateSolved' xs tm@(Bind n b t)

@@ -146,7 +165,7 @@ updateSolvedTerm' xs x = -- updateSolved' xs x where

146 (b', ub) = updateSolvedB' xs b in

165 (b', ub) = updateSolvedB' xs b in

147 if ut || ub then (Bind n b' t', True)

166 if ut || ub then (Bind n b' t', True)

148 else (tm, False)

167 else (tm, False)

149− updateSolved' xs t@(App f a)

168+ updateSolved' xs t@(App f a)

150 = let (f', uf) = updateSolved' xs f

169 = let (f', uf) = updateSolved' xs f

151 (a', ua) = updateSolved' xs a in

170 (a', ua) = updateSolved' xs a in

152 if uf || ua then (App f' a', True)

171 if uf || ua then (App f' a', True)

@@ -176,10 +195,14 @@ updateSolvedTerm' xs x = -- updateSolved' xs x where

176 noneOfB ns b = noneOf ns (binderTy b)

195 noneOfB ns b = noneOf ns (binderTy b)

177 noneOf ns _ = True

196 noneOf ns _ = True

178

197

198+-- | Apply solutions to an environment.

199+updateEnv :: [(Name, Term)] -> Env -> Env

179updateEnv [] e = e

200updateEnv [] e = e

180updateEnv ns [] = []

201updateEnv ns [] = []

181updateEnv ns ((n, b) : env) = (n, fmap (updateSolvedTerm ns) b) : updateEnv ns env

202updateEnv ns ((n, b) : env) = (n, fmap (updateSolvedTerm ns) b) : updateEnv ns env

182

203

204+-- | Fill out solved holes in a term zipper.

205+updateSolvedPath :: [(Name, Term)] -> TermPath -> TermPath

183updateSolvedPath [] t = t

206updateSolvedPath [] t = t

184updateSolvedPath ns Top = Top

207updateSolvedPath ns Top = Top

185updateSolvedPath ns (AppL p r) = AppL (updateSolvedPath ns p) (updateSolvedTerm ns r)

208updateSolvedPath ns (AppL p r) = AppL (updateSolvedPath ns p) (updateSolvedTerm ns r)

src/Idris/DeepSeq.hs+2

@@ -250,6 +250,7 @@ instance (NFData t) => NFData (PTactic' t) where

250 rnf (Induction x1) = rnf x1 `seq` ()

251 rnf (CaseTac x1) = rnf x1 `seq` ()

252 rnf (Equiv x1) = rnf x1 `seq` ()

253+ rnf (Claim x1 x2) = rnf x1 `seq` rnf x2 `seq` ()

253 rnf (MatchRefine x1) = rnf x1 `seq` ()

254 rnf (MatchRefine x1) = rnf x1 `seq` ()

254 rnf (LetTac x1 x2) = rnf x1 `seq` rnf x2 `seq` ()

255 rnf (LetTac x1 x2) = rnf x1 `seq` rnf x2 `seq` ()

255 rnf (LetTacTy x1 x2 x3) = rnf x1 `seq` rnf x2 `seq` rnf x3 `seq` ()

256 rnf (LetTacTy x1 x2 x3) = rnf x1 `seq` rnf x2 `seq` rnf x3 `seq` ()

@@ -280,6 +281,7 @@ instance (NFData t) => NFData (PTactic' t) where

280 rnf Skip = ()

281 rnf Skip = ()

281 rnf (TFail x1) = rnf x1 `seq` ()

282 rnf (TFail x1) = rnf x1 `seq` ()

282 rnf SourceFC = ()

283 rnf SourceFC = ()

284+ rnf Unfocus = ()

283

285

284instance NFData ErrorReportPart where

286instance NFData ErrorReportPart where

285 rnf (TermPart x1) = rnf x1 `seq` ()

287 rnf (TermPart x1) = rnf x1 `seq` ()

src/Idris/ElabQuasiquote.hs+1

@@ -36,6 +36,7 @@ extractTUnquotes n (GoalType s tac)

36 return (GoalType s tac', ex)

37extractTUnquotes n (TCheck t) = extract1 n TCheck t

38extractTUnquotes n (TEval t) = extract1 n TEval t

39+extractTUnquotes n (Claim name t) = extract1 n (Claim name) t

39extractTUnquotes n tac = return (tac, []) -- the rest don't contain PTerms

40extractTUnquotes n tac = return (tac, []) -- the rest don't contain PTerms

41extractPArgUnquotes :: Int -> PArg -> Elab' aux (PArg, [(Name, PTerm)])

42extractPArgUnquotes :: Int -> PArg -> Elab' aux (PArg, [(Name, PTerm)])

src/Idris/ElabTerm.hs+14

@@ -1517,6 +1517,12 @@ runTac autoSolve ist perhapsFC fn tac

1517 when autoSolve solveAll

1518 runT DoUnify = do unify_all

1519 when autoSolve solveAll

1520+ runT (Claim n tm) = do tmHole <- getNameFrom (sMN 0 "newGoal")

1521+ claim tmHole RType

1522+ claim n (Var tmHole)

1523+ focus tmHole

1524+ elab ist toplevel ERHS [] (sMN 0 "tac") tm

1525+ focus n

1520 runT (Equiv tm) -- let bind tm, then

1526 runT (Equiv tm) -- let bind tm, then

1521 = do attack

1527 = do attack

1522 tyn <- getNameFrom (sMN 0 "ety")

1528 tyn <- getNameFrom (sMN 0 "ety")

@@ -1577,6 +1583,10 @@ runTac autoSolve ist perhapsFC fn tac

1577 = do proofSearch' ist rec False depth prover top fn hints

1583 = do proofSearch' ist rec False depth prover top fn hints

1578 when autoSolve solveAll

1584 when autoSolve solveAll

1579 runT (Focus n) = focus n

1585 runT (Focus n) = focus n

1586+ runT Unfocus = do hs <- get_holes

1587+ case hs of

1588+ [] -> return ()

1589+ (h : _) -> movelast h

1580 runT Solve = solve

1590 runT Solve = solve

1581 runT (Try l r) = do try' (runT l) (runT r) True

1591 runT (Try l r) = do try' (runT l) (runT r) True

1582 runT (TSeq l r) = do runT l; runT r

1592 runT (TSeq l r) = do runT l; runT r

@@ -1721,6 +1731,7 @@ reify _ (P _ n _) | n == reflm "Solve" = return Solve

1721reify _ (P _ n _) | n == reflm "Compute" = return Compute

1731reify _ (P _ n _) | n == reflm "Compute" = return Compute

1722reify _ (P _ n _) | n == reflm "Skip" = return Skip

1732reify _ (P _ n _) | n == reflm "Skip" = return Skip

1723reify _ (P _ n _) | n == reflm "SourceFC" = return SourceFC

1733reify _ (P _ n _) | n == reflm "SourceFC" = return SourceFC

1734+reify _ (P _ n _) | n == reflm "Unfocus" = return Unfocus

1724reify ist t@(App _ _)

1735reify ist t@(App _ _)

1725 | (P _ f _, args) <- unApply t = reifyApp ist f args

1736 | (P _ f _, args) <- unApply t = reifyApp ist f args

1726reify _ t = fail ("Unknown tactic " ++ show t)

1737reify _ t = fail ("Unknown tactic " ++ show t)

@@ -1732,6 +1743,9 @@ reifyApp _ t [Constant (I i)]

1732reifyApp _ t [x]

1743reifyApp _ t [x]

1733 | t == reflm "Refine" = do n <- reifyTTName x

1744 | t == reflm "Refine" = do n <- reifyTTName x

1734 return $ Refine n []

1745 return $ Refine n []

1746+reifyApp ist t [n, ty] | t == reflm "Claim" = do n' <- reifyTTName n

1747+ goal <- reifyTT ty

1748+ return $ Claim n' (delab ist goal)

1735reifyApp ist t [l, r] | t == reflm "Seq" = liftM2 TSeq (reify ist l) (reify ist r)

1749reifyApp ist t [l, r] | t == reflm "Seq" = liftM2 TSeq (reify ist l) (reify ist r)

1736reifyApp ist t [Constant (Str n), x]

1750reifyApp ist t [Constant (Str n), x]

1737 | t == reflm "GoalType" = liftM (GoalType n) (reify ist x)

1751 | t == reflm "GoalType" = liftM (GoalType n) (reify ist x)

src/Idris/IdeMode.hs+4

@@ -230,6 +230,7 @@ data IdeModeCommand = REPLCompletions String

230 | PrintDef String

231 | ErrString Err

232 | ErrPPrint Err

233+ | GetIdrisVersion

233

234

234sexpToCommand :: SExp -> Maybe IdeModeCommand

235sexpToCommand :: SExp -> Maybe IdeModeCommand

235sexpToCommand (SexpList (x:[])) = sexpToCommand x

236sexpToCommand (SexpList (x:[])) = sexpToCommand x

@@ -275,6 +276,7 @@ sexpToCommand (SexpList [SymbolAtom "hide-term-implicits", StringAtom encoded])

275sexpToCommand (SexpList [SymbolAtom "print-definition", StringAtom name]) = Just (PrintDef name)

276sexpToCommand (SexpList [SymbolAtom "print-definition", StringAtom name]) = Just (PrintDef name)

276sexpToCommand (SexpList [SymbolAtom "error-string", StringAtom encoded]) = Just . ErrString . decodeErr $ encoded

277sexpToCommand (SexpList [SymbolAtom "error-string", StringAtom encoded]) = Just . ErrString . decodeErr $ encoded

277sexpToCommand (SexpList [SymbolAtom "error-pprint", StringAtom encoded]) = Just . ErrPPrint . decodeErr $ encoded

278sexpToCommand (SexpList [SymbolAtom "error-pprint", StringAtom encoded]) = Just . ErrPPrint . decodeErr $ encoded

279+sexpToCommand (SymbolAtom "version") = Just GetIdrisVersion

278sexpToCommand _ = Nothing

280sexpToCommand _ = Nothing

279

281

280parseMessage :: String -> Either Err (SExp, Integer)

282parseMessage :: String -> Either Err (SExp, Integer)

@@ -298,5 +300,7 @@ convSExp pre s id =

298getHexLength :: String -> String

300getHexLength :: String -> String

299getHexLength s = printf "%06x" (1 + (length s))

301getHexLength s = printf "%06x" (1 + (length s))

300

302

303+-- | The version of the IDE mode command set. Increment this when you

304+-- change it so clients can adapt.

301ideModeEpoch :: Int

305ideModeEpoch :: Int

302ideModeEpoch = 1

306ideModeEpoch = 1

src/Idris/ParseExpr.hs+6−1

@@ -1251,10 +1251,15 @@ tactics =

1251 [ (["intro"], Nothing, const $ -- FIXME syntax for intro (fresh name)

1252 do ns <- sepBy (spaced name) (lchar ','); return $ Intro ns)

1253 , noArgs ["intros"] Intros

1254+ , noArgs ["unfocus"] Unfocus

1254 , (["refine"], Just ExprTArg, const $

1255 , (["refine"], Just ExprTArg, const $

1255 do n <- spaced fnName

1256 do n <- spaced fnName

1256 imps <- many imp

1257 imps <- many imp

1257 return $ Refine n imps)

1258 return $ Refine n imps)

1259+ , (["claim"], Nothing, \syn ->

1260+ do n <- indentPropHolds gtProp *> name

1261+ goal <- indentPropHolds gtProp *> expr syn

1262+ return $ Claim n goal)

1258 , (["mrefine"], Just ExprTArg, const $

1263 , (["mrefine"], Just ExprTArg, const $

1259 do n <- spaced fnName

1264 do n <- spaced fnName

1260 return $ MatchRefine n)

1265 return $ MatchRefine n)

@@ -1329,7 +1334,7 @@ tactics =

1329

1334

1330

1335

1331tactic :: SyntaxInfo -> IdrisParser PTactic

1336tactic :: SyntaxInfo -> IdrisParser PTactic

1332−tactic syn = choice [ do choice (map reserved names); parser syn

1337+tactic syn = choice [ do choice (map reserved names); parser syn

1333 | (names, _, parser) <- tactics ]

1338 | (names, _, parser) <- tactics ]

1334 <|> do lchar '{'

1339 <|> do lchar '{'

1335 t <- tactic syn;

1340 t <- tactic syn;

src/Idris/REPL.hs+9−1

@@ -508,6 +508,14 @@ runIdeModeCommand h id orig fn modes (IdeMode.ErrPPrint e) =

508 fmap (fancifyAnnots ist) $ pprintErr ist e

509 msg = (IdeMode.SymbolAtom "ok", out, spans)

510 runIO . hPutStrLn h $ IdeMode.convSExp "return" msg id

511+runIdeModeCommand h id orig fn modes IdeMode.GetIdrisVersion =

512+ let idrisVersion = (versionBranch version,

513+ if not (null gitHash)

514+ then [gitHash]

515+ else [])

516+ msg = (IdeMode.SymbolAtom "ok", idrisVersion)

517+ in runIO . hPutStrLn h $ IdeMode.convSExp "return" msg id

518+

511

519

512-- | Show a term for IDEMode with the specified implicitness

520-- | Show a term for IDEMode with the specified implicitness

513ideModeForceTermImplicits :: Handle -> Integer -> [(Name, Bool)] -> Bool -> Term -> Idris ()

521ideModeForceTermImplicits :: Handle -> Integer -> [(Name, Bool)] -> Bool -> Term -> Idris ()

@@ -1798,7 +1806,7 @@ getPort (_:xs) = getPort xs

1798opt :: (Opt -> Maybe a) -> [Opt] -> [a]

1806opt :: (Opt -> Maybe a) -> [Opt] -> [a]

1799opt = mapMaybe

1807opt = mapMaybe

1800

1808

1801−ver = showVersion version ++ gitHash

1809+ver = showVersion version ++ "-" ++ gitHash

1802

1810

1803defaultPort :: PortID

1811defaultPort :: PortID

1804defaultPort = PortNumber (fromIntegral 4294)

1812defaultPort = PortNumber (fromIntegral 4294)

test/proof008/ClaimAndUnfocus.idrnew file+17

@@ -0,0 +1,17 @@

1+module ClaimAndUnfocus

3+foo : Nat -> Nat

4+foo = ?foo_rhs

6+---------- Proofs ----------

8+ClaimAndUnfocus.foo_rhs = proof

9+ claim bar Nat -> Nat -> Nat

10+ unfocus

11+ intro x

12+ exact bar x x

13+ intro x,y

14+ refine plus

15+ refine x

16+ refine y

17+

test/proof008/expectednew file

No changes to the content.

test/proof008/runnew file+3

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

1+#!/usr/bin/env bash

2+idris --check $@ ClaimAndUnfocus.idr

3+rm -f *.ibc