99 open Hints_declaration
142 (** val keyword_rect_Type4 :
143 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1
144 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> keyword -> 'a1 **)
145 let rec keyword_rect_Type4 h_kwCOMMENT h_kwMOVE h_kwPOP h_kwPUSH h_kwADDRESS h_kwOPACCS h_kwOP1 h_kwOP2 h_kwCLEAR_CARRY h_kwSET_CARRY h_kwLOAD h_kwSTORE h_kwCOST_LABEL h_kwCOND h_kwCALL h_kwGOTO h_kwRETURN h_kwTAILCALL h_kwFCOND = function
146 | KwCOMMENT -> h_kwCOMMENT
150 | KwADDRESS -> h_kwADDRESS
151 | KwOPACCS -> h_kwOPACCS
154 | KwCLEAR_CARRY -> h_kwCLEAR_CARRY
155 | KwSET_CARRY -> h_kwSET_CARRY
157 | KwSTORE -> h_kwSTORE
158 | KwCOST_LABEL -> h_kwCOST_LABEL
162 | KwRETURN -> h_kwRETURN
163 | KwTAILCALL -> h_kwTAILCALL
164 | KwFCOND -> h_kwFCOND
166 (** val keyword_rect_Type5 :
167 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1
168 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> keyword -> 'a1 **)
169 let rec keyword_rect_Type5 h_kwCOMMENT h_kwMOVE h_kwPOP h_kwPUSH h_kwADDRESS h_kwOPACCS h_kwOP1 h_kwOP2 h_kwCLEAR_CARRY h_kwSET_CARRY h_kwLOAD h_kwSTORE h_kwCOST_LABEL h_kwCOND h_kwCALL h_kwGOTO h_kwRETURN h_kwTAILCALL h_kwFCOND = function
170 | KwCOMMENT -> h_kwCOMMENT
174 | KwADDRESS -> h_kwADDRESS
175 | KwOPACCS -> h_kwOPACCS
178 | KwCLEAR_CARRY -> h_kwCLEAR_CARRY
179 | KwSET_CARRY -> h_kwSET_CARRY
181 | KwSTORE -> h_kwSTORE
182 | KwCOST_LABEL -> h_kwCOST_LABEL
186 | KwRETURN -> h_kwRETURN
187 | KwTAILCALL -> h_kwTAILCALL
188 | KwFCOND -> h_kwFCOND
190 (** val keyword_rect_Type3 :
191 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1
192 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> keyword -> 'a1 **)
193 let rec keyword_rect_Type3 h_kwCOMMENT h_kwMOVE h_kwPOP h_kwPUSH h_kwADDRESS h_kwOPACCS h_kwOP1 h_kwOP2 h_kwCLEAR_CARRY h_kwSET_CARRY h_kwLOAD h_kwSTORE h_kwCOST_LABEL h_kwCOND h_kwCALL h_kwGOTO h_kwRETURN h_kwTAILCALL h_kwFCOND = function
194 | KwCOMMENT -> h_kwCOMMENT
198 | KwADDRESS -> h_kwADDRESS
199 | KwOPACCS -> h_kwOPACCS
202 | KwCLEAR_CARRY -> h_kwCLEAR_CARRY
203 | KwSET_CARRY -> h_kwSET_CARRY
205 | KwSTORE -> h_kwSTORE
206 | KwCOST_LABEL -> h_kwCOST_LABEL
210 | KwRETURN -> h_kwRETURN
211 | KwTAILCALL -> h_kwTAILCALL
212 | KwFCOND -> h_kwFCOND
214 (** val keyword_rect_Type2 :
215 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1
216 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> keyword -> 'a1 **)
217 let rec keyword_rect_Type2 h_kwCOMMENT h_kwMOVE h_kwPOP h_kwPUSH h_kwADDRESS h_kwOPACCS h_kwOP1 h_kwOP2 h_kwCLEAR_CARRY h_kwSET_CARRY h_kwLOAD h_kwSTORE h_kwCOST_LABEL h_kwCOND h_kwCALL h_kwGOTO h_kwRETURN h_kwTAILCALL h_kwFCOND = function
218 | KwCOMMENT -> h_kwCOMMENT
222 | KwADDRESS -> h_kwADDRESS
223 | KwOPACCS -> h_kwOPACCS
226 | KwCLEAR_CARRY -> h_kwCLEAR_CARRY
227 | KwSET_CARRY -> h_kwSET_CARRY
229 | KwSTORE -> h_kwSTORE
230 | KwCOST_LABEL -> h_kwCOST_LABEL
234 | KwRETURN -> h_kwRETURN
235 | KwTAILCALL -> h_kwTAILCALL
236 | KwFCOND -> h_kwFCOND
238 (** val keyword_rect_Type1 :
239 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1
240 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> keyword -> 'a1 **)
241 let rec keyword_rect_Type1 h_kwCOMMENT h_kwMOVE h_kwPOP h_kwPUSH h_kwADDRESS h_kwOPACCS h_kwOP1 h_kwOP2 h_kwCLEAR_CARRY h_kwSET_CARRY h_kwLOAD h_kwSTORE h_kwCOST_LABEL h_kwCOND h_kwCALL h_kwGOTO h_kwRETURN h_kwTAILCALL h_kwFCOND = function
242 | KwCOMMENT -> h_kwCOMMENT
246 | KwADDRESS -> h_kwADDRESS
247 | KwOPACCS -> h_kwOPACCS
250 | KwCLEAR_CARRY -> h_kwCLEAR_CARRY
251 | KwSET_CARRY -> h_kwSET_CARRY
253 | KwSTORE -> h_kwSTORE
254 | KwCOST_LABEL -> h_kwCOST_LABEL
258 | KwRETURN -> h_kwRETURN
259 | KwTAILCALL -> h_kwTAILCALL
260 | KwFCOND -> h_kwFCOND
262 (** val keyword_rect_Type0 :
263 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1
264 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> keyword -> 'a1 **)
265 let rec keyword_rect_Type0 h_kwCOMMENT h_kwMOVE h_kwPOP h_kwPUSH h_kwADDRESS h_kwOPACCS h_kwOP1 h_kwOP2 h_kwCLEAR_CARRY h_kwSET_CARRY h_kwLOAD h_kwSTORE h_kwCOST_LABEL h_kwCOND h_kwCALL h_kwGOTO h_kwRETURN h_kwTAILCALL h_kwFCOND = function
266 | KwCOMMENT -> h_kwCOMMENT
270 | KwADDRESS -> h_kwADDRESS
271 | KwOPACCS -> h_kwOPACCS
274 | KwCLEAR_CARRY -> h_kwCLEAR_CARRY
275 | KwSET_CARRY -> h_kwSET_CARRY
277 | KwSTORE -> h_kwSTORE
278 | KwCOST_LABEL -> h_kwCOST_LABEL
282 | KwRETURN -> h_kwRETURN
283 | KwTAILCALL -> h_kwTAILCALL
284 | KwFCOND -> h_kwFCOND
286 (** val keyword_inv_rect_Type4 :
287 keyword -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) ->
288 (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1)
289 -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ ->
290 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__
292 let keyword_inv_rect_Type4 hterm h1 h2 h3 h4 h5 h6 h7 h8 h9 h10 h11 h12 h13 h14 h15 h16 h17 h18 h19 =
294 keyword_rect_Type4 h1 h2 h3 h4 h5 h6 h7 h8 h9 h10 h11 h12 h13 h14 h15 h16
299 (** val keyword_inv_rect_Type3 :
300 keyword -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) ->
301 (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1)
302 -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ ->
303 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__
305 let keyword_inv_rect_Type3 hterm h1 h2 h3 h4 h5 h6 h7 h8 h9 h10 h11 h12 h13 h14 h15 h16 h17 h18 h19 =
307 keyword_rect_Type3 h1 h2 h3 h4 h5 h6 h7 h8 h9 h10 h11 h12 h13 h14 h15 h16
312 (** val keyword_inv_rect_Type2 :
313 keyword -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) ->
314 (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1)
315 -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ ->
316 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__
318 let keyword_inv_rect_Type2 hterm h1 h2 h3 h4 h5 h6 h7 h8 h9 h10 h11 h12 h13 h14 h15 h16 h17 h18 h19 =
320 keyword_rect_Type2 h1 h2 h3 h4 h5 h6 h7 h8 h9 h10 h11 h12 h13 h14 h15 h16
325 (** val keyword_inv_rect_Type1 :
326 keyword -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) ->
327 (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1)
328 -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ ->
329 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__
331 let keyword_inv_rect_Type1 hterm h1 h2 h3 h4 h5 h6 h7 h8 h9 h10 h11 h12 h13 h14 h15 h16 h17 h18 h19 =
333 keyword_rect_Type1 h1 h2 h3 h4 h5 h6 h7 h8 h9 h10 h11 h12 h13 h14 h15 h16
338 (** val keyword_inv_rect_Type0 :
339 keyword -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) ->
340 (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1)
341 -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ ->
342 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__
344 let keyword_inv_rect_Type0 hterm h1 h2 h3 h4 h5 h6 h7 h8 h9 h10 h11 h12 h13 h14 h15 h16 h17 h18 h19 =
346 keyword_rect_Type0 h1 h2 h3 h4 h5 h6 h7 h8 h9 h10 h11 h12 h13 h14 h15 h16
351 (** val keyword_discr : keyword -> keyword -> __ **)
352 let keyword_discr x y =
353 Logic.eq_rect_Type2 x
355 | KwCOMMENT -> Obj.magic (fun _ dH -> dH)
356 | KwMOVE -> Obj.magic (fun _ dH -> dH)
357 | KwPOP -> Obj.magic (fun _ dH -> dH)
358 | KwPUSH -> Obj.magic (fun _ dH -> dH)
359 | KwADDRESS -> Obj.magic (fun _ dH -> dH)
360 | KwOPACCS -> Obj.magic (fun _ dH -> dH)
361 | KwOP1 -> Obj.magic (fun _ dH -> dH)
362 | KwOP2 -> Obj.magic (fun _ dH -> dH)
363 | KwCLEAR_CARRY -> Obj.magic (fun _ dH -> dH)
364 | KwSET_CARRY -> Obj.magic (fun _ dH -> dH)
365 | KwLOAD -> Obj.magic (fun _ dH -> dH)
366 | KwSTORE -> Obj.magic (fun _ dH -> dH)
367 | KwCOST_LABEL -> Obj.magic (fun _ dH -> dH)
368 | KwCOND -> Obj.magic (fun _ dH -> dH)
369 | KwCALL -> Obj.magic (fun _ dH -> dH)
370 | KwGOTO -> Obj.magic (fun _ dH -> dH)
371 | KwRETURN -> Obj.magic (fun _ dH -> dH)
372 | KwTAILCALL -> Obj.magic (fun _ dH -> dH)
373 | KwFCOND -> Obj.magic (fun _ dH -> dH)) y
375 (** val keyword_jmdiscr : keyword -> keyword -> __ **)
376 let keyword_jmdiscr x y =
377 Logic.eq_rect_Type2 x
379 | KwCOMMENT -> Obj.magic (fun _ dH -> dH)
380 | KwMOVE -> Obj.magic (fun _ dH -> dH)
381 | KwPOP -> Obj.magic (fun _ dH -> dH)
382 | KwPUSH -> Obj.magic (fun _ dH -> dH)
383 | KwADDRESS -> Obj.magic (fun _ dH -> dH)
384 | KwOPACCS -> Obj.magic (fun _ dH -> dH)
385 | KwOP1 -> Obj.magic (fun _ dH -> dH)
386 | KwOP2 -> Obj.magic (fun _ dH -> dH)
387 | KwCLEAR_CARRY -> Obj.magic (fun _ dH -> dH)
388 | KwSET_CARRY -> Obj.magic (fun _ dH -> dH)
389 | KwLOAD -> Obj.magic (fun _ dH -> dH)
390 | KwSTORE -> Obj.magic (fun _ dH -> dH)
391 | KwCOST_LABEL -> Obj.magic (fun _ dH -> dH)
392 | KwCOND -> Obj.magic (fun _ dH -> dH)
393 | KwCALL -> Obj.magic (fun _ dH -> dH)
394 | KwGOTO -> Obj.magic (fun _ dH -> dH)
395 | KwRETURN -> Obj.magic (fun _ dH -> dH)
396 | KwTAILCALL -> Obj.magic (fun _ dH -> dH)
397 | KwFCOND -> Obj.magic (fun _ dH -> dH)) y
399 type 'string printing_pass_independent_params = { print_String : (String.string
401 print_keyword : (keyword ->
403 print_concat : ('string ->
406 print_empty : 'string;
407 print_ident : (AST.ident ->
409 print_costlabel : (CostLabel.costlabel
412 print_label : (Graphs.label
414 print_OpAccs : (BackEndOps.opAccs
416 print_Op1 : (BackEndOps.op1
418 print_Op2 : (BackEndOps.op2
420 print_nat : (Nat.nat ->
422 print_bitvector : (Nat.nat
428 (** val printing_pass_independent_params_rect_Type4 :
429 ((String.string -> 'a1) -> (keyword -> 'a1) -> ('a1 -> 'a1 -> 'a1) -> 'a1
430 -> (AST.ident -> 'a1) -> (CostLabel.costlabel -> 'a1) -> (Graphs.label ->
431 'a1) -> (BackEndOps.opAccs -> 'a1) -> (BackEndOps.op1 -> 'a1) ->
432 (BackEndOps.op2 -> 'a1) -> (Nat.nat -> 'a1) -> (Nat.nat ->
433 BitVector.bitVector -> 'a1) -> 'a2) -> 'a1
434 printing_pass_independent_params -> 'a2 **)
435 let rec printing_pass_independent_params_rect_Type4 h_mk_printing_pass_independent_params x_25506 =
436 let { print_String = print_String0; print_keyword = print_keyword0;
437 print_concat = print_concat0; print_empty = print_empty0; print_ident =
438 print_ident0; print_costlabel = print_costlabel0; print_label =
439 print_label0; print_OpAccs = print_OpAccs0; print_Op1 = print_Op3;
440 print_Op2 = print_Op4; print_nat = print_nat0; print_bitvector =
441 print_bitvector0 } = x_25506
443 h_mk_printing_pass_independent_params print_String0 print_keyword0
444 print_concat0 print_empty0 print_ident0 print_costlabel0 print_label0
445 print_OpAccs0 print_Op3 print_Op4 print_nat0 print_bitvector0
447 (** val printing_pass_independent_params_rect_Type5 :
448 ((String.string -> 'a1) -> (keyword -> 'a1) -> ('a1 -> 'a1 -> 'a1) -> 'a1
449 -> (AST.ident -> 'a1) -> (CostLabel.costlabel -> 'a1) -> (Graphs.label ->
450 'a1) -> (BackEndOps.opAccs -> 'a1) -> (BackEndOps.op1 -> 'a1) ->
451 (BackEndOps.op2 -> 'a1) -> (Nat.nat -> 'a1) -> (Nat.nat ->
452 BitVector.bitVector -> 'a1) -> 'a2) -> 'a1
453 printing_pass_independent_params -> 'a2 **)
454 let rec printing_pass_independent_params_rect_Type5 h_mk_printing_pass_independent_params x_25508 =
455 let { print_String = print_String0; print_keyword = print_keyword0;
456 print_concat = print_concat0; print_empty = print_empty0; print_ident =
457 print_ident0; print_costlabel = print_costlabel0; print_label =
458 print_label0; print_OpAccs = print_OpAccs0; print_Op1 = print_Op3;
459 print_Op2 = print_Op4; print_nat = print_nat0; print_bitvector =
460 print_bitvector0 } = x_25508
462 h_mk_printing_pass_independent_params print_String0 print_keyword0
463 print_concat0 print_empty0 print_ident0 print_costlabel0 print_label0
464 print_OpAccs0 print_Op3 print_Op4 print_nat0 print_bitvector0
466 (** val printing_pass_independent_params_rect_Type3 :
467 ((String.string -> 'a1) -> (keyword -> 'a1) -> ('a1 -> 'a1 -> 'a1) -> 'a1
468 -> (AST.ident -> 'a1) -> (CostLabel.costlabel -> 'a1) -> (Graphs.label ->
469 'a1) -> (BackEndOps.opAccs -> 'a1) -> (BackEndOps.op1 -> 'a1) ->
470 (BackEndOps.op2 -> 'a1) -> (Nat.nat -> 'a1) -> (Nat.nat ->
471 BitVector.bitVector -> 'a1) -> 'a2) -> 'a1
472 printing_pass_independent_params -> 'a2 **)
473 let rec printing_pass_independent_params_rect_Type3 h_mk_printing_pass_independent_params x_25510 =
474 let { print_String = print_String0; print_keyword = print_keyword0;
475 print_concat = print_concat0; print_empty = print_empty0; print_ident =
476 print_ident0; print_costlabel = print_costlabel0; print_label =
477 print_label0; print_OpAccs = print_OpAccs0; print_Op1 = print_Op3;
478 print_Op2 = print_Op4; print_nat = print_nat0; print_bitvector =
479 print_bitvector0 } = x_25510
481 h_mk_printing_pass_independent_params print_String0 print_keyword0
482 print_concat0 print_empty0 print_ident0 print_costlabel0 print_label0
483 print_OpAccs0 print_Op3 print_Op4 print_nat0 print_bitvector0
485 (** val printing_pass_independent_params_rect_Type2 :
486 ((String.string -> 'a1) -> (keyword -> 'a1) -> ('a1 -> 'a1 -> 'a1) -> 'a1
487 -> (AST.ident -> 'a1) -> (CostLabel.costlabel -> 'a1) -> (Graphs.label ->
488 'a1) -> (BackEndOps.opAccs -> 'a1) -> (BackEndOps.op1 -> 'a1) ->
489 (BackEndOps.op2 -> 'a1) -> (Nat.nat -> 'a1) -> (Nat.nat ->
490 BitVector.bitVector -> 'a1) -> 'a2) -> 'a1
491 printing_pass_independent_params -> 'a2 **)
492 let rec printing_pass_independent_params_rect_Type2 h_mk_printing_pass_independent_params x_25512 =
493 let { print_String = print_String0; print_keyword = print_keyword0;
494 print_concat = print_concat0; print_empty = print_empty0; print_ident =
495 print_ident0; print_costlabel = print_costlabel0; print_label =
496 print_label0; print_OpAccs = print_OpAccs0; print_Op1 = print_Op3;
497 print_Op2 = print_Op4; print_nat = print_nat0; print_bitvector =
498 print_bitvector0 } = x_25512
500 h_mk_printing_pass_independent_params print_String0 print_keyword0
501 print_concat0 print_empty0 print_ident0 print_costlabel0 print_label0
502 print_OpAccs0 print_Op3 print_Op4 print_nat0 print_bitvector0
504 (** val printing_pass_independent_params_rect_Type1 :
505 ((String.string -> 'a1) -> (keyword -> 'a1) -> ('a1 -> 'a1 -> 'a1) -> 'a1
506 -> (AST.ident -> 'a1) -> (CostLabel.costlabel -> 'a1) -> (Graphs.label ->
507 'a1) -> (BackEndOps.opAccs -> 'a1) -> (BackEndOps.op1 -> 'a1) ->
508 (BackEndOps.op2 -> 'a1) -> (Nat.nat -> 'a1) -> (Nat.nat ->
509 BitVector.bitVector -> 'a1) -> 'a2) -> 'a1
510 printing_pass_independent_params -> 'a2 **)
511 let rec printing_pass_independent_params_rect_Type1 h_mk_printing_pass_independent_params x_25514 =
512 let { print_String = print_String0; print_keyword = print_keyword0;
513 print_concat = print_concat0; print_empty = print_empty0; print_ident =
514 print_ident0; print_costlabel = print_costlabel0; print_label =
515 print_label0; print_OpAccs = print_OpAccs0; print_Op1 = print_Op3;
516 print_Op2 = print_Op4; print_nat = print_nat0; print_bitvector =
517 print_bitvector0 } = x_25514
519 h_mk_printing_pass_independent_params print_String0 print_keyword0
520 print_concat0 print_empty0 print_ident0 print_costlabel0 print_label0
521 print_OpAccs0 print_Op3 print_Op4 print_nat0 print_bitvector0
523 (** val printing_pass_independent_params_rect_Type0 :
524 ((String.string -> 'a1) -> (keyword -> 'a1) -> ('a1 -> 'a1 -> 'a1) -> 'a1
525 -> (AST.ident -> 'a1) -> (CostLabel.costlabel -> 'a1) -> (Graphs.label ->
526 'a1) -> (BackEndOps.opAccs -> 'a1) -> (BackEndOps.op1 -> 'a1) ->
527 (BackEndOps.op2 -> 'a1) -> (Nat.nat -> 'a1) -> (Nat.nat ->
528 BitVector.bitVector -> 'a1) -> 'a2) -> 'a1
529 printing_pass_independent_params -> 'a2 **)
530 let rec printing_pass_independent_params_rect_Type0 h_mk_printing_pass_independent_params x_25516 =
531 let { print_String = print_String0; print_keyword = print_keyword0;
532 print_concat = print_concat0; print_empty = print_empty0; print_ident =
533 print_ident0; print_costlabel = print_costlabel0; print_label =
534 print_label0; print_OpAccs = print_OpAccs0; print_Op1 = print_Op3;
535 print_Op2 = print_Op4; print_nat = print_nat0; print_bitvector =
536 print_bitvector0 } = x_25516
538 h_mk_printing_pass_independent_params print_String0 print_keyword0
539 print_concat0 print_empty0 print_ident0 print_costlabel0 print_label0
540 print_OpAccs0 print_Op3 print_Op4 print_nat0 print_bitvector0
542 (** val print_String :
543 'a1 printing_pass_independent_params -> String.string -> 'a1 **)
544 let rec print_String xxx =
547 (** val print_keyword :
548 'a1 printing_pass_independent_params -> keyword -> 'a1 **)
549 let rec print_keyword xxx =
552 (** val print_concat :
553 'a1 printing_pass_independent_params -> 'a1 -> 'a1 -> 'a1 **)
554 let rec print_concat xxx =
557 (** val print_empty : 'a1 printing_pass_independent_params -> 'a1 **)
558 let rec print_empty xxx =
561 (** val print_ident :
562 'a1 printing_pass_independent_params -> AST.ident -> 'a1 **)
563 let rec print_ident xxx =
566 (** val print_costlabel :
567 'a1 printing_pass_independent_params -> CostLabel.costlabel -> 'a1 **)
568 let rec print_costlabel xxx =
571 (** val print_label :
572 'a1 printing_pass_independent_params -> Graphs.label -> 'a1 **)
573 let rec print_label xxx =
576 (** val print_OpAccs :
577 'a1 printing_pass_independent_params -> BackEndOps.opAccs -> 'a1 **)
578 let rec print_OpAccs xxx =
582 'a1 printing_pass_independent_params -> BackEndOps.op1 -> 'a1 **)
583 let rec print_Op1 xxx =
587 'a1 printing_pass_independent_params -> BackEndOps.op2 -> 'a1 **)
588 let rec print_Op2 xxx =
592 'a1 printing_pass_independent_params -> Nat.nat -> 'a1 **)
593 let rec print_nat xxx =
596 (** val print_bitvector :
597 'a1 printing_pass_independent_params -> Nat.nat -> BitVector.bitVector ->
599 let rec print_bitvector xxx =
602 (** val printing_pass_independent_params_inv_rect_Type4 :
603 'a1 printing_pass_independent_params -> ((String.string -> 'a1) ->
604 (keyword -> 'a1) -> ('a1 -> 'a1 -> 'a1) -> 'a1 -> (AST.ident -> 'a1) ->
605 (CostLabel.costlabel -> 'a1) -> (Graphs.label -> 'a1) ->
606 (BackEndOps.opAccs -> 'a1) -> (BackEndOps.op1 -> 'a1) -> (BackEndOps.op2
607 -> 'a1) -> (Nat.nat -> 'a1) -> (Nat.nat -> BitVector.bitVector -> 'a1) ->
608 __ -> 'a2) -> 'a2 **)
609 let printing_pass_independent_params_inv_rect_Type4 hterm h1 =
610 let hcut = printing_pass_independent_params_rect_Type4 h1 hterm in hcut __
612 (** val printing_pass_independent_params_inv_rect_Type3 :
613 'a1 printing_pass_independent_params -> ((String.string -> 'a1) ->
614 (keyword -> 'a1) -> ('a1 -> 'a1 -> 'a1) -> 'a1 -> (AST.ident -> 'a1) ->
615 (CostLabel.costlabel -> 'a1) -> (Graphs.label -> 'a1) ->
616 (BackEndOps.opAccs -> 'a1) -> (BackEndOps.op1 -> 'a1) -> (BackEndOps.op2
617 -> 'a1) -> (Nat.nat -> 'a1) -> (Nat.nat -> BitVector.bitVector -> 'a1) ->
618 __ -> 'a2) -> 'a2 **)
619 let printing_pass_independent_params_inv_rect_Type3 hterm h1 =
620 let hcut = printing_pass_independent_params_rect_Type3 h1 hterm in hcut __
622 (** val printing_pass_independent_params_inv_rect_Type2 :
623 'a1 printing_pass_independent_params -> ((String.string -> 'a1) ->
624 (keyword -> 'a1) -> ('a1 -> 'a1 -> 'a1) -> 'a1 -> (AST.ident -> 'a1) ->
625 (CostLabel.costlabel -> 'a1) -> (Graphs.label -> 'a1) ->
626 (BackEndOps.opAccs -> 'a1) -> (BackEndOps.op1 -> 'a1) -> (BackEndOps.op2
627 -> 'a1) -> (Nat.nat -> 'a1) -> (Nat.nat -> BitVector.bitVector -> 'a1) ->
628 __ -> 'a2) -> 'a2 **)
629 let printing_pass_independent_params_inv_rect_Type2 hterm h1 =
630 let hcut = printing_pass_independent_params_rect_Type2 h1 hterm in hcut __
632 (** val printing_pass_independent_params_inv_rect_Type1 :
633 'a1 printing_pass_independent_params -> ((String.string -> 'a1) ->
634 (keyword -> 'a1) -> ('a1 -> 'a1 -> 'a1) -> 'a1 -> (AST.ident -> 'a1) ->
635 (CostLabel.costlabel -> 'a1) -> (Graphs.label -> 'a1) ->
636 (BackEndOps.opAccs -> 'a1) -> (BackEndOps.op1 -> 'a1) -> (BackEndOps.op2
637 -> 'a1) -> (Nat.nat -> 'a1) -> (Nat.nat -> BitVector.bitVector -> 'a1) ->
638 __ -> 'a2) -> 'a2 **)
639 let printing_pass_independent_params_inv_rect_Type1 hterm h1 =
640 let hcut = printing_pass_independent_params_rect_Type1 h1 hterm in hcut __
642 (** val printing_pass_independent_params_inv_rect_Type0 :
643 'a1 printing_pass_independent_params -> ((String.string -> 'a1) ->
644 (keyword -> 'a1) -> ('a1 -> 'a1 -> 'a1) -> 'a1 -> (AST.ident -> 'a1) ->
645 (CostLabel.costlabel -> 'a1) -> (Graphs.label -> 'a1) ->
646 (BackEndOps.opAccs -> 'a1) -> (BackEndOps.op1 -> 'a1) -> (BackEndOps.op2
647 -> 'a1) -> (Nat.nat -> 'a1) -> (Nat.nat -> BitVector.bitVector -> 'a1) ->
648 __ -> 'a2) -> 'a2 **)
649 let printing_pass_independent_params_inv_rect_Type0 hterm h1 =
650 let hcut = printing_pass_independent_params_rect_Type0 h1 hterm in hcut __
652 (** val printing_pass_independent_params_jmdiscr :
653 'a1 printing_pass_independent_params -> 'a1
654 printing_pass_independent_params -> __ **)
655 let printing_pass_independent_params_jmdiscr x y =
656 Logic.eq_rect_Type2 x
657 (let { print_String = a0; print_keyword = a10; print_concat = a2;
658 print_empty = a3; print_ident = a4; print_costlabel = a5;
659 print_label = a6; print_OpAccs = a7; print_Op1 = a8; print_Op2 = a9;
660 print_nat = a100; print_bitvector = a11 } = x
662 Obj.magic (fun _ dH -> dH __ __ __ __ __ __ __ __ __ __ __ __)) y
664 type 'string printing_params = { print_pass_ind : 'string
665 printing_pass_independent_params;
666 print_acc_a_reg : (__ -> 'string);
667 print_acc_b_reg : (__ -> 'string);
668 print_acc_a_arg : (__ -> 'string);
669 print_acc_b_arg : (__ -> 'string);
670 print_dpl_reg : (__ -> 'string);
671 print_dph_reg : (__ -> 'string);
672 print_dpl_arg : (__ -> 'string);
673 print_dph_arg : (__ -> 'string);
674 print_snd_arg : (__ -> 'string);
675 print_pair_move : (__ -> 'string);
676 print_call_args : (__ -> 'string);
677 print_call_dest : (__ -> 'string);
678 print_ext_seq : (__ -> 'string) }
680 (** val printing_params_rect_Type4 :
681 Joint.unserialized_params -> ('a1 printing_pass_independent_params -> (__
682 -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) ->
683 (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1)
684 -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> 'a2) -> 'a1
685 printing_params -> 'a2 **)
686 let rec printing_params_rect_Type4 p h_mk_printing_params x_25544 =
687 let { print_pass_ind = print_pass_ind0; print_acc_a_reg = print_acc_a_reg0;
688 print_acc_b_reg = print_acc_b_reg0; print_acc_a_arg = print_acc_a_arg0;
689 print_acc_b_arg = print_acc_b_arg0; print_dpl_reg = print_dpl_reg0;
690 print_dph_reg = print_dph_reg0; print_dpl_arg = print_dpl_arg0;
691 print_dph_arg = print_dph_arg0; print_snd_arg = print_snd_arg0;
692 print_pair_move = print_pair_move0; print_call_args = print_call_args0;
693 print_call_dest = print_call_dest0; print_ext_seq = print_ext_seq0 } =
696 h_mk_printing_params print_pass_ind0 print_acc_a_reg0 print_acc_b_reg0
697 print_acc_a_arg0 print_acc_b_arg0 print_dpl_reg0 print_dph_reg0
698 print_dpl_arg0 print_dph_arg0 print_snd_arg0 print_pair_move0
699 print_call_args0 print_call_dest0 print_ext_seq0
701 (** val printing_params_rect_Type5 :
702 Joint.unserialized_params -> ('a1 printing_pass_independent_params -> (__
703 -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) ->
704 (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1)
705 -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> 'a2) -> 'a1
706 printing_params -> 'a2 **)
707 let rec printing_params_rect_Type5 p h_mk_printing_params x_25546 =
708 let { print_pass_ind = print_pass_ind0; print_acc_a_reg = print_acc_a_reg0;
709 print_acc_b_reg = print_acc_b_reg0; print_acc_a_arg = print_acc_a_arg0;
710 print_acc_b_arg = print_acc_b_arg0; print_dpl_reg = print_dpl_reg0;
711 print_dph_reg = print_dph_reg0; print_dpl_arg = print_dpl_arg0;
712 print_dph_arg = print_dph_arg0; print_snd_arg = print_snd_arg0;
713 print_pair_move = print_pair_move0; print_call_args = print_call_args0;
714 print_call_dest = print_call_dest0; print_ext_seq = print_ext_seq0 } =
717 h_mk_printing_params print_pass_ind0 print_acc_a_reg0 print_acc_b_reg0
718 print_acc_a_arg0 print_acc_b_arg0 print_dpl_reg0 print_dph_reg0
719 print_dpl_arg0 print_dph_arg0 print_snd_arg0 print_pair_move0
720 print_call_args0 print_call_dest0 print_ext_seq0
722 (** val printing_params_rect_Type3 :
723 Joint.unserialized_params -> ('a1 printing_pass_independent_params -> (__
724 -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) ->
725 (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1)
726 -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> 'a2) -> 'a1
727 printing_params -> 'a2 **)
728 let rec printing_params_rect_Type3 p h_mk_printing_params x_25548 =
729 let { print_pass_ind = print_pass_ind0; print_acc_a_reg = print_acc_a_reg0;
730 print_acc_b_reg = print_acc_b_reg0; print_acc_a_arg = print_acc_a_arg0;
731 print_acc_b_arg = print_acc_b_arg0; print_dpl_reg = print_dpl_reg0;
732 print_dph_reg = print_dph_reg0; print_dpl_arg = print_dpl_arg0;
733 print_dph_arg = print_dph_arg0; print_snd_arg = print_snd_arg0;
734 print_pair_move = print_pair_move0; print_call_args = print_call_args0;
735 print_call_dest = print_call_dest0; print_ext_seq = print_ext_seq0 } =
738 h_mk_printing_params print_pass_ind0 print_acc_a_reg0 print_acc_b_reg0
739 print_acc_a_arg0 print_acc_b_arg0 print_dpl_reg0 print_dph_reg0
740 print_dpl_arg0 print_dph_arg0 print_snd_arg0 print_pair_move0
741 print_call_args0 print_call_dest0 print_ext_seq0
743 (** val printing_params_rect_Type2 :
744 Joint.unserialized_params -> ('a1 printing_pass_independent_params -> (__
745 -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) ->
746 (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1)
747 -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> 'a2) -> 'a1
748 printing_params -> 'a2 **)
749 let rec printing_params_rect_Type2 p h_mk_printing_params x_25550 =
750 let { print_pass_ind = print_pass_ind0; print_acc_a_reg = print_acc_a_reg0;
751 print_acc_b_reg = print_acc_b_reg0; print_acc_a_arg = print_acc_a_arg0;
752 print_acc_b_arg = print_acc_b_arg0; print_dpl_reg = print_dpl_reg0;
753 print_dph_reg = print_dph_reg0; print_dpl_arg = print_dpl_arg0;
754 print_dph_arg = print_dph_arg0; print_snd_arg = print_snd_arg0;
755 print_pair_move = print_pair_move0; print_call_args = print_call_args0;
756 print_call_dest = print_call_dest0; print_ext_seq = print_ext_seq0 } =
759 h_mk_printing_params print_pass_ind0 print_acc_a_reg0 print_acc_b_reg0
760 print_acc_a_arg0 print_acc_b_arg0 print_dpl_reg0 print_dph_reg0
761 print_dpl_arg0 print_dph_arg0 print_snd_arg0 print_pair_move0
762 print_call_args0 print_call_dest0 print_ext_seq0
764 (** val printing_params_rect_Type1 :
765 Joint.unserialized_params -> ('a1 printing_pass_independent_params -> (__
766 -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) ->
767 (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1)
768 -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> 'a2) -> 'a1
769 printing_params -> 'a2 **)
770 let rec printing_params_rect_Type1 p h_mk_printing_params x_25552 =
771 let { print_pass_ind = print_pass_ind0; print_acc_a_reg = print_acc_a_reg0;
772 print_acc_b_reg = print_acc_b_reg0; print_acc_a_arg = print_acc_a_arg0;
773 print_acc_b_arg = print_acc_b_arg0; print_dpl_reg = print_dpl_reg0;
774 print_dph_reg = print_dph_reg0; print_dpl_arg = print_dpl_arg0;
775 print_dph_arg = print_dph_arg0; print_snd_arg = print_snd_arg0;
776 print_pair_move = print_pair_move0; print_call_args = print_call_args0;
777 print_call_dest = print_call_dest0; print_ext_seq = print_ext_seq0 } =
780 h_mk_printing_params print_pass_ind0 print_acc_a_reg0 print_acc_b_reg0
781 print_acc_a_arg0 print_acc_b_arg0 print_dpl_reg0 print_dph_reg0
782 print_dpl_arg0 print_dph_arg0 print_snd_arg0 print_pair_move0
783 print_call_args0 print_call_dest0 print_ext_seq0
785 (** val printing_params_rect_Type0 :
786 Joint.unserialized_params -> ('a1 printing_pass_independent_params -> (__
787 -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) ->
788 (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1)
789 -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> 'a2) -> 'a1
790 printing_params -> 'a2 **)
791 let rec printing_params_rect_Type0 p h_mk_printing_params x_25554 =
792 let { print_pass_ind = print_pass_ind0; print_acc_a_reg = print_acc_a_reg0;
793 print_acc_b_reg = print_acc_b_reg0; print_acc_a_arg = print_acc_a_arg0;
794 print_acc_b_arg = print_acc_b_arg0; print_dpl_reg = print_dpl_reg0;
795 print_dph_reg = print_dph_reg0; print_dpl_arg = print_dpl_arg0;
796 print_dph_arg = print_dph_arg0; print_snd_arg = print_snd_arg0;
797 print_pair_move = print_pair_move0; print_call_args = print_call_args0;
798 print_call_dest = print_call_dest0; print_ext_seq = print_ext_seq0 } =
801 h_mk_printing_params print_pass_ind0 print_acc_a_reg0 print_acc_b_reg0
802 print_acc_a_arg0 print_acc_b_arg0 print_dpl_reg0 print_dph_reg0
803 print_dpl_arg0 print_dph_arg0 print_snd_arg0 print_pair_move0
804 print_call_args0 print_call_dest0 print_ext_seq0
806 (** val print_pass_ind :
807 Joint.unserialized_params -> 'a1 printing_params -> 'a1
808 printing_pass_independent_params **)
809 let rec print_pass_ind p xxx =
812 (** val print_acc_a_reg :
813 Joint.unserialized_params -> 'a1 printing_params -> __ -> 'a1 **)
814 let rec print_acc_a_reg p xxx =
817 (** val print_acc_b_reg :
818 Joint.unserialized_params -> 'a1 printing_params -> __ -> 'a1 **)
819 let rec print_acc_b_reg p xxx =
822 (** val print_acc_a_arg :
823 Joint.unserialized_params -> 'a1 printing_params -> __ -> 'a1 **)
824 let rec print_acc_a_arg p xxx =
827 (** val print_acc_b_arg :
828 Joint.unserialized_params -> 'a1 printing_params -> __ -> 'a1 **)
829 let rec print_acc_b_arg p xxx =
832 (** val print_dpl_reg :
833 Joint.unserialized_params -> 'a1 printing_params -> __ -> 'a1 **)
834 let rec print_dpl_reg p xxx =
837 (** val print_dph_reg :
838 Joint.unserialized_params -> 'a1 printing_params -> __ -> 'a1 **)
839 let rec print_dph_reg p xxx =
842 (** val print_dpl_arg :
843 Joint.unserialized_params -> 'a1 printing_params -> __ -> 'a1 **)
844 let rec print_dpl_arg p xxx =
847 (** val print_dph_arg :
848 Joint.unserialized_params -> 'a1 printing_params -> __ -> 'a1 **)
849 let rec print_dph_arg p xxx =
852 (** val print_snd_arg :
853 Joint.unserialized_params -> 'a1 printing_params -> __ -> 'a1 **)
854 let rec print_snd_arg p xxx =
857 (** val print_pair_move :
858 Joint.unserialized_params -> 'a1 printing_params -> __ -> 'a1 **)
859 let rec print_pair_move p xxx =
862 (** val print_call_args :
863 Joint.unserialized_params -> 'a1 printing_params -> __ -> 'a1 **)
864 let rec print_call_args p xxx =
867 (** val print_call_dest :
868 Joint.unserialized_params -> 'a1 printing_params -> __ -> 'a1 **)
869 let rec print_call_dest p xxx =
872 (** val print_ext_seq :
873 Joint.unserialized_params -> 'a1 printing_params -> __ -> 'a1 **)
874 let rec print_ext_seq p xxx =
877 (** val printing_params_inv_rect_Type4 :
878 Joint.unserialized_params -> 'a1 printing_params -> ('a1
879 printing_pass_independent_params -> (__ -> 'a1) -> (__ -> 'a1) -> (__ ->
880 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__
881 -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) ->
882 (__ -> 'a1) -> __ -> 'a2) -> 'a2 **)
883 let printing_params_inv_rect_Type4 x2 hterm h1 =
884 let hcut = printing_params_rect_Type4 x2 h1 hterm in hcut __
886 (** val printing_params_inv_rect_Type3 :
887 Joint.unserialized_params -> 'a1 printing_params -> ('a1
888 printing_pass_independent_params -> (__ -> 'a1) -> (__ -> 'a1) -> (__ ->
889 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__
890 -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) ->
891 (__ -> 'a1) -> __ -> 'a2) -> 'a2 **)
892 let printing_params_inv_rect_Type3 x2 hterm h1 =
893 let hcut = printing_params_rect_Type3 x2 h1 hterm in hcut __
895 (** val printing_params_inv_rect_Type2 :
896 Joint.unserialized_params -> 'a1 printing_params -> ('a1
897 printing_pass_independent_params -> (__ -> 'a1) -> (__ -> 'a1) -> (__ ->
898 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__
899 -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) ->
900 (__ -> 'a1) -> __ -> 'a2) -> 'a2 **)
901 let printing_params_inv_rect_Type2 x2 hterm h1 =
902 let hcut = printing_params_rect_Type2 x2 h1 hterm in hcut __
904 (** val printing_params_inv_rect_Type1 :
905 Joint.unserialized_params -> 'a1 printing_params -> ('a1
906 printing_pass_independent_params -> (__ -> 'a1) -> (__ -> 'a1) -> (__ ->
907 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__
908 -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) ->
909 (__ -> 'a1) -> __ -> 'a2) -> 'a2 **)
910 let printing_params_inv_rect_Type1 x2 hterm h1 =
911 let hcut = printing_params_rect_Type1 x2 h1 hterm in hcut __
913 (** val printing_params_inv_rect_Type0 :
914 Joint.unserialized_params -> 'a1 printing_params -> ('a1
915 printing_pass_independent_params -> (__ -> 'a1) -> (__ -> 'a1) -> (__ ->
916 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__
917 -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) ->
918 (__ -> 'a1) -> __ -> 'a2) -> 'a2 **)
919 let printing_params_inv_rect_Type0 x2 hterm h1 =
920 let hcut = printing_params_rect_Type0 x2 h1 hterm in hcut __
922 (** val printing_params_jmdiscr :
923 Joint.unserialized_params -> 'a1 printing_params -> 'a1 printing_params
925 let printing_params_jmdiscr a2 x y =
926 Logic.eq_rect_Type2 x
927 (let { print_pass_ind = a0; print_acc_a_reg = a10; print_acc_b_reg = a20;
928 print_acc_a_arg = a3; print_acc_b_arg = a4; print_dpl_reg = a5;
929 print_dph_reg = a6; print_dpl_arg = a7; print_dph_arg = a8;
930 print_snd_arg = a9; print_pair_move = a100; print_call_args = a11;
931 print_call_dest = a12; print_ext_seq = a13 } = x
933 Obj.magic (fun _ dH -> dH __ __ __ __ __ __ __ __ __ __ __ __ __ __)) y
935 (** val dpi1__o__print_pass_ind__o__inject :
936 Joint.unserialized_params -> ('a1 printing_params, 'a2) Types.dPair ->
937 'a1 printing_pass_independent_params Types.sig0 **)
938 let dpi1__o__print_pass_ind__o__inject x1 x4 =
939 x4.Types.dpi1.print_pass_ind
941 (** val eject__o__print_pass_ind__o__inject :
942 Joint.unserialized_params -> 'a1 printing_params Types.sig0 -> 'a1
943 printing_pass_independent_params Types.sig0 **)
944 let eject__o__print_pass_ind__o__inject x1 x4 =
945 (Types.pi1 x4).print_pass_ind
947 (** val print_pass_ind__o__inject :
948 Joint.unserialized_params -> 'a1 printing_params -> 'a1
949 printing_pass_independent_params Types.sig0 **)
950 let print_pass_ind__o__inject x1 x3 =
953 (** val dpi1__o__print_pass_ind :
954 Joint.unserialized_params -> ('a1 printing_params, 'a2) Types.dPair ->
955 'a1 printing_pass_independent_params **)
956 let dpi1__o__print_pass_ind x1 x3 =
957 x3.Types.dpi1.print_pass_ind
959 (** val eject__o__print_pass_ind :
960 Joint.unserialized_params -> 'a1 printing_params Types.sig0 -> 'a1
961 printing_pass_independent_params **)
962 let eject__o__print_pass_ind x1 x3 =
963 (Types.pi1 x3).print_pass_ind
965 type 'string print_serialization_params = { print_succ : (__ -> 'string);
966 print_code_point : (__ ->
969 (** val print_serialization_params_rect_Type4 :
970 Joint.params -> ((__ -> 'a1) -> (__ -> 'a1) -> 'a2) -> 'a1
971 print_serialization_params -> 'a2 **)
972 let rec print_serialization_params_rect_Type4 p h_mk_print_serialization_params x_25583 =
973 let { print_succ = print_succ0; print_code_point = print_code_point0 } =
976 h_mk_print_serialization_params print_succ0 print_code_point0
978 (** val print_serialization_params_rect_Type5 :
979 Joint.params -> ((__ -> 'a1) -> (__ -> 'a1) -> 'a2) -> 'a1
980 print_serialization_params -> 'a2 **)
981 let rec print_serialization_params_rect_Type5 p h_mk_print_serialization_params x_25585 =
982 let { print_succ = print_succ0; print_code_point = print_code_point0 } =
985 h_mk_print_serialization_params print_succ0 print_code_point0
987 (** val print_serialization_params_rect_Type3 :
988 Joint.params -> ((__ -> 'a1) -> (__ -> 'a1) -> 'a2) -> 'a1
989 print_serialization_params -> 'a2 **)
990 let rec print_serialization_params_rect_Type3 p h_mk_print_serialization_params x_25587 =
991 let { print_succ = print_succ0; print_code_point = print_code_point0 } =
994 h_mk_print_serialization_params print_succ0 print_code_point0
996 (** val print_serialization_params_rect_Type2 :
997 Joint.params -> ((__ -> 'a1) -> (__ -> 'a1) -> 'a2) -> 'a1
998 print_serialization_params -> 'a2 **)
999 let rec print_serialization_params_rect_Type2 p h_mk_print_serialization_params x_25589 =
1000 let { print_succ = print_succ0; print_code_point = print_code_point0 } =
1003 h_mk_print_serialization_params print_succ0 print_code_point0
1005 (** val print_serialization_params_rect_Type1 :
1006 Joint.params -> ((__ -> 'a1) -> (__ -> 'a1) -> 'a2) -> 'a1
1007 print_serialization_params -> 'a2 **)
1008 let rec print_serialization_params_rect_Type1 p h_mk_print_serialization_params x_25591 =
1009 let { print_succ = print_succ0; print_code_point = print_code_point0 } =
1012 h_mk_print_serialization_params print_succ0 print_code_point0
1014 (** val print_serialization_params_rect_Type0 :
1015 Joint.params -> ((__ -> 'a1) -> (__ -> 'a1) -> 'a2) -> 'a1
1016 print_serialization_params -> 'a2 **)
1017 let rec print_serialization_params_rect_Type0 p h_mk_print_serialization_params x_25593 =
1018 let { print_succ = print_succ0; print_code_point = print_code_point0 } =
1021 h_mk_print_serialization_params print_succ0 print_code_point0
1023 (** val print_succ :
1024 Joint.params -> 'a1 print_serialization_params -> __ -> 'a1 **)
1025 let rec print_succ p xxx =
1028 (** val print_code_point :
1029 Joint.params -> 'a1 print_serialization_params -> __ -> 'a1 **)
1030 let rec print_code_point p xxx =
1031 xxx.print_code_point
1033 (** val print_serialization_params_inv_rect_Type4 :
1034 Joint.params -> 'a1 print_serialization_params -> ((__ -> 'a1) -> (__ ->
1035 'a1) -> __ -> 'a2) -> 'a2 **)
1036 let print_serialization_params_inv_rect_Type4 x2 hterm h1 =
1037 let hcut = print_serialization_params_rect_Type4 x2 h1 hterm in hcut __
1039 (** val print_serialization_params_inv_rect_Type3 :
1040 Joint.params -> 'a1 print_serialization_params -> ((__ -> 'a1) -> (__ ->
1041 'a1) -> __ -> 'a2) -> 'a2 **)
1042 let print_serialization_params_inv_rect_Type3 x2 hterm h1 =
1043 let hcut = print_serialization_params_rect_Type3 x2 h1 hterm in hcut __
1045 (** val print_serialization_params_inv_rect_Type2 :
1046 Joint.params -> 'a1 print_serialization_params -> ((__ -> 'a1) -> (__ ->
1047 'a1) -> __ -> 'a2) -> 'a2 **)
1048 let print_serialization_params_inv_rect_Type2 x2 hterm h1 =
1049 let hcut = print_serialization_params_rect_Type2 x2 h1 hterm in hcut __
1051 (** val print_serialization_params_inv_rect_Type1 :
1052 Joint.params -> 'a1 print_serialization_params -> ((__ -> 'a1) -> (__ ->
1053 'a1) -> __ -> 'a2) -> 'a2 **)
1054 let print_serialization_params_inv_rect_Type1 x2 hterm h1 =
1055 let hcut = print_serialization_params_rect_Type1 x2 h1 hterm in hcut __
1057 (** val print_serialization_params_inv_rect_Type0 :
1058 Joint.params -> 'a1 print_serialization_params -> ((__ -> 'a1) -> (__ ->
1059 'a1) -> __ -> 'a2) -> 'a2 **)
1060 let print_serialization_params_inv_rect_Type0 x2 hterm h1 =
1061 let hcut = print_serialization_params_rect_Type0 x2 h1 hterm in hcut __
1063 (** val print_serialization_params_discr :
1064 Joint.params -> 'a1 print_serialization_params -> 'a1
1065 print_serialization_params -> __ **)
1066 let print_serialization_params_discr a2 x y =
1067 Logic.eq_rect_Type2 x
1068 (let { print_succ = a0; print_code_point = a10 } = x in
1069 Obj.magic (fun _ dH -> dH __ __)) y
1071 (** val print_serialization_params_jmdiscr :
1072 Joint.params -> 'a1 print_serialization_params -> 'a1
1073 print_serialization_params -> __ **)
1074 let print_serialization_params_jmdiscr a2 x y =
1075 Logic.eq_rect_Type2 x
1076 (let { print_succ = a0; print_code_point = a10 } = x in
1077 Obj.magic (fun _ dH -> dH __ __)) y
1079 type ('string, 'statementT) code_iteration_params = { cip_print_serialization_params :
1081 print_serialization_params;
1082 fold_code : (__ -> (__
1093 (** val code_iteration_params_rect_Type4 :
1094 Joint.params -> AST.ident List.list -> ('a1 print_serialization_params ->
1095 (__ -> (__ -> 'a2 -> __ -> __) -> __ -> __ -> __ -> __) -> ('a2 -> 'a1)
1096 -> 'a3) -> ('a1, 'a2) code_iteration_params -> 'a3 **)
1097 let rec code_iteration_params_rect_Type4 p globals h_mk_code_iteration_params x_25611 =
1098 let { cip_print_serialization_params = cip_print_serialization_params0;
1099 fold_code = fold_code0; print_statementT = print_statementT0 } = x_25611
1101 h_mk_code_iteration_params cip_print_serialization_params0 fold_code0
1104 (** val code_iteration_params_rect_Type5 :
1105 Joint.params -> AST.ident List.list -> ('a1 print_serialization_params ->
1106 (__ -> (__ -> 'a2 -> __ -> __) -> __ -> __ -> __ -> __) -> ('a2 -> 'a1)
1107 -> 'a3) -> ('a1, 'a2) code_iteration_params -> 'a3 **)
1108 let rec code_iteration_params_rect_Type5 p globals h_mk_code_iteration_params x_25613 =
1109 let { cip_print_serialization_params = cip_print_serialization_params0;
1110 fold_code = fold_code0; print_statementT = print_statementT0 } = x_25613
1112 h_mk_code_iteration_params cip_print_serialization_params0 fold_code0
1115 (** val code_iteration_params_rect_Type3 :
1116 Joint.params -> AST.ident List.list -> ('a1 print_serialization_params ->
1117 (__ -> (__ -> 'a2 -> __ -> __) -> __ -> __ -> __ -> __) -> ('a2 -> 'a1)
1118 -> 'a3) -> ('a1, 'a2) code_iteration_params -> 'a3 **)
1119 let rec code_iteration_params_rect_Type3 p globals h_mk_code_iteration_params x_25615 =
1120 let { cip_print_serialization_params = cip_print_serialization_params0;
1121 fold_code = fold_code0; print_statementT = print_statementT0 } = x_25615
1123 h_mk_code_iteration_params cip_print_serialization_params0 fold_code0
1126 (** val code_iteration_params_rect_Type2 :
1127 Joint.params -> AST.ident List.list -> ('a1 print_serialization_params ->
1128 (__ -> (__ -> 'a2 -> __ -> __) -> __ -> __ -> __ -> __) -> ('a2 -> 'a1)
1129 -> 'a3) -> ('a1, 'a2) code_iteration_params -> 'a3 **)
1130 let rec code_iteration_params_rect_Type2 p globals h_mk_code_iteration_params x_25617 =
1131 let { cip_print_serialization_params = cip_print_serialization_params0;
1132 fold_code = fold_code0; print_statementT = print_statementT0 } = x_25617
1134 h_mk_code_iteration_params cip_print_serialization_params0 fold_code0
1137 (** val code_iteration_params_rect_Type1 :
1138 Joint.params -> AST.ident List.list -> ('a1 print_serialization_params ->
1139 (__ -> (__ -> 'a2 -> __ -> __) -> __ -> __ -> __ -> __) -> ('a2 -> 'a1)
1140 -> 'a3) -> ('a1, 'a2) code_iteration_params -> 'a3 **)
1141 let rec code_iteration_params_rect_Type1 p globals h_mk_code_iteration_params x_25619 =
1142 let { cip_print_serialization_params = cip_print_serialization_params0;
1143 fold_code = fold_code0; print_statementT = print_statementT0 } = x_25619
1145 h_mk_code_iteration_params cip_print_serialization_params0 fold_code0
1148 (** val code_iteration_params_rect_Type0 :
1149 Joint.params -> AST.ident List.list -> ('a1 print_serialization_params ->
1150 (__ -> (__ -> 'a2 -> __ -> __) -> __ -> __ -> __ -> __) -> ('a2 -> 'a1)
1151 -> 'a3) -> ('a1, 'a2) code_iteration_params -> 'a3 **)
1152 let rec code_iteration_params_rect_Type0 p globals h_mk_code_iteration_params x_25621 =
1153 let { cip_print_serialization_params = cip_print_serialization_params0;
1154 fold_code = fold_code0; print_statementT = print_statementT0 } = x_25621
1156 h_mk_code_iteration_params cip_print_serialization_params0 fold_code0
1159 (** val cip_print_serialization_params :
1160 Joint.params -> AST.ident List.list -> ('a1, 'a2) code_iteration_params
1161 -> 'a1 print_serialization_params **)
1162 let rec cip_print_serialization_params p globals xxx =
1163 xxx.cip_print_serialization_params
1165 (** val fold_code0 :
1166 Joint.params -> AST.ident List.list -> ('a1, 'a2) code_iteration_params
1167 -> (__ -> 'a2 -> 'a3 -> 'a3) -> __ -> __ -> 'a3 -> 'a3 **)
1168 let rec fold_code0 p globals xxx x_25636 x_25637 x_25638 x_25639 =
1169 (let { cip_print_serialization_params = x; fold_code = yyy;
1170 print_statementT = x0 } = xxx
1172 Obj.magic yyy) __ x_25636 x_25637 x_25638 x_25639
1174 (** val print_statementT :
1175 Joint.params -> AST.ident List.list -> ('a1, 'a2) code_iteration_params
1177 let rec print_statementT p globals xxx =
1178 xxx.print_statementT
1180 (** val code_iteration_params_inv_rect_Type4 :
1181 Joint.params -> AST.ident List.list -> ('a1, 'a2) code_iteration_params
1182 -> ('a1 print_serialization_params -> (__ -> (__ -> 'a2 -> __ -> __) ->
1183 __ -> __ -> __ -> __) -> ('a2 -> 'a1) -> __ -> 'a3) -> 'a3 **)
1184 let code_iteration_params_inv_rect_Type4 x2 x4 hterm h1 =
1185 let hcut = code_iteration_params_rect_Type4 x2 x4 h1 hterm in hcut __
1187 (** val code_iteration_params_inv_rect_Type3 :
1188 Joint.params -> AST.ident List.list -> ('a1, 'a2) code_iteration_params
1189 -> ('a1 print_serialization_params -> (__ -> (__ -> 'a2 -> __ -> __) ->
1190 __ -> __ -> __ -> __) -> ('a2 -> 'a1) -> __ -> 'a3) -> 'a3 **)
1191 let code_iteration_params_inv_rect_Type3 x2 x4 hterm h1 =
1192 let hcut = code_iteration_params_rect_Type3 x2 x4 h1 hterm in hcut __
1194 (** val code_iteration_params_inv_rect_Type2 :
1195 Joint.params -> AST.ident List.list -> ('a1, 'a2) code_iteration_params
1196 -> ('a1 print_serialization_params -> (__ -> (__ -> 'a2 -> __ -> __) ->
1197 __ -> __ -> __ -> __) -> ('a2 -> 'a1) -> __ -> 'a3) -> 'a3 **)
1198 let code_iteration_params_inv_rect_Type2 x2 x4 hterm h1 =
1199 let hcut = code_iteration_params_rect_Type2 x2 x4 h1 hterm in hcut __
1201 (** val code_iteration_params_inv_rect_Type1 :
1202 Joint.params -> AST.ident List.list -> ('a1, 'a2) code_iteration_params
1203 -> ('a1 print_serialization_params -> (__ -> (__ -> 'a2 -> __ -> __) ->
1204 __ -> __ -> __ -> __) -> ('a2 -> 'a1) -> __ -> 'a3) -> 'a3 **)
1205 let code_iteration_params_inv_rect_Type1 x2 x4 hterm h1 =
1206 let hcut = code_iteration_params_rect_Type1 x2 x4 h1 hterm in hcut __
1208 (** val code_iteration_params_inv_rect_Type0 :
1209 Joint.params -> AST.ident List.list -> ('a1, 'a2) code_iteration_params
1210 -> ('a1 print_serialization_params -> (__ -> (__ -> 'a2 -> __ -> __) ->
1211 __ -> __ -> __ -> __) -> ('a2 -> 'a1) -> __ -> 'a3) -> 'a3 **)
1212 let code_iteration_params_inv_rect_Type0 x2 x4 hterm h1 =
1213 let hcut = code_iteration_params_rect_Type0 x2 x4 h1 hterm in hcut __
1215 (** val code_iteration_params_jmdiscr :
1216 Joint.params -> AST.ident List.list -> ('a1, 'a2) code_iteration_params
1217 -> ('a1, 'a2) code_iteration_params -> __ **)
1218 let code_iteration_params_jmdiscr a2 a4 x y =
1219 Logic.eq_rect_Type2 x
1220 (let { cip_print_serialization_params = a0; fold_code = a10;
1221 print_statementT = a20 } = x
1223 Obj.magic (fun _ dH -> dH __ __ __)) y
1225 (** val pm_choose_with_pref :
1226 'a1 PositiveMap.positive_map -> Positive.pos Types.option ->
1227 ((Positive.pos, 'a1) Types.prod, 'a1 PositiveMap.positive_map) Types.prod
1229 let pm_choose_with_pref m = function
1230 | Types.None -> PositiveMap.pm_choose m
1232 (match PositiveMap.pm_try_remove p m with
1233 | Types.None -> PositiveMap.pm_choose m
1235 let { Types.fst = a; Types.snd = m' } = res in
1236 Types.Some { Types.fst = { Types.fst = p; Types.snd = a }; Types.snd =
1239 (** val visit_graph :
1240 ('a1 -> Positive.pos Types.option) -> (Positive.pos -> 'a1 -> 'a2 -> 'a2)
1241 -> 'a2 -> Positive.pos Types.option -> 'a1 PositiveMap.positive_map ->
1243 let rec visit_graph next f b n m = function
1246 (match pm_choose_with_pref m n with
1249 let { Types.fst = eta32074; Types.snd = m' } = res in
1250 let { Types.fst = pos; Types.snd = a } = eta32074 in
1251 visit_graph next f (f pos a b) (next a) m' y)
1253 (** val print_list :
1254 'a1 printing_pass_independent_params -> 'a1 List.list -> 'a1 **)
1256 List.foldr pp.print_concat pp.print_empty
1258 (** val print_joint_seq :
1259 Joint.unserialized_params -> AST.ident List.list -> 'a1 printing_params
1260 -> Joint.joint_seq -> 'a1 **)
1261 let print_joint_seq p globals pp = function
1262 | Joint.COMMENT str ->
1263 print_list pp.print_pass_ind (List.Cons
1264 ((pp.print_pass_ind.print_keyword KwCOMMENT), (List.Cons
1265 ((pp.print_pass_ind.print_String str), List.Nil))))
1267 print_list pp.print_pass_ind (List.Cons
1268 ((pp.print_pass_ind.print_keyword KwMOVE), (List.Cons
1269 ((pp.print_pair_move pm), List.Nil))))
1271 print_list pp.print_pass_ind (List.Cons
1272 ((pp.print_pass_ind.print_keyword KwPOP), (List.Cons
1273 ((pp.print_acc_a_reg arg), List.Nil))))
1275 print_list pp.print_pass_ind (List.Cons
1276 ((pp.print_pass_ind.print_keyword KwPUSH), (List.Cons
1277 ((pp.print_acc_a_arg arg), List.Nil))))
1278 | Joint.ADDRESS (i, offset, arg1, arg2) ->
1279 print_list pp.print_pass_ind (List.Cons
1280 ((pp.print_pass_ind.print_keyword KwADDRESS), (List.Cons
1281 ((pp.print_pass_ind.print_ident i), (List.Cons
1282 ((pp.print_pass_ind.print_bitvector (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
1283 (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
1284 (Nat.S Nat.O)))))))))))))))) offset), (List.Cons
1285 ((pp.print_dpl_reg arg1), (List.Cons ((pp.print_dph_reg arg2),
1287 | Joint.OPACCS (opa, arg1, arg2, arg3, arg4) ->
1288 print_list pp.print_pass_ind (List.Cons
1289 ((pp.print_pass_ind.print_keyword KwOPACCS), (List.Cons
1290 ((pp.print_pass_ind.print_OpAccs opa), (List.Cons
1291 ((pp.print_acc_a_reg arg1), (List.Cons ((pp.print_acc_b_reg arg2),
1292 (List.Cons ((pp.print_acc_a_arg arg3), (List.Cons
1293 ((pp.print_acc_b_arg arg4), List.Nil))))))))))))
1294 | Joint.OP1 (op1, arg1, arg2) ->
1295 print_list pp.print_pass_ind (List.Cons
1296 ((pp.print_pass_ind.print_keyword KwOP1), (List.Cons
1297 ((pp.print_pass_ind.print_Op1 op1), (List.Cons
1298 ((pp.print_acc_a_reg arg1), (List.Cons ((pp.print_acc_a_reg arg2),
1300 | Joint.OP2 (op2, arg1, arg2, arg3) ->
1301 print_list pp.print_pass_ind (List.Cons
1302 ((pp.print_pass_ind.print_keyword KwOP2), (List.Cons
1303 ((pp.print_pass_ind.print_Op2 op2), (List.Cons
1304 ((pp.print_acc_a_reg arg1), (List.Cons ((pp.print_acc_a_arg arg2),
1305 (List.Cons ((pp.print_snd_arg arg3), List.Nil))))))))))
1306 | Joint.CLEAR_CARRY -> pp.print_pass_ind.print_keyword KwCLEAR_CARRY
1307 | Joint.SET_CARRY -> pp.print_pass_ind.print_keyword KwSET_CARRY
1308 | Joint.LOAD (arg1, arg2, arg3) ->
1309 print_list pp.print_pass_ind (List.Cons
1310 ((pp.print_pass_ind.print_keyword KwLOAD), (List.Cons
1311 ((pp.print_acc_a_reg arg1), (List.Cons ((pp.print_dpl_arg arg2),
1312 (List.Cons ((pp.print_dph_arg arg3), List.Nil))))))))
1313 | Joint.STORE (arg1, arg2, arg3) ->
1314 print_list pp.print_pass_ind (List.Cons
1315 ((pp.print_pass_ind.print_keyword KwSTORE), (List.Cons
1316 ((pp.print_dpl_arg arg1), (List.Cons ((pp.print_dph_arg arg2), (List.Cons
1317 ((pp.print_acc_a_arg arg3), List.Nil))))))))
1318 | Joint.Extension_seq ext -> pp.print_ext_seq ext
1320 (** val print_joint_step :
1321 Joint.unserialized_params -> AST.ident List.list -> 'a1 printing_params
1322 -> Joint.joint_step -> 'a1 **)
1323 let print_joint_step p globals pp = function
1324 | Joint.COST_LABEL arg ->
1325 print_list pp.print_pass_ind (List.Cons
1326 ((pp.print_pass_ind.print_keyword KwCOST_LABEL), (List.Cons
1327 ((pp.print_pass_ind.print_costlabel arg), List.Nil))))
1328 | Joint.CALL (arg1, arg2, arg3) ->
1329 print_list pp.print_pass_ind (List.Cons
1330 ((pp.print_pass_ind.print_keyword KwCALL), (List.Cons
1332 | Types.Inl id -> pp.print_pass_ind.print_ident id
1333 | Types.Inr arg11_arg12 ->
1334 pp.print_pass_ind.print_concat
1335 (pp.print_dpl_arg arg11_arg12.Types.fst)
1336 (pp.print_dph_arg arg11_arg12.Types.snd)), (List.Cons
1337 ((pp.print_call_args arg2), (List.Cons ((pp.print_call_dest arg3),
1339 | Joint.COND (arg1, arg2) ->
1340 print_list pp.print_pass_ind (List.Cons
1341 ((pp.print_pass_ind.print_keyword KwCOND), (List.Cons
1342 ((pp.print_acc_a_reg arg1), (List.Cons
1343 ((pp.print_pass_ind.print_label arg2), List.Nil))))))
1344 | Joint.Step_seq seq -> print_joint_seq p globals pp seq
1346 (** val print_joint_fin_step :
1347 Joint.unserialized_params -> 'a1 printing_params -> Joint.joint_fin_step
1349 let print_joint_fin_step p pp = function
1351 print_list pp.print_pass_ind (List.Cons
1352 ((pp.print_pass_ind.print_keyword KwGOTO), (List.Cons
1353 ((pp.print_pass_ind.print_label l), List.Nil))))
1354 | Joint.RETURN -> pp.print_pass_ind.print_keyword KwRETURN
1355 | Joint.TAILCALL (arg1, arg2) ->
1356 print_list pp.print_pass_ind (List.Cons
1357 ((pp.print_pass_ind.print_keyword KwTAILCALL), (List.Cons
1359 | Types.Inl id -> pp.print_pass_ind.print_ident id
1360 | Types.Inr arg11_arg12 ->
1361 pp.print_pass_ind.print_concat
1362 (pp.print_dpl_arg arg11_arg12.Types.fst)
1363 (pp.print_dph_arg arg11_arg12.Types.snd)), (List.Cons
1364 ((pp.print_call_args arg2), List.Nil))))))
1366 (** val print_joint_statement :
1367 Joint.params -> AST.ident List.list -> 'a1 printing_params -> 'a1
1368 print_serialization_params -> Joint.joint_statement -> 'a1 **)
1369 let print_joint_statement p globals pp cip = function
1370 | Joint.Sequential (js, arg1) ->
1371 pp.print_pass_ind.print_concat
1372 (print_joint_step (Joint.stmt_pars__o__uns_pars__o__u_pars p) globals pp
1373 js) (cip.print_succ arg1)
1374 | Joint.Final fin ->
1375 print_joint_fin_step (Joint.stmt_pars__o__uns_pars__o__u_pars p) pp fin
1376 | Joint.FCOND (arg1, arg2, arg3) ->
1377 print_list pp.print_pass_ind (List.Cons
1378 ((pp.print_pass_ind.print_keyword KwFCOND), (List.Cons
1379 ((pp.print_acc_a_reg arg1), (List.Cons
1380 ((pp.print_pass_ind.print_label arg2), (List.Cons
1381 ((pp.print_pass_ind.print_label arg3), List.Nil))))))))
1383 (** val graph_print_serialization_params :
1384 Joint.graph_params -> 'a1 printing_params -> 'a1
1385 print_serialization_params **)
1386 let graph_print_serialization_params gp pp =
1387 { print_succ = (Obj.magic pp.print_pass_ind.print_label);
1388 print_code_point = (Obj.magic pp.print_pass_ind.print_label) }
1390 (** val graph_code_iteration_params :
1391 Joint.graph_params -> AST.ident List.list -> 'a1 printing_params -> ('a1,
1392 Joint.joint_statement) code_iteration_params **)
1393 let graph_code_iteration_params gp globals pp =
1394 { cip_print_serialization_params =
1395 (graph_print_serialization_params gp pp); fold_code =
1396 (fun _ f m initl a ->
1397 visit_graph (fun stmt ->
1398 match Joint.stmt_implicit_label (Joint.gp_to_p__o__stmt_pars gp)
1400 | Types.None -> Types.None
1401 | Types.Some label -> let p = label in Types.Some p) (fun n ->
1402 Obj.magic f n) a (Types.Some
1403 (Identifiers.word_of_identifier PreIdentifiers.LabelTag
1404 (Obj.magic initl))) (let m' = Obj.magic m in m')
1405 (Identifiers.id_map_size PreIdentifiers.LabelTag (Obj.magic m)));
1407 (print_joint_statement (Joint.graph_params_to_params gp) globals pp
1408 (graph_print_serialization_params gp pp)) }
1410 (** val lin_print_serialization_params :
1411 Joint.lin_params -> 'a1 printing_params -> 'a1 print_serialization_params **)
1412 let lin_print_serialization_params gp pp =
1413 { print_succ = (fun x -> pp.print_pass_ind.print_empty); print_code_point =
1414 (Obj.magic pp.print_pass_ind.print_nat) }
1416 (** val lin_code_iteration_params :
1417 Joint.lin_params -> AST.ident List.list -> 'a1 printing_params -> ('a1,
1418 (Graphs.label Types.option, Joint.joint_statement) Types.prod)
1419 code_iteration_params **)
1420 let lin_code_iteration_params lp globals pp =
1421 { cip_print_serialization_params = (lin_print_serialization_params lp pp);
1422 fold_code = (fun _ f m x a ->
1423 (Util.foldl (fun res x0 ->
1424 let { Types.fst = pc; Types.snd = res' } = res in
1425 { Types.fst = (Nat.S pc); Types.snd = (Obj.magic f pc x0 res') })
1426 { Types.fst = Nat.O; Types.snd = a } (Obj.magic m)).Types.snd);
1427 print_statementT = (fun linstr ->
1428 match linstr.Types.fst with
1430 print_joint_statement (Joint.lin_params_to_params lp) globals pp
1431 (lin_print_serialization_params lp pp) linstr.Types.snd
1433 print_list pp.print_pass_ind (List.Cons
1434 ((pp.print_pass_ind.print_label l), (List.Cons
1435 ((print_joint_statement (Joint.lin_params_to_params lp) globals pp
1436 (lin_print_serialization_params lp pp) linstr.Types.snd),
1439 (** val print_joint_internal_function :
1440 Joint.params -> AST.ident List.list -> ('a2, 'a1) code_iteration_params
1441 -> 'a2 printing_params -> Joint.joint_internal_function -> 'a2 List.list **)
1442 let print_joint_internal_function p globals cip pp f =
1443 fold_code0 p globals cip (fun cp stmt acc -> List.Cons
1444 ((print_list pp.print_pass_ind (List.Cons
1445 ((cip.cip_print_serialization_params.print_code_point cp), (List.Cons
1446 ((cip.print_statementT stmt), List.Nil))))), acc))
1447 f.Joint.joint_if_code f.Joint.joint_if_entry List.Nil
1449 (** val print_joint_function :
1450 Joint.params -> AST.ident List.list -> AST.ident List.list -> ('a2, 'a1)
1451 code_iteration_params -> 'a2 printing_params -> Joint.joint_function ->
1453 let print_joint_function p globals functions cip pp = function
1454 | AST.Internal f0 ->
1455 print_joint_internal_function p (List.append globals functions) cip pp
1457 | AST.External f0 -> List.Nil
1459 (** val print_joint_program :
1460 Joint.params -> 'a2 printing_params -> Joint.joint_program -> ('a2, 'a1)
1461 code_iteration_params -> (AST.ident, 'a2 List.list) Types.prod List.list **)
1462 let print_joint_program p pp prog cip =
1463 List.foldr (fun f acc -> List.Cons ({ Types.fst = f.Types.fst; Types.snd =
1464 (print_joint_function p (AST.prog_var_names prog.Joint.joint_prog)
1465 prog.Joint.jp_functions cip pp f.Types.snd) }, acc)) List.Nil
1466 prog.Joint.joint_prog.AST.prog_funct