diff --git a/compiler/global/signature.ml b/compiler/global/signature.ml index 2db89e8..c040ab1 100644 --- a/compiler/global/signature.ml +++ b/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 } diff --git a/compiler/heptagon/parsing/hept_lexer.mll b/compiler/heptagon/parsing/hept_lexer.mll index e370f0d..6663ac2 100644 --- a/compiler/heptagon/parsing/hept_lexer.mll +++ b/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; diff --git a/compiler/heptagon/parsing/hept_parser.mly b/compiler/heptagon/parsing/hept_parser.mly index 30d2fdc..7e97d28 100644 --- a/compiler/heptagon/parsing/hept_parser.mly +++ b/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 } ; %% diff --git a/compiler/heptagon/parsing/hept_parsetree.ml b/compiler/heptagon/parsing/hept_parsetree.ml index a2f4436..68a26c2 100644 --- a/compiler/heptagon/parsing/hept_parsetree.ml +++ b/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 diff --git a/compiler/heptagon/parsing/hept_scoping.ml b/compiler/heptagon/parsing/hept_scoping.ml index 448ee16..6ba7b7a 100644 --- a/compiler/heptagon/parsing/hept_scoping.ml +++ b/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