gistfile1.txt

meta inductive expr_lens
| app_fun : expr_lens → expr → expr_lens
| app_arg : expr_lens → expr → expr_lens
| entire  : expr_lens

open expr_lens

meta def expr_lens.replace : expr_lens → expr → expr
| (app_fun l f) x := expr_lens.replace l (expr.app f x)
| (app_arg l x) f := expr_lens.replace l (expr.app f x)
| entire        e := e 

meta def expr_lens.congr : expr_lens → expr → tactic expr
| (app_fun l f) x_eq := do fx_eq ← mk_congr_arg f x_eq,
                                    expr_lens.congr l fx_eq
| (app_arg l x) f_eq := do fx_eq ← mk_congr_fun f_eq x,
                                    expr_lens.congr l fx_eq
| entire                  e_eq := pure e_eq

meta def rewrite_fold_aux {α} (F : expr_lens → expr → α → tactic α) : expr_lens → expr → α → tactic α 
| l e a := (do a' ← F l e a,
              match e with
              | (expr.app f x) := do a_f ← rewrite_fold_aux (expr_lens.app_arg l x) f a',
                                            rewrite_fold_aux (expr_lens.app_fun l f) x a_f
              | _ := pure a'
              end) <|> pure a
. 

meta def rewrite_fold {α} (F : expr_lens → expr → α → tactic α) (e : expr) (a : α) : tactic α := rewrite_fold_aux F expr_lens.entire e a

meta def rewrite_F (r : expr × bool) (l : expr_lens) (e : expr) (state : list (expr × expr)) : tactic (list (expr × expr)) := 
do 
  e_pp ← pretty_print e,
  r_pp ← pretty_print r.1,
  let r_pp := (if r.2 then "← " else "") ++ r_pp,
  -- tactic.trace format!"rewriting at {e_pp} via {r_pp}",
  (v, pr) ← rewrite_without_new_mvars r.1 e {symm := r.2},
  -- Now we determine whether the rewrite transforms the entire expression or not:
  (do 
    (w, qr) ← rewrite_entire r e,
    w_pp ← pretty_print w,
    -- tactic.trace format!"success (entire expression): {w_pp}",
    let w' := l.replace w,
    qr' ← l.congr qr | (do w_pp ← pretty_print w, qr_pp ← pretty_print qr, tactic.trace format!"lens congr failed: {w_pp} {qr_pp}"),
    -- tactic.trace "..",
    pure ((w', qr') :: state)
  ) <|>
  (do
    v_pp ← pretty_print v,
    -- tactic.trace format!"success (subexpression): {v_pp}",
    -- tactic.trace ".",
    pure (state)
  )

def remove_adjacent_duplicates {α β} (f : α → β) [decidable_eq β] : list α → list α
| (x :: y :: t) := if f x = f y then
                     remove_adjacent_duplicates (y :: t)
                   else
                     x :: (remove_adjacent_duplicates (y :: t))
| [x] := [x]
| [] := []

meta def all_rewrites (r : expr × bool) (e : expr) : tactic (list (expr × expr)) :=
do 
  --  pp ← pretty_print e,
   results ← rewrite_fold (rewrite_F r) e [],
   let results : list (expr × expr) := remove_adjacent_duplicates (λ p, p.1) results,
  --  results_pp ← results.mmap(λ p, pretty_print p.1),
  --  r_pp ← pretty_print r.1,
  --  let r_pp := (if r.2 then "← " else "") ++ r_pp,
  --  tactic.trace format!"⟫ finding all rewrites of {pp} via {r_pp}",
  --  results_pp.mmap'(λ r, tactic.trace format!"⟫⟫ {r}"),
   pure results