CristalCaveGem » LustreC

val expr_annotations: (string list, ident * tag) Hashtbl.t

  (* let module Ads = Ada_backend_ads.Main in

   * let module Adb = Ada_backend_adb.Main in

   * let module Wrapper = Ada_backend_wrapper.Main in *)

        Format.eprintf "Ada Code generation error: %a@." Error.pp

        raise (Error.Error (Location.dummy, Error.Main_not_found))

  List.iter (write_file destname (_pp_filename "ads") Ada_backend_ads.pp_file) _machines;

  List.iter (write_file destname (_pp_filename "adb") Ada_backend_adb.pp_file) _machines;

    write_file destname pp_main_filename Ada_backend_wrapper.pp_main_adb

      (fun fmt _ -> Ada_backend_wrapper.pp_project_name (basename ^ "_exe") fmt)

      (Ada_backend_wrapper.pp_project_file filtered_machines basename)

  write_file destname Ada_backend_wrapper.pp_project_configuration_name

    (fun fmt _ -> Ada_backend_wrapper.pp_project_configuration_file fmt)

    (fun fmt _ -> Ada_backend_wrapper.pp_project_name (basename ^ "_lib") fmt)

    (Ada_backend_wrapper.pp_project_file filtered_machines basename)

(** Main function of the Ada backend. It calls all the subfunction creating all

    the file and fill them with Ada code representing the machines list given.

    @param basename name of the lustre file @param prog list of machines to

    translate **)

val translate_to_ada: string -> Machine_code_types.machine_t list -> unit

open Utils

(** Printing function for basic assignement [var := value].

    @param fmt the formater to print on @param var_name the name of the

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

let pp_assign env fmt var value =

  fprintf fmt "%a := %a" (pp_var env) var (pp_value env) value

(** Printing function for instruction. See {!type:Machine_code_types.instr_t}

    for more details on machine types.

    @param typed_submachines list of all typed machine instances of this

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

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

let rec pp_machine_instr typed_submachines env instr fmt =

  let pp_instr = pp_machine_instr typed_submachines env in

  (* Print args for a step call *)

  let pp_state i fmt = fprintf fmt "%t.%s" pp_state_name i in

  (* Print a when branch of a case *)

  let pp_when (cond, instrs) fmt =

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

  in

  (* Print a case *)

  let pp_case fmt (g, hl) =

    fprintf fmt "case %a is@,%aend case" (pp_value env) g pp_block

      (List.map pp_when hl)

  in

  (* 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

     inverses the two branch and remove the negation doing a recursive call. *)

  let pp_if fmt (neg, g, instrs1, instrs2) =

    let pp_cond =

      if neg then fun fmt x -> fprintf fmt "! (%a)" (pp_value env) x

      else pp_value env

    let pp_else =

      match instrs2 with

        fun fmt -> fprintf fmt ""

      | Some i2 ->

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

    in

    fprintf fmt "if %a then@,%a%tend if" pp_cond g pp_block

      (List.map pp_instr instrs1)

      pp_else

  in

  match get_instr_desc instr with

  (* no reset *)

  | 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

    let args =

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

    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

    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 []

    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" (pp_print_list ~pp_sep:pp_print_nothing pp_oneline_comment) lines

  | _ ->

    assert false

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

    @param typed_submachines list of all typed machine instances of this

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

let pp_step_definition env typed_submachines fmt (m, m_spec_opt, guarantees) =

  let transform_local_to_state_assign instr =

    match instr.instr_desc with

    | MLocalAssign (ident, value) ->

      { instr with instr_desc = MStateAssign (ident, value) }

    | _ ->

      instr

  in

  let pp_local_ghost_list, spec_instrs =

    match m_spec_opt with

    | None ->

      [], []

    | Some m_spec ->

      ( List.map

          (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 )

  in

  pp_procedure pp_step_procedure_name (build_pp_arg_step m) None fmt content

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

    @param typed_submachines list of all typed machine instances of this

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

let pp_reset_definition env typed_submachines fmt (m, m_spec_opt) =

  let build_assign = function

    | var ->

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

  in

  let env, memory =

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

  in

  let assigns = List.map build_assign memory in

  let pp_instr_list =

    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))

(** Print the package definition(ads) of a machine. It requires the list of

    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))

  =

  let env = List.map (fun x -> x.var_id, pp_state_name) machine.mmemory in

  let pp_reset fmt =

    if is_machine_statefull machine then

      fprintf fmt "%a;@,@,"

        (pp_reset_definition env typed_submachines)

        (machine, opt_spec_machine)

    else fprintf fmt ""

  in

  let aux pkgs (id, _) =

    try

      let pkg, _ = List.assoc id ada_supported_funs in

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

    with Not_found -> pkgs

  in

  let packages = List.map pp_str (List.fold_left aux [] machine.mcalls) in

  let pp_content fmt =

    fprintf fmt "%t%a" (*Define the reset procedure*) pp_reset

      (*Define the step procedure*)

      (pp_step_definition env typed_submachines)

      (machine, opt_spec_machine, guarantees)

  in

  fprintf fmt "%a%a;@."

    (* Include all the required packages*)

    (pp_print_list

       ~pp_sep:pp_print_semicolon

       ~pp_epilogue:(fun fmt () -> fprintf fmt ";@,@,")

       (pp_with AdaPrivate))

    packages

    (*Print package*)

    (pp_package (pp_package_name machine) [] true)

    pp_content

open Utils

open Machine_code_types

(** Print the package definition(ads) of a machine. It requires the list of

    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 **)

val pp_file: Format.formatter -> (ident * ((tag * Types.t) list * machine_t)) list

                                 * ((machine_t option * ident list) * machine_t) -> unit

open Utils

let rec init f = function i when i < 0 -> [] | i -> f i :: init f (i - 1)

(*should be replaced by the init of list from ocaml std lib*)

let suffixOld = "_old"

let suffixNew = "_new"

let pp_invariant_name fmt = fprintf fmt "inv"

let pp_transition_name fmt = fprintf fmt "transition"

let pp_init_name fmt = fprintf fmt "init"

let pp_state_name_predicate suffix fmt =

  fprintf fmt "%t%s" pp_state_name suffix

let pp_axiomatize_package_name fmt = fprintf fmt "axiomatize"

(** Print the expression function representing the transition predicate.

    @param fmt the formater to print on **)

let pp_init_predicate fmt () =

  let new_state =

    AdaIn, pp_state_name_predicate suffixNew, pp_state_type, None

  in

  pp_predicate pp_init_name [ [ new_state ] ] true fmt None

(** Print the expression function representing the transition predicate.

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

let pp_transition_predicate fmt (_, m) =

  let old_state =

    AdaIn, pp_state_name_predicate suffixOld, pp_state_type, None

  in

  let new_state =

    AdaIn, pp_state_name_predicate suffixNew, pp_state_type, None

  in

  let inputs = build_pp_var_decl_step_input AdaIn None m in

  let outputs = build_pp_var_decl_step_output AdaIn None m in

  pp_predicate pp_transition_name

    ([ [ old_state; new_state ] ] @ inputs @ outputs)

    true fmt None

let pp_invariant_predicate fmt () =

  pp_predicate pp_invariant_name

    [ [ build_pp_state_decl AdaIn None ] ]

    true fmt None

(** Print a new statement instantiating a generic package. @param fmt the

    formater to print on @param substitutions the instanciation substitution

    @param machine the machine to instanciate **)

let pp_new_package fmt (substitutions, machine) =

  let pp_name = pp_package_name machine in

  let pp_new_name = pp_package_name_with_polymorphic substitutions machine in

  let instanciations =

    List.map

      (fun (id, typ) -> pp_polymorphic_type id, fun fmt -> pp_type fmt typ)

      substitutions

  in

  pp_package_instanciation pp_new_name pp_name fmt instanciations

(** Remove duplicates from a list according to a given predicate. @param eq

    the predicate defining equality @param l the list to parse **)

let remove_duplicates eq l =

  let aux l x = if List.exists (eq x) l then l else x :: l in

  List.fold_left aux [] l

(** Compare two typed machines. **)

let eq_typed_machine (subst1, machine1) (subst2, machine2) =

  String.equal machine1.mname.node_id machine2.mname.node_id

  && List.for_all2 (fun a b -> pp_eq_type (snd a) (snd b)) subst1 subst2

(** Print the package declaration(ads) of a machine. It requires the list of

    all typed instance. A typed submachine is a (ident, typed_machine) with -

    ident: the name - typed_machine: a (substitution, machine) with - machine:

    the submachine struct - substitution the instanciation of all its

    polymorphic types. @param fmt the formater to print on @param

    typed_submachines list of all typed submachines of this machine @param m

    the machine **)

let pp_file fmt (typed_submachines, ((m_spec_opt, guarantees), m)) =

  let typed_machines = snd (List.split typed_submachines) in

  let typed_machines_set =

    remove_duplicates eq_typed_machine typed_machines

  in

  let machines_to_import =

    List.map pp_package_name (snd (List.split typed_machines_set))

  in

  let polymorphic_types = find_all_polymorphic_type m in

  let typed_machines_to_instanciate =

    List.filter (fun (l, _) -> l != []) typed_machines_set

  in

  let typed_instances =

    List.filter is_submachine_statefull typed_submachines

  in

  let memories =

    match m_spec_opt with

    | None ->

      []

    | Some m ->

        (fun x ->

           pp_var_decl

             (build_pp_var_decl AdaNoMode (Some (true, false, [], [])) x))

        m.mmemory

  in

  let ghost_private = memories in

  (* Commented since not used. Could be reinjected in the code let vars_spec =

     match m_spec_opt with | None -> [] | Some m_spec -> List.map

     (build_pp_var_decl AdaNoMode (Some (true, false, [], [])))

     (m_spec.mmemory) in *)

  let vars = List.map (build_pp_var_decl AdaNoMode None) m.mmemory in

  let states =

    List.map

      (build_pp_state_decl_from_subinstance AdaNoMode None)

      typed_instances

  in

  let var_lists =

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

    @ if vars = [] then [] else [ vars ]

  in

  let pp_ifstatefull fmt pp =

    if is_machine_statefull m then fprintf fmt "%t" pp else fprintf fmt ""

  in

  let pp_state_decl_and_reset fmt =

    let init fmt =

      pp_call fmt

        ( pp_access pp_axiomatize_package_name pp_init_name,

          [ [ pp_state_name ] ] )

    let contract = Some (false, false, [], [ init ]) in

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

      (*Declare the state type*)

      (pp_type_decl pp_state_type AdaPrivate)

      (*Declare the reset procedure*)

      (pp_procedure pp_reset_procedure_name (build_pp_arg_reset m) contract)

      AdaNoContent

  in

  let pp_private_section fmt =

    fprintf fmt "@,private@,@,%a%a%a"

      (*Instantiate the polymorphic type that need to be instantiated*)

      (pp_print_list

         ~pp_sep:pp_print_semicolon

         ~pp_epilogue:(fun fmt () -> fprintf fmt ";@,@,")

         pp_new_package)

      typed_machines_to_instanciate

      (*Define the state type*)

      pp_ifstatefull

      (fun fmt -> pp_record pp_state_type fmt var_lists)

      (pp_print_list

         ~pp_sep:pp_print_semicolon

         ~pp_prologue:(fun fmt () -> fprintf fmt ";@,@,")

         (fun fmt pp -> pp fmt))

      ghost_private

  in

  let pp_content fmt =

    let pp_contract_opt =

      let pp_var x fmt = pp_clean_ada_identifier fmt x in

      let guarantee_post_conditions = List.map pp_var guarantees in

      let state_pre_conditions, state_post_conditions =

        if is_machine_statefull m then

          let input = List.map pp_var_name m.mstep.step_inputs in

          let output = List.map pp_var_name m.mstep.step_outputs in

          let args =

            [ [ pp_old pp_state_name; pp_state_name ] ]

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

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

          in

          let transition fmt =

            pp_call fmt

              (pp_access pp_axiomatize_package_name pp_transition_name, args)

          in

          let invariant fmt =

            pp_call fmt

              ( pp_access pp_axiomatize_package_name pp_invariant_name,

                [ [ pp_state_name ] ] )

          in

          [ invariant ], [ transition; invariant ]

        else [], []

      let post_conditions =

        state_post_conditions @ guarantee_post_conditions

      let pre_conditions = state_pre_conditions in

      if post_conditions = [] && pre_conditions = [] then None

      else Some (false, false, pre_conditions, post_conditions)

    in

    let pp_guarantee name =

      pp_var_decl

        ( AdaNoMode,

          (fun fmt -> pp_clean_ada_identifier fmt name),

          pp_boolean_type,

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

    let ghost_public = List.map pp_guarantee guarantees in

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

      (pp_print_list

         ~pp_sep:pp_print_semicolon

         ~pp_epilogue:(fun fmt () -> fprintf fmt ";@,@,")

         (fun fmt pp -> pp fmt))

      ghost_public

      pp_ifstatefull pp_state_decl_and_reset

      (*Declare the step procedure*)

      (pp_procedure pp_step_procedure_name (build_pp_arg_step m)

         pp_contract_opt)

      AdaNoContent pp_ifstatefull

      (fun fmt -> fprintf fmt ";@,")

      (pp_package pp_axiomatize_package_name [] false)

      (fun fmt ->

         fprintf fmt

           "pragma Annotate (GNATProve, External_Axiomatization);@,\

            @,\

            %a;@,\

            %a;@,\

            %a"

           (*Declare the init predicate*)

           pp_init_predicate ()

           (*Declare the transition predicate*)

           pp_transition_predicate (m_spec_opt, m)

           (*Declare the invariant predicate*)

           pp_invariant_predicate ())

      (*Print the private section*)

      pp_private_section

  in

  let pp_poly_type id = pp_type_decl (pp_polymorphic_type id) AdaPrivate in

  let pp_generics = List.map pp_poly_type polymorphic_types in

  fprintf fmt "@[<v>%a%a;@]@."

    (* Include all the subinstance package*)

    (pp_print_list

       ~pp_sep:pp_print_semicolon

       ~pp_epilogue:(fun fmt () -> fprintf fmt ";@,@,")

       (pp_with AdaNoVisibility))

    machines_to_import

    (*Begin the package*)

    (pp_package (pp_package_name m) pp_generics false)

    pp_content

open Utils

open Machine_code_types

(** Print the package declaration(ads) of a machine. It requires the list of

    all typed instance. A typed submachine is a (ident, typed_machine) with -

    ident: the name - typed_machine: a (substitution, machine) with - machine:

    the submachine struct - substitution the instanciation of all its

    polymorphic types. @param fmt the formater to print on @param

    typed_submachines list of all typed submachines of this machine @param m

    the machine **)

val pp_file: Format.formatter -> (ident * ((tag * Types.t) list * machine_t)) list

                                 * ((machine_t option * ident list) * machine_t) -> unit

open Utils

  let open Types in

  let t = repr typ in

  if is_bool_type t then

    pp_boolean_type fmt

  else if is_int_type t then

  else if is_real_type t then

  else match t.tdesc with

    | Tunivar ->

      pp_polymorphic_type typ.tid fmt

    | Tbasic _ ->

      eprintf "Tbasic@.";

      assert false (*TODO*)

    | Tconst _ ->

      eprintf "Tconst@.";

      assert false (*TODO*)

    | Tclock _ ->

      eprintf "Tclock@.";

      assert false (*TODO*)

    | Tarrow _ ->

      eprintf "Tarrow@.";

      assert false (*TODO*)

    | Ttuple l ->

      eprintf "Ttuple %a @." (pp_print_list print_ty) l;

      assert false (*TODO*)

    | Tenum _ ->

      eprintf "Tenum@.";

      assert false (*TODO*)

    | Tstruct _ ->

      eprintf "Tstruct@.";

      assert false (*TODO*)

    | Tarray _ ->

      eprintf "Tarray@.";

      assert false (*TODO*)

    | Tstatic _ ->

      eprintf "Tstatic@.";

      assert false (*TODO*)

    | Tlink _ ->

      eprintf "Tlink@.";

      assert false (*TODO*)

    | Tvar ->

      eprintf "Tvar@.";

      assert false

let default_ada_cst t =

  let open Types in

  if is_bool_type t then

    Const_tag tag_false

  else if is_int_type t then

  else if is_real_type t then

  else

  let t = Types.repr typ in

  match t.Types.tdesc with

  | Types.Tbasic _ ->

  fprintf fmt "%t%a"

    (pp_package_name machine)

    (pp_print_list

       ~pp_prologue:(fun fmt () -> pp_print_string fmt "_")

       ~pp_sep:(fun fmt () -> pp_print_string fmt "_")

       pp_type)

val pp_type : formatter -> Types.t -> unit

  (int * Types.t) list -> machine_t -> printer

val mk_default_value : Types.t -> value_t

  string * ((int * Types.t) list * Machine_code_types.machine_t) ->

open Utils

let build_text_io_package_local typ =

  AdaLocalPackage

    ( (fun fmt -> fprintf fmt "%s_IO" typ),

      (fun fmt -> fprintf fmt "Ada.Text_IO.%s_IO" typ),

      [ ((fun fmt -> fprintf fmt "Num"), fun fmt -> fprintf fmt "%s" typ) ] )

(** Print the main file calling in a loop the step function of the main

    machine. @param fmt the formater to print on @param machine the main

    machine **)

let pp_main_adb fmt machine =

  let statefull = is_machine_statefull machine in

  let pp_package = pp_package_name_with_polymorphic [] machine in

  (* Dependances *)

  let text_io = "Ada.Text_IO" in

  (* Locals *)

  let locals =

    [

        build_text_io_package_local "Integer";

        build_text_io_package_local "Float";

      ];

    ]

    @ (if statefull then

       else [])

    @ (if machine.mstep.step_inputs != [] then

       else [])

    @

    if machine.mstep.step_outputs != [] then

      [ List.map (build_pp_var_decl_local None) machine.mstep.step_outputs ]

    else []

  in

  (* Stream instructions *)

  let get_type var = Types.repr var.var_type in

  let pp_read fmt var =

    if Types.is_bool_type (get_type var) then

      fprintf fmt "%t := Integer'Value(Ada.Text_IO.Get_Line) /= 0"

        (pp_var_name var)

    else

      fprintf fmt "%t := %a'Value(Ada.Text_IO.Get_Line)" (pp_var_name var)

        pp_var_type var

  in

  let pp_write fmt var =

    let t = get_type var in

    if Types.is_bool_type t then

      fprintf fmt

        "Ada.Text_IO.Put_Line(\"'%t': '\" & (if %t then \"1\" else \"0\") & \

         \"' \")"

        (pp_var_name var) (pp_var_name var)

    else if Types.is_int_type t then

        "Ada.Text_IO.Put(\"'%t': '\");@,\

         Integer_IO.Put(%t);@,\

         Ada.Text_IO.Put_Line(\"' \")" (pp_var_name var) (pp_var_name var)

    else if Types.is_real_type t then

      fprintf fmt

        "Ada.Text_IO.Put(\"'%t': '\");@,\

         Float_IO.Put(%t, Fore=>0, Aft=> 15, Exp => 0);@,\

         Ada.Text_IO.Put_Line(\"' \")" (pp_var_name var) (pp_var_name var)

    else

      assert false

      (* Could not be the top level inputs *)

  in

  (* Loop instructions *)

  let pp_loop fmt =

    let args =

      pp_state_name

      ::

      List.map pp_var_name

        (machine.mstep.step_inputs @ machine.mstep.step_outputs)

    fprintf fmt

      "while not Ada.Text_IO.End_Of_File loop@,\

      \  @[<v>%a;@,\

       %a;@,\

       %a;@]@,\

       end loop"

      (pp_print_list ~pp_sep:pp_print_semicolon pp_read)

      machine.mstep.step_inputs pp_call

      (pp_package_access (pp_package, pp_step_procedure_name), [ args ])

      (pp_print_list ~pp_sep:pp_print_semicolon pp_write)

      machine.mstep.step_outputs

  in

  (* Print the file *)

  let instrs =

    (if statefull then

            pp_call fmt

              ( pp_package_access (pp_package, pp_reset_procedure_name),

                [ [ pp_state_name ] ] ));

     else [])

    @ [ pp_loop ]

  in

  fprintf fmt "@[<v>%a;@,%a;@,@,%a;@]" (pp_with AdaPrivate) (pp_str text_io)

    (pp_with AdaPrivate) (pp_package_name machine)

    (pp_procedure pp_main_procedure_name [] None)

    (AdaProcedureContent (locals, instrs))

(** Print the name of the ada project configuration file. @param fmt the

    formater to print on @param main_machine the machine associated to the

    main node **)

let pp_project_configuration_name fmt basename = fprintf fmt "%s.adc" basename

(** Print the project configuration file. @param fmt the formater to print on

    **)

let pp_project_configuration_file fmt = fprintf fmt "pragma SPARK_Mode (On);"

(** Print the name of the ada project file. @param base_name name of the

    lustre file @param fmt the formater to print on **)

let pp_project_name basename fmt = fprintf fmt "%s.gpr" basename

let pp_for_single name arg fmt = fprintf fmt "for %s use \"%s\"" name arg

let pp_for name args fmt =

  fprintf fmt "for %s use (@[%a@])" name

    (pp_comma_list (fun fmt arg -> fprintf fmt "\"%s\"" arg))

    args

let pp_content fmt lines =

  fprintf fmt "  @[<v>%a%a@]"

    (pp_print_list ~pp_sep:pp_print_semicolon (fun fmt pp -> fprintf fmt "%t" pp))

    lines

    (if lines = [] then pp_print_nothing else pp_print_semicolon) ()

let pp_package name lines fmt =

  fprintf fmt "package %s is@,%a@,end %s" name pp_content lines name

(** Print the gpr project file, if there is a machine in machine_opt then an

    executable project is made else it is a library. @param fmt the formater

    to print on @param machine_opt the main machine option **)

let pp_project_file machines basename fmt machine_opt =

  let adbs =

    List.map (asprintf "%a" (pp_machine_filename "adb")) machines

    @

    match machine_opt with

    | None ->

      []

    | Some m ->

      [ asprintf "%a" pp_main_filename m ]

  in

  let project_name =

    basename ^ if machine_opt = None then "_lib" else "_exe"

  in