CristalCaveGem » LustreC

module Main = struct

  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 pp_state_name_predicate suffix fmt =

    fprintf fmt "%t%s" pp_state_name suffix

  let pp_axiomatize_package_name fmt = fprintf fmt "axiomatize"

      @param fmt the formater to print on **)

    let new_state =

      AdaIn, pp_state_name_predicate suffixNew, pp_state_type, None

    in

    pp_predicate pp_init_name [ [ new_state ] ] true fmt None

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

    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

    pp_predicate pp_transition_name

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

      true fmt None

    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 instanciations =

      List.map

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

        substitutions

    in

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

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

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

  (** Compare two typed machines. **)

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

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

        List.map

          (fun x ->

            pp_var_decl

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

          m.mmemory

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

      List.map

        (build_pp_state_decl_from_subinstance AdaNoMode None)

        typed_instances

    in

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

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

    in

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

      let init fmt =

        pp_call fmt

          ( pp_access pp_axiomatize_package_name pp_init_name,

            [ [ pp_state_name ] ] )

      in

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

        (pp_procedure pp_reset_procedure_name (build_pp_arg_reset m) contract)

        AdaNoContent

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

        (fun fmt -> pp_record pp_state_type fmt var_lists)

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

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

        ghost_private

        let pp_var x fmt = pp_clean_ada_identifier fmt x in

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

            let invariant fmt =

              pp_call fmt

                ( pp_access pp_axiomatize_package_name pp_invariant_name,

                  [ [ pp_state_name ] ] )

            in

            [ invariant ], [ transition; invariant ]

          else [], []

        in

        let post_conditions =

          state_post_conditions @ guarantee_post_conditions

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

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

        ghost_public

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

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

      machines_to_import

      (pp_package (pp_package_name m) pp_generics false)

      pp_content