From 5ca18b8d2ed907bd602ba41e67c7e73776dd1892 Mon Sep 17 00:00:00 2001
From: Leonardo de Moura <leonardo@microsoft.com>
Date: Sat, 11 Feb 2017 16:52:06 -0800
Subject: [PATCH] feat(library/init/meta): add helper functions

---
 library/init/category/alternative.lean |  6 +++++
 library/init/meta/expr.lean            |  6 +++++
 library/init/meta/tactic.lean          | 31 +++++++++++++++++---------
 src/library/vm/vm_expr.cpp             | 10 +++++++--
 4 files changed, 41 insertions(+), 12 deletions(-)

diff --git a/library/init/category/alternative.lean b/library/init/category/alternative.lean
index bd0a3d4aae..d42db96782 100644
--- a/library/init/category/alternative.lean
+++ b/library/init/category/alternative.lean
@@ -21,3 +21,9 @@ infixr ` <|> `:2 := orelse
 
 @[inline] def guard {f : Type → Type v} [alternative f] (p : Prop) [decidable p] : f unit :=
 if p then pure () else failure
+
+/- Later we define a coercion from bool to Prop, but this version will still be useful.
+   Given (t : tactic bool), we can write t >>= guardb -/
+@[inline] def guardb {f : Type → Type v} [alternative f] : bool → f unit
+| tt := pure ()
+| ff := failure
diff --git a/library/init/meta/expr.lean b/library/init/meta/expr.lean
index 00d61ace36..dfbaf77139 100644
--- a/library/init/meta/expr.lean
+++ b/library/init/meta/expr.lean
@@ -90,6 +90,8 @@ meta constant expr.is_internal_cnstr : expr → option unsigned
 meta constant expr.get_nat_value : expr → option nat
 
 meta constant expr.collect_univ_params : expr → list name
+/-- `occurs e t` returns `tt` iff `e` occurs in `t` -/
+meta constant expr.occurs        : expr → expr → bool
 
 namespace expr
 open decidable
@@ -109,6 +111,10 @@ meta constant mk_sorry (type : expr) : expr
 /-- Checks whether e is sorry, and returns its type. -/
 meta constant is_sorry (e : expr) : option expr
 
+meta def is_var : expr → bool
+| (var _) := tt
+| _       := ff
+
 meta def app_of_list : expr → list expr → expr
 | f []      := f
 | f (p::ps) := app_of_list (f p) ps
diff --git a/library/init/meta/tactic.lean b/library/init/meta/tactic.lean
index 58ba11fbc3..64e7e6d8b4 100644
--- a/library/init/meta/tactic.lean
+++ b/library/init/meta/tactic.lean
@@ -115,27 +115,22 @@ end
 namespace tactic
 variables {α : Type u}
 
-meta def try_core (t : tactic α) : tactic bool :=
+meta def try_core (t : tactic α) : tactic (option α) :=
 λ s, tactic_result.cases_on (t s)
- (λ a, success tt)
- (λ e ref s', success ff s)
+ (λ a, success (some a))
+ (λ e ref s', success none s)
 
 meta def skip : tactic unit :=
 success ()
 
 meta def try (t : tactic α) : tactic unit :=
-try_core t >> skip
+try_core t >>[tactic] skip
 
 meta def fail_if_success {α : Type u} (t : tactic α) : tactic unit :=
 λ s, tactic_result.cases_on (t s)
  (λ a s, mk_exception "fail_if_success combinator failed, given tactic succeeded" none s)
  (λ e ref s', success () s)
 
-open list
-meta def foreach : list α → (α → tactic unit) → tactic unit
-| []      fn := skip
-| (e::es) fn := do fn e, foreach es fn
-
 open nat
 /- (repeat_at_most n t): repeat the given tactic at most n times or until t fails -/
 meta def repeat_at_most : nat → tactic unit → tactic unit
@@ -743,7 +738,7 @@ private meta def any_goals_core (tac : tactic unit) : list expr → list expr 
   do set_goals [g],
      succeeded ← try_core tac,
      new_gs    ← get_goals,
-     any_goals_core gs (ac ++ new_gs) (succeeded || progress)
+     any_goals_core gs (ac ++ new_gs) (succeeded^.is_some || progress)
 
 /- Apply the given tactic to any goal where it succeeds. The tactic succeeds only if
    tac succeeds for at least one goal. -/
@@ -972,6 +967,22 @@ meta def list_name.to_expr : list name → tactic expr
 notation [parsing_only] `command`:max := tactic unit
 
 open tactic
+
+namespace list
+
+meta def for_each {α} : list α → (α → tactic unit) → tactic unit
+| []      fn := skip
+| (e::es) fn := do fn e, for_each es fn
+
+meta def any_of {α β} : list α → (α → tactic β) → tactic β
+| []      fn := failed
+| (e::es) fn := do opt_b ← try_core (fn e),
+                   match opt_b with
+                   | some b := return b
+                   | none   := any_of es fn
+                   end
+end list
+
 /-
   Define id_locked using meta-programming because we don't have
   syntax for setting reducibility_hints.
diff --git a/src/library/vm/vm_expr.cpp b/src/library/vm/vm_expr.cpp
index 231c7375dc..b07c73a230 100644
--- a/src/library/vm/vm_expr.cpp
+++ b/src/library/vm/vm_expr.cpp
@@ -6,14 +6,15 @@ Author: Leonardo de Moura
 */
 #include <string>
 #include <iostream>
-#include "library/locals.h"
-#include "library/sorry.h"
 #include "kernel/expr.h"
 #include "kernel/free_vars.h"
 #include "kernel/instantiate.h"
 #include "kernel/abstract.h"
 #include "kernel/for_each_fn.h"
 #include "kernel/replace_fn.h"
+#include "library/locals.h"
+#include "library/sorry.h"
+#include "library/util.h"
 #include "library/expr_lt.h"
 #include "library/deep_copy.h"
 #include "library/comp_val.h"
@@ -428,6 +429,10 @@ vm_obj expr_is_sorry(vm_obj const & e_) {
     return to_obj(is_sorry(e) ? some(sorry_type(e)) : none_expr());
 }
 
+vm_obj expr_occurs(vm_obj const & e1, vm_obj const & e2) {
+    return mk_vm_bool(occurs(to_expr(e1), to_expr(e2)));
+}
+
 void initialize_vm_expr() {
     DECLARE_VM_BUILTIN(name({"expr", "var"}),              expr_var);
     DECLARE_VM_BUILTIN(name({"expr", "sort"}),             expr_sort);
@@ -461,6 +466,7 @@ void initialize_vm_expr() {
     DECLARE_VM_BUILTIN(name({"expr", "lower_vars"}),       expr_lower_vars);
     DECLARE_VM_BUILTIN(name({"expr", "hash"}),             expr_hash);
     DECLARE_VM_BUILTIN(name({"expr", "copy_pos_info"}),    expr_copy_pos_info);
+    DECLARE_VM_BUILTIN(name({"expr", "occurs"}),           expr_occurs);
     DECLARE_VM_BUILTIN(name({"expr", "collect_univ_params"}), expr_collect_univ_params);
     DECLARE_VM_CASES_BUILTIN(name({"expr", "cases_on"}),   expr_cases_on);