Source file Option.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
(******************************************************************************)
(*                                                                            *)
(*                                    Fix                                     *)
(*                                                                            *)
(*                       François Pottier, Inria Paris                        *)
(*                                                                            *)
(*  Copyright Inria. All rights reserved. This file is distributed under the  *)
(*  terms of the GNU Library General Public License version 2, with a         *)
(*  special exception on linking, as described in the file LICENSE.           *)
(*                                                                            *)
(******************************************************************************)

(* Although the code is polymorphic in the type of elements, it must still
   be packaged as a functor, because [property] cannot be a parameterized
   type. *)

module Option (X : sig type t end) = struct

  open X

  type property =
    t option

  let bottom =
    None

  let equal (o1 : property) (o2 : property) =
    (* It is permitted to assume that [o1 <= o2] holds. This implies that
       when [o1] is [Some x1] and [o2] is [Some x2] we may return [true]
       without actually comparing [x1] and [x2]. *)
    match o1, o2 with
    | Some _, None ->
        (* Because [o1 <= o2] holds, this cannot happen. *)
        let msg = Printf.sprintf "\n  Fix.Prop.Option says: \
          please check that your \"rhs\" function is \
          monotone.\n  %s\n" __LOC__ in
        raise (Invalid_argument msg)
    | None, Some _ ->
        false
    | None, None
    | Some _, Some _ ->
        true

  let is_maximal o =
    match o with
    | None ->
        false
    | Some _ ->
        true

end