Changeset 2997 for extracted/toRTLabs.ml


Ignore:
Timestamp:
Mar 28, 2013, 10:27:41 AM (7 years ago)
Author:
sacerdot
Message:

New extraction.

File:
1 edited

Legend:

Unmodified
Added
Removed
  • extracted/toRTLabs.ml

    r2974 r2997  
    121121  List.foldr (fun idt rsengen ->
    122122    let { Types.fst = id; Types.snd = ty } = idt in
    123     let { Types.fst = eta166; Types.snd = gen0 } = rsengen in
    124     let { Types.fst = rs; Types.snd = en0 } = eta166 in
     123    let { Types.fst = eta651; Types.snd = gen0 } = rsengen in
     124    let { Types.fst = rs; Types.snd = en0 } = eta651 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_207 =
     144let rec fixed_rect_Type4 h_mk_fixed x_1096 =
    145145  let { fx_gotos = fx_gotos0; fx_env = fx_env0; fx_rettyp = fx_rettyp0 } =
    146     x_207
     146    x_1096
    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_209 =
     153let rec fixed_rect_Type5 h_mk_fixed x_1098 =
    154154  let { fx_gotos = fx_gotos0; fx_env = fx_env0; fx_rettyp = fx_rettyp0 } =
    155     x_209
     155    x_1098
    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_211 =
     162let rec fixed_rect_Type3 h_mk_fixed x_1100 =
    163163  let { fx_gotos = fx_gotos0; fx_env = fx_env0; fx_rettyp = fx_rettyp0 } =
    164     x_211
     164    x_1100
    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_213 =
     171let rec fixed_rect_Type2 h_mk_fixed x_1102 =
    172172  let { fx_gotos = fx_gotos0; fx_env = fx_env0; fx_rettyp = fx_rettyp0 } =
    173     x_213
     173    x_1102
    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_215 =
     180let rec fixed_rect_Type1 h_mk_fixed x_1104 =
    181181  let { fx_gotos = fx_gotos0; fx_env = fx_env0; fx_rettyp = fx_rettyp0 } =
    182     x_215
     182    x_1104
    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_217 =
     189let rec fixed_rect_Type0 h_mk_fixed x_1106 =
    190190  let { fx_gotos = fx_gotos0; fx_env = fx_env0; fx_rettyp = fx_rettyp0 } =
    191     x_217
     191    x_1106
    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_233 =
    260   let gm_map = x_233 in h_mk_goto_map gm_map __ __
     259let rec goto_map_rect_Type4 fx g h_mk_goto_map x_1122 =
     260  let gm_map = x_1122 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_235 =
    267   let gm_map = x_235 in h_mk_goto_map gm_map __ __
     266let rec goto_map_rect_Type5 fx g h_mk_goto_map x_1124 =
     267  let gm_map = x_1124 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_237 =
    274   let gm_map = x_237 in h_mk_goto_map gm_map __ __
     273let rec goto_map_rect_Type3 fx g h_mk_goto_map x_1126 =
     274  let gm_map = x_1126 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_239 =
    281   let gm_map = x_239 in h_mk_goto_map gm_map __ __
     280let rec goto_map_rect_Type2 fx g h_mk_goto_map x_1128 =
     281  let gm_map = x_1128 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_241 =
    288   let gm_map = x_241 in h_mk_goto_map gm_map __ __
     287let rec goto_map_rect_Type1 fx g h_mk_goto_map x_1130 =
     288  let gm_map = x_1130 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_243 =
    295   let gm_map = x_243 in h_mk_goto_map gm_map __ __
     294let rec goto_map_rect_Type0 fx g h_mk_goto_map x_1132 =
     295  let gm_map = x_1132 in h_mk_goto_map gm_map __ __
    296296
    297297(** val gm_map :
     
    399399    Nat.nat -> RTLabs_syntax.statement Graphs.graph -> __ -> goto_map ->
    400400    PreIdentifiers.identifier Identifiers.identifier_map Types.sig0 -> __ ->
    401     Graphs.label Types.sig0 -> Graphs.label Types.sig0 -> 'a1) -> partial_fn
    402     -> 'a1 **)
    403 let rec partial_fn_rect_Type4 fx h_mk_partial_fn x_261 =
     401    Graphs.label Types.sig0 -> Graphs.label Types.sig0 -> __ -> 'a1) ->
     402    partial_fn -> 'a1 **)
     403let rec partial_fn_rect_Type4 fx h_mk_partial_fn x_1150 =
    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_261
     408    x_1150
    409409  in
    410410  h_mk_partial_fn pf_labgen0 pf_reggen0 pf_params0 pf_locals0 pf_result0 __
    411     pf_stacksize0 pf_graph0 __ pf_gotos0 pf_labels0 __ pf_entry0 pf_exit0
     411    pf_stacksize0 pf_graph0 __ pf_gotos0 pf_labels0 __ pf_entry0 pf_exit0 __
    412412
    413413(** val partial_fn_rect_Type5 :
     
    417417    Nat.nat -> RTLabs_syntax.statement Graphs.graph -> __ -> goto_map ->
    418418    PreIdentifiers.identifier Identifiers.identifier_map Types.sig0 -> __ ->
    419     Graphs.label Types.sig0 -> Graphs.label Types.sig0 -> 'a1) -> partial_fn
    420     -> 'a1 **)
    421 let rec partial_fn_rect_Type5 fx h_mk_partial_fn x_263 =
     419    Graphs.label Types.sig0 -> Graphs.label Types.sig0 -> __ -> 'a1) ->
     420    partial_fn -> 'a1 **)
     421let rec partial_fn_rect_Type5 fx h_mk_partial_fn x_1152 =
    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_263
     426    x_1152
    427427  in
    428428  h_mk_partial_fn pf_labgen0 pf_reggen0 pf_params0 pf_locals0 pf_result0 __
    429     pf_stacksize0 pf_graph0 __ pf_gotos0 pf_labels0 __ pf_entry0 pf_exit0
     429    pf_stacksize0 pf_graph0 __ pf_gotos0 pf_labels0 __ pf_entry0 pf_exit0 __
    430430
    431431(** val partial_fn_rect_Type3 :
     
    435435    Nat.nat -> RTLabs_syntax.statement Graphs.graph -> __ -> goto_map ->
    436436    PreIdentifiers.identifier Identifiers.identifier_map Types.sig0 -> __ ->
    437     Graphs.label Types.sig0 -> Graphs.label Types.sig0 -> 'a1) -> partial_fn
    438     -> 'a1 **)
    439 let rec partial_fn_rect_Type3 fx h_mk_partial_fn x_265 =
     437    Graphs.label Types.sig0 -> Graphs.label Types.sig0 -> __ -> 'a1) ->
     438    partial_fn -> 'a1 **)
     439let rec partial_fn_rect_Type3 fx h_mk_partial_fn x_1154 =
    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_265
     444    x_1154
    445445  in
    446446  h_mk_partial_fn pf_labgen0 pf_reggen0 pf_params0 pf_locals0 pf_result0 __
    447     pf_stacksize0 pf_graph0 __ pf_gotos0 pf_labels0 __ pf_entry0 pf_exit0
     447    pf_stacksize0 pf_graph0 __ pf_gotos0 pf_labels0 __ pf_entry0 pf_exit0 __
    448448
    449449(** val partial_fn_rect_Type2 :
     
    453453    Nat.nat -> RTLabs_syntax.statement Graphs.graph -> __ -> goto_map ->
    454454    PreIdentifiers.identifier Identifiers.identifier_map Types.sig0 -> __ ->
    455     Graphs.label Types.sig0 -> Graphs.label Types.sig0 -> 'a1) -> partial_fn
    456     -> 'a1 **)
    457 let rec partial_fn_rect_Type2 fx h_mk_partial_fn x_267 =
     455    Graphs.label Types.sig0 -> Graphs.label Types.sig0 -> __ -> 'a1) ->
     456    partial_fn -> 'a1 **)
     457let rec partial_fn_rect_Type2 fx h_mk_partial_fn x_1156 =
    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_267
     462    x_1156
    463463  in
    464464  h_mk_partial_fn pf_labgen0 pf_reggen0 pf_params0 pf_locals0 pf_result0 __
    465     pf_stacksize0 pf_graph0 __ pf_gotos0 pf_labels0 __ pf_entry0 pf_exit0
     465    pf_stacksize0 pf_graph0 __ pf_gotos0 pf_labels0 __ pf_entry0 pf_exit0 __
    466466
    467467(** val partial_fn_rect_Type1 :
     
    471471    Nat.nat -> RTLabs_syntax.statement Graphs.graph -> __ -> goto_map ->
    472472    PreIdentifiers.identifier Identifiers.identifier_map Types.sig0 -> __ ->
    473     Graphs.label Types.sig0 -> Graphs.label Types.sig0 -> 'a1) -> partial_fn
    474     -> 'a1 **)
    475 let rec partial_fn_rect_Type1 fx h_mk_partial_fn x_269 =
     473    Graphs.label Types.sig0 -> Graphs.label Types.sig0 -> __ -> 'a1) ->
     474    partial_fn -> 'a1 **)
     475let rec partial_fn_rect_Type1 fx h_mk_partial_fn x_1158 =
    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_269
     480    x_1158
    481481  in
    482482  h_mk_partial_fn pf_labgen0 pf_reggen0 pf_params0 pf_locals0 pf_result0 __
    483     pf_stacksize0 pf_graph0 __ pf_gotos0 pf_labels0 __ pf_entry0 pf_exit0
     483    pf_stacksize0 pf_graph0 __ pf_gotos0 pf_labels0 __ pf_entry0 pf_exit0 __
    484484
    485485(** val partial_fn_rect_Type0 :
     
    489489    Nat.nat -> RTLabs_syntax.statement Graphs.graph -> __ -> goto_map ->
    490490    PreIdentifiers.identifier Identifiers.identifier_map Types.sig0 -> __ ->
    491     Graphs.label Types.sig0 -> Graphs.label Types.sig0 -> 'a1) -> partial_fn
    492     -> 'a1 **)
    493 let rec partial_fn_rect_Type0 fx h_mk_partial_fn x_271 =
     491    Graphs.label Types.sig0 -> Graphs.label Types.sig0 -> __ -> 'a1) ->
     492    partial_fn -> 'a1 **)
     493let rec partial_fn_rect_Type0 fx h_mk_partial_fn x_1160 =
    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_271
     498    x_1160
    499499  in
    500500  h_mk_partial_fn pf_labgen0 pf_reggen0 pf_params0 pf_locals0 pf_result0 __
    501     pf_stacksize0 pf_graph0 __ pf_gotos0 pf_labels0 __ pf_entry0 pf_exit0
     501    pf_stacksize0 pf_graph0 __ pf_gotos0 pf_labels0 __ pf_entry0 pf_exit0 __
    502502
    503503(** val pf_labgen : fixed -> partial_fn -> Identifiers.universe **)
     
    556556    Nat.nat -> RTLabs_syntax.statement Graphs.graph -> __ -> goto_map ->
    557557    PreIdentifiers.identifier Identifiers.identifier_map Types.sig0 -> __ ->
    558     Graphs.label Types.sig0 -> Graphs.label Types.sig0 -> __ -> 'a1) -> 'a1 **)
     558    Graphs.label Types.sig0 -> Graphs.label Types.sig0 -> __ -> __ -> 'a1) ->
     559    'a1 **)
    559560let partial_fn_inv_rect_Type4 x1 hterm h1 =
    560561  let hcut = partial_fn_rect_Type4 x1 h1 hterm in hcut __
     
    566567    Nat.nat -> RTLabs_syntax.statement Graphs.graph -> __ -> goto_map ->
    567568    PreIdentifiers.identifier Identifiers.identifier_map Types.sig0 -> __ ->
    568     Graphs.label Types.sig0 -> Graphs.label Types.sig0 -> __ -> 'a1) -> 'a1 **)
     569    Graphs.label Types.sig0 -> Graphs.label Types.sig0 -> __ -> __ -> 'a1) ->
     570    'a1 **)
    569571let partial_fn_inv_rect_Type3 x1 hterm h1 =
    570572  let hcut = partial_fn_rect_Type3 x1 h1 hterm in hcut __
     
    576578    Nat.nat -> RTLabs_syntax.statement Graphs.graph -> __ -> goto_map ->
    577579    PreIdentifiers.identifier Identifiers.identifier_map Types.sig0 -> __ ->
    578     Graphs.label Types.sig0 -> Graphs.label Types.sig0 -> __ -> 'a1) -> 'a1 **)
     580    Graphs.label Types.sig0 -> Graphs.label Types.sig0 -> __ -> __ -> 'a1) ->
     581    'a1 **)
    579582let partial_fn_inv_rect_Type2 x1 hterm h1 =
    580583  let hcut = partial_fn_rect_Type2 x1 h1 hterm in hcut __
     
    586589    Nat.nat -> RTLabs_syntax.statement Graphs.graph -> __ -> goto_map ->
    587590    PreIdentifiers.identifier Identifiers.identifier_map Types.sig0 -> __ ->
    588     Graphs.label Types.sig0 -> Graphs.label Types.sig0 -> __ -> 'a1) -> 'a1 **)
     591    Graphs.label Types.sig0 -> Graphs.label Types.sig0 -> __ -> __ -> 'a1) ->
     592    'a1 **)
    589593let partial_fn_inv_rect_Type1 x1 hterm h1 =
    590594  let hcut = partial_fn_rect_Type1 x1 h1 hterm in hcut __
     
    596600    Nat.nat -> RTLabs_syntax.statement Graphs.graph -> __ -> goto_map ->
    597601    PreIdentifiers.identifier Identifiers.identifier_map Types.sig0 -> __ ->
    598     Graphs.label Types.sig0 -> Graphs.label Types.sig0 -> __ -> 'a1) -> 'a1 **)
     602    Graphs.label Types.sig0 -> Graphs.label Types.sig0 -> __ -> __ -> 'a1) ->
     603    'a1 **)
    599604let partial_fn_inv_rect_Type0 x1 hterm h1 =
    600605  let hcut = partial_fn_rect_Type0 x1 h1 hterm in hcut __
     
    607612       pf_labels = a100; pf_entry = a12; pf_exit = a13 } = x
    608613     in
    609     Obj.magic (fun _ dH -> dH __ __ __ __ __ __ __ __ __ __ __ __ __ __)) y
     614    Obj.magic (fun _ dH -> dH __ __ __ __ __ __ __ __ __ __ __ __ __ __ __))
     615    y
    610616
    611617(** val fn_contains_rect_Type4 :
     
    874880    Cminor_syntax.stmt -> partial_fn Types.sig0 -> 'a1) -> partial_fn ->
    875881    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_347 = function
     882let rec fn_con_because_rect_Type4 fx h_fn_con_eq h_fn_con_sig h_fn_con_addinv x_1237 = function
    877883| Fn_con_eq f -> h_fn_con_eq f
    878884| Fn_con_sig (f1, f2, f3) -> h_fn_con_sig f1 f2 __ f3
     
    884890    Cminor_syntax.stmt -> partial_fn Types.sig0 -> 'a1) -> partial_fn ->
    885891    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_354 = function
     892let rec fn_con_because_rect_Type5 fx h_fn_con_eq h_fn_con_sig h_fn_con_addinv x_1244 = function
    887893| Fn_con_eq f -> h_fn_con_eq f
    888894| Fn_con_sig (f1, f2, f3) -> h_fn_con_sig f1 f2 __ f3
     
    894900    Cminor_syntax.stmt -> partial_fn Types.sig0 -> 'a1) -> partial_fn ->
    895901    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_361 = function
     902let rec fn_con_because_rect_Type3 fx h_fn_con_eq h_fn_con_sig h_fn_con_addinv x_1251 = function
    897903| Fn_con_eq f -> h_fn_con_eq f
    898904| Fn_con_sig (f1, f2, f3) -> h_fn_con_sig f1 f2 __ f3
     
    904910    Cminor_syntax.stmt -> partial_fn Types.sig0 -> 'a1) -> partial_fn ->
    905911    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_368 = function
     912let rec fn_con_because_rect_Type2 fx h_fn_con_eq h_fn_con_sig h_fn_con_addinv x_1258 = function
    907913| Fn_con_eq f -> h_fn_con_eq f
    908914| Fn_con_sig (f1, f2, f3) -> h_fn_con_sig f1 f2 __ f3
     
    914920    Cminor_syntax.stmt -> partial_fn Types.sig0 -> 'a1) -> partial_fn ->
    915921    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_375 = function
     922let rec fn_con_because_rect_Type1 fx h_fn_con_eq h_fn_con_sig h_fn_con_addinv x_1265 = function
    917923| Fn_con_eq f -> h_fn_con_eq f
    918924| Fn_con_sig (f1, f2, f3) -> h_fn_con_sig f1 f2 __ f3
     
    924930    Cminor_syntax.stmt -> partial_fn Types.sig0 -> 'a1) -> partial_fn ->
    925931    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_382 = function
     932let rec fn_con_because_rect_Type0 fx h_fn_con_eq h_fn_con_sig h_fn_con_addinv x_1272 = function
    927933| Fn_con_eq f -> h_fn_con_eq f
    928934| Fn_con_sig (f1, f2, f3) -> h_fn_con_sig f1 f2 __ f3
     
    12341240  pf_stacksize = f.pf_stacksize; pf_graph =
    12351241  (Identifiers.add PreIdentifiers.LabelTag f.pf_graph l
    1236     RTLabs_syntax.St_return); pf_gotos =
     1242    (RTLabs_syntax.St_skip l)); pf_gotos =
    12371243  (Identifiers.add PreIdentifiers.LabelTag (gm_map fx f.pf_graph f.pf_gotos)
    12381244    l dest); pf_labels = (Types.pi1 f.pf_labels); pf_entry = l; pf_exit =
     
    13391345  let reggen0 = Identifiers.new_universe PreIdentifiers.RegisterTag in
    13401346  let cminor_labels = Cminor_syntax.labels_of f.Cminor_syntax.f_body in
    1341   (let { Types.fst = eta393; Types.snd = reggen1 } =
     1347  (let { Types.fst = eta878; Types.snd = reggen1 } =
    13421348     populate_env (Identifiers.empty_map PreIdentifiers.SymbolTag) reggen0
    13431349       f.Cminor_syntax.f_params
    13441350   in
    1345   let { Types.fst = params; Types.snd = env1 } = eta393 in
     1351  let { Types.fst = params; Types.snd = env1 } = eta878 in
    13461352  (fun _ ->
    1347   (let { Types.fst = eta392; Types.snd = reggen2 } =
     1353  (let { Types.fst = eta877; Types.snd = reggen2 } =
    13481354     populate_env env1 reggen1 f.Cminor_syntax.f_vars
    13491355   in
    1350   let { Types.fst = locals0; Types.snd = env0 } = eta392 in
     1356  let { Types.fst = locals0; Types.snd = env0 } = eta877 in
    13511357  (fun _ ->
    13521358  (let { Types.dpi1 = locals_reggen; Types.dpi2 = result } =
Note: See TracChangeset for help on using the changeset viewer.