The Coq mailing list

[Daniel Schepler <dschepler AT gmail.com>]

I'm curious if anybody has ever considered writing code to extract to
C++ (especially since C++11 introduced lambda expressions).

Not that I have a particular use case for it.  It was just a random
idea that I ended up needing to experiment with to satisfy my
curiosity.  I'm attaching a possible prototype for what extracted code
might look like.

Some other ideas:
The shared_ptr should not be necessary for non-recursive inductive
types (though for large enough structures it might still be useful to
provide an option to force using it, if it turns out repeated copying
is a significant performance drain).
The extraction of an inductive type with a single constructor (or no
constructors) wouldn't need the boost::variant.
The extraction of an inductive type where all constructors have no
arguments would be an "enum class".
In some situations like the ones where currently OCaml extraction uses
Obj.magic, the C++ extraction might need to use boost::any.
-- 
Daniel Schepler
#include <boost/variant.hpp>
#include <memory>
#include <iostream>

template <typename T>
class list_node;
template <typename T>
using list = std::shared_ptr<const list_node<T>>;

struct cons_tag_t { }; constexpr cons_tag_t cons_tag { };
struct nil_tag_t { }; constexpr nil_tag_t nil_tag { };

template <typename T>
class list_node {
public:
    list_node() = delete;
    list_node(const list_node&) = default;
    list_node(list_node&&) = default;
    list_node& operator=(const list_node&) = default;
    list_node& operator=(list_node&&) = default;

    list_node(cons_tag_t, T i_head, list<T> i_tail) :
        m_contents { cons_t { std::move(i_head), std::move(i_tail) } } { }
    list_node(nil_tag_t) :
        m_contents { nil_t { } } { }

    template <typename ConsFunctor, typename NilFunctor>
    auto match(ConsFunctor&& cons_case, NilFunctor&& nil_case) const {
        return boost::apply_visitor(
            visitor<ConsFunctor, NilFunctor> { cons_case, nil_case },
            m_contents);
    }

private:
    struct cons_t {
        T head;
        list<T> tail;
    };
    struct nil_t { };

    boost::variant<cons_t, nil_t> m_contents;

    template <typename ConsFunctor, typename NilFunctor>
    struct visitor {
    public:
        ConsFunctor& cons_case;
        NilFunctor& nil_case;
        auto operator()(const cons_t& v) const {
            return cons_case(v.head, v.tail);
        }
        auto operator()(const nil_t& v) const {
            return nil_case();
        }
    };
};

template <typename T>
list<T> cons(T head, list<T> tail) {
    return std::make_shared<const list_node<T>>(cons_tag, std::move(head), std::move(tail));
}

template <typename T>
list<T> nil() {
    static list<T> static_nil = std::make_shared<const list_node<T>>(nil_tag);
    return static_nil;
}

template <typename T>
list<T> append(const list<T>& l1, const list<T>& l2) {
    return l1->match(
        [&](const T& head, const list<T>& tail) {
            return cons(head, append(tail, l2));
        },
        [&]() {
            return l2;
        }
    );
}

struct default_tmpl_arg { };
template <typename T, typename U = default_tmpl_arg, typename Functor,
          typename U0 = std::conditional_t<std::is_same<U, default_tmpl_arg>::value,
                                           std::decay_t<decltype(std::declval<Functor>()(std::declval<T>()))>,
                                           U>>
// or maybe just:
// template <typename T, typename U, typename Functor>
// list<U0> map(Functor&& f, const list<T>& l)
// though that would then require users (not just extracted code) to always
// give some template arguments explicitly e.g. map<int, int>(sqr, l)
list<U0> map(Functor&& f, const list<T>& l) {
    return l->match(
        [&](const T& head, const list<T>& tail) {
            return cons<U0>(f(head), map<T, U, Functor, U0>(std::forward<Functor>(f), tail));
        },
        [&]() {
            return nil<U0>();
        }
    );
}

// END prototype of extracted code, following is usage test code

template <typename T>
void printList(std::ostream& os, const list<T>& l, bool first) {
    l->match(
        [&](const T& head, const list<T>& tail) {
            if (!first)
                os << ',';
            os << ' ' << head;
            printList(os, tail, false);
        },
        [&]() {
            if (!first)
                os << ' ';
        }
    );
}

template <typename T>
std::ostream& operator<<(std::ostream& os, const list<T>& l) {
    os << '[';
    printList(os, l, true);
    return os << ']';
}

void test() {
    list<int> l =
        cons(3,
             cons(4, nil<int>()));
    std::cout << "l = " << l << '\n';
    list<int> l2 = append(l, l);
    std::cout << "l2 = append(l, l) = " << l2 << '\n';
    list<int> l3 = map(
        [](int n) { return 2 * n + 5; },
        l);
    std::cout << "l3 = map(2.+5, l) = " << l3 << '\n';

    list<list<int>> ll =
        cons(l,
             cons(l2, nil<list<int>>()));
    std::cout << "ll = " << ll << '\n';
    // ll2 = map (append l3) ll
    list<list<int>> ll2 =
        map([l3](const list<int>& x) {
                return append(l3, x);
            },
            ll);
    std::cout << "ll2 = map (append l3) ll = " << ll2 << '\n';
}

int main() {
    test();
    return 0;
}