Added partial application for iterators
For instance: ... = map<<n>> (f<<se>>)((t1, t1'))(t2, t3) is translated to: for(int i =...) ... = f(t1, t1', t2[i], t3[i])
This commit is contained in:
parent
35775c4131
commit
b1b8e103f2
30 changed files with 159 additions and 77 deletions
|
@ -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
|
||||
|
|
|
@ -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) ->
|
||||
|
|
|
@ -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) ->
|
||||
|
|
|
@ -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
|
||||
|
|
|
@ -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) ->
|
||||
|
|
|
@ -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;
|
||||
|
|
|
@ -121,7 +121,9 @@ rule token = parse
|
|||
| [' ' '\t'] + { token lexbuf }
|
||||
| "." {DOT}
|
||||
| "(" {LPAREN}
|
||||
| "((" {LPARENLPAREN}
|
||||
| ")" {RPAREN}
|
||||
| "))" {RPARENRPAREN}
|
||||
| "*" { STAR }
|
||||
| "{" {LBRACE}
|
||||
| "}" {RBRACE}
|
||||
|
|
|
@ -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 <string> Constructor
|
||||
%token <string> 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)))]
|
||||
|
|
|
@ -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 }
|
||||
|
|
|
@ -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
|
||||
|
|
|
@ -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
|
||||
|
|
|
@ -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 =
|
||||
|
|
|
@ -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)
|
||||
|
|
|
@ -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 _
|
||||
|
|
|
@ -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
|
||||
|
|
|
@ -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)
|
||||
|
|
|
@ -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 <<n>> (exp, exp...) reset ident *)
|
||||
|
||||
and app = { a_op: op; a_params: static_exp list; a_unsafe: bool }
|
||||
|
|
|
@ -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
|
||||
|
||||
|
|
|
@ -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
|
||||
|
|
|
@ -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
|
||||
|
||||
|
|
|
@ -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
|
||||
|
|
|
@ -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
|
||||
|
|
|
@ -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) =
|
||||
|
|
|
@ -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
|
||||
|
||||
|
|
|
@ -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
|
||||
|
||||
|
|
|
@ -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 =
|
||||
|
|
|
@ -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)
|
||||
|
|
|
@ -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
|
||||
|
|
|
@ -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
|
||||
|
||||
|
|
|
@ -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
|
||||
|
||||
|
|
Loading…
Reference in a new issue