From 9a176485169cc7037d11118019d21510ddcbb659 Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?L=C3=A9onard=20G=C3=A9rard?= <leonard.gerard@ens.fr>
Date: Thu, 12 May 2011 00:54:02 +0200
Subject: [PATCH] good clocks in signatures

---
 compiler/global/clocks.ml                     |  6 +-
 compiler/global/idents.ml                     | 12 +--
 compiler/global/names.ml                      |  2 +-
 compiler/global/signature.ml                  | 70 ++++++++++++++++-
 compiler/heptagon/analysis/typing.ml          | 20 ++---
 compiler/heptagon/hept_utils.ml               | 14 ++++
 compiler/heptagon/parsing/hept_parser.mly     |  2 +-
 compiler/heptagon/parsing/hept_scoping.ml     | 78 ++++++++-----------
 .../heptagon/parsing/hept_static_scoping.ml   |  4 +-
 compiler/heptagon/transformations/inline.ml   | 10 +--
 compiler/heptagon/transformations/switch.ml   |  6 +-
 compiler/minils/analysis/clocking.ml          | 20 +++--
 compiler/minils/mls_utils.ml                  | 15 +++-
 13 files changed, 171 insertions(+), 88 deletions(-)

diff --git a/compiler/global/clocks.ml b/compiler/global/clocks.ml
index 04bbf50..0558f7b 100644
--- a/compiler/global/clocks.ml
+++ b/compiler/global/clocks.ml
@@ -115,11 +115,11 @@ let rec tuple ck = function
 *)
 (*
 let max ck_1 ck_2 = match ck_repr ck_1, ck_reprck_2 with
-  | 
+  |
 
 let rec optim_base_ck base_ck ct = match ct with
-  | Ck ck -> 
-  | Cprod c_l -> 
+  | Ck ck ->
+  | Cprod c_l ->
 *)
 
 
diff --git a/compiler/global/idents.ml b/compiler/global/idents.ml
index c7e3344..eca6811 100644
--- a/compiler/global/idents.ml
+++ b/compiler/global/idents.ml
@@ -93,14 +93,14 @@ module S = Set.Make (struct type t = string
 module UniqueNames =
 struct
   open Names
-  let used_names = ref (ref S.empty) (** Used strings in the current node *)
+  let used_names = ref (ref NamesSet.empty) (** Used strings in the current node *)
   let env = ref Env.empty (** Map idents to their string *)
-  let (node_env : S.t ref QualEnv.t ref) = ref QualEnv.empty
+  let (node_env : NamesSet.t ref QualEnv.t ref) = ref QualEnv.empty
 
   (** This function should be called every time we enter a node *)
   let enter_node n =
     (if not (QualEnv.mem n !node_env)
-    then node_env := QualEnv.add n (ref S.empty) !node_env);
+    then node_env := QualEnv.add n (ref NamesSet.empty) !node_env);
     used_names := QualEnv.find n !node_env
 
   (** @return a unique string for each identifier. Idents corresponding
@@ -113,11 +113,11 @@ struct
       s ^ "_" ^ (string_of_int !num) in
     let rec fresh_string base =
       let fs = fresh base in
-      if S.mem fs !(!used_names) then fresh_string base else fs in
+      if NamesSet.mem fs !(!used_names) then fresh_string base else fs in
     if not (Env.mem n !env) then
       (let s = n.source in
-       let s = if S.mem s !(!used_names) then fresh_string s else s in
-       !used_names := S.add s !(!used_names);
+       let s = if NamesSet.mem s !(!used_names) then fresh_string s else s in
+       !used_names := NamesSet.add s !(!used_names);
        env := Env.add n s !env)
 
   let name id =
diff --git a/compiler/global/names.ml b/compiler/global/names.ml
index 3f64dab..3593a33 100644
--- a/compiler/global/names.ml
+++ b/compiler/global/names.ml
@@ -42,9 +42,9 @@ module QualEnv = struct
   let append env' env = fold (fun key v env -> add key v env) env' env
 end
 
+module NamesSet = Set.Make (struct type t = string let compare = compare end)
 module QualSet = Set.Make (struct type t = qualname let compare = compare end)
 module ModulSet = Set.Make (struct type t = modul let compare = compare end)
-module S = Set.Make (struct type t = string let compare = compare end)
 
 
 let shortname { name = n; } = n
diff --git a/compiler/global/signature.ml b/compiler/global/signature.ml
index 2a57f94..10b3421 100644
--- a/compiler/global/signature.ml
+++ b/compiler/global/signature.ml
@@ -9,6 +9,7 @@
 (* global data in the symbol tables *)
 open Names
 open Types
+open Location
 
 (** Warning: Whenever these types are modified,
     interface_format_version should be incremented. *)
@@ -40,7 +41,8 @@ type node = {
   node_outputs            : arg list;
   node_stateful           : bool;
   node_params             : param list;
-  node_params_constraints : size_constraint list }
+  node_params_constraints : size_constraint list;
+  node_loc                : location}
 
 type field = { f_name : field_name; f_type : ty }
 type structure = field list
