From e7ef1b901d7c38443ed30f97cea08d89af83f295 Mon Sep 17 00:00:00 2001 From: Erwan Jahier <jahier@imag.fr> Date: Tue, 26 May 2009 15:02:29 +0200 Subject: [PATCH] Attach the clock of Eff.val_exp to the val_exp itself, instead of maintaining (ugly and error-prone) hash tables. That change revealed an untriggered bug in EvalClock.check_args: it was wrong to add in subst the substitutions made of the parameters and the arguments (it is enough to unify the clocks of the pars and of the args). For instance, consider the node (in should_work/clock/clock.lus) node clock5(x : bool; y: bool when x; z: bool when y) and the call z2 = clock5(a, b when a, c when e); I was adding y/b in the subst, which was wrong. Other minor changes: - move const_to_val_eff from Eff to UnifyClock. - GetEff.translate_val_exp now returns a substitution, in order to be able to unify clock vars and propagate the resulting substitution. --- lv6-ref-man/lv6-ref-man.tex | 4 +- release-lv6/Makefile | 3 +- src/Makefile | 3 + src/TODO | 3 + src/eff.ml | 54 +------- src/evalClock.ml | 188 ++++++++------------------ src/evalClock.mli | 17 +-- src/evalType.ml | 4 +- src/getEff.ml | 131 ++++++++++-------- src/getEff.mli | 2 +- src/inline.ml | 92 ++++++------- src/lazyCompiler.ml | 10 +- src/nodesExpand.ml | 16 +-- src/predefEvalType.ml | 6 +- src/split.ml | 57 ++++---- src/structArrayExpand.ml | 43 +++--- src/test/should_work/lionel/bug.lus | 29 ++++ src/test/should_work/lionel/pack1.lus | 24 ++++ src/test/test.res.exp | 34 +++++ src/unifyClock.ml | 86 +++++++++++- src/unifyClock.mli | 8 +- src/untested_line_counter | 2 +- 22 files changed, 438 insertions(+), 378 deletions(-) create mode 100644 src/test/should_work/lionel/bug.lus create mode 100644 src/test/should_work/lionel/pack1.lus diff --git a/lv6-ref-man/lv6-ref-man.tex b/lv6-ref-man/lv6-ref-man.tex index ec3a277d..28d3ce7c 100644 --- a/lv6-ref-man/lv6-ref-man.tex +++ b/lv6-ref-man/lv6-ref-man.tex @@ -1755,8 +1755,8 @@ following command is launched: {\tt lv6 foo.lus -main p::bar}. \begin{example}[Model instance] Here is how to obtain packages by instanciating the model given in Example~\ref{model-ex}: \begin{alltt} - \kwd{package} model_instance_examble_bool \kwd{is} model_example(bool); - \kwd{package} model_instance_examble_int \kwd{is} model_example(int); + \kwd{package} model_instance_examble_bool \kwd{is} model_example(t=bool,pi=3.14); + \kwd{package} model_instance_examble_int \kwd{is} model_example(t=int,pi=3.14); \end{alltt} In this way, {\tt model\_instance\_examble\_bool} is a package that provides the node: \begin{alltt} diff --git a/release-lv6/Makefile b/release-lv6/Makefile index c67b1988..f0babc70 100644 --- a/release-lv6/Makefile +++ b/release-lv6/Makefile @@ -14,7 +14,8 @@ RELNAME=$(RELNAME_PREFIX)$(shell date +%d-%m-%y)-$(shell uname) all: dir doc lus2lic lic2c test_files dir: - (rm -rf $(RELNAME) && mkdir $(RELNAME)) || mkdir $(RELNAME) + rm -rf $(RELNAME) || true + mkdir $(RELNAME) || true cp -rf rel-skel/* $(RELNAME)/ doc: diff --git a/src/Makefile b/src/Makefile index 665f19bf..cb0d3a1d 100644 --- a/src/Makefile +++ b/src/Makefile @@ -144,6 +144,9 @@ ci: wc: wc $(SOURCES) + +dot2ps: + dot -Tps lus2lic.dot > lus2lic.dot.ps # Specific rule (version) .PHONY: version.ml diff --git a/src/TODO b/src/TODO index 1cc56706..5235040f 100644 --- a/src/TODO +++ b/src/TODO @@ -125,6 +125,9 @@ A faire * Attacher l'horloge des expressions aux expressions elle-meme, plutot que d'utiliser une hashtbl (comme pour le type). +* pourquoi Eff.true_type_of_const n'est plus utiliser et qu'aucun des tests +de non reg ne semblent avoir echouer ? + * Ne pas générer de "current", "->", "pre" (i.e., les traduire en termes de "merge" et "fby"). diff --git a/src/eff.ml b/src/eff.ml index c567b693..5283d2f7 100644 --- a/src/eff.ml +++ b/src/eff.ml @@ -1,4 +1,4 @@ -(** Time-stamp: <modified the 12/03/2009 (at 09:54) by Erwan Jahier> *) +(** Time-stamp: <modified the 13/05/2009 (at 16:04) by Erwan Jahier> *) (** @@ -169,7 +169,8 @@ and val_exp = type info, and one without. But it is a big mutually recursive thing, and doing that would be a little bit heavy... *) -(* clk : clock *) + clk : clock list + (* ditto *) } and val_exp_core = | CallByPosEff of (by_pos_op srcflagged * operands) @@ -228,9 +229,10 @@ and const = | Extern_const_eff of (Ident.long * type_) | Abstract_const_eff of (Ident.long * type_ * const * bool) (* if the abstract const is exported (i.e., defined in the provided part), - then the bool flag is set to true. + then the bool flag is set to true. Well, it is not really an abstract + constant in that case... - nb: well, are abstract constant useful at all? I don't + nb: well, are exported abstract constant useful at all? I don't know, but it is not a reason to handle them unproperly... *) | Enum_const_eff of (Ident.long * type_) @@ -504,54 +506,12 @@ let (type_of_const: const -> type_) = | Array_const_eff (ct, teff) -> Array_type_eff (teff, List.length ct) (* Ignore the abstraction layer (necessary when expanding struct) *) +(* XXX not used anymore. This is very suspect... *) let (true_type_of_const: const -> type_) = function | Abstract_const_eff (s, teff, _v, _is_exported) -> teff | teff -> type_of_const teff -let rec (const_to_val_eff: Lxm.t -> bool -> const -> val_exp) = - fun lxm expand_const const -> - let mk_by_pos_op by_pos_op_eff = - { core = CallByPosEff(flagit by_pos_op_eff lxm, OperEff []) ; - typ = [type_of_const const] ; - } - in - let id_of_int i = Ident.of_string (string_of_int i) in - match const with - | Bool_const_eff b -> - mk_by_pos_op (Predef((if b then Predef.TRUE_n else Predef.FALSE_n), [])) - | Int_const_eff i -> - mk_by_pos_op (Predef((Predef.ICONST_n (id_of_int i)),[])) - | Real_const_eff r -> - mk_by_pos_op (Predef((Predef.RCONST_n (Ident.of_string r)),[])) - | Enum_const_eff (s, _) - | Extern_const_eff (s, _) -> mk_by_pos_op (IDENT (Ident.idref_of_long s)) - - | Abstract_const_eff (s, teff, c, is_exported) -> - if expand_const - then const_to_val_eff lxm expand_const c - else mk_by_pos_op (IDENT (Ident.idref_of_long s)) - - | Array_const_eff (ct, _) -> - mk_by_pos_op (ARRAY (List.map (const_to_val_eff lxm expand_const) ct)) - - | Struct_const_eff (fl, stype) -> - let sname = match stype with - | Struct_type_eff(sname, _) -> sname - | _ -> assert false - in - let pack = Ident.pack_of_long sname in - let name_op_flg = flagit (STRUCT(pack, Ident.idref_of_long sname)) lxm in - { core = (CallByNameEff( - name_op_flg, - List.map - (fun (id,const) -> - flagit id lxm ,const_to_val_eff lxm expand_const const) - fl - )); - typ = [stype] - } - let (type_of_left: left -> type_) = function diff --git a/src/evalClock.ml b/src/evalClock.ml index 382addca..c8d27dee 100644 --- a/src/evalClock.ml +++ b/src/evalClock.ml @@ -1,4 +1,4 @@ -(** Time-stamp: <modified the 11/03/2009 (at 17:44) by Erwan Jahier> *) +(** Time-stamp: <modified the 26/05/2009 (at 10:14) by Erwan Jahier> *) open Predef @@ -75,12 +75,11 @@ open UnifyClock let (check_args : Lxm.t -> subst -> Eff.id_clock list -> Eff.id_clock list -> subst) = - fun lxm (s1,s2) cil_par cil_arg -> + fun lxm s cil_par cil_arg -> assert (List.length cil_par = List.length cil_arg); let idl_par,cil_par = List.split cil_par and idl_arg,cil_arg = List.split cil_arg in - let s = (List.combine idl_par idl_arg)@s1, s2 in - let s = List.fold_left2 (UnifyClock.f lxm) s cil_par cil_arg in + let s = List.fold_left2 (UnifyClock.f lxm) s cil_arg cil_par in s (** Checking expression result @@ -178,137 +177,65 @@ let (get_clock_profile : Eff.node_exp -> clock_profile) = let ci2str = LicDump.string_of_clock2 -(******************************************************************************) -(* We tabulate the result of the Eff.val_exp clock ckecking. Note, - that there is no clash in that table because all var_exp_eff are - srcflagged. -*) - -let val_exp_eff_clk_tab:(Eff.val_exp, Eff.id_clock list) Hashtbl.t = Hashtbl.create 0 -let tabulate_res vef clock_eff_list = -(* print_string "*** '"; *) -(* print_string (LicDump.string_of_val_exp_eff vef); *) -(* let lxm = match vef with *) -(* |CallByPosEff(op,_) -> op.src *) -(* | CallByNameEff(op,_) -> op.src *) -(* in *) -(* print_string (Lxm.details lxm); *) -(* print_string "' -> "; *) -(* print_string (String.concat "," *) -(* (List.map (fun (_,clk) -> LicDump.string_of_clock2 clk) *) -(* clock_eff_list)); *) -(* print_string "\n"; *) -(* flush stdout; *) - - Hashtbl.replace val_exp_eff_clk_tab vef clock_eff_list - -let (add : Eff.val_exp -> Eff.id_clock list -> unit) = tabulate_res -(* fun ve cl -> *) -(* Hashtbl.add val_exp_eff_clk_tab ve cl *) - -let (lookup : Eff.val_exp -> Eff.id_clock list) = - fun vef -> - try - let res = Hashtbl.find val_exp_eff_clk_tab vef in -(* let rec var_clock_to_base = function *) -(* (* Some expressions migth be infered to be a variable clock *) -(* (e.g., constants). In that case, it is ok to consider that such *) -(* expressions are on the base clock in the end (i.e., at top-level). *) -(* *) *) -(* | BaseEff -> BaseEff *) -(* | ClockVar i -> BaseEff *) -(* | On(v, clk) -> On(v, var_clock_to_base clk) *) -(* in *) - List.map (fun (id,clk) -> id, (* var_clock_to_base *) clk) res - with Not_found -> - print_string "*** No entry in clock table for the expression '"; - print_string (LicDump.string_of_val_exp_eff vef); - print_string "'\n "; - flush stdout; - assert false - -let (copy : Eff.val_exp -> Eff.val_exp -> unit) = - fun ve1 ve2 -> - let tl = lookup ve2 in - Hashtbl.add val_exp_eff_clk_tab ve1 tl - (******************************************************************************) (** Now we can go on and define [f]. *) -(* During the inner call to f_aux, some intermediary clock variables - may remain. This function tries to get rid of them using s *) -let apply_subst_to_clk_tbl s = - Hashtbl.iter - (fun ve cel -> - let cel2 = - List.map - (fun (id,clk) -> - let clk = apply_subst2 s clk in - id, clk) - cel - in - if cel <> cel2 then ( -(* let lxm = match ve with *) -(* |CallByPosEff(op,_) -> op.src *) -(* | CallByNameEff(op,_) -> op.src *) -(* in *) -(* print_string ("*** Replacing the clock of " ^ *) -(* (string_of_val_exp_eff ve) ^ " [" ^(Lxm.position lxm) *) -(* ^ "] (which was bound to " ^ *) -(* (String.concat "," *) -(* (List.map (fun (_,clk) -> string_of_clock2 clk) cel))^ *) -(* ") by " ^ *) -(* (String.concat "," *) -(* (List.map (fun (_,clk) -> string_of_clock2 clk) cel2))^ *) -(* "\n"); *) -(* flush stdout; *) - Hashtbl.replace val_exp_eff_clk_tab ve cel2 - ); - ) - val_exp_eff_clk_tab let rec (f : Lxm.t -> Eff.id_solver -> subst -> Eff.val_exp -> Eff.clock list -> - Eff.id_clock list * subst) = + Eff.val_exp * Eff.id_clock list * subst) = fun lxm id_solver s ve exp_clks -> (* we split f so that we can reinit the fresh clock var generator *) - let inf_clks, s = f_aux id_solver s ve in - let s = List.fold_left2 - (fun s eclk iclk -> UnifyClock.f lxm s eclk iclk) - s - exp_clks - (List.map (fun (_,clk) -> clk) inf_clks) - in - apply_subst_to_clk_tbl s; - inf_clks, s + let ve, inf_clks, s = f_aux id_solver s ve in + let s = + if exp_clks = [] then s else + List.fold_left2 + (fun s eclk iclk -> UnifyClock.f lxm s eclk iclk) + s + exp_clks + (List.map (fun (_,clk) -> clk) inf_clks) + in + let inf_clks = List.map (fun (id,clk) -> id, apply_subst2 s clk) inf_clks in + let clks = snd (List.split inf_clks) in + let ve = { ve with clk = clks } in + Verbose.print_string ~level:3 ( + "Clocking the expression '" ^ (LicDump.string_of_val_exp_eff ve) ^"': "^ + (LicDump.string_of_clock2 (List.hd clks)) ^"\n"); + ve, inf_clks, s and f_aux id_solver s ve = - let cel, s = - match ve.core with - | CallByPosEff ({it=posop; src=lxm}, OperEff args) -> - eval_by_pos_clock id_solver posop lxm args s - - | CallByNameEff ({it=nmop; src=lxm}, nmargs ) -> - try eval_by_name_clock id_solver nmop lxm nmargs s - with EvalConst_error msg -> - raise (Compile_error(lxm, "\n*** can't eval constant: "^msg)) - in - tabulate_res ve cel; - cel, s + let (cel, s), lxm = + match ve.core with + | CallByPosEff ({it=posop; src=lxm}, OperEff args) -> + eval_by_pos_clock id_solver posop lxm args s, lxm + + | CallByNameEff ({it=nmop; src=lxm}, nmargs ) -> + try eval_by_name_clock id_solver nmop lxm nmargs s, lxm + with EvalConst_error msg -> + raise (Compile_error(lxm, "\n*** can't eval constant: "^msg)) + in + let new_clk = snd (List.split cel) in + let s, ve = + if ve.clk = [] then (s, { ve with clk = new_clk }) else + let s = List.fold_left2 (UnifyClock.f lxm) s ve.clk new_clk in + s, ve + in + apply_subst_val_exp s ve, cel, s (* iterate f on a list of expressions *) and (f_list : Eff.id_solver -> subst -> Eff.val_exp list -> - Eff.id_clock list list * subst) = + Eff.val_exp list * Eff.id_clock list list * subst) = fun id_solver s args -> - let aux (acc,s) arg = - let cil, s = f_aux id_solver s arg in - (cil::acc, s) + let aux (args,acc,s) arg = + let arg, cil, s = f_aux id_solver s arg in + (arg::args, cil::acc, s) in - let (cil, s) = List.fold_left aux ([],s) args in + let (args, cil, s) = List.fold_left aux ([],[],s) args in + let args = List.rev args in let cil = List.rev cil in - apply_subst_to_clk_tbl s; - cil, s + let cil = List.map (List.map(fun (id,clk) -> id, apply_subst2 s clk)) cil in + args, cil, s and (eval_by_pos_clock : Eff.id_solver -> Eff.by_pos_op -> Lxm.t -> Eff.val_exp list -> subst -> Eff.id_clock list * subst) = @@ -316,7 +243,7 @@ and (eval_by_pos_clock : Eff.id_solver -> Eff.by_pos_op -> Lxm.t -> Eff.val_exp let apply_subst s (id,clk) = id, UnifyClock.apply_subst s clk in match posop,args with | Eff.CURRENT,args -> ( (* we return the clock of the argument *) - let clocks_of_args, s = f_list id_solver s args in + let _args, clocks_of_args, s = f_list id_solver s args in let current_clock = function | (id, BaseEff) -> (id, BaseEff) | (id, On(_,clk)) -> (id, clk) @@ -369,11 +296,11 @@ and (eval_by_pos_clock : Eff.id_solver -> Eff.by_pos_op -> Lxm.t -> Eff.val_exp le traitement du cas ou la liste ne contient qu'un element n'a aucun raison d'etre particulier, si ??? *) - | [[exp_clk]], s -> + | _args,[[exp_clk]], s -> let (exp_clk,s) = aux_when exp_clk s in ([exp_clk], s) - | [exp_clk_list], s -> + | _args, [exp_clk_list], s -> (* when on tuples *) let exp_clk_list, s = List.fold_left @@ -392,7 +319,9 @@ and (eval_by_pos_clock : Eff.id_solver -> Eff.by_pos_op -> Lxm.t -> Eff.val_exp | Eff.MERGE _,args -> assert false (* TODO *) (* f_aux id_solver (List.hd args) *) - | Eff.HAT(i,ve),args -> f_aux id_solver s ve + | Eff.HAT(i,ve),args -> + let (_,clk,s) = f_aux id_solver s ve in + clk,s (* nb: the args have been put inside the HAT_eff constructor *) @@ -425,7 +354,7 @@ and (eval_by_pos_clock : Eff.id_solver -> Eff.by_pos_op -> Lxm.t -> Eff.val_exp in let cil_arg = List.map (replace_base rel_base) cil_arg in let cil_res = List.map (replace_base rel_base) cil_res in - let clk_args, s = f_list id_solver s args in + let args, clk_args, s = f_list id_solver s args in let s = check_args lxm s cil_arg (List.flatten clk_args) in List.map (apply_subst s) cil_res, s @@ -435,10 +364,11 @@ and (eval_by_pos_clock : Eff.id_solver -> Eff.by_pos_op -> Lxm.t -> Eff.val_exp | Eff.ARRAY_ACCES (_),args | Eff.ARRAY_SLICE (_),args -> assert(List.length args = 1); - f_aux id_solver s (List.hd args) + let (_,clk,s) = f_aux id_solver s (List.hd args) in + clk,s | Eff.Predef (op,sargs),args -> - let clk_args, s = f_list id_solver s args in + let args, clk_args, s = f_list id_solver s args in let flat_clk_args = List.flatten clk_args in (* => mono-clock! *) let _,flat_clk_args = List.split flat_clk_args in let clk_list, s = @@ -460,7 +390,7 @@ and (eval_by_pos_clock : Eff.id_solver -> Eff.by_pos_op -> Lxm.t -> Eff.val_exp mono-clocks (i.e., when they return tuples, all elements are on the same clock). It would be sensible to have, e.g., arrows on multiple clocks. We'll refine later. *) - let clk_args, s = f_list id_solver s args in + let args, clk_args, s = f_list id_solver s args in let flat_clk_args = List.flatten clk_args in (* => mono-clock! *) let idl,flat_clk_args = List.split flat_clk_args in let clk,s = UnifyClock.list lxm flat_clk_args s in @@ -473,7 +403,9 @@ and (eval_by_pos_clock : Eff.id_solver -> Eff.by_pos_op -> Lxm.t -> Eff.val_exp in clk_list, s ) - | Eff.WITH(ve),args -> f_aux id_solver s ve + | Eff.WITH(ve),args -> + let (_,clk,s) = f_aux id_solver s ve in + clk, s @@ -487,7 +419,7 @@ and (eval_by_name_clock : Eff.id_solver -> Eff.by_name_op -> Lxm.t -> let apply_subst s (id,clk) = id, UnifyClock.apply_subst s clk in let args = List.map (fun (id,ve) -> ve) namargs in (* XXX The 3 following lines duplicates the code of TUPLE_eff and co *) - let clk_args, s = f_list id_solver s args in + let args, clk_args, s = f_list id_solver s args in let flat_clk_args = List.flatten clk_args in (* => mono-clock! *) let _,flat_clk_args = List.split flat_clk_args in let clk,s = UnifyClock.list lxm flat_clk_args s in diff --git a/src/evalClock.mli b/src/evalClock.mli index 6de00355..8c49f40d 100644 --- a/src/evalClock.mli +++ b/src/evalClock.mli @@ -1,14 +1,14 @@ -(** Time-stamp: <modified the 05/03/2009 (at 10:16) by Erwan Jahier> *) +(** Time-stamp: <modified the 13/05/2009 (at 15:22) by Erwan Jahier> *) open UnifyClock -(** [f ids ve] checks that [ve] is well-clocked (i.e., for node calls, +(** [f lxm ids s ve cl] checks that [ve] is well-clocked (i.e., for node calls, it checks that the argument and the parameter clocks are compatible), and returns a clock profile that contains all the necessary information - to be able to check. + so that the caller can perform additional clock checks. *) val f : Lxm.t -> Eff.id_solver -> subst -> Eff.val_exp -> Eff.clock list -> - Eff.id_clock list * subst + Eff.val_exp * Eff.id_clock list * subst (** [check_res lxm cel cil] checks that the expected output clock @@ -26,12 +26,3 @@ val f : Lxm.t -> Eff.id_solver -> subst -> Eff.val_exp -> Eff.clock list -> val check_res : Lxm.t -> subst -> Eff.left list -> Eff.id_clock list -> unit - -(* Returns the clock of an expression. Note that this function uses - an internal table, and therefore it should not be called before - the clock checking has been done (by the function f above).*) -val lookup : Eff.val_exp -> Eff.id_clock list -val add : Eff.val_exp -> Eff.id_clock list -> unit - -(* [copy ve1 ve2] declares that ve1 has the same clock than ve2 *) -val copy : Eff.val_exp -> Eff.val_exp -> unit diff --git a/src/evalType.ml b/src/evalType.ml index f8f7b503..e0d12d1e 100644 --- a/src/evalType.ml +++ b/src/evalType.ml @@ -1,4 +1,4 @@ -(** Time-stamp: <modified the 11/03/2009 (at 17:44) by Erwan Jahier> *) +(** Time-stamp: <modified the 12/03/2009 (at 14:03) by Erwan Jahier> *) open Predef @@ -41,7 +41,7 @@ let rec (f : Eff.id_solver -> Eff.val_exp -> Eff.val_exp * Eff.type_ list) = in CallByNameEff ({it=nmop; src=lxm}, nmargs ), tl in - { core = ve_core; typ = tl}, tl + { core = ve_core; typ = tl ; clk = ve.clk }, tl and (eval_by_pos_type : Eff.id_solver -> Eff.by_pos_op -> Lxm.t -> diff --git a/src/getEff.ml b/src/getEff.ml index d48da298..f128a272 100644 --- a/src/getEff.ml +++ b/src/getEff.ml @@ -1,4 +1,4 @@ -(** Time-stamp: <modified the 11/03/2009 (at 17:45) by Erwan Jahier> *) +(** Time-stamp: <modified the 26/05/2009 (at 15:27) by Erwan Jahier> *) open Lxm @@ -92,14 +92,12 @@ and (type_check_equation: Eff.id_solver -> Lxm.t -> Eff.left list -> right_part (* Checks that the left part has the same clock as the right one. *) -and (clock_check_equation:Eff.id_solver -> Lxm.t -> Eff.left list -> - Eff.val_exp -> unit) = - fun id_solver lxm lpl_eff ve_eff -> +and (clock_check_equation:Eff.id_solver -> Lxm.t -> UnifyClock.subst -> + Eff.left list -> Eff.val_exp -> unit) = + fun id_solver lxm s lpl_eff ve_eff -> let clk_list = List.map Eff.clock_of_left lpl_eff in - let right_part,s = - EvalClock.f lxm id_solver UnifyClock.empty_subst ve_eff clk_list - in - EvalClock.check_res lxm s lpl_eff right_part + let _, right_part_clks, s = EvalClock.f lxm id_solver s ve_eff clk_list in + EvalClock.check_res lxm s lpl_eff right_part_clks (******************************************************************************) @@ -120,8 +118,7 @@ let (dump_polymorphic_nodes : Eff.type_ -> unit) = output_string !Global.oc str ) nodes; - Polymorphism.reset_type () - + Polymorphism.reset_type () (******************************************************************************) let (get_static_params_from_idref : SymbolTab.t -> Lxm.t -> Ident.idref -> @@ -296,10 +293,10 @@ and (eq:Eff.id_solver -> SyntaxTreeCore.eq_info srcflagged -> Eff.eq_info srcfla fun id_solver eq_info -> let (lpl, ve) = eq_info.it in let lpl_eff = List.map (translate_left_part id_solver) lpl - and ve_eff = translate_val_exp id_solver ve + and clk_subst,ve_eff = translate_val_exp id_solver UnifyClock.empty_subst ve in type_check_equation id_solver eq_info.src lpl_eff ve_eff; - clock_check_equation id_solver eq_info.src lpl_eff ve_eff; + clock_check_equation id_solver eq_info.src clk_subst lpl_eff ve_eff; flagit (lpl_eff, ve_eff) eq_info.src @@ -349,23 +346,42 @@ and (translate_left_part : id_solver -> SyntaxTreeCore.left_part -> Eff.left) = ) -and (translate_val_exp : Eff.id_solver -> SyntaxTreeCore.val_exp -> Eff.val_exp) = - fun id_solver ve -> - let vef_core = +and (translate_val_exp : Eff.id_solver -> UnifyClock.subst -> + SyntaxTreeCore.val_exp -> UnifyClock.subst * Eff.val_exp) = + fun id_solver s ve -> + let s, vef_core, lxm = match ve with | CallByName(by_name_op, field_list) -> + let s,fl = List.fold_left + (fun (s,fl) f -> + let s,f = translate_field id_solver s f in + s,f::fl + ) + (s,[]) + field_list + in + let fl = List.rev fl in + s, (CallByNameEff( - flagit (translate_by_name_op id_solver by_name_op) by_name_op.src, - List.map (translate_field id_solver) field_list)) + flagit (translate_by_name_op id_solver by_name_op) by_name_op.src, fl)), + by_name_op.src | CallByPos(by_pos_op, Oper vel) -> - let vel_eff = List.map (translate_val_exp id_solver) vel in + let s, vel_eff = + List.fold_left + (fun (s,vel) ve -> + let s, ve = translate_val_exp id_solver s ve in + s,ve::vel + ) + (s,[]) vel + in + let vel_eff = List.rev vel_eff in let lxm = by_pos_op.src in let by_pos_op = by_pos_op.it in let mk_by_pos_op by_pos_op_eff = CallByPosEff(flagit by_pos_op_eff lxm, OperEff vel_eff) in - let vef_core = + let s, vef_core = match by_pos_op with (* put that in another module ? yes, see above.*) | Predef_n(Map, sargs) @@ -393,6 +409,9 @@ and (translate_val_exp : Eff.id_solver -> SyntaxTreeCore.val_exp -> Eff.val_exp) in let type_l_exp = snd (List.split (fst iter_profile)) in let sargs_eff = + if List.length type_l <> List.length type_l_exp then + raise (Compile_error(lxm, "the iterator has a wrong arity.")) + else match UnifyType.f type_l type_l_exp with | UnifyType.Equal -> sargs_eff | UnifyType.Unif typ -> @@ -404,24 +423,24 @@ and (translate_val_exp : Eff.id_solver -> SyntaxTreeCore.val_exp -> Eff.val_exp) | UnifyType.Ko str -> raise (Compile_error(lxm, str)) in - mk_by_pos_op (Eff.Predef(iter_op, sargs_eff)) + s, mk_by_pos_op (Eff.Predef(iter_op, sargs_eff)) (* other predef operators *) | Predef_n(op, args) -> - assert (args=[]); mk_by_pos_op(Predef (op,[])) + assert (args=[]); s, mk_by_pos_op(Predef (op,[])) | CALL_n node_exp_f -> - mk_by_pos_op(Eff.CALL (flagit (node id_solver node_exp_f) + s, mk_by_pos_op(Eff.CALL (flagit (node id_solver node_exp_f) node_exp_f.src)) | IDENT_n idref -> ( try - let const = - Eff.const_to_val_eff lxm false (id_solver.id2const idref lxm) + let s, const = UnifyClock.const_to_val_eff lxm false s + (id_solver.id2const idref lxm) in - const.core - with _ -> (* It migth not be a static constant... *) + s, const.core + with _ -> (* In case idref is not a static constant. *) match Ident.pack_of_idref idref with - | Some pn -> mk_by_pos_op(Eff.IDENT idref) + | Some pn -> s, mk_by_pos_op(Eff.IDENT idref) (** Constant with a pack name are treated as Eff.IDENT. *) | None -> @@ -432,41 +451,44 @@ and (translate_val_exp : Eff.id_solver -> SyntaxTreeCore.val_exp -> Eff.val_exp) SymbolTab.find_pack_of_const id_solver.symbols id lxm in let idref = Ident.make_idref pn id in - mk_by_pos_op(Eff.IDENT (idref)) + s, mk_by_pos_op(Eff.IDENT (idref)) with _ -> - mk_by_pos_op(Eff.IDENT idref) + s, mk_by_pos_op(Eff.IDENT idref) ) - | CURRENT_n -> mk_by_pos_op Eff.CURRENT - | PRE_n -> mk_by_pos_op Eff.PRE + | CURRENT_n -> s, mk_by_pos_op Eff.CURRENT + | PRE_n -> s, mk_by_pos_op Eff.PRE - | ARROW_n -> mk_by_pos_op Eff.ARROW - | FBY_n -> mk_by_pos_op Eff.FBY - | CONCAT_n -> mk_by_pos_op Eff.CONCAT - | TUPLE_n -> mk_by_pos_op Eff.TUPLE + | ARROW_n -> s, mk_by_pos_op Eff.ARROW + | FBY_n -> s, mk_by_pos_op Eff.FBY + | CONCAT_n -> s, mk_by_pos_op Eff.CONCAT + | TUPLE_n -> s, mk_by_pos_op Eff.TUPLE | ARRAY_n -> - CallByPosEff(flagit (Eff.ARRAY vel_eff) lxm, OperEff []) + s, CallByPosEff(flagit (Eff.ARRAY vel_eff) lxm, OperEff []) | WITH_n(c,e1,e2) -> let c_eff = EvalConst.f id_solver c in if c_eff = [ Bool_const_eff true ] then - mk_by_pos_op (Eff.WITH (translate_val_exp id_solver e1)) + let s, ve1 = translate_val_exp id_solver s e1 in + s, mk_by_pos_op (Eff.WITH (ve1)) else - mk_by_pos_op (Eff.WITH (translate_val_exp id_solver e2)) + let s, ve2 = translate_val_exp id_solver s e2 in + s, mk_by_pos_op (Eff.WITH (ve2)) | STRUCT_ACCESS_n fid -> - mk_by_pos_op (Eff.STRUCT_ACCESS (fid)) + s, mk_by_pos_op (Eff.STRUCT_ACCESS (fid)) - | WHEN_n Base -> mk_by_pos_op (Eff.WHEN Base) + | WHEN_n Base -> s, mk_by_pos_op (Eff.WHEN Base) | WHEN_n (NamedClock { it = (cc,cv) ; src = lxm }) -> let cc = add_pack_name id_solver lxm cc in - mk_by_pos_op (Eff.WHEN (NamedClock { it = (cc,cv) ; src = lxm })) + s, + mk_by_pos_op (Eff.WHEN (NamedClock { it = (cc,cv) ; src = lxm })) | ARRAY_ACCES_n ve_index -> - mk_by_pos_op ( + s, mk_by_pos_op ( Eff.ARRAY_ACCES( EvalConst.eval_array_index id_solver ve_index lxm)) | ARRAY_SLICE_n si -> - mk_by_pos_op + s, mk_by_pos_op (Eff.ARRAY_SLICE( EvalConst.eval_array_slice id_solver si lxm)) @@ -474,20 +496,21 @@ and (translate_val_exp : Eff.id_solver -> SyntaxTreeCore.val_exp -> Eff.val_exp) match vel with | [exp; ve_size] -> let size_const_eff = EvalConst.f id_solver ve_size - and exp_eff = translate_val_exp id_solver exp in + and s, exp_eff = translate_val_exp id_solver s exp in (match size_const_eff with | [Int_const_eff size] -> - mk_by_pos_op (Eff.HAT(size, exp_eff)) + s, mk_by_pos_op (Eff.HAT(size, exp_eff)) | _ -> assert false) | _ -> assert false ) - | MERGE_n(id, idl) -> mk_by_pos_op (Eff.MERGE(id, idl)) + | MERGE_n(id, idl) -> s, mk_by_pos_op (Eff.MERGE(id, idl)) in - vef_core + s, vef_core, lxm in - let vef, tl = EvalType.f id_solver { core=vef_core;typ=[] } in - vef + let vef, tl = EvalType.f id_solver { core=vef_core; typ=[]; clk = [] } in + let vef, _, s = EvalClock.f lxm id_solver s vef [] in + s, vef and translate_by_name_op id_solver op = match op.it with @@ -501,7 +524,9 @@ and translate_by_name_op id_solver op = STRUCT (pn, idref) | Some pn -> STRUCT (pn, idref) -and translate_field id_solver (id, ve) = (id, translate_val_exp id_solver ve) +and translate_field id_solver s (id, ve) = + let s, ve = translate_val_exp id_solver s ve in + s, (id, ve) (* XXX autre nom, autre module ? ca fait partie de la definition des iterateurs d'une certaine maniere... @@ -690,7 +715,7 @@ and (translate_slice_info : Eff.id_solver -> SyntaxTreeCore.slice_info -> let (assertion : Eff.id_solver -> SyntaxTreeCore.val_exp Lxm.srcflagged -> Eff.val_exp Lxm.srcflagged) = fun id_solver vef -> - let val_exp_eff = translate_val_exp id_solver vef.it in + let s, val_exp_eff = translate_val_exp id_solver UnifyClock.empty_subst vef.it in (* Check that the assert is a bool. *) let val_exp_eff, evaled_exp = EvalType.f id_solver val_exp_eff in List.iter @@ -706,8 +731,8 @@ let (assertion : Eff.id_solver -> SyntaxTreeCore.val_exp Lxm.srcflagged -> (* type is ok *) (* Clock check the assertion*) - let clock_eff_list, _s = - EvalClock.f vef.src id_solver UnifyClock.empty_subst val_exp_eff [BaseEff] + let _, clock_eff_list, _s = + EvalClock.f vef.src id_solver s val_exp_eff [BaseEff] in match clock_eff_list with | [id, BaseEff] diff --git a/src/getEff.mli b/src/getEff.mli index b396988b..01832639 100644 --- a/src/getEff.mli +++ b/src/getEff.mli @@ -1,4 +1,4 @@ -(** Time-stamp: <modified the 12/03/2009 (at 09:17) by Erwan Jahier> *) +(** Time-stamp: <modified the 12/03/2009 (at 11:14) by Erwan Jahier> *) (** This module defines functions that translate SyntaxTreeCore datatypes into diff --git a/src/inline.ml b/src/inline.ml index e46b0414..5cc0e4b3 100644 --- a/src/inline.ml +++ b/src/inline.ml @@ -1,4 +1,4 @@ -(** Time-stamp: <modified the 12/03/2009 (at 10:23) by Erwan Jahier> *) +(** Time-stamp: <modified the 13/05/2009 (at 16:35) by Erwan Jahier> *) open Lxm @@ -15,7 +15,7 @@ let new_var str node_env type_eff clock_eff = var_number_eff = -1; (* this field is used only for i/o. Should i rather put something sensible there ? *) var_type_eff = type_eff; - var_clock_eff = clock_eff; + var_clock_eff = id, clock_eff; } in Hashtbl.add node_env.lenv_vars id var; @@ -65,7 +65,7 @@ let (check_clock_and_type : type inline_acc = (Eff.eq_info srcflagged) list * Eff.var_info list let rec (inline_eq: Eff.local_env -> - Eff.id_solver -> inline_acc -> Eff.eq_info srcflagged -> inline_acc) = + Eff.id_solver -> inline_acc -> Eff.eq_info srcflagged -> inline_acc) = fun node_env id_solver (eqs, locs) eq -> let { src = lxm_eq ; it = (lhs, rhs) } = eq in match rhs.core with @@ -111,19 +111,18 @@ let rec (inline_eq: Eff.local_env -> let op_flg = { src = lxm_ve ; it = ARRAY_ACCES(i) } in let narg = { core = CallByPosEff(op_flg, OperEff [arg]); - typ = [t_elt] + typ = [t_elt]; + clk = arg.clk } in - EvalClock.copy narg arg; narg ) args in let nrhs = { rhs with core = - CallByPosEff({ src = lxm_ve ; it = (CALL node)}, OperEff args) } + CallByPosEff({ src = lxm_ve ; it = (CALL node)}, OperEff args) } in let eq = { src = lxm_eq ; it = (lhs, nrhs) } in - EvalClock.copy nrhs rhs; (eq::eqs,locs) ) (eqs,locs) @@ -156,7 +155,7 @@ let rec (inline_eq: Eff.local_env -> <=> exists acc_0, ..., acc_c-1, where acc_o=acc_in, and acc_c-1=acc_out such that, for all i = 0, ..., c-1; - (acc_i+1, Y1[i], ... ,Yl[i]) = N(acc_i,X_1[i], ... ,X_k[i]) + (acc_i+1, Y1[i], ... ,Yl[i]) = N(acc_i,X_1[i], ... ,X_k[i]) *) let ((node,_,_),c) = match sargs with | [ConstStaticArgEff(_,Int_const_eff(c)) ; NodeStaticArgEff(_,node)] @@ -174,7 +173,7 @@ let rec (inline_eq: Eff.local_env -> let args = List.tl args in let type_exp,clock_exp = List.hd (acc_in.typ), - List.hd (EvalClock.lookup acc_in) + List.hd (acc_in.clk) in let (acc_vars : var_info list) = let rec f i acc = @@ -195,9 +194,9 @@ let rec (inline_eq: Eff.local_env -> let op_flg = { src = lxm_ve ; it = IDENT id } in let ve = { typ = [vi.var_type_eff]; + clk = [snd vi.var_clock_eff]; core = CallByPosEff(op_flg, OperEff []) } in - EvalClock.add ve [vi.var_clock_eff]; ve ) acc_vars) @@ -211,10 +210,12 @@ let rec (inline_eq: Eff.local_env -> let t_elt = elt_type_of_array arg.typ in let op_flg = {src = lxm_ve ; it = ARRAY_ACCES(i)} in let new_arg = - { core = CallByPosEff(op_flg, OperEff [arg]); typ=[t_elt] } + { core = CallByPosEff(op_flg, OperEff [arg]); + typ=[t_elt]; + clk=[clock_exp]; + } in - EvalClock.add new_arg [clock_exp]; - new_arg + new_arg ) args in @@ -233,12 +234,10 @@ let rec (inline_eq: Eff.local_env -> in let rhs = { typ = tl; + clk = List.map snd cl; core = CallByPosEff({src=lxm_ve;it = (CALL node)}, OperEff args) } in - let eq = - EvalClock.add rhs cl; - { src = lxm_eq ; it = (lhs, rhs) } - in + let eq = { src = lxm_eq ; it = (lhs, rhs) } in eq ) index_list @@ -255,7 +254,7 @@ let rec (inline_eq: Eff.local_env -> (* a diese is a particular kind of boolred: #(A,...,an) = boolred(1,1,n)([a1,...,an]) *) - let clk = EvalClock.lookup rhs in + let clk = rhs.clk in let n = List.length args in let sargs = [ConstStaticArgEff(Ident.of_string "i",Int_const_eff 1); ConstStaticArgEff(Ident.of_string "j",Int_const_eff 1); @@ -265,15 +264,15 @@ let rec (inline_eq: Eff.local_env -> let boolred_op = Eff.Predef(Predef.BoolRed,sargs) in let arg = { typ = [Array_type_eff(Bool_type_eff,n) ]; + clk = clk; core = CallByPosEff({src=lxm_ve;it= ARRAY args}, OperEff [])} in let rhs = { typ = [Bool_type_eff]; + clk = clk; core = CallByPosEff({src=lxm_ve;it=boolred_op}, OperEff [arg]) } in let eq = { src = lxm_eq ; it = (lhs, rhs) } in - EvalClock.add arg clk; - EvalClock.add rhs clk; - inline_eq node_env id_solver (eqs, locs) eq + inline_eq node_env id_solver (eqs, locs) eq | CallByPosEff( {src=lxm_ve;it=CALL ({it = {node_key_eff = (("Lustre", "nor"),_)}})}, @@ -282,7 +281,7 @@ let rec (inline_eq: Eff.local_env -> (* a nor is a particular kind of boolred too: #(A,...,an) = boolred(0,0,n)([a1,...,an]) *) - let clk = EvalClock.lookup rhs in + let clk = rhs.clk in let n = List.length args in let sargs = [ConstStaticArgEff(Ident.of_string "i",Int_const_eff 0); ConstStaticArgEff(Ident.of_string "j",Int_const_eff 0); @@ -292,16 +291,16 @@ let rec (inline_eq: Eff.local_env -> let boolred_op = Eff.Predef(Predef.BoolRed,sargs) in let arg = { typ = [Array_type_eff(Bool_type_eff,n) ]; + clk = clk; core = CallByPosEff({src=lxm_ve;it=ARRAY args}, OperEff []) } in let rhs = { typ = [Bool_type_eff]; + clk = clk; core = CallByPosEff({src=lxm_ve;it=boolred_op}, OperEff [arg]) } in let eq = { src = lxm_eq ; it = (lhs, rhs) } in - EvalClock.add arg clk; - EvalClock.add rhs clk; - inline_eq node_env id_solver (eqs, locs) eq + inline_eq node_env id_solver (eqs, locs) eq | CallByPosEff({src=lxm_ve;it=CALL ( {it = {node_key_eff = (("Lustre", "boolred"),sargs)}})}, @@ -313,11 +312,11 @@ let rec (inline_eq: Eff.local_env -> and res = boolred<<i,j,k>>(A); - <=> + <=> cpt = (if A[0] then 1 else 0) + ... + (if A[k-1] then 1 else 0); res = i <= cpt && cpt <= j; *) - let rhs_clk = EvalClock.lookup rhs in + let rhs_clk = rhs.clk in let (i,j,k) = match sargs with | [ConstStaticArgEff(_,Int_const_eff i); @@ -330,7 +329,7 @@ let rec (inline_eq: Eff.local_env -> let index_list = fill 0 k in let lp = try List.hd lhs with Not_found -> assert false in let res_clock = (Eff.var_info_of_left lp).var_clock_eff in - let cpt = new_var "cpt" node_env Int_type_eff res_clock in + let cpt = new_var "cpt" node_env Int_type_eff (snd res_clock) in let id_of_int i = Predef.ICONST_n(Ident.of_string (string_of_int i)) in let rhs = (* i <= cpt && cpt <= j; *) let i_op = { it = Predef(id_of_int i,[]) ; src = lxm_ve } @@ -338,22 +337,19 @@ let rec (inline_eq: Eff.local_env -> and cpt_op = { it = IDENT (Ident.to_idref cpt.var_name_eff);src=lxm_ve } and and_op = { it = Predef(Predef.AND_n,[]) ; src = lxm_ve } and inf_op = { it = Predef(Predef.LTE_n,[]) ; src = lxm_ve } in - let i_eff = { typ = [Int_type_eff]; core = CallByPosEff(i_op, OperEff []) } - and j_eff = { typ = [Int_type_eff]; core = CallByPosEff(j_op, OperEff [])} - and cpt_eff = { typ = [Int_type_eff]; core = CallByPosEff(cpt_op, OperEff []) } + let i_eff = { clk=rhs_clk; typ = [Int_type_eff]; core = CallByPosEff(i_op, OperEff []) } + and j_eff = { clk=rhs_clk; typ = [Int_type_eff]; core = CallByPosEff(j_op, OperEff [])} + and cpt_eff = { clk=rhs_clk; typ = [Int_type_eff]; core = CallByPosEff(cpt_op, OperEff []) } in - let i_inf_cpt = { typ = [Bool_type_eff]; + let i_inf_cpt = { clk=rhs_clk; typ = [Bool_type_eff]; core = CallByPosEff(inf_op,OperEff[i_eff;cpt_eff]) } - and cpt_if_j = { typ = [Bool_type_eff]; + and cpt_if_j = { clk=rhs_clk; typ = [Bool_type_eff]; core = CallByPosEff(inf_op,OperEff[cpt_eff;j_eff]) } in - EvalClock.add i_inf_cpt rhs_clk; - EvalClock.add cpt_if_j rhs_clk; - { typ = [Bool_type_eff]; - core = CallByPosEff(and_op, OperEff [i_inf_cpt; cpt_if_j]) } + { clk=rhs_clk; typ = [Bool_type_eff]; + core = CallByPosEff(and_op, OperEff [i_inf_cpt; cpt_if_j]) } in let eq = - EvalClock.add rhs rhs_clk; check_clock_and_type id_solver lxm_eq rhs Bool_type_eff res_clock; { src = lxm_eq ; it = (lhs, rhs) } in @@ -361,42 +357,38 @@ let rec (inline_eq: Eff.local_env -> let lhs = [LeftVarEff(cpt,lxm_ve)] in (* (if A[0] then 1 else 0) + ... + (if A[k-1] then 1 else 0) *) let zero = { - typ = [Int_type_eff]; + clk = rhs_clk; typ = [Int_type_eff]; core = CallByPosEff({it=Predef(id_of_int 0,[]);src=lxm_ve},OperEff[])} and one = { + clk = rhs_clk; typ = [Int_type_eff]; core = CallByPosEff({it=Predef(id_of_int 1,[]);src=lxm_ve},OperEff[]) } and plus_op = { it = Predef(Predef.IPLUS_n,[]) ; src = lxm_ve } and ite_op = { it = Predef(Predef.IF_n,[]) ; src = lxm_ve } in let array, type_elt = - EvalClock.add zero rhs_clk; - EvalClock.add one rhs_clk; match args with | [arg] -> arg,elt_type_of_array arg.typ | _ -> assert false in let make_ite i = (* returns '(if A[i] then 1 else 0)' *) let a_op = { it = ARRAY_ACCES(i) ; src = lxm_ve } in - let a_i = { typ = [type_elt]; + let a_i = { clk = rhs_clk; typ = [type_elt]; core = CallByPosEff(a_op, OperEff [array]) } in let nve = { - typ = [Int_type_eff]; - core = CallByPosEff(ite_op, OperEff [a_i;one;zero]) } + clk=rhs_clk; typ = [Int_type_eff]; + core = CallByPosEff(ite_op, OperEff [a_i;one;zero]) } in - EvalClock.add a_i rhs_clk; - EvalClock.add nve rhs_clk; - nve + nve in let rhs = List.fold_left (fun acc i -> let nve = { - typ = [Int_type_eff]; + clk=rhs_clk; typ = [Int_type_eff]; core = CallByPosEff(plus_op, OperEff [acc; make_ite i]) } in - EvalClock.add nve rhs_clk; nve ) (make_ite (List.hd index_list)) @@ -419,7 +411,7 @@ let rec (inline_eq: Eff.local_env -> | _ -> (eq::eqs, locs) - + (* exported *) diff --git a/src/lazyCompiler.ml b/src/lazyCompiler.ml index fd73920d..1c97b1d8 100644 --- a/src/lazyCompiler.ml +++ b/src/lazyCompiler.ml @@ -1,4 +1,4 @@ -(** Time-stamp: <modified the 12/03/2009 (at 09:55) by Erwan Jahier> *) +(** Time-stamp: <modified the 13/05/2009 (at 16:36) by Erwan Jahier> *) open Lxm @@ -856,6 +856,7 @@ and (node_check_do: t -> Eff.node_key -> Lxm.t -> SymbolTab.t -> and vol = List.map2 instanciate_var_info aliased_node.outlist_eff ol_decl in let (outs:Eff.left list) = List.map (fun vi -> LeftVarEff (vi, lxm)) vol in let tl = List.map Eff.type_of_left outs in + let cl = List.map (fun l -> (Eff.var_info_of_left l).var_clock_eff) outs in let (aliased_node_call : Eff.val_exp) = { core = CallByPosEff( @@ -865,19 +866,18 @@ and (node_check_do: t -> Eff.node_key -> Lxm.t -> SymbolTab.t -> (fun vi -> (* build operands*) let ve = { typ = [vi.var_type_eff]; + clk = [snd vi.var_clock_eff]; core = CallByPosEff( Lxm.flagit (Eff.IDENT( Ident.to_idref vi.var_name_eff)) lxm, OperEff [])} in - EvalClock.add ve [vi.var_clock_eff]; ve ) vil))); - typ = tl + typ = tl; + clk = List.map snd cl; } in - let cl = List.map (fun l -> (Eff.var_info_of_left l).var_clock_eff) outs in - EvalClock.add aliased_node_call cl; { aliased_node with node_key_eff = nk; diff --git a/src/nodesExpand.ml b/src/nodesExpand.ml index a1e11226..68f9ec69 100644 --- a/src/nodesExpand.ml +++ b/src/nodesExpand.ml @@ -1,4 +1,4 @@ -(** Time-stamp: <modified the 12/03/2009 (at 10:43) by Erwan Jahier> *) +(** Time-stamp: <modified the 13/05/2009 (at 16:24) by Erwan Jahier> *) (** nb : only user nodes are expanded. @@ -114,7 +114,6 @@ let rec (substitute : fun s { it = (lhs,ve) ; src = lxm } -> let lhs = List.map (subst_in_left s) lhs in let newve = subst_in_val_exp s ve in - EvalClock.copy newve ve; { it = (lhs,newve) ; src = lxm } and subst_in_left s left = @@ -166,7 +165,6 @@ and (subst_in_val_exp : subst -> val_exp -> val_exp) = CallByNameEff(by_name_op, fl) } in - EvalClock.copy newve ve; newve let mk_loc_subst = List.combine @@ -216,13 +214,11 @@ let (mk_output_subst : Eff.local_env -> Lxm.t -> var_info list -> Eff.left list let nv_idref = Ident.to_idref nv.var_name_eff in let nve = { core = CallByPosEff({it=IDENT nv_idref;src = lxm },OperEff []); - typ = [nv.var_type_eff] + typ = [nv.var_type_eff]; + clk = [snd nv.var_clock_eff] } in - let neq = - EvalClock.add nve [nv.var_clock_eff]; - [left], nve - in + let neq = [left], nve in let neq = flagit neq lxm in (* for equations of the form x.field = n(...); @@ -295,10 +291,10 @@ and (expand_assert : Eff.local_env -> acc -> val_exp srcflagged -> acc) = let assert_op = Eff.IDENT(Ident.to_idref assert_var.var_name_eff) in let nve = { core = CallByPosEff((Lxm.flagit assert_op lxm, OperEff [])); - typ = [Bool_type_eff] + typ = [Bool_type_eff]; + clk = [BaseEff] } in - EvalClock.copy nve ve; expand_eq n_env ((Lxm.flagit nve lxm)::a_acc, e_acc, assert_var::v_acc) assert_eq diff --git a/src/predefEvalType.ml b/src/predefEvalType.ml index 0b0f43c7..136e94e8 100644 --- a/src/predefEvalType.ml +++ b/src/predefEvalType.ml @@ -1,4 +1,4 @@ -(** Time-stamp: <modified the 04/03/2009 (at 14:15) by Erwan Jahier> *) +(** Time-stamp: <modified the 26/05/2009 (at 15:34) by Erwan Jahier> *) open Predef open Lxm @@ -81,8 +81,8 @@ let (get_node_and_constant: Lxm.t -> match sargs with | [NodeStaticArgEff(_,(n, inlist, outlist)); ConstStaticArgEff(_,Int_const_eff c)] -> n, inlist, outlist, c - | [NodeStaticArgEff(_,(n, inlist, outlist)); - ConstStaticArgEff(_, const)] -> + + | [NodeStaticArgEff(_,(n, inlist, outlist)); ConstStaticArgEff(_, const)] -> let msg = "an integer is expected, whereas a " ^ (LicDump.string_of_type_eff4msg (Eff.type_of_const const)) ^ " was provided.\n" diff --git a/src/split.ml b/src/split.ml index 8b775722..af7000a6 100644 --- a/src/split.ml +++ b/src/split.ml @@ -1,4 +1,4 @@ -(** Time-stamp: <modified the 12/03/2009 (at 10:26) by Erwan Jahier> *) +(** Time-stamp: <modified the 19/05/2009 (at 15:43) by Erwan Jahier> *) open Lxm @@ -16,7 +16,7 @@ let new_var node_env type_eff clock_eff = var_number_eff = -1; (* this field is used only for i/o. Should i rather put something sensible there ? *) var_type_eff = type_eff; - var_clock_eff = clock_eff; + var_clock_eff = id,clock_eff; } in Hashtbl.add node_env.lenv_vars id var; @@ -57,7 +57,8 @@ let (break_it : val_exp -> val_exp list) = { core = CallByPosEff({it=Eff.Predef(Predef.IF_n,[]);src=lxm}, OperEff [c;ve1;ve2]); - typ = ve1.typ + typ = ve1.typ; + clk = ve1.clk; } ) vel1 @@ -92,7 +93,8 @@ let (break_it : val_exp -> val_exp list) = List.map2 (fun ve1 ve2 -> { core = CallByPosEff({it=op ; src=lxm }, OperEff [ve1;ve2]); - typ = ve1.typ } + typ = ve1.typ; + clk = ve1.clk } ) vel1 vel2 @@ -100,10 +102,9 @@ let (break_it : val_exp -> val_exp list) = | _ -> assert false (* dead code since it is guarded by to_be_broken... *) in let tl = ve.typ - and cl = EvalClock.lookup ve in - let nvel = List.map2 (fun nve t -> { nve with typ = [t] } ) nvel ve.typ in + and cl = ve.clk in + let nvel = List.map2 (fun nve t -> { nve with typ = [t]; clk=cl } ) nvel ve.typ in assert(ve.typ = tl); - List.iter2 (fun c nve -> EvalClock.add nve [c]) cl nvel; nvel let (split_tuples:Eff.eq_info Lxm.srcflagged list -> Eff.eq_info Lxm.srcflagged list) = @@ -148,17 +149,16 @@ and (split_eq_acc : and (split_val_exp : bool -> bool -> Eff.local_env -> Eff.val_exp -> Eff.val_exp * split_acc) = fun when_flag top_level node_env ve -> - (* when_flag is true is the call is made from a "when" statement. + (* [when_flag] is true is the call is made from a "when" statement. We need this flag in order to know if it is necessary to add - a when on constants. Indeed, in Lustre, it is not necessary - to write " 1 when clk + x " if x in on clk (its more sweet). + a when on constants. Indeed, in Lustre V6, it is not necessary + to write " 1 when clk + x " if x in on clk (it's more sweet). So we need to add it (because if we split "1+1+x", then it - is hard to know the "1" are on the clock of x). + is hard to know the "1" are on the clock of x ; moreover, lustre + v4 (and the other backends) cannot infer such clock). But is is not forbidden either! so we need to make sure that there is no "when"... - - *) match ve.core with | CallByPosEff({it=Eff.IDENT _}, _) -> ve, ([],[]) @@ -171,8 +171,8 @@ and (split_val_exp : bool -> bool -> Eff.local_env -> Eff.val_exp -> but *) -> if not when_flag then - let clk = EvalClock.lookup ve in - match snd (List.hd clk) with + let clk = ve.clk in + match (List.hd clk) with | On(clock,_) -> let clk_exp = SyntaxTreeCore.NamedClock (Lxm.flagit clock lxm) in { ve with core = @@ -185,7 +185,7 @@ and (split_val_exp : bool -> bool -> Eff.local_env -> Eff.val_exp -> ve, ([],[]) | CallByNameEff (by_name_op_eff, fl) -> - let lxm = by_name_op_eff.src in + let lxm = by_name_op_eff.src in let fl, eql, vl = List.fold_left (fun (fl_acc, eql_acc, vl_acc) (fn, fv) -> @@ -195,13 +195,15 @@ and (split_val_exp : bool -> bool -> Eff.local_env -> Eff.val_exp -> ([],[],[]) fl in - let rhs = { ve with core = CallByNameEff (by_name_op_eff, List.rev fl) } in - EvalClock.copy rhs ve; + let rhs = { ve with + core = CallByNameEff (by_name_op_eff, List.rev fl) + } + in if top_level then rhs, (eql, vl) else (* create the var for the current call *) - let clk_l = EvalClock.lookup ve in + let clk_l = ve.clk in let typ_l = ve.typ in let nv_l = List.map2 (new_var node_env) typ_l clk_l in let nve = match nv_l with @@ -214,8 +216,7 @@ and (split_val_exp : bool -> bool -> Eff.local_env -> Eff.val_exp -> in let lpl = List.map (fun nv -> LeftVarEff(nv, lxm)) nv_l in let eq = Lxm.flagit (lpl, rhs) lxm in - EvalClock.copy nve ve; - nve, (eql@[eq], vl@nv_l) + nve, (eql@[eq], vl@nv_l) | CallByPosEff(by_pos_op_eff, OperEff vel) -> (* recursively split the arguments *) @@ -254,12 +255,11 @@ and (split_val_exp : bool -> bool -> Eff.local_env -> Eff.val_exp -> rhs, (eql, vl) in let rhs = { ve with core = rhs } in - EvalClock.copy rhs ve; - if top_level || by_pos_op_eff.it = TUPLE then + if top_level || by_pos_op_eff.it = TUPLE then rhs, (eql, vl) else (* create the var for the current call *) - let clk_l = EvalClock.lookup ve in + let clk_l = ve.clk in let typ_l = ve.typ in let nv_l = List.map2 (new_var node_env) typ_l clk_l in @@ -267,12 +267,14 @@ and (split_val_exp : bool -> bool -> Eff.local_env -> Eff.val_exp -> match nv_l with | [nv] -> { typ = [nv.var_type_eff]; + clk = clk_l; core = CallByPosEff( Lxm.flagit (Eff.IDENT (Ident.to_idref nv.var_name_eff)) lxm, OperEff []) } | _ -> { typ = List.map (fun v -> v.var_type_eff) nv_l; + clk = clk_l; core = CallByPosEff( Lxm.flagit Eff.TUPLE lxm, OperEff @@ -283,10 +285,10 @@ and (split_val_exp : bool -> bool -> Eff.local_env -> Eff.val_exp -> (Lxm.flagit (Eff.IDENT (Ident.to_idref nv.var_name_eff)) lxm, OperEff []); - typ = [nv.var_type_eff] + typ = [nv.var_type_eff]; + clk = [snd nv.var_clock_eff] } in - EvalClock.add nnv [nv.var_clock_eff]; nnv ) nv_l @@ -296,8 +298,7 @@ and (split_val_exp : bool -> bool -> Eff.local_env -> Eff.val_exp -> in let lpl = List.map (fun nv -> LeftVarEff(nv, lxm)) nv_l in let eq = Lxm.flagit (lpl, rhs) lxm in - EvalClock.copy nve ve; - nve, (eql@[eq], vl@nv_l) + nve, (eql@[eq], vl@nv_l) and (split_val_exp_list : bool -> diff --git a/src/structArrayExpand.ml b/src/structArrayExpand.ml index b3c15316..e2e898d0 100644 --- a/src/structArrayExpand.ml +++ b/src/structArrayExpand.ml @@ -1,4 +1,4 @@ -(** Time-stamp: <modified the 12/03/2009 (at 10:24) by Erwan Jahier> *) +(** Time-stamp: <modified the 13/05/2009 (at 16:16) by Erwan Jahier> *) (* Replace structures and arrays by as many variables as necessary. Since structures can be recursive, it migth be a lot of new variables... @@ -49,7 +49,7 @@ let new_var str node_env type_eff clock_eff = var_number_eff = -1; (* this field is used only for i/o. Should i rather put something sensible there ? *) var_type_eff = type_eff; - var_clock_eff = clock_eff; + var_clock_eff = id, clock_eff; } in Hashtbl.add node_env.lenv_vars id var; @@ -215,7 +215,7 @@ let rec (make_new_loc : Eff.local_env -> Eff.id_solver -> Lxm.t -> acc -> Eff.val_exp -> acc * var_info) = fun nenv id_solver lxm acc ve -> let teff = List.hd ve.typ in - let ceff = List.hd (EvalClock.lookup ve) in + let ceff = List.hd ve.clk in let nv = new_var "v" nenv teff ceff in let neq = [LeftVarEff(nv,lxm)], ve in let neq = flagit neq lxm in @@ -230,7 +230,8 @@ and (var_trees_of_val_exp : Eff.local_env -> Eff.id_solver -> acc -> Eff.val_exp let prefix = (Ident.to_string vi.var_name_eff) ^ prefix in let idref = Ident.idref_of_string prefix in { core = CallByPosEff({src=lxm;it=(IDENT idref)}, OperEff []); - typ = [vi.var_type_eff] } + typ = [vi.var_type_eff] ; + clk = [snd vi.var_clock_eff] } in let loop = var_trees_of_val_exp nenv id_solver acc in match ve.core with @@ -265,7 +266,6 @@ and (var_trees_of_val_exp : Eff.local_env -> Eff.id_solver -> acc -> Eff.val_exp (acc, gen_var_trees (make_val_exp nenv lxm vi) "" vi.var_type_eff) with _ -> - let const = try id_solver.id2const idref lxm with _ -> let msg = @@ -279,10 +279,8 @@ and (var_trees_of_val_exp : Eff.local_env -> Eff.id_solver -> acc -> Eff.val_exp in raise (Errors.Compile_error(lxm, msg)) in - let ceff = EvalClock.lookup ve in - let ve_const = Eff.const_to_val_eff lxm true const in - let _ = - EvalClock.add ve_const ceff; + let s, ve_const = + UnifyClock.const_to_val_eff lxm true UnifyClock.empty_subst const in let ve_const,acc = match ve_const.core with @@ -378,8 +376,9 @@ and (break_tuple : Lxm.t -> left list -> val_exp -> Eff.eq_info srcflagged list) else List.map2 (fun l ve -> - EvalClock.add ve [(Eff.var_info_of_left l).var_clock_eff]; - { src = lxm ; it = ([l], { ve with typ = [Eff.type_of_left l]}) } + let clk = [snd (Eff.var_info_of_left l).var_clock_eff] in + { src = lxm ; + it = ([l], { ve with typ = [Eff.type_of_left l] ; clk = clk}) } ) left_list vel @@ -444,9 +443,9 @@ and (expand_val_exp: Eff.local_env -> Eff.id_solver -> acc -> val_exp -> in let newve = CallByPosEff(Lxm.flagit by_pos_op lxm, OperEff vel) in let newve = { ve with core = newve } in - if newve <> ve then ( - EvalClock.copy newve ve - ); +(* if newve.core <> ve.core then ( *) +(* EvalClock.copy newve ve *) +(* ); *) newve, acc | CallByNameEff(by_name_op, fl_val) -> @@ -454,7 +453,6 @@ and (expand_val_exp: Eff.local_env -> Eff.id_solver -> acc -> val_exp -> Moreover, we have to deal with default value. *) let teff = ve.typ in - let ceff = EvalClock.lookup ve in match teff with | [Struct_type_eff(_,fl)] -> let lxm = by_name_op.src in @@ -470,11 +468,9 @@ and (expand_val_exp: Eff.local_env -> Eff.id_solver -> acc -> val_exp -> | None -> assert false (* ougth to have been checked before *) | Some const -> - let ve_const = - Eff.const_to_val_eff lxm true const - in - let _ = - EvalClock.add ve_const ceff; + let s, ve_const = (* XXX *) + UnifyClock.const_to_val_eff lxm true + UnifyClock.empty_subst const in let ve_const,acc= expand_val_exp n_env id_solver acc ve_const @@ -486,12 +482,13 @@ and (expand_val_exp: Eff.local_env -> Eff.id_solver -> acc -> val_exp -> in let newve = { typ = ve.typ; + clk = ve.clk; core=CallByPosEff({ src=lxm ; it=TUPLE }, OperEff (List.rev vel)) } in - if newve <> ve then ( - EvalClock.copy newve ve - ); +(* if newve.core <> ve.core then ( *) +(* EvalClock.copy newve ve *) +(* ); *) newve, acc | _ -> assert false diff --git a/src/test/should_work/lionel/bug.lus b/src/test/should_work/lionel/bug.lus new file mode 100644 index 00000000..5b8bf7cd --- /dev/null +++ b/src/test/should_work/lionel/bug.lus @@ -0,0 +1,29 @@ +package bug +uses pack1; + +provides + +node system(ck1 : bool) returns (out : int); + +body + +node system(ck1 : bool) returns (out : int); +var + ckout : bool; + out1 : int when ck1; +-- out2 : int when ckout; +let + (out1, ckout) = n1(ck1); +-- out2 = n2(ckout, out1); + out = current(out1); +tel + +node n1bis(ck : bool^pack1::toto) returns (ckout : bool^pack1::toto); +var cpt : int; +let + cpt = 0 -> pre(cpt)+1; + ckout = map<<Lustre::not, pack1::toto>>(ck); + +tel + +end \ No newline at end of file diff --git a/src/test/should_work/lionel/pack1.lus b/src/test/should_work/lionel/pack1.lus new file mode 100644 index 00000000..9c4ecc1c --- /dev/null +++ b/src/test/should_work/lionel/pack1.lus @@ -0,0 +1,24 @@ +package pack1 + +provides +node n1(ck : bool) returns (out : int when ck; ckout : bool); +node n2(ck : bool; in : int) returns (out : int when ck); +const toto: int =3; + +body + +const toto: int =3; +node n1(ck : bool) returns (out : int when ck; ckout : bool); +var cpt : int; +let + cpt = 0 -> pre(cpt)+1; + out = cpt when ck; + ckout = ck; +tel + +node n2(ck : bool; in : int) returns (out : int when ck); +let + out = in when ck; +tel + +end \ No newline at end of file diff --git a/src/test/test.res.exp b/src/test/test.res.exp index c90f1995..d0b31223 100644 --- a/src/test/test.res.exp +++ b/src/test/test.res.exp @@ -17372,6 +17372,15 @@ type A_A_bool_4_3 = A_bool_4^3; type A_int_4 = int^4; type A_A_int_4_3 = A_int_4^3; type A_A_int_4_3 = A_int_4^3; +---------------------------------------------------------------------- +====> ../lus2lic -vl 2 should_work/lionel/bug.lus +Opening file should_work/lionel/bug.lus +-- ../lus2lic -vl 2 should_work/lionel/bug.lus + +*** Error in file "should_work/lionel/bug.lus", line 2, col 6 to 10, token 'pack1': +*** unknown package + + ---------------------------------------------------------------------- ====> ../lus2lic -vl 2 should_work/lionel/calculs_max.lus Opening file should_work/lionel/calculs_max.lus @@ -18326,6 +18335,31 @@ type A__normal::T_InfoGenIndiv_4 = _normal::T_InfoGenIndiv^4; type A__normal::T_InfoChgGlob_20 = _normal::T_InfoChgGlob^20; type A_A_int_20_4 = A_int_20^4; type A_int_20 = int^20; +---------------------------------------------------------------------- +====> ../lus2lic -vl 2 should_work/lionel/pack1.lus +Opening file should_work/lionel/pack1.lus +-- ../lus2lic -vl 2 should_work/lionel/pack1.lus + +const pack1::toto = 3; +node pack1::n1(ck:bool) returns (out:int when ck; ckout:bool); +var + cpt:int; + _v1:int; + _v2:int; +let + cpt = 0 -> _v2; + _v1 = pre (cpt); + _v2 = _v1 + 1; + out = cpt when ck; + ckout = ck; +tel +-- end of node pack1::n1 +node pack1::n2(ck:bool; in:int) returns (out:int when ck); +let + out = in when ck; +tel +-- end of node pack1::n2 + ---------------------------------------------------------------------- ====> ../lus2lic -vl 2 should_work/lionel/pilote-1.0.lus Opening file should_work/lionel/pilote-1.0.lus diff --git a/src/unifyClock.ml b/src/unifyClock.ml index d3cea2cf..c8c6ebed 100644 --- a/src/unifyClock.ml +++ b/src/unifyClock.ml @@ -1,4 +1,4 @@ -(** Time-stamp: <modified the 09/03/2009 (at 16:11) by Erwan Jahier> *) +(** Time-stamp: <modified the 25/05/2009 (at 17:13) by Erwan Jahier> *) open LicDump @@ -163,12 +163,6 @@ let (new_clock_var : subst -> subst * Eff.clock) = (s1, s2), clk -(* exported *) -let (reset_clock_var : subst -> subst) = - fun (s1, s2) -> (s1, empty_subst2) - - - (* exported *) let rec (apply_subst:subst -> Eff.clock -> Eff.clock) = fun (s1,s2) c -> @@ -198,6 +192,22 @@ let rec (apply_subst2:subst -> Eff.clock -> Eff.clock) = | Some clk -> apply_subst2 (s1,s2) clk | None -> c +let rec (apply_subst_val_exp : subst -> Eff.val_exp -> Eff.val_exp) = + fun s ve -> + let ve_core = + match ve.core with + | CallByPosEff (by_pos_op, OperEff vel) -> + let vel = List.map (apply_subst_val_exp s) vel in + CallByPosEff (by_pos_op, OperEff vel) + | CallByNameEff(by_name_op, fl) -> + let fl = List.map + (fun (fn,ve) -> (fn, apply_subst_val_exp s ve)) fl + in + CallByNameEff(by_name_op, fl) + in + let new_clk = List.map (apply_subst s) ve.clk in + let ve = { ve with core = ve_core ; clk = new_clk } in + ve let is_clock_var = function @@ -259,3 +269,65 @@ let (list : Lxm.t -> Eff.clock list -> subst -> Eff.clock * subst) = ) (List.hd cl, s) (List.tl cl) +(******************************************************************************) +(* exported *) +let rec (const_to_val_eff: Lxm.t -> bool -> subst -> const -> subst * val_exp) = + fun lxm expand_const s const -> + let mk_by_pos_op by_pos_op_eff = + let s, clk = new_clock_var s in + { core = CallByPosEff(flagit by_pos_op_eff lxm, OperEff []) ; + typ = [type_of_const const] ; + clk = [clk]; + } + in + let id_of_int i = Ident.of_string (string_of_int i) in + match const with + | Bool_const_eff b -> + s, mk_by_pos_op (Predef((if b then Predef.TRUE_n else Predef.FALSE_n), [])) + | Int_const_eff i -> + s, mk_by_pos_op (Predef((Predef.ICONST_n (id_of_int i)),[])) + | Real_const_eff r -> + s, mk_by_pos_op (Predef((Predef.RCONST_n (Ident.of_string r)),[])) + | Enum_const_eff (l, _) + | Extern_const_eff (l, _) -> s, mk_by_pos_op (IDENT (Ident.idref_of_long l)) + + | Abstract_const_eff (l, teff, c, is_exported) -> + if expand_const + then const_to_val_eff lxm expand_const s c + else s, mk_by_pos_op (IDENT (Ident.idref_of_long l)) + + | Array_const_eff (ct, _) -> + let s, vel = + List.fold_left + (fun (s,vel) c -> + let s,ve = const_to_val_eff lxm expand_const s c in + (s,ve::vel) + ) + (s,[]) + ct + in + let vel = List.rev vel in + s, mk_by_pos_op (ARRAY vel) + + | Struct_const_eff (fl, stype) -> + let sname = match stype with + | Struct_type_eff(sname, _) -> sname + | _ -> assert false + in + let pack = Ident.pack_of_long sname in + let name_op_flg = flagit (STRUCT(pack, Ident.idref_of_long sname)) lxm in + + let s, fl = + List.fold_left + (fun (s,fl) (id,const) -> + let s, ve = const_to_val_eff lxm expand_const s const in + s, (flagit id lxm, ve)::fl + ) + (s,[]) + fl + in + let fl = List.rev fl in + s, { core = (CallByNameEff(name_op_flg, fl)); + typ = [stype] ; + clk = [BaseEff] + } diff --git a/src/unifyClock.mli b/src/unifyClock.mli index ff1aa24d..02e99516 100644 --- a/src/unifyClock.mli +++ b/src/unifyClock.mli @@ -1,4 +1,4 @@ -(** Time-stamp: <modified the 09/03/2009 (at 15:20) by Erwan Jahier> *) +(** Time-stamp: <modified the 19/05/2009 (at 17:32) by Erwan Jahier> *) (* XXX use Map.t @@ -39,12 +39,12 @@ val apply_subst2:subst -> Eff.clock -> Eff.clock val add_subst2 : int -> Eff.clock -> subst2 -> subst2 val add_link2 : int -> int -> subst2 -> subst2 +val apply_subst_val_exp : subst -> Eff.val_exp -> Eff.val_exp + (** Raises a Compile_error is the 2 Eff.clock are not unifiable *) val f : Lxm.t -> subst -> Eff.clock -> Eff.clock -> subst val list : Lxm.t -> Eff.clock list -> subst -> Eff.clock * subst - - val new_clock_var : subst -> subst * Eff.clock -val reset_clock_var : subst -> subst +val const_to_val_eff: Lxm.t -> bool -> subst -> Eff.const -> subst * Eff.val_exp diff --git a/src/untested_line_counter b/src/untested_line_counter index d46f8dbe..576b4f31 100644 --- a/src/untested_line_counter +++ b/src/untested_line_counter @@ -1 +1 @@ -389 / 1584 = 24.55 % +702 / 2128 = 32.98 % -- GitLab