CristalCaveGem » LustreC

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

(*                                                                  *)

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

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

(*                                                                  *)

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

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

(*  version 2.1.                                                    *)

(*                                                                  *)

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

open Utils

open Format 

  if !Options.main_node = "" then

    begin

  begin

    if not (Sys.file_exists !Options.dest_dir) then

      begin

      end;

    if (Unix.stat !Options.dest_dir).Unix.st_kind <> Unix.S_DIR then

      begin

	eprintf "Failure: destination %s is not a directory.@.@." !Options.dest_dir;

	exit 1

      end

  end

  (* let f_in = open_in filename in *)

  (* let lexbuf = Lexing.from_channel f_in in *)

  (* Location.init lexbuf filename; *)

                | ".lusi" ->

                  Log.report ~level:1

                    (fun fmt -> fprintf fmt ".. parsing header file %s@ " filename);

                  Header

                | ".lus" ->

                  Log.report ~level:1

                    (fun fmt -> fprintf fmt ".. parsing source file %s@ " filename);

                  Program

                | _ -> assert false))

     *    Parse.report_error err;

     *    raise exc *)

        Location.pp_loc loc;

    )

    Automata.expand_decls decls

    raise exc

    Stateless.check_prog decls

  with (Stateless.Error (loc, err)) as exc ->

      Location.pp_loc loc;

    raise exc

    Stateless.force_prog decls

  with (Stateless.Error (loc, err)) as exc ->

    eprintf "Stateless status error: %a%a@."

      Stateless.pp_error err

      Location.pp_loc loc;

    raise exc

      Typing.type_prog env decls

    with Types.Error (loc,err) as exc ->

      eprintf "Typing error: %a%a@."

        Types.pp_error err

        Location.pp_loc loc;

      raise exc

  new_env

let clock_decls env decls = 

      Clock_calculus.clock_prog env decls

    with (Clocks.Error (loc,err)) as exc ->

      eprintf "Clock calculus error: %a%a@." Clocks.pp_error err Location.pp_loc loc;

      raise exc

  new_env

  let new_tenv = type_decls Basic_library.type_env header in   (* Typing *)

  let new_cenv = clock_decls Basic_library.clock_env header in   (* Clock calculus *)

  header, new_tenv, new_cenv

