Changeset 2775 for extracted/toRTLabs.ml
 Timestamp:
 Mar 5, 2013, 9:52:39 PM (8 years ago)
 File:

 1 edited
Legend:
 Unmodified
 Added
 Removed

extracted/toRTLabs.ml
r2773 r2775 121 121 List.foldr (fun idt rsengen > 122 122 let { Types.fst = id; Types.snd = ty } = idt in 123 let { Types.fst = eta 1690; Types.snd = gen0 } = rsengen in124 let { Types.fst = rs; Types.snd = en0 } = eta 1690in123 let { Types.fst = eta2912; Types.snd = gen0 } = rsengen in 124 let { Types.fst = rs; Types.snd = en0 } = eta2912 in 125 125 let { Types.fst = r; Types.snd = gen' } = 126 126 Identifiers.fresh PreIdentifiers.RegisterTag gen0 … … 142 142 (Identifiers.identifier_set > env > AST.typ Types.option > 'a1) > 143 143 fixed > 'a1 **) 144 let rec fixed_rect_Type4 h_mk_fixed x_1 0525=144 let rec fixed_rect_Type4 h_mk_fixed x_15356 = 145 145 let { fx_gotos = fx_gotos0; fx_env = fx_env0; fx_rettyp = fx_rettyp0 } = 146 x_1 0525146 x_15356 147 147 in 148 148 h_mk_fixed fx_gotos0 fx_env0 fx_rettyp0 … … 151 151 (Identifiers.identifier_set > env > AST.typ Types.option > 'a1) > 152 152 fixed > 'a1 **) 153 let rec fixed_rect_Type5 h_mk_fixed x_1 0527=153 let rec fixed_rect_Type5 h_mk_fixed x_15358 = 154 154 let { fx_gotos = fx_gotos0; fx_env = fx_env0; fx_rettyp = fx_rettyp0 } = 155 x_1 0527155 x_15358 156 156 in 157 157 h_mk_fixed fx_gotos0 fx_env0 fx_rettyp0 … … 160 160 (Identifiers.identifier_set > env > AST.typ Types.option > 'a1) > 161 161 fixed > 'a1 **) 162 let rec fixed_rect_Type3 h_mk_fixed x_1 0529=162 let rec fixed_rect_Type3 h_mk_fixed x_15360 = 163 163 let { fx_gotos = fx_gotos0; fx_env = fx_env0; fx_rettyp = fx_rettyp0 } = 164 x_1 0529164 x_15360 165 165 in 166 166 h_mk_fixed fx_gotos0 fx_env0 fx_rettyp0 … … 169 169 (Identifiers.identifier_set > env > AST.typ Types.option > 'a1) > 170 170 fixed > 'a1 **) 171 let rec fixed_rect_Type2 h_mk_fixed x_1 0531=171 let rec fixed_rect_Type2 h_mk_fixed x_15362 = 172 172 let { fx_gotos = fx_gotos0; fx_env = fx_env0; fx_rettyp = fx_rettyp0 } = 173 x_1 0531173 x_15362 174 174 in 175 175 h_mk_fixed fx_gotos0 fx_env0 fx_rettyp0 … … 178 178 (Identifiers.identifier_set > env > AST.typ Types.option > 'a1) > 179 179 fixed > 'a1 **) 180 let rec fixed_rect_Type1 h_mk_fixed x_1 0533=180 let rec fixed_rect_Type1 h_mk_fixed x_15364 = 181 181 let { fx_gotos = fx_gotos0; fx_env = fx_env0; fx_rettyp = fx_rettyp0 } = 182 x_1 0533182 x_15364 183 183 in 184 184 h_mk_fixed fx_gotos0 fx_env0 fx_rettyp0 … … 187 187 (Identifiers.identifier_set > env > AST.typ Types.option > 'a1) > 188 188 fixed > 'a1 **) 189 let rec fixed_rect_Type0 h_mk_fixed x_1 0535=189 let rec fixed_rect_Type0 h_mk_fixed x_15366 = 190 190 let { fx_gotos = fx_gotos0; fx_env = fx_env0; fx_rettyp = fx_rettyp0 } = 191 x_1 0535191 x_15366 192 192 in 193 193 h_mk_fixed fx_gotos0 fx_env0 fx_rettyp0 … … 257 257 (PreIdentifiers.identifier Identifiers.identifier_map > __ > __ > 'a1) 258 258 > goto_map > 'a1 **) 259 let rec goto_map_rect_Type4 fx g h_mk_goto_map x_1 0551=260 let gm_map = x_1 0551in h_mk_goto_map gm_map __ __259 let rec goto_map_rect_Type4 fx g h_mk_goto_map x_15382 = 260 let gm_map = x_15382 in h_mk_goto_map gm_map __ __ 261 261 262 262 (** val goto_map_rect_Type5 : … … 264 264 (PreIdentifiers.identifier Identifiers.identifier_map > __ > __ > 'a1) 265 265 > goto_map > 'a1 **) 266 let rec goto_map_rect_Type5 fx g h_mk_goto_map x_1 0553=267 let gm_map = x_1 0553in h_mk_goto_map gm_map __ __266 let rec goto_map_rect_Type5 fx g h_mk_goto_map x_15384 = 267 let gm_map = x_15384 in h_mk_goto_map gm_map __ __ 268 268 269 269 (** val goto_map_rect_Type3 : … … 271 271 (PreIdentifiers.identifier Identifiers.identifier_map > __ > __ > 'a1) 272 272 > goto_map > 'a1 **) 273 let rec goto_map_rect_Type3 fx g h_mk_goto_map x_1 0555=274 let gm_map = x_1 0555in h_mk_goto_map gm_map __ __273 let rec goto_map_rect_Type3 fx g h_mk_goto_map x_15386 = 274 let gm_map = x_15386 in h_mk_goto_map gm_map __ __ 275 275 276 276 (** val goto_map_rect_Type2 : … … 278 278 (PreIdentifiers.identifier Identifiers.identifier_map > __ > __ > 'a1) 279 279 > goto_map > 'a1 **) 280 let rec goto_map_rect_Type2 fx g h_mk_goto_map x_1 0557=281 let gm_map = x_1 0557in h_mk_goto_map gm_map __ __280 let rec goto_map_rect_Type2 fx g h_mk_goto_map x_15388 = 281 let gm_map = x_15388 in h_mk_goto_map gm_map __ __ 282 282 283 283 (** val goto_map_rect_Type1 : … … 285 285 (PreIdentifiers.identifier Identifiers.identifier_map > __ > __ > 'a1) 286 286 > goto_map > 'a1 **) 287 let rec goto_map_rect_Type1 fx g h_mk_goto_map x_1 0559=288 let gm_map = x_1 0559in h_mk_goto_map gm_map __ __287 let rec goto_map_rect_Type1 fx g h_mk_goto_map x_15390 = 288 let gm_map = x_15390 in h_mk_goto_map gm_map __ __ 289 289 290 290 (** val goto_map_rect_Type0 : … … 292 292 (PreIdentifiers.identifier Identifiers.identifier_map > __ > __ > 'a1) 293 293 > goto_map > 'a1 **) 294 let rec goto_map_rect_Type0 fx g h_mk_goto_map x_1 0561=295 let gm_map = x_1 0561in h_mk_goto_map gm_map __ __294 let rec goto_map_rect_Type0 fx g h_mk_goto_map x_15392 = 295 let gm_map = x_15392 in h_mk_goto_map gm_map __ __ 296 296 297 297 (** val gm_map : … … 401 401 Graphs.label Types.sig0 > Graphs.label Types.sig0 > 'a1) > partial_fn 402 402 > 'a1 **) 403 let rec partial_fn_rect_Type4 fx h_mk_partial_fn x_1 0579=403 let rec partial_fn_rect_Type4 fx h_mk_partial_fn x_15410 = 404 404 let { pf_labgen = pf_labgen0; pf_reggen = pf_reggen0; pf_params = 405 405 pf_params0; pf_locals = pf_locals0; pf_result = pf_result0; 406 406 pf_stacksize = pf_stacksize0; pf_graph = pf_graph0; pf_gotos = pf_gotos0; 407 407 pf_labels = pf_labels0; pf_entry = pf_entry0; pf_exit = pf_exit0 } = 408 x_1 0579408 x_15410 409 409 in 410 410 h_mk_partial_fn pf_labgen0 pf_reggen0 pf_params0 pf_locals0 pf_result0 __ … … 419 419 Graphs.label Types.sig0 > Graphs.label Types.sig0 > 'a1) > partial_fn 420 420 > 'a1 **) 421 let rec partial_fn_rect_Type5 fx h_mk_partial_fn x_1 0581=421 let rec partial_fn_rect_Type5 fx h_mk_partial_fn x_15412 = 422 422 let { pf_labgen = pf_labgen0; pf_reggen = pf_reggen0; pf_params = 423 423 pf_params0; pf_locals = pf_locals0; pf_result = pf_result0; 424 424 pf_stacksize = pf_stacksize0; pf_graph = pf_graph0; pf_gotos = pf_gotos0; 425 425 pf_labels = pf_labels0; pf_entry = pf_entry0; pf_exit = pf_exit0 } = 426 x_1 0581426 x_15412 427 427 in 428 428 h_mk_partial_fn pf_labgen0 pf_reggen0 pf_params0 pf_locals0 pf_result0 __ … … 437 437 Graphs.label Types.sig0 > Graphs.label Types.sig0 > 'a1) > partial_fn 438 438 > 'a1 **) 439 let rec partial_fn_rect_Type3 fx h_mk_partial_fn x_1 0583=439 let rec partial_fn_rect_Type3 fx h_mk_partial_fn x_15414 = 440 440 let { pf_labgen = pf_labgen0; pf_reggen = pf_reggen0; pf_params = 441 441 pf_params0; pf_locals = pf_locals0; pf_result = pf_result0; 442 442 pf_stacksize = pf_stacksize0; pf_graph = pf_graph0; pf_gotos = pf_gotos0; 443 443 pf_labels = pf_labels0; pf_entry = pf_entry0; pf_exit = pf_exit0 } = 444 x_1 0583444 x_15414 445 445 in 446 446 h_mk_partial_fn pf_labgen0 pf_reggen0 pf_params0 pf_locals0 pf_result0 __ … … 455 455 Graphs.label Types.sig0 > Graphs.label Types.sig0 > 'a1) > partial_fn 456 456 > 'a1 **) 457 let rec partial_fn_rect_Type2 fx h_mk_partial_fn x_1 0585=457 let rec partial_fn_rect_Type2 fx h_mk_partial_fn x_15416 = 458 458 let { pf_labgen = pf_labgen0; pf_reggen = pf_reggen0; pf_params = 459 459 pf_params0; pf_locals = pf_locals0; pf_result = pf_result0; 460 460 pf_stacksize = pf_stacksize0; pf_graph = pf_graph0; pf_gotos = pf_gotos0; 461 461 pf_labels = pf_labels0; pf_entry = pf_entry0; pf_exit = pf_exit0 } = 462 x_1 0585462 x_15416 463 463 in 464 464 h_mk_partial_fn pf_labgen0 pf_reggen0 pf_params0 pf_locals0 pf_result0 __ … … 473 473 Graphs.label Types.sig0 > Graphs.label Types.sig0 > 'a1) > partial_fn 474 474 > 'a1 **) 475 let rec partial_fn_rect_Type1 fx h_mk_partial_fn x_1 0587=475 let rec partial_fn_rect_Type1 fx h_mk_partial_fn x_15418 = 476 476 let { pf_labgen = pf_labgen0; pf_reggen = pf_reggen0; pf_params = 477 477 pf_params0; pf_locals = pf_locals0; pf_result = pf_result0; 478 478 pf_stacksize = pf_stacksize0; pf_graph = pf_graph0; pf_gotos = pf_gotos0; 479 479 pf_labels = pf_labels0; pf_entry = pf_entry0; pf_exit = pf_exit0 } = 480 x_1 0587480 x_15418 481 481 in 482 482 h_mk_partial_fn pf_labgen0 pf_reggen0 pf_params0 pf_locals0 pf_result0 __ … … 491 491 Graphs.label Types.sig0 > Graphs.label Types.sig0 > 'a1) > partial_fn 492 492 > 'a1 **) 493 let rec partial_fn_rect_Type0 fx h_mk_partial_fn x_1 0589=493 let rec partial_fn_rect_Type0 fx h_mk_partial_fn x_15420 = 494 494 let { pf_labgen = pf_labgen0; pf_reggen = pf_reggen0; pf_params = 495 495 pf_params0; pf_locals = pf_locals0; pf_result = pf_result0; 496 496 pf_stacksize = pf_stacksize0; pf_graph = pf_graph0; pf_gotos = pf_gotos0; 497 497 pf_labels = pf_labels0; pf_entry = pf_entry0; pf_exit = pf_exit0 } = 498 x_1 0589498 x_15420 499 499 in 500 500 h_mk_partial_fn pf_labgen0 pf_reggen0 pf_params0 pf_locals0 pf_result0 __ … … 874 874 Cminor_syntax.stmt > partial_fn Types.sig0 > 'a1) > partial_fn > 875 875 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_1 0665= function876 let rec fn_con_because_rect_Type4 fx h_fn_con_eq h_fn_con_sig h_fn_con_addinv x_15496 = function 877 877  Fn_con_eq f > h_fn_con_eq f 878 878  Fn_con_sig (f1, f2, f3) > h_fn_con_sig f1 f2 __ f3 … … 884 884 Cminor_syntax.stmt > partial_fn Types.sig0 > 'a1) > partial_fn > 885 885 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_1 0672= function886 let rec fn_con_because_rect_Type5 fx h_fn_con_eq h_fn_con_sig h_fn_con_addinv x_15503 = function 887 887  Fn_con_eq f > h_fn_con_eq f 888 888  Fn_con_sig (f1, f2, f3) > h_fn_con_sig f1 f2 __ f3 … … 894 894 Cminor_syntax.stmt > partial_fn Types.sig0 > 'a1) > partial_fn > 895 895 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_1 0679= function896 let rec fn_con_because_rect_Type3 fx h_fn_con_eq h_fn_con_sig h_fn_con_addinv x_15510 = function 897 897  Fn_con_eq f > h_fn_con_eq f 898 898  Fn_con_sig (f1, f2, f3) > h_fn_con_sig f1 f2 __ f3 … … 904 904 Cminor_syntax.stmt > partial_fn Types.sig0 > 'a1) > partial_fn > 905 905 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_1 0686= function906 let rec fn_con_because_rect_Type2 fx h_fn_con_eq h_fn_con_sig h_fn_con_addinv x_15517 = function 907 907  Fn_con_eq f > h_fn_con_eq f 908 908  Fn_con_sig (f1, f2, f3) > h_fn_con_sig f1 f2 __ f3 … … 914 914 Cminor_syntax.stmt > partial_fn Types.sig0 > 'a1) > partial_fn > 915 915 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_1 0693= function916 let rec fn_con_because_rect_Type1 fx h_fn_con_eq h_fn_con_sig h_fn_con_addinv x_15524 = function 917 917  Fn_con_eq f > h_fn_con_eq f 918 918  Fn_con_sig (f1, f2, f3) > h_fn_con_sig f1 f2 __ f3 … … 924 924 Cminor_syntax.stmt > partial_fn Types.sig0 > 'a1) > partial_fn > 925 925 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_1 0700= function926 let rec fn_con_because_rect_Type0 fx h_fn_con_eq h_fn_con_sig h_fn_con_addinv x_15531 = function 927 927  Fn_con_eq f > h_fn_con_eq f 928 928  Fn_con_sig (f1, f2, f3) > h_fn_con_sig f1 f2 __ f3 … … 1332 1332 let reggen0 = Identifiers.new_universe PreIdentifiers.RegisterTag in 1333 1333 let cminor_labels = Cminor_syntax.labels_of f.Cminor_syntax.f_body in 1334 (let { Types.fst = eta 1917; Types.snd = reggen1 } =1334 (let { Types.fst = eta3139; Types.snd = reggen1 } = 1335 1335 populate_env (Identifiers.empty_map PreIdentifiers.SymbolTag) reggen0 1336 1336 f.Cminor_syntax.f_params 1337 1337 in 1338 let { Types.fst = params; Types.snd = env1 } = eta 1917in1338 let { Types.fst = params; Types.snd = env1 } = eta3139 in 1339 1339 (fun _ > 1340 (let { Types.fst = eta 1916; Types.snd = reggen2 } =1340 (let { Types.fst = eta3138; Types.snd = reggen2 } = 1341 1341 populate_env env1 reggen1 f.Cminor_syntax.f_vars 1342 1342 in 1343 let { Types.fst = locals0; Types.snd = env0 } = eta 1916in1343 let { Types.fst = locals0; Types.snd = env0 } = eta3138 in 1344 1344 (fun _ > 1345 1345 (let { Types.dpi1 = locals_reggen; Types.dpi2 = result } =
Note: See TracChangeset
for help on using the changeset viewer.