socExec.ml

(* Time-stamp: <modified the 06/06/2013 (at 10:29) 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 
          let ctx = SocExecEvalPredef.get soc.key ctx in
          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 = do_step inst_name node_step ctx soc_tbl node_soc vel_in vel_out in
            let ctx = { ctx with s = sadd ctx.s ("$first_step"::ctx.cpath) (B false) } 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
          let ctx = List.fold_left (do_gao lxm soc_tbl) ctx gaol in
          ctx
        with Not_found -> ctx
      )
      | Call(vel_out, Assign, vel_in) -> (
        let ctx = 
          try List.fold_left2 assign_expr ctx vel_in vel_out
          with _ -> assert false
        in
        ctx
      )
      | 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) ->
    print_string "Extern node not yet supported, sorry\n"; flush stdout;
    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
    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;
    }