From e7760eaa0b4613439026ee55d40329804d12eaae Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Mon, 19 Mar 2018 17:39:46 -0700 Subject: [PATCH] doc(tmp/lean4): `expr`, `level`, `name`, ... in Lean --- tmp/lean4.md | 10 ++++++++++ 1 file changed, 10 insertions(+) diff --git a/tmp/lean4.md b/tmp/lean4.md index faaa57945c..a0aae277be 100644 --- a/tmp/lean4.md +++ b/tmp/lean4.md @@ -223,6 +223,16 @@ where more than one .olean contains the same monomorphised function. We see two names for monomorphised functions; we generate unique names, and accept the fact the environment will contain duplicates. It is just a space issue. +- In Lean3, `name`, `level` and `expr` are all implemented in C++. To expose these objects in Lean, we have to wrap them +using a subclass of `vm_external`. This generates a significant performance overhead. For example, suppose we have a lean +function that traverses a big expression; for each visited expression `e`, we need to create a `vm_expr` object for wrapping `e`. +Moreover, we have two layers of reference counting: one at `expr` and another at `vm_obj`. +This design decision is fine in Lean3 because the most expensive tasks are implemented in C++, and Lean code is only +used to "glue" together existing procedures implemented in C++. This is not the case in Lean4. +So, in Lean4, all these objects will be implemented directly in Lean. +As described above, we will have a tool that will generate C++ functions for creating and accessing these objects. +We believe this will not affect much how we code in C++, and it will eliminate a lot of boilerplate code we currently use. + # IR - Register based.