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
let ( <.> ) f g x = f (g x)
let identity x = x
type ('a, 'b) t = { to_ : 'a -> 'b; of_ : 'b -> 'a }
let v ~fwd ~bwd = { to_ = fwd; of_ = bwd }
let bwd { of_; _ } = of_
let fwd { to_; _ } = to_
let flip { of_; to_ } = { to_ = of_; of_ = to_ }
let product u v =
{
to_ = (fun (a, b) -> (u.to_ a, v.to_ b));
of_ = (fun (a, b) -> (u.of_ a, v.of_ b));
}
let compose u v = { to_ = v.to_ <.> u.to_; of_ = u.of_ <.> v.of_ }
let commute = { to_ = (fun (a, b) -> (b, a)); of_ = (fun (b, a) -> (a, b)) }
let identity = { to_ = identity; of_ = identity }
exception Bijection
let cons =
{
to_ = (fun (x, r) -> x :: r);
of_ = (function x :: r -> (x, r) | [] -> raise Bijection);
}
let char chr =
{
to_ = (fun chr' -> if Char.equal chr chr' then () else raise Bijection);
of_ = (fun () -> chr);
}
let string str =
{
to_ = (fun str' -> if String.equal str str' then () else raise Bijection);
of_ = (fun () -> str);
}
let element p =
{
to_ = (fun v -> if p v then v else raise Bijection);
of_ = (fun v -> if p v then v else raise Bijection);
}
let some =
{
to_ = (fun x -> Some x);
of_ = (function Some x -> x | None -> raise Bijection);
}
let obj3 =
{ to_ = (fun ((x, y), z) -> (x, y, z)); of_ = (fun (x, y, z) -> ((x, y), z)) }
let obj4 =
{
to_ = (fun (((w, x), y), z) -> (w, x, y, z));
of_ = (fun (w, x, y, z) -> (((w, x), y), z));
}
let obj5 =
{
to_ = (fun ((((v, w), x), y), z) -> (v, w, x, y, z));
of_ = (fun (v, w, x, y, z) -> ((((v, w), x), y), z));
}
let obj6 =
{
to_ = (fun (((((u, v), w), x), y), z) -> (u, v, w, x, y, z));
of_ = (fun (u, v, w, x, y, z) -> (((((u, v), w), x), y), z));
}