Compiler Explorer

Source code

// A C++ template metaprogramming translation of some of the Coq code from
// the first chapter of Adam Chlipala's book
// "Certified Programming with Dependent Types"

// Compile with gcc trunk or clang trunk, and add option --std=c++17
// to get auto template parameters.

// A C++ strongly typed enum can directly represent
// an Inductive definition iff the Inductive definition
// does not contain any cases with additional parameters.
/* Inductive binop : Set := Plus | Times. */
enum class binop { Plus, Times };

// This Inductive definition contains clauses which do have parameters,
// so we will need to use helper structs instead of an enum.
/*
    Inductive exp : Set :=
    | Const : nat -> exp
    | Binop : binop -> exp -> exp -> exp.
*/

// Helper struct for "Const", holds a nat argument.
/* | Const : nat -> exp */
template <int> struct exp_Const {};

// Helper struct for "Binop", holds Plus|Times and two child exp's.
/* | Binop : binop -> exp -> exp -> exp. */
template <binop,typename,typename> struct exp_Binop {};

// Signature for the exp struct which holds either a Const or Binop.
/* Inductive exp : Set */
template <typename> struct exp
/* {} */; // Non-specialized case intentionally undefined
 // (so that only the specializations can be used).

// An exp_Const of some number is an exp.
/* | Const : nat -> exp */
template <int N> struct exp<exp_Const<N>> {};

// A Binop (binop::Plus or binop::Times), with arguments
// of exp<LHS> and RHS exp<E1>, is also an exp.
/* | Binop : binop -> exp -> exp -> exp. */
template <binop op, typename LHS, typename RHS>
struct exp< exp_Binop< op, exp<LHS>, exp<RHS> > >{};

/*
    Definition binopDenote (b : binop) : nat -> nat -> nat :=
    match b with
        | Plus => plus
        | Times => mult
    end.
*/

/* Definition binopDenote (b : binop) : nat -> nat -> nat := */
template <binop b> constexpr auto binopDenote();

/* 
 match b with
 | Plus => plus
*/
template <> constexpr auto binopDenote<binop::Plus>()
{
 return [](int a, int b) { return a+b; };
}

/*
 match b with
 | Times => mult
*/
template <> constexpr auto binopDenote<binop::Times>()
{
 return [](int a, int b) { return a*b; };
}

// "Fixpoint" looks hard to translate, but C++'s function-overload
// pattern matching eats this kind of problem for breakfast daily.
/*
Fixpoint expDenote (e : exp) : nat :=
  match e with
    | Const n => n
    | Binop b e1 e2 => (binopDenote b) (expDenote e1) (expDenote e2)
  end.
*/

// This function template extracts the "int n" from a Const exp.
/* | Const n => n */
template <int n>
constexpr auto expDenote(exp<exp_Const<n>>)
{
 return n;
}

// This function template recursively evaluates the binop.
/* | Binop b e1 e2 => (binopDenote b) (expDenote e1) (expDenote e2) */
template <binop b, typename e1, typename e2>
constexpr auto expDenote(exp<exp_Binop<b, e1, e2>>)
{
 // Aside from the extra parens, this is almost token for token
 // the same as the Coq expression after the =>, above.
 return (binopDenote())(expDenote(e1()), expDenote(e2()));
}

// Convenience typedefs.
template <int n> using Const = exp<exp_Const<n>>;

template <binop b, typename LHS, typename RHS>
using Binop = exp<exp_Binop<b, LHS, RHS > >;

template <typename LHS, typename RHS>
using Binop_Plus = exp<exp_Binop<binop::Plus, LHS, RHS > >;

template <typename LHS, typename RHS>
using Binop_Times = exp<exp_Binop<binop::Times, LHS, RHS > >;

/* Eval simpl in expDenote (Const 42). */
static_assert(expDenote(Const<42>()) == 42);

/* Eval simpl in expDenote (Binop Plus (Const 2) (Const 2)). */
static_assert( expDenote(
 Binop_Plus< Const<2>, Const<2> >()
) == 4);

/* Eval simpl in expDenote (Binop Times (Binop Plus (Const 2) (Const 2)) (Const 7)). */
static_assert( expDenote(
 Binop_Times< Binop_Plus<Const<2>, Const<2>> , Const<7> >()
) == 28 );

