diff --git a/lv6-ref-man/lv6-ref-man.tex b/lv6-ref-man/lv6-ref-man.tex index e403fd9c9ad39f653f090dff4b6c892b1212428a..8f0a22d44eeddbf1f054a8eadab2d8278f62bc5d 100644 --- a/lv6-ref-man/lv6-ref-man.tex +++ b/lv6-ref-man/lv6-ref-man.tex @@ -1474,7 +1474,7 @@ For any integer constant {\tt n} and any node {\tt N} of type:\\ $\tau\times\tau_1\times\ldots\times\tau_k \rightarrow \tau\times\theta_1\times\ldots\times\theta_\ell$, }\\ -\verb'map<<N; n>>' denotes a node of type:\\ +where $k$ and $\ell \geq 0$; \verb'fillred<<N; n>>' denotes a node of type:\\ \centerline{ $\tau\times\tau_1\power n\times\ldots\times\tau_k\power n \rightarrow \tau\times\theta_1\power n\times\ldots\times\theta_\ell\power n$ @@ -1482,8 +1482,8 @@ $\tau\times\tau_1\power n\times\ldots\times\tau_k\power n \rightarrow such that\\ \centerline{ \tt (a$_{out}$,Y$_1$,$\cdots$,Y$_\ell$) = -map<<N; n>>(a$_{in}$,X$_1$,$\cdots$,X$_k$)} -if and only if, $\exists \prg{a}_0, \cdots \prg{a}_n$ such that +fillred<<N; n>>(a$_{in}$,X$_1$,$\cdots$,X$_k$)} +if and only if, $\exists \prg{a}_0, \cdots, \prg{a}_n$ such that $\prg{a}_0 = \prg{a}_{in}$, $\prg{a}_n = \prg{a}_{out}$, and\\ \centerline{ $\forall i = 0 \cdots \mbox{\tt n}-1$, @@ -1492,9 +1492,11 @@ $\forall i = 0 \cdots \mbox{\tt n}-1$, \end{defi} \noindent -\erwan{ montrer comment les autres iterateurs se reecrivent en terme - de fillred (si c'est pas trop compliqué).. pas si facile en fait. plus precisement, -c'est impossible dans le cas général, pas trop dur pour chaque cas } +\erwan{en fait, une fois que fillred est definit, qu'elle +est l'interet de fill et de red ???? + +D'ailleurs, dans lus2lis et dans lic2loc, j'appelle la même fonction +dans les 3 cas ...} \begin{example}[\fillredop] diff --git a/src/Makefile b/src/Makefile index a7a4cdb327886e6a7243a699aeb28b5897e83591..fb1d7d91a14374c7c7690213eda772fd3162296b 100644 --- a/src/Makefile +++ b/src/Makefile @@ -54,6 +54,8 @@ SOURCES = \ ./getEff.ml \ ./uniqueOutput.mli \ ./uniqueOutput.ml \ + ./inline.mli \ + ./inline.ml \ ./split.mli \ ./split.ml \ ./lazyCompiler.ml \ diff --git a/src/TODO b/src/TODO index 0af0b138996800b0db3891bd73ab407536775604..e67d0f290b259d0af84696245021916e510b61d7 100644 --- a/src/TODO +++ b/src/TODO @@ -144,6 +144,14 @@ n'est pas le cas pour l'instant... cf [solve_ident] termes de "merge" et "fby"). +* l'unesting des iterateurs devrait etre fait dans split, et pas dans +LicDump. D'abord par soucis d'élégance. Mais aussi parce que sinon, +ca rend complement impossible l'inlining de ces itérateurs imbriqués. + +En plus, finalement, ca n'a pas l'air si dur: il suffit d'étendre le type +split_acc pour y rajouter une liste de definitions de noeud, qui contiendrait +des definitions d'alias. ces noueds peuvent etre contruit en mimiquant +LicDump.dump_node_alias. *** facile ---------- @@ -258,7 +266,7 @@ du code mort ou bien des tests * le merge -* dependance checking +* dependance checking (lic2loc le fait ; faut-il le faire en amont ? ) ex : a=b; b=a; diff --git a/src/evalClock.ml b/src/evalClock.ml index c27d5ffc5a92a4c6084ff77da5c20bd5db9f9727..fdbbb18da5eb17d1aeea21b11d1d118473492d90 100644 --- a/src/evalClock.ml +++ b/src/evalClock.ml @@ -1,4 +1,4 @@ -(** Time-stamp: <modified the 27/10/2008 (at 10:19) by Erwan Jahier> *) +(** Time-stamp: <modified the 20/11/2008 (at 12:06) by Erwan Jahier> *) open Predef @@ -197,7 +197,7 @@ let (get_val_exp_eff : Eff.val_exp -> Eff.id_clock list) = in List.map (fun (id,clk) -> id, var_clock_to_base clk) res with _ -> - print_string "*** No entry for '"; + print_string "*** No entry in clock table for the expression '"; print_string (LicDump.string_of_val_exp_eff vef); print_string "'\n "; flush stdout; diff --git a/src/evalType.ml b/src/evalType.ml index 45f1c7de8fdd2e269e0458693752ab79fe8ae50e..0e225901cbc5d832091f5e1e56d2c767b4605319 100644 --- a/src/evalType.ml +++ b/src/evalType.ml @@ -1,4 +1,4 @@ -(** Time-stamp: <modified the 04/11/2008 (at 16:57) by Erwan Jahier> *) +(** Time-stamp: <modified the 20/11/2008 (at 13:45) by Erwan Jahier> *) open Predef @@ -25,7 +25,25 @@ let tabulate_res val_exp_eff type_eff_list = let (val_exp_eff : Eff.val_exp -> Eff.type_ list) = fun vef -> try Hashtbl.find val_exp_eff_type_tab vef - with _ -> assert false + with _ -> + let lxm = + match vef with + | CallByPosEff(op,_) -> op.src + | CallByNameEff(op,_) -> op.src + in + print_string ( + "*** " ^(Lxm.details lxm) ^ " can not find the exp " ^ + (LicDump.string_of_val_exp_eff vef) ^ " in the table \n\t" ^ + (if Verbose.get_level() <= 2 then "" else + (Hashtbl.fold + (fun ve t acc -> (LicDump.string_of_val_exp_eff ve) ^ "\n\t"^acc) + val_exp_eff_type_tab + "\n" + ) + )); + flush stdout; + assert false + (******************************************************************************) diff --git a/src/global.ml b/src/global.ml index 4cdc7ff92a95a2b048f9377f6efff53e90d7b7cf..95f848ad87781f8269e6323a5e50f118978b6d4b 100644 --- a/src/global.ml +++ b/src/global.ml @@ -1,4 +1,4 @@ -(** Time-stamp: <modified the 14/08/2008 (at 15:31) by Erwan Jahier> *) +(** Time-stamp: <modified the 20/11/2008 (at 13:43) by Erwan Jahier> *) (** Some global variables. @@ -16,6 +16,7 @@ let main_node = ref "" let compile_all_items = ref false let run_unit_test = ref false let one_op_per_equation = ref true +let inline_iterator = ref false (* the output channel *) let oc = ref Pervasives.stdout diff --git a/src/inline.ml b/src/inline.ml new file mode 100644 index 0000000000000000000000000000000000000000..a9f3ea8578c91844720e9ed783ff05729d9cb919 --- /dev/null +++ b/src/inline.ml @@ -0,0 +1,230 @@ +(** Time-stamp: <modified the 20/11/2008 (at 13:37) by Erwan Jahier> *) + + +open Lxm +open Eff + +(********************************************************************************) +(* stuff to create fresh var names. *) +let var_cpt = ref 0 +let new_var node_env type_eff clock_eff = + incr var_cpt; + let id = Ident.of_string ("_acc" ^ (string_of_int !var_cpt)) in + let var = + { + var_name_eff = id; + var_nature_eff = SyntaxTreeCore.VarLocal; + 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; + } + in + Hashtbl.add node_env.lenv_vars id var; + var + + +let init_var () = + var_cpt := 0 + +(********************************************************************************) +(* A small util function followed by a quick unit test. *) +let rec fill i size = if i >= size then [] else i::(fill (i+1) size) +let _ = assert (fill 0 5 = [0;1;2;3;4]) + +let (elt_type_of_array : Eff.type_ list -> Eff.type_) = + function + | [Array_type_eff(t, _)] -> t + | _ -> assert false (* it ougth to be an array... *) + +let rec (list_map3: + ('a -> 'b -> 'c -> 'd) -> 'a list -> 'b list -> 'c list -> 'd list) = + fun f l1 l2 l3 -> + match (l1, l2, l3) with + | ([], [], []) -> [] + | (e1::t1, e2::t2, e3::t3) -> (f e1 e2 e3)::(list_map3 f t1 t2 t3) + | _ -> (* should not occur *) + print_string "*** list_map3 called with lists of different size.\n"; + flush stdout; + assert false + + +(********************************************************************************) +(* The functions below accumulate + (1) the new equations + (2) the fresh variables. +*) +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) = + fun node_env id_solver (eqs, locs) eq -> + let { src = lxm_eq ; it = (lhs, rhs) } = eq in + match rhs with + | CallByPosEff({src=lxm_ve;it=Eff.Predef(Predef.Map, sargs)}, OperEff args) + -> + (* Given + - a node n of type: tau_1 * ... * tau_n -> teta_1 * ... * teta_l + - and an integer c + + The profile of map<<node,c>> is: + tau_1^c * ... * tau_n^c -> teta_1^c * ... * teta_l^c + and + + Y1, ... ,Yl = map<<node; c>>(X1,...,Xk) + <=> + for all i = 0, ..., c-1; (Y1[i], ... ,Yl[i]) = N(X_1[i], ... ,X_k[i]) + *) + let (node,c) = match sargs with + | [ConstStaticArgEff(_,Int_const_eff(c)) ; NodeStaticArgEff(_,node)] + | [NodeStaticArgEff(_,node) ; ConstStaticArgEff(_,Int_const_eff(c))] -> + node, c + | _ -> assert false (* todo: issue an error *) + in + let node = { it = node ; src = lxm_ve } in + let index_list = fill 0 c in + List.fold_left + (fun (eqs,locs) i -> + let lhs = List.map + (fun lp -> + let t_elt = elt_type_of_array [type_of_left lp] in + LeftArrayEff(lp, i, t_elt)) + lhs + in + let args = + List.map + (fun arg -> + let t_elt = elt_type_of_array (EvalType.f id_solver arg) in + let op_flg = { src = lxm_ve ; it = ARRAY_ACCES(i,t_elt) } in + CallByPosEff(op_flg, OperEff [arg])) + args + in + let rhs = + CallByPosEff({ src = lxm_ve ; it = (CALL node)}, OperEff args) + in + let eq = { src = lxm_eq ; it = (lhs, rhs) } in + (eq::eqs,locs) + ) + (eqs,locs) + index_list + + | CallByPosEff({src=lxm_ve;it=Eff.Predef(Predef.Fill, sargs)}, OperEff args) + | CallByPosEff({src=lxm_ve;it=Eff.Predef(Predef.Red, sargs)}, OperEff args) + | CallByPosEff({src=lxm_ve;it=Eff.Predef(Predef.FillRed,sargs)}, OperEff args) + -> + (* Given + - a node n of type + tau * tau_1 * ... * tau_n -> tau * teta_1 * ... * teta_l + - a integer c + + the fillred expression has the profile: + tau * tau_1^c * ... * tau_n^c -> tau * teta_1^c * ... * teta_l^c + + acc_out, Y1, ... ,Yl = fillred<<node; c>>(acc_in,X1,...,Xk) + <=> + 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]) + *) + let (node,c) = match sargs with + | [ConstStaticArgEff(_,Int_const_eff(c)) ; NodeStaticArgEff(_,node)] + | [NodeStaticArgEff(_,node) ; ConstStaticArgEff(_,Int_const_eff(c))] -> + node, c + | _ -> assert false (* todo: issue an error *) + in + let node = { it = node ; src = lxm_ve } in + let index_list = fill 0 c in + (* Retreive acc_in and acc_out *) + let acc_out = List.hd lhs in + let lhs = List.tl lhs in + let acc_in = List.hd args in + let args = List.tl args in + + let _ = EvalClock.f id_solver UnifyClock.empty_subst acc_in in + let type_exp,clock_exp = + List.hd (EvalType.f id_solver acc_in), + (ignore (EvalClock.f id_solver UnifyClock.empty_subst acc_in); + List.hd (EvalClock.get_val_exp_eff acc_in)) + in + let (acc_vars : var_info list) = + let rec f i acc = + if i = 0 then acc else + f (i-1) ((new_var node_env type_exp clock_exp)::acc) + in + (* coquetry: reverse the list to have the name in a nice order *) + List.rev(f (c-1) []) + in + let (acc_left_list : left list) = + (List.map (fun vi -> LeftVarEff(vi,lxm_ve)) acc_vars)@[acc_out] + in + let (acc_rigth_list : val_exp list) = + acc_in::( + List.map + (fun vi -> + let id = Ident.to_idref vi.var_name_eff in + let op_flg = { src = lxm_ve ; it = IDENT id } in + CallByPosEff(op_flg, OperEff [])) + acc_vars) + in + let neqs = + list_map3 + (fun i acc_left acc_rigth -> + + let args = + List.map + (fun arg -> + let t_elt = elt_type_of_array (EvalType.f id_solver arg) in + let op_flg = {src = lxm_ve ; it = ARRAY_ACCES(i,t_elt)} in + CallByPosEff(op_flg, OperEff [arg]) + ) + args + in + let args = acc_rigth::args in + let lhs = + List.map + (fun lp -> + let t_elt = elt_type_of_array [type_of_left lp] in + LeftArrayEff(lp,i,t_elt)) + lhs + in + let lhs = acc_left::lhs in + let rhs = + CallByPosEff({ src = lxm_ve ; it = (CALL node)}, OperEff args) + in + let eq = { src = lxm_eq ; it = (lhs, rhs) } in + eq + ) + index_list + acc_left_list + acc_rigth_list + in + + (List.rev_append neqs eqs, acc_vars@locs) + +(* | CallByPosEff({src=lxm_ve;it=Eff.Predef(Predef.BoolRed,sargs)}, OperEff args) *) + | _ -> + (eq::eqs, locs) + + + + +(* exported *) +let (iterators : Eff.local_env -> Eff.id_solver -> Eff.node_exp -> Eff.node_exp) = + fun node_env id_solver n -> + match n.def_eff with + | ExternEff + | AbstractEff -> n + | BodyEff b -> + init_var (); + let loc = match n.loclist_eff with None -> [] | Some l -> l in + let (neqs, nv) = + List.fold_left (inline_eq node_env id_solver) ([], loc) b.eqs_eff + in + let nb = { b with eqs_eff = List.rev neqs } in + let res = + { n with + loclist_eff = Some nv; + def_eff = BodyEff nb + } + in + res diff --git a/src/inline.mli b/src/inline.mli new file mode 100644 index 0000000000000000000000000000000000000000..0f2e46a62bfcd458b9990a6be391f403a2f85c80 --- /dev/null +++ b/src/inline.mli @@ -0,0 +1,10 @@ +(** Time-stamp: <modified the 20/11/2008 (at 13:44) by Erwan Jahier> *) + + +(** Inline iterators + + The node local_env is provided so that we can update its table, as + we add some fresh local variables during the code transmation. + +*) +val iterators : Eff.local_env -> Eff.id_solver -> Eff.node_exp -> Eff.node_exp diff --git a/src/lazyCompiler.ml b/src/lazyCompiler.ml index 6db5163e74e87b0e2a7b223f0654484c4fe67802..3281998dbdacec4886491c5f47bb5062289bfa1f 100644 --- a/src/lazyCompiler.ml +++ b/src/lazyCompiler.ml @@ -1,4 +1,4 @@ -(** Time-stamp: <modified the 11/09/2008 (at 16:22) by Erwan Jahier> *) +(** Time-stamp: <modified the 20/11/2008 (at 11:21) by Erwan Jahier> *) open Lxm @@ -785,7 +785,12 @@ and (node_check_do: t -> Eff.node_key -> Lxm.t -> SymbolTab.t -> alias_node ) in - let res = if !Global.one_op_per_equation then Split.node res else res in + let res = if !Global.one_op_per_equation then Split.node local_env res else res in + let res = + if !Global.inline_iterator + then Inline.iterators local_env node_id_solver res + else res + in if not provide_flag then output_string !Global.oc (LicDump.node_of_node_exp_eff res); UniqueOutput.check res node_def.src; diff --git a/src/main.ml b/src/main.ml index 61254dd577e5e3f9ec2981059b9e05516830b3b6..01c0a1e66ca93c95526d6f316545008126602f4f 100644 --- a/src/main.ml +++ b/src/main.ml @@ -1,4 +1,4 @@ -(** Time-stamp: <modified the 23/10/2008 (at 11:32) by Erwan Jahier> *) +(** Time-stamp: <modified the 19/11/2008 (at 15:45) by Erwan Jahier> *) (** Here follows a description of the different modules used by this lus2lic compiler. @@ -102,6 +102,9 @@ let rec arg_list = [ "\tKeep nested calls" ); + ( "--inline-iterators", Arg.Unit (fun _ -> Global.inline_iterator := true), + "\tInline iterators" + ); ("-h", Arg.Unit (fun _ -> (Arg.usage arg_list usage_msg; exit 0)), "" ); ("-help", Arg.Unit (fun _ -> (Arg.usage arg_list usage_msg; exit 0)),"" ); diff --git a/src/split.ml b/src/split.ml index 796121e1f13ffac95a2f1c74f884d56ff89b0ea7..8bc4d349d13c7e78ccf1d79b425dcd9f0594c76b 100644 --- a/src/split.ml +++ b/src/split.ml @@ -1,4 +1,4 @@ -(** Time-stamp: <modified the 04/11/2008 (at 16:59) by Erwan Jahier> *) +(** Time-stamp: <modified the 20/11/2008 (at 10:47) by Erwan Jahier> *) open Lxm @@ -7,17 +7,21 @@ open Eff (********************************************************************************) (* stuff to create fresh var names. *) let var_cpt = ref 0 -let new_var type_eff clock_eff = +let new_var node_env type_eff clock_eff = incr var_cpt; - { - var_name_eff = Ident.of_string ("_v" ^ (string_of_int !var_cpt)); - var_nature_eff = SyntaxTreeCore.VarLocal; - 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; - } - + let id = Ident.of_string ("_v" ^ (string_of_int !var_cpt)) in + let var = + { + var_name_eff = id; + var_nature_eff = SyntaxTreeCore.VarLocal; + 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; + } + in + Hashtbl.add node_env.lenv_vars id var; + var let init_var () = var_cpt := 0 @@ -114,19 +118,20 @@ let (split_tuples:Eff.eq_info Lxm.srcflagged list -> Eff.eq_info Lxm.srcflagged *) type split_acc = (Eff.eq_info srcflagged) list * Eff.var_info list -let rec (split_eq : split_acc -> Eff.eq_info srcflagged -> split_acc) = - fun (eqs, locs) eq -> - let (neqs, nlocs) = split_eq_do eq in +let rec (split_eq : + Eff.local_env -> split_acc -> Eff.eq_info srcflagged -> split_acc) = + fun node_env (eqs, locs) eq -> + let (neqs, nlocs) = split_eq_do node_env eq in (split_tuples (eqs@neqs), locs@nlocs) -and (split_eq_do : Eff.eq_info Lxm.srcflagged -> split_acc) = - fun { src = lxm_eq ; it = (lhs, rhs) } -> - let n_rhs, (neqs, nlocs) = split_val_exp true rhs in +and (split_eq_do : Eff.local_env -> Eff.eq_info Lxm.srcflagged -> split_acc) = + fun node_env { src = lxm_eq ; it = (lhs, rhs) } -> + let n_rhs, (neqs, nlocs) = split_val_exp true node_env rhs in { src = lxm_eq ; it = (lhs, n_rhs) }::neqs, nlocs -and (split_val_exp : bool -> Eff.val_exp -> Eff.val_exp * split_acc) = - fun top_level ve -> +and (split_val_exp : bool -> Eff.local_env -> Eff.val_exp -> Eff.val_exp * split_acc) = + fun top_level node_env ve -> match ve with | CallByPosEff({it=Eff.IDENT _}, _) | CallByPosEff({it=Eff.CONST _}, _) @@ -141,7 +146,7 @@ and (split_val_exp : bool -> Eff.val_exp -> Eff.val_exp * split_acc) = let fl, eql, vl = List.fold_left (fun (fl_acc, eql_acc, vl_acc) (fn, fv) -> - let fv, (eql, vl) = split_val_exp false fv in + let fv, (eql, vl) = split_val_exp false node_env fv in ((fn,fv)::fl_acc, eql@eql_acc, vl@vl_acc) ) ([],[],[]) @@ -158,25 +163,25 @@ and (split_val_exp : bool -> Eff.val_exp -> Eff.val_exp * split_acc) = (* for WITH and HAT, a particular treatment is done because the val_exp is attached to them *) | Eff.WITH(ve) -> - let ve, (eql, vl) = split_val_exp false ve in + let ve, (eql, vl) = split_val_exp false node_env ve in let by_pos_op_eff = Lxm.flagit (Eff.WITH(ve)) lxm in let rhs = CallByPosEff(by_pos_op_eff, OperEff []) in rhs, (eql, vl) | Eff.HAT(i,ve) -> - let ve, (eql, vl) = split_val_exp false ve in + let ve, (eql, vl) = split_val_exp false node_env ve in let by_pos_op_eff = Lxm.flagit (Eff.HAT(i, ve)) lxm in let rhs = CallByPosEff(by_pos_op_eff, OperEff []) in rhs, (eql, vl) | Eff.WHEN ve -> (* should we create a var for the clock ? *) - let vel,(eql, vl) = split_val_exp_list false vel in + let vel,(eql, vl) = split_val_exp_list false node_env vel in let by_pos_op_eff = Lxm.flagit (Eff.WHEN(ve)) lxm in let rhs = CallByPosEff(by_pos_op_eff, OperEff vel) in rhs, (eql, vl) | _ -> - let vel, (eql, vl) = split_val_exp_list false vel in + let vel, (eql, vl) = split_val_exp_list false node_env vel in let rhs = CallByPosEff(by_pos_op_eff, OperEff vel) in rhs, (eql, vl) in @@ -186,7 +191,7 @@ and (split_val_exp : bool -> Eff.val_exp -> Eff.val_exp * split_acc) = (* create the var for the current call *) let clk_l = EvalClock.get_val_exp_eff ve in let typ_l = EvalType.val_exp_eff ve in - let nv_l = List.map2 new_var typ_l clk_l in + let nv_l = List.map2 (new_var node_env) typ_l clk_l in let nve = match nv_l with | [nv] -> CallByPosEff( @@ -213,26 +218,29 @@ and (split_val_exp : bool -> Eff.val_exp -> Eff.val_exp * split_acc) = nve, (eql@[eq], vl@nv_l) -and (split_val_exp_list : bool -> Eff.val_exp list -> Eff.val_exp list * split_acc) = - fun top_level vel -> - let vel, accl = List.split (List.map (split_val_exp top_level) vel) in +and (split_val_exp_list : + bool -> Eff.local_env -> Eff.val_exp list -> Eff.val_exp list * split_acc) = + fun top_level node_env vel -> + let vel, accl = List.split (List.map (split_val_exp top_level node_env) vel) in let eqll,vll = List.split accl in let eql, vl = List.flatten eqll, List.flatten vll in (vel,(eql,vl)) (* exported *) -let (node : Eff.node_exp -> Eff.node_exp) = - fun n -> +let (node : Eff.local_env -> Eff.node_exp -> Eff.node_exp) = + fun n_env n -> match n.def_eff with | ExternEff | AbstractEff -> n | BodyEff b -> init_var (); let loc = match n.loclist_eff with None -> [] | Some l -> l in - let (neqs, nv) = List.fold_left split_eq ([], loc) b.eqs_eff in + let (neqs, nv) = List.fold_left (split_eq n_env) ([], loc) b.eqs_eff in let asserts = List.map (fun x -> x.it) b.asserts_eff in let lxm_asserts = List.map (fun x -> x.src) b.asserts_eff in - let nasserts,(neqs_asserts,nv_asserts) = split_val_exp_list true asserts in + let nasserts,(neqs_asserts,nv_asserts) = + split_val_exp_list true n_env asserts + in let nasserts = List.map2 Lxm.flagit nasserts lxm_asserts in let (neqs, nv) = (neqs@neqs_asserts, nv@nv_asserts) in let nb = { eqs_eff = neqs ; asserts_eff = nasserts } in diff --git a/src/split.mli b/src/split.mli index fe859a0cec2fe72c6dc9ba2ca9d94353e0302b73..88f907889b3cf8736eb992f9937bf665865ca4ed 100644 --- a/src/split.mli +++ b/src/split.mli @@ -1,4 +1,4 @@ -(** Time-stamp: <modified the 29/08/2008 (at 16:29) by Erwan Jahier> *) +(** Time-stamp: <modified the 20/11/2008 (at 13:44) by Erwan Jahier> *) (** Split the equations of a node into several ones, in such a way @@ -17,5 +17,7 @@ c = 3 -> _v3; (_v1, _v2, _v3) = titi(x); + The node local_env is provided so that we can update its table, as + we add some fresh local variables during the code transmation. *) -val node : Eff.node_exp -> Eff.node_exp +val node : Eff.local_env -> Eff.node_exp -> Eff.node_exp diff --git a/src/test/should_work/NONREG/param_node.lus b/src/test/should_work/NONREG/param_node.lus index 152fabec5290b92a12e7c882820d309cf485d607..433b4507f12fa1b1c33fa31ae98fdb875ea511b0 100644 --- a/src/test/should_work/NONREG/param_node.lus +++ b/src/test/should_work/NONREG/param_node.lus @@ -1,13 +1,11 @@ - --- A node parametrized by a node - -node toto_n<<node f(a, b: int) returns (x: int); const n : int>>(a: int) -returns (x: int^n); +---- A node parametrized by a node and a const +node toto_n<< + node f(a, b: int) returns (x: int); + const n : int + >>(a: int) returns (x: int^n); var v : int; let v = f(a, 1); x = v ^ n; -tel - +tel --- node toto_3 = toto_n<<Lustre::iplus, 3>>; - diff --git a/src/test/should_work/lionel/mapiter.lus b/src/test/should_work/lionel/mapiter.lus index c691d7e729a599b79d6f6f1ba9026a5e8da627c6..27203013c11f514842c942af3de0d85a038206b7 100644 --- a/src/test/should_work/lionel/mapiter.lus +++ b/src/test/should_work/lionel/mapiter.lus @@ -44,8 +44,8 @@ tel node map_egal = map<< Lustre::eq , L>>; node composemat ( i1, i2 : T_Reg_H ) returns ( s1 : T_Reg_H ); let --- s1 = map<< map<< = , L>> , H>>( i1, i2 ); - s1 = map<<map_egal , H>>( i1, i2 ); + s1 = map<< map<< Lustre::eq , L>> , H>>( i1, i2 ); +-- s1 = map<<map_egal , H>>( i1, i2 ); tel -- compte le nombre de case a vrai diff --git a/src/test/should_work/packEnvTest/complex.lus b/src/test/should_work/packEnvTest/complex.lus index b7e402baa7a415c4dcfa63adb94ba122a13f8550..6bf2371567e3cd53804c65e79650cbc6414ae0d8 100644 --- a/src/test/should_work/packEnvTest/complex.lus +++ b/src/test/should_work/packEnvTest/complex.lus @@ -1,7 +1,7 @@ package complex -- uses trigo, math, ... ; provides type t; -- Encapsulation - const i:t; + const i:t; function re(c: t) returns (r:real); --- body type t = struct { re : real ; im : real }; diff --git a/src/test/should_work/packEnvTest/model.lus b/src/test/should_work/packEnvTest/model.lus index b26152a329b89fcd8b31c4242d3843958e505cfe..bfecc616cfd4bad02771acec572481fa51c18ebc 100644 --- a/src/test/should_work/packEnvTest/model.lus +++ b/src/test/should_work/packEnvTest/model.lus @@ -1,9 +1,9 @@ model modSimple needs type t; provides - node fby1(init, fb: t) returns (next: t); + node fby1(init, fb: t) returns (next: t); --- body node fby1(init, fb: t) returns (next: t); let next = init -> pre fb; tel -end +end --- package pint is modSimple(t=int); diff --git a/src/test/test.res.exp b/src/test/test.res.exp index 06f5a53c689d3bbb43ec3e7201435c222b783e60..967fb073adf0f9fce5d5c887f55137a49d28cb61 100644 --- a/src/test/test.res.exp +++ b/src/test/test.res.exp @@ -13,6 +13,7 @@ usage: lus2lic [options] <lustre files> | lus2lic -help --verbose-level <int> -vl <int> Set verbose level --keep-nested-calls Keep nested calls + --inline-iterators Inline iterators -h -help --help Display this list of options @@ -7237,26 +7238,26 @@ type A_int_3 = int^3; ---------------------------------------------------------------------- ====> ../lus2lic -vl 2 --compile-all-items should_work/NONREG/param_node2.lus Opening file should_work/NONREG/param_node2.lus -node param_node2::toto_n_int_3_3(a:int) returns (res:A_int_3); +node param_node2::mk_tab_int_0_3(a:int) returns (res:A_int_3); let - res = a^3; + res = init^3; tel --- end of node param_node2::toto_n_int_3_3 -node param_node2::toto_int3(a:int) returns (res:A_int_3); +-- end of node param_node2::mk_tab_int_0_3 +node param_node2::tab_int3(a:int) returns (res:A_int_3); let - res = param_node2::toto_n_int_3_3(a); + res = param_node2::mk_tab_int_0_3(a); tel --- end of node param_node2::toto_int3 -node param_node2::toto_n_bool_0_4(a:bool) returns (res:A_bool_4); +-- end of node param_node2::tab_int3 +node param_node2::mk_tab_bool_true_4(a:bool) returns (res:A_bool_4); let - res = a^4; + res = init^4; tel --- end of node param_node2::toto_n_bool_0_4 -node param_node2::toto_bool4(a:bool) returns (res:A_bool_4); +-- end of node param_node2::mk_tab_bool_true_4 +node param_node2::tab_bool4(a:bool) returns (res:A_bool_4); let - res = param_node2::toto_n_bool_0_4(a); + res = param_node2::mk_tab_bool_true_4(a); tel --- end of node param_node2::toto_bool4 +-- end of node param_node2::tab_bool4 -- automatically defined aliases: type A_bool_4 = bool^4; type A_int_3 = int^3; @@ -16990,7 +16991,7 @@ node mapiter::composemat( returns ( s1:A_A_bool_2_3); let - s1 = map<<mapiter::map_egal, 3>>(i1, i2); + s1 = map<<_node_alias_1_Lustre::map, 3>>(i1, i2); tel -- end of node mapiter::composemat node mapiter::mapiter(a:bool) returns (nbTrue:int); @@ -17013,6 +17014,11 @@ tel type A_A_bool_2_3 = A_bool_2^3; type A_a_2 = a^2; type A_bool_2 = bool^2; +node _node_alias_1_Lustre::map(i1:A_bool_2; i2:A_bool_2) returns (o:A_bool_2); +let + o = Lustre::map<<Lustre::equal, 2>>(i1,i2); +tel + ---------------------------------------------------------------------- ====> ../lus2lic -vl 2 --compile-all-items should_work/lionel/matrice.lus