Heptc compiles again
AFor now expects expressions instead of static exps
This commit is contained in:
parent
c6991977a0
commit
c6aa63b444
24 changed files with 273 additions and 207 deletions
|
@ -101,12 +101,8 @@ and type_compare ty1 ty2 = match ty1, ty2 with
|
|||
| Tarray (ty1, se1), Tarray (ty2, se2) ->
|
||||
let cr = type_compare ty1 ty2 in
|
||||
if cr <> 0 then cr else static_exp_compare se1 se2
|
||||
| Tunit, Tunit -> 0
|
||||
| Tinvalid, _ | _, Tinvalid -> -1
|
||||
| Tprod _, _ -> 1
|
||||
| Tid _, Tprod _ -> -1
|
||||
| Tid _, _ -> 1
|
||||
| Tarray _, (Tprod _ | Tid _) -> -1
|
||||
| Tarray _, _ -> 1
|
||||
| Tmutable _, (Tprod _ | Tid _ | Tarray _) -> -1
|
||||
| Tmutable _, _ -> 1
|
||||
| Tunit, _ -> -1
|
||||
|
|
|
@ -53,6 +53,9 @@ let compile_program p =
|
|||
(* Every *)
|
||||
let p = pass "Every" true Every.program p pp in
|
||||
|
||||
(* Iterator fusion *)
|
||||
let p = pass "Iterator fusion" !do_iterator_fusion Itfusion.program p pp in
|
||||
|
||||
(* Normalization *)
|
||||
let p = pass "Normalization" true Normalize.program p pp in
|
||||
|
||||
|
|
|
@ -141,4 +141,5 @@ let edesc funs acc ed =
|
|||
let program p =
|
||||
let funs = { Hept_mapfold.defaults with edesc = edesc } in
|
||||
let p, _ = Hept_mapfold.program_it funs false p in
|
||||
p
|
||||
let added_nodes = QualEnv.fold (fun _ nd l -> nd::l) !anon_nodes [] in
|
||||
{ p with p_nodes = added_nodes @ p.p_nodes }
|
||||
|
|
|
@ -137,16 +137,6 @@ let rec translate kind context e =
|
|||
let context, e_list = translate_list ExtValue context e_list in
|
||||
context, { e with e_desc = Eapp(app, flatten_e_list e_list, r) }
|
||||
| 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 ->
|
||||
let nd = Itfusion.find_anon_node f in
|
||||
let d_list, eq_list =
|
||||
translate_eq_list nd.n_block.b_local nd.n_block.b_equs in
|
||||
let b = { nd.n_block with b_local = d_list; b_equs = eq_list } in
|
||||
let nd = { nd with n_block = b } in
|
||||
Itfusion.replace_anon_node f nd
|
||||
| _ -> () );
|
||||
let context, pe_list = translate_list ExtValue context pe_list in
|
||||
let context, e_list = translate_list ExtValue context e_list in
|
||||
context, { e with e_desc = Eiterator(it, app, n, flatten_e_list pe_list,
|
||||
|
|
|
@ -27,6 +27,7 @@ struct
|
|||
type error =
|
||||
| Ereset_not_var
|
||||
| Eunsupported_language_construct
|
||||
| Enormalization
|
||||
|
||||
let message loc kind =
|
||||
begin match kind with
|
||||
|
@ -71,7 +72,7 @@ let rec translate_op = function
|
|||
| Heptagon.Eifthenelse -> Eifthenelse
|
||||
| Heptagon.Efun f -> Efun f
|
||||
| Heptagon.Enode f -> Enode f
|
||||
| Heptagon.Efield -> Efield
|
||||
| Heptagon.Efield -> assert false
|
||||
| Heptagon.Efield_update -> Efield_update
|
||||
| Heptagon.Earray_fill -> Earray_fill
|
||||
| Heptagon.Eselect -> Eselect
|
||||
|
@ -88,55 +89,55 @@ let translate_app app =
|
|||
mk_app ~params:app.Heptagon.a_params
|
||||
~unsafe:app.Heptagon.a_unsafe (translate_op app.Heptagon.a_op)
|
||||
|
||||
let translate_extvalue
|
||||
let rec translate_extvalue
|
||||
{ Heptagon.e_desc = desc; Heptagon.e_ty = ty;
|
||||
Heptagon.e_loc = loc } =
|
||||
let mk_extvalue = mk_extvalue ~loc:loc ~ty:ty in
|
||||
match desc with
|
||||
| Heptagon.Econst c ->
|
||||
Env.const env (mk_extvalue (Wconst c))
|
||||
| Heptagon.Evar x ->
|
||||
Env.con env x (mk_extvalue (Wvar x))
|
||||
| Heptagon.Econst c -> mk_extvalue (Wconst c)
|
||||
| Heptagon.Evar x -> mk_extvalue (Wvar x)
|
||||
| Heptagon.Ewhen (e, c, ce) ->
|
||||
(match ce.Heptagon.e_desc with
|
||||
| Heptagon.Evar x ->
|
||||
mk_exp (Wwhen (translate_ext_value e, c, x))
|
||||
mk_extvalue (Wwhen (translate_extvalue e, c, x))
|
||||
| _ -> Error.message loc Error.Enormalization)
|
||||
| Heptagon.Eapp({ a_op = Efield; a_params = params }, e_list, reset) ->
|
||||
| Heptagon.Eapp({ Heptagon.a_op = Heptagon.Efield;
|
||||
Heptagon.a_params = params }, e_list, reset) ->
|
||||
let e = assert_1 e_list in
|
||||
let f = assert_1 params in
|
||||
let fn = match f with Sfield fn -> fn | _ -> asssert false in
|
||||
mk_extvalue (Wfield (translate_ext_value e, fn))
|
||||
let fn = match f.se_desc with Sfield fn -> fn | _ -> assert false in
|
||||
mk_extvalue (Wfield (translate_extvalue e, fn))
|
||||
| _ -> Error.message loc Error.Enormalization
|
||||
|
||||
let translate
|
||||
{ Heptagon.e_desc = desc; Heptagon.e_ty = ty;
|
||||
Heptagon.e_loc = loc } =
|
||||
({ Heptagon.e_desc = desc; Heptagon.e_ty = ty;
|
||||
Heptagon.e_loc = loc } as e) =
|
||||
let mk_exp = mk_exp ~loc:loc in
|
||||
match desc with
|
||||
| Heptagon.Econst _
|
||||
| Heptagon.Evar _
|
||||
| Heptagon.Ewhen _
|
||||
| Heptagon.Eapp({ a_op = Efield }, _, _) ->
|
||||
| Heptagon.Eapp({ Heptagon.a_op = Heptagon.Efield }, _, _) ->
|
||||
let w = translate_extvalue e in
|
||||
mk_exp ~loc:loc ~ty:ty (Eextvalue w)
|
||||
mk_exp ty (Eextvalue w)
|
||||
| Heptagon.Epre(None, e) ->
|
||||
mk_exp ~loc:loc ~ty:ty (Efby(None, translate_ext_value e))
|
||||
mk_exp ty (Efby(None, translate_extvalue e))
|
||||
| Heptagon.Epre(Some c, e) ->
|
||||
mk_exp ~loc:loc ~ty:ty (Efby(Some c, translate_extvalue e))
|
||||
mk_exp ty (Efby(Some c, translate_extvalue e))
|
||||
| Heptagon.Efby ({ Heptagon.e_desc = Heptagon.Econst c }, e) ->
|
||||
mk_exp ~loc:loc ~ty:ty (Efby(Some c, translate_extvalue e))
|
||||
mk_exp ty (Efby(Some c, translate_extvalue e))
|
||||
| Heptagon.Estruct f_e_list ->
|
||||
let f_e_list = List.map
|
||||
(fun (f, e) -> (f, translate_extvalue e)) f_e_list in
|
||||
mk_exp ~loc:loc ~ty:ty (Estruct f_e_list)
|
||||
| Heptagon.Eapp({ a_op = Earrow }, _, _) ->
|
||||
mk_exp ty (Estruct f_e_list)
|
||||
| Heptagon.Eapp({ Heptagon.a_op = Heptagon.Earrow }, _, _) ->
|
||||
Error.message loc Error.Eunsupported_language_construct
|
||||
| Heptagon.Eapp(app, e_list, reset) ->
|
||||
mk_exp ~loc:loc ~ty:ty (Eapp (translate_app app,
|
||||
mk_exp ty (Eapp (translate_app app,
|
||||
List.map translate_extvalue e_list,
|
||||
translate_reset reset))
|
||||
| Heptagon.Eiterator(it, app, n, pe_list, e_list, reset) ->
|
||||
mk_exp ~loc:loc ~ty:ty
|
||||
mk_exp ty
|
||||
(Eiterator (translate_iterator_type it,
|
||||
translate_app app, n,
|
||||
List.map translate_extvalue pe_list,
|
||||
|
@ -148,7 +149,7 @@ let translate
|
|||
| Heptagon.Emerge (e, c_e_list) ->
|
||||
(match e.Heptagon.e_desc with
|
||||
| Heptagon.Evar x ->
|
||||
mk_exp ~loc:loc ~ty:ty
|
||||
mk_exp ty
|
||||
(Emerge (x, List.map (fun (c,e)->c,
|
||||
translate_extvalue e) c_e_list))
|
||||
| _ -> Error.message loc Error.Enormalization)
|
||||
|
@ -157,12 +158,12 @@ let rec translate_pat = function
|
|||
| Heptagon.Evarpat(n) -> Evarpat n
|
||||
| Heptagon.Etuplepat(l) -> Etuplepat (List.map translate_pat l)
|
||||
|
||||
let rec translate_eq env
|
||||
let rec translate_eq
|
||||
{ Heptagon.eq_desc = desc; Heptagon.eq_loc = loc } =
|
||||
match desc with
|
||||
| Heptagon.Eeq(p, e) ->
|
||||
mk_equation ~loc:loc (translate_pat p) (translate env e)
|
||||
| Heptagon.Eblock _ | Heptagon.Eswitch
|
||||
mk_equation ~loc:loc (translate_pat p) (translate e)
|
||||
| Heptagon.Eblock _ | Heptagon.Eswitch _
|
||||
| Heptagon.Epresent _ | Heptagon.Eautomaton _ | Heptagon.Ereset _ ->
|
||||
Error.message loc Error.Eunsupported_language_construct
|
||||
|
||||
|
@ -183,11 +184,11 @@ let translate_contract contract =
|
|||
let node n =
|
||||
{ n_name = n.Heptagon.n_name;
|
||||
n_stateful = n.Heptagon.n_stateful;
|
||||
n_input = List.map translate_var n.Heptagon.n_inputs;
|
||||
n_output = List.map translate_var n.Heptagon.n_outputs;
|
||||
n_input = List.map translate_var n.Heptagon.n_input;
|
||||
n_output = List.map translate_var n.Heptagon.n_output;
|
||||
n_contract = translate_contract n.Heptagon.n_contract;
|
||||
n_local = List.map translate_var n.Heptagon.n_block.Heptagon.n_locals;
|
||||
n_equs = List.map translate_eq n.Heptagon.n_block.Heptagon.n_equs;
|
||||
n_local = List.map translate_var n.Heptagon.n_block.Heptagon.b_local;
|
||||
n_equs = List.map translate_eq n.Heptagon.n_block.Heptagon.b_equs;
|
||||
n_loc = n.Heptagon.n_loc ;
|
||||
n_params = n.Heptagon.n_params;
|
||||
n_params_constraints = n.Heptagon.n_params_constraints }
|
||||
|
|
|
@ -20,6 +20,25 @@ open Types
|
|||
open Static
|
||||
open Initial
|
||||
|
||||
|
||||
let build_anon, find_anon =
|
||||
let anon_nodes = ref QualEnv.empty in
|
||||
|
||||
let build_anon nodes =
|
||||
let build env nd =
|
||||
if Itfusion.is_anon_node nd.Minils.n_name then
|
||||
QualEnv.add nd.Minils.n_name nd env
|
||||
else
|
||||
env
|
||||
in
|
||||
anon_nodes := List.fold_left build QualEnv.empty nodes
|
||||
in
|
||||
|
||||
let find_anon qn =
|
||||
QualEnv.find qn !anon_nodes
|
||||
in
|
||||
build_anon, find_anon
|
||||
|
||||
let var_from_name map x =
|
||||
begin try
|
||||
Env.find x map
|
||||
|
@ -84,6 +103,14 @@ let rec bound_check_expr idx_list bounds =
|
|||
[e; bound_check_expr idx_list bounds]))
|
||||
| (_, _) -> internal_error "mls2obc" 3
|
||||
|
||||
let mk_plus_one e = match e.e_desc with
|
||||
| Econst idx ->
|
||||
let idx_plus_one = mk_static_int_op (mk_pervasives "+") [idx; mk_static_int 1] in
|
||||
{ e with e_desc = Econst idx_plus_one }
|
||||
| _ ->
|
||||
let idx_plus_one = Eop (mk_pervasives "+", [e; mk_exp_const_int 1]) in
|
||||
{ e with e_desc = idx_plus_one }
|
||||
|
||||
(** Creates the action list that copies [src] to [dest],
|
||||
updating the value at index [idx_list] with the value [v]. *)
|
||||
let rec update_array dest src idx_list v = match dest.pat_ty, idx_list with
|
||||
|
@ -95,14 +122,14 @@ let rec update_array dest src idx_list v = match dest.pat_ty, idx_list with
|
|||
[Aassgn(dest_i, src_i)]
|
||||
in
|
||||
(*Copy values < idx*)
|
||||
let a_lower = fresh_for (mk_static_int 0) idx copy in
|
||||
let a_lower = fresh_for (mk_exp_const_int 0) idx copy in
|
||||
(* Update the correct element*)
|
||||
let src_idx = mk_pattern t (Larray (src, mk_exp_int (Econst idx))) in
|
||||
let dest_idx = mk_pattern t (Larray (dest, mk_exp_int (Econst idx))) in
|
||||
let src_idx = mk_pattern t (Larray (src, idx)) in
|
||||
let dest_idx = mk_pattern t (Larray (dest, idx)) in
|
||||
let a_update = update_array dest_idx src_idx idx_list v in
|
||||
(*Copy values > idx*)
|
||||
let idx_plus_one = mk_static_int_op (mk_pervasives "+") [idx; mk_static_int 1] in
|
||||
let a_upper = fresh_for idx_plus_one n copy in
|
||||
let idx_plus_one = mk_plus_one idx in
|
||||
let a_upper = fresh_for idx_plus_one (mk_exp_static_int n) copy in
|
||||
[a_lower] @ a_update @ [a_upper]
|
||||
| _, _ ->
|
||||
[Aassgn(dest, v)]
|
||||
|
@ -196,22 +223,25 @@ let rec translate map e =
|
|||
in
|
||||
mk_exp e.Minils.e_ty desc
|
||||
|
||||
and translate_act_extvalue map pat w =
|
||||
match pat with
|
||||
| Minils.Evarpat n ->
|
||||
[Aassgn (var_from_name map n, translate_extvalue map w)]
|
||||
| _ -> assert false
|
||||
|
||||
(* [translate pat act = si, d] *)
|
||||
and translate_act map pat
|
||||
({ Minils.e_desc = desc } as act) =
|
||||
match pat, desc with
|
||||
| Minils.Etuplepat p_list,
|
||||
Minils.Eapp ({ Minils.a_op = Minils.Etuple }, act_list, _) ->
|
||||
List.flatten (List.map2 (translate_act map) p_list act_list)
|
||||
| Minils.Etuplepat p_list,
|
||||
Minils.Eextvalue { Minils.w_desc = Minils.Wconst { se_desc = Stuple se_list }} ->
|
||||
let const_list = Mls_utils.exp_list_of_static_exp_list se_list in
|
||||
List.flatten (List.map2 (translate_act map) p_list const_list)
|
||||
(* When Merge *)
|
||||
| pat, Minils.Emerge (x, c_act_list) ->
|
||||
let pattern = var_from_name map x in
|
||||
| Minils.Evarpat x, Minils.Emerge (y, c_act_list) ->
|
||||
let x = var_from_name map x in
|
||||
let translate_c_extvalue (c, w) =
|
||||
c, mk_block [Aassgn (x, translate_extvalue map w)]
|
||||
in
|
||||
let pattern = var_from_name map y in
|
||||
[Acase (mk_exp pattern.pat_ty (Epattern pattern),
|
||||
translate_c_act_list map pat c_act_list)]
|
||||
List.map translate_c_extvalue c_act_list)]
|
||||
(* Array ops *)
|
||||
| Minils.Evarpat x,
|
||||
Minils.Eapp ({ Minils.a_op = Minils.Econcat }, [e1; e2], _) ->
|
||||
|
@ -219,19 +249,19 @@ and translate_act map pat
|
|||
let cpt2, cpt2d = fresh_it () in
|
||||
let x = var_from_name map x in
|
||||
let t = x.pat_ty in
|
||||
(match e1.Minils.e_ty, e2.Minils.e_ty with
|
||||
(match e1.Minils.w_ty, e2.Minils.w_ty with
|
||||
| Tarray (t1, n1), Tarray (t2, n2) ->
|
||||
let e1 = translate_extvalue map e1 in
|
||||
let e2 = translate_extvalue map e2 in
|
||||
let a1 =
|
||||
Afor (cpt1d, mk_static_int 0, n1,
|
||||
Afor (cpt1d, mk_exp_const_int 0, mk_exp_static_int n1,
|
||||
mk_block [Aassgn (mk_pattern t1 (Larray (x, mk_evar_int cpt1)),
|
||||
mk_pattern_exp t1 (Larray (pattern_of_exp e1,
|
||||
mk_evar_int cpt1)))] ) in
|
||||
let idx = mk_exp_int (Eop (op_from_string "+",
|
||||
[ mk_exp_int (Econst n1); mk_evar_int cpt2])) in
|
||||
let p2 = mk_pattern_exp t2 (Larray (pattern_of_exp e2, mk_evar_int cpt2)) in
|
||||
let a2 = Afor (cpt2d, mk_static_int 0, n2,
|
||||
let a2 = Afor (cpt2d, mk_exp_const_int 0, mk_exp_static_int n2,
|
||||
mk_block [Aassgn (mk_pattern t2 (Larray (x, idx)), p2)] )
|
||||
in
|
||||
[a1; a2]
|
||||
|
@ -247,7 +277,7 @@ and translate_act map pat
|
|||
| _ -> Misc.internal_error "mls2obc select slice type" 5
|
||||
in
|
||||
let b = mk_block [Aassgn (mk_pattern t (Larray (x, mk_evar_int cpt)), e) ] in
|
||||
[ Afor (cptd, mk_static_int 0, n, b) ]
|
||||
[ Afor (cptd, mk_exp_const_int 0, mk_exp_static_int n, b) ]
|
||||
|
||||
| Minils.Evarpat x,
|
||||
Minils.Eapp ({ Minils.a_op = Minils.Eselect_slice;
|
||||
|
@ -264,24 +294,24 @@ and translate_act map pat
|
|||
(* bound = (idx2 - idx1) + 1*)
|
||||
let bound = mk_static_int_op (op_from_string "+")
|
||||
[ mk_static_int 1; mk_static_int_op (op_from_string "-") [idx2;idx1] ] in
|
||||
[ Afor (cptd, mk_static_int 0, bound,
|
||||
[ Afor (cptd, mk_exp_const_int 0, mk_exp_static_int bound,
|
||||
mk_block [Aassgn (mk_pattern t (Larray (x, mk_evar_int cpt)),
|
||||
mk_pattern_exp t (Larray (pattern_of_exp e, idx)))] ) ]
|
||||
|
||||
| Minils.Evarpat x, Minils.Eapp ({ Minils.a_op = Minils.Eselect_dyn }, e1::e2::idx, _) ->
|
||||
let x = var_from_name map x in
|
||||
let bounds = Mls_utils.bounds_list e1.Minils.e_ty in
|
||||
let bounds = Mls_utils.bounds_list e1.Minils.w_ty in
|
||||
let e1 = translate_extvalue map e1 in
|
||||
let idx = List.map (translate_extvalue map) idx in
|
||||
let p = pattern_of_idx_list (pattern_of_exp e1) idx in
|
||||
let true_act = Aassgn (x, mk_exp p.pat_ty (Epattern p)) in
|
||||
let false_act = Aassgn (x, translate_extvalue map e2) in
|
||||
let cond = bound_check_expr idx bounds in
|
||||
[ mk_ifthenelse cond true_act false_act ]
|
||||
[ mk_ifthenelse cond [true_act] [false_act] ]
|
||||
|
||||
| Minils.Evarpat x, Minils.Eapp ({ Minils.a_op = Minils.Eselect_trunc }, e1::idx, _) ->
|
||||
let x = var_from_name map x in
|
||||
let bounds = Mls_utils.bounds_list e1.Minils.e_ty in
|
||||
let bounds = Mls_utils.bounds_list e1.Minils.w_ty in
|
||||
let e1 = translate_extvalue map e1 in
|
||||
let idx = List.map (translate_extvalue map) idx in
|
||||
let p = pattern_of_trunc_idx_list (pattern_of_exp e1) idx in
|
||||
|
@ -289,18 +319,22 @@ and translate_act map pat
|
|||
|
||||
| Minils.Evarpat x, Minils.Eapp ({ Minils.a_op = Minils.Eupdate }, e1::e2::idx, _) ->
|
||||
let x = var_from_name map x in
|
||||
let bounds = Mls_utils.bounds_list e1.Minils.e_ty in
|
||||
let bounds = Mls_utils.bounds_list e1.Minils.w_ty in
|
||||
let idx = List.map (translate_extvalue map) idx in
|
||||
let e1 = translate_extvalue map e1 in
|
||||
let e2 = translate_extvalue map e2 in
|
||||
let cond = bound_check_expr idx bounds in
|
||||
let true_act = update_array x e1 e2 idx in
|
||||
let true_act = update_array x (pattern_of_exp e1) idx e2 in
|
||||
let false_act = Aassgn (x, e1) in
|
||||
[ mk_ifthenelse cond true_act false_act ]
|
||||
[ mk_ifthenelse cond true_act [false_act] ]
|
||||
|
||||
| Minils.Evarpat x,
|
||||
Minils.Eapp ({ Minils.a_op = Minils.Efield_update;
|
||||
Minils.a_params = [{ se_desc = Sfield f }] }, [e1; e2], _) ->
|
||||
let x = var_from_name map x in
|
||||
update_record x e1 f e2
|
||||
let e1 = translate_extvalue map e1 in
|
||||
let e2 = translate_extvalue map e2 in
|
||||
update_record x (pattern_of_exp e1) f e2
|
||||
|
||||
| Minils.Evarpat n, _ ->
|
||||
[Aassgn (var_from_name map n, translate map act)]
|
||||
|
@ -309,11 +343,6 @@ and translate_act map pat
|
|||
Location.print_location act.Minils.e_loc Mls_printer.print_pat pat;
|
||||
assert false
|
||||
|
||||
and translate_c_act_list map pat c_act_list =
|
||||
List.map
|
||||
(fun (c, act) -> (c, mk_block (translate_act map pat act)))
|
||||
c_act_list
|
||||
|
||||
(** In an iteration, objects used are element of object arrays *)
|
||||
type obj_array = { oa_index : Obc.pattern; oa_size : static_exp }
|
||||
|
||||
|
@ -356,13 +385,9 @@ let rec translate_eq map call_context { Minils.eq_lhs = pat; Minils.eq_rhs = e }
|
|||
*)
|
||||
| pat, Minils.Eapp({ Minils.a_op = Minils.Eifthenelse }, [e1;e2;e3], _) ->
|
||||
let cond = translate_extvalue map e1 in
|
||||
let vt, si, j, true_act = translate_act map pat e2 in
|
||||
let vf, si, j, false_act = translate_act map pat e3 in
|
||||
let vf = translate_var_dec vf in
|
||||
let vt = translate_var_dec vt in
|
||||
let action =
|
||||
Acase (cond, [ptrue, mk_block ~locals:vt true_act;
|
||||
pfalse, mk_block ~locals:vf false_act]) in
|
||||
let true_act = translate_act_extvalue map pat e2 in
|
||||
let false_act = translate_act_extvalue map pat e3 in
|
||||
let action = mk_ifthenelse cond true_act false_act in
|
||||
v, si, j, (control map ck action) :: s
|
||||
|
||||
| pat, Minils.Eapp ({ Minils.a_op = Minils.Efun _ | Minils.Enode _ } as app, e_list, r) ->
|
||||
|
@ -386,6 +411,7 @@ let rec translate_eq map call_context { Minils.eq_lhs = pat; Minils.eq_rhs = e }
|
|||
let x, xd = fresh_it () in
|
||||
let call_context =
|
||||
Some { oa_index = mk_pattern_int (Lvar x); oa_size = n} in
|
||||
let n = mk_exp_static_int 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 map ck) action in
|
||||
|
@ -430,7 +456,7 @@ and mk_node_call map call_context app loc name_list args ty =
|
|||
act_list
|
||||
in
|
||||
|
||||
let nd = Itfusion.find_anon_node f in
|
||||
let nd = find_anon f in
|
||||
let map = List.fold_left add_input map nd.Minils.n_input in
|
||||
let map = List.fold_left2 build map nd.Minils.n_output name_list in
|
||||
let map = List.fold_left add_input map nd.Minils.n_local in
|
||||
|
@ -476,8 +502,8 @@ and translate_iterator map call_context it name_list
|
|||
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_exp_const_int 0, n, bi)], j,
|
||||
[Afor (xd, mk_exp_const_int 0, n, b)]
|
||||
|
||||
| Minils.Imapi ->
|
||||
let c_list = array_of_input c_list in
|
||||
|
@ -489,8 +515,8 @@ and translate_iterator map call_context it name_list
|
|||
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_exp_const_int 0, n, bi)], j,
|
||||
[Afor (xd, mk_exp_const_int 0, n, b)]
|
||||
|
||||
| Minils.Imapfold ->
|
||||
let (c_list, acc_in) = split_last c_list in
|
||||
|
@ -508,8 +534,8 @@ and translate_iterator map call_context it name_list
|
|||
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_exp_const_int 0, n, bi)], j,
|
||||
[Aassgn (acc_out, acc_in); Afor (xd, mk_exp_const_int 0, n, b)]
|
||||
|
||||
| Minils.Ifold ->
|
||||
let (c_list, acc_in) = split_last c_list in
|
||||
|
@ -522,8 +548,8 @@ and translate_iterator map call_context it name_list
|
|||
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_exp_const_int 0, n, bi)], j,
|
||||
[ Aassgn (acc_out, acc_in); Afor (xd, mk_exp_const_int 0, n, b) ]
|
||||
|
||||
| Minils.Ifoldi ->
|
||||
let (c_list, acc_in) = split_last c_list in
|
||||
|
@ -536,8 +562,8 @@ and translate_iterator map call_context it name_list
|
|||
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_exp_const_int 0, n, bi)], j,
|
||||
[ Aassgn (acc_out, acc_in); Afor (xd, mk_exp_const_int 0, n, b) ]
|
||||
|
||||
let remove m d_list =
|
||||
List.filter (fun { Minils.v_ident = n } -> not (List.mem_assoc n m)) d_list
|
||||
|
@ -619,10 +645,14 @@ let translate_const_def { Minils.c_name = name; Minils.c_value = se;
|
|||
let program { Minils.p_modname = p_modname; Minils.p_opened = p_module_list;
|
||||
Minils.p_types = p_type_list;
|
||||
Minils.p_nodes = p_node_list; Minils.p_consts = p_const_list } =
|
||||
build_anon p_node_list;
|
||||
(* dont't translate anonymous nodes, they will be inlined *)
|
||||
let p_nodes_list = List.filter
|
||||
(fun nd -> not (Itfusion.is_anon_node nd.Minils.n_name)) p_node_list in
|
||||
{ p_modname = p_modname;
|
||||
p_opened = p_module_list;
|
||||
p_types = List.map translate_ty_def p_type_list;
|
||||
p_consts = List.map translate_const_def p_const_list;
|
||||
p_classes = List.map translate_node p_node_list; }
|
||||
p_classes = List.map translate_node p_nodes_list; }
|
||||
|
||||
|
||||
|
|
|
@ -41,7 +41,7 @@ let write_obc_file p =
|
|||
let no_conf () = ()
|
||||
|
||||
let targets = [ "c",(Obc_no_params Cmain.program, no_conf);
|
||||
"java", (Obc Java_main.program, java_conf);
|
||||
"java", (Obc Java_main.program, Java_main.java_conf);
|
||||
"obc", (Obc write_obc_file, no_conf);
|
||||
"obc_np", (Obc_no_params write_obc_file, no_conf);
|
||||
"epo", (Minils write_object_file, no_conf) ]
|
||||
|
@ -67,7 +67,7 @@ let generate_target p s =
|
|||
| Obc_no_params convert_fun ->
|
||||
let p_list = Callgraph.program p in
|
||||
let o_list = List.map Mls2obc.program p_list in
|
||||
let o_list = List.map Obc_compiler.program o_list in
|
||||
let o_list = List.map Obc_compiler.compile_program o_list in
|
||||
List.iter convert_fun o_list
|
||||
|
||||
let load_conf () =
|
||||
|
|
|
@ -33,11 +33,29 @@ let error_message loc = function
|
|||
|
||||
let typ_of_name h x = Env.find x h
|
||||
|
||||
let rec typing_extvalue h w =
|
||||
let ct = match w.w_desc with
|
||||
| Wconst se -> skeleton (fresh_clock ()) se.se_ty
|
||||
| Wvar x -> Ck (typ_of_name h x)
|
||||
| Wwhen (w1, c, n) ->
|
||||
let ck_n = typ_of_name h n in
|
||||
(expect h (skeleton ck_n w1.w_ty) w1; skeleton (Con (ck_n, c, n)) w1.w_ty)
|
||||
| Wfield (w1, f) ->
|
||||
let ck = fresh_clock () in
|
||||
let ct = skeleton ck w1.w_ty in (expect h (Ck ck) w1; ct)
|
||||
in (w.w_ck <- ckofct ct; ct)
|
||||
|
||||
and expect h expected_ty e =
|
||||
let actual_ty = typing_extvalue h e in
|
||||
try unify actual_ty expected_ty
|
||||
with
|
||||
| Unify -> eprintf "%a : " print_extvalue e;
|
||||
error_message e.w_loc (Etypeclash (actual_ty, expected_ty))
|
||||
|
||||
let rec typing h e =
|
||||
let ct = match e.e_desc with
|
||||
| Econst se -> skeleton (fresh_clock ()) se.se_ty
|
||||
| Evar x -> Ck (typ_of_name h x)
|
||||
| Efby (_, e) -> typing h e
|
||||
| Eextvalue w -> typing_extvalue h w
|
||||
| Efby (_, e) -> typing_extvalue h e
|
||||
| Eapp({a_op = op}, args, r) ->
|
||||
let ck = match r with
|
||||
| None -> fresh_clock ()
|
||||
|
@ -52,73 +70,67 @@ let rec typing h e =
|
|||
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)
|
||||
| Emerge (n, c_e_list) ->
|
||||
let ck_c = typ_of_name h n in
|
||||
(typing_c_e_list h ck_c n c_e_list; skeleton ck_c e.e_ty)
|
||||
| Estruct l ->
|
||||
let ck = fresh_clock () in
|
||||
(List.iter
|
||||
(fun (_, e) -> let ct = skeleton ck e.e_ty in expect h ct e) l;
|
||||
(fun (_, e) -> let ct = skeleton ck e.w_ty in expect h ct e) l;
|
||||
Ck ck)
|
||||
in (e.e_ck <- ckofct ct; ct)
|
||||
|
||||
and typing_op op e_list h e ck = match op with
|
||||
| (Eequal | Efun _ | Enode _) -> (*LA*)
|
||||
List.iter (fun e -> expect h (skeleton ck e.e_ty) e) e_list;
|
||||
List.iter (fun e -> expect h (skeleton ck e.w_ty) e) e_list;
|
||||
skeleton ck e.e_ty
|
||||
| Etuple ->
|
||||
Cprod (List.map (typing h) e_list)
|
||||
Cprod (List.map (typing_extvalue h) e_list)
|
||||
| Eifthenelse ->
|
||||
let e1, e2, e3 = assert_3 e_list in
|
||||
let ct = skeleton ck e.e_ty
|
||||
in (expect h (Ck ck) e1; expect h ct e2; expect h ct e3; ct)
|
||||
| Efield ->
|
||||
let e1 = assert_1 e_list in
|
||||
let ct = skeleton ck e1.e_ty in (expect h (Ck ck) e1; ct)
|
||||
| Efield_update ->
|
||||
let e1, e2 = assert_2 e_list in
|
||||
let ct = skeleton ck e.e_ty
|
||||
in (expect h (Ck ck) e1; expect h ct e2; ct)
|
||||
| Earray ->
|
||||
(List.iter (expect h (Ck ck)) e_list; skeleton ck e.e_ty)
|
||||
| Earray_fill -> let e = assert_1 e_list in typing h e
|
||||
| Eselect -> let e = assert_1 e_list in typing h e
|
||||
| Earray_fill -> let e = assert_1 e_list in typing_extvalue h e
|
||||
| Eselect -> let e = assert_1 e_list in typing_extvalue h e
|
||||
| Eselect_dyn -> (* TODO defe not treated ? *)
|
||||
let e1, defe, idx = assert_2min e_list in
|
||||
let ct = skeleton ck e1.e_ty
|
||||
let ct = skeleton ck e1.w_ty
|
||||
in (List.iter (expect h ct) (e1::defe::idx); ct)
|
||||
| Eselect_trunc ->
|
||||
let e1, idx = assert_1min e_list in
|
||||
let ct = skeleton ck e1.e_ty
|
||||
let ct = skeleton ck e1.w_ty
|
||||
in (List.iter (expect h ct) (e1::idx); ct)
|
||||
| Eupdate ->
|
||||
let e1, e2, idx = assert_2min e_list in
|
||||
let ct = skeleton ck e.e_ty
|
||||
in (expect h (Ck ck) e1; expect h ct e2; List.iter (expect h ct) idx; ct)
|
||||
| Eselect_slice -> let e = assert_1 e_list in typing h e
|
||||
| Eselect_slice -> let e = assert_1 e_list in typing_extvalue h e
|
||||
| Econcat ->
|
||||
let e1, e2 = assert_2 e_list in
|
||||
let ct = skeleton ck e.e_ty
|
||||
in (expect h (Ck ck) e1; expect h ct e2; ct)
|
||||
|
||||
and expect h expected_ty e =
|
||||
let actual_ty = typing h e in
|
||||
try unify actual_ty expected_ty
|
||||
with
|
||||
| Unify -> eprintf "%a : " print_exp e;
|
||||
error_message e.e_loc (Etypeclash (actual_ty, expected_ty))
|
||||
|
||||
and typing_c_e_list h ck_c n c_e_list =
|
||||
let rec typrec =
|
||||
function
|
||||
| [] -> ()
|
||||
| (c, e) :: c_e_list ->
|
||||
(expect h (skeleton (Con (ck_c, c, n)) e.e_ty) e; typrec c_e_list)
|
||||
(expect h (skeleton (Con (ck_c, c, n)) e.w_ty) e; typrec c_e_list)
|
||||
in typrec c_e_list
|
||||
|
||||
let expect_exp h expected_ty e =
|
||||
let actual_ty = typing h e in
|
||||
try unify actual_ty expected_ty
|
||||
with
|
||||
| Unify -> eprintf "%a : " print_exp e;
|
||||
error_message e.e_loc (Etypeclash (actual_ty, expected_ty))
|
||||
|
||||
let rec typing_pat h =
|
||||
function
|
||||
| Evarpat x -> Ck (typ_of_name h x)
|
||||
|
@ -127,7 +139,7 @@ let rec typing_pat h =
|
|||
let typing_eqs h eq_list = (*TODO FIXME*)
|
||||
let typing_eq { eq_lhs = pat; eq_rhs = e } =
|
||||
let ty_pat = typing_pat h pat in
|
||||
(try expect h ty_pat e with
|
||||
(try expect_exp h ty_pat e with
|
||||
| Errors.Error -> (* DEBUG *)
|
||||
Format.eprintf "Complete expression: %a@\nClock pattern: %a@."
|
||||
Mls_printer.print_exp e
|
||||
|
@ -153,8 +165,8 @@ let typing_contract h contract base =
|
|||
(* assumption *)
|
||||
(* property *)
|
||||
typing_eqs h' eq_list;
|
||||
expect h' (Ck base) e_a;
|
||||
expect h' (Ck base) e_g;
|
||||
expect_exp h' (Ck base) e_a;
|
||||
expect_exp h' (Ck base) e_g;
|
||||
sbuild h c_list base
|
||||
|
||||
let typing_node ({ n_input = i_list;
|
||||
|
|
|
@ -20,19 +20,16 @@ let compile_program p =
|
|||
(* Check that the dataflow code is well initialized *)
|
||||
(*let p = silent_pass "Initialization check" !init Init.program p in *)
|
||||
|
||||
(* Iterator fusion *)
|
||||
let p = pass "Iterator fusion" !do_iterator_fusion Itfusion.program p pp in
|
||||
|
||||
(* Automata minimization *)
|
||||
(*
|
||||
let p =
|
||||
let call_tomato = !tomato or (List.length !tomato_nodes > 0) in
|
||||
pass "Automata minimization" call_tomato Tomato.program p pp in
|
||||
|
||||
*)
|
||||
(** TODO: re enable when ported to the new AST
|
||||
let p =
|
||||
pass "Automata minimization checks" true Tomato.tomato_checks p pp in
|
||||
|
||||
(* Normalization to maximize opportunities *)
|
||||
let p = pass "Normalization" true Normalize.program p pp in
|
||||
*)
|
||||
|
||||
(* Scheduling *)
|
||||
let p = pass "Scheduling" true Schedule.program p pp in
|
||||
|
|
|
@ -14,6 +14,32 @@ open Minils
|
|||
open Misc
|
||||
open Global_compare
|
||||
|
||||
let rec extvalue_compare w1 w2 =
|
||||
let cr = type_compare w1.w_ty w2.w_ty in
|
||||
if cr <> 0 then cr
|
||||
else
|
||||
match w1.w_desc, w2.w_desc with
|
||||
| Wconst se1, Wconst se2 -> static_exp_compare se1 se2
|
||||
| Wvar vi1, Wvar vi2 -> ident_compare vi1 vi2
|
||||
| Wwhen (e1, cn1, vi1), Wwhen (e2, cn2, vi2) ->
|
||||
let cr = Pervasives.compare cn1 cn2 in
|
||||
if cr <> 0 then cr else
|
||||
let cr = ident_compare vi1 vi2 in
|
||||
if cr <> 0 then cr else extvalue_compare e1 e2
|
||||
| Wfield (r1, f1), Wfield(r2, f2) ->
|
||||
let cr = compare f1 f2 in
|
||||
if cr <> 0 then cr else extvalue_compare w1 w2
|
||||
|
||||
| Wconst _, _ -> 1
|
||||
|
||||
| Wvar _, Wconst _ -> -1
|
||||
| Wvar _, _ -> 1
|
||||
|
||||
| Wwhen _, (Wconst _ | Wvar _) -> -1
|
||||
| Wwhen _, _ -> 1
|
||||
|
||||
| Wfield _, _ -> -1
|
||||
|
||||
let rec exp_compare e1 e2 =
|
||||
let cr = type_compare e1.e_ty e2.e_ty in
|
||||
if cr <> 0 then cr
|
||||
|
@ -22,31 +48,26 @@ let rec exp_compare e1 e2 =
|
|||
if cr <> 0 then cr
|
||||
else
|
||||
match e1.e_desc, e2.e_desc with
|
||||
| Econst se1, Econst se2 -> static_exp_compare se1 se2
|
||||
| Evar vi1, Evar vi2 -> ident_compare vi1 vi2
|
||||
| Eextvalue w1, Eextvalue w2 ->
|
||||
extvalue_compare w1 w2
|
||||
| Efby (seo1, e1), Efby (seo2, e2) ->
|
||||
let cr = option_compare static_exp_compare seo1 seo2 in
|
||||
if cr <> 0 then cr else exp_compare e1 e2
|
||||
if cr <> 0 then cr else extvalue_compare e1 e2
|
||||
| Eapp (app1, el1, vio1), Eapp (app2, el2, vio2) ->
|
||||
let cr = app_compare app1 app2 in
|
||||
if cr <> 0 then cr
|
||||
else let cr = list_compare exp_compare el1 el2 in
|
||||
else let cr = list_compare extvalue_compare el1 el2 in
|
||||
if cr <> 0 then cr else option_compare ident_compare vio1 vio2
|
||||
| Ewhen (e1, cn1, vi1), Ewhen (e2, cn2, vi2) ->
|
||||
let cr = Pervasives.compare cn1 cn2 in
|
||||
if cr <> 0 then cr else
|
||||
let cr = ident_compare vi1 vi2 in
|
||||
if cr <> 0 then cr else exp_compare e1 e2
|
||||
| Emerge (vi1, cnel1), Emerge (vi2, cnel2) ->
|
||||
let compare_cne (cn1, e1) (cn2, e2) =
|
||||
let cr = compare cn1 cn2 in
|
||||
if cr <> 0 then cr else exp_compare e1 e2 in
|
||||
if cr <> 0 then cr else extvalue_compare e1 e2 in
|
||||
let cr = ident_compare vi1 vi2 in
|
||||
if cr <> 0 then cr else list_compare compare_cne cnel1 cnel2
|
||||
| Estruct fnel1, Estruct fnel2 ->
|
||||
let compare_fne (fn1, e1) (fn2, e2) =
|
||||
let cr = compare fn1 fn2 in
|
||||
if cr <> 0 then cr else exp_compare e1 e2 in
|
||||
if cr <> 0 then cr else extvalue_compare e1 e2 in
|
||||
list_compare compare_fne fnel1 fnel2
|
||||
| Eiterator (it1, app1, se1, pel1, el1, vio1),
|
||||
Eiterator (it2, app2, se2, pel2, el2, vio2) ->
|
||||
|
@ -58,23 +79,17 @@ let rec exp_compare e1 e2 =
|
|||
if cr <> 0 then cr else
|
||||
let cr = option_compare ident_compare vio1 vio2 in
|
||||
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
|
||||
let cr = list_compare extvalue_compare pel1 pel2 in
|
||||
if cr <> 0 then cr else list_compare extvalue_compare el1 el2
|
||||
|
||||
| Econst _, _ -> 1
|
||||
| Eextvalue _, _ -> 1
|
||||
|
||||
| Evar _, Econst _ -> -1
|
||||
| Evar _, _ -> 1
|
||||
|
||||
| Efby _, (Econst _ | Evar _) -> -1
|
||||
| Efby _, Eextvalue _ -> -1
|
||||
| Efby _, _ -> 1
|
||||
|
||||
| Eapp _, (Econst _ | Evar _ | Efby _) -> -1
|
||||
| Eapp _, (Eextvalue _ | Efby _) -> -1
|
||||
| Eapp _, _ -> 1
|
||||
|
||||
| Ewhen _, (Estruct _ | Eiterator _ | Emerge _) -> 1
|
||||
| Ewhen _, _ -> -1
|
||||
|
||||
| Emerge _, (Estruct _ | Eiterator _) -> 1
|
||||
| Emerge _, _ -> -1
|
||||
|
||||
|
@ -89,7 +104,7 @@ and app_compare app1 app2 =
|
|||
if cr <> 0 then cr else let cr = match app1.a_op, app2.a_op with
|
||||
| Efun ln1, Efun ln2 -> compare ln1 ln2
|
||||
| x, y when x = y -> 0 (* all constructors can be compared with P.compare *)
|
||||
| (Eequal | Etuple | Efun _ | Enode _ | Eifthenelse | Efield
|
||||
| (Eequal | Etuple | Efun _ | Enode _ | Eifthenelse
|
||||
| Efield_update), _ -> -1
|
||||
| (Earray | Earray_fill | Eselect | Eselect_slice | Eselect_dyn
|
||||
| Eselect_trunc | Eupdate | Econcat ), _ -> 1 in
|
||||
|
|
|
@ -56,7 +56,7 @@ let is_record_type ty = match ty with
|
|||
|
||||
let is_op = function
|
||||
| { qual = Pervasives; name = _ } -> true | _ -> false
|
||||
(*
|
||||
|
||||
module Vars =
|
||||
struct
|
||||
let add x acc = if List.mem x acc then acc else x :: acc
|
||||
|
@ -65,25 +65,37 @@ struct
|
|||
| Evarpat x -> x :: acc
|
||||
| Etuplepat pat_list -> List.fold_left vars_pat acc pat_list
|
||||
|
||||
let def acc { eq_lhs = pat } = vars_pat acc pat
|
||||
|
||||
let rec vars_ck acc = function
|
||||
| Con(_, _, n) -> add n acc
|
||||
| Cbase | Cvar { contents = Cindex _ } -> acc
|
||||
| Cvar { contents = Clink ck } -> vars_ck acc ck
|
||||
|
||||
let read_extvalue read_funs (is_left, acc_init) w =
|
||||
(* recursive call *)
|
||||
let _,(_, acc) = Mls_mapfold.extvalue read_funs (is_left, acc_init) w in
|
||||
let acc = match w.w_desc with
|
||||
| Wvar x | Wwhen(_, _, x) ->
|
||||
add x acc
|
||||
| _ -> acc
|
||||
in
|
||||
w, (is_left, vars_ck acc w.w_ck)
|
||||
|
||||
let read_exp read_funs (is_left, acc_init) e =
|
||||
(* recursive call *)
|
||||
let _,(_, acc) = Mls_mapfold.exp read_funs (is_left, acc_init) e in
|
||||
|
||||
(* special cases *)
|
||||
let acc = match e.e_desc with
|
||||
| Evar x | Emerge(x,_) | Ewhen(_, _, x)
|
||||
| Emerge(x,_)
|
||||
| Eapp(_, _, Some x) | Eiterator (_, _, _, _, _, Some x) ->
|
||||
add x acc
|
||||
| Efby(_, e) ->
|
||||
if is_left then
|
||||
(* do not consider variables to the right
|
||||
of the fby, only clocks*)
|
||||
vars_ck acc_init e.e_ck
|
||||
vars_ck acc_init e.w_ck
|
||||
else acc
|
||||
| _ -> acc
|
||||
in
|
||||
|
@ -92,7 +104,16 @@ struct
|
|||
let read_exp is_left acc e =
|
||||
let _, (_, acc) =
|
||||
Mls_mapfold.exp_it
|
||||
{ Mls_mapfold.defaults with Mls_mapfold.exp = read_exp }
|
||||
{ Mls_mapfold.defaults with
|
||||
Mls_mapfold.exp = read_exp;
|
||||
Mls_mapfold.extvalue = read_extvalue }
|
||||
(is_left, acc) e in
|
||||
acc
|
||||
|
||||
let read_extvalue is_left acc e =
|
||||
let _, (_, acc) =
|
||||
Mls_mapfold.extvalue_it
|
||||
{ Mls_mapfold.defaults with Mls_mapfold.extvalue = read_extvalue }
|
||||
(is_left, acc) e in
|
||||
acc
|
||||
|
||||
|
@ -100,20 +121,18 @@ struct
|
|||
| [] -> []
|
||||
| y :: l -> if x = y then l else y :: remove x l
|
||||
|
||||
let def acc { eq_lhs = pat } = vars_pat acc pat
|
||||
|
||||
let read is_left { eq_lhs = pat; eq_rhs = e } = match pat, e.e_desc with
|
||||
| Evarpat(n), Efby(_, e1) ->
|
||||
if is_left
|
||||
then remove n (read_exp is_left [] e1)
|
||||
else read_exp is_left [] e1
|
||||
then remove n (read_extvalue is_left [] e1)
|
||||
else read_extvalue is_left [] e1
|
||||
| _ -> read_exp is_left [] e
|
||||
|
||||
let antidep { eq_rhs = e } =
|
||||
match e.e_desc with Efby _ -> true | _ -> false
|
||||
|
||||
let clock { eq_rhs = e } = match e.e_desc with
|
||||
| Emerge(_, (_, e) :: _) -> e.e_ck
|
||||
| Emerge(_, (_, e) :: _) -> e.w_ck
|
||||
| _ -> e.e_ck
|
||||
|
||||
let head ck =
|
||||
|
@ -166,4 +185,4 @@ module AllDep = Dep.Make
|
|||
end)
|
||||
|
||||
let eq_find id = List.find (fun eq -> List.mem id (Vars.def [] eq))
|
||||
*)
|
||||
|
||||
|
|
|
@ -77,16 +77,7 @@ let eqs funs () eq_list =
|
|||
let eqs, () = Mls_mapfold.eqs funs () eq_list in
|
||||
schedule eqs, ()
|
||||
|
||||
let edesc _ () = function
|
||||
| Eiterator(it, ({ a_op = Enode f } as app),
|
||||
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), ()
|
||||
| _ -> raise Errors.Fallback
|
||||
|
||||
let program p =
|
||||
let p, () = Mls_mapfold.program_it
|
||||
{ Mls_mapfold.defaults with Mls_mapfold.eqs = eqs;
|
||||
Mls_mapfold.edesc = edesc } () p in p
|
||||
let funs = { Mls_mapfold.defaults with Mls_mapfold.eqs = eqs } in
|
||||
let p, () = Mls_mapfold.program_it funs () p in
|
||||
p
|
||||
|
|
|
@ -44,14 +44,14 @@ struct
|
|||
let uses = find_uses ident use_count in
|
||||
match uses with
|
||||
| Clock | Reset -> false
|
||||
| Var i -> i < 2 || (match e.e_desc with Econst _ -> true | _ -> false)
|
||||
| Var i -> i < 2 || (match e.e_desc with Eextvalue { w_desc = Wconst _ } -> true | _ -> false)
|
||||
|
||||
let edesc funs use_counts edesc =
|
||||
let (edesc, use_counts) = Mls_mapfold.edesc funs use_counts edesc in
|
||||
let use_counts = match edesc with
|
||||
| Evar vi -> add_var_use vi use_counts
|
||||
| Eextvalue { w_desc = Wvar vi } -> add_var_use vi use_counts
|
||||
| Emerge (vi, _) -> add_clock_use vi use_counts
|
||||
| Ewhen (_, _, vi) -> add_clock_use vi use_counts
|
||||
| Eextvalue { w_desc = Wwhen (_, _, vi) } -> add_clock_use vi use_counts
|
||||
| Eapp (_, _, Some vi) | Eiterator (_, _, _, _, _, Some vi) ->
|
||||
add_reset_use vi use_counts
|
||||
| _ -> use_counts in
|
||||
|
@ -67,7 +67,7 @@ struct
|
|||
let exp funs subst exp =
|
||||
let (exp, subst) = Mls_mapfold.exp funs subst exp in
|
||||
match exp.e_desc with
|
||||
| Evar vi -> (try Env.find vi subst with Not_found -> exp), subst
|
||||
| Eextvalue { w_desc = Wvar vi } -> (try Env.find vi subst with Not_found -> exp), subst
|
||||
| _ -> (exp, subst)
|
||||
|
||||
let inline_node subst nd =
|
||||
|
|
|
@ -20,6 +20,8 @@ open Clocks
|
|||
open Pp_tools
|
||||
open Mls_compare
|
||||
|
||||
(** TODO: remove all references to Introvars *)
|
||||
|
||||
let debug_do = Introvars.debug_do
|
||||
|
||||
module IntMap = Map.Make(struct
|
||||
|
@ -159,7 +161,7 @@ struct
|
|||
end
|
||||
|
||||
let empty_var = Idents.gen_var "tomato" "EMPTY"
|
||||
let dummy_exp = mk_exp ~ty:Types.Tunit (Evar empty_var)
|
||||
let dummy_exp = mk_exp Types.Tinvalid (Evar empty_var)
|
||||
|
||||
let exp_of_ident ~ty vi = mk_exp ~ty:ty (Evar vi)
|
||||
and ident_of_exp { e_desc = e_d; } = match e_d with
|
||||
|
@ -536,9 +538,9 @@ let node nd =
|
|||
Format.printf
|
||||
"TOMATO: factored out %d expressions.@."
|
||||
(orig_eq_count - List.length nd.n_equs);
|
||||
|
||||
(*
|
||||
let nd = Singletonvars.node nd in
|
||||
|
||||
*)
|
||||
debug_do (fun _ ->
|
||||
Format.printf "Factored node:@\n%a@\n" print_node nd);
|
||||
|
||||
|
@ -556,5 +558,7 @@ let node nd =
|
|||
|
||||
let program p = { p with p_nodes = List.map node p.p_nodes; }
|
||||
|
||||
(*
|
||||
let tomato_checks p =
|
||||
Checkpass.add_checks "tomato" node !Compiler_options.tomato_check p
|
||||
*)
|
||||
|
|
|
@ -1 +1 @@
|
|||
<transformations> or <c> or <java>:include
|
||||
<main> or <transformations> or <c> or <java>:include
|
||||
|
|
|
@ -95,7 +95,7 @@ and cstm =
|
|||
| Cif of cexpr * cstm list * cstm list (** Alternative *)
|
||||
| Cswitch of cexpr * (string * cstm list) list (** Case/switch over an enum.*)
|
||||
| Cwhile of cexpr * cstm list (** While loop. *)
|
||||
| Cfor of string * int * int * cstm list (** For loop. int <= string < int *)
|
||||
| Cfor of string * cexpr * cexpr * cstm list (** For loop. int <= string < int *)
|
||||
| Creturn of cexpr (** Ends a procedure/function by returning an expression.*)
|
||||
|
||||
(** C type declarations ; will {b always} correspond to a typedef in emitted
|
||||
|
@ -221,9 +221,9 @@ and pp_cstm fmt stm = match stm with
|
|||
fprintf fmt "@[<v>@[<v 2>if (%a) {%a@]@ @[<v 2>} else {%a@]@ }@]"
|
||||
pp_cexpr c pp_cstm_list t pp_cstm_list e
|
||||
| Cfor(x, lower, upper, e) ->
|
||||
fprintf fmt "@[<v>@[<v 2>for (int %a = %d; %a < %d; ++%a) {%a@]@ }@]"
|
||||
pp_string x lower pp_string x
|
||||
upper pp_string x pp_cstm_list e
|
||||
fprintf fmt "@[<v>@[<v 2>for (int %a = %a; %a < %a; ++%a) {%a@]@ }@]"
|
||||
pp_string x pp_cexpr lower pp_string x
|
||||
pp_cexpr upper pp_string x pp_cstm_list e
|
||||
| Cwhile (e, b) ->
|
||||
fprintf fmt "@[<v>@[<v 2>while (%a) {%a@]@ }@]" pp_cexpr e pp_cstm_list b
|
||||
| Csblock cb -> pp_cblock fmt cb
|
||||
|
|
|
@ -67,7 +67,7 @@ and cstm =
|
|||
| Cif of cexpr * cstm list * cstm list (** Alternative *)
|
||||
| Cswitch of cexpr * (string * cstm list) list (** Case/switch over an enum.*)
|
||||
| Cwhile of cexpr * cstm list (** While loop. *)
|
||||
| Cfor of string * int * int * cstm list (** For loop. int <= string < int *)
|
||||
| Cfor of string * cexpr * cexpr * cstm list (** For loop. int <= string < int *)
|
||||
| Creturn of cexpr (** Ends a procedure/function by returning an expression.*)
|
||||
|
||||
(** C type declarations ; will {b always} correspond to a typedef in emitted
|
||||
|
|
|
@ -141,7 +141,7 @@ let rec copy_array src dest bounds =
|
|||
| [] -> [Caffect (dest, Clhs src)]
|
||||
| n::bounds ->
|
||||
let x = gen_symbol () in
|
||||
[Cfor(x, 0, n,
|
||||
[Cfor(x, Cconst (Ccint 0), n,
|
||||
copy_array (Carray (src, Clhs (Cvar x)))
|
||||
(Carray (dest, Clhs (Cvar x))) bounds)]
|
||||
|
||||
|
@ -208,7 +208,7 @@ and create_affect_stm dest src ty =
|
|||
| Carraylit l -> create_affect_lit dest l bty
|
||||
| Clhs src ->
|
||||
let x = gen_symbol () in
|
||||
[Cfor(x, 0, n,
|
||||
[Cfor(x, Cconst (Ccint 0), Cconst (Ccint n),
|
||||
create_affect_stm (Carray (dest, Clhs (Cvar x)))
|
||||
(Clhs (Carray (src, Clhs (Cvar x)))) bty)]
|
||||
| _ -> assert false (** TODO: add missing cases eg for records *)
|
||||
|
@ -420,7 +420,7 @@ let rec create_affect_const var_env dest c =
|
|||
create_affect_const var_env dest se
|
||||
| Sarray_power(c, n) ->
|
||||
let x = gen_symbol () in
|
||||
[Cfor(x, 0, int_of_static_exp n,
|
||||
[Cfor(x, Cconst (Ccint 0), cexpr_of_static_exp n,
|
||||
create_affect_const var_env (Carray (dest, Clhs (Cvar x))) c)]
|
||||
| Sarray cl ->
|
||||
let create_affect_idx c (i, affl) =
|
||||
|
@ -471,8 +471,8 @@ let rec cstm_of_act var_env obj_env act =
|
|||
(** For composition of statements, just recursively apply our
|
||||
translation function on sub-statements. *)
|
||||
| Afor ({ v_ident = x }, i1, i2, act) ->
|
||||
[Cfor(name x, int_of_static_exp i1,
|
||||
int_of_static_exp i2, cstm_of_act_list var_env obj_env act)]
|
||||
[Cfor(name x, cexpr_of_exp var_env i1,
|
||||
cexpr_of_exp var_env i2, cstm_of_act_list var_env obj_env act)]
|
||||
|
||||
(** Special case for x = 0^n^n...*)
|
||||
| Aassgn (vn, { e_desc = Econst c }) ->
|
||||
|
@ -503,7 +503,7 @@ let rec cstm_of_act var_env obj_env act =
|
|||
let x = gen_symbol () in
|
||||
let field = Cfield (Cderef (Cvar "self"), local_qn (name on)) in
|
||||
let elt = [Caddrof( Carray(field, Clhs (Cvar x)) )] in
|
||||
[Cfor(x, 0, int_of_static_exp size,
|
||||
[Cfor(x, Cconst (Ccint 0), cexpr_of_static_exp size,
|
||||
[Csexpr (Cfun_call (classn ^ "_reset", elt ))] )]
|
||||
)
|
||||
|
||||
|
|
|
@ -112,7 +112,7 @@ let main_def_of_class_def cd =
|
|||
let iter_var = fresh "i" in
|
||||
let lhs = Carray (lhs, Clhs (Cvar iter_var)) in
|
||||
let (reads, bufs) = read_lhs_of_ty lhs ty in
|
||||
([Cfor (iter_var, 0, int_of_static_exp n, reads)], bufs)
|
||||
([Cfor (iter_var, Cconst (Ccint 0), cexpr_of_static_exp n, reads)], bufs)
|
||||
| _ ->
|
||||
let rec mk_prompt lhs = match lhs with
|
||||
| Cvar vn -> (vn, [])
|
||||
|
@ -149,7 +149,7 @@ let main_def_of_class_def cd =
|
|||
let lhs = Carray (lhs, Clhs (Cvar iter_var)) in
|
||||
let (reads, bufs) = write_lhs_of_ty lhs ty in
|
||||
([cprint_string "[ ";
|
||||
Cfor (iter_var, 0, int_of_static_exp n, reads);
|
||||
Cfor (iter_var, Cconst (Ccint 0), cexpr_of_static_exp n, reads);
|
||||
cprint_string "]"], bufs)
|
||||
| _ ->
|
||||
let varn = fresh "buf" in
|
||||
|
|
|
@ -213,7 +213,8 @@ let rec act_list param_env act_l acts =
|
|||
let acase = Aswitch (exp param_env e, List.map _c_b c_b_l) in
|
||||
acase::acts
|
||||
| Obc.Afor (v, se, se', b) ->
|
||||
let afor = Afor (var_dec param_env v, static_exp param_env se, static_exp param_env se', block param_env b) in
|
||||
let afor = Afor (var_dec param_env v,
|
||||
exp param_env se, exp param_env se', block param_env b) in
|
||||
afor::acts
|
||||
| Obc.Ablock b ->
|
||||
let ablock = Ablock (block param_env b) in
|
||||
|
|
|
@ -69,7 +69,7 @@ type act =
|
|||
| Aassgn of pattern * exp
|
||||
| Acall of pattern list * obj_ref * method_name * exp list
|
||||
| Acase of exp * (constructor_name * block) list
|
||||
| Afor of var_dec * static_exp * static_exp * block
|
||||
| Afor of var_dec * exp * exp * block
|
||||
| Ablock of block
|
||||
|
||||
and block =
|
||||
|
|
|
@ -104,8 +104,8 @@ and act funs acc a = match a with
|
|||
let c_b_list, acc = mapfold aux acc c_b_list in
|
||||
Acase(x, c_b_list), acc
|
||||
| Afor(x, idx1, idx2, b) ->
|
||||
let idx1, acc = static_exp_it funs.global_funs acc idx1 in
|
||||
let idx2, acc = static_exp_it funs.global_funs acc idx2 in
|
||||
let idx1, acc = exp_it funs acc idx1 in
|
||||
let idx2, acc = exp_it funs acc idx2 in
|
||||
let b, acc = block_it funs acc b in
|
||||
Afor(x, idx1, idx2, b), acc
|
||||
| Ablock b ->
|
||||
|
|
|
@ -90,8 +90,8 @@ let rec print_act ff a =
|
|||
| Afor(x, i1, i2, act_list) ->
|
||||
fprintf ff "@[<v>@[<v 2>for %a = %a to %a {@ %a @]@,}@]"
|
||||
print_vd x
|
||||
print_static_exp i1
|
||||
print_static_exp i2
|
||||
print_exp i1
|
||||
print_exp i2
|
||||
print_block act_list
|
||||
| Acall (var_list, o, meth, es) ->
|
||||
fprintf ff "@[<2>%a%a.%a(%a)@]"
|
||||
|
|
|
@ -25,6 +25,12 @@ let mk_exp ?(loc=no_location) ty desc =
|
|||
let mk_exp_int ?(loc=no_location) desc =
|
||||
{ e_desc = desc; e_ty = Initial.tint; e_loc = loc }
|
||||
|
||||
let mk_exp_static_int ?(loc=no_location) se =
|
||||
mk_exp_int ~loc:loc (Econst se)
|
||||
|
||||
let mk_exp_const_int ?(loc=no_location) i =
|
||||
mk_exp_int ~loc:loc (Econst (Initial.mk_static_int i))
|
||||
|
||||
let mk_exp_bool ?(loc=no_location) desc =
|
||||
{ e_desc = desc; e_ty = Initial.tbool; e_loc = loc }
|
||||
|
||||
|
@ -49,7 +55,7 @@ let mk_block ?(locals=[]) eq_list =
|
|||
b_body = eq_list }
|
||||
|
||||
let mk_ifthenelse cond true_act false_act =
|
||||
Acase (cond, [ Initial.ptrue, mk_block [true_act]; Initial.pfalse, mk_block [false_act] ])
|
||||
Acase (cond, [ Initial.ptrue, mk_block true_act; Initial.pfalse, mk_block false_act ])
|
||||
|
||||
let rec var_name x =
|
||||
match x.pat_desc with
|
||||
|
@ -188,4 +194,4 @@ let rec copy_array pass dest src = match dest.l_ty with
|
|||
fresh_for pass (mk_static_int 0) n copy
|
||||
| _ ->
|
||||
Aassgn(dest, Epattern src)
|
||||
*)
|
||||
*)
|
||||
|
|
Loading…
Reference in a new issue