CristalCaveGem » LustreC

(* Multiple export channels for switched systems: - lustre - matlab - text *)

open Lustre_types

open Machine_code_types

open Seal_utils

let verbose = true

let process_sw vars f_e sw =

  let process_branch g_opt up =

    let el = List.map (fun (v, e) -> v, f_e e) up in

    (* Sorting list of elements, according to vars, safety check to ensure that

       no variable is forgotten. *)

    let el, forgotten =

      List.fold_right

        (fun v (res, remaining) ->

          let vid = v.var_id in

          if List.mem_assoc vid remaining then

            List.assoc vid remaining :: res, List.remove_assoc vid remaining

          else (

            Format.eprintf

              "Looking for variable %s in remaining expressions: [%a]@." vid

              (Utils.fprintf_list ~sep:";@ " (fun fmt (id, e) ->

                   Format.fprintf fmt "(%s -> %a)" id Printers.pp_expr e))

              remaining;

            assert false (* Missing variable v in list *)))

        vars ([], el)

    in

    assert (forgotten = []);

    let loc = (List.hd el).expr_loc in

    let new_e = Corelang.mkexpr loc (Expr_tuple el) in

    match g_opt with

    | None ->

      None, new_e, loc

    | Some g ->

      let g = f_e g in

      let ee = Corelang.mkeexpr loc g in

      let new_e =

        if verbose then

          {

            new_e with

            expr_annot =

              Some { annots = [ [ "seal"; "guards" ], ee ]; annot_loc = loc };

          }

        else new_e

      in

      Some g, new_e, loc

  in

  let rec process_sw f_e sw =

    match sw with

    | [] ->

      assert false

    | [ (g_opt, up) ] ->

      (* last case, no need to guard it *)

      let _, up_e, _ = process_branch g_opt up in

      up_e

    | (g_opt, up) :: tl -> (

      let g_opt, up_e, loc = process_branch g_opt up in

      match g_opt with

      | None ->

        Format.eprintf "SEAL issue: process_sw with %a"

          (pp_sys Printers.pp_expr) sw;

        assert false (* How could this happen anyway ? *)

      | Some g ->

        let tl_e = process_sw f_e tl in

        Corelang.mkexpr loc (Expr_ite (g, up_e, tl_e)))

  in

  process_sw f_e sw

let sw_to_lustre m sw_init sw_step init_out update_out =

  let orig_nd = m.mname in

  let copy_nd = orig_nd (*Corelang.copy_node orig_nd *) in

  let vl =

    (* vl are memories *)

    match sw_init with

    | [] ->

      [] (* the system is stateless. Returning an empty list shall do the job *)

    | (_, up) :: _ ->

      List.map (fun (v, _) -> v) up

  in

  let loc = Location.dummy_loc in

  let mem_eq =

    if m.mmemory = [] then []

    else

      let e_init = process_sw m.mmemory (fun x -> x) sw_init in

      let e_step = process_sw m.mmemory (Corelang.add_pre_expr vl) sw_step in

      [

        Eq

          {

            eq_loc = loc;

            eq_lhs = vl;

            eq_rhs = Corelang.mkexpr loc (Expr_arrow (e_init, e_step));

          };

      ]

  in

  let output_eq =

    let e_init_out = process_sw copy_nd.node_outputs (fun x -> x) init_out in

    let e_update_out =

      process_sw copy_nd.node_outputs (Corelang.add_pre_expr vl) update_out

    in

    [

      Eq

        {

          eq_loc = loc;

          eq_lhs = List.map (fun v -> v.var_id) copy_nd.node_outputs;

          eq_rhs = Corelang.mkexpr loc (Expr_arrow (e_init_out, e_update_out));

        };

    ]

  in

  let new_nd =

    {

      copy_nd with

      node_id = copy_nd.node_id ^ "_seal";

      node_locals = m.mmemory;

      node_stmts = mem_eq @ output_eq;

    }

  in

  new_nd, orig_nd

let funsw_to_lustre m update_out =

  let orig_nd = m.mname in

  let copy_nd = orig_nd (*Corelang.copy_node orig_nd *) in

  let output_eq =

    let e_update_out =

      process_sw copy_nd.node_outputs (fun x -> x) update_out

    in

    [

      Eq

        {

          eq_loc = Location.dummy_loc;

          eq_lhs = List.map (fun v -> v.var_id) copy_nd.node_outputs;

          eq_rhs = e_update_out;

        };

    ]

  in

  let new_nd =

    {

      copy_nd with

      node_id = copy_nd.node_id ^ "_seal";

      node_locals = [];

      node_stmts = output_eq;

    }

  in

  new_nd, orig_nd

let to_lustre basename prog new_node orig_node =

  let loc = Location.dummy_loc in

  Global.type_env := Typing.type_node !Global.type_env new_node loc;

  Global.clock_env := Clock_calculus.clock_node !Global.clock_env loc new_node;

  (* Format.eprintf "%a@." Printers.pp_node new_node; *)

  (* Main output *)

  let output_file = !Options.dest_dir ^ "/" ^ basename ^ "_seal.lus" in

  let new_top =

    Corelang.mktop_decl Location.dummy_loc output_file false (Node new_node)

  in

  let out = open_out output_file in

  let fmt = Format.formatter_of_out_channel out in

  Format.fprintf fmt "%a@." Printers.pp_prog [ new_top ];

  (* Verif output *)

  let output_file_verif =

    !Options.dest_dir ^ "/" ^ basename ^ "_seal_verif.lus"

  in

  let out_verif = open_out output_file_verif in

  let fmt_verif = Format.formatter_of_out_channel out_verif in

  let check_nd = Lustre_utils.check_eq new_node orig_node in

  let check_top =

    Corelang.mktop_decl Location.dummy_loc output_file_verif false

      (Node check_nd)

  in

  Format.fprintf fmt_verif "%a@." Printers.pp_prog

    (prog @ [ new_top; check_top ])

let node_to_lustre basename prog m sw_init sw_step init_out update_out =

  let new_node, orig_nd = sw_to_lustre m sw_init sw_step init_out update_out in

  to_lustre basename prog new_node orig_nd

let fun_to_lustre basename prog m update_out =

  let new_node, orig_nd = funsw_to_lustre m update_out in

  to_lustre basename prog new_node orig_nd