/*++
Copyright (c) 2010 Microsoft Corporation

Module Name:

    z3_theory_stubs.c

Abstract:

    OCaml C bindings for callbacks between OCaml and C for
    theory plugins. 
    The API for theory plugins require associating a set of
    callbacks as C function pointers.  
    We use the following strategy:

    - store in the user_ext_data blob that theory constructors allow
      a record of callback functions.

    - define catch-all static callback functions that access the 
      ML record with the callbacks. It then invokes these through user-registered
      application functions that apply the callback stored in the record to the
      actual parameters.
      It is tempting to avoid this user-registered callback and directly access 
      the record of callback functions and apply the proper field. 
      However, the layout of records appears to be opaque, or at least we assume it is
      so, from the C runtime.

Author:


Revision History:
--*/

#include <stddef.h>
#include <string.h>
#include <caml/mlvalues.h>
#include <caml/memory.h>
#include <caml/alloc.h>
#include <caml/fail.h>
#include <caml/callback.h>
#ifdef Custom_tag
#include <caml/custom.h>
#include <caml/bigarray.h>
#endif

#include "z3.h"

#define ML_SIZE(_ty) ((sizeof(_ty) + sizeof(value) - 1)/ sizeof(value))

static value mk_func_decl(Z3_func_decl f) {
    value _f = alloc(ML_SIZE(Z3_func_decl), Abstract_tag);
    *((Z3_func_decl*) Bp_val(_f)) = f;
    return _f;
}

static value Val_ast(Z3_ast a) {
    value _a = alloc(ML_SIZE(Z3_ast), Abstract_tag);
    *((Z3_ast*) Bp_val(_a)) = a;
    return _a;
}


static value Val_ast_array(unsigned int sz, Z3_ast const args[]) {
    value res;
    Z3_ast* args1;
    unsigned int i;
    args1 = malloc((sz+1)*sizeof(Z3_ast));
    for (i = 0; i < sz; ++i) {
        args1[i] = args[i];
    }
    args1[sz] = 0;
    res = alloc_array((value (*)(char const*))Val_ast, (const char**)args1);
    free(args1);
    return res;
}

// ------------------
// get_theory_callbacks
// 

value get_theory_callbacks(value th) 
{
    Z3_theory _th = *((Z3_theory*) Bp_val(th));
    return (value) Z3_theory_get_ext_data(_th);
}

// ------------------
// delete_theory
// 
static void delete_callback_static(Z3_theory th) 
{
    CAMLparam0();
    CAMLlocal1(f);  
    value user_data = (value) Z3_theory_get_ext_data(th);
    f = *(caml_named_value("apply_delete")) ;
    callback(f, user_data);
    remove_global_root(&user_data);
    CAMLreturn0;
}

#define SET_CALLBACK(_cb_name)                     \
    value set_ ## _cb_name ## _callback_register(value th)  \
    {                                              \
        CAMLparam1(th);                                         \
        Z3_theory _th = *((Z3_theory*) Bp_val(th));                     \
        Z3_set_ ## _cb_name ## _callback(_th, _cb_name ## _callback_static);   \
        CAMLreturn(Val_unit);                                           \
    }                                                                   \

SET_CALLBACK(delete);


// ------------------
// mk_theory
// 

value mk_theory_register(value context, value name, value user_data) 
{
    CAMLparam3(context, name, user_data);
    Z3_context _context = *((Z3_context *) Bp_val(context));
    value _th;
    Z3_theory th;
    register_global_root(&user_data);
    th = Z3_mk_theory(_context, String_val(name), (void*)user_data);
    Z3_set_delete_callback(th, delete_callback_static);
    _th = alloc(ML_SIZE(Z3_context), Abstract_tag);
    *((Z3_theory*) Bp_val(_th)) = th;
    CAMLreturn(_th);
}


// -------------------
// reduce_app_callback

static Z3_bool reduce_app_callback_static(Z3_theory th, Z3_func_decl f, unsigned num_args, Z3_ast const args[], Z3_ast* r) {
    CAMLparam0();
    CAMLlocal4(cb, _r, _v, _args);
    value user_data;
    Z3_bool result;

    _args = Val_ast_array(num_args, args);

    user_data = (value) Z3_theory_get_ext_data(th);

    cb = *(caml_named_value("apply_reduce_app"));
    _r = callback3(cb, user_data, mk_func_decl(f), _args);

    cb = *(caml_named_value("is_some"));
    _v = callback(cb, _r);
    result = 0 != Bool_val(_v);

    if (result && r) {
        cb = *(caml_named_value("get_some"));
        _v = callback(cb, _r);
        *r = *((Z3_ast*) Bp_val(_v));
    }

    CAMLreturn (result);
}

SET_CALLBACK(reduce_app);

// -------------------
// reduce_eq_callback

static Z3_bool reduce_eq_callback_static(Z3_theory th, Z3_ast a, Z3_ast b, Z3_ast * r) 
{
    CAMLparam0();
    CAMLlocal5(cb, _r, _a, _b, _v);
    value user_data;
    Z3_bool result;

    _a = Val_ast(a);
    _b = Val_ast(b);

    user_data = (value) Z3_theory_get_ext_data(th);

    cb = *(caml_named_value("apply_reduce_eq"));
    _r = callback3(cb, user_data, _a, _b);

    cb = *(caml_named_value("is_some"));
    _v = callback(cb, _r);
    result = 0 != Bool_val(_v);

    if (result && r) {
        cb = *(caml_named_value("get_some"));
        _v = callback(cb, _r);
        *r = *((Z3_ast*) Bp_val(_v));
    }

    CAMLreturn (result);
}

