diff --git a/compiler/global/signature.ml b/compiler/global/signature.ml index 1c99fa5..be57d6f 100644 --- a/compiler/global/signature.ml +++ b/compiler/global/signature.ml @@ -18,7 +18,7 @@ let interface_format_version = "8" (** Node argument *) type arg = { a_name : name option; a_type : ty } -type param = { p_name : name } +type param = { p_name : name; p_type : ty } (** Node signature *) type node = @@ -40,7 +40,7 @@ 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_param name = { p_name = name } +let mk_param name ty = { p_name = name; p_type = ty } let mk_field n ty = { f_name = n; f_type = ty } diff --git a/compiler/heptagon/analysis/typing.ml b/compiler/heptagon/analysis/typing.ml index 339962f..a1ff811 100644 --- a/compiler/heptagon/analysis/typing.ml +++ b/compiler/heptagon/analysis/typing.ml @@ -599,9 +599,11 @@ and typing_app statefull const_env h op e_list = params in let expected_ty_list = List.map (subst_type_vars m) expected_ty_list in let typed_e_list = typing_args statefull h expected_ty_list e_list in + let result_ty_list = List.map (subst_type_vars m) result_ty_list in + (* Type static parameters and generate constraints *) + typing_node_params const_env h ty_desc.node_params params; let size_constrs = instanciate_constr m ty_desc.node_params_constraints in - let result_ty_list = List.map (subst_type_vars m) result_ty_list in List.iter add_size_constraint size_constrs; (prod result_ty_list, Ecall ( { op_desc with op_name = Modname q; op_kind = k }, reset), @@ -767,6 +769,10 @@ and typing_args statefull h expected_ty_list e_list = with Invalid_argument _ -> error (Earity_clash(List.length e_list, List.length expected_ty_list)) +and typing_node_params const_env h params_sig params = + List.map2 (fun p_sig p -> expect_static_exp const_env no_location + p_sig.p_type p) params_sig params + let rec typing_pat h acc = function | Evarpat(x) -> let ty = typ_of_name h x in @@ -977,7 +983,7 @@ let solve loc env cl = Solve_failed c -> message loc (Econstraint_solve_failed c) let build_node_params const_env l = - List.fold_left (fun env n -> NamesEnv.add n (Tid Initial.pint) env) + List.fold_left (fun env p -> NamesEnv.add p.p_name p.p_type env) const_env l let node const_env const_value_env ({ n_name = f; n_statefull = statefull; @@ -1043,9 +1049,9 @@ let build_const_value_env cd_list = NamesEnv.empty cd_list let build_const_env cd_list = - let typing_const_dec const_envenv cd = + let typing_const_dec const_env cd = expect_static_exp const_env cd.c_loc cd.c_type cd.c_value; - NamesEnv.add cd.c_name cd.c_type env + NamesEnv.add cd.c_name cd.c_type const_env in List.fold_left typing_const_env NamesEnv.empty cd_list diff --git a/compiler/heptagon/parsing/hept_parser.mly b/compiler/heptagon/parsing/hept_parser.mly index d03297d..fdd35d2 100644 --- a/compiler/heptagon/parsing/hept_parser.mly +++ b/compiler/heptagon/parsing/hept_parser.mly @@ -197,7 +197,7 @@ nonmt_out_params: node_params: | /* empty */ { [] } - | DOUBLE_LESS ident_list DOUBLE_GREATER { $2 } + | DOUBLE_LESS nonmt_params DOUBLE_GREATER { $2 } ; contract: diff --git a/compiler/heptagon/parsing/parsetree.ml b/compiler/heptagon/parsing/parsetree.ml index a2cc43f..ae8f60e 100644 --- a/compiler/heptagon/parsing/parsetree.ml +++ b/compiler/heptagon/parsing/parsetree.ml @@ -127,7 +127,7 @@ type node_dec = n_contract : contract option; n_equs : eq list; n_loc : location; - n_params : name list; } + n_params : var_dec list; } type const_dec = { c_name : name; diff --git a/compiler/heptagon/parsing/scoping.ml b/compiler/heptagon/parsing/scoping.ml index 434e39c..ff9abb5 100644 --- a/compiler/heptagon/parsing/scoping.ml +++ b/compiler/heptagon/parsing/scoping.ml @@ -284,6 +284,9 @@ let translate_contract const_env env ct = Heptagon.c_local = translate_vd_list const_env env ct.c_local; Heptagon.c_eq = List.map (translate_eq const_env env) ct.c_eq } +let param_of_var_dec vd = + mk_param vd.v_name vd.v_type + let translate_node const_env env node = let const_env = build_id_list node.n_loc const_env node.n_params in let env = build_vd_list env (node.n_input @ node.n_output @ node.n_local) in @@ -296,7 +299,7 @@ let translate_node const_env env node = (translate_contract const_env env) node.n_contract; Heptagon.n_equs = List.map (translate_eq const_env env) node.n_equs; Heptagon.n_loc = node.n_loc; - Heptagon.n_params = List.map Signature.mk_param node.n_params; + Heptagon.n_params = List.map param_of_var_dec node.n_params; Heptagon.n_params_constraints = []; } let translate_typedec const_env ty =