/*
Inductive instr : Set :=
  | iConst : nat -> instr
  | iBinop : binop -> instr.
*/

template <int> struct instr_iConst {};
template <binop> struct instr_iBinop {};
template <typename> struct instr /* {} */;
template <int n> struct instr<instr_iConst<n>> {};
template <binop b> struct instr<instr_iBinop> {};

template <int n> using iConst = instr<instr_iConst<n>>;
template <binop b> using iBinop = instr<instr_iBinop>;

// We need some list utilities.
template <typename... Ts> struct type_list {};
template <int... Is> struct int_list {};

template <typename... Ts, typename... Us>
auto operator +(type_list<Ts...>, type_list<Us...>) 
{
 return type_list<Ts..., Us...>();
}

/*
Definition prog := list instr.
Definition stack := list nat.
*/

template <typename... Ts> using prog = type_list< Ts... >;
template <int... Is> using stack = int_list< Is... >;

/* Definitions below will require a compile-time "option" type. */

struct option_None {};

template <typename T>
struct option_Some {};

template <typename> struct option /* {} */;
template <> struct option<option_None> {};
template <typename T> struct option<option_Some<T>> {};

// Convenience typedefs.
using None = option<option_None>;
template <typename T> using Some = option<option_Some<T>>;

// Convert a Some<T> back into a plain "T" (or None).
template <typename T>
constexpr auto remove_some(Some<T>) { return T(); }

constexpr auto remove_some(None) { return None(); }

Definition instrDenote (i : instr) (s : stack) : option stack :=
  match i with
    | iConst n => Some (n :: s)
    | iBinop b =>
      match s with
        | arg1 :: arg2 :: s' => Some ((binopDenote b) arg1 arg2 :: s')
        | _ => None
      end
  end.

template <int n, int... s>
auto instrDenote(iConst<n>, stack<s...>)
{
 return Some< stack< n, s...> >();
}

template <binop b, int arg1, int arg2, int... s_>
auto instrDenote(iBinop, stack<arg1, arg2, s_...>)
{
 return Some< stack< 
 binopDenote()(arg1,arg2) , s_...
 > >();
}

template <binop b>
auto instrDenote(iBinop, ...)
{
 return None();
}

// This one was trickier to translate than the last Fixpoint...
/*
Fixpoint progDenote (p : prog) (s : stack) : option stack :=
  match p with
    | nil => Some s
    | i :: p' =>
      match instrDenote i s with
        | None => None
        | Some s' => progDenote p' s'
      end
  end.
*/

// This case is straightforward; empty program returns stack unchanged.
/*
 match p with
 | nil => Some s
*/
template <int... s>
constexpr auto progDenote(prog<>, stack<s...>)
{
 return Some< stack<s...> >();
}

// The inner match requires a helper, but it has to be forward-declared
// since one case recursively calls progDenote, but progDenote calls it.
// Making it a struct allows us to delay resolution, and making it depend
// on a template parameter (which one case needs, anyway) delays resolution
// long enough to prevent an error message about it being forward declared.
template <typename... p_>
struct progDenote_helper;

template <typename i, typename... p_, int... s>
constexpr auto progDenote(prog<i, p_...>, stack<s...>)
{
 return progDenote_helper<p_...>::match(
 instrDenote(i(), stack<s...>())
 );
}

// The helper forward-declared above.
/*
 match instrDenote i s with
 | None => None
 | Some s' => progDenote p' s'
 end
*/
template <typename... p_>
struct progDenote_helper
{
 static constexpr auto match(None) { return None(); }

template <int... s_>
 static constexpr auto match(Some< stack<s_...> >)
 { return progDenote(prog<p_...>(), stack<s_...>() ); }
};

/*
Fixpoint compile (e : exp) : prog :=
  match e with
    | Const n => iConst n :: nil
    | Binop b e1 e2 => compile e2 ++ compile e1 ++ iBinop b :: nil
  end.
*/

template <int n>
auto compile(Const<n>)
{
 return prog< iConst<n> >();
}

template <binop b, typename e1, typename e2>
auto compile(Binop<b,e1,e2>)
{
 return compile(e2()) + compile(e1()) + prog<iBinop>();
}

