Changeset 2982


Ignore:
Timestamp:
Mar 27, 2013, 6:05:41 PM (4 years ago)
Author:
sacerdot
Message:

Pretty priting of LIN implemented.

Files:
4 edited

Legend:

Unmodified
Added
Removed
  • driver/printer.ml

    r2901 r2982  
    5858 ; print_Op1 = print_op1
    5959 ; print_Op2 = print_op2
     60 ; print_nat = (fun n -> string_of_int (Extracted.Glue.int_of_matitanat n))
    6061 }
    6162
     
    242243      beprint
    243244       (Extracted.LTL_printer.print_LTL_program joint_LTL_LIN_printing_params)
     245   | Extracted.Compiler.Lin_pass ->
     246      beprint
     247       (Extracted.LIN_printer.print_LIN_program joint_LTL_LIN_printing_params)
    244248   | Extracted.Compiler.Object_code_pass ->
    245249      ASMPrinter.print_program (Extracted.ASM.oc (Obj.magic program))
  • extracted/joint_printer.ml

    r2951 r2982  
    417417                                                              -> 'string);
    418418                                                  print_Op2 : (BackEndOps.op2
    419                                                               -> 'string) }
     419                                                              -> 'string);
     420                                                  print_nat : (Nat.nat ->
     421                                                              'string) }
    420422
    421423(** val printing_pass_independent_params_rect_Type4 :
     
    423425    -> (AST.ident -> 'a1) -> (CostLabel.costlabel -> 'a1) -> (Graphs.label ->
    424426    'a1) -> (BackEndOps.opAccs -> 'a1) -> (BackEndOps.op1 -> 'a1) ->
    425     (BackEndOps.op2 -> 'a1) -> 'a2) -> 'a1 printing_pass_independent_params
    426     -> 'a2 **)
     427    (BackEndOps.op2 -> 'a1) -> (Nat.nat -> 'a1) -> 'a2) -> 'a1
     428    printing_pass_independent_params -> 'a2 **)
    427429let rec printing_pass_independent_params_rect_Type4 h_mk_printing_pass_independent_params x_263 =
    428430  let { print_String = print_String0; print_keyword = print_keyword0;
     
    430432    print_ident0; print_costlabel = print_costlabel0; print_label =
    431433    print_label0; print_OpAccs = print_OpAccs0; print_Op1 = print_Op3;
    432     print_Op2 = print_Op4 } = x_263
     434    print_Op2 = print_Op4; print_nat = print_nat0 } = x_263
    433435  in
    434436  h_mk_printing_pass_independent_params print_String0 print_keyword0
    435437    print_concat0 print_empty0 print_ident0 print_costlabel0 print_label0
    436     print_OpAccs0 print_Op3 print_Op4
     438    print_OpAccs0 print_Op3 print_Op4 print_nat0
    437439
    438440(** val printing_pass_independent_params_rect_Type5 :
     
    440442    -> (AST.ident -> 'a1) -> (CostLabel.costlabel -> 'a1) -> (Graphs.label ->
    441443    'a1) -> (BackEndOps.opAccs -> 'a1) -> (BackEndOps.op1 -> 'a1) ->
    442     (BackEndOps.op2 -> 'a1) -> 'a2) -> 'a1 printing_pass_independent_params
    443     -> 'a2 **)
     444    (BackEndOps.op2 -> 'a1) -> (Nat.nat -> 'a1) -> 'a2) -> 'a1
     445    printing_pass_independent_params -> 'a2 **)
    444446let rec printing_pass_independent_params_rect_Type5 h_mk_printing_pass_independent_params x_265 =
    445447  let { print_String = print_String0; print_keyword = print_keyword0;
     
    447449    print_ident0; print_costlabel = print_costlabel0; print_label =
    448450    print_label0; print_OpAccs = print_OpAccs0; print_Op1 = print_Op3;
    449     print_Op2 = print_Op4 } = x_265
     451    print_Op2 = print_Op4; print_nat = print_nat0 } = x_265
    450452  in
    451453  h_mk_printing_pass_independent_params print_String0 print_keyword0
    452454    print_concat0 print_empty0 print_ident0 print_costlabel0 print_label0
    453     print_OpAccs0 print_Op3 print_Op4
     455    print_OpAccs0 print_Op3 print_Op4 print_nat0
    454456
    455457(** val printing_pass_independent_params_rect_Type3 :
     
    457459    -> (AST.ident -> 'a1) -> (CostLabel.costlabel -> 'a1) -> (Graphs.label ->
    458460    'a1) -> (BackEndOps.opAccs -> 'a1) -> (BackEndOps.op1 -> 'a1) ->
    459     (BackEndOps.op2 -> 'a1) -> 'a2) -> 'a1 printing_pass_independent_params
    460     -> 'a2 **)
     461    (BackEndOps.op2 -> 'a1) -> (Nat.nat -> 'a1) -> 'a2) -> 'a1
     462    printing_pass_independent_params -> 'a2 **)
    461463let rec printing_pass_independent_params_rect_Type3 h_mk_printing_pass_independent_params x_267 =
    462464  let { print_String = print_String0; print_keyword = print_keyword0;
     
    464466    print_ident0; print_costlabel = print_costlabel0; print_label =
    465467    print_label0; print_OpAccs = print_OpAccs0; print_Op1 = print_Op3;
    466     print_Op2 = print_Op4 } = x_267
     468    print_Op2 = print_Op4; print_nat = print_nat0 } = x_267
    467469  in
    468470  h_mk_printing_pass_independent_params print_String0 print_keyword0
    469471    print_concat0 print_empty0 print_ident0 print_costlabel0 print_label0
    470     print_OpAccs0 print_Op3 print_Op4
     472    print_OpAccs0 print_Op3 print_Op4 print_nat0
    471473
    472474(** val printing_pass_independent_params_rect_Type2 :
     
    474476    -> (AST.ident -> 'a1) -> (CostLabel.costlabel -> 'a1) -> (Graphs.label ->
    475477    'a1) -> (BackEndOps.opAccs -> 'a1) -> (BackEndOps.op1 -> 'a1) ->
    476     (BackEndOps.op2 -> 'a1) -> 'a2) -> 'a1 printing_pass_independent_params
    477     -> 'a2 **)
     478    (BackEndOps.op2 -> 'a1) -> (Nat.nat -> 'a1) -> 'a2) -> 'a1
     479    printing_pass_independent_params -> 'a2 **)
    478480let rec printing_pass_independent_params_rect_Type2 h_mk_printing_pass_independent_params x_269 =
    479481  let { print_String = print_String0; print_keyword = print_keyword0;
     
    481483    print_ident0; print_costlabel = print_costlabel0; print_label =
    482484    print_label0; print_OpAccs = print_OpAccs0; print_Op1 = print_Op3;
    483     print_Op2 = print_Op4 } = x_269
     485    print_Op2 = print_Op4; print_nat = print_nat0 } = x_269
    484486  in
    485487  h_mk_printing_pass_independent_params print_String0 print_keyword0
    486488    print_concat0 print_empty0 print_ident0 print_costlabel0 print_label0
    487     print_OpAccs0 print_Op3 print_Op4
     489    print_OpAccs0 print_Op3 print_Op4 print_nat0
    488490
    489491(** val printing_pass_independent_params_rect_Type1 :
     
    491493    -> (AST.ident -> 'a1) -> (CostLabel.costlabel -> 'a1) -> (Graphs.label ->
    492494    'a1) -> (BackEndOps.opAccs -> 'a1) -> (BackEndOps.op1 -> 'a1) ->
    493     (BackEndOps.op2 -> 'a1) -> 'a2) -> 'a1 printing_pass_independent_params
    494     -> 'a2 **)
     495    (BackEndOps.op2 -> 'a1) -> (Nat.nat -> 'a1) -> 'a2) -> 'a1
     496    printing_pass_independent_params -> 'a2 **)
    495497let rec printing_pass_independent_params_rect_Type1 h_mk_printing_pass_independent_params x_271 =
    496498  let { print_String = print_String0; print_keyword = print_keyword0;
     
    498500    print_ident0; print_costlabel = print_costlabel0; print_label =
    499501    print_label0; print_OpAccs = print_OpAccs0; print_Op1 = print_Op3;
    500     print_Op2 = print_Op4 } = x_271
     502    print_Op2 = print_Op4; print_nat = print_nat0 } = x_271
    501503  in
    502504  h_mk_printing_pass_independent_params print_String0 print_keyword0
    503505    print_concat0 print_empty0 print_ident0 print_costlabel0 print_label0
    504     print_OpAccs0 print_Op3 print_Op4
     506    print_OpAccs0 print_Op3 print_Op4 print_nat0
    505507
    506508(** val printing_pass_independent_params_rect_Type0 :
     
    508510    -> (AST.ident -> 'a1) -> (CostLabel.costlabel -> 'a1) -> (Graphs.label ->
    509511    'a1) -> (BackEndOps.opAccs -> 'a1) -> (BackEndOps.op1 -> 'a1) ->
    510     (BackEndOps.op2 -> 'a1) -> 'a2) -> 'a1 printing_pass_independent_params
    511     -> 'a2 **)
     512    (BackEndOps.op2 -> 'a1) -> (Nat.nat -> 'a1) -> 'a2) -> 'a1
     513    printing_pass_independent_params -> 'a2 **)
    512514let rec printing_pass_independent_params_rect_Type0 h_mk_printing_pass_independent_params x_273 =
    513515  let { print_String = print_String0; print_keyword = print_keyword0;
     
    515517    print_ident0; print_costlabel = print_costlabel0; print_label =
    516518    print_label0; print_OpAccs = print_OpAccs0; print_Op1 = print_Op3;
    517     print_Op2 = print_Op4 } = x_273
     519    print_Op2 = print_Op4; print_nat = print_nat0 } = x_273
    518520  in
    519521  h_mk_printing_pass_independent_params print_String0 print_keyword0
    520522    print_concat0 print_empty0 print_ident0 print_costlabel0 print_label0
    521     print_OpAccs0 print_Op3 print_Op4
     523    print_OpAccs0 print_Op3 print_Op4 print_nat0
    522524
    523525(** val print_String :
     
    569571let rec print_Op2 xxx =
    570572  xxx.print_Op2
     573
     574(** val print_nat :
     575    'a1 printing_pass_independent_params -> Nat.nat -> 'a1 **)
     576let rec print_nat xxx =
     577  xxx.print_nat
    571578
    572579(** val printing_pass_independent_params_inv_rect_Type4 :
     
    575582    (CostLabel.costlabel -> 'a1) -> (Graphs.label -> 'a1) ->
    576583    (BackEndOps.opAccs -> 'a1) -> (BackEndOps.op1 -> 'a1) -> (BackEndOps.op2
    577     -> 'a1) -> __ -> 'a2) -> 'a2 **)
     584    -> 'a1) -> (Nat.nat -> 'a1) -> __ -> 'a2) -> 'a2 **)
    578585let printing_pass_independent_params_inv_rect_Type4 hterm h1 =
    579586  let hcut = printing_pass_independent_params_rect_Type4 h1 hterm in hcut __
     
    584591    (CostLabel.costlabel -> 'a1) -> (Graphs.label -> 'a1) ->
    585592    (BackEndOps.opAccs -> 'a1) -> (BackEndOps.op1 -> 'a1) -> (BackEndOps.op2
    586     -> 'a1) -> __ -> 'a2) -> 'a2 **)
     593    -> 'a1) -> (Nat.nat -> 'a1) -> __ -> 'a2) -> 'a2 **)
    587594let printing_pass_independent_params_inv_rect_Type3 hterm h1 =
    588595  let hcut = printing_pass_independent_params_rect_Type3 h1 hterm in hcut __
     
    593600    (CostLabel.costlabel -> 'a1) -> (Graphs.label -> 'a1) ->
    594601    (BackEndOps.opAccs -> 'a1) -> (BackEndOps.op1 -> 'a1) -> (BackEndOps.op2
    595     -> 'a1) -> __ -> 'a2) -> 'a2 **)
     602    -> 'a1) -> (Nat.nat -> 'a1) -> __ -> 'a2) -> 'a2 **)
    596603let printing_pass_independent_params_inv_rect_Type2 hterm h1 =
    597604  let hcut = printing_pass_independent_params_rect_Type2 h1 hterm in hcut __
     
    602609    (CostLabel.costlabel -> 'a1) -> (Graphs.label -> 'a1) ->
    603610    (BackEndOps.opAccs -> 'a1) -> (BackEndOps.op1 -> 'a1) -> (BackEndOps.op2
    604     -> 'a1) -> __ -> 'a2) -> 'a2 **)
     611    -> 'a1) -> (Nat.nat -> 'a1) -> __ -> 'a2) -> 'a2 **)
    605612let printing_pass_independent_params_inv_rect_Type1 hterm h1 =
    606613  let hcut = printing_pass_independent_params_rect_Type1 h1 hterm in hcut __
     
    611618    (CostLabel.costlabel -> 'a1) -> (Graphs.label -> 'a1) ->
    612619    (BackEndOps.opAccs -> 'a1) -> (BackEndOps.op1 -> 'a1) -> (BackEndOps.op2
    613     -> 'a1) -> __ -> 'a2) -> 'a2 **)
     620    -> 'a1) -> (Nat.nat -> 'a1) -> __ -> 'a2) -> 'a2 **)
    614621let printing_pass_independent_params_inv_rect_Type0 hterm h1 =
    615622  let hcut = printing_pass_independent_params_rect_Type0 h1 hterm in hcut __
     
    622629    (let { print_String = a0; print_keyword = a10; print_concat = a2;
    623630       print_empty = a3; print_ident = a4; print_costlabel = a5;
    624        print_label = a6; print_OpAccs = a7; print_Op1 = a8; print_Op2 =
    625        a9 } = x
     631       print_label = a6; print_OpAccs = a7; print_Op1 = a8; print_Op2 = a9;
     632       print_nat = a100 } = x
    626633     in
    627     Obj.magic (fun _ dH -> dH __ __ __ __ __ __ __ __ __ __)) y
     634    Obj.magic (fun _ dH -> dH __ __ __ __ __ __ __ __ __ __ __)) y
    628635
    629636type 'string printing_params = { print_pass_ind : 'string
     
    649656    -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> 'a2) -> 'a1
    650657    printing_params -> 'a2 **)
    651 let rec printing_params_rect_Type4 p h_mk_printing_params x_299 =
     658let rec printing_params_rect_Type4 p h_mk_printing_params x_300 =
    652659  let { print_pass_ind = print_pass_ind0; print_acc_a_reg = print_acc_a_reg0;
    653660    print_acc_b_reg = print_acc_b_reg0; print_acc_a_arg = print_acc_a_arg0;
     
    657664    print_pair_move = print_pair_move0; print_call_args = print_call_args0;
    658665    print_call_dest = print_call_dest0; print_ext_seq = print_ext_seq0 } =
    659     x_299
     666    x_300
    660667  in
    661668  h_mk_printing_params print_pass_ind0 print_acc_a_reg0 print_acc_b_reg0
     
    670677    -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> 'a2) -> 'a1
    671678    printing_params -> 'a2 **)
    672 let rec printing_params_rect_Type5 p h_mk_printing_params x_301 =
     679let rec printing_params_rect_Type5 p h_mk_printing_params x_302 =
    673680  let { print_pass_ind = print_pass_ind0; print_acc_a_reg = print_acc_a_reg0;
    674681    print_acc_b_reg = print_acc_b_reg0; print_acc_a_arg = print_acc_a_arg0;
     
    678685    print_pair_move = print_pair_move0; print_call_args = print_call_args0;
    679686    print_call_dest = print_call_dest0; print_ext_seq = print_ext_seq0 } =
    680     x_301
     687    x_302
    681688  in
    682689  h_mk_printing_params print_pass_ind0 print_acc_a_reg0 print_acc_b_reg0
     
    691698    -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> 'a2) -> 'a1
    692699    printing_params -> 'a2 **)
    693 let rec printing_params_rect_Type3 p h_mk_printing_params x_303 =
     700let rec printing_params_rect_Type3 p h_mk_printing_params x_304 =
    694701  let { print_pass_ind = print_pass_ind0; print_acc_a_reg = print_acc_a_reg0;
    695702    print_acc_b_reg = print_acc_b_reg0; print_acc_a_arg = print_acc_a_arg0;
     
    699706    print_pair_move = print_pair_move0; print_call_args = print_call_args0;
    700707    print_call_dest = print_call_dest0; print_ext_seq = print_ext_seq0 } =
    701     x_303
     708    x_304
    702709  in
    703710  h_mk_printing_params print_pass_ind0 print_acc_a_reg0 print_acc_b_reg0
     
    712719    -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> 'a2) -> 'a1
    713720    printing_params -> 'a2 **)
    714 let rec printing_params_rect_Type2 p h_mk_printing_params x_305 =
     721let rec printing_params_rect_Type2 p h_mk_printing_params x_306 =
    715722  let { print_pass_ind = print_pass_ind0; print_acc_a_reg = print_acc_a_reg0;
    716723    print_acc_b_reg = print_acc_b_reg0; print_acc_a_arg = print_acc_a_arg0;
     
    720727    print_pair_move = print_pair_move0; print_call_args = print_call_args0;
    721728    print_call_dest = print_call_dest0; print_ext_seq = print_ext_seq0 } =
    722     x_305
     729    x_306
    723730  in
    724731  h_mk_printing_params print_pass_ind0 print_acc_a_reg0 print_acc_b_reg0
     
    733740    -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> 'a2) -> 'a1
    734741    printing_params -> 'a2 **)
    735 let rec printing_params_rect_Type1 p h_mk_printing_params x_307 =
     742let rec printing_params_rect_Type1 p h_mk_printing_params x_308 =
    736743  let { print_pass_ind = print_pass_ind0; print_acc_a_reg = print_acc_a_reg0;
    737744    print_acc_b_reg = print_acc_b_reg0; print_acc_a_arg = print_acc_a_arg0;
     
    741748    print_pair_move = print_pair_move0; print_call_args = print_call_args0;
    742749    print_call_dest = print_call_dest0; print_ext_seq = print_ext_seq0 } =
    743     x_307
     750    x_308
    744751  in
    745752  h_mk_printing_params print_pass_ind0 print_acc_a_reg0 print_acc_b_reg0
     
    754761    -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> 'a2) -> 'a1
    755762    printing_params -> 'a2 **)
    756 let rec printing_params_rect_Type0 p h_mk_printing_params x_309 =
     763let rec printing_params_rect_Type0 p h_mk_printing_params x_310 =
    757764  let { print_pass_ind = print_pass_ind0; print_acc_a_reg = print_acc_a_reg0;
    758765    print_acc_b_reg = print_acc_b_reg0; print_acc_a_arg = print_acc_a_arg0;
     
    762769    print_pair_move = print_pair_move0; print_call_args = print_call_args0;
    763770    print_call_dest = print_call_dest0; print_ext_seq = print_ext_seq0 } =
    764     x_309
     771    x_310
    765772  in
    766773  h_mk_printing_params print_pass_ind0 print_acc_a_reg0 print_acc_b_reg0
     
    928935  (Types.pi1 x3).print_pass_ind
    929936
    930 type 'string code_iteration_params = { fold_code : (__ -> (__ ->
    931                                                    Joint.joint_statement ->
    932                                                    __ -> __) -> __ -> __ ->
    933                                                    __);
    934                                        print_succ : (__ -> 'string);
    935                                        print_code_point : (__ -> 'string) }
     937type 'string print_serialization_params = { print_succ : (__ -> 'string);
     938                                            print_code_point : (__ ->
     939                                                               'string) }
     940
     941(** val print_serialization_params_rect_Type4 :
     942    Joint.params -> ((__ -> 'a1) -> (__ -> 'a1) -> 'a2) -> 'a1
     943    print_serialization_params -> 'a2 **)
     944let rec print_serialization_params_rect_Type4 p h_mk_print_serialization_params x_339 =
     945  let { print_succ = print_succ0; print_code_point = print_code_point0 } =
     946    x_339
     947  in
     948  h_mk_print_serialization_params print_succ0 print_code_point0
     949
     950(** val print_serialization_params_rect_Type5 :
     951    Joint.params -> ((__ -> 'a1) -> (__ -> 'a1) -> 'a2) -> 'a1
     952    print_serialization_params -> 'a2 **)
     953let rec print_serialization_params_rect_Type5 p h_mk_print_serialization_params x_341 =
     954  let { print_succ = print_succ0; print_code_point = print_code_point0 } =
     955    x_341
     956  in
     957  h_mk_print_serialization_params print_succ0 print_code_point0
     958
     959(** val print_serialization_params_rect_Type3 :
     960    Joint.params -> ((__ -> 'a1) -> (__ -> 'a1) -> 'a2) -> 'a1
     961    print_serialization_params -> 'a2 **)
     962let rec print_serialization_params_rect_Type3 p h_mk_print_serialization_params x_343 =
     963  let { print_succ = print_succ0; print_code_point = print_code_point0 } =
     964    x_343
     965  in
     966  h_mk_print_serialization_params print_succ0 print_code_point0
     967
     968(** val print_serialization_params_rect_Type2 :
     969    Joint.params -> ((__ -> 'a1) -> (__ -> 'a1) -> 'a2) -> 'a1
     970    print_serialization_params -> 'a2 **)
     971let rec print_serialization_params_rect_Type2 p h_mk_print_serialization_params x_345 =
     972  let { print_succ = print_succ0; print_code_point = print_code_point0 } =
     973    x_345
     974  in
     975  h_mk_print_serialization_params print_succ0 print_code_point0
     976
     977(** val print_serialization_params_rect_Type1 :
     978    Joint.params -> ((__ -> 'a1) -> (__ -> 'a1) -> 'a2) -> 'a1
     979    print_serialization_params -> 'a2 **)
     980let rec print_serialization_params_rect_Type1 p h_mk_print_serialization_params x_347 =
     981  let { print_succ = print_succ0; print_code_point = print_code_point0 } =
     982    x_347
     983  in
     984  h_mk_print_serialization_params print_succ0 print_code_point0
     985
     986(** val print_serialization_params_rect_Type0 :
     987    Joint.params -> ((__ -> 'a1) -> (__ -> 'a1) -> 'a2) -> 'a1
     988    print_serialization_params -> 'a2 **)
     989let rec print_serialization_params_rect_Type0 p h_mk_print_serialization_params x_349 =
     990  let { print_succ = print_succ0; print_code_point = print_code_point0 } =
     991    x_349
     992  in
     993  h_mk_print_serialization_params print_succ0 print_code_point0
     994
     995(** val print_succ :
     996    Joint.params -> 'a1 print_serialization_params -> __ -> 'a1 **)
     997let rec print_succ p xxx =
     998  xxx.print_succ
     999
     1000(** val print_code_point :
     1001    Joint.params -> 'a1 print_serialization_params -> __ -> 'a1 **)
     1002let rec print_code_point p xxx =
     1003  xxx.print_code_point
     1004
     1005(** val print_serialization_params_inv_rect_Type4 :
     1006    Joint.params -> 'a1 print_serialization_params -> ((__ -> 'a1) -> (__ ->
     1007    'a1) -> __ -> 'a2) -> 'a2 **)
     1008let print_serialization_params_inv_rect_Type4 x2 hterm h1 =
     1009  let hcut = print_serialization_params_rect_Type4 x2 h1 hterm in hcut __
     1010
     1011(** val print_serialization_params_inv_rect_Type3 :
     1012    Joint.params -> 'a1 print_serialization_params -> ((__ -> 'a1) -> (__ ->
     1013    'a1) -> __ -> 'a2) -> 'a2 **)
     1014let print_serialization_params_inv_rect_Type3 x2 hterm h1 =
     1015  let hcut = print_serialization_params_rect_Type3 x2 h1 hterm in hcut __
     1016
     1017(** val print_serialization_params_inv_rect_Type2 :
     1018    Joint.params -> 'a1 print_serialization_params -> ((__ -> 'a1) -> (__ ->
     1019    'a1) -> __ -> 'a2) -> 'a2 **)
     1020let print_serialization_params_inv_rect_Type2 x2 hterm h1 =
     1021  let hcut = print_serialization_params_rect_Type2 x2 h1 hterm in hcut __
     1022
     1023(** val print_serialization_params_inv_rect_Type1 :
     1024    Joint.params -> 'a1 print_serialization_params -> ((__ -> 'a1) -> (__ ->
     1025    'a1) -> __ -> 'a2) -> 'a2 **)
     1026let print_serialization_params_inv_rect_Type1 x2 hterm h1 =
     1027  let hcut = print_serialization_params_rect_Type1 x2 h1 hterm in hcut __
     1028
     1029(** val print_serialization_params_inv_rect_Type0 :
     1030    Joint.params -> 'a1 print_serialization_params -> ((__ -> 'a1) -> (__ ->
     1031    'a1) -> __ -> 'a2) -> 'a2 **)
     1032let print_serialization_params_inv_rect_Type0 x2 hterm h1 =
     1033  let hcut = print_serialization_params_rect_Type0 x2 h1 hterm in hcut __
     1034
     1035(** val print_serialization_params_discr :
     1036    Joint.params -> 'a1 print_serialization_params -> 'a1
     1037    print_serialization_params -> __ **)
     1038let print_serialization_params_discr a2 x y =
     1039  Logic.eq_rect_Type2 x
     1040    (let { print_succ = a0; print_code_point = a10 } = x in
     1041    Obj.magic (fun _ dH -> dH __ __)) y
     1042
     1043(** val print_serialization_params_jmdiscr :
     1044    Joint.params -> 'a1 print_serialization_params -> 'a1
     1045    print_serialization_params -> __ **)
     1046let print_serialization_params_jmdiscr a2 x y =
     1047  Logic.eq_rect_Type2 x
     1048    (let { print_succ = a0; print_code_point = a10 } = x in
     1049    Obj.magic (fun _ dH -> dH __ __)) y
     1050
     1051type ('string, 'statementT) code_iteration_params = { cip_print_serialization_params :
     1052                                                      'string
     1053                                                      print_serialization_params;
     1054                                                      fold_code : (__ -> (__
     1055                                                                  ->
     1056                                                                  'statementT
     1057                                                                  -> __ ->
     1058                                                                  __) -> __
     1059                                                                  -> __ ->
     1060                                                                  __);
     1061                                                      print_statementT :
     1062                                                      ('statementT ->
     1063                                                      'string) }
    9361064
    9371065(** val code_iteration_params_rect_Type4 :
    938     Joint.params -> AST.ident List.list -> ((__ -> (__ ->
    939     Joint.joint_statement -> __ -> __) -> __ -> __ -> __) -> (__ -> 'a1) ->
    940     (__ -> 'a1) -> 'a2) -> 'a1 code_iteration_params -> 'a2 **)
    941 let rec code_iteration_params_rect_Type4 p globals h_mk_code_iteration_params x_338 =
    942   let { fold_code = fold_code0; print_succ = print_succ0; print_code_point =
    943     print_code_point0 } = x_338
    944   in
    945   h_mk_code_iteration_params fold_code0 print_succ0 print_code_point0
     1066    Joint.params -> AST.ident List.list -> ('a1 print_serialization_params ->
     1067    (__ -> (__ -> 'a2 -> __ -> __) -> __ -> __ -> __) -> ('a2 -> 'a1) -> 'a3)
     1068    -> ('a1, 'a2) code_iteration_params -> 'a3 **)
     1069let rec code_iteration_params_rect_Type4 p globals h_mk_code_iteration_params x_367 =
     1070  let { cip_print_serialization_params = cip_print_serialization_params0;
     1071    fold_code = fold_code0; print_statementT = print_statementT0 } = x_367
     1072  in
     1073  h_mk_code_iteration_params cip_print_serialization_params0 fold_code0
     1074    print_statementT0
    9461075
    9471076(** val code_iteration_params_rect_Type5 :
    948     Joint.params -> AST.ident List.list -> ((__ -> (__ ->
    949     Joint.joint_statement -> __ -> __) -> __ -> __ -> __) -> (__ -> 'a1) ->
    950     (__ -> 'a1) -> 'a2) -> 'a1 code_iteration_params -> 'a2 **)
    951 let rec code_iteration_params_rect_Type5 p globals h_mk_code_iteration_params x_340 =
    952   let { fold_code = fold_code0; print_succ = print_succ0; print_code_point =
    953     print_code_point0 } = x_340
    954   in
    955   h_mk_code_iteration_params fold_code0 print_succ0 print_code_point0
     1077    Joint.params -> AST.ident List.list -> ('a1 print_serialization_params ->
     1078    (__ -> (__ -> 'a2 -> __ -> __) -> __ -> __ -> __) -> ('a2 -> 'a1) -> 'a3)
     1079    -> ('a1, 'a2) code_iteration_params -> 'a3 **)
     1080let rec code_iteration_params_rect_Type5 p globals h_mk_code_iteration_params x_369 =
     1081  let { cip_print_serialization_params = cip_print_serialization_params0;
     1082    fold_code = fold_code0; print_statementT = print_statementT0 } = x_369
     1083  in
     1084  h_mk_code_iteration_params cip_print_serialization_params0 fold_code0
     1085    print_statementT0
    9561086
    9571087(** val code_iteration_params_rect_Type3 :
    958     Joint.params -> AST.ident List.list -> ((__ -> (__ ->
    959     Joint.joint_statement -> __ -> __) -> __ -> __ -> __) -> (__ -> 'a1) ->
    960     (__ -> 'a1) -> 'a2) -> 'a1 code_iteration_params -> 'a2 **)
    961 let rec code_iteration_params_rect_Type3 p globals h_mk_code_iteration_params x_342 =
    962   let { fold_code = fold_code0; print_succ = print_succ0; print_code_point =
    963     print_code_point0 } = x_342
    964   in
    965   h_mk_code_iteration_params fold_code0 print_succ0 print_code_point0
     1088    Joint.params -> AST.ident List.list -> ('a1 print_serialization_params ->
     1089    (__ -> (__ -> 'a2 -> __ -> __) -> __ -> __ -> __) -> ('a2 -> 'a1) -> 'a3)
     1090    -> ('a1, 'a2) code_iteration_params -> 'a3 **)
     1091let rec code_iteration_params_rect_Type3 p globals h_mk_code_iteration_params x_371 =
     1092  let { cip_print_serialization_params = cip_print_serialization_params0;
     1093    fold_code = fold_code0; print_statementT = print_statementT0 } = x_371
     1094  in
     1095  h_mk_code_iteration_params cip_print_serialization_params0 fold_code0
     1096    print_statementT0
    9661097
    9671098(** val code_iteration_params_rect_Type2 :
    968     Joint.params -> AST.ident List.list -> ((__ -> (__ ->
    969     Joint.joint_statement -> __ -> __) -> __ -> __ -> __) -> (__ -> 'a1) ->
    970     (__ -> 'a1) -> 'a2) -> 'a1 code_iteration_params -> 'a2 **)
    971 let rec code_iteration_params_rect_Type2 p globals h_mk_code_iteration_params x_344 =
    972   let { fold_code = fold_code0; print_succ = print_succ0; print_code_point =
    973     print_code_point0 } = x_344
    974   in
    975   h_mk_code_iteration_params fold_code0 print_succ0 print_code_point0
     1099    Joint.params -> AST.ident List.list -> ('a1 print_serialization_params ->
     1100    (__ -> (__ -> 'a2 -> __ -> __) -> __ -> __ -> __) -> ('a2 -> 'a1) -> 'a3)
     1101    -> ('a1, 'a2) code_iteration_params -> 'a3 **)
     1102let rec code_iteration_params_rect_Type2 p globals h_mk_code_iteration_params x_373 =
     1103  let { cip_print_serialization_params = cip_print_serialization_params0;
     1104    fold_code = fold_code0; print_statementT = print_statementT0 } = x_373
     1105  in
     1106  h_mk_code_iteration_params cip_print_serialization_params0 fold_code0
     1107    print_statementT0
    9761108
    9771109(** val code_iteration_params_rect_Type1 :
    978     Joint.params -> AST.ident List.list -> ((__ -> (__ ->
    979     Joint.joint_statement -> __ -> __) -> __ -> __ -> __) -> (__ -> 'a1) ->
    980     (__ -> 'a1) -> 'a2) -> 'a1 code_iteration_params -> 'a2 **)
    981 let rec code_iteration_params_rect_Type1 p globals h_mk_code_iteration_params x_346 =
    982   let { fold_code = fold_code0; print_succ = print_succ0; print_code_point =
    983     print_code_point0 } = x_346
    984   in
    985   h_mk_code_iteration_params fold_code0 print_succ0 print_code_point0
     1110    Joint.params -> AST.ident List.list -> ('a1 print_serialization_params ->
     1111    (__ -> (__ -> 'a2 -> __ -> __) -> __ -> __ -> __) -> ('a2 -> 'a1) -> 'a3)
     1112    -> ('a1, 'a2) code_iteration_params -> 'a3 **)
     1113let rec code_iteration_params_rect_Type1 p globals h_mk_code_iteration_params x_375 =
     1114  let { cip_print_serialization_params = cip_print_serialization_params0;
     1115    fold_code = fold_code0; print_statementT = print_statementT0 } = x_375
     1116  in
     1117  h_mk_code_iteration_params cip_print_serialization_params0 fold_code0
     1118    print_statementT0
    9861119
    9871120(** val code_iteration_params_rect_Type0 :
    988     Joint.params -> AST.ident List.list -> ((__ -> (__ ->
    989     Joint.joint_statement -> __ -> __) -> __ -> __ -> __) -> (__ -> 'a1) ->
    990     (__ -> 'a1) -> 'a2) -> 'a1 code_iteration_params -> 'a2 **)
    991 let rec code_iteration_params_rect_Type0 p globals h_mk_code_iteration_params x_348 =
    992   let { fold_code = fold_code0; print_succ = print_succ0; print_code_point =
    993     print_code_point0 } = x_348
    994   in
    995   h_mk_code_iteration_params fold_code0 print_succ0 print_code_point0
     1121    Joint.params -> AST.ident List.list -> ('a1 print_serialization_params ->
     1122    (__ -> (__ -> 'a2 -> __ -> __) -> __ -> __ -> __) -> ('a2 -> 'a1) -> 'a3)
     1123    -> ('a1, 'a2) code_iteration_params -> 'a3 **)
     1124let rec code_iteration_params_rect_Type0 p globals h_mk_code_iteration_params x_377 =
     1125  let { cip_print_serialization_params = cip_print_serialization_params0;
     1126    fold_code = fold_code0; print_statementT = print_statementT0 } = x_377
     1127  in
     1128  h_mk_code_iteration_params cip_print_serialization_params0 fold_code0
     1129    print_statementT0
     1130
     1131(** val cip_print_serialization_params :
     1132    Joint.params -> AST.ident List.list -> ('a1, 'a2) code_iteration_params
     1133    -> 'a1 print_serialization_params **)
     1134let rec cip_print_serialization_params p globals xxx =
     1135  xxx.cip_print_serialization_params
    9961136
    9971137(** val fold_code0 :
    998     Joint.params -> AST.ident List.list -> 'a1 code_iteration_params -> (__
    999     -> Joint.joint_statement -> 'a2 -> 'a2) -> __ -> 'a2 -> 'a2 **)
    1000 let rec fold_code0 p globals xxx x_364 x_365 x_366 =
    1001   (let { fold_code = yyy; print_succ = x; print_code_point = x0 } = xxx in
    1002   Obj.magic yyy) __ x_364 x_365 x_366
    1003 
    1004 (** val print_succ :
    1005     Joint.params -> AST.ident List.list -> 'a1 code_iteration_params -> __ ->
    1006     'a1 **)
    1007 let rec print_succ p globals xxx =
    1008   xxx.print_succ
    1009 
    1010 (** val print_code_point :
    1011     Joint.params -> AST.ident List.list -> 'a1 code_iteration_params -> __ ->
    1012     'a1 **)
    1013 let rec print_code_point p globals xxx =
    1014   xxx.print_code_point
     1138    Joint.params -> AST.ident List.list -> ('a1, 'a2) code_iteration_params
     1139    -> (__ -> 'a2 -> 'a3 -> 'a3) -> __ -> 'a3 -> 'a3 **)
     1140let rec fold_code0 p globals xxx x_392 x_393 x_394 =
     1141  (let { cip_print_serialization_params = x; fold_code = yyy;
     1142     print_statementT = x0 } = xxx
     1143   in
     1144  Obj.magic yyy) __ x_392 x_393 x_394
     1145
     1146(** val print_statementT :
     1147    Joint.params -> AST.ident List.list -> ('a1, 'a2) code_iteration_params
     1148    -> 'a2 -> 'a1 **)
     1149let rec print_statementT p globals xxx =
     1150  xxx.print_statementT
    10151151
    10161152(** val code_iteration_params_inv_rect_Type4 :
    1017     Joint.params -> AST.ident List.list -> 'a1 code_iteration_params -> ((__
    1018     -> (__ -> Joint.joint_statement -> __ -> __) -> __ -> __ -> __) -> (__ ->
    1019     'a1) -> (__ -> 'a1) -> __ -> 'a2) -> 'a2 **)
    1020 let code_iteration_params_inv_rect_Type4 x2 x3 hterm h1 =
    1021   let hcut = code_iteration_params_rect_Type4 x2 x3 h1 hterm in hcut __
     1153    Joint.params -> AST.ident List.list -> ('a1, 'a2) code_iteration_params
     1154    -> ('a1 print_serialization_params -> (__ -> (__ -> 'a2 -> __ -> __) ->
     1155    __ -> __ -> __) -> ('a2 -> 'a1) -> __ -> 'a3) -> 'a3 **)
     1156let code_iteration_params_inv_rect_Type4 x2 x4 hterm h1 =
     1157  let hcut = code_iteration_params_rect_Type4 x2 x4 h1 hterm in hcut __
    10221158
    10231159(** val code_iteration_params_inv_rect_Type3 :
    1024     Joint.params -> AST.ident List.list -> 'a1 code_iteration_params -> ((__
    1025     -> (__ -> Joint.joint_statement -> __ -> __) -> __ -> __ -> __) -> (__ ->
    1026     'a1) -> (__ -> 'a1) -> __ -> 'a2) -> 'a2 **)
    1027 let code_iteration_params_inv_rect_Type3 x2 x3 hterm h1 =
    1028   let hcut = code_iteration_params_rect_Type3 x2 x3 h1 hterm in hcut __
     1160    Joint.params -> AST.ident List.list -> ('a1, 'a2) code_iteration_params
     1161    -> ('a1 print_serialization_params -> (__ -> (__ -> 'a2 -> __ -> __) ->
     1162    __ -> __ -> __) -> ('a2 -> 'a1) -> __ -> 'a3) -> 'a3 **)
     1163let code_iteration_params_inv_rect_Type3 x2 x4 hterm h1 =
     1164  let hcut = code_iteration_params_rect_Type3 x2 x4 h1 hterm in hcut __
    10291165
    10301166(** val code_iteration_params_inv_rect_Type2 :
    1031     Joint.params -> AST.ident List.list -> 'a1 code_iteration_params -> ((__
    1032     -> (__ -> Joint.joint_statement -> __ -> __) -> __ -> __ -> __) -> (__ ->
    1033     'a1) -> (__ -> 'a1) -> __ -> 'a2) -> 'a2 **)
    1034 let code_iteration_params_inv_rect_Type2 x2 x3 hterm h1 =
    1035   let hcut = code_iteration_params_rect_Type2 x2 x3 h1 hterm in hcut __
     1167    Joint.params -> AST.ident List.list -> ('a1, 'a2) code_iteration_params
     1168    -> ('a1 print_serialization_params -> (__ -> (__ -> 'a2 -> __ -> __) ->
     1169    __ -> __ -> __) -> ('a2 -> 'a1) -> __ -> 'a3) -> 'a3 **)
     1170let code_iteration_params_inv_rect_Type2 x2 x4 hterm h1 =
     1171  let hcut = code_iteration_params_rect_Type2 x2 x4 h1 hterm in hcut __
    10361172
    10371173(** val code_iteration_params_inv_rect_Type1 :
    1038     Joint.params -> AST.ident List.list -> 'a1 code_iteration_params -> ((__
    1039     -> (__ -> Joint.joint_statement -> __ -> __) -> __ -> __ -> __) -> (__ ->
    1040     'a1) -> (__ -> 'a1) -> __ -> 'a2) -> 'a2 **)
    1041 let code_iteration_params_inv_rect_Type1 x2 x3 hterm h1 =
    1042   let hcut = code_iteration_params_rect_Type1 x2 x3 h1 hterm in hcut __
     1174    Joint.params -> AST.ident List.list -> ('a1, 'a2) code_iteration_params
     1175    -> ('a1 print_serialization_params -> (__ -> (__ -> 'a2 -> __ -> __) ->
     1176    __ -> __ -> __) -> ('a2 -> 'a1) -> __ -> 'a3) -> 'a3 **)
     1177let code_iteration_params_inv_rect_Type1 x2 x4 hterm h1 =
     1178  let hcut = code_iteration_params_rect_Type1 x2 x4 h1 hterm in hcut __
    10431179
    10441180(** val code_iteration_params_inv_rect_Type0 :
    1045     Joint.params -> AST.ident List.list -> 'a1 code_iteration_params -> ((__
    1046     -> (__ -> Joint.joint_statement -> __ -> __) -> __ -> __ -> __) -> (__ ->
    1047     'a1) -> (__ -> 'a1) -> __ -> 'a2) -> 'a2 **)
    1048 let code_iteration_params_inv_rect_Type0 x2 x3 hterm h1 =
    1049   let hcut = code_iteration_params_rect_Type0 x2 x3 h1 hterm in hcut __
     1181    Joint.params -> AST.ident List.list -> ('a1, 'a2) code_iteration_params
     1182    -> ('a1 print_serialization_params -> (__ -> (__ -> 'a2 -> __ -> __) ->
     1183    __ -> __ -> __) -> ('a2 -> 'a1) -> __ -> 'a3) -> 'a3 **)
     1184let code_iteration_params_inv_rect_Type0 x2 x4 hterm h1 =
     1185  let hcut = code_iteration_params_rect_Type0 x2 x4 h1 hterm in hcut __
    10501186
    10511187(** val code_iteration_params_jmdiscr :
    1052     Joint.params -> AST.ident List.list -> 'a1 code_iteration_params -> 'a1
    1053     code_iteration_params -> __ **)
    1054 let code_iteration_params_jmdiscr a2 a3 x y =
     1188    Joint.params -> AST.ident List.list -> ('a1, 'a2) code_iteration_params
     1189    -> ('a1, 'a2) code_iteration_params -> __ **)
     1190let code_iteration_params_jmdiscr a2 a4 x y =
    10551191  Logic.eq_rect_Type2 x
    1056     (let { fold_code = a0; print_succ = a10; print_code_point = a20 } = x in
     1192    (let { cip_print_serialization_params = a0; fold_code = a10;
     1193       print_statementT = a20 } = x
     1194     in
    10571195    Obj.magic (fun _ dH -> dH __ __ __)) y
    10581196
     
    10851223     visit_graph next f (f pos a b) (next a) m' y)
    10861224
    1087 (** val graph_code_iteration_params :
    1088     Joint.graph_params -> AST.ident List.list -> 'a1 printing_params -> 'a1
    1089     code_iteration_params **)
    1090 let graph_code_iteration_params gp globals pp =
    1091   { fold_code = (fun _ f m a ->
    1092     visit_graph (fun stmt ->
    1093       match Joint.stmt_implicit_label (Joint.gp_to_p__o__stmt_pars gp)
    1094               globals stmt with
    1095       | Types.None -> Types.None
    1096       | Types.Some label -> let p = label in Types.Some p) (fun n ->
    1097       Obj.magic f n) a (Types.Some Positive.One) (let m' = Obj.magic m in m')
    1098       (Identifiers.id_map_size PreIdentifiers.LabelTag (Obj.magic m)));
    1099     print_succ = (Obj.magic pp.print_pass_ind.print_label);
    1100     print_code_point = (Obj.magic pp.print_pass_ind.print_label) }
    1101 
    11021225(** val print_list :
    11031226    'a1 printing_pass_independent_params -> 'a1 List.list -> 'a1 **)
     
    12111334(** val print_joint_statement :
    12121335    Joint.params -> AST.ident List.list -> 'a1 printing_params -> 'a1
    1213     code_iteration_params -> Joint.joint_statement -> 'a1 **)
     1336    print_serialization_params -> Joint.joint_statement -> 'a1 **)
    12141337let print_joint_statement p globals pp cip = function
    12151338| Joint.Sequential (js, arg1) ->
     
    12261349    ((pp.print_pass_ind.print_label arg3), List.Nil))))))))
    12271350
     1351(** val graph_print_serialization_params :
     1352    Joint.graph_params -> 'a1 printing_params -> 'a1
     1353    print_serialization_params **)
     1354let graph_print_serialization_params gp pp =
     1355  { print_succ = (Obj.magic pp.print_pass_ind.print_label);
     1356    print_code_point = (Obj.magic pp.print_pass_ind.print_label) }
     1357
     1358(** val graph_code_iteration_params :
     1359    Joint.graph_params -> AST.ident List.list -> 'a1 printing_params -> ('a1,
     1360    Joint.joint_statement) code_iteration_params **)
     1361let graph_code_iteration_params gp globals pp =
     1362  { cip_print_serialization_params =
     1363    (graph_print_serialization_params gp pp); fold_code = (fun _ f m a ->
     1364    visit_graph (fun stmt ->
     1365      match Joint.stmt_implicit_label (Joint.gp_to_p__o__stmt_pars gp)
     1366              globals stmt with
     1367      | Types.None -> Types.None
     1368      | Types.Some label -> let p = label in Types.Some p) (fun n ->
     1369      Obj.magic f n) a (Types.Some Positive.One) (let m' = Obj.magic m in m')
     1370      (Identifiers.id_map_size PreIdentifiers.LabelTag (Obj.magic m)));
     1371    print_statementT =
     1372    (print_joint_statement (Joint.graph_params_to_params gp) globals pp
     1373      (graph_print_serialization_params gp pp)) }
     1374
     1375(** val lin_print_serialization_params :
     1376    Joint.lin_params -> 'a1 printing_params -> 'a1 print_serialization_params **)
     1377let lin_print_serialization_params gp pp =
     1378  { print_succ = (fun x -> pp.print_pass_ind.print_empty); print_code_point =
     1379    (Obj.magic pp.print_pass_ind.print_nat) }
     1380
     1381(** val lin_code_iteration_params :
     1382    Joint.lin_params -> AST.ident List.list -> 'a1 printing_params -> ('a1,
     1383    (Graphs.label Types.option, Joint.joint_statement) Types.prod)
     1384    code_iteration_params **)
     1385let lin_code_iteration_params lp globals pp =
     1386  { cip_print_serialization_params = (lin_print_serialization_params lp pp);
     1387    fold_code = (fun _ f m a ->
     1388    (List.foldr (fun x res ->
     1389      let { Types.fst = pc; Types.snd = res' } = res in
     1390      { Types.fst = (Nat.S pc); Types.snd = (Obj.magic f pc x res') })
     1391      { Types.fst = Nat.O; Types.snd = a } (Obj.magic m)).Types.snd);
     1392    print_statementT = (fun linstr ->
     1393    match linstr.Types.fst with
     1394    | Types.None ->
     1395      print_joint_statement (Joint.lin_params_to_params lp) globals pp
     1396        (lin_print_serialization_params lp pp) linstr.Types.snd
     1397    | Types.Some l ->
     1398      print_list pp.print_pass_ind (List.Cons
     1399        ((pp.print_pass_ind.print_label l), (List.Cons
     1400        ((print_joint_statement (Joint.lin_params_to_params lp) globals pp
     1401           (lin_print_serialization_params lp pp) linstr.Types.snd),
     1402        List.Nil))))) }
     1403
    12281404(** val print_joint_internal_function :
    1229     Joint.params -> AST.ident List.list -> 'a1 code_iteration_params -> 'a1
    1230     printing_params -> Joint.joint_internal_function -> 'a1 List.list **)
     1405    Joint.params -> AST.ident List.list -> ('a2, 'a1) code_iteration_params
     1406    -> 'a2 printing_params -> Joint.joint_internal_function -> 'a2 List.list **)
    12311407let print_joint_internal_function p globals cip pp f =
    12321408  fold_code0 p globals cip (fun cp stmt acc -> List.Cons
    1233     ((print_list pp.print_pass_ind (List.Cons ((cip.print_code_point cp),
    1234        (List.Cons ((print_joint_statement p globals pp cip stmt),
    1235        List.Nil))))), acc)) f.Joint.joint_if_code List.Nil
     1409    ((print_list pp.print_pass_ind (List.Cons
     1410       ((cip.cip_print_serialization_params.print_code_point cp), (List.Cons
     1411       ((cip.print_statementT stmt), List.Nil))))), acc))
     1412    f.Joint.joint_if_code List.Nil
    12361413
    12371414(** val print_joint_function :
    1238     Joint.params -> AST.ident List.list -> 'a1 code_iteration_params -> 'a1
    1239     printing_params -> Joint.joint_function -> 'a1 List.list **)
     1415    Joint.params -> AST.ident List.list -> ('a2, 'a1) code_iteration_params
     1416    -> 'a2 printing_params -> Joint.joint_function -> 'a2 List.list **)
    12401417let print_joint_function p globals cip pp = function
    12411418| AST.Internal f0 ->
     
    12441421
    12451422(** val print_joint_program :
    1246     Joint.params -> 'a1 printing_params -> Joint.joint_program -> 'a1
    1247     code_iteration_params -> (AST.ident, 'a1 List.list) Types.prod List.list **)
     1423    Joint.params -> 'a2 printing_params -> Joint.joint_program -> ('a2, 'a1)
     1424    code_iteration_params -> (AST.ident, 'a2 List.list) Types.prod List.list **)
    12481425let print_joint_program p pp prog cip =
    12491426  List.foldr (fun f acc -> List.Cons ({ Types.fst = f.Types.fst; Types.snd =
  • extracted/joint_printer.mli

    r2951 r2982  
    218218                                                              -> 'string);
    219219                                                  print_Op2 : (BackEndOps.op2
    220                                                               -> 'string) }
     220                                                              -> 'string);
     221                                                  print_nat : (Nat.nat ->
     222                                                              'string) }
    221223
    222224val printing_pass_independent_params_rect_Type4 :
     
    224226  -> (AST.ident -> 'a1) -> (CostLabel.costlabel -> 'a1) -> (Graphs.label ->
    225227  'a1) -> (BackEndOps.opAccs -> 'a1) -> (BackEndOps.op1 -> 'a1) ->
    226   (BackEndOps.op2 -> 'a1) -> 'a2) -> 'a1 printing_pass_independent_params ->
    227   'a2
     228  (BackEndOps.op2 -> 'a1) -> (Nat.nat -> 'a1) -> 'a2) -> 'a1
     229  printing_pass_independent_params -> 'a2
    228230
    229231val printing_pass_independent_params_rect_Type5 :
     
    231233  -> (AST.ident -> 'a1) -> (CostLabel.costlabel -> 'a1) -> (Graphs.label ->
    232234  'a1) -> (BackEndOps.opAccs -> 'a1) -> (BackEndOps.op1 -> 'a1) ->
    233   (BackEndOps.op2 -> 'a1) -> 'a2) -> 'a1 printing_pass_independent_params ->
    234   'a2
     235  (BackEndOps.op2 -> 'a1) -> (Nat.nat -> 'a1) -> 'a2) -> 'a1
     236  printing_pass_independent_params -> 'a2
    235237
    236238val printing_pass_independent_params_rect_Type3 :
     
    238240  -> (AST.ident -> 'a1) -> (CostLabel.costlabel -> 'a1) -> (Graphs.label ->
    239241  'a1) -> (BackEndOps.opAccs -> 'a1) -> (BackEndOps.op1 -> 'a1) ->
    240   (BackEndOps.op2 -> 'a1) -> 'a2) -> 'a1 printing_pass_independent_params ->
    241   'a2
     242  (BackEndOps.op2 -> 'a1) -> (Nat.nat -> 'a1) -> 'a2) -> 'a1
     243  printing_pass_independent_params -> 'a2
    242244
    243245val printing_pass_independent_params_rect_Type2 :
     
    245247  -> (AST.ident -> 'a1) -> (CostLabel.costlabel -> 'a1) -> (Graphs.label ->
    246248  'a1) -> (BackEndOps.opAccs -> 'a1) -> (BackEndOps.op1 -> 'a1) ->
    247   (BackEndOps.op2 -> 'a1) -> 'a2) -> 'a1 printing_pass_independent_params ->
    248   'a2
     249  (BackEndOps.op2 -> 'a1) -> (Nat.nat -> 'a1) -> 'a2) -> 'a1
     250  printing_pass_independent_params -> 'a2
    249251
    250252val printing_pass_independent_params_rect_Type1 :
     
    252254  -> (AST.ident -> 'a1) -> (CostLabel.costlabel -> 'a1) -> (Graphs.label ->
    253255  'a1) -> (BackEndOps.opAccs -> 'a1) -> (BackEndOps.op1 -> 'a1) ->
    254   (BackEndOps.op2 -> 'a1) -> 'a2) -> 'a1 printing_pass_independent_params ->
    255   'a2
     256  (BackEndOps.op2 -> 'a1) -> (Nat.nat -> 'a1) -> 'a2) -> 'a1
     257  printing_pass_independent_params -> 'a2
    256258
    257259val printing_pass_independent_params_rect_Type0 :
     
    259261  -> (AST.ident -> 'a1) -> (CostLabel.costlabel -> 'a1) -> (Graphs.label ->
    260262  'a1) -> (BackEndOps.opAccs -> 'a1) -> (BackEndOps.op1 -> 'a1) ->
    261   (BackEndOps.op2 -> 'a1) -> 'a2) -> 'a1 printing_pass_independent_params ->
    262   'a2
     263  (BackEndOps.op2 -> 'a1) -> (Nat.nat -> 'a1) -> 'a2) -> 'a1
     264  printing_pass_independent_params -> 'a2
    263265
    264266val print_String :
     
    284286
    285287val print_Op2 : 'a1 printing_pass_independent_params -> BackEndOps.op2 -> 'a1
     288
     289val print_nat : 'a1 printing_pass_independent_params -> Nat.nat -> 'a1
    286290
    287291val printing_pass_independent_params_inv_rect_Type4 :
     
    289293  -> 'a1) -> ('a1 -> 'a1 -> 'a1) -> 'a1 -> (AST.ident -> 'a1) ->
    290294  (CostLabel.costlabel -> 'a1) -> (Graphs.label -> 'a1) -> (BackEndOps.opAccs
    291   -> 'a1) -> (BackEndOps.op1 -> 'a1) -> (BackEndOps.op2 -> 'a1) -> __ -> 'a2)
    292   -> 'a2
     295  -> 'a1) -> (BackEndOps.op1 -> 'a1) -> (BackEndOps.op2 -> 'a1) -> (Nat.nat
     296  -> 'a1) -> __ -> 'a2) -> 'a2
    293297
    294298val printing_pass_independent_params_inv_rect_Type3 :
     
    296300  -> 'a1) -> ('a1 -> 'a1 -> 'a1) -> 'a1 -> (AST.ident -> 'a1) ->
    297301  (CostLabel.costlabel -> 'a1) -> (Graphs.label -> 'a1) -> (BackEndOps.opAccs
    298   -> 'a1) -> (BackEndOps.op1 -> 'a1) -> (BackEndOps.op2 -> 'a1) -> __ -> 'a2)
    299   -> 'a2
     302  -> 'a1) -> (BackEndOps.op1 -> 'a1) -> (BackEndOps.op2 -> 'a1) -> (Nat.nat
     303  -> 'a1) -> __ -> 'a2) -> 'a2
    300304
    301305val printing_pass_independent_params_inv_rect_Type2 :
     
    303307  -> 'a1) -> ('a1 -> 'a1 -> 'a1) -> 'a1 -> (AST.ident -> 'a1) ->
    304308  (CostLabel.costlabel -> 'a1) -> (Graphs.label -> 'a1) -> (BackEndOps.opAccs
    305   -> 'a1) -> (BackEndOps.op1 -> 'a1) -> (BackEndOps.op2 -> 'a1) -> __ -> 'a2)
    306   -> 'a2
     309  -> 'a1) -> (BackEndOps.op1 -> 'a1) -> (BackEndOps.op2 -> 'a1) -> (Nat.nat
     310  -> 'a1) -> __ -> 'a2) -> 'a2
    307311
    308312val printing_pass_independent_params_inv_rect_Type1 :
     
    310314  -> 'a1) -> ('a1 -> 'a1 -> 'a1) -> 'a1 -> (AST.ident -> 'a1) ->
    311315  (CostLabel.costlabel -> 'a1) -> (Graphs.label -> 'a1) -> (BackEndOps.opAccs
    312   -> 'a1) -> (BackEndOps.op1 -> 'a1) -> (BackEndOps.op2 -> 'a1) -> __ -> 'a2)
    313   -> 'a2
     316  -> 'a1) -> (BackEndOps.op1 -> 'a1) -> (BackEndOps.op2 -> 'a1) -> (Nat.nat
     317  -> 'a1) -> __ -> 'a2) -> 'a2
    314318
    315319val printing_pass_independent_params_inv_rect_Type0 :
     
    317321  -> 'a1) -> ('a1 -> 'a1 -> 'a1) -> 'a1 -> (AST.ident -> 'a1) ->
    318322  (CostLabel.costlabel -> 'a1) -> (Graphs.label -> 'a1) -> (BackEndOps.opAccs
    319   -> 'a1) -> (BackEndOps.op1 -> 'a1) -> (BackEndOps.op2 -> 'a1) -> __ -> 'a2)
    320   -> 'a2
     323  -> 'a1) -> (BackEndOps.op1 -> 'a1) -> (BackEndOps.op2 -> 'a1) -> (Nat.nat
     324  -> 'a1) -> __ -> 'a2) -> 'a2
    321325
    322326val printing_pass_independent_params_jmdiscr :
     
    478482  printing_pass_independent_params
    479483
    480 type 'string code_iteration_params = { fold_code : (__ -> (__ ->
    481                                                    Joint.joint_statement ->
    482                                                    __ -> __) -> __ -> __ ->
    483                                                    __);
    484                                        print_succ : (__ -> 'string);
    485                                        print_code_point : (__ -> 'string) }
     484type 'string print_serialization_params = { print_succ : (__ -> 'string);
     485                                            print_code_point : (__ ->
     486                                                               'string) }
     487
     488val print_serialization_params_rect_Type4 :
     489  Joint.params -> ((__ -> 'a1) -> (__ -> 'a1) -> 'a2) -> 'a1
     490  print_serialization_params -> 'a2
     491
     492val print_serialization_params_rect_Type5 :
     493  Joint.params -> ((__ -> 'a1) -> (__ -> 'a1) -> 'a2) -> 'a1
     494  print_serialization_params -> 'a2
     495
     496val print_serialization_params_rect_Type3 :
     497  Joint.params -> ((__ -> 'a1) -> (__ -> 'a1) -> 'a2) -> 'a1
     498  print_serialization_params -> 'a2
     499
     500val print_serialization_params_rect_Type2 :
     501  Joint.params -> ((__ -> 'a1) -> (__ -> 'a1) -> 'a2) -> 'a1
     502  print_serialization_params -> 'a2
     503
     504val print_serialization_params_rect_Type1 :
     505  Joint.params -> ((__ -> 'a1) -> (__ -> 'a1) -> 'a2) -> 'a1
     506  print_serialization_params -> 'a2
     507
     508val print_serialization_params_rect_Type0 :
     509  Joint.params -> ((__ -> 'a1) -> (__ -> 'a1) -> 'a2) -> 'a1
     510  print_serialization_params -> 'a2
     511
     512val print_succ : Joint.params -> 'a1 print_serialization_params -> __ -> 'a1
     513
     514val print_code_point :
     515  Joint.params -> 'a1 print_serialization_params -> __ -> 'a1
     516
     517val print_serialization_params_inv_rect_Type4 :
     518  Joint.params -> 'a1 print_serialization_params -> ((__ -> 'a1) -> (__ ->
     519  'a1) -> __ -> 'a2) -> 'a2
     520
     521val print_serialization_params_inv_rect_Type3 :
     522  Joint.params -> 'a1 print_serialization_params -> ((__ -> 'a1) -> (__ ->
     523  'a1) -> __ -> 'a2) -> 'a2
     524
     525val print_serialization_params_inv_rect_Type2 :
     526  Joint.params -> 'a1 print_serialization_params -> ((__ -> 'a1) -> (__ ->
     527  'a1) -> __ -> 'a2) -> 'a2
     528
     529val print_serialization_params_inv_rect_Type1 :
     530  Joint.params -> 'a1 print_serialization_params -> ((__ -> 'a1) -> (__ ->
     531  'a1) -> __ -> 'a2) -> 'a2
     532
     533val print_serialization_params_inv_rect_Type0 :
     534  Joint.params -> 'a1 print_serialization_params -> ((__ -> 'a1) -> (__ ->
     535  'a1) -> __ -> 'a2) -> 'a2
     536
     537val print_serialization_params_discr :
     538  Joint.params -> 'a1 print_serialization_params -> 'a1
     539  print_serialization_params -> __
     540
     541val print_serialization_params_jmdiscr :
     542  Joint.params -> 'a1 print_serialization_params -> 'a1
     543  print_serialization_params -> __
     544
     545type ('string, 'statementT) code_iteration_params = { cip_print_serialization_params :
     546                                                      'string
     547                                                      print_serialization_params;
     548                                                      fold_code : (__ -> (__
     549                                                                  ->
     550                                                                  'statementT
     551                                                                  -> __ ->
     552                                                                  __) -> __
     553                                                                  -> __ ->
     554                                                                  __);
     555                                                      print_statementT :
     556                                                      ('statementT ->
     557                                                      'string) }
    486558
    487559val code_iteration_params_rect_Type4 :
    488   Joint.params -> AST.ident List.list -> ((__ -> (__ -> Joint.joint_statement
    489   -> __ -> __) -> __ -> __ -> __) -> (__ -> 'a1) -> (__ -> 'a1) -> 'a2) ->
    490   'a1 code_iteration_params -> 'a2
     560  Joint.params -> AST.ident List.list -> ('a1 print_serialization_params ->
     561  (__ -> (__ -> 'a2 -> __ -> __) -> __ -> __ -> __) -> ('a2 -> 'a1) -> 'a3)
     562  -> ('a1, 'a2) code_iteration_params -> 'a3
    491563
    492564val code_iteration_params_rect_Type5 :
    493   Joint.params -> AST.ident List.list -> ((__ -> (__ -> Joint.joint_statement
    494   -> __ -> __) -> __ -> __ -> __) -> (__ -> 'a1) -> (__ -> 'a1) -> 'a2) ->
    495   'a1 code_iteration_params -> 'a2
     565  Joint.params -> AST.ident List.list -> ('a1 print_serialization_params ->
     566  (__ -> (__ -> 'a2 -> __ -> __) -> __ -> __ -> __) -> ('a2 -> 'a1) -> 'a3)
     567  -> ('a1, 'a2) code_iteration_params -> 'a3
    496568
    497569val code_iteration_params_rect_Type3 :
    498   Joint.params -> AST.ident List.list -> ((__ -> (__ -> Joint.joint_statement
    499   -> __ -> __) -> __ -> __ -> __) -> (__ -> 'a1) -> (__ -> 'a1) -> 'a2) ->
    500   'a1 code_iteration_params -> 'a2
     570  Joint.params -> AST.ident List.list -> ('a1 print_serialization_params ->
     571  (__ -> (__ -> 'a2 -> __ -> __) -> __ -> __ -> __) -> ('a2 -> 'a1) -> 'a3)
     572  -> ('a1, 'a2) code_iteration_params -> 'a3
    501573
    502574val code_iteration_params_rect_Type2 :
    503   Joint.params -> AST.ident List.list -> ((__ -> (__ -> Joint.joint_statement
    504   -> __ -> __) -> __ -> __ -> __) -> (__ -> 'a1) -> (__ -> 'a1) -> 'a2) ->
    505   'a1 code_iteration_params -> 'a2
     575  Joint.params -> AST.ident List.list -> ('a1 print_serialization_params ->
     576  (__ -> (__ -> 'a2 -> __ -> __) -> __ -> __ -> __) -> ('a2 -> 'a1) -> 'a3)
     577  -> ('a1, 'a2) code_iteration_params -> 'a3
    506578
    507579val code_iteration_params_rect_Type1 :
    508   Joint.params -> AST.ident List.list -> ((__ -> (__ -> Joint.joint_statement
    509   -> __ -> __) -> __ -> __ -> __) -> (__ -> 'a1) -> (__ -> 'a1) -> 'a2) ->
    510   'a1 code_iteration_params -> 'a2
     580  Joint.params -> AST.ident List.list -> ('a1 print_serialization_params ->
     581  (__ -> (__ -> 'a2 -> __ -> __) -> __ -> __ -> __) -> ('a2 -> 'a1) -> 'a3)
     582  -> ('a1, 'a2) code_iteration_params -> 'a3
    511583
    512584val code_iteration_params_rect_Type0 :
    513   Joint.params -> AST.ident List.list -> ((__ -> (__ -> Joint.joint_statement
    514   -> __ -> __) -> __ -> __ -> __) -> (__ -> 'a1) -> (__ -> 'a1) -> 'a2) ->
    515   'a1 code_iteration_params -> 'a2
     585  Joint.params -> AST.ident List.list -> ('a1 print_serialization_params ->
     586  (__ -> (__ -> 'a2 -> __ -> __) -> __ -> __ -> __) -> ('a2 -> 'a1) -> 'a3)
     587  -> ('a1, 'a2) code_iteration_params -> 'a3
     588
     589val cip_print_serialization_params :
     590  Joint.params -> AST.ident List.list -> ('a1, 'a2) code_iteration_params ->
     591  'a1 print_serialization_params
    516592
    517593val fold_code0 :
    518   Joint.params -> AST.ident List.list -> 'a1 code_iteration_params -> (__ ->
    519   Joint.joint_statement -> 'a2 -> 'a2) -> __ -> 'a2 -> 'a2
    520 
    521 val print_succ :
    522   Joint.params -> AST.ident List.list -> 'a1 code_iteration_params -> __ ->
    523   'a1
    524 
    525 val print_code_point :
    526   Joint.params -> AST.ident List.list -> 'a1 code_iteration_params -> __ ->
    527   'a1
     594  Joint.params -> AST.ident List.list -> ('a1, 'a2) code_iteration_params ->
     595  (__ -> 'a2 -> 'a3 -> 'a3) -> __ -> 'a3 -> 'a3
     596
     597val print_statementT :
     598  Joint.params -> AST.ident List.list -> ('a1, 'a2) code_iteration_params ->
     599  'a2 -> 'a1
    528600
    529601val code_iteration_params_inv_rect_Type4 :
    530   Joint.params -> AST.ident List.list -> 'a1 code_iteration_params -> ((__ ->
    531   (__ -> Joint.joint_statement -> __ -> __) -> __ -> __ -> __) -> (__ -> 'a1)
    532   -> (__ -> 'a1) -> __ -> 'a2) -> 'a2
     602  Joint.params -> AST.ident List.list -> ('a1, 'a2) code_iteration_params ->
     603  ('a1 print_serialization_params -> (__ -> (__ -> 'a2 -> __ -> __) -> __ ->
     604  __ -> __) -> ('a2 -> 'a1) -> __ -> 'a3) -> 'a3
    533605
    534606val code_iteration_params_inv_rect_Type3 :
    535   Joint.params -> AST.ident List.list -> 'a1 code_iteration_params -> ((__ ->
    536   (__ -> Joint.joint_statement -> __ -> __) -> __ -> __ -> __) -> (__ -> 'a1)
    537   -> (__ -> 'a1) -> __ -> 'a2) -> 'a2
     607  Joint.params -> AST.ident List.list -> ('a1, 'a2) code_iteration_params ->
     608  ('a1 print_serialization_params -> (__ -> (__ -> 'a2 -> __ -> __) -> __ ->
     609  __ -> __) -> ('a2 -> 'a1) -> __ -> 'a3) -> 'a3
    538610
    539611val code_iteration_params_inv_rect_Type2 :
    540   Joint.params -> AST.ident List.list -> 'a1 code_iteration_params -> ((__ ->
    541   (__ -> Joint.joint_statement -> __ -> __) -> __ -> __ -> __) -> (__ -> 'a1)
    542   -> (__ -> 'a1) -> __ -> 'a2) -> 'a2
     612  Joint.params -> AST.ident List.list -> ('a1, 'a2) code_iteration_params ->
     613  ('a1 print_serialization_params -> (__ -> (__ -> 'a2 -> __ -> __) -> __ ->
     614  __ -> __) -> ('a2 -> 'a1) -> __ -> 'a3) -> 'a3
    543615
    544616val code_iteration_params_inv_rect_Type1 :
    545   Joint.params -> AST.ident List.list -> 'a1 code_iteration_params -> ((__ ->
    546   (__ -> Joint.joint_statement -> __ -> __) -> __ -> __ -> __) -> (__ -> 'a1)
    547   -> (__ -> 'a1) -> __ -> 'a2) -> 'a2
     617  Joint.params -> AST.ident List.list -> ('a1, 'a2) code_iteration_params ->
     618  ('a1 print_serialization_params -> (__ -> (__ -> 'a2 -> __ -> __) -> __ ->
     619  __ -> __) -> ('a2 -> 'a1) -> __ -> 'a3) -> 'a3
    548620
    549621val code_iteration_params_inv_rect_Type0 :
    550   Joint.params -> AST.ident List.list -> 'a1 code_iteration_params -> ((__ ->
    551   (__ -> Joint.joint_statement -> __ -> __) -> __ -> __ -> __) -> (__ -> 'a1)
    552   -> (__ -> 'a1) -> __ -> 'a2) -> 'a2
     622  Joint.params -> AST.ident List.list -> ('a1, 'a2) code_iteration_params ->
     623  ('a1 print_serialization_params -> (__ -> (__ -> 'a2 -> __ -> __) -> __ ->
     624  __ -> __) -> ('a2 -> 'a1) -> __ -> 'a3) -> 'a3
    553625
    554626val code_iteration_params_jmdiscr :
    555   Joint.params -> AST.ident List.list -> 'a1 code_iteration_params -> 'a1
    556   code_iteration_params -> __
     627  Joint.params -> AST.ident List.list -> ('a1, 'a2) code_iteration_params ->
     628  ('a1, 'a2) code_iteration_params -> __
    557629
    558630val pm_choose_with_pref :
     
    566638  Nat.nat -> 'a2
    567639
    568 val graph_code_iteration_params :
    569   Joint.graph_params -> AST.ident List.list -> 'a1 printing_params -> 'a1
    570   code_iteration_params
    571 
    572640val print_list : 'a1 printing_pass_independent_params -> 'a1 List.list -> 'a1
    573641
     
    586654val print_joint_statement :
    587655  Joint.params -> AST.ident List.list -> 'a1 printing_params -> 'a1
    588   code_iteration_params -> Joint.joint_statement -> 'a1
     656  print_serialization_params -> Joint.joint_statement -> 'a1
     657
     658val graph_print_serialization_params :
     659  Joint.graph_params -> 'a1 printing_params -> 'a1 print_serialization_params
     660
     661val graph_code_iteration_params :
     662  Joint.graph_params -> AST.ident List.list -> 'a1 printing_params -> ('a1,
     663  Joint.joint_statement) code_iteration_params
     664
     665val lin_print_serialization_params :
     666  Joint.lin_params -> 'a1 printing_params -> 'a1 print_serialization_params
     667
     668val lin_code_iteration_params :
     669  Joint.lin_params -> AST.ident List.list -> 'a1 printing_params -> ('a1,
     670  (Graphs.label Types.option, Joint.joint_statement) Types.prod)
     671  code_iteration_params
    589672
    590673val print_joint_internal_function :
    591   Joint.params -> AST.ident List.list -> 'a1 code_iteration_params -> 'a1
    592   printing_params -> Joint.joint_internal_function -> 'a1 List.list
     674  Joint.params -> AST.ident List.list -> ('a2, 'a1) code_iteration_params ->
     675  'a2 printing_params -> Joint.joint_internal_function -> 'a2 List.list
    593676
    594677val print_joint_function :
    595   Joint.params -> AST.ident List.list -> 'a1 code_iteration_params -> 'a1
    596   printing_params -> Joint.joint_function -> 'a1 List.list
     678  Joint.params -> AST.ident List.list -> ('a2, 'a1) code_iteration_params ->
     679  'a2 printing_params -> Joint.joint_function -> 'a2 List.list
    597680
    598681val print_joint_program :
    599   Joint.params -> 'a1 printing_params -> Joint.joint_program -> 'a1
    600   code_iteration_params -> (AST.ident, 'a1 List.list) Types.prod List.list
    601 
     682  Joint.params -> 'a2 printing_params -> Joint.joint_program -> ('a2, 'a1)
     683  code_iteration_params -> (AST.ident, 'a2 List.list) Types.prod List.list
     684
  • src/joint/joint_printer.ma

    r2859 r2982  
    4646 ; print_OpAccs: OpAccs → string
    4747 ; print_Op1: Op1 → string
    48  ; print_Op2: Op2 → string }.
     48 ; print_Op2: Op2 → string
     49 ; print_nat: nat → string }.
    4950
    5051record printing_params (string: Type[0]) (P: unserialized_params) : Type[0] ≝
     
    6667 }.
    6768
    68 record code_iteration_params (string: Type[0]) (p:params) (globals) : Type[1] ≝
    69  { fold_code:
    70     ∀A:Type[0].
    71      (code_point p → joint_statement p globals → A → A) →
    72       codeT p globals → A → A
    73  ; print_succ: succ … p → string
     69record print_serialization_params (string: Type[0]) (p:params) : Type[1] ≝
     70 { print_succ: succ … p → string
    7471 ; print_code_point: code_point p → string
     72 }.
     73
     74record code_iteration_params (string: Type[0]) (p:params) (statementT: Type[0])
     75  (globals) : Type[1] ≝
     76 { cip_print_serialization_params :> print_serialization_params string p
     77 ; fold_code:
     78    ∀A:Type[0]. (code_point p → statementT → A → A) → codeT p globals → A → A
     79 ; print_statementT: statementT → string
    7580 }.
    7681
     
    95100       let 〈pos,a,M'〉 ≝ res in
    96101        visit_graph A next B f (f pos a b) (next a) M' y ]].
    97 
    98 definition graph_code_iteration_params:
    99  ∀string,graph_params,globals.
    100   printing_params string (graph_params_to_params graph_params) →
    101    code_iteration_params string (graph_params_to_params graph_params) globals ≝
    102  λstring,gp,globals,pp.
    103   mk_code_iteration_params ???
    104    (λA.λf:code_point (graph_params_to_params …) → ?.λM.λa.
    105      visit_graph (joint_statement … gp globals)
    106      (λstmt. match stmt_implicit_label ?? stmt with
    107        [ None ⇒ None … | Some label ⇒ match label with [an_identifier p ⇒ Some … p]])
    108      ? (λn. f (an_identifier … n)) a (Some … one)
    109      (match M with [an_id_map M' ⇒ M']) (id_map_size … M))
    110    (print_label … pp) (print_label … pp).
    111102
    112103definition print_list:
     
    219210definition print_joint_statement:
    220211 ∀p:params.∀globals. ∀string. printing_params string p →
    221   code_iteration_params string p globals → joint_statement p globals → string ≝
     212  print_serialization_params string p → joint_statement p globals → string ≝
    222213 λp,globals,string,pp,cip,stmt.
    223214  match stmt with
     
    232223        print_label … pp arg3 ]].
    233224
     225definition graph_print_serialization_params:
     226 ∀string,graph_params.
     227  printing_params string (graph_params_to_params graph_params) →
     228   print_serialization_params string (graph_params_to_params graph_params) ≝
     229 λstring,gp,pp.
     230  mk_print_serialization_params … (print_label … pp) (print_label … pp).
     231
     232definition graph_code_iteration_params:
     233 ∀string,graph_params,globals.
     234  printing_params string (graph_params_to_params graph_params) →
     235   code_iteration_params string (graph_params_to_params graph_params) … globals ≝
     236 λstring,gp,globals,pp.
     237  mk_code_iteration_params …
     238   (graph_print_serialization_params … pp)
     239   (λA.λf:code_point (graph_params_to_params …) → ?.λM.λa.
     240     visit_graph (joint_statement … gp globals)
     241     (λstmt. match stmt_implicit_label ?? stmt with
     242       [ None ⇒ None … | Some label ⇒ match label with [an_identifier p ⇒ Some … p]])
     243     ? (λn. f (an_identifier … n)) a (Some … one)
     244     (match M with [an_id_map M' ⇒ M']) (id_map_size … M))
     245     (print_joint_statement … pp … (graph_print_serialization_params … pp)).
     246
     247definition lin_print_serialization_params:
     248 ∀string,lin_params.
     249  printing_params string (lin_params_to_params lin_params) →
     250   print_serialization_params string (lin_params_to_params lin_params) ≝
     251 λstring,gp,pp.
     252  mk_print_serialization_params … (λ_.print_empty … pp) (print_nat … pp).
     253
     254definition lin_code_iteration_params:
     255 ∀string,lin_params,globals.
     256  printing_params string (lin_params_to_params lin_params) →
     257   code_iteration_params string (lin_params_to_params lin_params) ? globals ≝
     258 λstring,lp,globals,pp.
     259  mk_code_iteration_params ?? (? × (joint_statement ??)) ?
     260   (lin_print_serialization_params … pp)
     261   (λA.λf:code_point (lin_params_to_params …) → ?.λM:codeT lp globals.
     262    λa.
     263     \snd (foldr ??
     264      (λx.λres. let 〈pc,res'〉 ≝ res in 〈S pc,f pc x res'〉)
     265      〈0,a〉 M))
     266     (λlinstr.
     267       match \fst linstr with
     268       [ None ⇒
     269          print_joint_statement … pp … (lin_print_serialization_params … pp)
     270           (\snd linstr)
     271       | Some l ⇒
     272          print_list ? pp
     273           [ print_label … pp l;
     274             print_joint_statement … pp … (lin_print_serialization_params … pp)
     275              (\snd linstr) ]]).
     276
    234277definition print_joint_internal_function:
    235  ∀p:params. ∀globals. ∀string. code_iteration_params string p globals →
     278 ∀p:params. ∀lines. ∀globals. ∀string. code_iteration_params string p lines globals →
    236279  printing_params string p → joint_internal_function p globals → list string
    237 ≝ λp,globals,string,cip,pp,f.
     280≝ λp,lines,globals,string,cip,pp,f.
    238281   fold_code … cip …
    239282    (λcp.λstmt.λacc.
    240       print_list pp
     283      print_list ? pp
    241284       [ print_code_point … cip cp;
    242          print_joint_statement … pp cip stmt ]::acc)
     285         print_statementT … cip stmt ]::acc)
    243286    (joint_if_code … f) [].
    244287
    245288definition print_joint_function:
    246  ∀p:params. ∀globals. ∀string. code_iteration_params string p globals → printing_params string p →
     289 ∀p:params. ∀lines. ∀globals. ∀string. code_iteration_params string p lines globals → printing_params string p →
    247290  joint_function p globals → list string ≝
    248  λp,globals,string,cip,pp,f.
     291 λp,lines,globals,string,cip,pp,f.
    249292  match f with
    250293  [ Internal f ⇒ print_joint_internal_function … cip … pp f
     
    252295
    253296definition print_joint_program:
    254  ∀p:params. ∀string.
     297 ∀p:params. ∀lines. ∀string.
    255298  printing_params string p →
    256299  ∀prog:joint_program p.
    257    code_iteration_params string p (map … (λx. \fst (\fst x)) (prog_vars ?? prog)) →
     300   code_iteration_params string p lines (map … (λx. \fst (\fst x)) (prog_vars ?? prog)) →
    258301   list (ident × (list string)) ≝
    259  λp,string,pp,prog,cip.
     302 λp,lines,string,pp,prog,cip.
    260303  foldr ?? (λf,acc. 〈\fst f,print_joint_function … cip … pp (\snd f)〉 :: acc)
    261304   [] (prog_funct … prog).
Note: See TracChangeset for help on using the changeset viewer.