Changeset 2649 for extracted/toRTLabs.ml


Ignore:
Timestamp:
Feb 7, 2013, 10:43:49 PM (7 years ago)
Author:
sacerdot
Message:

...

File:
1 edited

Legend:

Unmodified
Added
Removed
  • extracted/toRTLabs.ml

    r2601 r2649  
    3737open Extra_bool
    3838
     39open Coqlib
     40
    3941open Values
    4042
     
    6769open Identifiers
    6870
    69 open Coqlib
    70 
    71 open Floats
    72 
    7371open Arithmetic
    7472
     
    8583open AST
    8684
     85open ErrorMessages
     86
    8787open Positive
    88 
    89 open Char
    90 
    91 open String
    9288
    9389open PreIdentifiers
     
    123119  List.foldr (fun idt rsengen ->
    124120    let { Types.fst = id; Types.snd = ty } = idt in
    125     let { Types.fst = eta2845; Types.snd = gen0 } = rsengen in
    126     let { Types.fst = rs; Types.snd = en0 } = eta2845 in
     121    let { Types.fst = eta1303; Types.snd = gen0 } = rsengen in
     122    let { Types.fst = rs; Types.snd = en0 } = eta1303 in
    127123    let { Types.fst = r; Types.snd = gen' } =
    128       Identifiers.fresh Registers.registerTag gen0
     124      Identifiers.fresh PreIdentifiers.RegisterTag gen0
    129125    in
    130126    { Types.fst = { Types.fst = (List.Cons ({ Types.fst = r; Types.snd =
    131127    ty }, rs)); Types.snd =
    132     (Identifiers.add AST.symbolTag en0 id { Types.fst = r; Types.snd = ty }) };
    133     Types.snd = gen' }) { Types.fst = { Types.fst = List.Nil; Types.snd =
    134     en }; Types.snd = gen }
     128    (Identifiers.add PreIdentifiers.SymbolTag en0 id { Types.fst = r;
     129      Types.snd = ty }) }; Types.snd = gen' }) { Types.fst = { Types.fst =
     130    List.Nil; Types.snd = en }; Types.snd = gen }
    135131
    136132(** val lookup_reg : env -> AST.ident -> AST.typ -> Registers.register **)
    137133let lookup_reg e0 id ty =
    138   (Identifiers.lookup_present AST.symbolTag e0 id).Types.fst
     134  (Identifiers.lookup_present PreIdentifiers.SymbolTag e0 id).Types.fst
    139135
    140136type fixed = { fx_gotos : Identifiers.identifier_set; fx_env : env;
     
    144140    (Identifiers.identifier_set -> env -> AST.typ Types.option -> 'a1) ->
    145141    fixed -> 'a1 **)
    146 let rec fixed_rect_Type4 h_mk_fixed x_14420 =
     142let rec fixed_rect_Type4 h_mk_fixed x_12027 =
    147143  let { fx_gotos = fx_gotos0; fx_env = fx_env0; fx_rettyp = fx_rettyp0 } =
    148     x_14420
     144    x_12027
    149145  in
    150146  h_mk_fixed fx_gotos0 fx_env0 fx_rettyp0
     
    153149    (Identifiers.identifier_set -> env -> AST.typ Types.option -> 'a1) ->
    154150    fixed -> 'a1 **)
    155 let rec fixed_rect_Type5 h_mk_fixed x_14422 =
     151let rec fixed_rect_Type5 h_mk_fixed x_12029 =
    156152  let { fx_gotos = fx_gotos0; fx_env = fx_env0; fx_rettyp = fx_rettyp0 } =
    157     x_14422
     153    x_12029
    158154  in
    159155  h_mk_fixed fx_gotos0 fx_env0 fx_rettyp0
     
    162158    (Identifiers.identifier_set -> env -> AST.typ Types.option -> 'a1) ->
    163159    fixed -> 'a1 **)
    164 let rec fixed_rect_Type3 h_mk_fixed x_14424 =
     160let rec fixed_rect_Type3 h_mk_fixed x_12031 =
    165161  let { fx_gotos = fx_gotos0; fx_env = fx_env0; fx_rettyp = fx_rettyp0 } =
    166     x_14424
     162    x_12031
    167163  in
    168164  h_mk_fixed fx_gotos0 fx_env0 fx_rettyp0
     
    171167    (Identifiers.identifier_set -> env -> AST.typ Types.option -> 'a1) ->
    172168    fixed -> 'a1 **)
    173 let rec fixed_rect_Type2 h_mk_fixed x_14426 =
     169let rec fixed_rect_Type2 h_mk_fixed x_12033 =
    174170  let { fx_gotos = fx_gotos0; fx_env = fx_env0; fx_rettyp = fx_rettyp0 } =
    175     x_14426
     171    x_12033
    176172  in
    177173  h_mk_fixed fx_gotos0 fx_env0 fx_rettyp0
     
    180176    (Identifiers.identifier_set -> env -> AST.typ Types.option -> 'a1) ->
    181177    fixed -> 'a1 **)
    182 let rec fixed_rect_Type1 h_mk_fixed x_14428 =
     178let rec fixed_rect_Type1 h_mk_fixed x_12035 =
    183179  let { fx_gotos = fx_gotos0; fx_env = fx_env0; fx_rettyp = fx_rettyp0 } =
    184     x_14428
     180    x_12035
    185181  in
    186182  h_mk_fixed fx_gotos0 fx_env0 fx_rettyp0
     
    189185    (Identifiers.identifier_set -> env -> AST.typ Types.option -> 'a1) ->
    190186    fixed -> 'a1 **)
    191 let rec fixed_rect_Type0 h_mk_fixed x_14430 =
     187let rec fixed_rect_Type0 h_mk_fixed x_12037 =
    192188  let { fx_gotos = fx_gotos0; fx_env = fx_env0; fx_rettyp = fx_rettyp0 } =
    193     x_14430
     189    x_12037
    194190  in
    195191  h_mk_fixed fx_gotos0 fx_env0 fx_rettyp0
     
    259255    (PreIdentifiers.identifier Identifiers.identifier_map -> __ -> __ -> 'a1)
    260256    -> goto_map -> 'a1 **)
    261 let rec goto_map_rect_Type4 fx g0 h_mk_goto_map x_14446 =
    262   let gm_map = x_14446 in h_mk_goto_map gm_map __ __
     257let rec goto_map_rect_Type4 fx g0 h_mk_goto_map x_12053 =
     258  let gm_map = x_12053 in h_mk_goto_map gm_map __ __
    263259
    264260(** val goto_map_rect_Type5 :
     
    266262    (PreIdentifiers.identifier Identifiers.identifier_map -> __ -> __ -> 'a1)
    267263    -> goto_map -> 'a1 **)
    268 let rec goto_map_rect_Type5 fx g0 h_mk_goto_map x_14448 =
    269   let gm_map = x_14448 in h_mk_goto_map gm_map __ __
     264let rec goto_map_rect_Type5 fx g0 h_mk_goto_map x_12055 =
     265  let gm_map = x_12055 in h_mk_goto_map gm_map __ __
    270266
    271267(** val goto_map_rect_Type3 :
     
    273269    (PreIdentifiers.identifier Identifiers.identifier_map -> __ -> __ -> 'a1)
    274270    -> goto_map -> 'a1 **)
    275 let rec goto_map_rect_Type3 fx g0 h_mk_goto_map x_14450 =
    276   let gm_map = x_14450 in h_mk_goto_map gm_map __ __
     271let rec goto_map_rect_Type3 fx g0 h_mk_goto_map x_12057 =
     272  let gm_map = x_12057 in h_mk_goto_map gm_map __ __
    277273
    278274(** val goto_map_rect_Type2 :
     
    280276    (PreIdentifiers.identifier Identifiers.identifier_map -> __ -> __ -> 'a1)
    281277    -> goto_map -> 'a1 **)
    282 let rec goto_map_rect_Type2 fx g0 h_mk_goto_map x_14452 =
    283   let gm_map = x_14452 in h_mk_goto_map gm_map __ __
     278let rec goto_map_rect_Type2 fx g0 h_mk_goto_map x_12059 =
     279  let gm_map = x_12059 in h_mk_goto_map gm_map __ __
    284280
    285281(** val goto_map_rect_Type1 :
     
    287283    (PreIdentifiers.identifier Identifiers.identifier_map -> __ -> __ -> 'a1)
    288284    -> goto_map -> 'a1 **)
    289 let rec goto_map_rect_Type1 fx g0 h_mk_goto_map x_14454 =
    290   let gm_map = x_14454 in h_mk_goto_map gm_map __ __
     285let rec goto_map_rect_Type1 fx g0 h_mk_goto_map x_12061 =
     286  let gm_map = x_12061 in h_mk_goto_map gm_map __ __
    291287
    292288(** val goto_map_rect_Type0 :
     
    294290    (PreIdentifiers.identifier Identifiers.identifier_map -> __ -> __ -> 'a1)
    295291    -> goto_map -> 'a1 **)
    296 let rec goto_map_rect_Type0 fx g0 h_mk_goto_map x_14456 =
    297   let gm_map = x_14456 in h_mk_goto_map gm_map __ __
     292let rec goto_map_rect_Type0 fx g0 h_mk_goto_map x_12063 =
     293  let gm_map = x_12063 in h_mk_goto_map gm_map __ __
    298294
    299295(** val gm_map :
     
    403399    Graphs.label Types.sig0 -> Graphs.label Types.sig0 -> 'a1) -> partial_fn
    404400    -> 'a1 **)
    405 let rec partial_fn_rect_Type4 fx h_mk_partial_fn x_14474 =
     401let rec partial_fn_rect_Type4 fx h_mk_partial_fn x_12081 =
    406402  let { pf_labgen = pf_labgen0; pf_reggen = pf_reggen0; pf_params =
    407403    pf_params0; pf_locals = pf_locals0; pf_result = pf_result0;
    408404    pf_stacksize = pf_stacksize0; pf_graph = pf_graph0; pf_gotos = pf_gotos0;
    409405    pf_labels = pf_labels0; pf_entry = pf_entry0; pf_exit = pf_exit0 } =
    410     x_14474
     406    x_12081
    411407  in
    412408  h_mk_partial_fn pf_labgen0 pf_reggen0 pf_params0 pf_locals0 pf_result0 __
     
    421417    Graphs.label Types.sig0 -> Graphs.label Types.sig0 -> 'a1) -> partial_fn
    422418    -> 'a1 **)
    423 let rec partial_fn_rect_Type5 fx h_mk_partial_fn x_14476 =
     419let rec partial_fn_rect_Type5 fx h_mk_partial_fn x_12083 =
    424420  let { pf_labgen = pf_labgen0; pf_reggen = pf_reggen0; pf_params =
    425421    pf_params0; pf_locals = pf_locals0; pf_result = pf_result0;
    426422    pf_stacksize = pf_stacksize0; pf_graph = pf_graph0; pf_gotos = pf_gotos0;
    427423    pf_labels = pf_labels0; pf_entry = pf_entry0; pf_exit = pf_exit0 } =
    428     x_14476
     424    x_12083
    429425  in
    430426  h_mk_partial_fn pf_labgen0 pf_reggen0 pf_params0 pf_locals0 pf_result0 __
     
    439435    Graphs.label Types.sig0 -> Graphs.label Types.sig0 -> 'a1) -> partial_fn
    440436    -> 'a1 **)
    441 let rec partial_fn_rect_Type3 fx h_mk_partial_fn x_14478 =
     437let rec partial_fn_rect_Type3 fx h_mk_partial_fn x_12085 =
    442438  let { pf_labgen = pf_labgen0; pf_reggen = pf_reggen0; pf_params =
    443439    pf_params0; pf_locals = pf_locals0; pf_result = pf_result0;
    444440    pf_stacksize = pf_stacksize0; pf_graph = pf_graph0; pf_gotos = pf_gotos0;
    445441    pf_labels = pf_labels0; pf_entry = pf_entry0; pf_exit = pf_exit0 } =
    446     x_14478
     442    x_12085
    447443  in
    448444  h_mk_partial_fn pf_labgen0 pf_reggen0 pf_params0 pf_locals0 pf_result0 __
     
    457453    Graphs.label Types.sig0 -> Graphs.label Types.sig0 -> 'a1) -> partial_fn
    458454    -> 'a1 **)
    459 let rec partial_fn_rect_Type2 fx h_mk_partial_fn x_14480 =
     455let rec partial_fn_rect_Type2 fx h_mk_partial_fn x_12087 =
    460456  let { pf_labgen = pf_labgen0; pf_reggen = pf_reggen0; pf_params =
    461457    pf_params0; pf_locals = pf_locals0; pf_result = pf_result0;
    462458    pf_stacksize = pf_stacksize0; pf_graph = pf_graph0; pf_gotos = pf_gotos0;
    463459    pf_labels = pf_labels0; pf_entry = pf_entry0; pf_exit = pf_exit0 } =
    464     x_14480
     460    x_12087
    465461  in
    466462  h_mk_partial_fn pf_labgen0 pf_reggen0 pf_params0 pf_locals0 pf_result0 __
     
    475471    Graphs.label Types.sig0 -> Graphs.label Types.sig0 -> 'a1) -> partial_fn
    476472    -> 'a1 **)
    477 let rec partial_fn_rect_Type1 fx h_mk_partial_fn x_14482 =
     473let rec partial_fn_rect_Type1 fx h_mk_partial_fn x_12089 =
    478474  let { pf_labgen = pf_labgen0; pf_reggen = pf_reggen0; pf_params =
    479475    pf_params0; pf_locals = pf_locals0; pf_result = pf_result0;
    480476    pf_stacksize = pf_stacksize0; pf_graph = pf_graph0; pf_gotos = pf_gotos0;
    481477    pf_labels = pf_labels0; pf_entry = pf_entry0; pf_exit = pf_exit0 } =
    482     x_14482
     478    x_12089
    483479  in
    484480  h_mk_partial_fn pf_labgen0 pf_reggen0 pf_params0 pf_locals0 pf_result0 __
     
    493489    Graphs.label Types.sig0 -> Graphs.label Types.sig0 -> 'a1) -> partial_fn
    494490    -> 'a1 **)
    495 let rec partial_fn_rect_Type0 fx h_mk_partial_fn x_14484 =
     491let rec partial_fn_rect_Type0 fx h_mk_partial_fn x_12091 =
    496492  let { pf_labgen = pf_labgen0; pf_reggen = pf_reggen0; pf_params =
    497493    pf_params0; pf_locals = pf_locals0; pf_result = pf_result0;
    498494    pf_stacksize = pf_stacksize0; pf_graph = pf_graph0; pf_gotos = pf_gotos0;
    499495    pf_labels = pf_labels0; pf_entry = pf_entry0; pf_exit = pf_exit0 } =
    500     x_14484
     496    x_12091
    501497  in
    502498  h_mk_partial_fn pf_labgen0 pf_reggen0 pf_params0 pf_locals0 pf_result0 __
     
    681677    f.pf_params; pf_locals = f.pf_locals; pf_result = f.pf_result;
    682678    pf_stacksize = f.pf_stacksize; pf_graph =
    683     (Identifiers.add Graphs.labelTag f.pf_graph l s); pf_gotos =
     679    (Identifiers.add PreIdentifiers.LabelTag f.pf_graph l s); pf_gotos =
    684680    (gm_map fx f.pf_graph f.pf_gotos); pf_labels = (Types.pi1 f.pf_labels);
    685681    pf_entry = (Types.pi1 f.pf_entry); pf_exit = (Types.pi1 f.pf_exit) }
     
    692688    f.pf_params; pf_locals = f.pf_locals; pf_result = f.pf_result;
    693689    pf_stacksize = f.pf_stacksize; pf_graph =
    694     (Identifiers.add Graphs.labelTag f.pf_graph l s); pf_gotos =
     690    (Identifiers.add PreIdentifiers.LabelTag f.pf_graph l s); pf_gotos =
    695691    (let m = f.pf_gotos in m); pf_labels = (let m = f.pf_labels in m);
    696692    pf_entry = l; pf_exit = (Types.pi1 f.pf_exit) }
     
    709705let add_fresh_to_graph fx s f =
    710706  (let { Types.fst = l; Types.snd = g0 } =
    711      Identifiers.fresh Graphs.labelTag f.pf_labgen
     707     Identifiers.fresh PreIdentifiers.LabelTag f.pf_labgen
    712708   in
    713709  (fun _ ->
     
    716712  pf_locals = f.pf_locals; pf_result = f.pf_result; pf_stacksize =
    717713  f.pf_stacksize; pf_graph =
    718   (Identifiers.add Graphs.labelTag f.pf_graph l s1); pf_gotos =
     714  (Identifiers.add PreIdentifiers.LabelTag f.pf_graph l s1); pf_gotos =
    719715  (let m = f.pf_gotos in m); pf_labels = (let m = f.pf_labels in m);
    720716  pf_entry = l; pf_exit = (Types.pi1 f.pf_exit) })) __
     
    725721let fresh_reg fx f ty =
    726722  let { Types.fst = r; Types.snd = g0 } =
    727     Identifiers.fresh Registers.registerTag f.pf_reggen
     723    Identifiers.fresh PreIdentifiers.RegisterTag f.pf_reggen
    728724  in
    729725  let f' = { pf_labgen = f.pf_labgen; pf_reggen = g0; pf_params =
     
    876872    Cminor_syntax.stmt -> partial_fn Types.sig0 -> 'a1) -> partial_fn ->
    877873    fn_con_because -> 'a1 **)
    878 let rec fn_con_because_rect_Type4 fx h_fn_con_eq h_fn_con_sig h_fn_con_addinv x_14560 = function
     874let rec fn_con_because_rect_Type4 fx h_fn_con_eq h_fn_con_sig h_fn_con_addinv x_12167 = function
    879875| Fn_con_eq f -> h_fn_con_eq f
    880876| Fn_con_sig (f1, f2, f3) -> h_fn_con_sig f1 f2 __ f3
     
    886882    Cminor_syntax.stmt -> partial_fn Types.sig0 -> 'a1) -> partial_fn ->
    887883    fn_con_because -> 'a1 **)
    888 let rec fn_con_because_rect_Type5 fx h_fn_con_eq h_fn_con_sig h_fn_con_addinv x_14567 = function
     884let rec fn_con_because_rect_Type5 fx h_fn_con_eq h_fn_con_sig h_fn_con_addinv x_12174 = function
    889885| Fn_con_eq f -> h_fn_con_eq f
    890886| Fn_con_sig (f1, f2, f3) -> h_fn_con_sig f1 f2 __ f3
     
    896892    Cminor_syntax.stmt -> partial_fn Types.sig0 -> 'a1) -> partial_fn ->
    897893    fn_con_because -> 'a1 **)
    898 let rec fn_con_because_rect_Type3 fx h_fn_con_eq h_fn_con_sig h_fn_con_addinv x_14574 = function
     894let rec fn_con_because_rect_Type3 fx h_fn_con_eq h_fn_con_sig h_fn_con_addinv x_12181 = function
    899895| Fn_con_eq f -> h_fn_con_eq f
    900896| Fn_con_sig (f1, f2, f3) -> h_fn_con_sig f1 f2 __ f3
     
    906902    Cminor_syntax.stmt -> partial_fn Types.sig0 -> 'a1) -> partial_fn ->
    907903    fn_con_because -> 'a1 **)
    908 let rec fn_con_because_rect_Type2 fx h_fn_con_eq h_fn_con_sig h_fn_con_addinv x_14581 = function
     904let rec fn_con_because_rect_Type2 fx h_fn_con_eq h_fn_con_sig h_fn_con_addinv x_12188 = function
    909905| Fn_con_eq f -> h_fn_con_eq f
    910906| Fn_con_sig (f1, f2, f3) -> h_fn_con_sig f1 f2 __ f3
     
    916912    Cminor_syntax.stmt -> partial_fn Types.sig0 -> 'a1) -> partial_fn ->
    917913    fn_con_because -> 'a1 **)
    918 let rec fn_con_because_rect_Type1 fx h_fn_con_eq h_fn_con_sig h_fn_con_addinv x_14588 = function
     914let rec fn_con_because_rect_Type1 fx h_fn_con_eq h_fn_con_sig h_fn_con_addinv x_12195 = function
    919915| Fn_con_eq f -> h_fn_con_eq f
    920916| Fn_con_sig (f1, f2, f3) -> h_fn_con_sig f1 f2 __ f3
     
    926922    Cminor_syntax.stmt -> partial_fn Types.sig0 -> 'a1) -> partial_fn ->
    927923    fn_con_because -> 'a1 **)
    928 let rec fn_con_because_rect_Type0 fx h_fn_con_eq h_fn_con_sig h_fn_con_addinv x_14595 = function
     924let rec fn_con_because_rect_Type0 fx h_fn_con_eq h_fn_con_sig h_fn_con_addinv x_12202 = function
    929925| Fn_con_eq f -> h_fn_con_eq f
    930926| Fn_con_sig (f1, f2, f3) -> h_fn_con_sig f1 f2 __ f3
     
    12161212    pf_stacksize = f.pf_stacksize; pf_graph = f.pf_graph; pf_gotos =
    12171213    f.pf_gotos; pf_labels =
    1218     (Identifiers.add Cminor_syntax.label (Types.pi1 f.pf_labels) l
     1214    (Identifiers.add PreIdentifiers.Label (Types.pi1 f.pf_labels) l
    12191215      (Types.pi1 f.pf_entry)); pf_entry = f.pf_entry; pf_exit = f.pf_exit }
    12201216
     
    12231219let add_goto_dummy fx f dest =
    12241220  (let { Types.fst = l; Types.snd = g0 } =
    1225      Identifiers.fresh Graphs.labelTag f.pf_labgen
     1221     Identifiers.fresh PreIdentifiers.LabelTag f.pf_labgen
    12261222   in
    12271223  (fun _ -> { pf_labgen = g0; pf_reggen = f.pf_reggen; pf_params =
    12281224  f.pf_params; pf_locals = f.pf_locals; pf_result = f.pf_result;
    12291225  pf_stacksize = f.pf_stacksize; pf_graph =
    1230   (Identifiers.add Graphs.labelTag f.pf_graph l RTLabs_syntax.St_return);
    1231   pf_gotos =
    1232   (Identifiers.add Graphs.labelTag (gm_map fx f.pf_graph f.pf_gotos) l dest);
    1233   pf_labels = (Types.pi1 f.pf_labels); pf_entry = l; pf_exit =
     1226  (Identifiers.add PreIdentifiers.LabelTag f.pf_graph l
     1227    RTLabs_syntax.St_return); pf_gotos =
     1228  (Identifiers.add PreIdentifiers.LabelTag (gm_map fx f.pf_graph f.pf_gotos)
     1229    l dest); pf_labels = (Types.pi1 f.pf_labels); pf_entry = l; pf_exit =
    12341230  (Types.pi1 f.pf_exit) })) __
    12351231
     
    13211317(** val patch_gotos : fixed -> partial_fn -> partial_fn Types.sig0 **)
    13221318let patch_gotos fx f =
    1323   Identifiers.fold_inf Graphs.labelTag (gm_map fx f.pf_graph f.pf_gotos)
    1324     (fun l l' _ f' ->
     1319  Identifiers.fold_inf PreIdentifiers.LabelTag
     1320    (gm_map fx f.pf_graph f.pf_gotos) (fun l l' _ f' ->
    13251321    Types.pi1
    13261322      (fill_in_statement fx l (RTLabs_syntax.St_skip
    1327         (Identifiers.lookup_present Cminor_syntax.label
     1323        (Identifiers.lookup_present PreIdentifiers.Label
    13281324          (Types.pi1 (Types.pi1 f').pf_labels) l')) (Types.pi1 f'))) f
    13291325
     
    13311327    Cminor_syntax.internal_function -> RTLabs_syntax.internal_function **)
    13321328let c2ra_function f =
    1333   let labgen0 = Identifiers.new_universe Graphs.labelTag in
    1334   let reggen0 = Identifiers.new_universe Registers.registerTag in
     1329  let labgen0 = Identifiers.new_universe PreIdentifiers.LabelTag in
     1330  let reggen0 = Identifiers.new_universe PreIdentifiers.RegisterTag in
    13351331  let cminor_labels = Cminor_syntax.labels_of f.Cminor_syntax.f_body in
    1336   (let { Types.fst = eta3072; Types.snd = reggen1 } =
    1337      populate_env (Identifiers.empty_map AST.symbolTag) reggen0
     1332  (let { Types.fst = eta1530; Types.snd = reggen1 } =
     1333     populate_env (Identifiers.empty_map PreIdentifiers.SymbolTag) reggen0
    13381334       f.Cminor_syntax.f_params
    13391335   in
    1340   let { Types.fst = params; Types.snd = env1 } = eta3072 in
     1336  let { Types.fst = params; Types.snd = env1 } = eta1530 in
    13411337  (fun _ ->
    1342   (let { Types.fst = eta3071; Types.snd = reggen2 } =
     1338  (let { Types.fst = eta1529; Types.snd = reggen2 } =
    13431339     populate_env env1 reggen1 f.Cminor_syntax.f_vars
    13441340   in
    1345   let { Types.fst = locals0; Types.snd = env0 } = eta3071 in
     1341  let { Types.fst = locals0; Types.snd = env0 } = eta1529 in
    13461342  (fun _ ->
    13471343  (let { Types.dpi1 = locals_reggen; Types.dpi2 = result } =
     
    13521348     | Types.Some ty ->
    13531349       let { Types.fst = r; Types.snd = gen } =
    1354          Identifiers.fresh Registers.registerTag reggen2
     1350         Identifiers.fresh PreIdentifiers.RegisterTag reggen2
    13551351       in
    13561352       { Types.dpi1 = { Types.fst = (List.Cons ({ Types.fst = r; Types.snd =
     
    13611357  let reggen = locals_reggen.Types.snd in
    13621358  let { Types.fst = l; Types.snd = labgen } =
    1363     Identifiers.fresh Graphs.labelTag labgen0
     1359    Identifiers.fresh PreIdentifiers.LabelTag labgen0
    13641360  in
    13651361  let fixed0 = { fx_gotos =
    1366     (Identifiers.set_of_list Cminor_syntax.label
     1362    (Identifiers.set_of_list PreIdentifiers.Label
    13671363      (Cminor_syntax.labels_of f.Cminor_syntax.f_body)); fx_env = env0;
    13681364    fx_rettyp = f.Cminor_syntax.f_return }
     
    13711367    pf_locals = locals; pf_result = (Obj.magic result); pf_stacksize =
    13721368    f.Cminor_syntax.f_stacksize; pf_graph =
    1373     (Identifiers.add Graphs.labelTag (Identifiers.empty_map Graphs.labelTag)
    1374       l RTLabs_syntax.St_return); pf_gotos =
    1375     (Identifiers.empty_map Graphs.labelTag); pf_labels =
    1376     (Identifiers.empty_map Cminor_syntax.label); pf_entry = l; pf_exit = l }
     1369    (Identifiers.add PreIdentifiers.LabelTag
     1370      (Identifiers.empty_map PreIdentifiers.LabelTag) l
     1371      RTLabs_syntax.St_return); pf_gotos =
     1372    (Identifiers.empty_map PreIdentifiers.LabelTag); pf_labels =
     1373    (Identifiers.empty_map PreIdentifiers.Label); pf_entry = l; pf_exit = l }
    13771374  in
    13781375  let f0 = add_stmt fixed0 f.Cminor_syntax.f_body emptyfn in
Note: See TracChangeset for help on using the changeset viewer.