derive functor and traversable instances

Author: cipher1024

data/traversable/derive.lean

@@ -6,9 +6,9 @@ Author: Simon Hudon
 Automation to construct `traversable` instances
 -/
 
-import .basic
+import .basic .instances
 import category.basic
-import tactic.basic
+import tactic.basic tactic.cache
 
 namespace tactic.interactive
 
@@ -17,19 +17,53 @@ open tactic list monad functor
 def succeeds {m : Type* → Type*} [alternative m] {α} (cmd : m α) : m bool :=
 (tt <$ cmd) <|> pure ff
 
-meta def traverse_field (n : name) (cl f v e : expr) : tactic (option expr) :=
+meta def nested_map (f v : expr) : expr → tactic expr
+| t :=
+do t ← instantiate_mvars t,
+   mcond (succeeds $ is_def_eq t v)
+      (pure f)
+      (if ¬ v.occurs (t.app_fn)
+          then do
+            cl ← mk_app ``functor [t.app_fn],
+            _inst ← mk_instance cl,
+            f' ← nested_map t.app_arg,
+            mk_mapp ``functor.map [t.app_fn,_inst,none,none,f']
+          else fail format!"type {t} is not a functor with respect to variable {v}")
+
+meta def map_field (n : name) (cl f v e : expr) : tactic expr :=
 do t ← infer_type e >>= whnf,
    if t.get_app_fn.const_name = n
-   then return none
+   then fail "recursive types not supported"
    else if v.occurs t
-   then   mcond (succeeds $ is_def_eq t v)
-                (pure $ some $ expr.app f e)
-                (if ¬ v.occurs (t.app_fn)
-                    then some <$> to_expr ``(compose.mk (traversable.traverse %%f %%e))
-                    else fail format!"type {t} is not traversable with respect to variable {v}")
+   then do f' ← nested_map f v t,
+           pure $ f' e
    else
-         (is_def_eq t.app_fn cl >> some <$> to_expr ``(compose.mk %%e))
-     <|> some <$> to_expr ``(@pure %%cl _ _ %%e)
+         (is_def_eq t.app_fn cl >> to_expr ``(compose.mk %%e))
+     <|> pure e
+
+meta def nested_traverse (f v : expr) : expr → tactic expr
+| t :=
+do t ← instantiate_mvars t,
+   mcond (succeeds $ is_def_eq t v)
+      (pure f)
+      (if ¬ v.occurs (t.app_fn)
+          then do
+            cl ← mk_app ``traversable [t.app_fn],
+            _inst ← mk_instance cl,
+            f' ← nested_traverse t.app_arg,
+            mk_mapp ``traversable.traverse [t.app_fn,_inst,none,none,none,none,f']
+          else fail format!"type {t} is not traversable with respect to variable {v}")
+
+meta def traverse_field (n : name) (_inst cl f v e : expr) : tactic expr :=
+do t ← infer_type e >>= whnf,
+   if t.get_app_fn.const_name = n
+   then fail "recursive types not supported"
+   else if v.occurs t
+   then do f' ← nested_traverse f v t,
+           pure $ f' e
+   else
+         (is_def_eq t.app_fn cl >> to_expr ``(compose.mk %%e))
+     <|> to_expr ``(@pure _ (%%_inst).to_has_pure _ (ulift.up %%e))
 
 meta def seq_apply_constructor : list expr → expr → tactic expr
 | (x :: xs) e := to_expr ``(%%e <*> %%x) >>= seq_apply_constructor xs
@@ -48,32 +82,132 @@ do c ← mk_const n,
    t ← infer_type c,
    fill_implicit_arg' c t
 
-meta def traverse_constructor (c n : name) (f v : expr) (args : list expr) : tactic unit :=
+meta def mk_down (e : expr) : tactic expr :=
+to_expr ``(ulift.down %%e) <|> pure e
+
+meta def map_constructor (c n : name) (f v : expr) (args : list expr) : tactic unit :=
 do g ← target,
-   args' ← mmap (traverse_field n g.app_fn f v) args,
+   args' ← mmap (map_field n g.app_fn f v) args,
    constr ← fill_implicit_arg c,
-   constr' ← to_expr ``(@pure %%(g.app_fn) _ _ %%constr),
-   r ← seq_apply_constructor (filter_map id args') constr',
-   () <$ tactic.apply r
+   let r := constr.mk_app args',
+   () <$ tactic.exact r
 
-open applicative
+meta def mk_map (type : name) (cs : list name) := do
+   `[intros α β f x],
+   reset_instance_cache,
+   x ← get_local `x,
+   xs ← tactic.induction x,
+   f ← get_local `f,
+   α ← get_local `α,
+   β ← get_local `β,
+   () <$ mmap₂'
+      (λ (c : name) (x : name × list expr × list (name × expr)),
+      solve1 (map_constructor c type f α x.2.1))
+      cs xs
 
-meta def derive_traverse : tactic unit :=
-do `(traversable %%f) ← target | failed,
-   env ← get_env,
-   let n := f.get_app_fn.const_name,
-   let cs := env.constructors_of n,
-   constructor,
-   `[intros m _ α β f x],
+meta def traverse_constructor (c n : name) (_inst f v : expr) (args : list expr) : tactic unit :=
+do g ← target,
+   args' ← mmap (traverse_field n _inst g.app_fn f v) args,
+   constr ← fill_implicit_arg c,
+   v ← mk_mvar,
+   constr' ← to_expr ``(@pure %%(g.app_fn) (%%_inst).to_has_pure _ %%v),
+   r ← seq_apply_constructor args' constr',
+   gs ← get_goals,
+   set_goals [v],
+   vs ← tactic.intros >>= mmap mk_down,
+   tactic.exact (constr.mk_app vs),
+   done,
+   set_goals gs,
+   () <$ tactic.exact r
+
+meta def mk_traverse (type : name) (cs : list name) := do
+   `[intros m _inst α β f x],
    reset_instance_cache,
    x ← get_local `x,
    xs ← tactic.induction x,
    f ← get_local `f,
+   _inst ← get_local `_inst,
    α ← get_local `α,
    β ← get_local `β,
    m ← get_local `m,
    () <$ mmap₂'
-      (λ (c : name) (x : name × list expr × _), solve1 (traverse_constructor c n f α x.2.1))
+      (λ (c : name) (x : name × list expr × list (name × expr)),
+      solve1 (traverse_constructor c type _inst f α x.2.1))
       cs xs
 
+open applicative
+
+meta def derive_functor : tactic unit :=
+do `(functor %%f) ← target | failed,
+   env ← get_env,
+   let n := f.get_app_fn.const_name,
+   let cs := env.constructors_of n,
+   refine ``( { functor . map := _ , .. } ),
+   mk_map n cs
+
+meta def derive_traverse : tactic unit :=
+do `(traversable %%f) ← target | failed,
+   env ← get_env,
+   let n := f.get_app_fn.const_name,
+   let cs := env.constructors_of n,
+   constructor,
+   mk_traverse n cs
+
+meta def mk_one_instance
+  (n : name)
+  (cls : name)
+  (tac : tactic unit) : tactic unit :=
+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, level.param n,
+   -- 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 params := params.init,
+   let tgt := tgt.mk_app params,
+   tgt ← mk_app cls [tgt] <|> fail "fish a",
+   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] <|> fail "fish b",
+        -- 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,
+   () <$ mk_instance tgt <|> do
+     (_, val) ← tactic.solve_aux tgt (do
+       tactic.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),
+     set_basic_attribute `instance (n ++ cls) tt
+
+open function
+meta def higher_order_derive_handler
+  (cls : name)
+  (tac : tactic unit)
+  (deps : list (name × tactic unit) := []) :
+  derive_handler :=
+λ p n,
+if p.is_constant_of cls then
+do mmap' (uncurry $ mk_one_instance n) deps,
+   mk_one_instance n cls tac,
+   pure true
+else pure false
+
+@[derive_handler]
+meta def functor_derive_handler :=
+higher_order_derive_handler ``functor derive_functor
+
+@[derive_handler]
+meta def traversable_derive_handler :=
+higher_order_derive_handler ``traversable derive_traverse [(``functor,derive_functor)]
+
 end tactic.interactive

data/traversable/instances.lean

@@ -66,7 +66,7 @@ open function functor
 variables {f f' : Type u → Type u}
 variables [applicative f] [applicative f']
 
-def option.traverse {α β : Type u} (g : α → f β) : option α → f (option β)
+protected def option.traverse {α β : Type u} (g : α → f β) : option α → f (option β)
 | none := pure none
 | (some x) := some <$> g x
 
@@ -114,7 +114,7 @@ variables {α β : Type u}
 open applicative functor
 open list (cons)
 
-def list.traverse (g : α → f β) : list α → f (list β)
+protected def list.traverse (g : α → f β) : list α → f (list β)
 | [] := pure []
 | (x :: xs) := cons <$> g x <*> list.traverse xs
 

tests/examples.lean

@@ -1,4 +1,5 @@
 import tactic data.stream.basic data.set.basic data.finset data.multiset
+       data.traversable.derive
 open tactic
 
 universe u
@@ -92,3 +93,46 @@ begin
     admit },
   trivial
 end
+
+/- traversable -/
+
+meta def check_defn (n : name) (e : pexpr) : tactic unit :=
+do (declaration.defn _ _ _ d _ _) ← get_decl n,
+   e' ← to_expr e,
+   guard (d =ₐ e') <|> trace d >> failed
+
+set_option trace.app_builder true
+
+@[derive traversable]
+structure my_struct (α : Type) :=
+  (y : ℤ)
+
+run_cmd do
+check_defn ``my_struct.traversable
+  ``( { traversable .
+        to_functor := my_struct.functor,
+        traverse := λ (m : Type → Type) (_inst : applicative m) (α β : Type) (f : α → m β) (x : my_struct α),
+               my_struct.rec (λ (x : ℤ), pure (λ (a : ulift ℤ), {y := a.down}) <*> pure {down := x}) x} )
+
+@[derive traversable]
+structure my_struct2 (α : Type u) : Type u :=
+  (x : α)
+  (y : ℤ)
+  (z : list α)
+  (k : list (list α))
+
+run_cmd do
+check_defn ``my_struct2.traversable
+  ``( { traversable .
+        to_functor := my_struct2.functor,
+        traverse := λ (m : Type u → Type u) (_inst : applicative m) (α β : Type u) (f : α → m β) (x : my_struct2 α),
+               my_struct2.rec
+                 (λ (x_x : α) (x_y : ℤ) (x_z : list α) (x_k : list (list α)),
+                    pure
+                              (λ (a : β) (a_1 : ulift ℤ) (a_2 : list β) (a_3 : list (list β)),
+                                 {x := a, y := a_1.down, z := a_2, k := a_3}) <*>
+                            f x_x <*>
+                          pure {down := x_y} <*>
+                        traverse f x_z <*>
+                      traverse (traverse f) x_k)
+                 x } )