From 4dadf6b4d669b89002e32c28aec511d18a5c9ad8 Mon Sep 17 00:00:00 2001
From: Timothy Bourke <tim@tbrk.org>
Date: Mon, 23 Jan 2017 15:13:28 +0100
Subject: [PATCH] Enforce well-formedness of clocks

For a clock (ck on x) to be well-formed in an environment H, we must
have H x = ck, i.e., the clock of x is the same as the clock ck of the
stream being sampled.

This constraint is guaranteed by construction for fully inferred clocks
(by the rules for when and merge), but nothing guarantees that user
declarations be well-formed. This can lead to problems.

For instance, this invalid program is incorrectly accepted:

    node f (x : bool; a : bool :: . on b;
		      b : bool :: . on a) returns (y:bool);
    let
	y = true;
    tel

as is this one:

    node f(a: bool :: . on a; b: bool :: . on a)
    returns (z: bool);
    var w : bool;
    let
	w = a when b;
	z = false fby w;
    tel

This invalid program is incorrectly accepted and leads to an internal
compiler error:

    node f (x : bool) returns (y:bool);
    var a : bool :: . on b;
	b : bool :: . on a;
    let
	y = true;
	a = true;
	b = true;
    tel

This patch enforces the well-formedness constraint. It gives a sensible
error message when the constraint cannot be satisfied.
---
 compiler/minils/analysis/clocking.ml | 12 ++++++++++++
 1 file changed, 12 insertions(+)

diff --git a/compiler/minils/analysis/clocking.ml b/compiler/minils/analysis/clocking.ml
index da7537b..cfe9570 100644
--- a/compiler/minils/analysis/clocking.ml
+++ b/compiler/minils/analysis/clocking.ml
@@ -276,11 +276,23 @@ let typing_contract h0 h contract =
         let h = append_env h c_list in
         Some { contract with c_eq = eq_list }, h
 
+let rec constrain_on loc h = function
+  | Clocks.Cbase | Clocks.Cvar _ -> ()
+  | Clocks.Con (ck', c, n) ->
+      (try unify_ck (ck_of_name h n) ck'
+       with Unify -> error_message loc (Eclockclash (ck_of_name h n, ck')));
+      constrain_on loc h ck'
+
+let constrain_on_over h xs =
+  List.iter (fun vd -> constrain_on vd.v_loc h (ck_of_name h vd.v_ident)) xs
 
 let typing_node node =
   let h0 = append_env Env.empty node.n_input in
   let h0 = append_env h0 node.n_output in
   let h = append_env h0 node.n_local in
+  constrain_on_over h node.n_input;
+  constrain_on_over h node.n_output;
+  constrain_on_over h node.n_local;
   let contract, h = typing_contract h0 h node.n_contract in
   (*   let h = append_env h node.n_local in *)
   let equs = typing_eqs h node.n_equs in