Changeset 2717 for extracted/cexec.ml
 Timestamp:
 Feb 23, 2013, 1:16:55 AM (7 years ago)
 File:

 1 edited
Legend:
 Unmodified
 Added
 Removed

extracted/cexec.ml
r2649 r2717 29 29 open Extralib 30 30 31 open BitVectorTrie 32 31 33 open CostLabel 32 34 … … 44 46 45 47 open Division 48 49 open Exp 46 50 47 51 open Arithmetic … … 805 809 Obj.magic 806 810 (IO.ret { Types.fst = (Events.eapp tr2 tr3); Types.snd = 807 (Csem.Callstate ( fd, vargs, (Csem.Kcall (Types.None, f,808 e1, k)), m)) })811 (Csem.Callstate (vf, fd, vargs, (Csem.Kcall (Types.None, 812 f, e1, k)), m)) }) 809 813  Types.Some lhs' > 810 814 Monad.m_bind2 (Monad.max_def IOMonad.iOMonad) … … 814 818 (IO.ret { Types.fst = 815 819 (Events.eapp tr1 (Events.eapp tr2 tr3)); Types.snd = 816 (Csem.Callstate ( fd, vargs, (Csem.Kcall ((Types.Some817 { Types.fst = locofs; Types.snd =820 (Csem.Callstate (vf, fd, vargs, (Csem.Kcall 821 ((Types.Some { Types.fst = locofs; Types.snd = 818 822 (Csyntax.typeof lhs') }), f, e1, k)), m)) }))))))) 819 823  Csyntax.Ssequence (s1, s2) > … … 1035 1039 IO.ret { Types.fst = (Events.echarge lbl); Types.snd = (Csem.State (f, 1036 1040 s', k, e1, m)) }) 1037  Csem.Callstate ( f0, vargs, k, m) >1041  Csem.Callstate (x, f0, vargs, k, m) > 1038 1042 (match f0 with 1039 1043  Csyntax.CL_Internal f > … … 1044 1048 Obj.magic 1045 1049 (Monad.m_bind0 (Monad.max_def IOMonad.iOMonad) 1046 (let x =1050 (let x0 = 1047 1051 IOMonad.err_to_io 1048 1052 (exec_bind_parameters e1 m1 f.Csyntax.fn_params vargs) 1049 1053 in 1050 Obj.magic x ) (fun m2 >1054 Obj.magic x0) (fun m2 > 1051 1055 Obj.magic 1052 1056 (IO.ret { Types.fst = Events.e0; Types.snd = (Csem.State (f, … … 1055 1059 Obj.magic 1056 1060 (Monad.m_bind0 (Monad.max_def IOMonad.iOMonad) 1057 (let x =1061 (let x0 = 1058 1062 IOMonad.err_to_io 1059 1063 (IO.check_eventval_list vargs 1060 1064 (Csyntax.typlist_of_typelist argtys)) 1061 1065 in 1062 Obj.magic x ) (fun evargs >1066 Obj.magic x0) (fun evargs > 1063 1067 Monad.m_bind0 (Monad.max_def IOMonad.iOMonad) 1064 1068 (Obj.magic … … 1143 1147 (Errors.opt_to_res (Errors.msg ErrorMessages.MainMissing) 1144 1148 (Globalenvs.find_funct_ptr ge0 b))) (fun f > 1145 Obj.magic (Errors.OK (Csem.Callstate (f, List.Nil, Csem.Kstop, 1146 m0))))))) 1149 Obj.magic (Errors.OK (Csem.Callstate ((Values.Vptr 1150 { Pointers.pblock = b; Pointers.poff = Pointers.zero_offset }), 1151 f, List.Nil, Csem.Kstop, m0))))))) 1147 1152 1148 1153 (** val is_final0 : Csem.state0 > Integers.int Types.option **) 1149 1154 let rec is_final0 = function 1150 1155  Csem.State (x, x0, x1, x2, x3) > Types.None 1151  Csem.Callstate (x, x0, x1, x2 ) > Types.None1156  Csem.Callstate (x, x0, x1, x2, x3) > Types.None 1152 1157  Csem.Returnstate (x, x0, x1) > Types.None 1153 1158  Csem.Finalstate r > Types.Some r … … 1156 1161 Csem.state0 > (Integers.int Types.sig0, __) Types.sum **) 1157 1162 let is_final_state st = 1158 Csem.state_rect_Type0 (fun f s k e1 m > Types.Inr __) (fun f l k m >1163 Csem.state_rect_Type0 (fun f s k e1 m > Types.Inr __) (fun vf f l k m > 1159 1164 Types.Inr __) (fun v k m > Types.Inr __) (fun r > Types.Inl r) st 1160 1165 1161 (** val exec_steps :1166 (** val exec_steps0 : 1162 1167 Nat.nat > Csem.genv0 > Csem.state0 > (IO.io_out, IO.io_in, 1163 1168 (Events.trace, Csem.state0) Types.prod) IOMonad.iO **) 1164 let rec exec_steps n ge0 s =1169 let rec exec_steps0 n ge0 s = 1165 1170 match is_final_state s with 1166 1171  Types.Inl x > IO.ret { Types.fst = Events.e0; Types.snd = s } … … 1173 1178 (Obj.magic (exec_step ge0 s)) (fun t s' > 1174 1179 Monad.m_bind2 (Monad.max_def IOMonad.iOMonad) 1175 (Obj.magic (exec_steps n' ge0 s')) (fun t' s'' >1180 (Obj.magic (exec_steps0 n' ge0 s')) (fun t' s'' > 1176 1181 Obj.magic 1177 1182 (IO.ret { Types.fst = (Events.eapp t t'); Types.snd = s'' })))))
Note: See TracChangeset
for help on using the changeset viewer.