aboutsummaryrefslogtreecommitdiffstats
path: root/lib/constraint.mli
diff options
context:
space:
mode:
Diffstat (limited to '')
-rw-r--r--lib/constraint.mli91
1 files changed, 0 insertions, 91 deletions
diff --git a/lib/constraint.mli b/lib/constraint.mli
deleted file mode 100644
index c86ef89..0000000
--- a/lib/constraint.mli
+++ /dev/null
@@ -1,91 +0,0 @@
-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