From fd00f099f56bc03240b9c751829191b68df8beb2 Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?L=C3=A9onard=20G=C3=A9rard?= <leonard.gerard@ens.fr>
Date: Mon, 23 May 2011 14:03:45 +0200
Subject: [PATCH] correct reset and level clock

---
 compiler/heptagon/transformations/reset.ml  | 47 +++++++++++++++------
 compiler/heptagon/transformations/switch.ml |  2 +-
 compiler/minils/analysis/level_clock.ml     |  7 +--
 3 files changed, 39 insertions(+), 17 deletions(-)

diff --git a/compiler/heptagon/transformations/reset.ml b/compiler/heptagon/transformations/reset.ml
index c872601..36918f8 100644
--- a/compiler/heptagon/transformations/reset.ml
+++ b/compiler/heptagon/transformations/reset.ml
@@ -45,37 +45,58 @@ let ifres res e2 e3 =
     | None -> mk_op_app Eifthenelse [init e3.e_loc; e2; e3]
     | Some re -> mk_op_app Eifthenelse [re; e2; e3]
 
-(** Keep when ever possible the initialization value *)
+(** Keep whenever possible the initialization value *)
 let default e =
   match e.e_desc with
     | Econst c -> Some c
     | _ -> None
 
 
-let edesc funs (res,stateful) ed =
-  let ed, _ = Hept_mapfold.edesc funs (res,stateful) ed in
-  let ed = match ed with
+let edesc funs ((res,stateful) as acc) ed = match ed with
     | Efby (e1, e2) ->
+        let e1,_ = Hept_mapfold.exp_it funs acc e1 in
+        let e2,_ = Hept_mapfold.exp_it funs acc e2 in
         (match res, e1 with
          | None, { e_desc = Econst c } ->
             (* no reset : [if res] useless, the initialization is sufficient *)
             Epre(Some c, e2)
-         | _ -> ifres res e1 { e2 with e_desc = Epre(default e1, e2) })
+         | _ -> ifres res e1 { e2 with e_desc = Epre(default e1, e2) }), acc
     | Eapp({ a_op = Earrow }, [e1;e2], _) ->
-        ifres res e1 e2
+        let e1,_ = Hept_mapfold.exp_it funs acc e1 in
+        let e2,_ = Hept_mapfold.exp_it funs acc e2 in
+        ifres res e1 e2, acc
     | Eapp({ a_op = Enode _ } as op, e_list, re) ->
-        Eapp(op, e_list, merge_resets res re)
+        let args,_ = mapfold (Hept_mapfold.exp_it funs) acc e_list in
+        let re,_ = optional_wacc (Hept_mapfold.exp_it funs) acc re in
+        Eapp(op, e_list, merge_resets res re), acc
     | Eiterator(it, ({ a_op = Enode _ } as op), n, pe_list, e_list, re) ->
-        Eiterator(it, op, n, pe_list, e_list, merge_resets res re)
+        let pargs,_ = mapfold (Hept_mapfold.exp_it funs) acc pe_list in
+        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, merge_resets res re), acc
     | Eapp({ a_op = Efun _ } as op, e_list, re) ->
-        Eapp(op, e_list, None) (* funs don't need resets *)
+        let args,_ = mapfold (Hept_mapfold.exp_it funs) acc e_list in
+        let re,_ = optional_wacc (Hept_mapfold.exp_it funs) acc re in
+        Eapp(op, args, None), acc (* funs don't need resets *)
     | Eiterator(it, ({ a_op = Efun _ } as op), n, pe_list, e_list, re) ->
-        Eiterator(it, op, n, pe_list, e_list, None) (* funs don't need resets *)
-    | _ -> ed
-  in
-    ed, (res,stateful)
+        let pargs,_ = mapfold (Hept_mapfold.exp_it funs) acc pe_list in
+        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 =
   Hept_mapfold.eq funs (res,eq.eq_stateful) eq
 
diff --git a/compiler/heptagon/transformations/switch.ml b/compiler/heptagon/transformations/switch.ml
index ea6eaf5..bcb5f4c 100644
--- a/compiler/heptagon/transformations/switch.ml
+++ b/compiler/heptagon/transformations/switch.ml
@@ -7,7 +7,7 @@
 (*                                                                        *)
 (**************************************************************************)
 
-(* ASSUMES no automaton, no present, no last *)
+(* ASSUMES no automaton, no present, no last, no reset *)
 
 (* Removing switch statements *)
 
diff --git a/compiler/minils/analysis/level_clock.ml b/compiler/minils/analysis/level_clock.ml
index ffcfec4..b7bfe75 100644
--- a/compiler/minils/analysis/level_clock.ml
+++ b/compiler/minils/analysis/level_clock.ml
@@ -19,14 +19,15 @@ open Minils
    The other ones are coming from one like this one,
    indeed if it was Con (Cvar,c,x) x would have to be defined with an expression of clock Cvar.*)
 
-let exp _ acc e =
+let eq _ acc eq =
+  let e = eq.eq_rhs in
   let _ = match ck_repr e.e_base_ck with
     | Cvar {contents = Cindex _} -> unify_ck e.e_base_ck e.e_level_ck
     | _ -> ()
   in
-  e,acc (* no recursion since in minils exps are not recursive *)
+  eq,acc (* no recursion since in minils exps are not recursive *)
 
 let program p =
-  let funs = { Mls_mapfold.defaults with Mls_mapfold.exp = exp } in
+  let funs = { Mls_mapfold.defaults with Mls_mapfold.eq = eq } in
   let p, _ = Mls_mapfold.program_it funs [] p in
   p
\ No newline at end of file