sig
  type t
  exception Node_not_found of LustreIdent.t * Lib.position
  exception Type_not_found of LustreIdent.t * Lib.position
  exception Contract_not_found of LustreIdent.t * Lib.position
  val mk_empty_context : unit -> LustreContext.t
  val set_guard_flag : LustreContext.t -> bool -> LustreContext.t
  val reset_guard_flag : LustreContext.t -> LustreContext.t
  val guard_flag : LustreContext.t -> bool
  val set_in_automaton : LustreContext.t -> bool -> LustreContext.t
  val reset_in_automaton : LustreContext.t -> LustreContext.t
  val in_automaton : LustreContext.t -> bool
  val push_scope : LustreContext.t -> string -> LustreContext.t
  val pop_scope : LustreContext.t -> LustreContext.t
  val push_contract_scope : LustreContext.t -> string -> LustreContext.t
  val pop_contract_scope : LustreContext.t -> LustreContext.t
  val contract_scope_of : LustreContext.t -> string list
  val scope_of_context : LustreContext.t -> string list
  val create_node :
    LustreContext.t -> LustreIdent.t -> bool -> LustreContext.t
  val current_node_name : LustreContext.t -> LustreIdent.t option
  val current_node_map :
    LustreContext.t -> (LustreNode.t -> LustreNode.t) -> LustreContext.t
  val current_node_calls : LustreContext.t -> LustreNode.node_call list
  val current_node_modes :
    LustreContext.t -> LustreContract.mode list option option
  val create_function : LustreContext.t -> LustreIdent.t -> LustreContext.t
  val add_node_to_context :
    LustreContext.t -> LustreContext.t -> LustreContext.t
  val solve_fref :
    LustreContext.t ->
    LustreAst.declaration ->
    LustreDependencies.decl * LustreIdent.t * Lib.position ->
    LustreAst.declaration list -> LustreAst.declaration list
  val add_free_constant :
    LustreContext.t -> LustreIdent.t -> Var.t LustreIndex.t -> unit
  val get_free_constants :
    LustreContext.t -> (LustreIdent.t * Var.t LustreIndex.t) list
  val free_constant_expr_of_ident :
    LustreContext.t -> LustreIdent.t -> LustreExpr.t LustreIndex.t
  val add_expr_for_ident :
    ?shadow:bool ->
    LustreContext.t ->
    LustreIdent.t -> LustreExpr.t LustreIndex.t -> LustreContext.t
  val remove_expr_for_ident :
    LustreContext.t -> LustreIdent.t -> LustreContext.t
  val add_type_for_ident :
    LustreContext.t ->
    LustreIdent.t -> Type.t LustreIndex.t -> LustreContext.t
  val get_nodes : LustreContext.t -> LustreNode.t list
  val get_node : LustreContext.t -> LustreNode.t option
  val prev : LustreContext.t -> LustreContext.t
  val get_state_var_bounds :
    LustreContext.t ->
    LustreExpr.expr LustreExpr.bound_or_fixed list StateVar.StateVarHashtbl.t
  val contract_nodes : LustreContext.t -> LustreAst.contract_node_decl list
  val trace_svars_of :
    LustreContext.t -> LustreExpr.t -> StateVar.StateVarSet.t option
  val add_contract_node_decl_to_context :
    LustreContext.t ->
    Lib.position * LustreAst.contract_node_decl -> LustreContext.t
  val contract_node_decl_of_ident :
    LustreContext.t -> string -> Lib.position * LustreAst.contract_node_decl
  val fail_on_new_definition :
    LustreContext.t -> Lib.position -> string -> LustreContext.t
  val raise_no_new_definition_exc : LustreContext.t -> 'a
  val expr_of_ident :
    LustreContext.t -> LustreIdent.t -> LustreExpr.t LustreIndex.t
  val assignable_state_var_of_ident :
    LustreContext.t -> LustreIdent.t -> StateVar.t LustreIndex.t
  val type_of_ident :
    LustreContext.t -> LustreIdent.t -> Type.t LustreIndex.t
  val expr_in_context : LustreContext.t -> LustreIdent.t -> bool
  val type_in_context : LustreContext.t -> LustreIdent.t -> bool
  val node_in_context : LustreContext.t -> LustreIdent.t -> bool
  val prop_name_in_context : LustreContext.t -> string -> bool
  val mk_state_var :
    ?is_input:bool ->
    ?is_const:bool ->
    ?for_inv_gen:bool ->
    ?shadow:bool ->
    LustreContext.t ->
    Ident.t list ->
    LustreIdent.t ->
    LustreIndex.index ->
    Type.t ->
    LustreNode.state_var_source option -> StateVar.t * LustreContext.t
  val mk_fresh_local :
    ?is_input:bool ->
    ?is_const:bool ->
    ?for_inv_gen:bool ->
    ?bounds:LustreExpr.expr LustreExpr.bound_or_fixed list ->
    LustreContext.t -> Type.t -> StateVar.t * LustreContext.t
  val set_state_var_source :
    LustreContext.t ->
    StateVar.t -> LustreNode.state_var_source -> LustreContext.t
  val mk_local_for_expr :
    ?is_input:bool ->
    ?is_const:bool ->
    ?for_inv_gen:bool ->
    ?bounds:LustreExpr.expr LustreExpr.bound_or_fixed list ->
    ?is_ghost:bool ->
    ?original:LustreAst.expr ->
    Lib.position ->
    LustreContext.t ->
    LustreExpr.t -> LustreNode.equation_lhs * LustreContext.t
  val mk_fresh_oracle :
    ?is_input:bool ->
    ?is_const:bool ->
    ?for_inv_gen:bool ->
    ?bounds:LustreExpr.expr LustreExpr.bound_or_fixed list ->
    LustreContext.t -> Type.t -> StateVar.t * LustreContext.t
  val mk_fresh_oracle_for_state_var :
    ?bounds:LustreExpr.expr LustreExpr.bound_or_fixed list ->
    LustreContext.t -> StateVar.t -> StateVar.t * LustreContext.t
  val node_of_name : LustreContext.t -> LustreIdent.t -> LustreNode.t
  val call_outputs_of_node_call :
    LustreContext.t ->
    LustreIdent.t ->
    LustreNode.call_cond list ->
    StateVar.t LustreIndex.t ->
    LustreExpr.t LustreIndex.t option -> StateVar.t LustreIndex.t option
  val add_node_input :
    ?is_const:bool ->
    LustreContext.t ->
    LustreIdent.t -> Type.t LustreIndex.t -> LustreContext.t
  val add_node_output :
    ?is_single:bool ->
    LustreContext.t ->
    LustreIdent.t -> Lib.position -> Type.t LustreIndex.t -> LustreContext.t
  val outputs_of_current_node : LustreContext.t -> StateVar.t LustreIndex.t
  val add_node_local :
    ?ghost:bool ->
    LustreContext.t ->
    LustreIdent.t -> Lib.position -> Type.t LustreIndex.t -> LustreContext.t
  val add_node_ass :
    LustreContext.t -> LustreContract.svar list -> LustreContext.t
  val add_node_gua :
    LustreContext.t -> (LustreContract.svar * bool) list -> LustreContext.t
  val add_node_mode :
    LustreContext.t -> LustreContract.mode -> LustreContext.t
  val add_node_assert : LustreContext.t -> LustreExpr.t -> LustreContext.t
  val add_node_property :
    LustreContext.t ->
    Property.prop_source -> string -> LustreExpr.t -> LustreContext.t
  val add_node_equation :
    LustreContext.t ->
    Lib.position ->
    StateVar.t ->
    LustreExpr.expr LustreExpr.bound_or_fixed list ->
    int -> LustreExpr.t -> LustreContext.t
  val add_node_call :
    LustreContext.t ->
    Lib.position -> LustreNode.node_call -> LustreContext.t
  val set_node_main : LustreContext.t -> LustreContext.t
  val set_node_function : LustreContext.t -> LustreContext.t
  val get_node_function_flag : LustreContext.t -> bool
  val close_expr :
    ?bounds:LustreExpr.expr LustreExpr.bound_or_fixed list ->
    ?original:LustreAst.expr ->
    Lib.position ->
    LustreExpr.t * LustreContext.t -> LustreExpr.t * LustreContext.t
  val check_vars_defined : LustreContext.t -> unit
  val fail_at_position : Lib.position -> string -> 'a
  val warn_at_position : Lib.position -> string -> unit
  val fail_no_position : string -> 'a
  val warn_no_position : string -> unit
  val are_definitions_allowed : LustreContext.t -> bool
end