From c86d7af0b155bef7a06f3327aa88938e3816eed6 Mon Sep 17 00:00:00 2001
From: Nicolas Berthier <nicolas.berthier@inria.fr>
Date: Mon, 15 Dec 2014 15:42:37 +0100
Subject: [PATCH] Introducing a hack to normalize comparison of tuples in
 Heptagon.

---
 compiler/heptagon/analysis/hept_clocking.ml    |  4 ++--
 compiler/heptagon/transformations/normalize.ml | 12 ++++++++++++
 compiler/minils/analysis/clocking.ml           |  3 ++-
 3 files changed, 16 insertions(+), 3 deletions(-)

diff --git a/compiler/heptagon/analysis/hept_clocking.ml b/compiler/heptagon/analysis/hept_clocking.ml
index fdd231f..6f7d0cb 100644
--- a/compiler/heptagon/analysis/hept_clocking.ml
+++ b/compiler/heptagon/analysis/hept_clocking.ml
@@ -207,8 +207,8 @@ and typing_app h base pat op e_list = match op with
           | None -> build_env a_l v_l env
           | Some n -> build_env a_l v_l ((n,v)::env))
         | _ ->
-            Printf.printf "Fun/node : %s\n" (Names.fullname f);
-            Misc.internal_error "Clocking, non matching signature"
+            Misc.internal_error ("Clocking, non matching signature in call of "^
+                                    Names.fullname f);
       in
       let env_pat = build_env node.node_outputs pat_id_list [] in
       let env_args = build_env node.node_inputs e_list [] in
diff --git a/compiler/heptagon/transformations/normalize.ml b/compiler/heptagon/transformations/normalize.ml
index 24ac63d..18f37f4 100644
--- a/compiler/heptagon/transformations/normalize.ml
+++ b/compiler/heptagon/transformations/normalize.ml
@@ -175,6 +175,18 @@ let rec translate kind context e =
         merge context e n tag_e_list
     | Eapp({ a_op = Eifthenelse }, [e1; e2; e3], _) ->
         ifthenelse context e e1 e2 e3
+    (* XXX Huge hack to avoid comparing tuples... (temporary, until this is
+       fixed where it should be) *)
+    | Eapp({ a_op = (Efun ({ Names.qual = Names.Pervasives; Names.name = "=" }) as op)},
+           [x;y], reset) when is_list x ->
+        let x = e_to_e_list x and y = e_to_e_list y in
+        let xy = List.fold_left2 (fun acc x y ->
+          let cmp = mk_exp (mk_op_app op [x; y] ~reset) Initial.tbool ~linearity:Ltop in
+          mk_exp (mk_op_app (Efun Initial.pand) [acc; cmp] ~reset) Initial.tbool ~linearity:Ltop)
+          dtrue
+          x y
+        in
+        translate kind context xy
     | Eapp(app, e_list, r) ->
         let context, e_list = translate_list ExtValue context e_list in
           context, { e with e_desc = Eapp(app, flatten_e_list e_list, r) }
diff --git a/compiler/minils/analysis/clocking.ml b/compiler/minils/analysis/clocking.ml
index 371ee2d..c2bd993 100644
--- a/compiler/minils/analysis/clocking.ml
+++ b/compiler/minils/analysis/clocking.ml
@@ -137,7 +137,8 @@ let typing_app h base pat op w_list = match op with
         | a::a_l, v::v_l -> (match a.a_name with
           | None -> build_env a_l v_l env
           | Some n -> build_env a_l v_l ((n,v)::env))
-        | _ -> Misc.internal_error "Clocking, non matching signature"
+        | _ -> Misc.internal_error ("Clocking, non matching signature in call of " ^
+                                      Names.fullname f)
       in
       let env_pat = build_env node.node_outputs pat_id_list [] in
       let env_args = build_env node.node_inputs w_list [] in