First try at a normalization in Heptagon
I can't see if it compiles yet
This commit is contained in:
Cédric Pasteur
parent
2c7b609d2e
commit
cbf92beba2
4 changed files with 257 additions and 363 deletions
|
|
@ -53,6 +53,9 @@ let compile_program p =
|
|||
(* Every *)
|
||||
let p = pass "Every" true Every.program p pp in
|
||||
|
||||
(* Normalization *)
|
||||
let p = pass "Normalization" true Normalize.program p pp in
|
||||
|
||||
(* Block flatten *)
|
||||
let p = pass "Block" true Block.program p pp in
|
||||
|
||||
|
|
|
|||
253
compiler/heptagon/transformations/normalize.ml
Normal file
253
compiler/heptagon/transformations/normalize.ml
Normal file
|
|
@ -0,0 +1,253 @@
|
|||
(**************************************************************************)
|
||||
(* *)
|
||||
(* Heptagon *)
|
||||
(* *)
|
||||
(* Author : Marc Pouzet *)
|
||||
(* Organization : Demons, LRI, University of Paris-Sud, Orsay *)
|
||||
(* *)
|
||||
(**************************************************************************)
|
||||
open Misc
|
||||
open Initial
|
||||
open Names
|
||||
open Idents
|
||||
open Signature
|
||||
open Heptagon
|
||||
open Types
|
||||
open Clocks
|
||||
|
||||
|
||||
(** Normalization pass
|
||||
The normal form of the language is given in the manual *)
|
||||
|
||||
module Error =
|
||||
struct
|
||||
type error =
|
||||
| Eunsupported_language_construct
|
||||
|
||||
let message loc kind =
|
||||
begin match kind with
|
||||
| Eunsupported_language_construct ->
|
||||
eprintf "%aThis construct is not supported by MiniLS.@."
|
||||
print_location loc
|
||||
end;
|
||||
raise Errors.Error
|
||||
end
|
||||
|
||||
let is_list e = match e.e_desc with
|
||||
| Eapp({ a_op = Etuple }, e_list, _)
|
||||
| Econst { se_desc = Stuple se_list } -> true
|
||||
| _ -> false
|
||||
|
||||
let e_to_e_list e = match e.e_desc with
|
||||
| Eapp({ a_op = Etuple }, e_list, _) -> e_list
|
||||
| Econst { se_desc = Stuple se_list } ->
|
||||
exp_list_of_static_exp_list se_list
|
||||
|
||||
let flatten_e_list l =
|
||||
let flatten = function
|
||||
| { e_desc = Eapp({ a_op = Etuple }, l, _) } -> l
|
||||
| e -> [e]
|
||||
in
|
||||
List.flatten (List.map flatten l)
|
||||
|
||||
let equation (d_list, eq_list) e =
|
||||
let add_one_var ty d_list =
|
||||
let n = Idents.gen_var "normalize" "v" in
|
||||
let d_list = (mk_var_dec ~clock:e.e_ck n ty) :: d_list in
|
||||
n, d_list
|
||||
in
|
||||
match e.e_ty with
|
||||
| Tprod ty_list ->
|
||||
let var_list, d_list =
|
||||
mapfold (fun d_list ty -> add_one_var ty d_list) d_list ty_list in
|
||||
let pat_list = List.map (fun n -> Evarpat n) var_list in
|
||||
let eq_list = (mk_equation (Etuplepat pat_list) e) :: eq_list in
|
||||
let e_list = List.map2
|
||||
(fun n ty -> mk_exp ~ty:ty (Evar n)) var_list ty_list in
|
||||
let e = Eapp(mk_app Etuple, e_list, None) in
|
||||
(d_list, eq_list), e
|
||||
| _ ->
|
||||
let n, d_list = add_one_var e.e_ty d_list in
|
||||
let eq_list = (mk_equation (Evarpat n) e) :: eq_list in
|
||||
(d_list, eq_list), Evar n
|
||||
|
||||
(* [(e1,...,ek) when C(n) = (e1 when C(n),...,ek when C(n))] *)
|
||||
let rec whenc context e c n =
|
||||
let when_on_c c n e =
|
||||
{ e with e_desc = Ewhen(e, c, n); e_ck = Con(e.e_ck, c, n) }
|
||||
in
|
||||
if is_list e then (
|
||||
let e_list = List.map (when_on_c c n) (e_to_e_list e) in
|
||||
context, { e with e_desc = Eapp (app, e_list, r);
|
||||
e_ck = Con(e.e_ck, c, n) }
|
||||
) else
|
||||
context, when_on_c c n e
|
||||
|
||||
let const e c =
|
||||
let rec const = function
|
||||
| Cbase | Cvar { contents = Cindex _ } -> c
|
||||
| Con(ck_on, tag, x) ->
|
||||
Ewhen({ e with e_desc = const ck_on; e_ck = ck_on }, tag, x)
|
||||
| Cvar { contents = Clink ck } -> const ck in
|
||||
const e.e_ck
|
||||
|
||||
type kind = ExtValue | Any
|
||||
|
||||
let add context expected_kind ({ e_desc = de } as e) =
|
||||
let up = match de, expected_kind with
|
||||
| (Evar _ | Eapp ({ a_op = Efield }, _, _) | Ewhen _
|
||||
| Eapp ({ a_op = Etuple }, _, _) | Econst) , ExtValue -> false
|
||||
| _ , ExtValue -> true
|
||||
| _ -> false in
|
||||
if up then
|
||||
let context, n = equation context e in
|
||||
context, { e with e_desc = n }
|
||||
else
|
||||
context, e
|
||||
|
||||
let rec translate kind context e =
|
||||
let context, e = match e.e_desc with
|
||||
| Econst c -> context, { e with e_desc = const e (Econst c) }
|
||||
| Evar _ -> context, e
|
||||
| Epre(v, e1) -> fby kind context e v e1
|
||||
| Efby({ e_desc = Econst v }, e1) -> fby kind context e (Some v) e1
|
||||
| Estruct l ->
|
||||
let translate_field (f, e) context =
|
||||
let context, e = translate ExtValue context e in
|
||||
context, (f, e)
|
||||
in
|
||||
let context, l = mapfold translate_field context l in
|
||||
context, { e with e_desc = Estruct l }
|
||||
| Ewhen(e1, c, n) ->
|
||||
let context, e1 = translate kind context e1 in
|
||||
whenc context e1 c n
|
||||
| Emerge(n, tag_e_list) ->
|
||||
merge context n tag_e_list
|
||||
| Eapp({ a_op = Eifthenelse }, [e1; e2; e3], _) ->
|
||||
ifthenelse context e1 e2 e3
|
||||
| Eapp(app, e_list, r) ->
|
||||
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_local nd.n_equs in
|
||||
let nd = { nd with n_equs = eq_list; n_local = d_list } 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,
|
||||
flatten_e_list e_list, reset) }
|
||||
| Elast _ | Efby _ -> message e.e_loc Eunsupported_language_construct
|
||||
in add context kind e
|
||||
|
||||
and translate_list kind context e_list =
|
||||
match e_list with
|
||||
| [] -> context, []
|
||||
| e :: e_list ->
|
||||
let context, e = translate kind context e in
|
||||
let context, e_list = translate_list kind context e_list in
|
||||
context, e :: e_list
|
||||
|
||||
and fby kind context e v e1 =
|
||||
let mk_fby c e =
|
||||
mk_exp ~ty:e.e_ty ~loc:e.e_loc (Efby(Some c, e)) in
|
||||
let mk_pre e =
|
||||
mk_exp ~ty:e.e_ty ~loc:e.e_loc (Efby(None, e)) in
|
||||
let e1 = translate ExtValue context e1 in
|
||||
match e1.e_desc, v with
|
||||
| Eapp({ a_op = Etuple } as app, e_list, r),
|
||||
Some { se_desc = Stuple se_list } ->
|
||||
let e_list = List.map2 mk_fby se_list e_list in
|
||||
let e = { e with e_desc = Eapp(app, e_list, r) } in
|
||||
translate kind context e
|
||||
| Econst { se_desc = Stuple se_list },
|
||||
Some { se_desc = Stuple v_list } ->
|
||||
let e_list = List.map2 mk_fby v_list
|
||||
(exp_list_of_static_exp_list se_list) in
|
||||
let e = { e with e_desc = Eapp(mk_app Etuple, e_list, None) } in
|
||||
translate kind context e
|
||||
| Eapp({ a_op = Etuple } as app, e_list, r), None ->
|
||||
let e_list = List.map mk_pre e_list in
|
||||
let e = { e with e_desc = Eapp(app, e_list, r) } in
|
||||
translate kind context e
|
||||
| Econst { se_desc = Stuple se_list }, None ->
|
||||
let e_list = List.map mk_pre (exp_list_of_static_exp_list se_list) in
|
||||
let e = { e with e_desc = Eapp(app, e_list, r) } in
|
||||
translate kind context e
|
||||
| _ -> context, { e with e_desc = Efby(v, e1) }
|
||||
|
||||
(** transforms [if x then e1, ..., en else e'1,..., e'n]
|
||||
into [if x then e1 else e'1, ..., if x then en else e'n] *)
|
||||
and ifthenelse context e e1 e2 e3 =
|
||||
let context, e1 = translate ExtValue context e1 in
|
||||
let context, e2 = translate ExtValue context e2 in
|
||||
let context, e3 = translate ExtValue context e3 in
|
||||
let mk_ite_list e2_list e3_list =
|
||||
let mk_ite e2 e3 =
|
||||
mk_exp ~ty:e2.e_ty ~loc:e.e_loc (Eifthenelse(e1, e2, e3))
|
||||
in
|
||||
let e_list = List.map2 mk_ite e2_list e3_list in
|
||||
{ e with e_desc = Eapp(mk_app Etuple, e_list, None) }
|
||||
in
|
||||
if is_list e2 then
|
||||
context, mk_ite_list context (e_to_e_list e2) (e_to_e_list e2)
|
||||
else
|
||||
context, { e with e_desc = Eifthenelse(e1, e2, e3)}
|
||||
|
||||
(** transforms [merge x (c1, (e11,...,e1n));...;(ck, (ek1,...,ekn))] into
|
||||
[merge x (c1, e11)...(ck, ek1),..., merge x (c1, e1n)...(ck, ekn)] *)
|
||||
and merge context e x c_e_list =
|
||||
let translate_tag (tag, e) context =
|
||||
let context, e = translate ExtValue context e in
|
||||
context, (tag, e)
|
||||
in
|
||||
let mk_merge x c_list e_list =
|
||||
let ty = (hd e_list).e_e_ty in
|
||||
let t_e_list = List.map2 (fun t e -> (t,e)) c_list e_list in
|
||||
mk_exp ~ty:ty ~loc:e.e_loc (Emerge(x, t_e_list))
|
||||
in
|
||||
let context, x = translate ExtValue context x in
|
||||
let context, c_e_list = mapfold translate_tag context ta_list in
|
||||
match c_e_list with
|
||||
| [] -> assert false
|
||||
| (_,e)::_ ->
|
||||
if is_list e then
|
||||
let c_list = List.map (fun (t,_) -> t) c_e_list in
|
||||
let e_lists = List.map (fun (_,e) -> e_to_e_list e) c_e_list in
|
||||
let e_list = List.map (mk_merge x c_list) e_lists in
|
||||
context, { e with e_desc = Eapp(mk_app Etuple, e_list, None) }
|
||||
else
|
||||
context, { e with e_desc = Emerge(x, c_e_list) }
|
||||
|
||||
(* applies distribution rules *)
|
||||
(* [x = v fby e] should verifies that x is local *)
|
||||
(* [(p1,...,pn) = (e1,...,en)] into [p1 = e1;...;pn = en] *)
|
||||
and distribute ((d_list, eq_list) as context) pat e =
|
||||
match pat, e.e_desc with
|
||||
| Evarpat(x), Efby _ when not (vd_mem x d_list) ->
|
||||
let (d_list, eq_list), n = equation context e in
|
||||
d_list,
|
||||
{ eq with eq_rhs = { e with e_desc = n } } :: eq_list
|
||||
| Etuplepat(pat_list), Eapp({ a_op = Etuple }, e_list, _) ->
|
||||
let eqs = List.map2 mk_equation pat_list e_list in
|
||||
List.fold_left distribute context eqs
|
||||
| _ -> d_list, Eeq(pat, e) :: eq_list
|
||||
|
||||
and translate_eq context eq = match eq with
|
||||
| Eeq (pat, e) ->
|
||||
let context, e = translate Any context e in
|
||||
distribute context pat e
|
||||
| _ -> raise Fallback
|
||||
|
||||
let block funs _ b =
|
||||
let _, (v_acc, eq_acc) = Hept_mapfold.block funs ([],[]) b in
|
||||
{ b with b_local = v_acc@b.b_local; b_equs = eq_acc}, ([], [])
|
||||
|
||||
let program p =
|
||||
let funs = { defaults with eq = translate_eq; } in
|
||||
let p, _ = Hept_mapfold.program funs ([], []) p in
|
||||
p
|
||||
|
|
@ -48,7 +48,7 @@ and extvalue = {
|
|||
and extvalue_desc =
|
||||
| Wconst of static_exp
|
||||
| Wvar of var_ident
|
||||
| Wfield of ext_value * field_name
|
||||
| Wfield of extvalue * field_name
|
||||
| Wwhen of extvalue * constructor_name * var_ident
|
||||
(** extvalue when Constructor(ident) *)
|
||||
|
||||
|
|
|
|||
|
|
@ -1,362 +0,0 @@
|
|||
(**************************************************************************)
|
||||
(* *)
|
||||
(* Heptagon *)
|
||||
(* *)
|
||||
(* Author : Marc Pouzet *)
|
||||
(* Organization : Demons, LRI, University of Paris-Sud, Orsay *)
|
||||
(* *)
|
||||
(**************************************************************************)
|
||||
open Misc
|
||||
open Initial
|
||||
open Names
|
||||
open Idents
|
||||
open Signature
|
||||
open Minils
|
||||
open Mls_utils
|
||||
open Types
|
||||
open Clocks
|
||||
|
||||
let flatten_e_list l =
|
||||
let flatten = function
|
||||
| { e_desc = Eapp({ a_op = Etuple }, l, _) } -> l
|
||||
| e -> [e]
|
||||
in
|
||||
List.flatten (List.map flatten l)
|
||||
|
||||
let equation (d_list, eq_list) e =
|
||||
let add_one_var ty d_list =
|
||||
let n = Idents.gen_var "normalize" "v" in
|
||||
let d_list = (mk_var_dec ~clock:e.e_ck n ty) :: d_list in
|
||||
n, d_list
|
||||
in
|
||||
match e.e_ty with
|
||||
| Tprod ty_list ->
|
||||
let var_list, d_list =
|
||||
mapfold (fun d_list ty -> add_one_var ty d_list) d_list ty_list in
|
||||
let pat_list = List.map (fun n -> Evarpat n) var_list in
|
||||
let eq_list = (mk_equation (Etuplepat pat_list) e) :: eq_list in
|
||||
let e_list = List.map2
|
||||
(fun n ty -> mk_exp ~ty:ty (Evar n)) var_list ty_list in
|
||||
let e = Eapp(mk_app Etuple, e_list, None) in
|
||||
(d_list, eq_list), e
|
||||
| _ ->
|
||||
let n, d_list = add_one_var e.e_ty d_list in
|
||||
let eq_list = (mk_equation (Evarpat n) e) :: eq_list in
|
||||
(d_list, eq_list), Evar n
|
||||
|
||||
let intro context e =
|
||||
match e.e_desc with
|
||||
| Evar n -> context, Evar n
|
||||
| _ -> equation context e
|
||||
|
||||
(* distribution: [(e1,...,ek) when C(n) = (e1 when C(n),...,ek when C(n))] *)
|
||||
let rec whenc context e c n =
|
||||
let when_on_c c n e =
|
||||
{ e with e_desc = Ewhen(e, c, n); e_ck = Con(e.e_ck, c, n) } in
|
||||
|
||||
match e.e_desc with
|
||||
| Eapp({ a_op = Etuple } as app, e_list, r) ->
|
||||
let context, e_list =
|
||||
List.fold_right
|
||||
(fun e (context, e_list) -> let context, e = whenc context e c n in
|
||||
(context, e :: e_list))
|
||||
e_list (context, []) in
|
||||
context, { e with e_desc = Eapp (app, e_list, r);
|
||||
e_ck = Con(e.e_ck, c, n) }
|
||||
| Econst { se_desc = Stuple se_list } ->
|
||||
let e_list = exp_list_of_static_exp_list se_list in
|
||||
let context, e_list =
|
||||
List.fold_right
|
||||
(fun e (context, e_list) -> let context, e = whenc context e c n in
|
||||
(context, e :: e_list))
|
||||
e_list (context, []) in
|
||||
context, { e with e_desc = Eapp (mk_app Etuple, e_list, None);
|
||||
e_ck = Con(e.e_ck, c, n) }
|
||||
|
||||
(* | Emerge _ -> let context, x = equation context e in
|
||||
context, when_on_c c n { e with e_desc = Evar(x) } *)
|
||||
| _ -> context, when_on_c c n e
|
||||
|
||||
(* transforms [merge x (c1, (e11,...,e1n));...;(ck, (ek1,...,ekn))] into *)
|
||||
(* [merge x (c1, e11)...(ck, ek1),..., merge x (c1, e1n)...(ck, ekn)] *)
|
||||
let rec merge e x ci_a_list =
|
||||
let rec split ci_tas_list =
|
||||
match ci_tas_list with
|
||||
| [] | (_, _, []) :: _ -> [], []
|
||||
| (ci, b, a :: tas) :: ci_tas_list ->
|
||||
let ci_ta_list, ci_tas_list = split ci_tas_list in
|
||||
(ci, a) :: ci_ta_list, (ci, b, tas) :: ci_tas_list in
|
||||
let rec distribute ci_tas_list =
|
||||
match ci_tas_list with
|
||||
| [] | (_, _, []) :: _ -> []
|
||||
| (_, b, (eo :: _)) :: _ ->
|
||||
let ci_ta_list, ci_tas_list = split ci_tas_list in
|
||||
let ci_tas_list = distribute ci_tas_list in
|
||||
(if b then
|
||||
{ eo with e_desc = Emerge(x, ci_ta_list);
|
||||
e_ck = e.e_ck; e_loc = e.e_loc }
|
||||
else
|
||||
merge e x ci_ta_list)
|
||||
:: ci_tas_list in
|
||||
let rec erasetuple ci_a_list =
|
||||
match ci_a_list with
|
||||
| [] -> []
|
||||
| (ci, { e_desc = Eapp({ a_op = Etuple }, l, _) }) :: ci_a_list ->
|
||||
(ci, false, l) :: erasetuple ci_a_list
|
||||
| (ci, { e_desc = Econst { se_desc = Stuple se_list } }) :: ci_a_list ->
|
||||
let l = exp_list_of_static_exp_list se_list in
|
||||
(ci, false, l) :: erasetuple ci_a_list
|
||||
| (ci, e) :: ci_a_list ->
|
||||
(ci, true, [e]) :: erasetuple ci_a_list in
|
||||
let ci_tas_list = erasetuple ci_a_list in
|
||||
let ci_tas_list = distribute ci_tas_list in
|
||||
match ci_tas_list with
|
||||
| [e] -> e
|
||||
| l -> { e with e_desc = Eapp(mk_app Etuple, l, None) }
|
||||
|
||||
let ifthenelse context e1 e2 e3 =
|
||||
let context, n = intro context e1 in
|
||||
let n = (match n with Evar n -> n | _ -> assert false) in
|
||||
let context, e2 = whenc context e2 ptrue n in
|
||||
let context, e3 = whenc context e3 pfalse n in
|
||||
context, merge e1 n [ptrue, e2; pfalse, e3]
|
||||
|
||||
let const e c =
|
||||
let rec const = function
|
||||
| Cbase | Cvar { contents = Cindex _ } -> c
|
||||
| Con(ck_on, tag, x) ->
|
||||
Ewhen({ e with e_desc = const ck_on; e_ck = ck_on }, tag, x)
|
||||
| Cvar { contents = Clink ck } -> const ck in
|
||||
const e.e_ck
|
||||
|
||||
(* normal form for expressions and equations: *)
|
||||
(* - e ::= op(e,...,e) | x | C | e when C(x) *)
|
||||
(* - act ::= e | merge x (C1 -> act) ... (Cn -> act) | (act,...,act) *)
|
||||
(* - eq ::= [x = v fby e] | [pat = act] | [pat = f(e1,...,en) every n *)
|
||||
(* - A-normal form: (e1,...,en) when c(x) = (e1 when c(x),...,en when c(x) *)
|
||||
type kind = VRef | Exp | Act | Any
|
||||
|
||||
let function_args_kind = Exp
|
||||
let merge_kind = Act
|
||||
|
||||
let rec constant e = match e.e_desc with
|
||||
| Econst _ -> true
|
||||
| Ewhen(e, _, _) -> constant e
|
||||
| Evar _ -> true
|
||||
| _ -> false
|
||||
|
||||
let add context expected_kind ({ e_desc = de } as e) =
|
||||
let up = match de, expected_kind with
|
||||
| (Evar _ | Eapp ({ a_op = Efield }, _, _)) , VRef -> false
|
||||
| _ , VRef -> true
|
||||
| Eapp ({ a_op = Efun n }, _, _),
|
||||
(Exp|Act) when is_op n -> false
|
||||
| Eapp ({ a_op = Eequal }, _, _), (Exp|Act) -> false
|
||||
| ( Emerge _ | Eapp _ | Eiterator _ | Efby _ ), Exp -> true
|
||||
| ( Eapp({ a_op = Efun _ | Enode _ }, _, _)
|
||||
| Eiterator _ | Efby _ ), Act -> true
|
||||
| _ -> false in
|
||||
if up then
|
||||
let context, n = equation context e in
|
||||
context, { e with e_desc = n }
|
||||
else context, e
|
||||
|
||||
let rec translate kind context e =
|
||||
let context, e = match e.e_desc with
|
||||
| Emerge(n, tag_e_list) ->
|
||||
let context, ta_list =
|
||||
List.fold_right
|
||||
(fun (tag, e) (context, ta_list) ->
|
||||
let context, act = translate merge_kind context e in
|
||||
context, ((tag, act) :: ta_list))
|
||||
tag_e_list (context, []) in
|
||||
context, merge e n ta_list
|
||||
| Ewhen(e1, c, n) ->
|
||||
let context, e1 = translate kind context e1 in
|
||||
whenc context e1 c n
|
||||
| Efby(v, e1) ->
|
||||
let context, e1 = translate Act context e1 in
|
||||
fby kind context e v e1
|
||||
| Evar _ -> context, e
|
||||
| Econst c -> context, { e with e_desc = const e (Econst c) }
|
||||
| Estruct(l) ->
|
||||
let context, l =
|
||||
List.fold_right
|
||||
(fun (field, e) (context, field_desc_list) ->
|
||||
let context, e = translate Exp context e in
|
||||
context, ((field, e) :: field_desc_list))
|
||||
l (context, []) in
|
||||
context, { e with e_desc = Estruct l }
|
||||
| Eapp({ a_op = Eifthenelse }, [e1; e2; e3], _) ->
|
||||
let context, e1 = translate Any context e1 in
|
||||
let context, e2 = translate Act context e2 in
|
||||
let context, e3 = translate Act context e3 in
|
||||
ifthenelse context e1 e2 e3
|
||||
| Eapp({ a_op = Efun _ | Enode _ } as app, e_list, r) ->
|
||||
let context, e_list =
|
||||
translate_list function_args_kind context e_list in
|
||||
context, { e with e_desc = Eapp(app, flatten_e_list e_list, r) }
|
||||
| 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, 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_local nd.n_equs in
|
||||
let nd = { nd with n_equs = eq_list; n_local = d_list } in
|
||||
Itfusion.replace_anon_node f nd
|
||||
| _ -> () );
|
||||
|
||||
(* Add an intermediate equation for each array lit argument. *)
|
||||
let translate_iterator_arg_list context e_list =
|
||||
let add e context =
|
||||
let kind = match e.e_desc with
|
||||
| Econst { se_desc = Sarray _; } -> VRef
|
||||
| _ -> function_args_kind in
|
||||
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, flatten_e_list pe_list,
|
||||
flatten_e_list e_list, reset) }
|
||||
in add context kind e
|
||||
|
||||
and translate_app kind context op e_list =
|
||||
match op with
|
||||
| Eequal ->
|
||||
let context, e_list =
|
||||
translate_list function_args_kind context e_list in
|
||||
context, e_list
|
||||
| Etuple ->
|
||||
let context, e_list = translate_list kind context e_list in
|
||||
context, e_list
|
||||
| Efield ->
|
||||
let e' = assert_1 e_list in
|
||||
let context, e' = translate Exp context e' in
|
||||
context, [e']
|
||||
| Efield_update ->
|
||||
let e1, e2 = assert_2 e_list in
|
||||
let context, e1 = translate VRef context e1 in
|
||||
let context, e2 = translate Exp context e2 in
|
||||
context, [e1; e2]
|
||||
| Earray ->
|
||||
let context, e_list = translate_list kind context e_list in
|
||||
context, e_list
|
||||
| Earray_fill ->
|
||||
let e = assert_1 e_list in
|
||||
let context, e = translate Exp context e in
|
||||
context, [e]
|
||||
| Eselect ->
|
||||
let e' = assert_1 e_list in
|
||||
let context, e' = translate VRef context e' in
|
||||
context, [e']
|
||||
| Eselect_dyn ->
|
||||
let e1, e2, idx = assert_2min e_list in
|
||||
let context, e1 = translate VRef context e1 in
|
||||
let context, idx = translate_list Exp context idx in
|
||||
let context, e2 = translate Exp context e2 in
|
||||
context, e1::e2::idx
|
||||
| Eselect_trunc ->
|
||||
let e1, idx = assert_1min e_list in
|
||||
let context, e1 = translate VRef context e1 in
|
||||
let context, idx = translate_list Exp context idx in
|
||||
context, e1::idx
|
||||
| Eupdate ->
|
||||
let e1, e2, idx = assert_2min e_list in
|
||||
let context, e1 = translate VRef context e1 in
|
||||
let context, idx = translate_list Exp context idx in
|
||||
let context, e2 = translate Exp context e2 in
|
||||
context, e1::e2::idx
|
||||
| Eselect_slice ->
|
||||
let e' = assert_1 e_list in
|
||||
let context, e' = translate VRef context e' in
|
||||
context, [e']
|
||||
| Econcat ->
|
||||
let e1, e2 = assert_2 e_list in
|
||||
let context, e1 = translate VRef context e1 in
|
||||
let context, e2 = translate VRef context e2 in
|
||||
context, [e1; e2]
|
||||
| Enode _ | Efun _ | Eifthenelse _ ->
|
||||
assert false (*already done in translate*)
|
||||
|
||||
and translate_list kind context e_list =
|
||||
match e_list with
|
||||
[] -> context, []
|
||||
| e :: e_list ->
|
||||
let context, e = translate kind context e in
|
||||
let context, e_list = translate_list kind context e_list in
|
||||
context, e :: e_list
|
||||
|
||||
and fby kind context e v e1 =
|
||||
let mk_fby c e =
|
||||
mk_exp ~ty:e.e_ty ~loc:e.e_loc (Efby(Some c, e)) in
|
||||
let mk_pre e =
|
||||
mk_exp ~ty:e.e_ty ~loc:e.e_loc (Efby(None, e)) in
|
||||
match e1.e_desc, v with
|
||||
| Eapp({ a_op = Etuple } as app, e_list, r),
|
||||
Some { se_desc = Stuple se_list } ->
|
||||
let e_list = List.map2 mk_fby se_list e_list in
|
||||
let e = { e with e_desc = Eapp(app, e_list, r) } in
|
||||
translate kind context e
|
||||
| Econst { se_desc = Stuple se_list },
|
||||
Some { se_desc = Stuple v_list } ->
|
||||
let e_list = List.map2 mk_fby v_list
|
||||
(exp_list_of_static_exp_list se_list) in
|
||||
let e = { e with e_desc = Eapp(mk_app Etuple, e_list, None) } in
|
||||
translate kind context e
|
||||
| Eapp({ a_op = Etuple } as app, e_list, r), None ->
|
||||
let e_list = List.map mk_pre e_list in
|
||||
let e = { e with e_desc = Eapp(app, e_list, r) } in
|
||||
translate kind context e
|
||||
| Econst { se_desc = Stuple _ }, None ->
|
||||
context, e1
|
||||
| _ ->
|
||||
let context, e1' =
|
||||
if constant e1 then context, e1
|
||||
else let context, n = equation context e1 in
|
||||
context, { e1 with e_desc = n } in
|
||||
context, { e with e_desc = Efby(v, e1') }
|
||||
|
||||
and translate_eq context eq =
|
||||
(* applies distribution rules *)
|
||||
(* [x = v fby e] should verifies that x is local *)
|
||||
(* [(p1,...,pn) = (e1,...,en)] into [p1 = e1;...;pn = en] *)
|
||||
let rec distribute ((d_list, eq_list) as context)
|
||||
({ eq_lhs = pat; eq_rhs = e } as eq) =
|
||||
match pat, e.e_desc with
|
||||
| Evarpat(x), Efby _ when not (vd_mem x d_list) ->
|
||||
let (d_list, eq_list), n = equation context e in
|
||||
d_list,
|
||||
{ eq with eq_rhs = { e with e_desc = n } } :: eq_list
|
||||
| Etuplepat(pat_list), Eapp({ a_op = Etuple }, e_list, _) ->
|
||||
let eqs = List.map2 mk_equation pat_list e_list in
|
||||
List.fold_left distribute context eqs
|
||||
| _ -> d_list, eq :: eq_list in
|
||||
|
||||
let context, e = translate Any context eq.eq_rhs in
|
||||
distribute context { eq with eq_rhs = e }
|
||||
|
||||
and translate_eq_list d_list eq_list =
|
||||
List.fold_left
|
||||
(fun context eq -> translate_eq context eq)
|
||||
(d_list, []) eq_list
|
||||
|
||||
let translate_contract ({ c_eq = eq_list; c_local = d_list } as c) =
|
||||
let d_list,eq_list = translate_eq_list d_list eq_list in
|
||||
{ c with
|
||||
c_local = d_list;
|
||||
c_eq = eq_list }
|
||||
|
||||
let translate_node ({ n_contract = contract;
|
||||
n_local = d_list; n_equs = eq_list } as node) =
|
||||
let contract = optional translate_contract contract in
|
||||
let d_list, eq_list = translate_eq_list d_list eq_list in
|
||||
{ node with n_contract = contract; n_local = d_list; n_equs = eq_list }
|
||||
|
||||
let program ({ p_nodes = p_node_list } as p) =
|
||||
{ p with p_nodes = List.map translate_node p_node_list }
|
||||
Loading…
Reference in a new issue