diff --git a/lib/ast2lic.ml b/lib/ast2lic.ml index 2276ad38343167efd92d6e3d3bdd1eff47bfeac7..73f0105212af5f262281de51248a8e8a7b9c0acd 100644 --- a/lib/ast2lic.ml +++ b/lib/ast2lic.ml @@ -1,4 +1,4 @@ -(* Time-stamp: <modified the 29/08/2019 (at 15:28) by Erwan Jahier> *) +(* Time-stamp: <modified the 15/04/2024 (at 11:56) by Erwan Jahier> *) open Lxm @@ -28,21 +28,21 @@ let rec (of_type: IdSolver.t -> AstCore.type_exp -> Lic.type_) = try let sz = EvalConst.eval_array_size env szexp in Array_type_eff (elt_teff, sz) - with EvalConst.EvalArray_error msg -> + with EvalConst.EvalArray_error msg -> let lxm = AstCore.lxm_of_val_exp szexp in raise (Compile_error(lxm, "can't eval type: "^msg)) let (_add_pack_name : IdSolver.t -> Lxm.t -> Lv6Id.idref -> Lv6Id.idref) = - fun id_solver lxm cc -> + fun id_solver lxm cc -> try match Lv6Id.pack_of_idref cc with | Some _ -> cc | None -> let id = Lv6Id.of_idref false cc in - let pn = - AstTabSymbol.find_pack_of_const id_solver.global_symbols id lxm + let pn = + AstTabSymbol.find_pack_of_const id_solver.global_symbols id lxm in Lv6Id.make_idref pn id with _ -> cc (* raise en error? *) @@ -61,31 +61,31 @@ let (of_clock : IdSolver.t -> AstCore.var_info -> Lic.id_clock)= (******************************************************************************) (* Checks that the left part has the same type as the right one. *) -and (type_check_equation: IdSolver.t -> Lxm.t -> Lic.left list -> +and (type_check_equation: IdSolver.t -> Lxm.t -> Lic.left list -> Lic.val_exp -> unit) = - fun id_solver lxm lpl_eff ve_eff -> + fun id_solver lxm lpl_eff ve_eff -> let lpl_teff = List.map Lic.type_of_left lpl_eff in let ve_eff, right_part = EvalType.f id_solver ve_eff in if (List.length lpl_teff <> List.length right_part) then - raise (Compile_error(lxm, - "tuple size error: \n*** the tuple size is\n***\t"^ + raise (Compile_error(lxm, + "tuple size error: \n*** the tuple size is\n***\t"^ (string_of_int (List.length lpl_teff)) ^ - " for the left-hand-side, and \n***\t" ^ + " for the left-hand-side, and \n***\t" ^ (string_of_int (List.length right_part)) ^ " for the right-hand-side (in " ^ (String.concat - "," + "," (List.map (LicDump.string_of_leff false) lpl_eff)) ^ " = " ^ - (LicDump.string_of_val_exp_eff false ve_eff) ^ ")\n" + (LicDump.string_of_val_exp_eff false ve_eff) ^ ")\n" )) else List.iter2 - (fun le re -> + (fun le re -> if le <> re then - let msg = "type mismatch: \n***\t'" - ^ (Lic.string_of_type le) ^ - "' (left-hand-side) \n*** is not compatible with \n***\t'" + let msg = "type mismatch: \n***\t'" + ^ (Lic.string_of_type le) ^ + "' (left-hand-side) \n*** is not compatible with \n***\t'" ^ (Lic.string_of_type re) ^ "' (right-hand-side)" in raise (Compile_error(lxm, msg)) @@ -94,7 +94,7 @@ and (type_check_equation: IdSolver.t -> Lxm.t -> Lic.left list -> right_part (* Checks that the left part has the same clock as the right one. *) -and (clock_check_equation:IdSolver.t -> Lxm.t -> UnifyClock.subst -> +and (clock_check_equation:IdSolver.t -> Lxm.t -> UnifyClock.subst -> Lic.left list -> Lic.id_clock list -> Lic.val_exp -> Lic.val_exp) = fun _id_solver _lxm s lpl_eff right_part_clks ve_eff -> let lxms = List.map Lic.lxm_of_left lpl_eff in @@ -102,20 +102,20 @@ and (clock_check_equation:IdSolver.t -> Lxm.t -> UnifyClock.subst -> ve_eff (******************************************************************************) -(* +(* ICI : BEQUILLE(S) on fait un lookup dans la table des operateurs -pour rechercher leurs (éventuels) parametres statiques : +pour rechercher leurs (éventuels) parametres statiques : TRAITER LES MACROS PREDEF : - ici, on juste besoin de fabriquer les arguments statiques effectifs à partir des arguments donnés et des args attendus. -- on cherche pas à faire rentrer dans le moule, on délègue +- on cherche pas à faire rentrer dans le moule, on délègue -- 2015/07 -> probleme des node avec param statiques identifies par pack::node +- 2015/07 -> probleme des node avec param statiques identifies par pack::node c'etait pas prevu du tout ... rajout du champs "all_srcs" dans le id solver qui premet de retrouver - n'importe quelle info source (un peu extreme comme solution ...) + n'importe quelle info source (un peu extreme comme solution ...) *) (* pour abstraire la nature des params statiques *) @@ -124,7 +124,7 @@ type abstract_static_param = | ASP_type of Lv6Id.t | ASP_node of Lv6Id.t -let do_abstract_static_param x = +let do_abstract_static_param x = match x.it with | StaticParamType id -> ASP_type id | StaticParamConst (id,_) -> ASP_const id @@ -137,7 +137,7 @@ let get_abstract_static_params (lxm: Lxm.t) (idref: Lv6Id.idref) : abstract_static_param list = - + Lv6Verbose.exe ~flag:dbg (fun () -> Printf.fprintf stderr "#DBG: Ast2lic.get_abstract_static %s\n" (Lv6Id.raw_string_of_idref idref) @@ -145,6 +145,7 @@ let get_abstract_static_params match (idref.id_pack, idref.id_id) with | (Some "Lustre", "map") | (Some "Lustre", "red") + | (Some "Lustre", "fold") | (Some "Lustre", "fill") | (Some "Lustre", "fillred") -> [ ASP_node "oper"; ASP_const "size" ] | (Some "Lustre", "boolred") -> [ ASP_const "min"; ASP_const "max"; ASP_const "size"] @@ -172,18 +173,18 @@ let get_abstract_static_params (* can occur for static node parameters, which cannot themselves have static parameters. A better solution ougth to be to add node static parameters in the AstTabSymbol.t - however (in Lazycompiler.node_check_do most probably). - + however (in Lazycompiler.node_check_do most probably). + OUI MAIS GROS BUG : qu'est-ce-qui se passe si si le 'static node parameter' porte le meme nom qu'un noeud existant dans AstTabSymbol ??? - + C'est clairement pas la bonne méthode ... Voir + bas ... - + *) (* [] *) - ) + ) (* exported *) @@ -205,12 +206,13 @@ let rec of_node | (None, "red") | (None, "fill") | (None, "fillred") + | (None, "fold") | (None, "boolred") | (None, "condact") -> {idref with id_pack = Some "Lustre"} | _ -> idref in (* BUG des param statique node avec le meme nom - qu'un node template global : + qu'un node template global : pis-aller : si static_args = [], on a peut-etre affaire à un static param node, donc on appelle directement id_solver.id2node et c'est lui @@ -231,17 +233,17 @@ let rec of_node let static_params = get_abstract_static_params id_solver.all_srcs id_solver.global_symbols lxm idref in - let sp_l = List.length static_params + let sp_l = List.length static_params and sa_l = List.length static_args in if (sp_l <> sa_l) then - let msg = "Bad number of (static) arguments: " ^ - (string_of_int sp_l) ^ " expected, and " ^ + let msg = "Bad number of (static) arguments: " ^ + (string_of_int sp_l) ^ " expected, and " ^ (string_of_int sa_l) ^ " provided." in raise (Compile_error(lxm, msg)) else - List.map2 (check_static_arg id_solver) - static_params + List.map2 (check_static_arg id_solver) + static_params static_args in let res = id_solver.id2node idref static_args_eff lxm in @@ -255,13 +257,13 @@ let rec of_node and check_static_arg (node_id_solver: IdSolver.t) - (asp: abstract_static_param) - (sa: AstCore.static_arg srcflagged) + (asp: abstract_static_param) + (sa: AstCore.static_arg srcflagged) : Lic.static_arg = ( (* 1ere passe : on utilise expected juste pour résoudre la nature, - on "compile" les args + on "compile" les args *) let nature_error nat = let msg = Printf.sprintf "Bad static argument nature, a %s was expected" nat in @@ -311,7 +313,7 @@ and check_static_arg (* exported *) and (of_eq: IdSolver.t -> AstCore.eq_info srcflagged -> Lic.eq_info srcflagged) = - fun id_solver eq_info -> + fun id_solver eq_info -> let (lpl, ve) = eq_info.it in let lpl_eff = List.map (translate_left_part id_solver) lpl in let exp_clks = List.map Lic.clock_of_left lpl_eff in @@ -325,9 +327,9 @@ and (of_eq: IdSolver.t -> AstCore.eq_info srcflagged -> Lic.eq_info srcflagged) and (translate_left_part : IdSolver.t -> AstCore.left_part -> Lic.left) = - fun id_solver lp_top -> + fun id_solver lp_top -> match lp_top with - | LeftVar id -> + | LeftVar id -> let vi_eff = id_solver.id2var id.it id.src in LeftVarLic (vi_eff, id.src) | LeftField (lp, id) -> ( @@ -358,9 +360,9 @@ and (translate_left_part : IdSolver.t -> AstCore.left_part -> Lic.left) = | LeftSlice (lp, sif) -> ( let lp_eff = translate_left_part id_solver lp in let teff = Lic.type_of_left lp_eff in - match teff with + match teff with | Abstract_type_eff(_,Array_type_eff(teff_elt, _size)) - | Array_type_eff(teff_elt, _size) -> + | Array_type_eff(teff_elt, _size) -> let sieff = translate_slice_info id_solver sif.it sif.src in let size_slice = sieff.se_width in let teff_slice = Array_type_eff(teff_elt, size_slice) in @@ -370,14 +372,14 @@ and (translate_left_part : IdSolver.t -> AstCore.left_part -> Lic.left) = (* Translate and performs the checks *) -and (translate_val_exp_check : IdSolver.t -> Lic.clock list -> UnifyClock.subst -> +and (translate_val_exp_check : IdSolver.t -> Lic.clock list -> UnifyClock.subst -> AstCore.val_exp -> Lic.val_exp * Lic.id_clock list * UnifyClock.subst) = fun id_solver exp_clks s ve -> let s,vef = translate_val_exp id_solver s ve in let lxm = AstCore.lxm_of_val_exp ve in let lxms = List.map (fun _ -> lxm) exp_clks in (* let vef, tl = EvalType.f id_solver vef in *) - EvalClock.f id_solver s vef lxms exp_clks + EvalClock.f id_solver s vef lxms exp_clks and (translate_val_exp : IdSolver.t -> UnifyClock.subst -> AstCore.val_exp @@ -386,19 +388,19 @@ and (translate_val_exp : IdSolver.t -> UnifyClock.subst -> AstCore.val_exp (match ve with | CallByPos({it=WITH_n(c,e1,e2);_}, Oper vel) -> assert (vel=[]); - if EvalConst.f id_solver c = [ Bool_const_eff true ] - then translate_val_exp id_solver s e1 + if EvalConst.f id_solver c = [ Bool_const_eff true ] + then translate_val_exp id_solver s e1 else translate_val_exp id_solver s e2 - | _ -> + | _ -> let s, vef_core, lxm = match ve with - | Merge_n(ve, cl) -> + | Merge_n(ve, cl) -> let lxm_ve = ve.src in let ve = ve.it in let s,ve = translate_val_exp id_solver s ve in let s, cl = List.fold_left - (fun (s,cl) (id,ve) -> + (fun (s,cl) (id,ve) -> let s, ve = translate_val_exp id_solver s ve in let const = id_solver.id2const id.it id.src in s,(flagit const id.src, ve)::cl @@ -418,8 +420,8 @@ and (translate_val_exp : IdSolver.t -> UnifyClock.subst -> AstCore.val_exp s, Lic.Merge(ve, [case_true; case_false]), lxm_ve | CallByName(by_name_op, field_list) -> - let s,fl = List.fold_left - (fun (s,fl) f -> + let s,fl = List.fold_left + (fun (s,fl) f -> let s,f = translate_field id_solver s f in s,f::fl ) @@ -428,17 +430,17 @@ and (translate_val_exp : IdSolver.t -> UnifyClock.subst -> AstCore.val_exp in let fl = List.rev fl in let s, by_name_op = translate_by_name_op id_solver by_name_op s in - s, + s, (CallByNameLic(by_name_op, fl)), by_name_op.src | CallByPos(by_pos_op, Oper vel) -> - let s, vel_eff = - List.fold_left - (fun (s,vel) ve -> + 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 + (s,[]) vel in let vel_eff = List.rev vel_eff in let lxm = by_pos_op.src in @@ -446,7 +448,7 @@ and (translate_val_exp : IdSolver.t -> UnifyClock.subst -> AstCore.val_exp let mk_by_pos_op by_pos_op_eff = CallByPosLic(flagit by_pos_op_eff lxm, vel_eff) in - let mk_nary_pos_op by_pos_op_eff = + let mk_nary_pos_op by_pos_op_eff = (* For nor and diese: internally, nor and diese takes an array of val_exp, to make it easier the translation into boolred. @@ -458,7 +460,7 @@ and (translate_val_exp : IdSolver.t -> UnifyClock.subst -> AstCore.val_exp ve_typ = [Array_type_eff(List.hd (List.hd vel_eff).ve_typ, List.length vel_eff)]; ve_clk = (List.hd vel_eff).ve_clk; - ve_src = lxm + ve_src = lxm } in CallByPosLic(flagit by_pos_op_eff lxm, [array_val_exp]) @@ -480,7 +482,7 @@ and (translate_val_exp : IdSolver.t -> UnifyClock.subst -> AstCore.val_exp Lic.PREDEF_CALL (flagit (AstPredef.op_to_long DIESE_n,[]) lxm)) | Predef_n(op) -> s, mk_by_pos_op( Lic.PREDEF_CALL (flagit (AstPredef.op_to_long op.it,[]) op.src)) - | CALL_n node_exp_f -> + | CALL_n node_exp_f -> let neff = of_node id_solver node_exp_f in let ceff = Lic.CALL (flagit neff.node_key_eff node_exp_f.src) in Lv6Verbose.exe ~flag:dbg (fun () -> @@ -507,11 +509,11 @@ and (translate_val_exp : IdSolver.t -> UnifyClock.subst -> AstCore.val_exp | FBY_n -> (* XXX temporary crutch: translate "e1 fby e2" into "e2 -> pre(e2)" *) (match vel_eff with - | [e1;e2] -> + | [e1;e2] -> let ve_pre = CallByPosLic(flagit Lic.PRE lxm, [e2]) in let ve_pre = { e2 with ve_core=ve_pre } in let lxm = Lxm.override_name "->" lxm in - s,CallByPosLic(flagit Lic.ARROW lxm, [e1;ve_pre]) + s,CallByPosLic(flagit Lic.ARROW lxm, [e1;ve_pre]) | _ -> assert false ) (* | FBY_n -> s, mk_by_pos_op Lic.FBY *) @@ -522,7 +524,7 @@ and (translate_val_exp : IdSolver.t -> UnifyClock.subst -> AstCore.val_exp s, mk_by_pos_op (Lic.STRUCT_ACCESS (fid)) | WHEN_n Base -> s, mk_by_pos_op (Lic.WHEN BaseLic) - | WHEN_n (NamedClock { it = (cc,c) ; src = lxm }) -> + | WHEN_n (NamedClock { it = (cc,c) ; src = lxm }) -> let var_info = id_solver.id2var c lxm in let _, clk = var_info.var_clock_eff in let ct = var_info.var_type_eff in @@ -538,8 +540,8 @@ and (translate_val_exp : IdSolver.t -> UnifyClock.subst -> AstCore.val_exp | HAT_n -> ( match vel with - | [_exp; ve_size] -> - let size_const_eff = EvalConst.f id_solver ve_size in + | [_exp; ve_size] -> + let size_const_eff = EvalConst.f id_solver ve_size in (match size_const_eff with | [Int_const_eff sz] -> s, mk_by_pos_op (Lic.HAT(int_of_string sz)) | _ -> assert false) @@ -551,10 +553,10 @@ and (translate_val_exp : IdSolver.t -> UnifyClock.subst -> AstCore.val_exp let vef = { ve_core=vef_core; ve_typ=[]; ve_clk = []; ve_src = lxm } in let vef, _tl = EvalType.f id_solver vef in s,vef - ) + ) -and translate_by_name_op id_solver op s = +and translate_by_name_op id_solver op s = let to_long idref = match Lv6Id.pack_of_idref idref with | None -> (* If no pack name is provided, we lookup it in the symbol table *) @@ -567,33 +569,33 @@ and translate_by_name_op id_solver op s = match op.it with | STRUCT_anonymous_n -> s, STRUCT_anonymous | STRUCT_n idref -> s, STRUCT (to_long idref) - | STRUCT_WITH_n (idref1, idref2) -> + | STRUCT_WITH_n (idref1, idref2) -> s, STRUCT_with (to_long idref1, idref2.id_id) in s, flagit nop op.src -and translate_field id_solver s (id, 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 ? +(* XXX autre nom, autre module ? node_of_static_arg : appelé QUAND ON SAIT qu'un sarg doit etre un NODE const_of_static_arg : appelé QUAND ON SAIT qu'un sarg doit etre une CONST -> sert pour les macros predefs ca fait partie de la definition des iterateurs d'une certaine maniere... - -> créer 2 modules, Iterator + IteratorSemantics + -> créer 2 modules, Iterator + IteratorSemantics *) -and _const_of_static_arg id_solver const_or_const_ident lxm = +and _const_of_static_arg id_solver const_or_const_ident lxm = match const_or_const_ident with | StaticArgConst(c) -> ( match EvalConst.f id_solver c with | [x] -> x - | xl -> + | xl -> (* EvalConst.f ne fabrique PAS de tuple, on le fait ici *) Tuple_const_eff xl ) - | StaticArgLv6Id(id) -> id_solver.id2const id lxm + | StaticArgLv6Id(id) -> id_solver.id2const id lxm | StaticArgType _ | StaticArgNode _ -> raise (Compile_error(lxm, "a constant was expected")) @@ -601,9 +603,9 @@ and _const_of_static_arg id_solver const_or_const_ident lxm = and _node_of_static_arg id_solver node_or_node_ident lxm = match node_or_node_ident with - | StaticArgLv6Id(id) -> + | StaticArgLv6Id(id) -> let sargs = [] in (* it is an alias: no static arg *) - id_solver.id2node id sargs lxm + id_solver.id2node id sargs lxm | StaticArgNode(CALL_n ne) -> of_node id_solver ne | StaticArgNode(Predef_n (op)) -> @@ -611,10 +613,10 @@ and _node_of_static_arg id_solver node_or_node_ident lxm = | StaticArgNode(_) -> assert false - | StaticArgType _ + | StaticArgType _ | StaticArgConst _ -> raise (Compile_error(lxm, "a node was expected")) -and (translate_slice_info : IdSolver.t -> AstCore.slice_info -> +and (translate_slice_info : IdSolver.t -> AstCore.slice_info -> Lxm.t -> Lic.slice_info) = fun id_solver si lxm -> EvalConst.eval_array_slice id_solver si lxm @@ -622,7 +624,7 @@ and (translate_slice_info : IdSolver.t -> AstCore.slice_info -> (**********************************************************************************) (* exported *) -let (of_assertion : IdSolver.t -> AstCore.val_exp Lxm.srcflagged -> +let (of_assertion : IdSolver.t -> AstCore.val_exp Lxm.srcflagged -> Lic.val_exp Lxm.srcflagged) = fun id_solver vef -> let s = UnifyClock.empty_subst in @@ -631,10 +633,10 @@ let (of_assertion : IdSolver.t -> AstCore.val_exp Lxm.srcflagged -> (* Check that the assert is a bool. *) let val_exp_eff, evaled_exp = EvalType.f id_solver val_exp_eff in List.iter - (fun ve -> + (fun ve -> if ve <> Bool_type_eff then - let msg = "type mismatch: \n\tthe content of the assertion is of type " - ^ (Lic.string_of_type ve) + let msg = "type mismatch: \n\tthe content of the assertion is of type " + ^ (Lic.string_of_type ve) ^ " whereas it shoud be a Boolean\n" in raise (Compile_error(vef.src, msg)) @@ -643,21 +645,21 @@ let (of_assertion : IdSolver.t -> AstCore.val_exp Lxm.srcflagged -> (* type is ok *) (* Clock check the assertion*) - let _, clock_eff_list, _s = + let _, clock_eff_list, _s = EvalClock.f id_solver s val_exp_eff [vef.src] [BaseLic] in match clock_eff_list with - | [_id, BaseLic] + | [_id, BaseLic] | [_id, On(_,BaseLic)] | [_id, ClockVar _] -> Lxm.flagit val_exp_eff vef.src - | [_id, ce] -> + | [_id, ce] -> let msg = "clock error: assert should be on the base clock, "^ "but it is on "^ (LicDump.string_of_clock2 ce) ^ "\n" in raise (Compile_error(vef.src, msg)) | _ -> assert false - + (******************************************************************************) (******************************************************************************) diff --git a/lib/l2lExpandMetaOp.ml b/lib/l2lExpandMetaOp.ml index 63d33e2048996f87ce7ce513197ad4e2e547b1bc..dab0009f1b4a4de8587c04811a1246fee9b924de 100644 --- a/lib/l2lExpandMetaOp.ml +++ b/lib/l2lExpandMetaOp.ml @@ -1,4 +1,4 @@ -(** Time-stamp: <modified the 05/05/2022 (at 08:40) by Erwan Jahier> *) +(** Time-stamp: <modified the 15/04/2024 (at 11:54) by Erwan Jahier> *) open Lxm open Lic @@ -6,20 +6,20 @@ open Lic let dbg = (Lv6Verbose.get_flag "ei") (* pack useful info into a single struct *) -type local_ctx = { +type local_ctx = { node : Lic.node_exp; prg : LicPrg.t; } (********************************************************************************) (* stuff to create fresh var names. *) -let new_var str _lctx type_eff clock_eff = - let id = Lv6Id.of_string (FreshName.local_var (str)) in +let new_var str _lctx type_eff clock_eff = + let id = Lv6Id.of_string (FreshName.local_var (str)) in let var = - { + { var_name_eff = id; var_nature_eff = AstCore.VarLocal; - var_number_eff = -1; (* this field is used only for i/o. + 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 = id, clock_eff; @@ -29,16 +29,16 @@ let new_var str _lctx type_eff clock_eff = (********************************************************************************) (* 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 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 rec (list_map3: + +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 *) + | _ -> (* should not occur *) print_string "*** list_map3 called with lists of different size.\n"; flush stdout; assert false @@ -49,81 +49,81 @@ let rec (list_map3: let lxm = Lxm.dummy "no_source" let (val_exp_of_var_info : Lxm.t -> Lic.var_info -> Lic.val_exp) = - fun lxm vi -> - { - ve_core = CallByPosLic({src=lxm;it=Lic.VAR_REF vi.var_name_eff}, []); + fun lxm vi -> + { + ve_core = CallByPosLic({src=lxm;it=Lic.VAR_REF vi.var_name_eff}, []); ve_typ = [vi.var_type_eff]; ve_clk = [snd vi.var_clock_eff]; ve_src = lxm } let (val_exp_of_ident : Lxm.t -> string -> Lic.type_ -> Lic.clock -> Lic.val_exp) = - fun lxm id t clk -> - { - ve_clk = [clk]; - ve_typ = [t]; + fun lxm id t clk -> + { + ve_clk = [clk]; + ve_typ = [t]; ve_core = CallByPosLic({it=Lic.VAR_REF id;src=lxm},[]); ve_src = lxm } let (val_exp_of_int : Lxm.t -> string -> Lic.clock -> Lic.val_exp) = - fun lxm i clk -> - { - ve_clk = [clk]; - ve_typ = [Int_type_eff]; + fun lxm i clk -> + { + ve_clk = [clk]; + ve_typ = [Int_type_eff]; ve_core = CallByPosLic({it= CONST(Int_const_eff i);src=lxm},[]); ve_src = lxm } let (val_exp_of_const : Lic.const -> Lic.val_exp) = - fun c -> + fun c -> let _,ve = UnifyClock.const_to_val_eff lxm true UnifyClock.empty_subst c in ve let (add_when : Lic.clock -> Lic.val_exp -> Lic.val_exp) = - fun clk ve -> - { ve with - ve_clk = List.map (fun _ -> clk) ve.ve_clk; + fun clk ve -> + { ve with + ve_clk = List.map (fun _ -> clk) ve.ve_clk; ve_core = CallByPosLic({it= WHEN clk;src=lxm},[ve]); } (* [add_current ve clk out_cl] return the expression current(ve when clk) *) let (add_current : Lic.val_exp -> Lic.clock -> Lic.clock list -> Lic.val_exp) = - fun ve clk out_cl -> + fun ve clk out_cl -> match clk with | On((cc,cv,_),sclk) -> let lxm = ve.ve_src in let clk_exp = val_exp_of_ident lxm cv Bool_type_eff sclk in { ve with - ve_clk = out_cl; + ve_clk = out_cl; ve_core = CallByPosLic({it= CURRENT(Some cc);src=lxm},[clk_exp;ve]) } | _ -> assert false (* SNO *) - + let rec (elt_type_of_array : Lic.type_ -> Lic.type_) = function | Array_type_eff(t, _) -> t | Abstract_type_eff(_,t) -> elt_type_of_array t - | _ -> assert false + | _ -> assert false let (array_var_to_val_exp : Lxm.t -> int -> var_info -> val_exp) = - fun lxm i vi -> + fun lxm i vi -> (* vi holds x of type array and returns x.[i] *) let t_elt = elt_type_of_array vi.var_type_eff in let op_flg = {src = lxm ; it = ARRAY_ACCES(i)} in - { - ve_core = CallByPosLic(op_flg, [val_exp_of_var_info lxm vi]); + { + ve_core = CallByPosLic(op_flg, [val_exp_of_var_info lxm vi]); ve_typ = [t_elt]; ve_clk = [snd vi.var_clock_eff]; ve_src = lxm } -let (node_to_val_exp : Lxm.t -> Lic.node_key -> Lic.type_ list -> Lic.clock list -> +let (node_to_val_exp : Lxm.t -> Lic.node_key -> Lic.type_ list -> Lic.clock list -> val_exp list -> val_exp) = - fun lxm nk tl cl vel -> + fun lxm nk tl cl vel -> let nk = { src = lxm ; it = nk } in let core = CallByPosLic( { src = lxm ; it = CALL nk }, vel) in { @@ -131,7 +131,7 @@ let (node_to_val_exp : Lxm.t -> Lic.node_key -> Lic.type_ list -> Lic.clock list ve_typ = tl; ve_core = core; ve_src = lxm - } + } let (binop_to_val_exp : Lxm.t -> Lv6Id.t -> val_exp -> val_exp -> val_exp) = fun lxm op ve1 ve2 -> let op = { it = PREDEF_CALL({src=lxm;it=("Lustre",op),[]}) ; src = lxm } in @@ -149,7 +149,7 @@ let (binop_to_val_exp_bool : Lxm.t -> Lv6Id.t -> val_exp -> val_exp -> val_exp) ve_typ = [Bool_type_eff]; ve_core = CallByPosLic(op, [ve1; ve2]); ve_src = lxm - + } let (fby_to_val_exp : Lxm.t -> val_exp -> val_exp -> val_exp) = fun lxm ve1 ve2 -> @@ -173,14 +173,14 @@ let (ite_to_val_exp : Lxm.t -> val_exp -> val_exp -> val_exp -> val_exp) = fun lxm ve1 ve2 ve3 -> let ite_op = { it = PREDEF_CALL({src=lxm;it=("Lustre","if"),[]}); src = lxm } in { - ve_clk = ve2.ve_clk; + ve_clk = ve2.ve_clk; ve_typ = ve2.ve_typ; ve_core = CallByPosLic(ite_op, [ve1; ve2; ve3]) ; ve_src = lxm - } + } let (array_var_to_left : int -> var_info -> Lic.left) = - fun i vi -> + fun i vi -> let lp = LeftVarLic(vi,lxm) in let t_elt = elt_type_of_array vi.var_type_eff in LeftArrayLic(lp,i,t_elt) @@ -189,18 +189,18 @@ let (array_var_to_left : int -> var_info -> Lic.left) = let (create_fillred_body: local_ctx -> Lic.static_arg list -> Lic.node_body * var_info list) = fun lctx sargs -> - (* Given + (* 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: + + the fillred expression has the profile: tau * tau_1^c * ... * tau_n^c -> tau * teta_1^c * ... * teta_l^c *) let iter_node,c = match List.sort compare sargs with | [ConstStaticArgLic(_,Int_const_eff(c));NodeStaticArgLic(_,_node_key)] | [ConstStaticArgLic(_,Int_const_eff(c));TypeStaticArgLic(_); NodeStaticArgLic(_,_node_key)] - -> + -> _node_key,c | _ -> assert false in @@ -208,7 +208,7 @@ let (create_fillred_body: local_ctx -> Lic.static_arg list -> let iter_node = Lxm.flagit iter_node lxm in (* Hence: - node(acc_in:tau; X1:tau_1^c ; ... ; Xn:tau_n^c) + node(acc_in:tau; X1:tau_1^c ; ... ; Xn:tau_n^c) returns (acc_out:tau; Y1:teta_1^c; ... ; Yl:teta_l^c) = fillred<<n,c>>; *) assert (lctx.node.Lic.inlist_eff <> []); @@ -219,25 +219,25 @@ let (create_fillred_body: local_ctx -> Lic.static_arg list -> let (x1_xn : var_info list) = List.tl lctx.node.Lic.outlist_eff in (* can be defined like this: - node(acc_in:tau; X1:tau_1^c ; ... ; Xn:tau_n^c) + node(acc_in:tau; X1:tau_1^c ; ... ; Xn:tau_n^c) returns (acc_out:tau; Y1 : teta1^c; ... ; Yl: teta_l^c) = var acc_1, ..., acc_c-2 : tau; - let - + let + acc_1, Y1[0], ... ,Yl[0] = n(acc_in,X1[0], ... ,Xk[0]); acc_2, Y1[1], ... ,Yl[1] = n(acc_1, X1[1], ... ,Xk[1]); - ... + ... acc_i+1, Y1[i], ... ,Yl[i] = n(acc_i,X1[i], ... ,Xk[i]); ... acc_out, Y1[c-1], ... ,Yl[c-1] = n(acc_c-1,X1[c-1], ... ,Xk[c-1]); - - « for all i = 0, ..., c-1 » + + « for all i = 0, ..., c-1 » acc_i+1, Y1[i], ... ,Yl[i] = n(acc_i,X1[i], ... ,Xk[i]) tel *) let c = int_of_string c in - let index_list = fill 0 c in + let index_list = fill 0 c in (* Building this list "acc_left_list" as [acc_1, ..., acc_c-2, acc_out] *) let type_exp,clock_exp = acc_in.var_type_eff, snd acc_in.var_clock_eff in let (acc_vars : var_info list) = @@ -258,7 +258,7 @@ let (create_fillred_body: local_ctx -> Lic.static_arg list -> So now we build those equations ; acc_1, Y1[0], ... ,Yl[0] = n(acc_in,X1[0], ... ,Xk[0]); acc_2, Y1[1], ... ,Yl[1] = n(acc_1, X1[1], ... ,Xk[1]); - ... + ... acc_i+1, Y1[i], ... ,Yl[i] = n(acc_i,X1[i], ... ,Xk[i]); ... acc_out, Y1[c-1], ... ,Yl[c-1] = n(acc_c-1,X1[c-1], ... ,Xk[c-1]); @@ -273,13 +273,13 @@ let (create_fillred_body: local_ctx -> Lic.static_arg list -> List.map (array_var_to_left i) x1_xn in let lhs = acc_left::yi_k in - let cl = + let cl = List.map (fun l -> snd (Lic.var_info_of_left l).var_clock_eff) lhs in let rhs = { ve_typ = List.map Lic.type_of_left lhs; ve_clk = cl; - ve_core = + ve_core = if AstPredef.is_a_predef_op (snd(fst iter_node.it)) then CallByPosLic({src=lxm;it=(Lic.PREDEF_CALL iter_node)}, args) else @@ -288,7 +288,7 @@ let (create_fillred_body: local_ctx -> Lic.static_arg list -> } in let eq = { src = lxm ; it = (lhs, rhs) } in - eq + eq ) index_list acc_left_list @@ -301,11 +301,11 @@ let (create_map_body: local_ctx -> Lic.static_arg list -> Lic.node_body * var_in (* 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]) @@ -314,7 +314,7 @@ let (create_map_body: local_ctx -> Lic.static_arg list -> Lic.node_body * var_in | [ConstStaticArgLic(_,Int_const_eff(c)) ; NodeStaticArgLic(_,node_key)] | [ConstStaticArgLic(_,Int_const_eff(c)) ; TypeStaticArgLic(_); NodeStaticArgLic(_,node_key)] - -> + -> node_key,c | _ -> assert false in @@ -322,7 +322,7 @@ let (create_map_body: local_ctx -> Lic.static_arg list -> Lic.node_body * var_in let (y1_yl : var_info list) = lctx.node.Lic.inlist_eff in let (x1_xn : var_info list) = lctx.node.Lic.outlist_eff in let c = int_of_string c in - let index_list = fill 0 c in + let index_list = fill 0 c in let neqs = List.map (fun i -> @@ -348,7 +348,7 @@ let (create_map_body: local_ctx -> Lic.static_arg list -> Lic.node_body * var_in } in let eq = { src = lxm ; it = (lhs, rhs) } in - eq + eq ) index_list in @@ -359,12 +359,12 @@ let (create_boolred_body: local_ctx -> int -> int -> int -> Lic.node_body * var_ fun lctx i j k -> (* Given - 3 integers i, j, k boolred<<i,j,k>> has the profile: bool^n -> bool and is defined by - node toto = boolred<<i,j,k>>(tab); + node toto = boolred<<i,j,k>>(tab); <=> node toto(tab:bool^n) returns (res:bool); - var + var cpt:int; - let + let cpt = (if tab[0] then 1 else 0) + ... + (if tab[k-1] then 1 else 0); res = i <= cpt && cpt <= j; tel @@ -372,11 +372,11 @@ let (create_boolred_body: local_ctx -> int -> int -> int -> Lic.node_body * var_ assert(0 <= i && i <= j && j <= k && k>0); let lxm = lctx.node.Lic.lxm in let (tab_vi : var_info) = match lctx.node.Lic.inlist_eff with - | [vi] -> vi + | [vi] -> vi | _ -> assert false in let (res_vi : var_info) = match lctx.node.Lic.outlist_eff with - | [vi] -> vi + | [vi] -> vi | _ -> assert false in let (cpt_vi : var_info) = new_var "cpt" lctx Int_type_eff BaseLic in @@ -403,16 +403,16 @@ let (create_boolred_body: local_ctx -> int -> int -> int -> Lic.node_body * var_ let i_inf_cpt = binop_to_val_exp_bool lxm "lte" i_eff cpt_eff in let cpt_inf_j = binop_to_val_exp_bool lxm "lte" cpt_eff j_eff in binop_to_val_exp lxm "and" i_inf_cpt cpt_inf_j - in + in let cpt_eq = { src = lxm ; it = ([cpt_left], cpt_rigth) } in let res_eq = { src = lxm ; it = ([res_left], res_rigth) } in - { - asserts_eff = []; - eqs_eff = [cpt_eq; res_eq] + { + asserts_eff = []; + eqs_eff = [cpt_eq; res_eq] }, [cpt_vi] let rec (replace_base : Lic.clock -> Lic.clock -> Lic.clock) = - fun ck1 ck2 -> + fun ck1 ck2 -> match ck2 with | BaseLic -> ck1 | On(x,sck) -> On(x,replace_base sck ck2) @@ -436,20 +436,20 @@ let (create_condact_body: local_ctx -> Lic.static_arg list -> Lic.node_body * va -> node_key,c | _ -> assert false in - let cond_exp, inputs = + let cond_exp, inputs = match List.map (val_exp_of_var_info lxm) lctx.node.Lic.inlist_eff with [] -> assert false | x::t -> x,t - in + in let outputs_clk = List.map (fun var -> snd var.var_clock_eff) lctx.node.Lic.outlist_eff in let left = List.map (fun x -> LeftVarLic (x,lxm)) lctx.node.Lic.outlist_eff in - let node_out_type_list = - List.map (fun x -> x.Lic.var_type_eff) lctx.node.Lic.outlist_eff + let node_out_type_list = + List.map (fun x -> x.Lic.var_type_eff) lctx.node.Lic.outlist_eff in let true_cc = ("Lustre","true") in let i0 = List.hd lctx.node.Lic.inlist_eff in let i0_clk = Lic.On((true_cc, i0.var_name_eff,Bool_type_eff), snd i0.var_clock_eff) in - let inputs_when_i0 = List.map (add_when i0_clk) inputs in + let inputs_when_i0 = List.map (add_when i0_clk) inputs in let outputs_clk_when_i0 = (* replace baseLic by i0_clk *) List.map (replace_base i0_clk) outputs_clk in @@ -458,8 +458,8 @@ let (create_condact_body: local_ctx -> Lic.static_arg list -> Lic.node_body * va in let then_exp = add_current then_exp i0_clk outputs_clk in let const_exp = val_exp_of_const c in - let out_exp = match lctx.node.Lic.outlist_eff with - [o] -> val_exp_of_var_info lxm o + let out_exp = match lctx.node.Lic.outlist_eff with + [o] -> val_exp_of_var_info lxm o | _ -> tuple_to_val_exp lxm (List.map (val_exp_of_var_info lxm) lctx.node.Lic.outlist_eff) in @@ -477,41 +477,41 @@ let (create_merge_body: local_ctx -> Lic.static_arg list -> Lic.node_body * var_ let (create_meta_op_body: local_ctx -> Lic.node_key -> Lic.node_body * var_info list) = fun lctx (nk,sargs) -> match nk with - | "Lustre", "fill" - | "Lustre", "red" + | "Lustre", "fold" + | "Lustre", "fill" + | "Lustre", "red" | "Lustre", "fillred" -> create_fillred_body lctx sargs | "Lustre", "map" -> create_map_body lctx sargs | "Lustre", "boolred" -> ( let (i,j,k) = - match sargs with + match sargs with | [ConstStaticArgLic(_, Int_const_eff i); ConstStaticArgLic(_, Int_const_eff j); ConstStaticArgLic(_, Int_const_eff k) - ] -> + ] -> (ios i,ios j,ios k) | _ -> assert false in - create_boolred_body lctx i j k + create_boolred_body lctx i j k ) | "Lustre", "diese" -> ( (* a diese is a particular kind of boolred: #(A,...,an) = boolred(0,1,n)([a1,...,an]) *) let n = List.length lctx.node.Lic.inlist_eff in - create_boolred_body lctx 0 1 n + create_boolred_body lctx 0 1 n ) | "Lustre", "nor" -> ( (* a nor is a particular kind of boolred too: nor(A,...,an) = boolred(0,0,n)([a1,...,an]) *) let n = List.length lctx.node.Lic.inlist_eff in - create_boolred_body lctx 0 0 n + create_boolred_body lctx 0 0 n ) | "Lustre", "condact" -> create_condact_body lctx sargs | "Lustre", "merge" -> create_merge_body lctx sargs | _,_ -> assert false - let rec (node : local_ctx -> Lic.node_exp -> bool -> Lic.node_exp) = fun lctx n only_boolred -> let sonk = Lic.string_of_node_key in @@ -522,26 +522,26 @@ let rec (node : local_ctx -> Lic.node_exp -> bool -> Lic.node_exp) = if only_boolred && (fst n.node_key_eff) <> ("Lustre", "boolred") then n else let nk = n.node_key_eff in let nbody, nlocs = create_meta_op_body lctx nk in - { n with + { n with def_eff = BodyLic nbody; loclist_eff = Some nlocs; } - | ExternLic + | ExternLic | AbstractLic None -> n | AbstractLic (Some pn) -> { n with def_eff = AbstractLic (Some (node lctx pn only_boolred)) } | BodyLic _b -> n - + (* exported *) let (doit : LicPrg.t -> LicPrg.t) = - fun inprg -> + fun inprg -> let outprg = LicPrg.empty in (* types and constants do not change *) let outprg = LicPrg.fold_types LicPrg.add_type inprg outprg in let outprg = LicPrg.fold_consts LicPrg.add_const inprg outprg in (* transform nodes *) - let (do_node : Lic.node_key -> Lic.node_exp -> LicPrg.t -> LicPrg.t) = - fun nk ne outprg -> + let (do_node : Lic.node_key -> Lic.node_exp -> LicPrg.t -> LicPrg.t) = + fun nk ne outprg -> let lctx = { node = ne; prg = inprg; @@ -555,14 +555,14 @@ let (doit : LicPrg.t -> LicPrg.t) = (* exported *) let (doit_boolred : LicPrg.t -> LicPrg.t) = - fun inprg -> + fun inprg -> let outprg = LicPrg.empty in (* types and constants do not change *) let outprg = LicPrg.fold_types LicPrg.add_type inprg outprg in let outprg = LicPrg.fold_consts LicPrg.add_const inprg outprg in (* transform nodes *) - let (do_node : Lic.node_key -> Lic.node_exp -> LicPrg.t -> LicPrg.t) = - fun nk ne outprg -> + let (do_node : Lic.node_key -> Lic.node_exp -> LicPrg.t -> LicPrg.t) = + fun nk ne outprg -> let lctx = { node = ne; prg = inprg; diff --git a/lib/licMetaOp.ml b/lib/licMetaOp.ml index 52da36cf0fe1d1590a79b59cbe01521172b5e79e..f0b151e485bb7804ebc751f75f062ad77f41b957 100644 --- a/lib/licMetaOp.ml +++ b/lib/licMetaOp.ml @@ -1,4 +1,4 @@ -(* Time-stamp: <modified the 29/08/2019 (at 16:16) by Erwan Jahier> *) +(* Time-stamp: <modified the 15/04/2024 (at 11:58) by Erwan Jahier> *) (* *) @@ -26,23 +26,24 @@ let get_node_and_int_const (lxm: Lxm.t) (sargs: Lic.static_arg list) raise (Compile_error(lxm, msg)) (* transforme en array une variable *) -let var_to_array (c:int) (vi: Lic.var_info) : Lic.var_info = +let var_to_array (c:int) (vi: Lic.var_info) : Lic.var_info = { vi with var_type_eff = Array_type_eff(vi.var_type_eff,c) } (* -On a éventuellement besoin du node_exp des args +On a éventuellement besoin du node_exp des args *) let rec do_node (nk2nd: Lic.node_key -> Lic.node_exp) (nk: Lic.node_key) (lxm: Lxm.t) : (Lic.node_exp) = - let (pk,id) = fst nk in + let (pk,id) = fst nk in match (pk, id) with | ("Lustre", "map") -> do_map nk2nd nk lxm | ("Lustre", "red") | ("Lustre", "fill") + | ("Lustre", "fold") | ("Lustre", "fillred") -> do_fillred nk2nd nk lxm | ("Lustre", "boolred") -> do_boolred nk2nd nk lxm | ("Lustre", "condact") -> do_condact nk2nd nk lxm @@ -51,10 +52,10 @@ let rec do_node (*-------------------------------------------------------------------- MAP ---------------------------------------------------------------------- - Given : + Given : - A node n of type: a_1 * ... * a_n -> b_1 * ... * b_k - A (int) const c - Gen a node of type : a_1^c * ... * a_n^c -> b_1^c * ... * b_k^c + Gen a node of type : a_1^c * ... * a_n^c -> b_1^c * ... * b_k^c --------------------------------------------------------------------*) and do_map nk2nd nk lxm = let sargs = snd nk in @@ -68,17 +69,17 @@ and do_map nk2nd nk lxm = outlist_eff = List.map (var_to_array c) outs; loclist_eff = None; def_eff = MetaOpLic; - has_mem_eff = nd.has_mem_eff; - is_safe_eff = nd.is_safe_eff; + has_mem_eff = nd.has_mem_eff; + is_safe_eff = nd.is_safe_eff; lxm = lxm; } (*-------------------------------------------------------------------- FILLRED ---------------------------------------------------------------------- - Given : + Given : - A node : aa * a_1 * ... * a_n -> aa * b_1 * ... * b_k - An int c - Gen a node : aa * a_1^c * ... * a_n^c -> aa * b_1^c * ... * b_k^c + Gen a node : aa * a_1^c * ... * a_n^c -> aa * b_1^c * ... * b_k^c --------------------------------------------------------------------*) and do_fillred nk2nd nk lxm = let sargs = snd nk in @@ -99,24 +100,24 @@ and do_fillred nk2nd nk lxm = (LicDump.string_of_type_eff false t2) in raise (Compile_error(lxm, msg)) - else + else { node_key_eff = nk; inlist_eff = ins'; outlist_eff = outs'; loclist_eff = None; def_eff = MetaOpLic; - has_mem_eff = nd.has_mem_eff; - is_safe_eff = nd.is_safe_eff; + has_mem_eff = nd.has_mem_eff; + is_safe_eff = nd.is_safe_eff; lxm = lxm; } (*-------------------------------------------------------------------- CONDACT ---------------------------------------------------------------------- - Given : + Given : - A node n of type: a_1 * ... * a_n -> b_1 * ... * b_k - A (tuple) const: b_1 * ... * b_k - Gen a node of type : bool * a_1 * ... * a_n -> b_1 * ... * b_k + Gen a node of type : bool * a_1 * ... * a_n -> b_1 * ... * b_k ---------------------------------------------------------------------*) (* nb : @@ -138,7 +139,7 @@ tel is it a good idea? *) and (do_condact : (Lic.node_key -> Lic.node_exp) -> node_key -> Lxm.t -> Lic.node_exp) = -fun nk2nd nk lxm -> +fun nk2nd nk lxm -> try let sargs = snd nk in let np, dflt = @@ -155,7 +156,7 @@ fun nk2nd nk lxm -> let out_types = List.map (fun x -> x.var_type_eff) outlist in let matches = try UnifyType.is_matched out_types dflt_types - with UnifyType.Match_failed msg -> + with UnifyType.Match_failed msg -> raise (Compile_error(lxm, "in condact default output "^msg)) in let out_types = Lic.apply_type_matches matches out_types in @@ -175,8 +176,8 @@ fun nk2nd nk lxm -> outlist_eff = outs; loclist_eff = None; def_eff = MetaOpLic; - has_mem_eff = ne.has_mem_eff; - is_safe_eff = ne.is_safe_eff; + has_mem_eff = ne.has_mem_eff; + is_safe_eff = ne.is_safe_eff; lxm = lxm; } with @@ -186,9 +187,9 @@ fun nk2nd nk lxm -> (*-------------------------------------------------------------------- BOOLRED ---------------------------------------------------------------------- - Given - - 3 integer constant i, j, k - + Given + - 3 integer constant i, j, k + returns the profile bool^k -> bool ---------------------------------------------------------------------*) and do_boolred _nk2nd nk lxm = @@ -214,4 +215,3 @@ and do_boolred _nk2nd nk lxm = is_safe_eff = true; lxm = lxm; } - diff --git a/lv6-ref-man/lv6-ref-man.tex b/lv6-ref-man/lv6-ref-man.tex index 34212a914f618dafd3adea6f222e96a4a34e61ca..3008d86efb8beed972fc92e5b58bad21b4be11b0 100644 --- a/lv6-ref-man/lv6-ref-man.tex +++ b/lv6-ref-man/lv6-ref-man.tex @@ -1246,6 +1246,7 @@ Here are a few examples of array declarations and definitions. \newcommand{\reduceop}{{\tt red}} % Reduce \newcommand{\redop}{{\tt red}} % Reduce \newcommand{\fillredop}{{\tt fillred}} % fill/reduce +\newcommand{\foldop}{{\tt fold}} % f \newcommand{\boolredop}{{\tt boolred}} %Boolean reduce @@ -1439,7 +1440,7 @@ $\forall i = 0 \cdots \mbox{\tt n}-1$, %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% %%%%% FILLRED ITERATOR -\subsection{From arrays to arrays: \fillredop} +\subsection{From arrays to arrays: \fillredop (a.k.a. \foldop} \label{fillred-iterator}