CristalCaveGem » LustreC

open Format

let fprintf_list = Utils.fprintf_list

  | MStep ([ _ ], i, vl) -> (

      try

        let name = (get_node_def i m).node_id in

        match name, vl with

        | "_arrow", [ v1; v2 ] -> (

            match v1.value_desc, v2.value_desc with

            | Cst c1, Cst c2 ->

                if

                  c1 = Corelang.const_of_bool true

                  && c2 = Corelang.const_of_bool false

                then true

                else assert false

            (* only handle true -> false *)

            | _ -> assert false)

        | _ -> false

      with Not_found ->

        false

        (* Not declared (should have been detected now, or

           imported node) *))

      match eq.eq_rhs.expr_desc with

      | Expr_appl (_, _, reset) -> (

          match reset with None -> false | Some _ -> true)

      | Expr_arrow _ -> true

      | _ ->

          Format.eprintf "reseting expr %a@.@?" Printers.pp_expr eq.eq_rhs;

          assert false)

  | None -> assert false

(* should have been assigned to an original lustre equation *)

  | MLocalAssign (lhs, _) | MStateAssign (lhs, _) -> pp_var_name fmt lhs

  | MBranch _ ->

      incr branch_cpt;

      fprintf fmt "branch_%i" !branch_cpt

      print_protect fmt (fun fmt ->

          fprintf fmt "%a_%s" (fprintf_list ~sep:"_" pp_var_name) outs id)

  | _ -> ()

(* No name *)

      let all_defined_vars, common_def_vars, read_vars =

        branch_instr_vars m i

      in

      ( ISet.union accu_all_def all_defined_vars,

        ISet.union accu_def common_def_vars,

        VSet.union accu_read read_vars ))

    (ISet.empty, ISet.empty, VSet.empty)

    il

  | MLocalAssign (var, expr) | MStateAssign (var, expr) ->

      ISet.singleton var.var_id, ISet.singleton var.var_id, get_expr_vars expr

  | MStep (vars, f, args) ->

      let is_stateful = List.mem_assoc f m.minstances in

      let lhs = ISet.of_list (List.map (fun v -> v.var_id) vars) in

      let args_vars =

        List.fold_left

          (fun accu v -> VSet.union accu (get_expr_vars v))

          VSet.empty args

      in

      ( lhs,

        lhs,

        if is_stateful && is_resetable_fun i.lustre_eq then

          let reset_var =

            let loc = Location.dummy_loc in

            Corelang.mkvar_decl loc

              ( reset_name f,

                Corelang.mktyp loc Tydec_bool,

                Corelang.mkclock loc Ckdec_any,

                false,

                None,

                None )

          in

          VSet.add reset_var args_vars

        else args_vars )

  | MBranch (g, (_, hd_il) :: tl) ->

      (* We focus on variables defined in all branches *)

      let read_guard = get_expr_vars g in

      (* Bootstrapping with first item *)

      let all_def_vars_hd, def_vars_hd, read_vars_hd =

        branch_block_vars m hd_il

      in

      let all_def_vars, def_vars, read_vars =

        List.fold_left

          (fun (all_def_vars, def_vars, read_vars) (_, il) ->

            (* We accumulate reads but intersect writes *)

            let all_writes_il, writes_il, reads_il = branch_block_vars m il in

            ( ISet.union all_def_vars all_writes_il,

              ISet.inter def_vars writes_il,

              VSet.union read_vars reads_il ))

          (all_def_vars_hd, def_vars_hd, read_vars_hd)

          tl

      in

      (* all_def_vars correspond to variables written or defined in one

         of the branch. It may happen that a variable is defined in one

         but not in the other, because of reset for example.

         def_vars are variables defined in all branches. *)

      all_def_vars, def_vars, VSet.union read_guard read_vars

  | MBranch _ ->

      assert false (* branch instruction should admit at least one case *)

  | MSetReset ni | MNoReset ni ->

      let write = ISet.singleton (reset_name ni) in

      write, write, VSet.empty

  | MSpec _ | MComment _ -> assert false

