extern "C" {
#include <stdio.h>
#include <stdlib.h>
#include <caml/mlvalues.h>
#include <caml/memory.h>
#include <caml/alloc.h>
#include <caml/fail.h>
#include <caml/callback.h>
}

// activate asserts for this file
#undef NDEBUG

#include <cassert>
#include <fstream>
#include <sstream>

#include <utap/utap.h>

// TODO move the utility caml callbacks (such as list and pair manipulation) into a dedicated file

using namespace UTAP;

class TimedAutomatonBuilder : public UTAP::SystemVisitor
{
public:
    // WARNING  to live in harmony with the GC, the visitor cannot live longer than `pa`
    //          having it as a reference should make it clearer to C++ devs
    explicit TimedAutomatonBuilder(value & pa): _nb_process(0), _process_array(pa) {}
    virtual ~TimedAutomatonBuilder() {}

    void visitSystemBefore(TimedAutomataSystem *ta) { /* nothing to do before */ }
    void visitSystemAfter(TimedAutomataSystem *) { /* nothing to do after */ }

    // global variables are passed to this method
    void visitVariable(variable_t &);

    bool visitTemplateBefore(template_t &) { /* visit templates? */ return false; }
    void visitTemplateAfter(template_t &) { /* nothing to do */ }

    void visitState(state_t &) {}
    void visitEdge(edge_t &) {}

    void visitInstance(instance_t &) {}
    void visitProcess(instance_t &);

    void
    visitFunction(function_t &)
    {
        // not supported by tiamo
        caml_failwith("functions are not supported by TiAMo");
    }
    void visitTypeDef(symbol_t) {}

    void visitIODecl(iodecl_t&) {} // supported by tiamo?
    void visitProgressMeasure(progress_t &) {} // supported by tiamo?
    void visitGanttChart(gantt_t&) {} // supported by tiamo?
    void visitInstanceLine(instanceLine_t &) {} // supported by tiamo?
    void visitMessage(message_t &) {} // supported by tiamo?

    void visitCondition(condition_t &) {} // supported by tiamo?
    void visitUpdate(update_t &) {} // supported by tiamo?

private:
    value & _process_array;
    int _nb_process;
};

/** An expression is one of:
 *      Constant of int
 *      Variable of int
 *      Clock of int
 *      Sum of expression * expression
 *      Product of expression * expression
 *      Subtraction of expression * expression
 *      Division of expression * expression
 *
 * `process` is of OCaml type 'int option' (None for global scope, Some procId for scope in proc
 * this applies to all other functions make_* (make_guard, make_channel, make_update...)
 */
