From 7593ee14685006ce5ed635451b312aadba64c0bb Mon Sep 17 00:00:00 2001
From: Leonardo de Moura <leonardo@microsoft.com>
Date: Wed, 2 Jul 2014 07:08:20 -0700
Subject: [PATCH] refactor(library/standard): remove parameter from 'tactic'
 inductive type

Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
---
 library/standard/tactic.lean          | 38 ++++++++++++++-------------
 src/library/tactic/expr_to_tactic.cpp | 18 ++++++++++---
 tests/lean/run/tactic4.lean           |  2 +-
 3 files changed, 35 insertions(+), 23 deletions(-)

diff --git a/library/standard/tactic.lean b/library/standard/tactic.lean
index 933e6b9f1..18c4e457a 100644
--- a/library/standard/tactic.lean
+++ b/library/standard/tactic.lean
@@ -1,30 +1,32 @@
+-- Copyright (c) 2014 Microsoft Corporation. All rights reserved.
+-- Released under Apache 2.0 license as described in the file LICENSE.
+-- Author: Leonardo de Moura
 import logic
 
 -- This is just a trick to embed the 'tactic language' as a
--- Lean expression. We should view (tactic A) as automation
--- that when execute produces a term of type A.
+-- Lean expression. We should view 'tactic' as automation
+-- that when execute produces a term.
 -- tactic_value is just a "dummy" for creating the "fake"
-inductive tactic (A : Type) : Type :=
-| tactic_value {} : tactic A
+-- definitions
+inductive tactic : Type :=
+| tactic_value : tactic
 -- Remark the following names are not arbitrary, the tactic module
 -- uses them when converting Lean expressions into actual tactic objects.
 -- The bultin 'by' construct triggers the process of converting a
--- a term of type (tactic A) into a tactic that sythesizes a term
--- of type A
-definition then_tac   {A : Type} (t1 t2 : tactic A) : tactic A := tactic_value
-definition orelse_tac {A : Type} (t1 t2 : tactic A) : tactic A := tactic_value
-definition repeat_tac {A : Type} (t : tactic A) : tactic A := tactic_value
-definition now_tac    {A : Type} : tactic A := tactic_value
-definition exact_tac  {A : Type} : tactic A := tactic_value
-definition state_tac  {A : Type} : tactic A := tactic_value
-definition fail_tac   {A : Type} : tactic A := tactic_value
-definition id_tac     {A : Type} : tactic A := tactic_value
-definition beta_tac   {A : Type} : tactic A := tactic_value
-definition apply      {A : Type} {B : Type} (b : B) : tactic A := tactic_value
-definition unfold_tac {A : Type} {B : Type} (b : B) : tactic A := tactic_value
+-- a term of type 'tactic' into a tactic that sythesizes a term
+definition then_tac   (t1 t2 : tactic) : tactic := tactic_value
+definition orelse_tac (t1 t2 : tactic) : tactic := tactic_value
+definition repeat_tac (t : tactic) : tactic := tactic_value
+definition now_tac    : tactic := tactic_value
+definition exact_tac  : tactic := tactic_value
+definition state_tac  : tactic := tactic_value
+definition fail_tac   : tactic := tactic_value
+definition id_tac     : tactic := tactic_value
+definition beta_tac   : tactic := tactic_value
+definition apply      {B : Type} (b : B) : tactic := tactic_value
+definition unfold_tac {B : Type} (b : B) : tactic := tactic_value
 
 infixl `;`:200         := then_tac
 infixl `|`:100         := orelse_tac
 notation `!`:max t:max := repeat_tac t
 
-
diff --git a/src/library/tactic/expr_to_tactic.cpp b/src/library/tactic/expr_to_tactic.cpp
index 77b70ac38..347657382 100644
--- a/src/library/tactic/expr_to_tactic.cpp
+++ b/src/library/tactic/expr_to_tactic.cpp
@@ -49,21 +49,31 @@ tactic expr_to_tactic(environment const & env, expr const & e, pos_info_provider
 }
 
 register_simple_tac::register_simple_tac(name const & n, std::function<tactic()> f) {
-    register_expr_to_tactic(n, [=](environment const &, expr const &, pos_info_provider const *) {
+    register_expr_to_tactic(n, [=](environment const &, expr const & e, pos_info_provider const *) {
+            if (!is_constant(e))
+                throw exception("invalid constant tactic");
             return f();
         });
 }
 
 register_bin_tac::register_bin_tac(name const & n, std::function<tactic(tactic const &, tactic const &)> f) {
     register_expr_to_tactic(n, [=](environment const & env, expr const & e, pos_info_provider const * p) {
-            return f(expr_to_tactic(env, app_arg(app_fn(e)), p),
-                     expr_to_tactic(env, app_arg(e), p));
+            buffer<expr> args;
+            get_app_args(e, args);
+            if (args.size() != 2)
+                throw exception("invalid binary tactic, it must have two arguments");
+            return f(expr_to_tactic(env, args[0], p),
+                     expr_to_tactic(env, args[1], p));
         });
 }
 
 register_unary_tac::register_unary_tac(name const & n, std::function<tactic(tactic const &)> f) {
     register_expr_to_tactic(n, [=](environment const & env, expr const & e, pos_info_provider const * p) {
-            return f(expr_to_tactic(env, app_arg(e), p));
+            buffer<expr> args;
+            get_app_args(e, args);
+            if (args.size() != 1)
+                throw exception("invalid unary tactic, it must have one argument");
+            return f(expr_to_tactic(env, args[0], p));
         });
 }
 
diff --git a/tests/lean/run/tactic4.lean b/tests/lean/run/tactic4.lean
index e269fee89..97d0de97c 100644
--- a/tests/lean/run/tactic4.lean
+++ b/tests/lean/run/tactic4.lean
@@ -2,7 +2,7 @@ import standard
 
 definition id {A : Type} (a : A) := a
 
-definition simple_tac {A : Bool} : tactic A
+definition simple_tac {A : Bool} : tactic
 := unfold_tac @id.{1}; exact_tac
 
 theorem tst {A B : Bool} (H1 : A) (H2 : B) : id A