From 81947eca40c01c3671016179aae55220c36955fa Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?C=C3=A9dric=20Pasteur?= <cedric.pasteur@ens.fr>
Date: Wed, 7 Sep 2011 17:51:31 +0200
Subject: [PATCH] Made linearity field not optional

This helped solve a few bugs with linear types,
for instance when using automata.
The intermediate code is not well-typed (wrt to
linear types only), after the encoding of automata.
---
 compiler/heptagon/analysis/hept_clocking.ml   |   2 +
 compiler/heptagon/analysis/typing.ml          |  28 +--
 compiler/heptagon/hept_utils.ml               |   8 +-
 compiler/heptagon/heptagon.ml                 |   2 +-
 compiler/heptagon/transformations/automata.ml |  31 +--
 compiler/heptagon/transformations/boolean.ml  | 176 +++++++++---------
 .../heptagon/transformations/completion.ml    |   6 +-
 compiler/heptagon/transformations/inline.ml   |   5 +-
 compiler/heptagon/transformations/itfusion.ml |  36 ++--
 compiler/heptagon/transformations/last.ml     |  10 +-
 .../heptagon/transformations/normalize.ml     |  36 ++--
 compiler/heptagon/transformations/reset.ml    |   9 +-
 compiler/heptagon/transformations/switch.ml   |  14 +-
 compiler/main/hept2mls.ml                     |  13 +-
 compiler/minils/analysis/clocking.ml          |   4 +-
 compiler/minils/analysis/interference.ml      |   4 +-
 compiler/minils/minils.ml                     |  12 +-
 compiler/minils/mls_utils.ml                  |   2 +-
 .../minils/transformations/normalize_mem.ml   |   8 +-
 compiler/minils/transformations/tomato.ml     |  30 ++-
 test/good/linear_automata.ept                 |  25 ++-
 21 files changed, 265 insertions(+), 196 deletions(-)

diff --git a/compiler/heptagon/analysis/hept_clocking.ml b/compiler/heptagon/analysis/hept_clocking.ml
index 204056e..1d26c47 100644
--- a/compiler/heptagon/analysis/hept_clocking.ml
+++ b/compiler/heptagon/analysis/hept_clocking.ml
@@ -111,6 +111,7 @@ let rec typing h pat e =
 			    (Econst (Initial.mk_static_int 0))
 			    ~ct_annot:(Some(Ck(base_ck)))
 			    Initial.tint
+          ~linearity:Linearity.Ltop
 			 ) nl
               in
               typing_app h base_ck pat op (pargs@args@il)
@@ -126,6 +127,7 @@ let rec typing h pat e =
 			    (Econst (Initial.mk_static_int 0))
 			    ~ct_annot:(Some(Ck(base_ck)))
 			    Initial.tint
+          ~linearity:Linearity.Ltop
 			 ) nl
               in
               let rec insert_i args = match args with
diff --git a/compiler/heptagon/analysis/typing.ml b/compiler/heptagon/analysis/typing.ml
index 4986f35..592f04a 100644
--- a/compiler/heptagon/analysis/typing.ml
+++ b/compiler/heptagon/analysis/typing.ml
@@ -23,7 +23,7 @@ open Hept_mapfold
 open Pp_tools
 open Format
 
-type value = { ty: ty; mutable last: bool }
+type value = { vd: var_dec; mutable last: bool }
 
 type error =
   | Emissing of name
@@ -235,7 +235,13 @@ let kind f ty_desc =
 
 let typ_of_name h x =
   try
-    let { ty = ty } = Env.find x h in ty
+    let { vd = vd } = Env.find x h in vd.v_type
+  with
+      Not_found -> error (Eundefined(name x))
+
+let vd_of_name h x =
+  try
+    let { vd = vd } = Env.find x h in vd
   with
       Not_found -> error (Eundefined(name x))
 
@@ -258,11 +264,11 @@ let rec subst_type_vars m = function
   | Tprod l -> Tprod (List.map (subst_type_vars m) l)
   | t -> t
 
-let add_distinct_env id ty env =
+let add_distinct_env id vd env =
   if Env.mem id env then
     error (Ealready_defined(name id))
   else
-    Env.add id ty env
+    Env.add id vd env
 
 let add_distinct_qualset n acc =
   if QualSet.mem n acc then
@@ -309,8 +315,8 @@ let rec merge local_names_list =
   let two s1 s2 =
     let total, partial = Env.partition (fun elt -> Env.mem elt s2) s1 in
     let partial =
-      Env.fold (fun elt ty env ->
-                  if not (Env.mem elt total) then Env.add elt ty env
+      Env.fold (fun elt vd env ->
+                  if not (Env.mem elt total) then Env.add elt vd env
                   else env)
         s2 partial in
     total, partial in
@@ -951,9 +957,9 @@ and typing_node_params cenv params_sig params =
 
 let rec typing_pat h acc = function
   | Evarpat(x) ->
-      let ty = typ_of_name h x in
-      let acc = add_distinct_env x ty acc in
-      acc, ty
+      let vd = vd_of_name h x in
+      let acc = add_distinct_env x vd acc in
+      acc, vd.v_type
   | Etuplepat(pat_list) ->
       let acc, ty_list =
         List.fold_right
@@ -1097,8 +1103,8 @@ and build cenv h dec =
       if Env.mem vd.v_ident h then
         error (Ealready_defined(name vd.v_ident));
 
-      let acc_defined = Env.add vd.v_ident ty acc_defined in
-      let h = Env.add vd.v_ident { ty = ty; last = last vd.v_last } h in
+      let acc_defined = Env.add vd.v_ident vd acc_defined in
+      let h = Env.add vd.v_ident { vd = vd; last = last vd.v_last } h in
       { vd with v_last = last_dec; v_type = ty }, (acc_defined, h)
     with
         TypingError(kind) -> message vd.v_loc kind
diff --git a/compiler/heptagon/hept_utils.ml b/compiler/heptagon/hept_utils.ml
index 10d11b6..93f5690 100644
--- a/compiler/heptagon/hept_utils.ml
+++ b/compiler/heptagon/hept_utils.ml
@@ -21,7 +21,7 @@ open Heptagon
 
 (* Helper functions to create AST. *)
 (* TODO : After switch, all mk_exp should take care of level_ck *)
-let mk_exp desc ?(linearity = Ltop) ?(level_ck = Cbase) ?(ct_annot = None) ?(loc = no_location) ty =
+let mk_exp desc ?(level_ck = Cbase) ?(ct_annot = None) ?(loc = no_location) ty ~linearity =
   { e_desc = desc; e_ty = ty; e_ct_annot = ct_annot; e_linearity = linearity;
     e_level_ck = level_ck; e_loc = loc; }
 
@@ -41,7 +41,7 @@ let mk_equation ?(loc=no_location) desc =
     eq_inits = Lno_init;
     eq_loc = loc; }
 
-let mk_var_dec ?(last = Var) ?(linearity = Ltop) ?(clock = fresh_clock()) name ty =
+let mk_var_dec ?(last = Var) ?(clock = fresh_clock()) name ty ~linearity =
   { v_ident = name; v_type = ty; v_linearity = linearity; v_clock = clock;
     v_last = last; v_loc = no_location }
 
@@ -50,9 +50,9 @@ let mk_block ?(stateful = true) ?(defnames = Env.empty) ?(locals = []) eqs =
     b_stateful = stateful; b_loc = no_location; }
 
 let dfalse =
-  mk_exp (Econst (mk_static_bool false)) (Tid Initial.pbool)
+  mk_exp (Econst (mk_static_bool false)) (Tid Initial.pbool) ~linearity:Ltop
 let dtrue =
-  mk_exp (Econst (mk_static_bool true)) (Tid Initial.pbool)
+  mk_exp (Econst (mk_static_bool true)) (Tid Initial.pbool) ~linearity:Ltop
 
 let mk_ifthenelse e1 e2 e3 =
   { e3 with e_desc = mk_op_app Eifthenelse [e1; e2; e3] }
diff --git a/compiler/heptagon/heptagon.ml b/compiler/heptagon/heptagon.ml
index 6b54fa5..63f8b26 100644
--- a/compiler/heptagon/heptagon.ml
+++ b/compiler/heptagon/heptagon.ml
@@ -96,7 +96,7 @@ and eqdesc =
 and block = {
   b_local     : var_dec list;
   b_equs      : eq list;
-  b_defnames  : ty Env.t;
+  b_defnames  : var_dec Env.t;
   b_stateful : bool;
   b_loc       : location; }
 
