Source file strong.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
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132
133
134
135
136
137
138
139
140
141
142
143
144
145
146
147
148
149
150
151
152
153
154
155
156
157
158
159
160
161
162
163
(* Type-level equality *)
type (_, _) eq = Refl : ('a, 'a) eq
let follow_eq (type a b) (Refl : (a, b) eq) (x : a) : b = x

(* Strongly typed ordering *)
module Order = struct type (_, _) t = Lt | Eq : ('a, 'a) t | Gt end
type ('a, 'b) order = ('a, 'b) Order.t

let order_from_comparison n =
  if n < 0 then Order.Lt
  else if n > 0 then Order.Gt
  else Order.Eq

(* Uninhabitated type *)
type void = { void : 'a. 'a }
let void v = v.void

module Natural : sig
  type 'a t
  val order : 'a t -> 'b t -> ('a, 'b) order
  val lift_eq : ('a, 'b) eq -> ('a t, 'b t) eq

  val to_int : 'a t -> int

  type zero
  val zero : zero t

  type one
  val one : one t

  module type T = sig type n val n : n t end
  module Nth (N : sig val n : int end) : T
  val nth : int -> (module T)

  type ('a, 'b) sum
  val add : 'a t -> 'b t -> ('a, 'b) sum t
  val sum_comm : (('a, 'b) sum, ('b, 'a) sum) eq
  val sum_assoc : ((('a, 'b) sum, 'c) sum, ('a, ('b, 'c) sum) sum) eq

  type ('a, 'b) prod
  val mul : 'a t -> 'b t -> ('a, 'b) prod t
  val prod_comm : (('a, 'b) prod, ('b, 'a) prod) eq
  val prod_assoc : ((('a, 'b) prod, 'c) prod, ('a, ('b, 'c) prod) prod) eq
end = struct
  type 'a t = T : int -> unit t

  let order (type a b) (T a : a t) (T b : b t) : (a, b) order =
    Order.(if a < b then Lt else if a > b then Gt else Eq)

  let lift_eq (type a b) (Refl : (a, b) eq) : (a t, b t) eq =
    Refl

  let to_int (type n) (T n : n t) = n

  type zero = unit
  let zero : zero t = T 0

  type one = unit
  let one : one t = T 1

  module type T = sig type n val n : n t end

  module Nth (N : sig val n : int end) : T = struct
    type n = unit let n : n t = T N.n
  end

  let nth n =
    let module N = struct
      type n = unit
      let n = T n
    end
    in
    (module N : T)

  type ('a, 'b) sum = unit
  let add (type a b) (T a : a t) (T b : b t) : (a, b) sum t =
    T (a + b)
  let sum_comm (type a b)
    : ((a, b) sum, (b, a) sum) eq = Refl
  let sum_assoc (type a b c)
    : (((a, b) sum, c) sum, (a, (b, c) sum) sum) eq = Refl

  type ('a, 'b) prod = unit
  let mul (type a b) (T a : a t) (T b : b t) : (a, b) prod t =
    T (a * b)
  let prod_comm (type a b)
    : ((a, b) prod, (b, a) prod) eq = Refl
  let prod_assoc (type a b c)
    : (((a, b) prod, c) prod, (a, (b, c) prod) prod) eq = Refl
end

(* Finite sets: interpret naturals as the cardinality of a set *)
module Finite : sig
  type 'a set = 'a Natural.t
  module type Set = Natural.T
  val cardinal : 'a set -> int

  type 'a elt = private int
  val elt_of_int : 'a set -> int -> 'a elt
  val elt_to_int : 'a elt -> int
  val iter_set : 'a set -> ('a elt -> unit) -> unit
  val rev_iter_set : 'a set -> ('a elt -> unit) -> unit
  val all_elements : 'a set -> 'a elt array

  (* Temporary API, should be replaced by something array-like in the future *)
  module type Map = sig
    type domain
    val domain : domain set
    type codomain
    val get : domain elt -> codomain
  end
  type 'a map = (module Map with type codomain = 'a)

  module Map_of_array (A : sig type codomain val table : codomain array end) :
    Map with type codomain = A.codomain

  val iter_map : 'a map -> ('a -> unit) -> unit
end = struct
  type 'a set = 'a Natural.t
  module type Set = Natural.T
  let cardinal = Natural.to_int

  type 'a elt = int

  let elt_of_int (type a) (set : a set) n : a elt =
    let c = cardinal set in
    if n >= 0 && n < c then n else
      Printf.ksprintf invalid_arg
        "Strong.Finite.of_int #%d %d: %d is not in [0; %d[" c n n c

  let elt_to_int x = x

  let iter_set (type a) (set : a set) f =
    for i = 0 to cardinal set - 1 do f i done

  let rev_iter_set (type a) (set : a set) f =
    for i = cardinal set - 1 downto 0 do f i done

  let all_elements (type a) (set : a set) =
    Array.init (cardinal set) (fun x -> x)

  (* Temporary API, should be replaced by something array-like in the future *)
  module type Map = sig
    type domain
    val domain : domain set
    type codomain
    val get : domain elt -> codomain
  end
  type 'a map = (module Map with type codomain = 'a)

  module Map_of_array (A : sig type codomain val table : codomain array end) :
    Map with type codomain = A.codomain =
  struct
    module Card = Natural.Nth(struct let n = Array.length A.table end)
    type domain = Card.n
    let domain = Card.n
    type codomain = A.codomain
    let get i = A.table.(i)
  end

  let iter_map (type a) ((module Map) : a map) (f : a -> unit) : unit =
    iter_set Map.domain (fun elt -> f (Map.get elt))
end