extern "C" CAMLprim value
make_expression(value process, const expression_t &expression)
{
    CAMLparam1(process);
    CAMLlocal4(result, lhs, rhs, indices);
    value * cb_pointer = NULL;

    switch (expression.getKind())
    {
        case Constants::CONSTANT:
            assert(expression.getSize() == 0);
            result = caml_callback(*caml_named_value("cb_expression_constant"), Val_int(expression.getValue()));
            break;
        case Constants::DOT:
            caml_failwith("dot expressions are not supported in queries");
            break;
        case Constants::IDENTIFIER:
            // it is a clock
            if (expression.getType().isClock())
            {
                result = caml_callback2(*caml_named_value("cb_expression_clock"),
                                        process,
                                        caml_copy_string(expression.getSymbol().getName().c_str()));

            }
            // it is a variable
            else if (expression.getType().isIntegral())
            {
                result = caml_callback2(*caml_named_value("cb_expression_variable"),
                                        process,
                                        caml_copy_string(expression.getSymbol().getName().c_str()));
            }
            else
            {
                // not a clock nor a variable, fail
                std::stringstream exc_txt("invalid identifier ");
                exc_txt << expression.toString();
                caml_failwith(exc_txt.str().c_str());
            }

            break;
        case Constants::UNARY_MINUS:
            assert(expression.getSize() == 1);
            lhs = caml_callback(*caml_named_value("cb_expression_constant"), Val_int(0));
            rhs = make_expression(process, expression[0]);
            result = caml_callback2(*caml_named_value("cb_expression_substraction"), lhs, rhs);
            break;
        case Constants::PLUS:
        case Constants::MULT:
        case Constants::MINUS:
        case Constants::DIV:
            switch (expression.getKind())
            {
                case Constants::PLUS:
                    cb_pointer = caml_named_value("cb_expression_sum");
                    break;
                case Constants::MULT:
                    cb_pointer = caml_named_value("cb_expression_product");
                    break;
                case Constants::MINUS:
                    cb_pointer = caml_named_value("cb_expression_substraction");
                    break;
                case Constants::DIV:
                    cb_pointer = caml_named_value("cb_expression_division");
                    break;
                default: // cannot happen
                    caml_failwith("this line of code is unreacheable");
            }
            assert(expression.getSize() > 1);
            lhs = make_expression(process, expression[0]);
            rhs = make_expression(process, expression[1]);
            result = caml_callback2(*cb_pointer, lhs, rhs);
            for (int i = 2; i < expression.getSize(); ++i)
            {
                lhs = make_expression(process, expression[i]);
                result = caml_callback2(*cb_pointer, lhs, result);
            }
            break;
        case Constants::ARRAY:
            indices = callback(*caml_named_value("cb_empty_list"), Val_unit);
            {
                expression_t current = expression;
                while (current.getKind() == Constants::ARRAY)
                {
                    assert(current.getSize() == 2);
                    indices = caml_callback2(*caml_named_value("cb_build_list"),
                                             make_expression(process, current[1]),
                                             indices);
                    current = current[0];
                }
                result = caml_callback3(*caml_named_value("cb_expression_array"),
                                        process,
                                        caml_copy_string(current.toString().c_str()),
                                        indices);
            }
            break;

        case Constants::COST:
            printf("expr is a cost\n");
        case Constants::RATE:
            printf("expr is a rate\n");
        default:
            printf("expr is %s\n", expression.toString().c_str());
            caml_failwith("not a valid expression");
    }

    CAMLreturn(result);
}

/** A channel is:
 *      either a channel id
 *      or an access in an array of channels
 */
extern "C" CAMLprim value
make_channel(const expression_t &chanexp, value process)
{
    CAMLparam1(process);
    CAMLlocal2(result, indices);

    switch (chanexp.getKind())
    {
        case Constants::IDENTIFIER:
            result = caml_callback(*caml_named_value("cb_channel_simple"),
                                   caml_copy_string(chanexp.toString().c_str()));
            break;
        case Constants::ARRAY:
            indices = callback(*caml_named_value("cb_empty_list"), Val_unit);
        {
            expression_t current = chanexp;
            while (current.getKind() == Constants::ARRAY)
            {
                assert(current.getSize() == 2);
                indices = caml_callback2(*caml_named_value("cb_build_list"),
                                         make_expression(process, current[1]),
                                         indices);
                current = current[0];
            }
            result = caml_callback2(*caml_named_value("cb_channel_array"),
                                    caml_copy_string(current.toString().c_str()),
                                    indices);
        }
            break;
        default:
            printf("not a valid channel reference: %s\n", chanexp.toString().c_str());
            caml_failwith("invalid channel reference");
    }

    CAMLreturn(result);
}

/** An atomic guard is a comparison between two expressions */
extern "C" CAMLprim value
make_atomic_guard(value process, const expression_t &atom_guard)
{
    CAMLparam1(process);
    CAMLlocal3(result, sonleft, sonright);
    assert(atom_guard.getSize() == 2);
    sonleft = make_expression(process, atom_guard[0]);
    sonright = make_expression(process, atom_guard[1]);
    value * cb_pointer = NULL;
    switch (atom_guard.getKind())
    {
        case Constants::LT:
            cb_pointer = caml_named_value("cb_atomic_guard_LT");
            break;
        case Constants::LE:
            cb_pointer = caml_named_value("cb_atomic_guard_LE");
            break;
        case Constants::EQ:
            cb_pointer = caml_named_value("cb_atomic_guard_EQ");
            break;
        case Constants::NEQ:
            cb_pointer = caml_named_value("cb_atomic_guard_NEQ");
            break;
        case Constants::GE:
            cb_pointer = caml_named_value("cb_atomic_guard_GE");
            break;
        case Constants::GT:
            cb_pointer = caml_named_value("cb_atomic_guard_GT");
            break;
        default:
            caml_failwith("not a valid atomic guard");
    }
    assert(cb_pointer);
    result = caml_callback2(*cb_pointer, sonleft, sonright);
    CAMLreturn(result);
}

