diff --git a/compiler/heptagon/analysis/causality.ml b/compiler/heptagon/analysis/causality.ml index 289b470..f4582d1 100644 --- a/compiler/heptagon/analysis/causality.ml +++ b/compiler/heptagon/analysis/causality.ml @@ -106,8 +106,8 @@ let rec typing e = | Estruct(l) -> let l = List.map (fun (_, e) -> typing e) l in candlist l - | Eiterator (_, _, _, e_list, _) -> - ctuplelist (List.map typing e_list) + | Eiterator (_, _, _, pe_list, e_list, _) -> + ctuplelist (List.map typing (pe_list@e_list)) | Ewhen (e, c, ce) -> let t = typing e in let tc = typing ce in diff --git a/compiler/heptagon/analysis/initialization.ml b/compiler/heptagon/analysis/initialization.ml index 159b2ba..9232a1f 100644 --- a/compiler/heptagon/analysis/initialization.ml +++ b/compiler/heptagon/analysis/initialization.ml @@ -246,7 +246,8 @@ let rec typing h e = List.fold_left (fun acc (_, e) -> imax acc (itype (typing h e))) izero l in skeleton i e.e_ty - | Eiterator (_, _, _, e_list, _) -> + | Eiterator (_, _, _, pe_list, e_list, _) -> + List.iter (fun e -> initialized_exp h e) pe_list; List.iter (fun e -> initialized_exp h e) e_list; skeleton izero e.e_ty | Ewhen (e, _, ce) -> diff --git a/compiler/heptagon/analysis/typing.ml b/compiler/heptagon/analysis/typing.ml index 429660b..e59f7b2 100644 --- a/compiler/heptagon/analysis/typing.ml +++ b/compiler/heptagon/analysis/typing.ml @@ -519,7 +519,7 @@ let rec typing const_env h e = | Eiterator (it, ({ a_op = (Enode f | Efun f); a_params = params } as app), - n, e_list, reset) -> + n, pe_list, e_list, reset) -> let ty_desc = find_value f in let op, expected_ty_list, result_ty_list = kind f ty_desc in let node_params = @@ -529,6 +529,11 @@ let rec typing const_env h e = List.map (subst_type_vars m) expected_ty_list in let result_ty_list = List.map (subst_type_vars m) result_ty_list in let typed_n = expect_static_exp const_env (Tid Initial.pint) n in + (*typing of partial application*) + let p_ty_list, expected_ty_list = + Misc.split_at (List.length pe_list) expected_ty_list in + let typed_pe_list = typing_args const_env h p_ty_list pe_list in + (*typing of other arguments*) let ty, typed_e_list = typing_iterator const_env h it n expected_ty_list result_ty_list e_list in let typed_params = typing_node_params const_env @@ -540,7 +545,7 @@ let rec typing const_env h e = List.iter add_size_constraint size_constrs; (* return the type *) Eiterator(it, { app with a_op = op; a_params = typed_params } - , typed_n, typed_e_list, reset), ty + , typed_n, typed_pe_list, typed_e_list, reset), ty | Eiterator _ -> assert false | Ewhen (e, c, ce) -> diff --git a/compiler/heptagon/hept_mapfold.ml b/compiler/heptagon/hept_mapfold.ml index 3d730ea..65bde82 100644 --- a/compiler/heptagon/hept_mapfold.ml +++ b/compiler/heptagon/hept_mapfold.ml @@ -129,12 +129,13 @@ and edesc funs acc ed = match ed with let args, acc = mapfold (exp_it funs) acc args in let reset, acc = optional_wacc (exp_it funs) acc reset in Eapp (app, args, reset), acc - | Eiterator (i, app, param, args, reset) -> + | Eiterator (i, app, param, pargs, args, reset) -> let app, acc = app_it funs acc app in let param, acc = static_exp_it funs.global_funs acc param in + let pargs, acc = mapfold (exp_it funs) acc pargs in let args, acc = mapfold (exp_it funs) acc args in let reset, acc = optional_wacc (exp_it funs) acc reset in - Eiterator (i, app, param, args, reset), acc + Eiterator (i, app, param, pargs, args, reset), acc | Ewhen (e, c, n) -> let e, acc = exp_it funs acc e in Ewhen (e, c, n), acc diff --git a/compiler/heptagon/hept_printer.ml b/compiler/heptagon/hept_printer.ml index 7085fc5..7674de6 100644 --- a/compiler/heptagon/hept_printer.ml +++ b/compiler/heptagon/hept_printer.ml @@ -105,11 +105,12 @@ and print_exp_desc ff = function print_app (app, args) print_every reset | Estruct(f_e_list) -> print_record (print_couple print_qualname print_exp """ = """) ff f_e_list - | Eiterator (it, f, param, args, reset) -> - fprintf ff "@[<2>(%s (%a)<<%a>>)@,%a@]%a" + | Eiterator (it, f, param, pargs, args, reset) -> + fprintf ff "@[<2>(%s (%a)<<%a>>)@,(%a)%a@]%a" (iterator_to_string it) print_app (f, []) print_static_exp param + print_exp_tuple pargs print_exp_tuple args print_every reset | Ewhen (e, c, ec) -> diff --git a/compiler/heptagon/heptagon.ml b/compiler/heptagon/heptagon.ml index d702cbf..f18f793 100644 --- a/compiler/heptagon/heptagon.ml +++ b/compiler/heptagon/heptagon.ml @@ -36,7 +36,8 @@ and desc = | Econst of static_exp | Evar of var_ident | Elast of var_ident - | Epre of static_exp option * exp (* the static_exp purpose is the initialization of the mem_var *) + (* the static_exp purpose is the initialization of the mem_var *) + | Epre of static_exp option * exp | Efby of exp * exp | Estruct of (field_name * exp) list | Ewhen of exp * constructor_name * exp @@ -44,7 +45,8 @@ and desc = | Emerge of exp * (constructor_name * exp) list (** merge ident (Constructor -> exp)+ *) | Eapp of app * exp list * exp option - | Eiterator of iterator_type * app * static_exp * exp list * exp option + | Eiterator of iterator_type * app * static_exp + * exp list * exp list * exp option and app = { a_op : op; diff --git a/compiler/heptagon/parsing/hept_lexer.mll b/compiler/heptagon/parsing/hept_lexer.mll index 9f035a9..3c8dd74 100644 --- a/compiler/heptagon/parsing/hept_lexer.mll +++ b/compiler/heptagon/parsing/hept_lexer.mll @@ -121,7 +121,9 @@ rule token = parse | [' ' '\t'] + { token lexbuf } | "." {DOT} | "(" {LPAREN} + | "((" {LPARENLPAREN} | ")" {RPAREN} + | "))" {RPARENRPAREN} | "*" { STAR } | "{" {LBRACE} | "}" {RBRACE} diff --git a/compiler/heptagon/parsing/hept_parser.mly b/compiler/heptagon/parsing/hept_parser.mly index caf13f6..3a783d9 100644 --- a/compiler/heptagon/parsing/hept_parser.mly +++ b/compiler/heptagon/parsing/hept_parser.mly @@ -9,7 +9,7 @@ open Hept_parsetree %} -%token DOT LPAREN RPAREN LBRACE RBRACE COLON SEMICOL +%token DOT LPAREN LPARENLPAREN RPAREN RPARENRPAREN LBRACE RBRACE COLON SEMICOL %token EQUAL EQUALEQUAL LESS_GREATER BARBAR COMMA BAR ARROW LET TEL %token Constructor %token IDENT @@ -96,6 +96,10 @@ slist(S, x) : | {[]} | x=x {[x]} | x=x S r=slist(S,x) {x::r} +/* Separated list with delimiter*/ +delim_slist(S, L, R, x) : + | {[]} + | L l=slist(S, x) R {l} /*Separated Nonempty list */ snlist(S, x) : | x=x {[x]} @@ -503,11 +507,15 @@ _exp: | exp AROBASE exp { mk_call Econcat [$1; $3] } /*Iterators*/ - | iterator qualname DOUBLE_LESS simple_exp DOUBLE_GREATER LPAREN exps RPAREN - { mk_iterator_call $1 $2 [] $4 $7 } - | iterator LPAREN qualname DOUBLE_LESS array_exp_list DOUBLE_GREATER - RPAREN DOUBLE_LESS simple_exp DOUBLE_GREATER LPAREN exps RPAREN - { mk_iterator_call $1 $3 $5 $9 $12 } + | it=iterator DOUBLE_LESS n=simple_exp DOUBLE_GREATER q=qualname + pargs=delim_slist(COMMA, LPARENLPAREN, RPARENRPAREN, exp) + LPAREN args=exps RPAREN + { mk_iterator_call it q [] n pargs args } + | it=iterator DOUBLE_LESS n=simple_exp DOUBLE_GREATER + LPAREN q=qualname DOUBLE_LESS sa=array_exp_list DOUBLE_GREATER RPAREN + pargs=delim_slist(COMMA, LPARENLPAREN, RPARENRPAREN, exp) + LPAREN args=exps RPAREN + { mk_iterator_call it q sa n pargs args } /*Records operators */ | LBRACE simple_exp WITH DOT c=qualname EQUAL exp RBRACE { mk_call ~params:[mk_field_exp c (Loc($startpos(c),$endpos(c)))] diff --git a/compiler/heptagon/parsing/hept_parsetree.ml b/compiler/heptagon/parsing/hept_parsetree.ml index ad2e5c1..cac2ae4 100644 --- a/compiler/heptagon/parsing/hept_parsetree.ml +++ b/compiler/heptagon/parsing/hept_parsetree.ml @@ -72,7 +72,7 @@ and edesc = | Efby of exp * exp | Estruct of (qualname * exp) list | Eapp of app * exp list - | Eiterator of iterator_type * app * exp * exp list + | Eiterator of iterator_type * app * exp * exp list * exp list | Ewhen of exp * constructor_name * var_name | Emerge of var_name * (constructor_name * exp) list @@ -222,8 +222,8 @@ let mk_call ?(params=[]) op exps = let mk_op_call ?(params=[]) s exps = mk_call ~params:params (Efun (Q (Names.pervasives_qn s))) exps -let mk_iterator_call it ln params n exps = - Eiterator (it, mk_app (Enode ln) params, n, exps) +let mk_iterator_call it ln params n pexps exps = + Eiterator (it, mk_app (Enode ln) params, n, pexps, exps) let mk_static_exp desc loc = { se_desc = desc; se_loc = loc } diff --git a/compiler/heptagon/parsing/hept_parsetree_mapfold.ml b/compiler/heptagon/parsing/hept_parsetree_mapfold.ml index 912fefc..afe872f 100644 --- a/compiler/heptagon/parsing/hept_parsetree_mapfold.ml +++ b/compiler/heptagon/parsing/hept_parsetree_mapfold.ml @@ -146,11 +146,12 @@ and edesc funs acc ed = match ed with let app, acc = app_it funs acc app in let args, acc = mapfold (exp_it funs) acc args in Eapp (app, args), acc - | Eiterator (i, app, param, args) -> + | Eiterator (i, app, param, pargs, args) -> let app, acc = app_it funs acc app in let param, acc = exp_it funs acc param in + let pargs, acc = mapfold (exp_it funs) acc pargs in let args, acc = mapfold (exp_it funs) acc args in - Eiterator (i, app, param, args), acc + Eiterator (i, app, param, pargs, args), acc and app_it funs acc a = funs.app funs acc a diff --git a/compiler/heptagon/parsing/hept_scoping.ml b/compiler/heptagon/parsing/hept_scoping.ml index 9789696..3d14b38 100644 --- a/compiler/heptagon/parsing/hept_scoping.ml +++ b/compiler/heptagon/parsing/hept_scoping.ml @@ -249,13 +249,14 @@ and translate_desc loc env = function let app = Heptagon.mk_app ~params:params (translate_op op) in Heptagon.Eapp (app, e_list, None) - | Eiterator (it, { a_op = op; a_params = params }, n, e_list) -> + | Eiterator (it, { a_op = op; a_params = params }, n, pe_list, e_list) -> let e_list = List.map (translate_exp env) e_list in + let pe_list = List.map (translate_exp env) pe_list in let n = expect_static_exp n in let params = List.map (expect_static_exp) params in let app = Heptagon.mk_app ~params:params (translate_op op) in Heptagon.Eiterator (translate_iterator_type it, - app, n, e_list, None) + app, n, pe_list, e_list, None) | Ewhen (e, c, ce) -> let e = translate_exp env e in let c = qualify_constrs c in diff --git a/compiler/heptagon/transformations/every.ml b/compiler/heptagon/transformations/every.ml index bcf6ae0..836f9d9 100644 --- a/compiler/heptagon/transformations/every.ml +++ b/compiler/heptagon/transformations/every.ml @@ -18,9 +18,10 @@ let edesc funs (v,acc_eq_list) ed = | Eapp (op, e_list, Some re) when not (is_var re) -> let re, vre, eqre = Reset.bool_var_from_exp re in Eapp(op, e_list, Some re), (vre::v, eqre::acc_eq_list) - | Eiterator(it, op, n, e_list, Some re) when not (is_var re) -> + | Eiterator(it, op, n, pe_list, e_list, Some re) when not (is_var re) -> let re, vre, eqre = Reset.bool_var_from_exp re in - Eiterator(it, op, n, e_list, Some re), (vre::v, eqre::acc_eq_list) + Eiterator(it, op, n, pe_list, e_list, Some re), + (vre::v, eqre::acc_eq_list) | _ -> ed, (v, acc_eq_list) let program p = diff --git a/compiler/heptagon/transformations/reset.ml b/compiler/heptagon/transformations/reset.ml index 8720a43..d000d0c 100644 --- a/compiler/heptagon/transformations/reset.ml +++ b/compiler/heptagon/transformations/reset.ml @@ -66,8 +66,8 @@ let edesc funs (res,s) ed = ifres res e1 e2 | Eapp({ a_op = Enode _ } as op, e_list, re) -> Eapp(op, e_list, merge_resets res re) - | Eiterator(it, ({ a_op = Enode _ } as op), n, e_list, re) -> - Eiterator(it, op, n, e_list, merge_resets res re) + | Eiterator(it, ({ a_op = Enode _ } as op), n, pe_list, e_list, re) -> + Eiterator(it, op, n, pe_list, e_list, merge_resets res re) | _ -> ed in ed, (res,s) diff --git a/compiler/main/hept2mls.ml b/compiler/main/hept2mls.ml index 8b8c313..e4548f8 100644 --- a/compiler/main/hept2mls.ml +++ b/compiler/main/hept2mls.ml @@ -237,10 +237,11 @@ let rec translate env mk_exp ~loc:loc ~ty:ty (Eapp (translate_app app, List.map (translate env) e_list, translate_reset reset)) - | Heptagon.Eiterator(it, app, n, e_list, reset) -> + | Heptagon.Eiterator(it, app, n, pe_list, e_list, reset) -> mk_exp ~loc:loc ~ty:ty (Eiterator (translate_iterator_type it, translate_app app, n, + List.map (translate env) pe_list, List.map (translate env) e_list, translate_reset reset)) | Heptagon.Efby _ diff --git a/compiler/main/mls2obc.ml b/compiler/main/mls2obc.ml index 33ae13b..adafc5c 100644 --- a/compiler/main/mls2obc.ml +++ b/compiler/main/mls2obc.ml @@ -272,12 +272,15 @@ let rec translate_eq map call_context { Minils.eq_lhs = pat; Minils.eq_rhs = e } | _, _ -> action @ s) in v' @ v, si'@si, j'@j, s - | pat, Minils.Eiterator (it, app, n, e_list, reset) -> + | pat, Minils.Eiterator (it, app, n, pe_list, e_list, reset) -> let name_list = translate_pat map pat in + let p_list = List.map (translate map) pe_list in let c_list = List.map (translate map) e_list in let x, xd = fresh_it () in - let call_context = Some { oa_index = mk_pattern_int (Lvar x); oa_size = n} in - let si', j', action = translate_iterator map call_context it name_list app loc n x xd c_list e.Minils.e_ty in + let call_context = + Some { oa_index = mk_pattern_int (Lvar x); oa_size = n} in + let si', j', action = translate_iterator map call_context it + name_list app loc n x xd p_list c_list e.Minils.e_ty in let action = List.map (Control.control map ck) action in let s = (match reset, app.Minils.a_op with @@ -303,7 +306,8 @@ and mk_node_call map call_context app loc name_list args ty = [], [], [], [Aassgn(List.hd name_list, e)] | Minils.Enode f when Itfusion.is_anon_node f -> - let add_input env vd = Env.add vd.Minils.v_ident (mk_pattern vd.Minils.v_type (Lvar vd.Minils.v_ident)) env in + let add_input env vd = Env.add vd.Minils.v_ident + (mk_pattern vd.Minils.v_type (Lvar vd.Minils.v_ident)) env in let build env vd a = Env.add vd.Minils.v_ident a env in let subst_act_list env act_list = let exp funs env e = match e.e_desc with @@ -341,26 +345,33 @@ and mk_node_call map call_context app loc name_list args ty = [], si, [obj], s | _ -> assert false -and translate_iterator map call_context it name_list app loc n x xd c_list ty = +and translate_iterator map call_context it name_list + app loc n x xd p_list c_list ty = let unarray ty = match ty with | Tarray (t,_) -> t - | _ -> Format.eprintf "%a" Global_printer.print_type ty; internal_error "mls2obc" 6 + | _ -> + Format.eprintf "%a" Global_printer.print_type ty; + internal_error "mls2obc" 6 in let array_of_output name_list ty_list = - List.map2 (fun l ty -> mk_pattern ty (Larray (l, mk_evar_int x))) name_list ty_list + List.map2 (fun l ty -> mk_pattern ty (Larray (l, mk_evar_int x))) + name_list ty_list in - let array_of_input c_list = List.map (array_elt_of_exp (mk_pattern_int (Lvar x))) c_list in + let array_of_input c_list = + List.map (array_elt_of_exp (mk_pattern_int (Lvar x))) c_list in match it with | Minils.Imap -> let c_list = array_of_input c_list in let ty_list = List.map unarray (Types.unprod ty) in let name_list = array_of_output name_list ty_list in let node_out_ty = Types.prod ty_list in - let v, si, j, action = mk_node_call map call_context app loc name_list c_list node_out_ty in + let v, si, j, action = mk_node_call map call_context + app loc name_list (p_list@c_list) node_out_ty in let v = translate_var_dec v in let b = mk_block ~locals:v action in let bi = mk_block si in - [Afor (xd, mk_static_int 0, n, bi)], j, [Afor (xd, mk_static_int 0, n, b)] + [Afor (xd, mk_static_int 0, n, bi)], j, + [Afor (xd, mk_static_int 0, n, b)] | Minils.Imapfold -> let (c_list, acc_in) = split_last c_list in @@ -370,37 +381,44 @@ and translate_iterator map call_context it name_list app loc n x xd c_list ty = let (name_list, acc_out) = Misc.split_last name_list in let name_list = array_of_output name_list ty_name_list in let node_out_ty = Types.prod ty_list in - let v, si, j, action = mk_node_call map call_context app loc (name_list @ [ acc_out ]) - (c_list @ [ mk_exp acc_out.pat_ty (Epattern acc_out) ]) node_out_ty + let v, si, j, action = mk_node_call map call_context app loc + (name_list @ [ acc_out ]) + (p_list @ c_list @ [ mk_exp acc_out.pat_ty (Epattern acc_out) ]) + node_out_ty in let v = translate_var_dec v in let b = mk_block ~locals:v action in let bi = mk_block si in - [Afor (xd, mk_static_int 0, n, bi)], j, [Aassgn (acc_out, acc_in); Afor (xd, mk_static_int 0, n, b)] + [Afor (xd, mk_static_int 0, n, bi)], j, + [Aassgn (acc_out, acc_in); Afor (xd, mk_static_int 0, n, b)] | Minils.Ifold -> let (c_list, acc_in) = split_last c_list in let c_list = array_of_input c_list in let acc_out = last_element name_list in let v, si, j, action = - mk_node_call map call_context app loc name_list (c_list @ [ mk_exp acc_out.pat_ty (Epattern acc_out) ]) ty + mk_node_call map call_context app loc name_list + (p_list @ c_list @ [ mk_exp acc_out.pat_ty (Epattern acc_out) ]) ty in let v = translate_var_dec v in let b = mk_block ~locals:v action in let bi = mk_block si in - [Afor (xd, mk_static_int 0, n, bi)], j, [ Aassgn (acc_out, acc_in); Afor (xd, mk_static_int 0, n, b) ] + [Afor (xd, mk_static_int 0, n, bi)], j, + [ Aassgn (acc_out, acc_in); Afor (xd, mk_static_int 0, n, b) ] | Minils.Ifoldi -> let (c_list, acc_in) = split_last c_list in let c_list = array_of_input c_list in let acc_out = last_element name_list in let v, si, j, action = mk_node_call map call_context app loc name_list - (c_list @ [ mk_evar_int x; mk_exp acc_out.pat_ty (Epattern acc_out) ]) ty + (p_list @ c_list @ [ mk_evar_int x; + mk_exp acc_out.pat_ty (Epattern acc_out) ]) ty in let v = translate_var_dec v in let b = mk_block ~locals:v action in let bi = mk_block si in - [Afor (xd, mk_static_int 0, n, bi)], j, [ Aassgn (acc_out, acc_in); Afor (xd, mk_static_int 0, n, b) ] + [Afor (xd, mk_static_int 0, n, bi)], j, + [ Aassgn (acc_out, acc_in); Afor (xd, mk_static_int 0, n, b) ] let remove m d_list = List.filter (fun { Minils.v_ident = n } -> not (List.mem_assoc n m)) d_list diff --git a/compiler/minils/analysis/clocking.ml b/compiler/minils/analysis/clocking.ml index b13cc27..981cf27 100644 --- a/compiler/minils/analysis/clocking.ml +++ b/compiler/minils/analysis/clocking.ml @@ -43,11 +43,15 @@ let rec typing h e = | None -> fresh_clock () | Some(reset) -> typ_of_name h reset in typing_op op args h e ck - | Eiterator (_, _, _, args, r) -> (* Typed exactly as a fun or a node... *) + (* Typed exactly as a fun or a node... *) + | Eiterator (_, _, _, pargs, args, r) -> let ck = match r with | None -> fresh_clock() | Some(reset) -> typ_of_name h reset - in (List.iter (expect h (Ck ck)) args; skeleton ck e.e_ty) + in + List.iter (expect h (Ck ck)) pargs; + List.iter (expect h (Ck ck)) args; + skeleton ck e.e_ty | Ewhen (e, c, n) -> let ck_n = typ_of_name h n in (expect h (skeleton ck_n e.e_ty) e; skeleton (Con (ck_n, c, n)) e.e_ty) diff --git a/compiler/minils/minils.ml b/compiler/minils/minils.ml index 97aa073..0daa021 100644 --- a/compiler/minils/minils.ml +++ b/compiler/minils/minils.ml @@ -58,7 +58,7 @@ and edesc = (** merge ident (Constructor -> exp)+ *) | Estruct of (field_name * exp) list (** { field=exp; ... } *) - | Eiterator of iterator_type * app * static_exp * exp list * var_ident option + | Eiterator of iterator_type * app * static_exp * exp list * exp list * var_ident option (** map f <> (exp, exp...) reset ident *) and app = { a_op: op; a_params: static_exp list; a_unsafe: bool } diff --git a/compiler/minils/mls_compare.ml b/compiler/minils/mls_compare.ml index 3425abb..b9b9a77 100644 --- a/compiler/minils/mls_compare.ml +++ b/compiler/minils/mls_compare.ml @@ -48,8 +48,8 @@ let rec exp_compare e1 e2 = let cr = compare fn1 fn2 in if cr <> 0 then cr else exp_compare e1 e2 in list_compare compare_fne fnel1 fnel2 - | Eiterator (it1, app1, se1, el1, vio1), - Eiterator (it2, app2, se2, el2, vio2) -> + | Eiterator (it1, app1, se1, pel1, el1, vio1), + Eiterator (it2, app2, se2, pel2, el2, vio2) -> let cr = compare it1 it2 in if cr <> 0 then cr else let cr = static_exp_compare se1 se2 in @@ -57,7 +57,9 @@ let rec exp_compare e1 e2 = let cr = app_compare app1 app2 in if cr <> 0 then cr else let cr = option_compare ident_compare vio1 vio2 in - if cr <> 0 then cr else list_compare exp_compare el1 el2 + if cr <> 0 then cr else + let cr = list_compare exp_compare pel1 pel2 in + if cr <> 0 then cr else list_compare exp_compare el1 el2 | Econst _, _ -> 1 diff --git a/compiler/minils/mls_mapfold.ml b/compiler/minils/mls_mapfold.ml index 314ff4b..d5e7aa2 100644 --- a/compiler/minils/mls_mapfold.ml +++ b/compiler/minils/mls_mapfold.ml @@ -73,11 +73,12 @@ and edesc funs acc ed = match ed with (n,e), acc in let n_e_list, acc = mapfold aux acc n_e_list in Estruct n_e_list, acc - | Eiterator (i, app, param, args, reset) -> + | Eiterator (i, app, param, pargs, args, reset) -> let app, acc = app_it funs acc app in let param, acc = static_exp_it funs.global_funs acc param in + let pargs, acc = mapfold (exp_it funs) acc pargs in let args, acc = mapfold (exp_it funs) acc args in - Eiterator (i, app, param, args, reset), acc + Eiterator (i, app, param, pargs, args, reset), acc and app_it funs acc a = funs.app funs acc a diff --git a/compiler/minils/mls_printer.ml b/compiler/minils/mls_printer.ml index 2ac3761..76bbe40 100644 --- a/compiler/minils/mls_printer.ml +++ b/compiler/minils/mls_printer.ml @@ -102,11 +102,12 @@ and print_exp_desc ff = function print_ident x print_tag_e_list tag_e_list | Estruct f_e_list -> print_record (print_couple print_qualname print_exp """ = """) ff f_e_list - | Eiterator (it, f, param, args, reset) -> - fprintf ff "@[<2>(%s (%a)<<%a>>)@,%a@]%a" + | Eiterator (it, f, param, pargs, args, reset) -> + fprintf ff "@[<2>(%s (%a)<<%a>>)@,(%a)%a@]%a" (iterator_to_string it) print_app (f, []) print_static_exp param + print_exp_tuple pargs print_exp_tuple args print_every reset diff --git a/compiler/minils/mls_utils.ml b/compiler/minils/mls_utils.ml index 5fbd79a..c58a57b 100644 --- a/compiler/minils/mls_utils.ml +++ b/compiler/minils/mls_utils.ml @@ -80,7 +80,7 @@ struct (* special cases *) let acc = match e.e_desc with | Evar x | Emerge(x,_) | Ewhen(_, _, x) - | Eapp(_, _, Some x) | Eiterator (_, _, _, _, Some x) -> + | Eapp(_, _, Some x) | Eiterator (_, _, _, _, _, Some x) -> add x acc | Efby(_, e) -> if is_left then diff --git a/compiler/minils/transformations/callgraph.ml b/compiler/minils/transformations/callgraph.ml index 5139331..1563ade 100644 --- a/compiler/minils/transformations/callgraph.ml +++ b/compiler/minils/transformations/callgraph.ml @@ -156,13 +156,15 @@ struct let op = Enode (node_for_params_call ln (instantiate m params)) in Eapp ({ app with a_op = op; a_params = [] }, e_list, r) | Eiterator(it, ({ a_op = Efun ln; a_params = params } as app), - n, e_list, r) -> + n, pe_list, e_list, r) -> let op = Efun (node_for_params_call ln (instantiate m params)) in - Eiterator(it, {app with a_op = op; a_params = [] }, n, e_list, r) + Eiterator(it, {app with a_op = op; a_params = [] }, + n, pe_list, e_list, r) | Eiterator(it, ({ a_op = Enode ln; a_params = params } as app), - n, e_list, r) -> + n, pe_list, e_list, r) -> let op = Enode (node_for_params_call ln (instantiate m params)) in - Eiterator(it,{app with a_op = op; a_params = [] }, n, e_list, r) + Eiterator(it,{app with a_op = op; a_params = [] }, + n, pe_list, e_list, r) | _ -> ed in ed, m @@ -269,7 +271,7 @@ let collect_node_calls ln = | Eapp ({ a_op = (Enode ln | Efun ln); a_params = params }, _, _) -> ed, add_called_node ln params acc | Eiterator(_, { a_op = (Enode ln | Efun ln); a_params = params }, - _, _, _) -> + _, _, _, _) -> ed, add_called_node ln params acc | _ -> raise Errors.Fallback in diff --git a/compiler/minils/transformations/introvars.ml b/compiler/minils/transformations/introvars.ml index f0c910b..e06f815 100644 --- a/compiler/minils/transformations/introvars.ml +++ b/compiler/minils/transformations/introvars.ml @@ -76,10 +76,12 @@ let rec exp e (eq_list, var_list) = match e.e_desc with intro_vars e_list (eq_list, var_list) in let fnel = List.combine (List.map fst fnel) e_list in Estruct fnel, eq_list, var_list - | Eiterator (it, app, se, e_list, vio) -> + | Eiterator (it, app, se, pe_list, e_list, vio) -> let (e_list, eq_list, var_list) = intro_vars e_list (eq_list, var_list) in - Eiterator (it, app, se, e_list, vio), eq_list, var_list in + let (pe_list, eq_list, var_list) = + intro_vars pe_list (eq_list, var_list) in + Eiterator (it, app, se, pe_list, e_list, vio), eq_list, var_list in ({ e with e_desc = e_desc; }, eq_list, var_list) and intro_vars e_list (eq_list, var_list) = diff --git a/compiler/minils/transformations/itfusion.ml b/compiler/minils/transformations/itfusion.ml index d36c3d6..4e4bcc7 100644 --- a/compiler/minils/transformations/itfusion.ml +++ b/compiler/minils/transformations/itfusion.ml @@ -89,7 +89,7 @@ let mk_call app acc_eq_list = let edesc funs acc ed = let ed, acc = Mls_mapfold.edesc funs acc ed in match ed with - | Eiterator(Imap, f, n, e_list, r) -> + | Eiterator(Imap, f, n, [], e_list, r) -> (** @return the list of inputs of the anonymous function, a list of created equations (the body of the function), the args for the call of f in the lambda, @@ -102,7 +102,7 @@ let edesc funs acc ed = o1, o2 = f (_v1, _v2, z') *) let mk_arg e (inp, acc_eq_list, largs, args, b) = match e.e_desc with - | Eiterator(Imap, g, m, local_args, _) when are_equal n m -> + | Eiterator(Imap, g, m, [], local_args, _) when are_equal n m -> let new_inp, e, acc_eq_list = mk_call g acc_eq_list in new_inp @ inp, acc_eq_list, e::largs, local_args @ args, true | _ -> @@ -122,7 +122,7 @@ let edesc funs acc ed = let eq = mk_equation (pat_of_vd_list outp) call in (* create the lambda *) let anon = mk_app (Enode (add_anon_node inp outp [] (eq::acc_eq_list))) in - Eiterator(Imap, anon, n, args, r), acc) + Eiterator(Imap, anon, n, [], args, r), acc) else ed, acc diff --git a/compiler/minils/transformations/normalize.ml b/compiler/minils/transformations/normalize.ml index 31aa9c6..e07cf94 100644 --- a/compiler/minils/transformations/normalize.ml +++ b/compiler/minils/transformations/normalize.ml @@ -199,7 +199,7 @@ let rec translate kind context e = | Eapp(app, e_list, r) -> let context, e_list = translate_app kind context app.a_op e_list in context, { e with e_desc = Eapp(app, e_list, r) } - | Eiterator (it, app, n, e_list, reset) -> + | Eiterator (it, app, n, pe_list, e_list, reset) -> (* normalize anonymous nodes *) (match app.a_op with | Enode f when Itfusion.is_anon_node f -> @@ -218,9 +218,11 @@ let rec translate kind context e = translate kind context e in Misc.mapfold_right add e_list context in + let context, pe_list = + translate_list function_args_kind context pe_list in let context, e_list = translate_iterator_arg_list context e_list in - context, { e with e_desc = Eiterator(it, app, n, + context, { e with e_desc = Eiterator(it, app, n, flatten_e_list pe_list, flatten_e_list e_list, reset) } in add context kind e diff --git a/compiler/minils/transformations/schedule.ml b/compiler/minils/transformations/schedule.ml index 10a4c94..6ccfc27 100644 --- a/compiler/minils/transformations/schedule.ml +++ b/compiler/minils/transformations/schedule.ml @@ -79,11 +79,11 @@ let eqs funs () eq_list = let edesc _ () = function | Eiterator(it, ({ a_op = Enode f } as app), - n, e_list, r) when Itfusion.is_anon_node f -> + n, [], e_list, r) when Itfusion.is_anon_node f -> let nd = Itfusion.find_anon_node f in let nd = { nd with n_equs = schedule nd.n_equs } in Itfusion.replace_anon_node f nd; - Eiterator(it, app, n, e_list, r), () + Eiterator(it, app, n, [], e_list, r), () | _ -> raise Errors.Fallback let program p = diff --git a/compiler/minils/transformations/singletonvars.ml b/compiler/minils/transformations/singletonvars.ml index 9e86558..0759da7 100644 --- a/compiler/minils/transformations/singletonvars.ml +++ b/compiler/minils/transformations/singletonvars.ml @@ -52,7 +52,7 @@ struct | Evar vi -> add_var_use vi use_counts | Emerge (vi, _) -> add_clock_use vi use_counts | Ewhen (_, _, vi) -> add_clock_use vi use_counts - | Eapp (_, _, Some vi) | Eiterator (_, _, _, _, Some vi) -> + | Eapp (_, _, Some vi) | Eiterator (_, _, _, _, _, Some vi) -> add_reset_use vi use_counts | _ -> use_counts in (edesc, use_counts) diff --git a/compiler/minils/transformations/tomato.ml b/compiler/minils/transformations/tomato.ml index 809d824..2873792 100644 --- a/compiler/minils/transformations/tomato.ml +++ b/compiler/minils/transformations/tomato.ml @@ -206,9 +206,12 @@ let behead e = List.split (List.map (fun (ln, e) -> ((ln, dummy_exp), e)) lne_list) in (Estruct lne_list, e_list) - | Eiterator (it, op, s, e_list, rst) -> + | Eiterator (it, op, s, pe_list, e_list, rst) -> let (rst, l) = encode_reset rst in - (Eiterator (it, op, s, [], rst), l @ e_list) in + (* count is the number of partial arguments *) + let count = mk_exp ~ty:Initial.tint + (Econst (Initial.mk_static_int (List.length pe_list))) in + (Eiterator (it, op, s, [], [], rst), count :: (pe_list @ l @ e_list)) in ({ e with e_desc = e_desc; }, children) let pat_name pat = @@ -425,11 +428,19 @@ let rec reconstruct input_type (env : PatEnv.t) = List.combine (List.map fst cnel) (List.tl e_list)) | Estruct fnel, e_list -> Estruct (List.combine (List.map fst fnel) e_list) - | Eiterator (it, app, se, [], rst), e_list -> + | Eiterator (it, app, se, [], [], rst), e_list -> + (* the first element is the number of partial arguments *) + let count, e_list = assert_1min e_list in + let c = (match count.e_desc with + | Econst { se_desc = Sint c } -> c + | _ -> assert false) + in + let pe_list, e_list = Misc.split_at c e_list in let rst, e_list = rst_of_e_list rst e_list in - Eiterator (it, app, se, e_list, rst) + Eiterator (it, app, se, pe_list, e_list, rst) - | (Eiterator (_, _, _, _ :: _, _) | Ewhen _ | Efby _ | Evar _ | Econst _) + | (Eiterator (_, _, _, _, _, _) | Ewhen _ + | Efby _ | Evar _ | Econst _) , _ -> assert false (* invariant *) in (mk_equation pat { head with e_desc = e_desc; } :: eq_list, mk_var_decs pat head.e_ty var_list) in diff --git a/compiler/utilities/misc.ml b/compiler/utilities/misc.ml index 089e08b..5c2d88c 100644 --- a/compiler/utilities/misc.ml +++ b/compiler/utilities/misc.ml @@ -64,6 +64,16 @@ let rec split_last = function let l, a = split_last l in v::l, a +exception List_too_short +(** [split_at n l] splits [l] in two after the [n]th value. + Raises List_too_short exception if the list is too short. *) +let rec split_at n l = match n, l with + | 0, l -> [], l + | _, [] -> raise List_too_short + | n, x::l -> + let l1, l2 = split_at (n-1) l in + x::l1, l2 + let remove x l = List.filter (fun y -> x <> y) l diff --git a/compiler/utilities/misc.mli b/compiler/utilities/misc.mli index 6f305e9..2daf31f 100644 --- a/compiler/utilities/misc.mli +++ b/compiler/utilities/misc.mli @@ -36,6 +36,11 @@ val last_element : 'a list -> 'a and the last element of the list .*) val split_last : 'a list -> ('a list * 'a) +exception List_too_short +(** [split_at n l] splits [l] in two after the [n]th value. + Raises List_too_short exception if the list is too short. *) +val split_at : int -> 'a list -> 'a list * 'a list + (** [remove x l] removes all occurrences of x from list l.*) val remove : 'a -> 'a list -> 'a list