open Lexing
open Util


type 'a ext = 'a * extent

type id = string

type typ =
    | AST_TINT
    | AST_TBOOL
    | AST_TREAL

type unary_op =
    | AST_UPLUS
    | AST_UMINUS

type binary_op =
    (* num * num -> num *)
    | AST_PLUS
    | AST_MINUS
    | AST_MUL
    | AST_DIV
    | AST_MOD

type binary_rel_op =
    (* 'a * 'a -> bool *)
    | AST_EQ
    | AST_NE
    (* num * num -> bool *)
    | AST_LT
    | AST_LE
    | AST_GT
    | AST_GE

type bin_bool_op =
    (* bool * bool -> bool *)
    | AST_AND
    | AST_OR

type expr =
    | AST_identifier  of id ext
    | AST_idconst     of id ext
    (* on numerical values *)
    | AST_int_const   of string ext
    | AST_real_const  of string ext
    | AST_unary       of unary_op * (expr ext)
    | AST_binary      of binary_op * (expr ext) * (expr ext)
    | AST_cast        of (expr ext) * typ
    (* on boolean values *)
    | AST_bool_const  of bool
    | AST_binary_rel  of binary_rel_op * (expr ext) * (expr ext)
    | AST_binary_bool of bin_bool_op * (expr ext) * (expr ext)
    | AST_not         of expr ext
    (* temporal primitives *)
    | AST_pre         of expr ext * id
    | AST_arrow       of (expr ext) * (expr ext)
    (* other *)
    | AST_if          of (expr ext) * (expr ext) * (expr ext)
    | AST_instance    of (id ext) * (expr ext list) * id
    | AST_tuple       of expr ext list

type var_def = bool * id * typ

type automaton = id * state ext list * id list
and  state = {
    initial   : bool;
    st_name   : id;
    st_locals : var_def list;
    body      : eqn ext list;
    until     : transition list;
    (* these two rst info are determined after parsing, in typing.ml when
        the variable list is extracted *)
    mutable i_rst : bool;       (* resettable by S -> S transition *)
    mutable o_rst : bool;       (* resettable by S' -> S transition *)
}
and transition = (expr ext) * (id ext) * bool   (* bool : does it reset ? *)

and activate_block = {
    act_id     : id;
    act_locals : var_def list;
    body       : eqn ext list;
}
and activate_if =
    | AST_activate_body of activate_block
    | AST_activate_if of expr ext * activate_if * activate_if
and activate = activate_if * id list

and eqn =
    | AST_assign     of (id ext list) * (expr ext)
    | AST_assume     of (id ext) * (expr ext)
    | AST_guarantee  of (id ext) * (expr ext)
    | AST_automaton  of automaton
    | AST_activate   of activate

type node_decl = {
    n_name : id;
    args   : var_def list;
    ret    : var_def list;
    var    : var_def list;
    body   : eqn ext list;
}

type const_decl = {
    c_name : id;
    typ    : typ;
    value  : expr ext;
}

type toplevel =
    | AST_node_decl  of node_decl ext
    | AST_const_decl of const_decl ext

type prog = toplevel list