(*-----------------------------------------------------------------------
** Copyright (C) 2001 - Verimag.
** This file may only be copied under the terms of the GNU Library General
** Public License 
**-----------------------------------------------------------------------
**
** File: generate_lurette_interface.ml
** Main author: jahier@imag.fr
**
** 
** Implements a program that takes as input the string "sut"
** (resp. "oracle") as well as a C header file `<foo>.h' to interface,
** and which outputs stub files named `lurette_sut.h' and
** `lurette_sut.c' (resp. `lurette_oracle.h' and `lurette_oracle.c').
** Those files are used by the lurette Makefile to interface the sut
** (resp. the oracle).
** 
** Note that <foo>.h should follows the poc convention (e.g., generated
** by a lustre compiler). Namely, it 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>
*)

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


type file = string
type module_name = string

type var_name = string
type c_type = string
type ml_type = string
type fresh_var_name = string

type vn_ct = var_name * c_type
type vn_ct_mlt_fvn = var_name * c_type * ml_type * fresh_var_name


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


(* XXX Is it really a good idea to use regexp to parse those files ? *)

let reg_typedef = Str.regexp "^typedef" 
let reg_blank = Str.regexp " " 
let reg_semicol = Str.regexp ";" 

type alias = c_type * c_type

let rec 
  (get_typedef_alias: file -> alias list) =
(*
** [get_typedef_alias file] reads `file' (a C header file) and search 
** for typedef C expressions and returns the list of (alias_type, C_type) 
** found in `file'.
*)
  fun file -> 
    let str = Util.readfile file in  
      find_typedef_list str 0 [] 
and
  (find_typedef_list: string -> int -> alias list -> alias list) =
  fun str sptr list -> 
    try
      let (alias, sptr1) = find_next_typedef str sptr in
	find_typedef_list str sptr1 (alias::list)
    with Not_found -> list
and
  (find_next_typedef: string -> int -> ((string * string) * int)) =
  fun str sptr -> 
    let sptr1 = Str.search_forward reg_typedef str sptr in
    let sptr2 = Str.search_forward reg_blank str (sptr1+1) in
    let sptr3 = Str.search_forward reg_blank str (sptr2+1) in
    let sptr4 = Str.search_forward reg_semicol str (sptr3+1) in
    let c_type = String.sub str (sptr2 + 1) (sptr3 - sptr2 - 1) in
    let alias_type = String.sub str (sptr3 + 1) (sptr4 - sptr3 - 1)  in
      ((alias_type, c_type), sptr4)

(* let () = assert(
  (Util.list_are_equals 
     (get_typedef_alias "tram_simple.h")
     (Util.sort_list_string_pair  [("_float", "float"); ("_double", "double"); 
			      ("_real", "double"); ("_string", "char*"); 
			      ("_integer", "int"); ("_boolean", "int")] )))
*)

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

let reg_MOD = Str.regexp "^//MODULE:" 
let reg_IN = Str.regexp "^//IN:" 
let reg_OUT = Str.regexp "^//OUT:" 
let reg_cr = Str.regexp "\n" 

let rec (get_vn_and_ct_list: file -> module_name * vn_ct list * vn_ct list) = 
(*
** Parses poc pragmas in a C header file and returns the module name, the 
** list of input vars, and the list of output vars name and type. 
** 
** poc pragmas have the following shape:
** 
** //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>
*)
  fun file -> 
    let str = Util.readfile file in        
    let (mod_name, ni, no, str_ptr1) = find_module_name str in 
    let (vi, str_ptr2) = find_var_list reg_IN str str_ptr1 [] in 
    let (vo, _) = find_var_list reg_OUT str str_ptr2 [] in  
      if (List.length vi = ni && List.length vo = no) then  
	(mod_name, vi, vo) 
      else  
	failwith ("Inconsistent pragmas found in `" ^ file ^   
		  "'. The number of variables is wrong: " ^ 
		  (string_of_int ni)  ^ " and " ^ (string_of_int no)  ^
		  " were declared whereas "  ^ (string_of_int (List.length vi))  ^ 
		  " and " ^ (string_of_int (List.length vo))  ^ " were counted")

