Commit 84f8ec82 authored by Kim Nguyễn's avatar Kim Nguyễn
Browse files

Document types/normal.mli

parent a328d18b
Pipeline #138 passed with stages
in 6 minutes and 46 seconds
(** This module implements the normalisation of Cartesian products of sets.
Given an DNF (union of intersection of positive and negative products),
this module contains functions that return:
- a union of products (that is, the intersections are pushed below the
- a union of product in normal form, that is a list of {i(t{_ i}}, s{_ i})}
products where the {i t{_ i}} are pair-wise disjoint and neither the
{i t{_ i}} nor the {i s{_ i}} are empty.
(** This signature represent abstract sets *)
module type S =
(** The type of a set *)
type t
(** The universal set *)
val any: t
(** The empty set *)
val empty: t
(** Boolean connectives *)
val cup: t -> t -> t
val cap: t -> t -> t
val diff: t -> t -> t
(** Test for emptiness*)
val is_empty: t -> bool
(** An DNF given as a List of pairs of list:
[ [ (p1, n1); (p2, n2); ... ] ] where the [pi] are lists of positive
atoms and the [ni] are lists of negative atoms.
type 'a bool = ('a list * 'a list) list
module Make(X1 : S)(X2 : S) :
(** The functor implementing the normalisation of products *)
module Make(X1 : S) (X2 : S) :
(** The type of a simplified DNF : a list of products *)
type t = (X1.t * X2.t) list
(** Returns the normal form a of simplified form:
[normal l] returns a list [ (t1, s1); (t2, s2); ... ] ] where :
- the [ti] are pair-wise disjoint
- the [(ti,si)] are non empty products.
The empty product is returned as [ [] ].
val normal: t -> t
(* normalized form:
(t1,t2),...,(s1,s2) ==> t1 & s1 = 0
(t1,t2) => t1 <> 0, t2 <> 0
(** [boolean_normal l] returns the normal form from a DNF representation *)
val boolean_normal: (X1.t * X2.t) bool -> t
(* return a normalized form *)
(** [boolean l] returns a simplified form from the DNF representation *)
val boolean: (X1.t * X2.t) bool -> t
(** [pi1 l] returns the union of all first components of [l] *)
val pi1: t -> X1.t
(** [pi2 l] returns the union of all second components of [l] *)
val pi2: t -> X2.t
(** [pi2 restr l] returns the union of all second components for
which the first component intersects [restr] *)
val pi2_restricted: X1.t -> t -> X2.t
Markdown is supported
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment