%% -*- erlang-indent-level: 2 -*-
%%------------------------------------------------------------------------------

%%====================================================================
%% Types
%%====================================================================

%% Code and Monitor servers' info.
-record(svs, {
  code    :: pid(),
  monitor :: pid()
}).

%% Tags of an AST's node.
-record(tags, {
  this = undefined :: cuter_cerl:tag() | undefined,
  next = undefined :: cuter_cerl:tag() | undefined
}).

-type loaded_ret_atoms() :: cover_compiled | preloaded | non_existing.
-type servers() :: #svs{}.
-type ast_tags() :: #tags{}.

%%====================================================================
%% Directories
%%====================================================================

-define(RELATIVE_TMP_DIR, "temp").
-define(PYTHON_CALL, ?PYTHON_PATH ++ " -u " ++ ?PRIV ++ "/cuter_interface.py").

%%====================================================================
%% Prefixes
%%====================================================================

-define(DEPTH_PREFIX, '__conc_depth').
-define(EXECUTION_PREFIX, '__conc_prefix').
-define(SYMBOLIC_PREFIX, '__s').
-define(CONCOLIC_PREFIX_MSG, '__concm').
-define(ZIPPED_VALUE_PREFIX, '__czip').
-define(CONCOLIC_PREFIX_PDICT, '__concp').
-define(FUNCTION_PREFIX, '__cfunc').
-define(UNBOUND_VAR_PREFIX, '__uboundvar').
-define(BRANCH_TAG_PREFIX, '__branch_tag').
-define(VISITED_TAGS_PREFIX, '__visited_tags').
-define(EXECUTION_COUNTER_PREFIX, '__exec_counter').

%%====================================================================
%% Flags & Default Values
%%====================================================================

-define(LOGGING_FLAG, ok).
-define(DELETE_TRACE, ok).
-define(LOG_UNSUPPORTED_MFAS, ok).
%%-define(VERBOSE_SCHEDULER, ok).
%%-define(VERBOSE_FILE_DELETION, ok).
%%-define(VERBOSE_SOLVING, ok).
%%-define(VERBOSE_MERGING, ok).
%%-define(VERBOSE_REPORTING, ok).
-define(USE_SPECS, ok).

%%====================================================================
%% Solver Responses
%%====================================================================

-define(RSP_MODEL_DELIMITER_START, <<"model_start">>).
-define(RSP_MODEL_DELIMITER_END, <<"model_end">>).

%%====================================================================
%% OpCodes for types in JSON objects
%%====================================================================

-define(JSON_TYPE_ANY, 0).
-define(JSON_TYPE_INT, 1).
-define(JSON_TYPE_FLOAT, 2).
-define(JSON_TYPE_ATOM, 3).
-define(JSON_TYPE_LIST, 4).
-define(JSON_TYPE_TUPLE, 5).
-define(JSON_TYPE_PID, 6).
-define(JSON_TYPE_REF, 7).

%%====================================================================
%% OpCodes for the commands to the solver
%%====================================================================

-define(JSON_CMD_LOAD_TRACE_FILE, 1).
-define(JSON_CMD_SOLVE, 2).
-define(JSON_CMD_GET_MODEL, 3).
-define(JSON_CMD_ADD_AXIOMS, 4).
-define(JSON_CMD_FIX_VARIABLE, 5).
-define(JSON_CMD_RESET_SOLVER, 6).
-define(JSON_CMD_STOP, 42).

%%====================================================================
%% OpCodes for constraint types
%%====================================================================

-define(CONSTRAINT_TRUE, 1).
-define(CONSTRAINT_FALSE, 2).
-define(NOT_CONSTRAINT, 3).

-define(CONSTRAINT_TRUE_REPR, 84).   %% $T
-define(CONSTRAINT_FALSE_REPR, 70).  %% $F

%%====================================================================
%% OpCodes of constraints & built-in operations
%%====================================================================

%% Empty tag ID
-define(EMPTY_TAG_ID, 0).

