Structures in meta

Stream: general

[Fabian Glöckle]

Hello everyone, my attempts at auto-generating the corresponding homomorphism types and categories for the classes we have already defined in mathlib have moved a bit. For example

run_cmd add_homomorphism_type `ordered_ring
#print ordered_ring_homomorphism

yields

def ordered_ring_homomorphism : Π {α : Type u} {β : Type v} [i₁ : ordered_ring α] [i₂ : ordered_ring β], (α → β) → Prop :=
λ {α : Type u} {β : Type v} [i₁ : ordered_ring α] [i₂ : ordered_ring β] (f : α → β),
  (∀ {x0 x1 : α}, f (ordered_ring.add x0 x1) = ordered_ring.add (f x0) (f x1)) ∧
    f (ordered_ring.zero α) = ordered_ring.zero β ∧
      (∀ {x0 : α}, f (ordered_ring.neg x0) = ordered_ring.neg (f x0)) ∧
        (∀ {x0 x1 : α}, f (ordered_ring.mul x0 x1) = ordered_ring.mul (f x0) (f x1)) ∧
          f (ordered_ring.one α) = ordered_ring.one β ∧
            (∀ {x0 x1 : α}, ordered_ring.le x0 x1 → ordered_ring.le (f x0) (f x1)) ∧
              ∀ {x0 x1 : α}, ordered_ring.lt x0 x1 → ordered_ring.lt (f x0) (f x1)

This is not perfect though, as one would hope for a class for the homomorphism type (to access the fields more easily).
How can I generate structures/classes in meta code?
And connected to that: can one retrieve the information that groupextends monoid programmatically somehow, or is this immediately inlined?

[Mario Carneiro]

The only way to create structures and classes in 3.4 is to use emit_code_here and build a string to send to the parser. There is an API for this in 3.5c

[Johan Commelin]

I guess it should be possible to write a wrapper around emit_code_here that works in 3.4, right?

[Johan Commelin]

It would take some expr and traverse it to build the string for you.

[Johan Commelin]

@Edward Ayers Did you by chance already write such a wrapper?

[Edward Ayers]

sorry Johan!

[Fabian Glöckle]

The only way to create structures and classes in 3.4 is to use emit_code_here and build a string to send to the parser. There is an API for this in 3.5c

Thanks @Mario Carneiro ! Follow-up: how does one "call" a lean.parser unit as a user?

[Simon Hudon]

You have to write a user command. You can look through mathlib and core for the occurrence of @[user_command] to show you examples of how it's done

[Fabian Glöckle]

ah, I already tried this and got stuck. What is wrong about this?

@[user_command]
meta def emit_homomorphism_structure (_ : interactive.parse $ lean.parser.tk "emitte") (struct_name : name) : lean.parser unit :=
do s ← lean.parser.of_tactic $ homomorphism_structure struct_name,
   emit_structure_here s

[Fabian Glöckle]

the error message reads

invalid user-defined command, must return type `lean.parser unit`

[Mario Carneiro]

you can't put struct_name in the type; use struct_name <- ident in the body

[Fabian Glöckle]

thanks, it now works!
I had to put a dot after the last line, what does it mean?

[Reid Barton]

Dot ends a top-level command. Usually it should be optional.

[Fabian Glöckle]

Another question: i am using expr.to_string to create the strings for emit_code_here but the results do not parse straight away

eq.{succ v} β (f (group.mul.{u} α i₁ x0 x1)) (group.mul.{v} β i₂ (f x0) (f x1))

[Fabian Glöckle]

is this intended, are there better methods, workarounds?
(implicit parameters are one problem, and succ uinstead of u+1the other)