summaryrefslogtreecommitdiff
path: root/compiler/InterpreterExpansion.mli
blob: 7140d55f4de89b34cf5f2fb9a0498c9db39449a3 (plain)
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
open Values
open Contexts
open Cps
module SA = SymbolicAst

type proj_kind = LoanProj | BorrowProj

(** Apply a symbolic expansion to a context, by replacing the original
    symbolic value with its expanded value. Is valid only if the expansion
    is *not a borrow* (i.e., an adt...).

    This function does *not* update the synthesis.
*)
val apply_symbolic_expansion_non_borrow :
  config ->
  Meta.meta ->
  symbolic_value ->
  eval_ctx ->
  symbolic_expansion ->
  eval_ctx

(** Expand a symhbolic value, without branching *)
val expand_symbolic_value_no_branching :
  config -> Meta.meta -> symbolic_value -> SA.mplace option -> cm_fun

(** Expand a symbolic enumeration (leads to branching if the enumeration has
    more than one variant).

    Parameters:
    - [config]
    - [meta]
    - [sv]
    - [sv_place]
 *)
val expand_symbolic_adt :
  config ->
  Meta.meta ->
  symbolic_value ->
  SA.mplace option ->
  eval_ctx ->
  eval_ctx list * (SymbolicAst.expression list option -> eval_result)

(** Expand a symbolic boolean.

    Parameters: see {!expand_symbolic_adt}.
 *)
val expand_symbolic_bool :
  config ->
  Meta.meta ->
  symbolic_value ->
  SA.mplace option ->
  eval_ctx ->
  (eval_ctx * eval_ctx)
  * ((SymbolicAst.expression * SymbolicAst.expression) option -> eval_result)

(** Symbolic integers are expanded upon evaluating a [SwitchInt].

    When expanding a boolean upon evaluating an [if ... then ... else ...],
    or an enumeration just before matching over it, we can simply expand the
    boolean/enumeration (generating a list of contexts from which to execute)
    then retry evaluating the [if ... then ... else ...] or the [match]: as
    the scrutinee will then have a concrete value, the interpreter will switch
    to the proper branch.

    When expanding a "regular" integer for a switch there is always an *otherwise*
    branch. We treat it separately: for this reason we return a pair of a list
    of evaluation contexts (for the branches which are not the otherwise branch)
    and an additional evaluation context for the otherwise branch.
 *)
val expand_symbolic_int :
  config ->
  Meta.meta ->
  symbolic_value ->
  SA.mplace option ->
  integer_type ->
  scalar_value list ->
  eval_ctx ->
  (eval_ctx list * eval_ctx)
  * ((SymbolicAst.expression list * SymbolicAst.expression) option ->
    eval_result)

(** If this mode is activated through the [config], greedily expand the symbolic
    values which need to be expanded. See {!type:Contexts.config} for more information.
 *)
val greedy_expand_symbolic_values : config -> Meta.meta -> cm_fun