heptagon/compiler/main/mls2obc.ml
Cédric Pasteur a081f2dacf Added foldi iterator
Same as fold but the iterated function takes an 
integer as the last but one argument.
This is not something that is necessarily 
important to have in trunk but the patch is so 
small that it doesn't hurt.
2010-07-26 09:33:22 +02:00

503 lines
20 KiB
OCaml

(**************************************************************************)
(* *)
(* Heptagon *)
(* *)
(* Author : Marc Pouzet *)
(* Organization : Demons, LRI, University of Paris-Sud, Orsay *)
(* *)
(**************************************************************************)
(* Translation from Minils to Obc. *)
open Misc
open Names
open Idents
open Signature
open Obc
open Types
open Control
open Static
open Obc_mapfold
let gen_obj_name n =
(shortname n) ^ "_mem" ^ (gen_symbol ())
let op_from_string op = Modname { qual = "Pervasives"; id = op; }
let rec lhs_of_idx_list e = function
| [] -> e | idx :: l -> mk_lhs (Larray (lhs_of_idx_list e l, idx))
let array_elt_of_exp idx e =
match e.e_desc with
| Econst ({ se_desc = Sarray_power (c, _) }) ->
mk_exp (Econst c)
| _ ->
mk_lhs_exp (Larray(lhs_of_exp e, mk_exp (Elhs idx)))
(** Creates the expression that checks that the indices
in idx_list are in the bounds. If idx_list=[e1;..;ep]
and bounds = [n1;..;np], it returns
e1 <= n1 && .. && ep <= np *)
let rec bound_check_expr idx_list bounds =
match (idx_list, bounds) with
| [idx], [n] ->
mk_exp (Eop (op_from_string "<",
[ idx; mk_exp (Econst n)]))
| (idx :: idx_list, n :: bounds) ->
let e = mk_exp (Eop (op_from_string "<",
[idx; mk_exp (Econst n)])) in
mk_exp (Eop (op_from_string "&",
[e; bound_check_expr idx_list bounds]))
| (_, _) -> assert false
let reinit o =
Acall ([], o, Mreset, [])
let rec translate_pat map = function
| Minils.Evarpat x -> [ var_from_name map x ]
| Minils.Etuplepat pat_list ->
List.fold_right (fun pat acc -> (translate_pat map pat) @ acc)
pat_list []
let translate_var_dec map l =
let one_var { Minils.v_ident = x; Minils.v_type = t; v_loc = loc } =
mk_var_dec ~loc:loc x t
in
List.map one_var l
(* [translate e = c] *)
let rec translate map (si, j, s) e =
let desc = match e.Minils.e_desc with
| Minils.Econst v -> Econst v
| Minils.Evar n -> Elhs (var_from_name map n)
| Minils.Eapp ({ Minils.a_op = Minils.Efun n },
e_list, _) when Mls_utils.is_op n ->
Eop (n, List.map (translate map (si, j, s)) e_list)
| Minils.Ewhen (e, _, _) ->
let e = translate map (si, j, s) e in
e.e_desc
| Minils.Estruct f_e_list ->
let type_name =
(match e.Minils.e_ty with
| Tid name -> name
| _ -> assert false) in
let f_e_list =
List.map
(fun (f, e) -> (f, (translate map (si, j, s) e)))
f_e_list
in Estruct (type_name, f_e_list)
| Minils.Eapp ({ Minils.a_op = Minils.Efield;
Minils.a_params = [{ se_desc = Sconstructor f }] },
[e], _) ->
let e = translate map (si, j, s) e in
Elhs (mk_lhs (Lfield (lhs_of_exp e, f)))
(*Array operators*)
| Minils.Eapp ({ Minils.a_op = Minils.Earray }, e_list, _) ->
Earray (List.map (translate map (si, j, s)) e_list)
| Minils.Eapp ({ Minils.a_op = Minils.Eselect;
Minils.a_params = idx }, [e], _) ->
let e = translate map (si, j, s) e in
let idx_list = List.map (fun idx -> mk_exp (Econst idx)) idx in
Elhs (lhs_of_idx_list (lhs_of_exp e) idx_list)
| _ -> (*Minils_printer.print_exp stdout e; flush stdout;*) assert false
in
mk_exp ~ty:e.Minils.e_ty desc
(* [translate pat act = si, j, d, s] *)
and translate_act map context 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 context) p_list act_list)
| Minils.Etuplepat p_list,
Minils.Econst { 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 context) p_list const_list)
| pat, Minils.Ewhen (e, _, _) ->
translate_act map context pat e
| pat, Minils.Emerge (x, c_act_list) ->
let lhs = var_from_name map x in
[Acase (mk_exp (Elhs lhs),
translate_c_act_list map context pat c_act_list)]
| Minils.Evarpat n, _ ->
[Aassgn (var_from_name map n, translate map context act)]
| _ -> (*Minils_printer.print_exp stdout act;*) assert false
and translate_c_act_list map context pat c_act_list =
List.map
(fun (c, act) -> (c, mk_block (translate_act map context pat act)))
c_act_list
let mk_obj_call_from_context (o, _) n =
match o with
| Oobj _ -> Oobj n
| Oarray (_, lhs) -> Oarray(n, lhs)
let size_from_call_context (_, n) = n
let empty_call_context = Oobj "n", None
let rec translate_eq map call_context { Minils.eq_lhs = pat; Minils.eq_rhs = e }
(v, si, j, s) =
let { Minils.e_desc = desc; Minils.e_ty = ty;
Minils.e_ck = ck; Minils.e_loc = loc } = e in
match (pat, desc) with
| Minils.Evarpat n, Minils.Efby (opt_c, e) ->
let x = var_from_name map n in
let si = (match opt_c with
| None -> si
| Some c ->
(Aassgn (x,
mk_exp (Econst c))) :: si) in
let action = Aassgn (var_from_name map n,
translate map (si, j, s) e)
in
v, si, j, (control map ck action) :: s
| Minils.Etuplepat p_list,
Minils.Eapp({ Minils.a_op = Minils.Etuple }, act_list, _) ->
List.fold_right2
(fun pat e ->
translate_eq map call_context
(Minils.mk_equation pat e))
p_list act_list (v, si, j, s)
| pat, Minils.Eapp({ Minils.a_op = Minils.Eifthenelse }, [e1;e2;e3], _) ->
let cond = translate map (si, j, s) e1 in
let vt, si, j, true_act = translate_eq map call_context
(Minils.mk_equation pat e2) (v, si, j, s) in
let vf, si, j, false_act = translate_eq map call_context
(Minils.mk_equation pat e3) (v, si, j, s) in
let vf = translate_var_dec map vf in
let vt = translate_var_dec map vt in
let action =
Acase (cond, [Name "true", mk_block ~locals:vt true_act;
Name "false", mk_block ~locals:vf false_act]) in
v, si, j, (control map ck action) :: s
| Minils.Evarpat x,
Minils.Eapp ({ Minils.a_op = Minils.Efield_update;
Minils.a_params = [{ se_desc = Sconstructor f }] },
[e1; e2], _) ->
let x = var_from_name map x in
let copy = Aassgn (x, translate map (si, j, s) e1) in
let action =
Aassgn (mk_lhs (Lfield (x, f)), translate map (si, j, s) e2)
in
v, si, j, (control map ck copy) :: (control map ck action) :: s
| Minils.Evarpat x,
Minils.Eapp ({ Minils.a_op = Minils.Eselect_slice;
Minils.a_params = [idx1; idx2] }, [e], _) ->
let cpt = Idents.fresh "i" in
let e = translate map (si, j, s) e in
let idx = mk_exp (Eop (op_from_string "+",
[mk_evar cpt;
mk_exp (Econst idx1) ])) in
(* bound = (idx2 - idx1) + 1*)
let bound =
mk_static_exp (Sop(op_from_string "+",
[ mk_static_exp (Sint 1);
mk_static_exp (Sop (op_from_string "-",
[idx2;idx1])) ])) in
let action =
Afor (cpt, mk_static_exp (Sint 0), bound,
mk_block [Aassgn (mk_lhs (Larray (var_from_name map x,
mk_evar cpt)),
mk_lhs_exp (Larray (lhs_of_exp e, idx)))] )
in
v, si, j, (control map ck action) :: s
| 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 e1 = translate map (si, j, s) e1 in
let idx = List.map (translate map (si, j, s)) idx in
let true_act =
Aassgn (x, mk_exp (Elhs (lhs_of_idx_list (lhs_of_exp e1) idx))) in
let false_act = Aassgn (x, translate map (si, j, s) e2) in
let cond = bound_check_expr idx bounds in
let action = Acase (cond, [ Name "true", mk_block [true_act];
Name "false", mk_block [false_act] ]) in
v, si, j, (control map ck action) :: s
| Minils.Evarpat x,
Minils.Eapp ({ Minils.a_op = Minils.Eupdate;
Minils.a_params = idx }, [e1; e2], _) ->
let x = var_from_name map x in
let copy = Aassgn (x, translate map (si, j, s) e1) in
let idx = List.map (fun idx -> mk_exp (Econst idx)) idx in
let action = Aassgn (lhs_of_idx_list x idx,
translate map (si, j, s) e2)
in
v, si, j, (control map ck copy) :: (control map ck action) :: s
| Minils.Evarpat x,
Minils.Eapp ({ Minils.a_op = Minils.Earray_fill;
Minils.a_params = [n] }, [e], _) ->
let cpt = Idents.fresh "i" in
let action =
Afor (cpt, mk_static_exp (Sint 0), n,
mk_block [Aassgn (mk_lhs (Larray (var_from_name map x,
mk_evar cpt)),
translate map (si, j, s) e) ])
in
v, si, j, (control map ck action) :: s
| Minils.Evarpat x,
Minils.Eapp ({ Minils.a_op = Minils.Econcat }, [e1; e2], _) ->
let cpt1 = Idents.fresh "i" in
let cpt2 = Idents.fresh "i" in
let x = var_from_name map x in
(match e1.Minils.e_ty, e2.Minils.e_ty with
| Tarray (_, n1), Tarray (_, n2) ->
let e1 = translate map (si, j, s) e1 in
let e2 = translate map (si, j, s) e2 in
let a1 =
Afor (cpt1, mk_static_exp (Sint 0), n1,
mk_block [Aassgn (mk_lhs (Larray (x, mk_evar cpt1)),
mk_lhs_exp (Larray (lhs_of_exp e1,
mk_evar cpt1)))] ) in
let idx = mk_exp (Eop (op_from_string "+",
[ mk_exp (Econst n1); mk_evar cpt2])) in
let a2 =
Afor (cpt2, static_exp_of_int 0, n2,
mk_block [Aassgn (mk_lhs (Larray (x, idx)),
mk_lhs_exp (Larray (lhs_of_exp e2,
mk_evar cpt2)))] )
in
v, si, j, (control map ck a1) :: (control map ck a2) :: s
| _ -> assert false )
| pat, Minils.Eapp ({ Minils.a_op = Minils.Efun _ | Minils.Enode _ } as app,
e_list, r) ->
let name_list = translate_pat map pat in
let c_list = List.map (translate map (si, j, s)) e_list in
let v', si', j', action = mk_node_call map call_context
app loc name_list c_list in
let action = List.map (control map ck) action in
let s = (match r, app.Minils.a_op with
| Some r, Minils.Enode _ ->
let ra = List.map (control map ck) si' in
ra @ action @ s
| _, _ -> action @ s) in
v' @ v, si'@si, j'@j, s
| pat, Minils.Eiterator (it, app, n, e_list, reset) ->
let name_list = translate_pat map pat in
let c_list =
List.map (translate map (si, j, s)) e_list in
let x = Idents.fresh "i" in
let call_context = Oarray ("n", mk_lhs (Lvar x)), Some n in
let si', j', action = translate_iterator map call_context it
name_list app loc n x c_list in
let action = List.map (control map ck) action in
let s =
(match reset, app.Minils.a_op with
| Some r, Minils.Enode _ ->
let ra = List.map (control map ck) si' in
ra @ action @ s
| _, _ -> action @ s)
in (v, si' @ si, j' @ j, s)
| (pat, _) ->
let action = translate_act map (si, j, s) pat e in
let action = List.map (control map ck) action in
v, si, j, action @ s
and translate_eq_list map call_context act_list =
List.fold_right (translate_eq map call_context) act_list ([], [], [], [])
and mk_node_call map call_context app loc name_list args =
match app.Minils.a_op with
| Minils.Enode f | Minils.Efun f ->
let o = mk_obj_call_from_context call_context (gen_obj_name f) in
let obj =
{ o_name = obj_call_name o; o_class = f;
o_params = app.Minils.a_params;
o_size = size_from_call_context call_context; o_loc = loc } in
let si =
(match app.Minils.a_op with
| Minils.Efun _ -> []
| Minils.Enode _ -> [reinit o]) in
[], si, [obj], [Acall (name_list, o, Mstep, args)]
| Minils.Elambda(inp, outp, locals, eq_list) ->
let add_input env vd =
Env.add vd.Minils.v_ident (mk_lhs (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
| Elhs { l_desc = Lvar x } ->
let e =
(try Env.find x env
with Not_found -> e) in
e, env
| _ -> Obc_mapfold.exp funs env e
in
let funs = { Obc_mapfold.defaults with exp = exp } in
let act_list, _ = mapfold (Obc_mapfold.act_it funs) env act_list in
act_list
in
let map = List.fold_left add_input map inp in
let map = List.fold_left2 build map outp name_list in
let map = List.fold_left add_input map locals in
let v, si, j, s = translate_eq_list map call_context eq_list in
let env = List.fold_left2 build Env.empty inp args in
v @ locals, si, j, subst_act_list env s
| _ -> assert false
and translate_iterator map call_context it name_list app loc n x c_list =
let array_of_output name_list =
List.map (fun l -> mk_lhs (Larray (l, mk_evar x))) name_list in
let array_of_input c_list =
List.map (array_elt_of_exp (mk_lhs (Lvar x))) c_list in
match it with
| Minils.Imap ->
let c_list = array_of_input c_list in
let name_list = array_of_output name_list in
let v, si, j, action = mk_node_call map call_context
app loc name_list c_list in
let v = translate_var_dec map v in
let b = mk_block ~locals:v action in
si, j, [ Afor (x, static_exp_of_int 0, n, b) ]
| Minils.Imapfold ->
let (c_list, acc_in) = split_last c_list in
let c_list = array_of_input c_list in
let (name_list, acc_out) = split_last name_list in
let name_list = array_of_output name_list in
let v, si, j, action = mk_node_call map call_context
app loc (name_list @ [ acc_out ])
(c_list @ [ mk_exp (Elhs acc_out) ]) in
let v = translate_var_dec map v in
let b = mk_block ~locals:v action in
si, j, [Aassgn (acc_out, acc_in);
Afor (x, static_exp_of_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 (Elhs acc_out) ]) in
let v = translate_var_dec map v in
let b = mk_block ~locals:v action in
si, j, [ Aassgn (acc_out, acc_in);
Afor (x, static_exp_of_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 x; mk_exp (Elhs acc_out) ]) in
let v = translate_var_dec map v in
let b = mk_block ~locals:v action in
si, j, [ Aassgn (acc_out, acc_in);
Afor (x, static_exp_of_int 0, n, b) ]
let remove m d_list =
List.filter (fun { Minils.v_ident = n } -> not (List.mem_assoc n m)) d_list
let translate_contract map mem_vars =
function
| None -> ([], [], [], [])
| Some
{
Minils.c_eq = eq_list;
Minils.c_local = d_list;
Minils.c_assume = e_a;
Minils.c_enforce = e_c
} ->
let (v, si, j, s_list) = translate_eq_list map
empty_call_context eq_list in
let d_list = translate_var_dec map (v @ d_list) in
let d_list = List.filter
(fun vd -> not (List.mem vd.v_ident mem_vars)) d_list in
(si, j, s_list, d_list)
(** Returns a map, mapping variables names to the variables
where they will be stored. *)
let subst_map inputs outputs locals mems =
(* Create a map that simply maps each var to itself *)
let m =
List.fold_left
(fun m { Minils.v_ident = x } -> Env.add x (mk_lhs (Lvar x)) m)
Env.empty (inputs @ outputs @ locals)
in
List.fold_left (fun m x -> Env.add x (mk_lhs (Lmem x)) m) m mems
let translate_node
({
Minils.n_name = f;
Minils.n_input = i_list;
Minils.n_output = o_list;
Minils.n_local = d_list;
Minils.n_equs = eq_list;
Minils.n_contract = contract;
Minils.n_params = params;
Minils.n_loc = loc;
} as n) =
let mem_vars = Mls_utils.node_memory_vars n in
let subst_map = subst_map i_list o_list d_list mem_vars in
let (v, si, j, s_list) = translate_eq_list subst_map
empty_call_context eq_list in
let (si', j', s_list', d_list') =
translate_contract subst_map mem_vars contract in
let i_list = translate_var_dec subst_map i_list in
let o_list = translate_var_dec subst_map o_list in
let d_list = translate_var_dec subst_map (v @ d_list) in
let m, d_list = List.partition
(fun vd -> List.mem vd.v_ident mem_vars) d_list in
let s = joinlist (s_list @ s_list') in
let j = j' @ j in
let si = joinlist (si @ si') in
let stepm = {
m_name = Mstep; m_inputs = i_list; m_outputs = o_list;
m_body = mk_block ~locals:(d_list' @ d_list) s } in
let resetm = {
m_name = Mreset; m_inputs = []; m_outputs = [];
m_body = mk_block si } in
{ cd_name = f; cd_mems = m; cd_params = params;
cd_objs = j; cd_methods = [stepm; resetm];
cd_loc = loc }
let translate_ty_def { Minils.t_name = name; Minils.t_desc = tdesc;
Minils.t_loc = loc } =
let tdesc =
match tdesc with
| Minils.Type_abs -> Type_abs
| Minils.Type_enum tag_name_list -> Type_enum tag_name_list
| Minils.Type_struct field_ty_list ->
Type_struct field_ty_list
in { t_name = name; t_desc = tdesc; t_loc = loc }
let translate_const_def { Minils.c_name = name; Minils.c_value = se;
Minils.c_type = ty; Minils.c_loc = loc } =
{ c_name = name;
c_value = se;
c_type = ty;
c_loc = loc }
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
} =
{
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_defs = List.map translate_node p_node_list;
}