From e8a3785474542948e82394cb36e3a577321d4230 Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?L=C3=A9onard=20G=C3=A9rard?= <leonard.gerard@ens.fr>
Date: Tue, 15 Jun 2010 14:05:26 +0200
Subject: [PATCH] Bonjour je suis le nouveau heptgon ! my cute name is heptc.

---
 global/global.ml                    |  68 ----
 global/ident.ml                     |  10 +
 global/ident.mli                    |  40 +--
 global/initial.ml                   |   9 +-
 global/modules.ml                   |  73 +++--
 global/names.ml                     |   7 +-
 global/signature.ml                 |  38 +++
 global/static.ml                    | 242 +++++++--------
 global/types.ml                     |  17 +
 heptagon/analysis/interface.ml      |   2 +-
 heptagon/analysis/typing.ml         |  34 +-
 heptagon/heptagon.ml                | 461 +++++++++++-----------------
 heptagon/parsing/scoping.ml         |  12 +-
 heptagon/printer.ml                 |  23 +-
 main/hept2mls.ml                    |  16 +-
 minils/minils.ml                    |  53 ++--
 minils/sequential/c.ml              |   4 +-
 minils/sequential/cgen.ml           |   8 +-
 minils/sequential/mls2obc.ml        |  14 +-
 minils/sequential/obc.ml            |  31 +-
 minils/transformations/normalize.ml |   2 +-
 utilities/misc.ml                   |  13 -
 utilities/misc.mli                  |   2 -
 23 files changed, 523 insertions(+), 656 deletions(-)
 delete mode 100644 global/global.ml
 create mode 100644 global/signature.ml
 create mode 100644 global/types.ml

diff --git a/global/global.ml b/global/global.ml
deleted file mode 100644
index b6b9645..0000000
--- a/global/global.ml
+++ /dev/null
@@ -1,68 +0,0 @@
-(**************************************************************************)
-(*                                                                        *)
-(*  Heptagon                                                              *)
-(*                                                                        *)
-(*  Author : Marc Pouzet                                                  *)
-(*  Organization : Demons, LRI, University of Paris-Sud, Orsay            *)
-(*                                                                        *)
-(**************************************************************************)
-(* global data in the symbol tables *)
-(* $Id$ *)
-open Names
-open Ident
-open Linearity
-open Heptagon
-open Static
-
-(** Warning: Whenever these types are modified, 
-    interface_format_version in misc.ml should be incremented. *)
-type arg_dec = 
-    { a_type : ty;
-      a_name : name option;
-      a_linearity : linearity;
-      a_pass_by_ref: bool; }
-
-type sig_desc = 
-    { inputs : arg_dec list;
-      outputs : arg_dec list;
-      contract : contract option;
-      node : bool;
-      safe : bool; 
-      targeting : (int*int) list; 
-      params: name list;
-      params_constraints : size_constr list; }
-
-and field_desc =
-    { arg: base_ty; (* if x:arg then x.m: res *)
-      res: base_ty;
-    }
-
-and struct_desc = 
-    { fields : (name * base_ty) list; }
-
-and typ_desc =
-    | Tabstract
-    | Tenum of name list
-    | Tstruct of (name * base_ty) list
-
-type 'a info = { qualid : qualident; info : 'a }
-
-type ivar =
-  | IVar of ident
-  | IField of ident * longname
-
-(** [filter_vars l] returns a list of variables identifiers from
-    a list of ivar.*)
-let rec filter_vars = function
-  | [] -> []
-  | (IVar id)::l -> id::(filter_vars l)
-  | _::l -> filter_vars l
-
-let names l =
-  List.map (fun ad -> ad.a_name) l
-
-let types l =
-  List.map (fun ad -> ad.a_type) l
-
-let linearities l =
-  List.map (fun ad -> ad.a_linearity) l
diff --git a/global/ident.ml b/global/ident.ml
index 43c5f6d..6982642 100644
--- a/global/ident.ml
+++ b/global/ident.ml
@@ -1,5 +1,15 @@
+(**************************************************************************)
+(*                                                                        *)
+(*  Heptagon                                                              *)
+(*                                                                        *)
+(*  Author : Marc Pouzet                                                  *)
+(*  Organization : Demons, LRI, University of Paris-Sud, Orsay            *)
+(*                                                                        *)
+(**************************************************************************)
+
 (* naming and local environment *)
 
+
 type ident = {
   num : int;        (* a unique index *)
   source : string;  (* the original name in the source *)
diff --git a/global/ident.mli b/global/ident.mli
index b609d1f..b691327 100644
--- a/global/ident.mli
+++ b/global/ident.mli
@@ -1,35 +1,39 @@
+
+(** This modules manages unique identifiers,
+  [fresh] generates an identifier from a name
+  [name] returns a unique name from an identifier. *)
+
+
 (** The (abstract) type of identifiers*)
-type ident 
+type ident
 
 (** Get the source name from an identifier*)
 val sourcename : ident -> string
-(** Get the full name of an identifier (it is
-    guaranteed to be unique)*)
+(** Get the full name of an identifier (it is guaranteed to be unique) *)
 val name : ident -> string
-(** [set_sourcename id v] returns id with its
-    source name changed to v. *)
+(** [set_sourcename id v] returns id with its source name changed to v. *)
 val set_sourcename : ident -> string -> ident
 
 (** [fresh n] returns a fresh identifier with source name n *)
 val fresh : string -> ident
 (** [ident_of_var n] returns an identifier corresponding
-    to a _source_ variable (do not use it for generated variables). *)
+  to a _source_ variable (do not use it for generated variables). *)
 val ident_of_var : string -> ident
 
 (** Maps taking an identifier as a key. *)
 module Env :
-  sig
-    include (Map.S with type key = ident)
-
-    val append : 'a t -> 'a t -> 'a t
-    val union : 'a t -> 'a t -> 'a t
-    val diff : 'a t -> 'b t -> 'a t
-    val partition : (key -> bool) -> 'a t -> 'a t * 'a t
-  end
+sig
+  include (Map.S with type key = ident)
+  
+  val append : 'a t -> 'a t -> 'a t
+  val union : 'a t -> 'a t -> 'a t
+  val diff : 'a t -> 'b t -> 'a t
+  val partition : (key -> bool) -> 'a t -> 'a t * 'a t
+end
 
 (** A set of identifiers. *)
 module IdentSet :
-  sig
-    include (Set.S with type elt = ident)
-    val fprint_t : Format.formatter -> t -> unit
-  end
+sig
+  include (Set.S with type elt = ident)
+  val fprint_t : Format.formatter -> t -> unit
+end
diff --git a/global/initial.ml b/global/initial.ml
index 203ea3b..5f25bb6 100644
--- a/global/initial.ml
+++ b/global/initial.ml
@@ -8,12 +8,7 @@
 (**************************************************************************)
 (* initialization of the typing environment *)
 
-(* $Id$ *)
-
-open Misc
 open Names
-open Global
-open Modules
 
 let tglobal = []
 let cglobal = []
@@ -27,5 +22,5 @@ let pfloat = Modname({ qual = "Pervasives"; id = "float" })
 
 (* build the initial environment *)
 let initialize () =
-  List.iter (fun (f, ty) -> add_type f ty) tglobal;
-  List.iter (fun (f, ty) -> add_constr f ty) cglobal
+  List.iter (fun (f, ty) -> Modules.add_type f ty) tglobal;
+  List.iter (fun (f, ty) -> Modules.add_constr f ty) cglobal
diff --git a/global/modules.ml b/global/modules.ml
index ba3915b..2b7f389 100644
--- a/global/modules.ml
+++ b/global/modules.ml
@@ -8,43 +8,41 @@
 (**************************************************************************)
 (* global symbol tables *)
 
-(* $Id$ *)
 
 open Misc
-open Heptagon
-open Global
+open Signature
 open Names
+open Types
 
 exception Already_defined
 
 exception Cannot_find_file of string
-  
-(** Warning: Whenever this type is modified, 
-    interface_format_version in misc.ml should be incremented. *)
+
+(** Warning: Whenever this type is modified,
+    interface_format_version in signature.ml should be incremented. *)
 type env =
     { mutable name: string;
-      mutable values: sig_desc NamesEnv.t;
-      mutable types: typ_desc NamesEnv.t;
-      mutable constr: base_ty NamesEnv.t;
-      mutable field: field_desc NamesEnv.t;
-      mutable structs : struct_desc NamesEnv.t;
+      mutable values: node NamesEnv.t;
+      mutable types: type_def NamesEnv.t;
+      mutable constr: ty NamesEnv.t;
+      mutable structs : structure NamesEnv.t;
       format_version : string;
     }
-      
+
 type modules =
     { current: env;                (* associated symbol table *)
       mutable opened: env list;    (* opened tables *)
       mutable modules: env NamesEnv.t;  (* tables loaded in memory *)
     }
