lustre_types.mli

open Utils

type label = ident

type type_dec = { ty_dec_desc : type_dec_desc; ty_dec_loc : Location.t }

and type_dec_desc =
  | Tydec_any
  | Tydec_int
  | Tydec_real
  (* | Tydec_float *)
  | Tydec_bool
  | Tydec_clock of type_dec_desc
  | Tydec_const of ident
  | Tydec_enum of ident list
  | Tydec_struct of (ident * type_dec_desc) list
  | Tydec_array of Dimension.t * type_dec_desc

type typedec_desc = { tydec_id : ident }

type typedef_desc = { tydef_id : ident; tydef_desc : type_dec_desc }

type clock_dec = { ck_dec_desc : clock_dec_desc; ck_dec_loc : Location.t }

and clock_dec_desc = Ckdec_any | Ckdec_bool of (ident * ident) list

type constant =
  | Const_int of int
  | Const_real of Real.t
  | Const_array of constant list
  | Const_tag of label
  | Const_string of string
  (* used only for annotations *)
  | Const_modeid of string
  (* used only for annotations *)
  | Const_struct of (label * constant) list

type quantifier_type = Exists | Forall

type var_decl = {
  var_id : ident;
  var_orig : bool;
  var_dec_type : type_dec;
  var_dec_clock : clock_dec;
  var_dec_const : bool;
  var_dec_value : expr option;
  mutable var_parent_nodeid : ident option;
  mutable var_type : Types.t;
  mutable var_clock : Clocks.t;
  var_loc : Location.t;
  var_is_contract: bool;
}
(* The tag of an expression is a unique identifier used to distinguish different
   instances of the same node *)

(** The core language and its ast. Every element of the ast contains its
    location in the program text. The type and clock of an ast element is
    mutable (and initialized to dummy values). This avoids to have to duplicate
    ast structures (e.g. ast, typed_ast, clocked_ast). *)

and expr = {
  expr_tag : tag;
  expr_desc : expr_desc;
  mutable expr_type : Types.t;
  mutable expr_clock : Clocks.t;
  mutable expr_delay : Delay.t;
  mutable expr_annot : expr_annot option;
  expr_loc : Location.t;
}

and expr_desc =
  | Expr_const of constant
  | Expr_ident of ident
  | Expr_tuple of expr list
  | Expr_ite of expr * expr * expr
  | Expr_arrow of expr * expr
  | Expr_fby of expr * expr
  | Expr_array of expr list
  | Expr_access of expr * Dimension.t
  | Expr_power of expr * Dimension.t
  | Expr_pre of expr
  | Expr_when of expr * ident * label
  | Expr_merge of ident * (label * expr) list
  | Expr_appl of call_t

and call_t = ident * expr * expr option
(* The third part denotes the boolean condition for resetting *)

and eq = { eq_lhs : ident list; eq_rhs : expr; eq_loc : Location.t }

(* The tag of an expression is a unique identifier used to distinguish different
   instances of the same node *)
and eexpr = {
  eexpr_tag : tag;
  eexpr_qfexpr : expr;
  eexpr_quantifiers : (quantifier_type * var_decl list) list;
  eexpr_name : string option;
  mutable eexpr_type : Types.t;
  mutable eexpr_clock : Clocks.t;
  (* mutable eexpr_normalized: (var_decl * eq list * var_decl list) option; *)
  eexpr_loc : Location.t;
}

and expr_annot = { annots : (string list * eexpr) list; annot_loc : Location.t }

type contract_mode = {
  mode_id : ident;
  require : eexpr list;
  ensure : eexpr list;
  mode_loc : Location.t;
}

type contract_import = {
  import_nodeid : ident;
  inputs : expr;
  outputs : expr;
  import_loc : Location.t;
}

type offset = Index of Dimension.t | Field of label

type assert_t = { assert_expr : expr; assert_loc : Location.t }

type statement = Eq of eq | Aut of automata_desc

and automata_desc = {
  aut_id : ident;
  aut_handlers : handler_desc list;
  aut_loc : Location.t;
}

and handler_desc = {
  hand_state : ident;
  hand_unless : (Location.t * expr * bool * ident) list;
  hand_until : (Location.t * expr * bool * ident) list;
  hand_locals : var_decl list;
  hand_stmts : statement list;
  hand_asserts : assert_t list;
  hand_annots : expr_annot list;
  hand_loc : Location.t;
}

type proof_annotation = Kinduction of int

type contract_desc = {
  consts : var_decl list;
  locals : var_decl list;
  stmts : statement list;
  assume : eexpr list;
  guarantees : eexpr list;
  modes : contract_mode list;
  imports : contract_import list;
  spec_loc : Location.t;
  proof : proof_annotation option
}

type 'a node_spec_t = Contract of 'a | NodeSpec of ident

type node_desc = {
  node_id : ident;
  mutable node_type : Types.t;
  mutable node_clock : Clocks.t;
  node_inputs : var_decl list;
  node_outputs : var_decl list;
  node_locals : var_decl list;
  mutable node_gencalls : expr list;
  mutable node_checks : Dimension.t list;
  node_asserts : assert_t list;
  node_stmts : statement list;
  mutable node_dec_stateless : bool;
  mutable node_stateless : bool option;
  node_spec : contract_desc node_spec_t option;
  node_annot : expr_annot list;
  node_iscontract : bool;
}

type imported_node_desc = {
  nodei_id : ident;
  mutable nodei_type : Types.t;
  mutable nodei_clock : Clocks.t;
  nodei_inputs : var_decl list;
  nodei_outputs : var_decl list;
  nodei_stateless : bool;
  nodei_spec : contract_desc node_spec_t option;
  (* nodei_annot: expr_annot list; *)
  nodei_prototype : string option;
  nodei_in_lib : string list;
  nodei_iscontract : bool;
}

type const_desc = {
  const_id : ident;
  const_loc : Location.t;
  const_value : constant;
  mutable const_type : Types.t;
}

type top_decl_desc =
  | Node of node_desc
  | Const of const_desc
  | ImportedNode of imported_node_desc
  | Open of bool * string
  (* the boolean set to true denotes a local lusi vs a lusi installed at system
     level *)
  | Include of string
  (* the boolean set to true denotes a local lus vs a lus installed at system
     level *)
  | TypeDef of typedef_desc

type top_decl = {
  top_decl_desc : top_decl_desc;
  (* description of the symbol *)
  top_decl_owner : Location.filename;
  (* the module where it is defined *)
  top_decl_itf : bool;
  (* header or source file ? *)
  top_decl_loc : Location.t;
}

type program_t = top_decl list

type dep_t = {
  local : bool;
  name : ident;
  content : program_t;
  is_stateful : bool;
}

type spec_types =
  | LocalContract of contract_desc
  | TopContract of top_decl list

val tag_true : label

val tag_false : label

val node_as_contract: node_desc -> contract_desc