Source file `Univ.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
(******************************************************************************)
(*                                                                            *)
(*                                 UnionFind                                  *)
(*                                                                            *)
(*                       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.           *)
(*                                                                            *)
(******************************************************************************)

(* Our universal type is an extensible algebraic data type. *)

type univ =
  ..

(* [make] is implemented by generating a fresh data constructor [Tag].
   The functions [project] and [inject] respectively apply [Tag] and
   match against [Tag]. *)

let make (type a) () : (a -> univ) * (univ -> a option) =

  let module T = struct

    type univ += Tag of a

    let inject (x : a) : univ =
      Tag x

    let project (u : univ) : a option =
      match u with
      | Tag x ->
	  Some x
      | _ ->
	  None

  end in
  T.inject, T.project