diff --git a/src/inline.ml b/src/inline.ml
index d01ebf1847d25db3085eedfba7b67acbc3ff5f2e..69343d5420fc12813e3315af72bd6eae34d92020 100644
--- a/src/inline.ml
+++ b/src/inline.ml
@@ -1,4 +1,4 @@
-(** Time-stamp: <modified the 21/11/2008 (at 17:16) by Erwan Jahier> *)
+(** Time-stamp: <modified the 26/11/2008 (at 09:39) by Erwan Jahier> *)
open Lxm
@@ -6,10 +6,8 @@ open Eff
(********************************************************************************)
(* stuff to create fresh var names. *)
-let var_cpt = ref 0
let new_var str node_env type_eff clock_eff =
- incr var_cpt;
- let id = Ident.of_string (str ^ (string_of_int !var_cpt)) in
+ let id = Ident.of_string (Name.new_local_var str) in
let var =
{
var_name_eff = id;
@@ -23,10 +21,6 @@ let new_var str node_env type_eff clock_eff =
Hashtbl.add node_env.lenv_vars id var;
var
-
-let init_var () =
- var_cpt := 0
-
(********************************************************************************)
(* A small util function followed by a quick unit test. *)
let rec fill i size = if i >= size then [] else i::(fill (i+1) size)
@@ -164,7 +158,7 @@ let rec (inline_eq: Eff.local_env ->
let (acc_vars : var_info list) =
let rec f i acc =
if i = 0 then acc else
- f (i-1) ((new_var "_acc" node_env type_exp clock_exp)::acc)
+ f (i-1) ((new_var "acc" node_env type_exp clock_exp)::acc)
in
(* coquetry: reverse the list to have the name in a nice order *)
List.rev(f (c-1) [])
@@ -237,7 +231,7 @@ let rec (inline_eq: Eff.local_env ->
let index_list = fill 0 k in
let lp = try List.hd lhs with Not_found -> assert false in
let res_clock = (Eff.var_info_of_left lp).var_clock_eff in
- let cpt = new_var "_cpt" node_env Int_type_eff res_clock in
+ let cpt = new_var "cpt" node_env Int_type_eff res_clock in
let id_of_int i = Predef.ICONST_n(Ident.of_string (string_of_int i)) in
let rhs = (* i <= cpt && cpt <= j; *)
let i_op = { it = Predef(id_of_int i,[]) ; src = lxm_ve }
@@ -306,7 +300,8 @@ let (iterators : Eff.local_env -> Eff.id_solver -> Eff.node_exp -> Eff.node_exp)
| ExternEff
| AbstractEff -> n
| BodyEff b ->
- init_var ();
+ Name.reset_local_var_prefix "acc";
+ Name.reset_local_var_prefix "cpt";
let loc = match n.loclist_eff with None -> [] | Some l -> l in
let (neqs, nv) =
List.fold_left (inline_eq node_env id_solver) ([], loc) b.eqs_eff
diff --git a/src/licDump.ml b/src/licDump.ml
index 76b0c1b39f296e1ee787d9e8bc8d33cbe6711ceb..6b2a665ad29632b988d495690693854a91b752fe 100644
--- a/src/licDump.ml
+++ b/src/licDump.ml
@@ -1,4 +1,4 @@
-(** Time-stamp: <modified the 25/11/2008 (at 17:31) by Erwan Jahier> *)
+(** Time-stamp: <modified the 26/11/2008 (at 09:57) by Erwan Jahier> *)
open Printf
open Lxm
@@ -165,20 +165,15 @@ and string_of_type_eff = function
we want to print (via string_of_type_eff) a type that is not a named type.
Then, at the end, we will dump that table in the lic file.
- This table is filled by [array_alias].
-
- In order to avoid name clashes, we prefix all user name type by [prefix] (cf
- at the top of this file).
-
+ This table is filled by [array_alias].
*)
and (array_alias : Eff.type_ -> int -> string) =
fun t size ->
let array_t = Array_type_eff(t,size) in
- try
- Hashtbl.find type_alias_table array_t
+ try Hashtbl.find type_alias_table array_t
with Not_found ->
let alias_t = string_of_type_eff t in
- let res = "A_"^ alias_t ^ "_" ^(string_of_int size) in
+ let res = Name.array_type array_t (alias_t ^ "_" ^(string_of_int size)) in
Hashtbl.add type_alias_table array_t res;
res
diff --git a/src/name.ml b/src/name.ml
index 902db855dff2a9fe5446138d3e810402c7705a56..423691d941854552e525f8e6efb4c7a7f068233b 100644
--- a/src/name.ml
+++ b/src/name.ml
@@ -1,4 +1,4 @@
-(** Time-stamp: <modified the 25/11/2008 (at 17:54) by Erwan Jahier> *)
+(** Time-stamp: <modified the 26/11/2008 (at 09:56) by Erwan Jahier> *)
@@ -42,4 +42,31 @@ let (node_key: Eff.node_key -> string -> string) =
Hashtbl.add node_key_tbl nk fresh_name;
fresh_name
-
+
+
+(********************************************************************************)
+(* Dealing with fresh local (to the node) variable idents *)
+let local_var_tbl = Hashtbl.create 0
+
+(* exported *)
+let (reset_local_var_prefix : string -> unit) =
+ fun str ->
+ Hashtbl.remove local_var_tbl str
+
+(* exported *)
+let (new_local_var : string -> string) =
+ fun prefix ->
+ try
+ let cpt = Hashtbl.find local_var_tbl prefix in
+ Hashtbl.replace local_var_tbl prefix (cpt+1);
+ "_" ^ prefix ^ (string_of_int cpt)
+ with
+ Not_found ->
+ Hashtbl.add local_var_tbl prefix 2;
+ "_" ^ prefix ^ "1"
+
+(********************************************************************************)
+
+let (array_type : Eff.type_ -> string -> string) =
+ fun t name ->
+ "A_" ^ name
diff --git a/src/name.mli b/src/name.mli
index 4ecb8b0d83ebc1e5b59662d0158a633f82d0b27a..d3e78b54d5bcafded76f0c70f09f9b75b82aa1cf 100644
--- a/src/name.mli
+++ b/src/name.mli
@@ -1,4 +1,4 @@
-(** Time-stamp: <modified the 25/11/2008 (at 17:48) by Erwan Jahier> *)
+(** Time-stamp: <modified the 26/11/2008 (at 09:56) by Erwan Jahier> *)
(** All new identifier names ougth to be created via this module.
@@ -18,3 +18,15 @@
(which means that [name] migth be ignored).
*)
val node_key: Eff.node_key -> string -> string
+
+
+(** Dealing with fresh local (to the node) variable idents *)
+
+(** Returns a fresh local var name *)
+val new_local_var : string -> string
+
+(** since those are local to the node, name can be re-used *)
+val reset_local_var_prefix : string -> unit
+
+(** *)
+val array_type : Eff.type_ -> string -> string
diff --git a/src/split.ml b/src/split.ml
index 18b050058e8ba5f079a50b526e2ed14080b038ab..51c6850555a69d331b16273ae005e289912d59fa 100644
--- a/src/split.ml
+++ b/src/split.ml
@@ -1,4 +1,4 @@
-(** Time-stamp: <modified the 25/11/2008 (at 14:47) by Erwan Jahier> *)
+(** Time-stamp: <modified the 26/11/2008 (at 09:39) by Erwan Jahier> *)
open Lxm
@@ -6,10 +6,8 @@ open Eff
(********************************************************************************)
(* stuff to create fresh var names. *)
-let var_cpt = ref 0
let new_var node_env type_eff clock_eff =
- incr var_cpt;
- let id = Ident.of_string ("_v" ^ (string_of_int !var_cpt)) in
+ let id = Ident.of_string (Name.new_local_var "v") in
let var =
{
var_name_eff = id;
@@ -22,8 +20,6 @@ let new_var node_env type_eff clock_eff =
in
Hashtbl.add node_env.lenv_vars id var;
var
-let init_var () =
- var_cpt := 0
(********************************************************************************)
@@ -257,12 +253,12 @@ let (node : Eff.local_env -> Eff.node_exp -> Eff.node_exp) =
| ExternEff
| AbstractEff -> n
| BodyEff b ->
- init_var ();
+ Name.reset_local_var_prefix "v";
let loc = match n.loclist_eff with None -> [] | Some l -> l in
let (neqs, nv) = List.fold_left (split_eq_acc n_env) ([], loc) b.eqs_eff in
let asserts = List.map (fun x -> x.it) b.asserts_eff in
let lxm_asserts = List.map (fun x -> x.src) b.asserts_eff in
- let nasserts,(neqs_asserts,nv_asserts) =
+ let nasserts,(neqs_asserts,nv_asserts) =
split_val_exp_list true n_env asserts
in
let nasserts = List.map2 Lxm.flagit nasserts lxm_asserts in