Source file `Tag.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
(******************************************************************************)
(*                                                                            *)
(*                                  Monolith                                  *)
(*                                                                            *)
(*                              François Pottier                              *)
(*                                                                            *)
(*  Copyright Inria. All rights reserved. This file is distributed under the  *)
(*  terms of the GNU Lesser General Public License as published by the Free   *)
(*  Software Foundation, either version 3 of the License, or (at your         *)
(*  option) any later version, as described in the file LICENSE.              *)
(*                                                                            *)
(******************************************************************************)

open Eq

(* The type ['a tags] is declared as an extensible type. *)

type 'a tags = ..

(* The type ['a tag] is then declared as follows. In short, a value of type
   ['a tag] is a data constructor [Tag], together with a proof that this data
   constructor is a member of the type ['a tags]. This apparently convoluted
   declaration allows us to use [Tag] both for construction and for
   deconstruction. *)

module type TAG = sig
  type t
  type 'a tags += Tag : t tags
end

type 'a tag = (module TAG with type t = 'a)

let new_tag (type a) () : a tag =
  (* Extend the type [_ tags] with a new data constructor [Tag]. *)
  let module T = struct
    type t = a
    type _ tags +=
      | Tag : a tags
  end in
  (* Return this module. *)
  (module T)

exception RuntimeTagError

let equal (type a1 a2) ((module A1) : a1 tag) ((module A2) : a2 tag) : (a1, a2) eq =
    match A1.Tag with
    | A2.Tag ->
        Eq
    | _ ->
        raise RuntimeTagError