/** A guard is a conjunction (as a list) of atomic guards */
extern "C" CAMLprim value
make_guard(value process, const expression_t &guard)
{
    CAMLparam1(process);
    CAMLlocal1(result);
    result = caml_callback(*caml_named_value("cb_empty_list"), Val_unit);
    if (!guard.empty())
    {
        switch (guard.getKind())
        {
            case Constants::LT:
            case Constants::LE:
            case Constants::EQ:
            case Constants::NEQ:
            case Constants::GT:
            case Constants::GE:
                result = caml_callback2(*caml_named_value("cb_build_list"),
                                        make_atomic_guard(process, guard),
                                        result);
                break;
            case Constants::AND:
                for (int i = 0; i != guard.getSize(); ++i)
                {
                    result = caml_callback2(*caml_named_value("cb_concat_list"),
                                            make_guard(process, guard[i]),
                                            result);
                }
                break;
            case Constants::CONSTANT:
                assert(guard.getSize() == 0);
                assert(guard.isTrue());
                // nothing to do, empty guard
                break;
            default:
                caml_failwith("not a valid guard");
        }
    }
    CAMLreturn(result);
}

/** a query is a boolean combination of atomic queries */
/** an atomic query is either a regular atomic guard, or a location specification */
extern "C" CAMLprim value
make_query(const expression_t &query)
{
    CAMLparam0();
    CAMLlocal4(result, tmp, procId, locId);

    switch (query.getKind()) {
        case Constants::AND:
            result = make_query(query[0]);
            for (int i = 1; i != query.getSize(); ++i)
            {
                tmp = make_query(query[i]);
                result = caml_callback2(*caml_named_value("cb_qb_make_and"),
                                        result,
                                        tmp);
            }
            break;

        case Constants::OR:
            result = make_query(query[0]);
            for (int i = 1; i != query.getSize(); ++i)
            {
                tmp = make_query(query[i]);
                result = caml_callback2(*caml_named_value("cb_qb_make_or"),
                                        result,
                                        tmp);
            }
            break;

        // there are no global location
        case Constants::DOT:
            // NB: the string right of the dot is: query[0].getType().getRecordLabel(query.getIndex()).c_str()
            procId = caml_callback(*caml_named_value("cb_get_proc"),
                                   caml_copy_string(query.getSymbol().getName().c_str()));
            assert(Int_val(procId) >= 0);
            locId = caml_callback2(*caml_named_value("cb_get_loc"),
                                   procId,
                                   caml_copy_string(query.toString().c_str()));
            assert(Int_val(locId) >= 0);
            result = caml_callback2(*caml_named_value("cb_qb_location"), procId, locId);
            break;

        default:
            result = make_atomic_guard(Val_int(-1), query);
            break;
    }

    CAMLreturn(result);
}

// transforms an assignment 'e @= f' into 'e = e @ f'
// where @ is one of +,-,*,/
expression_t
normalize_assignment(const expression_t &update)
{
    switch (update.getKind())
    {
        case Constants::ASSPLUS:
        case Constants::ASSMINUS:
        case Constants::ASSMULT:
        case Constants::ASSDIV:
        {
            expression_t new_rhs;
            Constants::kind_t op;
            switch (update.getKind())
            {
                case Constants::ASSPLUS:
                    op = Constants::PLUS;
                    break;
                case Constants::ASSMINUS:
                    op = Constants::MINUS;
                    break;
                case Constants::ASSMULT:
                    op = Constants::MULT;
                    break;
                case Constants::ASSDIV:
                    op = Constants::DIV;
                    break;
                default: // cannot happen
                    assert(false);
                    throw "cannot happen";
            }
            new_rhs = expression_t::createBinary(op, update[0], update[1]);
            return expression_t::createBinary(Constants::ASSIGN, update[0], new_rhs);
        }
        default:
            return update;
    }
}

