From 3657018861cf362f36acc300ade5eb8909ad2a2b Mon Sep 17 00:00:00 2001 From: Adrien Guatto Date: Mon, 4 Jul 2011 12:42:40 +0200 Subject: [PATCH] Tomato: finer equivalence classes for Eapp and Eiterator when a reset variable is present. --- compiler/minils/transformations/tomato.ml | 69 +++++++++++++++++------ 1 file changed, 51 insertions(+), 18 deletions(-) diff --git a/compiler/minils/transformations/tomato.ml b/compiler/minils/transformations/tomato.ml index cb54e1d..a1bfd4a 100644 --- a/compiler/minils/transformations/tomato.ml +++ b/compiler/minils/transformations/tomato.ml @@ -165,24 +165,43 @@ let rec add_equation is_input (tenv : tom_env) eq = | Eextvalue w -> let class_id_list, w = extvalue is_input w [] in Eextvalue w, id, 0, class_id_list + | Eapp (app, w_list, rst) -> let class_id_list, w_list = mapfold_right (extvalue is_input) w_list [] in - Eapp (app, w_list, rst), id, 0, class_id_list + let class_id_list = match rst with + | None -> class_id_list + | Some rst -> + class_ref_of_var is_input (mk_extvalue ~ty:Initial.tbool (Wvar rst)) rst + :: class_id_list in + Eapp (app, w_list, optional (fun _ -> dummy_var) rst), id, 0, class_id_list + | Efby (seo, w) -> let class_id_list, w = extvalue is_input w [] in Efby (seo, w), id, 0, class_id_list + | Ewhen (e', cn, x) -> let ed, add_when, when_count, class_id_list = decompose e' in ed, (fun e' -> { e with e_desc = Ewhen (add_when e', cn, x) }), when_count + 1, class_ref_of_var is_input (mk_extvalue ~clock:e'.e_base_ck ~ty:Initial.tbool (Wvar x)) x :: class_id_list - | Emerge (vi, clause_list) -> + + | Emerge (x, clause_list) -> let class_id_list, clause_list = mapfold_right add_clause clause_list [] in - Emerge (vi, clause_list), id, 0, class_id_list + let x_id = + class_ref_of_var is_input (mk_extvalue ~clock:e.e_base_ck ~ty:Initial.tbool (Wvar x)) x in + Emerge (dummy_var, clause_list), id, 0, x_id :: class_id_list + | Eiterator (it, app, se, partial_w_list, w_list, rst) -> let class_id_list, partial_w_list = mapfold_right (extvalue is_input) partial_w_list [] in let class_id_list, w_list = mapfold_right (extvalue is_input) w_list class_id_list in - Eiterator (it, app, se, partial_w_list, w_list, rst), id, 0, class_id_list + let class_id_list = match rst with + | None -> class_id_list + | Some rst -> + class_ref_of_var is_input (mk_extvalue ~ty:Initial.tbool (Wvar rst)) rst + :: class_id_list in + Eiterator (it, app, se, partial_w_list, w_list, optional (fun _ -> dummy_var) rst), + id, 0, class_id_list + | Estruct field_val_list -> let class_id_list, field_val_list = mapfold_right add_clause field_val_list [] in Estruct field_val_list, id, 0, class_id_list @@ -277,38 +296,48 @@ let rec reconstruct (((tenv : tom_env), cenv) as env) = mk_equation pat e :: eq_list in IntMap.fold reconstruct_class cenv [] -and reconstruct_exp_desc ((tenv : tom_env), (cenv : eq_repr list IntMap.t) as env) headd children = - let reconstruct_clauses clause_list = +and reconstruct_exp_desc (((tenv : tom_env), (cenv : eq_repr list IntMap.t)) as env) headd children = + let reconstruct_clauses clause_list children = let (qn_list, w_list) = List.split clause_list in let w_list = reconstruct_extvalues env w_list children in List.combine qn_list w_list in match headd with + | Eextvalue w -> let w = assert_1 (reconstruct_extvalues env [w] children) in Eextvalue w + | Efby (ini, w) -> let w = assert_1 (reconstruct_extvalues env [w] children) in Efby (ini, w) - | Eapp (app, w_list, rst) -> - Eapp (app, reconstruct_extvalues env w_list children, optional (new_ident_for env) rst) + + | Eapp (app, w_list, rst_dummy) -> + let rst, children = match rst_dummy with + | None -> None, children + | Some _ -> Some (reconstruct_class_ref env (List.hd children)), List.tl children in + Eapp (app, reconstruct_extvalues env w_list children, optional extract_name rst) + | Ewhen _ -> assert false (* no Ewhen in exprs *) - | Emerge (ck_x, clause_list) -> - Emerge (new_ident_for env ck_x, reconstruct_clauses clause_list) + + | Emerge (x_ref, clause_list) -> + let x_ref, children = List.hd children, List.tl children in + Emerge (extract_name (reconstruct_class_ref env x_ref), + reconstruct_clauses clause_list children) + | Estruct field_val_list -> - let field_val_list = reconstruct_clauses field_val_list in + let field_val_list = reconstruct_clauses field_val_list children in Estruct field_val_list - | Eiterator (it, app, se, partial_w_list, w_list, rst) -> + + | Eiterator (it, app, se, partial_w_list, w_list, rst_dummy) -> + let rst, children = match rst_dummy with + | None -> None, children + | Some _ -> Some (reconstruct_class_ref env (List.hd children)), List.tl children in let total_w_list = reconstruct_extvalues env (partial_w_list @ w_list) children in let partial_w_list, w_list = split_at (List.length partial_w_list) total_w_list in - Eiterator (it, app, se, partial_w_list, w_list, optional (new_ident_for env) rst) + Eiterator (it, app, se, partial_w_list, w_list, optional extract_name rst) and reconstruct_extvalues env w_list children = - let extract_name w = match w.w_desc with - | Wvar x -> x - | _ -> invalid_arg "extract_name: not a var" - in - let rec reconstruct_extvalue w (children : class_ref list) = match w.w_desc with | Wconst _ -> w, children | Wvar _ -> @@ -331,6 +360,10 @@ and reconstruct_extvalues env w_list children = let (children, w_list) = List.fold_right consume w_list (List.rev children, []) in w_list +and extract_name w = match w.w_desc with + | Wvar x -> x + | _ -> invalid_arg "extract_name: not a var" + and reconstruct_class_ref (tenv, cenv) cr = match cr with | Cr_input w -> w | Cr_plain w ->