`structure_helper` tactic

structure_helper.lean

import data.string
import tactic.core

namespace tactic

private meta def attempt_instance_build (n : name) (ns : list name) : tactic unit :=
do sorries ← ns.mmap $ λ _, to_pexpr <$> mk_sorry,
   let s : structure_instance_info := {
       struct := some n,
       field_names := ns,
       field_values := sorries,
   },
   to_expr $ pexpr.mk_structure_instance s,
   tactic.skip

private meta def capture_failure_message (tac : tactic unit) : tactic (option string) := λ s,
match tac s with
  | result.success a s'              := result.success none s
  | result.exception (some msg) _ s' := result.success (to_string $ msg ()) s
  | result.exception none pos s'     := result.exception (some $ λ _, format!"no fail msg") pos s
end

private meta def find_explicit_constructor_args_core (n : name)
  : list name → tactic (list name)
| ns :=
do msg ← capture_failure_message $ attempt_instance_build n ns,
   do { msg ← msg,
        newn ← (msg.split_on '\'').nth 1,
        find_explicit_constructor_args_core (newn :: ns)
   } <|> return ns

meta def find_explicit_structure_args (n : name) : tactic (list name) :=
do env ← get_env,
   match env.structure_fields n with
   | none := fail format!"'{n}' not a structure!"
   | some _ := list.reverse <$> find_explicit_constructor_args_core n []
   end

meta inductive constructor_arg
| default (n : name)
| implicit
| auto (tac : tactic unit)
| opt (v : expr)

namespace constructor_arg

meta def to_tactic_format : constructor_arg → tactic format
| (default n) := pure format!"(default {n})"
| (implicit) := pure format!"(implicit)"
| (auto tac) := pure format!"(auto)"
| (opt v) := do v ← pp v, pure format!"(opt {v})"

meta instance : has_to_tactic_format constructor_arg := ⟨to_tactic_format⟩

meta def classify (n : name) : binder_info → expr → tactic constructor_arg
| binder_info.default `(opt_param %%t %%v) := return $ constructor_arg.opt v
| binder_info.default `(auto_param %%t %%tac) :=
  do tac ← eval_expr name tac,
     tac ← resolve_name tac >>= to_expr >>= eval_expr (tactic unit),
     return $ constructor_arg.auto tac
| binder_info.default e := return $ constructor_arg.default n
| _ _ := return constructor_arg.implicit

meta def name_permutor := name → tactic unit

namespace name_permutor

meta def id (n : name) : tactic unit :=
applyc n

meta def has : name → tactic unit
| (name.mk_string str head) := applyc $ (head.mk_string $ "has_" ++ str).mk_string str
| _ := failed

meta def nspace (n : name) : tactic unit :=
do ns :: _ ← open_namespaces,
   applyc (ns ++ n)

meta def resolve (n : name) : tactic unit :=
resolve_name n >>= to_expr >>= apply >> skip

meta def permutors := [
  id,
  has,
  nspace,
  resolve
]

end name_permutor

private meta def dispatch_via_name_guess_core (n : name) : list name_permutor → tactic unit
| [] := fail format!"could not fill field {n}"
| (t :: rest) := t n <|> dispatch_via_name_guess_core rest

meta def dispatch_via_name_guess (n : name) : tactic unit :=
dispatch_via_name_guess_core n name_permutor.permutors

private meta def dispatch_core : constructor_arg → tactic unit
| (implicit)  := skip
| (auto tac)  := tac
| (opt v)     := exact v
| (default n) := dispatch_via_name_guess n

meta def dispatch (a : constructor_arg) : tactic unit :=
focus1 (dispatch_core a)

end constructor_arg

meta def parse_constructor_args : expr → tactic (list constructor_arg)
| (expr.pi n bi t b) :=
  do m ← mk_meta_var t,
     h ← constructor_arg.classify n bi t,
     list.cons h <$> parse_constructor_args (b.instantiate_var m)
| _ := return []

end tactic

namespace environment

meta def get_constructor_type (e : environment) (n : name) : tactic expr :=
do r ← e.get n,
   match r with
   | declaration.cnst _ _ t _ := pure t
   | _ := tactic.fail "not a constructor"
   end

end environment

namespace tactic

meta def instantiate_with_minimal (n : name) : tactic unit :=
do l ← find_explicit_structure_args n,
   let placeholders := l.map $ λ _, pexpr.mk_placeholder,
   let s : structure_instance_info := {
       struct := n,
       field_names := l,
       field_values := placeholders,
   },
   tactic.refine $ pexpr.mk_structure_instance s

meta def structure_helper : tactic unit :=
do t ← target,
   env ← get_env,
   match t with
   | expr.app (expr.const sn _) e :=
     match env.structure_fields sn with
     | some l :=
       do tactic.fsplit,
          ty ← env.get_constructor_type (sn ++ `mk),
          args ← parse_constructor_args ty,
          args.mmap' constructor_arg.dispatch
     | none := fail "goal not a structure"
     end
   | _ := fail "unsupported goal"
end

run_cmd add_interactive [`structure_helper]

end tactic