and
  (find_module_name: string -> module_name * int * int * int) =
  fun str -> 
    let beg = Str.search_forward reg_MOD str 0 in
    let mod_name_beg = Str.search_forward reg_blank str beg in
    let mod_name_end = Str.search_forward reg_blank str (mod_name_beg+1) in
    let mod_name = String.sub str (mod_name_beg+1) (mod_name_end - mod_name_beg - 1) in
    let vi_nb_end = Str.search_forward reg_blank str (mod_name_end+1) in 
    let vi_nb_str = String.sub str (mod_name_end+1) (vi_nb_end - mod_name_end - 1) in 
    let vi_nb =  
      try (int_of_string vi_nb_str)  
      with _ -> failwith ("*** `" ^ vi_nb_str ^ "'is not an int") 
    in 
    let vo_nb_end = Str.search_forward reg_cr str (vi_nb_end + 1) in 
    let vo_nb_str = String.sub str (vi_nb_end+1) (vo_nb_end - vi_nb_end - 1) in 
    let vo_nb =  
      try(int_of_string vo_nb_str)  
      with _ -> failwith ("*** `" ^  vo_nb_str ^ "'is not an int") 
    in 
      (mod_name,  vi_nb, vo_nb, vo_nb_end) 
and 
  (find_var_list: Str.regexp -> string -> int -> vn_ct list -> vn_ct list * int) = 
  fun reg str sptr vars ->  
    try
      let beg =        Str.search_forward reg       str sptr in
      let var_type_b = Str.search_forward reg_blank str beg in 
      let var_name_b = Str.search_forward reg_blank str (var_type_b + 1) in
      let var_name_e = Str.search_forward reg_cr    str (var_name_b + 1) in 

      let var_type = String.sub str (var_type_b + 1) (var_name_b - var_type_b - 1) in 
      let var_name = String.sub str (var_name_b + 1) (var_name_e - var_name_b - 1) in 
	find_var_list reg str var_name_e ((var_name, var_type)::vars)
    with _  -> (vars, sptr) 

let _ = match (get_vn_and_ct_list "tram_simple.h") with 
    (m, lin, lout) -> 
      assert( 
	m = "tram_simple" &&
	      (Util.list_are_equals lin ["attention_depart", "_boolean"; 
				    "porte_ouverte", "_boolean";
				    "en_station", "_boolean"; 
				    "demande_porte", "_boolean"]) &&
	      (Util.list_are_equals lout ["depart_imminent", "_boolean"; 
				    "porte_demandee", "_boolean";
				    "accepter_demande", "_boolean"; 
				    "depart", "_boolean";
				    "attention_depart_a_retentit", "_boolean";
				    "porte_ok", "_boolean";
				    "ouvrir_porte", "_boolean"; 
				    "fermer_porte", "_boolean"]))


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

let (replace_ct_by_their_alias: vn_ct list -> alias list -> vn_ct list) =
  fun list alias -> 
    List.map (fun (vn, ct) -> (vn, (List.assoc ct alias))) list

let _ = assert ((replace_ct_by_their_alias [] []) = [])
let _ = assert (
  (replace_ct_by_their_alias [("a", "foo_int")] [("foo_int", "int")]) 
  = [("a", "int")]
)

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

type res = Ok | Error of string

let (check_var_type: vn_ct list -> vn_ct list -> vn_ct list -> res) = 
(*
** [check_var_type sut_vars or_vi or_vo]  checks the consistency 
** of variable names and types of the sut and the oracle.  
*)
  fun sut_vars or_vi or_vo -> 
    let print_var_list vl = 
      List.iter 
	(fun (v, t) -> 
	   print_string (v ^ " of type " ^ t ^ "; ")) 
	vl  
    in
      if (not (sut_vars = or_vi)) then
	(
	  print_string "\n*** sut input and output vars are: ";
	  print_var_list sut_vars;
	  print_string "\n*** whereas oracle inputs are: ";
	  print_var_list or_vi ;
	  Error("\n*** sut inputs union sut outputs" ^ 
		    " should be the same as oracle inputs.\n")
	)
      else 
	if 
	  (match or_vo with 
	       [(_, t)] -> (t <> "boolean") 
	     | _        -> false
	   ) 
	then 
	  (
	    print_string "\noracle outputs: ";
	    print_var_list or_vo  ;
	    Error("\n*** Oracle outputs should be of one variable " ^ 
		      "of type boolean.\n")
	  )
	else 
	  Ok

let _ = assert ((check_var_type [] [] []) = Ok)
let _ = assert ((check_var_type 
		   [("a","boolean"); ("b","boolean")] 
		   [("a","boolean"); ("b","boolean")] 
		   [("ok", "boolean")]) = Ok)

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

