CristalCaveGem » LustreC

(* ----------------------------------------------------------------------------

 * SchedMCore - A MultiCore Scheduling Framework

 * Copyright (C) 2009-2013, ONERA, Toulouse, FRANCE - LIFL, Lille, FRANCE

 * Copyright (C) 2012-2013, INPT, Toulouse, FRANCE

 *

 * This file is part of Prelude

 *

 * Prelude is free software; you can redistribute it and/or

 * modify it under the terms of the GNU Lesser General Public License

 * as published by the Free Software Foundation ; either version 2 of

 * the License, or (at your option) any later version.

 *

 * Prelude is distributed in the hope that it will be useful, but

 * WITHOUT ANY WARRANTY ; without even the implied warranty of

 * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the GNU

 * Lesser General Public License for more details.

 *

 * You should have received a copy of the GNU Lesser General Public

 * License along with this program ; if not, write to the Free Software

 * Foundation, Inc., 59 Temple Place, Suite 330, Boston, MA 02111-1307

 * USA

 *---------------------------------------------------------------------------- *)

(* This module is used for the lustre to C compiler *)

open Format

open LustreSpec

open Machine_code

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

(*                         Translation function                                             *)

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

let makefile_opt print basename dependencies makefile_fmt machines =

  (* If a main node is identified, generate a main target for it *)

  match !Options.main_node with

  | "" ->  ()

  | main_node -> (

    match Machine_code.get_machine_opt main_node machines with

    | None -> Format.eprintf "Unable to find a main node named %s@.@?" main_node; ()

    | Some _ -> print basename !Options.main_node dependencies makefile_fmt

  )

module type MODIFIER = sig

    module HdrMod : C_backend_header.MODIFIERS_HDR

    module SrcMod : C_backend_src.MODIFIERS_SRC

    module MainMod : C_backend_main.MODIFIERS_MAINSRC

    module MakefileMod : C_backend_makefile.MODIFIERS_MKF

    module CoqMod : C_backend_coq.MODIFIERS_COQ

    val init : machine_t list -> unit

end

module EmptyMod = struct

    module HdrMod = C_backend_header.EmptyMod

    module SrcMod = C_backend_src.EmptyMod

    module MainMod = C_backend_main.EmptyMod

    module MakefileMod = C_backend_makefile.EmptyMod

    module CoqMod = C_backend_coq.EmptyMod

    let init machines = ()

end

module Backend = functor (Mod:MODIFIER) ->

struct

    module Header = C_backend_header.Main (Mod.HdrMod)

    module Source = C_backend_src.Main (Mod.SrcMod)

    module SourceMain = C_backend_main.Main (Mod.MainMod)

    module Makefile = C_backend_makefile.Main (Mod.MakefileMod)

    module Coq = C_backend_coq.Main (Mod.CoqMod)

    let gen_files basename prog machines dependencies header_file source_lib_file source_main_file makefile_file coq_file machines =

      Mod.init machines;

      let header_out = open_out header_file in

      let header_fmt = formatter_of_out_channel header_out in

      let source_lib_out = open_out source_lib_file in

      let source_lib_fmt = formatter_of_out_channel source_lib_out in

      (* Generating H file *)

      Header.print_header header_fmt basename prog machines;

      (* Generating Lib C file *)

      Source.print_lib_c source_lib_fmt basename prog machines dependencies;

      (match coq_file with

        | None -> ()

        | Some path ->

          let coq_lib_out = open_out path in

          let coq_lib_fmt = formatter_of_out_channel coq_lib_out in

          Coq.print_lib_coq coq_lib_fmt basename prog machines

      );

      match !Options.main_node with

      | "" ->  () (* No main node: we do not genenrate main nor makefile *)

      | main_node -> (

        match Machine_code.get_machine_opt main_node machines with

        | None -> Format.eprintf "Unable to find a main node named %s@.@?" main_node; assert false

        | Some m -> begin

          let source_main_out = open_out source_main_file in

          let source_main_fmt = formatter_of_out_channel source_main_out in

          let makefile_out = open_out makefile_file in

          let makefile_fmt = formatter_of_out_channel makefile_out in

          (* Generating Main C file *)

          SourceMain.print_main_c source_main_fmt m basename prog machines dependencies;

          (* Generating Makefile *)

         Makefile.print_makefile basename main_node dependencies makefile_fmt

        end

      )

end

let translate_to_c header source_lib source_main makefile coq_file basename prog machines dependencies =

  Format.printf "%a" (Utils.fprintf_list ~sep:"\n@ " pp_machine) machines;

  let module SpecArg = struct 

    let prog = prog 

    let machines = arrow_machine::machines

  end in

  let module ProofArg = struct 

    let prog = prog 

    let machines = arrow_machine::machines

  end in

  let module SpecMod = C_backend_spec.Make (SpecArg) in

  let module ProofMod = C_backend_proof.Make (ProofArg) in

  match !Options.spec with

  | "no" -> begin

    let module B = Backend(EmptyMod) in

    B.gen_files basename prog machines dependencies header source_lib source_main makefile None machines

  end

  | "acsl" -> begin

    let module B = Backend(SpecMod) in

    B.gen_files basename prog machines dependencies header source_lib source_main makefile None machines

  end

  | "proof" -> begin

    let module B = Backend(ProofMod) in

    B.gen_files basename prog machines dependencies header source_lib source_main makefile (Some coq_file) machines

  end

  | "c" -> begin

    assert false (* not implemented yet *)

  end

  | _ -> assert false

(* Local Variables: *)

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

(* End: *)