Changeset 2827 for extracted/cminor_semantics.ml
 Timestamp:
 Mar 8, 2013, 9:07:28 PM (7 years ago)
 File:

 1 edited
Legend:
 Unmodified
 Added
 Removed

extracted/cminor_semantics.ml
r2810 r2827 123 123 let rec cont_rect_Type4 h_Kend h_Kseq h_Kblock = function 124 124  Kend > h_Kend 125  Kseq (x_ 10, x_9) >126 h_Kseq x_ 10 x_9 (cont_rect_Type4 h_Kend h_Kseq h_Kblock x_9)127  Kblock x_ 11 > h_Kblock x_11 (cont_rect_Type4 h_Kend h_Kseq h_Kblock x_11)125  Kseq (x_70, x_69) > 126 h_Kseq x_70 x_69 (cont_rect_Type4 h_Kend h_Kseq h_Kblock x_69) 127  Kblock x_71 > h_Kblock x_71 (cont_rect_Type4 h_Kend h_Kseq h_Kblock x_71) 128 128 129 129 (** val cont_rect_Type3 : … … 132 132 let rec cont_rect_Type3 h_Kend h_Kseq h_Kblock = function 133 133  Kend > h_Kend 134  Kseq (x_ 24, x_23) >135 h_Kseq x_ 24 x_23 (cont_rect_Type3 h_Kend h_Kseq h_Kblock x_23)136  Kblock x_ 25 > h_Kblock x_25 (cont_rect_Type3 h_Kend h_Kseq h_Kblock x_25)134  Kseq (x_84, x_83) > 135 h_Kseq x_84 x_83 (cont_rect_Type3 h_Kend h_Kseq h_Kblock x_83) 136  Kblock x_85 > h_Kblock x_85 (cont_rect_Type3 h_Kend h_Kseq h_Kblock x_85) 137 137 138 138 (** val cont_rect_Type2 : … … 141 141 let rec cont_rect_Type2 h_Kend h_Kseq h_Kblock = function 142 142  Kend > h_Kend 143  Kseq (x_ 31, x_30) >144 h_Kseq x_ 31 x_30 (cont_rect_Type2 h_Kend h_Kseq h_Kblock x_30)145  Kblock x_ 32 > h_Kblock x_32 (cont_rect_Type2 h_Kend h_Kseq h_Kblock x_32)143  Kseq (x_91, x_90) > 144 h_Kseq x_91 x_90 (cont_rect_Type2 h_Kend h_Kseq h_Kblock x_90) 145  Kblock x_92 > h_Kblock x_92 (cont_rect_Type2 h_Kend h_Kseq h_Kblock x_92) 146 146 147 147 (** val cont_rect_Type1 : … … 150 150 let rec cont_rect_Type1 h_Kend h_Kseq h_Kblock = function 151 151  Kend > h_Kend 152  Kseq (x_ 38, x_37) >153 h_Kseq x_ 38 x_37 (cont_rect_Type1 h_Kend h_Kseq h_Kblock x_37)154  Kblock x_ 39 > h_Kblock x_39 (cont_rect_Type1 h_Kend h_Kseq h_Kblock x_39)152  Kseq (x_98, x_97) > 153 h_Kseq x_98 x_97 (cont_rect_Type1 h_Kend h_Kseq h_Kblock x_97) 154  Kblock x_99 > h_Kblock x_99 (cont_rect_Type1 h_Kend h_Kseq h_Kblock x_99) 155 155 156 156 (** val cont_rect_Type0 : … … 159 159 let rec cont_rect_Type0 h_Kend h_Kseq h_Kblock = function 160 160  Kend > h_Kend 161  Kseq (x_45, x_44) > 162 h_Kseq x_45 x_44 (cont_rect_Type0 h_Kend h_Kseq h_Kblock x_44) 163  Kblock x_46 > h_Kblock x_46 (cont_rect_Type0 h_Kend h_Kseq h_Kblock x_46) 161  Kseq (x_105, x_104) > 162 h_Kseq x_105 x_104 (cont_rect_Type0 h_Kend h_Kseq h_Kblock x_104) 163  Kblock x_106 > 164 h_Kblock x_106 (cont_rect_Type0 h_Kend h_Kseq h_Kblock x_106) 164 165 165 166 (** val cont_inv_rect_Type4 : … … 221 222 let rec stack_rect_Type4 h_SStop h_Scall = function 222 223  SStop > h_SStop 223  Scall (dest, f, x_1 05, en, k, x_101) >224 h_Scall dest f x_1 05 en __ __ k __ x_101225 (stack_rect_Type4 h_SStop h_Scall x_1 01)224  Scall (dest, f, x_165, en, k, x_161) > 225 h_Scall dest f x_165 en __ __ k __ x_161 226 (stack_rect_Type4 h_SStop h_Scall x_161) 226 227 227 228 (** val stack_rect_Type3 : … … 231 232 let rec stack_rect_Type3 h_SStop h_Scall = function 232 233  SStop > h_SStop 233  Scall (dest, f, x_1 21, en, k, x_117) >234 h_Scall dest f x_1 21 en __ __ k __ x_117235 (stack_rect_Type3 h_SStop h_Scall x_1 17)234  Scall (dest, f, x_181, en, k, x_177) > 235 h_Scall dest f x_181 en __ __ k __ x_177 236 (stack_rect_Type3 h_SStop h_Scall x_177) 236 237 237 238 (** val stack_rect_Type2 : … … 241 242 let rec stack_rect_Type2 h_SStop h_Scall = function 242 243  SStop > h_SStop 243  Scall (dest, f, x_1 29, en, k, x_125) >244 h_Scall dest f x_1 29 en __ __ k __ x_125245 (stack_rect_Type2 h_SStop h_Scall x_1 25)244  Scall (dest, f, x_189, en, k, x_185) > 245 h_Scall dest f x_189 en __ __ k __ x_185 246 (stack_rect_Type2 h_SStop h_Scall x_185) 246 247 247 248 (** val stack_rect_Type1 : … … 251 252 let rec stack_rect_Type1 h_SStop h_Scall = function 252 253  SStop > h_SStop 253  Scall (dest, f, x_1 37, en, k, x_133) >254 h_Scall dest f x_1 37 en __ __ k __ x_133255 (stack_rect_Type1 h_SStop h_Scall x_1 33)254  Scall (dest, f, x_197, en, k, x_193) > 255 h_Scall dest f x_197 en __ __ k __ x_193 256 (stack_rect_Type1 h_SStop h_Scall x_193) 256 257 257 258 (** val stack_rect_Type0 : … … 261 262 let rec stack_rect_Type0 h_SStop h_Scall = function 262 263  SStop > h_SStop 263  Scall (dest, f, x_ 145, en, k, x_141) >264 h_Scall dest f x_ 145 en __ __ k __ x_141265 (stack_rect_Type0 h_SStop h_Scall x_ 141)264  Scall (dest, f, x_205, en, k, x_201) > 265 h_Scall dest f x_205 en __ __ k __ x_201 266 (stack_rect_Type0 h_SStop h_Scall x_201) 266 267 267 268 (** val stack_inv_rect_Type4 : … … 701 702 (Obj.magic 702 703 (trace_map_inv (fun e > 703 let { Types.dpi1 = ty; Types.dpi2 = e 1} = e in704 (fun _ > eval_expr ge ty e 1en sp m)) args))704 let { Types.dpi1 = ty; Types.dpi2 = e0 } = e in 705 (fun _ > eval_expr ge ty e0 en sp m)) args)) 705 706 (fun tr' vargs > 706 707 Monad.m_return0 (Monad.max_def Errors.res0) { Types.fst = … … 735 736 (GenMem.free m sp), st0)) })) 736 737  Types.Some e > 737 let { Types.dpi1 = ty; Types.dpi2 = e 1} = e in738 let { Types.dpi1 = ty; Types.dpi2 = e0 } = e in 738 739 (fun _ > 739 740 Obj.magic 740 741 (Monad.m_bind2 (Monad.max_def Errors.res0) 741 (Obj.magic (eval_expr ge ty e 1en sp m)) (fun tr v >742 (Obj.magic (eval_expr ge ty e0 en sp m)) (fun tr v > 742 743 Monad.m_return0 (Monad.max_def Errors.res0) { Types.fst = tr; 743 744 Types.snd = (Returnstate ((Types.Some v), … … 750 751  Cminor_syntax.St_goto l > 751 752 (fun _ > 752 let sk = find_label_always l (Cminor_syntax.f_body f)Kend f en in753 let sk = find_label_always l f.Cminor_syntax.f_body Kend f en in 753 754 Obj.magic 754 755 (Monad.m_return0 (Monad.max_def Errors.res0) { Types.fst = … … 767 768 (let { Types.fst = m'; Types.snd = sp } = 768 769 GenMem.alloc m (Z.z_of_nat Nat.O) 769 (Z.z_of_nat (Cminor_syntax.f_stacksize f))770 (Z.z_of_nat f.Cminor_syntax.f_stacksize) 770 771 in 771 772 Obj.magic 772 773 (Monad.m_bind0 (Monad.max_def Errors.res0) 773 (Obj.magic (bind_params args (Cminor_syntax.f_params f))) 774 (fun en > 774 (Obj.magic (bind_params args f.Cminor_syntax.f_params)) (fun en > 775 775 Monad.m_return0 (Monad.max_def Errors.res0) { Types.fst = 776 Events.e0; Types.snd = (State (f, (Cminor_syntax.f_body f),777 (init_locals (Types.pi1 en) (Cminor_syntax.f_vars f)), m', sp,776 Events.e0; Types.snd = (State (f, f.Cminor_syntax.f_body, 777 (init_locals (Types.pi1 en) f.Cminor_syntax.f_vars), m', sp, 778 778 Kend, st0)) }))) 779 779  AST.External fn > … … 782 782 (Obj.magic 783 783 (IOMonad.err_to_io 784 (IO.check_eventval_list args (AST.sig_args (AST.ef_sig fn)))))784 (IO.check_eventval_list args fn.AST.ef_sig.AST.sig_args))) 785 785 (fun evargs > 786 786 Monad.m_bind0 (Monad.max_def IOMonad.iOMonad) 787 787 (Obj.magic 788 (IO.do_io (AST.ef_id fn) evargs789 (AST.proj_sig_res (AST.ef_sig fn))))(fun evres >788 (IO.do_io fn.AST.ef_id evargs (AST.proj_sig_res fn.AST.ef_sig))) 789 (fun evres > 790 790 let res = 791 match AST.sig_res (AST.ef_sig fn)with791 match fn.AST.ef_sig.AST.sig_res with 792 792  Types.None > Types.None 793 793  Types.Some x0 > 794 Types.Some 795 (IO.mk_val (AST.proj_sig_res (AST.ef_sig fn)) evres) 794 Types.Some (IO.mk_val (AST.proj_sig_res fn.AST.ef_sig) evres) 796 795 in 797 796 Monad.m_return0 (Monad.max_def IOMonad.iOMonad) { Types.fst = 798 (Events.eextcall (AST.ef_id fn)evargs799 (IO.mk_eventval (AST.proj_sig_res (AST.ef_sig fn)) evres));797 (Events.eextcall fn.AST.ef_id evargs 798 (IO.mk_eventval (AST.proj_sig_res fn.AST.ef_sig) evres)); 800 799 Types.snd = (Returnstate (res, m, st0)) })))) 801 800  Returnstate (result, m, st0) > … … 880 879 (Obj.magic 881 880 (Errors.opt_to_res (Errors.msg ErrorMessages.MainMissing) 882 (Globalenvs.find_symbol ge (AST.prog_main p)))) (fun b >881 (Globalenvs.find_symbol ge p.AST.prog_main))) (fun b > 883 882 Monad.m_bind0 (Monad.max_def Errors.res0) 884 883 (Obj.magic 885 884 (Errors.opt_to_res (Errors.msg ErrorMessages.MainMissing) 886 885 (Globalenvs.find_funct_ptr ge b))) (fun f > 887 Obj.magic (Errors.OK (Callstate ( (AST.prog_main p), f, List.Nil, m,886 Obj.magic (Errors.OK (Callstate (p.AST.prog_main, f, List.Nil, m, 888 887 SStop))))))) 889 888 … … 910 909 (Obj.magic 911 910 (Errors.opt_to_res (Errors.msg ErrorMessages.MainMissing) 912 (Globalenvs.find_symbol ge (AST.prog_main p)))) (fun b >911 (Globalenvs.find_symbol ge p.AST.prog_main))) (fun b > 913 912 Monad.m_bind0 (Monad.max_def Errors.res0) 914 913 (Obj.magic 915 914 (Errors.opt_to_res (Errors.msg ErrorMessages.MainMissing) 916 915 (Globalenvs.find_funct_ptr ge b))) (fun f > 917 Obj.magic (Errors.OK (Callstate ( (AST.prog_main p), f, List.Nil, m,916 Obj.magic (Errors.OK (Callstate (p.AST.prog_main, f, List.Nil, m, 918 917 SStop))))))) 919 918
Note: See TracChangeset
for help on using the changeset viewer.