Stream: lean4

Topic: olean files to source

Aurélien Saue (Apr 01 2021 at 10:35):

Hello,
In an effort to convert the olean files created by mathport into source files, I am trying to make a tool that is able to read olean files.
I have found the readModuleData function from Environment.lean which is able to read an olean file into a ModuleData object.
Using toString on the contents gives a basic first result but could be improved a lot.
Do you know which better functions could be used to display the expressions?

Daniel Selsam (Apr 01 2021 at 15:03):

The delaborator (as in "de-elaborator") maps Expr to Syntax, and can be customized e.g. by various pp.<flag> options. It is here: https://github.com/leanprover/lean4/blob/master/src/Lean/PrettyPrinter/Delaborator/Basic.lean#L382. ppTerm goes from Syntax to Format: https://github.com/leanprover/lean4/blob/master/src/Lean/PrettyPrinter.lean#L22-L25

Aurélien Saue (Apr 12 2021 at 09:58):

Hi!
Using the delaborator as proposed I get fine results except that the implicit arguments of functions are displayed.
I guess I could solve that using the pp.explicit option but I don't manage to pass the options because I don't understand how the OptionsPerPos argument works or how to create it.
Could anyone help me a little?

Sebastian Ullrich (Apr 12 2021 at 10:00):

The implicit arguments are displayed? That should not be the default.

Aurélien Saue (Apr 12 2021 at 10:13):

Yes... Maybe the expressions I get with readModuleData have nonly explicit arguments?

Aurélien Saue (Apr 12 2021 at 10:14):

I mean maybe the implicit arguments are stored as explicit in the olean file so when I try to extract them back I cannot know if they were implicit or not

Aurélien Saue (Apr 12 2021 at 10:57):

What is weird is that in the function definitions all the implicit arguments are printed as implicit but in function applications the implicit arguments are displayed and there is no @ before the function name

Last updated: May 07 2021 at 11:09 UTC