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

.gitignore+2

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

1414.DS_Store

1515.hpc

1616*.tix

17+.projectile

18+.dir-locals.el

1719custom.mk

1820libs/base/base_doc/

1921libs/effects/effects_doc/

CHANGELOG+3

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

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

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

44 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

58

69New in 0.9.16:

710--------------

Setup.hs+1−1

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

106106 "gitHash :: String\n" ++

107107 if release

108108 then "gitHash = \"\"\n"

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

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

110110

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

112112generateTargetModule verbosity dir targetDir = do

idris.cabal+3

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

497497 test/proof004/run

498498 test/proof004/*.idr

499499 test/proof004/expected

500+ test/proof008/run

501+ test/proof008/*.idr

502+ test/proof008/expected

500503

501504 test/quasiquote001/run

502505 test/quasiquote001/*.idr

libs/prelude/Language/Reflection.idr+7

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

213213 Refine TTName |

214214 ||| Apply both tactics in sequence

215215 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 |

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

217221 Trivial |

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

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

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

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

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

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

480+ quote Unfocus = `(Unfocus)

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

476482 quote Trivial = `(Trivial)

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

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

494500 quote Skip = `(Skip)

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

496502 quote SourceFC = `(SourceFC)

503+

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

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

1717

1818||| Appends two strings together.

1919|||

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

21−||| "ABC" : String

20+||| ```idris example

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

22+||| ```

2223(++) : String -> String -> String

2324(++) = prim__concat

2425

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

2627|||

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

2829|||

29−||| Idris> strHead "A"

30−||| 'A' : Char

30+||| ```idris example

31+||| strHead "A"

32+||| ```

3133partial

3234strHead : String -> Char

3335strHead = prim__strHead

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

3638|||

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

3840|||

39−||| Idris> strTail "AB"

40−||| "B" : String

41−||| Idris> strTail "A"

42−||| "" : String

41+||| ```idris example

42+||| strTail "AB"

43+||| ```

44+||| ```idris example

45+||| strTail "A"

46+||| ```

4347partial

4448strTail : String -> String

4549strTail = prim__strTail

4650

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

4852|||

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

50−||| "AB" : String

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

52−||| "A" : String

53+||| ```idris example

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

55+||| ```

56+||| ```idris example

57+||| strCons 'A' ""

58+||| ```

5359strCons : Char -> String -> String

5460strCons = prim__strCons

5561

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

5763|||

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

5965|||

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

61−||| 'B' : Char

66+||| ```idris example

67+||| strIndex "AB" 1

68+||| ```

6269partial

6370strIndex : String -> Int -> Char

6471strIndex = prim__strIndex

6572

6673||| Reverses the elements within a String.

6774|||

68−||| Idris> reverse "ABC"

69−||| "CBA" : String

70−||| Idris> reverse ""

71−||| "" : String

75+||| ```idris example

76+||| reverse "ABC"

77+||| ```

78+||| ```idris example

79+||| reverse ""

80+||| ```

7281reverse : String -> String

7382reverse = prim__strRev

7483

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

103112

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

105114|||

106−||| Idris> unpack "ABC"

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

115+||| ```idris example

116+||| unpack "ABC"

117+||| ```

108118unpack : String -> List Char

109119unpack s with (strM s)

110120 unpack "" | StrNil = []

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

116126

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

118128|||

119−||| Idris> singleton 'A'

120−||| "A" : String

129+||| ```idris example

130+||| singleton 'A'

131+||| ```

121132singleton : Char -> String

122133singleton c = strCons c ""

123134

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

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

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

141152|||

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

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

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

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

153+||| ```idris example

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

155+||| ```

156+||| ```idris example

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

158+||| ```

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

147160span p xs with (strM xs)

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

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

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

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

156169|||

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

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

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

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

170+||| ```idris example

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

172+||| ```

173+||| ```idris example

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

175+||| ```

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

162177break p = span (not . p)

163178

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

165180||| indicating separator characters.

166181|||

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

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

182+||| ```idris example

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

184+||| ```

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

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

171187

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

173189||| the start of the string.

174190|||

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

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

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

178−||| "AB" : String

191+||| ```idris example

192+||| ltrim " A\nB"

193+||| ```

194+||| ```idris example

195+||| ltrim " \nAB"

196+||| ```

179197ltrim : String -> String

180198ltrim xs with (strM xs)

181199 ltrim "" | StrNil = ""

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

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

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

187205|||

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

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

206+||| ```idris example

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

208+||| ```

190209trim : String -> String

191210trim xs = ltrim (reverse (ltrim (reverse xs)))

192211

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

194213|||

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

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

214+||| ```idris example

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

216+||| ```

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

198218words' s = case dropWhile isSpace s of

199219 [] => []

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

202222

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

204224|||

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

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

225+||| ```idris example

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

227+||| ```

207228words : String -> List String

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

209230

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

211232|||

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

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

233+||| ```idris example

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

235+||| ```

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

215237lines' s = case dropWhile isNL s of

216238 [] => []

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

219241

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

221243|||

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

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

244+||| ```idris example

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

246+||| ```

224247lines : String -> List String

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

226249

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

235258

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

237260|||

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

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

261+||| ```idris example

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

263+||| ```

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

241265unwords' [] = []

242266unwords' ws = assert_total (foldr1 addSpace ws)

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

246270

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

248272|||

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

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

273+||| ```idris example

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

275+||| ```

251276unwords : List String -> String

252277unwords = pack . unwords' . map unpack

253278

254279||| Returns the length of the string.

255280|||

256−||| Idris> length ""

257−||| 0 : Nat

258−||| Idris> length "ABC"

259−||| 3 : Nat

281+||| ```idris example

282+||| length ""

283+||| ```

284+||| ```idris example

285+||| length "ABC"

286+||| ```

260287length : String -> Nat

261288length = fromInteger . prim__zextInt_BigInt . prim_lenString

262289

263290||| Lowercases all characters in the string.

264291|||

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

266−||| "abc12!" : String

292+||| ```idris example

293+||| toLower "aBc12!"

294+||| ```

267295toLower : String -> String

268296toLower x with (strM x)

269297 strToLower "" | StrNil = ""

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

272300

273301||| Uppercases all characters in the string.

274302|||

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

276−||| "ABC12!" : String

303+||| ```idris example

304+||| toLower "aBc12!"

305+||| ```

277306toUpper : String -> String

278307toUpper x with (strM x)

279308 strToLower "" | StrNil = ""

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

281310 strCons (toUpper c) (toUpper (assert_smaller (strCons c cs) cs ))

282−

311+

283312--------------------------------------------------------------------------------

284313-- Predicates

285314--------------------------------------------------------------------------------

src/Idris/AbsSyntaxTree.hs+2

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

830830 | Induction t

831831 | CaseTac t

832832 | Equiv t

833+ | Claim Name t

834+ | Unfocus

833835 | MatchRefine Name

834836 | LetTac Name t | LetTacTy Name t t

835837 | Exact t | Compute | Trivial | TCInstance

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

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

2323import Util.Pretty hiding (fill)

2424

2525data ProofState = PS { thname :: Name,

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

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

28− nextname :: Int, -- name supply

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

30− ptype :: Type, -- original goal

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

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

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

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

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

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

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

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

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

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

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

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

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

3636 solved :: Maybe (Name, Term),

3737 problems :: Fails,

3838 injective :: [Name],

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

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

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

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

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

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

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

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

4343 context :: Context,

4444 plog :: String,

4545 unifylog :: Bool,

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

290290

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

292292newProof n ctxt ty = let h = holeName 0

293− ty' = vToP ty in

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

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

296− Nothing [] []

297− [] [] []

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

293+ ty' = vToP ty

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

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

296+ Nothing [] []

297+ [] [] []

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

299299

300300type TState = ProofState -- [TacticAction])

301301type RunTactic = RunTactic' TState

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

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

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

22

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

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

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

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

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

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

6+-}

67

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

89 updateSolved, updateSolvedTerm, updateSolvedTerm',

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

1819import Data.List

1920import Debug.Trace

2021

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

2123data TermPath = Top

2224 | AppL TermPath Term

2325 | AppR Term TermPath

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

2527 | InScope Name (Binder Term) TermPath

2628 deriving Show

2729

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

2831data BinderPath = Binder (Binder TermPath)

2932 | LetT TermPath Term

3033 | LetV Term TermPath

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

3235 | GuessV Term TermPath

3336 deriving Show

3437

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

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

3540replaceTop :: TermPath -> TermPath -> TermPath

3641replaceTop p Top = p

3742replaceTop 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

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

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

4752

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

4854rebuildTerm :: Term -> TermPath -> Term

4955rebuildTerm tm Top = tm

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

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

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

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

5460

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

5562rebuildBinder :: Term -> BinderPath -> Binder Term

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

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

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

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

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

6168

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.

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

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

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

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

8090 fhB env path b

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

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

83− fhB _ _ _ = Nothing

93+ fhB _ _ _ = Nothing

8494

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

8696 path :: TermPath,

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

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

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

94104

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

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

95107refocus :: Hole -> ProofTerm -> ProofTerm

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

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

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

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

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

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

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

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

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

103117 = PT p' env' tm' []

104118 | otherwise = pt

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

118132same Nothing n = True

119133same (Just x) n = x == n

120134

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

121136hole :: Binder b -> Bool

122137hole (Hole _) = True

123138hole (Guess _ _) = True

124139hole _ = False

125140

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

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

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

127143updateSolvedTerm xs x = fst $ updateSolvedTerm' xs x

128144

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)

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

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

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

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

133−-- 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 :).

135− updateSolved' xs x where

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

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

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

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

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

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

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

138− | Just v <- lookup n xs

157+ | Just v <- lookup n xs

139158 = case xs of

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

141− -- explicit names

160+ -- explicit names

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

143162 (subst n v t', True)

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

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

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

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

148167 else (tm, False)

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

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

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

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

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

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

176195 noneOfB ns b = noneOf ns (binderTy b)

177196 noneOf ns _ = True

178197

198+-- | Apply solutions to an environment.

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

179200updateEnv [] e = e

180201updateEnv ns [] = []

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

182203

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

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

183206updateSolvedPath [] t = t

184207updateSolvedPath ns Top = Top

185208updateSolvedPath 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

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

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

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

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

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

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

255256 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

280281 rnf Skip = ()

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

282283 rnf SourceFC = ()

284+ rnf Unfocus = ()

283285

284286instance NFData ErrorReportPart where

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

src/Idris/ElabQuasiquote.hs+1

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

3636 return (GoalType s tac', ex)

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

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

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

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

4041

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

src/Idris/ElabTerm.hs+14

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

15171517 when autoSolve solveAll

15181518 runT DoUnify = do unify_all

15191519 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

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

15211527 = do attack

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

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

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

15781584 when autoSolve solveAll

15791585 runT (Focus n) = focus n

1586+ runT Unfocus = do hs <- get_holes

1587+ case hs of

1588+ [] -> return ()

1589+ (h : _) -> movelast h

15801590 runT Solve = solve

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

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

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

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

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

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

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

17241735reify ist t@(App _ _)

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

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

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

17321743reifyApp _ t [x]

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

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

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

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

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

src/Idris/IdeMode.hs+4

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

230230 | PrintDef String

231231 | ErrString Err

232232 | ErrPPrint Err

233+ | GetIdrisVersion

233234

234235sexpToCommand :: SExp -> Maybe IdeModeCommand

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

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

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

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

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

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

278280sexpToCommand _ = Nothing

279281

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

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

298300getHexLength :: String -> String

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

300302

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

304+-- change it so clients can adapt.

301305ideModeEpoch :: Int

302306ideModeEpoch = 1

src/Idris/ParseExpr.hs+6−1

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

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

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

12531253 , noArgs ["intros"] Intros

1254+ , noArgs ["unfocus"] Unfocus

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

12551256 do n <- spaced fnName

12561257 imps <- many imp

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

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

12591264 do n <- spaced fnName

12601265 return $ MatchRefine n)

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

13291334

13301335

13311336tactic :: 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

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

13341339 <|> do lchar '{'

13351340 t <- tactic syn;

src/Idris/REPL.hs+9−1

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

508508 fmap (fancifyAnnots ist) $ pprintErr ist e

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

510510 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+

511519

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

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

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

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

17991807opt = mapMaybe

18001808

1801−ver = showVersion version ++ gitHash

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

18021810

18031811defaultPort :: PortID

18041812defaultPort = PortNumber (fromIntegral 4294)

test/proof008/ClaimAndUnfocus.idrnew file+17

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

1+module ClaimAndUnfocus

2+

3+foo : Nat -> Nat

4+foo = ?foo_rhs

5+

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

7+

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