@@ -53,6 +55,67 @@ type type_def =
 
 type const_def = { c_type : ty; c_value : static_exp }
 
+
+(** { 3 Signature helper functions } *)
+
+type error =
+  | Eckvar_unbound of name option * name
+  | Eckvar_unbound_input of name option * name
+  | Eckvar_unbound_ouput of name option * name
+
+exception SignatureError of error
+
+let message loc e = begin match e with
+  | Eckvar_unbound_input(var_name,ck_name) ->
+      let a,name = match var_name with None -> "a","" | Some n -> "the"," "^n in
+      Format.eprintf "%aThe variable %s is unbound.@\n
+               Note that %s sampled input%s should come together with its clock.@."
+        print_location loc
+        ck_name a name
+  | Eckvar_unbound_ouput (var_name,ck_name) ->
+      let a,name = match var_name with None -> "a","" | Some n -> "the"," "^n in
+      Format.eprintf "%aThe variable %s is unbound.@\n
+               Note that %s sampled ouput%s should be returned with its clock.@."
+        print_location loc
+        ck_name a name
+  | Eckvar_unbound(var_name,ck_name) ->
+      Format.eprintf "%aThe variable %s is unbound.@." print_location loc ck_name
+  end;
+  raise Errors.Error
+
+
+(** @raise Errors.Error after printing the error *)
+let check_signature s =
+  (* a simple env of defined names will be used, represented by a Set *)
+  let rec append env sa_l = match sa_l with
+    | [] -> env
+    | sa::sa_l -> match sa.a_name with
+        | None -> append env sa_l
+        | Some x -> append (NamesSet.add x env) sa_l
+  in
+  (* the clock of [arg] is correct if all the vars used are in [env] *)
+  let check env arg =
+    let n = arg.a_name in
+    let rec f = function
+      | Cbase -> ()
+      | Con(ck,_,x) ->
+          if not (NamesSet.mem x env)
+          then raise (SignatureError (Eckvar_unbound (n,x)));
+          f ck
+    in
+    f arg.a_clock
+  in
+  (*initial env with only the inputs*)
+  let env = append NamesSet.empty s.node_inputs in
+  (try List.iter (check env) s.node_inputs
+  with SignatureError (Eckvar_unbound (x,c)) ->
+    message s.node_loc (Eckvar_unbound_input (x,c)));
+  let env = append env s.node_outputs in
+  try List.iter (check env) s.node_outputs
+  with SignatureError (Eckvar_unbound (x,c)) ->
+    message s.node_loc (Eckvar_unbound_ouput (x,c))
+
+
 let rec ck_to_sck ck =
   let ck = Clocks.ck_repr ck in
   match ck with
@@ -74,12 +137,13 @@ let mk_field n ty = { f_name = n; f_type = ty }
 let mk_const_def ty value =
   { c_type = ty; c_value = value }
 
-let mk_node ?(constraints = []) ins outs stateful params =
+let mk_node ?(constraints = []) loc ins outs stateful params =
   { node_inputs = ins;
     node_outputs  = outs;
     node_stateful = stateful;
     node_params = params;
-    node_params_constraints = constraints }
+    node_params_constraints = constraints;
+    node_loc = loc}
 
 let rec field_assoc f = function
   | [] -> raise Not_found
