Changeset 2974


Ignore:
Timestamp:
Mar 27, 2013, 4:03:51 PM (4 years ago)
Author:
sacerdot
Message:

New extraction.

Location:
extracted
Files:
4 edited

Legend:

Unmodified
Added
Removed
  • extracted/semanticsUtils.ml

    r2960 r2974  
    168168    (ByteValues.beval BitVectorTrie.bitVectorTrie -> ByteValues.bebit -> 'a1)
    169169    -> hw_register_env -> 'a1 **)
    170 let rec hw_register_env_rect_Type4 h_mk_hw_register_env x_432 =
    171   let { reg_env = reg_env0; other_bit = other_bit0 } = x_432 in
     170let rec hw_register_env_rect_Type4 h_mk_hw_register_env x_101 =
     171  let { reg_env = reg_env0; other_bit = other_bit0 } = x_101 in
    172172  h_mk_hw_register_env reg_env0 other_bit0
    173173
     
    175175    (ByteValues.beval BitVectorTrie.bitVectorTrie -> ByteValues.bebit -> 'a1)
    176176    -> hw_register_env -> 'a1 **)
    177 let rec hw_register_env_rect_Type5 h_mk_hw_register_env x_434 =
    178   let { reg_env = reg_env0; other_bit = other_bit0 } = x_434 in
     177let rec hw_register_env_rect_Type5 h_mk_hw_register_env x_103 =
     178  let { reg_env = reg_env0; other_bit = other_bit0 } = x_103 in
    179179  h_mk_hw_register_env reg_env0 other_bit0
    180180
     
    182182    (ByteValues.beval BitVectorTrie.bitVectorTrie -> ByteValues.bebit -> 'a1)
    183183    -> hw_register_env -> 'a1 **)
    184 let rec hw_register_env_rect_Type3 h_mk_hw_register_env x_436 =
    185   let { reg_env = reg_env0; other_bit = other_bit0 } = x_436 in
     184let rec hw_register_env_rect_Type3 h_mk_hw_register_env x_105 =
     185  let { reg_env = reg_env0; other_bit = other_bit0 } = x_105 in
    186186  h_mk_hw_register_env reg_env0 other_bit0
    187187
     
    189189    (ByteValues.beval BitVectorTrie.bitVectorTrie -> ByteValues.bebit -> 'a1)
    190190    -> hw_register_env -> 'a1 **)
    191 let rec hw_register_env_rect_Type2 h_mk_hw_register_env x_438 =
    192   let { reg_env = reg_env0; other_bit = other_bit0 } = x_438 in
     191let rec hw_register_env_rect_Type2 h_mk_hw_register_env x_107 =
     192  let { reg_env = reg_env0; other_bit = other_bit0 } = x_107 in
    193193  h_mk_hw_register_env reg_env0 other_bit0
    194194
     
    196196    (ByteValues.beval BitVectorTrie.bitVectorTrie -> ByteValues.bebit -> 'a1)
    197197    -> hw_register_env -> 'a1 **)
    198 let rec hw_register_env_rect_Type1 h_mk_hw_register_env x_440 =
    199   let { reg_env = reg_env0; other_bit = other_bit0 } = x_440 in
     198let rec hw_register_env_rect_Type1 h_mk_hw_register_env x_109 =
     199  let { reg_env = reg_env0; other_bit = other_bit0 } = x_109 in
    200200  h_mk_hw_register_env reg_env0 other_bit0
    201201
     
    203203    (ByteValues.beval BitVectorTrie.bitVectorTrie -> ByteValues.bebit -> 'a1)
    204204    -> hw_register_env -> 'a1 **)
    205 let rec hw_register_env_rect_Type0 h_mk_hw_register_env x_442 =
    206   let { reg_env = reg_env0; other_bit = other_bit0 } = x_442 in
     205let rec hw_register_env_rect_Type0 h_mk_hw_register_env x_111 =
     206  let { reg_env = reg_env0; other_bit = other_bit0 } = x_111 in
    207207  h_mk_hw_register_env reg_env0 other_bit0
    208208
     
    319319    -> (Joint.joint_program -> Joint.joint_closed_internal_function) -> 'a1)
    320320    -> sem_graph_params -> 'a1 **)
    321 let rec sem_graph_params_rect_Type4 h_mk_sem_graph_params x_458 =
     321let rec sem_graph_params_rect_Type4 h_mk_sem_graph_params x_127 =
    322322  let { sgp_pars = sgp_pars0; sgp_sup = sgp_sup0; graph_pre_main_generator =
    323     graph_pre_main_generator0 } = x_458
     323    graph_pre_main_generator0 } = x_127
    324324  in
    325325  h_mk_sem_graph_params sgp_pars0 sgp_sup0 graph_pre_main_generator0
     
    329329    -> (Joint.joint_program -> Joint.joint_closed_internal_function) -> 'a1)
    330330    -> sem_graph_params -> 'a1 **)
    331 let rec sem_graph_params_rect_Type5 h_mk_sem_graph_params x_460 =
     331let rec sem_graph_params_rect_Type5 h_mk_sem_graph_params x_129 =
    332332  let { sgp_pars = sgp_pars0; sgp_sup = sgp_sup0; graph_pre_main_generator =
    333     graph_pre_main_generator0 } = x_460
     333    graph_pre_main_generator0 } = x_129
    334334  in
    335335  h_mk_sem_graph_params sgp_pars0 sgp_sup0 graph_pre_main_generator0
     
    339339    -> (Joint.joint_program -> Joint.joint_closed_internal_function) -> 'a1)
    340340    -> sem_graph_params -> 'a1 **)
    341 let rec sem_graph_params_rect_Type3 h_mk_sem_graph_params x_462 =
     341let rec sem_graph_params_rect_Type3 h_mk_sem_graph_params x_131 =
    342342  let { sgp_pars = sgp_pars0; sgp_sup = sgp_sup0; graph_pre_main_generator =
    343     graph_pre_main_generator0 } = x_462
     343    graph_pre_main_generator0 } = x_131
    344344  in
    345345  h_mk_sem_graph_params sgp_pars0 sgp_sup0 graph_pre_main_generator0
     
    349349    -> (Joint.joint_program -> Joint.joint_closed_internal_function) -> 'a1)
    350350    -> sem_graph_params -> 'a1 **)
    351 let rec sem_graph_params_rect_Type2 h_mk_sem_graph_params x_464 =
     351let rec sem_graph_params_rect_Type2 h_mk_sem_graph_params x_133 =
    352352  let { sgp_pars = sgp_pars0; sgp_sup = sgp_sup0; graph_pre_main_generator =
    353     graph_pre_main_generator0 } = x_464
     353    graph_pre_main_generator0 } = x_133
    354354  in
    355355  h_mk_sem_graph_params sgp_pars0 sgp_sup0 graph_pre_main_generator0
     
    359359    -> (Joint.joint_program -> Joint.joint_closed_internal_function) -> 'a1)
    360360    -> sem_graph_params -> 'a1 **)
    361 let rec sem_graph_params_rect_Type1 h_mk_sem_graph_params x_466 =
     361let rec sem_graph_params_rect_Type1 h_mk_sem_graph_params x_135 =
    362362  let { sgp_pars = sgp_pars0; sgp_sup = sgp_sup0; graph_pre_main_generator =
    363     graph_pre_main_generator0 } = x_466
     363    graph_pre_main_generator0 } = x_135
    364364  in
    365365  h_mk_sem_graph_params sgp_pars0 sgp_sup0 graph_pre_main_generator0
     
    369369    -> (Joint.joint_program -> Joint.joint_closed_internal_function) -> 'a1)
    370370    -> sem_graph_params -> 'a1 **)
    371 let rec sem_graph_params_rect_Type0 h_mk_sem_graph_params x_468 =
     371let rec sem_graph_params_rect_Type0 h_mk_sem_graph_params x_137 =
    372372  let { sgp_pars = sgp_pars0; sgp_sup = sgp_sup0; graph_pre_main_generator =
    373     graph_pre_main_generator0 } = x_468
     373    graph_pre_main_generator0 } = x_137
    374374  in
    375375  h_mk_sem_graph_params sgp_pars0 sgp_sup0 graph_pre_main_generator0
     
    501501    -> (Joint.joint_program -> Joint.joint_closed_internal_function) -> 'a1)
    502502    -> sem_lin_params -> 'a1 **)
    503 let rec sem_lin_params_rect_Type4 h_mk_sem_lin_params x_485 =
     503let rec sem_lin_params_rect_Type4 h_mk_sem_lin_params x_154 =
    504504  let { slp_pars = slp_pars0; slp_sup = slp_sup0; lin_pre_main_generator =
    505     lin_pre_main_generator0 } = x_485
     505    lin_pre_main_generator0 } = x_154
    506506  in
    507507  h_mk_sem_lin_params slp_pars0 slp_sup0 lin_pre_main_generator0
     
    511511    -> (Joint.joint_program -> Joint.joint_closed_internal_function) -> 'a1)
    512512    -> sem_lin_params -> 'a1 **)
    513 let rec sem_lin_params_rect_Type5 h_mk_sem_lin_params x_487 =
     513let rec sem_lin_params_rect_Type5 h_mk_sem_lin_params x_156 =
    514514  let { slp_pars = slp_pars0; slp_sup = slp_sup0; lin_pre_main_generator =
    515     lin_pre_main_generator0 } = x_487
     515    lin_pre_main_generator0 } = x_156
    516516  in
    517517  h_mk_sem_lin_params slp_pars0 slp_sup0 lin_pre_main_generator0
     
    521521    -> (Joint.joint_program -> Joint.joint_closed_internal_function) -> 'a1)
    522522    -> sem_lin_params -> 'a1 **)
    523 let rec sem_lin_params_rect_Type3 h_mk_sem_lin_params x_489 =
     523let rec sem_lin_params_rect_Type3 h_mk_sem_lin_params x_158 =
    524524  let { slp_pars = slp_pars0; slp_sup = slp_sup0; lin_pre_main_generator =
    525     lin_pre_main_generator0 } = x_489
     525    lin_pre_main_generator0 } = x_158
    526526  in
    527527  h_mk_sem_lin_params slp_pars0 slp_sup0 lin_pre_main_generator0
     
    531531    -> (Joint.joint_program -> Joint.joint_closed_internal_function) -> 'a1)
    532532    -> sem_lin_params -> 'a1 **)
    533 let rec sem_lin_params_rect_Type2 h_mk_sem_lin_params x_491 =
     533let rec sem_lin_params_rect_Type2 h_mk_sem_lin_params x_160 =
    534534  let { slp_pars = slp_pars0; slp_sup = slp_sup0; lin_pre_main_generator =
    535     lin_pre_main_generator0 } = x_491
     535    lin_pre_main_generator0 } = x_160
    536536  in
    537537  h_mk_sem_lin_params slp_pars0 slp_sup0 lin_pre_main_generator0
     
    541541    -> (Joint.joint_program -> Joint.joint_closed_internal_function) -> 'a1)
    542542    -> sem_lin_params -> 'a1 **)
    543 let rec sem_lin_params_rect_Type1 h_mk_sem_lin_params x_493 =
     543let rec sem_lin_params_rect_Type1 h_mk_sem_lin_params x_162 =
    544544  let { slp_pars = slp_pars0; slp_sup = slp_sup0; lin_pre_main_generator =
    545     lin_pre_main_generator0 } = x_493
     545    lin_pre_main_generator0 } = x_162
    546546  in
    547547  h_mk_sem_lin_params slp_pars0 slp_sup0 lin_pre_main_generator0
     
    551551    -> (Joint.joint_program -> Joint.joint_closed_internal_function) -> 'a1)
    552552    -> sem_lin_params -> 'a1 **)
    553 let rec sem_lin_params_rect_Type0 h_mk_sem_lin_params x_495 =
     553let rec sem_lin_params_rect_Type0 h_mk_sem_lin_params x_164 =
    554554  let { slp_pars = slp_pars0; slp_sup = slp_sup0; lin_pre_main_generator =
    555     lin_pre_main_generator0 } = x_495
     555    lin_pre_main_generator0 } = x_164
    556556  in
    557557  h_mk_sem_lin_params slp_pars0 slp_sup0 lin_pre_main_generator0
  • extracted/toRTLabs.ml

    r2951 r2974  
    121121  List.foldr (fun idt rsengen ->
    122122    let { Types.fst = id; Types.snd = ty } = idt in
    123     let { Types.fst = eta2914; Types.snd = gen0 } = rsengen in
    124     let { Types.fst = rs; Types.snd = en0 } = eta2914 in
     123    let { Types.fst = eta166; Types.snd = gen0 } = rsengen in
     124    let { Types.fst = rs; Types.snd = en0 } = eta166 in
    125125    let { Types.fst = r; Types.snd = gen' } =
    126126      Identifiers.fresh PreIdentifiers.RegisterTag gen0
     
    142142    (Identifiers.identifier_set -> env -> AST.typ Types.option -> 'a1) ->
    143143    fixed -> 'a1 **)
    144 let rec fixed_rect_Type4 h_mk_fixed x_15525 =
     144let rec fixed_rect_Type4 h_mk_fixed x_207 =
    145145  let { fx_gotos = fx_gotos0; fx_env = fx_env0; fx_rettyp = fx_rettyp0 } =
    146     x_15525
     146    x_207
    147147  in
    148148  h_mk_fixed fx_gotos0 fx_env0 fx_rettyp0
     
    151151    (Identifiers.identifier_set -> env -> AST.typ Types.option -> 'a1) ->
    152152    fixed -> 'a1 **)
    153 let rec fixed_rect_Type5 h_mk_fixed x_15527 =
     153let rec fixed_rect_Type5 h_mk_fixed x_209 =
    154154  let { fx_gotos = fx_gotos0; fx_env = fx_env0; fx_rettyp = fx_rettyp0 } =
    155     x_15527
     155    x_209
    156156  in
    157157  h_mk_fixed fx_gotos0 fx_env0 fx_rettyp0
     
    160160    (Identifiers.identifier_set -> env -> AST.typ Types.option -> 'a1) ->
    161161    fixed -> 'a1 **)
    162 let rec fixed_rect_Type3 h_mk_fixed x_15529 =
     162let rec fixed_rect_Type3 h_mk_fixed x_211 =
    163163  let { fx_gotos = fx_gotos0; fx_env = fx_env0; fx_rettyp = fx_rettyp0 } =
    164     x_15529
     164    x_211
    165165  in
    166166  h_mk_fixed fx_gotos0 fx_env0 fx_rettyp0
     
    169169    (Identifiers.identifier_set -> env -> AST.typ Types.option -> 'a1) ->
    170170    fixed -> 'a1 **)
    171 let rec fixed_rect_Type2 h_mk_fixed x_15531 =
     171let rec fixed_rect_Type2 h_mk_fixed x_213 =
    172172  let { fx_gotos = fx_gotos0; fx_env = fx_env0; fx_rettyp = fx_rettyp0 } =
    173     x_15531
     173    x_213
    174174  in
    175175  h_mk_fixed fx_gotos0 fx_env0 fx_rettyp0
     
    178178    (Identifiers.identifier_set -> env -> AST.typ Types.option -> 'a1) ->
    179179    fixed -> 'a1 **)
    180 let rec fixed_rect_Type1 h_mk_fixed x_15533 =
     180let rec fixed_rect_Type1 h_mk_fixed x_215 =
    181181  let { fx_gotos = fx_gotos0; fx_env = fx_env0; fx_rettyp = fx_rettyp0 } =
    182     x_15533
     182    x_215
    183183  in
    184184  h_mk_fixed fx_gotos0 fx_env0 fx_rettyp0
     
    187187    (Identifiers.identifier_set -> env -> AST.typ Types.option -> 'a1) ->
    188188    fixed -> 'a1 **)
    189 let rec fixed_rect_Type0 h_mk_fixed x_15535 =
     189let rec fixed_rect_Type0 h_mk_fixed x_217 =
    190190  let { fx_gotos = fx_gotos0; fx_env = fx_env0; fx_rettyp = fx_rettyp0 } =
    191     x_15535
     191    x_217
    192192  in
    193193  h_mk_fixed fx_gotos0 fx_env0 fx_rettyp0
     
    257257    (PreIdentifiers.identifier Identifiers.identifier_map -> __ -> __ -> 'a1)
    258258    -> goto_map -> 'a1 **)
    259 let rec goto_map_rect_Type4 fx g h_mk_goto_map x_15551 =
    260   let gm_map = x_15551 in h_mk_goto_map gm_map __ __
     259let rec goto_map_rect_Type4 fx g h_mk_goto_map x_233 =
     260  let gm_map = x_233 in h_mk_goto_map gm_map __ __
    261261
    262262(** val goto_map_rect_Type5 :
     
    264264    (PreIdentifiers.identifier Identifiers.identifier_map -> __ -> __ -> 'a1)
    265265    -> goto_map -> 'a1 **)
    266 let rec goto_map_rect_Type5 fx g h_mk_goto_map x_15553 =
    267   let gm_map = x_15553 in h_mk_goto_map gm_map __ __
     266let rec goto_map_rect_Type5 fx g h_mk_goto_map x_235 =
     267  let gm_map = x_235 in h_mk_goto_map gm_map __ __
    268268
    269269(** val goto_map_rect_Type3 :
     
    271271    (PreIdentifiers.identifier Identifiers.identifier_map -> __ -> __ -> 'a1)
    272272    -> goto_map -> 'a1 **)
    273 let rec goto_map_rect_Type3 fx g h_mk_goto_map x_15555 =
    274   let gm_map = x_15555 in h_mk_goto_map gm_map __ __
     273let rec goto_map_rect_Type3 fx g h_mk_goto_map x_237 =
     274  let gm_map = x_237 in h_mk_goto_map gm_map __ __
    275275
    276276(** val goto_map_rect_Type2 :
     
    278278    (PreIdentifiers.identifier Identifiers.identifier_map -> __ -> __ -> 'a1)
    279279    -> goto_map -> 'a1 **)
    280 let rec goto_map_rect_Type2 fx g h_mk_goto_map x_15557 =
    281   let gm_map = x_15557 in h_mk_goto_map gm_map __ __
     280let rec goto_map_rect_Type2 fx g h_mk_goto_map x_239 =
     281  let gm_map = x_239 in h_mk_goto_map gm_map __ __
    282282
    283283(** val goto_map_rect_Type1 :
     
    285285    (PreIdentifiers.identifier Identifiers.identifier_map -> __ -> __ -> 'a1)
    286286    -> goto_map -> 'a1 **)
    287 let rec goto_map_rect_Type1 fx g h_mk_goto_map x_15559 =
    288   let gm_map = x_15559 in h_mk_goto_map gm_map __ __
     287let rec goto_map_rect_Type1 fx g h_mk_goto_map x_241 =
     288  let gm_map = x_241 in h_mk_goto_map gm_map __ __
    289289
    290290(** val goto_map_rect_Type0 :
     
    292292    (PreIdentifiers.identifier Identifiers.identifier_map -> __ -> __ -> 'a1)
    293293    -> goto_map -> 'a1 **)
    294 let rec goto_map_rect_Type0 fx g h_mk_goto_map x_15561 =
    295   let gm_map = x_15561 in h_mk_goto_map gm_map __ __
     294let rec goto_map_rect_Type0 fx g h_mk_goto_map x_243 =
     295  let gm_map = x_243 in h_mk_goto_map gm_map __ __
    296296
    297297(** val gm_map :
     
    401401    Graphs.label Types.sig0 -> Graphs.label Types.sig0 -> 'a1) -> partial_fn
    402402    -> 'a1 **)
    403 let rec partial_fn_rect_Type4 fx h_mk_partial_fn x_15579 =
     403let rec partial_fn_rect_Type4 fx h_mk_partial_fn x_261 =
    404404  let { pf_labgen = pf_labgen0; pf_reggen = pf_reggen0; pf_params =
    405405    pf_params0; pf_locals = pf_locals0; pf_result = pf_result0;
    406406    pf_stacksize = pf_stacksize0; pf_graph = pf_graph0; pf_gotos = pf_gotos0;
    407407    pf_labels = pf_labels0; pf_entry = pf_entry0; pf_exit = pf_exit0 } =
    408     x_15579
     408    x_261
    409409  in
    410410  h_mk_partial_fn pf_labgen0 pf_reggen0 pf_params0 pf_locals0 pf_result0 __
     
    419419    Graphs.label Types.sig0 -> Graphs.label Types.sig0 -> 'a1) -> partial_fn
    420420    -> 'a1 **)
    421 let rec partial_fn_rect_Type5 fx h_mk_partial_fn x_15581 =
     421let rec partial_fn_rect_Type5 fx h_mk_partial_fn x_263 =
    422422  let { pf_labgen = pf_labgen0; pf_reggen = pf_reggen0; pf_params =
    423423    pf_params0; pf_locals = pf_locals0; pf_result = pf_result0;
    424424    pf_stacksize = pf_stacksize0; pf_graph = pf_graph0; pf_gotos = pf_gotos0;
    425425    pf_labels = pf_labels0; pf_entry = pf_entry0; pf_exit = pf_exit0 } =
    426     x_15581
     426    x_263
    427427  in
    428428  h_mk_partial_fn pf_labgen0 pf_reggen0 pf_params0 pf_locals0 pf_result0 __
     
    437437    Graphs.label Types.sig0 -> Graphs.label Types.sig0 -> 'a1) -> partial_fn
    438438    -> 'a1 **)
    439 let rec partial_fn_rect_Type3 fx h_mk_partial_fn x_15583 =
     439let rec partial_fn_rect_Type3 fx h_mk_partial_fn x_265 =
    440440  let { pf_labgen = pf_labgen0; pf_reggen = pf_reggen0; pf_params =
    441441    pf_params0; pf_locals = pf_locals0; pf_result = pf_result0;
    442442    pf_stacksize = pf_stacksize0; pf_graph = pf_graph0; pf_gotos = pf_gotos0;
    443443    pf_labels = pf_labels0; pf_entry = pf_entry0; pf_exit = pf_exit0 } =
    444     x_15583
     444    x_265
    445445  in
    446446  h_mk_partial_fn pf_labgen0 pf_reggen0 pf_params0 pf_locals0 pf_result0 __
     
    455455    Graphs.label Types.sig0 -> Graphs.label Types.sig0 -> 'a1) -> partial_fn
    456456    -> 'a1 **)
    457 let rec partial_fn_rect_Type2 fx h_mk_partial_fn x_15585 =
     457let rec partial_fn_rect_Type2 fx h_mk_partial_fn x_267 =
    458458  let { pf_labgen = pf_labgen0; pf_reggen = pf_reggen0; pf_params =
    459459    pf_params0; pf_locals = pf_locals0; pf_result = pf_result0;
    460460    pf_stacksize = pf_stacksize0; pf_graph = pf_graph0; pf_gotos = pf_gotos0;
    461461    pf_labels = pf_labels0; pf_entry = pf_entry0; pf_exit = pf_exit0 } =
    462     x_15585
     462    x_267
    463463  in
    464464  h_mk_partial_fn pf_labgen0 pf_reggen0 pf_params0 pf_locals0 pf_result0 __
     
    473473    Graphs.label Types.sig0 -> Graphs.label Types.sig0 -> 'a1) -> partial_fn
    474474    -> 'a1 **)
    475 let rec partial_fn_rect_Type1 fx h_mk_partial_fn x_15587 =
     475let rec partial_fn_rect_Type1 fx h_mk_partial_fn x_269 =
    476476  let { pf_labgen = pf_labgen0; pf_reggen = pf_reggen0; pf_params =
    477477    pf_params0; pf_locals = pf_locals0; pf_result = pf_result0;
    478478    pf_stacksize = pf_stacksize0; pf_graph = pf_graph0; pf_gotos = pf_gotos0;
    479479    pf_labels = pf_labels0; pf_entry = pf_entry0; pf_exit = pf_exit0 } =
    480     x_15587
     480    x_269
    481481  in
    482482  h_mk_partial_fn pf_labgen0 pf_reggen0 pf_params0 pf_locals0 pf_result0 __
     
    491491    Graphs.label Types.sig0 -> Graphs.label Types.sig0 -> 'a1) -> partial_fn
    492492    -> 'a1 **)
    493 let rec partial_fn_rect_Type0 fx h_mk_partial_fn x_15589 =
     493let rec partial_fn_rect_Type0 fx h_mk_partial_fn x_271 =
    494494  let { pf_labgen = pf_labgen0; pf_reggen = pf_reggen0; pf_params =
    495495    pf_params0; pf_locals = pf_locals0; pf_result = pf_result0;
    496496    pf_stacksize = pf_stacksize0; pf_graph = pf_graph0; pf_gotos = pf_gotos0;
    497497    pf_labels = pf_labels0; pf_entry = pf_entry0; pf_exit = pf_exit0 } =
    498     x_15589
     498    x_271
    499499  in
    500500  h_mk_partial_fn pf_labgen0 pf_reggen0 pf_params0 pf_locals0 pf_result0 __
     
    874874    Cminor_syntax.stmt -> partial_fn Types.sig0 -> 'a1) -> partial_fn ->
    875875    fn_con_because -> 'a1 **)
    876 let rec fn_con_because_rect_Type4 fx h_fn_con_eq h_fn_con_sig h_fn_con_addinv x_15665 = function
     876let rec fn_con_because_rect_Type4 fx h_fn_con_eq h_fn_con_sig h_fn_con_addinv x_347 = function
    877877| Fn_con_eq f -> h_fn_con_eq f
    878878| Fn_con_sig (f1, f2, f3) -> h_fn_con_sig f1 f2 __ f3
     
    884884    Cminor_syntax.stmt -> partial_fn Types.sig0 -> 'a1) -> partial_fn ->
    885885    fn_con_because -> 'a1 **)
    886 let rec fn_con_because_rect_Type5 fx h_fn_con_eq h_fn_con_sig h_fn_con_addinv x_15672 = function
     886let rec fn_con_because_rect_Type5 fx h_fn_con_eq h_fn_con_sig h_fn_con_addinv x_354 = function
    887887| Fn_con_eq f -> h_fn_con_eq f
    888888| Fn_con_sig (f1, f2, f3) -> h_fn_con_sig f1 f2 __ f3
     
    894894    Cminor_syntax.stmt -> partial_fn Types.sig0 -> 'a1) -> partial_fn ->
    895895    fn_con_because -> 'a1 **)
    896 let rec fn_con_because_rect_Type3 fx h_fn_con_eq h_fn_con_sig h_fn_con_addinv x_15679 = function
     896let rec fn_con_because_rect_Type3 fx h_fn_con_eq h_fn_con_sig h_fn_con_addinv x_361 = function
    897897| Fn_con_eq f -> h_fn_con_eq f
    898898| Fn_con_sig (f1, f2, f3) -> h_fn_con_sig f1 f2 __ f3
     
    904904    Cminor_syntax.stmt -> partial_fn Types.sig0 -> 'a1) -> partial_fn ->
    905905    fn_con_because -> 'a1 **)
    906 let rec fn_con_because_rect_Type2 fx h_fn_con_eq h_fn_con_sig h_fn_con_addinv x_15686 = function
     906let rec fn_con_because_rect_Type2 fx h_fn_con_eq h_fn_con_sig h_fn_con_addinv x_368 = function
    907907| Fn_con_eq f -> h_fn_con_eq f
    908908| Fn_con_sig (f1, f2, f3) -> h_fn_con_sig f1 f2 __ f3
     
    914914    Cminor_syntax.stmt -> partial_fn Types.sig0 -> 'a1) -> partial_fn ->
    915915    fn_con_because -> 'a1 **)
    916 let rec fn_con_because_rect_Type1 fx h_fn_con_eq h_fn_con_sig h_fn_con_addinv x_15693 = function
     916let rec fn_con_because_rect_Type1 fx h_fn_con_eq h_fn_con_sig h_fn_con_addinv x_375 = function
    917917| Fn_con_eq f -> h_fn_con_eq f
    918918| Fn_con_sig (f1, f2, f3) -> h_fn_con_sig f1 f2 __ f3
     
    924924    Cminor_syntax.stmt -> partial_fn Types.sig0 -> 'a1) -> partial_fn ->
    925925    fn_con_because -> 'a1 **)
    926 let rec fn_con_because_rect_Type0 fx h_fn_con_eq h_fn_con_sig h_fn_con_addinv x_15700 = function
     926let rec fn_con_because_rect_Type0 fx h_fn_con_eq h_fn_con_sig h_fn_con_addinv x_382 = function
    927927| Fn_con_eq f -> h_fn_con_eq f
    928928| Fn_con_sig (f1, f2, f3) -> h_fn_con_sig f1 f2 __ f3
     
    12001200let add_return fx opt_e f =
    12011201  let f0 = f in
    1202   let f1 = add_fresh_to_graph fx (fun x -> RTLabs_syntax.St_return) f in
     1202  let f1 = change_entry fx f (Types.pi1 f.pf_exit) in
    12031203  (match opt_e with
    12041204   | Types.None -> (fun _ -> Types.pi1 f1)
     
    13391339  let reggen0 = Identifiers.new_universe PreIdentifiers.RegisterTag in
    13401340  let cminor_labels = Cminor_syntax.labels_of f.Cminor_syntax.f_body in
    1341   (let { Types.fst = eta3141; Types.snd = reggen1 } =
     1341  (let { Types.fst = eta393; Types.snd = reggen1 } =
    13421342     populate_env (Identifiers.empty_map PreIdentifiers.SymbolTag) reggen0
    13431343       f.Cminor_syntax.f_params
    13441344   in
    1345   let { Types.fst = params; Types.snd = env1 } = eta3141 in
     1345  let { Types.fst = params; Types.snd = env1 } = eta393 in
    13461346  (fun _ ->
    1347   (let { Types.fst = eta3140; Types.snd = reggen2 } =
     1347  (let { Types.fst = eta392; Types.snd = reggen2 } =
    13481348     populate_env env1 reggen1 f.Cminor_syntax.f_vars
    13491349   in
    1350   let { Types.fst = locals0; Types.snd = env0 } = eta3140 in
     1350  let { Types.fst = locals0; Types.snd = env0 } = eta392 in
    13511351  (fun _ ->
    13521352  (let { Types.dpi1 = locals_reggen; Types.dpi2 = result } =
  • extracted/translateUtils.ml

    r2951 r2974  
    217217  Joint.add_graph g_pars globals mid (Joint.Final last) def0
    218218
    219 (** val append_seq_list :
    220     Joint.params -> AST.ident List.list -> Blocks.bind_step_block ->
    221     (Registers.register, Joint.joint_seq List.list) Bind_new.bind_new ->
    222     Blocks.bind_step_block **)
    223 let append_seq_list p g bbl bl =
    224   Obj.magic
    225     (Monad.m_bind3 (Monad.max_def Bind_new.bindNew) (Obj.magic bbl)
    226       (fun pref op post ->
    227       Monad.m_bind0 (Monad.max_def Bind_new.bindNew) (Obj.magic bl) (fun l ->
    228         Monad.m_return0 (Monad.max_def Bind_new.bindNew) { Types.fst =
    229           { Types.fst = pref; Types.snd = op }; Types.snd =
    230           (List.append post l) })))
    231 
    232219(** val b_adds_graph :
    233220    Joint.graph_params -> AST.ident List.list -> Blocks.bind_step_block ->
     
    282269    -> (Graphs.label -> Joint.joint_fin_step -> Blocks.bind_fin_block) -> __
    283270    -> __ -> __ -> __ -> 'a1) -> b_graph_translate_data -> 'a1 **)
    284 let rec b_graph_translate_data_rect_Type4 src dst globals h_mk_b_graph_translate_data x_18305 =
     271let rec b_graph_translate_data_rect_Type4 src dst globals h_mk_b_graph_translate_data x_3 =
    285272  let { init_ret = init_ret0; init_params = init_params0; init_stack_size =
    286273    init_stack_size0; added_prologue = added_prologue0; new_regs = new_regs0;
    287     f_step = f_step0; f_fin = f_fin0 } = x_18305
     274    f_step = f_step0; f_fin = f_fin0 } = x_3
    288275  in
    289276  h_mk_b_graph_translate_data init_ret0 init_params0 init_stack_size0
     
    296283    -> (Graphs.label -> Joint.joint_fin_step -> Blocks.bind_fin_block) -> __
    297284    -> __ -> __ -> __ -> 'a1) -> b_graph_translate_data -> 'a1 **)
    298 let rec b_graph_translate_data_rect_Type5 src dst globals h_mk_b_graph_translate_data x_18307 =
     285let rec b_graph_translate_data_rect_Type5 src dst globals h_mk_b_graph_translate_data x_5 =
    299286  let { init_ret = init_ret0; init_params = init_params0; init_stack_size =
    300287    init_stack_size0; added_prologue = added_prologue0; new_regs = new_regs0;
    301     f_step = f_step0; f_fin = f_fin0 } = x_18307
     288    f_step = f_step0; f_fin = f_fin0 } = x_5
    302289  in
    303290  h_mk_b_graph_translate_data init_ret0 init_params0 init_stack_size0
     
    310297    -> (Graphs.label -> Joint.joint_fin_step -> Blocks.bind_fin_block) -> __
    311298    -> __ -> __ -> __ -> 'a1) -> b_graph_translate_data -> 'a1 **)
    312 let rec b_graph_translate_data_rect_Type3 src dst globals h_mk_b_graph_translate_data x_18309 =
     299let rec b_graph_translate_data_rect_Type3 src dst globals h_mk_b_graph_translate_data x_7 =
    313300  let { init_ret = init_ret0; init_params = init_params0; init_stack_size =
    314301    init_stack_size0; added_prologue = added_prologue0; new_regs = new_regs0;
    315     f_step = f_step0; f_fin = f_fin0 } = x_18309
     302    f_step = f_step0; f_fin = f_fin0 } = x_7
    316303  in
    317304  h_mk_b_graph_translate_data init_ret0 init_params0 init_stack_size0
     
    324311    -> (Graphs.label -> Joint.joint_fin_step -> Blocks.bind_fin_block) -> __
    325312    -> __ -> __ -> __ -> 'a1) -> b_graph_translate_data -> 'a1 **)
    326 let rec b_graph_translate_data_rect_Type2 src dst globals h_mk_b_graph_translate_data x_18311 =
     313let rec b_graph_translate_data_rect_Type2 src dst globals h_mk_b_graph_translate_data x_9 =
    327314  let { init_ret = init_ret0; init_params = init_params0; init_stack_size =
    328315    init_stack_size0; added_prologue = added_prologue0; new_regs = new_regs0;
    329     f_step = f_step0; f_fin = f_fin0 } = x_18311
     316    f_step = f_step0; f_fin = f_fin0 } = x_9
    330317  in
    331318  h_mk_b_graph_translate_data init_ret0 init_params0 init_stack_size0
     
    338325    -> (Graphs.label -> Joint.joint_fin_step -> Blocks.bind_fin_block) -> __
    339326    -> __ -> __ -> __ -> 'a1) -> b_graph_translate_data -> 'a1 **)
    340 let rec b_graph_translate_data_rect_Type1 src dst globals h_mk_b_graph_translate_data x_18313 =
     327let rec b_graph_translate_data_rect_Type1 src dst globals h_mk_b_graph_translate_data x_11 =
    341328  let { init_ret = init_ret0; init_params = init_params0; init_stack_size =
    342329    init_stack_size0; added_prologue = added_prologue0; new_regs = new_regs0;
    343     f_step = f_step0; f_fin = f_fin0 } = x_18313
     330    f_step = f_step0; f_fin = f_fin0 } = x_11
    344331  in
    345332  h_mk_b_graph_translate_data init_ret0 init_params0 init_stack_size0
     
    352339    -> (Graphs.label -> Joint.joint_fin_step -> Blocks.bind_fin_block) -> __
    353340    -> __ -> __ -> __ -> 'a1) -> b_graph_translate_data -> 'a1 **)
    354 let rec b_graph_translate_data_rect_Type0 src dst globals h_mk_b_graph_translate_data x_18315 =
     341let rec b_graph_translate_data_rect_Type0 src dst globals h_mk_b_graph_translate_data x_13 =
    355342  let { init_ret = init_ret0; init_params = init_params0; init_stack_size =
    356343    init_stack_size0; added_prologue = added_prologue0; new_regs = new_regs0;
    357     f_step = f_step0; f_fin = f_fin0 } = x_18315
     344    f_step = f_step0; f_fin = f_fin0 } = x_13
    358345  in
    359346  h_mk_b_graph_translate_data init_ret0 init_params0 init_stack_size0
     
    469456(** val get_first_costlabel :
    470457    Joint.params -> AST.ident List.list ->
    471     Joint.joint_closed_internal_function -> (CostLabel.costlabel, __)
    472     Types.prod **)
     458    Joint.joint_closed_internal_function -> CostLabel.costlabel **)
    473459let get_first_costlabel p g def =
    474460  (match p.Joint.stmt_at g (Types.pi1 def).Joint.joint_if_code
     
    479465      | Joint.Sequential (s', nxt) ->
    480466        (match s' with
    481          | Joint.COST_LABEL c ->
    482            (fun _ -> { Types.fst = c; Types.snd = nxt })
     467         | Joint.COST_LABEL c -> (fun _ -> c)
    483468         | Joint.CALL (x, x0, x1) ->
    484469           (fun _ -> assert false (* absurd case *))
     
    489474    __
    490475
     476(** val not_emptyb : 'a1 List.list -> Bool.bool **)
     477let not_emptyb = function
     478| List.Nil -> Bool.False
     479| List.Cons (x, x0) -> Bool.True
     480
    491481(** val b_graph_translate_props_rect_Type4 :
    492482    Joint.graph_params -> Joint.graph_params -> AST.ident List.list ->
     
    610600let pair_swap pr =
    611601  { Types.fst = pr.Types.snd; Types.snd = pr.Types.fst }
     602
     603(** val set_entry :
     604    AST.ident List.list -> Joint.params -> Joint.joint_internal_function ->
     605    __ -> Joint.joint_internal_function **)
     606let set_entry globals pars int_fun entry =
     607  { Joint.joint_if_luniverse = int_fun.Joint.joint_if_luniverse;
     608    Joint.joint_if_runiverse = int_fun.Joint.joint_if_runiverse;
     609    Joint.joint_if_result = int_fun.Joint.joint_if_result;
     610    Joint.joint_if_params = int_fun.Joint.joint_if_params;
     611    Joint.joint_if_stacksize = int_fun.Joint.joint_if_stacksize;
     612    Joint.joint_if_local_stacksize = int_fun.Joint.joint_if_local_stacksize;
     613    Joint.joint_if_code = int_fun.Joint.joint_if_code; Joint.joint_if_entry =
     614    entry }
    612615
    613616(** val b_graph_translate :
     
    632635    Joint.joint_if_local_stacksize =
    633636    (Types.pi1 def).Joint.joint_if_local_stacksize; Joint.joint_if_code =
    634     (Obj.magic
    635       (Identifiers.add PreIdentifiers.LabelTag
    636         (Identifiers.empty_map PreIdentifiers.LabelTag) (Obj.magic entry)
    637         (Joint.Final Joint.RETURN))); Joint.joint_if_entry = entry }
     637    (Obj.magic (Identifiers.empty_map PreIdentifiers.LabelTag));
     638    Joint.joint_if_entry = entry }
     639  in
     640  let prologue = data0.added_prologue in
     641  let { Types.fst = init0; Types.snd = entry' } =
     642    Obj.magic adds_graph_pre dst_g_pars globals (fun x i -> i) prologue
     643      (Obj.magic entry) init
     644  in
     645  let f_step0 =
     646    match not_emptyb prologue with
     647    | Bool.True ->
     648      (fun lbl ->
     649        match Identifiers.eq_identifier PreIdentifiers.LabelTag lbl
     650                (Obj.magic entry) with
     651        | Bool.True ->
     652          (fun x -> Bind_new.Bret
     653            (Blocks.ensure_step_block
     654              (Joint.graph_params_to_params dst_g_pars) globals List.Nil))
     655        | Bool.False -> data0.f_step lbl)
     656    | Bool.False -> data0.f_step
    638657  in
    639658  let f = fun lbl stmt def0 ->
    640659    match stmt with
    641660    | Joint.Sequential (inst, next) ->
    642       b_adds_graph dst_g_pars globals (data0.f_step lbl inst) lbl
    643         (Obj.magic next) def0
     661      b_adds_graph dst_g_pars globals (f_step0 lbl inst) lbl (Obj.magic next)
     662        def0
    644663    | Joint.Final inst ->
    645664      b_fin_adds_graph dst_g_pars globals (data0.f_fin lbl inst) lbl def0
     
    648667  let def_out =
    649668    Identifiers.foldi PreIdentifiers.LabelTag f
    650       (Obj.magic (Types.pi1 def).Joint.joint_if_code) init
    651   in
    652   let init_c_nxt =
    653     get_first_costlabel (Joint.graph_params_to_params src_g_pars) globals def
    654   in
    655   let def_out_nxt =
    656     Obj.magic adds_graph_post dst_g_pars globals data0.added_prologue
    657       (Obj.magic init_c_nxt).Types.snd def_out
    658   in
    659   Joint.add_graph dst_g_pars globals (Obj.magic entry) (Joint.Sequential
    660     ((Joint.COST_LABEL init_c_nxt.Types.fst), def_out_nxt.Types.snd))
    661     def_out_nxt.Types.fst
     669      (Obj.magic (Types.pi1 def).Joint.joint_if_code) init0
     670  in
     671  let def_out0 =
     672    match not_emptyb prologue with
     673    | Bool.True ->
     674      let init_c =
     675        get_first_costlabel (Joint.graph_params_to_params src_g_pars) globals
     676          def
     677      in
     678      let { Types.fst = def_out0; Types.snd = entry'' } =
     679        Obj.magic fresh_label (Joint.graph_params_to_params dst_g_pars)
     680          globals def_out
     681      in
     682      let def_out1 =
     683        Joint.add_graph dst_g_pars globals entry'' (Joint.Sequential
     684          ((Joint.COST_LABEL init_c), entry')) def_out0
     685      in
     686      set_entry globals (Joint.graph_params_to_params dst_g_pars) def_out1
     687        (Obj.magic entry'')
     688    | Bool.False -> def_out
     689  in
     690  def_out0
    662691
    663692(** val b_graph_transform_program :
  • extracted/translateUtils.mli

    r2951 r2974  
    155155  Graphs.label -> Joint.joint_internal_function ->
    156156  Joint.joint_internal_function
    157 
    158 val append_seq_list :
    159   Joint.params -> AST.ident List.list -> Blocks.bind_step_block ->
    160   (Registers.register, Joint.joint_seq List.list) Bind_new.bind_new ->
    161   Blocks.bind_step_block
    162157
    163158val b_adds_graph :
     
    303298val get_first_costlabel :
    304299  Joint.params -> AST.ident List.list -> Joint.joint_closed_internal_function
    305   -> (CostLabel.costlabel, __) Types.prod
     300  -> CostLabel.costlabel
     301
     302val not_emptyb : 'a1 List.list -> Bool.bool
    306303
    307304val b_graph_translate_props_rect_Type4 :
     
    389386
    390387val pair_swap : ('a1, 'a2) Types.prod -> ('a2, 'a1) Types.prod
     388
     389val set_entry :
     390  AST.ident List.list -> Joint.params -> Joint.joint_internal_function -> __
     391  -> Joint.joint_internal_function
    391392
    392393val b_graph_translate :
Note: See TracChangeset for help on using the changeset viewer.