a1c42ad · Idris-dev · git.iko.soy

idris.cabal+3

compare with master

unifiedsplit

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

548 test/sugar005/*.idr

549 test/sugar005/expected

550

551+ test/tactics001/run

552+ test/tactics001/*.idr

553+ test/tactics001/expected

551

554

552 test/totality001/run

555 test/totality001/run

553 test/totality001/*.idr

556 test/totality001/*.idr

libs/prelude/Language/Reflection/Tactical.idr+5

@@ -34,6 +34,8 @@ data Tactical : Type -> Type where

34 prim__Unfocus : TTName -> Tactical ()

35 prim__Attack : Tactical ()

36

37+ prim__Rewrite : Raw -> Tactical ()

38+

37 prim__Claim : TTName -> Raw -> Tactical ()

39 prim__Claim : TTName -> Raw -> Tactical ()

38 prim__Intro : Maybe TTName -> Tactical ()

40 prim__Intro : Maybe TTName -> Tactical ()

39

41

@@ -109,3 +111,6 @@ sourceLocation : Tactical ()

109sourceLocation = do loc <- getSourceLocation

111sourceLocation = do loc <- getSourceLocation

110 fill (quote loc)

112 fill (quote loc)

111 solve

113 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 ()

1578 | n == tacN "prim__Attack", [] <- args

1579 = do attack

1580 returnUnit

1581+ | n == tacN "prim__Rewrite", [rule] <- args

1582+ = do r <- reifyRaw rule

1583+ rewrite r

1584+ returnUnit

1581 | n == tacN "prim__Focus", [what] <- args

1585 | n == tacN "prim__Focus", [what] <- args

1582 = do n' <- reifyTTName what

1586 = do n' <- reifyTTName what

1583 focus n'

1587 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