Changeset 2773 for extracted/toRTLabs.ml
 Timestamp:
 Mar 4, 2013, 10:03:33 AM (7 years ago)
 File:

 1 edited
Legend:
 Unmodified
 Added
 Removed

extracted/toRTLabs.ml
r2743 r2773 95 95 open Globalenvs 96 96 97 open CostLabel 98 99 open FrontEndOps 100 101 open Cminor_syntax 102 97 103 open BitVectorTrie 98 99 open CostLabel100 101 open FrontEndOps102 103 open Cminor_syntax104 104 105 105 open Graphs … … 121 121 List.foldr (fun idt rsengen > 122 122 let { Types.fst = id; Types.snd = ty } = idt in 123 let { Types.fst = eta 2917; Types.snd = gen0 } = rsengen in124 let { Types.fst = rs; Types.snd = en0 } = eta 2917in123 let { Types.fst = eta1690; Types.snd = gen0 } = rsengen in 124 let { Types.fst = rs; Types.snd = en0 } = eta1690 in 125 125 let { Types.fst = r; Types.snd = gen' } = 126 126 Identifiers.fresh PreIdentifiers.RegisterTag gen0 … … 133 133 134 134 (** val lookup_reg : env > AST.ident > AST.typ > Registers.register **) 135 let lookup_reg e 0id ty =136 (Identifiers.lookup_present PreIdentifiers.SymbolTag e 0id).Types.fst135 let lookup_reg e id ty = 136 (Identifiers.lookup_present PreIdentifiers.SymbolTag e id).Types.fst 137 137 138 138 type fixed = { fx_gotos : Identifiers.identifier_set; fx_env : env; … … 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 5343=144 let rec fixed_rect_Type4 h_mk_fixed x_10525 = 145 145 let { fx_gotos = fx_gotos0; fx_env = fx_env0; fx_rettyp = fx_rettyp0 } = 146 x_1 5343146 x_10525 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 5345=153 let rec fixed_rect_Type5 h_mk_fixed x_10527 = 154 154 let { fx_gotos = fx_gotos0; fx_env = fx_env0; fx_rettyp = fx_rettyp0 } = 155 x_1 5345155 x_10527 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 5347=162 let rec fixed_rect_Type3 h_mk_fixed x_10529 = 163 163 let { fx_gotos = fx_gotos0; fx_env = fx_env0; fx_rettyp = fx_rettyp0 } = 164 x_1 5347164 x_10529 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 5349=171 let rec fixed_rect_Type2 h_mk_fixed x_10531 = 172 172 let { fx_gotos = fx_gotos0; fx_env = fx_env0; fx_rettyp = fx_rettyp0 } = 173 x_1 5349173 x_10531 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 5351=180 let rec fixed_rect_Type1 h_mk_fixed x_10533 = 181 181 let { fx_gotos = fx_gotos0; fx_env = fx_env0; fx_rettyp = fx_rettyp0 } = 182 x_1 5351182 x_10533 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 5353=189 let rec fixed_rect_Type0 h_mk_fixed x_10535 = 190 190 let { fx_gotos = fx_gotos0; fx_env = fx_env0; fx_rettyp = fx_rettyp0 } = 191 x_1 5353191 x_10535 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 0 h_mk_goto_map x_15369=260 let gm_map = x_1 5369in h_mk_goto_map gm_map __ __259 let rec goto_map_rect_Type4 fx g h_mk_goto_map x_10551 = 260 let gm_map = x_10551 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 0 h_mk_goto_map x_15371=267 let gm_map = x_1 5371in h_mk_goto_map gm_map __ __266 let rec goto_map_rect_Type5 fx g h_mk_goto_map x_10553 = 267 let gm_map = x_10553 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 0 h_mk_goto_map x_15373=274 let gm_map = x_1 5373in h_mk_goto_map gm_map __ __273 let rec goto_map_rect_Type3 fx g h_mk_goto_map x_10555 = 274 let gm_map = x_10555 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 0 h_mk_goto_map x_15375=281 let gm_map = x_1 5375in h_mk_goto_map gm_map __ __280 let rec goto_map_rect_Type2 fx g h_mk_goto_map x_10557 = 281 let gm_map = x_10557 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 0 h_mk_goto_map x_15377=288 let gm_map = x_1 5377in h_mk_goto_map gm_map __ __287 let rec goto_map_rect_Type1 fx g h_mk_goto_map x_10559 = 288 let gm_map = x_10559 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 0 h_mk_goto_map x_15379=295 let gm_map = x_1 5379in h_mk_goto_map gm_map __ __294 let rec goto_map_rect_Type0 fx g h_mk_goto_map x_10561 = 295 let gm_map = x_10561 in h_mk_goto_map gm_map __ __ 296 296 297 297 (** val gm_map : 298 298 fixed > RTLabs_syntax.statement Graphs.graph > goto_map > 299 299 PreIdentifiers.identifier Identifiers.identifier_map **) 300 let rec gm_map fx g 0xxx =300 let rec gm_map fx g xxx = 301 301 let yyy = xxx in yyy 302 302 … … 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 5397=403 let rec partial_fn_rect_Type4 fx h_mk_partial_fn x_10579 = 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 5397408 x_10579 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 5399=421 let rec partial_fn_rect_Type5 fx h_mk_partial_fn x_10581 = 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 5399426 x_10581 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 5401=439 let rec partial_fn_rect_Type3 fx h_mk_partial_fn x_10583 = 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 5401444 x_10583 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 5403=457 let rec partial_fn_rect_Type2 fx h_mk_partial_fn x_10585 = 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 5403462 x_10585 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 5405=475 let rec partial_fn_rect_Type1 fx h_mk_partial_fn x_10587 = 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 5405480 x_10587 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 5407=493 let rec partial_fn_rect_Type0 fx h_mk_partial_fn x_10589 = 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 5407498 x_10589 499 499 in 500 500 h_mk_partial_fn pf_labgen0 pf_reggen0 pf_params0 pf_locals0 pf_result0 __ … … 706 706 partial_fn Types.sig0 **) 707 707 let add_fresh_to_graph fx s f = 708 (let { Types.fst = l; Types.snd = g 0} =708 (let { Types.fst = l; Types.snd = g } = 709 709 Identifiers.fresh PreIdentifiers.LabelTag f.pf_labgen 710 710 in 711 711 (fun _ > 712 712 let s1 = s (Types.pi1 f.pf_entry) in 713 { pf_labgen = g 0; pf_reggen = f.pf_reggen; pf_params = f.pf_params;713 { pf_labgen = g; pf_reggen = f.pf_reggen; pf_params = f.pf_params; 714 714 pf_locals = f.pf_locals; pf_result = f.pf_result; pf_stacksize = 715 715 f.pf_stacksize; pf_graph = … … 722 722 Registers.register Types.sig0) Types.dPair **) 723 723 let fresh_reg fx f ty = 724 let { Types.fst = r; Types.snd = g 0} =724 let { Types.fst = r; Types.snd = g } = 725 725 Identifiers.fresh PreIdentifiers.RegisterTag f.pf_reggen 726 726 in 727 let f' = { pf_labgen = f.pf_labgen; pf_reggen = g 0; pf_params =728 f.pf_params; pf_locals = (List.Cons ({ Types.fst = r; Types.snd = ty },729 f.pf_locals));pf_result =727 let f' = { pf_labgen = f.pf_labgen; pf_reggen = g; pf_params = f.pf_params; 728 pf_locals = (List.Cons ({ Types.fst = r; Types.snd = ty }, f.pf_locals)); 729 pf_result = 730 730 ((match fx.fx_rettyp with 731 731  Types.None > Obj.magic __ … … 741 741 fixed > AST.typ > Cminor_syntax.expr > partial_fn > (partial_fn 742 742 Types.sig0, Registers.register Types.sig0) Types.dPair **) 743 let choose_reg fx ty e 0f =744 (match e 0with743 let choose_reg fx ty e f = 744 (match e with 745 745  Cminor_syntax.Id (t, i) > 746 746 (fun _ > { Types.dpi1 = f; Types.dpi2 = (lookup_reg fx.fx_env i t) }) … … 777 777 Types.sig0) Types.dPair **) 778 778 let choose_regs fx es f = 779 foldr_all' (fun e 0_ tl acc >779 foldr_all' (fun e _ tl acc > 780 780 let { Types.dpi1 = f1; Types.dpi2 = rs } = acc in 781 (let { Types.dpi1 = t; Types.dpi2 = e 1 } = e0in781 (let { Types.dpi1 = t; Types.dpi2 = e0 } = e in 782 782 (fun _ > 783 783 let { Types.dpi1 = f'; Types.dpi2 = r } = 784 choose_reg fx t e 1(Types.pi1 f1)784 choose_reg fx t e0 (Types.pi1 f1) 785 785 in 786 786 { Types.dpi1 = (Types.pi1 f'); Types.dpi2 = (List.Cons ((Types.pi1 r), … … 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 5483= function876 let rec fn_con_because_rect_Type4 fx h_fn_con_eq h_fn_con_sig h_fn_con_addinv x_10665 = 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 5490= function886 let rec fn_con_because_rect_Type5 fx h_fn_con_eq h_fn_con_sig h_fn_con_addinv x_10672 = 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 5497= function896 let rec fn_con_because_rect_Type3 fx h_fn_con_eq h_fn_con_sig h_fn_con_addinv x_10679 = 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 5504= function906 let rec fn_con_because_rect_Type2 fx h_fn_con_eq h_fn_con_sig h_fn_con_addinv x_10686 = 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 5511= function916 let rec fn_con_because_rect_Type1 fx h_fn_con_eq h_fn_con_sig h_fn_con_addinv x_10693 = 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 5518= function926 let rec fn_con_because_rect_Type0 fx h_fn_con_eq h_fn_con_sig h_fn_con_addinv x_10700 = 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 … … 999 999 fixed > AST.typ > Cminor_syntax.expr > partial_fn > 1000 1000 Registers.register Types.sig0 > partial_fn Types.sig0 **) 1001 let rec add_expr fx ty e 0f dst =1002 (match e 0with1001 let rec add_expr fx ty e f dst = 1002 (match e with 1003 1003  Cminor_syntax.Id (t, i) > 1004 1004 (fun _ dst0 > … … 1015 1015 (add_fresh_to_graph fx (fun x0 > RTLabs_syntax.St_const (x, 1016 1016 (Types.pi1 dst0), c, x0)) f)) 1017  Cminor_syntax.Op1 (t, t', op 0, e') >1017  Cminor_syntax.Op1 (t, t', op, e') > 1018 1018 (fun _ dst0 > 1019 1019 let { Types.dpi1 = f0; Types.dpi2 = r } = choose_reg fx t e' f in 1020 1020 let f1 = 1021 add_fresh_to_graph fx (fun x > RTLabs_syntax.St_op1 (t', t, op 0,1021 add_fresh_to_graph fx (fun x > RTLabs_syntax.St_op1 (t', t, op, 1022 1022 (Types.pi1 dst0), (Types.pi1 r), x)) (Types.pi1 f0) 1023 1023 in 1024 1024 let f2 = add_expr fx t e' (Types.pi1 f1) (Types.pi1 r) in Types.pi1 f2) 1025  Cminor_syntax.Op2 (x, x0, x1, op 0, e1, e2) >1025  Cminor_syntax.Op2 (x, x0, x1, op, e1, e2) > 1026 1026 (fun _ dst0 > 1027 let { Types.dpi1 = f0; Types.dpi2 = r 5} = choose_reg fx x e1 f in1028 let { Types.dpi1 = f1; Types.dpi2 = r 6} =1027 let { Types.dpi1 = f0; Types.dpi2 = r1 } = choose_reg fx x e1 f in 1028 let { Types.dpi1 = f1; Types.dpi2 = r2 } = 1029 1029 choose_reg fx x0 e2 (Types.pi1 f0) 1030 1030 in 1031 1031 let f2 = 1032 1032 add_fresh_to_graph fx (fun x2 > RTLabs_syntax.St_op2 (x1, x, x0, 1033 op 0, (Types.pi1 dst0), (Types.pi1 r5), (Types.pi1 r6), x2))1033 op, (Types.pi1 dst0), (Types.pi1 r1), (Types.pi1 r2), x2)) 1034 1034 (Types.pi1 f1) 1035 1035 in 1036 let f3 = add_expr fx x0 e2 (Types.pi1 f2) (Types.pi1 r 6) in1037 let f4 = add_expr fx x e1 (Types.pi1 f3) (Types.pi1 r 5) in1036 let f3 = add_expr fx x0 e2 (Types.pi1 f2) (Types.pi1 r2) in 1037 let f4 = add_expr fx x e1 (Types.pi1 f3) (Types.pi1 r1) in 1038 1038 Types.pi1 f4) 1039 1039  Cminor_syntax.Mem (t, e') > … … 1088 1088  List.Nil > (fun _ > f) 1089 1089  List.Cons (x1, x2) > (fun _ > assert false (* absurd case *))) 1090  List.Cons (e 0, et) >1090  List.Cons (e, et) > 1091 1091 (fun _ > 1092 1092 match dsts with … … 1095 1095 (fun _ _ > 1096 1096 let f' = add_exprs fx et rt f in 1097 (let { Types.dpi1 = ty; Types.dpi2 = e 1 } = e0in1097 (let { Types.dpi1 = ty; Types.dpi2 = e0 } = e in 1098 1098 (fun _ _ > 1099 let f'' = add_expr fx ty e 1(Types.pi1 f') r in Types.pi1 f'')) __1099 let f'' = add_expr fx ty e0 (Types.pi1 f') r in Types.pi1 f'')) __ 1100 1100 __))) __ __ __ 1101 1102 (** val stmt_inv_rect_Type4 : 1103 fixed > Cminor_syntax.stmt > (__ > __ > __ > 'a1) > 'a1 **) 1104 let rec stmt_inv_rect_Type4 fx s h_mk_stmt_inv = 1105 h_mk_stmt_inv __ __ __ 1101 1106 1102 1107 (** val stmt_inv_rect_Type5 : … … 1105 1110 h_mk_stmt_inv __ __ __ 1106 1111 1107 (** val stmt_inv_rect_Type 6:1112 (** val stmt_inv_rect_Type3 : 1108 1113 fixed > Cminor_syntax.stmt > (__ > __ > __ > 'a1) > 'a1 **) 1109 let rec stmt_inv_rect_Type 6fx s h_mk_stmt_inv =1114 let rec stmt_inv_rect_Type3 fx s h_mk_stmt_inv = 1110 1115 h_mk_stmt_inv __ __ __ 1111 1116 1112 (** val stmt_inv_rect_Type 7:1117 (** val stmt_inv_rect_Type2 : 1113 1118 fixed > Cminor_syntax.stmt > (__ > __ > __ > 'a1) > 'a1 **) 1114 let rec stmt_inv_rect_Type 7fx s h_mk_stmt_inv =1119 let rec stmt_inv_rect_Type2 fx s h_mk_stmt_inv = 1115 1120 h_mk_stmt_inv __ __ __ 1116 1121 1117 (** val stmt_inv_rect_Type 8:1122 (** val stmt_inv_rect_Type1 : 1118 1123 fixed > Cminor_syntax.stmt > (__ > __ > __ > 'a1) > 'a1 **) 1119 let rec stmt_inv_rect_Type 8fx s h_mk_stmt_inv =1124 let rec stmt_inv_rect_Type1 fx s h_mk_stmt_inv = 1120 1125 h_mk_stmt_inv __ __ __ 1121 1126 1122 (** val stmt_inv_rect_Type 9:1127 (** val stmt_inv_rect_Type0 : 1123 1128 fixed > Cminor_syntax.stmt > (__ > __ > __ > 'a1) > 'a1 **) 1124 let rec stmt_inv_rect_Type9 fx s h_mk_stmt_inv = 1125 h_mk_stmt_inv __ __ __ 1126 1127 (** val stmt_inv_rect_Type10 : 1128 fixed > Cminor_syntax.stmt > (__ > __ > __ > 'a1) > 'a1 **) 1129 let rec stmt_inv_rect_Type10 fx s h_mk_stmt_inv = 1129 let rec stmt_inv_rect_Type0 fx s h_mk_stmt_inv = 1130 1130 h_mk_stmt_inv __ __ __ 1131 1131 … … 1133 1133 fixed > Cminor_syntax.stmt > (__ > __ > __ > __ > 'a1) > 'a1 **) 1134 1134 let stmt_inv_inv_rect_Type4 x1 x2 h1 = 1135 let hcut = stmt_inv_rect_Type 5x1 x2 h1 in hcut __1135 let hcut = stmt_inv_rect_Type4 x1 x2 h1 in hcut __ 1136 1136 1137 1137 (** val stmt_inv_inv_rect_Type3 : 1138 1138 fixed > Cminor_syntax.stmt > (__ > __ > __ > __ > 'a1) > 'a1 **) 1139 1139 let stmt_inv_inv_rect_Type3 x1 x2 h1 = 1140 let hcut = stmt_inv_rect_Type 7x1 x2 h1 in hcut __1140 let hcut = stmt_inv_rect_Type3 x1 x2 h1 in hcut __ 1141 1141 1142 1142 (** val stmt_inv_inv_rect_Type2 : 1143 1143 fixed > Cminor_syntax.stmt > (__ > __ > __ > __ > 'a1) > 'a1 **) 1144 1144 let stmt_inv_inv_rect_Type2 x1 x2 h1 = 1145 let hcut = stmt_inv_rect_Type 8x1 x2 h1 in hcut __1145 let hcut = stmt_inv_rect_Type2 x1 x2 h1 in hcut __ 1146 1146 1147 1147 (** val stmt_inv_inv_rect_Type1 : 1148 1148 fixed > Cminor_syntax.stmt > (__ > __ > __ > __ > 'a1) > 'a1 **) 1149 1149 let stmt_inv_inv_rect_Type1 x1 x2 h1 = 1150 let hcut = stmt_inv_rect_Type 9x1 x2 h1 in hcut __1150 let hcut = stmt_inv_rect_Type1 x1 x2 h1 in hcut __ 1151 1151 1152 1152 (** val stmt_inv_inv_rect_Type0 : 1153 1153 fixed > Cminor_syntax.stmt > (__ > __ > __ > __ > 'a1) > 'a1 **) 1154 1154 let stmt_inv_inv_rect_Type0 x1 x2 h1 = 1155 let hcut = stmt_inv_rect_Type 10 x1 x2 h1 in hcut __1155 let hcut = stmt_inv_rect_Type0 x1 x2 h1 in hcut __ 1156 1156 1157 1157 (** val stmt_inv_discr : fixed > Cminor_syntax.stmt > __ **) … … 1197 1197  Types.None > (fun _ > Types.pi1 f1) 1198 1198  Types.Some et > 1199 let { Types.dpi1 = ty; Types.dpi2 = e 0} = et in1199 let { Types.dpi1 = ty; Types.dpi2 = e } = et in 1200 1200 (fun _ > 1201 1201 (match fx.fx_rettyp with … … 1203 1203  Types.Some t > 1204 1204 (fun _ r > 1205 let r 5= Obj.magic r in1206 let f2 = add_expr fx ty e 0 (Types.pi1 f1) r5in Types.pi1 f2)) __1205 let r0 = Obj.magic r in 1206 let f2 = add_expr fx ty e (Types.pi1 f1) r0 in Types.pi1 f2)) __ 1207 1207 (Types.pi1 f1).pf_result)) __ 1208 1208 … … 1220 1220 fixed > partial_fn > PreIdentifiers.identifier > partial_fn Types.sig0 **) 1221 1221 let add_goto_dummy fx f dest = 1222 (let { Types.fst = l; Types.snd = g 0} =1222 (let { Types.fst = l; Types.snd = g } = 1223 1223 Identifiers.fresh PreIdentifiers.LabelTag f.pf_labgen 1224 1224 in 1225 (fun _ > { pf_labgen = g 0; pf_reggen = f.pf_reggen; pf_params =1225 (fun _ > { pf_labgen = g; pf_reggen = f.pf_reggen; pf_params = 1226 1226 f.pf_params; pf_locals = f.pf_locals; pf_result = f.pf_result; 1227 1227 pf_stacksize = f.pf_stacksize; pf_graph = … … 1237 1237 (match s with 1238 1238  Cminor_syntax.St_skip > (fun _ > f) 1239  Cminor_syntax.St_assign (t, x, e 0) >1239  Cminor_syntax.St_assign (t, x, e) > 1240 1240 (fun _ > 1241 1241 let dst = lookup_reg fx.fx_env x t in 1242 Types.pi1 (add_expr fx t e 0f dst))1242 Types.pi1 (add_expr fx t e f dst)) 1243 1243  Cminor_syntax.St_store (t, e1, e2) > 1244 1244 (fun _ > … … 1255 1255 in 1256 1256 Types.pi1 (add_expr fx t e2 (Types.pi1 f3) (Types.pi1 val_reg))) 1257  Cminor_syntax.St_call (return_opt_id, e 0, args) >1257  Cminor_syntax.St_call (return_opt_id, e, args) > 1258 1258 (fun _ > 1259 1259 let return_opt_reg = … … 1268 1268 in 1269 1269 let f1 = 1270 match expr_is_Id AST.ASTptr e 0with1270 match expr_is_Id AST.ASTptr e with 1271 1271  Types.None > 1272 1272 let { Types.dpi1 = f1; Types.dpi2 = fnr } = 1273 choose_reg fx AST.ASTptr e 0(Types.pi1 f0)1273 choose_reg fx AST.ASTptr e (Types.pi1 f0) 1274 1274 in 1275 1275 let f2 = … … 1279 1279 in 1280 1280 Types.pi1 1281 (add_expr fx AST.ASTptr e 0(Types.pi1 f2) (Types.pi1 fnr))1281 (add_expr fx AST.ASTptr e (Types.pi1 f2) (Types.pi1 fnr)) 1282 1282  Types.Some id > 1283 1283 add_fresh_to_graph fx (fun x > RTLabs_syntax.St_call_id (id, … … 1289 1289 let f2 = add_stmt fx s2 f in 1290 1290 let f1 = add_stmt fx s1 (Types.pi1 f2) in Types.pi1 f1) 1291  Cminor_syntax.St_ifthenelse (x, x0, e 0, s1, s2) >1291  Cminor_syntax.St_ifthenelse (x, x0, e, s1, s2) > 1292 1292 (fun _ > 1293 1293 let l_next = f.pf_entry in … … 1297 1297 let f1 = add_stmt fx s1 (Types.pi1 f0) in 1298 1298 let { Types.dpi1 = f3; Types.dpi2 = r } = 1299 choose_reg fx (AST.ASTint (x, x0)) e 0(Types.pi1 f1)1299 choose_reg fx (AST.ASTint (x, x0)) e (Types.pi1 f1) 1300 1300 in 1301 1301 let f4 = … … 1304 1304 in 1305 1305 Types.pi1 1306 (add_expr fx (AST.ASTint (x, x0)) e 0(Types.pi1 f4) (Types.pi1 r)))1306 (add_expr fx (AST.ASTint (x, x0)) e (Types.pi1 f4) (Types.pi1 r))) 1307 1307  Cminor_syntax.St_return opt_e > (fun _ > add_return fx opt_e f) 1308 1308  Cminor_syntax.St_label (l, s') > … … 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 3144; Types.snd = reggen1 } =1334 (let { Types.fst = eta1917; 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 3144in1338 let { Types.fst = params; Types.snd = env1 } = eta1917 in 1339 1339 (fun _ > 1340 (let { Types.fst = eta 3143; Types.snd = reggen2 } =1340 (let { Types.fst = eta1916; 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 3143in1343 let { Types.fst = locals0; Types.snd = env0 } = eta1916 in 1344 1344 (fun _ > 1345 1345 (let { Types.dpi1 = locals_reggen; Types.dpi2 = result } =
Note: See TracChangeset
for help on using the changeset viewer.