gillian » Gillian » Gil_syntax » Expr

Module Gil_syntax.Expr

type t =

1. | Lit of 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 UnOp.t * t
   (*

   Unary operators (UnOp.t)

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

   Binary operators (BinOp.t)

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

   Sublist

   *)
8. | NOp of 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 * Type.t option) list * t
    (*

    Existential quantification.

    *)
12. | ForAll of (string * 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 lit : Literal.t -> t

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 false_ : t

val true_ : t

val to_literal : t -> 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_ : 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 -> Type.t -> t

val is_concrete_zero_i : t -> bool

module Infix : sig ... end

Floating point math

val conjunct : t list -> t

val disjunct : t list -> t

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_custom : pp:t Fmt.t -> t Fmt.t

Pretty-printer

val pp : t Fmt.t

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 push_in_negations : t -> t

push_in_negations e pushes all negations in e "downwards", recursively

val negate : t -> t

negate e negates the expression, recursively

val is_boolean_expr : t -> bool

Returns if this expression is a boolean expression, recursively.

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 : 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