Source file resumptions.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
164
165
166
167
168
169
170
171
172
173
174
175
176
177
178
179
180
181
182
183
184
185
186
187
open UtilsLib
module Log = Xlog.Make (struct
let name = "Resumptions"
end)
module type Resumptions_sig =
sig
type 'a resumptions
type 'a computation
type w
val empty : alt_max:int -> 'a resumptions
val regular_sorting : 'a resumptions -> bool
val is_empty : 'a resumptions -> bool
val extend_resumptions : computation:'a computation ->
weight:w -> 'a resumptions -> 'a resumptions
val pp : Format.formatter -> 'a resumptions -> unit
val swap: ?current_computation:'a computation * w ->
'a resumptions -> 'a computation * w * 'a resumptions
end
module Make(W : Weight.Weight_sig)(C:sig type 'a computation end) =
struct
exception Empty
type 'a computation = 'a C.computation
type w = W.w
type 'a resumptions = { resumptions : 'a C.computation W.WMap.t;
alt_max : int ;
alt_number : int ;
regular_sorting : bool ;
unordered_resumptions : ('a C.computation * w) list ;
unordered_number : int;
}
let rec pow a = function
| 0 -> 1
| 1 -> a
| n ->
let b = pow a (n / 2) in
b * b * (if n mod 2 = 0 then 1 else a)
let empty ~alt_max =
let alt_max = max 0 alt_max in
{
resumptions = W.WMap.empty;
alt_max = pow 10 alt_max ;
alt_number = 0 ;
regular_sorting = true;
unordered_resumptions = [];
unordered_number = 0;}
let regular_sorting res = res.regular_sorting
let is_empty res =
match W.WMap.optimum res.resumptions, res.unordered_resumptions with
| None, [] ->
let () = assert (res.alt_number = 0) in
let () = assert (res.unordered_number = 0) in
true
| Some _, _ -> false
| None, _ :: _ -> false
let extend_resumptions ~computation ~weight resumptions =
if
resumptions.alt_number <= resumptions.alt_max &&
resumptions.regular_sorting then
{ resumptions with
resumptions = W.WMap.add weight computation resumptions.resumptions ;
alt_number = resumptions.alt_number + 1 }
else
let () = if resumptions.regular_sorting then
Logs.warn
(fun m -> m "The@ grammar@ is@ too@ ambiguous.@ \
Breaking@ regular@ sorting@ is@ needed@ in@ \
order@ to@ avoid@ stack@ overflow") in
{ resumptions with
alt_number = resumptions.alt_number + 1 ;
regular_sorting = false;
unordered_resumptions = (computation, weight) :: resumptions.unordered_resumptions;
unordered_number = resumptions.unordered_number + 1}
let pp fmt { resumptions ;
alt_number;
alt_max;
regular_sorting = _;
unordered_resumptions = _;
unordered_number = _;} =
Format.fprintf
fmt
"Current resumption is as follow:@ @[%d alternatives (max is %d).@ @[%a@]@]"
alt_number
alt_max
W.WMap.pp
resumptions[@@warning "-32"]
(** [swap ~current_computation resumptions] returns [(alternative_states,
new_resumption)] where [alternative_states] correspond to the
optimal binding of the resumption, and [new_resumption] the new
resumption when the optimal one has been removed. If
[current_computation] is provided, it is taken into account to check
the optimal binding, except if sorting is not regular in which
case it is directly returned (in order to stop swapping).
*)
let rec swap
?current_computation
({ resumptions=resumption_map ;
alt_number ;
alt_max=_ ;
regular_sorting ;
unordered_resumptions;
unordered_number;} as resumptions) =
match regular_sorting,
current_computation,
W.WMap.optimum resumption_map,
unordered_resumptions with
| true, _, _ , _ :: _ ->
failwith "Bug: the unorderd_resumptions should be empty when \
regular sorting is true"
| true, Some (computation, w), None, [] -> computation, w, resumptions
| true, Some (computation, w), Some opt, _ when (W.is_better w opt || W.is_equal w opt) ->
computation, w, resumptions
| true, Some (computation, w), Some _, _ ->
let new_resumptions =
extend_resumptions
~computation:computation
~weight:w
resumptions in
swap new_resumptions
| true, None, None, [] -> raise Empty
| false, Some (computation, w), _, _ :: _ ->
computation, w, resumptions
| false, Some (computation, w), _, [] ->
let () = Logs.warn (fun m -> m "Back@ to@ normal@ sorting") in
computation, w, {resumptions with regular_sorting = true}
| false, None, None, [] -> raise Empty
| false, None, _, (computation, w) :: tl ->
computation,
w,
{resumptions with
unordered_resumptions = tl;
unordered_number = unordered_number - 1;
}
| _, None, Some _, [] ->
let opt_computation, opt_w, new_map =
match W.WMap.pop_optimum resumption_map with
| None -> failwith "Bug: the optimume should not be set to None"
| Some res -> res in
opt_computation,
opt_w,
{ resumptions with
resumptions = new_map ;
alt_number = alt_number - 1 ;
regular_sorting = true ;
}
end