Rebase bzr branch on old decade

compiler/heptagon/parsing/hept_scoping.ml

@@ -247,7 +247,7 @@ and translate_desc loc env = function
   | Eapp ({ a_op = op; a_params = params; a_inlined = inl }, e_list) ->
       let e_list = List.map (translate_exp env) e_list in
       let params = List.map (expect_static_exp) params in
-      let app = Heptagon.mk_op ~params:params ~inlined:inl (translate_op op) in
+      let app = Heptagon.mk_app ~params:params ~inlined:inl (translate_op op) in
       Heptagon.Eapp (app, e_list, None)
 
   | Eiterator (it, { a_op = op; a_params = params }, n, pe_list, e_list) ->

compiler/main/hept2mls.ml

@@ -191,12 +191,14 @@ let node n =
     n_input = List.map translate_var n.Heptagon.n_input;
     n_output = List.map translate_var n.Heptagon.n_output;
     n_contract = translate_contract n.Heptagon.n_contract;
+    n_controller_call = ([],[]);
     n_local = List.map translate_var n.Heptagon.n_block.Heptagon.b_local;
     n_equs = List.map translate_eq n.Heptagon.n_block.Heptagon.b_equs;
     n_loc = n.Heptagon.n_loc ;
     n_params = n.Heptagon.n_params;
     n_params_constraints = n.Heptagon.n_params_constraints }
 
+
 let typedec
     {Heptagon.t_name = n; Heptagon.t_desc = tdesc; Heptagon.t_loc = loc} =
   let onetype = function

compiler/main/mls2obc.ml

@@ -463,8 +463,8 @@ and mk_node_call map call_context app loc name_list args ty =
     | Minils.Enode f | Minils.Efun f ->
 	let id =
 	  begin match app.Minils.a_id with
-	    None -> gen_obj_name f
+	    None -> gen_obj_ident f
-	  | Some id -> name id
+	  | Some id -> id
 	  end in
         let o = mk_obj_call_from_context call_context id in
         let obj =

compiler/minils/minils.ml

@@ -166,7 +166,8 @@ let mk_equation ?(loc = no_location) pat exp =
   { eq_lhs = pat; eq_rhs = exp; eq_loc = loc }
 
 let mk_node