-      
-let current = 
-  { name = ""; values = NamesEnv.empty; types = NamesEnv.empty; 
-    constr = NamesEnv.empty; field = NamesEnv.empty; structs = NamesEnv.empty;
+
+let current =
+  { name = ""; values = NamesEnv.empty; types = NamesEnv.empty;
+    constr = NamesEnv.empty; structs = NamesEnv.empty;
     format_version = interface_format_version }
-    
-let modules = 
+
+let modules =
   { current = current; opened = []; modules = NamesEnv.empty }
-    
+
 let findfile filename =
   if Sys.file_exists filename then
     filename
@@ -58,7 +56,7 @@ let findfile filename =
         let b = Filename.concat a filename in
           if Sys.file_exists b then b else find rest
     in find !load_path
-    
+
 let load_module modname =
   let name = String.uncapitalize modname in
     try
@@ -85,7 +83,7 @@ let load_module modname =
 	  Printf.eprintf "Cannot find the compiled interface file %s.\n"
 	    filename;
 	  raise Error
-	    
+
 let find_module modname =
   try
     NamesEnv.find modname modules.modules
@@ -94,7 +92,10 @@ let find_module modname =
 	let m = load_module modname in
 	  modules.modules <- NamesEnv.add modname m modules.modules;
 	  m
-	    
+
+
+type 'a info = { qualid : qualident; info : 'a }
+
 let find where qualname =
     let rec findrec ident = function
       | [] -> raise Not_found
@@ -102,44 +103,40 @@ let find where qualname =
 	  try { qualid = { qual = m.name; id = ident };
 		info = where ident m }
 	  with Not_found -> findrec ident l in
-      
+
       match qualname with
-	| Modname({ qual = m; id = ident } as q) -> 
+	| Modname({ qual = m; id = ident } as q) ->
 	    let current = if current.name = m then current else find_module m in
 	    { qualid = q; info = where ident current }
 	| Name(ident) -> findrec ident (current :: modules.opened)
-	    
+
 (* exported functions *)
 let open_module modname =
   let m = find_module modname in
   modules.opened <- m :: modules.opened
-      
-let initialize modname = 
+
+let initialize modname =
   current.name <- modname;
   List.iter open_module !default_used_modules
-  
-let add_value f signature = 
+
+let add_value f signature =
   if NamesEnv.mem f current.values then raise Already_defined;
   current.values <- NamesEnv.add f signature current.values
-let add_type f typ_desc =
+let add_type f type_def =
   if NamesEnv.mem f current.types then raise Already_defined;
-  current.types <- NamesEnv.add f typ_desc current.types
+  current.types <- NamesEnv.add f type_def current.types
 let add_constr f ty_res =
   if NamesEnv.mem f current.constr then raise Already_defined;
   current.constr <- NamesEnv.add f ty_res current.constr
-let add_field f ty_arg ty_res =
-  if NamesEnv.mem f current.field then raise Already_defined;
-  current.field <- NamesEnv.add f { arg = ty_arg; res = ty_res } current.field
 let add_struct f fields =
   if NamesEnv.mem f current.structs then raise Already_defined;
-  current.structs <- NamesEnv.add f { fields = fields } current.structs    
+  current.structs <- NamesEnv.add f fields current.structs
 
 let find_value = find (fun ident m -> NamesEnv.find ident m.values)
 let find_type = find (fun ident m -> NamesEnv.find ident m.types)
 let find_constr = find (fun ident m -> NamesEnv.find ident m.constr)
-let find_field = find (fun ident m -> NamesEnv.find ident m.field)
 let find_struct = find (fun ident m -> NamesEnv.find ident m.structs)
-  
+
 let replace_value f signature =
   current.values <- NamesEnv.remove f current.values;
   current.values <- NamesEnv.add f signature current.values
@@ -150,6 +147,6 @@ let longname n = Modname({ qual = current.name; id = n })
 let currentname longname =
   match longname with
     | Name(n) -> longname
-    | Modname{ qual = q; id = id} -> 
+    | Modname{ qual = q; id = id} ->
 	if current.name = q then Name(id) else longname
 
diff --git a/global/names.ml b/global/names.ml
index e125d6d..253bd0f 100644
--- a/global/names.ml
+++ b/global/names.ml
@@ -1,4 +1,6 @@
-(* long identifiers *)
+(** Define qualified names "Module.name" (longname)
+  [shortname] longname -> name
+  [fullname] longname -> Module.name *)
 
 type name = string
 
@@ -23,6 +25,7 @@ end
 
 module S = Set.Make (struct type t = string let compare = compare end)
 
+
 let shortname = function
   | Name s -> s
   | Modname { id = id; } -> id
@@ -38,4 +41,4 @@ let mk_longname s =
     Modname { qual = String.sub s 0 ind; id = id; }
   with Not_found -> Name s
 