diff --git a/compiler/heptagon/analysis/typing.ml b/compiler/heptagon/analysis/typing.ml
index 9e7eb08..4a1d5e8 100644
--- a/compiler/heptagon/analysis/typing.ml
+++ b/compiler/heptagon/analysis/typing.ml
@@ -272,10 +272,10 @@ let add_distinct_qualset n acc =
     QualSet.add n acc
 
 let add_distinct_S n acc =
-  if S.mem n acc then
+  if NamesSet.mem n acc then
     error (Ealready_defined n)
   else
-    S.add n acc
+    NamesSet.add n acc
 
 (** Add two sets of names provided they are distinct *)
 let add env1 env2 =
@@ -337,23 +337,23 @@ let last = function | Var -> false | Last _ -> true
     of field name, exp.*)
 let check_field_unicity l =
   let add_field acc (f,e) =
-    if S.mem (shortname f) acc then
+    if NamesSet.mem (shortname f) acc then
       message e.e_loc (Ealready_defined (fullname f))
     else
-      S.add (shortname f) acc
+      NamesSet.add (shortname f) acc
   in
-  ignore (List.fold_left add_field S.empty l)
+  ignore (List.fold_left add_field NamesSet.empty l)
 
 (** Checks that a field is not defined twice in a list
     of field name, exp.*)
 let check_static_field_unicity l =
   let add_field acc (f,se) =
-    if S.mem (shortname f) acc then
+    if NamesSet.mem (shortname f) acc then
       message se.se_loc (Ealready_defined (fullname f))
     else
-      S.add (shortname f) acc
+      NamesSet.add (shortname f) acc
   in
-  ignore (List.fold_left add_field S.empty l)
+  ignore (List.fold_left add_field NamesSet.empty l)
 
 (** @return the qualified name and list of fields of
     the type with name [n].
@@ -917,10 +917,10 @@ and typing_automaton_handlers const_env h acc state_handlers =
   (* checks unicity of states *)
   let addname acc { s_state = n } =
     add_distinct_S n acc in
-  let states =  List.fold_left addname S.empty state_handlers in
+  let states =  List.fold_left addname NamesSet.empty state_handlers in
 
   let escape h ({ e_cond = e; e_next_state = n } as esc) =
-    if not (S.mem n states) then error (Eundefined(n));
+    if not (NamesSet.mem n states) then error (Eundefined(n));
     let typed_e = expect const_env h (Tid Initial.pbool) e in
     { esc with e_cond = typed_e } in
 
diff --git a/compiler/heptagon/hept_utils.ml b/compiler/heptagon/hept_utils.ml
index 919c449..c793242 100644
--- a/compiler/heptagon/hept_utils.ml
+++ b/compiler/heptagon/hept_utils.ml
@@ -98,3 +98,17 @@ let vars_pat pat =
 let rec vd_mem n = function
   | [] -> false
   | vd::l -> vd.v_ident = n or (vd_mem n l)
+
+let args_of_var_decs =
+  (* before the clocking the clock is wrong in the signature *)
+ List.map (fun vd -> Signature.mk_arg (Some (Idents.source_name vd.v_ident))
+                                      vd.v_type Signature.Cbase)
+
+let signature_of_node n =
+    { node_inputs = args_of_var_decs n.n_input;
+      node_outputs  = args_of_var_decs n.n_output;
+      node_stateful = n.n_stateful;
+      node_params = n.n_params;
+      node_params_constraints = n.n_params_constraints;
+      node_loc = n.n_loc }
+
diff --git a/compiler/heptagon/parsing/hept_parser.mly b/compiler/heptagon/parsing/hept_parser.mly
index 73a1a0e..41c1e09 100644
--- a/compiler/heptagon/parsing/hept_parser.mly
+++ b/compiler/heptagon/parsing/hept_parser.mly
@@ -279,7 +279,7 @@ ck_annot:
   | COLONCOLON ck=ck
   | ON ck=on_ck       { Some ck }
 
-ck:                                
+ck:
   | DOT                  { Cbase }
   | ck=on_ck             { ck }
 
diff --git a/compiler/heptagon/parsing/hept_scoping.ml b/compiler/heptagon/parsing/hept_scoping.ml
index b50c3f0..397bd30 100644
--- a/compiler/heptagon/parsing/hept_scoping.ml
+++ b/compiler/heptagon/parsing/hept_scoping.ml
@@ -103,7 +103,7 @@ let qualify_field = _qualify_with_error "field" qualify_field check_field
 (** Qualify a var name as a constant variable,
     if not in local_const or global_const then raise Not_found *)
 let qualify_var_as_const local_const c =
-  if S.mem c local_const
+  if NamesSet.mem c local_const
   then local_qn c
   else qualify_const c
 
@@ -165,12 +165,12 @@ let mk_signature name ins outs stateful params loc =
 (** Function to build the defined static parameters set *)
 let build_const loc vd_list =
   let _add_const_var loc c local_const =
-    if S.mem c local_const
+    if NamesSet.mem c local_const
     then Error.message loc (Error.Econst_variable_already_defined c)
-    else S.add c local_const in
+    else NamesSet.add c local_const in
   let build local_const vd =
     _add_const_var loc vd.v_name local_const in
-  List.fold_left build S.empty vd_list
+  List.fold_left build NamesSet.empty vd_list
 
 
 (** { 3 Translate the AST into Heptagon. } *)
@@ -410,39 +410,34 @@ let params_of_var_decs =
                         vd.v_name
                         (translate_type vd.v_loc vd.v_type))
 