-    ?(input = []) ?(output = []) ?(contract = None) ?(local = []) ?(eq = [])
+    ?(input = []) ?(output = []) ?(contract = None) ?(pinst = ([],[]))
+    ?(local = []) ?(eq = [])
     ?(stateful = true) ?(loc = no_location) ?(param = []) ?(constraints = [])
     name =
   { n_name = name;
@@ -174,6 +175,7 @@ let mk_node
     n_input = input;
     n_output = output;
     n_contract = contract;
+    n_controller_call = pinst;
     n_local = local;
     n_equs = eq;
     n_loc = loc;

compiler/minils/sigali/sigalimain.ml

@@ -22,8 +22,8 @@ open Sigali
 type mtype = Tint | Tbool | Tother
 
 let actual_ty = function
-  | Tid({ qual = "Pervasives"; name = "bool"}) -> Tbool
+  | Tid({ qual = Pervasives; name = "bool"}) -> Tbool
-  | Tid({ qual = "Pervasives"; name = "int"}) -> Tint
+  | Tid({ qual = Pervasives; name = "int"}) -> Tint
   | _ -> Tother
 
 let var_list prefix n =
@@ -73,7 +73,7 @@ let rec translate prefix ({ Minils.e_desc = desc; Minils.e_ty = ty } as e) =
 	end
     | Minils.Evar(n) -> Svar(prefix ^ (name n))
     | Minils.Eapp (* pervasives binary or unary stateless operations *)
-	({ Minils.a_op = Minils.Efun({qual="Pervasives";name=n})},
+	({ Minils.a_op = Minils.Efun({qual=Pervasives;name=n})},
 	 e_list, _) ->
 	begin
 	  match n, e_list with
@@ -134,7 +134,7 @@ let rec translate prefix ({ Minils.e_desc = desc; Minils.e_ty = ty } as e) =
 	end
     | Minils.Estruct(_) ->
 	failwith("Sigali: structures not implemented")
-    | Minils.Eiterator(_,_,_,_,_) ->
+    | Minils.Eiterator(_,_,_,_,_,_) ->
 	failwith("Sigali: iterators not implemented")
     | Minils.Eapp({Minils.a_op = Minils.Enode(_)},_,_) ->
 	failwith("Sigali: node in expressions; programs should be normalized")
@@ -657,7 +657,7 @@ let program p =
       (NamesEnv.empty,[])
       p.Minils.p_nodes in
   let procs = List.rev acc_proc in
-  let filename = filename_of_name p.Minils.p_modname in
+  let filename = filename_of_name (modul_to_string p.Minils.p_modname) in
   let dirname = build_path (filename ^ "_z3z") in
   let dir = clean_dir dirname in
   Sigali.Printer.print dir procs

compiler/minils/transformations/boolean.ml

@@ -51,7 +51,7 @@ open Minils
 
 let fresh = Idents.gen_fresh "bool" (fun s -> s)
 
-let ty_bool = Tid({ qual = "Pervasives"; name = "bool"})
+let ty_bool = Tid({ qual = Pervasives; name = "bool"})
 
 let strue = mk_static_exp ~ty:ty_bool (Sbool(true))
 let sfalse = mk_static_exp ~ty:ty_bool (Sbool(false))
@@ -60,8 +60,8 @@ let sbool = function
   | true -> strue
   | false -> sfalse
 
-let ctrue = { qual = "Pervasives"; name = "true" }
+let ctrue = { qual = Pervasives; name = "true" }
-let cfalse = { qual = "Pervasives"; name = "false" }
+let cfalse = { qual = Pervasives; name = "false" }
 
 let mk_tuple e_l =
   Eapp((mk_app Etuple),e_l,None)
@@ -224,7 +224,7 @@ let translate_pat env pat =
 let translate_ty ty =
   let rec trans ty =
     match ty with
-    | Tid({ qual = "Pervasives"; name = "bool" }) -> ty
+    | Tid({ qual = Pervasives; name = "bool" }) -> ty
     | Tid(name) ->
 	begin
 	  try
@@ -240,6 +240,7 @@ let translate_ty ty =
 	end
     | Tprod(ty_list) -> Tprod(List.map trans ty_list)
     | Tarray(ty,se) -> Tarray(trans ty,se)
+    | Tmutable ty -> Tmutable(trans ty)
     | Tunit -> Tunit
   in
   trans ty
@@ -271,7 +272,7 @@ let rec translate_ck env ck =
 
 let translate_const c ty e =
   match c.se_desc,ty with
-  | _, Tid({ qual = "Pervasives"; name = "bool" }) -> Econst(c)
+  | _, Tid({ qual = Pervasives; name = "bool" }) -> Econst(c)
   | Sconstructor(cname),Tid(tname) ->
       begin
 	try
@@ -352,11 +353,11 @@ let rec when_ck desc ty ck =
 
 let rec base_value ck ty =
   match ty with
-  | Tid({qual = "Pervasives"; name = "int" }) -> 
+  | Tid({qual = Pervasives; name = "int" }) -> 
       when_ck (Econst(mk_static_exp ~ty:ty (Sint(0)))) ty ck
-  | Tid({qual = "Pervasives"; name = "float"}) ->
+  | Tid({qual = Pervasives; name = "float"}) ->
       when_ck (Econst(mk_static_exp ~ty:ty (Sfloat(0.)))) ty ck
-  | Tid({qual = "Pervasives"; name = "bool" }) ->  
+  | Tid({qual = Pervasives; name = "bool" }) ->  
       when_ck (Econst(strue)) ty ck
   | Tid(sname) ->
       begin
@@ -411,6 +412,9 @@ let rec base_value ck ty =
 	e_ck = ck;
 	e_loc = no_location;
       }
+  | Tmutable ty ->
+      let e = base_value ck ty in
+      e
   | Tunit ->
       { e_desc = Eapp (mk_app Etuple, [], None);
         e_ty = Tunit;
@@ -530,9 +534,10 @@ let rec translate env context ({e_desc = desc; e_ty = ty; e_ck = ck} as e) =
 	       (context,(c,e)::acc)) 
 	    (context,[]) l in
 	context,Estruct(List.rev acc)
-    | Eiterator(it,app,se,e_list,r) ->
+    | Eiterator(it,app,se,pe_list,e_list,r) ->
+	let context,pe_list = translate_list env context pe_list in
 	let context,e_list = translate_list env context e_list in
-	context,Eiterator(it,app,se,e_list,r)
+	context,Eiterator(it,app,se,pe_list,e_list,r)
   in
   context,{ e with
 	      e_desc = desc;
@@ -678,11 +683,12 @@ let var_dec_list (acc_vd,acc_loc,acc_eq) var_from n =
 
 let buildenv_var_dec (acc_vd,acc_loc,acc_eq,env) ({v_type = ty} as v) =
   match ty with
-  | Tprod _ | Tarray _ | Tunit -> v::acc_vd, acc_loc, acc_eq, env
+  | Tprod _ | Tarray _ | Tmutable _ | Tunit ->
+      v::acc_vd, acc_loc, acc_eq, env
   | Tid(tname) ->
       begin
 	match tname with
-	| { qual = "Pervasives"; name = ("bool" | "int" | "float") } ->
+	| { qual = Pervasives; name = ("bool" | "int" | "float") } ->
 	    v::acc_vd, acc_loc, acc_eq, env
 	| _ ->
 	    begin