package idd

  1. Overview
  2. Docs

Source file algebra.ml

1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42

(** Boolean algebra  *)
module type BA = sig
  type t
  val ctrue : t
  val cfalse : t
  val conj : t -> t -> t
  val disj : t -> t -> t
  val neg : t -> t -> t
end

(** Kleene algebra  *)
module type KA = sig
  type t
  val zero : t
  val one : t
  val seq : t -> t -> t
  val union : t -> t -> t
  val star : t -> t
end

(** Kleene algebra with tests  *)
module type KAT = sig
  type b
  type t
  val test : b -> t
  include BA with type t := b
  include KA with type t := t
end

(** Guarded Kleene algebra with tests *)
module type GKAT = sig
  type b
  type t
  val test : b -> t
  include BA with type t := b
  val zero : t
  val one : t
  val seq : t -> t -> t
  val ite : b -> t -> t
  val whl : b -> t
end