From 68ecd0e781dbd11d1151b165a24a295eee168473 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?C=C3=A9dric=20Pasteur?= Date: Wed, 7 Jul 2010 16:43:23 +0200 Subject: [PATCH] Added consts in the signature of a module --- compiler/global/modules.ml | 8 +- compiler/global/signature.ml | 6 +- compiler/global/static.ml | 19 ++++- compiler/heptagon/analysis/interface.ml | 15 +++- compiler/heptagon/analysis/typing.ml | 84 ++++++++++----------- compiler/heptagon/heptagon.ml | 1 + compiler/heptagon/parsing/hept_parser.mly | 1 + compiler/heptagon/parsing/hept_parsetree.ml | 1 + compiler/heptagon/parsing/hept_scoping.ml | 1 + 9 files changed, 84 insertions(+), 52 deletions(-) diff --git a/compiler/global/modules.ml b/compiler/global/modules.ml index 1a36225..0f5febf 100644 --- a/compiler/global/modules.ml +++ b/compiler/global/modules.ml @@ -27,7 +27,7 @@ type env = mutable constr: ty NamesEnv.t; mutable structs: structure NamesEnv.t; mutable fields: name NamesEnv.t; - (* TODO CP mutable consts: const_def NamesEnv.t; *) + mutable consts: const_def NamesEnv.t; format_version : string; } @@ -40,7 +40,7 @@ type modules = let current = { name = ""; values = NamesEnv.empty; types = NamesEnv.empty; constr = NamesEnv.empty; structs = NamesEnv.empty; fields = NamesEnv.empty; - format_version = interface_format_version } + consts = NamesEnv.empty; format_version = interface_format_version } let modules = { current = current; opened = []; modules = NamesEnv.empty } @@ -136,12 +136,16 @@ let add_struct f fields = let add_field f n = if NamesEnv.mem f current.fields then raise Already_defined; current.fields <- NamesEnv.add f n current.fields +let add_const c n = + if NamesEnv.mem f current.consts then raise Already_defined; + current.consts <- NamesEnv.add f n current.consts let find_value = find (fun ident m -> NamesEnv.find ident m.values) let find_type = find (fun ident m -> NamesEnv.find ident m.types) let find_constr = find (fun ident m -> NamesEnv.find ident m.constr) let find_struct = find (fun ident m -> NamesEnv.find ident m.structs) let find_field = find (fun ident m -> NamesEnv.find ident m.fields) +let find_const = find (fun ident m -> NamesEnv.find ident m.consts) let replace_value f signature = current.values <- NamesEnv.remove f current.values; diff --git a/compiler/global/signature.ml b/compiler/global/signature.ml index fa41431..dc91a93 100644 --- a/compiler/global/signature.ml +++ b/compiler/global/signature.ml @@ -13,7 +13,7 @@ open Static (** Warning: Whenever these types are modified, interface_format_version should be incremented. *) -let interface_format_version = "8" +let interface_format_version = "9" (** Node argument *) type arg = { a_name : name option; a_type : ty } @@ -34,6 +34,8 @@ type structure = field list type type_def = | Tabstract | Tenum of name list | Tstruct of structure +type const_def = { c_name : name; c_type : ty; c_value : static_exp } + 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 @@ -44,6 +46,8 @@ let mk_param name ty = { p_name = name; p_type = ty } let mk_field n ty = { f_name = n; f_type = ty } +let mk_const_def name ty value = + { c_name = name; c_type = ty; c_value = value } let rec field_assoc f = function | [] -> raise Not_found diff --git a/compiler/global/static.ml b/compiler/global/static.ml index e4bd165..e64c671 100644 --- a/compiler/global/static.ml +++ b/compiler/global/static.ml @@ -56,8 +56,16 @@ let apply_int_op op n1 n2 = let rec simplify env se = match se.se_desc with | Sint _ | Sfloat _ | Sbool _ | Sconstructor _ -> se - | Svar id -> - (try simplify env (NamesEnv.find (shortname id) env) with | _ -> se) + | Svar ln -> + (try + let { info = cd } = find_const ln in + simplify env cd.c_value + with + Not_found -> + (match ln with + | Name n -> (try simplify env (NamesEnv.find id env) with | _ -> se) + | Modname _ -> se) + ) | Sop (op, [e1; e2]) -> let e1 = simplify env e1 in let e2 = simplify env e2 in @@ -126,8 +134,11 @@ let rec solve const_env = (** Substitutes variables in the size exp with their value in the map (mapping vars to size exps). *) let rec static_exp_subst m se = - let desc = match se.se_desc with - | Svar n -> (try List.assoc n m with | Not_found -> Svar n) + let desc = match se.e_desc with + | Svar ln -> + (match ln with + | Name n -> (try List.assoc n m with | Not_found -> Svar n) + | Modname _ -> Svar ln) | Sop (op, se_list) -> Sop (op, List.map (static_exp_subst m) se_list) | Sarray_power (se, n) -> Sarray_power (static_exp_subst m se, static_exp_subst m n) diff --git a/compiler/heptagon/analysis/interface.ml b/compiler/heptagon/analysis/interface.ml index 350205f..6d66b93 100644 --- a/compiler/heptagon/analysis/interface.ml +++ b/compiler/heptagon/analysis/interface.ml @@ -34,6 +34,7 @@ struct match desc with | Iopen(n) -> open_module n | Itypedef(tydesc) -> deftype NamesEnv.empty NamesEnv.empty tydesc + | Iconstdef cd -> typing_const_dec cd | Isignature(s) -> let name, s = sigtype s in add_value name s @@ -65,6 +66,15 @@ struct print_type ff ty) "{" ";" "}" ff f_ty_list; fprintf ff "@]@.@]" + let constdef ff c = + fprintf ff "@[const "; + print_name ff c.c_name; + fprintf ff " : "; + print_type ff c.c_type; + fprintf ff " = "; + print_static_exp ff c.c_value; + fprintf ff "@.@]" + let signature ff name { node_inputs = inputs; node_outputs = outputs; node_params = params; @@ -100,6 +110,7 @@ struct let print oc = let ff = formatter_of_out_channel oc in - NamesEnv.iter (fun key typdesc -> deftype ff key typdesc) current.types; - NamesEnv.iter (fun key sigtype -> signature ff key sigtype) current.values; + NamesEnv.iter (fun key typdesc -> deftype ff key typdesc) current.types; + NamesEnv.iter (fun key constdec -> constdef ff key constdec) current.consts; + NamesEnv.iter (fun key sigtype -> signature ff key sigtype) current.values; end diff --git a/compiler/heptagon/analysis/typing.ml b/compiler/heptagon/analysis/typing.ml index b0d48b2..d853070 100644 --- a/compiler/heptagon/analysis/typing.ml +++ b/compiler/heptagon/analysis/typing.ml @@ -40,7 +40,7 @@ type error = | Esome_fields_are_missing | Esubscripted_value_not_an_array of ty | Earray_subscript_should_be_const - | Eundefined_const of name + | Eundefined_const of longname | Econstraint_solve_failed of size_constraint | Etype_should_be_static of ty | Erecord_type_expected of ty @@ -123,11 +123,11 @@ let message loc kind = Printf.eprintf "%aSubscript has to be a static value.\n" output_location loc - | Eundefined_const id -> + | Eundefined_const ln -> Printf.eprintf - "%aThe const name '%s' is unbound.\n" + "%aThe const name '%a' is unbound.\n" output_location loc - id + print_longname ln | Econstraint_solve_failed c -> Printf.eprintf "%aThe following constraint cannot be satisified:\n %a.\n" @@ -166,6 +166,8 @@ let add_struct f fields = try add_struct f fields with Already_defined -> error (Ealready_defined f) let add_field f n = try add_field f n with Already_defined -> error (Ealready_defined f) +let add_const f n = + try add_const f n with Already_defined -> error (Ealready_defined f) let find_value f = try find_value f with Not_found -> error (Eundefined(fullname f)) @@ -282,18 +284,24 @@ let prod = function | ty_list -> Tprod ty_list let typing_static_exp const_env se = - let desc, ty = match se with + let desc, ty = match se.e_desc with | Sint -> Sint, Initial.pint | Sbool -> Sbool, Initial.pbool | Sfloat -> Sfloat, Initial.pfloat - | Svar n -> - (try - Svar n, NamesEnv.find n const_env - with - Not_found -> message no_location (Eundefined_const n)) + | Svar ln -> + (try (* this can be a global const*) + let { qualid = q; info = cd } = find_const ln in + Svar q, cd.c_type + with Not_found -> (* or a static parameter *) + (match ln with + | Name n -> + (try Svar ln, NamesEnv.find n const_env + with Not_found -> message se.se_loc (Eundefined_const ln)) + | Modname _ -> message se.se_loc (Eundefined_const ln)) + ) | Sconstructor c -> let { qualid = q; info = ty } = find_constr c in - Sconstructor(Modname q), ty + Sconstructor(Modname q), t | Sop (op, se_list) -> let { qualid = q; info = ty_desc } = find_value op in let typed_se_list = List.map2 (typing_static_args const_env) @@ -305,7 +313,7 @@ let typing_static_exp const_env se = let typed_se, ty = typing_static_exp const_env se in Sarray_power (typed_se, typed_n), Tarray(ty, n) | Sarray [] -> - message no_location Eempty_array + message se.se_loc Eempty_array | Sarray se::se_list -> let typed_se, ty = typing_static_exp const_env se in let typed_se_list = List.map (expect_static_exp const_env ty) se_list in @@ -987,9 +995,9 @@ let typing_contract statefull h contract = c_enforce = typed_e_g }, controllable_names, h -let signature const_value_env statefull inputs returns params constraints = +let signature statefull inputs returns params constraints = let arg_dec_of_var_dec vd = - mk_arg (Some (name vd.v_ident)) (simplify_type const_value_env vd.v_type) + mk_arg (Some (name vd.v_ident)) (simplify_type NamesEnv.empty vd.v_type) in { node_inputs = List.map arg_dec_of_var_dec inputs; node_outputs = List.map arg_dec_of_var_dec returns; @@ -1007,13 +1015,13 @@ 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 node const_env const_value_env ({ n_name = f; n_statefull = statefull; - n_input = i_list; n_output = o_list; - n_contract = contract; - n_local = l_list; n_equs = eq_list; n_loc = loc; - n_params = node_params; } as n) = +let node ({ n_name = f; n_statefull = statefull; + n_input = i_list; n_output = o_list; + n_contract = contract; + n_local = l_list; n_equs = eq_list; n_loc = loc; + n_params = node_params; } as n) = try - let const_env = build_node_params const_env node_params in + 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_o_list, output_names, h = build const_env h h o_list in @@ -1032,8 +1040,8 @@ let node const_env const_value_env ({ n_name = f; n_statefull = statefull; included_env defined_names expected_names; let cl = get_size_constraint () in - let cl = solve loc const_value_env cl in - add_value f (signature const_value_env statefull i_list o_list node_params cl); + let cl = solve loc cl in + add_value f (signature statefull i_list o_list node_params cl); { n with n_input = List.rev typed_i_list; @@ -1044,7 +1052,7 @@ let node const_env const_value_env ({ n_name = f; n_statefull = statefull; with | TypingError(error) -> message loc error -let deftype const_env const_value_env { t_name = n; t_desc = tdesc; t_loc = loc } = +let deftype { t_name = n; t_desc = tdesc; t_loc = loc } = try match tdesc with | Type_abs -> add_type n Tabstract @@ -1055,7 +1063,7 @@ let deftype const_env const_value_env { t_name = n; t_desc = tdesc; t_loc = loc let field_ty_list = List.map (fun f -> mk_field f.f_name - (simplify_type loc const_value_env + (simplify_type loc NamesEnv.empty (check_type const_env f.f_type)) field_ty_list in add_type n (Tstruct field_ty_list); @@ -1065,26 +1073,16 @@ let deftype const_env const_value_env { t_name = n; t_desc = tdesc; t_loc = loc with TypingError(error) -> message loc error -let build_const_value_env cd_list = - List.fold_left (fun env cd -> NamesEnv.add cd.c_name cd.c_value env) - NamesEnv.empty cd_list - -let build_const_env cd_list = - let typing_const_dec (const_env, cd_list) cd = - let ty = expect_static_exp const_env cd.c_loc cd.c_type cd.c_value in - let cd = { cd with c_type = ty } in - NamesEnv.add cd.c_name cd.c_type const_env, cd::cd_list - in - let const_env, cd_list = List.fold_left typing_const_env - NamesEnv.empty cd_list in - const_env, List.rev cd_list +let typing_const_dec cd = + let ty = expect_static_exp NamesEnv.empty cd.c_loc cd.c_type cd.c_value in + let cd = { cd with c_type = ty } in + add_const cd.c_name (mk_const_def cd.c_name cd.c_type cd.c_value) let program ({ p_opened = opened; p_types = p_type_list; p_nodes = p_node_list; p_consts = p_consts_list } as p) = - let const_env, cd_list = build_const_env p_consts_list in - let const_value_env = build_const_value_env p_consts_list in - List.iter open_module opened; - List.iter (deftype const_env const_value_env) p_type_list; - let typed_node_list = List.map (node const_env const_value_env) p_node_list in - { p with p_nodes = typed_node_list; p_consts = cd_list } + List.iter typing_const_dec p_consts_list; + List.iter open_module opened; + List.iter deftype p_type_list; + let typed_node_list = List.map node p_node_list in + { p with p_nodes = typed_node_list; p_consts = cd_list } diff --git a/compiler/heptagon/heptagon.ml b/compiler/heptagon/heptagon.ml index 8d044a3..da98bc1 100644 --- a/compiler/heptagon/heptagon.ml +++ b/compiler/heptagon/heptagon.ml @@ -143,6 +143,7 @@ and interface_decl = { interf_desc : interface_desc; interf_loc : location } and interface_desc = | Iopen of name | Itypedef of type_dec + | Iconstdef of const_dec | Isignature of signature (* Helper functions to create AST. *) diff --git a/compiler/heptagon/parsing/hept_parser.mly b/compiler/heptagon/parsing/hept_parser.mly index e7c515f..2115582 100644 --- a/compiler/heptagon/parsing/hept_parser.mly +++ b/compiler/heptagon/parsing/hept_parser.mly @@ -550,6 +550,7 @@ interface_decls: interface_decl: | type_dec { mk_interface_decl (Itypedef $1) } + | const_dec { mk_interface_decl (Iconstdef $1) } | OPEN Constructor { mk_interface_decl (Iopen $2) } | VAL node_or_fun ident node_params LPAREN params_signature RPAREN RETURNS LPAREN params_signature RPAREN diff --git a/compiler/heptagon/parsing/hept_parsetree.ml b/compiler/heptagon/parsing/hept_parsetree.ml index ae8f60e..5d96f30 100644 --- a/compiler/heptagon/parsing/hept_parsetree.ml +++ b/compiler/heptagon/parsing/hept_parsetree.ml @@ -160,6 +160,7 @@ and interface_decl = and interface_desc = | Iopen of name | Itypedef of type_dec + | Iconstdef of const_dec | Isignature of signature (* Helper functions to create AST. *) diff --git a/compiler/heptagon/parsing/hept_scoping.ml b/compiler/heptagon/parsing/hept_scoping.ml index 58f93cb..f772ff4 100644 --- a/compiler/heptagon/parsing/hept_scoping.ml +++ b/compiler/heptagon/parsing/hept_scoping.ml @@ -347,6 +347,7 @@ let translate_signature s = let translate_interface_desc const_env = function | Iopen n -> Heptagon.Iopen n | Itypedef tydec -> Heptagon.Itypedef (translate_typedec const_env tydec) + | Iconstdef const_dec -> Heptagon.Iconstdef (translate_const_dec const_env const_dec) | Isignature s -> Heptagon.Isignature (translate_signature s) let translate_interface_decl const_env idecl =