CristalCaveGem » LustreC

(********************************************************************)

(*                                                                  *)

(*  The LustreC compiler toolset   /  The LustreC Development Team  *)

(*  Copyright 2012 -    --   ONERA - CNRS - INPT - ISAE-SUPAERO     *)

(*                                                                  *)

(*  LustreC is free software, distributed WITHOUT ANY WARRANTY      *)

(*  under the terms of the GNU Lesser General Public License        *)

(*  version 2.1.                                                    *)

(*                                                                  *)

(********************************************************************)

open Machine_code_types

open Lustre_types

open Corelang

open Machine_code_common

open Misc_lustre_function

open Ada_printer

module Main = struct

      variable @param value the value to be assigned **)

      for more details on machine types.

      machine @param machine the current machine @param fmt the formater to

      print on @param instr the instruction to print **)

    let pp_instr = pp_machine_instr typed_submachines env in

      fprintf fmt "when %s =>@,%a" cond pp_block (List.map pp_instr instrs)

    (* Print a case *)

        (List.map pp_when hl)

    (* Print a if *)

    (* If neg is true the we must test for the negation of the condition. It

       first check that we don't have a negation and a else case, if so it

      let pp_cond =

        else pp_value env

        match instrs2 with

        | None ->

          fun fmt -> fprintf fmt ""

        | Some i2 ->

          fun fmt -> fprintf fmt "else@,%a" pp_block (List.map pp_instr i2)

        (List.map pp_instr instrs1)

    | MNoReset _ ->

      ()

    (* TODO: handle clear_reset *)

    | MClearReset ->

      ()

    (* reset *)

    | MSetReset i when List.mem_assoc i typed_submachines ->

      let substitution, submachine = get_instance i typed_submachines in

      let pp_package =

        pp_package_name_with_polymorphic substitution submachine

      in

      let args =

        if is_machine_statefull submachine then [ [ pp_state i ] ] else []

      in

      pp_call fmt (pp_package_access (pp_package, pp_reset_procedure_name), args)

    | MLocalAssign (ident, value) ->

      pp_assign env fmt ident value

    | MStateAssign (ident, value) ->

      pp_assign env fmt ident value

    | MStep ([ i0 ], i, vl) when is_builtin_fun i ->

      let value = mk_val (Fun (i, vl)) i0.var_type in

      pp_assign env fmt i0 value

    | MStep (il, i, vl) when List.mem_assoc i typed_submachines ->

      let substitution, submachine = get_instance i typed_submachines in

      let pp_package =

        pp_package_name_with_polymorphic substitution submachine

      in

      let input = List.map (fun x fmt -> pp_value env fmt x) vl in

      let output = List.map pp_var_name il in

      let args =

        (if is_machine_statefull submachine then [ [ pp_state i ] ] else [])

        @ (if input != [] then [ input ] else [])

        @ if output != [] then [ output ] else []

      in

      pp_call fmt (pp_package_access (pp_package, pp_step_procedure_name), args)

    | MBranch (_, []) ->

      assert false

    | MBranch (g, (c1, i1) :: tl) when c1 = tag_false || c1 = tag_true ->

      pp_if fmt (build_if g c1 i1 tl)

    | MBranch (g, hl) ->

      pp_case fmt (g, hl)

    | MComment s ->

      let lines = String.split_on_char '\n' s in

      fprintf fmt "%a" (Utils.fprintf_list ~sep:"" pp_oneline_comment) lines

    | _ ->

      assert false

      machine @param fmt the formater to print on @param machine the machine **)

      match instr.instr_desc with

      | MLocalAssign (ident, value) ->

        instr

      match m_spec_opt with

      | None ->

        [], []

            (build_pp_var_decl_local (Some (true, false, [], [])))

            (List.filter

               (fun x -> not (List.mem x.var_id guarantees))

               m_spec.mstep.step_locals),

          List.map transform_local_to_state_assign m_spec.mstep.step_instrs )

    in

    let pp_local_list =

      List.map (build_pp_var_decl_local None) m.mstep.step_locals

    in

    let pp_instr_list =

      List.map

        (pp_machine_instr typed_submachines env)

        (m.mstep.step_instrs @ spec_instrs)

    in

    let content =

      AdaProcedureContent

        ( ((if pp_local_ghost_list = [] then [] else [ pp_local_ghost_list ])

          @ if pp_local_list = [] then [] else [ pp_local_list ]),

          pp_instr_list )

    pp_procedure pp_step_procedure_name (build_pp_arg_step m) None fmt content

  (** Print the definition of the reset procedure from a machine.

      machine @param fmt the formater to print on @param machine the machine **)

      | var ->

        mkinstr (MStateAssign (var, mk_default_value var.var_type))

      match m_spec_opt with None -> env, m.mmemory | Some _ -> env, m.mmemory

    let assigns = List.map build_assign memory in

      List.map (pp_machine_instr typed_submachines env) (assigns @ m.minit)

    in

    pp_procedure pp_reset_procedure_name (build_pp_arg_reset m) None fmt

      (AdaProcedureContent ([], pp_instr_list))

      all typed instance. A typed submachine instance is (ident, type_machine)

      with ident the instance name and typed_machine is (substitution, machine)

      with machine the machine associated to the instance and substitution the

      instanciation of all its polymorphic types. @param fmt the formater to

      print on @param typed_submachines list of all typed machine instances of

      this machine @param m the machine **)

  let pp_file fmt (typed_submachines, ((opt_spec_machine, guarantees), machine))

      =

      if is_machine_statefull machine then

          (pp_reset_definition env typed_submachines)

          (machine, opt_spec_machine)

      else fprintf fmt ""

    let aux pkgs (id, _) =

      try

        if List.mem pkg pkgs then pkgs else pkg :: pkgs

    in

    let pp_content fmt =

        (machine, opt_spec_machine, guarantees)

    fprintf fmt "%a%t%a;@."

      packages

      pp_content

(* Local Variables: *)

(* compile-command: "make -C ../../.." *)

(* End: *)