package subtype-refinement

  1. Overview
  2. Docs

Source file subtype_refinement.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
53
module type IValue = sig
  type t

  val value : t
end

module type IConstraint = sig
  type t

  val where : t -> bool
end

module type Subtype = sig
  type super
  type t = private super

  exception FailedDownCast of super

  val upcast   : t     -> super
  val downcast : super -> t
end

module Refine (Constraint : IConstraint) : Subtype with
  type super = Constraint.t
= struct
  type super = Constraint.t
  type t     = Constraint.t

  exception FailedDownCast of Constraint.t

  let upcast value = value

  let downcast value =
    if Constraint.where value then value else raise (FailedDownCast value)
end

let refine (type a) condition =
  let module Module = Refine (struct
    type t = a

    let where = condition
  end) in
  (module Module : Subtype with type super = a)

module Singleton (Value : IValue) = struct
  include Refine (struct
    type t = Value.t

    let where value = (value == Value.value)
  end)
end

(* END *)