open Lexing

type position = Lexing.position
let position_unknown = Lexing.dummy_pos

type extent = position * position
let extent_unknown = (position_unknown, position_unknown)

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
    (* 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)
    (* 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

type var_def = bool * (id ext) * typ

type automaton = id * state ext list * id list
and  state = {
    initial : bool;
    name    : id;
    locals  : var_def list;
    body    : eqn ext list;
    until   : transition list;
}
and transition = (expr ext) * (id ext)

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

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

type const_decl = {
    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