%% MFA's Parameters & Spec definitions.
-define(OP_PARAMS, 1).
-define(OP_SPEC, 2).
%% Constraints.
-define(OP_GUARD_TRUE, 3).
-define(OP_GUARD_FALSE, 4).
-define(OP_MATCH_EQUAL_TRUE, 5).
-define(OP_MATCH_EQUAL_FALSE, 6).
-define(OP_TUPLE_SZ, 7).
-define(OP_TUPLE_NOT_SZ, 8).
-define(OP_TUPLE_NOT_TPL, 9).
-define(OP_LIST_NON_EMPTY, 10).
-define(OP_LIST_EMPTY, 11).
-define(OP_LIST_NOT_LST, 12).
%% Information used for syncing & merging the traces of many processes.
-define(OP_SPAWN, 13).
-define(OP_SPAWNED, 14).
-define(OP_MSG_SEND, 15).
-define(OP_MSG_RECEIVE, 16).
-define(OP_MSG_CONSUME, 17).
%% Necessary operations for the evaluation of Core Erlang.
-define(OP_UNFOLD_TUPLE, 18).
-define(OP_UNFOLD_LIST, 19).
%% Bogus operation (operations interpreted as the identity function).
-define(OP_BOGUS, 48).
%% Type conversions.
-define(OP_FLOAT, 47).
-define(OP_LIST_TO_TUPLE, 52).
-define(OP_TUPLE_TO_LIST, 53).
%% Query types.
-define(OP_IS_INTEGER, 27).
-define(OP_IS_ATOM, 28).
-define(OP_IS_FLOAT, 29).
-define(OP_IS_LIST, 30).
-define(OP_IS_TUPLE, 31).
-define(OP_IS_BOOLEAN, 32).
-define(OP_IS_NUMBER, 33).
%% Arithmetic operations.
-define(OP_PLUS, 34).
-define(OP_MINUS, 35).
-define(OP_TIMES, 36).
-define(OP_RDIV, 37).
-define(OP_IDIV_NAT, 38).
-define(OP_REM_NAT, 39).
-define(OP_UNARY, 40).
%% Operations on atoms.
-define(OP_ATOM_NIL, 49).
-define(OP_ATOM_HEAD, 50).
-define(OP_ATOM_TAIL, 51).
%% Operations on lists.
-define(OP_HD, 25).
-define(OP_TL, 26).
-define(OP_CONS, 56).
%% Operations on tuples.
-define(OP_TCONS, 57).
%% Comparisons.
-define(OP_EQUAL, 41).
-define(OP_UNEQUAL, 42).
-define(OP_LT_INT, 54).
-define(OP_LT_FLOAT, 55).

%% Maps MFAs to their JSON Opcodes
-define(OPCODE_MAPPING,
  dict:from_list([ %% Simulated built-in operations
                   { {cuter_erlang, atom_to_list_bogus, 1}, ?OP_BOGUS         }
                 , { {cuter_erlang, is_atom_nil,        1}, ?OP_ATOM_NIL      }
                 , { {cuter_erlang, safe_atom_head,     1}, ?OP_ATOM_HEAD     }
                 , { {cuter_erlang, safe_atom_tail,     1}, ?OP_ATOM_TAIL     }
                 , { {cuter_erlang, safe_pos_div,       2}, ?OP_IDIV_NAT      }
                 , { {cuter_erlang, safe_pos_rem,       2}, ?OP_REM_NAT       }
                 , { {cuter_erlang, lt_int,             2}, ?OP_LT_INT        }
                 , { {cuter_erlang, lt_float,           2}, ?OP_LT_FLOAT      }
                 , { {cuter_erlang, safe_plus,          2}, ?OP_PLUS          }
                 , { {cuter_erlang, safe_minus,         2}, ?OP_MINUS         }
                 , { {cuter_erlang, safe_times,         2}, ?OP_TIMES         }
                 , { {cuter_erlang, safe_rdiv,          2}, ?OP_RDIV          }
                 , { {cuter_erlang, safe_float,         1}, ?OP_FLOAT         }
                 , { {cuter_erlang, safe_list_to_tuple, 1}, ?OP_LIST_TO_TUPLE }
                 , { {cuter_erlang, safe_tuple_to_list, 1}, ?OP_TUPLE_TO_LIST }
                 , { {bogus_erlang, cons,               2}, ?OP_CONS          }
                   %% Actual erlang BIFs
                 , { {erlang, hd,            1}, ?OP_HD            }
                 , { {erlang, tl,            1}, ?OP_TL            }
                 , { {erlang, is_integer,    1}, ?OP_IS_INTEGER    }
                 , { {erlang, is_atom,       1}, ?OP_IS_ATOM       }
                 , { {erlang, is_boolean,    1}, ?OP_IS_BOOLEAN    }
                 , { {erlang, is_float,      1}, ?OP_IS_FLOAT      }
                 , { {erlang, is_list,       1}, ?OP_IS_LIST       }
                 , { {erlang, is_tuple,      1}, ?OP_IS_TUPLE      }
                 , { {erlang, is_number,     1}, ?OP_IS_NUMBER     }
                 , { {erlang, '-',           1}, ?OP_UNARY         }
                 , { {erlang, '=:=',         2}, ?OP_EQUAL         }
                 , { {erlang, '=/=',         2}, ?OP_UNEQUAL       }
                 ])).

%% All the MFAs that are supported for symbolic evaluation.
-define(SUPPORTED_MFAS, gb_sets:from_list(dict:fetch_keys(?OPCODE_MAPPING))).

-define(UNSUPPORTED_MFAS,
  gb_sets:from_list([ {cuter_erlang, unsupported_lt, 2} ])).

%% The set of all the built-in operations that the solver can try to reverse.
-define (REVERSIBLE_OPERATIONS,
  gb_sets:from_list([ ?OP_HD, ?OP_TL
                    ])).