(* Time-stamp: <modified the 07/05/2013 (at 08:15) by Erwan Jahier> *) open Soc open Data open SocExecValue let dbg = (Verbose.get_flag "exec") let (assign_expr : ctx -> var_expr -> var_expr -> ctx) = fun ctx ve_in ve_out -> (* ve_out := ve_in (in ctx) *) Verbose.exe ~flag:dbg (fun () -> print_string ("Assigning "^(SocUtils.string_of_filter ve_out) ^ " to " ^(SocUtils.string_of_filter ve_in) ^ "\n"); flush stdout); { ctx with s = let v = SocExecValue.get_value ctx ve_in in sadd_partial ctx.s ve_out ctx.cpath v } (* [array_index i v] returns the var_expr v[i] *) let (array_index : int -> var -> var_expr) = fun i (vn,vt) -> let vt_elt = match vt with | Array(vt_elt,_) -> vt_elt | _ -> assert false in Index(Var(vn,vt),i,vt_elt) let rec (soc_step : Soc.step_method -> Soc.tbl -> Soc.t -> SocExecValue.ctx -> SocExecValue.ctx) = fun step soc_tbl soc ctx -> let soc_name,_,_ = soc.key in match step.impl with | Predef -> ( try SocExecEvalPredef.get soc.key ctx with Not_found -> (* Not a predef op *) print_string ( "*** internal error in "^soc_name^". Is it defined in SocExecEvalPredef?\n"); flush stdout; assert false ) | Gaol(vl,gaol) -> List.fold_left (do_gao step.lxm soc_tbl) ctx gaol | Boolred(i,j,k) -> ( (* XXX mettre ce code dans socPredef ? (ou socMetaopPredef)*) let inputs, outputs = soc.profile in let b_array = (List.hd inputs) in let cpt = ref 0 in for i = 0 to k-1 do let a_i = array_index i b_array in let v = SocExecValue.get_value ctx a_i in if v = B true then incr cpt; done; let res = B (!cpt >= i && !cpt <= j) in let res_var = fst (List.hd outputs) in let s = sadd ctx.s (res_var::ctx.cpath) res in { ctx with s = s } ) | Condact(node_sk, dft_cst) -> ( let clk = SocExecValue.get_value ctx (Var ("i0",Bool)) in let vel_in, vel_out = soc.profile in let vel_in = List.map (fun x -> Var x) (List.tl vel_in) in let vel_out = List.map (fun x -> Var x) vel_out in let node_soc = SocUtils.find step.lxm node_sk soc_tbl in let inst_name = match soc.instances with | [] -> let (proc_name,_,_) = node_soc.key in proc_name | [inst] -> fst inst | _ -> assert false in let path_saved = ctx.cpath in let ctx = { ctx with cpath=inst_name::ctx.cpath } in let ctx = if clk = B true then let node_step = match node_soc.step with [step] -> step | _ -> assert false in let ctx = { ctx with s = sadd ctx.s ("$first_step"::ctx.cpath) (B false) } in let ctx = do_step inst_name node_step ctx soc_tbl node_soc vel_in vel_out in { ctx with cpath=path_saved } else let first_step = Var ("$first_step",Bool) in let v = get_value ctx first_step in if v <> U then (* We are not on the first step of node_soc; hence we do nothing and the output will keep their previous value. *) { ctx with cpath=path_saved } else (* We are on the first step of node_soc; - we assign the output var to the default values *) let ctx = { ctx with cpath=path_saved } in List.fold_left2 assign_expr ctx dft_cst vel_out in ctx ) | Iterator(iter, node_sk, n) -> let node_soc = SocUtils.find step.lxm node_sk soc_tbl in let node_step = match node_soc.step with [step] -> step | _ -> assert false in let iter_inputs,iter_outputs = soc.profile in let rctx = ref ctx in let (proc_name,_,_) = node_soc.key in let inst_name = match soc.instances with | [] -> Array.make n proc_name | _ -> Array.of_list (List.map fst soc.instances) in for i = 0 to n-1 do rctx := { !rctx with cpath = inst_name.(i)::ctx.cpath }; let vel_in, vel_out = match iter with | "map" -> (List.map (array_index i) iter_inputs, List.map (array_index i) iter_outputs) | "fold" | "red" | "fill" | "fillred" -> let a_in = Var (List.hd iter_inputs) in ( a_in::(List.map (array_index i) (List.tl iter_inputs)), a_in::(List.map (array_index i) (List.tl iter_outputs))) | _ -> assert false (* should not occur *) in rctx := do_step inst_name.(i) node_step !rctx soc_tbl node_soc vel_in vel_out; rctx := { !rctx with cpath = List.tl !rctx.cpath }; done; if iter <> "map" then ( let a_in = Var (List.hd iter_inputs) in let a_out = Var (List.hd iter_outputs) in rctx := assign_expr !rctx a_in a_out); (* a_out=a_n *) !rctx; and (do_gao : Lxm.t -> Soc.tbl -> SocExecValue.ctx -> gao -> SocExecValue.ctx) = fun lxm soc_tbl ctx gao -> match gao with | Case(id, id_gao_l) -> ( try let id_val = get_enum id ctx in let gaol = List.assoc id_val id_gao_l in List.fold_left (do_gao lxm soc_tbl) ctx gaol with Not_found -> ctx ) | Call(vel_out, Assign, vel_in) -> ( try List.fold_left2 assign_expr ctx vel_in vel_out with _ -> assert false ) | Call(vel_out, Procedure sk, vel_in) -> ( let (proc_name,_,_) = sk in let path_saved = ctx.cpath in let ctx = { ctx with cpath = proc_name::ctx.cpath } in let soc = SocUtils.find lxm sk soc_tbl in let step = match soc.step with [step] -> step | _ -> assert false in let ctx = do_step proc_name step ctx soc_tbl soc vel_in vel_out in { ctx with cpath = path_saved } ) | Call(vel_out, Method((inst_name,sk),step_name), vel_in) -> ( let path_saved = ctx.cpath in let ctx = { ctx with cpath = inst_name::ctx.cpath } in let soc = SocUtils.find lxm sk soc_tbl in let step = try List.find (fun sm -> sm.name = step_name) soc.step with Not_found -> assert false in let ctx = do_step inst_name step ctx soc_tbl soc vel_in vel_out in let ctx = { s = sadd ctx.s ("$first_step"::ctx.cpath) (B false); cpath = path_saved } in ctx ) and (do_step : Ident.t -> step_method -> SocExecValue.ctx -> Soc.tbl -> Soc.t -> var_expr list -> var_expr list -> SocExecValue.ctx) = fun name step ctx soc_tbl soc vel_in vel_out -> let soc_in_vars, soc_out_vars = soc.profile in let step_in_vars = filter_params soc soc_in_vars step.idx_ins in let step_out_vars = filter_params soc soc_out_vars step.idx_outs in let new_s = substitute_args_and_params vel_in step_in_vars ctx in let ctx = soc_step step soc_tbl soc { ctx with s=new_s } in let s_out = substitute_params_and_args step_out_vars vel_out ctx in { ctx with s = s_out } (* get the step params from its soc params *) and (filter_params : Soc.t -> Soc.var list -> int list -> Soc.var list) = fun soc el il -> let local_nth i l = try List.nth l i with _ -> print_string ( "\n*** Cannot get the " ^ (string_of_int (i+1)) ^ "the element of a list of size " ^ (string_of_int (List.length l))^"\n"); flush stdout; assert false in let res = List.map (fun i -> local_nth i el) il in res (* exported *) let rec (expand_profile : bool -> Soc.var list -> Soc.var list) = fun enum_flag vl -> let res = List.flatten (List.map (expand_var enum_flag) vl) in (* fix point. now useless ? *) if List.length res = List.length vl then res else expand_profile enum_flag res and expand_var enum_flag var = match var with | (vn,(Bool| Int | Real)) -> [var] | (vn,Enum(n,l)) -> if enum_flag then [vn,Int] else [var] | (vn,Array(vt,i)) -> let res = ref [] in for k=i-1 downto 0 do res := (vn^"_"^(string_of_int k),vt) :: !res; done; (expand_profile enum_flag !res) | (vn,Struct(name,fl)) -> expand_profile enum_flag (List.map (fun (fn,t) -> vn^"_"^fn,t ) fl) | (vn,Extern id) -> assert false (* finish me! *) | (vn,Alpha _) -> assert false (* should not occur *) let (int_to_enum : Data.v -> Soc.ident list -> Data.v) = fun v el -> match v with | I i -> (try E (List.nth el i,i) with _ -> failwith ("Enum out of the range [0,"^(string_of_int (List.length el))^"]")) | _ -> assert false (* should not occur *) let rec (expand_subst: Data.subst -> Data.subst list) = fun s -> let rec aux acc (n,v) = match v with | U | I _ | F _ | B _ -> (n,v)::acc | E(_e,i) -> (n,I i)::acc | S fl -> let f (fn,fv) = n^"_"^fn, fv in let fl = List.map f fl in List.fold_left aux acc fl | A a -> let res = ref acc in for i=0 to (Array.length a)-1 do let n_i = n^"_"^(string_of_int i) in res := aux !res (n_i, a.(i)); done; !res in aux [] s (* A local shortcut to ease the profile def *) type sl = Data.subst list (* Reconstruct the flattenned data *) let (unexpand_profile : sl -> Soc.var list -> sl) = fun sl vl -> let rec (aux : sl -> sl -> Soc.var list -> sl * sl)= fun sl_done sl_todo vl -> (* Returns the (accumulated) result and the unused subst (which should be empty at the top-level call) *) match sl_todo, vl with | _,[] -> sl_done, sl_todo | s::sl, (_, (Bool| Int | Real))::vl -> aux (s::sl_done) sl vl | (id,v)::sl, (_,Enum(n,el))::vl -> let s = (id, int_to_enum v el) in aux (s::sl_done) sl vl | _, (vn, Array(vt,i))::vl -> ( let sl_todo_ref = ref sl_todo in let sl_done_ref = ref [] in let a_fake_value = I 42 in let res = Array.make i a_fake_value in for k=0 to i-1 do let (vk_l:Soc.var list) = [("fake_name",vt)] in let (sl_done_v, sl_todo_v) = aux !sl_done_ref !sl_todo_ref vk_l in sl_todo_ref:=sl_todo_v; sl_done_ref:=sl_done_v; Array.set res k (snd (List.hd !sl_done_ref)); done; let sl_done = (vn, A res)::sl_done in aux sl_done !sl_todo_ref vl ) | _, (vn,Struct(sn,fl))::vl -> let sl_todo, fl = List.fold_left aux_field (sl_todo,[]) fl in let sl_done = (vn, S fl)::sl_done in aux sl_done sl_todo vl | _, (vn,Extern id)::_ -> assert false (* finish me! *) | _, (vn,Alpha _ )::_ -> assert false (* should not occur *) | [],_::_ -> assert false (* should not occur *) and (aux_field : sl * (ident * Data.v) list -> ident * Data.t -> sl * (ident * Data.v) list ) = fun (sl_todo, fl) (fn, t) -> let new_sl_done, sl_todo = aux [] sl_todo [fn,t] in let (_,v) = List.hd new_sl_done in sl_todo, (fn,v)::fl in let res, remaining = aux [] sl vl in assert (remaining=[]); res (* [add_data_subst vtnl data_s s] add the data_s to s; *) let (add_data_subst : var list -> Data.subst list -> SocExecValue.substs -> SocExecValue.substs) = fun vntl_i s ctx_s -> let s = unexpand_profile s vntl_i in List.fold_left (fun acc (id,v) -> sadd acc [id] v) ctx_s s let (read_soc_input : var list -> Data.vntl -> out_channel -> substs -> substs) = fun vntl_i exp_vntl_i_str oc ctx_s -> let s:Data.subst list = Rif_base.read stdin (Some oc) exp_vntl_i_str in add_data_subst vntl_i s ctx_s let rec (loop_step : Lv6MainArgs.t -> Soc.tbl -> Soc.var list -> Data.vntl -> Data.vntl -> Soc.t -> SocExecValue.ctx -> int -> out_channel -> unit) = fun opt soc_tbl vntl_i exp_vntl_i_str exp_vntl_o_str soc ctx step_nb oc -> Rif_base.write oc ("\n#step " ^ (string_of_int step_nb)^"\n"); let ctx = { ctx with s = read_soc_input vntl_i exp_vntl_i_str oc ctx.s } in let step = match soc.step with [step] -> step | _ -> assert false in let ctx = soc_step step soc_tbl soc ctx in let ctx = { ctx with s = sadd ctx.s ("$first_step"::ctx.cpath) (B false)} in (* dump_substs ctx.s; *) let s = SocExecValue.filter_top_subst ctx.s in let s = List.flatten(List.map expand_subst s) in let f2s = SocUtils.my_string_of_float_precision opt.Lv6MainArgs.precision in Rif_base.write oc " #outs "; Rif_base.write_outputs oc f2s exp_vntl_o_str s; Rif_base.flush oc; Verbose.exe ~flag:dbg (fun () -> dump_substs ctx.s; flush stdout); loop_step opt soc_tbl vntl_i exp_vntl_i_str exp_vntl_o_str soc ctx (step_nb+1) oc let (f : Lv6MainArgs.t -> Soc.tbl -> Soc.key -> unit) = fun opt soc_tbl sk -> let soc = try SocMap.find sk soc_tbl with Not_found -> assert false in let ctx = SocExecValue.create_ctx soc_tbl soc in let vntl_of_profile = List.map (fun (x,t) -> x,SocUtils.string_of_type_ref t) in let exp_vntl_i = expand_profile true (fst soc.profile) in let exp_vntl_o = expand_profile true (snd soc.profile) in let exp_vntl_i_str = vntl_of_profile exp_vntl_i in let exp_vntl_o_str = vntl_of_profile exp_vntl_o in let oc = if opt.Lv6MainArgs.outfile = "" then stdout else let rif_file = try (Filename.chop_extension opt.Lv6MainArgs.outfile) ^ ".rif" with _ -> opt.Lv6MainArgs.outfile ^ ".rif" in open_out rif_file in Lv6util.dump_entete oc; Rif_base.write_interface oc exp_vntl_i_str exp_vntl_o_str None None; Rif_base.flush oc; try loop_step opt soc_tbl (fst soc.profile) exp_vntl_i_str exp_vntl_o_str soc ctx 1 oc with Rif_base.Bye -> close_out oc (**************************************************************************************) (* exported *) let rec (do_step : Soc.tbl -> Soc.t -> SocExecValue.ctx -> SocExecValue.ctx) = fun soc_tbl soc ctx -> let step = match soc.step with [step] -> step | _ -> assert false in let ctx = soc_step step soc_tbl soc ctx in let ctx = { ctx with s = sadd ctx.s ("$first_step"::ctx.cpath) (B false) } in ctx (* exported *) let rec (do_step_dbg : Soc.tbl -> Soc.t -> Event.ctx -> SocExecValue.ctx -> (SocExecValue.ctx -> Event.t) -> Event.t) = fun soc_tbl soc ectx ctx cont -> (* XXX un peu exegéré de mettre tout ?*) (* let (datal:Data.subst list) = SocExecValue.substs_to_data_subst ctx.s in *) let (datal:Data.subst list) = SocExecValue.filter_top_subst ctx.s in let (soc_name,_,_) = soc.key in let ectx = { ectx with Event.ctx_name = soc_name; Event.ctx_depth = ectx.Event.ctx_depth+1; Event.ctx_data = datal; Event.ctx_inputs = List.map fst (fst soc.profile); Event.ctx_outputs = List.map fst (snd soc.profile); } in let cont2 ctx = let lazy_si = (fun () -> let soc_step = match soc.step with [step] -> step | _ -> assert false in let lxm = soc_step.lxm in [{ Event.str = Lxm.str lxm; Event.file = Lxm.file lxm ; Event.line = Lxm.line lxm,Lxm.line lxm; Event.char = Lxm.cstart lxm, Lxm.cend lxm; (* Event.stack = if tl=[] then None else Some (to_src_info tl); *) Event.stack = None; (* XXX stub *) }]) in let enb = Event.incr_nb (); Event.get_nb () in { Event.step = ectx.Event.ctx_step; Event.nb = enb; Event.depth = ectx.Event.ctx_depth; Event.kind = Event.Node { Event.lang = "lustre"; Event.name = soc_name; Event.port = Event.Exit ("",Expr.True,lazy_si); Event.inputs = ectx.Event.ctx_inputs; Event.outputs = ectx.Event.ctx_outputs; }; Event.data = ectx.Event.ctx_data; Event.other = ""; Event.next = (fun () -> Event.event_nb := enb; cont ctx); Event.terminate = ectx.Event.ctx_terminate; } in { Event.step = ectx.Event.ctx_step; Event.nb = (Event.incr_nb (); Event.get_nb ()); Event.depth = ectx.Event.ctx_depth; Event.kind = Event.Node { Event.lang = "lustre"; Event.name = soc_name; Event.port = Event.Call; Event.inputs = ectx.Event.ctx_inputs; Event.outputs = ectx.Event.ctx_outputs; }; Event.data = ectx.Event.ctx_data; Event.other = ""; Event.next = (fun () -> let step = match soc.step with [step] -> step | _ -> assert false in let ctx = soc_step step soc_tbl soc ctx in let ctx = { ctx with s = sadd ctx.s ("$first_step"::ctx.cpath) (B false) } in cont2 ctx ); Event.terminate = ectx.Event.ctx_terminate; }