let (generate_stub_c: module_name -> string -> vn_ct list -> vn_ct list -> unit) = 
(* 
** [generate_stub_c mod_name str vi vo] generates a file named `<str>_stub.c' 
** that interfaces the sut and the oracle with Lurette.
*)
  fun mod_name str vi vo ->  
    let oc = open_out (str ^ "_stub.c") in
    let put s = output_string oc s in
    let ov = List.rev vo in
    let (lo_v, lo_t) = List.hd ov in
    let vo_pre = List.tl ov in

(* 
** Compiler directive 
*)
      put ("// Automatically generated from " ^ mod_name ^ ".h by interface/gen_stubs.\n" ^
	   "#include <stdlib.h>\n" ^
	   "#include \"" ^ mod_name ^ ".h\" \n" ^
	   " \n") ;

(*
** variable declarations   
*)
      put "typedef int boolean;\n" ;
      put "\n" ;

      List.iter (fun (v, t) -> put ("static " ^ t ^ "\t" ^ v ^ ";\n")) vi ;
      List.iter (fun (v, t) -> put ("static " ^ t ^ "\t" ^ v ^ ";\n")) vo ;

      put ("static struct " ^ mod_name ^ "_ctx *prg; \n") ;
      put ("static struct " ^ mod_name ^ "_ctx *prg_copy; \n") ;
      put "\n" ;


(*
** Program state initialisation   
*)
      put "// Program state initialisation \n" ;
      put ("void " ^ str ^ "_init() \n{\n" ^
		"  prg = " ^ mod_name ^ "_new_ctx(NULL); \n") ;
      put ("  prg_copy = " ^ mod_name ^ "_new_ctx(NULL); \n}\n") ;
      put "\n" ;

(*
** Output procedures   
*)
      put "// Output procedures (get the output values) \n" ;
      List.iter 
	(fun (v, t) -> 
           put ("void " ^ mod_name ^ "_O_" ^ v ^ "(void *client_data, " ^ t ^ " " ^ v ^ "_toto) \n{\n" ^
		"  " ^ v ^ " = " ^ v ^ "_toto ; \n}\n\n")
	) 
	vo ;

(*
** Step   
*)
      put "\n" ;
      put "// Step \n" ;
      put ("void " ^ str ^ "_step(") ;
      List.iter (fun (v, t) -> put (t ^ " " ^ v ^ ", ")) vi ;

      List.iter (fun (v, t) -> put (t ^ " *" ^ v ^ "_ptr, ")) vo_pre ;
      put (lo_t ^ " *" ^ lo_v ^ "_ptr) \n{\n");

      List.iter  
	(fun (v, t) -> put ("  " ^ mod_name ^ "_I_" ^ v ^ "(prg, " ^ v ^ ");\n"))
	vi ;

      put ("  " ^ mod_name ^ "_step(prg);\n") ;
      List.iter (fun (v, t) -> put ("  *" ^ v ^ "_ptr = " ^ v ^ ";\n")) vo ;
      put "}\n" ;

(*
** Try   
*)
      put "\n" ;
      put "// Try \n" ;
      put ("void " ^ str ^ "_try(") ;
      List.iter (fun (v, t) -> put (t ^ " " ^ v ^ ", ")) vi ;

      List.iter (fun (v, t) -> put (t ^ " *" ^ v ^ "_ptr, ")) vo_pre ;
      put (lo_t ^ " *" ^ lo_v ^ "_ptr) \n{\n");

      put ("  " ^ mod_name ^ "_copy_ctx(prg_copy, prg);\n") ;
      put ("  " ^ str ^ "_step(") ; 
      List.iter (fun (v, t) -> put (v ^ ", ")) vi ;
      List.iter (fun (v, t) -> put (v ^ "_ptr, ")) vo_pre ;
      put (lo_v ^ "_ptr); \n");
      put ("  " ^ mod_name ^ "_copy_ctx(prg, prg_copy);\n") ;
      put "}\n" ;

      close_out oc 


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

type sut_or_oracle = string

let (generate_idl : module_name -> sut_or_oracle -> vn_ct list -> vn_ct list 
       -> unit) = 
(* 
** [generate_idl mod_name str vi vo] generates an idl file named 
** `<str>_idl_stub.idl' that camlidl processes to generate stub files that
** will interface C poc files with lurette. 
*)
  fun mod_name str vi vo ->  
    let oc = open_out (str ^ "_idl_stub.idl") in
    let put s = output_string oc s in
    let ov = List.rev vo in
    let (lo_v, lo_t) = List.hd ov in
    let vo_pre = List.tl ov in
    
      put ("// Automatically generated file from " ^ mod_name 
	   ^ ".h by interface/gen_stubs.\n") ;
      put "\n" ;

       (* 
       ** Program state initialisation   
       *)
      put ("void " ^ str ^ "_init(); \n") ;
      put "\n" ;

       (* 
       ** Step   
       *)
      put ("void " ^ str ^ "_step(\n") ;
      List.iter 
	(fun (v, t) -> 
	   put ("  [in]  " ^ t ^ "  \t" ^ v ^ ", \n")) 
	vi ;

      List.iter 
	(fun (v, t) -> put ("  [out] " ^ t ^ "  \t*" ^ v ^ "_ptr,\n"))
	vo_pre ;
      put ("  [out] " ^ lo_t ^ "   \t*" ^ lo_v ^ "_ptr\n); \n");
      put "\n" ;

       (* 
       ** Try   
       *)
      put ("void " ^ str ^ "_try(\n") ;
      List.iter 
	(fun (v, t) -> 
	   put ("  [in]  " ^ t ^ "  \t" ^ v ^ ", \n")) 
	vi ;

      List.iter 
	(fun (v, t) -> 
	   put ("  [out] " ^ t ^ "  \t*" ^ v ^ "_ptr,\n")) 
	vo_pre ;
      put ("  [out] " ^ lo_t ^ "   \t*" ^ lo_v ^ "_ptr\n); \n");
      
      close_out oc 

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

