(*-----------------------------------------------------------------------
** Copyright (C) - Verimag.
** This file may only be copied under the terms of the GNU Library General
** Public License
**-----------------------------------------------------------------------
**
** File: gen_stubs.ml
** Author: jahier@imag.fr
**
*)

open List
open Gen_stubs_common


(** Parses a C header file and to generate stub files for calling poc
    C programs from lurette. Its main function takes as input the name
    of the sut and the name of the oracle (file names without
    extension), and outputs all the necessary stub files.

    Note that the C files should follows the poc convention (e.g., generated
    by a lustre compiler). For instance, the header files  should contain
    the following pragmas:

    //MODULE: <module name> n m
    //    where [n] is the input var number, and [m] the output var one

  //IN:  <C type of the first input var> <a C identifier for the first input var>

  ...

  //IN:  <C type of the nth input var> <a C identifier for the nth input var>

  //OUT: <C type of the first output var> <a C identifier for the first output var>

    ...

  //OUT: <C type of the mth output var> <a C identifier for the mth output var>
*)



(****************************************************************************)
(** Generates a fake oracle (that always returns true) so that the
  user does not have to write it if he does not have any assertion to
  check. It can also be used as a skeleton.
*)
let (gen_a_fake_oracle : string -> string -> string -> compiler -> string -> bool) =
  fun user_dir tmp_dir sut_node compiler sut_h ->
(*     try *)
      let (tdl, sut_h, sut_vi, sut_vo) =
	match compiler with
	  | VerimagV6
	  | VerimagV4 ->
	      let (tdl, vi, vo) = Parse_poc.get_vn_and_ct_list sut_h in
		(tdl, sut_h, vi, vo)
	  | Scade ->
	      let (tdl, vi, vo) = Parse_c_scade.get_vn_and_ct_list sut_h sut_node compiler in
		(tdl, sut_h, vi, vo)
	  | ScadeGUI ->
	      let (tdl, vi, vo) = Parse_c_scade.get_vn_and_ct_list sut_h sut_node compiler in
		(tdl, sut_h, vi, vo)
	  | Sildex -> 
	      let (tdl, vi, vo) = Parse_sildex.get_vn_and_ct_list sut_h in
		(tdl, sut_h, vi, vo)
      in
      let vn_ct_l = (List.append sut_vi sut_vo)  in
      let vn_st_str_l =
	List.map
	  (fun (vn, ct) ->
	   (vn ^ ":" ^ (c_type_to_scade_type tdl ct))
	  )
	  vn_ct_l
      in
      let oc = 
	open_out (Filename.concat user_dir (sut_node ^ "_always_true.lus")) 
      in
      let put s = output_string oc s in
	
	put "-- Automatically generated from ";
	put sut_h ;
	put "\n-- Migth be overrided: rename it if you modify it." ;
	put "\n\n";
	put ("node " ^ sut_node ^ "_always_true(\n\t");
	put (format_string_list "; \n\t" vn_st_str_l) ;

	put (") returns (" ^ sut_node ^ "__ok:bool);\n");
	put ("let \n  " ^ sut_node ^ "__ok = true ; \ntel\n");
	put "\n";
	close_out oc;
	true
(*     with e ->  *)
(*       output_string stderr (Printexc.to_string e); *)
(*       false *)



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

