Derive bundled

derive_bundled.lean

-- Big thanks to Simon Hudon for dictating this file to me
-- and explaining what's going on!

import category_theory.concrete_category

namespace string

def camel_case (s : string) : string :=
(join $ split (λ c, c = '_') s) ++ "'"
  -- TODO make first char uppercase of each elem in list
  -- appending a prime for now

end string

namespace name

def camel_case : name -> name
| anonymous := name.anonymous
| (mk_string s n) := mk_string s.camel_case n
| (mk_numeral num n) := mk_numeral num n

end name

open tactic
open category_theory

meta def mk_bundled_instance : tactic unit := trace_state

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 trace p,
   trace n.camel_case,
   mk_const n >>= infer_type >>= trace,
   mk_const ``bundled >>= infer_type >>= trace,
   d ← get_decl n,
   let params := d.univ_params.map level.param,
   let x : expr := expr.const n params,
   mk_mapp ``bundled [x] >>= infer_type >>= trace,
   df ← mk_mapp ``bundled [x],
   t ← infer_type df,
   add_decl $ mk_definition n.camel_case d.univ_params t df,
   trace_state,
   return tt
else return ff

@[derive_handler] meta def bundled_derive_handler :=
instance_derive_handler' ``bundled mk_bundled_instance

attribute [derive bundled] group

#print group'

@[derive bundled]
structure groupy_thing (X : Type*) :=
(fld₁ : X → X → X)
(fld₂ : X)

#print groupything'