Source file `bounded_lattice.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
43
44
45
46
47
48
49
50
51
52
module Core_via_bounded_join_lattice_and_bounded_meet_lattice
    (Req : Preface_specs.Bounded_lattice
           .WITH_BOUNDED_JOIN_LATTICE_AND_BOUNDED_MEET_LATTICE) =
  Req

module Core_over_bounded_join_lattice_and_bounded_meet_lattice
    (Join_req : Preface_specs.Bounded_join_semilattice.CORE)
    (Meet_req : Preface_specs.Bounded_meet_semilattice.CORE
                  with type t = Join_req.t) =
struct
  include Join_req
  include Meet_req
end

module Infix (Core : Preface_specs.Bounded_lattice.CORE) = struct
  include Bounded_join_semilattice.Infix (Core)
  include Bounded_meet_semilattice.Infix (Core)
end

module Via
    (Core : Preface_specs.Bounded_lattice.CORE)
    (Infix : Preface_specs.Bounded_lattice.INFIX) =
struct
  include Core
  module Infix = Infix
  include Infix
end

module Via_bounded_join_lattice_and_bounded_meet_lattice
    (Req : Preface_specs.Bounded_lattice
           .WITH_BOUNDED_JOIN_LATTICE_AND_BOUNDED_MEET_LATTICE) =
struct
  module Core = Core_via_bounded_join_lattice_and_bounded_meet_lattice (Req)
  include Core
  module Infix = Infix (Core)
  include Infix
end

module Over_bounded_join_lattice_and_bounded_meet_lattice
    (Join_req : Preface_specs.Bounded_join_semilattice.CORE)
    (Meet_req : Preface_specs.Bounded_meet_semilattice.CORE
                  with type t = Join_req.t) =
struct
  module Core =
    Core_over_bounded_join_lattice_and_bounded_meet_lattice
      (Join_req)
      (Meet_req)

  include Core
  module Infix = Infix (Core)
  include Infix
end