feat(init/meta/mk_has_reflect_instance): add derive_handler for has_reflect

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

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

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

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

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 _) := `(_)
-

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)
 

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

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 -/

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

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 -/

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