-let fprint_t ff id = Format.fprintf ff "%s" (fullname id)
+let print_longname ff id = Format.fprintf ff "%s" (fullname id)
diff --git a/global/signature.ml b/global/signature.ml
new file mode 100644
index 0000000..a82091e
--- /dev/null
+++ b/global/signature.ml
@@ -0,0 +1,38 @@
+(**************************************************************************)
+(*                                                                        *)
+(*  Heptagon                                                              *)
+(*                                                                        *)
+(*  Author : Marc Pouzet                                                  *)
+(*  Organization : Demons, LRI, University of Paris-Sud, Orsay            *)
+(*                                                                        *)
+(**************************************************************************)
+(* global data in the symbol tables *)
+open Names
+open Types
+open Static
+
+(** Warning: Whenever these types are modified,
+    interface_format_version should be incremented. *)
+let interface_format_version = "6"
+
+(** Node argument *)
+type arg = { a_type : ty; a_name : name option }
+
+type param = { p_name : name }
+
+(** Node signature *)
+type node =
+  { node_inputs : arg list;
+    node_outputs : arg list;
+    node_params : param list; (** Static parameters *)
+    node_params_constraints : size_constr list }
+
+type structure = (name * ty) list
+
+type type_def = | Tabstract | Tenum of name list | Tstruct of structure
+
+
+let names_of_arg_list l = List.map (fun ad -> ad.a_name) l
+
+let types_of_arg_list l = List.map (fun ad -> ad.a_type) l
+
diff --git a/global/static.ml b/global/static.ml
index 31d021f..04da672 100644
--- a/global/static.ml
+++ b/global/static.ml
@@ -1,176 +1,164 @@
-(** This module defines static expressions, used in arrays definition and anywhere 
-    a static value is expected. For instance:
-    const n:int = 3;
-    var x : int^n; var y : int^(n+2);
-    x[n-1], x[1+3],...
+(** This module defines static expressions, used in arrays definition
+
+    and anywhere a static value is expected. For instance:
+    const n: int = 3;
+    var x : int^n; var y : int^(n + 2);
+    x[n - 1], x[1 + 3],...
 *)
 open Names
+  
 open Format
-
-type op = SPlus | SMinus | STimes | SDiv
+  
+type op = | SPlus | SMinus | STimes | SDiv
 
 type size_exp =
-  | SConst of int
-  | SVar of name
-  | SOp of op * size_exp * size_exp
+  | SConst of int | SVar of name | SOp of op * size_exp * size_exp
 
 (** Constraints on size expressions. *)
 type size_constr =
   | Equal of size_exp * size_exp (* e1 = e2*)
   | LEqual of size_exp * size_exp (* e1 <= e2 *)
-  | False (* unsatisfiable constraint *)
+  | False
 
-exception Instanciation_failed 
+(* unsatisfiable constraint *)
+exception Instanciation_failed
+  
 exception Not_static
-
+  
 (** Returns the op from an operator full name. *)
 let op_from_app_name n =
   match n with
-    | Modname({ qual = "Pervasives"; id = "+" }) | Name "+" -> SPlus
-    | Modname({ qual = "Pervasives"; id = "-" }) | Name "-" -> SMinus
-    | Modname({ qual = "Pervasives"; id = "*" }) | Name "*" -> STimes
-    | Modname({ qual = "Pervasives"; id = "/" }) | Name "/" -> SDiv
-    | _ -> raise Not_static
-
+  | Modname { qual = "Pervasives"; id = "+" } | Name "+" -> SPlus
+  | Modname { qual = "Pervasives"; id = "-" } | Name "-" -> SMinus
+  | Modname { qual = "Pervasives"; id = "*" } | Name "*" -> STimes
+  | Modname { qual = "Pervasives"; id = "/" } | Name "/" -> SDiv
+  | _ -> raise Not_static
+  
 (** [simplify env e] returns e simplified with the
     variables values taken from env (mapping vars to integers).
     Variables are replaced with their values and every operator
     that can be computed is replaced with the value of the result. *)
-let rec simplify env = function
+let rec simplify env =
+  function
   | SConst n -> SConst n
-  | SVar id -> 
-      (try 
-	simplify env (NamesEnv.find id env) 
-      with
-	  _ -> SVar id
-      )
-  | SOp(op, e1, e2) ->
+  | SVar id -> (try simplify env (NamesEnv.find id env) with | _ -> SVar id)
+  | SOp (op, e1, e2) ->
       let e1 = simplify env e1 in
-      let e2 = simplify env e2 in
-	(match e1, e2 with
-	   | SConst n1, SConst n2 -> 
-	       let n = (match op with
-		  | SPlus -> n1 + n2
-		  | SMinus -> n1 - n2
-		  | STimes -> n1 * n2
-		  | SDiv ->
-		      if n2 = 0 then
-			raise Instanciation_failed
-		      else
-			n1 / n2
-	       ) in
-		 SConst n
-	   | _, _ -> SOp(op, e1, e2)
-	)
-
+      let e2 = simplify env e2
+      in
+        (match (e1, e2) with
+         | (SConst n1, SConst n2) ->
+             let n =
+               (match op with
+                | SPlus -> n1 + n2
+                | SMinus -> n1 - n2
+                | STimes -> n1 * n2
+                | SDiv ->
+                    if n2 = 0 then raise Instanciation_failed else n1 / n2)
+             in SConst n
+         | (_, _) -> SOp (op, e1, e2))
+  
 (** [int_of_size_exp env e] returns the value of the expression
     [e] in the environment [env], mapping vars to integers. Raises
     Instanciation_failed if it cannot be computed (if a var has no value).*)
 let int_of_size_exp env e =
-  match simplify env e with
-    | SConst n -> n
-    | _ -> raise Instanciation_failed      
-
+  match simplify env e with | SConst n -> n | _ -> raise Instanciation_failed
+  
 (** [is_true env constr] returns whether the constraint is satisfied
     in the environment (or None if this can be decided)
+
     and a simplified constraint. *)
-let is_true env = function
-  | Equal (e1,e2) when e1 = e2 -> 
-      Some true, Equal (simplify env e1, simplify env e2)
+let is_true env =
+  function
+  | Equal (e1, e2) when e1 = e2 ->
+      ((Some true), (Equal (simplify env e1, simplify env e2)))
   | Equal (e1, e2) ->
       let e1 = simplify env e1 in
-      let e2 = simplify env e2 in
-	(match e1, e2 with
-	   | SConst n1, SConst n2 ->
-	       Some (n1 = n2), Equal (e1,e2)
-	   | _, _ -> None, Equal (e1,e2)
-	)
+      let e2 = simplify env e2
+      in
+        (match (e1, e2) with
+         | (SConst n1, SConst n2) -> ((Some (n1 = n2)), (Equal (e1, e2)))
+         | (_, _) -> (None, (Equal (e1, e2))))
   | LEqual (e1, e2) ->
       let e1 = simplify env e1 in
-      let e2 = simplify env e2 in
-	(match e1, e2 with
-	   | SConst n1, SConst n2 ->
-	       Some (n1 <= n2), LEqual (e1,e2)
-	   | _, _ -> None, LEqual (e1,e2)
-	)
-  | False -> None, False
-
+      let e2 = simplify env e2
+      in
+        (match (e1, e2) with
+         | (SConst n1, SConst n2) -> ((Some (n1 <= n2)), (LEqual (e1, e2)))
+         | (_, _) -> (None, (LEqual (e1, e2))))
+  | False -> (None, False)
+  
 exception Solve_failed of size_constr
+  
 (** [solve env constr_list solves a list of constraints. It
-    removes equations that can be decided and simplify others. 
+    removes equations that can be decided and simplify others.
     If one equation cannot be satisfied, it raises Solve_failed. ]*)
-let rec solve const_env = function
+let rec solve const_env =
+  function
   | [] -> []
-  | c::l -> 
+  | c :: l ->
       let l = solve const_env l in
-      let res, c = is_true const_env c in
-	(match res with
-	   | None -> c::l
-	   | Some v -> if not v then raise (Solve_failed c) else l
-	)
-
+      let (res, c) = is_true const_env c
+      in
+        (match res with
+         | None -> c :: l
+         | Some v -> if not v then raise (Solve_failed c) else l)
+  
 (** Substitutes variables in the size exp with their value
     in the map (mapping vars to size exps). *)
-let rec size_exp_subst m = function
-  | SVar n ->
-      (try 
-	List.assoc n m
-      with 
-	  Not_found -> SVar n
-      )
-  | SOp(op,e1,e2) -> SOp(op, size_exp_subst m e1, size_exp_subst m e2)
+let rec size_exp_subst m =
+  function
+  | SVar n -> (try List.assoc n m with | Not_found -> SVar n)
+  | SOp (op, e1, e2) -> SOp (op, size_exp_subst m e1, size_exp_subst m e2)
   | s -> s
-
+  
 (** Substitutes variables in the constraint list with their value
     in the map (mapping vars to size exps). *)
 let instanciate_constr m constr =
-  let replace_one m = function
-    | Equal(e1,e2) -> Equal(size_exp_subst m e1, size_exp_subst m e2)
-    | LEqual(e1,e2) -> LEqual(size_exp_subst m e1, size_exp_subst m e2)
-  in
-    List.map (replace_one m) constr 
-
-let op_to_string = function
-  | SPlus -> "+"
-  | SMinus -> "-"
-  | STimes -> "*"
-  | SDiv -> "/"
-
-let rec print_size_exp ff = function
+  let replace_one m =
+    function
+    | Equal (e1, e2) -> Equal (size_exp_subst m e1, size_exp_subst m e2)
+    | LEqual (e1, e2) -> LEqual (size_exp_subst m e1, size_exp_subst m e2)
+    | False -> False
+  in List.map (replace_one m) constr
+  
+let op_to_string =
+  function | SPlus -> "+" | SMinus -> "-" | STimes -> "*" | SDiv -> "/"
+  
+let rec print_size_exp ff =
+  function
   | SConst i -> fprintf ff "%d" i
   | SVar id -> fprintf ff "%s" id
   | SOp (op, e1, e2) ->
-      fprintf ff "@[(";
-      print_size_exp ff e1;
-      fprintf ff " %s " (op_to_string op);
-      print_size_exp ff e2;
-      fprintf ff ")@]"
-
+      (fprintf ff "@[(";
+       print_size_exp ff e1;
+       fprintf ff " %s " (op_to_string op);
+       print_size_exp ff e2;
+       fprintf ff ")@]")
+  
 let rec print_list ff print sep l =
   match l with
-    | [] -> ()
-    | [x] -> print ff x
-    | x :: l ->
-        print ff x;
-        fprintf ff "%s@ " sep;
-        print_list ff print sep l
-
-let print_size_constr ff = function
-  | Equal (e1, e2) ->      
-      fprintf ff "@[";
-      print_size_exp ff e1;
-      fprintf ff " = ";
-      print_size_exp ff e2;
-      fprintf ff "@]"
-  | LEqual (e1, e2) ->      
-      fprintf ff "@[";
-      print_size_exp ff e1;
-      fprintf ff " <= ";
-      print_size_exp ff e2;
-      fprintf ff "@]"
-  | False ->
-      fprintf ff "False"
-
+  | [] -> ()
+  | [ x ] -> print ff x
+  | x :: l -> (print ff x; fprintf ff "%s@ " sep; print_list ff print sep l)
+  
+let print_size_constr ff =
+  function
+  | Equal (e1, e2) ->
+      (fprintf ff "@[";
+       print_size_exp ff e1;
+       fprintf ff " = ";
+       print_size_exp ff e2;
+       fprintf ff "@]")
+  | LEqual (e1, e2) ->
+      (fprintf ff "@[";
+       print_size_exp ff e1;
+       fprintf ff " <= ";
+       print_size_exp ff e2;
+       fprintf ff "@]")
+  | False -> fprintf ff "False"
+  
 let psize_constr oc c =
-  let ff = formatter_of_out_channel oc in
-    print_size_constr ff c; fprintf ff "@?"
+  let ff = formatter_of_out_channel oc
+  in (print_size_constr ff c; fprintf ff "@?")
+  
diff --git a/global/types.ml b/global/types.ml
new file mode 100644
index 0000000..4489d1c
--- /dev/null
+++ b/global/types.ml
@@ -0,0 +1,17 @@
+(**************************************************************************)
+(*                                                                        *)
+(*  Heptagon                                                              *)
+(*                                                                        *)
+(*  Author : Marc Pouzet                                                  *)
+(*  Organization : Demons, LRI, University of Paris-Sud, Orsay            *)
+(*                                                                        *)
+(**************************************************************************)
+open Static
+open Names
+
+type ty =
+  | Tprod of ty list | Tid of longname | Tarray of ty * size_exp
+
+
+
+let const_array_of ty n = Tarray (ty, SConst n)
\ No newline at end of file
diff --git a/heptagon/analysis/interface.ml b/heptagon/analysis/interface.ml
index ffb5e7b..bdd698b 100644
--- a/heptagon/analysis/interface.ml
+++ b/heptagon/analysis/interface.ml
@@ -83,7 +83,7 @@ struct
 	  print_list ff 
 	    (fun ff (field, ty) -> print_name ff field;
               fprintf ff ": ";
-	      print_base_type ff ty) ";" f_ty_list;
+	      print_type ff ty) ";" f_ty_list;
 	  fprintf ff "}@]@.@]"
 
   let signature ff name { inputs = inputs;
diff --git a/heptagon/analysis/typing.ml b/heptagon/analysis/typing.ml
index 92face8..89c51c7 100644
--- a/heptagon/analysis/typing.ml
+++ b/heptagon/analysis/typing.ml
@@ -139,8 +139,8 @@ let message loc kind =
 
 let add_value f signature =
   try add_value f signature with Already_defined -> error (Ealready_defined f)
-let add_type f typ_desc =
-  try add_type f typ_desc with Already_defined -> error (Ealready_defined f)
+let add_type f type_def =
+  try add_type f type_def with Already_defined -> error (Ealready_defined f)
 let add_constr f ty_res =
   try add_constr f ty_res with Already_defined -> error (Ealready_defined f)
 let add_field f ty_arg ty_res =
@@ -223,17 +223,17 @@ let prod = function
   | ty_list -> Tprod(ty_list)
 
 let rec typing_const c = 
-  let typed_c, base_ty = match c with
+  let typed_c, ty = match c with
     | Cint _     -> c, Tid(pint)
     | Cfloat _   -> c, Tid(pfloat)
     | Cconstr(c) -> 
-	let { qualid = q; info = base_ty } = find_constr c in
-	Cconstr(Modname(q)), base_ty
-    | Cconst_array(n, c) ->
+	let { qualid = q; info = ty } = find_constr c in
+	Cconstr(Modname(q)), ty
+    | Carray(n, c) ->
 	let c, ty = typing_const c in
-	  Cconst_array(n,c), Tarray(base_type ty, n)
+	  Carray(n,c), Tarray(type ty, n)
   in
-  typed_c, Tbase(base_ty)
+  typed_c, Tbase(ty)
 	
 let typ_of_name h x = 
   try 
@@ -294,12 +294,12 @@ let simplify_type loc const_env ty =
   with
     Instanciation_failed -> message loc (Etype_should_be_static (Tbase ty))
 
-let rec subst_base_type_vars m = function
-  | Tarray(ty, e) -> Tarray(subst_base_type_vars m ty, size_exp_subst m e)
+let rec subst_type_vars m = function
+  | Tarray(ty, e) -> Tarray(subst_type_vars m ty, size_exp_subst m e)
   | t -> t
 
 let rec subst_type_vars m = function
-  | Tbase ty -> Tbase (subst_base_type_vars m ty)
+  | Tbase ty -> Tbase (subst_type_vars m ty)
   | Tprod l -> Tprod (List.map (subst_type_vars m) l)
 
 let equal expected_tag_list actual_tag_list =
@@ -492,8 +492,8 @@ and typing_app statefull h op e_list =
 	  ty, op, typed_e1::typed_defe::typed_idx_list
     | Eupdate idx_list, [e1;e2] ->
 	let typed_e1, t1 = typing statefull h e1 in
-	let base_ty = typing_array_subscript statefull h idx_list t1 in
-	let typed_e2 = expect statefull h base_ty e2 in
+	let ty = typing_array_subscript statefull h idx_list t1 in
+	let typed_e2 = expect statefull h ty e2 in
 	  t1, op, [typed_e1; typed_e2]
     | Eselect_slice, [e; idx1; idx2] ->
 	let typed_idx1 = expect statefull h (Tbase(Tint)) idx1 in
@@ -612,10 +612,10 @@ and typing_iterator statefull h it n args_ty_list result_ty_list e_list =
 and typing_array_subscript statefull h idx_list ty  = 
   match ty, idx_list with
     | ty, [] -> ty 
-    | Tbase(Tarray(base_ty, exp)), idx::idx_list -> 
+    | Tbase(Tarray(ty, exp)), idx::idx_list -> 
 	add_size_constr (LEqual (SConst 0, idx));
 	add_size_constr (LEqual (idx, SOp(SMinus, exp, SConst 1)));
-	typing_array_subscript statefull h idx_list (Tbase base_ty) 
+	typing_array_subscript statefull h idx_list (Tbase ty) 
     | _, _ -> error (Esubscripted_value_not_an_array ty)
 
 (* This function checks that the array dimensions matches
@@ -623,10 +623,10 @@ and typing_array_subscript statefull h idx_list ty  =
 and typing_array_subscript_dyn statefull h idx_list ty = 
   match ty, idx_list with
     | ty, [] -> ty, [] 
-    | Tbase(Tarray(base_ty, exp)), idx::idx_list -> 
+    | Tbase(Tarray(ty, exp)), idx::idx_list -> 
 	let typed_idx = expect statefull h (Tbase(Tint)) idx in 
 	let ty, typed_idx_list = 
-	  typing_array_subscript_dyn statefull h idx_list (Tbase base_ty) in
+	  typing_array_subscript_dyn statefull h idx_list (Tbase ty) in
 	  ty, typed_idx::typed_idx_list 
     | _, _ -> error (Esubscripted_value_not_an_array ty)
 
diff --git a/heptagon/heptagon.ml b/heptagon/heptagon.ml
index 53b1ac5..7a23909 100644
--- a/heptagon/heptagon.ml
+++ b/heptagon/heptagon.ml
@@ -7,37 +7,23 @@
 (*                                                                        *)
 (**************************************************************************)
 (* the internal representation *)
-(* $Id$ *)
-
 open Location
 open Misc
 open Names
-open Linearity
-open Ident
-open Interference_graph
+open Ident  
 open Static
+open Signature
 
-type inlining_policy =
-  | Ino
-  | Ione
-  | Irec
 
-type ty =
-  | Tbase of base_ty
-  | Tprod of ty list
+type iterator_name = 
+  | Imap
+  | Ifold
+  | Imapfold
 
-and base_ty =
-  | Tint | Tfloat | Tbool
-  | Tid of longname
-  | Tarray of base_ty * size_exp
+type exp =
+  { e_desc : desc; e_ty : ty; e_loc : location }
 
-and exp =
-    { e_desc: desc;
-      mutable e_ty: ty;
-      mutable e_linearity : linearity;
-      e_loc: location }
-
-and desc =
+  and desc =
   | Econst of const
   | Evar of ident
   | Econstvar of name
@@ -47,324 +33,225 @@ and desc =
   | Efield of exp * longname
   | Estruct of (longname * exp) list
   | Earray of exp list
-  | Ereset_mem of ident * exp * ident
 
-and app =
-    { mutable a_op : op; (* hange of global name after typing *)
-      a_inlined : inlining_policy; (* node to inline or not *)
-    }
+  and app =
+  { a_op : op; }
 
-and op =
+  and op =
   | Epre of const option
-  | Efby | Earrow | Eifthenelse | Enode of longname * size_exp list
-  | Eevery of longname * size_exp list | Eop of longname * size_exp list
-  | Erepeat | Eselect of size_exp list | Eselect_dyn
+  | Efby
+  | Earrow
+  | Eifthenelse
+  | Earray_op of array_op
+  | Ecall of op_desc * exp option (** [op_desc] is the function called
+                                      [exp option] is the optional reset condition *)
+    
+  and array_op =
+  | Erepeat
+  | Eselect of size_exp list
+  | Eselect_dyn
   | Eupdate of size_exp list
   | Eselect_slice
-  | Econcat | Ecopy
-  | Eiterator of iterator_name * longname * size_exp list * exp option
-  | Efield_update of longname
-  | Eflatten of longname | Emake of longname
+  | Econcat
+  | Eiterator of iterator_name * op_desc * exp option
+  
+  and op_desc = longname * size_exp list * op_kind
+  and op_kind = | Eop | Enode
 
-and const =
+  and const =
   | Cint of int
   | Cfloat of float
   | Cconstr of longname
-  | Cconst_array of size_exp * const 
+  | Carray of size_exp * const
 
-and pat =
-  | Etuplepat of pat list
-  | Evarpat of ident
+  and pat =
+  | Etuplepat of pat list | Evarpat of ident
 
 type eq =
-    { eq_desc : eqdesc;
-      mutable eq_statefull : bool;
-      eq_loc : location }
+  { eq_desc : eqdesc; eq_statefull : bool; eq_loc : location }
 
-and eqdesc =
+  and eqdesc =
   | Eautomaton of state_handler list
   | Eswitch of exp * switch_handler list
   | Epresent of present_handler list * block
   | Ereset of eq list * exp
   | Eeq of pat * exp
 
-and block =
-    { b_local: var_dec list;
-      b_equs: eq list;
-      mutable b_defnames: ty Env.t;
-      mutable b_statefull: bool;
-      b_loc: location; }
+  and block =
+  { b_local : var_dec list; b_equs : eq list; mutable b_defnames : ty Env.t;
+    mutable b_statefull : bool; b_loc : location
+  }
 
-and state_handler =
-    { s_state : name;
-      s_block : block;
-      s_until : escape list;
-      s_unless : escape list; }
+  and state_handler =
+  { s_state : name; s_block : block; s_until : escape list;
+    s_unless : escape list
+  }
 
-and escape =
-    { e_cond : exp;
-      e_reset : bool;
-      e_next_state : name; }
+  and escape =
+  { e_cond : exp; e_reset : bool; e_next_state : name
+  }
 
-and switch_handler =
-    { w_name : longname;
-      w_block : block; }
+  and switch_handler =
+  { w_name : longname; w_block : block
+  }
 
-and present_handler =
-    { p_cond : exp;
-      p_block : block; }
+  and present_handler =
+  { p_cond : exp; p_block : block
+  }
 
-and var_dec =
-    { v_name : ident;
-      mutable v_type : base_ty;
-      mutable v_linearity : linearity;
-      v_last : last;
-      v_loc  : location; }
+  and var_dec =
+  { v_name : ident; mutable v_type : ty; v_last : last; v_loc : location }
 
-and last = Var | Last of const option
+  and last =
+  | Var | Last of const option
 
 type type_dec =
-    { t_name : name;
-      t_desc : type_desc;
-      t_loc  : location }
+  { t_name : name; t_desc : type_desc; t_loc : location }
 
-and type_desc =
-  | Type_abs
-  | Type_enum of name list
-  | Type_struct of (name * base_ty) list
+  and type_desc =
+  | Type_abs | Type_enum of name list | Type_struct of structure
 
 type contract =
-    { c_assume : exp;
-      c_enforce : exp;
-      c_controllables : var_dec list;
-      c_local : var_dec list;
-      c_eq : eq list;
-    }
+  { c_assume : exp; c_enforce : exp; c_controllables : var_dec list;
+    c_local : var_dec list; c_eq : eq list
+  }
 
 type node_dec =
-    { n_name      : name;
-      n_statefull : bool;
-      n_input     : var_dec list;
-      n_output    : var_dec list;
-      n_local     : var_dec list;
-      n_contract  : contract option;
-      n_equs      : eq list;
-      n_loc       : location; 
-      n_states_graph : (name,name) interf_graph; 
-      n_params : name list;
-      n_params_constraints : size_constr list;
-    }
+  { n_name : name; n_statefull : bool; n_input : var_dec list;
+    n_output : var_dec list; n_local : var_dec list;
+    n_contract : contract option; n_equs : eq list; n_loc : location;
+    n_params : name list;
+    n_params_constraints : size_constr list
+  }
 
 type const_dec =
-    { c_name : name;
-      c_type : base_ty;
-      c_value : size_exp;
-      c_loc : location; }
+  { c_name : name; c_type : ty; c_value : size_exp; c_loc : location }
 
 type program =
-    { p_pragmas: (name * string) list;
-      p_opened : name list;
-      p_types  : type_dec list;
-      p_nodes  : node_dec list;
-      p_consts : const_dec list; }
+  { p_pragmas : (name * string) list; p_opened : name list;
+    p_types : type_dec list; p_nodes : node_dec list;
+    p_consts : const_dec list
+  }
 
 type signature =
-    { sig_name    : name;
-      sig_inputs  : (name option * base_ty * linearity) list;
-      sig_outputs : (name option * base_ty * linearity) list;
-      sig_node    : bool;
-      sig_safe    : bool;
-      sig_params  : name list; }
+  { sig_name : name; sig_inputs : arg list;
+    sig_outputs : arg list; sig_params : param list
+  }
 
-type interface = interface_decl list
+type interface =
+  interface_decl list
 
-and interface_decl =
-    { interf_desc : interface_desc;
-      interf_loc  : location }
-
-and interface_desc =
-  | Iopen of name
-  | Itypedef of type_dec
-  | Isignature of signature
-
-let tbool = Tbool
+  and interface_decl =
+  { interf_desc : interface_desc; interf_loc : location
+  }
 
+  and interface_desc =
+  | Iopen of name | Itypedef of type_dec | Isignature of signature
+  
 let edesc e = e.e_desc
+  
 let eqdesc eq = eq.eq_desc
+  
+(* Helper functions to create AST. *) (*TODO refactor en mk_*)
 
-(* Helper functions to create AST. *)
-let pbool = Modname({ qual = "Pervasives"; id = "bool" })
-let ptrue = Modname({ qual = "Pervasives"; id = "true" })
-let pfalse = Modname({ qual = "Pervasives"; id = "false" })
-let por = Modname({ qual = "Pervasives"; id = "or" })
-let pint = Modname({ qual = "Pervasives"; id = "int" })
-let pfloat = Modname({ qual = "Pervasives"; id = "float" })
-
-let emake desc ty = { e_desc = desc; e_ty = ty; 
-		      e_linearity = NotLinear; e_loc = no_location }
-let eop op = { a_op = op; a_inlined = Ino }
-let tmake name desc = { t_name = name; t_desc = desc; t_loc = no_location }
-let eqmake desc = { eq_desc = desc; eq_statefull = true; eq_loc = no_location }
-
-let tybool = Tbase(tbool)
-let cfalse = Cconstr(pfalse)
-let ctrue = Cconstr(ptrue)
-
+let emake desc ty =
+  { e_desc = desc; e_ty = ty; e_linearity = NotLinear; e_loc = no_location; }
+  
+let eop op = { a_op = op; a_inlined = Ino; }
+  
+let tmake name desc = { t_name = name; t_desc = desc; t_loc = no_location; }
+  
+let eqmake desc =
+  { eq_desc = desc; eq_statefull = true; eq_loc = no_location; }
+  
+let tybool = Tbase tbool
+  
+let cfalse = Cconstr pfalse
+  
+let ctrue = Cconstr ptrue
+  
 let make_bool desc = emake desc tybool
-let bool_var n = make_bool (Evar(n))
+  
+let bool_var n = make_bool (Evar n)
+  
 let bool_param n =
-  { v_name = n; v_type = tbool; v_last = Var; 
-    v_loc = no_location; v_linearity = NotLinear }
-
-let dfalse = make_bool (Econst(Cconstr(pfalse)))
-let dtrue = make_bool (Econst(Cconstr(ptrue)))
-
-let var n ty = emake (Evar(n)) ty
+  {
+    v_name = n;
+    v_type = tbool;
+    v_last = Var;
+    v_loc = no_location;
+    v_linearity = NotLinear;
+  }
+  
+let dfalse = make_bool (Econst (Cconstr pfalse))
+  
+let dtrue = make_bool (Econst (Cconstr ptrue))
+  
+let var n ty = emake (Evar n) ty
+  
 let param n ty =
-  { v_name = n; v_type = ty; v_linearity = NotLinear; 
-    v_last = Var; v_loc = no_location }
+  {
+    v_name = n;
+    v_type = ty;
+    v_linearity = NotLinear;
+    v_last = Var;
+    v_loc = no_location;
+  }
+  
 let fby_state initial e =
-  { e with e_desc = Eapp(eop (Epre(Some(Cconstr initial))), [e]) }
-let fby_false e = emake (Eapp(eop (Epre(Some(cfalse))), [e])) tybool
-let last_false x = emake (Elast(x)) tybool
-let ifthenelse e1 e2 e3 = emake (Eapp(eop Eifthenelse, [e1;e2;e3])) e2.e_ty
-let rec or_op e1 e2 = { e1 with e_desc = Eapp(eop (Eop(por, [])), [e1; e2]) }
-let pair e1 e2 = emake (Etuple([e1;e2])) (Tprod [e1.e_ty;e2.e_ty])
+  { (e) with e_desc = Eapp (eop (Epre (Some (Cconstr initial))), [ e ]); }
+  
+let fby_false e = emake (Eapp (eop (Epre (Some cfalse)), [ e ])) tybool
+  
+let last_false x = emake (Elast x) tybool
+  
+let ifthenelse e1 e2 e3 =
+  emake (Eapp (eop Eifthenelse, [ e1; e2; e3 ])) e2.e_ty
+  
+let rec or_op e1 e2 =
+  { (e1) with e_desc = Eapp (eop (Eop (por, [])), [ e1; e2 ]); }
+  
+let pair e1 e2 = emake (Etuple [ e1; e2 ]) (Tprod [ e1.e_ty; e2.e_ty ])
+  
 let block defnames eqs =
-  { b_local = []; b_equs = eqs; b_defnames = defnames;
-    b_statefull = true; b_loc = no_location }
-let eq pat e = eqmake (Eeq(pat, e))
-let reset eq_list e = eqmake (Ereset(eq_list, e))
-let switch e l = eqmake (Eswitch(e, l))
-
-let varpat n = Evarpat(n)
-
-(* Helper functions to work with type*)
-let base_type ty =
-  match ty with
-    | Tbase ty -> ty
-    | _ -> assert false
-
-let is_scalar_type ty =
-  let pint = Modname({ qual = "Pervasives"; id = "int" }) in
-  let pfloat = Modname({ qual = "Pervasives"; id = "float" }) in
-  let pbool = Modname({ qual = "Pervasives"; id = "bool" }) in
-    match ty with
-      | Tbase(Tint) | Tbase(Tfloat) | Tbase(Tbool) -> true
-      | Tbase(Tid name_int) when name_int = pint -> true
-      | Tbase(Tid name_float) when name_float = pfloat -> true
-      | Tbase(Tid name_bool) when name_bool = pbool -> true	  
-      | _ -> false 
-	
-let array_of ty exp =
-  Tbase(Tarray (base_type ty, exp))
-
-let const_array_of ty n =
-  array_of ty (SConst n)
-
+  {
+    b_local = [];
+    b_equs = eqs;
+    b_defnames = defnames;
+    b_statefull = true;
+    b_loc = no_location;
+  }
+  
+let eq pat e = eqmake (Eeq (pat, e))
+  
+let reset eq_list e = eqmake (Ereset (eq_list, e))
+  
+let switch e l = eqmake (Eswitch (e, l))
+  
+let varpat n = Evarpat n
+  
 let op_from_app app =
   match app.a_op with
-    | Eop (n,_) -> op_from_app_name n
-    | _ -> raise Not_static
-
+  | Eop (n, _) -> op_from_app_name n
+  | _ -> raise Not_static
+  
 let rec size_exp_of_exp e =
-  match e.e_desc with 
+  match e.e_desc with
   | Econstvar n -> SVar n
   | Econst (Cint i) -> SConst i
-  | Eapp(app, [e1;e2]) ->
-      let op = op_from_app app in
-	SOp(op, size_exp_of_exp e1, size_exp_of_exp e2)
+  | Eapp (app, ([ e1; e2 ])) ->
+      let op = op_from_app app
+      in SOp (op, size_exp_of_exp e1, size_exp_of_exp e2)
   | _ -> raise Not_static
 
-module Vars =
-struct
-  let rec vars_pat locals acc = function
-    | Evarpat(x) ->
-        if (IdentSet.mem x locals) or (IdentSet.mem x acc) then
-	  acc 
-	else 
-	  IdentSet.add x acc
-    | Etuplepat(pat_list) -> List.fold_left (vars_pat locals) acc pat_list
+(** @return the set of variables defined in [pat]. *)
+let vars_pat pat =
+  let rec _vars_pat locals acc = function
+      | Evarpat x ->
+          if (IdentSet.mem x locals) or (IdentSet.mem x acc)
+          then acc
+          else IdentSet.add x acc
+      | Etuplepat pat_list -> List.fold_left (_vars_pat locals) acc pat_list
+  in _vars_pat IdentSet.empty IdentSet.empty pat
 
-  let rec left locals acc e =
-    match e.e_desc with
-      | Eapp({a_op = Epre _},[e]) -> acc
-      | Eapp({a_op = Efby}, [e1;e2]) -> left locals acc e1
-      | Etuple(e_list) | Eapp({a_op = _}, e_list) | Earray(e_list)->
-          List.fold_left (left locals) acc e_list
-      | Evar(n) | Ereset_mem (_, _, n) ->
-          if (IdentSet.mem n acc) or (IdentSet.mem n locals) then
-	    acc 
-	  else
-	    IdentSet.add n acc
-      | Efield(e, _) -> left locals acc e
-      | Estruct(f_e_list) ->
-          List.fold_left (fun acc (_, e) -> left locals acc e) acc f_e_list
-      | Elast _ | Econst _ | Econstvar _  -> acc
-
-  let rec read locals acc eq =
-    match eq.eq_desc with
-      | Eeq(pat, e) -> left locals acc e
-      | Ereset(eq_list, e) ->
-          List.fold_left (read locals) (left locals acc e) eq_list
-      | Eautomaton(state_handlers) ->
-          let escapes locals acc e_list =
-            List.fold_left
-              (fun acc { e_cond = e } -> left locals acc e) acc e_list in
-          List.fold_left
-            (fun acc {s_block = b; s_until = e_list1; s_unless = e_list2} ->
-               let new_locals, acc = read_and_locals_block locals acc b in
-               let acc = escapes new_locals acc e_list1 in
-               escapes locals acc e_list2)
-            acc state_handlers
-      | Eswitch(e, switch_handlers) ->
-          List.fold_left
-            (fun acc { w_block = b } -> read_block locals acc b)
-            (left locals acc e) switch_handlers
-      | Epresent(present_handlers, b) ->
-          List.fold_left
-            (fun acc { p_cond = e; p_block = b } ->
-               read_block locals (left locals acc e) b)
-            (read_block locals acc b) present_handlers
-
-  and read_and_locals_block locals acc { b_local = l; b_equs = eq_list } =
-    let locals =
-      List.fold_left
-        (fun acc { v_name = n } -> if IdentSet.mem n acc then acc else IdentSet.add n acc)
-        locals l in
-    locals, List.fold_left (read locals) acc eq_list
-
-  and read_block locals acc b =
-    let _, acc = read_and_locals_block locals acc b in acc
-
-  let rec def locals acc eq =
-    match eq.eq_desc with
-      | Eeq(pat, _) -> vars_pat locals acc pat
-      | Eautomaton(state_handler) ->
-          List.fold_left
-            (fun acc { s_block = b } ->
-               def_block locals acc b) acc state_handler
-      | Eswitch(_, switch_handler) ->
-          List.fold_left
-            (fun acc { w_block = b } ->
-               def_block locals acc b) acc switch_handler
-      | Epresent(present_handler, b) ->
-          List.fold_left
-            (fun acc { p_block = b } -> def_block locals acc b)
-            (def_block locals acc b) present_handler
-      | Ereset(eq_list, _) -> def_list locals acc eq_list
-
-  and def_block locals acc ({ b_local = l; b_equs = eq_list }) =
-    let locals =
-      List.fold_left
-        (fun acc { v_name = n } -> if IdentSet.mem n acc then acc else IdentSet.add n acc)
-        locals l in
-    def_list locals acc eq_list
-
-  and def_list locals acc def_list = List.fold_left (def locals) acc def_list
-
-  let read eq = IdentSet.elements (read IdentSet.empty IdentSet.empty eq)
-  let def eq = IdentSet.elements (def IdentSet.empty IdentSet.empty eq)
-  let antidep eq = false
-  let vars_list pat = IdentSet.elements (vars_pat IdentSet.empty IdentSet.empty pat)
-end
+  
diff --git a/heptagon/parsing/scoping.ml b/heptagon/parsing/scoping.ml
index 35a378c..758e5c6 100644
--- a/heptagon/parsing/scoping.ml
+++ b/heptagon/parsing/scoping.ml
@@ -128,7 +128,7 @@ let rec translate_type const_env = function
       Heptagon.Tprod(List.map (translate_type const_env) ty_list)
   | Tid ln -> Heptagon.Tbase (Heptagon.Tid ln)
   | Tarray (ty, e) -> 
-      let ty = Heptagon.base_type (translate_type const_env ty) in
+      let ty = Heptagon.type (translate_type const_env ty) in
 	Heptagon.Tbase (Heptagon.Tarray (ty, translate_size_exp const_env e))
 
 and translate_exp const_env env e = 
@@ -178,7 +178,7 @@ and translate_desc loc const_env env = function
       let e_list = List.map (translate_exp const_env env) e_list in
 	(match e_list with
 	   | [{ Heptagon.e_desc = Heptagon.Econst c }; e1 ] -> 
-	       Heptagon.Econst (Heptagon.Cconst_array (Heptagon.size_exp_of_exp e1, c))
+	       Heptagon.Econst (Heptagon.Carray (Heptagon.size_exp_of_exp e1, c))
 	   | _ -> Heptagon.Eapp (translate_app const_env env app, e_list)
 	)
   | Eapp (app, e_list) ->
@@ -244,7 +244,7 @@ and translate_switch_handler loc const_env env sh =
 
 and translate_var_dec const_env env vd = 
   { Heptagon.v_name = Rename.name vd.v_loc env vd.v_name;
-    Heptagon.v_type = Heptagon.base_type (translate_type const_env vd.v_type);
+    Heptagon.v_type = Heptagon.type (translate_type const_env vd.v_type);
     Heptagon.v_linearity = vd.v_linearity;
     Heptagon.v_last = translate_last env vd.v_last;
     Heptagon.v_loc = vd.v_loc } 
@@ -285,7 +285,7 @@ let translate_typedec const_env ty =
     | Type_enum(tag_list) -> Heptagon.Type_enum(tag_list)
     | Type_struct(field_ty_list) ->
 	let translate_field_type (f,ty) = 
-	  f, Heptagon.base_type (translate_type const_env ty)
+	  f, Heptagon.type (translate_type const_env ty)
 	in
 	  Heptagon.Type_struct (List.map translate_field_type field_ty_list)
   in
@@ -295,7 +295,7 @@ let translate_typedec const_env ty =
 
 let translate_const_dec const_env cd =
   { Heptagon.c_name = cd.c_name;
-    Heptagon.c_type = Heptagon.base_type (translate_type const_env cd.c_type);
+    Heptagon.c_type = Heptagon.type (translate_type const_env cd.c_type);
     Heptagon.c_value = translate_size_exp const_env cd.c_value;
     Heptagon.c_loc = cd.c_loc; }
 
@@ -309,7 +309,7 @@ let translate_program p =
 
 let translate_signature const_env s =
   let translate_field_type (f,(ty,lin)) = 
-    f, Heptagon.base_type (translate_type const_env ty), lin
+    f, Heptagon.type (translate_type const_env ty), lin
   in
     
   let const_env = build_id_list no_location const_env s.sig_params in
diff --git a/heptagon/printer.ml b/heptagon/printer.ml
index 5042bbc..8423936 100644
--- a/heptagon/printer.ml
+++ b/heptagon/printer.ml
@@ -19,6 +19,15 @@ open Modules
 open Static
 open Format
 
+
+
+let iterator_to_string i = 
+  match i with 
+    | Imap -> "map"
+    | Ifold -> "fold"
+    | Imapfold -> "mapfold"
+
+
 let rec print_list ff print sep l =
   match l with
     | [] -> ()
@@ -69,18 +78,18 @@ let rec print_pat ff = function
       print_list ff print_pat "," pat_list;
       fprintf ff ")@]"
 
-let rec print_base_type ff = function
+let rec print_type ff = function
   | Tint -> fprintf ff  "int"
   | Tbool -> fprintf ff "bool"
   | Tfloat -> fprintf ff  "float"
   | Tid(id) -> print_longname ff id
   | Tarray(ty, e) ->
-      print_base_type ff ty;
+      print_type ff ty;
       fprintf ff "^";
       print_size_exp ff e;
 
 and print_type ff = function
-  | Tbase(base_ty) -> print_base_type ff base_ty
+  | Tbase(ty) -> print_type ff ty
   | Tprod(ty_list) ->
       fprintf ff "@[(";
       print_list ff print_type " *" ty_list;
@@ -90,7 +99,7 @@ and print_c ff = function
   | Cint i -> fprintf ff "%d" i
   | Cfloat f -> fprintf ff "%f" f
   | Cconstr(tag) -> print_longname ff tag
-  | Cconst_array (n, c) ->
+  | Carray (n, c) ->
       print_c ff c;
       fprintf ff "^";
       print_size_exp ff n
@@ -100,7 +109,7 @@ and print_vd ff { v_name = n; v_type = ty; v_last = last } =
   begin match last with Last _ -> fprintf ff "last " | _ -> () end;
   print_ident ff n;
   fprintf ff ": ";
-  print_base_type ff ty;
+  print_type ff ty;
   begin
     match last with Last(Some(v)) -> fprintf ff "= ";print_c ff v
       | _ -> ()
@@ -378,14 +387,14 @@ let print_type_def ff { t_name = name; t_desc = tdesc } =
           (fun ff (field, ty) ->
              print_name ff field;
              fprintf ff ": ";
-             print_base_type ff ty) ";" f_ty_list;
+             print_type ff ty) ";" f_ty_list;
         fprintf ff "}@]@.@]"
 
 let print_const_dec ff c =
   fprintf ff "@[const ";
   print_name ff c.c_name;
   fprintf ff " : ";
-  print_base_type ff c.c_type;
+  print_type ff c.c_type;
   fprintf ff " = ";
   print_size_exp ff c.c_value;
   fprintf ff "@.@]"
diff --git a/main/hept2mls.ml b/main/hept2mls.ml
index b845498..91de560 100644
--- a/main/hept2mls.ml
+++ b/main/hept2mls.ml
@@ -75,7 +75,7 @@ let equation locals l_eqs e =
   let n = Ident.fresh "ck" in
   n,
   { v_name = n; v_copy_of = None;
-    v_type = exp_base_type e; v_linearity = NotLinear; v_clock = Cbase } :: locals,
+    v_type = exp_type e; v_linearity = NotLinear; v_clock = Cbase } :: locals,
   { p_lhs = Evarpat(n); p_rhs = e } :: l_eqs
 
 (* inserts the definition [x,e] into the set of shared equations *)
