blob: c86ef89c6f6a7f15e931f4eec15476116afdd2e8 (
plain) (
tree)
|
|
type relation_name = string
type attr_name = string
type binding_expr = Var of attr_name | Const of Conventions.AbstractValue.t
module BindingMap : Map.S with type key = String.t
type binding = binding_expr BindingMap.t
type t =
| MemberOf of { target : relation_name; binding : binding }
| Not of { body : t; universe : relation_name }
| And of t list
| Or of t list
| Exists of { variable : attr_name; quantifier : relation_name; body : t }
| Forall of { variable : attr_name; quantifier : relation_name; body : t }
type diagnostic =
| MembershipFailed of {
target : string;
bound_values : (attr_name * Conventions.AbstractValue.t) list;
}
| RelationNotFound of string
| UnboundedQuantifier of { variable : attr_name; quantifier : relation_name }
| ConstraintFailures of (string * diagnostic) list
val vars_in : t -> attr_name list
val rename_vars : (attr_name * attr_name) list -> t -> t
val filter_by_attrs : attr_name list -> t -> t option
val merge : (string * t) list -> (string * t) list -> (string * t) list
val member_of : target:relation_name -> binding:binding -> t
val not_ : universe:relation_name -> t -> t
val and_ : t list -> t
val or_ : t list -> t
val exists : variable:attr_name -> quantifier:relation_name -> t -> t
val forall : variable:attr_name -> quantifier:relation_name -> t -> t
type eval_context = {
check_membership :
relation_name -> (attr_name * Conventions.AbstractValue.t) list -> bool;
iterate_finite :
relation_name -> (attr_name * Conventions.AbstractValue.t) list list option;
}
val bind :
binding ->
Tuple.materialized ->
(attr_name * Conventions.AbstractValue.t) list
val evaluate :
eval_context -> Tuple.materialized -> t -> (bool, diagnostic) result
val evaluate_named :
eval_context ->
Tuple.materialized ->
(string * t) list ->
(bool, diagnostic) result
val evaluate_first_failure :
eval_context ->
Tuple.materialized ->
(string * t) list ->
(bool, diagnostic) result
type polarity = Positive | Negative | Both
type polarity_index
val polarity_of : ?neg:bool -> t -> polarity_index
val polarity_find : relation_name -> polarity_index -> polarity option
type timing = Immediate | Deferred
val focused_filter :
t ->
relation_name ->
(attr_name * Conventions.AbstractValue.t) list ->
(attr_name * Conventions.AbstractValue.t) list
val trigger_constants :
t -> relation_name -> (attr_name * Conventions.AbstractValue.t) list
val substitute_transition :
t -> relation_name -> (attr_name * Conventions.AbstractValue.t) list -> t
val make_comparison_binding : left:binding_expr -> right:binding_expr -> binding
val lt : left:binding_expr -> right:binding_expr -> t
val lte : left:binding_expr -> right:binding_expr -> t
val gt : left:binding_expr -> right:binding_expr -> t
val gte : left:binding_expr -> right:binding_expr -> t
val eq : left:binding_expr -> right:binding_expr -> t
val neq : left:binding_expr -> right:binding_expr -> t
val between : value:binding_expr -> low:binding_expr -> high:binding_expr -> t
|