let usage = "
usage: gen_stub <sut> <sut_node> <sut_compiler> [<oracle> <oracle_node> \
<oracle_compiler>] dir

 where:
  o <sut> is the name of the SUT file
  o <sut_node> is the name of the main node
  o <sut_compiler> is the name of the lustre compiler (= \"verimag\" or \"scade\")
  o Ditto for <oracle>, <oracle_node>, and <oracle_compiler>
    The arguments related to the oracle are optionals.
  o <dir> is the name of the directory where to generate files

gen_stubs basically performs the following actions:
  o compile lustre/saofdm files, if necessary
  o generate a fake oracle (a lustre file), if not available
  o generate stub code (lurette__sut.c) so that lurette is
     - aware of sut variable names and types
     - able to call sut step and try functions

nb: gen_stubs is not meant to be used directly by end-users.
"

let compile_lustre_program_if_needed
  lustre_prog0 lustre_node compiler user_dir tmp_dir header_file =
  let prog_dir = Filename.dirname lustre_prog0 in
  let save_dir = Sys.getcwd () in
  let res =
    let (gen_c_file, gen_h_file) =
      ((Filename.chop_extension header_file) ^ ".c", header_file)
    in
    let lustre_prog_stat = 
      if Sys.file_exists lustre_prog0 then (Unix.stat lustre_prog0) else
	(
	  print_string  ("*** " ^ lustre_prog0 ^ " does not exist.\n");
	  flush stdout;
	  exit 2
	)
    in

    let lustre_prog =
      if
	(
	  (Filename.check_suffix lustre_prog0 ".etp") ||
	  (Filename.check_suffix lustre_prog0 ".vsp")
	)
      then 
	(if
	   Util2.etp_to_saofdm lustre_prog0 lustre_node
	 then
	   (Filename.chop_extension lustre_prog0) ^ ".saofdm"
	 else
	   exit 100
	)
      else
	lustre_prog0
    in
      Sys.chdir prog_dir;
      
      if
	(Filename.check_suffix lustre_prog ".c")
      then
	(*
	  if users provide C files for the sut and the oracle, we copy
	  them (.c and .h) to the tmp dir where they are expected to be
	*)
	(
	  (Util2.cp 
	     ((Filename.chop_suffix lustre_prog ".c") ^ ".h") 
	     tmp_dir stdout stderr
	  ) &&
	  (Util2.cp lustre_prog  tmp_dir stdout stderr)
	)
      else if
	(Filename.check_suffix lustre_prog ".saofdm")
	&&
	(
	  not (Sys.file_exists gen_c_file)
	  ||
	  not (Sys.file_exists gen_h_file)
	  ||
	  ((Unix.stat gen_c_file).Unix.st_mtime < lustre_prog_stat.Unix.st_mtime)
	  ||
	  ((Unix.stat gen_h_file).Unix.st_mtime < lustre_prog_stat.Unix.st_mtime)
	)
      then
	(
	  (* 	Util2.scade_cg lustre_prog lustre_node  tmp_dir;  *)
	  if Util2.scade2lustre lustre_prog then
	    (Util2.lustre2C
	       ((Filename.chop_extension lustre_prog) ^ ".lus")
	       lustre_node tmp_dir)
	  else
	    exit 101
	)
      else if
	(Filename.check_suffix lustre_prog ".lus")
	&&
	(
	  not (Sys.file_exists gen_c_file)
	  ||
	  not (Sys.file_exists gen_h_file)
	  ||
	  ((Unix.stat gen_c_file).Unix.st_mtime > lustre_prog_stat.Unix.st_mtime)
	  ||
	  ((Unix.stat gen_h_file).Unix.st_mtime < lustre_prog_stat.Unix.st_mtime)
	)
      then
	(* if no .h or .c exists, or if they are too old, we (re)generate them. *)
	(
	  match compiler with
	  | VerimagV6 ->
		output_string stderr (
		  "No " ^ lustre_node ^ ".c or no " ^ lustre_node ^
		  ".h exist(s), so I try to compile " ^ lustre_prog ^
		  " with node " ^ lustre_node ^
		  " with lv6 -ec and ec2c...\n");
		if Util2.lv62ec lustre_prog lustre_node user_dir then
		  Util2.ec2c lustre_node tmp_dir
		else
		  exit 102
	  | VerimagV4 ->
		output_string stderr (
		  "No " ^ lustre_node ^ ".c or no " ^ lustre_node ^
		  ".h exist(s), so I try to compile " ^ lustre_prog ^
		  " with node " ^ lustre_node ^
		  " with lus2ec and ec2c...\n");
		if Util2.lus2ec lustre_prog lustre_node user_dir then
		  Util2.ec2c lustre_node tmp_dir
		else
		  exit 103

	    | ScadeGUI ->
		output_string stderr (
		  "No " ^ lustre_node ^ ".c or no " ^ lustre_node ^
		  ".h exist(s), so I try to compile " ^ lustre_prog ^
		  " with node " ^ lustre_node ^
		  " with the lustre2C scade code generator.\n");
		Util2.lustre2C
		  ((Filename.chop_extension lustre_prog) ^ ".lus")
		  lustre_node tmp_dir
		
	    | Scade ->
		output_string stderr (
		  "No " ^ lustre_node ^ ".c or no " ^ lustre_node ^
		  ".h exist(s), so I try to compile " ^ lustre_prog ^
		  "with node " ^ lustre_node ^
		  " with the lustre2C scade code generator.\n");
		Util2.lustre2C
		  ((Filename.chop_extension lustre_prog) ^ ".lus")
		  lustre_node tmp_dir
		  
	    | Sildex -> (* XXX TODO *)
		output_string stderr (
		  "Lurette do not know how to compile Sildex code " ^
		  "yet. \nPlease provide the C files (for the sut and the oracle).\n");
		exit 104
		  
	)
      else
	(* No compilation seems to be required *)
	true
  in
    Sys.chdir save_dir;
    res


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

(* Sorts oracle var w.r.t. to their order in ref_list in order to check
   var names constency. *)
let (sort_vars: string list -> vn_ct list -> vn_ct list) =
  fun ref_list var_list ->
    List.sort
    (fun (vn1, t1) (vn2, t2) -> Util.compare_list ref_list vn1 vn2)
    var_list



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

let (gen_stubs_file : string -> string -> compiler -> string -> compiler -> 
       string -> string -> bool -> bool) =
  fun tmp_dir sut sut_compiler oracle oracle_compiler sut_h oracle_h 
      oracle_is_present ->
(*     try *)
      let sut_m = (Filename.basename sut) in
      let oracle_m = (Filename.basename oracle) in

      (* Get var names and types of the sut *)
      let (sut_tdl, sut_vi, sut_vo) =
	match sut_compiler with
	  | VerimagV6 
	  | VerimagV4 ->
	      let (x1, x2, x3) = Parse_poc.get_vn_and_ct_list sut_h in
		(x1, x2, x3)
	  | Scade ->
	      let (x1, x2, x3) = Parse_c_scade.get_vn_and_ct_list sut_h sut_m sut_compiler in
		(x1, x2, x3)
	  | ScadeGUI ->
	      let (x1, x2, x3) = Parse_c_scade.get_vn_and_ct_list sut_h sut_m sut_compiler  in
		(x1, x2, x3)
	  | Sildex ->
	      Parse_sildex.get_vn_and_ct_list sut_h
      in

      (* Get var names and types of the oracle *)
      let (oracle_tdl, oracle_vi, oracle_vo) =
	if 
	  not oracle_is_present 
	then
	  ([],[],[])
	else
	  match oracle_compiler with
	    | VerimagV6
	    | VerimagV4 ->
		let (x1, x2, x3) = Parse_poc.get_vn_and_ct_list oracle_h in
		  (x1, x2, x3)
	    | Scade ->
		let (x1, x2, x3) = Parse_c_scade.get_vn_and_ct_list oracle_h oracle_m oracle_compiler in
		  (x1, x2, x3)
	    | ScadeGUI ->
		let (x1, x2, x3) = Parse_c_scade.get_vn_and_ct_list oracle_h oracle_m oracle_compiler in
		  (x1, x2, x3)
	    | Sildex ->
		Parse_sildex.get_vn_and_ct_list oracle_h
      in

      (* sort vars according to the ordering in the sut (useless?) *)
      let v_list_ref = append (fst (split sut_vi)) (fst (split sut_vo)) in

	(
	  match sut_compiler with
	    | VerimagV6
	    | VerimagV4 ->
		Gen_stubs_poc.go sut_m "lurette__sut" sut_tdl sut_vi sut_vo
	    | ScadeGUI ->
		Gen_stubs_scade.go sut_m "lurette__sut" sut_tdl sut_vi sut_vo sut_h
	    | Scade ->
		Gen_stubs_scade.go sut_m "lurette__sut" sut_tdl sut_vi sut_vo sut_h
	    | Sildex ->
		Gen_stubs_sildex.go sut_m "lurette__sut" sut_tdl sut_vi sut_vo 
	);

	(* Update the stub files iff they have changed to avoid unnecessary
	   re-compilations *)
	update_file
	  (Filename.concat tmp_dir "lurette__sut.c.new")
	  (Filename.concat tmp_dir "lurette__sut.c");
	true
(*     with e ->  *)
(*       output_string stdout (Printexc.to_string e); *)
(*       flush stdout; *)
(*       false *)

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

(** gen_stubs top-level function *)
let (main : unit -> 'a) =
  fun _ ->

    let arg_nb = (Array.length Sys.argv) - 1 in

      output_string stderr "gen_stubs ";
      Array.iter (fun x -> output_string stderr (x ^ " ")) Sys.argv;
      output_string stderr "\n";
      flush stderr;

      (*       if true then *)
      (* 	for i = 0 to (arg_nb-1) do *)
      (* 	  print_string ("\n\targ" ^ (string_of_int i) ^ " = " ^ (Sys.argv.(i))); *)
      (* 	  print_string "\n"; *)
      (* 	done; *)
      (*       flush stdout; *)
	   

      if
	     (
	       arg_nb >= 1
	       &&
	       ((Sys.argv.(1) = "--help") || (Sys.argv.(1) = "-help")  ||
	          (Sys.argv.(1) = "-h")
	       )
	     )
	     || arg_nb = 0
      then
	     (
	       output_string stdout usage;
	       true
	     )
      else
	     (
	       if Sys.argv.(1) = "lurette__sut" then
	         (
	           output_string stderr (
		          "You cannot call your file lurette__sut.lus, sorry ;" ^
		            "please rename it.\n");
	           exit 2
	         );
	       let i = 
	         (* there is an extra argument (root node header file) for ScadeGUI *)
	         (if ((string_to_compiler Sys.argv.(3)) = ScadeGUI) then 1 else 0) in
	         if
	           arg_nb = 4 + i
	         then
	           (* No oracle is provided *)
	           let sut_path = Sys.argv.(1)
	           and sut_node = Sys.argv.(2)
	           and sut_compiler = (string_to_compiler Sys.argv.(3))
	           and tmp_dir = Sys.argv.(4)
	           in
	           let user_dir = Filename.dirname sut_path in
	           let header_file =
		          if 
		            (string_to_compiler Sys.argv.(3)) = ScadeGUI
		          then
		            (Filename.concat tmp_dir  Sys.argv.(5))
		          else
		            (Filename.concat tmp_dir (sut_node ^ ".h"))
	           in
		          (
		            (sut_compiler = ScadeGUI)
		            ||
		              (compile_lustre_program_if_needed 
		                 sut_path sut_node sut_compiler user_dir tmp_dir header_file)
		          )
                  (* 		&& *)
                  (* 		gen_oracle_always_true () *)
		          &&
		            gen_stubs_file tmp_dir
		            (Filename.concat user_dir sut_node) sut_compiler
		            (Filename.concat user_dir sut_node) sut_compiler 
		            header_file header_file false
		            
	         else true
        )
;;

if (main ()) then () else exit 105 ;;