@@ -190,7 +190,7 @@ let rec const = function
   | Heptagon.Cint i -> Cint i
   | Heptagon.Cfloat f -> Cfloat f
   | Heptagon.Cconstr t -> Cconstr t
-  | Heptagon.Cconst_array(n, c) -> Cconst_array(n, const c)
+  | Heptagon.Carray(n, c) -> Carray(n, const c)
 
 open Format
 
@@ -221,7 +221,7 @@ let application env { Heptagon.a_op = op;  Heptagon.a_inlined = inlined } e_list
   store the bounds (which will be used at code generation time, where the types 
   are harder to find). *)
     | Heptagon.Eselect_dyn, e::defe::idx_list ->
-	let bounds = bounds_list (exp_base_type e)  in
+	let bounds = bounds_list (exp_type e)  in
 	Eselect_dyn (idx_list, bounds,
 		     e, defe)
     | Heptagon.Eupdate idx_list, [e1;e2] ->
@@ -304,14 +304,14 @@ let rec translate_pat = function
   | Heptagon.Etuplepat(l) -> Etuplepat (List.map translate_pat l)
 
 let rec rename_pat ni locals s_eqs = function
-  | Heptagon.Evarpat(n), Heptagon.Tbase(base_ty) ->
+  | Heptagon.Evarpat(n), Heptagon.Tbase(ty) ->
       if IdentSet.mem n ni then
         let n_copy = Ident.fresh (sourcename n) in
