The Coq mailing list

[Mario Frank <mafrank AT uni-potsdam.de>]

    Dear Andrew and Joomy,
    
    thank you for forwarding my eMail and also, many thanks for
    clarifying this.
    The version of CertiCoq I use already generates the glue files. I
    just did not
    know how to use them properly. Getting the result from the closure
    works
    like a charm now.
    
    I just still seem to provide the values to the closure in a wrong
    fashion.
    But I think the purpose of my question is achieved for now, since I
    wanted
    to make a proof of concept.
    
    Best Regards,
    Mario

Am 07.10.23 um 16:34 schrieb Andrew Appel:

Joomy Korkut writes,

For some reason I did not receive Mario Frank's email about CertiCoq even though I'm subscribed to coq-club. Here's my response:

Suppose your Coq code looks like this:

```

Definition coq_fun (val1 : nat) (val2 : nat) (val3 : Z) (val4 : nat) : Z := ...

```

On the Coq side, you can compile your function and generate glue code with these two commands:

```

CertiCoq Compile coq_fun.

CertiCoq Generate Glue -file "glue" [ Z, nat ].

```

This generates a C and a header file for your program (named based on the module path) and the glue code (here it's named glue.{c,h}).

Now, keep in mind that the compiled Coq code produces a closure when `body` is called on the C side. In your case, it's a closure for a curried function that takes 4 arguments. You can use the `call` function in the glue code to call it. I see that you're trying to inspect the result, but `Int_val` doesn't achieve that. You have to use the glue functions for that as well.

If you're trying to check whether the result of coq_fun is -1 (that is `Zneg xH` in Coq), you would have to write the code below for that:

```

#include "gc.h"

typedef enum { Z0, ZPOS, ZNEG } tag_Z;

typedef enum { XI, XO, XH } tag_positive;

int my_fun(value val1, value val2, value val3, value val4)

{

  struct thread_info *ti = make_tinfo();

  value tmp = body(ti);

  tmp = call(ti, tmp, val1);

  tmp = call(ti, tmp, val2);

  tmp = call(ti, tmp, val3);

  tmp = call(ti, tmp, val4);

  switch (get_Coq_Numbers_BinNums_Z_tag(tmp)) {

    case ZNEG:

      return (get_Coq_Numbers_BinNums_positive_tag(get_args(tmp)[0]) == XH ? -1 : 0);

    default:

      return 0;

  }

}

```

(though keep in mind that make_tinfo can fail, it currently doesn't return a null pointer when it fails to malloc. But maybe it should do that.)

(You should link gc_stack.c when you're compiling, such as `gcc -g -o prog main.c gc_stack.c prog.prog.c glue.c`)

For more examples (with actual primitives), you can look at our repo's (github.com/CertiCoq/VeriFFI) examples folder. We're currently writing a paper on this, so there should be better documentation soon.