diff --git a/compiler/heptagon/analysis/hept_clocking.ml b/compiler/heptagon/analysis/hept_clocking.ml index 12351bb..204056e 100644 --- a/compiler/heptagon/analysis/hept_clocking.ml +++ b/compiler/heptagon/analysis/hept_clocking.ml @@ -72,10 +72,10 @@ let ident_list_of_pat pat = (* typing the expression, returns ct, ck_base *) let rec typing h pat e = let ct,base = match e.e_desc with - | Econst _ -> + | Econst _ -> let ck = fresh_clock() in Ck ck, ck - | Evar x -> + | Evar x -> let ck = ck_of_name h x in Ck ck, ck | Efby (e1, e2) -> @@ -143,7 +143,7 @@ let rec typing h pat e = in begin match e.e_ct_annot with None -> () - | Some e_ct -> + | Some e_ct -> try unify ct e_ct with Unify -> @@ -174,7 +174,7 @@ and typing_app h base pat op e_list = match op with | a::a_l, v::v_l -> (match a.a_name with | None -> build_env a_l v_l env | Some n -> build_env a_l v_l ((n,v)::env)) - | _ -> + | _ -> Printf.printf "Fun/node : %s\n" (Names.fullname f); Misc.internal_error "Clocking, non matching signature" in @@ -240,17 +240,17 @@ let typing_contract h contract = expect h' (Etuplepat []) (Ck Cbase) e_g; append_env h c_list -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_param_constraints = n.n_param_constraints; - node_loc = n.n_loc } +(* check signature causality and update it in the global env *) +let update_signature h node = + let set_arg_clock vd ad = + { ad with a_clock = Signature.ck_to_sck (ck_repr (Env.find vd.v_ident h)) } + in + let sign = Modules.find_value node.n_name in + let sign = + { sign with node_inputs = List.map2 set_arg_clock node.n_input sign.node_inputs; + node_outputs = List.map2 set_arg_clock node.n_output sign.node_outputs } in + Signature.check_signature sign; + Modules.replace_value node.n_name sign let typing_node node = let h0 = append_env Env.empty node.n_input in @@ -265,9 +265,7 @@ let typing_node node = n_output = List.map set_clock node.n_output } in (* check signature causality and update it in the global env *) - let sign = signature_of_node node in - Signature.check_signature sign; - Modules.replace_value node.n_name sign; + update_signature h node; node let program p = diff --git a/compiler/minils/analysis/clocking.ml b/compiler/minils/analysis/clocking.ml index 5ff5e43..a159a43 100644 --- a/compiler/minils/analysis/clocking.ml +++ b/compiler/minils/analysis/clocking.ml @@ -154,7 +154,7 @@ let typing_eq h { eq_lhs = pat; eq_rhs = e; eq_loc = loc } = typing_app h base_ck pat op (pargs@args) | Imapi -> (* clocking the node with the extra i input on [ck_r] *) let il (* stubs i as 0 *) = - List.map (fun x -> mk_extvalue ~ty:Initial.tint + List.map (fun x -> mk_extvalue ~ty:Initial.tint ~clock:base_ck (Wconst (Initial.mk_static_int 0))) nl in typing_app h base_ck pat op (pargs@args@il) @@ -165,7 +165,7 @@ let typing_eq h { eq_lhs = pat; eq_rhs = e; eq_loc = loc } = ct | Ifoldi -> (* clocking the node with the extra i and last in/out constraints *) let il (* stubs i as 0 *) = - List.map (fun x -> mk_extvalue ~ty:Initial.tint + List.map (fun x -> mk_extvalue ~ty:Initial.tint ~clock:base_ck (Wconst (Initial.mk_static_int 0))) nl in let rec insert_i args = match args with @@ -222,6 +222,18 @@ let typing_contract h contract = expect_extvalue h' Cbase e_g; append_env h c_list +(* check signature causality and update it in the global env *) +let update_signature h node = + let set_arg_clock vd ad = + { ad with a_clock = Signature.ck_to_sck (ck_repr (Env.find vd.v_ident h)) } + in + let sign = Modules.find_value node.n_name in + let sign = + { sign with node_inputs = List.map2 set_arg_clock node.n_input sign.node_inputs; + node_outputs = List.map2 set_arg_clock node.n_output sign.node_outputs } in + Signature.check_signature sign; + Modules.replace_value node.n_name sign + let typing_node node = let h0 = append_env Env.empty node.n_input in let h0 = append_env h0 node.n_output in @@ -236,10 +248,7 @@ let typing_node node = 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; + update_signature h node; node let program p = diff --git a/compiler/minils/mls_utils.ml b/compiler/minils/mls_utils.ml index 1be931b..b102fde 100644 --- a/compiler/minils/mls_utils.ml +++ b/compiler/minils/mls_utils.ml @@ -204,16 +204,3 @@ let ident_list_of_pat pat = | Etuplepat pat_l -> List.fold_left f acc pat_l in List.rev (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_param_constraints = n.n_param_constraints; - node_loc = n.n_loc }