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

module T = Types
module V = Values
module E = Expressions
module A = LlbcAst

(** "Meta"-place: a place stored as meta-data.

    Whenever we need to introduce new symbolic variables, for instance because
    of symbolic expansions, we try to store a "place", which gives information
    about the origin of the values (this place information comes from assignment
    information, etc.).
    We later use this place information to generate meaningful name, to prettify
    the generated code.
 *)
type mplace = {
  bv : Contexts.var_binder;
      (** It is important that we store the binder, and not just the variable id,
          because the most important information in a place is the name of the
          variable!
       *)
  projection : E.projection;
      (** We store the projection because we can, but it is actually not that useful *)
}
[@@deriving show]

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;
  ctx : Contexts.eval_ctx;
      (** The context upon calling the function (after the operands have been
          evaluated). We need it to compute the translated values for shared
          borrows (we need to perform lookups).
       *)
  abstractions : V.AbstractionId.id list;
  type_params : T.ety list;
  args : V.typed_value list;
  args_places : mplace option list;  (** Meta information *)
  dest : V.symbolic_value;
  dest_place : mplace option;  (** Meta information *)
}
[@@deriving show]

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

type meta =
  | Assignment of Contexts.eval_ctx * mplace * V.typed_value * mplace option
      (** We generated an assignment (destination, assigned value, src) *)
[@@deriving show]

(** **Rk.:** here, {!expression} is not at all equivalent to the expressions
    used in LLBC: they are a first step towards lambda-calculus expressions.
 *)
type expression =
  | Return of Contexts.eval_ctx * V.typed_value option
      (** There are two cases:
          - the AST is for a forward function: the typed value should contain
            the value which was in the return variable
          - the AST is for a backward function: the typed value should be [None]

          The context is the evaluation context upon reaching the return, We
          need it to translate shared borrows to pure values (we need to be able
          to look up the shared values in the context).
       *)
  | Panic
  | FunCall of call * expression
  | EndAbstraction of Contexts.eval_ctx * V.abs * expression
      (** The context is the evaluation context upon ending the abstraction,
          just after we removed the abstraction from the context.

          The context is the evaluation context from after evaluating the asserted
          value. It has the same purpose as for the {!Return} case.
       *)
  | EvalGlobal of A.GlobalDeclId.id * V.symbolic_value * expression
      (** Evaluate a global to a fresh symbolic value *)
  | Assertion of Contexts.eval_ctx * V.typed_value * expression
      (** An assertion.

          The context is the evaluation context from after evaluating the asserted
          value. It has the same purpose as for the {!Return} case.
       *)
  | Expansion of mplace option * V.symbolic_value * expansion
      (** Expansion of a symbolic value.
    
          The place is "meta": it gives the path to the symbolic value (if available)
          which got expanded (this path is available when the symbolic expansion
          comes from a path evaluation, during an assignment for instance).
          We use it to compute meaningful names for the variables we introduce,
          to prettify the generated code.
       *)
  | ForwardEnd of
      V.typed_value list option * expression * expression T.RegionGroupId.Map.t
      (** We use this delimiter to indicate at which point we switch to the
          generation of code specific to the backward function(s). This allows
          us in particular to factor the work out: we don't need to replay the
          symbolic execution up to this point, and can reuse it for the forward
          function and all the backward functions.

          The first expression gives the end of the translation for the forward
          function, the map from region group ids to expressions gives the end
          of the translation for the backward functions.

          The optional list of input values are input values for loops: upon
          entering a loop, in the translation we call the loop translation
          function, which takes care of the end of the execution.
       *)
  | Loop of loop  (** Loop *)
  | Meta of meta * expression  (** Meta information *)

and loop = {
  loop_id : V.LoopId.id;
  end_expr : expression;
      (** The end of the function (upon the moment it enters the loop) *)
  loop_expr : expression;  (** The symbolically executed loop body *)
}

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. *)
[@@deriving show]