extern "C" CAMLprim value
make_update(value process, const expression_t &u)
{
    CAMLparam1(process);
    CAMLlocal4(result, lhs, rhs, tmp);
    // remove compound assignments (+=, -=, *=, /=)
    expression_t update = normalize_assignment(u);

    result = caml_callback(*caml_named_value("cb_empty_list"), Val_unit);
    switch (update.getKind())
    {
        case Constants::CONSTANT:
            // nothing to do, empty list
            break;
        case Constants::ASSIGN:
            assert(update.getSize() == 2);
            lhs = make_expression(process, update[0]);
            rhs = make_expression(process, update[1]);
            tmp = caml_callback2(*caml_named_value("cb_build_pair"), lhs, rhs);
            result = caml_callback2(*caml_named_value("cb_build_list"), tmp, result);
            break;
        case Constants::COMMA:
            for (int i = 0; i < update.getSize(); ++i)
            {
                result = caml_callback2(*caml_named_value("cb_concat_list"),
                                        make_update(process, update[i]), result);
            }
            break;
        default:
            caml_failwith("invalid kind of update");
    }
    CAMLreturn(result);
}

// a helper function to evaluate an initial value
int
eval_expr(const expression_t &expr, value proc)
{
    CAMLparam1(proc);
    CAMLlocal1(tmp);
    tmp = make_expression(proc, expr);
    int res = Int_val(caml_callback(*caml_named_value("cb_evaluate_expr"), tmp));
    CAMLreturnT(int, res);
}

// a helper function to remove parameters from an expression
expression_t
subst_params(const expression_t &expr, const std::map<symbol_t, expression_t> &mapping)
{
    expression_t res = expr;
    for (auto &varval : mapping)
    {
        res = res.subst(varval.first, varval.second);
    }
    return res;
}