-let args_of_var_decs =
-  (* before the clocking the clock is wrong in the signature *)
- List.map (fun vd -> Signature.mk_arg (Some (Idents.source_name vd.Heptagon.v_ident))
-                                      vd.Heptagon.v_type Signature.Cbase)
-
 
 let translate_node node =
   let n = current_qual node.n_name in
   Idents.enter_node n;
   let params = params_of_var_decs node.n_params in
   let input_env = Rename.append Rename.empty (node.n_input) in
-  (* inputs should refer only to inputs *)  
+  (* inputs should refer only to inputs *)
   let inputs = translate_vd_list input_env node.n_input in
-  (* Inputs and outputs define the initial local env *)  
+  (* Inputs and outputs define the initial local env *)
   let env0 = Rename.append input_env node.n_output in
   let outputs = translate_vd_list env0 node.n_output in
   let b, env = translate_block env0 node.n_block in
-  (* the env of the block is used in the contract translation *) 
+  (* the env of the block is used in the contract translation *)
   let contract = Misc.optional (translate_contract env) node.n_contract in
   (* add the node signature to the environment *)
-  let i = args_of_var_decs inputs in
-  let o = args_of_var_decs outputs in
-  let p = params_of_var_decs node.n_params in
-  add_value n (Signature.mk_node i o node.n_stateful p);
-  { Heptagon.n_name = n;
-    Heptagon.n_stateful = node.n_stateful;
-    Heptagon.n_input = inputs;
-    Heptagon.n_output = outputs;
-    Heptagon.n_contract = contract;
-    Heptagon.n_block = b;
-    Heptagon.n_loc = node.n_loc;
-    Heptagon.n_params = params;
-    Heptagon.n_params_constraints = []; }
+  let node = { Heptagon.n_name = n;
+               Heptagon.n_stateful = node.n_stateful;
+               Heptagon.n_input = inputs;
+               Heptagon.n_output = outputs;
+               Heptagon.n_contract = contract;
+               Heptagon.n_block = b;
+               Heptagon.n_loc = node.n_loc;
+               Heptagon.n_params = params;
+               Heptagon.n_params_constraints = []; }
+  in
+  add_value n (Hept_utils.signature_of_node node);
+  node
+
 
 let translate_typedec ty =
     let n = current_qual ty.t_name in
@@ -496,33 +491,24 @@ let translate_program p =
     Heptagon.p_opened = p.p_opened;
     Heptagon.p_desc = desc; }
 
+
 let translate_signature s =
-  (* helper functions, having [env] as being the list of existing var names *)
-  let rec append env sa_l = match sa_l with
-    | [] -> env
-    | sa::sa_l -> match sa.a_name with
-        | None -> append env sa_l
-        | Some x -> append (x::env) sa_l
-  and translate_some_clock loc env ck = match ck with
+  let rec translate_some_clock ck = match ck with
     | None -> Signature.Cbase
