CristalCaveGem » LustreC

let get_machine machines node_name =

  List.find (fun m  -> m.mname.node_id = node_name) machines

let full_memory_vars machines machine =

  let rec aux fst prefix m =

    (rename_machine_list (if fst then prefix else concat prefix m.mname.node_id) m.mmemory) @

  in

  aux true machine.mname.node_id machine

let stateless_vars machines m =

  (rename_machine_list m.mname.node_id m.mstep.step_inputs)@

    (rename_machine_list m.mname.node_id m.mstep.step_outputs)

       (*   (Utils.fprintf_list ~sep:" " pp_var) (step_vars machines m); *)

       (match m.mstep.step_asserts with

       | [] ->

          begin

            Format.fprintf fmt "@[<v 2>(rule (=> @ %a@ (%a %a)@]@.))@.@."

                           (pp_conj (pp_instr false m.mname.node_id)) m.mstep.step_instrs

                           pp_machine_step_name m.mname.node_id

          end

       | assertsl ->

          begin

	    let pp_val = pp_horn_val ~is_lhs:true m.mname.node_id pp_var in

            (* print_string pp_val; *)

            let instrs_concat = m.mstep.step_instrs in

            Format.fprintf fmt "@[<v 2>(rule (=> @ (and @ %a@. %a)(%a %a)@]@.))@.@."

                           (pp_conj (pp_instr false m.mname.node_id)) instrs_concat

                           (pp_conj pp_val) assertsl

                           pp_machine_step_name m.mname.node_id

                           (Utils.fprintf_list ~sep:" " pp_var) (step_vars machines m);

	    (* Format.fprintf fmt " @[<v 2>%a@]@ @.@.@." *)

            (*                 (pp_conj pp_val) assertsl; *)

          end

       );

     end

    end

    (pp_conj pp_var) main_output

    (Utils.fprintf_list ~sep:" " pp_var) main_memory_next

    ;

let cex_computation machines fmt node machine =

    (pp_conj pp_var) cex_output

    (Utils.fprintf_list ~sep:" " pp_var) cex_memory_next

    ;

let main_print machines fmt =

    ignore (Modules.load_header ISet.empty header);

    ignore (check_top_decls header);

    create_dest_dir ();

      (fun fmt -> fprintf fmt ".. generating compiled header file %sc@," (destname ^ extension));

    Lusic.write_lusic true header destname lusic_ext;

    Lusic.print_lusic_to_h destname lusic_ext;

(* compile a .lus source file *)

let rec compile_source dirname basename extension =

  Log.report ~level:1 (fun fmt -> fprintf fmt "@[<v>");

  (* Parsing source *)

  let prog = parse_source source_name in

  let prog = Automata.expand_decls prog in

  (* Importing source *)

  (* Typing *)

  let computed_types_env = type_decls type_env prog in

  (* Clock calculus *)

  let computed_clocks_env = clock_decls clock_env prog in

  (* Perform global inlining *)

  let prog =

      (match !Options.main_node with | "" -> false | _ -> true) then

      Inliner.global_inline basename prog type_env clock_env

    else

  Log.report ~level:3 (fun fmt -> fprintf fmt "@[<v 2>@ %a@]@," Scheduling.pp_fanin_table node_schs);

  Log.report ~level:3 (fun fmt -> fprintf fmt "@[<v 2>@ %a@]@," Printers.pp_prog prog);

    - eliminate trivial expressions

 *)

    else

      prog

  in

  let machine_code = Machine_code.translate_prog prog node_schs in

  (* Optimize machine code *)

    if !Options.optimization >= 2 && !Options.output <> "horn" then

      begin

	Log.report ~level:1 (fun fmt -> fprintf fmt ".. machines optimization (phase 1)@,");

      end

    else

      machine_code

  (* Optimize machine code *)

    if !Options.optimization >= 3 && !Options.output <> "horn" then

      begin

	Log.report ~level:1 (fun fmt -> fprintf fmt ".. machines optimization (phase 2)@,");

  let basename    =  Filename.basename basename in

  let destname = !Options.dest_dir ^ "/" ^ basename in

  let _ = match !Options.output with

	begin

	  let alloc_header_file = destname ^ "_alloc.h" in (* Could be changed *)

	  let source_lib_file = destname ^ ".c" in (* Could be changed *)

	  let source_main_file = destname ^ "_main.c" in (* Could be changed *)

	  let makefile_file = destname ^ ".makefile" in (* Could be changed *)

	  Log.report ~level:1 (fun fmt -> fprintf fmt ".. C code generation@,");

	    alloc_header_file source_lib_file source_main_file makefile_file

	    basename prog machine_code dependencies

	end

	let traces_file = destname ^ ".traces" in (* Could be changed *)

	let traces_out = open_out traces_file in

	let fmt = formatter_of_out_channel traces_out in

	)

      end

      begin

	let source_file = destname ^ ".lustrec.lus" in (* Could be changed *)

	let source_out = open_out source_file in

  | _        -> assert false

let anonymous filename =

      else

    (false, "") extensions in

  if ok_ext then

    let dirname = Filename.dirname filename in

    Printexc.record_backtrace true;

    Arg.parse Options.options anonymous usage

  with

  | Types.Error (_,_) | Clocks.Error (_,_)

  | Causality.Cycle _ -> exit 1

  | Sys_error msg -> (eprintf "Failure: %s@." msg)

  | exc -> (Utils.track_exception (); raise exc)