diff --git a/src/compiledData.ml b/src/compiledData.ml index 898cafa265f019cf4b5ebca31db4f14f80b45dca..3485d894a0a5b4ab46c4ab7bf249b49c8a5cdde7 100644 --- a/src/compiledData.ml +++ b/src/compiledData.ml @@ -1,4 +1,4 @@ -(** Time-stamp: <modified the 21/08/2008 (at 18:06) by Erwan Jahier> *) +(** Time-stamp: <modified the 26/08/2008 (at 10:17) by Erwan Jahier> *) (** @@ -406,15 +406,15 @@ let (type_eff_are_compatible : type_eff -> type_eff -> bool) = | External_type_eff _, _ -> true | t1, t2 -> t1 = t2 +let rec (clock_eff_are_equals : clock_eff -> clock_eff -> bool) = + fun c1 c2 -> match c1, c2 with + | On(_,c1), On(_,c2) -> clock_eff_are_equals c1 c2 + | c1, c2 -> c1 = c2 + let (var_eff_are_compatible : var_info_eff -> var_info_eff -> bool) = fun v1 v2 -> - let type_is_ok = - match v1.var_type_eff, v2.var_type_eff with - | External_type_eff id1, External_type_eff id2 -> id1 = id2 - | External_type_eff _, _ -> true - | t1, t2 -> t1 = t2 - in - type_is_ok && v1.var_clock_eff = v2.var_clock_eff + (type_eff_are_compatible v1.var_type_eff v2.var_type_eff) && + (clock_eff_are_equals v1.var_clock_eff v2.var_clock_eff) (****************************************************************************) (* Utilitaires liƩs aux node_key *) diff --git a/src/lazyCompiler.ml b/src/lazyCompiler.ml index 41a2fbadacc9ceec7b35a88f3ff1ffeb813a0f91..1067ff8607b01cf69e23bb40dead991b964f1b0a 100644 --- a/src/lazyCompiler.ml +++ b/src/lazyCompiler.ml @@ -1,4 +1,4 @@ -(** Time-stamp: <modified the 25/08/2008 (at 11:44) by Erwan Jahier> *) +(** Time-stamp: <modified the 26/08/2008 (at 10:25) by Erwan Jahier> *) open Lxm @@ -486,28 +486,52 @@ and (node_check_interface_do: t -> CompiledData.node_key -> Lxm.t -> (** [type_eff_are_compatible t1 t2] checks that t1 is compatible with t2, i.e., if t1 = t2 or t1 is abstract and and t2. *) - let type_is_comp v1 v2 = CompiledData.var_eff_are_compatible v1 v2 in + let msg_prefix = + ("provided node for " ^ (Ident.string_of_long (fst nk)) ^ + " is not compatible with its implementation: ") + in + let str_of_var = LicDump.type_string_of_var_info_eff in + let type_is_not_comp v1 v2 = not (CompiledData.var_eff_are_compatible v1 v2) in if - prov_node_exp_eff.node_key_eff = body_node_exp_eff.node_key_eff && - (List.for_all2 type_is_comp - prov_node_exp_eff.inlist_eff body_node_exp_eff.inlist_eff) && - (List.for_all2 type_is_comp - prov_node_exp_eff.outlist_eff body_node_exp_eff.outlist_eff) && - prov_node_exp_eff.has_mem_eff = body_node_exp_eff.has_mem_eff && - prov_node_exp_eff.is_safe_eff = body_node_exp_eff.is_safe_eff && + prov_node_exp_eff.node_key_eff <> body_node_exp_eff.node_key_eff + then + raise(Compile_error (node_def.src, msg_prefix ^ " ??? ")) + else if + (List.exists2 type_is_not_comp + prov_node_exp_eff.inlist_eff body_node_exp_eff.inlist_eff) + then + let msg = msg_prefix ^ "bad input profile. \n*** " ^ + (String.concat "*" (List.map str_of_var prov_node_exp_eff.inlist_eff)) ^ + " <> " ^ + (String.concat "*" (List.map str_of_var body_node_exp_eff.inlist_eff)) + in + raise(Compile_error (node_def.src, msg)) + else if + (List.exists2 type_is_not_comp + prov_node_exp_eff.outlist_eff body_node_exp_eff.outlist_eff) + then + let msg = msg_prefix ^ "bad output profile. \n*** " ^ + (String.concat "*" (List.map str_of_var prov_node_exp_eff.outlist_eff)) ^ + " <> " ^ + (String.concat "*" (List.map str_of_var body_node_exp_eff.outlist_eff)) + in + raise(Compile_error (node_def.src, msg)) + else if + prov_node_exp_eff.has_mem_eff <> body_node_exp_eff.has_mem_eff + then + raise(Compile_error (node_def.src, msg_prefix ^ " node or function?")) + else if + prov_node_exp_eff.is_safe_eff <> body_node_exp_eff.is_safe_eff + then + raise(Compile_error (node_def.src, msg_prefix ^ "safe or unsafe?")) + else if match prov_node_exp_eff.def_eff, body_node_exp_eff.def_eff with - | (AbstractEff,_) -> true - | (_,_) -> prov_node_exp_eff.def_eff = body_node_exp_eff.def_eff + | (AbstractEff,_) -> false + | (_,_) -> prov_node_exp_eff.def_eff <> body_node_exp_eff.def_eff then - prov_node_exp_eff + raise(Compile_error (node_def.src, msg_prefix ^ "abstract or not?")) else - raise( - Compile_error ( - node_def.src, - ("provided node \n\t" ^ - (LicDump.profile_of_node_exp_eff prov_node_exp_eff) ^ - "\n is not compatible with its implementation \n\t" ^ - (LicDump.profile_of_node_exp_eff body_node_exp_eff)))) + prov_node_exp_eff and (node_check_do: t -> CompiledData.node_key -> Lxm.t -> SymbolTab.t -> diff --git a/src/licDump.ml b/src/licDump.ml index f2a9efcf167c78a2f13d9a030995893d01b3b4ed..ba3b3262324be72fe8106614f7846ad83d039159 100644 --- a/src/licDump.ml +++ b/src/licDump.ml @@ -1,4 +1,4 @@ -(** Time-stamp: <modified the 25/08/2008 (at 10:13) by Erwan Jahier> *) +(** Time-stamp: <modified the 25/08/2008 (at 18:16) by Erwan Jahier> *) open CompiledData open Printf @@ -238,6 +238,10 @@ and (string_of_var_info_eff: var_info_eff -> string) = fun x -> (Ident.to_string x.var_name_eff) ^ ":"^(string_of_type_eff x.var_type_eff) +and (type_string_of_var_info_eff: var_info_eff -> string) = + fun x -> (string_of_type_eff x.var_type_eff) ^ + (string_of_clock2 x.var_clock_eff) + and string_of_decl var_info_eff = (Ident.to_string var_info_eff.var_name_eff) ^ ":" ^ (string_of_type_eff var_info_eff.var_type_eff) ^ diff --git a/src/licDump.mli b/src/licDump.mli index bb1e3833d23b6c2ee8697aa4b6b4f59e02a1907f..e1a50f894b0b2cba403601b3e4336834091c7987 100644 --- a/src/licDump.mli +++ b/src/licDump.mli @@ -1,4 +1,4 @@ -(** Time-stamp: <modified the 22/08/2008 (at 14:53) by Erwan Jahier> *) +(** Time-stamp: <modified the 25/08/2008 (at 18:04) by Erwan Jahier> *) open CompiledData @@ -16,6 +16,7 @@ val const_decl: Ident.long -> const_eff -> string val profile_of_node_exp_eff: node_exp_eff -> string val string_of_var_info_eff: var_info_eff -> string +val type_string_of_var_info_eff: var_info_eff -> string val string_of_slice_info_eff : slice_info_eff -> string diff --git a/src/test/should_work/NONREG/model.lus b/src/test/should_work/NONREG/model.lus new file mode 100644 index 0000000000000000000000000000000000000000..c1c4fcb01f704f8e761f27b91270b004aed0b5a4 --- /dev/null +++ b/src/test/should_work/NONREG/model.lus @@ -0,0 +1,28 @@ + +model m +needs + type elementType; + node _isEqualTo_(e1 : elementType; e2 : elementType) returns (x : bool); +provides + node est_egal(e1 : elementType; e2 : elementType) returns (x : bool); +body + + +node est_egal = _isEqualTo_; + +end + + +package u +provides + node egal(i1:int; i2:int) returns (o:bool); +body + node egal(i1:int; i2:int) returns (o:bool); + let + o = (i1 = i2); + tel + +end + + +package p = m(int, u::egal); \ No newline at end of file diff --git a/src/test/test.res.exp b/src/test/test.res.exp index 4e6244f8d38f582d48e47894f15cdc88b5b74bb5..3011281ab194d5dfb2febca02c2c039ae397c1e3 100644 --- a/src/test/test.res.exp +++ b/src/test/test.res.exp @@ -3439,6 +3439,27 @@ tel -- end of node mm3::mm3 +---------------------------------------------------------------------- +====> ../lus2lic -vl 2 --compile-all-items should_work/NONREG/model.lus +Opening file should_work/NONREG/model.lus +node u::egal(i1:int; i2:int) returns (o:bool); +let + o = (i1 = i2); +tel +-- end of node u::egal +type _p::elementType = int; +node p::_isEqualTo_(i1:int; i2:int) returns (o:bool); +let + o = (u::egal(i1, i2)); +tel +-- end of node p::_isEqualTo_ +node p::est_egal(i1:int; i2:int) returns (o:bool); +let + o = (p::_isEqualTo_(i1, i2)); +tel +-- end of node p::est_egal + + ---------------------------------------------------------------------- ====> ../lus2lic -vl 2 --compile-all-items should_work/NONREG/mouse.lus Opening file should_work/NONREG/mouse.lus