glue.c

#include "gc_stack.h"

extern int is_ptr(value);

// Glue Code to interpret Coq natural numbers as C integers

// automatically generated by CertiCoq's glue code

unsigned long long get_unboxed_ordinal(value $v)
{
  return (unsigned long long) $v >> 1LL;
}

unsigned long long get_boxed_ordinal(value $v)
{
  return (unsigned long long) *((unsigned long long *) $v + -1LL) & 255LL;
}

unsigned long long get_Coq_Init_Datatypes_nat_tag(value $v)
{
  register _Bool $b;
  register unsigned long long $t;
  $b = is_ptr($v);
  if ($b) {
    $t = get_boxed_ordinal($v);
    switch ($t) {
    case 0:
      return 1;
      
    }
  } else {
    $t = get_unboxed_ordinal($v);
    switch ($t) {
    case 0:
      return 0;
      
    }
  }
}

value *get_args(value $v)
{
  return (value *) $v;
}


// currectly handwritten

int get_Coq_nat(value $v)
{
  register unsigned int $tag;
  register void *$args;
  $tag = get_Coq_Init_Datatypes_nat_tag($v);
  switch ($tag) {
  case 0:
    return 0;
  case 1:
    $args = get_args($v);
    return (1 + get_Coq_nat(*((value *) $args + 0)));
  }
}