gillian » Gillian » Gil_syntax » Pred

Module Gil_syntax.Pred

type t = {

1. pred_name : string;
   (*

   Name of the predicate

   *)
2. pred_source_path : string option;
3. pred_loc : Utils.Location.t option;
4. pred_internal : bool;
5. pred_num_params : int;
   (*

   Number of parameters

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

   Parameter names and (optional) types

   *)
7. pred_ins : int list;
   (*

   Ins

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

   Predicate definitions

   *)
9. pred_facts : Expr.t list;
   (*

   Facts that hold for every definition

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

    Cost for unfolding the predicate

    *)
11. pred_pure : bool;
    (*

    Is the predicate pure?

    *)
12. pred_abstract : bool;
    (*

    Is the predicate abstract?

    *)
13. pred_nounfold : bool;
    (*

    Should the predicate be unfolded?

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

val ins_and_outs : t -> Utils.Containers.SI.t * Utils.Containers.SI.t

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, string) Stdlib.result

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.atom

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.