guess_functor.lean

import category_theory.functor
import category_theory.products

open category_theory

namespace tactic.interactive
open tactic
open interactive interactive.types lean lean.parser parser

meta def go (fvar : expr) : pexpr → tactic expr
| (expr.var 0) := return fvar
| (expr.app (expr.app (expr.const ``prod.mk _) e₁) e₂) := do
  m₁ ← go e₁,
  m₂ ← go e₂,
  to_expr ``((%%m₁, %%m₂))
| (expr.app f e) := do
  f' ← to_expr f,
  ft ← infer_type f',
  -- should fall back to something else if this match fails
  `(@category_theory.functor.{0 0 0 0} %%c %%catc %%d %%catd) ← infer_type f',
  m ← go e,
  to_expr ``((%%f').map %%m)
| e := do
  e' ← to_expr e,
  to_expr ``(category.id.{0 0} %%e')

meta def guess_functor_core : pexpr → tactic expr
| (expr.lam var _ t body) := do
    t' ← to_expr t,
    xvar ← mk_local' "X" binder_info.default t',
    yvar ← mk_local' "Y" binder_info.default t',
    tcvar ← mk_mvar,
    map_var ← mk_local' "f" binder_info.default `(@category.hom.{0 0} %%t' %%tcvar %%xvar %%yvar),
    map_body ← go map_var body,
    map_fun ← lambdas [map_var] map_body,
    lambdas [xvar, yvar] map_fun
| e := fail "not a lambda"

meta def guess_functor (p : parse texpr) : tactic unit :=
do p' ← guess_functor_core p,
   exact ``({ category_theory.functor .
     obj := %%p,
     map' := %%p',
     map_id' := by tidy,
     map_comp' := by tidy })

end tactic.interactive


infixr ` ↝ `:80 := functor
variables {C : Type} [small_category C]
variables {F : C ↝ C} {Z : C}
include F Z

def myfun : C ↝ (C × C) := by guess_functor (λ x, (F (F x), Z))
#print myfun
.