(*

 List.fold_right

   (fun top_decl (ty_env, ck_env) ->

     match top_decl.top_decl_desc with

     | Node nd          -> (Env.add_value ty_env nd.node_id nd.node_type,

			    Env.add_value ck_env nd.node_id nd.node_clock)

     | ImportedNode ind -> (Env.add_value ty_env ind.nodei_id ind.nodei_type,

			    Env.add_value ck_env ind.nodei_id ind.nodei_clock)

     | Const c          -> get_envs_from_const c (ty_env, ck_env)

     | TypeDef _        -> List.fold_left (fun envs top -> consts_of_enum_type top_decl

     | Open _           -> (ty_env, ck_env))

   header

   (Env.initial, Env.initial)

 *)

    (* checking defined types are compatible with declared types*)

    Typing.check_typedef_compat header;

    (* checking type compatibility with computed types*)

    Typing.check_env_compat header declared_types_env computed_types_env;

    (* checking clocks compatibility with computed clocks*)

    Clock_calculus.check_env_compat header declared_clocks_env computed_clocks_env;

    (* checking stateless status compatibility *)

    Stateless.check_compat header

  with

  | (Types.Error (loc,err)) as exc ->

      Types.pp_error err

      Location.pp_loc loc;

  | Clocks.Error (loc, err) as exc ->

      Clocks.pp_error err

      Location.pp_loc loc;

  | Stateless.Error (loc, err) as exc ->

      Stateless.pp_error err

      Location.pp_loc loc;

let resolve_contracts prog =

  (* Bind a fresh node with a new name according to existing nodes and freshly binded contract node. Clean the contract to remove the stmts  *)

    let stmts, locals, c =

      List.fold_left (

          fun (stmts, locals, c) import ->

          (* Search for contract in prog.

             The node have to be processed already. Otherwise raise an error.

             Each stmts in injected with a fresh name

             Inputs are renamed and associated to the expression in1

             Same thing for outputs.

           *)

          let name = import.import_nodeid in

              if not (is_node_contract imp_nd) then

                assert false (* should be a contract *)

              else

                let imp_c = get_node_contract imp_nd in

                if not (imp_c.imports = [] && imp_c.locals = [] && imp_c.consts = [] && imp_c.stmts = []) then

                (  Format.eprintf "Invalid processed contract: %i %i %i %i@.@?" (List.length imp_c.imports) (List.length imp_c.locals) (List.length imp_c.consts) (List.length imp_c.stmts);

                assert false (* should be processed *)

                )

            let imp_nd = rename_node (fun x -> x (* not changing node names *)) name_prefix imp_nd in

            let imp_in = imp_nd.node_inputs in

            let imp_out = imp_nd.node_outputs in

            let imp_locals = imp_nd.node_locals in

            let locals = imp_in@imp_out@imp_locals@locals in

            let imp_c = get_node_contract imp_nd in

            (* Assigning in and out *)

            let mk_def vars_l e =

              let lhs = List.map (fun v -> v.var_id) vars_l in

              Eq (mkeq loc (lhs, e))

            let out_assigns = mk_def imp_out import.outputs in

            let stmts = in_assigns :: out_assigns :: imp_nd.node_stmts @ stmts in

            stmts, locals, c 

    in

              consts = [];

              stmts = [];

              imports = []

            }

    in

    (* Format.eprintf "Processed stmts: %a@." Printers.pp_node_stmts stmts;

     * Format.eprintf "Processed locals: %a@." Printers.pp_vars locals; *)

  in

  let process_contract_new_node accu_contracts prog top =

    let id, spec, inputs, outputs =

      match top.top_decl_desc with

      | Node nd -> nd.node_id, nd.node_spec, nd.node_inputs, nd.node_outputs

      | ImportedNode ind -> ind.nodei_id, ind.nodei_spec, ind.nodei_inputs, ind.nodei_outputs

      | _ -> assert false

    in

      match spec with

      | None | Some (NodeSpec _) -> assert false

      | Some (Contract c) ->

         process_contract accu_contracts c

    (* Create a fresh name *)

    let used v = List.exists (fun top ->

                     match top.top_decl_desc with

                     | Node _

                       | ImportedNode _ ->

                        (node_name top) = v

                     | _ -> false

                   ) (accu_contracts@prog)

    in

    let new_nd_id = mk_new_name used (id ^ "_coco") in

    let new_nd =

      mktop_decl

        c.spec_loc

        top.top_decl_owner

        top.top_decl_itf

             node_id = new_nd_id;

	     node_type = Types.new_var ();

	     node_clock = Clocks.new_var true;

	     node_inputs = inputs;

	     node_outputs = outputs;

	     node_locals = locals;

	     node_gencalls = [];

	     node_checks = [];

	     node_asserts = []; 

	     node_stmts = stmts;

	     node_dec_stateless = false;

	     node_stateless = None;

	     node_spec = Some (Contract c);

	     node_annot = [];

	     node_iscontract = true;

        }) in

  in

  (* Processing nodes in order. Should have been sorted by now

     Each top level contract is processed: stmts pushed in node

     Each regular imported node or node associated with a contract is

     replaced with a simplidfied contract and its contract is bound to

     a fresh node.

   *)

  let new_contracts, prog =

    List.fold_left

      (

        fun (accu_contracts, accu_nodes) top ->

        match top.top_decl_desc with

        | Node nd when nd.node_iscontract -> (

          match nd.node_spec with

          | None | Some (NodeSpec _) -> assert false

          | Some (Contract c) ->

             let stmts, locals, c = process_contract accu_contracts c in

               { nd with

                 node_locals = nd.node_locals @ locals;

                 node_stmts = nd.node_stmts @ stmts;

                 node_spec = Some (Contract c);

               }

             in

             { top with top_decl_desc = Node nd }::accu_contracts,

             accu_nodes

        )

        | Node nd -> (

          match nd.node_spec with

          | None -> accu_contracts, top::accu_nodes (* A boring node: no contract *)

             let new_nd = process_contract_new_node accu_contracts prog top in

             new_nd::accu_contracts,

             { top with top_decl_desc = Node nd }::accu_nodes

        )

        | ImportedNode ind -> ( (* Similar treatment for imported nodes *)

          match ind.nodei_spec with

            None -> accu_contracts, top::accu_nodes (* A boring node: no contract *)

             let new_nd = process_contract_new_node accu_contracts prog top in

             let ind = { ind with nodei_spec = (Some (NodeSpec (node_name new_nd))) } in

             new_nd::accu_contracts,

             { top with top_decl_desc = ImportedNode ind }::accu_nodes

        )

        | _ -> accu_contracts, top::accu_nodes

      ) ([],[]) prog

  in

  (List.rev new_contracts) @ (List.rev prog)

  if !Options.track_exceptions

  then (Printexc.print_backtrace stdout; flush stdout)

  else ()

  let update_vdecl_parents parent v =

    v.var_parent_nodeid <- Some parent

  in

  List.iter (

    fun top -> match top.top_decl_desc with

    | Node nd ->

       List.iter

	 (update_vdecl_parents nd.node_id)

	 (nd.node_inputs @ nd.node_outputs @ nd.node_locals )  

    | ImportedNode ind -> 

       List.iter

	 (update_vdecl_parents ind.nodei_id)

	 (ind.nodei_inputs @ ind.nodei_outputs )  

    | _ -> ()

  ) prog