void
handle_declaration(variable_t &var, value proc, const std::map<symbol_t, expression_t> &mapping)
{
    CAMLparam1(proc);
    CAMLlocal3(cb_array, cb_cell, indices);

    type_t varType = var.uid.getType();
    // a clock
    if (varType.isClock())
    {
        caml_callback2(*caml_named_value("cb_register_clock"),
                       proc,
                       caml_copy_string(var.uid.getName().c_str()));
    }
    // a variable
    else if (varType.isIntegral())
    {
        int init_value = 0;
        // evaluate the initializing expression in the caml world
        if (!var.expr.empty())
        {
            init_value = eval_expr(subst_params(var.expr, mapping), proc);
        }

        value * cb_pointer = NULL;
        // for a const variable
        if (varType.isConstant())
        {
            cb_pointer = caml_named_value("cb_register_constant");
        }
        else
        {
            cb_pointer = caml_named_value("cb_register_variable");
        }
        assert(cb_pointer);

        caml_callback3(*cb_pointer,
                       proc,
                       caml_copy_string(var.uid.getName().c_str()),
                       Val_int(init_value));
    }
    // a channel
    else if (varType.isChannel())
    {
        // raise a warning on urgent and broadcast channels, which are not supported by TiAMo
        if (varType.is(Constants::URGENT))
        {
            caml_failwith("Urgent channels are not supported by TiAMo");
        }
        else if (varType.is(Constants::BROADCAST))
        {
            caml_failwith("Broadcast channels are not supported by TiAMo");
        }
        // register channel
        caml_callback2(*caml_named_value("cb_register_channel"),
                       proc,
                       caml_copy_string(var.uid.getName().c_str()));
    }
    // an array
    else if (varType.isArray())
    {
        // recall: varType is an array, so it has two subtypes:
        //      the first one (varType.getSub()) is the element type
        //      the second one (varType.getArraySize()) is the array size

        // to differentiate with an array of clocks
        bool is_clock = varType.getSub().isClock();
        // to differentiate between an array of channels or of integers
        bool is_channel = varType.getSub().isChannel();
        // to differentiate between const and non-const arrays of integers
        bool is_const = varType.getSub().isConstant();

        if (is_channel)
        {
            cb_array = *caml_named_value("cb_register_channel_array_name");
            cb_cell = *caml_named_value("cb_register_channel_array_cell");
        }
        else if (is_clock)
        {
            cb_array = *caml_named_value("cb_register_clock_array_name");
            cb_cell = *caml_named_value("cb_register_clock_array_cell");
        }
        else if (is_const)
        {
            cb_array = *caml_named_value("cb_register_const_array_name");
            cb_cell = *caml_named_value("cb_register_const_array_cell");
        }
        else
        {
            cb_array = *caml_named_value("cb_register_array_name");
            cb_cell = *caml_named_value("cb_register_array_cell");
        }
        // partially apply with `proc` (1st argument common to all invocations)
        cb_array = caml_callback(cb_array, proc);
        cb_cell = caml_callback(cb_cell, proc);

        // if varType.getSub() is itself an array type, this makes arrays of arrays
        // to handle the general case, we need to retrieve all dimensions, say in a vector
        //      BEWARE of the order: top-most in the type = right-most in the declaration
        // then use this vector to iterate over the cells of the array and declare them as
        // regular variables with (possible several pairs of) square brackets []
        std::vector<int> multiSize;
        type_t currentType = varType;
        while (currentType.isArray())
        {
            // after looking at type_t::toDeclarationString (file type.cpp),
            // i discovered that the expression of the size of the array is as follows
            expression_t arraySizeExpr = currentType.getArraySize().getRange().second.get(0);
            // evaluate the size expression
            int arraySize = eval_expr(subst_params(arraySizeExpr, mapping), proc);
            // push this size in the vector
            multiSize.push_back(arraySize);
            // recursively descend in the type
            currentType = currentType.getSub();
        }

        indices = caml_callback(*caml_named_value("cb_empty_list"), Val_unit);
        for (auto it = multiSize.rbegin(); it != multiSize.rend(); ++it)
        {
            indices = caml_callback2(*caml_named_value("cb_build_list"),
                                     Val_int(*it),
                                     indices);
        }
        // first, register array name with its full dimension
        caml_callback2(cb_array,
                       caml_copy_string(var.uid.getName().c_str()),
                       indices);

        std::vector<int> index(multiSize.size(), 0);
        bool index_is_zero = true;
        do
        {
            indices = caml_callback(*caml_named_value("cb_empty_list"), Val_unit);
            for (auto it = index.rbegin(); it != index.rend(); ++it)
            {
                indices = caml_callback2(*caml_named_value("cb_build_list"),
                                         Val_int(*it),
                                         indices);
            }

            if (is_channel || is_clock) // no initial value, register cells directly
            {
                caml_callback2(cb_cell,
                               caml_copy_string(var.uid.getName().c_str()),
                               indices);
            }
            else // integer array, need to compute initial values
            {
                // retrieve the right initial value
                expression_t initExpr = var.expr;
                for (int i = 0; i != index.size(); ++i)
                {
                    // TODO what if the initExpr is a reference to a previously declared array?
                    //      we should register (in C) the declared arrays, and substitute
                    assert(multiSize[i] == initExpr.getSize());
                    assert(index[i] < initExpr.getSize());
                    initExpr = initExpr[index[i]];
                }
                int cellValue = eval_expr(subst_params(initExpr, mapping), proc);
                // declare current cell
                caml_callback3(cb_cell,
                               caml_copy_string(var.uid.getName().c_str()),
                               indices,
                               Val_int(cellValue));
            }

            // update index
            index_is_zero = true;
            for (int i = 0; i != index.size() ; ++i)
            {
                if (index[i] == multiSize[i]-1)
                {
                    index[i] = 0;
                }
                else
                {
                    index[i]++;
                    index_is_zero = false;
                    break;
                }
            }
        } while (!index_is_zero);


    }
    else
    {
        printf("invalid global declaration %s\n", var.toString().c_str());
        caml_failwith("invalid global declaration");
    }

    // return nothing
    CAMLreturn0;
}

// called when visiting global declarations
void
TimedAutomatonBuilder::visitVariable(variable_t &var)
{
    CAMLparam0();
    handle_declaration(var, caml_callback(*caml_named_value("cb_make_None"), Val_unit), std::map<symbol_t, expression_t>());
    CAMLreturn0;
}