let rec (generate_n_var_names: string -> int -> fresh_var_name list) =
   (* 
   ** [generate_n_var_names "x" 4] generates the list ["x1"; "x2"; "x3"; "x4"]
   *)
  fun x n -> 
    match n with 
	0 -> []
      | _ -> (List.append (generate_n_var_names x (n-1)) 
		[(x ^ (string_of_int n))])

let _ = assert ((generate_n_var_names "x" 0) = [])
let _ = assert ((generate_n_var_names "x" 4) = ["x1"; "x2"; "x3"; "x4"])



let (get_ml_type2: file -> vn_ct list -> vn_ct list -> vn_ct_mlt_fvn list * vn_ct_mlt_fvn list) = 
(* cf get_ml_type *)
   fun file lin lout -> 
     let str = Util.readfile file in  
     let reg_external = Str.regexp "^external sut_step :" in
     let reg_arrow = Str.regexp "->" in
     let reg_eol = Str.regexp "\n" in 
      
     let rec (read_type_list: int -> string list -> string list) =
       (* 
	** [read_type_list n []] returns the list of types (in reverse order) 
	** of the function sut_step, where n is the character position of the 
	** first char of the first type of sut_step.
	*)
       fun sptr acc ->  
	 let (t, sptr1) = read_next_type sptr in
           if (sptr1>0) then read_type_list sptr1 (t::acc)
	   else t::acc
     and
       (read_next_type: int -> string * int) =
       fun sptr -> 
	 let sptr1 = Str.search_forward reg_arrow str (sptr+1) in
	 let sptr2 = Str.search_forward reg_eol str (sptr+1) in
	   if (sptr1 < sptr2) then
	     (String.sub str (sptr+1) (sptr1 - sptr - 2), (sptr1+2))
	   else
	     (* last type *)
	     (String.sub str (sptr+1) (sptr2 - sptr - 1), -1)
     in
     let (sptr: int) = 
       (* 
	** `sptr' should point to the first char of the first 
	** type of sut_step. 
	*)
       try 
	 let sptr1 = Str.search_forward reg_external str 0 in
	 let sptr2 = Str.search_forward reg_blank str (sptr1+1) in
	 let sptr3 = Str.search_forward reg_blank str (sptr2+1) in
	 let sptr4 = Str.search_forward reg_blank str (sptr3+1) in
	   sptr4
       with Not_found -> assert false
     in
     let (vtl: string list) = read_type_list sptr [] in
       (* 
	** `vtl' ougth to contain the list of sut_try types in reverse order,
	** i.e., the output type in the first place, then the last argument
	** of (the currified version of) sut_try, and so on.
	*)
     let (sut_out_str, sut_in_list) = 
       match vtl with 
	   sut_out_str::sut_in_list_rev -> 
	     (sut_out_str, List.rev sut_in_list_rev)
	     (*
	      ** Any ocaml function have at least one arrow, i.e.,
	      ** vtl should contain at least 2 elements.
	      *)
	 | _ -> assert false
     in 
     let sut_out_list = Str.split (Str.regexp " \\* ") sut_out_str in 
       (*
	** Therefore now sut_out_str should be the type the sut_try output var,
	** sut_in_str be the type of the sut input, and sut_in_list be the list
	** of sut_try input vars (in the rigth order!). 
	*)
       
       (
	 (Util.list_map3 
	    (fun (vn, ct) mlt fvn -> (vn, ct, mlt, fvn)) 
	    lin
	    sut_in_list
	    (generate_n_var_names "x" (List.length lin))),
	 
	 (Util.list_map3
	    (fun (vn, ct) mlt fvn -> (vn, ct, mlt, fvn)) 
	    lout
	    sut_out_list
	    (generate_n_var_names "y" (List.length lout)))
       )

