More refactoring of reset
Use exp option to store resets instead of introducing a new type.
This commit is contained in:
parent
f752f895ce
commit
af0d28fda0
|
@ -46,46 +46,29 @@ let mk_bool_var n =
|
||||||
let mk_bool_param n =
|
let mk_bool_param n =
|
||||||
mk_var_dec n (Tid Initial.pbool)
|
mk_var_dec n (Tid Initial.pbool)
|
||||||
|
|
||||||
let or_op_call = mk_op (Efun Initial.por)
|
let or_op_call e_list = mk_op_app (Efun Initial.por) e_list
|
||||||
|
|
||||||
let pre_true e =
|
let pre_true e =
|
||||||
{ e with e_desc = Epre (Some (mk_static_exp ~ty:(Tid Initial.pbool)
|
{ e with e_desc = Epre (Some (mk_static_exp ~ty:(Tid Initial.pbool)
|
||||||
(Sconstructor Initial.ptrue)), e) }
|
(Sconstructor Initial.ptrue)), e) }
|
||||||
let init e = pre_true { dfalse with e_loc = e.e_loc }
|
let init e = pre_true { dfalse with e_loc = e.e_loc }
|
||||||
|
|
||||||
(* the boolean condition for a structural reset *)
|
let add_resets res e =
|
||||||
type reset =
|
match res, e with
|
||||||
| Rfalse
|
| None, _ -> e
|
||||||
| Rorthen of reset * ident
|
| _, None -> res
|
||||||
|
| Some re, Some e -> Some { e with e_desc = or_op_call [re; e] }
|
||||||
let rfalse = Rfalse
|
|
||||||
let rvar n = Rorthen(Rfalse, n)
|
|
||||||
|
|
||||||
let true_reset = function
|
|
||||||
| Rfalse -> false
|
|
||||||
| _ -> true
|
|
||||||
|
|
||||||
let rec or_op res e =
|
|
||||||
match res with
|
|
||||||
| Rfalse -> e
|
|
||||||
| Rorthen(res, n) ->
|
|
||||||
or_op res { e with e_desc = Eapp(or_op_call, [mk_bool_var n; e], None) }
|
|
||||||
|
|
||||||
let default e =
|
let default e =
|
||||||
match e.e_desc with
|
match e.e_desc with
|
||||||
| Econst c -> Some c
|
| Econst c -> Some c
|
||||||
| _ -> None
|
| _ -> None
|
||||||
|
|
||||||
let exp_of_res res =
|
|
||||||
match res with
|
|
||||||
| Rfalse -> dfalse
|
|
||||||
| Rorthen(res, n) -> or_op res (mk_bool_var n)
|
|
||||||
|
|
||||||
let ifres res e2 e3 =
|
let ifres res e2 e3 =
|
||||||
match res with
|
match res with
|
||||||
| Rfalse -> mk_op_app Eifthenelse [init e3; e2; e3]
|
| None -> mk_op_app Eifthenelse [init e3; e2; e3]
|
||||||
| _ -> (* a reset occurs *)
|
| Some re -> (* a reset occurs *)
|
||||||
mk_op_app Eifthenelse [exp_of_res res; e2; e3]
|
mk_op_app Eifthenelse [re; e2; e3]
|
||||||
|
|
||||||
(* add an equation *)
|
(* add an equation *)
|
||||||
let equation v acc_eq_list e =
|
let equation v acc_eq_list e =
|
||||||
|
@ -96,10 +79,10 @@ let equation v acc_eq_list e =
|
||||||
|
|
||||||
let orthen v acc_eq_list res e =
|
let orthen v acc_eq_list res e =
|
||||||
match e.e_desc with
|
match e.e_desc with
|
||||||
| Evar(n) -> v, acc_eq_list, Rorthen(res, n)
|
| Evar n -> add_resets res (Some e), v, acc_eq_list
|
||||||
| _ ->
|
| _ ->
|
||||||
let n, v, acc_eq_list = equation v acc_eq_list e in
|
let n, v, acc_eq_list = equation v acc_eq_list e in
|
||||||
v, acc_eq_list, Rorthen(res, n)
|
add_resets res (Some { e with e_desc = Evar n }), v, acc_eq_list
|
||||||
|
|
||||||
let mk_local_equation i k m lm =
|
let mk_local_equation i k m lm =
|
||||||
(* m_i = false; m_j = l_mj *)
|
(* m_i = false; m_j = l_mj *)
|
||||||
|
@ -113,7 +96,7 @@ let mk_global_equation res m lm =
|
||||||
l_mn = if res then true else true fby mn ] *)
|
l_mn = if res then true else true fby mn ] *)
|
||||||
let e =
|
let e =
|
||||||
(match res with
|
(match res with
|
||||||
| Rfalse -> pre_true (mk_bool_var m)
|
| None -> pre_true (mk_bool_var m)
|
||||||
| _ -> mk_exp (ifres res dtrue (pre_true (mk_bool_var m)))
|
| _ -> mk_exp (ifres res dtrue (pre_true (mk_bool_var m)))
|
||||||
(Tid Initial.pbool)
|
(Tid Initial.pbool)
|
||||||
) in
|
) in
|
||||||
|
@ -127,7 +110,7 @@ let edesc funs (res, v, acc_eq_list) ed =
|
||||||
let ed = match ed with
|
let ed = match ed with
|
||||||
| Efby (e1, e2) ->
|
| Efby (e1, e2) ->
|
||||||
(match res, e1 with
|
(match res, e1 with
|
||||||
| Rfalse, { e_desc = Econst c } ->
|
| None, { e_desc = Econst c } ->
|
||||||
(* no reset *)
|
(* no reset *)
|
||||||
Epre(Some c, e2)
|
Epre(Some c, e2)
|
||||||
| _ ->
|
| _ ->
|
||||||
|
@ -138,23 +121,11 @@ let edesc funs (res, v, acc_eq_list) ed =
|
||||||
ifres res e1 e2
|
ifres res e1 e2
|
||||||
|
|
||||||
(* add reset to the current reset exp. *)
|
(* add reset to the current reset exp. *)
|
||||||
| Eapp({ a_op = Enode _ } as op, e_list, Some re) ->
|
| Eapp({ a_op = Enode _ } as op, e_list, re) ->
|
||||||
Eapp(op, e_list, Some (or_op res re))
|
Eapp(op, e_list, add_resets res re)
|
||||||
(* create a new reset exp if necessary *)
|
|
||||||
| Eapp({ a_op = Enode _ } as op, e_list, None) ->
|
|
||||||
if true_reset res then
|
|
||||||
Eapp(op, e_list, Some (exp_of_res res))
|
|
||||||
else
|
|
||||||
Eapp(op, e_list, None)
|
|
||||||
(* add reset to the current reset exp. *)
|
(* add reset to the current reset exp. *)
|
||||||
| Eiterator(it, ({ a_op = Enode _ } as op), n, e_list, Some re) ->
|
| Eiterator(it, ({ a_op = Enode _ } as op), n, e_list, re) ->
|
||||||
Eiterator(it, op, n, e_list, Some (or_op res re))
|
Eiterator(it, op, n, e_list, add_resets res re)
|
||||||
(* create a new reset exp if necessary *)
|
|
||||||
| Eiterator(it, ({ a_op = Enode _ } as op), n, e_list, None) ->
|
|
||||||
if true_reset res then
|
|
||||||
Eiterator(it, op, n, e_list, Some (exp_of_res res))
|
|
||||||
else
|
|
||||||
Eiterator(it, op, n, e_list, None)
|
|
||||||
| _ -> ed
|
| _ -> ed
|
||||||
in
|
in
|
||||||
ed, (res, v, acc_eq_list)
|
ed, (res, v, acc_eq_list)
|
||||||
|
@ -168,7 +139,7 @@ let switch_handlers funs (res, v, acc_eq_list) switch_handlers =
|
||||||
let defnames = List.fold_left (fun acc m ->
|
let defnames = List.fold_left (fun acc m ->
|
||||||
Env.add m (Tid Initial.pbool) acc) b.b_defnames m_list in
|
Env.add m (Tid Initial.pbool) acc) b.b_defnames m_list in
|
||||||
let _, (_, v, acc_eq_list) =
|
let _, (_, v, acc_eq_list) =
|
||||||
mapfold (eq_it funs) (rvar lm, b.b_local, []) b.b_equs in
|
mapfold (eq_it funs) (Some (mk_bool_var lm), b.b_local, []) b.b_equs in
|
||||||
let added_eqs = mapi2 (mk_local_equation i) m_list lm_list in
|
let added_eqs = mapi2 (mk_local_equation i) m_list lm_list in
|
||||||
{ sh with w_block = { b with b_local = v; b_defnames = defnames;
|
{ sh with w_block = { b with b_local = v; b_defnames = defnames;
|
||||||
b_equs = added_eqs @ acc_eq_list } } in
|
b_equs = added_eqs @ acc_eq_list } } in
|
||||||
|
@ -190,12 +161,12 @@ let eq funs (res, v, acc_eq_list) equ =
|
||||||
|
|
||||||
| Ereset(eq_list, e) ->
|
| Ereset(eq_list, e) ->
|
||||||
let e, _ = exp_it funs (res, v, acc_eq_list) e in
|
let e, _ = exp_it funs (res, v, acc_eq_list) e in
|
||||||
let v, acc_eq_list, res =
|
let res, v, acc_eq_list =
|
||||||
if statefull eq_list then
|
(* if statefull eq_list then*)
|
||||||
orthen v acc_eq_list res e
|
orthen v acc_eq_list res e
|
||||||
else
|
(* else
|
||||||
let _, v, acc_eq_list = equation v acc_eq_list e in
|
let _, v, acc_eq_list = equation v acc_eq_list e in
|
||||||
v, acc_eq_list, res
|
res, v, acc_eq_list*)
|
||||||
in
|
in
|
||||||
let _, (res, v, acc_eq_list) =
|
let _, (res, v, acc_eq_list) =
|
||||||
mapfold (eq_it funs) (res, v, acc_eq_list) eq_list in
|
mapfold (eq_it funs) (res, v, acc_eq_list) eq_list in
|
||||||
|
@ -207,12 +178,11 @@ let eq funs (res, v, acc_eq_list) equ =
|
||||||
|
|
||||||
|
|
||||||
let node funs _ n =
|
let node funs _ n =
|
||||||
let n, (_, v, eq_list) = Hept_mapfold.node_dec funs (rfalse, [], []) n in
|
let n, (_, v, eq_list) = Hept_mapfold.node_dec funs (None, [], []) n in
|
||||||
{ n with n_local = v @ n.n_local; n_equs = eq_list; }, (rfalse, [], [])
|
{ n with n_local = v @ n.n_local; n_equs = eq_list; }, (None, [], [])
|
||||||
|
|
||||||
let program p =
|
let program p =
|
||||||
let funs = { Hept_mapfold.hept_funs_default with
|
let funs = { Hept_mapfold.hept_funs_default with
|
||||||
eq = eq; node_dec = node; edesc = edesc } in
|
eq = eq; node_dec = node; edesc = edesc } in
|
||||||
let p, _ = program_it funs (rfalse, [], []) p in
|
let p, _ = program_it funs (None, [], []) p in
|
||||||
p
|
p
|
||||||
|
|
||||||
|
|
Loading…
Reference in a new issue