From 9bae1eee2921fe2f0f931b0bed9867686ca2550d Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Fri, 21 Aug 2015 15:25:12 -0700 Subject: [PATCH] feat(api/univ): add lean_list_univ API --- src/api/lean_univ.h | 26 ++++++++++++++++--- src/api/univ.cpp | 57 ++++++++++++++++++++++++++++++++++++----- src/api/univ.h | 4 +++ src/tests/shared/univ.c | 12 ++++++++- 4 files changed, 87 insertions(+), 12 deletions(-) diff --git a/src/api/lean_univ.h b/src/api/lean_univ.h index 865c5a01af..e6d00d83e6 100644 --- a/src/api/lean_univ.h +++ b/src/api/lean_univ.h @@ -90,12 +90,30 @@ lean_bool lean_univ_get_name(lean_univ u, lean_name * r, lean_exception * ex); /** \brief Store in \c r the normal for of the given universe */ lean_bool lean_univ_normalize(lean_univ u, lean_univ * r, lean_exception * ex); -/** \brief Instantiate the universe parameters names ns[i] with us[i] in \c u, +LEAN_DEFINE_TYPE(lean_list_univ); + +/** \brief Create the empty list of univs */ +lean_bool lean_list_univ_mk_nil(lean_list_univ * r, lean_exception * ex); +/** \brief Create the list h :: t */ +lean_bool lean_list_univ_mk_cons(lean_univ h, lean_list_univ t, lean_list_univ * r, lean_exception * ex); +/** \brief Delete/dispose the given list of univs */ +void lean_list_univ_del(lean_list_univ l); +/** \brief Return true iff the list is a "cons" (i.e., it is not the nil list) */ +lean_bool lean_list_univ_is_cons(lean_list_univ l); +/** \brief Return true iff the two given lists are equal */ +lean_bool lean_list_univ_eq(lean_list_univ n1, lean_list_univ n2); +/** \brief Store in \c r the head of the given list + \pre lean_list_univ_is_cons(l) */ +lean_bool lean_list_univ_head(lean_list_univ l, lean_univ * r, lean_exception * ex); +/** \brief Store in \c r the tail of the given list + \pre lean_list_univ_is_cons(l) */ +lean_bool lean_list_univ_tail(lean_list_univ l, lean_list_univ * r, lean_exception * ex); + +/** \brief Instantiate the universe parameters names in ns with us in \c u, and store the result in \c r. - \remark \c ns and \c us are arrays of names and universes, and both have size \c sz. + \remark The given lists must have the same length. */ -lean_bool lean_univ_instantiate(lean_univ u, unsigned sz, lean_name const * ns, lean_univ const * us, - lean_univ * r, lean_exception * ex); +lean_bool lean_univ_instantiate(lean_univ u, lean_list_name ns, lean_list_univ us, lean_univ * r, lean_exception * ex); /*@}*/ /*@}*/ diff --git a/src/api/univ.cpp b/src/api/univ.cpp index 2743c42981..02f8a11763 100644 --- a/src/api/univ.cpp +++ b/src/api/univ.cpp @@ -179,18 +179,61 @@ lean_bool lean_univ_normalize(lean_univ u, lean_univ * r, lean_exception * ex) { LEAN_CATCH; } +lean_bool lean_list_univ_mk_nil(lean_list_univ * r, lean_exception * ex) { + LEAN_TRY; + *r = of_list_level(new list()); + LEAN_CATCH; +} + +lean_bool lean_list_univ_mk_cons(lean_univ h, lean_list_univ t, lean_list_univ * r, lean_exception * ex) { + LEAN_TRY; + check_nonnull(h); + check_nonnull(t); + *r = of_list_level(new list(to_level_ref(h), to_list_level_ref(t))); + LEAN_CATCH; +} + +void lean_list_univ_del(lean_list_univ l) { + delete to_list_level(l); +} + +lean_bool lean_list_univ_is_cons(lean_list_univ l) { + return l && !is_nil(to_list_level_ref(l)); +} + +lean_bool lean_list_univ_eq(lean_list_univ l1, lean_list_univ l2) { + return l1 && l2 && to_list_level_ref(l1) == to_list_level_ref(l2); +} + +lean_bool lean_list_univ_head(lean_list_univ l, lean_univ * r, lean_exception * ex) { + LEAN_TRY; + check_nonnull(l); + if (!lean_list_univ_is_cons(l)) + throw lean::exception("invalid argument, non-nil list expected"); + *r = of_level(new level(head(to_list_level_ref(l)))); + LEAN_CATCH; +} + +lean_bool lean_list_univ_tail(lean_list_univ l, lean_list_univ * r, lean_exception * ex) { + LEAN_TRY; + check_nonnull(l); + if (!lean_list_univ_is_cons(l)) + throw lean::exception("invalid argument, non-nil list expected"); + *r = of_list_level(new list(tail(to_list_level_ref(l)))); + LEAN_CATCH; +} + /** \brief Instantiate the universe parameters names ns[i] with us[i] in \c u, and store the result in \c r. \remark \c ns and \c us are arrays of names and universes, and both have size \c sz. */ -lean_bool lean_univ_instantiate(lean_univ u, unsigned sz, lean_name const * ns, lean_univ const * us, - lean_univ * r, lean_exception * ex) { +lean_bool lean_univ_instantiate(lean_univ u, lean_list_name ns, lean_list_univ us, lean_univ * r, lean_exception * ex) { LEAN_TRY; check_nonnull(u); - buffer tmp_ns; - buffer tmp_us; - to_buffer(sz, ns, tmp_ns); - to_buffer(sz, us, tmp_us); - *r = of_level(new level(instantiate(to_level_ref(u), to_list(tmp_ns), to_list(tmp_us)))); + check_nonnull(ns); + check_nonnull(us); + if (length(to_list_name_ref(ns)) != length(to_list_level_ref(us))) + throw lean::exception("invalid arguments, the given lists must have the same length"); + *r = of_level(new level(instantiate(to_level_ref(u), to_list_name_ref(ns), to_list_level_ref(us)))); LEAN_CATCH; } diff --git a/src/api/univ.h b/src/api/univ.h index 4129d1c4bd..0f093a0514 100644 --- a/src/api/univ.h +++ b/src/api/univ.h @@ -15,4 +15,8 @@ inline level * to_level(lean_univ n) { return reinterpret_cast(n); } inline level const & to_level_ref(lean_univ n) { return *reinterpret_cast(n); } inline lean_univ of_level(level * n) { return reinterpret_cast(n); } void to_buffer(unsigned sz, lean_univ const * us, buffer & r); + +inline list * to_list_level(lean_list_univ n) { return reinterpret_cast *>(n); } +inline list const & to_list_level_ref(lean_list_univ n) { return *reinterpret_cast *>(n); } +inline lean_list_univ of_list_level(list * n) { return reinterpret_cast(n); } } diff --git a/src/tests/shared/univ.c b/src/tests/shared/univ.c index 8a55c6d622..23bb4a307d 100644 --- a/src/tests/shared/univ.c +++ b/src/tests/shared/univ.c @@ -22,6 +22,8 @@ int main() { lean_name a, l, U, pp, pp_unicode, rn; lean_options o1, o2; lean_univ zero, one, p1, g1, m1, u, n, i, ru; + lean_list_name ln1, ln2; + lean_list_univ lu1, lu2; char const * s1; lean_bool r; @@ -48,7 +50,15 @@ int main() { check(lean_univ_geq(one, zero, &r, &ex) && r); /* replace l_1 with one in u */ - check(lean_univ_instantiate(u, 1, &l, &one, &i, &ex)); + check(lean_list_name_mk_nil(&ln1, &ex)); + check(lean_list_name_mk_cons(l, ln1, &ln2, &ex)); + check(lean_list_univ_mk_nil(&lu1, &ex)); + check(lean_list_univ_mk_cons(one, lu1, &lu2, &ex)); + check(lean_univ_instantiate(u, ln2, lu2, &i, &ex)); + lean_list_name_del(ln1); + lean_list_name_del(ln2); + lean_list_univ_del(lu1); + lean_list_univ_del(lu2); lean_string_del(s1); check(lean_univ_to_string_using(i, o2, &s1, &ex)); printf("universe: %s\n", s1);