void
TimedAutomatonBuilder::visitProcess(instance_t &process)
{
    CAMLparam0();
    CAMLlocal4(guard, edge_list, update, tmpedge);
    CAMLlocal2(proc_id, procref);
    CAMLlocalN(args, 8);
    CAMLlocal1(loc_array);
    CAMLlocal1(tmpproc);
    loc_array = caml_callback(*caml_named_value("cb_build_location_array"), Val_int(process.templ->states.size()));

    // ensure that the argument is an instance
    assert(&process == process.uid.getData());
    // ensure that process has no unbound parameters
    assert(process.parameters.getSize() == process.arguments);
    assert(process.unbound == 0);
    // ensure that the parent template is a real template
    assert(process.templ->arguments == 0);
    assert(process.templ->parameters.getSize() == process.parameters.getSize());
    // ensure that the parent template is its own parent
    assert(process.templ->templ == process.templ);


    proc_id = Val_int(_nb_process++);
    procref = caml_callback(*caml_named_value("cb_make_Some"), proc_id);


    // walk the parent template, replacing arguments with the mapping, to build the process
    // register process variables
    for (auto &var : process.templ->variables)
    {
        handle_declaration(var, procref, process.mapping);
    }

    // ensure that there are no branchpoints
    if (process.templ->branchpoints.size() != 0)
    {
        caml_failwith("branchpoints are not supported in TiAMo");
    }

    // visit all locations once, to associate them a unique ID
    std::map<state_t *, int> location_ids;
    int locid = 0;
    for (auto & location : process.templ->states)
    {
        location_ids[&location] = locid++;
    }

    // revisit the locations to actually build them in OCaml
    for (auto & location : process.templ->states)
    {
        edge_list = caml_callback(*caml_named_value("cb_empty_list"), Val_unit);
        for (auto & edge : process.templ->edges)
        {
            assert(edge.srcb == NULL && edge.dstb == NULL);
            if (edge.src == &location)
            {
                // TODO currently support at most one non-deterministic select
                assert(edge.select.getSize() < 2);
                symbol_t selectVar;
                std::vector<int32_t> selectValues;
                if (edge.select.getSize() != 0)
                {
                    selectVar = edge.select[0];
                    int valInf = eval_expr(selectVar.getType().getRange().first, procref);
                    int valSup = eval_expr(selectVar.getType().getRange().second, procref);
                    for (int32_t i = valInf; i <= valSup; ++i)
                    {
                        selectValues.push_back(i);
                    }
                }
                else
                {
                    selectValues.push_back(0);
                }


                int srcid = location_ids[edge.src];
                int dstid = location_ids[edge.dst];
                // the source
                args[0] = Val_int(srcid);
                // the destination
                args[1] = Val_int(dstid);
                // the synchronization (if any)
                if (edge.sync.empty())
                {
                    args[4] = caml_callback(*caml_named_value("cb_make_None"), Val_unit);
                }
                else
                {
                    // if not empty, edge.sync must be a synchronization
                    // TODO channels are currently resolved WITHOUT the select variable, if any
                    assert(edge.sync.getKind() == Constants::SYNC);
                    switch (edge.sync.getSync())
                    {
                        assert(edge.sync.getSize() == 1);
                        // receiving channel
                        case Constants::SYNC_QUE:
                            args[4] = caml_callback(*caml_named_value("cb_recv_channel"),
                                                    make_channel(subst_params(edge.sync[0], process.mapping), procref));
                            break;
                        // sending channel
                        case Constants::SYNC_BANG:
                            args[4] = caml_callback(*caml_named_value("cb_send_channel"),
                                                    make_channel(subst_params(edge.sync[0], process.mapping), procref));
                            break;
                        // TODO what is the semantics of this?
                        case Constants::SYNC_CSP:
                            caml_failwith("CSP synchronization is not supported by TiAMo");
                            break;
                    }
                }
                // the containing process id
                args[5] = proc_id;
                // whether the edge is controllable
                args[6] = Val_bool(edge.control);

                for (auto selval : selectValues)
                {
                    std::map<symbol_t, expression_t> local_mapping = process.mapping;
                    local_mapping[selectVar] = expression_t::createConstant(selval);

                    // the guard
                    args[2] = make_guard(procref, subst_params(edge.guard, local_mapping));
                    // the updates
                    args[3] = make_update(procref, subst_params(edge.assign, local_mapping));

                    // build the edge
                    tmpedge = caml_callbackN(*caml_named_value("cb_build_edge"), 7, args);
                    // add it to the edge list of the current location
                    edge_list = caml_callback2(*caml_named_value("cb_build_list"), tmpedge, edge_list);
                }
            }
        }
        // the location id
        args[0] = Val_int(location_ids[&location]);
        // the location name
        args[1] = caml_copy_string(location.uid.getName().c_str());
        // TODO is that correct?
        args[2] = Val_bool(location.uid.getType().is(Constants::COMMITTED));
        // TODO is that correct?
        args[3] = Val_bool(location.uid.getType().is(Constants::URGENT));
        // the invariant
        args[4] = make_guard(procref, subst_params(location.invariant, process.mapping));
        // the list of edges (built above)
        args[5] = edge_list;
        // the containing process id
        args[6] = proc_id;
        // the rate of the location
        args[7] = location.costRate.empty() ?
            caml_callback(*caml_named_value("cb_make_None"), Val_unit) :
            caml_callback(*caml_named_value("cb_make_Some"), make_expression(procref, subst_params(location.costRate, process.mapping)));
        // GC-friendly version of: loc_array[loc_id] = build_location()
        caml_modify(&Field(loc_array, location_ids[&location]),
                    caml_callbackN(*caml_named_value("cb_build_location"), 8, args));
    }
    // we now build the process
    // the process name
    args[0] = caml_copy_string(process.uid.getName().c_str());
    // the process id
    args[1] = proc_id;
    // the array of locations (built above)
    args[2] = loc_array;
    // the id of the initial location
    args[3] = Val_int(location_ids[static_cast<state_t*>(process.templ->init.getData())]);

    // build the process
    tmpproc = caml_callbackN(*caml_named_value("cb_build_process"), 4, args);

    // GC-friendly version of: _process_array[proc_id] = build_process()
    caml_modify(&Field(_process_array, Int_val(proc_id)),
                tmpproc);

    CAMLreturn0;
}

