Module Gil_syntax.Pred

GIL Predicates

type t = {
  1. pred_name : string;
    (*

    Name of the predicate

    *)
  2. pred_source_path : string option;
  3. pred_internal : bool;
  4. pred_num_params : int;
    (*

    Number of parameters

    *)
  5. pred_params : (string * Type.t option) list;
    (*

    Parameter names and (optional) types

    *)
  6. pred_ins : int list;
    (*

    Ins

    *)
  7. pred_definitions : ((string * string list) option * Asrt.t) list;
    (*

    Predicate definitions

    *)
  8. pred_facts : Formula.t list;
    (*

    Facts that hold for every definition

    *)
  9. pred_guard : Asrt.t option;
    (*

    Cost for unfolding the predicate

    *)
  10. pred_pure : bool;
    (*

    Is the predicate pure?

    *)
  11. pred_abstract : bool;
    (*

    Is the predicate abstract?

    *)
  12. pred_nounfold : bool;
    (*

    Should the predicate be unfolded?

    *)
  13. pred_normalised : bool;
    (*

    Has the predicate been previously normalised?

    *)
}
val init : t list -> (string, t) Utils.Prelude.Hashtbl.t

Populates a Hashtbl from the given predicate list

Returns the sets of in- and out-parameters of a predicate

val in_params : t -> string list

Returns the names of in-parameters

val in_args : t -> 'a list -> 'a list

Returns the in-parameters given all parameters

val out_params : t -> string list

Returns the names of in-parameters

val out_args : t -> 'a list -> 'a list

Returns the out-parameters given all parameters

val pp : Stdlib.Format.formatter -> t -> unit

Pretty-printer

val check_pvars : (string, t) Utils.Prelude.Hashtbl.t -> unit

Sanity check on program variables inside normalised predicates

val explicit_param_types : (string, t) Utils.Prelude.Hashtbl.t -> t -> t

Infers parameter types and makes them explicit in the assertions

val combine_ins_outs : t -> 'a list -> 'a list -> 'a list

Combines a list of ins and a list of outs putting them in the right order according to a given predicate.

val iter_ins_outs : t -> ('a -> unit) -> ('b -> unit) -> ('a list * 'b list) -> unit

iter_ins_outs p f_ins f_outs (ins, outs) will iterate, applying f_ins on the ins and f_outs on the outs, in the order specified

val pp_ins_outs : t -> (Stdlib.Format.formatter -> 'a -> unit) -> (Stdlib.Format.formatter -> 'b -> unit) -> Stdlib.Format.formatter -> ('a list * 'b list) -> unit

Prints the ins and outs in the right order

val get : (string, t) Utils.Prelude.Hashtbl.t -> string -> t

Retrieves a predicate definition by name

val close_token_name : t -> string

Given a guarded predicate, return the name of its close token. Fails if the predicate isn't guarded.

val close_token_call : t -> Asrt.t

Given a guarded predicate, return a "call" to its close token. The arguments given are PVars with the same name as the ins of the predicate.

val pred_name_from_close_token_name : string -> string option

Given a name, if it's a close_token name, returns the name of the corresponding predicate, otherwise return None.