mit-pdos / mcqc Goto Github PK

Fixpoint expressions are annoying, because they capture the enclosing scope and must be outlined together with their scope references to work in C++

Implement with tagged union

Reproduce with

Fixpoint add (a b: nat) :=
  match a with
    | 0    => b
    | S a' =>
       match b with
         | 0    => a
         | S b' => S (S (add a' b'))
       end
  end.

Right now, link :: CDecl -> Env CDecl uses the name of the functions in the context to substitute.
As a result, polymorphic functions such as length for strings and lists, are erroneously substituted.

While length is defined in include/string.hpp it is not defined for lists and must be generated
from the Coq definition.

Instead of being

template<class T>
using list = std::variant<Coq_Nil<T>, Coq_Cons<T>>

Make it be

template<class T>
using list = std::shared_ptr<std::variant<Coq_Nil<T>, Coq_Cons<T>>>

Which makes addPtr redundant, a good thing!

Right now, substituting free types is not kept in context as a constraint and thus we cannot do constraint solving. Add CTFree constraints in the context and remove them according to scoping.

Generated map

template<class T, class U, class V>
list<U> map(V f, list<T> l) {
  return match(l,
    [=]() { return list<U>{}; },
    [=](auto a, auto t) { return cons(f(a), map(f, t)); });
}

Working version; Notice that the order of template class declaration needs to change and a template
strict type annotation was added from f: T->U type in coq.

template<class T, class V, class U = std::invoke_result_t<V, T>>
list<U> map(V f, list<T> l) {
  return match(l,
    [=]() { return list<U>{}; },
    [=](auto a, auto t) { return cons(f(a), map(f, t)); });
}

In C++17 functional types are expressed as templated types, but that can cause issues as in #6. Regardless, raiseCTFunc to templates needs to happen much later, so we maintain
the arrow semantics of functions during type unification.

Refactor like so:

src/Compiler
  |---src/Compiler/Expr.hs
  |---src/Compiler/MExpr.hs
  |---src/Compiler/Decl.hs
  |---src/Compiler/MDecl.hs

Where Expr has all the CExpr -> CExpr functions like semantics, MExpr has the monadic
functions Monad t => CExpr -> t CExpr and similar for Decl and MDecl. Cleanup
src/Codegen/Compiler.hs.

Escape ' in names, such as map' clang gets confused.

Cyclical recursive references of constructors is a problem. Hopefully, forward declaration in C++ works, so the following for a list is better

template<class T>
struct Coq_nil;
template<class T>
struct Coq_cons;
template<class T>
using list = std::variant<Coq_nil<T>, Coq_cons<T>>;

template<class T>
struct Coq_nil {};

template<class T>
struct Coq_cons {
  T a;
  std::shared_ptr<list<T>> b;
  Coq_cons(T a, std::shared_ptr<list<T>> b) {
    this->a = a;
    this->b = b;
  };
};

Should be:

Coq struct type declarations -> C struct type declarations

• accessor functions

in src/PrettyPrinter/Expr.hs CExprList are not specialized, so we output List<T> right now which is bad, need to derive T into a concrete type when we can.

Currying is easily supported and experiments show lambdas are elaborated at compile time by clang++, use curry() in include/curry.h.

Context is now a map, which does not allow for two polymorphic definitions to coexist, although clang clearly allows that (overloading). Substitute Map for Multimap in Context definition.

http://hackage.haskell.org/package/multimap-1.2.1/docs/Data-MultiMap.html