-        let base_ty = translate_btype base_ty in
+        let ty = translate_btype ty in
         Evarpat(n_copy),
       { v_name = n_copy; v_copy_of = None;
-	v_type = base_ty; v_linearity = NotLinear; v_clock = Cbase } :: locals,
-      add n (make_exp (Evar n_copy) (Tbase(base_ty)) NotLinear Cbase no_location)
+	v_type = ty; v_linearity = NotLinear; v_clock = Cbase } :: locals,
+      add n (make_exp (Evar n_copy) (Tbase(ty)) NotLinear Cbase no_location)
         s_eqs
       else Evarpat n, locals, s_eqs
   | Heptagon.Etuplepat(l), Heptagon.Tprod(l_ty) ->
@@ -325,7 +325,7 @@ let rec rename_pat ni locals s_eqs = function
   | _ -> assert false
 
 let all_locals ni p =
-  IdentSet.is_empty (IdentSet.inter (Heptagon.Vars.vars_pat IdentSet.empty IdentSet.empty p) ni)
+  IdentSet.is_empty (IdentSet.inter (Heptagon.vars_pat p) ni)
 
 let rec translate_eq env ni (locals, l_eqs, s_eqs) eq =
   match Heptagon.eqdesc eq with
diff --git a/minils/minils.ml b/minils/minils.ml
index 2940871..3fa34ac 100644
--- a/minils/minils.ml
+++ b/minils/minils.ml
@@ -21,11 +21,10 @@ open Interference_graph
 open Global
 open Static
 
