diff --git a/src/lv6MainArgs.ml b/src/lv6MainArgs.ml
index 13867d4b0da826aea890d5374efb747b44d7dcec..6da27780565b8a686167302532cb708994639154 100644
--- a/src/lv6MainArgs.ml
+++ b/src/lv6MainArgs.ml
@@ -1,4 +1,4 @@
-(* Time-stamp: <modified the 13/12/2013 (at 11:46) by Erwan Jahier> *)
+(* Time-stamp: <modified the 17/04/2014 (at 15:03) by Erwan Jahier> *)
 (*
 Le manager d'argument adapté de celui de lutin, plus joli
 N.B. solution un peu batarde : les options sont stockées, comme avant, dans Global,
@@ -32,6 +32,7 @@ type t = {
   mutable oc :  Pervasives.out_channel;
   mutable tlex :  bool;
   mutable exec :  bool;
+  mutable gen_c :  bool;
   mutable rif  :  bool;
   mutable gen_ocaml :  bool;
   mutable precision : int option;
@@ -84,6 +85,7 @@ let (make_opt : unit -> t) =
       oc =  Pervasives.stdout;
       tlex =  false;
       exec =  false;
+      gen_c =  false;
       rif  =  false;
       gen_ocaml =  false;
       precision = None;
@@ -210,6 +212,12 @@ let mkoptab (opt:t) : unit = (
         opt.exec <- true))
       ["interpret the program using RIF conventions for I/O (experimental)."]
     ;
+    mkopt opt
+      ["--to-c"; "-2c"]
+      (Arg.Unit (fun _ ->
+        opt.gen_c <- true))
+      ["generate C code (work in progress)."]
+    ;
     mkopt opt
       ["-rif"]
       (Arg.Unit(function s -> opt.rif <- true))
diff --git a/src/lv6MainArgs.mli b/src/lv6MainArgs.mli
index a6183eba7707f4921fc3caf77a1484b904f996cb..b7dbee86216310c70cd38d20d363d5680bb6de0e 100644
--- a/src/lv6MainArgs.mli
+++ b/src/lv6MainArgs.mli
@@ -28,6 +28,7 @@ type t = {
   mutable oc :  Pervasives.out_channel;
   mutable tlex :  bool;
   mutable exec :  bool;
+  mutable gen_c :  bool;
   mutable rif :  bool;
   mutable gen_ocaml :  bool;
   mutable precision : int option;
diff --git a/src/main.ml b/src/main.ml
index 1fefa6b832bf6921809749f8424bbdf7f91a1767..d9c712944ffad1aa54ca128f4ef0ed675409818a 100644
--- a/src/main.ml
+++ b/src/main.ml
@@ -1,4 +1,4 @@
-(* Time-stamp: <modified the 19/03/2014 (at 09:28) by Erwan Jahier> *)
+(* Time-stamp: <modified the 17/04/2014 (at 15:20) by Erwan Jahier> *)
 
 open Verbose
 open AstV6
@@ -204,7 +204,7 @@ let main () = (
       gen_autotest_files lic_prg main_node opt
     else if opt.gen_ocaml then
       GenOcamlGlue.f Sys.argv opt
-    else if opt.exec then
+    else if (opt.exec || opt.gen_c) then
       (match main_node with
         | None -> (
           let name = find_a_node opt in
@@ -213,9 +213,14 @@ let main () = (
             print_string ("WARNING: No main node is specified. I'll try with " ^ name ^"\n");
             flush stdout;
             info "Start compiling to soc...\n";
-            let msk, zesoc = Lic2soc.f lic_prg nk in
-            info "Soc Compilation done. Start interpreting soc...\n";
-            SocExec.f opt zesoc msk
+            let msk,zesoc  = Lic2soc.f lic_prg nk in
+            info "Soc Compilation done.\n";
+            if opt.gen_c then (
+              info "Start generating C code...\n";
+              Soc2c.f opt zesoc);
+            if opt.exec then (
+              info "Start interpreting soc...\n";
+              SocExec.f opt zesoc msk)          
           ) else (
             print_string ("Error: no node is specified, cannot exec.\n");
             flush stdout;
@@ -225,9 +230,16 @@ let main () = (
         | Some main_node -> 
           info "Start compiling to soc...\n";
           let msk, zesoc = Lic2soc.f lic_prg (Lic.node_key_of_idref main_node) in
-          info "Soc Compilation done. Start interpreting soc...\n";
-          SocExec.f opt zesoc msk
-      ) else (   
+
+          info "Soc Compilation done. \n";
+          if opt.gen_c then (
+            info "Start generating C code...\n";
+            Soc2c.f opt zesoc);
+
+          if opt.exec then (
+            info "Start interpreting soc...\n";
+            SocExec.f opt zesoc msk)
+      ) else (
         LicPrg.to_file opt lic_prg main_node
        );
 
diff --git a/src/soc.ml b/src/soc.ml
index 8c6a252f6ec9a050d251dde8310164a747410a5e..80307730c60396f74bfb39072a361a70d63b9702 100644
--- a/src/soc.ml
+++ b/src/soc.ml
@@ -1,4 +1,4 @@
-(* Time-stamp: <modified the 09/12/2013 (at 11:17) by Erwan Jahier> *)
+(* Time-stamp: <modified the 23/04/2014 (at 10:17) by Erwan Jahier> *)
 
 (** Synchronous Object Component *)
 
diff --git a/src/soc2c.ml b/src/soc2c.ml
new file mode 100644
index 0000000000000000000000000000000000000000..5258e6f5c3d0e0432d0052b0a71ced2d7beaffc4
--- /dev/null
+++ b/src/soc2c.ml
@@ -0,0 +1,215 @@
+(* Time-stamp: <modified the 25/04/2014 (at 16:55) by Erwan Jahier> *)
+
+
+(* let put (os: out_channel) (fmt:('a, unit, string, unit) format4) : 'a = *)
+(* 	Printf.kprintf (fun t -> output_string os t) fmt *)
+
+open Printf
+
+let rec (type_to_string : Data.t -> string) = 
+  fun v -> 
+    let str =
+      match v with
+        | Bool -> "_boolean"
+        | Int -> "_integer"
+        | Real-> "_real"
+        | Extern s -> s ^ "(*extern*)"
+        | Enum  (s, sl) -> s 
+        | Struct (sid,_) -> sid ^ "(*struct*)"
+        | Array (ty, sz) -> Printf.sprintf "%s^%d" (type_to_string ty) sz 
+        | Alpha nb -> assert false
+    in
+    str
+
+let colcol = Str.regexp "::"
+let id2s id =
+	match Str.split colcol id with
+	| [s] -> s
+	| [m;s] -> if Lv6MainArgs.global_opt.Lv6MainArgs.no_prefix then s else m^"_"^s 
+	| _ -> assert false
+
+
+(* Soc printer *)
+type 'a soc_pp = {
+  hfmt:  ('a, unit, string, unit) format4 -> 'a;
+  cfmt:  ('a, unit, string, unit) format4 -> 'a;
+  cput : string -> unit;
+  hput : string -> unit;
+  soc: Soc.t
+}
+
+let rec (type_to_short_string : Data.t -> string) = 
+  fun v -> 
+    let str =
+      match v with
+        | Data.Bool -> "b"
+        | Data.Int -> "i"
+        | Data.Real-> "r"
+        | Data.Extern s -> s 
+        | Data.Enum  (s, sl) -> s 
+        | Data.Struct (sid,_) -> sid
+        | Data.Array (ty, sz) -> Printf.sprintf "%sp%d" (type_to_string ty) sz 
+        | Data.Alpha nb ->
+        (* On génère des "types" à la Caml : 'a, 'b, 'c, etc. *)
+          let a_value = Char.code('a') in
+          let z_value = Char.code('z') in
+          let str =
+            if (nb >= 0 && nb <= (z_value - a_value)) then
+              ("'" ^ (Char.escaped (Char.chr(a_value + nb))))
+            else
+              ("'a" ^ (string_of_int nb))
+          in
+          str
+    in
+    str
+
+let (ctx_name : Soc.key -> string) =
+  fun (name,tl,_) -> 
+    let l = List.map type_to_short_string tl in
+    Printf.sprintf "%s_%s_ctx" (id2s name) (String.concat "" l)
+
+let (step_name : Soc.key -> string -> string) =
+  fun (soc_name,tl,_) sm -> 
+    let l = List.map type_to_short_string tl in
+    sprintf "%s_%s_%s" (id2s soc_name)  (String.concat "" l) sm
+
+
+let (string_of_soc_key : Soc.key -> string) =
+  fun (name,_,_) ->  (id2s name)
+
+let string_of_flow_decl (id, t) = Printf.sprintf "   %s %s;\n" (type_to_string t) id 
+
+let (mem_interface : Soc.t -> string -> bool) =
+  fun soc id -> 
+    let ins,outs = soc.profile in
+    List.mem_assoc id ins || List.mem_assoc id outs
+
+let rec (string_of_var_expr: Soc.t -> Soc.var_expr -> string) = 
+  fun soc -> function
+    | Const(id, _) | Var (id,_) -> if not (mem_interface soc id) then id else
+        sprintf "ctx->%s" id
+    | Field(f, id,_) -> sprintf "%s.%s" (string_of_var_expr soc f) id
+    | Index(f, index,_) -> sprintf "%s[%i]" (string_of_var_expr soc f) index
+    | Slice(f,fi,la,st,wi,vt) -> sprintf "%s[%i..%i step %i]; // XXX fixme!\n" 
+      (string_of_var_expr soc f) fi la st
+
+let (gao2c : 'a soc_pp -> Soc.gao -> unit) =
+  fun sp gao -> 
+    let string_of_var_expr_list vel =
+      let vel = List.map (string_of_var_expr sp.soc) vel in
+      String.concat "," vel
+    in
+    match gao with
+      | Case(id, id_gao_l) ->  assert false
+      | Call(vel_out, Assign, vel_in) ->  
+        let vel_in_str  = string_of_var_expr_list vel_in in
+        let vel_out_str = string_of_var_expr_list vel_out in
+        let str = sprintf "   %s = %s;\n" vel_out_str vel_in_str in
+        sp.cput str
+        
+      | Call(vel_out, Method((inst_name,sk),sname), vel_in) ->  
+(*         let vel_in_str  = string_of_var_expr_list vel_in in *)
+(*         let vel_out_str = string_of_var_expr_list vel_out in *)
+        let vel_str = string_of_var_expr_list (vel_in@vel_out) in
+        let str = sprintf "   %s(ctx->%s,%s); //method call\n" (* XXX fixme ! *)
+          (step_name sk sname) (id2s inst_name) vel_str in
+        sp.cput str
+
+
+      | Call(vel_out, Procedure sk, vel_in) ->
+        let vel_in_str  = string_of_var_expr_list vel_in in
+        let vel_out_str = string_of_var_expr_list vel_out in
+        let sk = (string_of_soc_key sk) in
+        let str = sprintf "   %s = %s(%s); //procedure call\n" vel_out_str sk vel_in_str in
+        sp.cput str
+
+
+
+let (step2c : 'a soc_pp -> Soc.step_method -> unit) =
+  fun sp sm -> 
+    let cname = ctx_name sp.soc.key in
+    let sm_str = SocUtils.string_of_method sp.soc sm in
+    let sname = step_name sp.soc.key sm.name in
+(*     sp.put (sprintf "/* %s */\n" sm_str); *)
+    sp.cfmt "void %s(%s* ctx){\n"  sname cname;    
+    (match sm.impl with
+      | Predef -> sp.cput "   //xxx predef_finish_me!"
+      | Gaol(vl, gaol) -> 
+(*         List.iter (fun v -> sp.cput (string_of_flow_decl v)) vl ;         *)
+(*         sp.cput "\n"; *)
+        List.iter (gao2c sp) gaol
+(*         of var list * gao list  (* local vars + body *) *)
+      | Iterator(it,it_soc,s) -> assert false
+      | Boolred(i,j,k) -> assert false
+      | Condact(k,el) -> assert false
+    );
+    sp.cput (sprintf "\n} // End of %s\n\n" sname)
+    
+
+let (soc2c: out_channel -> out_channel -> Soc.t -> unit) = 
+  fun hfile cfile soc -> 
+	 let hfmt fmt = Printf.kprintf (fun t -> output_string hfile t) fmt in
+	 let cfmt fmt = Printf.kprintf (fun t -> output_string cfile t) fmt in
+    let hput str = output_string hfile str in
+    let cput str = output_string cfile str in
+    let put str = cput str; hput str in
+    let fmt f str = cfmt f str; hfmt f str in
+    let string_of_instance (id,sk) = 
+      let (sk_id,tl,init_opt) = sk in
+      let init = match init_opt with
+        | Soc.Nomore -> ""
+        | Soc.Slic(_,_,_) -> assert false (* fixme *)
+        | Soc.MemInit(ve) -> Printf.sprintf " = %s" (string_of_var_expr soc ve) 
+      in
+      Printf.sprintf "   %s %s%s;\n" (ctx_name sk) (id2s id) init
+    in
+    
+    let name, _,_ = soc.key in
+    let name = id2s name in
+    let il,ol = soc.profile in
+    let sp = { hfmt = hfmt; cfmt=cfmt; hput = hput; cput = cput; soc = soc } in
+    let ctx_name = ctx_name soc.key in
+    
+    fmt "/* %s */\ntypedef struct {\n   /*INPUTS*/\n" ctx_name;
+    List.iter (fun v -> put (string_of_flow_decl v)) il ;
+
+    put "   /*OUTPUTS*/\n";
+    List.iter (fun v -> put (string_of_flow_decl v)) ol ;
+
+    (match soc.have_mem with
+      | None -> ()
+      | Some t -> 
+        put "   /*Memory cell*/\n";
+        fmt "   %s mem_pre;\n" (Data.type_to_string t) ;
+    );
+
+    if soc.instances <> [] then put "   /*INSTANCES*/\n";
+    List.iter (fun inst -> put (string_of_instance inst)) soc.instances;
+    fmt "} %s;\n\n" ctx_name; 
+
+    cfmt "// Step function(s) for %s\n" ctx_name;
+    List.iter (step2c sp) soc.step;
+    ()
+
+
+
+(* The entry point for lus2lic --to-c *)
+let (f : Lv6MainArgs.t -> Soc.tbl -> unit) =
+  fun args soc -> 
+    let socs = Soc.SocMap.bindings soc in
+    let socs = snd (List.split socs) in 
+(* XXX que fait-on pour les soc predef ? *)
+(*     let _, socs = List.partition is_predef socs in *)
+    let hfile = "hfile.h" in
+    let cfile = "cfile.c" in
+    let occ = open_out cfile in
+    let och = open_out hfile in
+
+    Lv6util.dump_entete stdout ;
+    List.iter (soc2c och occ) socs;
+    flush occ; close_out occ;
+    flush och; close_out och;
+    Printf.printf "%s and %s have been generated.\n" hfile cfile;
+
+    (* XXX remove me: *) List.iter (soc2c stdout stdout) socs
+
diff --git a/src/soc2c.mli b/src/soc2c.mli
new file mode 100644
index 0000000000000000000000000000000000000000..621fc9a88cab2779d1bb49bc63d8bfcbadec2e5a
--- /dev/null
+++ b/src/soc2c.mli
@@ -0,0 +1,4 @@
+(* Time-stamp: <modified the 17/04/2014 (at 15:20) by Erwan Jahier> *)
+
+(* The entry point for lus2lic -toC *)
+val f : Lv6MainArgs.t -> Soc.tbl -> unit
diff --git a/src/soc2cPredef.ml b/src/soc2cPredef.ml
new file mode 100644
index 0000000000000000000000000000000000000000..a33e3079f973ff2140065a97ea203b747534df5c
--- /dev/null
+++ b/src/soc2cPredef.ml
@@ -0,0 +1,377 @@
+(* Time-stamp: <modified the 23/04/2014 (at 09:06) by Erwan Jahier> *)
+
+
+
+(*
+let (lustre_plus : ctx -> ctx) =
+  fun ctx -> 
+    let l = [get_val "x" ctx; get_val "y" ctx] in
+    let (vn,vv) =
+      match l with
+        | [I x1; I x2] -> "z"::ctx.cpath,I(x1+x2)
+        | [F i1; F i2] -> "z"::ctx.cpath,F(i1+.i2)
+        | [U; _] | [_;U] -> "z"::ctx.cpath,U
+        | [v1;v2]  ->  type_error v1 v2; "z"::ctx.cpath,U
+        | _ -> assert false
+    in
+    { ctx with s = sadd ctx.s vn vv }
+
+let lustre_times ctx =
+  let (vn,vv) = 
+    match ([get_val "x" ctx; get_val "y" ctx]) with
+      | [I x1; I x2] -> "z"::ctx.cpath,I(x1 * x2)
+      | [F x1; F x2] -> "z"::ctx.cpath,F(x1 *. x2)
+      | [U; _] | [_;U] -> "z"::ctx.cpath,U
+      | [v1;v2]  ->  type_error v1 v2; "z"::ctx.cpath,U
+      | _  -> assert false
+  in
+  { ctx with s = sadd ctx.s vn vv }
+
+
+let lustre_div ctx =
+  let (vn,vv) = 
+    match ([get_val "x" ctx; get_val "y" ctx]) with
+      | [I x1; I x2] -> "z"::ctx.cpath,I(x1 / x2)
+      | [F x1; F x2] -> "z"::ctx.cpath,F(x1 /. x2)
+      | [U; _] | [_;U] -> "z"::ctx.cpath,U
+      | [v1;v2]  ->  type_error v1 v2;"z"::ctx.cpath,U
+      | _  -> assert false
+  in
+  { ctx with s = sadd ctx.s vn vv }
+
+let lustre_slash ctx =
+  let (vn,vv) = 
+    match ([get_val "x" ctx; get_val "y" ctx]) with
+      | [I x1; I x2] -> "z"::ctx.cpath,I(x1 / x2)
+      | [F x1; F x2] -> "z"::ctx.cpath,F(x1 /. x2)
+      | [U; _] | [_;U] -> "z"::ctx.cpath,U
+      | [v1;v2]  ->  type_error v1 v2;"z"::ctx.cpath,U
+      | _  -> assert false
+  in
+  { ctx with s = sadd ctx.s vn vv }
+
+
+let lustre_minus ctx =
+  let (vn,vv) = 
+    match ([get_val "x" ctx; get_val "y" ctx]) with
+      | [I x1; I x2] -> "z"::ctx.cpath,I(x1 - x2)
+      | [F x1; F x2] -> "z"::ctx.cpath,F(x1 -. x2)
+      | [U; _] | [_;U] -> "z"::ctx.cpath,U
+      | [v1;v2]  ->  type_error v1 v2; "z"::ctx.cpath,U
+      | [v1;v2]  ->  type_error v1 v2; "z"::ctx.cpath,U
+      | _  -> assert false
+  in
+  { ctx with s = sadd ctx.s vn vv }
+
+let lustre_mod ctx =
+  let (vn,vv) = 
+    match ([get_val "x" ctx; get_val "y" ctx]) with
+      | [I x1; I x2] -> "z"::ctx.cpath,I(x1 mod x2)
+      | [U; _] | [_;U] -> "z"::ctx.cpath,U
+      | [v1;v2]  ->  type_error v1 v2; "z"::ctx.cpath,U
+      | _  -> assert false
+  in
+  { ctx with s = sadd ctx.s vn vv }
+
+
+let lustre_eq ctx =
+  let (vn,vv) = 
+    match ([get_val "x" ctx; get_val "y" ctx]) with
+      | [U; _] | [_;U] -> "z"::ctx.cpath,U
+      | [x1; x2] -> "z"::ctx.cpath,B(x1 = x2)
+      | [v1;v2]  ->  type_error v1 v2; "z"::ctx.cpath,U
+      | _  -> assert false
+  in
+  { ctx with s = sadd ctx.s vn vv }
+
+let lustre_uminus ctx =
+  let (vn,vv) = 
+    match ([get_val "x" ctx]) with
+      | [I x1] -> "z"::ctx.cpath,I(- x1)
+      | [F x1] -> "z"::ctx.cpath,F(-. x1)
+      | [U; _] | [_;U] -> "z"::ctx.cpath,U
+      | [v1]  ->  type_error1 v1 "numeric";"z"::ctx.cpath,U
+      | _  -> assert false
+  in
+  { ctx with s = sadd ctx.s vn vv }
+
+let lustre_real2int ctx =
+  let (vn,vv) = 
+    match ([get_val "x" ctx]) with
+      | [F x1] -> "z"::ctx.cpath,I(int_of_float x1)
+      | [U] -> "z"::ctx.cpath,U
+      | [v1]  ->  type_error1 v1 "real";"z"::ctx.cpath,U
+      | _  -> assert false
+  in
+  { ctx with s = sadd ctx.s vn vv }
+
+
+let lustre_int2real ctx =
+  let (vn,vv) = 
+    match ([get_val "x" ctx]) with
+      | [I x1] -> "z"::ctx.cpath,F(float_of_int x1)
+      | [U] -> "z"::ctx.cpath,U
+      | [v1]  ->  type_error1 v1 "int";"z"::ctx.cpath,U
+      | _  -> assert false
+  in
+  { ctx with s = sadd ctx.s vn vv }
+
+
+let lustre_not ctx =
+  let (vn,vv) = 
+    match ([get_val "x" ctx]) with
+      | [B x1] -> "z"::ctx.cpath,B(not x1)
+      | [U] -> "z"::ctx.cpath,U
+      | [v1]  ->  type_error1 v1 "bool";"z"::ctx.cpath,U
+      | _  -> assert false
+  in
+  { ctx with s = sadd ctx.s vn vv }
+
+
+let lustre_lt ctx =
+  let (vn,vv) = 
+    match ([get_val "x" ctx; get_val "y" ctx]) with
+      | [U; _] | [_;U] -> "z"::ctx.cpath,U
+      | [x1; x2] -> "z"::ctx.cpath,B(x1 < x2)
+      | [v1;v2]  ->  type_error v1 v2; "z"::ctx.cpath,U
+      | _  -> assert false
+  in
+  { ctx with s = sadd ctx.s vn vv }
+ 
+let lustre_gt ctx =
+  let (vn,vv) = 
+    match ([get_val "x" ctx; get_val "y" ctx]) with
+      | [U; _] | [_;U] -> "z"::ctx.cpath,U
+      | [x1; x2] -> "z"::ctx.cpath,B(x1 > x2)
+      | [v1;v2]  ->  type_error v1 v2; "z"::ctx.cpath,U
+      | _  -> assert false
+  in
+  { ctx with s = sadd ctx.s vn vv }
+
+let lustre_lte ctx =
+  let (vn,vv) = 
+    match ([get_val "x" ctx; get_val "y" ctx]) with
+      | [U; _] | [_;U] -> "z"::ctx.cpath,U
+      | [x1; x2] -> "z"::ctx.cpath,B(x1 <= x2)
+      | [v1;v2]  ->  type_error v1 v2; "z"::ctx.cpath,U
+      | _  -> assert false
+  in
+  { ctx with s = sadd ctx.s vn vv }
+
+let lustre_gte ctx =
+  let (vn,vv) = 
+    match ([get_val "x" ctx; get_val "y" ctx]) with
+      | [U; _] | [_;U] -> "z"::ctx.cpath,U
+      | [x1; x2] -> "z"::ctx.cpath,B(x1 >= x2)
+      | [v1;v2]  ->  type_error v1 v2; "z"::ctx.cpath,U 
+      | _  -> assert false
+  in
+  { ctx with s = sadd ctx.s vn vv }
+
+let lustre_and ctx =
+  let (vn,vv) = 
+    match ([get_val "x" ctx; get_val "y" ctx]) with
+      | [B x1; B x2] -> "z"::ctx.cpath,B(x1 && x2)
+      | [U; _] | [_;U] -> "z"::ctx.cpath,U
+      | [v1;v2]  ->  type_error2 v1 v2 "bool";"z"::ctx.cpath,U
+      | _  -> assert false
+  in
+  { ctx with s = sadd ctx.s vn vv }
+
+let lustre_xor ctx =
+  let (vn,vv) = 
+    match ([get_val "x" ctx; get_val "y" ctx]) with
+      | [B x1; B x2] -> "z"::ctx.cpath,B(x1 <> x2)
+      | [U; _] | [_;U] -> "z"::ctx.cpath,U
+      | [v1;v2]  ->  type_error2 v1 v2 "bool";"z"::ctx.cpath,U
+      | _  -> assert false
+  in
+  { ctx with s = sadd ctx.s vn vv }
+
+
+let lustre_neq  ctx =
+  let (vn,vv) = 
+    match ([get_val "x" ctx; get_val "y" ctx]) with
+      | [U; _] | [_;U] -> "z"::ctx.cpath,U
+      | [x1; x2] -> "z"::ctx.cpath,B(x1 <> x2)
+      | _  -> assert false
+  in
+  { ctx with s = sadd ctx.s vn vv }
+
+
+let lustre_or  ctx =
+  let (vn,vv) = 
+    match ([get_val "x" ctx; get_val "y" ctx]) with
+      | [B x1; B x2] -> "z"::ctx.cpath,B(x1 || x2)
+      | [U; _] | [_;U] -> "z"::ctx.cpath,U
+      | [v1;v2]  ->  type_error2 v1 v2 "bool";"z"::ctx.cpath,U
+      | _  -> assert false
+  in
+  { ctx with s = sadd ctx.s vn vv }
+
+
+let lustre_impl ctx =
+  let (vn,vv) = 
+    match ([get_val "x" ctx; get_val "y" ctx]) with
+      | [B x1; B x2] -> "z"::ctx.cpath,B(not x1 or x2)
+      | [U; _] | [_;U] -> "z"::ctx.cpath,U
+      | [v1;v2]  ->  type_error2 v1 v2 "bool";"z"::ctx.cpath,U
+      | _  -> assert false
+  in
+  { ctx with s = sadd ctx.s vn vv }
+
+let lustre_if ctx =
+  let (vn,vv) = 
+    match ([get_val "c" ctx; get_val "xt" ctx; get_val "xe" ctx]) with
+      | [B c; v1; v2]  -> "z"::ctx.cpath, if c then v1 else v2
+      | [U;_; _] | [_;U;U] -> "z"::ctx.cpath,U
+      | [v1;v2]  ->  type_error v1 v2; "z"::ctx.cpath,U
+      | _  -> assert false
+  in
+  { ctx with s = sadd ctx.s vn vv }
+ 
+
+let make_names str start stop = 
+  let res = ref [] in
+  for k=stop downto start do
+    res:= (str^(string_of_int k)) :: !res;
+  done;
+  !res
+
+
+let lustre_array tl ctx =
+  let t,size = match List.hd (List.rev tl) with
+    | Data.Array(t,i) -> t,i
+    | _ -> assert false
+  in
+  let inames = make_names "x" 1 size in
+  let l = List.map (fun name -> get_val name ctx) inames in
+  let a = Array.of_list l in
+  { ctx with s = sadd ctx.s ("z"::ctx.cpath) (A a) }
+
+let lustre_merge tl ctx =
+  let (vn,vv) = match get_val "clk" ctx with
+    | B(true)  -> "z"::ctx.cpath, get_val "x0" ctx
+    | B(false) -> "z"::ctx.cpath, get_val "x1" ctx
+    | E(_,i)   -> "z"::ctx.cpath, get_val ("x"^(string_of_int i)) ctx 
+    | _ -> assert false
+  in
+  { ctx with s = sadd ctx.s vn vv }
+
+let lustre_slice tl si_opt ctx =
+  let _t,size = match List.hd (List.rev tl) with
+    | Data.Array(t,i) -> t,i
+    | _ -> assert false
+  in
+  let (vn,vv) = 
+    match ([get_val "x" ctx], si_opt) with
+      | [A a],Slic(b,e,step) -> 
+        let a_res = Array.make size a.(0) in
+        let j=ref 0 in
+        for i = b to e do
+          if (i-b) mod step = 0 then (
+            a_res.(!j) <- a.(i);
+            incr j
+          );
+        done;
+        "z"::ctx.cpath, A (a_res)
+      | [U],_ -> "z"::ctx.cpath, U
+      | _  -> assert false
+  in
+  { ctx with s = sadd ctx.s vn vv }
+
+let lustre_concat ctx =
+  let (vn,vv) = 
+    match ([get_val "x" ctx; get_val "y" ctx]) with
+      | [A a1; A a2]  -> "z"::ctx.cpath, A (Array.append a1 a2)
+      | [U;_] | [_;U] -> "z"::ctx.cpath, U
+      | _  -> assert false
+  in
+  { ctx with s = sadd ctx.s vn vv }
+
+let lustre_current ctx =
+  let (vn,vv) = 
+    match ([get_val "x" ctx]) with
+      | [v]  -> "z"::ctx.cpath, v
+      | _  -> assert false
+  in
+  { ctx with s = sadd ctx.s vn vv }
+
+let lustre_arrow ctx =
+  let (vn,vv) = 
+    match ([get_val "x" ctx; get_val "y" ctx;
+            get_val "$first_step" { ctx with cpath=List.tl ctx.cpath}]) 
+    with
+      | [v1;v2; fs]  -> "z"::ctx.cpath, if fs=B false then v2 else v1
+      | _  -> assert false
+  in
+  { ctx with s = sadd ctx.s vn vv }
+
+let lustre_hat tl ctx =
+  let i = match tl with
+    | [_;Data.Array(_,i)] -> i
+    | _ -> assert false
+  in
+  let (vn,vv) = 
+    match ([get_val "x" ctx]) with
+      | [U]  -> "z"::ctx.cpath,U
+      | [v]  -> "z"::ctx.cpath,A(Array.make i v)
+      | _  -> assert false
+  in
+  { ctx with s = sadd ctx.s vn vv }
+ 
+(* exported *)
+let (get: Soc.key -> (ctx -> ctx)) =
+  fun (n,tl,si_opt) -> 
+    match n with
+    | "Lustre::rplus" 
+    | "Lustre::iplus" 
+    | "Lustre::plus" -> lustre_plus
+    | "Lustre::itimes"
+    | "Lustre::rtimes"
+    | "Lustre::times"-> lustre_times 
+    | "Lustre::idiv"
+    | "Lustre::rdiv"
+    | "Lustre::div"  -> lustre_div 
+    | "Lustre::slash" | "Lustre::islash" | "Lustre::rslash" -> lustre_slash
+    | "Lustre::iminus"
+    | "Lustre::rminus"
+    | "Lustre::minus"-> lustre_minus
+
+    | "Lustre::mod" -> lustre_mod
+    | "Lustre::iuminus"
+    | "Lustre::ruminus"
+    | "Lustre::uminus" -> lustre_uminus
+    | "Lustre::not" -> lustre_not 
+    | "Lustre::real2int" -> lustre_real2int
+    | "Lustre::int2real" -> lustre_int2real
+
+    | "Lustre::lt"| "Lustre::rlt" | "Lustre::ilt"  -> lustre_lt
+    | "Lustre::gt"| "Lustre::rgt" | "Lustre::igt"  -> lustre_gt
+    | "Lustre::lte"| "Lustre::rlte" | "Lustre::ilte" -> lustre_lte
+    | "Lustre::gte"| "Lustre::rgte"| "Lustre::igte" -> lustre_gte
+
+    | "Lustre::xor" -> lustre_xor
+    | "Lustre::and" -> lustre_and 
+    | "Lustre::eq" -> lustre_eq 
+    | "Lustre::neq" -> lustre_neq 
+    | "Lustre::or"  -> lustre_or 
+
+    | "Lustre::impl" -> lustre_impl
+
+    | "Lustre::if"| "Lustre::rif"| "Lustre::iif" -> lustre_if
+
+    | "Lustre::hat" -> lustre_hat tl
+    | "Lustre::array" -> lustre_array tl
+    | "Lustre::concat" -> lustre_concat
+
+    | "Lustre::arrow" -> lustre_arrow
+    | "Lustre::current" -> lustre_current
+    | "Lustre::merge" -> lustre_merge tl
+
+    | "Lustre::array_slice" -> lustre_slice tl si_opt
+
+    | "Lustre::nor" -> assert false (* ougth to be translated into boolred *)
+    | "Lustre::diese" -> assert false (* ditto *)
+    | _ -> raise Not_found
+*)
diff --git a/src/socPredef.ml b/src/socPredef.ml
index 03f988b7ac198b19457e2809f8bf0c50300cbdbe..c4d53bc08bf83b189713e636324842f289c219d9 100644
--- a/src/socPredef.ml
+++ b/src/socPredef.ml
@@ -1,4 +1,4 @@
-(* Time-stamp: <modified the 04/06/2013 (at 17:48) by Erwan Jahier> *)
+(* Time-stamp: <modified the 25/04/2014 (at 16:44) by Erwan Jahier> *)
 
 (** Synchronous Object Code for Predefined operators. *)
 
@@ -194,14 +194,18 @@ let of_soc_key : Soc.key -> Soc.t =
               lxm     = Lxm.dummy "predef soc";
               idx_ins  = [];
               idx_outs = [0];
-              impl    = Gaol([pre_mem],[Call([Var(vout)], Assign, [Var(pre_mem)])]);
+(*               impl    = Predef; *)
+               impl    = Gaol([pre_mem],[Call([Var(vout)], Assign, [Var(pre_mem)])]); 
+(*               impl    = Gaol([pre_mem],[Call([Var(vout)], Assign, [Var(pre_mem)])]); *)
             };
             {
               name    = "set";  
               lxm     = Lxm.dummy "predef soc";
               idx_ins  = [0];
               idx_outs = [];
-              impl    = Gaol([pre_mem],[Call([Var(pre_mem)], Assign, [Var(v1)])]);
+(*               impl    = Predef; *)
+               impl    = Gaol([pre_mem],[Call([Var(pre_mem)], Assign, [Var(v1)])]); 
+(*               impl    = Gaol([pre_mem],[Call([Var(pre_mem)], Assign, [Var(v1)])]); *)
             };
           ];
           precedences = ["set", ["get"]];
diff --git a/src/socUtils.mli b/src/socUtils.mli
index 7b81391c564773df3817a1210dbcb89431a07f59..71ab4b1ac84b680cb5544f6c8b4003e653e60e27 100644
--- a/src/socUtils.mli
+++ b/src/socUtils.mli
@@ -1,4 +1,4 @@
-(** Time-stamp: <modified the 26/04/2013 (at 09:43) by Erwan Jahier> *)
+(** Time-stamp: <modified the 04/04/2014 (at 14:45) by Erwan Jahier> *)
 
 
 (** Donne toute les méthodes d'un composant. *)
@@ -20,18 +20,18 @@ val string_of_profile             : Soc.var list * Soc.var list -> string
 val string_interface_of_soc       : Soc.t -> string
 val string_of_soc                 : Soc.t -> string
 
-val string_of_type_ref_ff         : Data.t        -> Format.formatter -> unit
 val string_of_soc_key_ff          : Soc.key  -> Format.formatter -> unit
-val string_of_var_ff              : Soc.var            -> Format.formatter -> unit
+val string_of_type_ref_ff         : Data.t   -> Format.formatter -> unit
+val string_of_var_ff              : Soc.var  -> Format.formatter -> unit
 val string_of_operation_ff        : Soc.atomic_operation      -> Format.formatter -> unit
 val string_of_filter_ff           : Soc.var_expr         -> Format.formatter -> unit
-val string_of_gao_ff              : Soc.gao           -> Format.formatter -> unit
-val string_of_method_ff           : Soc.t      -> Soc.step_method -> Format.formatter -> unit
-val string_interface_of_method_ff : Soc.t      -> Soc.step_method -> Format.formatter -> unit
+val string_of_gao_ff              : Soc.gao  -> Format.formatter -> unit
+val string_of_method_ff           : Soc.t    -> Soc.step_method -> Format.formatter -> unit
+val string_interface_of_method_ff : Soc.t    -> Soc.step_method -> Format.formatter -> unit
 val string_of_precedence_ff       : string * string list   -> Format.formatter -> unit
 val string_of_profile_ff          : Soc.var list * Soc.var list    -> Format.formatter -> unit
-val string_interface_of_soc_ff    : Soc.t           -> Format.formatter -> unit
-val string_of_soc_ff              : Soc.t              -> Format.formatter -> unit
+val string_interface_of_soc_ff    : Soc.t -> Format.formatter -> unit
+val string_of_soc_ff              : Soc.t -> Format.formatter -> unit
 
 
 (** [output header_flag pack_name] dumps the soc list into a
diff --git a/test/lus2lic.sum b/test/lus2lic.sum
index 68b9b6a2de0e3ab2f923f142074b1a108d17341f..de76319ed6b6e11fd3e193b1a889cc9a0b3fc33e 100644
--- a/test/lus2lic.sum
+++ b/test/lus2lic.sum
@@ -1,4 +1,4 @@
-Test Run By jahier on Wed Mar 26 17:22:58 2014
+Test Run By jahier on Fri Apr 25 16:33:18 2014
 Native configuration is i686-pc-linux-gnu
 
 		=== lus2lic tests ===
@@ -1028,7 +1028,7 @@ XPASS: Test bad programs (semantics): lus2lic {-o /tmp/bug.lic should_fail/seman
 # of unexpected failures	74
 # of unexpected successes	21
 # of expected failures		37
-testcase ./lus2lic.tests/non-reg.exp completed in 105 seconds
-testcase ./lus2lic.tests/progression.exp completed in 0 seconds
-testcase ./lus2lic.tests/non-reg.exp completed in 105 seconds
-testcase ./lus2lic.tests/progression.exp completed in 0 seconds
+testcase ./lus2lic.tests/non-reg.exp completed in 114 seconds
+testcase ./lus2lic.tests/progression.exp completed in 1 seconds
+testcase ./lus2lic.tests/non-reg.exp completed in 114 seconds
+testcase ./lus2lic.tests/progression.exp completed in 1 seconds
diff --git a/test/lus2lic.time b/test/lus2lic.time
index b0bc17137c42bc07ab93b1b2e461af250f392667..940f4f135d73d511da48c462eb24859e52eb86a9 100644
--- a/test/lus2lic.time
+++ b/test/lus2lic.time
@@ -1,2 +1,2 @@
-testcase ./lus2lic.tests/non-reg.exp completed in 105 seconds
-testcase ./lus2lic.tests/progression.exp completed in 0 seconds
+testcase ./lus2lic.tests/non-reg.exp completed in 114 seconds
+testcase ./lus2lic.tests/progression.exp completed in 1 seconds
diff --git a/utils/test_lus2lic_no_node b/utils/test_lus2lic_no_node
index 9ea95c56d2c8c23b46d326b2ffff63bce01dcf69..a9f80844e7898c2de51b1de0c2fa1478bf30fe73 100755
--- a/utils/test_lus2lic_no_node
+++ b/utils/test_lus2lic_no_node
@@ -33,6 +33,7 @@ cat $lustre_file  >> $_oracle;
 if
     ./lus2lic $lustre_file -n $node  -ec  -o $ec;
 #    ./lus2lic $lustre_file -n $node  -en -lv4 -eei --no-prefix -o $lv4;
+#    lus2ec $lv4 $node
 then
     echo "lus2lic -lv4 done"
 else