(* not  available for EMF output *)

    List.fold_right

      (fun i (il, branches) ->

        match Corelang.get_instr_desc i with

        | MBranch _ -> il, i :: branches

        | _ -> i :: il, branches)

      instrs ([], [])

    | MBranch (g1, _), MBranch (g2, _) -> compare g1 g2

  instrs @ join_guards_list sorted_branches

    | MLocalAssign (lhs, expr) -> (

        match expr.value_desc with

            (*

           Thanks to normalization, vl shall only contain constant or

           local/state vars but not calls to other functions *)

            fprintf fmt "\"kind\": \"operator\",@ ";

            fprintf fmt "\"lhs\": \"%a\",@ " pp_var_name lhs;

            fprintf fmt "\"name\": \"%s\",@ \"args\": [@[%a@]]" fun_id

              (pp_emf_cst_or_var_list m) vl

        | Array _ | Access _ | Power _ | Cst _ | Var _ ->

            fprintf fmt

              "\"kind\": \"local_assign\",@ \"lhs\": \"%a\",@ \"rhs\": %a"

              pp_var_name lhs (pp_emf_cst_or_var m) expr

            (* TODO: handle reset flag *)

            assert false)

    | MStateAssign (lhs, expr)

    (* a Pre construct Shall only be defined by a

       variable or a constant, no function anymore! *) ->

        fprintf fmt "\"kind\": \"pre\",@ \"lhs\": \"%a\",@ \"rhs\": %a"

          pp_var_name lhs (pp_emf_cst_or_var m) expr

    | MSetReset id ->

        fprintf fmt "\"kind\": \"reset\",@ \"lhs\": \"%s\",@ \"rhs\": \"true\""

          (reset_name id)

    | MNoReset id ->

        fprintf fmt "\"kind\": \"reset\",@ \"lhs\": \"%s\",@ \"rhs\": \"false\""

          (reset_name id)

    | MBranch (g, hl) ->

        let inputs =

          VSet.filter (fun v -> not (ISet.mem v.var_id all_outputs)) inputs

        in

        (* Format.eprintf "Filtering in: %a@.@." *)

        (* 	pp_emf_vars_decl *)

        (* 	(VSet.elements inputs) *)

        (* ; *)

        fprintf fmt "\"kind\": \"branch\",@ ";

        fprintf fmt "\"guard\": %a,@ " (pp_emf_cst_or_var m) g;

        (* it has to be a variable or a constant *)

        fprintf fmt "\"outputs\": [%a],@ "

          (fprintf_list ~sep:", " pp_var_string)

          (ISet.elements outputs);

        fprintf fmt "\"inputs\": [%a],@ " pp_emf_vars_decl

          (*

           (let guard_inputs = get_expr_vars g in

           VSet.elements (VSet.diff inputs guard_inputs)) -- previous version to

           remove guard's variable from inputs *)

          (VSet.elements inputs);

        fprintf fmt "@[<v 2>\"branches\": {@ @[<v 0>%a@]@]@ }"

          (fprintf_list ~sep:",@ " (fun fmt (tag, instrs_tag) ->

               let branch_all_lhs, _, branch_inputs =

                 branch_block_vars m instrs_tag

               in

               let branch_inputs =

                 VSet.filter

                   (fun v -> not (ISet.mem v.var_id branch_all_lhs))

                   branch_inputs

               in

               fprintf fmt "@[<v 2>\"%a\": {@ " print_protect (fun fmt ->

                   Format.pp_print_string fmt tag);

               fprintf fmt "\"guard_value\": \"%a\",@ " pp_tag_id tag;

               fprintf fmt "\"inputs\": [%a],@ " pp_emf_vars_decl

                 (VSet.elements branch_inputs);

               fprintf fmt "@[<v 2>\"instrs\": {@ ";

               (pp_emf_instrs m) fmt instrs_tag;

               fprintf fmt "@]@ }";

               fprintf fmt "@]@ }"))

          hl

    | MStep ([ var ], f, _) when is_arrow_fun m i ->

        (* Arrow case *)

        fprintf fmt

          "\"kind\": \"arrow\",@ \"name\": \"%s\",@ \"lhs\": \"%a\",@ \"rhs\": \

           \"%s\""

          f pp_var_name var (reset_name f)

    | MStep (outputs, f, inputs) when not (is_imported_node f m) ->

        let node_f = get_node_def f m in

        let is_stateful = List.mem_assoc f m.minstances in

        fprintf fmt "\"kind\": \"%s\",@ \"name\": \"%a\",@ \"id\": \"%s\",@ "

          (if is_stateful then "statefulcall" else "statelesscall")

          print_protect

          (fun fmt -> pp_print_string fmt node_f.node_id)

          f;

        fprintf fmt "\"lhs\": [@[%a@]],@ \"args\": [@[%a@]]"

          (fprintf_list ~sep:",@ " (fun fmt v ->

               fprintf fmt "\"%a\"" pp_var_name v))

          outputs (pp_emf_cst_or_var_list m) inputs;

        if is_stateful then

          fprintf fmt ",@ \"reset\": { \"name\": \"%s\", \"resetable\": \"%b\"}"

            (reset_name f)

            (is_resetable_fun i.lustre_eq)

        else fprintf fmt "@ "

    | MStep (outputs, f, inputs) ->

        (* This is an imported node *)

        EMF_library_calls.pp_call fmt m f outputs inputs

    | MSpec _ | MComment _ ->

        Format.eprintf "unhandled comment in EMF@.@?";

        assert false

    (* not  available for EMF output *)

  fprintf fmt "@[ @[<v 2>\"%a\": {@ " get_instr_id i;

  fprintf fmt "%a" pp_content i;

  fprintf fmt "@]@]@ }"

and pp_emf_instrs m fmt instrs =

  fprintf_list ~sep:",@ " (pp_emf_instr m) fmt instrs

    fprintf fmt "\"ann%i\": { @[<hov 0>\"key\": [%a],@ \"eexpr\": %a@] }" !cpt

      (fprintf_list ~sep:"," (fun fmt s -> fprintf fmt "\"%s\"" s))

      key pp_emf_eexpr ee

  fprintf fmt "\"mode_id\": \"%s\",@ " m.mode_id;

  fprintf fmt "\"ensure\": [%a],@ " pp_emf_eexprs m.ensure;

  fprintf fmt "\"require\": [%a]@ " pp_emf_eexprs m.require;

  fprintf fmt "\"contract\": \"%s\",@ " i.import_nodeid;

  fprintf fmt "\"inputs\": [%a],@ " pp_emf_expr i.inputs;

  fprintf fmt "\"outputs\": [%a],@ " pp_emf_expr i.outputs;

  fprintf fmt "\"assume\": [%a],@ " pp_emf_eexprs spec.assume;

  fprintf fmt "\"guarantees\": [%a],@ " pp_emf_eexprs spec.guarantees;

  fprintf fmt "\"modes\": [%a]@ " pp_emf_spec_modes spec.modes;

   *   pp_emf_spec_imports spec.imports; *)