-(** Inlining policies, to be held in app records. *)
-type inlining_policy =
-  | Ino (** Do not inline. *)
-  | Ione (** Just inline on one step. *)
-  | Irec (** Recursively inline all sub-calls. *)
+type iterator_name = 
+  | Imap
+  | Ifold
+  | Imapfold
 
 type type_dec =
     { t_name: name;
@@ -35,7 +34,7 @@ type type_dec =
 and tdesc =
   | Type_abs
   | Type_enum of name list
-  | Type_struct of (name * base_ty) list
+  | Type_struct of (name * ty) list
 
 and exp =
     { e_desc: desc;        (* its descriptor *)
@@ -49,7 +48,6 @@ and desc =
   | Evar of ident
   | Econstvar of name
   | Efby of const option * exp
-  | Ereset_mem of ident * const * ident
   | Etuple of exp list
   | Eop of longname * size_exp list * exp list
   | Eapp of app * size_exp list * exp list
@@ -89,19 +87,19 @@ and link =
   | Clink of ck
 
 and ty =
-  | Tbase of base_ty
+  | Tbase of ty
   | Tprod of ty list
 
-and base_ty =
+and ty =
   | Tint | Tfloat
   | Tid of longname
-  | Tarray of base_ty * size_exp
+  | Tarray of ty * size_exp
 
 and const =
   | Cint of int
   | Cfloat of float
   | Cconstr of longname
-  | Cconst_array of size_exp * const 
+  | Carray of size_exp * const 
 
 and pat =
   | Etuplepat of pat list
@@ -114,7 +112,7 @@ type eq =
 type var_dec =
     { v_name : ident;
       v_copy_of : ident option;
-      v_type : base_ty;
+      v_type : ty;
       v_linearity : linearity;
       v_clock : ck }
 
@@ -135,7 +133,7 @@ type node_dec =
       n_equs   : eq list;
       n_loc    : location; 
       n_targeting : (int*int) list;
-      n_mem_alloc : (base_ty * ivar list) list;
+      n_mem_alloc : (ty * ivar list) list;
       n_states_graph : (name,name) interf_graph;
       n_params : name list; 
       n_params_constraints : size_constr list;
@@ -162,13 +160,24 @@ let make_dummy_exp desc ty =
     e_ck = Cbase; e_loc = no_location }
 
 (* Helper functions to work with types *)
-let base_type = function
+let type = function
     | Tbase(bty) -> bty
     | Tprod _ -> assert false
 
+(*TODO Cedric *)
+type ivar = | IVar of ident | IField of ident * longname
+
+(** [filter_vars l] returns a list of variables identifiers from
+    a list of ivar.*)
+let rec filter_vars =
+  function
+  | [] -> []
+  | IVar id :: l -> id :: (filter_vars l)
+  | _ :: l -> filter_vars l
+
 (* get the type of an expression ; assuming that this type is a base type *)
-let exp_base_type e = 
-  base_type e.e_ty
+let exp_type e = 
+  type e.e_ty
 
 let rec size_exp_of_exp e =
   match e.e_desc with 
@@ -423,17 +432,17 @@ struct
         print_list ff print_pat "," pat_list;
         fprintf ff ")@]"
 
-  let rec print_base_type ff = function
+  let rec print_type ff = function
     | Tint -> fprintf ff  "int"
     | Tfloat -> fprintf ff  "float"
     | Tid(id) -> print_longname ff id
     | Tarray(ty, n) -> 
-	print_base_type ff ty;
+	print_type ff ty;
 	fprintf ff "^";
 	print_size_exp ff n
 
   let rec print_type ff = function
-    | Tbase(base_ty) -> print_base_type ff base_ty
+    | Tbase(ty) -> print_type ff ty
     | Tprod(ty_list) ->
         fprintf ff "@[(";
         print_list ff print_type " *" ty_list;
@@ -459,7 +468,7 @@ struct
     fprintf ff "@[<v>";
     print_ident ff n;
     fprintf ff ":";
-    print_base_type ff ty;
+    print_type ff ty;
     fprintf ff " at ";
     print_ck ff ck;
     fprintf ff "@]"
@@ -468,7 +477,7 @@ struct
     | Cint i -> fprintf ff "%d" i
     | Cfloat f -> fprintf ff "%f" f
     | Cconstr(tag) -> print_longname ff tag
-    | Cconst_array (n, c) ->
+    | Carray (n, c) ->
 	print_c ff c;
 	fprintf ff "^";
 	print_size_exp ff n
@@ -675,7 +684,7 @@ struct
           print_list ff
             (fun ff (field, ty) -> print_name ff field;
                fprintf ff ": ";
-               print_base_type ff ty) ";" f_ty_list;
+               print_type ff ty) ";" f_ty_list;
           fprintf ff "}@]@\n@]"
 
   let print_contract ff {c_local = l;
diff --git a/minils/sequential/c.ml b/minils/sequential/c.ml
index 035f0d0..8083a64 100644
--- a/minils/sequential/c.ml
+++ b/minils/sequential/c.ml
@@ -167,8 +167,8 @@ let rec pp_array_decl cty =
    syntax! *)
 let rec pp_vardecl fmt (s, cty) = match cty with
   | Cty_arr (n, cty') -> 
-      let base_ty, indices = pp_array_decl cty in
-	fprintf fmt "%a %s%s" pp_cty base_ty s indices
+      let ty, indices = pp_array_decl cty in
+	fprintf fmt "%a %s%s" pp_cty ty s indices
   | _ -> fprintf fmt "%a %s" pp_cty cty s
 and pp_paramdecl fmt (s, cty) = match cty with
   | Cty_arr (n, cty') -> fprintf fmt "%a* %s" pp_cty cty' s
diff --git a/minils/sequential/cgen.ml b/minils/sequential/cgen.ml
index b0b0a21..9f35187 100644
--- a/minils/sequential/cgen.ml
+++ b/minils/sequential/cgen.ml
@@ -107,7 +107,7 @@ let node_info classln =
 let output_names_list sig_info = 
   let remove_option ad = match ad.a_name with
     | Some n -> n
-    | None -> Error.message no_location Error.Eno_unnamed_output
+    | None -> Error.message no_location Error.Eno_unnamed_output (*TODO fresh*)
   in
     List.map remove_option sig_info.info.outputs
 
@@ -142,7 +142,7 @@ let rec ctype_of_otype oty =
 
 let ctype_of_heptty ty =
   let ty = Merge.translate_btype ty in
-  let ty = Translate.translate_base_type NamesEnv.empty ty in
+  let ty = Translate.translate_type NamesEnv.empty ty in
     ctype_of_otype ty
 
 let cvarlist_of_ovarlist vl =
@@ -266,7 +266,7 @@ let rec cexpr_of_exp var_env exp =
           | Cint i -> Cconst (Ccint i)
           | Cfloat f -> Cconst (Ccfloat f)
           | Cconstr c -> Cconst (Ctag (shortname c))
-	  | Cconst_array(n,c) -> 
+	  | Carray(n,c) -> 
 	      let cc = cexpr_of_exp var_env (Const c) in
 		Carraylit (repeat_list cc n)
         end
@@ -415,7 +415,7 @@ let generate_function_call var_env obj_env outvl objn args mem =
 (** Create the statement dest = c where c = v^n^m... *)
 let rec create_affect_const var_env dest c =
   match c with
-    | Cconst_array(n,c) -> 
+    | Carray(n,c) -> 
 	let x = gen_symbol () in
 	  [ Cfor(x, 0, n, 
 		create_affect_const var_env (Carray (dest, Clhs (Cvar x))) c) ]
diff --git a/minils/sequential/mls2obc.ml b/minils/sequential/mls2obc.ml
index c1b24ff..fda05df 100644
--- a/minils/sequential/mls2obc.ml
+++ b/minils/sequential/mls2obc.ml
@@ -54,22 +54,22 @@ let is_op = function
   | _ -> false
 
 let rec translate_type const_env = function
-  | Minils.Tbase(btyp) -> translate_base_type const_env btyp
+  | Minils.Tbase(btyp) -> translate_type const_env btyp
   | Minils.Tprod _     -> assert false
 
-and translate_base_type const_env = function
+and translate_type const_env = function
   | Minils.Tint -> Tint
   | Minils.Tfloat  -> Tfloat
   | Minils.Tid(id) -> Tid(id)
-  | Minils.Tarray(ty, n) -> Tarray (translate_base_type const_env ty,
+  | Minils.Tarray(ty, n) -> Tarray (translate_type const_env ty,
 				    int_of_size_exp const_env n)
 
 let rec translate_const const_env = function
   | Minils.Cint(v) -> Cint(v)
   | Minils.Cfloat(v) -> Cfloat(v)
   | Minils.Cconstr(c) -> Cconstr(c)
-  | Minils.Cconst_array(n,c) -> 
-      Cconst_array(int_of_size_exp const_env n, translate_const const_env c)
+  | Minils.Carray(n,c) -> 
+      Carray(int_of_size_exp const_env n, translate_const const_env c)
 
 let rec translate_pat map = function
   | Minils.Evarpat(x) -> [var_from_name map x]
@@ -259,7 +259,7 @@ let obj_decl l = List.map (fun (x, t, i) -> { obj = x; cls = t; n = i }) l
 
 let translate_var_dec const_env map l =
   let one_var { Minils.v_name = x; Minils.v_type = t } =
-     { v_name = x; v_type = translate_base_type const_env t; v_pass_by_ref = false }
+     { v_name = x; v_type = translate_type const_env t; v_pass_by_ref = false }
   in
     (* remove unused vars *)
   let l = List.filter (fun { Minils.v_name = x } -> 
@@ -395,7 +395,7 @@ let translate_ty_def const_env { Minils.t_name = name; Minils.t_desc = tdesc } =
     | Minils.Type_enum(tag_name_list) -> Type_enum(tag_name_list)
     | Minils.Type_struct(field_ty_list) ->
         Type_struct
-          (List.map (fun (f, ty) -> (f, translate_base_type const_env ty)) field_ty_list)
+          (List.map (fun (f, ty) -> (f, translate_type const_env ty)) field_ty_list)
   in
   { t_name = name; t_desc = tdesc }
 
diff --git a/minils/sequential/obc.ml b/minils/sequential/obc.ml
index d927bbc..2a1de98 100644
--- a/minils/sequential/obc.ml
+++ b/minils/sequential/obc.ml
@@ -23,6 +23,12 @@ type obj_name = name
 type op_name = longname
 type field_name = longname
 
+type iterator_name = 
+  | Imap
+  | Ifold
+  | Imapfold
+
+
 type ty =
     | Tint
     | Tfloat
@@ -42,7 +48,7 @@ type const =
     | Cint of int
     | Cfloat of float
     | Cconstr of longname
-    | Cconst_array of int * const
+    | Carray of int * const
 
 type lhs =
   | Var of var_name
@@ -108,24 +114,11 @@ type program =
 (** [is_scalar_type vd] returns whether the type corresponding
     to this variable declaration is scalar (ie a type that can
     be returned by a C function). *)
-let is_scalar_type vd =
-  let pint = Modname({ qual = "Pervasives"; id = "int" }) in
-  let pfloat = Modname({ qual = "Pervasives"; id = "float" }) in
-  let pbool = Modname({ qual = "Pervasives"; id = "bool" }) in
-    match vd.v_type with
-      | Tint | Tfloat -> true
-      | Tid name_int when name_int = pint -> true
-      | Tid name_float when name_float = pfloat -> true
-      | Tid name_bool when name_bool = pbool -> true
-      | _ -> false 
-
-let actual_type ty =
+let is_scalar_type ty =
   match ty with
-    | Tid(Name("float"))
-    | Tid(Modname { qual = "Pervasives"; id = "float" }) -> Tfloat
-    | Tid(Name("int"))
-    | Tid(Modname { qual = "Pervasives"; id = "int" }) -> Tint
-    | _ -> ty
+  | Tid x ->
+      (x = Initial.pint) or (x = Initial.pfloat) or (x = Initial.pbool)
+  | _ -> false
 
 let rec var_name x =
   match x with
@@ -220,7 +213,7 @@ struct
     | Cint i       -> fprintf ff "%d" i
     | Cfloat f     -> fprintf ff "%f" f
     | Cconstr(tag) -> print_longname ff tag
-    | Cconst_array(n,c) ->
+    | Carray(n,c) ->
 	print_c ff c;
 	fprintf ff "^%d" n
 
diff --git a/minils/transformations/normalize.ml b/minils/transformations/normalize.ml
index 11e6d74..a46ae02 100644
--- a/minils/transformations/normalize.ml
+++ b/minils/transformations/normalize.ml
@@ -20,7 +20,7 @@ and cfalse = Name("false")
 let equation (d_list, eq_list) ({ e_ty = te; e_linearity = l; e_ck = ck } as e) =
   let n = Ident.fresh "_v" in
   let d_list = { v_name = n; v_copy_of = None;
-		 v_type = base_type te; v_linearity = l; v_clock = ck } :: d_list
+		 v_type = type te; v_linearity = l; v_clock = ck } :: d_list
   and eq_list = { p_lhs = Evarpat(n); p_rhs = e } :: eq_list in
   (d_list, eq_list), n
 
diff --git a/utilities/misc.ml b/utilities/misc.ml
index 9d6438b..b1f4bcf 100644
--- a/utilities/misc.ml
+++ b/utilities/misc.ml
@@ -7,11 +7,9 @@
 (*                                                                        *)
 (**************************************************************************)
 (* useful stuff *)
-(* $Id$ *)
 
 (* version of the compiler *)
 let version = "0.4"
-let interface_format_version = "5"
 let date = "DATE"
 
 (* standard module *)
@@ -142,17 +140,6 @@ let unique l =
   List.iter (fun i -> Hashtbl.replace tbl i ()) l;
   Hashtbl.fold (fun key data accu -> key :: accu) tbl []
 
-type iterator_name = 
-    Imap
-  | Ifold
-  | Imapfold
-
-let iterator_to_string i = 
-  match i with 
-    | Imap -> "map"
-    | Ifold -> "fold"
-    | Imapfold -> "mapfold"
-
 let rec incomplete_map f l =
   match l with 
     | [] -> []
diff --git a/utilities/misc.mli b/utilities/misc.mli
index 1c8f22c..425c7a5 100644
--- a/utilities/misc.mli
+++ b/utilities/misc.mli
@@ -7,11 +7,9 @@
 (*                                                                        *)
 (**************************************************************************)
 
-(* $Id$ *)
 
 (* Version and date of compilation *)
 val version : string
-val interface_format_version: string
 val date : string
 
 (* List of modules initially opened *)