resets are now without constraint.

compiler/global/idents.ml

@@ -19,8 +19,11 @@ type ident = {
   num : int;        (* a unique index *)
   source : string;  (* the original name in the source *)
   is_generated : bool;
+  is_reset : bool;
 }
 
+let is_reset id = id.is_reset
+
 type var_ident = ident
 
 let num = ref 0
@@ -124,18 +127,19 @@ struct
     Env.find id !env
 end
 
-let gen_fresh pass_name kind_to_string kind =
+let gen_fresh pass_name kind_to_string ?(reset=false) kind =
   let s = kind_to_string kind in
   let s = if !Compiler_options.full_name then "__"^pass_name ^ "_" ^ s else s in
   num := !num + 1;
-  let id = { num = !num; source = s; is_generated = true } in
+  let id = { num = !num; source = s; is_generated = true; is_reset = reset } in
     UniqueNames.assign_name id; id
 
-let gen_var pass_name name = gen_fresh pass_name (fun () -> name) ()
+let gen_var pass_name ?(reset=false) name =
+  gen_fresh pass_name (fun () -> name) ~reset:reset ()
 
-let ident_of_name s =
+let ident_of_name ?(reset=false) s =
   num := !num + 1;
-  let id = { num = !num; source = s; is_generated = false } in
+  let id = { num = !num; source = s; is_generated = false; is_reset = reset } in
     UniqueNames.assign_name id; id
 
 let source_name id = id.source

compiler/global/idents.mli

@@ -24,15 +24,17 @@ val source_name : ident -> string
 (** [gen_fresh pass_name kind_to_string kind]
     generate a fresh ident with a sweet [name].
     It should be used to define a [fresh] function specific to a pass. *)
-val gen_fresh : string -> ('a -> string) -> 'a -> ident
+val gen_fresh : string -> ('a -> string) -> ?reset:bool -> 'a -> ident
 
 (** [gen_var pass_name name]
     generates a fresh ident with a sweet [name] *)
-val gen_var : string -> string -> ident
+val gen_var : string -> ?reset:bool -> string -> ident
 
 (** [ident_of_name n] returns an fresh identifier corresponding
   to a _source_ variable (do not use it for generated variables). *)
-val ident_of_name : string -> ident
+val ident_of_name : ?reset:bool -> string -> ident
+
+val is_reset : ident -> bool
 
 (** /!\ This function should be called every time we enter a node *)
 val enter_node : Names.qualname -> unit

compiler/heptagon/transformations/every.ml

@@ -16,10 +16,10 @@ let edesc funs (v,acc_eq_list) ed =
   let ed, (v, acc_eq_list) = Hept_mapfold.edesc funs (v,acc_eq_list) ed in
   match ed with
     | Eapp (op, e_list, Some re) when not (is_var re) ->
-        let re, vre, eqre = Reset.bool_var_from_exp re in
+        let re, vre, eqre = Reset.reset_var_from_exp re in
         Eapp(op, e_list, Some re), (vre::v, eqre::acc_eq_list)
     | Eiterator(it, op, n, pe_list, e_list, Some re) when not (is_var re) ->
-        let re, vre, eqre = Reset.bool_var_from_exp re in
+        let re, vre, eqre = Reset.reset_var_from_exp re in
           Eiterator(it, op, n, pe_list, e_list, Some re),
              (vre::v, eqre::acc_eq_list)
     | _ -> ed, (v, acc_eq_list)

compiler/heptagon/transformations/reset.ml

@@ -22,10 +22,10 @@ open Initial
 
 
 
-let fresh = Idents.gen_fresh "reset" (fun () -> "r")
+let fresh = Idents.gen_fresh "reset" ~reset:true (fun () -> "r")
 
 (* get e and return r, var_dec_r, r = e *)
-let bool_var_from_exp 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))
 
@@ -83,18 +83,6 @@ let edesc funs ((res,stateful) as acc) ed = match ed with
         let args,_ = mapfold (Hept_mapfold.exp_it funs) acc e_list in
         let re,_ = optional_wacc (Hept_mapfold.exp_it funs) acc re in
         Eiterator(it, op, n, pargs, args, None), acc (* funs don't need resets *)
-    | Emerge(x, c_e_l) ->
-        let aux acc (c,e) =
-          let res = match res with
-            | None -> None
-            | Some r -> Some (mk_exp (Ewhen (r,c,x)) Initial.tbool) in
-          let e,_ = Hept_mapfold.exp_it funs (res,stateful) e in
-          (c,e), acc
-        in
-        let c_e_l, acc = mapfold aux acc c_e_l in
-        Emerge(x, c_e_l), acc
-
-
     | _ -> raise Errors.Fallback
 
 let eq funs (res,_) eq =
@@ -109,7 +97,7 @@ let eqdesc funs (res,stateful) = function
   | Ereset(b, e) ->
       if stateful then (
         let e, _ = Hept_mapfold.exp_it funs (res,stateful) e in
-        let e, vd, eq = bool_var_from_exp e in
+        let e, vd, eq = reset_var_from_exp e in
         let r = merge_resets res (Some e) in
         let b, _ = Hept_mapfold.block_it funs (r,stateful) b in
         let b = { b with b_equs = eq::b.b_equs; b_local = vd::b.b_local; b_stateful = true } in

compiler/minils/analysis/clocking.ml

@@ -52,7 +52,10 @@ let error_message loc = function
       raise Errors.Error
 
 
-let ck_of_name h x = Env.find x h
+let ck_of_name h x =
+  if is_reset x
+  then fresh_clock()
+  else Env.find x h
 
 let rec typing_extvalue h w =
   let ck = match w.w_desc with