From 3bf2d82d45d8fd5ca8696ca2952841f5bef334a2 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?C=C3=A9dric=20Pasteur?= Date: Fri, 9 Jul 2010 10:28:09 +0200 Subject: [PATCH] Make sure to run check_type on every Types declared by the user must be checked (this will also replaced names with the correct longname). --- compiler/heptagon/analysis/interface.ml | 4 +-- compiler/heptagon/analysis/typing.ml | 32 ++++++++++++--------- compiler/heptagon/parsing/hept_parsetree.ml | 3 +- compiler/heptagon/parsing/hept_scoping.ml | 2 +- 4 files changed, 24 insertions(+), 17 deletions(-) diff --git a/compiler/heptagon/analysis/interface.ml b/compiler/heptagon/analysis/interface.ml index 036399c..d492035 100644 --- a/compiler/heptagon/analysis/interface.ml +++ b/compiler/heptagon/analysis/interface.ml @@ -21,12 +21,12 @@ module Type = struct let sigtype { sig_name = name; sig_inputs = i_list; sig_statefull = statefull; sig_outputs = o_list; sig_params = params } = - let const_env = build_node_params NamesEnv.empty params in + let typed_params, const_env = build_node_params NamesEnv.empty params in let check_arg a = { a with a_type = check_type const_env a.a_type } in name, { node_inputs = List.map check_arg i_list; node_outputs = List.map check_arg o_list; node_statefull = statefull; - node_params = params; + node_params = typed_params; node_params_constraints = []; } let read { interf_desc = desc; interf_loc = loc } = diff --git a/compiler/heptagon/analysis/typing.ml b/compiler/heptagon/analysis/typing.ml index 0104524..1dab1a5 100644 --- a/compiler/heptagon/analysis/typing.ml +++ b/compiler/heptagon/analysis/typing.ml @@ -545,11 +545,11 @@ and typing_static_args const_env expected_ty_list e_list = error (Earity_clash(List.length e_list, List.length expected_ty_list)) and expect_static_exp const_env exp_ty se = - let se, ty = typing_static_exp const_env se in - try - unify ty exp_ty; se - with - Unify -> message se.se_loc (Etype_clash(ty, exp_ty)) + let se, ty = typing_static_exp const_env se in + try + unify ty exp_ty; se + with + _ -> message se.se_loc (Etype_clash(ty, exp_ty)) (** @return the type of the field with name [f] in the list [fields]. [t1] is the corresponding record type and [loc] is @@ -1078,8 +1078,11 @@ let solve loc cl = Solve_failed c -> message loc (Econstraint_solve_failed c) let build_node_params const_env l = - List.fold_left (fun env p -> NamesEnv.add p.p_name p.p_type env) - const_env l + let check_param env p = + let ty = check_type const_env p.p_type in + { p with p_type = ty }, NamesEnv.add p.p_name ty env + in + mapfold check_param const_env l let node ({ n_name = f; n_statefull = statefull; n_input = i_list; n_output = o_list; @@ -1087,9 +1090,10 @@ let node ({ n_name = f; n_statefull = statefull; n_local = l_list; n_equs = eq_list; n_loc = loc; n_params = node_params; } as n) = try - let const_env = build_node_params NamesEnv.empty node_params in - - let typed_i_list, input_names, h = build const_env Env.empty Env.empty i_list in + let typed_params, const_env = + build_node_params NamesEnv.empty node_params in + let typed_i_list, input_names, h = + build const_env Env.empty Env.empty i_list in let typed_o_list, output_names, h = build const_env h h o_list in (* typing contract *) @@ -1107,12 +1111,13 @@ let node ({ n_name = f; n_statefull = statefull; let cl = get_size_constraint () in let cl = solve loc cl in - add_value f (signature statefull i_list o_list node_params cl); + add_value f (signature statefull typed_i_list typed_o_list typed_params cl); { n with n_input = List.rev typed_i_list; n_output = List.rev typed_o_list; n_local = typed_l_list; + n_params = typed_params; n_contract = typed_contract; n_equs = typed_eq_list } with @@ -1140,8 +1145,9 @@ let deftype { t_name = n; t_desc = tdesc; t_loc = loc } = TypingError(error) -> message loc error let typing_const_dec cd = - let se = expect_static_exp NamesEnv.empty cd.c_type cd.c_value in - let cd = { cd with c_value = se } in + let ty = check_type NamesEnv.empty cd.c_type in + let se = expect_static_exp NamesEnv.empty ty cd.c_value in + let cd = { cd with c_value = se; c_type = ty } in add_const cd.c_name (mk_const_def cd.c_name cd.c_type cd.c_value); cd diff --git a/compiler/heptagon/parsing/hept_parsetree.ml b/compiler/heptagon/parsing/hept_parsetree.ml index 334ae7f..f3643bf 100644 --- a/compiler/heptagon/parsing/hept_parsetree.ml +++ b/compiler/heptagon/parsing/hept_parsetree.ml @@ -176,7 +176,8 @@ let mk_call ?(params=[]) op exps = Eapp (mk_app op params, exps) let mk_op_call ?(params=[]) s exps = - mk_call ~params:params (Efun (Name s)) exps + mk_call ~params:params + (Efun (Modname { qual = "Pervasives"; id = s })) exps let mk_iterator_call it ln params n exps = Eiterator (it, mk_app (Enode ln) params, n, exps) diff --git a/compiler/heptagon/parsing/hept_scoping.ml b/compiler/heptagon/parsing/hept_scoping.ml index b29cf00..4345bf5 100644 --- a/compiler/heptagon/parsing/hept_scoping.ml +++ b/compiler/heptagon/parsing/hept_scoping.ml @@ -102,7 +102,7 @@ let translate_iterator_type = function let op_from_app loc app = match app.a_op with - | Efun op -> op_from_app_name op + | Efun op | Enode op -> op_from_app_name op | _ -> raise Not_static let rec static_exp_of_exp const_env e =