106 | St_skip of Graphs.label
107 | St_cost of CostLabel.costlabel * Graphs.label
108 | St_const of AST.typ * Registers.register * FrontEndOps.constant
110 | St_op1 of AST.typ * AST.typ * FrontEndOps.unary_operation
111 * Registers.register * Registers.register * Graphs.label
112 | St_op2 of AST.typ * AST.typ * AST.typ * FrontEndOps.binary_operation
113 * Registers.register * Registers.register * Registers.register
115 | St_load of AST.typ * Registers.register * Registers.register * Graphs.label
116 | St_store of AST.typ * Registers.register * Registers.register
118 | St_call_id of AST.ident * Registers.register List.list
119 * Registers.register Types.option * Graphs.label
120 | St_call_ptr of Registers.register * Registers.register List.list
121 * Registers.register Types.option * Graphs.label
122 | St_cond of Registers.register * Graphs.label * Graphs.label
125 (** val statement_rect_Type4 :
126 (Graphs.label -> 'a1) -> (CostLabel.costlabel -> Graphs.label -> 'a1) ->
127 (AST.typ -> Registers.register -> FrontEndOps.constant -> Graphs.label ->
128 'a1) -> (AST.typ -> AST.typ -> FrontEndOps.unary_operation ->
129 Registers.register -> Registers.register -> Graphs.label -> 'a1) ->
130 (AST.typ -> AST.typ -> AST.typ -> FrontEndOps.binary_operation ->
131 Registers.register -> Registers.register -> Registers.register ->
132 Graphs.label -> 'a1) -> (AST.typ -> Registers.register ->
133 Registers.register -> Graphs.label -> 'a1) -> (AST.typ ->
134 Registers.register -> Registers.register -> Graphs.label -> 'a1) ->
135 (AST.ident -> Registers.register List.list -> Registers.register
136 Types.option -> Graphs.label -> 'a1) -> (Registers.register ->
137 Registers.register List.list -> Registers.register Types.option ->
138 Graphs.label -> 'a1) -> (Registers.register -> Graphs.label ->
139 Graphs.label -> 'a1) -> 'a1 -> statement -> 'a1 **)
140 let rec statement_rect_Type4 h_St_skip h_St_cost h_St_const h_St_op1 h_St_op2 h_St_load h_St_store h_St_call_id h_St_call_ptr h_St_cond h_St_return = function
141 | St_skip x_14903 -> h_St_skip x_14903
142 | St_cost (x_14905, x_14904) -> h_St_cost x_14905 x_14904
143 | St_const (t, x_14908, x_14907, x_14906) ->
144 h_St_const t x_14908 x_14907 x_14906
145 | St_op1 (t', t, x_14912, x_14911, x_14910, x_14909) ->
146 h_St_op1 t' t x_14912 x_14911 x_14910 x_14909
147 | St_op2 (t', t1, t2, x_14917, x_14916, x_14915, x_14914, x_14913) ->
148 h_St_op2 t' t1 t2 x_14917 x_14916 x_14915 x_14914 x_14913
149 | St_load (x_14921, x_14920, x_14919, x_14918) ->
150 h_St_load x_14921 x_14920 x_14919 x_14918
151 | St_store (x_14925, x_14924, x_14923, x_14922) ->
152 h_St_store x_14925 x_14924 x_14923 x_14922
153 | St_call_id (x_14929, x_14928, x_14927, x_14926) ->
154 h_St_call_id x_14929 x_14928 x_14927 x_14926
155 | St_call_ptr (x_14933, x_14932, x_14931, x_14930) ->
156 h_St_call_ptr x_14933 x_14932 x_14931 x_14930
157 | St_cond (x_14936, x_14935, x_14934) -> h_St_cond x_14936 x_14935 x_14934
158 | St_return -> h_St_return
160 (** val statement_rect_Type5 :
161 (Graphs.label -> 'a1) -> (CostLabel.costlabel -> Graphs.label -> 'a1) ->
162 (AST.typ -> Registers.register -> FrontEndOps.constant -> Graphs.label ->
163 'a1) -> (AST.typ -> AST.typ -> FrontEndOps.unary_operation ->
164 Registers.register -> Registers.register -> Graphs.label -> 'a1) ->
165 (AST.typ -> AST.typ -> AST.typ -> FrontEndOps.binary_operation ->
166 Registers.register -> Registers.register -> Registers.register ->
167 Graphs.label -> 'a1) -> (AST.typ -> Registers.register ->
168 Registers.register -> Graphs.label -> 'a1) -> (AST.typ ->
169 Registers.register -> Registers.register -> Graphs.label -> 'a1) ->
170 (AST.ident -> Registers.register List.list -> Registers.register
171 Types.option -> Graphs.label -> 'a1) -> (Registers.register ->
172 Registers.register List.list -> Registers.register Types.option ->
173 Graphs.label -> 'a1) -> (Registers.register -> Graphs.label ->
174 Graphs.label -> 'a1) -> 'a1 -> statement -> 'a1 **)
175 let rec statement_rect_Type5 h_St_skip h_St_cost h_St_const h_St_op1 h_St_op2 h_St_load h_St_store h_St_call_id h_St_call_ptr h_St_cond h_St_return = function
176 | St_skip x_14949 -> h_St_skip x_14949
177 | St_cost (x_14951, x_14950) -> h_St_cost x_14951 x_14950
178 | St_const (t, x_14954, x_14953, x_14952) ->
179 h_St_const t x_14954 x_14953 x_14952
180 | St_op1 (t', t, x_14958, x_14957, x_14956, x_14955) ->
181 h_St_op1 t' t x_14958 x_14957 x_14956 x_14955
182 | St_op2 (t', t1, t2, x_14963, x_14962, x_14961, x_14960, x_14959) ->
183 h_St_op2 t' t1 t2 x_14963 x_14962 x_14961 x_14960 x_14959
184 | St_load (x_14967, x_14966, x_14965, x_14964) ->
185 h_St_load x_14967 x_14966 x_14965 x_14964
186 | St_store (x_14971, x_14970, x_14969, x_14968) ->
187 h_St_store x_14971 x_14970 x_14969 x_14968
188 | St_call_id (x_14975, x_14974, x_14973, x_14972) ->
189 h_St_call_id x_14975 x_14974 x_14973 x_14972
190 | St_call_ptr (x_14979, x_14978, x_14977, x_14976) ->
191 h_St_call_ptr x_14979 x_14978 x_14977 x_14976
192 | St_cond (x_14982, x_14981, x_14980) -> h_St_cond x_14982 x_14981 x_14980
193 | St_return -> h_St_return
195 (** val statement_rect_Type3 :
196 (Graphs.label -> 'a1) -> (CostLabel.costlabel -> Graphs.label -> 'a1) ->
197 (AST.typ -> Registers.register -> FrontEndOps.constant -> Graphs.label ->
198 'a1) -> (AST.typ -> AST.typ -> FrontEndOps.unary_operation ->
199 Registers.register -> Registers.register -> Graphs.label -> 'a1) ->
200 (AST.typ -> AST.typ -> AST.typ -> FrontEndOps.binary_operation ->
201 Registers.register -> Registers.register -> Registers.register ->
202 Graphs.label -> 'a1) -> (AST.typ -> Registers.register ->
203 Registers.register -> Graphs.label -> 'a1) -> (AST.typ ->
204 Registers.register -> Registers.register -> Graphs.label -> 'a1) ->
205 (AST.ident -> Registers.register List.list -> Registers.register
206 Types.option -> Graphs.label -> 'a1) -> (Registers.register ->
207 Registers.register List.list -> Registers.register Types.option ->
208 Graphs.label -> 'a1) -> (Registers.register -> Graphs.label ->
209 Graphs.label -> 'a1) -> 'a1 -> statement -> 'a1 **)
210 let rec statement_rect_Type3 h_St_skip h_St_cost h_St_const h_St_op1 h_St_op2 h_St_load h_St_store h_St_call_id h_St_call_ptr h_St_cond h_St_return = function
211 | St_skip x_14995 -> h_St_skip x_14995
212 | St_cost (x_14997, x_14996) -> h_St_cost x_14997 x_14996
213 | St_const (t, x_15000, x_14999, x_14998) ->
214 h_St_const t x_15000 x_14999 x_14998
215 | St_op1 (t', t, x_15004, x_15003, x_15002, x_15001) ->
216 h_St_op1 t' t x_15004 x_15003 x_15002 x_15001
217 | St_op2 (t', t1, t2, x_15009, x_15008, x_15007, x_15006, x_15005) ->
218 h_St_op2 t' t1 t2 x_15009 x_15008 x_15007 x_15006 x_15005
219 | St_load (x_15013, x_15012, x_15011, x_15010) ->
220 h_St_load x_15013 x_15012 x_15011 x_15010
221 | St_store (x_15017, x_15016, x_15015, x_15014) ->
222 h_St_store x_15017 x_15016 x_15015 x_15014
223 | St_call_id (x_15021, x_15020, x_15019, x_15018) ->
224 h_St_call_id x_15021 x_15020 x_15019 x_15018
225 | St_call_ptr (x_15025, x_15024, x_15023, x_15022) ->
226 h_St_call_ptr x_15025 x_15024 x_15023 x_15022
227 | St_cond (x_15028, x_15027, x_15026) -> h_St_cond x_15028 x_15027 x_15026
228 | St_return -> h_St_return
230 (** val statement_rect_Type2 :
231 (Graphs.label -> 'a1) -> (CostLabel.costlabel -> Graphs.label -> 'a1) ->
232 (AST.typ -> Registers.register -> FrontEndOps.constant -> Graphs.label ->
233 'a1) -> (AST.typ -> AST.typ -> FrontEndOps.unary_operation ->
234 Registers.register -> Registers.register -> Graphs.label -> 'a1) ->
235 (AST.typ -> AST.typ -> AST.typ -> FrontEndOps.binary_operation ->
236 Registers.register -> Registers.register -> Registers.register ->
237 Graphs.label -> 'a1) -> (AST.typ -> Registers.register ->
238 Registers.register -> Graphs.label -> 'a1) -> (AST.typ ->
239 Registers.register -> Registers.register -> Graphs.label -> 'a1) ->
240 (AST.ident -> Registers.register List.list -> Registers.register
241 Types.option -> Graphs.label -> 'a1) -> (Registers.register ->
242 Registers.register List.list -> Registers.register Types.option ->
243 Graphs.label -> 'a1) -> (Registers.register -> Graphs.label ->
244 Graphs.label -> 'a1) -> 'a1 -> statement -> 'a1 **)
245 let rec statement_rect_Type2 h_St_skip h_St_cost h_St_const h_St_op1 h_St_op2 h_St_load h_St_store h_St_call_id h_St_call_ptr h_St_cond h_St_return = function
246 | St_skip x_15041 -> h_St_skip x_15041
247 | St_cost (x_15043, x_15042) -> h_St_cost x_15043 x_15042
248 | St_const (t, x_15046, x_15045, x_15044) ->
249 h_St_const t x_15046 x_15045 x_15044
250 | St_op1 (t', t, x_15050, x_15049, x_15048, x_15047) ->
251 h_St_op1 t' t x_15050 x_15049 x_15048 x_15047
252 | St_op2 (t', t1, t2, x_15055, x_15054, x_15053, x_15052, x_15051) ->
253 h_St_op2 t' t1 t2 x_15055 x_15054 x_15053 x_15052 x_15051
254 | St_load (x_15059, x_15058, x_15057, x_15056) ->
255 h_St_load x_15059 x_15058 x_15057 x_15056
256 | St_store (x_15063, x_15062, x_15061, x_15060) ->
257 h_St_store x_15063 x_15062 x_15061 x_15060
258 | St_call_id (x_15067, x_15066, x_15065, x_15064) ->
259 h_St_call_id x_15067 x_15066 x_15065 x_15064
260 | St_call_ptr (x_15071, x_15070, x_15069, x_15068) ->
261 h_St_call_ptr x_15071 x_15070 x_15069 x_15068
262 | St_cond (x_15074, x_15073, x_15072) -> h_St_cond x_15074 x_15073 x_15072
263 | St_return -> h_St_return
265 (** val statement_rect_Type1 :
266 (Graphs.label -> 'a1) -> (CostLabel.costlabel -> Graphs.label -> 'a1) ->
267 (AST.typ -> Registers.register -> FrontEndOps.constant -> Graphs.label ->
268 'a1) -> (AST.typ -> AST.typ -> FrontEndOps.unary_operation ->
269 Registers.register -> Registers.register -> Graphs.label -> 'a1) ->
270 (AST.typ -> AST.typ -> AST.typ -> FrontEndOps.binary_operation ->
271 Registers.register -> Registers.register -> Registers.register ->
272 Graphs.label -> 'a1) -> (AST.typ -> Registers.register ->
273 Registers.register -> Graphs.label -> 'a1) -> (AST.typ ->
274 Registers.register -> Registers.register -> Graphs.label -> 'a1) ->
275 (AST.ident -> Registers.register List.list -> Registers.register
276 Types.option -> Graphs.label -> 'a1) -> (Registers.register ->
277 Registers.register List.list -> Registers.register Types.option ->
278 Graphs.label -> 'a1) -> (Registers.register -> Graphs.label ->
279 Graphs.label -> 'a1) -> 'a1 -> statement -> 'a1 **)
280 let rec statement_rect_Type1 h_St_skip h_St_cost h_St_const h_St_op1 h_St_op2 h_St_load h_St_store h_St_call_id h_St_call_ptr h_St_cond h_St_return = function
281 | St_skip x_15087 -> h_St_skip x_15087
282 | St_cost (x_15089, x_15088) -> h_St_cost x_15089 x_15088
283 | St_const (t, x_15092, x_15091, x_15090) ->
284 h_St_const t x_15092 x_15091 x_15090
285 | St_op1 (t', t, x_15096, x_15095, x_15094, x_15093) ->
286 h_St_op1 t' t x_15096 x_15095 x_15094 x_15093
287 | St_op2 (t', t1, t2, x_15101, x_15100, x_15099, x_15098, x_15097) ->
288 h_St_op2 t' t1 t2 x_15101 x_15100 x_15099 x_15098 x_15097
289 | St_load (x_15105, x_15104, x_15103, x_15102) ->
290 h_St_load x_15105 x_15104 x_15103 x_15102
291 | St_store (x_15109, x_15108, x_15107, x_15106) ->
292 h_St_store x_15109 x_15108 x_15107 x_15106
293 | St_call_id (x_15113, x_15112, x_15111, x_15110) ->
294 h_St_call_id x_15113 x_15112 x_15111 x_15110
295 | St_call_ptr (x_15117, x_15116, x_15115, x_15114) ->
296 h_St_call_ptr x_15117 x_15116 x_15115 x_15114
297 | St_cond (x_15120, x_15119, x_15118) -> h_St_cond x_15120 x_15119 x_15118
298 | St_return -> h_St_return
300 (** val statement_rect_Type0 :
301 (Graphs.label -> 'a1) -> (CostLabel.costlabel -> Graphs.label -> 'a1) ->
302 (AST.typ -> Registers.register -> FrontEndOps.constant -> Graphs.label ->
303 'a1) -> (AST.typ -> AST.typ -> FrontEndOps.unary_operation ->
304 Registers.register -> Registers.register -> Graphs.label -> 'a1) ->
305 (AST.typ -> AST.typ -> AST.typ -> FrontEndOps.binary_operation ->
306 Registers.register -> Registers.register -> Registers.register ->
307 Graphs.label -> 'a1) -> (AST.typ -> Registers.register ->
308 Registers.register -> Graphs.label -> 'a1) -> (AST.typ ->
309 Registers.register -> Registers.register -> Graphs.label -> 'a1) ->
310 (AST.ident -> Registers.register List.list -> Registers.register
311 Types.option -> Graphs.label -> 'a1) -> (Registers.register ->
312 Registers.register List.list -> Registers.register Types.option ->
313 Graphs.label -> 'a1) -> (Registers.register -> Graphs.label ->
314 Graphs.label -> 'a1) -> 'a1 -> statement -> 'a1 **)
315 let rec statement_rect_Type0 h_St_skip h_St_cost h_St_const h_St_op1 h_St_op2 h_St_load h_St_store h_St_call_id h_St_call_ptr h_St_cond h_St_return = function
316 | St_skip x_15133 -> h_St_skip x_15133
317 | St_cost (x_15135, x_15134) -> h_St_cost x_15135 x_15134
318 | St_const (t, x_15138, x_15137, x_15136) ->
319 h_St_const t x_15138 x_15137 x_15136
320 | St_op1 (t', t, x_15142, x_15141, x_15140, x_15139) ->
321 h_St_op1 t' t x_15142 x_15141 x_15140 x_15139
322 | St_op2 (t', t1, t2, x_15147, x_15146, x_15145, x_15144, x_15143) ->
323 h_St_op2 t' t1 t2 x_15147 x_15146 x_15145 x_15144 x_15143
324 | St_load (x_15151, x_15150, x_15149, x_15148) ->
325 h_St_load x_15151 x_15150 x_15149 x_15148
326 | St_store (x_15155, x_15154, x_15153, x_15152) ->
327 h_St_store x_15155 x_15154 x_15153 x_15152
328 | St_call_id (x_15159, x_15158, x_15157, x_15156) ->
329 h_St_call_id x_15159 x_15158 x_15157 x_15156
330 | St_call_ptr (x_15163, x_15162, x_15161, x_15160) ->
331 h_St_call_ptr x_15163 x_15162 x_15161 x_15160
332 | St_cond (x_15166, x_15165, x_15164) -> h_St_cond x_15166 x_15165 x_15164
333 | St_return -> h_St_return
335 (** val statement_inv_rect_Type4 :
336 statement -> (Graphs.label -> __ -> 'a1) -> (CostLabel.costlabel ->
337 Graphs.label -> __ -> 'a1) -> (AST.typ -> Registers.register ->
338 FrontEndOps.constant -> Graphs.label -> __ -> 'a1) -> (AST.typ -> AST.typ
339 -> FrontEndOps.unary_operation -> Registers.register ->
340 Registers.register -> Graphs.label -> __ -> 'a1) -> (AST.typ -> AST.typ
341 -> AST.typ -> FrontEndOps.binary_operation -> Registers.register ->
342 Registers.register -> Registers.register -> Graphs.label -> __ -> 'a1) ->
343 (AST.typ -> Registers.register -> Registers.register -> Graphs.label ->
344 __ -> 'a1) -> (AST.typ -> Registers.register -> Registers.register ->
345 Graphs.label -> __ -> 'a1) -> (AST.ident -> Registers.register List.list
346 -> Registers.register Types.option -> Graphs.label -> __ -> 'a1) ->
347 (Registers.register -> Registers.register List.list -> Registers.register
348 Types.option -> Graphs.label -> __ -> 'a1) -> (Registers.register ->
349 Graphs.label -> Graphs.label -> __ -> 'a1) -> (__ -> 'a1) -> 'a1 **)
350 let statement_inv_rect_Type4 hterm h1 h2 h3 h4 h5 h6 h7 h8 h9 h10 h11 =
351 let hcut = statement_rect_Type4 h1 h2 h3 h4 h5 h6 h7 h8 h9 h10 h11 hterm in
354 (** val statement_inv_rect_Type3 :
355 statement -> (Graphs.label -> __ -> 'a1) -> (CostLabel.costlabel ->
356 Graphs.label -> __ -> 'a1) -> (AST.typ -> Registers.register ->
357 FrontEndOps.constant -> Graphs.label -> __ -> 'a1) -> (AST.typ -> AST.typ
358 -> FrontEndOps.unary_operation -> Registers.register ->
359 Registers.register -> Graphs.label -> __ -> 'a1) -> (AST.typ -> AST.typ
360 -> AST.typ -> FrontEndOps.binary_operation -> Registers.register ->
361 Registers.register -> Registers.register -> Graphs.label -> __ -> 'a1) ->
362 (AST.typ -> Registers.register -> Registers.register -> Graphs.label ->
363 __ -> 'a1) -> (AST.typ -> Registers.register -> Registers.register ->
364 Graphs.label -> __ -> 'a1) -> (AST.ident -> Registers.register List.list
365 -> Registers.register Types.option -> Graphs.label -> __ -> 'a1) ->
366 (Registers.register -> Registers.register List.list -> Registers.register
367 Types.option -> Graphs.label -> __ -> 'a1) -> (Registers.register ->
368 Graphs.label -> Graphs.label -> __ -> 'a1) -> (__ -> 'a1) -> 'a1 **)
369 let statement_inv_rect_Type3 hterm h1 h2 h3 h4 h5 h6 h7 h8 h9 h10 h11 =
370 let hcut = statement_rect_Type3 h1 h2 h3 h4 h5 h6 h7 h8 h9 h10 h11 hterm in
373 (** val statement_inv_rect_Type2 :
374 statement -> (Graphs.label -> __ -> 'a1) -> (CostLabel.costlabel ->
375 Graphs.label -> __ -> 'a1) -> (AST.typ -> Registers.register ->
376 FrontEndOps.constant -> Graphs.label -> __ -> 'a1) -> (AST.typ -> AST.typ
377 -> FrontEndOps.unary_operation -> Registers.register ->
378 Registers.register -> Graphs.label -> __ -> 'a1) -> (AST.typ -> AST.typ
379 -> AST.typ -> FrontEndOps.binary_operation -> Registers.register ->
380 Registers.register -> Registers.register -> Graphs.label -> __ -> 'a1) ->
381 (AST.typ -> Registers.register -> Registers.register -> Graphs.label ->
382 __ -> 'a1) -> (AST.typ -> Registers.register -> Registers.register ->
383 Graphs.label -> __ -> 'a1) -> (AST.ident -> Registers.register List.list
384 -> Registers.register Types.option -> Graphs.label -> __ -> 'a1) ->
385 (Registers.register -> Registers.register List.list -> Registers.register
386 Types.option -> Graphs.label -> __ -> 'a1) -> (Registers.register ->
387 Graphs.label -> Graphs.label -> __ -> 'a1) -> (__ -> 'a1) -> 'a1 **)
388 let statement_inv_rect_Type2 hterm h1 h2 h3 h4 h5 h6 h7 h8 h9 h10 h11 =
389 let hcut = statement_rect_Type2 h1 h2 h3 h4 h5 h6 h7 h8 h9 h10 h11 hterm in
392 (** val statement_inv_rect_Type1 :
393 statement -> (Graphs.label -> __ -> 'a1) -> (CostLabel.costlabel ->
394 Graphs.label -> __ -> 'a1) -> (AST.typ -> Registers.register ->
395 FrontEndOps.constant -> Graphs.label -> __ -> 'a1) -> (AST.typ -> AST.typ
396 -> FrontEndOps.unary_operation -> Registers.register ->
397 Registers.register -> Graphs.label -> __ -> 'a1) -> (AST.typ -> AST.typ
398 -> AST.typ -> FrontEndOps.binary_operation -> Registers.register ->
399 Registers.register -> Registers.register -> Graphs.label -> __ -> 'a1) ->
400 (AST.typ -> Registers.register -> Registers.register -> Graphs.label ->
401 __ -> 'a1) -> (AST.typ -> Registers.register -> Registers.register ->
402 Graphs.label -> __ -> 'a1) -> (AST.ident -> Registers.register List.list
403 -> Registers.register Types.option -> Graphs.label -> __ -> 'a1) ->
404 (Registers.register -> Registers.register List.list -> Registers.register
405 Types.option -> Graphs.label -> __ -> 'a1) -> (Registers.register ->
406 Graphs.label -> Graphs.label -> __ -> 'a1) -> (__ -> 'a1) -> 'a1 **)
407 let statement_inv_rect_Type1 hterm h1 h2 h3 h4 h5 h6 h7 h8 h9 h10 h11 =
408 let hcut = statement_rect_Type1 h1 h2 h3 h4 h5 h6 h7 h8 h9 h10 h11 hterm in
411 (** val statement_inv_rect_Type0 :
412 statement -> (Graphs.label -> __ -> 'a1) -> (CostLabel.costlabel ->
413 Graphs.label -> __ -> 'a1) -> (AST.typ -> Registers.register ->
414 FrontEndOps.constant -> Graphs.label -> __ -> 'a1) -> (AST.typ -> AST.typ
415 -> FrontEndOps.unary_operation -> Registers.register ->
416 Registers.register -> Graphs.label -> __ -> 'a1) -> (AST.typ -> AST.typ
417 -> AST.typ -> FrontEndOps.binary_operation -> Registers.register ->
418 Registers.register -> Registers.register -> Graphs.label -> __ -> 'a1) ->
419 (AST.typ -> Registers.register -> Registers.register -> Graphs.label ->
420 __ -> 'a1) -> (AST.typ -> Registers.register -> Registers.register ->
421 Graphs.label -> __ -> 'a1) -> (AST.ident -> Registers.register List.list
422 -> Registers.register Types.option -> Graphs.label -> __ -> 'a1) ->
423 (Registers.register -> Registers.register List.list -> Registers.register
424 Types.option -> Graphs.label -> __ -> 'a1) -> (Registers.register ->
425 Graphs.label -> Graphs.label -> __ -> 'a1) -> (__ -> 'a1) -> 'a1 **)
426 let statement_inv_rect_Type0 hterm h1 h2 h3 h4 h5 h6 h7 h8 h9 h10 h11 =
427 let hcut = statement_rect_Type0 h1 h2 h3 h4 h5 h6 h7 h8 h9 h10 h11 hterm in
430 (** val statement_jmdiscr : statement -> statement -> __ **)
431 let statement_jmdiscr x y =
432 Logic.eq_rect_Type2 x
434 | St_skip a0 -> Obj.magic (fun _ dH -> dH __)
435 | St_cost (a0, a1) -> Obj.magic (fun _ dH -> dH __ __)
436 | St_const (a0, a1, a2, a3) -> Obj.magic (fun _ dH -> dH __ __ __ __)
437 | St_op1 (a0, a1, a2, a3, a4, a5) ->
438 Obj.magic (fun _ dH -> dH __ __ __ __ __ __)
439 | St_op2 (a0, a1, a2, a3, a4, a5, a6, a7) ->
440 Obj.magic (fun _ dH -> dH __ __ __ __ __ __ __ __)
441 | St_load (a0, a1, a2, a3) -> Obj.magic (fun _ dH -> dH __ __ __ __)
442 | St_store (a0, a1, a2, a3) -> Obj.magic (fun _ dH -> dH __ __ __ __)
443 | St_call_id (a0, a1, a2, a3) -> Obj.magic (fun _ dH -> dH __ __ __ __)
444 | St_call_ptr (a0, a1, a2, a3) -> Obj.magic (fun _ dH -> dH __ __ __ __)
445 | St_cond (a0, a1, a2) -> Obj.magic (fun _ dH -> dH __ __ __)
446 | St_return -> Obj.magic (fun _ dH -> dH)) y
448 type internal_function = { f_labgen : Identifiers.universe;
449 f_reggen : Identifiers.universe;
450 f_result : (Registers.register, AST.typ)
451 Types.prod Types.option;
452 f_params : (Registers.register, AST.typ)
453 Types.prod List.list;
454 f_locals : (Registers.register, AST.typ)
455 Types.prod List.list;
456 f_stacksize : Nat.nat;
457 f_graph : statement Graphs.graph;
458 f_entry : Graphs.label Types.sig0;
459 f_exit : Graphs.label Types.sig0 }
461 (** val internal_function_rect_Type4 :
462 (Identifiers.universe -> Identifiers.universe -> (Registers.register,
463 AST.typ) Types.prod Types.option -> (Registers.register, AST.typ)
464 Types.prod List.list -> (Registers.register, AST.typ) Types.prod
465 List.list -> Nat.nat -> statement Graphs.graph -> __ -> __ ->
466 Graphs.label Types.sig0 -> Graphs.label Types.sig0 -> __ -> 'a1) ->
467 internal_function -> 'a1 **)
468 let rec internal_function_rect_Type4 h_mk_internal_function x_15456 =
469 let { f_labgen = f_labgen0; f_reggen = f_reggen0; f_result = f_result0;
470 f_params = f_params0; f_locals = f_locals0; f_stacksize = f_stacksize0;
471 f_graph = f_graph0; f_entry = f_entry0; f_exit = f_exit0 } = x_15456
473 h_mk_internal_function f_labgen0 f_reggen0 f_result0 f_params0 f_locals0
474 f_stacksize0 f_graph0 __ __ f_entry0 f_exit0 __
476 (** val internal_function_rect_Type5 :
477 (Identifiers.universe -> Identifiers.universe -> (Registers.register,
478 AST.typ) Types.prod Types.option -> (Registers.register, AST.typ)
479 Types.prod List.list -> (Registers.register, AST.typ) Types.prod
480 List.list -> Nat.nat -> statement Graphs.graph -> __ -> __ ->
481 Graphs.label Types.sig0 -> Graphs.label Types.sig0 -> __ -> 'a1) ->
482 internal_function -> 'a1 **)
483 let rec internal_function_rect_Type5 h_mk_internal_function x_15458 =
484 let { f_labgen = f_labgen0; f_reggen = f_reggen0; f_result = f_result0;
485 f_params = f_params0; f_locals = f_locals0; f_stacksize = f_stacksize0;
486 f_graph = f_graph0; f_entry = f_entry0; f_exit = f_exit0 } = x_15458
488 h_mk_internal_function f_labgen0 f_reggen0 f_result0 f_params0 f_locals0
489 f_stacksize0 f_graph0 __ __ f_entry0 f_exit0 __
491 (** val internal_function_rect_Type3 :
492 (Identifiers.universe -> Identifiers.universe -> (Registers.register,
493 AST.typ) Types.prod Types.option -> (Registers.register, AST.typ)
494 Types.prod List.list -> (Registers.register, AST.typ) Types.prod
495 List.list -> Nat.nat -> statement Graphs.graph -> __ -> __ ->
496 Graphs.label Types.sig0 -> Graphs.label Types.sig0 -> __ -> 'a1) ->
497 internal_function -> 'a1 **)
498 let rec internal_function_rect_Type3 h_mk_internal_function x_15460 =
499 let { f_labgen = f_labgen0; f_reggen = f_reggen0; f_result = f_result0;
500 f_params = f_params0; f_locals = f_locals0; f_stacksize = f_stacksize0;
501 f_graph = f_graph0; f_entry = f_entry0; f_exit = f_exit0 } = x_15460
503 h_mk_internal_function f_labgen0 f_reggen0 f_result0 f_params0 f_locals0
504 f_stacksize0 f_graph0 __ __ f_entry0 f_exit0 __
506 (** val internal_function_rect_Type2 :
507 (Identifiers.universe -> Identifiers.universe -> (Registers.register,
508 AST.typ) Types.prod Types.option -> (Registers.register, AST.typ)
509 Types.prod List.list -> (Registers.register, AST.typ) Types.prod
510 List.list -> Nat.nat -> statement Graphs.graph -> __ -> __ ->
511 Graphs.label Types.sig0 -> Graphs.label Types.sig0 -> __ -> 'a1) ->
512 internal_function -> 'a1 **)
513 let rec internal_function_rect_Type2 h_mk_internal_function x_15462 =
514 let { f_labgen = f_labgen0; f_reggen = f_reggen0; f_result = f_result0;
515 f_params = f_params0; f_locals = f_locals0; f_stacksize = f_stacksize0;
516 f_graph = f_graph0; f_entry = f_entry0; f_exit = f_exit0 } = x_15462
518 h_mk_internal_function f_labgen0 f_reggen0 f_result0 f_params0 f_locals0
519 f_stacksize0 f_graph0 __ __ f_entry0 f_exit0 __
521 (** val internal_function_rect_Type1 :
522 (Identifiers.universe -> Identifiers.universe -> (Registers.register,
523 AST.typ) Types.prod Types.option -> (Registers.register, AST.typ)
524 Types.prod List.list -> (Registers.register, AST.typ) Types.prod
525 List.list -> Nat.nat -> statement Graphs.graph -> __ -> __ ->
526 Graphs.label Types.sig0 -> Graphs.label Types.sig0 -> __ -> 'a1) ->
527 internal_function -> 'a1 **)
528 let rec internal_function_rect_Type1 h_mk_internal_function x_15464 =
529 let { f_labgen = f_labgen0; f_reggen = f_reggen0; f_result = f_result0;
530 f_params = f_params0; f_locals = f_locals0; f_stacksize = f_stacksize0;
531 f_graph = f_graph0; f_entry = f_entry0; f_exit = f_exit0 } = x_15464
533 h_mk_internal_function f_labgen0 f_reggen0 f_result0 f_params0 f_locals0
534 f_stacksize0 f_graph0 __ __ f_entry0 f_exit0 __
536 (** val internal_function_rect_Type0 :
537 (Identifiers.universe -> Identifiers.universe -> (Registers.register,
538 AST.typ) Types.prod Types.option -> (Registers.register, AST.typ)
539 Types.prod List.list -> (Registers.register, AST.typ) Types.prod
540 List.list -> Nat.nat -> statement Graphs.graph -> __ -> __ ->
541 Graphs.label Types.sig0 -> Graphs.label Types.sig0 -> __ -> 'a1) ->
542 internal_function -> 'a1 **)
543 let rec internal_function_rect_Type0 h_mk_internal_function x_15466 =
544 let { f_labgen = f_labgen0; f_reggen = f_reggen0; f_result = f_result0;
545 f_params = f_params0; f_locals = f_locals0; f_stacksize = f_stacksize0;
546 f_graph = f_graph0; f_entry = f_entry0; f_exit = f_exit0 } = x_15466
548 h_mk_internal_function f_labgen0 f_reggen0 f_result0 f_params0 f_locals0
549 f_stacksize0 f_graph0 __ __ f_entry0 f_exit0 __
551 (** val f_labgen : internal_function -> Identifiers.universe **)
552 let rec f_labgen xxx =
555 (** val f_reggen : internal_function -> Identifiers.universe **)
556 let rec f_reggen xxx =
560 internal_function -> (Registers.register, AST.typ) Types.prod
562 let rec f_result xxx =
566 internal_function -> (Registers.register, AST.typ) Types.prod List.list **)
567 let rec f_params xxx =
571 internal_function -> (Registers.register, AST.typ) Types.prod List.list **)
572 let rec f_locals xxx =
575 (** val f_stacksize : internal_function -> Nat.nat **)
576 let rec f_stacksize xxx =
579 (** val f_graph : internal_function -> statement Graphs.graph **)
580 let rec f_graph xxx =
583 (** val f_entry : internal_function -> Graphs.label Types.sig0 **)
584 let rec f_entry xxx =
587 (** val f_exit : internal_function -> Graphs.label Types.sig0 **)
591 (** val internal_function_inv_rect_Type4 :
592 internal_function -> (Identifiers.universe -> Identifiers.universe ->
593 (Registers.register, AST.typ) Types.prod Types.option ->
594 (Registers.register, AST.typ) Types.prod List.list ->
595 (Registers.register, AST.typ) Types.prod List.list -> Nat.nat ->
596 statement Graphs.graph -> __ -> __ -> Graphs.label Types.sig0 ->
597 Graphs.label Types.sig0 -> __ -> __ -> 'a1) -> 'a1 **)
598 let internal_function_inv_rect_Type4 hterm h1 =
599 let hcut = internal_function_rect_Type4 h1 hterm in hcut __
601 (** val internal_function_inv_rect_Type3 :
602 internal_function -> (Identifiers.universe -> Identifiers.universe ->
603 (Registers.register, AST.typ) Types.prod Types.option ->
604 (Registers.register, AST.typ) Types.prod List.list ->
605 (Registers.register, AST.typ) Types.prod List.list -> Nat.nat ->
606 statement Graphs.graph -> __ -> __ -> Graphs.label Types.sig0 ->
607 Graphs.label Types.sig0 -> __ -> __ -> 'a1) -> 'a1 **)
608 let internal_function_inv_rect_Type3 hterm h1 =
609 let hcut = internal_function_rect_Type3 h1 hterm in hcut __
611 (** val internal_function_inv_rect_Type2 :
612 internal_function -> (Identifiers.universe -> Identifiers.universe ->
613 (Registers.register, AST.typ) Types.prod Types.option ->
614 (Registers.register, AST.typ) Types.prod List.list ->
615 (Registers.register, AST.typ) Types.prod List.list -> Nat.nat ->
616 statement Graphs.graph -> __ -> __ -> Graphs.label Types.sig0 ->
617 Graphs.label Types.sig0 -> __ -> __ -> 'a1) -> 'a1 **)
618 let internal_function_inv_rect_Type2 hterm h1 =
619 let hcut = internal_function_rect_Type2 h1 hterm in hcut __
621 (** val internal_function_inv_rect_Type1 :
622 internal_function -> (Identifiers.universe -> Identifiers.universe ->
623 (Registers.register, AST.typ) Types.prod Types.option ->
624 (Registers.register, AST.typ) Types.prod List.list ->
625 (Registers.register, AST.typ) Types.prod List.list -> Nat.nat ->
626 statement Graphs.graph -> __ -> __ -> Graphs.label Types.sig0 ->
627 Graphs.label Types.sig0 -> __ -> __ -> 'a1) -> 'a1 **)
628 let internal_function_inv_rect_Type1 hterm h1 =
629 let hcut = internal_function_rect_Type1 h1 hterm in hcut __
631 (** val internal_function_inv_rect_Type0 :
632 internal_function -> (Identifiers.universe -> Identifiers.universe ->
633 (Registers.register, AST.typ) Types.prod Types.option ->
634 (Registers.register, AST.typ) Types.prod List.list ->
635 (Registers.register, AST.typ) Types.prod List.list -> Nat.nat ->
636 statement Graphs.graph -> __ -> __ -> Graphs.label Types.sig0 ->
637 Graphs.label Types.sig0 -> __ -> __ -> 'a1) -> 'a1 **)
638 let internal_function_inv_rect_Type0 hterm h1 =
639 let hcut = internal_function_rect_Type0 h1 hterm in hcut __
641 (** val internal_function_jmdiscr :
642 internal_function -> internal_function -> __ **)
643 let internal_function_jmdiscr x y =
644 Logic.eq_rect_Type2 x
645 (let { f_labgen = a0; f_reggen = a1; f_result = a2; f_params = a3;
646 f_locals = a4; f_stacksize = a5; f_graph = a6; f_entry = a9; f_exit =
649 Obj.magic (fun _ dH -> dH __ __ __ __ __ __ __ __ __ __ __ __)) y
651 type rTLabs_program =
652 (internal_function AST.fundef, AST.init_data List.list) AST.program