a_clock in signatures

compiler/global/signature.ml

@@ -9,13 +9,18 @@
 (* global data in the symbol tables *)
 open Names
 open Types
+open Clocks
 
 (** Warning: Whenever these types are modified,
     interface_format_version should be incremented. *)
-let interface_format_version = "20"
+let interface_format_version = "30"
 
-(** Node argument *)
-type arg = { a_name : name option; a_type : ty }
+(** Node argument : inputs and outputs *)
+type arg = {
+  a_name  : name option;
+  a_type  : ty;
+  a_clock : ck; (** [a_clock] set to [Cbase] means at the node activation clock *)
+}
 
 (** Node static parameters *)
 type param = { p_name : name; p_type : ty }
@@ -28,10 +33,10 @@ type size_constraint =
 
 (** Node signature *)
 type node = {
-  node_inputs : arg list;
-  node_outputs : arg list;
-  node_stateful : bool;
-  node_params : param list;
+  node_inputs             : arg list;
+  node_outputs            : arg list;
+  node_stateful           : bool;
+  node_params             : param list;
   node_params_constraints : size_constraint list }
 
 type field = { f_name : field_name; f_type : ty }
@@ -49,7 +54,7 @@ let names_of_arg_list l = List.map (fun ad -> ad.a_name) l
 
 let types_of_arg_list l = List.map (fun ad -> ad.a_type) l
 
-let mk_arg name ty = { a_type = ty; a_name = name }
+let mk_arg name ty ck = { a_type = ty; a_name = name; a_clock = ck }
 
 let mk_param name ty = { p_name = name; p_type = ty }
 

compiler/heptagon/parsing/hept_lexer.mll

@@ -55,6 +55,7 @@ List.iter (fun (str,tok) -> Hashtbl.add keyword_table str tok) [
  "with", WITH;
  "when", WHEN;
  "merge", MERGE;
+ "on", ON;
  "map", MAP;
  "mapi", MAPI;
  "fold", FOLD;

compiler/heptagon/parsing/hept_parser.mly

@@ -39,7 +39,7 @@ open Hept_parsetree
 %token ASSUME
 %token ENFORCE
 %token WITH
-%token WHEN MERGE
+%token WHEN MERGE ON
 %token POWER
 %token LBRACKET LBRACKETGREATER
 %token RBRACKET LESSRBRACKET
@@ -268,6 +268,10 @@ ty_ident:
       { Tarray ($1, $3) }
 ;
 
+on_ck:
+  | /*empty */                                              { Cbase }
+  | b=on_ck ON c=constructor_or_bool LPAREN x=IDENT RPAREN  { Con (b,c,x) }
+
 equs:
   | /* empty */                      { [] }
   | eqs=optsnlist(SEMICOL,equ)       { eqs }
@@ -626,8 +630,8 @@ nonmt_params_signature:
 ;
 
 param_signature:
-  | IDENT COLON ty_ident { mk_arg (Some $1) $3 }
-  | ty_ident { mk_arg None $1 }
+  | IDENT COLON ty_ident ck=on_ck { mk_arg (Some $1) $3 ck }
+  | ty_ident ck=on_ck { mk_arg None $1 ck }
 ;
 
 %%

compiler/heptagon/parsing/hept_parsetree.ml

@@ -61,6 +61,11 @@ type ty =
   | Tid of qualname
   | Tarray of ty * exp
 
+and ck =
+  | Cbase
+  | Con of ck * constructor_name * var_name
+
+
 and exp =
   { e_desc : edesc;
     e_ct_annot : Clocks.ct;
@@ -192,8 +197,9 @@ and program_desc =
 
 
 type arg =
-  { a_type : ty;
-    a_name : var_name option }
+  { a_type  : ty;
+    a_clock : ck;
+    a_name  : var_name option }
 
 type signature =
   { sig_name      : dec_name;
@@ -261,8 +267,8 @@ let mk_block locals eqs loc =
 let mk_const_dec id ty e loc =
   { c_name = id; c_type = ty; c_value = e; c_loc = loc }
 
-let mk_arg name ty =
-  { a_type = ty; a_name = name }
+let mk_arg name ty ck =
+  { a_type = ty; a_name = name; a_clock = ck}
 
 let ptrue = Q Initial.ptrue
 let pfalse = Q Initial.pfalse

compiler/heptagon/parsing/hept_scoping.ml

@@ -233,6 +233,7 @@ let rec translate_type loc ty =
   with
     | ScopingError err -> message loc err
 
+
 let rec translate_exp env e =
   try
     { Heptagon.e_desc = translate_desc e.e_loc env e.e_desc;
@@ -399,7 +400,8 @@ let params_of_var_decs =
 let args_of_var_decs =
   List.map (fun vd -> Signature.mk_arg
                         (Some vd.v_name)
-                        (translate_type vd.v_loc vd.v_type))
+                        (translate_type vd.v_loc vd.v_type)
+                        Clocks.Cbase) (* before clocking and without annotations, default choice.*)
 
 let translate_node node =
   let n = current_qual node.n_name in
@@ -482,7 +484,10 @@ let translate_program p =
 
 let translate_signature s =
   let translate_arg a =
-    Signature.mk_arg a.a_name (translate_type s.sig_loc a.a_type) in
+    Signature.mk_arg a.a_name
+      (translate_type s.sig_loc a.a_type)
+      (translate_clock s.sig_loc a.a_clock))
+  in
   let n = current_qual s.sig_name in
   let i = List.map translate_arg s.sig_inputs in
   let o = List.map translate_arg s.sig_outputs in