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 Format

open Machine_code_types

open Lustre_types

open Corelang

open Machine_code_common

open Ada_backend_common

(** Functions printing the .ads file **)

module Main =

struct

  (** Print the declaration of a state element of a subinstance of a machine.

     @param machine the machine

     @param fmt the formater to print on

     @param substitution correspondance between polymorphic type id and their instantiation

     @param ident the identifier of the subinstance

     @param submachine the submachine of the subinstance

  **)

  let pp_machine_subinstance_state_decl fmt (ident, (substitution, submachine)) =

    pp_node_state_decl substitution ident fmt submachine

  (** Print the state record for a machine.

     @param fmt the formater to print on

     @param var_list list of all state var

     @param typed_instances list typed instances

  **)

  let pp_state_record_definition fmt (var_list, typed_instances) =

    fprintf fmt "@,  @[<v>record@,  @[<v>%a%t%t%a%t@]@,end record@]"

      (Utils.fprintf_list ~sep:";@;" pp_machine_subinstance_state_decl)

      typed_instances

      (Utils.pp_final_char_if_non_empty ";" typed_instances)

      (fun fmt -> if var_list!=[] && typed_instances!= [] then fprintf fmt "@,@," else fprintf fmt "")

      (Utils.fprintf_list ~sep:";@;" (pp_machine_var_decl NoMode))

      var_list

      (Utils.pp_final_char_if_non_empty ";" var_list)

  (** Print the declaration for polymorphic types.

     @param fmt the formater to print on

     @param polymorphic_types all the types to print

  **)

  let pp_generic fmt polymorphic_types =

    let pp_polymorphic_types =

      List.map (fun id fmt -> pp_polymorphic_type fmt id) polymorphic_types in

    if polymorphic_types != [] then

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

          (Utils.fprintf_list ~sep:";@," pp_private_type_decl)

          pp_polymorphic_types

    else

      fprintf fmt ""

  (** Print instanciation of a generic type in a new statement.

     @param fmt the formater to print on

     @param id id of the polymorphic type

     @param typ the new type

  **)

  let pp_generic_instanciation fmt (id, typ) =

    fprintf fmt "%a => %a" pp_polymorphic_type id pp_type typ

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

    fprintf fmt "package %a is new %a @[<v>(%a)@]"

      (pp_package_name_with_polymorphic substitutions) machine

      pp_package_name machine

      (Utils.fprintf_list ~sep:",@," pp_generic_instanciation) substitutions

  let pp_eexpr fmt eexpr = fprintf fmt "true"

  (** Print a precondition in aspect

     @param fmt the formater to print on

     @param expr the expession to print as pre

  **)

  let pp_pre fmt expr =

    fprintf fmt "Pre => %a"

      pp_eexpr expr

  (** Print a postcondition in aspect

     @param fmt the formater to print on

     @param expr the expession to print as pre

  **)

  let pp_post fmt expr =

    fprintf fmt "Post => %a"

      pp_eexpr expr

  (** Print the declaration of a procedure with a contract

     @param pp_prototype the prototype printer

     @param fmt the formater to print on

     @param contract the contract for the function to declare

  **)

  let pp_procedure_prototype_contract pp_prototype fmt opt_contract =

    match opt_contract with

      | None -> pp_prototype fmt

      | Some (NodeSpec ident) -> pp_prototype fmt (*TODO*)

      | Some (Contract contract) ->

          fprintf fmt "@[<v 2>%t with@,Global => null;@,%a%t%a@]"

            pp_prototype

            (Utils.fprintf_list ~sep:",@," pp_pre) contract.assume

            (Utils.pp_final_char_if_non_empty ",@," contract.assume)

            (Utils.fprintf_list ~sep:",@," pp_post) contract.guarantees

  (** Print the prototype with a contract of the reset procedure from a machine.

     @param fmt the formater to print on

     @param machine the machine

  **)

  let pp_step_prototype_contract fmt m =

    pp_procedure_prototype_contract

      (pp_step_prototype m)

      fmt

      m.mspec

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

    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 = 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 pp_record fmt =

      pp_state_record_definition fmt (m.mmemory, typed_instances) in

    let pp_state_decl_and_reset fmt = fprintf fmt "%a;@,@,%t;@,@,"

      (*Declare the state type*)

      pp_private_limited_type_decl pp_state_type

      (*Declare the reset procedure*)

      (pp_reset_prototype m)

    in

    let pp_private_section fmt = fprintf fmt "@,private@,@,%a%t%a;@,"

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

      (Utils.fprintf_list ~sep:";@," pp_new_package) typed_machines_to_instanciate

      (Utils.pp_final_char_if_non_empty ";@,@," typed_machines_to_instanciate)

      (*Define the state type*)

      pp_type_decl (pp_state_type, pp_record)

    in

    let pp_ifstatefull fmt pp =

      if is_machine_statefull m then

        fprintf fmt "%t" pp

      else

        fprintf fmt ""

    in

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

      (* Include all the subinstance package*)

      (Utils.fprintf_list ~sep:";@," pp_with_machine) machines_to_import

      (Utils.pp_final_char_if_non_empty ";@,@," machines_to_import)

      pp_generic polymorphic_types

      (*Begin the package*)

      (pp_begin_package false) m

      pp_ifstatefull pp_state_decl_and_reset

      (*Declare the step procedure*)

      pp_step_prototype_contract m

      (*Print the private section*)

      pp_ifstatefull pp_private_section

      (*End the package*)

      pp_end_package m

end