(** The "symbolic" AST is the AST directly generated by the symbolic execution.
    It is very rough and meant to be extremely straightforward to build during
    the symbolic execution: we later apply transformations to generate the
    pure AST that we export. *)

open Identifiers
module T = Types
module V = Values
module E = Expressions
module A = CfimAst

type call_id =
  | Fun of A.fun_id * V.FunCallId.id
      (** A "regular" function (i.e., a function which is not a primitive operation) *)
  | Unop of E.unop
  | Binop of E.binop
[@@deriving show, ord]

type call = {
  call_id : call_id;
  type_params : T.ety list;
  args : V.typed_value list;
  dest : V.symbolic_value;
}

(** **Rk.:** here, [expression] is not at all equivalent to the expressions
    used in CFIM: they are a first step towards lambda-calculus expressions.
 *)
type expression =
  | Return of V.typed_value
      (** The typed value stored in [Return] is the value contained in the return
          variable upon returning
       *)
  | Panic
  | FunCall of call * expression
  | EndAbstraction of V.abs * expression
  | Expansion of V.symbolic_value * expansion
  | Meta of meta * expression  (** Meta information *)

and expansion =
  | ExpandNoBranch of V.symbolic_expansion * expression
      (** A symbolic expansion which doesn't generate a branching.
          Includes:
          - concrete expansion
          - borrow expansion
          *Doesn't* include:
          - expansion of ADTs with one variant
       *)
  | ExpandAdt of
      (T.VariantId.id option * V.symbolic_value list * expression) list
      (** ADT expansion *)
  | ExpandBool of expression * expression
      (** A boolean expansion (i.e, an `if ... then ... else ...`) *)
  | ExpandInt of
      T.integer_type * (V.scalar_value * expression) list * expression
      (** An integer expansion (i.e, a switch over an integer). The last
          expression is for the "otherwise" branch. *)

(** Meta information, not necessary for synthesis but useful to guide it to
    generate a pretty output.
 *)

and meta = Aggregate of V.typed_value  (** We generated an aggregate value *)