Adding a declaration but with non-quoted value

Stream: lean4

[Andrej Bauer]

I know how to use CoreM.addAndCompile to add a new declaration, given a quoted expression and its type. But what if I have an honest expression (not quoted), and would like to bind it to a declaration? (I need this so that in the next step I can add a instance using Meta.addInstance).

[Mario Carneiro]

when you say a "quoted expression" I guess you mean an element of type Expr?

[Mario Carneiro]

For things of other types, these are just runtime values and not really expressions at all. E.g if you have a Nat in a metaprogram it can only ever be a numeral. You can reflect things of various types into Expr using the ToExpr class but it won't be the same as the original expression, it will be a representation of the normal form itself. And of course for function types you can't do it at all.

[Mario Carneiro]

This all leads me to believe there is some element of #xy problem here. How did you obtain this "unquoted expression"?

[Andrej Bauer]

The whole scenario is this:

1. Using Lean.FromJson I obtain a value v of type structure CowData .... deriving Lean.FromJson.
2. There is a type class class Cow (P : Pasture) extends CowData (it's literally just that). Note that I do not have a P when v is created in step 1.
3. I obtain a P : Pasture and would like to install Cow.mk v as an instance of Cow P.

[Mario Carneiro]

In that case you most likely do want to use ToExpr on the CowData. Whether you need it for the P : Pasture depends on how it is "obtained"

[Andrej Bauer]

It's generated by JsonData.loadJsonData from a file.

[Mario Carneiro]

The only thing that lean knows how to handle in its generic infrastructure is the Expr type. If you want to make a declaration the contents of that declaration have to be an Expr. There are very few places which allow general types, usually as opaque blobs for "user data" which lean can preserve

[Eric Wieser]

Does the eval% elaborator help at all here?

[Andrej Bauer]

I am happy to use ToExpr if that won't anger the Lean high priests.

[Mario Carneiro]

@Eric Wieser my guess is that Andrej is doing all of this inside an elab which plays a role similar to eval%

[Mario Carneiro]

(eval% also uses ToExpr to perform the conversion: docs#Mathlib.Meta.elabEvalExpr )

[Andrej Bauer]

CowData is just a bunch of optional Nat and Bool fields, but like 30, so it would be nice not to have to write too much boiler-plate code. (And yes, it's all inside Elab.)

[Andrej Bauer]

It can't find an instance of ToExpr for CowData.

[Mario Carneiro]

you should be able to derive ToExpr on your type

[Mario Carneiro]

oh but you will need file#Mathlib/Tactic/DeriveToExpr

[Mario Carneiro]

@Kyle Miller should this be upstreamed to std4 or lean core?

[Eric Wieser]

This was held up by #5952, which perhaps I should go back to (but adds a Qq dependency which makes upstreaming impossible)

[Andrej Bauer]

I can derive ToExpr on CowData easily, but not on Cow because Pasture is "complicated". So I could do it if there were a way to convert CowData to Q(CowData).

[Mario Carneiro]

That's exactly ToExpr (on CowData)

[Andrej Bauer]

Ah, perhaps I should not force it to have type Expr...

[Mario Carneiro]

The return value of toExpr (c : CowData) is Expr but you can coerce it to Q(CowData)

[Mario Carneiro]

(Does Qq have a well typed version of ToExpr?)

[Eric Wieser]

(In #5952, yes)

[Andrej Bauer]

ToExpr did the trick, it seems. Thanks. Also, why are you people awake?

[Mario Carneiro]

You will probably have to implement ToExpr (Cow P) manually, or write a function that does what you want with some related type signature. You can make use of ToExpr CowData in the implementation though

[Andrej Bauer]

I just derived ToExpr CowData and then used $(@Cow.mk $cowData) to circumvent deriving ToExpr (Cow P).