Ignore:
Timestamp:
Mar 25, 2013, 11:30:01 PM (7 years ago)
Author:
sacerdot
Message:

New extraction. Novely: a pre-main is used in the back-end. Initialization
of global data is performed in LINToASM.

Note: the cost-emission of the initialization costlabel in the front-end is
virtual, but not performed in the traces I generate and print. To be fixed
(how?)

File:
1 edited

Legend:

Unmodified
Added
Removed
  • extracted/joint_printer.ml

    r2867 r2951  
    11open Preamble
     2
     3open Extra_bool
     4
     5open Coqlib
     6
     7open Values
     8
     9open FrontEndVal
     10
     11open GenMem
     12
     13open FrontEndMem
     14
     15open Globalenvs
    216
    317open String
     
    411425    (BackEndOps.op2 -> 'a1) -> 'a2) -> 'a1 printing_pass_independent_params
    412426    -> 'a2 **)
    413 let rec printing_pass_independent_params_rect_Type4 h_mk_printing_pass_independent_params x_549 =
     427let rec printing_pass_independent_params_rect_Type4 h_mk_printing_pass_independent_params x_263 =
    414428  let { print_String = print_String0; print_keyword = print_keyword0;
    415429    print_concat = print_concat0; print_empty = print_empty0; print_ident =
    416430    print_ident0; print_costlabel = print_costlabel0; print_label =
    417431    print_label0; print_OpAccs = print_OpAccs0; print_Op1 = print_Op3;
    418     print_Op2 = print_Op4 } = x_549
     432    print_Op2 = print_Op4 } = x_263
    419433  in
    420434  h_mk_printing_pass_independent_params print_String0 print_keyword0
     
    428442    (BackEndOps.op2 -> 'a1) -> 'a2) -> 'a1 printing_pass_independent_params
    429443    -> 'a2 **)
    430 let rec printing_pass_independent_params_rect_Type5 h_mk_printing_pass_independent_params x_551 =
     444let rec printing_pass_independent_params_rect_Type5 h_mk_printing_pass_independent_params x_265 =
    431445  let { print_String = print_String0; print_keyword = print_keyword0;
    432446    print_concat = print_concat0; print_empty = print_empty0; print_ident =
    433447    print_ident0; print_costlabel = print_costlabel0; print_label =
    434448    print_label0; print_OpAccs = print_OpAccs0; print_Op1 = print_Op3;
    435     print_Op2 = print_Op4 } = x_551
     449    print_Op2 = print_Op4 } = x_265
    436450  in
    437451  h_mk_printing_pass_independent_params print_String0 print_keyword0
     
    445459    (BackEndOps.op2 -> 'a1) -> 'a2) -> 'a1 printing_pass_independent_params
    446460    -> 'a2 **)
    447 let rec printing_pass_independent_params_rect_Type3 h_mk_printing_pass_independent_params x_553 =
     461let rec printing_pass_independent_params_rect_Type3 h_mk_printing_pass_independent_params x_267 =
    448462  let { print_String = print_String0; print_keyword = print_keyword0;
    449463    print_concat = print_concat0; print_empty = print_empty0; print_ident =
    450464    print_ident0; print_costlabel = print_costlabel0; print_label =
    451465    print_label0; print_OpAccs = print_OpAccs0; print_Op1 = print_Op3;
    452     print_Op2 = print_Op4 } = x_553
     466    print_Op2 = print_Op4 } = x_267
    453467  in
    454468  h_mk_printing_pass_independent_params print_String0 print_keyword0
     
    462476    (BackEndOps.op2 -> 'a1) -> 'a2) -> 'a1 printing_pass_independent_params
    463477    -> 'a2 **)
    464 let rec printing_pass_independent_params_rect_Type2 h_mk_printing_pass_independent_params x_555 =
     478let rec printing_pass_independent_params_rect_Type2 h_mk_printing_pass_independent_params x_269 =
    465479  let { print_String = print_String0; print_keyword = print_keyword0;
    466480    print_concat = print_concat0; print_empty = print_empty0; print_ident =
    467481    print_ident0; print_costlabel = print_costlabel0; print_label =
    468482    print_label0; print_OpAccs = print_OpAccs0; print_Op1 = print_Op3;
    469     print_Op2 = print_Op4 } = x_555
     483    print_Op2 = print_Op4 } = x_269
    470484  in
    471485  h_mk_printing_pass_independent_params print_String0 print_keyword0
     
    479493    (BackEndOps.op2 -> 'a1) -> 'a2) -> 'a1 printing_pass_independent_params
    480494    -> 'a2 **)
    481 let rec printing_pass_independent_params_rect_Type1 h_mk_printing_pass_independent_params x_557 =
     495let rec printing_pass_independent_params_rect_Type1 h_mk_printing_pass_independent_params x_271 =
    482496  let { print_String = print_String0; print_keyword = print_keyword0;
    483497    print_concat = print_concat0; print_empty = print_empty0; print_ident =
    484498    print_ident0; print_costlabel = print_costlabel0; print_label =
    485499    print_label0; print_OpAccs = print_OpAccs0; print_Op1 = print_Op3;
    486     print_Op2 = print_Op4 } = x_557
     500    print_Op2 = print_Op4 } = x_271
    487501  in
    488502  h_mk_printing_pass_independent_params print_String0 print_keyword0
     
    496510    (BackEndOps.op2 -> 'a1) -> 'a2) -> 'a1 printing_pass_independent_params
    497511    -> 'a2 **)
    498 let rec printing_pass_independent_params_rect_Type0 h_mk_printing_pass_independent_params x_559 =
     512let rec printing_pass_independent_params_rect_Type0 h_mk_printing_pass_independent_params x_273 =
    499513  let { print_String = print_String0; print_keyword = print_keyword0;
    500514    print_concat = print_concat0; print_empty = print_empty0; print_ident =
    501515    print_ident0; print_costlabel = print_costlabel0; print_label =
    502516    print_label0; print_OpAccs = print_OpAccs0; print_Op1 = print_Op3;
    503     print_Op2 = print_Op4 } = x_559
     517    print_Op2 = print_Op4 } = x_273
    504518  in
    505519  h_mk_printing_pass_independent_params print_String0 print_keyword0
     
    635649    -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> 'a2) -> 'a1
    636650    printing_params -> 'a2 **)
    637 let rec printing_params_rect_Type4 p h_mk_printing_params x_585 =
     651let rec printing_params_rect_Type4 p h_mk_printing_params x_299 =
    638652  let { print_pass_ind = print_pass_ind0; print_acc_a_reg = print_acc_a_reg0;
    639653    print_acc_b_reg = print_acc_b_reg0; print_acc_a_arg = print_acc_a_arg0;
     
    643657    print_pair_move = print_pair_move0; print_call_args = print_call_args0;
    644658    print_call_dest = print_call_dest0; print_ext_seq = print_ext_seq0 } =
    645     x_585
     659    x_299
    646660  in
    647661  h_mk_printing_params print_pass_ind0 print_acc_a_reg0 print_acc_b_reg0
     
    656670    -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> 'a2) -> 'a1
    657671    printing_params -> 'a2 **)
    658 let rec printing_params_rect_Type5 p h_mk_printing_params x_587 =
     672let rec printing_params_rect_Type5 p h_mk_printing_params x_301 =
    659673  let { print_pass_ind = print_pass_ind0; print_acc_a_reg = print_acc_a_reg0;
    660674    print_acc_b_reg = print_acc_b_reg0; print_acc_a_arg = print_acc_a_arg0;
     
    664678    print_pair_move = print_pair_move0; print_call_args = print_call_args0;
    665679    print_call_dest = print_call_dest0; print_ext_seq = print_ext_seq0 } =
    666     x_587
     680    x_301
    667681  in
    668682  h_mk_printing_params print_pass_ind0 print_acc_a_reg0 print_acc_b_reg0
     
    677691    -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> 'a2) -> 'a1
    678692    printing_params -> 'a2 **)
    679 let rec printing_params_rect_Type3 p h_mk_printing_params x_589 =
     693let rec printing_params_rect_Type3 p h_mk_printing_params x_303 =
    680694  let { print_pass_ind = print_pass_ind0; print_acc_a_reg = print_acc_a_reg0;
    681695    print_acc_b_reg = print_acc_b_reg0; print_acc_a_arg = print_acc_a_arg0;
     
    685699    print_pair_move = print_pair_move0; print_call_args = print_call_args0;
    686700    print_call_dest = print_call_dest0; print_ext_seq = print_ext_seq0 } =
    687     x_589
     701    x_303
    688702  in
    689703  h_mk_printing_params print_pass_ind0 print_acc_a_reg0 print_acc_b_reg0
     
    698712    -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> 'a2) -> 'a1
    699713    printing_params -> 'a2 **)
    700 let rec printing_params_rect_Type2 p h_mk_printing_params x_591 =
     714let rec printing_params_rect_Type2 p h_mk_printing_params x_305 =
    701715  let { print_pass_ind = print_pass_ind0; print_acc_a_reg = print_acc_a_reg0;
    702716    print_acc_b_reg = print_acc_b_reg0; print_acc_a_arg = print_acc_a_arg0;
     
    706720    print_pair_move = print_pair_move0; print_call_args = print_call_args0;
    707721    print_call_dest = print_call_dest0; print_ext_seq = print_ext_seq0 } =
    708     x_591
     722    x_305
    709723  in
    710724  h_mk_printing_params print_pass_ind0 print_acc_a_reg0 print_acc_b_reg0
     
    719733    -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> 'a2) -> 'a1
    720734    printing_params -> 'a2 **)
    721 let rec printing_params_rect_Type1 p h_mk_printing_params x_593 =
     735let rec printing_params_rect_Type1 p h_mk_printing_params x_307 =
    722736  let { print_pass_ind = print_pass_ind0; print_acc_a_reg = print_acc_a_reg0;
    723737    print_acc_b_reg = print_acc_b_reg0; print_acc_a_arg = print_acc_a_arg0;
     
    727741    print_pair_move = print_pair_move0; print_call_args = print_call_args0;
    728742    print_call_dest = print_call_dest0; print_ext_seq = print_ext_seq0 } =
    729     x_593
     743    x_307
    730744  in
    731745  h_mk_printing_params print_pass_ind0 print_acc_a_reg0 print_acc_b_reg0
     
    740754    -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> 'a2) -> 'a1
    741755    printing_params -> 'a2 **)
    742 let rec printing_params_rect_Type0 p h_mk_printing_params x_595 =
     756let rec printing_params_rect_Type0 p h_mk_printing_params x_309 =
    743757  let { print_pass_ind = print_pass_ind0; print_acc_a_reg = print_acc_a_reg0;
    744758    print_acc_b_reg = print_acc_b_reg0; print_acc_a_arg = print_acc_a_arg0;
     
    748762    print_pair_move = print_pair_move0; print_call_args = print_call_args0;
    749763    print_call_dest = print_call_dest0; print_ext_seq = print_ext_seq0 } =
    750     x_595
     764    x_309
    751765  in
    752766  h_mk_printing_params print_pass_ind0 print_acc_a_reg0 print_acc_b_reg0
     
    925939    Joint.joint_statement -> __ -> __) -> __ -> __ -> __) -> (__ -> 'a1) ->
    926940    (__ -> 'a1) -> 'a2) -> 'a1 code_iteration_params -> 'a2 **)
    927 let rec code_iteration_params_rect_Type4 p globals h_mk_code_iteration_params x_624 =
     941let rec code_iteration_params_rect_Type4 p globals h_mk_code_iteration_params x_338 =
    928942  let { fold_code = fold_code0; print_succ = print_succ0; print_code_point =
    929     print_code_point0 } = x_624
     943    print_code_point0 } = x_338
    930944  in
    931945  h_mk_code_iteration_params fold_code0 print_succ0 print_code_point0
     
    935949    Joint.joint_statement -> __ -> __) -> __ -> __ -> __) -> (__ -> 'a1) ->
    936950    (__ -> 'a1) -> 'a2) -> 'a1 code_iteration_params -> 'a2 **)
    937 let rec code_iteration_params_rect_Type5 p globals h_mk_code_iteration_params x_626 =
     951let rec code_iteration_params_rect_Type5 p globals h_mk_code_iteration_params x_340 =
    938952  let { fold_code = fold_code0; print_succ = print_succ0; print_code_point =
    939     print_code_point0 } = x_626
     953    print_code_point0 } = x_340
    940954  in
    941955  h_mk_code_iteration_params fold_code0 print_succ0 print_code_point0
     
    945959    Joint.joint_statement -> __ -> __) -> __ -> __ -> __) -> (__ -> 'a1) ->
    946960    (__ -> 'a1) -> 'a2) -> 'a1 code_iteration_params -> 'a2 **)
    947 let rec code_iteration_params_rect_Type3 p globals h_mk_code_iteration_params x_628 =
     961let rec code_iteration_params_rect_Type3 p globals h_mk_code_iteration_params x_342 =
    948962  let { fold_code = fold_code0; print_succ = print_succ0; print_code_point =
    949     print_code_point0 } = x_628
     963    print_code_point0 } = x_342
    950964  in
    951965  h_mk_code_iteration_params fold_code0 print_succ0 print_code_point0
     
    955969    Joint.joint_statement -> __ -> __) -> __ -> __ -> __) -> (__ -> 'a1) ->
    956970    (__ -> 'a1) -> 'a2) -> 'a1 code_iteration_params -> 'a2 **)
    957 let rec code_iteration_params_rect_Type2 p globals h_mk_code_iteration_params x_630 =
     971let rec code_iteration_params_rect_Type2 p globals h_mk_code_iteration_params x_344 =
    958972  let { fold_code = fold_code0; print_succ = print_succ0; print_code_point =
    959     print_code_point0 } = x_630
     973    print_code_point0 } = x_344
    960974  in
    961975  h_mk_code_iteration_params fold_code0 print_succ0 print_code_point0
     
    965979    Joint.joint_statement -> __ -> __) -> __ -> __ -> __) -> (__ -> 'a1) ->
    966980    (__ -> 'a1) -> 'a2) -> 'a1 code_iteration_params -> 'a2 **)
    967 let rec code_iteration_params_rect_Type1 p globals h_mk_code_iteration_params x_632 =
     981let rec code_iteration_params_rect_Type1 p globals h_mk_code_iteration_params x_346 =
    968982  let { fold_code = fold_code0; print_succ = print_succ0; print_code_point =
    969     print_code_point0 } = x_632
     983    print_code_point0 } = x_346
    970984  in
    971985  h_mk_code_iteration_params fold_code0 print_succ0 print_code_point0
     
    975989    Joint.joint_statement -> __ -> __) -> __ -> __ -> __) -> (__ -> 'a1) ->
    976990    (__ -> 'a1) -> 'a2) -> 'a1 code_iteration_params -> 'a2 **)
    977 let rec code_iteration_params_rect_Type0 p globals h_mk_code_iteration_params x_634 =
     991let rec code_iteration_params_rect_Type0 p globals h_mk_code_iteration_params x_348 =
    978992  let { fold_code = fold_code0; print_succ = print_succ0; print_code_point =
    979     print_code_point0 } = x_634
     993    print_code_point0 } = x_348
    980994  in
    981995  h_mk_code_iteration_params fold_code0 print_succ0 print_code_point0
     
    984998    Joint.params -> AST.ident List.list -> 'a1 code_iteration_params -> (__
    985999    -> Joint.joint_statement -> 'a2 -> 'a2) -> __ -> 'a2 -> 'a2 **)
    986 let rec fold_code0 p globals xxx x_650 x_651 x_652 =
     1000let rec fold_code0 p globals xxx x_364 x_365 x_366 =
    9871001  (let { fold_code = yyy; print_succ = x; print_code_point = x0 } = xxx in
    988   Obj.magic yyy) __ x_650 x_651 x_652
     1002  Obj.magic yyy) __ x_364 x_365 x_366
    9891003
    9901004(** val print_succ :
     
    10671081   | Types.None -> b
    10681082   | Types.Some res ->
    1069      let { Types.fst = eta6; Types.snd = m' } = res in
    1070      let { Types.fst = pos; Types.snd = a } = eta6 in
     1083     let { Types.fst = eta2; Types.snd = m' } = res in
     1084     let { Types.fst = pos; Types.snd = a } = eta2 in
    10711085     visit_graph next f (f pos a b) (next a) m' y)
    10721086
     
    12351249  List.foldr (fun f acc -> List.Cons ({ Types.fst = f.Types.fst; Types.snd =
    12361250    (print_joint_function p
    1237       (List.map (fun x -> x.Types.fst.Types.fst) prog.AST.prog_vars) cip pp
    1238       f.Types.snd) }, acc)) List.Nil prog.AST.prog_funct
    1239 
     1251      (List.map (fun x -> x.Types.fst.Types.fst)
     1252        prog.Joint.joint_prog.AST.prog_vars) cip pp f.Types.snd) }, acc))
     1253    List.Nil prog.Joint.joint_prog.AST.prog_funct
     1254
Note: See TracChangeset for help on using the changeset viewer.