let (get_ml_type: vn_ct list -> vn_ct list -> vn_ct_mlt_fvn list * vn_ct_mlt_fvn list) =
(*
** [get_ml_type sut_in sut_out] parses Sut_idl_stub.ml in order to get 
** the C-ocaml mapping used by camlidl. It returns 2 lists (the 1st one for 
** the input vars, the 2nd one for the output ones) of tuples containing 
** a var name, its ml type, as well as a fresh variable name that will be 
** used later.
*)
  fun lin lout -> 
    get_ml_type2 "sut_idl_stub.ml" lin lout 


(*
** interface/sut_idl_stub.ml has been defined to be able to check that 
** assertion.
*)
let _ = assert 
	  ( (get_ml_type2 "/home/jahier/lurette/interface/sut_idl_stub.ml"
	       [("a","int"); ("b","boolean")] 
	       [("res1","boolean"); ("res2","float")] )
	    = 
	      ([("a","int","int","x1"); ("b","boolean","bool","x2")], 
	       [("res1","boolean","bool","y1"); ("res2","float","float","y2")])
	  )

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

let (generate_lurette_stub_file: vn_ct_mlt_fvn list * vn_ct_mlt_fvn list -> unit) = 
(*
** [generate_lurette_stub_file sut_vi sut_vo] generates an ocaml file that defines:
**    - the type of sut inputs (as a tuple containing the sut variables
**      ordered lexicographically w.r.t. their names)
**    - the type of sut outputs (in the same manner)
**    - Defines a version of `sut_try' that takes as argument a tuple 
**      instead of a currified list of input values as camlidl provides.
**    - ditto for `sut_step', `oracle_try', and `oracle_step'
**    - a list of sut (input and output) variable names and types (so that
**      we can check later that the environment variable names and types are
**      consistent with the ones of the sut).
**    - 2 functions (lookup_sut_in and lookup_sut_out) to access a value from 
**      the input and output tuples given a variable name.
*)
  fun (sut_in, sut_out) -> 

    let oc = open_out "lurette_stub.ml" in
    let put s = output_string oc s in
    let rec (format_string_list: string -> string list -> string) =
       (* 
       ** [format_string_list " * " ["int"; "bool"; "float"]] returns the string
       ** "int * bool * float".
       *)
      fun str list -> 
	match list with
	    [] -> ""
	  | [e] -> e
	  | e::t -> (e ^ str ^ (format_string_list str t))
    in
    let _ = assert ((format_string_list " * " ["int"; "bool"; "float"]) 
		    = "int * bool * float")
    in
    let (put_atomic_expr_rule: vn_ct_mlt_fvn -> unit) =
       (* 
       ** Used to define lookup_in and lookup_out.
       *)
      fun (vn, _, mlt, fvn) -> 
	match mlt with
	    "bool"  -> put ("  \"" ^ vn ^ "\" -> Some(Bool(" ^ fvn ^ "))")
	  | "float" -> put ("  \"" ^ vn ^ "\" -> Some(Float(" ^ fvn ^ "))")
	  | "int"   -> put ("  \"" ^ vn ^ "\" -> Some(Int(" ^ fvn ^ "))")
	  | _ -> assert false
    in
    let (put_fake_value: vn_ct_mlt_fvn -> unit) =
       (* 
       ** Used to define sut_in_init ans sut_out_init.
       *)
      fun (_, _, mlt, _) -> 
	match mlt with
	    "bool"  -> put "false"
	  | "float" -> put "0.0"
	  | "int"   -> put "0"
	  | _ -> assert false
    in
    let put_printer =
      (*
       ** Used to define print_sut_in and print_sut_out
       *)
      fun mlt fvn -> 
	match mlt with
            "int" -> put "    output_string oc (string_of_int " ; 
	      put fvn ; put "); output_string oc \" \"" 
          | "bool" -> put "    output_string oc (my_string_of_bool "; 
	      put  fvn ; put "); output_string oc \" \"" 
	  | "float" -> put "    output_string oc (string_of_float "; 
	      put fvn ; put "); output_string oc \" \"" 
	  | _ -> put "output_string \"***\";\n" ;
    in
    let vnl_in =  List.map (fun (w,x,y,z) -> w) sut_in in
    let vn_ctl_in =  List.map (fun (w,x,y,z) -> (w,x)) sut_in in
    let mltl_in = List.map (fun (w,x,y,z) -> y) sut_in in
    let fvnl_in = List.map (fun (w,x,y,z) -> z) sut_in in

    let vnl_out =  List.map (fun (w,x,y,z) -> w) sut_out in
    let vn_ctl_out =  List.map (fun (w,x,y,z) -> (w,x)) sut_out in
    let mltl_out = List.map (fun (w,x,y,z) -> y) sut_out in
    let fvnl_out = List.map (fun (w,x,y,z) -> z) sut_out in

    let fael_in = 
      List.map2 
	(fun x t -> 
	   match t with 
	       "int" -> ("Int(" ^ x ^ ")")
	     | "bool" -> ("Bool(" ^ x ^ ")")
	     | "float" -> ("Float(" ^ x ^ ")")
	     | _ -> assert false 
	)
	fvnl_in
	mltl_in
    in
      (* 
       ** fael stands for <<fresh atomic expression list>>.
       ** e.g., if mltl_in = [int, bool], then fvnl_in = ["Int(x1)"; "Bool(x2)"]
       *)

      put "(* Automatically generated from sut_idl_stub.ml by interface/gen_stubs. *)\n" ;
      put "open Format\n\n";
      
       (*
       **  Defines the type of sut inputs and outputs.
       *)
      put "type sut_in = " ;
      put (format_string_list " * " mltl_in) ;
      put "\n\n" ;
      
      put "type sut_out = " ;
      put (format_string_list " * " mltl_out) ;
      put "\n\n" ;

       (*
       ** Defines a version of `sut_try' that takes as argument a tuple 
       ** instead of a currified list of input values as camlidl provides.
       *)
      put ("let (sut_try: sut_in -> sut_out) = \n") ;
      put "  fun (";
      put (format_string_list ", " fvnl_in) ;
      put ") -> \n    Sut_idl_stub.sut_try " ;
      put (format_string_list " " fvnl_in) ;
      put "\n\n" ;

       (*
       ** Ditto for `sut_step'.
       *)
      put ("let (sut_step: sut_in -> sut_out) = \n") ;
      put "  fun (";
      put (format_string_list ", " fvnl_in) ;
      put ") -> \n    Sut_idl_stub.sut_step " ;
      put (format_string_list " " fvnl_in) ;
      put "\n\n" ;
      
       (*
       ** Ditto for `oracle_try'.
       *)
      put ("let (oracle_try: sut_in * sut_out -> bool) = \n") ;
      put "  fun ((";
      put (format_string_list ", " fvnl_in) ;
      put "), (";
      put (format_string_list ", " fvnl_out) ;
      put ")) -> \n    Oracle_idl_stub.oracle_try " ;
      put (format_string_list " " fvnl_in) ;
      put " " ; 
      put (format_string_list " " fvnl_out) ;
      put "\n\n" ;

       (*
       ** Ditto for `oracle_step'.
       *)
      put ("let (oracle_step: sut_in * sut_out -> bool) = \n") ;
      put "  fun ((";
      put (format_string_list ", " fvnl_in) ;
      put "), (";
      put (format_string_list ", " fvnl_out) ;
      put ")) -> \n    Oracle_idl_stub.oracle_step " ;
      put (format_string_list " " fvnl_in) ;
      put " " ; 
      put (format_string_list " " fvnl_out) ;
      put "\n\n" ;
      
       (*
       ** Defines 2 variables that contains the list of sut inputs 
       ** (resp outputs) variable names and types so that we can check 
       ** later that the environment variable names and types are 
       ** consistent with the ones of the sut and the oracle. 
       *)

      put "let sut_input_var_name_and_type_list = [" ;
      ( match (List.hd vn_ctl_in) with 
	    (vn, t) -> put ("(\"" ^ vn ^ "\", \"" ^ t ^ "\")") );
      List.iter (fun (vn, t) -> put ("; (\"" ^ vn ^ "\", \"" ^ t ^ "\") ")) (List.tl vn_ctl_in) ;
      put "]\n\n" ;

      put "let sut_output_var_name_and_type_list = [" ;
      ( match (List.hd vn_ctl_out) with 
	    (vn, t) -> put ("(\"" ^ vn ^ "\", \"" ^ t ^ "\")")) ;
      List.iter (fun (vn, t) -> put ("; (\"" ^ vn ^ "\", \"" ^ t ^ "\") ")) (List.tl vn_ctl_out) ;
      put "]\n\n" ;
      							    
       (*
       ** I define that type here because I both need it here and in env.ml, 
       ** and this (generated) module is already imported by env.ml ...
       *)
      put ("type atomic_expr = \n" ^
	   "  | Int of int\n" ^
	   "  | Bool of bool\n" ^
	   "  | Float of float\n" ^
	   "\n\n" ^
	   "let print_atomic_expr e oc = \n" ^
	   "  match e with \n" ^
	   "        Int(i) -> output_string oc (string_of_int i)\n" ^
	   "      | Bool(true) -> output_string oc \"t\" \n" ^
	   "      | Bool(false) -> output_string oc \"f\"\n" ^
	   "      | Float(f) -> output_string oc (string_of_float f)\n" ^
	   "\n\n" ) ;

      (*
       ** Defines 2 functions to access a value from the inputs and outputs
       ** given a variable name. For example, if sut_try have the ml type
       ** `int -> bool -> float -> bool * int', where the corresponding variable
       ** names are respectively "a_i", "b", "f", "res_b" and "res_i", then 
       ** lookup_sut_in and lookup_sut_out will (should) be defined as follows:
       ** 
       ** let (lookup_sut_in: string -> sut_in -> atomic_expr) = 
       **   fun var_name (x1, x2, x3) -> 
       **     match var_name with
       **       "a_i" -> Int(x1)
       **     | "b" -> Bool(x2)
       **     | "f" -> Float(x3)
       **     | _ -> raise Not_found
       **
       ** and
       ** 
       ** let (lookup_sut_out: string -> sut_out -> atomic_expr) = 
       **   fun var_name (x1, x2) -> 
       **     match var_name with
       **       "res_b" -> Bool(x1)
       **     | "res_i" -> Int(x2)
       **     | _ -> raise Not_found
       **
       *)

      put ("let (lookup_sut_in: string -> sut_in -> atomic_expr option) = \n" ^
	   "  fun var_name (");
      put (format_string_list ", " fvnl_in) ;
      put ") -> \n    match var_name with \n" ;

      put "      " ;
      put_atomic_expr_rule (List.hd sut_in) ;
      List.iter 
	(fun x -> 
	   put "\n      |  ";
	   put_atomic_expr_rule x)
	(List.tl sut_in) ;
      put ("\n      | _ -> None \n\n"); 


      put ("let (lookup_sut_out: string -> sut_out -> atomic_expr option) = \n" ^
	   "  fun var_name (");
      put (format_string_list ", " fvnl_out) ;
      put ") -> \n    match var_name with \n" ;

      put "      " ;
      put_atomic_expr_rule (List.hd sut_out) ;
      List.iter 
	(fun x -> 
	   put "\n      |  ";
	   put_atomic_expr_rule x)
	(List.tl sut_out) ;
      put ("\n      | _ -> None \n\n"); 
      
       (*
       ** Defines sut_in_init and sut_out_init that provide fake initial
       ** values to input and output tuples at ``boot'' time, i.e., when
       ** lurette starts. 
       *)
      put "let sut_in_init = (";
      put_fake_value (List.hd sut_in) ;
      List.iter 
	(fun x -> put ", "; put_fake_value x)
	(List.tl sut_in) ;
      put ")\n\n";

      put "let sut_out_init = (";
      put_fake_value (List.hd sut_out) ;
      List.iter 
	(fun x -> put ", "; put_fake_value x)
	(List.tl sut_out) ;
      put ")\n\n";

       (*
       ** Defines list_ae_to_sut_in which transform a list of atomic_expr 
       ** into a sut_in, i.e., a tuple of values.
       *)
      put "let (list_ae_to_sut_in: atomic_expr list -> sut_in) =\n" ;
      put "  fun list ->\n    match list with\n" ;
      put "        [" ;
      put (format_string_list "; " fael_in) ;
      put "] -> (" ;
      put (format_string_list ", " fvnl_in) ;
      put ")\n";
      put "      | _ -> assert false\n\n" ;


      (*
       ** Defines print_sut_in and print_sut_out.
       *)
      put "let my_string_of_bool = function true -> \"t\" | false -> \"f\" \n\n" ;

      put "let (print_sut_in: sut_in -> out_channel -> unit) =\n" ;
      put "  fun (" ;
      put (format_string_list ", " fvnl_in) ;
      put ") oc -> \n" ;
      List.iter2
	(fun x y -> put_printer x y; put ";\n")
	mltl_in
	fvnl_in ;
      put "    flush oc\n\n" ;

      put "let (print_sut_out: sut_out -> out_channel -> unit) =\n" ;
      put "  fun (" ;
      put (format_string_list ", " fvnl_out) ;
      put ") oc -> \n" ;
      List.iter2 
	(fun x y ->  put_printer x y; put ";\n")
	mltl_out
	fvnl_out ;
      put "    flush oc\n\n" ;
      
      close_out oc 


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

