Module Gil_syntax.Expr

GIL Expressions

type t =
  1. | Lit of Gillian.Gil_syntax.Literal.t
    (*

    GIL literals

    *)
  2. | PVar of string
    (*

    GIL program variables

    *)
  3. | LVar of string
    (*

    GIL logical variables (interpreted symbols)

    *)
  4. | ALoc of string
    (*

    GIL abstract locations (uninterpreted symbols)

    *)
  5. | UnOp of Gillian.Gil_syntax.UnOp.t * t
    (*

    Unary operators (UnOp.t)

    *)
  6. | BinOp of t * Gillian.Gil_syntax.BinOp.t * t
    (*

    Binary operators (BinOp.t)

    *)
  7. | LstSub of t * t * t
    (*

    Sublist

    *)
  8. | NOp of Gillian.Gil_syntax.NOp.t * t list
    (*

    n-ary operators (NOp.t)

    *)
  9. | EList of t list
    (*

    Lists of expressions

    *)
  10. | ESet of t list
    (*

    Sets of expressions

    *)
  11. | Exists of (string * Gillian.Gil_syntax.Type.t option) list * t
    (*

    Existential quantification. This is now a circus because the separation between Formula and Expr doesn't make sense anymore.

    *)
  12. | EForall of (string * Gillian.Gil_syntax.Type.t option) list * t
val to_yojson : t -> Yojson.Safe.t
val of_yojson : Yojson.Safe.t -> t Ppx_deriving_yojson_runtime.error_or

Helpers for building expressions

Operations will be optimised away if possible, e.g. type_ (EList x) will give Lit (Type ListType) directly instead of using UnOp.t.TypeOf

val num : float -> t
val num_int : int -> t
val int : int -> t
val int_z : Z.t -> t
val string : string -> t
val bool : bool -> t
val to_literal : t -> Gillian.Gil_syntax.Literal.t option
val zero_i : t

Lit (Int Z.zero)

val one_i : t

Lit (Int Z.one)

val int_to_num : t -> t
val num_to_int : t -> t
val type_ : Gillian.Gil_syntax.Type.t -> t
val list : t list -> t
val list_length : t -> t
val list_nth : t -> int -> t
val list_nth_e : t -> t -> t
val list_sub : lst:t -> start:t -> size:t -> t
val list_repeat : t -> t -> t
val list_cons : t -> t -> t
val list_cat : t -> t -> t
val typeof : t -> t
val fmod : t -> t -> t
val imod : t -> t -> t
val type_eq : t -> Gillian.Gil_syntax.Type.t -> t
val is_concrete_zero_i : t -> bool
module Infix : sig ... end

Floating point math

module Set : Stdlib.Set.S with type elt := t

Sets of expressions

module Map : Utils.Prelude.Map.S with type key := t

Maps with expressions as keys

val equal : t -> t -> bool

Equality (derived)

val compare : t -> t -> int

Comparison (derived)

val map_opt : (t -> t option * bool) -> (t -> t) option -> t -> t option

Optional mapper

val pp : t Fmt.t

Pretty-printer

val full_pp : t Fmt.t

Pretty-printer with constructors (will not parse)

val to_list : t -> t list option

If the expression is a list (either an EList _ of Lit (LList _)), returns the list of expressions.

val from_list : t list -> t

from_list EList with the provided elements

val lvars : t -> Utils.Prelude.SS.t

lvars e returns all logical variables in e

val pvars : t -> Utils.Prelude.SS.t

pvars e returns all program variables in e

val alocs : t -> Utils.Prelude.SS.t

alocs e returns all abstract locations in e

val clocs : t -> Utils.Prelude.SS.t

clocs e returns all concrete locations in e

val locs : t -> Utils.Prelude.SS.t

locs e returns all concrete and abstract locations in e

val vars : t -> Utils.Prelude.SS.t

vars e returns all variables in e (includes lvars, pvars, alocs and clocs)

val substitutables : t -> Utils.Prelude.SS.t

substitutables e returns all lvars and alocs

val is_concrete : t -> bool

is_concrete e returns true iff the expression contains no lvar or aloc

val all_literals : t list -> bool

all_literals lst returns true iff all elements of the given list lst are literals

val from_lit_list : Gillian.Gil_syntax.Literal.t -> t

from_lit_list lst lifts a literal list to an expression list

val lists : t -> t list

lists e all sub-expressions of e of the form Lit (LList lst) and EList lst

val subst_clocs : (string -> t) -> t -> t

subst_clocs subst e substitutes expressions of the form Lit (Loc l) with subst l in e

val from_var_name : string -> t

from_var_name var returns either an aloc, an lvar or a pvar if var name matches one of these types (see Utils.Names.is_aloc_name, Utils.Names.is_lvar_name and Utils.Names.is_pvar_name)

val loc_from_loc_name : string -> t

loc_from_loc_name loc Has the same behaviour as from_var_name except that it returns either an ALoc loc or a Lit (Loc loc)

val subst_expr_for_expr : to_subst:t -> subst_with:t -> t -> t

subst_expr_for_expr ~to_subst ~subst_with expr substitutes every occurence of the expression to_subst with the expression subst_with in expr

val base_elements : t -> t list

base_elements e returns the list containing all logical variables, abstract locations, and non-list literals in e

val var_to_expr : string -> t

var_to_expr x returns the expression representing the program/logical variable or abstract location x

val is_matchable : t -> bool

is_matchable x returns whether or not the expression e is matchable