Changeset 2854


Ignore:
Timestamp:
Mar 12, 2013, 5:53:56 PM (4 years ago)
Author:
sacerdot
Message:

Pretty printing of the LTL program.

Files:
6 added
17 edited

Legend:

Unmodified
Added
Removed
  • driver/build

    r2834 r2854  
    1212ocamlc -I ../Deliverables/D2.2/8051/lib -c -g error.ml
    1313ocamlc -I ../Deliverables/D2.2/8051/lib -c -g *.ml
    14 ocamlc -custom -g -I ../Deliverables/D2.2/8051/lib extracted.cmo  ../Deliverables/D2.2/8051/lib/libcparser.a ../Deliverables/D2.2/8051/lib/cparser.cma clightFromC.cmo clightParser.cmo clightPrinter.cmo IntelHex.cmo ASMPrinter.cmo error.cmo cerco.cmo -o cerco
     14ocamlc -custom -g -I ../Deliverables/D2.2/8051/lib extracted.cmo  ../Deliverables/D2.2/8051/lib/libcparser.a ../Deliverables/D2.2/8051/lib/cparser.cma clightFromC.cmo clightParser.cmo clightPrinter.cmo backendPrinter.cmo IntelHex.cmo ASMPrinter.cmo error.cmo cerco.cmo -o cerco
  • driver/cerco.ml

    r2834 r2854  
    4242  let rec infinity = Extracted.Nat.S infinity in
    4343  (fun pass prog ->
     44    if pass = Extracted.Compiler.Ltl_pass then
     45     print_string (BackendPrinter.print_LTL_program (fst (Obj.magic prog)));
    4446    Extracted.Semantics.run_and_print pass prog infinity
    4547     (fun p -> print_endline ("\n" ^ string_of_pass p ^ ":"); Extracted.Types.It)
  • extracted/aSMCosts.ml

    r2833 r2854  
    129129      Nat.O)))))))))))))))) (Obj.magic pc) cost_labels);
    130130    StructuredTraces.as_result = (fun x -> assert false (* absurd case *));
    131     StructuredTraces.as_call_ident = (fun x -> assert false (* absurd case *));
    132     StructuredTraces.as_tailcall_ident = (fun x -> assert false (* absurd case *)) }
     131    StructuredTraces.as_call_ident = (fun x -> assert false
     132    (* absurd case *)); StructuredTraces.as_tailcall_ident = (fun x ->
     133    assert false (* absurd case *)) }
    133134
    134135(** val trace_any_label_length :
     
    208209   | Nat.S program_size' ->
    209210     (fun _ ->
    210        (let { Types.fst = eta31776; Types.snd = ticks } =
     211       (let { Types.fst = eta9; Types.snd = ticks } =
    211212          Fetch.fetch code_memory' program_counter'
    212213        in
    213        let { Types.fst = instruction; Types.snd = program_counter'' } =
    214          eta31776
     214       let { Types.fst = instruction; Types.snd = program_counter'' } = eta9
    215215       in
    216216       (fun _ ->
  • extracted/compiler.ml

    r2842 r2854  
    510510  let i2 = Obj.magic observe Ertlptr_pass { Types.fst = p2; Types.snd = st1 }
    511511  in
    512   let { Types.fst = eta20; Types.snd = max_stack } =
     512  let { Types.fst = eta1115; Types.snd = max_stack } =
    513513    ERTLptrToLTL.ertlptr_to_ltl compute_fixpoint colour_graph p2
    514514  in
    515   let { Types.fst = p3; Types.snd = stack_cost0 } = eta20 in
     515  let { Types.fst = p3; Types.snd = stack_cost } = eta1115 in
    516516  let st2 = lookup_stack_cost (Joint.graph_params_to_params LTL.lTL) p3 in
    517517  let i3 = Obj.magic observe Ltl_pass { Types.fst = p3; Types.snd = st2 } in
     
    526526          (LINToASM.lin_to_asm p4))) (fun p5 ->
    527527      Monad.m_return0 (Monad.max_def Errors.res0) { Types.fst = { Types.fst =
    528         p5; Types.snd = stack_cost0 }; Types.snd = max_stack }))
     528        p5; Types.snd = stack_cost }; Types.snd = max_stack }))
    529529
    530530open Assembly
     
    586586    Csyntax.clight_program -> Label.clight_cost_map -> 'a1) ->
    587587    compiler_output -> 'a1 **)
    588 let rec compiler_output_rect_Type4 h_mk_compiler_output x_172 =
     588let rec compiler_output_rect_Type4 h_mk_compiler_output x_3610 =
    589589  let { c_labelled_object_code = c_labelled_object_code0; c_stack_cost =
    590590    c_stack_cost0; c_max_stack = c_max_stack0; c_labelled_clight =
    591     c_labelled_clight0; c_clight_cost_map = c_clight_cost_map0 } = x_172
     591    c_labelled_clight0; c_clight_cost_map = c_clight_cost_map0 } = x_3610
    592592  in
    593593  h_mk_compiler_output c_labelled_object_code0 c_stack_cost0 c_max_stack0
     
    598598    Csyntax.clight_program -> Label.clight_cost_map -> 'a1) ->
    599599    compiler_output -> 'a1 **)
    600 let rec compiler_output_rect_Type5 h_mk_compiler_output x_174 =
     600let rec compiler_output_rect_Type5 h_mk_compiler_output x_3612 =
    601601  let { c_labelled_object_code = c_labelled_object_code0; c_stack_cost =
    602602    c_stack_cost0; c_max_stack = c_max_stack0; c_labelled_clight =
    603     c_labelled_clight0; c_clight_cost_map = c_clight_cost_map0 } = x_174
     603    c_labelled_clight0; c_clight_cost_map = c_clight_cost_map0 } = x_3612
    604604  in
    605605  h_mk_compiler_output c_labelled_object_code0 c_stack_cost0 c_max_stack0
     
    610610    Csyntax.clight_program -> Label.clight_cost_map -> 'a1) ->
    611611    compiler_output -> 'a1 **)
    612 let rec compiler_output_rect_Type3 h_mk_compiler_output x_176 =
     612let rec compiler_output_rect_Type3 h_mk_compiler_output x_3614 =
    613613  let { c_labelled_object_code = c_labelled_object_code0; c_stack_cost =
    614614    c_stack_cost0; c_max_stack = c_max_stack0; c_labelled_clight =
    615     c_labelled_clight0; c_clight_cost_map = c_clight_cost_map0 } = x_176
     615    c_labelled_clight0; c_clight_cost_map = c_clight_cost_map0 } = x_3614
    616616  in
    617617  h_mk_compiler_output c_labelled_object_code0 c_stack_cost0 c_max_stack0
     
    622622    Csyntax.clight_program -> Label.clight_cost_map -> 'a1) ->
    623623    compiler_output -> 'a1 **)
    624 let rec compiler_output_rect_Type2 h_mk_compiler_output x_178 =
     624let rec compiler_output_rect_Type2 h_mk_compiler_output x_3616 =
    625625  let { c_labelled_object_code = c_labelled_object_code0; c_stack_cost =
    626626    c_stack_cost0; c_max_stack = c_max_stack0; c_labelled_clight =
    627     c_labelled_clight0; c_clight_cost_map = c_clight_cost_map0 } = x_178
     627    c_labelled_clight0; c_clight_cost_map = c_clight_cost_map0 } = x_3616
    628628  in
    629629  h_mk_compiler_output c_labelled_object_code0 c_stack_cost0 c_max_stack0
     
    634634    Csyntax.clight_program -> Label.clight_cost_map -> 'a1) ->
    635635    compiler_output -> 'a1 **)
    636 let rec compiler_output_rect_Type1 h_mk_compiler_output x_180 =
     636let rec compiler_output_rect_Type1 h_mk_compiler_output x_3618 =
    637637  let { c_labelled_object_code = c_labelled_object_code0; c_stack_cost =
    638638    c_stack_cost0; c_max_stack = c_max_stack0; c_labelled_clight =
    639     c_labelled_clight0; c_clight_cost_map = c_clight_cost_map0 } = x_180
     639    c_labelled_clight0; c_clight_cost_map = c_clight_cost_map0 } = x_3618
    640640  in
    641641  h_mk_compiler_output c_labelled_object_code0 c_stack_cost0 c_max_stack0
     
    646646    Csyntax.clight_program -> Label.clight_cost_map -> 'a1) ->
    647647    compiler_output -> 'a1 **)
    648 let rec compiler_output_rect_Type0 h_mk_compiler_output x_182 =
     648let rec compiler_output_rect_Type0 h_mk_compiler_output x_3620 =
    649649  let { c_labelled_object_code = c_labelled_object_code0; c_stack_cost =
    650650    c_stack_cost0; c_max_stack = c_max_stack0; c_labelled_clight =
    651     c_labelled_clight0; c_clight_cost_map = c_clight_cost_map0 } = x_182
     651    c_labelled_clight0; c_clight_cost_map = c_clight_cost_map0 } = x_3620
    652652  in
    653653  h_mk_compiler_output c_labelled_object_code0 c_stack_cost0 c_max_stack0
     
    734734      (Obj.magic (front_end observe p)) (fun init_cost p' p0 ->
    735735      Monad.m_bind3 (Monad.max_def Errors.res0)
    736         (Obj.magic (back_end observe p0)) (fun p1 stack_cost0 max_stack ->
     736        (Obj.magic (back_end observe p0)) (fun p1 stack_cost max_stack ->
    737737        Monad.m_bind0 (Monad.max_def Errors.res0) (Obj.magic (assembler p1))
    738738          (fun p2 ->
     
    743743          in
    744744          Monad.m_return0 (Monad.max_def Errors.res0)
    745             { c_labelled_object_code = p2; c_stack_cost = stack_cost0;
     745            { c_labelled_object_code = p2; c_stack_cost = stack_cost;
    746746            c_max_stack = max_stack; c_labelled_clight = p';
    747747            c_clight_cost_map = k' }))))
  • extracted/eRTL.ml

    r2827 r2854  
    112112    (Registers.register -> 'a1) -> (I8051.register -> 'a1) -> move_dst -> 'a1 **)
    113113let rec move_dst_rect_Type4 h_PSD h_HDW = function
    114 | PSD x_21247 -> h_PSD x_21247
    115 | HDW x_21248 -> h_HDW x_21248
     114| PSD x_1252 -> h_PSD x_1252
     115| HDW x_1253 -> h_HDW x_1253
    116116
    117117(** val move_dst_rect_Type5 :
    118118    (Registers.register -> 'a1) -> (I8051.register -> 'a1) -> move_dst -> 'a1 **)
    119119let rec move_dst_rect_Type5 h_PSD h_HDW = function
    120 | PSD x_21252 -> h_PSD x_21252
    121 | HDW x_21253 -> h_HDW x_21253
     120| PSD x_1257 -> h_PSD x_1257
     121| HDW x_1258 -> h_HDW x_1258
    122122
    123123(** val move_dst_rect_Type3 :
    124124    (Registers.register -> 'a1) -> (I8051.register -> 'a1) -> move_dst -> 'a1 **)
    125125let rec move_dst_rect_Type3 h_PSD h_HDW = function
    126 | PSD x_21257 -> h_PSD x_21257
    127 | HDW x_21258 -> h_HDW x_21258
     126| PSD x_1262 -> h_PSD x_1262
     127| HDW x_1263 -> h_HDW x_1263
    128128
    129129(** val move_dst_rect_Type2 :
    130130    (Registers.register -> 'a1) -> (I8051.register -> 'a1) -> move_dst -> 'a1 **)
    131131let rec move_dst_rect_Type2 h_PSD h_HDW = function
    132 | PSD x_21262 -> h_PSD x_21262
    133 | HDW x_21263 -> h_HDW x_21263
     132| PSD x_1267 -> h_PSD x_1267
     133| HDW x_1268 -> h_HDW x_1268
    134134
    135135(** val move_dst_rect_Type1 :
    136136    (Registers.register -> 'a1) -> (I8051.register -> 'a1) -> move_dst -> 'a1 **)
    137137let rec move_dst_rect_Type1 h_PSD h_HDW = function
    138 | PSD x_21267 -> h_PSD x_21267
    139 | HDW x_21268 -> h_HDW x_21268
     138| PSD x_1272 -> h_PSD x_1272
     139| HDW x_1273 -> h_HDW x_1273
    140140
    141141(** val move_dst_rect_Type0 :
    142142    (Registers.register -> 'a1) -> (I8051.register -> 'a1) -> move_dst -> 'a1 **)
    143143let rec move_dst_rect_Type0 h_PSD h_HDW = function
    144 | PSD x_21272 -> h_PSD x_21272
    145 | HDW x_21273 -> h_HDW x_21273
     144| PSD x_1277 -> h_PSD x_1277
     145| HDW x_1278 -> h_HDW x_1278
    146146
    147147(** val move_dst_inv_rect_Type4 :
     
    338338| Ertl_new_frame -> h_ertl_new_frame
    339339| Ertl_del_frame -> h_ertl_del_frame
    340 | Ertl_frame_size x_21312 -> h_ertl_frame_size x_21312
     340| Ertl_frame_size x_1317 -> h_ertl_frame_size x_1317
    341341
    342342(** val ertl_seq_rect_Type5 :
     
    345345| Ertl_new_frame -> h_ertl_new_frame
    346346| Ertl_del_frame -> h_ertl_del_frame
    347 | Ertl_frame_size x_21317 -> h_ertl_frame_size x_21317
     347| Ertl_frame_size x_1322 -> h_ertl_frame_size x_1322
    348348
    349349(** val ertl_seq_rect_Type3 :
     
    352352| Ertl_new_frame -> h_ertl_new_frame
    353353| Ertl_del_frame -> h_ertl_del_frame
    354 | Ertl_frame_size x_21322 -> h_ertl_frame_size x_21322
     354| Ertl_frame_size x_1327 -> h_ertl_frame_size x_1327
    355355
    356356(** val ertl_seq_rect_Type2 :
     
    359359| Ertl_new_frame -> h_ertl_new_frame
    360360| Ertl_del_frame -> h_ertl_del_frame
    361 | Ertl_frame_size x_21327 -> h_ertl_frame_size x_21327
     361| Ertl_frame_size x_1332 -> h_ertl_frame_size x_1332
    362362
    363363(** val ertl_seq_rect_Type1 :
     
    366366| Ertl_new_frame -> h_ertl_new_frame
    367367| Ertl_del_frame -> h_ertl_del_frame
    368 | Ertl_frame_size x_21332 -> h_ertl_frame_size x_21332
     368| Ertl_frame_size x_1337 -> h_ertl_frame_size x_1337
    369369
    370370(** val ertl_seq_rect_Type0 :
     
    373373| Ertl_new_frame -> h_ertl_new_frame
    374374| Ertl_del_frame -> h_ertl_del_frame
    375 | Ertl_frame_size x_21337 -> h_ertl_frame_size x_21337
     375| Ertl_frame_size x_1342 -> h_ertl_frame_size x_1342
    376376
    377377(** val ertl_seq_inv_rect_Type4 :
  • extracted/eRTLptr.ml

    r2827 r2854  
    116116    (Registers.register -> Graphs.label -> 'a1) -> ertlptr_seq -> 'a1 **)
    117117let rec ertlptr_seq_rect_Type4 h_ertlptr_ertl h_LOW_ADDRESS h_HIGH_ADDRESS = function
    118 | Ertlptr_ertl x_21381 -> h_ertlptr_ertl x_21381
    119 | LOW_ADDRESS (x_21383, x_21382) -> h_LOW_ADDRESS x_21383 x_21382
    120 | HIGH_ADDRESS (x_21385, x_21384) -> h_HIGH_ADDRESS x_21385 x_21384
     118| Ertlptr_ertl x_1386 -> h_ertlptr_ertl x_1386
     119| LOW_ADDRESS (x_1388, x_1387) -> h_LOW_ADDRESS x_1388 x_1387
     120| HIGH_ADDRESS (x_1390, x_1389) -> h_HIGH_ADDRESS x_1390 x_1389
    121121
    122122(** val ertlptr_seq_rect_Type5 :
     
    124124    (Registers.register -> Graphs.label -> 'a1) -> ertlptr_seq -> 'a1 **)
    125125let rec ertlptr_seq_rect_Type5 h_ertlptr_ertl h_LOW_ADDRESS h_HIGH_ADDRESS = function
    126 | Ertlptr_ertl x_21390 -> h_ertlptr_ertl x_21390
    127 | LOW_ADDRESS (x_21392, x_21391) -> h_LOW_ADDRESS x_21392 x_21391
    128 | HIGH_ADDRESS (x_21394, x_21393) -> h_HIGH_ADDRESS x_21394 x_21393
     126| Ertlptr_ertl x_1395 -> h_ertlptr_ertl x_1395
     127| LOW_ADDRESS (x_1397, x_1396) -> h_LOW_ADDRESS x_1397 x_1396
     128| HIGH_ADDRESS (x_1399, x_1398) -> h_HIGH_ADDRESS x_1399 x_1398
    129129
    130130(** val ertlptr_seq_rect_Type3 :
     
    132132    (Registers.register -> Graphs.label -> 'a1) -> ertlptr_seq -> 'a1 **)
    133133let rec ertlptr_seq_rect_Type3 h_ertlptr_ertl h_LOW_ADDRESS h_HIGH_ADDRESS = function
    134 | Ertlptr_ertl x_21399 -> h_ertlptr_ertl x_21399
    135 | LOW_ADDRESS (x_21401, x_21400) -> h_LOW_ADDRESS x_21401 x_21400
    136 | HIGH_ADDRESS (x_21403, x_21402) -> h_HIGH_ADDRESS x_21403 x_21402
     134| Ertlptr_ertl x_1404 -> h_ertlptr_ertl x_1404
     135| LOW_ADDRESS (x_1406, x_1405) -> h_LOW_ADDRESS x_1406 x_1405
     136| HIGH_ADDRESS (x_1408, x_1407) -> h_HIGH_ADDRESS x_1408 x_1407
    137137
    138138(** val ertlptr_seq_rect_Type2 :
     
    140140    (Registers.register -> Graphs.label -> 'a1) -> ertlptr_seq -> 'a1 **)
    141141let rec ertlptr_seq_rect_Type2 h_ertlptr_ertl h_LOW_ADDRESS h_HIGH_ADDRESS = function
    142 | Ertlptr_ertl x_21408 -> h_ertlptr_ertl x_21408
    143 | LOW_ADDRESS (x_21410, x_21409) -> h_LOW_ADDRESS x_21410 x_21409
    144 | HIGH_ADDRESS (x_21412, x_21411) -> h_HIGH_ADDRESS x_21412 x_21411
     142| Ertlptr_ertl x_1413 -> h_ertlptr_ertl x_1413
     143| LOW_ADDRESS (x_1415, x_1414) -> h_LOW_ADDRESS x_1415 x_1414
     144| HIGH_ADDRESS (x_1417, x_1416) -> h_HIGH_ADDRESS x_1417 x_1416
    145145
    146146(** val ertlptr_seq_rect_Type1 :
     
    148148    (Registers.register -> Graphs.label -> 'a1) -> ertlptr_seq -> 'a1 **)
    149149let rec ertlptr_seq_rect_Type1 h_ertlptr_ertl h_LOW_ADDRESS h_HIGH_ADDRESS = function
    150 | Ertlptr_ertl x_21417 -> h_ertlptr_ertl x_21417
    151 | LOW_ADDRESS (x_21419, x_21418) -> h_LOW_ADDRESS x_21419 x_21418
    152 | HIGH_ADDRESS (x_21421, x_21420) -> h_HIGH_ADDRESS x_21421 x_21420
     150| Ertlptr_ertl x_1422 -> h_ertlptr_ertl x_1422
     151| LOW_ADDRESS (x_1424, x_1423) -> h_LOW_ADDRESS x_1424 x_1423
     152| HIGH_ADDRESS (x_1426, x_1425) -> h_HIGH_ADDRESS x_1426 x_1425
    153153
    154154(** val ertlptr_seq_rect_Type0 :
     
    156156    (Registers.register -> Graphs.label -> 'a1) -> ertlptr_seq -> 'a1 **)
    157157let rec ertlptr_seq_rect_Type0 h_ertlptr_ertl h_LOW_ADDRESS h_HIGH_ADDRESS = function
    158 | Ertlptr_ertl x_21426 -> h_ertlptr_ertl x_21426
    159 | LOW_ADDRESS (x_21428, x_21427) -> h_LOW_ADDRESS x_21428 x_21427
    160 | HIGH_ADDRESS (x_21430, x_21429) -> h_HIGH_ADDRESS x_21430 x_21429
     158| Ertlptr_ertl x_1431 -> h_ertlptr_ertl x_1431
     159| LOW_ADDRESS (x_1433, x_1432) -> h_LOW_ADDRESS x_1433 x_1432
     160| HIGH_ADDRESS (x_1435, x_1434) -> h_HIGH_ADDRESS x_1435 x_1434
    161161
    162162(** val ertlptr_seq_inv_rect_Type4 :
  • extracted/eRTLptrToLTL.ml

    r2844 r2854  
    167167    arg_decision -> 'a1 **)
    168168let rec arg_decision_rect_Type4 h_arg_decision_colour h_arg_decision_spill h_arg_decision_imm = function
    169 | Arg_decision_colour x_21936 -> h_arg_decision_colour x_21936
    170 | Arg_decision_spill x_21937 -> h_arg_decision_spill x_21937
    171 | Arg_decision_imm x_21938 -> h_arg_decision_imm x_21938
     169| Arg_decision_colour x_2002 -> h_arg_decision_colour x_2002
     170| Arg_decision_spill x_2003 -> h_arg_decision_spill x_2003
     171| Arg_decision_imm x_2004 -> h_arg_decision_imm x_2004
    172172
    173173(** val arg_decision_rect_Type5 :
     
    175175    arg_decision -> 'a1 **)
    176176let rec arg_decision_rect_Type5 h_arg_decision_colour h_arg_decision_spill h_arg_decision_imm = function
    177 | Arg_decision_colour x_21943 -> h_arg_decision_colour x_21943
    178 | Arg_decision_spill x_21944 -> h_arg_decision_spill x_21944
    179 | Arg_decision_imm x_21945 -> h_arg_decision_imm x_21945
     177| Arg_decision_colour x_2009 -> h_arg_decision_colour x_2009
     178| Arg_decision_spill x_2010 -> h_arg_decision_spill x_2010
     179| Arg_decision_imm x_2011 -> h_arg_decision_imm x_2011
    180180
    181181(** val arg_decision_rect_Type3 :
     
    183183    arg_decision -> 'a1 **)
    184184let rec arg_decision_rect_Type3 h_arg_decision_colour h_arg_decision_spill h_arg_decision_imm = function
    185 | Arg_decision_colour x_21950 -> h_arg_decision_colour x_21950
    186 | Arg_decision_spill x_21951 -> h_arg_decision_spill x_21951
    187 | Arg_decision_imm x_21952 -> h_arg_decision_imm x_21952
     185| Arg_decision_colour x_2016 -> h_arg_decision_colour x_2016
     186| Arg_decision_spill x_2017 -> h_arg_decision_spill x_2017
     187| Arg_decision_imm x_2018 -> h_arg_decision_imm x_2018
    188188
    189189(** val arg_decision_rect_Type2 :
     
    191191    arg_decision -> 'a1 **)
    192192let rec arg_decision_rect_Type2 h_arg_decision_colour h_arg_decision_spill h_arg_decision_imm = function
    193 | Arg_decision_colour x_21957 -> h_arg_decision_colour x_21957
    194 | Arg_decision_spill x_21958 -> h_arg_decision_spill x_21958
    195 | Arg_decision_imm x_21959 -> h_arg_decision_imm x_21959
     193| Arg_decision_colour x_2023 -> h_arg_decision_colour x_2023
     194| Arg_decision_spill x_2024 -> h_arg_decision_spill x_2024
     195| Arg_decision_imm x_2025 -> h_arg_decision_imm x_2025
    196196
    197197(** val arg_decision_rect_Type1 :
     
    199199    arg_decision -> 'a1 **)
    200200let rec arg_decision_rect_Type1 h_arg_decision_colour h_arg_decision_spill h_arg_decision_imm = function
    201 | Arg_decision_colour x_21964 -> h_arg_decision_colour x_21964
    202 | Arg_decision_spill x_21965 -> h_arg_decision_spill x_21965
    203 | Arg_decision_imm x_21966 -> h_arg_decision_imm x_21966
     201| Arg_decision_colour x_2030 -> h_arg_decision_colour x_2030
     202| Arg_decision_spill x_2031 -> h_arg_decision_spill x_2031
     203| Arg_decision_imm x_2032 -> h_arg_decision_imm x_2032
    204204
    205205(** val arg_decision_rect_Type0 :
     
    207207    arg_decision -> 'a1 **)
    208208let rec arg_decision_rect_Type0 h_arg_decision_colour h_arg_decision_spill h_arg_decision_imm = function
    209 | Arg_decision_colour x_21971 -> h_arg_decision_colour x_21971
    210 | Arg_decision_spill x_21972 -> h_arg_decision_spill x_21972
    211 | Arg_decision_imm x_21973 -> h_arg_decision_imm x_21973
     209| Arg_decision_colour x_2037 -> h_arg_decision_colour x_2037
     210| Arg_decision_spill x_2038 -> h_arg_decision_spill x_2038
     211| Arg_decision_imm x_2039 -> h_arg_decision_imm x_2039
    212212
    213213(** val arg_decision_inv_rect_Type4 :
  • extracted/interference.ml

    r2827 r2854  
    122122    (Nat.nat -> 'a1) -> (I8051.register -> 'a1) -> decision -> 'a1 **)
    123123let rec decision_rect_Type4 h_decision_spill h_decision_colour = function
    124 | Decision_spill x_21838 -> h_decision_spill x_21838
    125 | Decision_colour x_21839 -> h_decision_colour x_21839
     124| Decision_spill x_1903 -> h_decision_spill x_1903
     125| Decision_colour x_1904 -> h_decision_colour x_1904
    126126
    127127(** val decision_rect_Type5 :
    128128    (Nat.nat -> 'a1) -> (I8051.register -> 'a1) -> decision -> 'a1 **)
    129129let rec decision_rect_Type5 h_decision_spill h_decision_colour = function
    130 | Decision_spill x_21843 -> h_decision_spill x_21843
    131 | Decision_colour x_21844 -> h_decision_colour x_21844
     130| Decision_spill x_1908 -> h_decision_spill x_1908
     131| Decision_colour x_1909 -> h_decision_colour x_1909
    132132
    133133(** val decision_rect_Type3 :
    134134    (Nat.nat -> 'a1) -> (I8051.register -> 'a1) -> decision -> 'a1 **)
    135135let rec decision_rect_Type3 h_decision_spill h_decision_colour = function
    136 | Decision_spill x_21848 -> h_decision_spill x_21848
    137 | Decision_colour x_21849 -> h_decision_colour x_21849
     136| Decision_spill x_1913 -> h_decision_spill x_1913
     137| Decision_colour x_1914 -> h_decision_colour x_1914
    138138
    139139(** val decision_rect_Type2 :
    140140    (Nat.nat -> 'a1) -> (I8051.register -> 'a1) -> decision -> 'a1 **)
    141141let rec decision_rect_Type2 h_decision_spill h_decision_colour = function
    142 | Decision_spill x_21853 -> h_decision_spill x_21853
    143 | Decision_colour x_21854 -> h_decision_colour x_21854
     142| Decision_spill x_1918 -> h_decision_spill x_1918
     143| Decision_colour x_1919 -> h_decision_colour x_1919
    144144
    145145(** val decision_rect_Type1 :
    146146    (Nat.nat -> 'a1) -> (I8051.register -> 'a1) -> decision -> 'a1 **)
    147147let rec decision_rect_Type1 h_decision_spill h_decision_colour = function
    148 | Decision_spill x_21858 -> h_decision_spill x_21858
    149 | Decision_colour x_21859 -> h_decision_colour x_21859
     148| Decision_spill x_1923 -> h_decision_spill x_1923
     149| Decision_colour x_1924 -> h_decision_colour x_1924
    150150
    151151(** val decision_rect_Type0 :
    152152    (Nat.nat -> 'a1) -> (I8051.register -> 'a1) -> decision -> 'a1 **)
    153153let rec decision_rect_Type0 h_decision_spill h_decision_colour = function
    154 | Decision_spill x_21863 -> h_decision_spill x_21863
    155 | Decision_colour x_21864 -> h_decision_colour x_21864
     154| Decision_spill x_1928 -> h_decision_spill x_1928
     155| Decision_colour x_1929 -> h_decision_colour x_1929
    156156
    157157(** val decision_inv_rect_Type4 :
     
    205205    Fixpoints.valuation -> ((Liveness.vertex -> decision) -> Nat.nat -> __ ->
    206206    __ -> 'a1) -> coloured_graph -> 'a1 **)
    207 let rec coloured_graph_rect_Type4 after h_mk_coloured_graph x_21899 =
    208   let { colouring = colouring0; spilled_no = spilled_no0 } = x_21899 in
     207let rec coloured_graph_rect_Type4 after h_mk_coloured_graph x_1964 =
     208  let { colouring = colouring0; spilled_no = spilled_no0 } = x_1964 in
    209209  h_mk_coloured_graph colouring0 spilled_no0 __ __
    210210
     
    212212    Fixpoints.valuation -> ((Liveness.vertex -> decision) -> Nat.nat -> __ ->
    213213    __ -> 'a1) -> coloured_graph -> 'a1 **)
    214 let rec coloured_graph_rect_Type5 after h_mk_coloured_graph x_21901 =
    215   let { colouring = colouring0; spilled_no = spilled_no0 } = x_21901 in
     214let rec coloured_graph_rect_Type5 after h_mk_coloured_graph x_1966 =
     215  let { colouring = colouring0; spilled_no = spilled_no0 } = x_1966 in
    216216  h_mk_coloured_graph colouring0 spilled_no0 __ __
    217217
     
    219219    Fixpoints.valuation -> ((Liveness.vertex -> decision) -> Nat.nat -> __ ->
    220220    __ -> 'a1) -> coloured_graph -> 'a1 **)
    221 let rec coloured_graph_rect_Type3 after h_mk_coloured_graph x_21903 =
    222   let { colouring = colouring0; spilled_no = spilled_no0 } = x_21903 in
     221let rec coloured_graph_rect_Type3 after h_mk_coloured_graph x_1968 =
     222  let { colouring = colouring0; spilled_no = spilled_no0 } = x_1968 in
    223223  h_mk_coloured_graph colouring0 spilled_no0 __ __
    224224
     
    226226    Fixpoints.valuation -> ((Liveness.vertex -> decision) -> Nat.nat -> __ ->
    227227    __ -> 'a1) -> coloured_graph -> 'a1 **)
    228 let rec coloured_graph_rect_Type2 after h_mk_coloured_graph x_21905 =
    229   let { colouring = colouring0; spilled_no = spilled_no0 } = x_21905 in
     228let rec coloured_graph_rect_Type2 after h_mk_coloured_graph x_1970 =
     229  let { colouring = colouring0; spilled_no = spilled_no0 } = x_1970 in
    230230  h_mk_coloured_graph colouring0 spilled_no0 __ __
    231231
     
    233233    Fixpoints.valuation -> ((Liveness.vertex -> decision) -> Nat.nat -> __ ->
    234234    __ -> 'a1) -> coloured_graph -> 'a1 **)
    235 let rec coloured_graph_rect_Type1 after h_mk_coloured_graph x_21907 =
    236   let { colouring = colouring0; spilled_no = spilled_no0 } = x_21907 in
     235let rec coloured_graph_rect_Type1 after h_mk_coloured_graph x_1972 =
     236  let { colouring = colouring0; spilled_no = spilled_no0 } = x_1972 in
    237237  h_mk_coloured_graph colouring0 spilled_no0 __ __
    238238
     
    240240    Fixpoints.valuation -> ((Liveness.vertex -> decision) -> Nat.nat -> __ ->
    241241    __ -> 'a1) -> coloured_graph -> 'a1 **)
    242 let rec coloured_graph_rect_Type0 after h_mk_coloured_graph x_21909 =
    243   let { colouring = colouring0; spilled_no = spilled_no0 } = x_21909 in
     242let rec coloured_graph_rect_Type0 after h_mk_coloured_graph x_1974 =
     243  let { colouring = colouring0; spilled_no = spilled_no0 } = x_1974 in
    244244  h_mk_coloured_graph colouring0 spilled_no0 __ __
    245245
  • extracted/joint.ml

    r2827 r2854  
    110110    ('a1 -> 'a2) -> (BitVector.byte -> 'a2) -> 'a1 argument -> 'a2 **)
    111111let rec argument_rect_Type4 h_Reg h_Imm = function
    112 | Reg x_19661 -> h_Reg x_19661
    113 | Imm x_19662 -> h_Imm x_19662
     112| Reg x_7 -> h_Reg x_7
     113| Imm x_8 -> h_Imm x_8
    114114
    115115(** val argument_rect_Type5 :
    116116    ('a1 -> 'a2) -> (BitVector.byte -> 'a2) -> 'a1 argument -> 'a2 **)
    117117let rec argument_rect_Type5 h_Reg h_Imm = function
    118 | Reg x_19666 -> h_Reg x_19666
    119 | Imm x_19667 -> h_Imm x_19667
     118| Reg x_12 -> h_Reg x_12
     119| Imm x_13 -> h_Imm x_13
    120120
    121121(** val argument_rect_Type3 :
    122122    ('a1 -> 'a2) -> (BitVector.byte -> 'a2) -> 'a1 argument -> 'a2 **)
    123123let rec argument_rect_Type3 h_Reg h_Imm = function
    124 | Reg x_19671 -> h_Reg x_19671
    125 | Imm x_19672 -> h_Imm x_19672
     124| Reg x_17 -> h_Reg x_17
     125| Imm x_18 -> h_Imm x_18
    126126
    127127(** val argument_rect_Type2 :
    128128    ('a1 -> 'a2) -> (BitVector.byte -> 'a2) -> 'a1 argument -> 'a2 **)
    129129let rec argument_rect_Type2 h_Reg h_Imm = function
    130 | Reg x_19676 -> h_Reg x_19676
    131 | Imm x_19677 -> h_Imm x_19677
     130| Reg x_22 -> h_Reg x_22
     131| Imm x_23 -> h_Imm x_23
    132132
    133133(** val argument_rect_Type1 :
    134134    ('a1 -> 'a2) -> (BitVector.byte -> 'a2) -> 'a1 argument -> 'a2 **)
    135135let rec argument_rect_Type1 h_Reg h_Imm = function
    136 | Reg x_19681 -> h_Reg x_19681
    137 | Imm x_19682 -> h_Imm x_19682
     136| Reg x_27 -> h_Reg x_27
     137| Imm x_28 -> h_Imm x_28
    138138
    139139(** val argument_rect_Type0 :
    140140    ('a1 -> 'a2) -> (BitVector.byte -> 'a2) -> 'a1 argument -> 'a2 **)
    141141let rec argument_rect_Type0 h_Reg h_Imm = function
    142 | Reg x_19686 -> h_Reg x_19686
    143 | Imm x_19687 -> h_Imm x_19687
     142| Reg x_32 -> h_Reg x_32
     143| Imm x_33 -> h_Imm x_33
    144144
    145145(** val argument_inv_rect_Type4 :
     
    324324    __ -> (__ -> Graphs.label List.list) -> Bool.bool -> __ -> 'a1) ->
    325325    unserialized_params -> 'a1 **)
    326 let rec unserialized_params_rect_Type4 h_mk_unserialized_params x_19722 =
     326let rec unserialized_params_rect_Type4 h_mk_unserialized_params x_68 =
    327327  let { ext_seq_labels = ext_seq_labels0; has_tailcalls = has_tailcalls0 } =
    328     x_19722
     328    x_68
    329329  in
    330330  h_mk_unserialized_params __ __ __ __ __ __ __ __ __ __ __ __ __
     
    335335    __ -> (__ -> Graphs.label List.list) -> Bool.bool -> __ -> 'a1) ->
    336336    unserialized_params -> 'a1 **)
    337 let rec unserialized_params_rect_Type5 h_mk_unserialized_params x_19724 =
     337let rec unserialized_params_rect_Type5 h_mk_unserialized_params x_70 =
    338338  let { ext_seq_labels = ext_seq_labels0; has_tailcalls = has_tailcalls0 } =
    339     x_19724
     339    x_70
    340340  in
    341341  h_mk_unserialized_params __ __ __ __ __ __ __ __ __ __ __ __ __
     
    346346    __ -> (__ -> Graphs.label List.list) -> Bool.bool -> __ -> 'a1) ->
    347347    unserialized_params -> 'a1 **)
    348 let rec unserialized_params_rect_Type3 h_mk_unserialized_params x_19726 =
     348let rec unserialized_params_rect_Type3 h_mk_unserialized_params x_72 =
    349349  let { ext_seq_labels = ext_seq_labels0; has_tailcalls = has_tailcalls0 } =
    350     x_19726
     350    x_72
    351351  in
    352352  h_mk_unserialized_params __ __ __ __ __ __ __ __ __ __ __ __ __
     
    357357    __ -> (__ -> Graphs.label List.list) -> Bool.bool -> __ -> 'a1) ->
    358358    unserialized_params -> 'a1 **)
    359 let rec unserialized_params_rect_Type2 h_mk_unserialized_params x_19728 =
     359let rec unserialized_params_rect_Type2 h_mk_unserialized_params x_74 =
    360360  let { ext_seq_labels = ext_seq_labels0; has_tailcalls = has_tailcalls0 } =
    361     x_19728
     361    x_74
    362362  in
    363363  h_mk_unserialized_params __ __ __ __ __ __ __ __ __ __ __ __ __
     
    368368    __ -> (__ -> Graphs.label List.list) -> Bool.bool -> __ -> 'a1) ->
    369369    unserialized_params -> 'a1 **)
    370 let rec unserialized_params_rect_Type1 h_mk_unserialized_params x_19730 =
     370let rec unserialized_params_rect_Type1 h_mk_unserialized_params x_76 =
    371371  let { ext_seq_labels = ext_seq_labels0; has_tailcalls = has_tailcalls0 } =
    372     x_19730
     372    x_76
    373373  in
    374374  h_mk_unserialized_params __ __ __ __ __ __ __ __ __ __ __ __ __
     
    379379    __ -> (__ -> Graphs.label List.list) -> Bool.bool -> __ -> 'a1) ->
    380380    unserialized_params -> 'a1 **)
    381 let rec unserialized_params_rect_Type0 h_mk_unserialized_params x_19732 =
     381let rec unserialized_params_rect_Type0 h_mk_unserialized_params x_78 =
    382382  let { ext_seq_labels = ext_seq_labels0; has_tailcalls = has_tailcalls0 } =
    383     x_19732
     383    x_78
    384384  in
    385385  h_mk_unserialized_params __ __ __ __ __ __ __ __ __ __ __ __ __
     
    506506    (__ -> Registers.register List.list) -> 'a1) -> get_pseudo_reg_functs ->
    507507    'a1 **)
    508 let rec get_pseudo_reg_functs_rect_Type4 p h_mk_get_pseudo_reg_functs x_19749 =
     508let rec get_pseudo_reg_functs_rect_Type4 p h_mk_get_pseudo_reg_functs x_95 =
    509509  let { acc_a_regs = acc_a_regs0; acc_b_regs = acc_b_regs0; acc_a_args =
    510510    acc_a_args0; acc_b_args = acc_b_args0; dpl_regs = dpl_regs0; dph_regs =
     
    512512    snd_args0; pair_move_regs = pair_move_regs0; f_call_args = f_call_args0;
    513513    f_call_dest = f_call_dest0; ext_seq_regs = ext_seq_regs0; params_regs =
    514     params_regs0 } = x_19749
     514    params_regs0 } = x_95
    515515  in
    516516  h_mk_get_pseudo_reg_functs acc_a_regs0 acc_b_regs0 acc_a_args0 acc_b_args0
     
    529529    (__ -> Registers.register List.list) -> 'a1) -> get_pseudo_reg_functs ->
    530530    'a1 **)
    531 let rec get_pseudo_reg_functs_rect_Type5 p h_mk_get_pseudo_reg_functs x_19751 =
     531let rec get_pseudo_reg_functs_rect_Type5 p h_mk_get_pseudo_reg_functs x_97 =
    532532  let { acc_a_regs = acc_a_regs0; acc_b_regs = acc_b_regs0; acc_a_args =
    533533    acc_a_args0; acc_b_args = acc_b_args0; dpl_regs = dpl_regs0; dph_regs =
     
    535535    snd_args0; pair_move_regs = pair_move_regs0; f_call_args = f_call_args0;
    536536    f_call_dest = f_call_dest0; ext_seq_regs = ext_seq_regs0; params_regs =
    537     params_regs0 } = x_19751
     537    params_regs0 } = x_97
    538538  in
    539539  h_mk_get_pseudo_reg_functs acc_a_regs0 acc_b_regs0 acc_a_args0 acc_b_args0
     
    552552    (__ -> Registers.register List.list) -> 'a1) -> get_pseudo_reg_functs ->
    553553    'a1 **)
    554 let rec get_pseudo_reg_functs_rect_Type3 p h_mk_get_pseudo_reg_functs x_19753 =
     554let rec get_pseudo_reg_functs_rect_Type3 p h_mk_get_pseudo_reg_functs x_99 =
    555555  let { acc_a_regs = acc_a_regs0; acc_b_regs = acc_b_regs0; acc_a_args =
    556556    acc_a_args0; acc_b_args = acc_b_args0; dpl_regs = dpl_regs0; dph_regs =
     
    558558    snd_args0; pair_move_regs = pair_move_regs0; f_call_args = f_call_args0;
    559559    f_call_dest = f_call_dest0; ext_seq_regs = ext_seq_regs0; params_regs =
    560     params_regs0 } = x_19753
     560    params_regs0 } = x_99
    561561  in
    562562  h_mk_get_pseudo_reg_functs acc_a_regs0 acc_b_regs0 acc_a_args0 acc_b_args0
     
    575575    (__ -> Registers.register List.list) -> 'a1) -> get_pseudo_reg_functs ->
    576576    'a1 **)
    577 let rec get_pseudo_reg_functs_rect_Type2 p h_mk_get_pseudo_reg_functs x_19755 =
     577let rec get_pseudo_reg_functs_rect_Type2 p h_mk_get_pseudo_reg_functs x_101 =
    578578  let { acc_a_regs = acc_a_regs0; acc_b_regs = acc_b_regs0; acc_a_args =
    579579    acc_a_args0; acc_b_args = acc_b_args0; dpl_regs = dpl_regs0; dph_regs =
     
    581581    snd_args0; pair_move_regs = pair_move_regs0; f_call_args = f_call_args0;
    582582    f_call_dest = f_call_dest0; ext_seq_regs = ext_seq_regs0; params_regs =
    583     params_regs0 } = x_19755
     583    params_regs0 } = x_101
    584584  in
    585585  h_mk_get_pseudo_reg_functs acc_a_regs0 acc_b_regs0 acc_a_args0 acc_b_args0
     
    598598    (__ -> Registers.register List.list) -> 'a1) -> get_pseudo_reg_functs ->
    599599    'a1 **)
    600 let rec get_pseudo_reg_functs_rect_Type1 p h_mk_get_pseudo_reg_functs x_19757 =
     600let rec get_pseudo_reg_functs_rect_Type1 p h_mk_get_pseudo_reg_functs x_103 =
    601601  let { acc_a_regs = acc_a_regs0; acc_b_regs = acc_b_regs0; acc_a_args =
    602602    acc_a_args0; acc_b_args = acc_b_args0; dpl_regs = dpl_regs0; dph_regs =
     
    604604    snd_args0; pair_move_regs = pair_move_regs0; f_call_args = f_call_args0;
    605605    f_call_dest = f_call_dest0; ext_seq_regs = ext_seq_regs0; params_regs =
    606     params_regs0 } = x_19757
     606    params_regs0 } = x_103
    607607  in
    608608  h_mk_get_pseudo_reg_functs acc_a_regs0 acc_b_regs0 acc_a_args0 acc_b_args0
     
    621621    (__ -> Registers.register List.list) -> 'a1) -> get_pseudo_reg_functs ->
    622622    'a1 **)
    623 let rec get_pseudo_reg_functs_rect_Type0 p h_mk_get_pseudo_reg_functs x_19759 =
     623let rec get_pseudo_reg_functs_rect_Type0 p h_mk_get_pseudo_reg_functs x_105 =
    624624  let { acc_a_regs = acc_a_regs0; acc_b_regs = acc_b_regs0; acc_a_args =
    625625    acc_a_args0; acc_b_args = acc_b_args0; dpl_regs = dpl_regs0; dph_regs =
     
    627627    snd_args0; pair_move_regs = pair_move_regs0; f_call_args = f_call_args0;
    628628    f_call_dest = f_call_dest0; ext_seq_regs = ext_seq_regs0; params_regs =
    629     params_regs0 } = x_19759
     629    params_regs0 } = x_105
    630630  in
    631631  h_mk_get_pseudo_reg_functs acc_a_regs0 acc_b_regs0 acc_a_args0 acc_b_args0
     
    805805    (unserialized_params -> get_pseudo_reg_functs -> 'a1) -> uns_params ->
    806806    'a1 **)
    807 let rec uns_params_rect_Type4 h_mk_uns_params x_19789 =
    808   let { u_pars = u_pars0; functs = functs0 } = x_19789 in
     807let rec uns_params_rect_Type4 h_mk_uns_params x_135 =
     808  let { u_pars = u_pars0; functs = functs0 } = x_135 in
    809809  h_mk_uns_params u_pars0 functs0
    810810
     
    812812    (unserialized_params -> get_pseudo_reg_functs -> 'a1) -> uns_params ->
    813813    'a1 **)
    814 let rec uns_params_rect_Type5 h_mk_uns_params x_19791 =
    815   let { u_pars = u_pars0; functs = functs0 } = x_19791 in
     814let rec uns_params_rect_Type5 h_mk_uns_params x_137 =
     815  let { u_pars = u_pars0; functs = functs0 } = x_137 in
    816816  h_mk_uns_params u_pars0 functs0
    817817
     
    819819    (unserialized_params -> get_pseudo_reg_functs -> 'a1) -> uns_params ->
    820820    'a1 **)
    821 let rec uns_params_rect_Type3 h_mk_uns_params x_19793 =
    822   let { u_pars = u_pars0; functs = functs0 } = x_19793 in
     821let rec uns_params_rect_Type3 h_mk_uns_params x_139 =
     822  let { u_pars = u_pars0; functs = functs0 } = x_139 in
    823823  h_mk_uns_params u_pars0 functs0
    824824
     
    826826    (unserialized_params -> get_pseudo_reg_functs -> 'a1) -> uns_params ->
    827827    'a1 **)
    828 let rec uns_params_rect_Type2 h_mk_uns_params x_19795 =
    829   let { u_pars = u_pars0; functs = functs0 } = x_19795 in
     828let rec uns_params_rect_Type2 h_mk_uns_params x_141 =
     829  let { u_pars = u_pars0; functs = functs0 } = x_141 in
    830830  h_mk_uns_params u_pars0 functs0
    831831
     
    833833    (unserialized_params -> get_pseudo_reg_functs -> 'a1) -> uns_params ->
    834834    'a1 **)
    835 let rec uns_params_rect_Type1 h_mk_uns_params x_19797 =
    836   let { u_pars = u_pars0; functs = functs0 } = x_19797 in
     835let rec uns_params_rect_Type1 h_mk_uns_params x_143 =
     836  let { u_pars = u_pars0; functs = functs0 } = x_143 in
    837837  h_mk_uns_params u_pars0 functs0
    838838
     
    840840    (unserialized_params -> get_pseudo_reg_functs -> 'a1) -> uns_params ->
    841841    'a1 **)
    842 let rec uns_params_rect_Type0 h_mk_uns_params x_19799 =
    843   let { u_pars = u_pars0; functs = functs0 } = x_19799 in
     842let rec uns_params_rect_Type0 h_mk_uns_params x_145 =
     843  let { u_pars = u_pars0; functs = functs0 } = x_145 in
    844844  h_mk_uns_params u_pars0 functs0
    845845
     
    911911    'a1) -> (__ -> 'a1) -> joint_seq -> 'a1 **)
    912912let rec joint_seq_rect_Type4 p globals h_COMMENT h_MOVE h_POP h_PUSH h_ADDRESS h_OPACCS h_OP1 h_OP2 h_CLEAR_CARRY h_SET_CARRY h_LOAD h_STORE h_extension_seq = function
    913 | COMMENT x_19854 -> h_COMMENT x_19854
    914 | MOVE x_19855 -> h_MOVE x_19855
    915 | POP x_19856 -> h_POP x_19856
    916 | PUSH x_19857 -> h_PUSH x_19857
    917 | ADDRESS (i, x_19859, x_19858) -> h_ADDRESS i __ x_19859 x_19858
    918 | OPACCS (x_19865, x_19864, x_19863, x_19862, x_19861) ->
    919   h_OPACCS x_19865 x_19864 x_19863 x_19862 x_19861
    920 | OP1 (x_19868, x_19867, x_19866) -> h_OP1 x_19868 x_19867 x_19866
    921 | OP2 (x_19872, x_19871, x_19870, x_19869) ->
    922   h_OP2 x_19872 x_19871 x_19870 x_19869
     913| COMMENT x_200 -> h_COMMENT x_200
     914| MOVE x_201 -> h_MOVE x_201
     915| POP x_202 -> h_POP x_202
     916| PUSH x_203 -> h_PUSH x_203
     917| ADDRESS (i, x_205, x_204) -> h_ADDRESS i __ x_205 x_204
     918| OPACCS (x_211, x_210, x_209, x_208, x_207) ->
     919  h_OPACCS x_211 x_210 x_209 x_208 x_207
     920| OP1 (x_214, x_213, x_212) -> h_OP1 x_214 x_213 x_212
     921| OP2 (x_218, x_217, x_216, x_215) -> h_OP2 x_218 x_217 x_216 x_215
    923922| CLEAR_CARRY -> h_CLEAR_CARRY
    924923| SET_CARRY -> h_SET_CARRY
    925 | LOAD (x_19875, x_19874, x_19873) -> h_LOAD x_19875 x_19874 x_19873
    926 | STORE (x_19878, x_19877, x_19876) -> h_STORE x_19878 x_19877 x_19876
    927 | Extension_seq x_19879 -> h_extension_seq x_19879
     924| LOAD (x_221, x_220, x_219) -> h_LOAD x_221 x_220 x_219
     925| STORE (x_224, x_223, x_222) -> h_STORE x_224 x_223 x_222
     926| Extension_seq x_225 -> h_extension_seq x_225
    928927
    929928(** val joint_seq_rect_Type5 :
     
    935934    'a1) -> (__ -> 'a1) -> joint_seq -> 'a1 **)
    936935let rec joint_seq_rect_Type5 p globals h_COMMENT h_MOVE h_POP h_PUSH h_ADDRESS h_OPACCS h_OP1 h_OP2 h_CLEAR_CARRY h_SET_CARRY h_LOAD h_STORE h_extension_seq = function
    937 | COMMENT x_19894 -> h_COMMENT x_19894
    938 | MOVE x_19895 -> h_MOVE x_19895
    939 | POP x_19896 -> h_POP x_19896
    940 | PUSH x_19897 -> h_PUSH x_19897
    941 | ADDRESS (i, x_19899, x_19898) -> h_ADDRESS i __ x_19899 x_19898
    942 | OPACCS (x_19905, x_19904, x_19903, x_19902, x_19901) ->
    943   h_OPACCS x_19905 x_19904 x_19903 x_19902 x_19901
    944 | OP1 (x_19908, x_19907, x_19906) -> h_OP1 x_19908 x_19907 x_19906
    945 | OP2 (x_19912, x_19911, x_19910, x_19909) ->
    946   h_OP2 x_19912 x_19911 x_19910 x_19909
     936| COMMENT x_240 -> h_COMMENT x_240
     937| MOVE x_241 -> h_MOVE x_241
     938| POP x_242 -> h_POP x_242
     939| PUSH x_243 -> h_PUSH x_243
     940| ADDRESS (i, x_245, x_244) -> h_ADDRESS i __ x_245 x_244
     941| OPACCS (x_251, x_250, x_249, x_248, x_247) ->
     942  h_OPACCS x_251 x_250 x_249 x_248 x_247
     943| OP1 (x_254, x_253, x_252) -> h_OP1 x_254 x_253 x_252
     944| OP2 (x_258, x_257, x_256, x_255) -> h_OP2 x_258 x_257 x_256 x_255
    947945| CLEAR_CARRY -> h_CLEAR_CARRY
    948946| SET_CARRY -> h_SET_CARRY
    949 | LOAD (x_19915, x_19914, x_19913) -> h_LOAD x_19915 x_19914 x_19913
    950 | STORE (x_19918, x_19917, x_19916) -> h_STORE x_19918 x_19917 x_19916
    951 | Extension_seq x_19919 -> h_extension_seq x_19919
     947| LOAD (x_261, x_260, x_259) -> h_LOAD x_261 x_260 x_259
     948| STORE (x_264, x_263, x_262) -> h_STORE x_264 x_263 x_262
     949| Extension_seq x_265 -> h_extension_seq x_265
    952950
    953951(** val joint_seq_rect_Type3 :
     
    959957    'a1) -> (__ -> 'a1) -> joint_seq -> 'a1 **)
    960958let rec joint_seq_rect_Type3 p globals h_COMMENT h_MOVE h_POP h_PUSH h_ADDRESS h_OPACCS h_OP1 h_OP2 h_CLEAR_CARRY h_SET_CARRY h_LOAD h_STORE h_extension_seq = function
    961 | COMMENT x_19934 -> h_COMMENT x_19934
    962 | MOVE x_19935 -> h_MOVE x_19935
    963 | POP x_19936 -> h_POP x_19936
    964 | PUSH x_19937 -> h_PUSH x_19937
    965 | ADDRESS (i, x_19939, x_19938) -> h_ADDRESS i __ x_19939 x_19938
    966 | OPACCS (x_19945, x_19944, x_19943, x_19942, x_19941) ->
    967   h_OPACCS x_19945 x_19944 x_19943 x_19942 x_19941
    968 | OP1 (x_19948, x_19947, x_19946) -> h_OP1 x_19948 x_19947 x_19946
    969 | OP2 (x_19952, x_19951, x_19950, x_19949) ->
    970   h_OP2 x_19952 x_19951 x_19950 x_19949
     959| COMMENT x_280 -> h_COMMENT x_280
     960| MOVE x_281 -> h_MOVE x_281
     961| POP x_282 -> h_POP x_282
     962| PUSH x_283 -> h_PUSH x_283
     963| ADDRESS (i, x_285, x_284) -> h_ADDRESS i __ x_285 x_284
     964| OPACCS (x_291, x_290, x_289, x_288, x_287) ->
     965  h_OPACCS x_291 x_290 x_289 x_288 x_287
     966| OP1 (x_294, x_293, x_292) -> h_OP1 x_294 x_293 x_292
     967| OP2 (x_298, x_297, x_296, x_295) -> h_OP2 x_298 x_297 x_296 x_295
    971968| CLEAR_CARRY -> h_CLEAR_CARRY
    972969| SET_CARRY -> h_SET_CARRY
    973 | LOAD (x_19955, x_19954, x_19953) -> h_LOAD x_19955 x_19954 x_19953
    974 | STORE (x_19958, x_19957, x_19956) -> h_STORE x_19958 x_19957 x_19956
    975 | Extension_seq x_19959 -> h_extension_seq x_19959
     970| LOAD (x_301, x_300, x_299) -> h_LOAD x_301 x_300 x_299
     971| STORE (x_304, x_303, x_302) -> h_STORE x_304 x_303 x_302
     972| Extension_seq x_305 -> h_extension_seq x_305
    976973
    977974(** val joint_seq_rect_Type2 :
     
    983980    'a1) -> (__ -> 'a1) -> joint_seq -> 'a1 **)
    984981let rec joint_seq_rect_Type2 p globals h_COMMENT h_MOVE h_POP h_PUSH h_ADDRESS h_OPACCS h_OP1 h_OP2 h_CLEAR_CARRY h_SET_CARRY h_LOAD h_STORE h_extension_seq = function
    985 | COMMENT x_19974 -> h_COMMENT x_19974
    986 | MOVE x_19975 -> h_MOVE x_19975
    987 | POP x_19976 -> h_POP x_19976
    988 | PUSH x_19977 -> h_PUSH x_19977
    989 | ADDRESS (i, x_19979, x_19978) -> h_ADDRESS i __ x_19979 x_19978
    990 | OPACCS (x_19985, x_19984, x_19983, x_19982, x_19981) ->
    991   h_OPACCS x_19985 x_19984 x_19983 x_19982 x_19981
    992 | OP1 (x_19988, x_19987, x_19986) -> h_OP1 x_19988 x_19987 x_19986
    993 | OP2 (x_19992, x_19991, x_19990, x_19989) ->
    994   h_OP2 x_19992 x_19991 x_19990 x_19989
     982| COMMENT x_320 -> h_COMMENT x_320
     983| MOVE x_321 -> h_MOVE x_321
     984| POP x_322 -> h_POP x_322
     985| PUSH x_323 -> h_PUSH x_323
     986| ADDRESS (i, x_325, x_324) -> h_ADDRESS i __ x_325 x_324
     987| OPACCS (x_331, x_330, x_329, x_328, x_327) ->
     988  h_OPACCS x_331 x_330 x_329 x_328 x_327
     989| OP1 (x_334, x_333, x_332) -> h_OP1 x_334 x_333 x_332
     990| OP2 (x_338, x_337, x_336, x_335) -> h_OP2 x_338 x_337 x_336 x_335
    995991| CLEAR_CARRY -> h_CLEAR_CARRY
    996992| SET_CARRY -> h_SET_CARRY
    997 | LOAD (x_19995, x_19994, x_19993) -> h_LOAD x_19995 x_19994 x_19993
    998 | STORE (x_19998, x_19997, x_19996) -> h_STORE x_19998 x_19997 x_19996
    999 | Extension_seq x_19999 -> h_extension_seq x_19999
     993| LOAD (x_341, x_340, x_339) -> h_LOAD x_341 x_340 x_339
     994| STORE (x_344, x_343, x_342) -> h_STORE x_344 x_343 x_342
     995| Extension_seq x_345 -> h_extension_seq x_345
    1000996
    1001997(** val joint_seq_rect_Type1 :
     
    10071003    'a1) -> (__ -> 'a1) -> joint_seq -> 'a1 **)
    10081004let rec joint_seq_rect_Type1 p globals h_COMMENT h_MOVE h_POP h_PUSH h_ADDRESS h_OPACCS h_OP1 h_OP2 h_CLEAR_CARRY h_SET_CARRY h_LOAD h_STORE h_extension_seq = function
    1009 | COMMENT x_20014 -> h_COMMENT x_20014
    1010 | MOVE x_20015 -> h_MOVE x_20015
    1011 | POP x_20016 -> h_POP x_20016
    1012 | PUSH x_20017 -> h_PUSH x_20017
    1013 | ADDRESS (i, x_20019, x_20018) -> h_ADDRESS i __ x_20019 x_20018
    1014 | OPACCS (x_20025, x_20024, x_20023, x_20022, x_20021) ->
    1015   h_OPACCS x_20025 x_20024 x_20023 x_20022 x_20021
    1016 | OP1 (x_20028, x_20027, x_20026) -> h_OP1 x_20028 x_20027 x_20026
    1017 | OP2 (x_20032, x_20031, x_20030, x_20029) ->
    1018   h_OP2 x_20032 x_20031 x_20030 x_20029
     1005| COMMENT x_360 -> h_COMMENT x_360
     1006| MOVE x_361 -> h_MOVE x_361
     1007| POP x_362 -> h_POP x_362
     1008| PUSH x_363 -> h_PUSH x_363
     1009| ADDRESS (i, x_365, x_364) -> h_ADDRESS i __ x_365 x_364
     1010| OPACCS (x_371, x_370, x_369, x_368, x_367) ->
     1011  h_OPACCS x_371 x_370 x_369 x_368 x_367
     1012| OP1 (x_374, x_373, x_372) -> h_OP1 x_374 x_373 x_372
     1013| OP2 (x_378, x_377, x_376, x_375) -> h_OP2 x_378 x_377 x_376 x_375
    10191014| CLEAR_CARRY -> h_CLEAR_CARRY
    10201015| SET_CARRY -> h_SET_CARRY
    1021 | LOAD (x_20035, x_20034, x_20033) -> h_LOAD x_20035 x_20034 x_20033
    1022 | STORE (x_20038, x_20037, x_20036) -> h_STORE x_20038 x_20037 x_20036
    1023 | Extension_seq x_20039 -> h_extension_seq x_20039
     1016| LOAD (x_381, x_380, x_379) -> h_LOAD x_381 x_380 x_379
     1017| STORE (x_384, x_383, x_382) -> h_STORE x_384 x_383 x_382
     1018| Extension_seq x_385 -> h_extension_seq x_385
    10241019
    10251020(** val joint_seq_rect_Type0 :
     
    10311026    'a1) -> (__ -> 'a1) -> joint_seq -> 'a1 **)
    10321027let rec joint_seq_rect_Type0 p globals h_COMMENT h_MOVE h_POP h_PUSH h_ADDRESS h_OPACCS h_OP1 h_OP2 h_CLEAR_CARRY h_SET_CARRY h_LOAD h_STORE h_extension_seq = function
    1033 | COMMENT x_20054 -> h_COMMENT x_20054
    1034 | MOVE x_20055 -> h_MOVE x_20055
    1035 | POP x_20056 -> h_POP x_20056
    1036 | PUSH x_20057 -> h_PUSH x_20057
    1037 | ADDRESS (i, x_20059, x_20058) -> h_ADDRESS i __ x_20059 x_20058
    1038 | OPACCS (x_20065, x_20064, x_20063, x_20062, x_20061) ->
    1039   h_OPACCS x_20065 x_20064 x_20063 x_20062 x_20061
    1040 | OP1 (x_20068, x_20067, x_20066) -> h_OP1 x_20068 x_20067 x_20066
    1041 | OP2 (x_20072, x_20071, x_20070, x_20069) ->
    1042   h_OP2 x_20072 x_20071 x_20070 x_20069
     1028| COMMENT x_400 -> h_COMMENT x_400
     1029| MOVE x_401 -> h_MOVE x_401
     1030| POP x_402 -> h_POP x_402
     1031| PUSH x_403 -> h_PUSH x_403
     1032| ADDRESS (i, x_405, x_404) -> h_ADDRESS i __ x_405 x_404
     1033| OPACCS (x_411, x_410, x_409, x_408, x_407) ->
     1034  h_OPACCS x_411 x_410 x_409 x_408 x_407
     1035| OP1 (x_414, x_413, x_412) -> h_OP1 x_414 x_413 x_412
     1036| OP2 (x_418, x_417, x_416, x_415) -> h_OP2 x_418 x_417 x_416 x_415
    10431037| CLEAR_CARRY -> h_CLEAR_CARRY
    10441038| SET_CARRY -> h_SET_CARRY
    1045 | LOAD (x_20075, x_20074, x_20073) -> h_LOAD x_20075 x_20074 x_20073
    1046 | STORE (x_20078, x_20077, x_20076) -> h_STORE x_20078 x_20077 x_20076
    1047 | Extension_seq x_20079 -> h_extension_seq x_20079
     1039| LOAD (x_421, x_420, x_419) -> h_LOAD x_421 x_420 x_419
     1040| STORE (x_424, x_423, x_422) -> h_STORE x_424 x_423 x_422
     1041| Extension_seq x_425 -> h_extension_seq x_425
    10481042
    10491043(** val joint_seq_inv_rect_Type4 :
     
    12361230    -> (__ -> Graphs.label -> 'a1) -> (joint_seq -> 'a1) -> joint_step -> 'a1 **)
    12371231let rec joint_step_rect_Type4 p globals h_COST_LABEL h_CALL h_COND h_step_seq = function
    1238 | COST_LABEL x_20346 -> h_COST_LABEL x_20346
    1239 | CALL (x_20349, x_20348, x_20347) -> h_CALL x_20349 x_20348 x_20347
    1240 | COND (x_20351, x_20350) -> h_COND x_20351 x_20350
    1241 | Step_seq x_20352 -> h_step_seq x_20352
     1232| COST_LABEL x_692 -> h_COST_LABEL x_692
     1233| CALL (x_695, x_694, x_693) -> h_CALL x_695 x_694 x_693
     1234| COND (x_697, x_696) -> h_COND x_697 x_696
     1235| Step_seq x_698 -> h_step_seq x_698
    12421236
    12431237(** val joint_step_rect_Type5 :
     
    12461240    -> (__ -> Graphs.label -> 'a1) -> (joint_seq -> 'a1) -> joint_step -> 'a1 **)
    12471241let rec joint_step_rect_Type5 p globals h_COST_LABEL h_CALL h_COND h_step_seq = function
    1248 | COST_LABEL x_20358 -> h_COST_LABEL x_20358
    1249 | CALL (x_20361, x_20360, x_20359) -> h_CALL x_20361 x_20360 x_20359
    1250 | COND (x_20363, x_20362) -> h_COND x_20363 x_20362
    1251 | Step_seq x_20364 -> h_step_seq x_20364
     1242| COST_LABEL x_704 -> h_COST_LABEL x_704
     1243| CALL (x_707, x_706, x_705) -> h_CALL x_707 x_706 x_705
     1244| COND (x_709, x_708) -> h_COND x_709 x_708
     1245| Step_seq x_710 -> h_step_seq x_710
    12521246
    12531247(** val joint_step_rect_Type3 :
     
    12561250    -> (__ -> Graphs.label -> 'a1) -> (joint_seq -> 'a1) -> joint_step -> 'a1 **)
    12571251let rec joint_step_rect_Type3 p globals h_COST_LABEL h_CALL h_COND h_step_seq = function
    1258 | COST_LABEL x_20370 -> h_COST_LABEL x_20370
    1259 | CALL (x_20373, x_20372, x_20371) -> h_CALL x_20373 x_20372 x_20371
    1260 | COND (x_20375, x_20374) -> h_COND x_20375 x_20374
    1261 | Step_seq x_20376 -> h_step_seq x_20376
     1252| COST_LABEL x_716 -> h_COST_LABEL x_716
     1253| CALL (x_719, x_718, x_717) -> h_CALL x_719 x_718 x_717
     1254| COND (x_721, x_720) -> h_COND x_721 x_720
     1255| Step_seq x_722 -> h_step_seq x_722
    12621256
    12631257(** val joint_step_rect_Type2 :
     
    12661260    -> (__ -> Graphs.label -> 'a1) -> (joint_seq -> 'a1) -> joint_step -> 'a1 **)
    12671261let rec joint_step_rect_Type2 p globals h_COST_LABEL h_CALL h_COND h_step_seq = function
    1268 | COST_LABEL x_20382 -> h_COST_LABEL x_20382
    1269 | CALL (x_20385, x_20384, x_20383) -> h_CALL x_20385 x_20384 x_20383
    1270 | COND (x_20387, x_20386) -> h_COND x_20387 x_20386
    1271 | Step_seq x_20388 -> h_step_seq x_20388
     1262| COST_LABEL x_728 -> h_COST_LABEL x_728
     1263| CALL (x_731, x_730, x_729) -> h_CALL x_731 x_730 x_729
     1264| COND (x_733, x_732) -> h_COND x_733 x_732
     1265| Step_seq x_734 -> h_step_seq x_734
    12721266
    12731267(** val joint_step_rect_Type1 :
     
    12761270    -> (__ -> Graphs.label -> 'a1) -> (joint_seq -> 'a1) -> joint_step -> 'a1 **)
    12771271let rec joint_step_rect_Type1 p globals h_COST_LABEL h_CALL h_COND h_step_seq = function
    1278 | COST_LABEL x_20394 -> h_COST_LABEL x_20394
    1279 | CALL (x_20397, x_20396, x_20395) -> h_CALL x_20397 x_20396 x_20395
    1280 | COND (x_20399, x_20398) -> h_COND x_20399 x_20398
    1281 | Step_seq x_20400 -> h_step_seq x_20400
     1272| COST_LABEL x_740 -> h_COST_LABEL x_740
     1273| CALL (x_743, x_742, x_741) -> h_CALL x_743 x_742 x_741
     1274| COND (x_745, x_744) -> h_COND x_745 x_744
     1275| Step_seq x_746 -> h_step_seq x_746
    12821276
    12831277(** val joint_step_rect_Type0 :
     
    12861280    -> (__ -> Graphs.label -> 'a1) -> (joint_seq -> 'a1) -> joint_step -> 'a1 **)
    12871281let rec joint_step_rect_Type0 p globals h_COST_LABEL h_CALL h_COND h_step_seq = function
    1288 | COST_LABEL x_20406 -> h_COST_LABEL x_20406
    1289 | CALL (x_20409, x_20408, x_20407) -> h_CALL x_20409 x_20408 x_20407
    1290 | COND (x_20411, x_20410) -> h_COND x_20411 x_20410
    1291 | Step_seq x_20412 -> h_step_seq x_20412
     1282| COST_LABEL x_752 -> h_COST_LABEL x_752
     1283| CALL (x_755, x_754, x_753) -> h_CALL x_755 x_754 x_753
     1284| COND (x_757, x_756) -> h_COND x_757 x_756
     1285| Step_seq x_758 -> h_step_seq x_758
    12921286
    12931287(** val joint_step_inv_rect_Type4 :
     
    13591353| COST_LABEL c -> List.Nil
    13601354| CALL (id, args, dest) ->
    1361   List.append (functs0.f_call_args args) (functs0.f_call_dest dest)
     1355  let r_id =
     1356    match id with
     1357    | Types.Inl x -> List.Nil
     1358    | Types.Inr ptr ->
     1359      List.append (functs0.dpl_args ptr.Types.fst)
     1360        (functs0.dph_args ptr.Types.snd)
     1361  in
     1362  List.append r_id
     1363    (List.append (functs0.f_call_args args) (functs0.f_call_dest dest))
    13621364| COND (r, lbl) -> functs0.acc_a_regs r
    13631365| Step_seq s -> get_used_registers_from_seq p globals functs0 s
     
    14561458    (uns_params -> __ -> (__ -> Graphs.label Types.option) -> Bool.bool ->
    14571459    'a1) -> stmt_params -> 'a1 **)
    1458 let rec stmt_params_rect_Type4 h_mk_stmt_params x_20491 =
     1460let rec stmt_params_rect_Type4 h_mk_stmt_params x_837 =
    14591461  let { uns_pars = uns_pars0; succ_label = succ_label0; has_fcond =
    1460     has_fcond0 } = x_20491
     1462    has_fcond0 } = x_837
    14611463  in
    14621464  h_mk_stmt_params uns_pars0 __ succ_label0 has_fcond0
     
    14651467    (uns_params -> __ -> (__ -> Graphs.label Types.option) -> Bool.bool ->
    14661468    'a1) -> stmt_params -> 'a1 **)
    1467 let rec stmt_params_rect_Type5 h_mk_stmt_params x_20493 =
     1469let rec stmt_params_rect_Type5 h_mk_stmt_params x_839 =
    14681470  let { uns_pars = uns_pars0; succ_label = succ_label0; has_fcond =
    1469     has_fcond0 } = x_20493
     1471    has_fcond0 } = x_839
    14701472  in
    14711473  h_mk_stmt_params uns_pars0 __ succ_label0 has_fcond0
     
    14741476    (uns_params -> __ -> (__ -> Graphs.label Types.option) -> Bool.bool ->
    14751477    'a1) -> stmt_params -> 'a1 **)
    1476 let rec stmt_params_rect_Type3 h_mk_stmt_params x_20495 =
     1478let rec stmt_params_rect_Type3 h_mk_stmt_params x_841 =
    14771479  let { uns_pars = uns_pars0; succ_label = succ_label0; has_fcond =
    1478     has_fcond0 } = x_20495
     1480    has_fcond0 } = x_841
    14791481  in
    14801482  h_mk_stmt_params uns_pars0 __ succ_label0 has_fcond0
     
    14831485    (uns_params -> __ -> (__ -> Graphs.label Types.option) -> Bool.bool ->
    14841486    'a1) -> stmt_params -> 'a1 **)
    1485 let rec stmt_params_rect_Type2 h_mk_stmt_params x_20497 =
     1487let rec stmt_params_rect_Type2 h_mk_stmt_params x_843 =
    14861488  let { uns_pars = uns_pars0; succ_label = succ_label0; has_fcond =
    1487     has_fcond0 } = x_20497
     1489    has_fcond0 } = x_843
    14881490  in
    14891491  h_mk_stmt_params uns_pars0 __ succ_label0 has_fcond0
     
    14921494    (uns_params -> __ -> (__ -> Graphs.label Types.option) -> Bool.bool ->
    14931495    'a1) -> stmt_params -> 'a1 **)
    1494 let rec stmt_params_rect_Type1 h_mk_stmt_params x_20499 =
     1496let rec stmt_params_rect_Type1 h_mk_stmt_params x_845 =
    14951497  let { uns_pars = uns_pars0; succ_label = succ_label0; has_fcond =
    1496     has_fcond0 } = x_20499
     1498    has_fcond0 } = x_845
    14971499  in
    14981500  h_mk_stmt_params uns_pars0 __ succ_label0 has_fcond0
     
    15011503    (uns_params -> __ -> (__ -> Graphs.label Types.option) -> Bool.bool ->
    15021504    'a1) -> stmt_params -> 'a1 **)
    1503 let rec stmt_params_rect_Type0 h_mk_stmt_params x_20501 =
     1505let rec stmt_params_rect_Type0 h_mk_stmt_params x_847 =
    15041506  let { uns_pars = uns_pars0; succ_label = succ_label0; has_fcond =
    1505     has_fcond0 } = x_20501
     1507    has_fcond0 } = x_847
    15061508  in
    15071509  h_mk_stmt_params uns_pars0 __ succ_label0 has_fcond0
     
    15701572    (__, __) Types.prod) Types.sum -> __ -> 'a1) -> joint_fin_step -> 'a1 **)
    15711573let rec joint_fin_step_rect_Type4 p h_GOTO h_RETURN h_TAILCALL = function
    1572 | GOTO x_20525 -> h_GOTO x_20525
     1574| GOTO x_871 -> h_GOTO x_871
    15731575| RETURN -> h_RETURN
    1574 | TAILCALL (x_20527, x_20526) -> h_TAILCALL __ x_20527 x_20526
     1576| TAILCALL (x_873, x_872) -> h_TAILCALL __ x_873 x_872
    15751577
    15761578(** val joint_fin_step_rect_Type5 :
     
    15781580    (__, __) Types.prod) Types.sum -> __ -> 'a1) -> joint_fin_step -> 'a1 **)
    15791581let rec joint_fin_step_rect_Type5 p h_GOTO h_RETURN h_TAILCALL = function
    1580 | GOTO x_20533 -> h_GOTO x_20533
     1582| GOTO x_879 -> h_GOTO x_879
    15811583| RETURN -> h_RETURN
    1582 | TAILCALL (x_20535, x_20534) -> h_TAILCALL __ x_20535 x_20534
     1584| TAILCALL (x_881, x_880) -> h_TAILCALL __ x_881 x_880
    15831585
    15841586(** val joint_fin_step_rect_Type3 :
     
    15861588    (__, __) Types.prod) Types.sum -> __ -> 'a1) -> joint_fin_step -> 'a1 **)
    15871589let rec joint_fin_step_rect_Type3 p h_GOTO h_RETURN h_TAILCALL = function
    1588 | GOTO x_20541 -> h_GOTO x_20541
     1590| GOTO x_887 -> h_GOTO x_887
    15891591| RETURN -> h_RETURN
    1590 | TAILCALL (x_20543, x_20542) -> h_TAILCALL __ x_20543 x_20542
     1592| TAILCALL (x_889, x_888) -> h_TAILCALL __ x_889 x_888
    15911593
    15921594(** val joint_fin_step_rect_Type2 :
     
    15941596    (__, __) Types.prod) Types.sum -> __ -> 'a1) -> joint_fin_step -> 'a1 **)
    15951597let rec joint_fin_step_rect_Type2 p h_GOTO h_RETURN h_TAILCALL = function
    1596 | GOTO x_20549 -> h_GOTO x_20549
     1598| GOTO x_895 -> h_GOTO x_895
    15971599| RETURN -> h_RETURN
    1598 | TAILCALL (x_20551, x_20550) -> h_TAILCALL __ x_20551 x_20550
     1600| TAILCALL (x_897, x_896) -> h_TAILCALL __ x_897 x_896
    15991601
    16001602(** val joint_fin_step_rect_Type1 :
     
    16021604    (__, __) Types.prod) Types.sum -> __ -> 'a1) -> joint_fin_step -> 'a1 **)
    16031605let rec joint_fin_step_rect_Type1 p h_GOTO h_RETURN h_TAILCALL = function
    1604 | GOTO x_20557 -> h_GOTO x_20557
     1606| GOTO x_903 -> h_GOTO x_903
    16051607| RETURN -> h_RETURN
    1606 | TAILCALL (x_20559, x_20558) -> h_TAILCALL __ x_20559 x_20558
     1608| TAILCALL (x_905, x_904) -> h_TAILCALL __ x_905 x_904
    16071609
    16081610(** val joint_fin_step_rect_Type0 :
     
    16101612    (__, __) Types.prod) Types.sum -> __ -> 'a1) -> joint_fin_step -> 'a1 **)
    16111613let rec joint_fin_step_rect_Type0 p h_GOTO h_RETURN h_TAILCALL = function
    1612 | GOTO x_20565 -> h_GOTO x_20565
     1614| GOTO x_911 -> h_GOTO x_911
    16131615| RETURN -> h_RETURN
    1614 | TAILCALL (x_20567, x_20566) -> h_TAILCALL __ x_20567 x_20566
     1616| TAILCALL (x_913, x_912) -> h_TAILCALL __ x_913 x_912
    16151617
    16161618(** val joint_fin_step_inv_rect_Type4 :
     
    16841686    'a1) -> joint_statement -> 'a1 **)
    16851687let rec joint_statement_rect_Type4 p globals h_sequential h_final h_FCOND = function
    1686 | Sequential (x_20633, x_20632) -> h_sequential x_20633 x_20632
    1687 | Final x_20634 -> h_final x_20634
    1688 | FCOND (x_20637, x_20636, x_20635) -> h_FCOND __ x_20637 x_20636 x_20635
     1688| Sequential (x_979, x_978) -> h_sequential x_979 x_978
     1689| Final x_980 -> h_final x_980
     1690| FCOND (x_983, x_982, x_981) -> h_FCOND __ x_983 x_982 x_981
    16891691
    16901692(** val joint_statement_rect_Type5 :
     
    16931695    'a1) -> joint_statement -> 'a1 **)
    16941696let rec joint_statement_rect_Type5 p globals h_sequential h_final h_FCOND = function
    1695 | Sequential (x_20644, x_20643) -> h_sequential x_20644 x_20643
    1696 | Final x_20645 -> h_final x_20645
    1697 | FCOND (x_20648, x_20647, x_20646) -> h_FCOND __ x_20648 x_20647 x_20646
     1697| Sequential (x_990, x_989) -> h_sequential x_990 x_989
     1698| Final x_991 -> h_final x_991
     1699| FCOND (x_994, x_993, x_992) -> h_FCOND __ x_994 x_993 x_992
    16981700
    16991701(** val joint_statement_rect_Type3 :
     
    17021704    'a1) -> joint_statement -> 'a1 **)
    17031705let rec joint_statement_rect_Type3 p globals h_sequential h_final h_FCOND = function
    1704 | Sequential (x_20655, x_20654) -> h_sequential x_20655 x_20654
    1705 | Final x_20656 -> h_final x_20656
    1706 | FCOND (x_20659, x_20658, x_20657) -> h_FCOND __ x_20659 x_20658 x_20657
     1706| Sequential (x_1001, x_1000) -> h_sequential x_1001 x_1000
     1707| Final x_1002 -> h_final x_1002
     1708| FCOND (x_1005, x_1004, x_1003) -> h_FCOND __ x_1005 x_1004 x_1003
    17071709
    17081710(** val joint_statement_rect_Type2 :
     
    17111713    'a1) -> joint_statement -> 'a1 **)
    17121714let rec joint_statement_rect_Type2 p globals h_sequential h_final h_FCOND = function
    1713 | Sequential (x_20666, x_20665) -> h_sequential x_20666 x_20665
    1714 | Final x_20667 -> h_final x_20667
    1715 | FCOND (x_20670, x_20669, x_20668) -> h_FCOND __ x_20670 x_20669 x_20668
     1715| Sequential (x_1012, x_1011) -> h_sequential x_1012 x_1011
     1716| Final x_1013 -> h_final x_1013
     1717| FCOND (x_1016, x_1015, x_1014) -> h_FCOND __ x_1016 x_1015 x_1014
    17161718
    17171719(** val joint_statement_rect_Type1 :
     
    17201722    'a1) -> joint_statement -> 'a1 **)
    17211723let rec joint_statement_rect_Type1 p globals h_sequential h_final h_FCOND = function
    1722 | Sequential (x_20677, x_20676) -> h_sequential x_20677 x_20676
    1723 | Final x_20678 -> h_final x_20678
    1724 | FCOND (x_20681, x_20680, x_20679) -> h_FCOND __ x_20681 x_20680 x_20679
     1724| Sequential (x_1023, x_1022) -> h_sequential x_1023 x_1022
     1725| Final x_1024 -> h_final x_1024
     1726| FCOND (x_1027, x_1026, x_1025) -> h_FCOND __ x_1027 x_1026 x_1025
    17251727
    17261728(** val joint_statement_rect_Type0 :
     
    17291731    'a1) -> joint_statement -> 'a1 **)
    17301732let rec joint_statement_rect_Type0 p globals h_sequential h_final h_FCOND = function
    1731 | Sequential (x_20688, x_20687) -> h_sequential x_20688 x_20687
    1732 | Final x_20689 -> h_final x_20689
    1733 | FCOND (x_20692, x_20691, x_20690) -> h_FCOND __ x_20692 x_20691 x_20690
     1733| Sequential (x_1034, x_1033) -> h_sequential x_1034 x_1033
     1734| Final x_1035 -> h_final x_1035
     1735| FCOND (x_1038, x_1037, x_1036) -> h_FCOND __ x_1038 x_1037 x_1036
    17341736
    17351737(** val joint_statement_inv_rect_Type4 :
     
    18301832    Graphs.label -> __ Types.option) -> (__ -> __ -> __) -> 'a1) -> params ->
    18311833    'a1 **)
    1832 let rec params_rect_Type4 h_mk_params x_20765 =
     1834let rec params_rect_Type4 h_mk_params x_1111 =
    18331835  let { stmt_pars = stmt_pars0; stmt_at = stmt_at0; point_of_label =
    1834     point_of_label0; point_of_succ = point_of_succ0 } = x_20765
     1836    point_of_label0; point_of_succ = point_of_succ0 } = x_1111
    18351837  in
    18361838  h_mk_params stmt_pars0 __ __ stmt_at0 point_of_label0 point_of_succ0
     
    18411843    Graphs.label -> __ Types.option) -> (__ -> __ -> __) -> 'a1) -> params ->
    18421844    'a1 **)
    1843 let rec params_rect_Type5 h_mk_params x_20767 =
     1845let rec params_rect_Type5 h_mk_params x_1113 =
    18441846  let { stmt_pars = stmt_pars0; stmt_at = stmt_at0; point_of_label =
    1845     point_of_label0; point_of_succ = point_of_succ0 } = x_20767
     1847    point_of_label0; point_of_succ = point_of_succ0 } = x_1113
    18461848  in
    18471849  h_mk_params stmt_pars0 __ __ stmt_at0 point_of_label0 point_of_succ0
     
    18521854    Graphs.label -> __ Types.option) -> (__ -> __ -> __) -> 'a1) -> params ->
    18531855    'a1 **)
    1854 let rec params_rect_Type3 h_mk_params x_20769 =
     1856let rec params_rect_Type3 h_mk_params x_1115 =
    18551857  let { stmt_pars = stmt_pars0; stmt_at = stmt_at0; point_of_label =
    1856     point_of_label0; point_of_succ = point_of_succ0 } = x_20769
     1858    point_of_label0; point_of_succ = point_of_succ0 } = x_1115
    18571859  in
    18581860  h_mk_params stmt_pars0 __ __ stmt_at0 point_of_label0 point_of_succ0
     
    18631865    Graphs.label -> __ Types.option) -> (__ -> __ -> __) -> 'a1) -> params ->
    18641866    'a1 **)
    1865 let rec params_rect_Type2 h_mk_params x_20771 =
     1867let rec params_rect_Type2 h_mk_params x_1117 =
    18661868  let { stmt_pars = stmt_pars0; stmt_at = stmt_at0; point_of_label =
    1867     point_of_label0; point_of_succ = point_of_succ0 } = x_20771
     1869    point_of_label0; point_of_succ = point_of_succ0 } = x_1117
    18681870  in
    18691871  h_mk_params stmt_pars0 __ __ stmt_at0 point_of_label0 point_of_succ0
     
    18741876    Graphs.label -> __ Types.option) -> (__ -> __ -> __) -> 'a1) -> params ->
    18751877    'a1 **)
    1876 let rec params_rect_Type1 h_mk_params x_20773 =
     1878let rec params_rect_Type1 h_mk_params x_1119 =
    18771879  let { stmt_pars = stmt_pars0; stmt_at = stmt_at0; point_of_label =
    1878     point_of_label0; point_of_succ = point_of_succ0 } = x_20773
     1880    point_of_label0; point_of_succ = point_of_succ0 } = x_1119
    18791881  in
    18801882  h_mk_params stmt_pars0 __ __ stmt_at0 point_of_label0 point_of_succ0
     
    18851887    Graphs.label -> __ Types.option) -> (__ -> __ -> __) -> 'a1) -> params ->
    18861888    'a1 **)
    1887 let rec params_rect_Type0 h_mk_params x_20775 =
     1889let rec params_rect_Type0 h_mk_params x_1121 =
    18881890  let { stmt_pars = stmt_pars0; stmt_at = stmt_at0; point_of_label =
    1889     point_of_label0; point_of_succ = point_of_succ0 } = x_20775
     1891    point_of_label0; point_of_succ = point_of_succ0 } = x_1121
    18901892  in
    18911893  h_mk_params stmt_pars0 __ __ stmt_at0 point_of_label0 point_of_succ0
     
    20222024
    20232025(** val lin_params_rect_Type4 : (uns_params -> 'a1) -> lin_params -> 'a1 **)
    2024 let rec lin_params_rect_Type4 h_mk_lin_params x_20798 =
    2025   let l_u_pars = x_20798 in h_mk_lin_params l_u_pars
     2026let rec lin_params_rect_Type4 h_mk_lin_params x_1144 =
     2027  let l_u_pars = x_1144 in h_mk_lin_params l_u_pars
    20262028
    20272029(** val lin_params_rect_Type5 : (uns_params -> 'a1) -> lin_params -> 'a1 **)
    2028 let rec lin_params_rect_Type5 h_mk_lin_params x_20800 =
    2029   let l_u_pars = x_20800 in h_mk_lin_params l_u_pars
     2030let rec lin_params_rect_Type5 h_mk_lin_params x_1146 =
     2031  let l_u_pars = x_1146 in h_mk_lin_params l_u_pars
    20302032
    20312033(** val lin_params_rect_Type3 : (uns_params -> 'a1) -> lin_params -> 'a1 **)
    2032 let rec lin_params_rect_Type3 h_mk_lin_params x_20802 =
    2033   let l_u_pars = x_20802 in h_mk_lin_params l_u_pars
     2034let rec lin_params_rect_Type3 h_mk_lin_params x_1148 =
     2035  let l_u_pars = x_1148 in h_mk_lin_params l_u_pars
    20342036
    20352037(** val lin_params_rect_Type2 : (uns_params -> 'a1) -> lin_params -> 'a1 **)
    2036 let rec lin_params_rect_Type2 h_mk_lin_params x_20804 =
    2037   let l_u_pars = x_20804 in h_mk_lin_params l_u_pars
     2038let rec lin_params_rect_Type2 h_mk_lin_params x_1150 =
     2039  let l_u_pars = x_1150 in h_mk_lin_params l_u_pars
    20382040
    20392041(** val lin_params_rect_Type1 : (uns_params -> 'a1) -> lin_params -> 'a1 **)
    2040 let rec lin_params_rect_Type1 h_mk_lin_params x_20806 =
    2041   let l_u_pars = x_20806 in h_mk_lin_params l_u_pars
     2042let rec lin_params_rect_Type1 h_mk_lin_params x_1152 =
     2043  let l_u_pars = x_1152 in h_mk_lin_params l_u_pars
    20422044
    20432045(** val lin_params_rect_Type0 : (uns_params -> 'a1) -> lin_params -> 'a1 **)
    2044 let rec lin_params_rect_Type0 h_mk_lin_params x_20808 =
    2045   let l_u_pars = x_20808 in h_mk_lin_params l_u_pars
     2046let rec lin_params_rect_Type0 h_mk_lin_params x_1154 =
     2047  let l_u_pars = x_1154 in h_mk_lin_params l_u_pars
    20462048
    20472049(** val l_u_pars : lin_params -> uns_params **)
     
    21172119(** val graph_params_rect_Type4 :
    21182120    (uns_params -> 'a1) -> graph_params -> 'a1 **)
    2119 let rec graph_params_rect_Type4 h_mk_graph_params x_20824 =
    2120   let g_u_pars = x_20824 in h_mk_graph_params g_u_pars
     2121let rec graph_params_rect_Type4 h_mk_graph_params x_1170 =
     2122  let g_u_pars = x_1170 in h_mk_graph_params g_u_pars
    21212123
    21222124(** val graph_params_rect_Type5 :
    21232125    (uns_params -> 'a1) -> graph_params -> 'a1 **)
    2124 let rec graph_params_rect_Type5 h_mk_graph_params x_20826 =
    2125   let g_u_pars = x_20826 in h_mk_graph_params g_u_pars
     2126let rec graph_params_rect_Type5 h_mk_graph_params x_1172 =
     2127  let g_u_pars = x_1172 in h_mk_graph_params g_u_pars
    21262128
    21272129(** val graph_params_rect_Type3 :
    21282130    (uns_params -> 'a1) -> graph_params -> 'a1 **)
    2129 let rec graph_params_rect_Type3 h_mk_graph_params x_20828 =
    2130   let g_u_pars = x_20828 in h_mk_graph_params g_u_pars
     2131let rec graph_params_rect_Type3 h_mk_graph_params x_1174 =
     2132  let g_u_pars = x_1174 in h_mk_graph_params g_u_pars
    21312133
    21322134(** val graph_params_rect_Type2 :
    21332135    (uns_params -> 'a1) -> graph_params -> 'a1 **)
    2134 let rec graph_params_rect_Type2 h_mk_graph_params x_20830 =
    2135   let g_u_pars = x_20830 in h_mk_graph_params g_u_pars
     2136let rec graph_params_rect_Type2 h_mk_graph_params x_1176 =
     2137  let g_u_pars = x_1176 in h_mk_graph_params g_u_pars
    21362138
    21372139(** val graph_params_rect_Type1 :
    21382140    (uns_params -> 'a1) -> graph_params -> 'a1 **)
    2139 let rec graph_params_rect_Type1 h_mk_graph_params x_20832 =
    2140   let g_u_pars = x_20832 in h_mk_graph_params g_u_pars
     2141let rec graph_params_rect_Type1 h_mk_graph_params x_1178 =
     2142  let g_u_pars = x_1178 in h_mk_graph_params g_u_pars
    21412143
    21422144(** val graph_params_rect_Type0 :
    21432145    (uns_params -> 'a1) -> graph_params -> 'a1 **)
    2144 let rec graph_params_rect_Type0 h_mk_graph_params x_20834 =
    2145   let g_u_pars = x_20834 in h_mk_graph_params g_u_pars
     2146let rec graph_params_rect_Type0 h_mk_graph_params x_1180 =
     2147  let g_u_pars = x_1180 in h_mk_graph_params g_u_pars
    21462148
    21472149(** val g_u_pars : graph_params -> uns_params **)
     
    22132215    Identifiers.universe -> __ -> __ -> Nat.nat -> Nat.nat -> __ -> __ ->
    22142216    'a1) -> joint_internal_function -> 'a1 **)
    2215 let rec joint_internal_function_rect_Type4 p globals h_mk_joint_internal_function x_20850 =
     2217let rec joint_internal_function_rect_Type4 p globals h_mk_joint_internal_function x_1196 =
    22162218  let { joint_if_luniverse = joint_if_luniverse0; joint_if_runiverse =
    22172219    joint_if_runiverse0; joint_if_result = joint_if_result0;
     
    22192221    joint_if_stacksize0; joint_if_local_stacksize =
    22202222    joint_if_local_stacksize0; joint_if_code = joint_if_code0;
    2221     joint_if_entry = joint_if_entry0 } = x_20850
     2223    joint_if_entry = joint_if_entry0 } = x_1196
    22222224  in
    22232225  h_mk_joint_internal_function joint_if_luniverse0 joint_if_runiverse0
     
    22292231    Identifiers.universe -> __ -> __ -> Nat.nat -> Nat.nat -> __ -> __ ->
    22302232    'a1) -> joint_internal_function -> 'a1 **)
    2231 let rec joint_internal_function_rect_Type5 p globals h_mk_joint_internal_function x_20852 =
     2233let rec joint_internal_function_rect_Type5 p globals h_mk_joint_internal_function x_1198 =
    22322234  let { joint_if_luniverse = joint_if_luniverse0; joint_if_runiverse =
    22332235    joint_if_runiverse0; joint_if_result = joint_if_result0;
     
    22352237    joint_if_stacksize0; joint_if_local_stacksize =
    22362238    joint_if_local_stacksize0; joint_if_code = joint_if_code0;
    2237     joint_if_entry = joint_if_entry0 } = x_20852
     2239    joint_if_entry = joint_if_entry0 } = x_1198
    22382240  in
    22392241  h_mk_joint_internal_function joint_if_luniverse0 joint_if_runiverse0
     
    22452247    Identifiers.universe -> __ -> __ -> Nat.nat -> Nat.nat -> __ -> __ ->
    22462248    'a1) -> joint_internal_function -> 'a1 **)
    2247 let rec joint_internal_function_rect_Type3 p globals h_mk_joint_internal_function x_20854 =
     2249let rec joint_internal_function_rect_Type3 p globals h_mk_joint_internal_function x_1200 =
    22482250  let { joint_if_luniverse = joint_if_luniverse0; joint_if_runiverse =
    22492251    joint_if_runiverse0; joint_if_result = joint_if_result0;
     
    22512253    joint_if_stacksize0; joint_if_local_stacksize =
    22522254    joint_if_local_stacksize0; joint_if_code = joint_if_code0;
    2253     joint_if_entry = joint_if_entry0 } = x_20854
     2255    joint_if_entry = joint_if_entry0 } = x_1200
    22542256  in
    22552257  h_mk_joint_internal_function joint_if_luniverse0 joint_if_runiverse0
     
    22612263    Identifiers.universe -> __ -> __ -> Nat.nat -> Nat.nat -> __ -> __ ->
    22622264    'a1) -> joint_internal_function -> 'a1 **)
    2263 let rec joint_internal_function_rect_Type2 p globals h_mk_joint_internal_function x_20856 =
     2265let rec joint_internal_function_rect_Type2 p globals h_mk_joint_internal_function x_1202 =
    22642266  let { joint_if_luniverse = joint_if_luniverse0; joint_if_runiverse =
    22652267    joint_if_runiverse0; joint_if_result = joint_if_result0;
     
    22672269    joint_if_stacksize0; joint_if_local_stacksize =
    22682270    joint_if_local_stacksize0; joint_if_code = joint_if_code0;
    2269     joint_if_entry = joint_if_entry0 } = x_20856
     2271    joint_if_entry = joint_if_entry0 } = x_1202
    22702272  in
    22712273  h_mk_joint_internal_function joint_if_luniverse0 joint_if_runiverse0
     
    22772279    Identifiers.universe -> __ -> __ -> Nat.nat -> Nat.nat -> __ -> __ ->
    22782280    'a1) -> joint_internal_function -> 'a1 **)
    2279 let rec joint_internal_function_rect_Type1 p globals h_mk_joint_internal_function x_20858 =
     2281let rec joint_internal_function_rect_Type1 p globals h_mk_joint_internal_function x_1204 =
    22802282  let { joint_if_luniverse = joint_if_luniverse0; joint_if_runiverse =
    22812283    joint_if_runiverse0; joint_if_result = joint_if_result0;
     
    22832285    joint_if_stacksize0; joint_if_local_stacksize =
    22842286    joint_if_local_stacksize0; joint_if_code = joint_if_code0;
    2285     joint_if_entry = joint_if_entry0 } = x_20858
     2287    joint_if_entry = joint_if_entry0 } = x_1204
    22862288  in
    22872289  h_mk_joint_internal_function joint_if_luniverse0 joint_if_runiverse0
     
    22932295    Identifiers.universe -> __ -> __ -> Nat.nat -> Nat.nat -> __ -> __ ->
    22942296    'a1) -> joint_internal_function -> 'a1 **)
    2295 let rec joint_internal_function_rect_Type0 p globals h_mk_joint_internal_function x_20860 =
     2297let rec joint_internal_function_rect_Type0 p globals h_mk_joint_internal_function x_1206 =
    22962298  let { joint_if_luniverse = joint_if_luniverse0; joint_if_runiverse =
    22972299    joint_if_runiverse0; joint_if_result = joint_if_result0;
     
    22992301    joint_if_stacksize0; joint_if_local_stacksize =
    23002302    joint_if_local_stacksize0; joint_if_code = joint_if_code0;
    2301     joint_if_entry = joint_if_entry0 } = x_20860
     2303    joint_if_entry = joint_if_entry0 } = x_1206
    23022304  in
    23032305  h_mk_joint_internal_function joint_if_luniverse0 joint_if_runiverse0
  • extracted/joint_LTL_LIN.ml

    r2827 r2854  
    116116    BitVector.byte -> 'a1) -> registers_move -> 'a1 **)
    117117let rec registers_move_rect_Type4 h_from_acc h_to_acc h_int_to_reg h_int_to_acc = function
    118 | From_acc (x_21503, x_21502) -> h_from_acc x_21503 x_21502
    119 | To_acc (x_21505, x_21504) -> h_to_acc x_21505 x_21504
    120 | Int_to_reg (x_21507, x_21506) -> h_int_to_reg x_21507 x_21506
    121 | Int_to_acc (x_21509, x_21508) -> h_int_to_acc x_21509 x_21508
     118| From_acc (x_1508, x_1507) -> h_from_acc x_1508 x_1507
     119| To_acc (x_1510, x_1509) -> h_to_acc x_1510 x_1509
     120| Int_to_reg (x_1512, x_1511) -> h_int_to_reg x_1512 x_1511
     121| Int_to_acc (x_1514, x_1513) -> h_int_to_acc x_1514 x_1513
    122122
    123123(** val registers_move_rect_Type5 :
     
    126126    BitVector.byte -> 'a1) -> registers_move -> 'a1 **)
    127127let rec registers_move_rect_Type5 h_from_acc h_to_acc h_int_to_reg h_int_to_acc = function
    128 | From_acc (x_21516, x_21515) -> h_from_acc x_21516 x_21515
    129 | To_acc (x_21518, x_21517) -> h_to_acc x_21518 x_21517
    130 | Int_to_reg (x_21520, x_21519) -> h_int_to_reg x_21520 x_21519
    131 | Int_to_acc (x_21522, x_21521) -> h_int_to_acc x_21522 x_21521
     128| From_acc (x_1521, x_1520) -> h_from_acc x_1521 x_1520
     129| To_acc (x_1523, x_1522) -> h_to_acc x_1523 x_1522
     130| Int_to_reg (x_1525, x_1524) -> h_int_to_reg x_1525 x_1524
     131| Int_to_acc (x_1527, x_1526) -> h_int_to_acc x_1527 x_1526
    132132
    133133(** val registers_move_rect_Type3 :
     
    136136    BitVector.byte -> 'a1) -> registers_move -> 'a1 **)
    137137let rec registers_move_rect_Type3 h_from_acc h_to_acc h_int_to_reg h_int_to_acc = function
    138 | From_acc (x_21529, x_21528) -> h_from_acc x_21529 x_21528
    139 | To_acc (x_21531, x_21530) -> h_to_acc x_21531 x_21530
    140 | Int_to_reg (x_21533, x_21532) -> h_int_to_reg x_21533 x_21532
    141 | Int_to_acc (x_21535, x_21534) -> h_int_to_acc x_21535 x_21534
     138| From_acc (x_1534, x_1533) -> h_from_acc x_1534 x_1533
     139| To_acc (x_1536, x_1535) -> h_to_acc x_1536 x_1535
     140| Int_to_reg (x_1538, x_1537) -> h_int_to_reg x_1538 x_1537
     141| Int_to_acc (x_1540, x_1539) -> h_int_to_acc x_1540 x_1539
    142142
    143143(** val registers_move_rect_Type2 :
     
    146146    BitVector.byte -> 'a1) -> registers_move -> 'a1 **)
    147147let rec registers_move_rect_Type2 h_from_acc h_to_acc h_int_to_reg h_int_to_acc = function
    148 | From_acc (x_21542, x_21541) -> h_from_acc x_21542 x_21541
    149 | To_acc (x_21544, x_21543) -> h_to_acc x_21544 x_21543
    150 | Int_to_reg (x_21546, x_21545) -> h_int_to_reg x_21546 x_21545
    151 | Int_to_acc (x_21548, x_21547) -> h_int_to_acc x_21548 x_21547
     148| From_acc (x_1547, x_1546) -> h_from_acc x_1547 x_1546
     149| To_acc (x_1549, x_1548) -> h_to_acc x_1549 x_1548
     150| Int_to_reg (x_1551, x_1550) -> h_int_to_reg x_1551 x_1550
     151| Int_to_acc (x_1553, x_1552) -> h_int_to_acc x_1553 x_1552
    152152
    153153(** val registers_move_rect_Type1 :
     
    156156    BitVector.byte -> 'a1) -> registers_move -> 'a1 **)
    157157let rec registers_move_rect_Type1 h_from_acc h_to_acc h_int_to_reg h_int_to_acc = function
    158 | From_acc (x_21555, x_21554) -> h_from_acc x_21555 x_21554
    159 | To_acc (x_21557, x_21556) -> h_to_acc x_21557 x_21556
    160 | Int_to_reg (x_21559, x_21558) -> h_int_to_reg x_21559 x_21558
    161 | Int_to_acc (x_21561, x_21560) -> h_int_to_acc x_21561 x_21560
     158| From_acc (x_1560, x_1559) -> h_from_acc x_1560 x_1559
     159| To_acc (x_1562, x_1561) -> h_to_acc x_1562 x_1561
     160| Int_to_reg (x_1564, x_1563) -> h_int_to_reg x_1564 x_1563
     161| Int_to_acc (x_1566, x_1565) -> h_int_to_acc x_1566 x_1565
    162162
    163163(** val registers_move_rect_Type0 :
     
    166166    BitVector.byte -> 'a1) -> registers_move -> 'a1 **)
    167167let rec registers_move_rect_Type0 h_from_acc h_to_acc h_int_to_reg h_int_to_acc = function
    168 | From_acc (x_21568, x_21567) -> h_from_acc x_21568 x_21567
    169 | To_acc (x_21570, x_21569) -> h_to_acc x_21570 x_21569
    170 | Int_to_reg (x_21572, x_21571) -> h_int_to_reg x_21572 x_21571
    171 | Int_to_acc (x_21574, x_21573) -> h_int_to_acc x_21574 x_21573
     168| From_acc (x_1573, x_1572) -> h_from_acc x_1573 x_1572
     169| To_acc (x_1575, x_1574) -> h_to_acc x_1575 x_1574
     170| Int_to_reg (x_1577, x_1576) -> h_int_to_reg x_1577 x_1576
     171| Int_to_acc (x_1579, x_1578) -> h_int_to_acc x_1579 x_1578
    172172
    173173(** val registers_move_inv_rect_Type4 :
     
    241241| SAVE_CARRY -> h_SAVE_CARRY
    242242| RESTORE_CARRY -> h_RESTORE_CARRY
    243 | LOW_ADDRESS (x_21668, x_21667) -> h_LOW_ADDRESS x_21668 x_21667
    244 | HIGH_ADDRESS (x_21670, x_21669) -> h_HIGH_ADDRESS x_21670 x_21669
     243| LOW_ADDRESS (x_1673, x_1672) -> h_LOW_ADDRESS x_1673 x_1672
     244| HIGH_ADDRESS (x_1675, x_1674) -> h_HIGH_ADDRESS x_1675 x_1674
    245245
    246246(** val ltl_lin_seq_rect_Type5 :
     
    250250| SAVE_CARRY -> h_SAVE_CARRY
    251251| RESTORE_CARRY -> h_RESTORE_CARRY
    252 | LOW_ADDRESS (x_21677, x_21676) -> h_LOW_ADDRESS x_21677 x_21676
    253 | HIGH_ADDRESS (x_21679, x_21678) -> h_HIGH_ADDRESS x_21679 x_21678
     252| LOW_ADDRESS (x_1682, x_1681) -> h_LOW_ADDRESS x_1682 x_1681
     253| HIGH_ADDRESS (x_1684, x_1683) -> h_HIGH_ADDRESS x_1684 x_1683
    254254
    255255(** val ltl_lin_seq_rect_Type3 :
     
    259259| SAVE_CARRY -> h_SAVE_CARRY
    260260| RESTORE_CARRY -> h_RESTORE_CARRY
    261 | LOW_ADDRESS (x_21686, x_21685) -> h_LOW_ADDRESS x_21686 x_21685
    262 | HIGH_ADDRESS (x_21688, x_21687) -> h_HIGH_ADDRESS x_21688 x_21687
     261| LOW_ADDRESS (x_1691, x_1690) -> h_LOW_ADDRESS x_1691 x_1690
     262| HIGH_ADDRESS (x_1693, x_1692) -> h_HIGH_ADDRESS x_1693 x_1692
    263263
    264264(** val ltl_lin_seq_rect_Type2 :
     
    268268| SAVE_CARRY -> h_SAVE_CARRY
    269269| RESTORE_CARRY -> h_RESTORE_CARRY
    270 | LOW_ADDRESS (x_21695, x_21694) -> h_LOW_ADDRESS x_21695 x_21694
    271 | HIGH_ADDRESS (x_21697, x_21696) -> h_HIGH_ADDRESS x_21697 x_21696
     270| LOW_ADDRESS (x_1700, x_1699) -> h_LOW_ADDRESS x_1700 x_1699
     271| HIGH_ADDRESS (x_1702, x_1701) -> h_HIGH_ADDRESS x_1702 x_1701
    272272
    273273(** val ltl_lin_seq_rect_Type1 :
     
    277277| SAVE_CARRY -> h_SAVE_CARRY
    278278| RESTORE_CARRY -> h_RESTORE_CARRY
    279 | LOW_ADDRESS (x_21704, x_21703) -> h_LOW_ADDRESS x_21704 x_21703
    280 | HIGH_ADDRESS (x_21706, x_21705) -> h_HIGH_ADDRESS x_21706 x_21705
     279| LOW_ADDRESS (x_1709, x_1708) -> h_LOW_ADDRESS x_1709 x_1708
     280| HIGH_ADDRESS (x_1711, x_1710) -> h_HIGH_ADDRESS x_1711 x_1710
    281281
    282282(** val ltl_lin_seq_rect_Type0 :
     
    286286| SAVE_CARRY -> h_SAVE_CARRY
    287287| RESTORE_CARRY -> h_RESTORE_CARRY
    288 | LOW_ADDRESS (x_21713, x_21712) -> h_LOW_ADDRESS x_21713 x_21712
    289 | HIGH_ADDRESS (x_21715, x_21714) -> h_HIGH_ADDRESS x_21715 x_21714
     288| LOW_ADDRESS (x_1718, x_1717) -> h_LOW_ADDRESS x_1718 x_1717
     289| HIGH_ADDRESS (x_1720, x_1719) -> h_HIGH_ADDRESS x_1720 x_1719
    290290
    291291(** val ltl_lin_seq_inv_rect_Type4 :
  • extracted/joint_LTL_LIN_semantics.ml

    r2831 r2854  
    252252    Joint_semantics.setup_call = (fun x x0 x1 st ->
    253253    Obj.magic (Monad.m_return0 (Monad.max_def Errors.res0) st));
    254     Joint_semantics.fetch_external_args = (fun x -> assert false (* absurd case *));
     254    Joint_semantics.fetch_external_args = (fun _ -> assert false (* absurd case *));
    255255    Joint_semantics.set_result = (Obj.magic ltl_lin_set_result);
    256256    Joint_semantics.call_args_for_main = (Obj.magic Nat.O);
     
    261261        (List.map
    262262          (SemanticsUtils.hwreg_retrieve (Obj.magic st.Joint_semantics.regs))
    263           I8051.registerRets))); Joint_semantics.eval_ext_seq = (fun x -> assert false
     263          I8051.registerRets))); Joint_semantics.eval_ext_seq = (fun _ -> assert false
    264264    (* absurd case *)); Joint_semantics.pop_frame = (fun x x0 x1 x2 st ->
    265265    Joint_semantics.pop_ra lTL_LIN_state st) }
  • extracted/lINToASM.ml

    r2827 r2854  
    127127    Identifiers.identifier_map Identifiers.identifier_map -> BitVector.word
    128128    Identifiers.identifier_map -> __ -> 'a1) -> aSM_universe -> 'a1 **)
    129 let rec aSM_universe_rect_Type4 globals h_mk_ASM_universe x_24413 =
     129let rec aSM_universe_rect_Type4 globals h_mk_ASM_universe x_1781 =
    130130  let { id_univ = id_univ0; current_funct = current_funct0; ident_map =
    131     ident_map0; label_map = label_map0; address_map = address_map0 } =
    132     x_24413
     131    ident_map0; label_map = label_map0; address_map = address_map0 } = x_1781
    133132  in
    134133  h_mk_ASM_universe id_univ0 current_funct0 ident_map0 label_map0
     
    140139    Identifiers.identifier_map Identifiers.identifier_map -> BitVector.word
    141140    Identifiers.identifier_map -> __ -> 'a1) -> aSM_universe -> 'a1 **)
    142 let rec aSM_universe_rect_Type5 globals h_mk_ASM_universe x_24415 =
     141let rec aSM_universe_rect_Type5 globals h_mk_ASM_universe x_1783 =
    143142  let { id_univ = id_univ0; current_funct = current_funct0; ident_map =
    144     ident_map0; label_map = label_map0; address_map = address_map0 } =
    145     x_24415
     143    ident_map0; label_map = label_map0; address_map = address_map0 } = x_1783
    146144  in
    147145  h_mk_ASM_universe id_univ0 current_funct0 ident_map0 label_map0
     
    153151    Identifiers.identifier_map Identifiers.identifier_map -> BitVector.word
    154152    Identifiers.identifier_map -> __ -> 'a1) -> aSM_universe -> 'a1 **)
    155 let rec aSM_universe_rect_Type3 globals h_mk_ASM_universe x_24417 =
     153let rec aSM_universe_rect_Type3 globals h_mk_ASM_universe x_1785 =
    156154  let { id_univ = id_univ0; current_funct = current_funct0; ident_map =
    157     ident_map0; label_map = label_map0; address_map = address_map0 } =
    158     x_24417
     155    ident_map0; label_map = label_map0; address_map = address_map0 } = x_1785
    159156  in
    160157  h_mk_ASM_universe id_univ0 current_funct0 ident_map0 label_map0
     
    166163    Identifiers.identifier_map Identifiers.identifier_map -> BitVector.word
    167164    Identifiers.identifier_map -> __ -> 'a1) -> aSM_universe -> 'a1 **)
    168 let rec aSM_universe_rect_Type2 globals h_mk_ASM_universe x_24419 =
     165let rec aSM_universe_rect_Type2 globals h_mk_ASM_universe x_1787 =
    169166  let { id_univ = id_univ0; current_funct = current_funct0; ident_map =
    170     ident_map0; label_map = label_map0; address_map = address_map0 } =
    171     x_24419
     167    ident_map0; label_map = label_map0; address_map = address_map0 } = x_1787
    172168  in
    173169  h_mk_ASM_universe id_univ0 current_funct0 ident_map0 label_map0
     
    179175    Identifiers.identifier_map Identifiers.identifier_map -> BitVector.word
    180176    Identifiers.identifier_map -> __ -> 'a1) -> aSM_universe -> 'a1 **)
    181 let rec aSM_universe_rect_Type1 globals h_mk_ASM_universe x_24421 =
     177let rec aSM_universe_rect_Type1 globals h_mk_ASM_universe x_1789 =
    182178  let { id_univ = id_univ0; current_funct = current_funct0; ident_map =
    183     ident_map0; label_map = label_map0; address_map = address_map0 } =
    184     x_24421
     179    ident_map0; label_map = label_map0; address_map = address_map0 } = x_1789
    185180  in
    186181  h_mk_ASM_universe id_univ0 current_funct0 ident_map0 label_map0
     
    192187    Identifiers.identifier_map Identifiers.identifier_map -> BitVector.word
    193188    Identifiers.identifier_map -> __ -> 'a1) -> aSM_universe -> 'a1 **)
    194 let rec aSM_universe_rect_Type0 globals h_mk_ASM_universe x_24423 =
     189let rec aSM_universe_rect_Type0 globals h_mk_ASM_universe x_1791 =
    195190  let { id_univ = id_univ0; current_funct = current_funct0; ident_map =
    196     ident_map0; label_map = label_map0; address_map = address_map0 } =
    197     x_24423
     191    ident_map0; label_map = label_map0; address_map = address_map0 } = x_1791
    198192  in
    199193  h_mk_ASM_universe id_univ0 current_funct0 ident_map0 label_map0
     
    280274  let globals_addr_internal = fun res_offset x_size ->
    281275    let { Types.fst = res; Types.snd = offset } = res_offset in
    282     let { Types.fst = eta29057; Types.snd = size } = x_size in
    283     let { Types.fst = x; Types.snd = region } = eta29057 in
     276    let { Types.fst = eta37; Types.snd = size } = x_size in
     277    let { Types.fst = x; Types.snd = region } = eta37 in
    284278    { Types.fst =
    285279    (Identifiers.add PreIdentifiers.SymbolTag res x
     
    309303        (Identifiers.empty_map PreIdentifiers.LabelTag)
    310304    in
    311     let { Types.fst = eta29058; Types.snd = lmap0 } =
     305    let { Types.fst = eta38; Types.snd = lmap0 } =
    312306      match Identifiers.lookup PreIdentifiers.LabelTag lmap l with
    313307      | Types.None ->
     
    321315          lmap }
    322316    in
    323     let { Types.fst = id; Types.snd = univ } = eta29058 in
     317    let { Types.fst = id; Types.snd = univ } = eta38 in
    324318    { Types.fst = { id_univ = univ; current_funct = current; ident_map =
    325319    u.ident_map; label_map =
     
    333327  Obj.magic (fun u ->
    334328    let imap = u.ident_map in
    335     let { Types.fst = eta29059; Types.snd = imap0 } =
     329    let { Types.fst = eta39; Types.snd = imap0 } =
    336330      match Identifiers.lookup PreIdentifiers.SymbolTag imap i with
    337331      | Types.None ->
     
    345339          imap }
    346340    in
    347     let { Types.fst = id; Types.snd = univ } = eta29059 in
     341    let { Types.fst = id; Types.snd = univ } = eta39 in
    348342    { Types.fst = { id_univ = univ; current_funct = u.current_funct;
    349343    ident_map = imap0; label_map = u.label_map; address_map =
  • extracted/rTL.ml

    r2827 r2854  
    111111    (Registers.register -> Registers.register -> 'a1) -> rtl_seq -> 'a1 **)
    112112let rec rtl_seq_rect_Type4 h_rtl_stack_address = function
    113 | Rtl_stack_address (x_20906, x_20905) -> h_rtl_stack_address x_20906 x_20905
     113| Rtl_stack_address (x_2091, x_2090) -> h_rtl_stack_address x_2091 x_2090
    114114
    115115(** val rtl_seq_rect_Type5 :
    116116    (Registers.register -> Registers.register -> 'a1) -> rtl_seq -> 'a1 **)
    117117let rec rtl_seq_rect_Type5 h_rtl_stack_address = function
    118 | Rtl_stack_address (x_20910, x_20909) -> h_rtl_stack_address x_20910 x_20909
     118| Rtl_stack_address (x_2095, x_2094) -> h_rtl_stack_address x_2095 x_2094
    119119
    120120(** val rtl_seq_rect_Type3 :
    121121    (Registers.register -> Registers.register -> 'a1) -> rtl_seq -> 'a1 **)
    122122let rec rtl_seq_rect_Type3 h_rtl_stack_address = function
    123 | Rtl_stack_address (x_20914, x_20913) -> h_rtl_stack_address x_20914 x_20913
     123| Rtl_stack_address (x_2099, x_2098) -> h_rtl_stack_address x_2099 x_2098
    124124
    125125(** val rtl_seq_rect_Type2 :
    126126    (Registers.register -> Registers.register -> 'a1) -> rtl_seq -> 'a1 **)
    127127let rec rtl_seq_rect_Type2 h_rtl_stack_address = function
    128 | Rtl_stack_address (x_20918, x_20917) -> h_rtl_stack_address x_20918 x_20917
     128| Rtl_stack_address (x_2103, x_2102) -> h_rtl_stack_address x_2103 x_2102
    129129
    130130(** val rtl_seq_rect_Type1 :
    131131    (Registers.register -> Registers.register -> 'a1) -> rtl_seq -> 'a1 **)
    132132let rec rtl_seq_rect_Type1 h_rtl_stack_address = function
    133 | Rtl_stack_address (x_20922, x_20921) -> h_rtl_stack_address x_20922 x_20921
     133| Rtl_stack_address (x_2107, x_2106) -> h_rtl_stack_address x_2107 x_2106
    134134
    135135(** val rtl_seq_rect_Type0 :
    136136    (Registers.register -> Registers.register -> 'a1) -> rtl_seq -> 'a1 **)
    137137let rec rtl_seq_rect_Type0 h_rtl_stack_address = function
    138 | Rtl_stack_address (x_20926, x_20925) -> h_rtl_stack_address x_20926 x_20925
     138| Rtl_stack_address (x_2111, x_2110) -> h_rtl_stack_address x_2111 x_2110
    139139
    140140(** val rtl_seq_inv_rect_Type4 :
  • extracted/rTLabsToRTL.ml

    r2827 r2854  
    150150    -> 'a1) -> register_type -> 'a1 **)
    151151let rec register_type_rect_Type4 h_register_int h_register_ptr = function
    152 | Register_int x_21128 -> h_register_int x_21128
    153 | Register_ptr (x_21130, x_21129) -> h_register_ptr x_21130 x_21129
     152| Register_int x_2144 -> h_register_int x_2144
     153| Register_ptr (x_2146, x_2145) -> h_register_ptr x_2146 x_2145
    154154
    155155(** val register_type_rect_Type5 :
     
    157157    -> 'a1) -> register_type -> 'a1 **)
    158158let rec register_type_rect_Type5 h_register_int h_register_ptr = function
    159 | Register_int x_21134 -> h_register_int x_21134
    160 | Register_ptr (x_21136, x_21135) -> h_register_ptr x_21136 x_21135
     159| Register_int x_2150 -> h_register_int x_2150
     160| Register_ptr (x_2152, x_2151) -> h_register_ptr x_2152 x_2151
    161161
    162162(** val register_type_rect_Type3 :
     
    164164    -> 'a1) -> register_type -> 'a1 **)
    165165let rec register_type_rect_Type3 h_register_int h_register_ptr = function
    166 | Register_int x_21140 -> h_register_int x_21140
    167 | Register_ptr (x_21142, x_21141) -> h_register_ptr x_21142 x_21141
     166| Register_int x_2156 -> h_register_int x_2156
     167| Register_ptr (x_2158, x_2157) -> h_register_ptr x_2158 x_2157
    168168
    169169(** val register_type_rect_Type2 :
     
    171171    -> 'a1) -> register_type -> 'a1 **)
    172172let rec register_type_rect_Type2 h_register_int h_register_ptr = function
    173 | Register_int x_21146 -> h_register_int x_21146
    174 | Register_ptr (x_21148, x_21147) -> h_register_ptr x_21148 x_21147
     173| Register_int x_2162 -> h_register_int x_2162
     174| Register_ptr (x_2164, x_2163) -> h_register_ptr x_2164 x_2163
    175175
    176176(** val register_type_rect_Type1 :
     
    178178    -> 'a1) -> register_type -> 'a1 **)
    179179let rec register_type_rect_Type1 h_register_int h_register_ptr = function
    180 | Register_int x_21152 -> h_register_int x_21152
    181 | Register_ptr (x_21154, x_21153) -> h_register_ptr x_21154 x_21153
     180| Register_int x_2168 -> h_register_int x_2168
     181| Register_ptr (x_2170, x_2169) -> h_register_ptr x_2170 x_2169
    182182
    183183(** val register_type_rect_Type0 :
     
    185185    -> 'a1) -> register_type -> 'a1 **)
    186186let rec register_type_rect_Type0 h_register_int h_register_ptr = function
    187 | Register_int x_21158 -> h_register_int x_21158
    188 | Register_ptr (x_21160, x_21159) -> h_register_ptr x_21160 x_21159
     187| Register_int x_2174 -> h_register_int x_2174
     188| Register_ptr (x_2176, x_2175) -> h_register_ptr x_2176 x_2175
    189189
    190190(** val register_type_inv_rect_Type4 :
  • extracted/rTLabs_traces.ml

    r2827 r2854  
    296296    'a1) -> Nat.nat -> RTLabs_semantics.state -> (IO.io_out, IO.io_in)
    297297    flat_trace -> will_return -> 'a1 **)
    298 let rec will_return_rect_Type4 ge h_wr_step h_wr_call h_wr_ret h_wr_base x_17709 s x_17708 = function
    299 | Wr_step (s0, tr, s', depth, trace, x_17711) ->
    300   h_wr_step s0 tr s' depth __ trace __ x_17711
     298let rec will_return_rect_Type4 ge h_wr_step h_wr_call h_wr_ret h_wr_base x_2230 s x_2229 = function
     299| Wr_step (s0, tr, s', depth, trace, x_2232) ->
     300  h_wr_step s0 tr s' depth __ trace __ x_2232
    301301    (will_return_rect_Type4 ge h_wr_step h_wr_call h_wr_ret h_wr_base depth
    302       s' trace x_17711)
    303 | Wr_call (s0, tr, s', depth, trace, x_17713) ->
    304   h_wr_call s0 tr s' depth __ trace __ x_17713
     302      s' trace x_2232)
     303| Wr_call (s0, tr, s', depth, trace, x_2234) ->
     304  h_wr_call s0 tr s' depth __ trace __ x_2234
    305305    (will_return_rect_Type4 ge h_wr_step h_wr_call h_wr_ret h_wr_base (Nat.S
    306       depth) s' trace x_17713)
    307 | Wr_ret (s0, tr, s', depth, trace, x_17715) ->
    308   h_wr_ret s0 tr s' depth __ trace __ x_17715
     306      depth) s' trace x_2234)
     307| Wr_ret (s0, tr, s', depth, trace, x_2236) ->
     308  h_wr_ret s0 tr s' depth __ trace __ x_2236
    309309    (will_return_rect_Type4 ge h_wr_step h_wr_call h_wr_ret h_wr_base depth
    310       s' trace x_17715)
     310      s' trace x_2236)
    311311| Wr_base (s0, tr, s', trace) -> h_wr_base s0 tr s' __ trace __
    312312
     
    323323    'a1) -> Nat.nat -> RTLabs_semantics.state -> (IO.io_out, IO.io_in)
    324324    flat_trace -> will_return -> 'a1 **)
    325 let rec will_return_rect_Type3 ge h_wr_step h_wr_call h_wr_ret h_wr_base x_17737 s x_17736 = function
    326 | Wr_step (s0, tr, s', depth, trace, x_17739) ->
    327   h_wr_step s0 tr s' depth __ trace __ x_17739
     325let rec will_return_rect_Type3 ge h_wr_step h_wr_call h_wr_ret h_wr_base x_2258 s x_2257 = function
     326| Wr_step (s0, tr, s', depth, trace, x_2260) ->
     327  h_wr_step s0 tr s' depth __ trace __ x_2260
    328328    (will_return_rect_Type3 ge h_wr_step h_wr_call h_wr_ret h_wr_base depth
    329       s' trace x_17739)
    330 | Wr_call (s0, tr, s', depth, trace, x_17741) ->
    331   h_wr_call s0 tr s' depth __ trace __ x_17741
     329      s' trace x_2260)
     330| Wr_call (s0, tr, s', depth, trace, x_2262) ->
     331  h_wr_call s0 tr s' depth __ trace __ x_2262
    332332    (will_return_rect_Type3 ge h_wr_step h_wr_call h_wr_ret h_wr_base (Nat.S
    333       depth) s' trace x_17741)
    334 | Wr_ret (s0, tr, s', depth, trace, x_17743) ->
    335   h_wr_ret s0 tr s' depth __ trace __ x_17743
     333      depth) s' trace x_2262)
     334| Wr_ret (s0, tr, s', depth, trace, x_2264) ->
     335  h_wr_ret s0 tr s' depth __ trace __ x_2264
    336336    (will_return_rect_Type3 ge h_wr_step h_wr_call h_wr_ret h_wr_base depth
    337       s' trace x_17743)
     337      s' trace x_2264)
    338338| Wr_base (s0, tr, s', trace) -> h_wr_base s0 tr s' __ trace __
    339339
     
    350350    'a1) -> Nat.nat -> RTLabs_semantics.state -> (IO.io_out, IO.io_in)
    351351    flat_trace -> will_return -> 'a1 **)
    352 let rec will_return_rect_Type2 ge h_wr_step h_wr_call h_wr_ret h_wr_base x_17751 s x_17750 = function
    353 | Wr_step (s0, tr, s', depth, trace, x_17753) ->
    354   h_wr_step s0 tr s' depth __ trace __ x_17753
     352let rec will_return_rect_Type2 ge h_wr_step h_wr_call h_wr_ret h_wr_base x_2272 s x_2271 = function
     353| Wr_step (s0, tr, s', depth, trace, x_2274) ->
     354  h_wr_step s0 tr s' depth __ trace __ x_2274
    355355    (will_return_rect_Type2 ge h_wr_step h_wr_call h_wr_ret h_wr_base depth
    356       s' trace x_17753)
    357 | Wr_call (s0, tr, s', depth, trace, x_17755) ->
    358   h_wr_call s0 tr s' depth __ trace __ x_17755
     356      s' trace x_2274)
     357| Wr_call (s0, tr, s', depth, trace, x_2276) ->
     358  h_wr_call s0 tr s' depth __ trace __ x_2276
    359359    (will_return_rect_Type2 ge h_wr_step h_wr_call h_wr_ret h_wr_base (Nat.S
    360       depth) s' trace x_17755)
    361 | Wr_ret (s0, tr, s', depth, trace, x_17757) ->
    362   h_wr_ret s0 tr s' depth __ trace __ x_17757
     360      depth) s' trace x_2276)
     361| Wr_ret (s0, tr, s', depth, trace, x_2278) ->
     362  h_wr_ret s0 tr s' depth __ trace __ x_2278
    363363    (will_return_rect_Type2 ge h_wr_step h_wr_call h_wr_ret h_wr_base depth
    364       s' trace x_17757)
     364      s' trace x_2278)
    365365| Wr_base (s0, tr, s', trace) -> h_wr_base s0 tr s' __ trace __
    366366
     
    377377    'a1) -> Nat.nat -> RTLabs_semantics.state -> (IO.io_out, IO.io_in)
    378378    flat_trace -> will_return -> 'a1 **)
    379 let rec will_return_rect_Type1 ge h_wr_step h_wr_call h_wr_ret h_wr_base x_17765 s x_17764 = function
    380 | Wr_step (s0, tr, s', depth, trace, x_17767) ->
    381   h_wr_step s0 tr s' depth __ trace __ x_17767
     379let rec will_return_rect_Type1 ge h_wr_step h_wr_call h_wr_ret h_wr_base x_2286 s x_2285 = function
     380| Wr_step (s0, tr, s', depth, trace, x_2288) ->
     381  h_wr_step s0 tr s' depth __ trace __ x_2288
    382382    (will_return_rect_Type1 ge h_wr_step h_wr_call h_wr_ret h_wr_base depth
    383       s' trace x_17767)
    384 | Wr_call (s0, tr, s', depth, trace, x_17769) ->
    385   h_wr_call s0 tr s' depth __ trace __ x_17769
     383      s' trace x_2288)
     384| Wr_call (s0, tr, s', depth, trace, x_2290) ->
     385  h_wr_call s0 tr s' depth __ trace __ x_2290
    386386    (will_return_rect_Type1 ge h_wr_step h_wr_call h_wr_ret h_wr_base (Nat.S
    387       depth) s' trace x_17769)
    388 | Wr_ret (s0, tr, s', depth, trace, x_17771) ->
    389   h_wr_ret s0 tr s' depth __ trace __ x_17771
     387      depth) s' trace x_2290)
     388| Wr_ret (s0, tr, s', depth, trace, x_2292) ->
     389  h_wr_ret s0 tr s' depth __ trace __ x_2292
    390390    (will_return_rect_Type1 ge h_wr_step h_wr_call h_wr_ret h_wr_base depth
    391       s' trace x_17771)
     391      s' trace x_2292)
    392392| Wr_base (s0, tr, s', trace) -> h_wr_base s0 tr s' __ trace __
    393393
     
    404404    'a1) -> Nat.nat -> RTLabs_semantics.state -> (IO.io_out, IO.io_in)
    405405    flat_trace -> will_return -> 'a1 **)
    406 let rec will_return_rect_Type0 ge h_wr_step h_wr_call h_wr_ret h_wr_base x_17779 s x_17778 = function
    407 | Wr_step (s0, tr, s', depth, trace, x_17781) ->
    408   h_wr_step s0 tr s' depth __ trace __ x_17781
     406let rec will_return_rect_Type0 ge h_wr_step h_wr_call h_wr_ret h_wr_base x_2300 s x_2299 = function
     407| Wr_step (s0, tr, s', depth, trace, x_2302) ->
     408  h_wr_step s0 tr s' depth __ trace __ x_2302
    409409    (will_return_rect_Type0 ge h_wr_step h_wr_call h_wr_ret h_wr_base depth
    410       s' trace x_17781)
    411 | Wr_call (s0, tr, s', depth, trace, x_17783) ->
    412   h_wr_call s0 tr s' depth __ trace __ x_17783
     410      s' trace x_2302)
     411| Wr_call (s0, tr, s', depth, trace, x_2304) ->
     412  h_wr_call s0 tr s' depth __ trace __ x_2304
    413413    (will_return_rect_Type0 ge h_wr_step h_wr_call h_wr_ret h_wr_base (Nat.S
    414       depth) s' trace x_17783)
    415 | Wr_ret (s0, tr, s', depth, trace, x_17785) ->
    416   h_wr_ret s0 tr s' depth __ trace __ x_17785
     414      depth) s' trace x_2304)
     415| Wr_ret (s0, tr, s', depth, trace, x_2306) ->
     416  h_wr_ret s0 tr s' depth __ trace __ x_2306
    417417    (will_return_rect_Type0 ge h_wr_step h_wr_call h_wr_ret h_wr_base depth
    418       s' trace x_17785)
     418      s' trace x_2306)
    419419| Wr_base (s0, tr, s', trace) -> h_wr_base s0 tr s' __ trace __
    420420
     
    839839    (IO.io_out, IO.io_in) flat_trace -> __ -> 'a1 -> __ -> __ -> 'a2) -> 'a1
    840840    trace_result -> 'a2 **)
    841 let rec trace_result_rect_Type4 ge depth ends start full original_terminates limit h_mk_trace_result x_18320 =
     841let rec trace_result_rect_Type4 ge depth ends start full original_terminates limit h_mk_trace_result x_2841 =
    842842  let { new_state = new_state0; remainder = remainder0; new_trace =
    843     new_trace0; terminates = terminates0 } = x_18320
     843    new_trace0; terminates = terminates0 } = x_2841
    844844  in
    845845  h_mk_trace_result new_state0 remainder0 __ new_trace0 __ terminates0
     
    851851    (IO.io_out, IO.io_in) flat_trace -> __ -> 'a1 -> __ -> __ -> 'a2) -> 'a1
    852852    trace_result -> 'a2 **)
    853 let rec trace_result_rect_Type5 ge depth ends start full original_terminates limit h_mk_trace_result x_18322 =
     853let rec trace_result_rect_Type5 ge depth ends start full original_terminates limit h_mk_trace_result x_2843 =
    854854  let { new_state = new_state0; remainder = remainder0; new_trace =
    855     new_trace0; terminates = terminates0 } = x_18322
     855    new_trace0; terminates = terminates0 } = x_2843
    856856  in
    857857  h_mk_trace_result new_state0 remainder0 __ new_trace0 __ terminates0
     
    863863    (IO.io_out, IO.io_in) flat_trace -> __ -> 'a1 -> __ -> __ -> 'a2) -> 'a1
    864864    trace_result -> 'a2 **)
    865 let rec trace_result_rect_Type3 ge depth ends start full original_terminates limit h_mk_trace_result x_18324 =
     865let rec trace_result_rect_Type3 ge depth ends start full original_terminates limit h_mk_trace_result x_2845 =
    866866  let { new_state = new_state0; remainder = remainder0; new_trace =
    867     new_trace0; terminates = terminates0 } = x_18324
     867    new_trace0; terminates = terminates0 } = x_2845
    868868  in
    869869  h_mk_trace_result new_state0 remainder0 __ new_trace0 __ terminates0
     
    875875    (IO.io_out, IO.io_in) flat_trace -> __ -> 'a1 -> __ -> __ -> 'a2) -> 'a1
    876876    trace_result -> 'a2 **)
    877 let rec trace_result_rect_Type2 ge depth ends start full original_terminates limit h_mk_trace_result x_18326 =
     877let rec trace_result_rect_Type2 ge depth ends start full original_terminates limit h_mk_trace_result x_2847 =
    878878  let { new_state = new_state0; remainder = remainder0; new_trace =
    879     new_trace0; terminates = terminates0 } = x_18326
     879    new_trace0; terminates = terminates0 } = x_2847
    880880  in
    881881  h_mk_trace_result new_state0 remainder0 __ new_trace0 __ terminates0
     
    887887    (IO.io_out, IO.io_in) flat_trace -> __ -> 'a1 -> __ -> __ -> 'a2) -> 'a1
    888888    trace_result -> 'a2 **)
    889 let rec trace_result_rect_Type1 ge depth ends start full original_terminates limit h_mk_trace_result x_18328 =
     889let rec trace_result_rect_Type1 ge depth ends start full original_terminates limit h_mk_trace_result x_2849 =
    890890  let { new_state = new_state0; remainder = remainder0; new_trace =
    891     new_trace0; terminates = terminates0 } = x_18328
     891    new_trace0; terminates = terminates0 } = x_2849
    892892  in
    893893  h_mk_trace_result new_state0 remainder0 __ new_trace0 __ terminates0
     
    899899    (IO.io_out, IO.io_in) flat_trace -> __ -> 'a1 -> __ -> __ -> 'a2) -> 'a1
    900900    trace_result -> 'a2 **)
    901 let rec trace_result_rect_Type0 ge depth ends start full original_terminates limit h_mk_trace_result x_18330 =
     901let rec trace_result_rect_Type0 ge depth ends start full original_terminates limit h_mk_trace_result x_2851 =
    902902  let { new_state = new_state0; remainder = remainder0; new_trace =
    903     new_trace0; terminates = terminates0 } = x_18330
     903    new_trace0; terminates = terminates0 } = x_2851
    904904  in
    905905  h_mk_trace_result new_state0 remainder0 __ new_trace0 __ terminates0
     
    999999    (StructuredTraces.trace_ends_with_ret -> 'a1 trace_result -> 'a2) -> 'a1
    10001000    sub_trace_result -> 'a2 **)
    1001 let rec sub_trace_result_rect_Type4 ge depth start full original_terminates limit h_mk_sub_trace_result x_18348 =
    1002   let { ends = ends0; trace_res = trace_res0 } = x_18348 in
     1001let rec sub_trace_result_rect_Type4 ge depth start full original_terminates limit h_mk_sub_trace_result x_2869 =
     1002  let { ends = ends0; trace_res = trace_res0 } = x_2869 in
    10031003  h_mk_sub_trace_result ends0 trace_res0
    10041004
     
    10081008    (StructuredTraces.trace_ends_with_ret -> 'a1 trace_result -> 'a2) -> 'a1
    10091009    sub_trace_result -> 'a2 **)
    1010 let rec sub_trace_result_rect_Type5 ge depth start full original_terminates limit h_mk_sub_trace_result x_18350 =
    1011   let { ends = ends0; trace_res = trace_res0 } = x_18350 in
     1010let rec sub_trace_result_rect_Type5 ge depth start full original_terminates limit h_mk_sub_trace_result x_2871 =
     1011  let { ends = ends0; trace_res = trace_res0 } = x_2871 in
    10121012  h_mk_sub_trace_result ends0 trace_res0
    10131013
     
    10171017    (StructuredTraces.trace_ends_with_ret -> 'a1 trace_result -> 'a2) -> 'a1
    10181018    sub_trace_result -> 'a2 **)
    1019 let rec sub_trace_result_rect_Type3 ge depth start full original_terminates limit h_mk_sub_trace_result x_18352 =
    1020   let { ends = ends0; trace_res = trace_res0 } = x_18352 in
     1019let rec sub_trace_result_rect_Type3 ge depth start full original_terminates limit h_mk_sub_trace_result x_2873 =
     1020  let { ends = ends0; trace_res = trace_res0 } = x_2873 in
    10211021  h_mk_sub_trace_result ends0 trace_res0
    10221022
     
    10261026    (StructuredTraces.trace_ends_with_ret -> 'a1 trace_result -> 'a2) -> 'a1
    10271027    sub_trace_result -> 'a2 **)
    1028 let rec sub_trace_result_rect_Type2 ge depth start full original_terminates limit h_mk_sub_trace_result x_18354 =
    1029   let { ends = ends0; trace_res = trace_res0 } = x_18354 in
     1028let rec sub_trace_result_rect_Type2 ge depth start full original_terminates limit h_mk_sub_trace_result x_2875 =
     1029  let { ends = ends0; trace_res = trace_res0 } = x_2875 in
    10301030  h_mk_sub_trace_result ends0 trace_res0
    10311031
     
    10351035    (StructuredTraces.trace_ends_with_ret -> 'a1 trace_result -> 'a2) -> 'a1
    10361036    sub_trace_result -> 'a2 **)
    1037 let rec sub_trace_result_rect_Type1 ge depth start full original_terminates limit h_mk_sub_trace_result x_18356 =
    1038   let { ends = ends0; trace_res = trace_res0 } = x_18356 in
     1037let rec sub_trace_result_rect_Type1 ge depth start full original_terminates limit h_mk_sub_trace_result x_2877 =
     1038  let { ends = ends0; trace_res = trace_res0 } = x_2877 in
    10391039  h_mk_sub_trace_result ends0 trace_res0
    10401040
     
    10441044    (StructuredTraces.trace_ends_with_ret -> 'a1 trace_result -> 'a2) -> 'a1
    10451045    sub_trace_result -> 'a2 **)
    1046 let rec sub_trace_result_rect_Type0 ge depth start full original_terminates limit h_mk_sub_trace_result x_18358 =
    1047   let { ends = ends0; trace_res = trace_res0 } = x_18358 in
     1046let rec sub_trace_result_rect_Type0 ge depth start full original_terminates limit h_mk_sub_trace_result x_2879 =
     1047  let { ends = ends0; trace_res = trace_res0 } = x_2879 in
    10481048  h_mk_sub_trace_result ends0 trace_res0
    10491049
     
    15581558    ('a1, 'a2) partial_flat_trace -> 'a3 -> 'a3) -> RTLabs_semantics.state ->
    15591559    RTLabs_semantics.state -> ('a1, 'a2) partial_flat_trace -> 'a3 **)
    1560 let rec partial_flat_trace_rect_Type4 ge h_pft_base h_pft_step x_18693 x_18692 = function
     1560let rec partial_flat_trace_rect_Type4 ge h_pft_base h_pft_step x_3214 x_3213 = function
    15611561| Pft_base (s, tr, s') -> h_pft_base s tr s' __
    1562 | Pft_step (s, tr, s', s'', x_18696) ->
    1563   h_pft_step s tr s' s'' __ x_18696
    1564     (partial_flat_trace_rect_Type4 ge h_pft_base h_pft_step s' s'' x_18696)
     1562| Pft_step (s, tr, s', s'', x_3217) ->
     1563  h_pft_step s tr s' s'' __ x_3217
     1564    (partial_flat_trace_rect_Type4 ge h_pft_base h_pft_step s' s'' x_3217)
    15651565
    15661566(** val partial_flat_trace_rect_Type3 :
     
    15701570    ('a1, 'a2) partial_flat_trace -> 'a3 -> 'a3) -> RTLabs_semantics.state ->
    15711571    RTLabs_semantics.state -> ('a1, 'a2) partial_flat_trace -> 'a3 **)
    1572 let rec partial_flat_trace_rect_Type3 ge h_pft_base h_pft_step x_18709 x_18708 = function
     1572let rec partial_flat_trace_rect_Type3 ge h_pft_base h_pft_step x_3230 x_3229 = function
    15731573| Pft_base (s, tr, s') -> h_pft_base s tr s' __
    1574 | Pft_step (s, tr, s', s'', x_18712) ->
    1575   h_pft_step s tr s' s'' __ x_18712
    1576     (partial_flat_trace_rect_Type3 ge h_pft_base h_pft_step s' s'' x_18712)
     1574| Pft_step (s, tr, s', s'', x_3233) ->
     1575  h_pft_step s tr s' s'' __ x_3233
     1576    (partial_flat_trace_rect_Type3 ge h_pft_base h_pft_step s' s'' x_3233)
    15771577
    15781578(** val partial_flat_trace_rect_Type2 :
     
    15821582    ('a1, 'a2) partial_flat_trace -> 'a3 -> 'a3) -> RTLabs_semantics.state ->
    15831583    RTLabs_semantics.state -> ('a1, 'a2) partial_flat_trace -> 'a3 **)
    1584 let rec partial_flat_trace_rect_Type2 ge h_pft_base h_pft_step x_18717 x_18716 = function
     1584let rec partial_flat_trace_rect_Type2 ge h_pft_base h_pft_step x_3238 x_3237 = function
    15851585| Pft_base (s, tr, s') -> h_pft_base s tr s' __
    1586 | Pft_step (s, tr, s', s'', x_18720) ->
    1587   h_pft_step s tr s' s'' __ x_18720
    1588     (partial_flat_trace_rect_Type2 ge h_pft_base h_pft_step s' s'' x_18720)
     1586| Pft_step (s, tr, s', s'', x_3241) ->
     1587  h_pft_step s tr s' s'' __ x_3241
     1588    (partial_flat_trace_rect_Type2 ge h_pft_base h_pft_step s' s'' x_3241)
    15891589
    15901590(** val partial_flat_trace_rect_Type1 :
     
    15941594    ('a1, 'a2) partial_flat_trace -> 'a3 -> 'a3) -> RTLabs_semantics.state ->
    15951595    RTLabs_semantics.state -> ('a1, 'a2) partial_flat_trace -> 'a3 **)
    1596 let rec partial_flat_trace_rect_Type1 ge h_pft_base h_pft_step x_18725 x_18724 = function
     1596let rec partial_flat_trace_rect_Type1 ge h_pft_base h_pft_step x_3246 x_3245 = function
    15971597| Pft_base (s, tr, s') -> h_pft_base s tr s' __
    1598 | Pft_step (s, tr, s', s'', x_18728) ->
    1599   h_pft_step s tr s' s'' __ x_18728
    1600     (partial_flat_trace_rect_Type1 ge h_pft_base h_pft_step s' s'' x_18728)
     1598| Pft_step (s, tr, s', s'', x_3249) ->
     1599  h_pft_step s tr s' s'' __ x_3249
     1600    (partial_flat_trace_rect_Type1 ge h_pft_base h_pft_step s' s'' x_3249)
    16011601
    16021602(** val partial_flat_trace_rect_Type0 :
     
    16061606    ('a1, 'a2) partial_flat_trace -> 'a3 -> 'a3) -> RTLabs_semantics.state ->
    16071607    RTLabs_semantics.state -> ('a1, 'a2) partial_flat_trace -> 'a3 **)
    1608 let rec partial_flat_trace_rect_Type0 ge h_pft_base h_pft_step x_18733 x_18732 = function
     1608let rec partial_flat_trace_rect_Type0 ge h_pft_base h_pft_step x_3254 x_3253 = function
    16091609| Pft_base (s, tr, s') -> h_pft_base s tr s' __
    1610 | Pft_step (s, tr, s', s'', x_18736) ->
    1611   h_pft_step s tr s' s'' __ x_18736
    1612     (partial_flat_trace_rect_Type0 ge h_pft_base h_pft_step s' s'' x_18736)
     1610| Pft_step (s, tr, s', s'', x_3257) ->
     1611  h_pft_step s tr s' s'' __ x_3257
     1612    (partial_flat_trace_rect_Type0 ge h_pft_base h_pft_step s' s'' x_3257)
    16131613
    16141614(** val partial_flat_trace_inv_rect_Type4 :
  • extracted/translateUtils.ml

    r2827 r2854  
    268268    -> (Graphs.label -> Joint.joint_fin_step -> Blocks.bind_fin_block) -> __
    269269    -> __ -> __ -> __ -> 'a1) -> b_graph_translate_data -> 'a1 **)
    270 let rec b_graph_translate_data_rect_Type4 src dst globals h_mk_b_graph_translate_data x_21032 =
     270let rec b_graph_translate_data_rect_Type4 src dst globals h_mk_b_graph_translate_data x_1808 =
    271271  let { init_ret = init_ret0; init_params = init_params0; init_stack_size =
    272272    init_stack_size0; added_prologue = added_prologue0; new_regs = new_regs0;
    273     f_step = f_step0; f_fin = f_fin0 } = x_21032
     273    f_step = f_step0; f_fin = f_fin0 } = x_1808
    274274  in
    275275  h_mk_b_graph_translate_data init_ret0 init_params0 init_stack_size0
     
    282282    -> (Graphs.label -> Joint.joint_fin_step -> Blocks.bind_fin_block) -> __
    283283    -> __ -> __ -> __ -> 'a1) -> b_graph_translate_data -> 'a1 **)
    284 let rec b_graph_translate_data_rect_Type5 src dst globals h_mk_b_graph_translate_data x_21034 =
     284let rec b_graph_translate_data_rect_Type5 src dst globals h_mk_b_graph_translate_data x_1810 =
    285285  let { init_ret = init_ret0; init_params = init_params0; init_stack_size =
    286286    init_stack_size0; added_prologue = added_prologue0; new_regs = new_regs0;
    287     f_step = f_step0; f_fin = f_fin0 } = x_21034
     287    f_step = f_step0; f_fin = f_fin0 } = x_1810
    288288  in
    289289  h_mk_b_graph_translate_data init_ret0 init_params0 init_stack_size0
     
    296296    -> (Graphs.label -> Joint.joint_fin_step -> Blocks.bind_fin_block) -> __
    297297    -> __ -> __ -> __ -> 'a1) -> b_graph_translate_data -> 'a1 **)
    298 let rec b_graph_translate_data_rect_Type3 src dst globals h_mk_b_graph_translate_data x_21036 =
     298let rec b_graph_translate_data_rect_Type3 src dst globals h_mk_b_graph_translate_data x_1812 =
    299299  let { init_ret = init_ret0; init_params = init_params0; init_stack_size =
    300300    init_stack_size0; added_prologue = added_prologue0; new_regs = new_regs0;
    301     f_step = f_step0; f_fin = f_fin0 } = x_21036
     301    f_step = f_step0; f_fin = f_fin0 } = x_1812
    302302  in
    303303  h_mk_b_graph_translate_data init_ret0 init_params0 init_stack_size0
     
    310310    -> (Graphs.label -> Joint.joint_fin_step -> Blocks.bind_fin_block) -> __
    311311    -> __ -> __ -> __ -> 'a1) -> b_graph_translate_data -> 'a1 **)
    312 let rec b_graph_translate_data_rect_Type2 src dst globals h_mk_b_graph_translate_data x_21038 =
     312let rec b_graph_translate_data_rect_Type2 src dst globals h_mk_b_graph_translate_data x_1814 =
    313313  let { init_ret = init_ret0; init_params = init_params0; init_stack_size =
    314314    init_stack_size0; added_prologue = added_prologue0; new_regs = new_regs0;
    315     f_step = f_step0; f_fin = f_fin0 } = x_21038
     315    f_step = f_step0; f_fin = f_fin0 } = x_1814
    316316  in
    317317  h_mk_b_graph_translate_data init_ret0 init_params0 init_stack_size0
     
    324324    -> (Graphs.label -> Joint.joint_fin_step -> Blocks.bind_fin_block) -> __
    325325    -> __ -> __ -> __ -> 'a1) -> b_graph_translate_data -> 'a1 **)
    326 let rec b_graph_translate_data_rect_Type1 src dst globals h_mk_b_graph_translate_data x_21040 =
     326let rec b_graph_translate_data_rect_Type1 src dst globals h_mk_b_graph_translate_data x_1816 =
    327327  let { init_ret = init_ret0; init_params = init_params0; init_stack_size =
    328328    init_stack_size0; added_prologue = added_prologue0; new_regs = new_regs0;
    329     f_step = f_step0; f_fin = f_fin0 } = x_21040
     329    f_step = f_step0; f_fin = f_fin0 } = x_1816
    330330  in
    331331  h_mk_b_graph_translate_data init_ret0 init_params0 init_stack_size0
     
    338338    -> (Graphs.label -> Joint.joint_fin_step -> Blocks.bind_fin_block) -> __
    339339    -> __ -> __ -> __ -> 'a1) -> b_graph_translate_data -> 'a1 **)
    340 let rec b_graph_translate_data_rect_Type0 src dst globals h_mk_b_graph_translate_data x_21042 =
     340let rec b_graph_translate_data_rect_Type0 src dst globals h_mk_b_graph_translate_data x_1818 =
    341341  let { init_ret = init_ret0; init_params = init_params0; init_stack_size =
    342342    init_stack_size0; added_prologue = added_prologue0; new_regs = new_regs0;
    343     f_step = f_step0; f_fin = f_fin0 } = x_21042
     343    f_step = f_step0; f_fin = f_fin0 } = x_1818
    344344  in
    345345  h_mk_b_graph_translate_data init_ret0 init_params0 init_stack_size0
     
    660660    Joint.graph_params -> AST.ident List.list ->
    661661    Joint.joint_internal_function -> (Graphs.label -> Registers.register
    662     List.list Types.option) -> Registers.register List.list **)
     662    List.list) -> Registers.register List.list **)
    663663let added_registers p g def f_regs =
    664   let f = fun lbl x acc ->
    665     match f_regs lbl with
    666     | Types.None -> acc
    667     | Types.Some regs -> List.append regs acc
    668   in
     664  let f = fun lbl x acc -> List.append (f_regs lbl) acc in
    669665  Identifiers.foldi PreIdentifiers.LabelTag f
    670666    (Obj.magic def.Joint.joint_if_code) List.Nil
  • extracted/translateUtils.mli

    r2827 r2854  
    388388val added_registers :
    389389  Joint.graph_params -> AST.ident List.list -> Joint.joint_internal_function
    390   -> (Graphs.label -> Registers.register List.list Types.option) ->
    391   Registers.register List.list
    392 
     390  -> (Graphs.label -> Registers.register List.list) -> Registers.register
     391  List.list
     392
Note: See TracChangeset for help on using the changeset viewer.