chore(library/init/meta): remove @[derive] and mk_has_reflect_instance
This commit is contained in:
Leonardo de Moura
parent
0aceeaf307
commit
ead68376b7
4 changed files with 2 additions and 172 deletions
|
|
@ -9,7 +9,7 @@ import init.meta.level init.meta.expr init.meta.environment init.meta.attribute
|
|||
import init.meta.tactic init.meta.contradiction_tactic init.meta.constructor_tactic
|
||||
import init.meta.injection_tactic init.meta.relation_tactics init.meta.fun_info
|
||||
import init.meta.congr_lemma init.meta.match_tactic init.meta.rewrite_tactic
|
||||
import init.meta.derive init.meta.simp_tactic init.meta.set_get_option_tactics
|
||||
import init.meta.simp_tactic init.meta.set_get_option_tactics
|
||||
import init.meta.interactive
|
||||
import init.meta.comp_value_tactics
|
||||
import init.meta.congr_tactic
|
||||
|
|
|
|||
|
|
@ -1,86 +0,0 @@
|
|||
/-
|
||||
Copyright (c) 2017 Microsoft Corporation. All rights reserved.
|
||||
Released under Apache 2.0 license as described in the file LICENSE.
|
||||
Authors: Sebastian Ullrich
|
||||
|
||||
Attribute that can automatically derive typeclass instances.
|
||||
-/
|
||||
prelude
|
||||
import init.meta.attribute
|
||||
import init.meta.interactive_base
|
||||
import init.meta.mk_has_reflect_instance
|
||||
|
||||
open lean3
|
||||
open interactive.types
|
||||
open tactic
|
||||
|
||||
/-- A handler that may or may not be able to implement the typeclass `cls` for `decl`.
|
||||
It should return `tt` if it was able to derive `cls` and `ff` if it does not know
|
||||
how to derive `cls`, in which case lower-priority handlers will be tried next. -/
|
||||
meta def derive_handler := Π (cls : pexpr) (decl : name), tactic bool
|
||||
|
||||
@[user_attribute]
|
||||
meta def derive_handler_attr : user_attribute :=
|
||||
{ name := `derive_handler, descr := "register a definition of type `derive_handler` for use in the [derive] attribute" }
|
||||
|
||||
private meta def try_handlers (p : pexpr) (n : name) : list derive_handler → tactic unit
|
||||
| [] := fail format!"failed to find a derive handler for '{p}'"
|
||||
| (h::hs) :=
|
||||
do success ← h p n,
|
||||
when (¬success) $
|
||||
try_handlers hs
|
||||
|
||||
@[user_attribute] meta def derive_attr : user_attribute unit (list pexpr) :=
|
||||
{ name := `derive, descr := "automatically derive typeclass instances",
|
||||
parser := pexpr_list_or_texpr,
|
||||
after_set := some (λ n _ _,
|
||||
do ps ← derive_attr.get_param n,
|
||||
handlers ← attribute.get_instances `derive_handler,
|
||||
handlers ← handlers.mmap (λ n, eval_expr derive_handler (expr.const n [])),
|
||||
ps.mmap' (λ p, try_handlers p n handlers)) }
|
||||
|
||||
/-- Given a tactic `tac` that can solve an application of `cls` in the right context,
|
||||
`instance_derive_handler` uses it to build an instance declaration of `cls n`. -/
|
||||
meta def instance_derive_handler (cls : name) (tac : tactic unit) (univ_poly := tt)
|
||||
(modify_target : name → list expr → expr → tactic expr := λ _ _, pure) : derive_handler :=
|
||||
λ p n,
|
||||
if p.is_constant_of cls then
|
||||
do decl ← get_decl n,
|
||||
cls_decl ← get_decl cls,
|
||||
env ← get_env,
|
||||
guard (env.is_inductive n) <|> fail format!"failed to derive '{cls}', '{n}' is not an inductive type",
|
||||
let ls := decl.univ_params.map $ λ n, if univ_poly then level.param n else level.zero,
|
||||
-- incrementally build up target expression `Π (hp : p) [cls hp] ..., cls (n.{ls} hp ...)`
|
||||
-- where `p ...` are the inductive parameter types of `n`
|
||||
let tgt : expr := expr.const n ls,
|
||||
⟨params, _⟩ ← mk_local_pis (decl.type.instantiate_univ_params (decl.univ_params.zip ls)),
|
||||
let tgt := tgt.mk_app params,
|
||||
tgt ← mk_app cls [tgt],
|
||||
tgt ← modify_target n params tgt,
|
||||
tgt ← params.enum.mfoldr (λ ⟨i, param⟩ tgt,
|
||||
do -- add typeclass hypothesis for each inductive parameter
|
||||
tgt ← do {
|
||||
guard $ i < env.inductive_num_params n,
|
||||
param_cls ← mk_app cls [param],
|
||||
-- TODO(sullrich): omit some typeclass parameters based on usage of `param`?
|
||||
pure $ expr.pi `a binder_info.inst_implicit param_cls tgt
|
||||
} <|> pure tgt,
|
||||
pure $ tgt.bind_pi param
|
||||
) tgt,
|
||||
(_, val) ← tactic.solve_aux tgt (intros >> tac),
|
||||
val ← instantiate_mvars val,
|
||||
let trusted := decl.is_trusted ∧ cls_decl.is_trusted,
|
||||
add_decl (declaration.defn (n ++ cls)
|
||||
(if univ_poly then decl.univ_params else [])
|
||||
tgt val reducibility_hints.abbrev trusted),
|
||||
set_basic_attribute `instance (n ++ cls) tt,
|
||||
pure true
|
||||
else pure false
|
||||
|
||||
@[derive_handler] meta def has_reflect_derive_handler :=
|
||||
instance_derive_handler ``has_reflect mk_has_reflect_instance ff (λ n params tgt,
|
||||
-- add additional `reflected` assumption for each parameter
|
||||
params.mfoldr (λ param tgt,
|
||||
do param_cls ← mk_app `reflected [param],
|
||||
pure $ expr.pi `a binder_info.inst_implicit param_cls tgt
|
||||
) tgt)
|
||||
|
|
@ -6,7 +6,7 @@ Authors: Leonardo de Moura
|
|||
prelude
|
||||
import init.meta.tactic init.meta.rewrite_tactic init.meta.simp_tactic
|
||||
import init.control.combinators
|
||||
import init.meta.interactive_base init.meta.derive init.meta.match_tactic
|
||||
import init.meta.interactive_base init.meta.match_tactic
|
||||
import init.meta.congr_tactic
|
||||
|
||||
open lean3
|
||||
|
|
|
|||
|
|
@ -1,84 +0,0 @@
|
|||
/-
|
||||
Copyright (c) 2017 Microsoft Corporation. All rights reserved.
|
||||
Released under Apache 2.0 license as described in the file LICENSE.
|
||||
Authors: Sebastian Ullrich
|
||||
|
||||
Helper tactic for constructing a has_reflect instance.
|
||||
-/
|
||||
prelude
|
||||
import init.meta.rec_util
|
||||
|
||||
namespace tactic
|
||||
open expr environment list
|
||||
|
||||
/- Retrieve the name of the type we are building a has_reflect instance for. -/
|
||||
private meta def get_has_reflect_type_name : tactic name :=
|
||||
do {
|
||||
(app (const n ls) t) ← target,
|
||||
when (n ≠ `has_reflect) failed,
|
||||
(const I ls) ← return (get_app_fn t),
|
||||
return I }
|
||||
<|>
|
||||
fail "mk_has_reflect_instance tactic failed, target type is expected to be of the form (has_reflect ...)"
|
||||
|
||||
/- Try to synthesize constructor argument using type class resolution -/
|
||||
private meta def mk_has_reflect_instance_for (a : expr) : tactic expr :=
|
||||
do t ← infer_type a,
|
||||
do {
|
||||
m ← mk_app `reflected [a],
|
||||
inst ← mk_instance m
|
||||
<|> do {
|
||||
f ← pp t,
|
||||
fail (to_fmt "mk_has_reflect_instance failed, failed to generate instance for" ++ format.nest 2 (format.line ++ f))
|
||||
},
|
||||
mk_app `reflect [a, inst] }
|
||||
|
||||
/- Synthesize (recursive) instances of `reflected` for all fields -/
|
||||
private meta def mk_reflect : name → name → list name → nat → tactic (list expr)
|
||||
| I_name F_name [] num_rec := return []
|
||||
| I_name F_name (fname::fnames) num_rec := do
|
||||
field ← get_local fname,
|
||||
rec ← is_type_app_of field I_name,
|
||||
quote ← if rec then mk_brec_on_rec_value F_name num_rec else mk_has_reflect_instance_for field,
|
||||
quotes ← mk_reflect I_name F_name fnames (if rec then num_rec + 1 else num_rec),
|
||||
return (quote :: quotes)
|
||||
|
||||
/- Solve the subgoal for constructor `F_name` -/
|
||||
private meta def has_reflect_case (I_name F_name : name) (field_names : list name) : tactic unit :=
|
||||
do field_quotes ← mk_reflect I_name F_name field_names 0,
|
||||
-- fn should be of the form `F_name ps fs`, where ps are the inductive parameter arguments,
|
||||
-- and `fs.length = field_names.length`
|
||||
`(reflected %%fn) ← target,
|
||||
-- `reflected (F_name ps)` should be synthesizable directly, using instances from the context
|
||||
let fn := field_names.foldl (λ fn _, expr.app_fn fn) fn,
|
||||
quote ← mk_app `reflected [fn] >>= mk_instance,
|
||||
-- now extend to an instance of `reflected (F_name ps fs)`
|
||||
quote ← field_quotes.mfoldl (λ quote fquote, to_expr ``(reflected.subst %%quote %%fquote)) quote,
|
||||
exact quote
|
||||
|
||||
private meta def for_each_has_reflect_goal : name → name → list (list name) → tactic unit
|
||||
| I_name F_name [] := done <|> fail "mk_has_reflect_instance failed, unexpected number of cases"
|
||||
| I_name F_name (ns::nss) := do
|
||||
solve1 (has_reflect_case I_name F_name ns),
|
||||
for_each_has_reflect_goal I_name F_name nss
|
||||
|
||||
/-- Solves a goal of the form `has_reflect α` where α is an inductive type.
|
||||
Needs to synthesize a `reflected` instance for each inductive parameter type of α
|
||||
and for each constructor parameter of α. -/
|
||||
meta def mk_has_reflect_instance : tactic unit :=
|
||||
do I_name ← get_has_reflect_type_name,
|
||||
env ← get_env,
|
||||
v_name : name ← return `_v,
|
||||
F_name : name ← return `_F,
|
||||
guard (env.inductive_num_indices I_name = 0) <|>
|
||||
fail "mk_has_reflect_instance failed, indexed families are currently not supported",
|
||||
-- Use brec_on if type is recursive.
|
||||
-- We store the functional in the variable F.
|
||||
if is_recursive env I_name
|
||||
then intro `_v >>= (λ x, induction x [v_name, F_name] (some $ I_name <.> "brec_on") >> return ())
|
||||
else intro v_name >> return (),
|
||||
arg_names : list (list name) ← mk_constructors_arg_names I_name `_p,
|
||||
get_local v_name >>= λ v, cases v (join arg_names),
|
||||
for_each_has_reflect_goal I_name F_name arg_names
|
||||
|
||||
end tactic
|
||||
Loading…
Add table
Reference in a new issue