Add a --alice options to luc2c to interface lucky and Alice.

source/Makefile.luc2c

@@ -52,7 +52,6 @@ SOURCES_OCAML = \
           $(HERE)/error.ml \
           $(HERE)/version.ml \
           $(HERE)/util.ml \
-          $(HERE)/util2.ml \
           $(HERE)/graphUtil.ml \
           $(HERE)/graphUtil.mli \
           $(HERE)/sol_nb.mli \
@@ -113,6 +112,7 @@ SOURCES_OCAML = \
           $(HERE)/fGen.ml  \
 \
           $(HERE)/luciole.ml \
+          $(HERE)/luc2alice.ml \
           $(HERE)/luc2c.ml
 
 ifdef MLONLY

source/fGen.ml

@@ -103,7 +103,7 @@ let rec (wt_list_to_cont : Var.env_in -> Prog.state -> wt_cont list ->
 	        | wt2, f2, n -> 
 		    let fgen' = 
 		      Cont (fun () -> 
-			call_cont (wt_list_to_cont input state (wt2::wtl') facc nl fgen))
+			      call_cont (wt_list_to_cont input state (wt2::wtl') facc nl fgen))
 		    in
 		      wt_list_to_cont input state wtl' f2 (n::nl) fgen'
 and
@@ -111,28 +111,26 @@ and
       Exp.formula -> wt_cont -> wt_cont * formula * LucParse.node) = 
   fun input state facc cont ->
     let _ = if debug then (print_string "XXX choose_one_formula_atomic\n"; flush stdout) in
-      if cont = WFinish then
-        WFinish, False, ""
-      else
-      if cont = WStop str then
-        WStop str, True, ""
-      else
-        let (cont', f, n) = call_wt_cont cont in
-        let _ = if debug then (print_string ("XXX "^ n ^ "\n"); flush stdout) in
-        let facc' = 
-	  match f,facc with
-	      True, True -> True
-	    | True, f -> f
-	    | f, True -> f
-	    | _,_ -> And(f,facc) 
-        in
-        let ctx_msg = Prog.ctrl_state_to_string_long state.d.ctrl_state in
-	  if 
-	    (Solver.is_satisfiable input state.d.memory state.d.verbose ctx_msg facc' "")
-	  then
-	    (cont', facc', n)
-          else 
-	    choose_one_formula_atomic input state facc cont'
+      match cont with
+        | WFinish ->  WFinish, False, ""
+        | WStop _ ->  cont, True, ""
+        | WCont _ ->
+            let (cont', f, n) = call_wt_cont cont in
+            let _ = if debug then (print_string ("XXX "^ n ^ "\n"); flush stdout) in
+            let facc' = 
+	      match f,facc with
+	          True, True -> True
+	        | True, f -> f
+	        | f, True -> f
+	        | _,_ -> And(f,facc) 
+            in
+            let ctx_msg = Prog.ctrl_state_to_string_long state.d.ctrl_state in
+	      if 
+	        (Solver.is_satisfiable input state.d.memory state.d.verbose ctx_msg facc' "")
+	      then
+	        (cont', facc', n)
+              else 
+	        choose_one_formula_atomic input state facc cont'
 
 
 and (wt_to_cont : Var.env_in -> Prog.state -> wt -> wt_cont -> wt_cont) =

source/luc2alice.ml

+(*-----------------------------------------------------------------------
+** Copyright (C) - Verimag.
+** This file may only be copied under the terms of the GNU Library General
+** Public License
+**-----------------------------------------------------------------------
+**
+** File: luc2c.ml
+** Author: jahier@imag.fr
+**
+** Generates C files to call Lucky from Alice.
+**
+*)
+
+
+(* put all args in one structure  *)
+type alice_args = { 
+  env_name : string;
+  alice_module_name : string ;
+  seed : int option;
+  env_in_vars : Exp.var list;
+  env_out_vars : Exp.var list;
+}
+
+
+(********************************************************************)
+
+(* let (cast : Type.t -> string) = function *)
+(*   | Type.BoolT -> "(_bool*)" *)
+(*   | Type.IntT  -> "(_int*)" *)
+(*   | Type.FloatT -> "(_real*)" *)
+(*   | Type.UT _ -> assert false *)
+(*  *)
+(*  *)
+(* let (declarer_importeurs : string -> Exp.var list -> string) = *)
+(* fun an vars  ->  *)
+(*   let make_one_decl var = *)
+(*     let vn = Var.name var in *)
+(*       ("    DeclarerImporteur(DaxFlags32( Nv3BaseDeModule::cEchangeSync ),\" "^ *)
+(*          an^":"^vn^":\", "^(cast (Var.typ var))^"&mCtx->_"^vn^");\n") *)
+(*   in *)
+(*   let items = List.map make_one_decl vars in *)
+(*      "" ^ (String.concat "" items) *)
+(*  *)
+(* let (declarer_exporteurs : string -> Exp.var list -> string) = *)
+(*   fun an vars  ->  *)
+(*     let make_one_decl var =  *)
+(*       let vn = Var.name var in *)
+(*         ("    DeclarerExporteur(DaxFlags32( Nv3BaseDeModule::cEchangeSync ),\" "^ *)
+(*            an^":"^vn^":\", "^(cast (Var.typ var))^" &mCtx->_"^vn^");\n") *)
+(*     in *)
+(*     let items = List.map make_one_decl vars in *)
+(*       "" ^ (String.concat "" items) *)
+(********************************************************************)
+
+
+let (lucky_seed : int option -> string) =
+  function
+    | Some i -> ("lucky_set_seed("^(string_of_int i)^");\n")
+    | None -> ""
+
+(********************************************************************)
+
+let (define_output_proc : string -> Exp.var list -> string) =
+  fun n vl ->
+    let f var =
+      let vn = Var.name var in
+      let t = Type.to_cstring  (Var.typ var) in
+      ("  void  "^n^"_O_"^vn^"("^n^"_ctx* ctx, "^t^" value){ ctx->_"^vn^" = value; };\n")
+    in
+      (String.concat "" (List.map f vl))
+
+
+(********************************************************************)
+(*
+** Variable names and types lists
+*)
+
+let soi = string_of_int
+
+let (to_char: Type.t -> string) =
+  function
+  | Type.BoolT -> "_bool_type_char"
+  | Type.IntT  -> "_int_type_char"
+  | Type.FloatT -> "_real_type_char"
+  | Type.UT _ -> assert false
+
+let (gen_alice_var_tab : string -> string -> Exp.var list -> string) =
+  fun alice_name name vl ->
+    let n = List.length vl in
+
+    let f (i,acc) var = i+1,acc ^
+      "  "^name^".tab[" ^ (soi i) ^ "].var_name = \"" ^ (Var.name var) ^ "\";\n" ^
+      "  "^name^".tab[" ^ (soi i) ^ "].var_type = " ^ (to_char(Var.typ var)) ^ ";\n" ^
+      "  "^name^".tab[" ^ (soi i) ^ "].var_adrs = &(mCtx->_" ^ (Var.name var)^ ");\n"
+    in
+      ("
+  "^name^".size="^(soi n)^";
+  "^name^".tab = new var_info["^(soi n)^"];\n" ^
+         (snd (List.fold_left f (0,"") vl))) 
+
+
+(********************************************************************)
+
+
+let (gen_alice_stub : alice_args -> string) =
+  fun args -> 
+    let alice_name = args.alice_module_name 
+    and fn = args.env_name 
+    and in_vars  = args.env_in_vars
+    and out_vars = args.env_out_vars
+    in
+
+("
+#include \""^alice_name^".h\"
+
+// Those procedures are used by the Lucky runtime to set the lucky outputs
+extern \"C\"
+{
+" ^ (define_output_proc fn out_vars) ^ "}
+
+int "^alice_name^"::instance_cpt=0;
+static structTab inputs;
+static structTab outputs;
+static structTab memories;
+
+
+/*  Build an instance of the Class "^alice_name^" */
+"^alice_name^"::"^alice_name^"()
+{  
+  instance_nb = instance_cpt++;
+  mCtx = rcm_env_new_ctx((void *) instance_nb);
+
+ // Inputs"
+ ^ (gen_alice_var_tab alice_name "inputs" in_vars)  ^
+"
+   // Outputs"
+ ^ (gen_alice_var_tab alice_name "outputs" out_vars) ^
+"
+   // Memories"
+ ^ (gen_alice_var_tab alice_name "memories" []) ^
+"
+}
+
+/* Remove an instance of the Class "^alice_name^" */
+"^alice_name^"::~"^alice_name^"()
+{
+  // rcm_env_delete_ctx(mCtx);
+  delete[] inputs.tab;
+  delete[] outputs.tab;
+  delete[] memories.tab;
+
+}
+
+/* Get a new object (for dynamic libs) */
+"^alice_name^"* "^alice_name^"::Factory () 
+{ 
+  return new "^alice_name^"();
+}
+
+/* Initialisation */
+void "^alice_name^"::Initialisation()
+{
+  //"^fn^"_reset_ctx(mCtx);" ^ (lucky_seed args.seed) ^ "
+}
+
+/* Step */
+void "^alice_name^"::Process()
+{
+  "^fn^"_step(mCtx, step_inside);
+}
+
+/* Terminate */
+void "^alice_name^"::Terminate()
+{
+  // pourquoi ne pas faire 'delete toto' plutot que 'toto.Terminate()' ? 
+  // Quand est appelé cette méthode finalement ?
+}
+
+/* Returns the Lucky input vars */
+structTab* Inputs() {
+   { return  &inputs;};
+}
+
+/* Returns the Lucky output vars */
+structTab* Outputs() {
+  { return  &outputs;};
+}
+
+/* Returns the Lucky output memories */
+structTab* Memories() {
+   { return  &memories;};
+}
+
+
+")
+
+
+let (gen_alice_stub_c : alice_args -> unit) =
+  fun args -> 
+    let oc = open_out (args.alice_module_name ^ ".cc") in
+    let put s = output_string oc s in
+    let putln s = output_string oc (s^"\n") in
+    let rec putlist = function
+	[] -> ()
+      |	[x] -> put x
+      | x::l' -> put x; put ", "; putlist l'
+    in 
+      putln (Util.entete "// ");
+      putln (gen_alice_stub args)
+
+
+let (gen_alice_stub_h : alice_args -> unit) =
+  fun args -> 
+    let amn = args.alice_module_name in
+    let oc = open_out (amn ^ ".h") in
+    let put s = output_string oc s in
+    let putln s = output_string oc (s^"\n") in
+    let rec putlist = function
+	[] -> ()
+      |	[x] -> put x
+      | x::l' -> put x; put ", "; putlist l'
+    in 
+    let fn = args.env_name in
+      putln (Util.entete "// ");
+      putln ("
+extern \"C\"
+{
+	#include \""^fn^".h\"
+}
+
+class "^amn^";
+
+#ifndef _real_type_char
+#define _real_type_char 'd'
+#endif
+#ifndef _int_type_char
+#define _int_type_char 'i'
+#endif
+#ifndef _bool_type_char
+#define _bool_type_char 'b'
+#endif
+
+
+
+struct var_info {
+  const char *var_name;
+  char  var_type;
+  void *var_adrs;
+};
+
+struct structTab {
+  int size;
+  var_info* tab;
+};
+
+
+class "^amn^" {
+
+  _"^fn^"_ctx * mCtx;
+  static structTab inputs;
+  static structTab outputs;
+  static structTab memories;
+  static int instance_cpt; 
+  int instance_nb;
+
+ public :      
+
+  "^amn^"();
+  ~"^amn^"();
+  static "^amn^"*  Factory();
+  void Initialisation();
+  void Process();
+  void	Terminate()   ;
+  structTab* Inputs();
+  structTab* Outputs();
+  structTab* Memories();
+};
+")

source/luc2c.ml

@@ -17,7 +17,7 @@ open Exp
 open Prog
 open Type
 
-type gen_mode = C | Lustre | Scade
+type gen_mode = C | Lustre | Scade | Alice
 type step_mode = Inside | Edges | Vertices
 
 let step_mode_to_str = function 
@@ -528,7 +528,7 @@ let usage = (usage_begin ^ usage_end)
 let more_usage = (usage_begin ^ "
  luc2c generates C stub code in a way that is very similar to ec2c.
 
- For example, \"luc2c f.luc\" generates \"f.\" and \"f.h\" that defines 
+ For example, \"luc2c f.luc\" generates \"f.c\" and \"f.h\" that defines 
  the type foo_ctx as well as the following functions:
 
     foo_ctx* foo_new_ctx(void* client_data) // a function to create a lucky process
@@ -546,13 +546,13 @@ let more_usage = (usage_begin ^ "
     ...
 
  The final executable needs to be linked in with the following C libs:
-      -lluc4c_nc -llucky_nc // distributed with luc2ec
+      -lluc4c_nc -llucky_nc // distributed with luc2c
       -lgmp                 // the Gnu Multi-precision Library
       -lm -ldl -lstdc++     // ...
  
  The lib path should (of course) contains a path to those libs. Moreover,
  the include path should contain a path to the \"luc4c_stubs.h\" header file,
- which is also distributed with luc2ec.
+ which is also distributed with luc2c.
 
 " ^ usage_end)
 
@@ -588,6 +588,11 @@ let rec speclist =
       (fun str -> flag.gen_mode <- Lustre;flag.calling_module_name <- str),
     "";
 
+    "--alice",  Arg.String
+      (fun str -> flag.gen_mode <- Alice;flag.calling_module_name <- str),
+    "Generate C++ code to be called from Alice";
+
+
     "--seed", Arg.String (fun str -> flag.seed <- Some (int_of_string str)),
     "\tTo set a seed to the lucky random generator (with --lustre option))";
 
@@ -658,8 +663,8 @@ let rec (main : unit -> 'a) =
     else
       ( try
 	  Arg.parse speclist
-	    (fun s -> flag.env <- (List.append flag.env [s]))
-	    usage
+	      (fun s -> flag.env <- (List.append flag.env [s]))
+	      usage
 	with
 	    Failure(e) ->
 	      print_string e;
@@ -684,11 +689,25 @@ let rec (main : unit -> 'a) =
 	let fn = build_file_name env_list in
 	  gen_c_file fn state.s.in_vars state.s.out_vars state.s.loc_vars;
 	  gen_h_file fn state.s.in_vars state.s.out_vars state.s.loc_vars;
-	  if flag.gen_mode = Lustre then (
-	    gen_lustre_ext_func_c fn state.s.in_vars state.s.out_vars ;
-	    gen_lustre_ext_func_h fn state.s.in_vars state.s.out_vars ;
-	    gen_lustre_ext_h fn ;
-	  );
+          
+          (match flag.gen_mode with
+             | Lustre ->
+	         gen_lustre_ext_func_c fn state.s.in_vars state.s.out_vars ;
+	         gen_lustre_ext_func_h fn state.s.in_vars state.s.out_vars ;
+	         gen_lustre_ext_h fn 
+	     | Alice ->
+                 let alice_args = {
+                   Luc2alice.env_name = fn;
+                   Luc2alice.alice_module_name = flag.calling_module_name ;
+                   Luc2alice.seed = flag.seed;
+                   Luc2alice.env_in_vars = state.s.in_vars ;
+                   Luc2alice.env_out_vars = state.s.out_vars ;
+
+                 }
+                 in
+                   Luc2alice.gen_alice_stub_c alice_args;
+                   Luc2alice.gen_alice_stub_h alice_args;
+          );
 	  if flag.luciole then
 	    (
 	      let var_to_vn_ct v =

source/util.ml

@@ -837,10 +837,11 @@ let entete comment =
   )
   and hostname = Unix.gethostname ()
   in
-    (comment ^ " Automatically generated by "^Sys.argv.(0)^
-       " version "^Version.str^" (" ^Version.sha^") .\n" ^
-       comment ^ " Generated on " ^ hostname ^ 
-       " the " ^ date ^ " at " ^ time_str ^ "\n\n")
+    (comment ^ " Automatically generated by "^ 
+       Sys.executable_name^" version "^Version.str^" (" ^Version.sha^")\n" ^
+       comment ^ " on " ^ hostname ^ 
+       " the " ^ date ^ " at " ^ time_str ^ "\n" ^
+       comment^(String.concat " " (Array.to_list Sys.argv))^ "\n\n")
 
 
 let generate_up_and_down_macro dir =