blob: 7053ed6817d5759a9439b602949f81e40f85110e (
plain)
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
|
(* TEST
* expect *)
module type Endpoint_intf = sig
type t
end
;;
[%%expect{|
module type Endpoint_intf = sig type t end
|}]
module type S = sig
module Endpoint : Endpoint_intf
type finite = [ `Before of Endpoint.t ]
type infinite = [ `Until_infinity ]
type +'a range = private { until : 'a } constraint 'a = [< finite | infinite ]
val until : 'a range -> 'a
end
;;
[%%expect{|
module type S =
sig
module Endpoint : Endpoint_intf
type finite = [ `Before of Endpoint.t ]
type infinite = [ `Until_infinity ]
type +'a range = private { until : 'a; }
constraint 'a = [< `Before of Endpoint.t | `Until_infinity ]
val until :
([< `Before of Endpoint.t | `Until_infinity ] as 'a) range -> 'a
end
|}]
module type Ranged = sig
module Endpoint : Endpoint_intf
module Range : S with type Endpoint.t = Endpoint.t
end
;;
[%%expect{|
module type Ranged =
sig
module Endpoint : Endpoint_intf
module Range :
sig
module Endpoint : sig type t = Endpoint.t end
type finite = [ `Before of Endpoint.t ]
type infinite = [ `Until_infinity ]
type +'a range = private { until : 'a; }
constraint 'a = [< `Before of Endpoint.t | `Until_infinity ]
val until :
([< `Before of Endpoint.t | `Until_infinity ] as 'a) range -> 'a
end
end
|}]
module Assume (Given : sig
module Make_range (Endpoint : Endpoint_intf) :
S with module Endpoint = Endpoint
module Make_ranged (Range : S) :
Ranged with module Endpoint = Range.Endpoint
and module Range = Range
end) =
struct
module Point = struct
type t
end
open Given
module Test_range = Make_range(Point)
module Test_ranged = Make_ranged(Test_range)
end
;;
[%%expect{|
module Assume :
functor
(Given : sig
module Make_range :
functor (Endpoint : Endpoint_intf) ->
sig
module Endpoint : sig type t = Endpoint.t end
type finite = [ `Before of Endpoint.t ]
type infinite = [ `Until_infinity ]
type +'a range = private { until : 'a; }
constraint 'a =
[< `Before of Endpoint.t | `Until_infinity ]
val until :
([< `Before of Endpoint.t | `Until_infinity ] as 'a)
range -> 'a
end
module Make_ranged :
functor (Range : S) ->
sig
module Endpoint : sig type t = Range.Endpoint.t end
module Range :
sig
module Endpoint : sig type t = Range.Endpoint.t end
type finite = [ `Before of Endpoint.t ]
type infinite = [ `Until_infinity ]
type +'a range =
'a Range.range = private {
until : 'a;
}
constraint 'a =
[< `Before of Endpoint.t | `Until_infinity ]
val until :
([< `Before of Endpoint.t | `Until_infinity ]
as 'a)
range -> 'a
end
end
end)
->
sig
module Point : sig type t end
module Test_range :
sig
module Endpoint : sig type t = Point.t end
type finite = [ `Before of Endpoint.t ]
type infinite = [ `Until_infinity ]
type +'a range =
'a Given.Make_range(Point).range = private {
until : 'a;
} constraint 'a = [< `Before of Endpoint.t | `Until_infinity ]
val until :
([< `Before of Endpoint.t | `Until_infinity ] as 'a) range -> 'a
end
module Test_ranged :
sig
module Endpoint : sig type t = Test_range.Endpoint.t end
module Range :
sig
module Endpoint : sig type t = Test_range.Endpoint.t end
type finite = [ `Before of Endpoint.t ]
type infinite = [ `Until_infinity ]
type +'a range = 'a Test_range.range = private { until : 'a; }
constraint 'a = [< `Before of Endpoint.t | `Until_infinity ]
val until :
([< `Before of Endpoint.t | `Until_infinity ] as 'a) range ->
'a
end
end
end
|}]
|
