e91819c · Idris-dev · git.iko.soy

CHANGELOG+4

compare with master

unifiedsplit

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

1+New in 0.9.14:

2+* Tactic for case analysis in proofs

3+* Induction and case tactic now work on expressions

4+

1New in 0.9.13:

5New in 0.9.13:

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

6--------------

3* IDE support for retrieving structured information about metavariables

7* IDE support for retrieving structured information about metavariables

src/Idris/Completion.hs+2−1

@@ -44,7 +44,8 @@ tacticArgs = [ ("intro", Nothing) -- FIXME syntax for intro (fresh name)

44 , ("reflect", Just ExprTArg)

45 , ("fill", Just ExprTArg)

46 , ("try", Just AltsTArg)

47− , ("induction", Just NameTArg)

47+ , ("induction", Just ExprTArg)

48+ , ("case", Just ExprTArg)

48 , (":t", Just ExprTArg)

49 , (":t", Just ExprTArg)

49 , (":type", Just ExprTArg)

50 , (":type", Just ExprTArg)

50 , (":e", Just ExprTArg)

51 , (":e", Just ExprTArg)

src/Idris/DeepSeq.hs+2

@@ -119,6 +119,7 @@ instance NFData FnOpt where

119instance NFData DataOpt where

120 rnf Codata = ()

121 rnf DefaultEliminator = ()

122+ rnf DefaultCaseFun = ()

122

123

123instance (NFData t) => NFData (PDecl' t) where

124instance (NFData t) => NFData (PDecl' t) where

124 rnf (PFix x1 x2 x3) = rnf x1 `seq` rnf x2 `seq` rnf x3 `seq` ()

125 rnf (PFix x1 x2 x3) = rnf x1 `seq` rnf x2 `seq` rnf x3 `seq` ()

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

238 rnf (Refine x1 x2) = rnf x1 `seq` rnf x2 `seq` ()

239 rnf (Refine x1 x2) = rnf x1 `seq` rnf x2 `seq` ()

239 rnf (Rewrite x1) = rnf x1 `seq` ()

240 rnf (Rewrite x1) = rnf x1 `seq` ()

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

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

242+ rnf (CaseTac x1) = rnf x1 `seq` ()

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

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

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

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

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

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

src/Idris/ElabTerm.hs+1

@@ -1234,6 +1234,7 @@ reifyApp ist t [Constant (Str n), x]

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

1235reifyApp _ t [n] | t == reflm "Intro" = liftM (Intro . (:[])) (reifyTTName n)

1236reifyApp ist t [t'] | t == reflm "Induction" = liftM (Induction . delab ist) (reifyTT t')

1237+reifyApp ist t [t'] | t == reflm "Case" = liftM (Induction . delab ist) (reifyTT t')

1237reifyApp ist t [t']

1238reifyApp ist t [t']

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

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

1239reifyApp ist t [t']

1240reifyApp ist t [t']

src/Idris/IdrisDoc.hs+1

@@ -335,6 +335,7 @@ extractPTactic (Focus n) = [n]

335extractPTactic (Refine n _) = [n]

336extractPTactic (Rewrite p) = extract p

337extractPTactic (Induction p) = extract p

338+extractPTactic (CaseTac p) = extract p

338extractPTactic (Equiv p) = extract p

339extractPTactic (Equiv p) = extract p

339extractPTactic (MatchRefine n) = [n]

340extractPTactic (MatchRefine n) = [n]

340extractPTactic (LetTac n p) = n : extract p

341extractPTactic (LetTac n p) = n : extract p