let pp_emf_annots cpt fmt annots =

  fprintf_list ~sep:",@ " (pp_emf_annot cpt) fmt annots.annots

let pp_emf_annots_list cpt fmt annots_list =

  fprintf_list ~sep:",@ " (pp_emf_annots cpt) fmt annots_list

  let instrs =

    (*merge_branches*)

    m.mstep.step_instrs

  in

    fprintf fmt "@[<v 2>\"%a\": {@ " print_protect (fun fmt ->

        pp_print_string fmt m.mname.node_id);

    | Some (Contract _) -> fprintf fmt "\"contract\": \"true\",@ "

    | _ -> ());

    fprintf fmt "\"kind\": %t,@ " (fun fmt ->

        if not (snd (get_stateless_status m)) then fprintf fmt "\"stateful\""

        else fprintf fmt "\"stateless\"");

    fprintf fmt "\"inputs\": [%a],@ " pp_emf_vars_decl m.mstep.step_inputs;

    fprintf fmt "\"outputs\": [%a],@ " pp_emf_vars_decl m.mstep.step_outputs;

    fprintf fmt "\"locals\": [%a],@ " pp_emf_vars_decl m.mstep.step_locals;

    fprintf fmt "\"mems\": [%a],@ " pp_emf_vars_decl m.mmemory;

    fprintf fmt "\"instrs\": {@[<v 0> %a@]@ },@ " (pp_emf_instrs m) instrs;

    | None -> ()

    | Some (Contract c) ->

        assert (c.locals = [] && c.consts = [] && c.stmts = [] && c.imports = []);

        fprintf fmt "\"spec\": %a,@ " pp_emf_spec c

    | Some (NodeSpec id) -> fprintf fmt "\"contract\": \"%s\",@ " id);

    fprintf fmt "\"annots\": {@[<v 0> %a@]@ }"

      (pp_emf_annots_list (ref 0))

      m.mannot;

  with Unhandled msg ->

    fprintf fmt "@[<v 2>\"%a\": {@ " print_protect (fun fmt ->

        pp_print_string fmt ind.nodei_id);

    fprintf fmt "\"inputs\": [%a],@ " pp_emf_vars_decl ind.nodei_inputs;

    fprintf fmt "\"outputs\": [%a],@ " pp_emf_vars_decl ind.nodei_outputs;

    (match ind.nodei_spec with

    | None -> fprintf fmt "@ "

    | Some (Contract _) -> assert false (* should have been processed *)

    | Some (NodeSpec id) -> fprintf fmt ",@ \"coco_contract\": %s" id);

  with Unhandled msg ->

    [

      "compiler-name", Filename.basename Sys.executable_name;

      "compiler-version", Version.number;

      "command", String.concat " " (Array.to_list Sys.argv);

      "source_file", basename;

    ];

    (pp_emf_list pp_emf_typedef)

    (Corelang.get_typedefs prog);

    (pp_emf_list pp_emf_top_const)

    (Corelang.get_consts prog);

  (* Previous alternative: mapping normalized lustre to EMF: