Sigali pass into compiler + added a_id field to applications

- Added "z3z" target language, calling sigali code generation

- a_id is application id, so as to identify node applications; added
to Minils AST. a_id is given on hept2mls pass.

This is needed for the controller execution from controller synthesis.

compiler/main/hept2mls.ml

@@ -44,6 +44,10 @@ struct
     raise Errors.Error
 end
 
+let fresh = Idents.gen_fresh "hept2mls" 
+              (function Heptagon.Enode f -> (shortname f) 
+		 | _ -> "n")
+
 (* add an equation *)
 let equation locals eqs e =
   let n = Idents.gen_var "hept2mls" "ck" in
@@ -87,7 +91,9 @@ let rec translate_op = function
 
 let translate_app app =
   mk_app ~params:app.Heptagon.a_params
-    ~unsafe:app.Heptagon.a_unsafe (translate_op app.Heptagon.a_op)
+    ~unsafe:app.Heptagon.a_unsafe
+    ~id:(Some (fresh app.Heptagon.a_op))
+    (translate_op app.Heptagon.a_op)
 
 let rec translate_extvalue e =
   let mk_extvalue = mk_extvalue ~loc:e.Heptagon.e_loc ~ty:e.Heptagon.e_ty in

compiler/main/mls2obc.ml

@@ -461,7 +461,12 @@ and mk_node_call map call_context app loc name_list args ty =
           v @ nd.Minils.n_local, si, j, subst_act_list env s
 
     | Minils.Enode f | Minils.Efun f ->
-        let o = mk_obj_call_from_context call_context (gen_obj_ident f) in
+	let id =
+	  begin match app.Minils.a_id with
+	    None -> gen_obj_name f
+	  | Some id -> name id
+	  end in
+        let o = mk_obj_call_from_context call_context id in
         let obj =
           { o_ident = obj_ref_name o; o_class = f;
             o_params = app.Minils.a_params;

compiler/main/mls2seq.ml

@@ -42,10 +42,12 @@ let no_conf () = ()
 
 let targets = [ "c",(Obc_no_params Cmain.program, no_conf);
                 "java", (Obc Java_main.program, no_conf);
+		"z3z", (Minils_no_params Sigalimain.program, no_conf);
                 "obc", (Obc write_obc_file, no_conf);
                 "obc_np", (Obc_no_params write_obc_file, no_conf);
                 "epo", (Minils write_object_file, no_conf) ]
 
+
 let generate_target p s =
   let print_unfolded p_list =
     comment "Unfolding";

compiler/minils/_tags

@@ -1 +1,2 @@
 <analysis> or <transformations> or <main> or <parsing>:include
+<sigali>:include

compiler/minils/minils.ml

@@ -72,7 +72,11 @@ and edesc =
                  * extvalue list * extvalue list * var_ident option
                        (** map f <<n>> (extvalue, extvalue...) reset ident *)
 
-and app = { a_op: op; a_params: static_exp list; a_unsafe: bool }
+and app = { a_op: op; 
+	    a_params: static_exp list;
+	    a_unsafe: bool;
+	    a_id: ident option;
+	    a_inlined: bool }
     (** Unsafe applications could have side effects
         and be delicate about optimizations, !be careful! *)
 
@@ -120,8 +124,8 @@ type node_dec = {
   n_input  : var_dec list;
   n_output : var_dec list;
   n_contract : contract option;
-  (* GD: inglorious hack for controller call
-  mutable n_controller_call : var_ident list * var_ident list; *)
+  (* GD: inglorious hack for controller call *)
+  mutable n_controller_call : string list * string list;
   n_local  : var_dec list;
   n_equs   : eq list;
   n_loc    : location;
@@ -182,6 +186,7 @@ let mk_type_dec type_desc name loc =
 let mk_const_dec id ty e loc =
   { c_name = id; c_type = ty; c_value = e; c_loc = loc }
 
-let mk_app ?(params=[]) ?(unsafe=false) op =
-  { a_op = op; a_params = params; a_unsafe = unsafe }
+let mk_app ?(params=[]) ?(unsafe=false) ?(id=None) ?(inlined=false) op =
+  { a_op = op; a_params = params; a_unsafe = unsafe;
+    a_id = id; a_inlined = inlined }