#include "querybuilder.c"

#include "utap/typechecker.h"

extern "C" CAMLprim value
xta_from_xmlfile(value filename, value qfilename, value enable_cora)
{
    CAMLparam3(filename, qfilename, enable_cora);
    CAMLlocal3(process_array, queryguard, result);

    // parse the input with the library utap
    UTAP::TimedAutomataSystem * ta = new UTAP::TimedAutomataSystem(Bool_val(enable_cora));
    int parse_res = parseXMLFile(String_val(filename), ta, true);
    assert(parse_res == 0);

    // running the type checker is mandatory to appropriately set costs (for CORA)
    UTAP::TypeChecker type_checker(ta);
    // TODO I do not understand how the type_checker works
    // building it correctly sets costs (CORA)
    // accepting it detects more errors but deletes the costs...
//    ta->accept(type_checker);

    // the type checker stores errors in the ta
    if (ta->hasErrors())
    {
        for (auto &e : ta->getErrors())
        {
            std::cerr << e << "\n";
        }
        std::cerr << "the input model has errors, aborting\n";
        exit(1);
    }

    // also report warnings
    if (ta->hasWarnings())
    {
        for (auto &w : ta->getWarnings())
        {
            std::cerr << w << "\n";
        }
        std::cerr << "the input model has warnings (see above)\n"
        << "computation goes on, but may be incorrect.\n";
    }

    // currently, we handle only one query
    assert(ta->getQueries().size() < 2);
    std::string squery;
    if (ta->getQueries().size() != 0)
    {
        squery = ta->getQueries()[0].formula;
    }
    else
    {
        // look into the .q file
        std::ifstream inqfile(String_val(qfilename));
        std::getline(inqfile, squery);
    }
    assert(squery != "");

    // build the array of process, to be populated by the TA visitor
    process_array = caml_callback(*caml_named_value("cb_build_process_array"),
                                  Val_int(ta->getProcesses().size()));

    // WARNING  to live in harmony with the GC, the visitor cannot live longer than the
    //          value (caml array) `process_array`
    TimedAutomatonBuilder v(process_array);
    ta->accept(v);

    // build the caml TA (before parsing the query)
    result = caml_callback(*caml_named_value("cb_build_ta"), process_array);

    // parse the query
    QueryBuilder qb(ta);
    parseProperty(squery.c_str(), &qb);
    const expression_t & query = qb.getResult();
    assert(query.getKind() == Constants::EF);
    queryguard = make_query(query[0]);

    // set the query
    result = caml_callback2(*caml_named_value("cb_set_query"), result, queryguard);

    CAMLreturn(result);
}