e91819c · Idris-dev · git.iko.soy

git.iko.soy/Idris-dev

Final cleanup/check of case tactic implementation

commite91819c34ac9a88ee6d86734cc7b0804ae778b6f authorAhmad Salim Al-Sibahi <asal@itu.dk> dateMon 9 Jun 2014, 19:01 (12 years ago) parent5045dae

5 files changed+10−1

compare with master

unifiedsplit

CHANGELOG+4 src/Idris/Completion.hs+2−1 src/Idris/DeepSeq.hs+2 src/Idris/ElabTerm.hs+1 src/Idris/IdrisDoc.hs+1

CHANGELOG+4

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

15New in 0.9.13:

26--------------

37* 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)

4444 , ("reflect", Just ExprTArg)

4545 , ("fill", Just ExprTArg)

4646 , ("try", Just AltsTArg)

47− , ("induction", Just NameTArg)

47+ , ("induction", Just ExprTArg)

48+ , ("case", Just ExprTArg)

4849 , (":t", Just ExprTArg)

4950 , (":type", Just ExprTArg)

5051 , (":e", Just ExprTArg)

src/Idris/DeepSeq.hs+2

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

119119instance NFData DataOpt where

120120 rnf Codata = ()

121121 rnf DefaultEliminator = ()

122+ rnf DefaultCaseFun = ()

122123

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

124125 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

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

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

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

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

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

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

243245 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]

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

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

12361236reifyApp 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')

12371238reifyApp ist t [t']

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

12391240reifyApp ist t [t']

src/Idris/IdrisDoc.hs+1

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

335335extractPTactic (Refine n _) = [n]

336336extractPTactic (Rewrite p) = extract p

337337extractPTactic (Induction p) = extract p

338+extractPTactic (CaseTac p) = extract p

338339extractPTactic (Equiv p) = extract p

339340extractPTactic (MatchRefine n) = [n]

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