-    | Some ck -> translate_clock loc env ck
-  and translate_clock loc env ck = match ck with
+    | Some ck -> translate_clock ck
+  and translate_clock ck = match ck with
     | Cbase -> Signature.Cbase
-    | Con(ck,c,x) ->
-        if not (List.mem x env)
-        then message loc (Evar_unbound x)
-        else Signature.Con(translate_clock loc env ck, qualify_constrs c, x)
-  and translate_arg env a =
-    Signature.mk_arg a.a_name (translate_type s.sig_loc a.a_type)
-                              (translate_some_clock s.sig_loc env a.a_clock)
+    | Con(ck,c,x) -> Signature.Con(translate_clock ck, qualify_constrs c, x)
+  and translate_arg a = Signature.mk_arg a.a_name (translate_type s.sig_loc a.a_type)
+                                                  (translate_some_clock a.a_clock)
   in
   let n = current_qual s.sig_name in
-  let env = append [] s.sig_inputs in
-  let i = List.map (translate_arg env) s.sig_inputs in
-  let env = append env s.sig_outputs in
-  let o = List.map (translate_arg env) s.sig_outputs in
+  let i = List.map translate_arg s.sig_inputs in
+  let o = List.map translate_arg s.sig_outputs in
   let p = params_of_var_decs s.sig_params in
-  add_value n (Signature.mk_node i o s.sig_stateful p);
+  let sig_node = Signature.mk_node s.sig_loc i o s.sig_stateful p in
+  Signature.check_signature sig_node;
+  add_value n sig_node;
   mk_signature n i o s.sig_stateful p s.sig_loc
 
 
diff --git a/compiler/heptagon/parsing/hept_static_scoping.ml b/compiler/heptagon/parsing/hept_static_scoping.ml
index 6128930..418c9b4 100644
--- a/compiler/heptagon/parsing/hept_static_scoping.ml
+++ b/compiler/heptagon/parsing/hept_static_scoping.ml
@@ -72,13 +72,13 @@ let const_dec funs local_const cd =
 let program p =
   let funs = { Hept_parsetree_mapfold.defaults
                with node_dec = node; exp = exp; static_exp = static_exp; const_dec = const_dec } in
-  let p, _ = Hept_parsetree_mapfold.program_it funs Names.S.empty p in
+  let p, _ = Hept_parsetree_mapfold.program_it funs Names.NamesSet.empty p in
   p
 
 (* (* TODO mapfold on interface *)
 let interface i =
   let funs = { Hept_parsetree_mapfold.defaults
                with node_dec = node; exp = exp; const_dec = const_dec } in
-  let i, _ = Hept_parsetree_mapfold.interface_it funs Names.S.empty i in
+  let i, _ = Hept_parsetree_mapfold.interface_it funs Names.NamesSet.empty i in
   i
 *)
diff --git a/compiler/heptagon/transformations/inline.ml b/compiler/heptagon/transformations/inline.ml
index 80ce425..4acec7f 100644
--- a/compiler/heptagon/transformations/inline.ml
+++ b/compiler/heptagon/transformations/inline.ml
@@ -117,11 +117,11 @@ let node_dec funs (env, newvars, newequs) nd =
 let program p =
   let env n =
     let d =
-      List.find 
-	(function 
-	   | Pnode nd -> nd.n_name = n
-	   | _ -> false) 
-	p.p_desc in
+      List.find
+  (function
+     | Pnode nd -> nd.n_name = n
+     | _ -> false)
+  p.p_desc in
     match d with
     | Pnode nd -> nd
     | _ -> assert false in
diff --git a/compiler/heptagon/transformations/switch.ml b/compiler/heptagon/transformations/switch.ml
index b3ac085..3b12b70 100644
--- a/compiler/heptagon/transformations/switch.ml
+++ b/compiler/heptagon/transformations/switch.ml
@@ -133,7 +133,7 @@ let add_to_locals vd_env locals h =
   let add_one n nn (locals,vd_env) =
     let orig_vd = Idents.Env.find n vd_env in
     let vd_nn = mk_var_dec nn orig_vd.v_type in
-    vd_nn::locals, Idents.Env.add vd_nn.v_ident vd_nn vd_env 
+    vd_nn::locals, Idents.Env.add vd_nn.v_ident vd_nn vd_env
   in
     fold add_one h (locals, vd_env)
 end
