max/lean4-htt
1
0
Fork 0
Code Issues Pull requests Projects Releases Packages Wiki Activity Actions 2

feat(library/init/lean/declaration): add ConstantInfo.instantiateTypeUnivParams and ConstantInfo.instantiateValueUnivParams

Browse source 
cc @dselsam

See new test for an example.
This commit is contained in:
Leonardo de Moura 2019-09-30 15:46:19 -07:00
parent 864b9c730c
commit 2b252a441e
3 changed files with 36 additions and 2 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

6
library/init/lean/declaration.lean
View file

@ -166,5 +166,11 @@ def hints : ConstantInfo → ReducibilityHints
| defnInfo {hints := r, ..} => r
| _ => ReducibilityHints.opaque
@[extern "lean_instantiate_type_lparams"]
constant instantiateTypeUnivParams (c : ConstantInfo) (ls : List Level) : Expr := default _
@[extern "lean_instantiate_value_lparams"]
constant instantiateValueUnivParams (c : ConstantInfo) (ls : List Level) : Expr := default _
end ConstantInfo
end Lean

18
src/kernel/instantiate.cpp
View file

@ -245,7 +245,8 @@ MK_THREAD_LOCAL_GET(instantiate_univ_cache, get_type_univ_cache, LEAN_INST_UNIV_
MK_THREAD_LOCAL_GET(instantiate_univ_cache, get_value_univ_cache, LEAN_INST_UNIV_CACHE_SIZE);
expr instantiate_type_lparams(constant_info const & info, levels const & ls) {
lean_assert(info.get_num_lparams() == length(ls));
if (info.get_num_lparams() != length(ls))
lean_panic("#universes mismatch at instantiateTypeUnivParams");
if (is_nil(ls) || !has_param_univ(info.get_type()))
return info.get_type();
instantiate_univ_cache & cache = get_type_univ_cache();
@ -257,7 +258,8 @@ expr instantiate_type_lparams(constant_info const & info, levels const & ls) {
}
expr instantiate_value_lparams(constant_info const & info, levels const & ls) {
lean_assert(info.get_num_lparams() == length(ls));
if (info.get_num_lparams() != length(ls))
lean_panic("#universes mismatch at instantiateValueUnivParams");
if (is_nil(ls) || !has_param_univ(info.get_value()))
return info.get_value();
instantiate_univ_cache & cache = get_value_univ_cache();
@ -268,6 +270,18 @@ expr instantiate_value_lparams(constant_info const & info, levels const & ls) {
return r;
}
extern "C" object * lean_instantiate_type_lparams(object * info0, object * ls0) {
constant_info const & a = reinterpret_cast<constant_info const &>(info0);
levels const & ls = reinterpret_cast<levels const &>(ls0);
return instantiate_type_lparams(a, ls).steal();
}
extern "C" object * lean_instantiate_value_lparams(object * info0, object * ls0) {
constant_info const & a = reinterpret_cast<constant_info const &>(info0);
levels const & ls = reinterpret_cast<levels const &>(ls0);
return instantiate_value_lparams(a, ls).steal();
}
void clear_instantiate_cache() {
get_type_univ_cache().clear();
get_value_univ_cache().clear();

14
tests/lean/run/instuniv.lean Normal file
View file

@ -0,0 +1,14 @@
import init.lean
open Lean
def tst : IO Unit :=
do env ← importModules [`init.data.array.default];
match env.find `Array.foldl with
| some info => do
IO.println (info.instantiateTypeUnivParams [Level.zero, Level.zero]);
IO.println (info.instantiateValueUnivParams [Level.zero, Level.zero]);
pure ()
| none => IO.println ("Array.foldl not found");
pure ()
#eval tst