diff --git a/compiler/heptagon/transformations/automata.ml b/compiler/heptagon/transformations/automata.ml
index 6ac1c77..4102d6d 100644
--- a/compiler/heptagon/transformations/automata.ml
+++ b/compiler/heptagon/transformations/automata.ml
@@ -25,10 +25,11 @@ let fresh = Idents.gen_fresh "automata"
   (function S -> "s" | NS -> "ns" | R -> "r" | NR -> "nr" | PNR -> "pnr")
 
 let mk_var_exp n ty =
-  mk_exp (Evar n) ty
+  mk_exp (Evar n) ty ~linearity:Linearity.Ltop
 
 let mk_pair e1 e2 =
   mk_exp (mk_op_app Etuple [e1;e2]) (Tprod [e1.e_ty; e2.e_ty])
+    ~linearity:(Linearity.Ltuple [Linearity.Ltop; Linearity.Ltop])
 
 let mk_reset_equation eq_list e =
   mk_equation (Ereset (mk_block eq_list, e))
@@ -38,7 +39,7 @@ let mk_switch_equation e l =
 
 let mk_exp_fby_false e =
   mk_exp (Epre (Some (mk_static_bool false), e))
-    (Tid Initial.pbool)
+    (Tid Initial.pbool) ~linearity:Linearity.Ltop
 
 let mk_constructor constr ty =
   mk_static_exp ty (Sconstructor constr)
@@ -95,7 +96,9 @@ let translate_automaton v eq_list handlers =
   let pre_next_resetname = fresh PNR in
 
   let name n = NamesEnv.find n state_env in
-  let state n = mk_exp (Econst (mk_constructor (name n) tstatetype)) tstatetype in
+  let state n =
+    mk_exp (Econst (mk_constructor (name n) tstatetype)) tstatetype ~linearity:Linearity.Ltop
+  in
   let statevar n = mk_var_exp n tstatetype in
   let boolvar n = mk_var_exp n (Tid Initial.pbool) in
 
@@ -107,8 +110,10 @@ let translate_automaton v eq_list handlers =
   in
 
   let strong { s_state = n; s_unless = su } =
-    let defnames = Env.add resetname (Tid Initial.pbool) Env.empty in
-    let defnames = Env.add statename tstatetype defnames in
+    let rst_vd = mk_var_dec resetname (Tid Initial.pbool) Linearity.Ltop in
+    let defnames = Env.add resetname rst_vd Env.empty in
+    let state_vd = mk_var_dec statename tstatetype Linearity.Ltop in
+    let defnames = Env.add statename state_vd defnames in
     let st_eq = mk_simple_equation
       (Etuplepat[Evarpat(statename); Evarpat(resetname)])
       (escapes n su (boolvar pre_next_resetname)) in
@@ -117,8 +122,10 @@ let translate_automaton v eq_list handlers =
   in
 
   let weak { s_state = n; s_block = b; s_until = su } =
-    let defnames = Env.add next_resetname (Tid Initial.pbool) b.b_defnames in
-    let defnames = Env.add next_statename tstatetype defnames in
+    let nextrst_vd = mk_var_dec next_resetname (Tid Initial.pbool) Linearity.Ltop in
+    let defnames = Env.add next_resetname nextrst_vd b.b_defnames in
+    let nextstate_vd = mk_var_dec next_statename tstatetype Linearity.Ltop in
+    let defnames = Env.add next_statename nextstate_vd defnames in
     let ns_eq = mk_simple_equation
       (Etuplepat[Evarpat(next_statename); Evarpat(next_resetname)])
       (escapes n su dfalse) in
@@ -130,10 +137,10 @@ let translate_automaton v eq_list handlers =
   in
 
   let v =
-    (mk_var_dec next_statename tstatetype) ::
-      (mk_var_dec resetname (Tid Initial.pbool)) ::
-      (mk_var_dec next_resetname (Tid Initial.pbool)) ::
-      (mk_var_dec pre_next_resetname (Tid Initial.pbool)) :: v in
+    (mk_var_dec next_statename tstatetype ~linearity:Linearity.Ltop) ::
+      (mk_var_dec resetname (Tid Initial.pbool) ~linearity:Linearity.Ltop) ::
+      (mk_var_dec next_resetname (Tid Initial.pbool) ~linearity:Linearity.Ltop) ::
+      (mk_var_dec pre_next_resetname (Tid Initial.pbool) ~linearity:Linearity.Ltop) :: v in
   if no_strong_transition handlers
   then (* Only weak transitions : a Moore automaton. *)
     let switch_e = mk_exp_fby_state initial (statevar next_statename) in
@@ -150,7 +157,7 @@ let translate_automaton v eq_list handlers =
     v, switch_eq :: nr_eq :: pnr_eq :: eq_list
   else (* General case,
           two switch to generate statename variable used and defined *)