SET_CALLBACK(reduce_eq);


// -------------------
// reduce_distinct

static Z3_bool reduce_distinct_callback_static(Z3_theory th, unsigned n, Z3_ast const args[], Z3_ast * r)
{
    CAMLparam0();
    CAMLlocal4(cb, _r, _args, _v);
    value user_data;
    Z3_bool result;

    _args = Val_ast_array(n, args);

    user_data = (value) Z3_theory_get_ext_data(th);

    cb = *(caml_named_value("apply_reduce_distinct"));
    _r = callback2(cb, user_data, _args);

    cb = *(caml_named_value("is_some"));
    _v = callback(cb, _r);
    result = 0 != Bool_val(_v);

    if (result && r) {
        cb = *(caml_named_value("get_some"));
        _v = callback(cb, _r);
        *r = *((Z3_ast*) Bp_val(_v));
    }

    CAMLreturn (result);
}

SET_CALLBACK(reduce_distinct);

// -------------------
// new_app

#define AST_CALLBACK(_cb_name) \
static void _cb_name##_callback_static(Z3_theory th, Z3_ast a)        \
{                                                           \
    CAMLparam0();                                           \
    CAMLlocal3(cb, _a, user_data);                          \
    _a = Val_ast(a);                                         \
    user_data = (value) Z3_theory_get_ext_data(th);         \
    cb = *(caml_named_value("apply_" #_cb_name));           \
    callback2(cb, user_data, _a);                           \
    CAMLreturn0;                                            \
}                                                           \

AST_CALLBACK(new_app);
SET_CALLBACK(new_app);

// -------------------
// new_elem

AST_CALLBACK(new_elem);
SET_CALLBACK(new_elem);

// -------------------
// init_search

#define TH_CALLBACK(_cb_name) \
static void _cb_name##_callback_static(Z3_theory th)        \
{                                                           \
    CAMLparam0();                                           \
    CAMLlocal2(cb, user_data);                              \
    user_data = (value) Z3_theory_get_ext_data(th);         \
    cb = *(caml_named_value("apply_" #_cb_name));           \
    callback(cb, user_data);                                \
    CAMLreturn0;                                            \
}                                                           \

TH_CALLBACK(init_search);
SET_CALLBACK(init_search);

// -------------------
// push

TH_CALLBACK(push);
SET_CALLBACK(push);

TH_CALLBACK(pop);
SET_CALLBACK(pop);

TH_CALLBACK(restart);
SET_CALLBACK(restart);

TH_CALLBACK(reset);
SET_CALLBACK(reset);

        
#define FC_CALLBACK(_cb_name) \
    static Z3_bool _cb_name##_callback_static(Z3_theory th)             \
    {                                                                   \
    CAMLparam0();                                                       \
    CAMLlocal3(cb, r, user_data);                                       \
    user_data = (value) Z3_theory_get_ext_data(th);                     \
    cb = *(caml_named_value("apply_" #_cb_name));                       \
    r = callback(cb, user_data);                                        \
    CAMLreturn (Bool_val(r) != 0);                                      \
    }                                                                   \
    
FC_CALLBACK(final_check);
SET_CALLBACK(final_check);

#define AST_AST_CALLBACK(_cb_name) \
    static void _cb_name##_callback_static(Z3_theory th, Z3_ast a, Z3_ast b)     \
    {                                                                   \
        CAMLparam0();                                                   \
        CAMLlocal4(cb, _a, _b, user_data);                              \
        _a = Val_ast(a);                                                \
        _b = Val_ast(b);                                                \
        user_data = (value) Z3_theory_get_ext_data(th);                 \
        cb = *(caml_named_value("apply_" #_cb_name));                   \
        callback3(cb, user_data, _a, _b);                               \
        CAMLreturn0;                                                    \
    }                                                                   \
    
AST_AST_CALLBACK(new_eq);
SET_CALLBACK(new_eq);

AST_AST_CALLBACK(new_diseq);
SET_CALLBACK(new_diseq);

#define AST_BOOL_CALLBACK(_cb_name) \
    static void _cb_name##_callback_static(Z3_theory th, Z3_ast a, Z3_bool b)     \
    {                                                                   \
        CAMLparam0();                                                   \
        CAMLlocal4(cb, _a, _b, user_data);                              \
        _a = Val_ast(a);                                                \
        _b = Val_bool(b);                                               \
        user_data = (value) Z3_theory_get_ext_data(th);                 \
        cb = *(caml_named_value("apply_" #_cb_name));                   \
        callback3(cb, user_data, _a, _b);                               \
        CAMLreturn0;                                                    \
    }                                                                   \

    
AST_BOOL_CALLBACK(new_assignment);
SET_CALLBACK(new_assignment);

AST_CALLBACK(new_relevant);
SET_CALLBACK(new_relevant);