git.iko.soy/Idris-dev
on master help sign in
Add "rewrite" to new-style tactics
commita1c42ad4c929ca28b3543b1db774176ee3df5e60 authorDavid Raymond Christiansen <david@davidchristiansen.dk> dateMon 2 Mar 2015, 21:58 (12 years ago) parent0550c86
6 files changed+42
compare with master
unifiedsplit
idris.cabal+3 libs/prelude/Language/Reflection/Tactical.idr+5 src/Idris/ElabTerm.hs+4 test/tactics001/Tactics.idr+27 test/tactics001/expected test/tactics001/run+3
idris.cabal+3
@@ -548,6 +548,9 @@ Extra-source-files:
548548 test/sugar005/*.idr
549549 test/sugar005/expected
550550
551+ test/tactics001/run
552+ test/tactics001/*.idr
553+ test/tactics001/expected
551554
552555 test/totality001/run
553556 test/totality001/*.idr
libs/prelude/Language/Reflection/Tactical.idr+5
@@ -34,6 +34,8 @@ data Tactical : Type -> Type where
3434 prim__Unfocus : TTName -> Tactical ()
3535 prim__Attack : Tactical ()
3636
37+ prim__Rewrite : Raw -> Tactical ()
38+
3739 prim__Claim : TTName -> Raw -> Tactical ()
3840 prim__Intro : Maybe TTName -> Tactical ()
3941
@@ -109,3 +111,6 @@ sourceLocation : Tactical ()
109111sourceLocation = do loc <- getSourceLocation
110112 fill (quote loc)
111113 solve
114+
115+rewriteWith : Raw -> Tactical ()
116+rewriteWith rule = prim__Rewrite rule
src/Idris/ElabTerm.hs+4
@@ -1578,6 +1578,10 @@ runTactical fc ctxt env tm = runTacTm (eval tm) >> return ()
15781578 | n == tacN "prim__Attack", [] <- args
15791579 = do attack
15801580 returnUnit
1581+ | n == tacN "prim__Rewrite", [rule] <- args
1582+ = do r <- reifyRaw rule
1583+ rewrite r
1584+ returnUnit
15811585 | n == tacN "prim__Focus", [what] <- args
15821586 = do n' <- reifyTTName what
15831587 focus n'
test/tactics001/Tactics.idrnew file+27
@@ -0,0 +1,27 @@
1+module Tactics
2+
3+import Language.Reflection.Tactical
4+
5+%default total
6+
7+-- Test that basic proofs with new-style tactics work
8+
9+||| Construct a Refl at some particular type for some particular term
10+||| @ t the type
11+||| @ x the term for equality to be reflexive at
12+refl : (t, x : Raw) -> Raw
13+refl t x = RApp (RApp (Var (UN "Refl")) t) x
14+
15+plusZeroRightNeutralNew : (n : Nat) -> plus n 0 = n
16+plusZeroRightNeutralNew Z = Refl
17+plusZeroRightNeutralNew (S k) =
18+ %runTactics (do rewriteWith `(sym $ plusZeroRightNeutralNew ~(Var "k"))
19+ fill $ refl `(Nat : Type) `(S ~(Var (UN "k")))
20+ solve)
21+
22+plusSuccRightSuccNew : (j, k : Nat) -> plus j (S k) = S (plus j k)
23+plusSuccRightSuccNew Z k = Refl
24+plusSuccRightSuccNew (S j) k =
25+ %runTactics (do rewriteWith `(sym $ plusSuccRightSuccNew ~(Var "j") ~(Var (UN "k")))
26+ fill $ refl `(Nat : Type) `(S (S (plus ~(Var (UN "j")) ~(Var (UN "k")))))
27+ solve)
test/tactics001/expectednew file

No changes to the content.

test/tactics001/runnew file+3
@@ -0,0 +1,3 @@
1+#!/usr/bin/env bash
2+idris $@ --check Tactics.idr
3+rm -f *.ibc