Add "rewrite" to new-style tactics

idris.cabal

@@ -548,6 +548,9 @@ Extra-source-files:
                        test/sugar005/*.idr
                        test/sugar005/expected
 
+                       test/tactics001/run
+                       test/tactics001/*.idr
+                       test/tactics001/expected
 
                        test/totality001/run
                        test/totality001/*.idr

libs/prelude/Language/Reflection/Tactical.idr

@@ -34,6 +34,8 @@ data Tactical : Type -> Type where
   prim__Unfocus : TTName -> Tactical ()
   prim__Attack : Tactical ()
 
+  prim__Rewrite : Raw -> Tactical ()
+
   prim__Claim : TTName -> Raw -> Tactical ()
   prim__Intro : Maybe TTName -> Tactical ()
 
@@ -109,3 +111,6 @@ sourceLocation : Tactical ()
 sourceLocation = do loc <- getSourceLocation
                     fill (quote loc)
                     solve
+
+rewriteWith : Raw -> Tactical ()
+rewriteWith rule = prim__Rewrite rule

src/Idris/ElabTerm.hs

@@ -1578,6 +1578,10 @@ runTactical fc ctxt env tm = runTacTm (eval tm) >> return ()
       | n == tacN "prim__Attack", [] <- args
       = do attack
            returnUnit
+      | n == tacN "prim__Rewrite", [rule] <- args
+      = do r <- reifyRaw rule
+           rewrite r
+           returnUnit
       | n == tacN "prim__Focus", [what] <- args
       = do n' <- reifyTTName what
            focus n'

test/tactics001/Tactics.idr

@@ -0,0 +1,27 @@
+module Tactics
+
+import Language.Reflection.Tactical
+
+%default total
+
+-- Test that basic proofs with new-style tactics work
+
+||| Construct a Refl at some particular type for some particular term
+||| @ t the type
+||| @ x the term for equality to be reflexive at
+refl : (t, x : Raw) -> Raw
+refl t x = RApp (RApp (Var (UN "Refl")) t) x
+
+plusZeroRightNeutralNew : (n : Nat) -> plus n 0 = n
+plusZeroRightNeutralNew Z = Refl
+plusZeroRightNeutralNew (S k) =
+  %runTactics (do rewriteWith `(sym $ plusZeroRightNeutralNew ~(Var "k"))
+                  fill $ refl `(Nat : Type) `(S ~(Var (UN "k")))
+                  solve)
+
+plusSuccRightSuccNew : (j, k : Nat) -> plus j (S k) = S (plus j k)
+plusSuccRightSuccNew Z k = Refl
+plusSuccRightSuccNew (S j) k =
+  %runTactics (do rewriteWith `(sym $ plusSuccRightSuccNew ~(Var "j") ~(Var (UN "k")))
+                  fill $ refl `(Nat : Type) `(S (S (plus ~(Var (UN "j")) ~(Var (UN "k")))))
+                  solve)

test/tactics001/run

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