open Identifiers
open Types
open Values
open Expressions

module FunDefId = IdGen ()

type assumed_fun_id = BoxNew | BoxDeref | BoxDerefMut | BoxFree

type fun_id = Local of FunDefId.id | Assumed of assumed_fun_id

type assertion = { cond : operand; expected : bool }

type fun_sig = {
  region_params : region_var RegionVarId.vector;
  num_early_bound_regions : int;
  type_params : type_var TypeVarId.vector;
  inputs : rty VarId.vector;
  output : rty;
}

type call = {
  func : fun_id;
  region_params : erased_region list;
  type_params : ety list;
  args : operand list;
  dest : place;
}

type statement =
  | Assign of place * rvalue
  | FakeRead of place
  | SetDiscriminant of place * VariantId.id
  | Drop of place
  | Assert of assertion
  | Call of call
  | Panic
  | Return
  | Break of int
      (** Break to (outer) loop. The [int] identifies the loop to break to:
          * 0: break to the first outer loop (the current loop)
          * 1: break to the second outer loop
          * ...
          *)
  | Continue of int
      (** Continue to (outer) loop. The loop identifier works
          the same way as for [Break] *)
  | Nop

type expression =
  | Statement of statement
  | Sequence of expression * expression
  | Switch of operand * switch_targets
  | Loop of expression

and switch_targets =
  | If of expression * expression  (** Gives the "if" and "else" blocks *)
  | SwitchInt of integer_type * (scalar_value * expression) list * expression
      (** The targets for a switch over an integer are:
          - the list `(matched value, expression to execute)`
          - the "otherwise" expression.
          Also note that we precise the type of the integer (uint32, int64, etc.)
          which we switch on. *)

type fun_def = {
  def_id : FunDefId.id;
  name : name;
  signature : fun_sig;
  divergent : bool;
  arg_count : int;
  locals : var VarId.vector;
  body : expression;
}