@@ -197,7 +197,7 @@ let eqdesc funs (vd_env,env,h) eqd = match eqd with
         let equs = (mk_equation (Eblock b_eq))::equs in
         ((constr,h)::c_h_l, locals, equs, vd_env)
       in
-      
+
       let (c_h_l, locals, equs, vd_env) =
         List.fold_left switch_handler ([], locals, equs, vd_env) sw_h_l
       in
@@ -212,7 +212,7 @@ let eqdesc funs (vd_env,env,h) eqd = match eqd with
       let equs =
         Idents.Env.fold (fun n ty equs -> new_merge n ty equs) defnames equs
       in
-     
+
         (* return the transformation in a block *)
       let b = mk_block ~defnames:defnames ~locals:locals equs in
       Eblock b, (vd_env,env,h)
diff --git a/compiler/minils/analysis/clocking.ml b/compiler/minils/analysis/clocking.ml
index fef4416..a3eac0e 100644
--- a/compiler/minils/analysis/clocking.ml
+++ b/compiler/minils/analysis/clocking.ml
@@ -14,7 +14,7 @@
   Idem for e_ct : if explicit, it represents a clock annotation.
   Unification is done on this mutable fields.
   e_base_ck is set according to node signatures.
-  
+
  *)
 
 open Misc
@@ -121,7 +121,7 @@ let typing_app h base pat op w_list = match op with
 let typing_eq h { eq_lhs = pat; eq_rhs = e } =
   (* typing the expression *)
   let ct,base = match e.e_desc with
-    | Eextvalue w 
+    | Eextvalue w
     | Efby (_, w) ->
         let ck = typing_extvalue h w in
         Ck ck, ck
@@ -138,7 +138,7 @@ let typing_eq h { eq_lhs = pat; eq_rhs = e } =
           | None -> fresh_clock ()
           | Some(reset) -> ck_of_name h reset in
         let ct = typing_app h ck_r pat op args in
-        ct, ck_r    
+        ct, ck_r
     | Eiterator (_, _, _, pargs, args, r) ->
         (* Typed exactly as a fun or a node... *)
         let ck_r = match r with
@@ -195,12 +195,18 @@ let typing_node node =
   let h = append_env h node.n_output in
   let h = typing_contract h node.n_contract in
   let h = append_env h node.n_local in
-  (typing_eqs h node.n_equs;
+  typing_eqs h node.n_equs;
   (*update clock info in variables descriptions *)
   let set_clock vd = { vd with v_clock = ck_repr (Env.find vd.v_ident h) } in
-  { node with n_input = List.map set_clock node.n_input;
-              n_output = List.map set_clock node.n_output;
-              n_local = List.map set_clock node.n_local })
+  let node = { node with n_input = List.map set_clock node.n_input;
+                         n_output = List.map set_clock node.n_output;
+                         n_local = List.map set_clock node.n_local }
+  in
+  (* check signature causality and update it in the global env *)
+  let sign = Mls_utils.signature_of_node node in
+  Signature.check_signature sign;
+  Modules.replace_value node.n_name sign;
+  node
 
 let program p =
   let program_desc pd = match pd with
diff --git a/compiler/minils/mls_utils.ml b/compiler/minils/mls_utils.ml
index 99f2e98..ed55270 100644
--- a/compiler/minils/mls_utils.ml
+++ b/compiler/minils/mls_utils.ml
@@ -196,4 +196,17 @@ let ident_list_of_pat pat =
     | Etuplepat [] -> acc
     | Etuplepat (pat::pat_l) -> f (f acc pat) (Etuplepat pat_l)
   in
-  f [] pat 
+  f [] pat
+
+
+let args_of_var_decs =
+ List.map (fun vd -> Signature.mk_arg (Some (Idents.source_name vd.v_ident))
+                                      vd.v_type (Signature.ck_to_sck vd.v_clock))
+
+let signature_of_node n =
+    { node_inputs = args_of_var_decs n.n_input;
+      node_outputs  = args_of_var_decs n.n_output;
+      node_stateful = n.n_stateful;
+      node_params = n.n_params;
+      node_params_constraints = n.n_params_constraints;
+      node_loc = n.n_loc }