let (replace_bool_representation: alias list -> alias list) =
  (*  
   ** Lustre defines `_boolean' as an `int', but camlidl maps C `boolean'
   ** to the caml `bool' type. 
   *)
  fun ta -> 
    ("_boolean", "boolean")::(List.remove_assoc "_boolean" ta)
  

let main2 sut oracle =
  let sut_h = (sut ^ ".h") in
  let oracle_h = (oracle ^ ".h") in

  let (sut_m, sut_vi0, sut_vo0) = get_vn_and_ct_list sut_h in 
  let sut_alias0 = get_typedef_alias sut_h in
  let sut_alias = replace_bool_representation sut_alias0 in
  let sut_vi = replace_ct_by_their_alias sut_vi0 sut_alias in
  let sut_vo = replace_ct_by_their_alias sut_vo0 sut_alias in
    
  let (oracle_m, oracle_vi0, oracle_vo0) = get_vn_and_ct_list oracle_h in 
  let oracle_alias0 = get_typedef_alias oracle_h in
  let oracle_alias = replace_bool_representation oracle_alias0 in
  let oracle_vi = replace_ct_by_their_alias oracle_vi0 oracle_alias in
  let oracle_vo = replace_ct_by_their_alias oracle_vo0 oracle_alias in
    
   (*
   ** Sorts variables lexicographically w.r.t. to their names.
   *)
  let (sort_vars:  vn_ct list -> vn_ct list) =
    fun var_list -> 
      List.sort (fun (vn1, t1) (vn2, t2) -> compare vn1 vn2) var_list 
  in
  let sut_vi_ord = sort_vars sut_vi in
  let sut_vo_ord = sort_vars sut_vo in
  let oracle_vi_ord = List.append sut_vi_ord sut_vo_ord in
  let oracle_vi_ord_decl = sort_vars oracle_vi in
  let sut_vars_ord = sort_vars (List.append sut_vi sut_vo) in
    
     (* 
     ** Aborts if the variables are inconsistent in the sut and in the oracle.
     *)
    (match check_var_type sut_vars_ord oracle_vi_ord_decl oracle_vo with
	 Ok -> () | Error(err_msg) -> failwith err_msg );
    
    generate_stub_c sut_m "sut" sut_vi_ord sut_vo_ord ; 
    generate_idl sut_m "sut" sut_vi_ord sut_vo_ord ;

    generate_stub_c oracle_m "oracle" oracle_vi_ord oracle_vo ; 
    generate_idl oracle_m "oracle" oracle_vi_ord oracle_vo ;

     (*
     ** We need to call camlidl now in order to get the ocaml types of the sut.
     *)
    if ((Sys.command ("echo \"camlidl -header sut_idl_stub.idl ...\" ;" ^
		      " /home/jahier/sun/bin/camlidl -header sut_idl_stub.idl ")) <> 0)  
    then print_string (" Can't call camlidl on sut_idl_stub.idl; " ^
		       "is camlidl in your path? Does sut_idl_stub.idl exist?\n\n") 
    else print_string "     ... ok\n";

    generate_lurette_stub_file (get_ml_type sut_vi_ord sut_vo_ord)

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

let usage = ("\n\nusage: gen_stub <sut> <oracle> \n\twhere <sut> " ^
	     " (reps <oracle>) is the name of the System Under Test C " ^
	     " file\n\t(resp the oracle file) without its extension.\n ")


let (main : unit -> 'a) =  
  fun _ ->  
    try 
      let sut = Sys.argv.(1) in
      let oracle = Sys.argv.(2) in
	main2 sut oracle 
    with Invalid_argument(_) -> 
      print_string usage 
      | Sys_error(errMsg) -> 
	  print_string ("\n*** " ^ errMsg ^ "\n") ; 
	  print_string usage 
      | ecxp -> 
	  raise ecxp
;;	  

main ();;