From 4d1c4aee0317dbb10cffbcd2274efe1801713f13 Mon Sep 17 00:00:00 2001 From: Sebastian Ullrich Date: Fri, 8 Sep 2017 19:36:18 +0200 Subject: [PATCH] feat(init/meta/mk_has_reflect_instance): add derive_handler for has_reflect --- library/init/meta/declaration.lean | 5 ++ library/init/meta/default.lean | 2 +- library/init/meta/derive.lean | 27 +++++-- library/init/meta/expr.lean | 21 ++++-- library/init/meta/has_reflect.lean | 23 +----- library/init/meta/interactive.lean | 17 +---- library/init/meta/interactive_base.lean | 4 - library/init/meta/mk_dec_eq_instance.lean | 3 + .../init/meta/mk_has_reflect_instance.lean | 73 +++++++++++++++++++ library/init/meta/smt/ematch.lean | 2 +- library/init/meta/vm.lean | 2 +- 11 files changed, 125 insertions(+), 54 deletions(-) create mode 100644 library/init/meta/mk_has_reflect_instance.lean diff --git a/library/init/meta/declaration.lean b/library/init/meta/declaration.lean index fc75f7bbae..22361c54e1 100644 --- a/library/init/meta/declaration.lean +++ b/library/init/meta/declaration.lean @@ -89,6 +89,11 @@ meta def value_task : declaration → task expr | (thm _ _ _ v) := v | _ := task.pure (default expr) +meta def is_trusted : declaration → bool +| (defn _ _ _ _ _ t) := t +| (cnst _ _ _ t) := t +| _ := tt + meta def update_type : declaration → expr → declaration | (defn n ls t v h tr) new_t := defn n ls new_t v h tr | (thm n ls t v) new_t := thm n ls new_t v diff --git a/library/init/meta/default.lean b/library/init/meta/default.lean index 081587fc60..5c414296ea 100644 --- a/library/init/meta/default.lean +++ b/library/init/meta/default.lean @@ -10,7 +10,7 @@ import init.meta.tactic init.meta.contradiction_tactic init.meta.constructor_tac import init.meta.injection_tactic init.meta.relation_tactics init.meta.fun_info import init.meta.congr_lemma init.meta.match_tactic init.meta.ac_tactics import init.meta.backward init.meta.rewrite_tactic -import init.meta.derive +import init.meta.derive init.meta.mk_dec_eq_instance import init.meta.simp_tactic init.meta.set_get_option_tactics import init.meta.interactive init.meta.converter init.meta.vm import init.meta.comp_value_tactics init.meta.smt diff --git a/library/init/meta/derive.lean b/library/init/meta/derive.lean index a1e8fde559..776a8e1b34 100644 --- a/library/init/meta/derive.lean +++ b/library/init/meta/derive.lean @@ -8,7 +8,7 @@ Attribute that can automatically derive typeclass instances. prelude import init.meta.attribute import init.meta.interactive_base -import init.meta.mk_dec_eq_instance +import init.meta.mk_has_reflect_instance import init.meta.mk_has_sizeof_instance import init.meta.mk_inhabited_instance @@ -41,18 +41,21 @@ do success ← h p n, handlers ← handlers.mmap (λ n, eval_expr derive_handler (expr.const n [])), ps.mmap' (λ p, try_handlers p n handlers)) } -meta def instance_derive_handler (cls : name) (tac : tactic unit) : derive_handler := +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 tgt : expr := expr.const n (decl.univ_params.map level.param), - ⟨params, _⟩ ← mk_local_pis decl.type, + let ls := decl.univ_params.map $ λ n, if univ_poly then level.param n else level.zero, + let tgt : expr := expr.const n ls, + ⟨params, _⟩ ← mk_local_pis (decl.type.instantiate_univ_params (decl.univ_params.zip ls)), let params := params.take (env.inductive_num_params n), let tgt := tgt.mk_app params, tgt ← mk_app cls [tgt], + tgt ← modify_target n params tgt, tgt ← params.mfoldr (λ param tgt, do param_cls ← mk_app cls [param], -- TODO(sullrich): omit some typeclass parameters based on usage of `param`? @@ -62,16 +65,26 @@ do decl ← get_decl n, (_, 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) decl.univ_params tgt val reducibility_hints.abbrev 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 decidable_eq_derive_handler := -instance_derive_handler ``decidable_eq mk_dec_eq_instance +@[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], + let tgt := expr.pi `a binder_info.inst_implicit param_cls tgt, + pure $ tgt +) tgt) @[derive_handler] meta def has_sizeof_derive_handler := instance_derive_handler ``has_sizeof mk_has_sizeof_instance @[derive_handler] meta def inhabited_derive_handler := instance_derive_handler ``inhabited mk_inhabited_instance + +attribute [derive has_reflect] bool prod sum option interactive.loc pos diff --git a/library/init/meta/expr.lean b/library/init/meta/expr.lean index f72b4fb86f..48f265ba30 100644 --- a/library/init/meta/expr.lean +++ b/library/init/meta/expr.lean @@ -141,7 +141,7 @@ meta constant expr.has_local_in : expr → name_set → bool The quotation expression `(a) (outside of patterns) is equivalent to `reflect a` and thus can be used as an explicit way of inferring an instance of `reflected a`. -/ -meta def reflected {α : Sort u} : α → Type := +@[class] meta def reflected {α : Sort u} : α → Type := λ _, expr @[inline] meta def reflected.to_expr {α : Sort u} {a : α} : reflected a → expr := @@ -154,17 +154,15 @@ id | _ := expr.app ef ea end -meta constant expr.reflect (e : expr elab) : reflected e -meta constant string.reflect (s : string) : reflected s - -attribute [class] reflected -attribute [instance] expr.reflect string.reflect attribute [irreducible] reflected reflected.subst reflected.to_expr +@[instance] protected meta constant expr.reflect (e : expr elab) : reflected e +@[instance] protected meta constant string.reflect (s : string) : reflected s + @[inline] meta instance {α : Sort u} (a : α) : has_coe (reflected a) expr := ⟨reflected.to_expr⟩ -meta def reflect {α : Sort u} (a : α) [h : reflected a] : reflected a := h +protected meta def reflect {α : Sort u} (a : α) [h : reflected a] : reflected a := h meta instance {α} (a : α) : has_to_format (reflected a) := ⟨λ h, to_fmt h.to_expr⟩ @@ -232,6 +230,15 @@ meta def mk_app : expr → list expr → expr | e [] := e | e (x::xs) := mk_app (e x) xs +meta def mk_binding (ctor : name → binder_info → expr → expr → expr) (e : expr) : Π (l : expr), expr +| (local_const n pp_n bi ty) := ctor pp_n bi ty (e.abstract_local n) +| _ := e + +/-- (bind_pi e l) abstracts and pi-binds the local `l` in `e` -/ +meta def bind_pi := mk_binding pi +/-- (bind_lambda e l) abstracts and lambda-binds the local `l` in `e` -/ +meta def bind_lambda := mk_binding lam + meta def ith_arg_aux : expr → nat → expr | (app f a) 0 := a | (app f a) (n+1) := ith_arg_aux f n diff --git a/library/init/meta/has_reflect.lean b/library/init/meta/has_reflect.lean index fe33fcabf8..9fd5e0ef0d 100644 --- a/library/init/meta/has_reflect.lean +++ b/library/init/meta/has_reflect.lean @@ -8,10 +8,6 @@ import init.meta.expr init.util @[reducible] meta def {u} has_reflect (α : Sort u) := Π a : α, reflected a -meta instance bool.reflect : has_reflect bool -| tt := `(tt) -| ff := `(ff) - section local attribute [semireducible] reflected @@ -26,6 +22,9 @@ meta instance unsigned.reflect : has_reflect unsigned end +/- Instances that [derive] depends on. All other basic instances are defined at the end of + derive.lean. -/ + meta instance name.reflect : has_reflect name | name.anonymous := `(name.anonymous) | (name.mk_string s n) := `(λ n, name.mk_string s n).subst (name.reflect n) @@ -35,22 +34,6 @@ meta instance list.reflect {α : Type} [has_reflect α] [reflected α] : has_ref | [] := `([]) | (h::t) := `(λ t, h :: t).subst (list.reflect t) -meta instance option.reflect {α : Type} [has_reflect α] [reflected α] : has_reflect (option α) -| (some x) := `(_) -| none := `(_) - meta instance unit.reflect : has_reflect unit | () := `(_) -meta instance prod.reflect {α β : Type} [has_reflect α] [reflected α] [has_reflect β] [reflected β] - : has_reflect (α × β) -| ⟨x, y⟩ := `(_) - -meta instance pos.reflect : has_reflect pos -| ⟨l, c⟩ := `(_) - -meta instance sum.reflect {α β : Type} [has_reflect α] [reflected α] [has_reflect β] [reflected β] - : has_reflect (sum α β) -| (sum.inl _) := `(_) -| (sum.inr _) := `(_) - diff --git a/library/init/meta/interactive.lean b/library/init/meta/interactive.lean index 3eb68d9f7d..53da43239a 100644 --- a/library/init/meta/interactive.lean +++ b/library/init/meta/interactive.lean @@ -6,7 +6,7 @@ Authors: Leonardo de Moura prelude import init.meta.tactic init.meta.rewrite_tactic init.meta.simp_tactic import init.meta.smt.congruence_closure init.category.combinators -import init.meta.interactive_base +import init.meta.interactive_base init.meta.derive open lean open lean.parser @@ -289,14 +289,12 @@ match p with | _ := i_to_expr p end +@[derive has_reflect] meta structure rw_rule := (pos : pos) (symm : bool) (rule : pexpr) -meta instance rw_rule.reflect : has_reflect rw_rule := -λ ⟨p, s, r⟩, `(_) - meta def get_rule_eqn_lemmas (r : rw_rule) : tactic (list name) := let aux (n : name) : tactic (list name) := do { p ← resolve_name n, @@ -337,13 +335,11 @@ private meta def rw_hyp (cfg : rewrite_cfg) : list rw_rule → expr → tactic u meta def rw_rule_p (ep : parser pexpr) : parser rw_rule := rw_rule.mk <$> cur_pos <*> (option.is_some <$> (with_desc "←" (tk "←" <|> tk "<-"))?) <*> ep +@[derive has_reflect] meta structure rw_rules_t := (rules : list rw_rule) (end_pos : option pos) -meta instance rw_rules_t.reflect : has_reflect rw_rules_t := -λ ⟨rs, p⟩, `(_) - -- accepts the same content as `pexpr_list_or_texpr`, but with correct goal info pos annotations meta def rw_rules : parser rw_rules_t := (tk "[" *> @@ -720,17 +716,12 @@ meta structure simp_config_ext extends simp_config := section mk_simp_set open expr interactive.types +@[derive has_reflect] meta inductive simp_arg_type : Type | all_hyps : simp_arg_type | except : name → simp_arg_type | expr : pexpr → simp_arg_type - -meta instance : has_reflect simp_arg_type -| simp_arg_type.all_hyps := `(_) -| (simp_arg_type.except _) := `(_) -| (simp_arg_type.expr _) := `(_) - meta def simp_arg : parser simp_arg_type := (tk "*" *> return simp_arg_type.all_hyps) <|> (tk "-" *> simp_arg_type.except <$> ident) <|> (simp_arg_type.expr <$> texpr) diff --git a/library/init/meta/interactive_base.lean b/library/init/meta/interactive_base.lean index 5c6ddec8c8..f325adc664 100644 --- a/library/init/meta/interactive_base.lean +++ b/library/init/meta/interactive_base.lean @@ -23,10 +23,6 @@ inductive loc : Type | wildcard : loc | ns : list (option name) → loc -meta instance : has_reflect loc -| loc.wildcard := `(_) -| (loc.ns xs) := `(_) - meta def loc.include_goal : loc → bool | loc.wildcard := tt | (loc.ns ls) := (ls.map option.is_none).bor diff --git a/library/init/meta/mk_dec_eq_instance.lean b/library/init/meta/mk_dec_eq_instance.lean index 97ce250aae..99bae05640 100644 --- a/library/init/meta/mk_dec_eq_instance.lean +++ b/library/init/meta/mk_dec_eq_instance.lean @@ -137,6 +137,9 @@ do env ← get_env, meta instance binder_info.has_decidable_eq : decidable_eq binder_info := by mk_dec_eq_instance +@[derive_handler] meta def decidable_eq_derive_handler := +instance_derive_handler ``decidable_eq tactic.mk_dec_eq_instance + end tactic /- instances of types in dependent files -/ diff --git a/library/init/meta/mk_has_reflect_instance.lean b/library/init/meta/mk_has_reflect_instance.lean new file mode 100644 index 0000000000..2b9fa95be6 --- /dev/null +++ b/library/init/meta/mk_has_reflect_instance.lean @@ -0,0 +1,73 @@ +/- +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 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] } + +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) + +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, + `(reflected %%fn) ← target, + let fn := field_names.foldl (λ fn _, expr.app_fn fn) fn, + quote ← mk_app `reflected [fn] >>= mk_instance, + 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 + +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, + -- 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 diff --git a/library/init/meta/smt/ematch.lean b/library/init/meta/smt/ematch.lean index 622f3ac510..5ba0fa3a13 100644 --- a/library/init/meta/smt/ematch.lean +++ b/library/init/meta/smt/ematch.lean @@ -6,7 +6,7 @@ Authors: Leonardo de Moura prelude import init.meta.smt.congruence_closure import init.meta.attribute init.meta.simp_tactic -import init.meta.interactive_base +import init.meta.interactive_base init.meta.derive open tactic /-- Heuristic instantiation lemma -/ diff --git a/library/init/meta/vm.lean b/library/init/meta/vm.lean index 10b3ac3cd9..687447e984 100644 --- a/library/init/meta/vm.lean +++ b/library/init/meta/vm.lean @@ -5,7 +5,7 @@ Authors: Leonardo de Moura -/ prelude import init.meta.tactic init.data.option_t -import init.meta.derive +import init.meta.mk_dec_eq_instance meta constant vm_obj : Type