From 1a9dc17618b3fda8c7c824263c34a9ac28dbf8a4 Mon Sep 17 00:00:00 2001
From: Adrien Guatto <adrien.guatto@laposte.net>
Date: Thu, 10 Nov 2011 15:36:54 +0100
Subject: [PATCH] Fixed clocking annotations.

1. Transmit annotations to extvaluese in Hept2mls.

2. Handle a pre-existing w_ck when clocking extvalues.
---
 compiler/main/hept2mls.ml            | 4 +++-
 compiler/minils/analysis/clocking.ml | 7 ++++++-
 2 files changed, 9 insertions(+), 2 deletions(-)

diff --git a/compiler/main/hept2mls.ml b/compiler/main/hept2mls.ml
index 2e57fab..1f148a8 100644
--- a/compiler/main/hept2mls.ml
+++ b/compiler/main/hept2mls.ml
@@ -90,7 +90,9 @@ let translate_app app =
 
 let rec translate_extvalue e =
   let mk_extvalue =
-    mk_extvalue ~loc:e.Heptagon.e_loc ~linearity:e.Heptagon.e_linearity ~ty:e.Heptagon.e_ty
+    mk_extvalue
+      ~loc:e.Heptagon.e_loc ~linearity:e.Heptagon.e_linearity ~ty:e.Heptagon.e_ty
+      ~clock:(match e.Heptagon.e_ct_annot with None -> fresh_clock () | Some ct -> assert_1 (unprod ct))
   in
   match e.Heptagon.e_desc with
     | Heptagon.Econst c -> mk_extvalue (Wconst c)
diff --git a/compiler/minils/analysis/clocking.ml b/compiler/minils/analysis/clocking.ml
index 40d76fe..0529843 100644
--- a/compiler/minils/analysis/clocking.ml
+++ b/compiler/minils/analysis/clocking.ml
@@ -73,6 +73,11 @@ let rec typing_extvalue h w =
       unify_ck t1 t2;
       t1
   in
+  (try unify_ck ck w.w_ck
+   with Unify ->
+     eprintf "Incoherent clock annotation for extvalue %a.@\n"
+       Mls_printer.print_extvalue w;
+     error_message w.w_loc (Etypeclash (Ck ck, Ck w.w_ck)));
   w.w_ck <- ck;
   ck
 
@@ -187,7 +192,7 @@ let typing_eq h { eq_lhs = pat; eq_rhs = e; eq_loc = loc } =
     e.e_base_ck <- base;
     (try unify ct e.e_ct
      with Unify ->
-       eprintf "Incoherent clock annotation for exp %a.@\n"
+       eprintf "Inconsistent clock annotation for exp %a.@\n"
        Mls_printer.print_exp e;
        error_message e.e_loc (Etypeclash (ct,e.e_ct)));
     e.e_ct <- ct;