-    let v = (mk_var_dec statename tstatetype) :: v in
+    let v = (mk_var_dec statename tstatetype ~linearity:Linearity.Ltop) :: v in
     let ns_switch_e = mk_exp_fby_state initial (statevar next_statename) in
     let ns_switch_handlers =
       List.map (fun ({ s_state = n } as case) ->
diff --git a/compiler/heptagon/transformations/boolean.ml b/compiler/heptagon/transformations/boolean.ml
index 3a74e4a..c4c624c 100644
--- a/compiler/heptagon/transformations/boolean.ml
+++ b/compiler/heptagon/transformations/boolean.ml
@@ -7,7 +7,7 @@
 (*                                                  *)
 (****************************************************)
 
-(* 
+(*
    Translate enumerated types (state variables) into boolean
 
    type t = A | B | C | D
@@ -28,7 +28,7 @@
    (e when A(x))
    -->
    (e when False(x1)) when False(x2_0)
-   
+
    ck on A(x)
    -->
    ck on False(x1) on False(x2_0)
@@ -68,7 +68,7 @@ let mk_tuple e_l =
   Eapp((mk_app Etuple),e_l,None)
 
 (* boolean decision tree ; left branch for true ; nodes are constructors *)
-type btree = Node of constructor_name option | Tree of btree * btree 
+type btree = Node of constructor_name option | Tree of btree * btree
 
 (* Debug
 let print_indent n =
@@ -78,7 +78,7 @@ let print_indent n =
 
 let rec print_btree indent bt =
   match bt with
-  | Node(None) -> 
+  | Node(None) ->
       print_indent indent;
       Printf.printf "None\n"
   | Node(Some c) ->
@@ -111,8 +111,8 @@ let rec print_bl bl =
 
 let print_enuminfo info =
   Printf.printf "{ ty_nb_var = %d;\n  ty_assoc = " info.ty_nb_var;
-  QualEnv.fold 
-    (fun c l () -> 
+  QualEnv.fold
+    (fun c l () ->
        Printf.printf "(%s : " (fullname c);
        print_bl l;
        Printf.printf "), ")
@@ -123,7 +123,7 @@ let print_enuminfo info =
 
 (* ty_nb_var = n : var x of enum type will be represented by
    boolean variables x_1,...,x_n
-   
+
    ty_assoc(A) = [b_1,...,b_n] : constant A will be represented by
    x_1,...,x_n where x_i = b_i
 
@@ -142,12 +142,12 @@ let print_enuminfo info =
    x2_0 being on clock False(x1)
    x2_1 being on clock True(x1)
  *)
-type var_tree = Vempty | VNode of var_ident * var_tree * var_tree 
+type var_tree = Vempty | VNode of var_ident * var_tree * var_tree
 
 (*
 let rec print_var_tree indent t =
   match t with
-  | Vempty -> 
+  | Vempty ->
       print_indent indent;
       Printf.printf "Empty\n"
   | VNode(v,t1,t2) ->
@@ -190,13 +190,13 @@ let print_enum_types () =
     ) !enum_types ()
 *)
 
-let get_enum name = 
+let get_enum name =
   QualEnv.find name !enum_types
 
 (* split2 k [x1;...;xn] = ([x1;...;xk],[xk+1;...;xn]) *)
 let split2 n l =
   let rec splitaux k acc l =
-    if k = 0 then (acc,l) else 
+    if k = 0 then (acc,l) else
       begin
 	match l with
 	| x::t -> splitaux (k-1) (x::acc) t
@@ -212,10 +212,10 @@ let rec var_list clist =
   match clist with
   | [] -> (0,QualEnv.empty,Node(None))
   | [c] -> (1, QualEnv.add c [false] QualEnv.empty, Tree(Node(Some c),Node(None)))
-  | [c1;c2] -> (1, 
+  | [c1;c2] -> (1,
 		QualEnv.add c1 [false] (QualEnv.add c2 [true] QualEnv.empty),
 		Tree(Node(Some c1),Node(Some c2)))
-  | l -> 
+  | l ->
       let n = List.length l in
       let n1 = n asr 1 in
       let l1,l2 = split2 n1 l in
@@ -239,11 +239,11 @@ let rec var_list clist =
 (* 	  | Some n -> n *)
 (* 	end in *)
 (*       assert (nt2 = nv2); *)
-      let vl = 
+      let vl =
 	QualEnv.fold (fun c l m -> QualEnv.add c (true::l) m) vl2
-	  (QualEnv.fold 
-	     (if nv1 = nv2 
-	      then (fun c l m -> QualEnv.add c (false::l) m) 
+	  (QualEnv.fold
+	     (if nv1 = nv2
+	      then (fun c l m -> QualEnv.add c (false::l) m)
 	      else (fun c l m -> QualEnv.add c (false::false::l) m))
 	     vl1
 	     QualEnv.empty) in
@@ -263,7 +263,7 @@ let translate_pat env pat =
   let rec trans = function
     | Evarpat(name) ->
 	begin
-	  try 
+	  try
 	    let info = Env.find name env in
 	    match info.var_enum.ty_nb_var with
 	    | 1 ->
@@ -287,7 +287,7 @@ let translate_ty ty =
 	    begin match info with
 	    | Type(_) -> ty
 	    | Enum { ty_nb_var = 1 } -> ty_bool
-	    | Enum { ty_nb_var = n } -> 
+	    | Enum { ty_nb_var = n } ->
 		let strlist = nvar_list "" n in
 		Tprod(List.map (fun _ -> ty_bool) strlist)
 	    end
@@ -312,7 +312,7 @@ let rec translate_ck env ck =
   | Cbase -> Cbase
   | Cvar {contents = Clink(ck)} -> translate_ck env ck
   | Cvar {contents = Cindex(_)} -> ck
-  | Con(ck,c,n) -> 
+  | Con(ck,c,n) ->
       let ck = translate_ck env ck in
       begin
 	try
@@ -335,22 +335,22 @@ let translate_const c ty e =
   | Sconstructor(cname),Tid(tname) ->
       begin
 	try
-	  begin 
+	  begin
 	    match (get_enum tname) with
 	    | Type _ -> Econst(c)
 	    | Enum { ty_assoc = assoc } ->
 		let bl = QualEnv.find cname assoc in
 		let b_list = List.map (fun b -> Econst(sbool b)) bl in
-		begin 
-		  match b_list with 
+		begin
+		  match b_list with
 		  | [] -> assert false
 		  | [b] -> b
 		  | _::_ ->
 		      mk_tuple
 			(List.map
-			   (fun b -> {e with 
+			   (fun b -> {e with
 					e_desc = b;
-					e_ty = ty_bool }) 
+					e_ty = ty_bool })
 			   b_list)
 		end
 	  end
@@ -364,7 +364,7 @@ let new_var_list d_list ty ck n =
     | n ->
 	let v = fresh "bool" in
 	let acc = v :: acc in
-	let d_list = (mk_var_dec ~clock:ck v ty) :: d_list in
+	let d_list = (mk_var_dec ~clock:ck v ty ~linearity:Linearity.Ltop) :: d_list in
 	varl acc d_list (n-1) in
   varl [] d_list n
 
@@ -373,13 +373,13 @@ let assert_ck = function
   | _ -> assert false
 
 let intro_tuple context e =
-  let n = 
+  let n =
     match e.e_ty with
-    | Tprod(l) -> List.length l 
+    | Tprod(l) -> List.length l
     | _ -> assert false in
   match e.e_desc with
     Eapp({a_op=Etuple},e_l,None) -> context,e_l
-  | _ -> 
+  | _ ->
       let (d_list,eq_list) = context in
       (* e is not a tuple, therefore e.e_ct_annot = Ck(ck) *)
       let ck = assert_ck e.e_ct_annot in
@@ -404,7 +404,7 @@ let rec when_list e bl vtree =
 
 let rec when_ck desc li ty ck =
   match ck with
-  | Cbase | Cvar _ -> 
+  | Cbase | Cvar _ ->
       { e_desc = desc;
 	e_level_ck = ck;
 	e_ct_annot = Some(Ck(ck));
@@ -423,11 +423,11 @@ let rec when_ck desc li ty ck =
 
 let rec base_value ck li ty =
   match ty with
-  | Tid({qual = Pervasives; name = "int" }) -> 
+  | Tid({qual = Pervasives; name = "int" }) ->
       when_ck (Econst(mk_static_exp ty (Sint(0)))) li ty ck
   | Tid({qual = Pervasives; name = "float"}) ->
       when_ck (Econst(mk_static_exp ty (Sfloat(0.)))) li ty ck
-  | Tid({qual = Pervasives; name = "bool" }) ->  
+  | Tid({qual = Pervasives; name = "bool" }) ->
       when_ck (Econst(strue)) li ty ck
   | Tid(sname) ->
       begin
@@ -439,17 +439,17 @@ let rec base_value ck li ty =
 	    | Type(Type_abs) -> failwith("Abstract types not implemented")
 	    | Type(Type_alias aty) -> base_value ck li aty
 	    | Type(Type_enum(l)) ->
-		when_ck 
-		  (Econst(mk_static_exp ty (Sconstructor(List.hd l)))) 
+		when_ck
+		  (Econst(mk_static_exp ty (Sconstructor(List.hd l))))
 		  li ty ck
 	    | Type(Type_struct(l)) ->
 		let fields =
-		  List.map 
-		    (fun {f_name = name; f_type = ty} -> 
-		       name,(base_value ck li ty)) 
+		  List.map
+		    (fun {f_name = name; f_type = ty} ->
+		       name,(base_value ck li ty))
 		    l in
 		when_ck (Estruct(fields)) li ty ck
-	    | Enum { ty_nb_var = 1 } -> 
+	    | Enum { ty_nb_var = 1 } ->
 		when_ck (Econst(strue)) li ty_bool ck
 	    | Enum { ty_nb_var = n } ->
 		let e = when_ck (Econst(strue)) li ty_bool ck in
@@ -486,7 +486,7 @@ let rec base_value ck li ty =
 	e_loc = no_location;
       }
   | Tinvalid -> failwith("Boolean: invalid type")
-  
+
 let rec merge_tree ck ty li e_map btree vtree =
   match btree, vtree with
   | Node(None), _ -> base_value ck li ty
@@ -509,7 +509,7 @@ let rec merge_tree ck ty li e_map btree vtree =
 
 let rec translate env context ({e_desc = desc; e_ty = ty; e_ct_annot = ct} as e) =
   let ct = Misc.optional (translate_ct env) ct in
-  let context,desc = 
+  let context,desc =
     match desc with
     | Econst(c) ->
 	context, translate_const c ty e
@@ -521,8 +521,8 @@ let rec translate env context ({e_desc = desc; e_ty = ty; e_ct_annot = ct} as e)
 	      Evar(List.nth info.var_list 0)
 	    else
 	      let ident_list = info.var_list in
-	      mk_tuple (List.map 
-			  (fun v -> { e with 
+	      mk_tuple (List.map
+			  (fun v -> { e with
 					e_ty = ty_bool;
 					e_ct_annot = ct;
 					e_desc = Evar(v); })
@@ -550,17 +550,17 @@ let rec translate env context ({e_desc = desc; e_ty = ty; e_ct_annot = ct} as e)
 				    | _ -> assert false) e_c_l in
 	      context,
 	      mk_tuple
-		(List.map2 
-		   (fun c e -> { e with 
+		(List.map2
+		   (fun c e -> { e with
 				   e_ty = ty_bool;
 				   e_desc = Epre(Some c,e)})
 		   c_l e_l)
 	  | _ -> assert false
 	end
-    | Eapp(app, e_list, r) -> 
+    | Eapp(app, e_list, r) ->
 	let context,e_list = translate_list env context e_list in
 	context, Eapp(app, e_list, r)
-    | Ewhen(e,c,ck) -> 
+    | Ewhen(e,c,ck) ->
 	let context,e = translate env context e in
 	begin
 	  try
@@ -573,18 +573,18 @@ let rec translate env context ({e_desc = desc; e_ty = ty; e_ct_annot = ct} as e)
 	    context,Ewhen(e,c,ck)
 	end
     | Emerge(ck,l) (* of name * (longname * exp) list *)
-      -> 
+      ->
 	begin
 	  try
 	    let info = Env.find ck env in
-	    let context,e_map = List.fold_left 
-	      (fun (context,e_map) (n,e) -> 
+	    let context,e_map = List.fold_left
+	      (fun (context,e_map) (n,e) ->
 		 let context,e = translate env context e in
-		 context,QualEnv.add n e e_map)  
+		 context,QualEnv.add n e e_map)
 	      (context,QualEnv.empty) l in
-	    let e_merge = 
-	      merge_tree (assert_ck ct) ty e.e_linearity e_map 
-		info.var_enum.ty_tree 
+	    let e_merge =
+	      merge_tree (assert_ck ct) ty e.e_linearity e_map
+		info.var_enum.ty_tree
 		info.clocked_var in
 	    context,e_merge.e_desc
 	  with Not_found ->
@@ -601,32 +601,32 @@ let rec translate env context ({e_desc = desc; e_ty = ty; e_ct_annot = ct} as e)
 	let context,e1 = translate env context e1 in
 	let context,e2 = translate env context e2 in
 	context,Esplit(e1,e2)
-    | Estruct(l) -> 
-	let context,acc = 
-	  List.fold_left 
-	    (fun (context,acc) (c,e) -> 
+    | Estruct(l) ->
+	let context,acc =
+	  List.fold_left
+	    (fun (context,acc) (c,e) ->
 	       let context,e = translate env context e in
-	       (context,(c,e)::acc)) 
+	       (context,(c,e)::acc))
 	    (context,[]) l in
 	context,Estruct(List.rev acc)
     | 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,pe_list,e_list,r)
-    | Elast _ -> 
+    | Elast _ ->
 	failwith("Boolean: not supported expression (abstract tree should be normalized)")
   in
   context,{ e with
 	      e_desc = desc;
 	      e_ty = translate_ty ty;
 	      e_ct_annot = ct}
-    
-and translate_list env context e_list = 
-  let context,acc_e = 
-    List.fold_left 
-      (fun (context,acc_e) e -> 
+
+and translate_list env context e_list =
+  let context,acc_e =
+    List.fold_left
+      (fun (context,acc_e) e ->
 	 let context,e = translate env context e in
-	 (context,e::acc_e)) 
+	 (context,e::acc_e))
       (context,[]) e_list in
   context,List.rev acc_e
 
@@ -636,14 +636,14 @@ and translate_list env context e_list =
    - equations of these added variables
 *)
 let var_dec_list (acc_vd,acc_loc,acc_eq) var_from n =
-  
+
   (* when_ck [v3_1_0;v2_1;v1] (ck on True(v1) on False(v2_1) on True(v3_1_0)) v4
      = ((v4 when True(v1)) when False(v2_1)) when True(v3_1_0)
      -> builds v4_1_0_1
   *)
   let rec when_ck ckvar_list ck var =
     match ckvar_list,ck with
-    | [], _ -> 
+    | [], _ ->
 	{ e_desc = Evar(var);
 	  e_level_ck = ck;
 	  e_ct_annot = Some(Ck(ck));
@@ -667,14 +667,14 @@ let var_dec_list (acc_vd,acc_loc,acc_eq) var_from n =
 
   (* From v, build of v1...vn *)
   let rec varl acc_vd k =
-    if k>n 
+    if k>n
     then acc_vd
     else
       begin
 	let var_prefix = prefix ^ "_" ^ (string_of_int k) in
 	let var = fresh var_prefix in
 	(* addition of var_k *)
-	let acc_vd = { var_from with 
+	let acc_vd = { var_from with
 			 v_ident = var;
 			 v_type = ty_bool } :: acc_vd in
 	varl acc_vd (k+1)
@@ -683,10 +683,10 @@ let var_dec_list (acc_vd,acc_loc,acc_eq) var_from n =
   let vd_list = varl [] 1 in
   (* v_list = [vn;...;v1] *)
   let acc_vd = List.rev_append vd_list acc_vd in
-  
+
   let v_list = List.rev_map (fun vd -> vd.v_ident) vd_list in
 
-  (* From v1...vn, build clocked tree 
+  (* From v1...vn, build clocked tree
      ( vi_(0|1)* on ... on (True|False) (v1) ) *)
   let rec clocked_tree (acc_loc,acc_eq) acc_var suffix v_list ck =
     begin match v_list, acc_var with
@@ -698,10 +698,10 @@ let var_dec_list (acc_vd,acc_loc,acc_eq) var_from n =
 	(* Build left son (ck on False(vi_...)) *)
 	let ck_0 = Con(ck,cfalse,v1) in
 	let acc_loc,acc_eq,t0 =
-	  clocked_tree 
+	  clocked_tree
 	    (acc_loc,acc_eq)
 	    ([v1])
-	    ("_0") 
+	    ("_0")
 	    v_list ck_0 in
 	(* Build right son (ck on True(vi_...))*)
 	let ck_1 = Con(ck,ctrue,v1) in
@@ -709,7 +709,7 @@ let var_dec_list (acc_vd,acc_loc,acc_eq) var_from n =
 	  clocked_tree
 	    (acc_loc,acc_eq)
 	    ([v1])
-	    ("_1") 
+	    ("_1")
 	    v_list ck_1 in
 	acc_loc,acc_eq,VNode(v1,t0,t1)
     | vi::v_list, _ ->
@@ -730,10 +730,10 @@ let var_dec_list (acc_vd,acc_loc,acc_eq) var_from n =
 	(* Build left son (ck on False(vi_...)) *)
 	let ck_0 = Con(ck,cfalse,id) in
 	let acc_loc,acc_eq,t0 =
-	  clocked_tree 
+	  clocked_tree
 	    (acc_loc,acc_eq)
 	    (id::acc_var)
-	    (suffix ^ "_0") 
+	    (suffix ^ "_0")
 	    v_list ck_0 in
 	(* Build right son (ck on True(vi_...))*)
 	let ck_1 = Con(ck,ctrue,id) in
@@ -741,12 +741,12 @@ let var_dec_list (acc_vd,acc_loc,acc_eq) var_from n =
 	  clocked_tree
 	    (acc_loc,acc_eq)
 	    (id::acc_var)
-	    (suffix ^ "_1") 
+	    (suffix ^ "_1")
 	    v_list ck_1 in
 	acc_loc,acc_eq,VNode(id,t0,t1)
-    end 
+    end
   in
-  
+
   let acc_loc,acc_eq,t =
     clocked_tree (acc_loc,acc_eq) [] "" v_list var_from.v_clock in
 
@@ -768,8 +768,8 @@ let buildenv_var_dec (acc_vd,acc_loc,acc_eq,env) ({v_type = ty} as v) =
 		  match (get_enum tname) with
 		  | Type _ -> v::acc_vd, acc_loc, acc_eq ,env
 		  | Enum(info) ->
-		      let (acc_vd,acc_loc,acc_eq,vl,t) = 
-			var_dec_list 
+		      let (acc_vd,acc_loc,acc_eq,vl,t) =
+			var_dec_list
 			  (acc_vd,acc_loc,acc_eq)
 			  v info.ty_nb_var in
 		      let vi = { var_enum = info;
@@ -806,12 +806,12 @@ let rec translate_block env add_locals add_eqs ({ b_local = v;
   let eq_list = eq_list@v_eq@add_eqs in
   let context = translate_eqs env eq_list in
   let d_list,eq_list = context in
-  { b with 
+  { b with
       b_local = v@d_list;
       b_equs = eq_list }, env
 
 and translate_eq env context ({eq_desc = desc} as eq) =
-  let desc,(d_list,eq_list) = 
+  let desc,(d_list,eq_list) =
     match desc with
     | Eblock block ->
 	let block, _ = translate_block env [] [] block in
@@ -829,7 +829,7 @@ and translate_eq env context ({eq_desc = desc} as eq) =
 and translate_eqs env eq_list =
   List.fold_left
     (fun context eq ->
-       translate_eq env context eq) ([],[]) eq_list 
+       translate_eq env context eq) ([],[]) eq_list
 
 let translate_contract env contract =
   match contract with
@@ -846,7 +846,7 @@ let translate_contract env contract =
       let context, e_a = translate env' (v,eqs) e_a in
       let context, e_g = translate env' context e_g in
       let (d_list,eq_list) = context in
-      Some { c_block = { b with 
+      Some { c_block = { b with
 			   b_local = d_list;
 			   b_equs = eq_list };
 	     c_assume = e_a;
@@ -864,7 +864,7 @@ let node ({ n_input = inputs;
   let add_locals = in_loc@out_loc in
   let add_eqs = in_eq@out_eq in
   let b,_ = translate_block env add_locals add_eqs b in
-  { n with 
+  { n with
       n_input = List.rev inputs;
       n_output = List.rev outputs;
       n_contract = contract;
@@ -874,12 +874,12 @@ let program_desc p_desc =
   match p_desc with
   | Pnode(n) -> Pnode(node n)
   | _ -> p_desc
-      
+
 let build p_desc =
   match p_desc with
   | Ptype(type_dec) ->
       begin
-	let tenv = 
+	let tenv =
 	  match type_dec.t_desc with
 	  | Type_enum clist ->
 	      let (n,env,t) = var_list clist in
diff --git a/compiler/heptagon/transformations/completion.ml b/compiler/heptagon/transformations/completion.ml
index 7f76ad1..734c99f 100644
--- a/compiler/heptagon/transformations/completion.ml
+++ b/compiler/heptagon/transformations/completion.ml
@@ -47,9 +47,9 @@ let funs_collect =
 (* adds an equation [x = last(x)] for every partially defined variable *)
 (* in a control structure *)
 let complete_with_last defined_names local_defined_names eq_list =
-  let last n ty = mk_exp (Elast n) ty in
-  let equation n ty eq_list =
-    (mk_equation (Eeq(Evarpat n, last n ty)))::eq_list in
+  let last n vd = mk_exp (Elast n) vd.v_type Linearity.Ltop in
+  let equation n vd eq_list =
+    (mk_equation (Eeq(Evarpat n, last n vd)))::eq_list in
   let d = Env.diff defined_names local_defined_names in
   Env.fold equation d eq_list
 
diff --git a/compiler/heptagon/transformations/inline.ml b/compiler/heptagon/transformations/inline.ml
index 487b551..daf9c06 100644
--- a/compiler/heptagon/transformations/inline.ml
+++ b/compiler/heptagon/transformations/inline.ml
@@ -82,7 +82,7 @@ let exp funs (env, newvars, newequs) exp = match exp.e_desc with
         fst (Hept_mapfold.node_dec funs () ni) in
 
       let mk_input_equ vd e = mk_equation (Eeq (Evarpat vd.v_ident, e)) in
-      let mk_output_exp vd = mk_exp (Evar vd.v_ident) vd.v_type in
+      let mk_output_exp vd = mk_exp (Evar vd.v_ident) vd.v_type ~linearity:vd.v_linearity in
 
       let newvars = ni.n_input @ ni.n_block.b_local @ ni.n_output @ newvars
       and newequs =
@@ -95,7 +95,8 @@ let exp funs (env, newvars, newequs) exp = match exp.e_desc with
         | [o] -> mk_output_exp o
         | _ ->
             mk_exp (Eapp ({ op with a_op = Etuple; },
-                          List.map mk_output_exp ni.n_output, None)) exp.e_ty in
+                          List.map mk_output_exp ni.n_output, None)) exp.e_ty
+                   ~linearity:exp.e_linearity in
       (res_e, (env, newvars, newequs))
   | _ -> Hept_mapfold.exp funs (env, newvars, newequs) exp
 
diff --git a/compiler/heptagon/transformations/itfusion.ml b/compiler/heptagon/transformations/itfusion.ml
index b0fd598..151b038 100644
--- a/compiler/heptagon/transformations/itfusion.ml
+++ b/compiler/heptagon/transformations/itfusion.ml
@@ -51,13 +51,23 @@ match l with
   | [vd] -> Evarpat (vd.v_ident)
   | _ -> Etuplepat (List.map (fun vd -> Evarpat vd.v_ident) l)
 
+let type_of_vd_list l =
+  Types.prod (List.map (fun vd -> vd.v_type) l)
+
+let linearity_of_vd_list l =
+  Linearity.prod (List.map (fun vd -> vd.v_linearity) l)
+
+let exp_of_vd vd =
+  mk_exp (Evar vd.v_ident) vd.v_type ~linearity:vd.v_linearity
+
 let tuple_of_vd_list l =
-  let el = List.map (fun vd -> mk_exp (Evar vd.v_ident) vd.v_type) l in
-  let ty = Types.prod (List.map (fun vd -> vd.v_type) l) in
-    mk_exp (Eapp (mk_app Etuple, el, None)) ty
+  let el = List.map exp_of_vd l in
+  let ty = type_of_vd_list l in
+  let lin = linearity_of_vd_list l in
+    mk_exp (Eapp (mk_app Etuple, el, None)) ty ~linearity:lin
 
 let vd_of_arg ad =
-    mk_var_dec (fresh_vd_of_arg ad) ad.a_type
+    mk_var_dec (fresh_vd_of_arg ad) ad.a_type ad.a_linearity
 
 (** @return the lists of inputs and outputs (as var_dec) of
     an app object. *)
@@ -80,10 +90,10 @@ let get_node_inp_outp app = match app.a_op with
     added equations. *)
 let mk_call app acc_eq_list =
   let new_inp, new_outp = get_node_inp_outp app in
-  let args = List.map (fun vd -> mk_exp
-                         (Evar vd.v_ident) vd.v_type) new_inp in
-  let out_ty = Types.prod (List.map (fun vd -> vd.v_type) new_outp) in
-  let e = mk_exp (Eapp (app, args, None)) out_ty in
+  let args = List.map exp_of_vd new_inp in
+  let out_ty = type_of_vd_list new_outp in
+  let out_lin = linearity_of_vd_list new_outp in
+  let e = mk_exp (Eapp (app, args, None)) out_ty ~linearity:out_lin in
   match List.length new_outp with
     | 1 -> new_inp, e, acc_eq_list
     | _ ->
@@ -112,9 +122,8 @@ let edesc funs acc ed =
               let new_inp, e, acc_eq_list = mk_call g acc_eq_list in
               new_inp @ inp, acc_eq_list, e::largs, local_args @ args, true
           | _ ->
-              let vd = mk_var_dec (fresh_var ()) e.e_ty in
-              let x = mk_exp (Evar vd.v_ident) vd.v_type in
-              vd::inp, acc_eq_list, x::largs, e::args, b
+              let vd = mk_var_dec (fresh_var ()) e.e_ty e.e_linearity in
+              vd::inp, acc_eq_list, (exp_of_vd vd)::largs, e::args, b
         in
 
         let inp, acc_eq_list, largs, args, can_be_fused =
@@ -123,8 +132,9 @@ let edesc funs acc ed =
         then (
           (* create the call to f in the lambda fun *)
           let _, outp = get_node_inp_outp f in
-          let f_out_type = Types.prod (List.map (fun v -> v.v_type) outp) in
-          let call = mk_exp (Eapp(f, largs, None)) f_out_type in
+          let f_out_type = type_of_vd_list outp in
+          let f_out_lin = linearity_of_vd_list outp in
+          let call = mk_exp (Eapp(f, largs, None)) f_out_type f_out_lin in
           let eq = mk_equation (Eeq(pat_of_vd_list outp, call)) in
           (* create the lambda *)
           let anon = mk_app
diff --git a/compiler/heptagon/transformations/last.ml b/compiler/heptagon/transformations/last.ml
index 15e6bd1..0906325 100644
--- a/compiler/heptagon/transformations/last.ml
+++ b/compiler/heptagon/transformations/last.ml
@@ -18,16 +18,18 @@ let fresh = Idents.gen_fresh "last" Idents.name
 
 (* introduce a fresh equation [last_x = pre(x)] for every *)
 (* variable declared with a last *)
-let last (eq_list, env, v) { v_ident = n; v_type = t; v_last = last } =
+let last (eq_list, env, v) { v_ident = n; v_type = t; v_linearity = lin; v_last = last } =
   match last with
     | Var -> (eq_list, env, v)
     | Last(default) ->
         let lastn = fresh n in
-        let eq = mk_equation (Eeq (Evarpat lastn,
-                                   mk_exp (Epre (default, mk_exp (Evar n) t)) t)) in
+        let eq =
+          mk_equation (Eeq (Evarpat lastn,
+                            mk_exp (Epre (default,
+                                          mk_exp (Evar n) t Linearity.Ltop)) t lin)) in
         eq:: eq_list,
         Env.add n lastn env,
-        (mk_var_dec lastn t) :: v
+        (mk_var_dec lastn t lin) :: v
 
 let extend_env env v = List.fold_left last ([], env, []) v
 
diff --git a/compiler/heptagon/transformations/normalize.ml b/compiler/heptagon/transformations/normalize.ml
index 0b5ed51..913fe6c 100644
--- a/compiler/heptagon/transformations/normalize.ml
+++ b/compiler/heptagon/transformations/normalize.ml
@@ -15,6 +15,7 @@ open Hept_utils
 open Hept_mapfold
 open Types
 open Clocks
+open Linearity
 open Format
 
 (** Normalization pass
@@ -36,7 +37,7 @@ end
 
 let exp_list_of_static_exp_list se_list =
   let mk_one_const se =
-    mk_exp (Econst se) se.se_ty
+    mk_exp (Econst se) se.se_ty ~linearity:Ltop
   in
     List.map mk_one_const se_list
 
@@ -61,23 +62,29 @@ let flatten_e_list l =
 (** Creates a new equation x = e, adds x to d_list
     and the equation to eq_list. *)
 let equation (d_list, eq_list) e =
-  let add_one_var ty d_list =
+  let add_one_var ty lin d_list =
     let n = Idents.gen_var "normalize" "v" in
-    let d_list = (mk_var_dec n ty) :: d_list in
+    let d_list = (mk_var_dec n ty lin) :: d_list in
       n, d_list
   in
     match e.e_ty with
       | Tprod ty_list ->
+          let lin_list =
+            (match e.e_linearity with
+              | Ltuple l -> l
+              | Ltop -> Misc.repeat_list Ltop (List.length ty_list)
+              | _ -> assert false)
+          in
           let var_list, d_list =
-            mapfold (fun d_list ty -> add_one_var ty d_list) d_list ty_list in
+            mapfold2 (fun d_list ty lin -> add_one_var ty lin d_list) d_list ty_list lin_list in
           let pat_list = List.map (fun n -> Evarpat n) var_list in
           let eq_list = (mk_equation (Eeq (Etuplepat pat_list, e))) :: eq_list in
-          let e_list = List.map2
-            (fun n ty -> mk_exp (Evar n) ty) var_list ty_list in
+          let e_list = Misc.map3
+            (fun n ty lin -> mk_exp (Evar n) ty lin) var_list ty_list lin_list in
           let e = Eapp(mk_app Etuple, e_list, None) in
             (d_list, eq_list), e
       | _ ->
-          let n, d_list = add_one_var e.e_ty d_list in
+          let n, d_list = add_one_var e.e_ty e.e_linearity d_list in
           let eq_list = (mk_equation (Eeq (Evarpat n, e))) :: eq_list in
             (d_list, eq_list), Evar n
 
@@ -172,9 +179,9 @@ and translate_list kind context e_list =
 
 and fby kind context e v e1 =
   let mk_fby c e =
-    mk_exp ~loc:e.e_loc (Epre(Some c, e)) e.e_ty in
+    mk_exp ~loc:e.e_loc (Epre(Some c, e)) e.e_ty ~linearity:Ltop in
   let mk_pre e =
-    mk_exp ~loc:e.e_loc (Epre(None, e)) e.e_ty in
+    mk_exp ~loc:e.e_loc (Epre(None, e)) e.e_ty ~linearity:Ltop in
   let context, e1 = translate ExtValue context e1 in
   match e1.e_desc, v with
     | Eapp({ a_op = Etuple } as app, e_list, r),
@@ -207,7 +214,7 @@ and ifthenelse context e e1 e2 e3 =
   let mk_ite_list e2_list e3_list =
     let mk_ite e'2 e'3 =
       mk_exp ~loc:e.e_loc
-        (Eapp (mk_app Eifthenelse, [e1; e'2; e'3], None)) e'2.e_ty
+        (Eapp (mk_app Eifthenelse, [e1; e'2; e'3], None)) e'2.e_ty ~linearity:e'2.e_linearity
     in
     let e_list = List.map2 mk_ite e2_list e3_list in
       { e with e_desc = Eapp(mk_app Etuple, e_list, None) }
@@ -228,6 +235,7 @@ and merge context e x c_e_list =
     in
     let rec mk_merge x c_list e_lists =
       let ty = (List.hd (List.hd e_lists)).e_ty in
+      let lin = (List.hd (List.hd e_lists)).e_linearity in
       let rec build_c_e_list c_list e_lists =
 	match c_list, e_lists with
 	| [], [] -> [], []
@@ -241,7 +249,7 @@ and merge context e x c_e_list =
 	| []::_ -> []
 	| _ ::_ ->
 	    let c_e_list, e_lists = build_c_e_list c_list e_lists in
-	    let e_merge = mk_exp ~loc:e.e_loc (Emerge(x, c_e_list)) ty in
+	    let e_merge = mk_exp ~loc:e.e_loc (Emerge(x, c_e_list)) ty ~linearity:lin in
 	    let e_merge_list = build_merge_list c_list e_lists in
 	    e_merge::e_merge_list in
       build_merge_list c_list e_lists
@@ -254,8 +262,8 @@ and merge context e x c_e_list =
               let c_list = List.map (fun (t,_) -> t) c_e_list in
               let e_lists = List.map (fun (_,e) -> e_to_e_list e) c_e_list in
               let e_lists, context =
-                mapfold 
-		  (fun context e_list -> add_list context ExtValue e_list) 
+                mapfold
+		  (fun context e_list -> add_list context ExtValue e_list)
 		  context e_lists in
               let e_list = mk_merge x c_list e_lists in
                 context, { e with
@@ -314,7 +322,7 @@ let block funs _ b =
 
 let contract funs context c =
   let ({ c_block = b } as c), void_context =
-    Hept_mapfold.contract funs context c in 
+    Hept_mapfold.contract funs context c in
   (* Non-void context could mean lost equations *)
   assert (void_context=([],[]));
   let context, e_a = translate ExtValue ([],[]) c.c_assume in
diff --git a/compiler/heptagon/transformations/reset.ml b/compiler/heptagon/transformations/reset.ml
index b5a347d..8262ad6 100644
--- a/compiler/heptagon/transformations/reset.ml
+++ b/compiler/heptagon/transformations/reset.ml
@@ -27,7 +27,9 @@ let fresh = Idents.gen_fresh "reset" ~reset:true (fun () -> "r")
 (* get e and return r, var_dec_r, r = e *)
 let reset_var_from_exp e =
   let r = fresh() in
-  { e with e_desc = Evar r }, mk_var_dec r (Tid Initial.pbool), mk_equation (Eeq(Evarpat r, e))
+  { e with e_desc = Evar r },
+  mk_var_dec r (Tid Initial.pbool) ~linearity:Linearity.Ltop,
+  mk_equation (Eeq(Evarpat r, e))
 
 (** Merge two reset conditions *)
 let merge_resets res1 res2 =
@@ -40,7 +42,10 @@ let merge_resets res1 res2 =
 
 (** if res then e2 else e3 *)
 let ifres res e2 e3 =
-  let init loc = mk_exp (Epre (Some (mk_static_bool true), dfalse)) ~loc:loc (Tid Initial.pbool) in
+  let init loc =
+    mk_exp (Epre (Some (mk_static_bool true), dfalse))
+      ~loc:loc (Tid Initial.pbool) ~linearity:Linearity.Ltop
+  in
   match res with
     | None -> mk_op_app Eifthenelse [init e3.e_loc; e2; e3]
     | Some re -> mk_op_app Eifthenelse [re; e2; e3]
diff --git a/compiler/heptagon/transformations/switch.ml b/compiler/heptagon/transformations/switch.ml
index 708e4ab..e13a9cd 100644
--- a/compiler/heptagon/transformations/switch.ml
+++ b/compiler/heptagon/transformations/switch.ml
@@ -132,7 +132,7 @@ let level_up defnames constr h =
 let add_to_locals vd_env locals h =
   let add_one n nn (locals,vd_env) =
     let orig_vd = Idents.Env.find n vd_env in
-    let vd_nn = mk_var_dec ~linearity:orig_vd.v_linearity nn orig_vd.v_type in
+    let vd_nn = mk_var_dec nn orig_vd.v_type orig_vd.v_linearity in
     vd_nn::locals, Idents.Env.add vd_nn.v_ident vd_nn vd_env
   in
     fold add_one h (locals, vd_env)
@@ -177,7 +177,7 @@ let eqdesc funs (vd_env,env,h) eqd = match eqd with
       (* create a clock var corresponding to the switch condition [e] *)
       let ck = fresh_clock_id () in
       let e, (vd_env,env,h) = exp_it funs (vd_env,env,h) e in
-      let locals = [mk_var_dec ck e.e_ty] in
+      let locals = [mk_var_dec ck e.e_ty e.e_linearity] in
       let equs = [mk_equation (Eeq (Evarpat ck, e))] in
 
       (* typing have proved that defined variables are the same among states *)
@@ -203,14 +203,16 @@ let eqdesc funs (vd_env,env,h) eqd = match eqd with
       in
 
       (* create a merge equation for each defnames *)
-      let new_merge n ty equs =
-        let c_h_to_c_e (constr,h) = constr, mk_exp (Evar(Rename.rename n h)) ty in
+      let new_merge n vd equs =
+        let c_h_to_c_e (constr,h) =
+          constr, mk_exp (Evar(Rename.rename n h)) vd.v_type ~linearity:vd.v_linearity
+        in
         let c_e_l = List.map c_h_to_c_e c_h_l in
-        let merge = mk_exp (Emerge (ck, c_e_l)) ty in
+        let merge = mk_exp (Emerge (ck, c_e_l)) vd.v_type ~linearity:vd.v_linearity in
         (mk_equation (Eeq (Evarpat (Rename.rename n h), merge))) :: equs
       in
       let equs =
-        Idents.Env.fold (fun n ty equs -> new_merge n ty equs) defnames equs
+        Idents.Env.fold (fun n vd equs -> new_merge n vd equs) defnames equs
       in
 
         (* return the transformation in a block *)
diff --git a/compiler/main/hept2mls.ml b/compiler/main/hept2mls.ml
index b291b25..10475ba 100644
--- a/compiler/main/hept2mls.ml
+++ b/compiler/main/hept2mls.ml
@@ -45,19 +45,12 @@ struct
 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
-  n,
-  (mk_var_dec n e.e_ty) :: locals,
-  (mk_equation (Evarpat n) e):: eqs
+  (function Heptagon.Enode f -> (shortname f)
+    | _ -> "n")
 
 let translate_var { Heptagon.v_ident = n; Heptagon.v_type = ty; Heptagon.v_linearity = linearity;
                     Heptagon.v_loc = loc; Heptagon.v_clock = ck } =
-  mk_var_dec ~loc:loc ~linearity:linearity n ty ck
+  mk_var_dec ~loc:loc n ty linearity ck
 
 let translate_reset = function
   | Some { Heptagon.e_desc = Heptagon.Evar n } -> Some n
diff --git a/compiler/minils/analysis/clocking.ml b/compiler/minils/analysis/clocking.ml
index a159a43..916a0e7 100644
--- a/compiler/minils/analysis/clocking.ml
+++ b/compiler/minils/analysis/clocking.ml
@@ -154,7 +154,7 @@ let typing_eq h { eq_lhs = pat; eq_rhs = e; eq_loc = loc } =
                 typing_app h base_ck pat op (pargs@args)
             | Imapi -> (* clocking the node with the extra i input on [ck_r] *)
                 let il (* stubs i as 0 *) =
-                  List.map (fun x -> mk_extvalue ~ty:Initial.tint
+                  List.map (fun x -> mk_extvalue ~ty:Initial.tint ~linearity:Linearity.Ltop
                     ~clock:base_ck (Wconst (Initial.mk_static_int 0))) nl
                 in
                 typing_app h base_ck pat op (pargs@args@il)
@@ -165,7 +165,7 @@ let typing_eq h { eq_lhs = pat; eq_rhs = e; eq_loc = loc } =
                 ct
             | Ifoldi -> (* clocking the node with the extra i and last in/out constraints *)
                 let il (* stubs i as 0 *) =
-                  List.map (fun x -> mk_extvalue ~ty:Initial.tint
+                  List.map (fun x -> mk_extvalue ~ty:Initial.tint ~linearity:Linearity.Ltop
                     ~clock:base_ck (Wconst (Initial.mk_static_int 0))) nl
                 in
                 let rec insert_i args = match args with
diff --git a/compiler/minils/analysis/interference.ml b/compiler/minils/analysis/interference.ml
index 51a351a..093e4bb 100644
--- a/compiler/minils/analysis/interference.ml
+++ b/compiler/minils/analysis/interference.ml
@@ -471,10 +471,10 @@ let process_eq ({ eq_lhs = pat; eq_rhs = e } as eq) =
 let add_init_return_eq f =
    (** a_1,..,a_p = __init__  *)
   let eq_init = mk_equation (Mls_utils.pat_from_dec_list f.n_input)
-    (mk_extvalue_exp Cbase Initial.tint (Wconst (Initial.mk_static_int 0))) in
+    (mk_extvalue_exp Cbase Initial.tint Ltop (Wconst (Initial.mk_static_int 0))) in
     (** __return__ = o_1,..,o_q *)
   let eq_return = mk_equation (Etuplepat [])
-    (mk_exp Cbase Tinvalid (Mls_utils.tuple_from_dec_list f.n_output)) in
+    (mk_exp Cbase Tinvalid Ltop (Mls_utils.tuple_from_dec_list f.n_output)) in
     (eq_init::f.n_equs)@[eq_return]
 
 
diff --git a/compiler/minils/minils.ml b/compiler/minils/minils.ml
index 3d3641d..5af07e8 100644
--- a/compiler/minils/minils.ml
+++ b/compiler/minils/minils.ml
@@ -178,21 +178,21 @@ and interface_desc =
 
 (*Helper functions to build the AST*)
 
-let mk_extvalue ~ty ?(linearity = Ltop) ?(clock = fresh_clock()) ?(loc = no_location) desc =
+let mk_extvalue ~ty ~linearity ?(clock = fresh_clock()) ?(loc = no_location) desc =
   { w_desc = desc; w_ty = ty; w_linearity = linearity;
     w_ck = clock; w_loc = loc }
 
-let mk_exp level_ck ty ?(linearity = Ltop) ?(ck = Cbase)
+let mk_exp level_ck ty ~linearity ?(ck = Cbase)
     ?(ct = fresh_ct ty) ?(loc = no_location) desc =
   { e_desc = desc; e_ty = ty; e_linearity = linearity;
     e_level_ck = level_ck; e_base_ck = ck; e_ct = ct; e_loc = loc }
 
-let mk_var_dec ?(loc = no_location) ?(linearity = Ltop) ident ty ck =
+let mk_var_dec ?(loc = no_location) ident ty linearity ck =
   { v_ident = ident; v_type = ty; v_linearity = linearity;  v_clock = ck; v_loc = loc }
 
-let mk_extvalue_exp ?(linearity = Ltop) ?(clock = fresh_clock())
-    ?(loc = no_location) level_ck ty desc =
-  mk_exp ~ck:clock ~loc:loc level_ck ty
+let mk_extvalue_exp ?(clock = fresh_clock())
+    ?(loc = no_location) level_ck ty ~linearity desc =
+  mk_exp ~ck:clock ~loc:loc level_ck ty ~linearity:linearity
     (Eextvalue (mk_extvalue ~clock:clock ~loc:loc ~linearity:linearity ~ty:ty desc))
 
 let mk_equation ?(loc = no_location) pat exp =
diff --git a/compiler/minils/mls_utils.ml b/compiler/minils/mls_utils.ml
index 9d386cc..54ffdfb 100644
--- a/compiler/minils/mls_utils.ml
+++ b/compiler/minils/mls_utils.ml
@@ -63,7 +63,7 @@ let pat_from_dec_list decs =
 
 let tuple_from_dec_list decs =
   let aux vd =
-    mk_extvalue ~clock:vd.v_clock ~ty:vd.v_type (Wvar vd.v_ident)
+    mk_extvalue ~clock:vd.v_clock ~ty:vd.v_type ~linearity:vd.v_linearity (Wvar vd.v_ident)
   in
     Eapp(mk_app Earray, List.map aux decs, None)
 
diff --git a/compiler/minils/transformations/normalize_mem.ml b/compiler/minils/transformations/normalize_mem.ml
index 52bc6a8..1437412 100644
--- a/compiler/minils/transformations/normalize_mem.ml
+++ b/compiler/minils/transformations/normalize_mem.ml
@@ -22,9 +22,13 @@ let eq _ (outputs, eqs, env) eq = match eq.eq_lhs, eq.eq_rhs.e_desc with
   | Evarpat x, Efby _ ->
       if Mls_utils.vd_mem x outputs then
         let ty = eq.eq_rhs.e_ty in
+        let lin = eq.eq_rhs.e_linearity in
         let ck = eq.eq_rhs.e_base_ck in
         let x_copy = Idents.gen_var "normalize_mem" ("out_"^(Idents.name x)) in
-        let exp_x = mk_exp ck ~ck:ck ~ct:(Clocks.Ck ck) ty (Eextvalue (mk_extvalue ~clock:ck ~ty:ty (Wvar x))) in
+        let exp_x =
+          mk_exp ck ~ck:ck ~ct:(Clocks.Ck ck) ty ~linearity:lin
+            (Eextvalue (mk_extvalue ~clock:ck ~ty:ty ~linearity:lin (Wvar x)))
+        in
         let eq_copy = { eq with eq_lhs = Evarpat x_copy; eq_rhs = exp_x } in
         let env = Env.add x x_copy env in
           eq, (outputs, eq::eq_copy::eqs, env)
@@ -49,7 +53,7 @@ let node funs acc nd =
   { nd with n_local = v; n_equs = List.rev eqs; n_output = o }, acc
 
 let program p =
-  let funs = { Mls_mapfold.defaults with 
+  let funs = { Mls_mapfold.defaults with
 		 eq = eq; node_dec = node; contract = contract } in
   let p, _ = Mls_mapfold.program_it funs ([], [], Env.empty) p in
     p
diff --git a/compiler/minils/transformations/tomato.ml b/compiler/minils/transformations/tomato.ml
index a8809e1..055630a 100644
--- a/compiler/minils/transformations/tomato.ml
+++ b/compiler/minils/transformations/tomato.ml
@@ -184,8 +184,10 @@ let rec add_equation is_input (tenv : tom_env) eq =
         let class_id_list = match rst with
           | None -> class_id_list
           | Some rst ->
-            class_ref_of_var is_input (mk_extvalue ~ty:Initial.tbool (Wvar rst)) rst
-            :: class_id_list in
+            class_ref_of_var is_input
+              (mk_extvalue ~ty:Initial.tbool ~linearity:Linearity.Ltop (Wvar rst)) rst
+            :: class_id_list
+        in
         Eapp (app, w_list, optional (fun _ -> dummy_var) rst), id, 0, class_id_list
 
       | Efby (seo, w) ->
@@ -195,13 +197,18 @@ let rec add_equation is_input (tenv : tom_env) eq =
       | Ewhen (e', cn, x) ->
         let ed, add_when, when_count, class_id_list = decompose e' in
         ed, (fun e' -> { e with e_desc = Ewhen (add_when e', cn, x) }), when_count + 1,
-        class_ref_of_var is_input (mk_extvalue ~clock:e'.e_base_ck ~ty:Initial.tbool (Wvar x)) x
+        class_ref_of_var is_input
+          (mk_extvalue ~clock:e'.e_base_ck ~ty:Initial.tbool
+                       ~linearity:Linearity.Ltop (Wvar x)) x
         :: class_id_list
 
       | Emerge (x, clause_list) ->
         let class_id_list, clause_list = mapfold_right add_clause clause_list [] in
         let x_id =
-          class_ref_of_var is_input (mk_extvalue ~clock:e.e_base_ck ~ty:Initial.tbool (Wvar x)) x in
+          class_ref_of_var is_input
+            (mk_extvalue ~clock:e.e_base_ck ~ty:Initial.tbool
+                         ~linearity:Linearity.Ltop (Wvar x)) x
+        in
         Emerge (dummy_var, clause_list), id, 0, x_id :: class_id_list
 
       | Eiterator (it, app, sel, partial_w_list, w_list, rst) ->
@@ -210,8 +217,10 @@ let rec add_equation is_input (tenv : tom_env) eq =
         let class_id_list = match rst with
           | None -> class_id_list
           | Some rst ->
-            class_ref_of_var is_input (mk_extvalue ~ty:Initial.tbool (Wvar rst)) rst
-            :: class_id_list in
+            class_ref_of_var is_input
+              (mk_extvalue ~ty:Initial.tbool ~linearity:Linearity.Ltop (Wvar rst)) rst
+            :: class_id_list
+        in
         Eiterator (it, app, sel, partial_w_list, w_list, optional (fun _ -> dummy_var) rst),
         id, 0, class_id_list
 
@@ -246,7 +255,7 @@ and extvalue is_input w class_id_list =
         class_id_list, Wfield (w, f)
       | Wwhen (w, cn, x) ->
         (* Create the extvalue representing x *)
-        let w_x = mk_extvalue ~ty:Initial.tbool ~clock:w.w_ck (Wvar x) in
+        let w_x = mk_extvalue ~ty:Initial.tbool ~clock:w.w_ck ~linearity:w.w_linearity (Wvar x) in
         let class_id_list, w = decompose w (class_ref_of_var is_input w_x x :: class_id_list) in
         class_id_list, Wwhen (w, cn, dummy_var)
     in
@@ -419,7 +428,7 @@ and reconstruct_class_ref mapping cr = match cr with
   | Cr_input w -> w
   | Cr_plain x ->
     let Info (x', ty, ck, _) = Env.find x mapping in
-    mk_extvalue ~clock:ck ~ty:ty (Wvar x')
+    mk_extvalue ~clock:ck ~ty:ty ~linearity:Linearity.Ltop (Wvar x')
 
 and reconstruct_clock mapping ck = match ck_repr ck with
   | Con (ck, c, x) -> Con (reconstruct_clock mapping ck, c, new_name mapping x)
@@ -537,10 +546,11 @@ let rec fix_output_var_dec mapping vd (seen, equs, vd_list) =
     let new_clock = reconstruct_clock mapping vd.v_clock in
     let new_vd = { vd with v_ident = new_id; v_clock = new_clock } in
     let new_eq =
-      let w = mk_extvalue ~ty:vd.v_type ~clock:new_clock (Wvar x) in
+      let w = mk_extvalue ~ty:vd.v_type ~clock:new_clock ~linearity:Linearity.Ltop (Wvar x) in
       mk_equation
         (Evarpat new_id)
-        (mk_exp new_clock vd.v_type ~ct:(Ck new_clock) ~ck:new_clock (Eextvalue w))
+        (mk_exp new_clock vd.v_type ~ct:(Ck new_clock)
+           ~ck:new_clock ~linearity:Linearity.Ltop (Eextvalue w))
     in
     (seen, new_eq :: equs, new_vd :: vd_list)
   else
diff --git a/test/good/linear_automata.ept b/test/good/linear_automata.ept
index 86bc2ff..b9f2960 100644
--- a/test/good/linear_automata.ept
+++ b/test/good/linear_automata.ept
@@ -10,7 +10,7 @@ let
   o = [ a with [n-1] = 0 ]
 tel
 
-node autom(a:int^n at r) returns (o:int^n at r)
+node autom(a:int^n at r) returns (o:int^n at r; u:int)
 let
   automaton
     state S1
@@ -22,5 +22,24 @@ let
     do
       o = g(a)
     until false then S1
-  end
-tel
\ No newline at end of file
+  end;
+  u = a[0]
+tel
+
+node autom_last() returns (u:int)
+var a:int^n at r; last o : int^n at r;
+let
+  init<<r>> a = 1^n;
+  automaton
+    state S1
+    do
+    until true then S2
+
+    state S2
+    do
+      o = g(a)
+    until false then S1
+  end;
+  u = a[0]
+tel
+