/*
Eval simpl in compile (Const 42).
Eval simpl in compile (Binop Plus (Const 2) (Const 2)).
Eval simpl in compile (Binop Times (Binop Plus (Const 2) (Const 2)) (Const 7)).
*/

static_assert(sizeof(decltype(
 compile( Const<42>() )
)));

static_assert(sizeof(decltype(
 compile( Binop_Plus<Const<2>, Const<2>>() )
)));

static_assert(sizeof(decltype(
 compile( Binop_Times< Binop_Plus<Const<2>, Const<2>> , Const<7> >() ) 
)));

/*
Eval simpl in progDenote (compile (Const 42)) nil.
Eval simpl in progDenote (compile (Binop Plus (Const 2) (Const 2))) nil.
Eval simpl in progDenote (compile (Binop Times (Binop Plus (Const 2) (Const 2)) (Const 7))) nil.
*/

static_assert(sizeof(decltype(
 progDenote(
 compile( Const<42>() ),
 stack<>()
 )
)));

static_assert(sizeof(decltype(
 progDenote(
 compile( Binop_Plus<Const<2>, Const<2>>() ),
 stack<>()
 )
)));

static_assert(sizeof(decltype(
 progDenote(
 compile( Binop_Times< Binop_Plus<Const<2>, Const<2>> , Const<7> >() ),
 stack<>()
 )
)));

/* 
Theorem compile_correct : forall e, progDenote (compile e) nil = Some (expDenote e :: nil).
Abort.
*/
template <typename e>
auto compile_correct(decltype(progDenote(compile(e()))))
 -> Some< stack< expDenote(e()) > >; // Forward declared

/*
Lemma compile_correct' : forall e p s,
 progDenote (compile e ++ p) s = progDenote p (expDenote e :: s).
*/
template <typename e, typename p, int... s>
auto compile_correct_(decltype(
 progDenote( compile(e()) + p(), stack<s...>())
 ))
 -> decltype(
 progDenote(p(), stack<expDenote(e()), s...>() ) 
 );

/*
Inductive type : Set := Nat | Bool.
Inductive tbinop : type -> type -> type -> Set :=
  | TPlus : tbinop Nat Nat Nat
  | TTimes : tbinop Nat Nat Nat
  | TEq : forall t, tbinop t t Bool
  | TLt : tbinop Nat Nat Bool.

// Inductive type : Set := Nat | Bool.
enum class type { Nat, Bool };

// Helper enum to give names to the tbinop cases. 
enum class tbinop_Tag { TPlus, TTimes, TEq, TLt };

// Inductive tbinop : type -> type -> type -> Set
template <tbinop_Tag,type,type,type> struct tbinop
/* {} */; // General case intentionally not defined.

// | TPlus : tbinop Nat Nat Nat
template <> struct tbinop<tbinop_Tag::TPlus, type::Nat, type::Nat, type::Nat> {};

// | TTimes : tbinop Nat Nat Nat
template <> struct tbinop<tbinop_Tag::TTimes, type::Nat, type::Nat, type::Nat> {};

// | TEq : forall t, tbinop t t Bool
template <type t> struct tbinop<tbinop_Tag::TEq, t, t, type::Bool> {};

// | TLt : tbinop Nat Nat Bool
template <> struct tbinop<tbinop_Tag::TLt, type::Nat, type::Nat, type::Bool> {};

/*
C++ equivalent for:

Inductive texp : type -> Set :=
    | TNConst : nat -> texp Nat
    | TBConst : bool -> texp Bool
    | TBinop : forall t1 t2 t, tbinop t1 t2 t -> texp t1 -> texp t2 -> texp t.

// Helper enum
enum class texp_Tag { TNConst, TBConst, TBinop };

// Inductive texp : type -> Set
template <texp_Tag, type> struct texp;
template <> struct texp<texp_Tag::TNConst, type::Nat> { /* nat -> ?? */};
template <> struct texp<texp_Tag::TBConst, type::Bool> { /* bool -> ?? */ };

int main()
{
 tbinop<tbinop_Tag::TPlus, type::Nat, type::Nat, type::Nat> a;
 return 0;
}