Remove old version of files
This commit is contained in:
Cédric Pasteur
parent
db64b6302b
commit
a81dd0b2b4
7 changed files with 0 additions and 929 deletions
|
|
@ -1,219 +0,0 @@
|
|||
(**************************************************************************)
|
||||
(* *)
|
||||
(* Heptagon *)
|
||||
(* *)
|
||||
(* Author : Marc Pouzet *)
|
||||
(* Organization : Demons, LRI, University of Paris-Sud, Orsay *)
|
||||
(* *)
|
||||
(**************************************************************************)
|
||||
(* removing automata statements *)
|
||||
|
||||
(* $Id$ *)
|
||||
|
||||
open Misc
|
||||
open Names
|
||||
open Idents
|
||||
open Heptagon
|
||||
open Types
|
||||
|
||||
let mk_var_exp n ty =
|
||||
mk_exp (Evar n) ty
|
||||
|
||||
let mk_pair e1 e2 =
|
||||
mk_exp (mk_op_app Etuple [e1;e2]) (Tprod [e1.e_ty; e2.e_ty])
|
||||
|
||||
let mk_reset_equation eq_list e =
|
||||
mk_equation (Ereset (eq_list, e))
|
||||
|
||||
let mk_switch_equation e l =
|
||||
mk_equation (Eswitch (e, l))
|
||||
|
||||
let mk_exp_fby_false e =
|
||||
mk_exp (Epre (Some (mk_static_exp (Sconstructor Initial.pfalse)), e))
|
||||
(Tid Initial.pbool)
|
||||
|
||||
let mk_exp_fby_state initial e =
|
||||
{ e with e_desc = Epre (Some (mk_static_exp (Sconstructor initial)), e) }
|
||||
|
||||
(* the list of enumerated types introduced to represent states *)
|
||||
let state_type_dec_list = ref []
|
||||
|
||||
let intro_type states =
|
||||
let list env = NamesEnv.fold (fun _ state l -> state :: l) env [] in
|
||||
let n = gen_symbol () in
|
||||
let state_type = "st" ^ n in
|
||||
state_type_dec_list :=
|
||||
(mk_type_dec state_type (Type_enum (list states))) :: !state_type_dec_list;
|
||||
Name(state_type)
|
||||
|
||||
(* an automaton may be a Moore automaton, i.e., with only weak transitions; *)
|
||||
(* a Mealy one, i.e., with only strong transition or mixed *)
|
||||
let moore_mealy state_handlers =
|
||||
let handler (moore, mealy) { s_until = l1; s_unless = l2 } =
|
||||
(moore or (l1 <> []), mealy or (l2 <> [])) in
|
||||
List.fold_left handler (false, false) state_handlers
|
||||
|
||||
let rec translate_eq (v, eq_list) eq =
|
||||
match eq.eq_desc with
|
||||
Eautomaton(state_handlers) ->
|
||||
translate_automaton v eq_list state_handlers
|
||||
| Eswitch(e, switch_handlers) ->
|
||||
let eq = { eq with eq_desc =
|
||||
Eswitch(e, translate_switch_handlers switch_handlers) } in
|
||||
v, eq::eq_list
|
||||
| Epresent(present_handlers, block) ->
|
||||
let eq = { eq with eq_desc =
|
||||
Epresent(translate_present_handlers present_handlers,
|
||||
translate_block block) } in
|
||||
v, eq::eq_list
|
||||
| Ereset(r_eq_list, e) ->
|
||||
let v, r_eq_list = translate_eqs v r_eq_list in
|
||||
let eq = { eq with eq_desc = Ereset(r_eq_list, e) } in
|
||||
v, eq::eq_list
|
||||
| Eeq _ -> v, eq :: eq_list
|
||||
|
||||
and translate_eqs v eq_list = List.fold_left translate_eq (v, []) eq_list
|
||||
|
||||
and translate_block ({ b_local = v; b_equs = eq_list } as b) =
|
||||
let v, eq_list = translate_eqs v eq_list in
|
||||
{ b with b_local = v; b_equs = eq_list }
|
||||
|
||||
and translate_switch_handlers handlers =
|
||||
let translate_switch_handler { w_name = n; w_block = b } =
|
||||
{ w_name = n; w_block = translate_block b } in
|
||||
List.map translate_switch_handler handlers
|
||||
|
||||
and translate_present_handlers handlers =
|
||||
let translate_present_handler { p_cond = e; p_block = b } =
|
||||
{ p_cond = e; p_block = translate_block b } in
|
||||
List.map translate_present_handler handlers
|
||||
|
||||
and translate_automaton v eq_list handlers =
|
||||
let has_until, has_unless = moore_mealy handlers in
|
||||
let states =
|
||||
let suffix = gen_symbol () in
|
||||
List.fold_left
|
||||
(fun env { s_state = n } -> NamesEnv.add n (n ^ suffix) env)
|
||||
NamesEnv.empty handlers in
|
||||
|
||||
let statetype = intro_type states in
|
||||
let tstatetype = Tid statetype in
|
||||
let initial = Name(NamesEnv.find (List.hd handlers).s_state states) in
|
||||
|
||||
let statename = Idents.fresh "s" in
|
||||
let next_statename = Idents.fresh "ns" in
|
||||
let resetname = Idents.fresh "r" in
|
||||
let next_resetname = Idents.fresh "nr" in
|
||||
let pre_next_resetname = Idents.fresh "pnr" in
|
||||
|
||||
let name n = Name(NamesEnv.find n states) in
|
||||
let state n = mk_exp (Econst (mk_static_exp
|
||||
(Sconstructor (name n)))) tstatetype in
|
||||
let statevar n = mk_var_exp n tstatetype in
|
||||
let boolvar n = mk_var_exp n (Tid Initial.pbool) in
|
||||
|
||||
let escapes n s rcont =
|
||||
let escape { e_cond = e; e_reset = r; e_next_state = n } cont =
|
||||
mk_ifthenelse e (mk_pair (state n) (if r then dtrue else dfalse)) cont
|
||||
in
|
||||
List.fold_right escape s (mk_pair (state n) rcont)
|
||||
in
|
||||
|
||||
let strong { s_state = n; s_unless = su } =
|
||||
let defnames = Env.add resetname (Tid Initial.pbool) Env.empty in
|
||||
let defnames = Env.add statename tstatetype defnames in
|
||||
let st_eq = mk_simple_equation
|
||||
(Etuplepat[Evarpat(statename); Evarpat(resetname)])
|
||||
(escapes n su (boolvar pre_next_resetname)) in
|
||||
mk_block defnames [mk_reset_equation [st_eq]
|
||||
(boolvar pre_next_resetname)]
|
||||
in
|
||||
|
||||
let weak { s_state = n; s_block = b; s_until = su } =
|
||||
let b = translate_block b in
|
||||
let defnames = Env.add next_resetname (Tid Initial.pbool) b.b_defnames in
|
||||
let defnames = Env.add next_statename tstatetype defnames in
|
||||
let ns_eq = mk_simple_equation
|
||||
(Etuplepat[Evarpat(next_statename); Evarpat(next_resetname)])
|
||||
(escapes n su dfalse) in
|
||||
{ b with b_equs =
|
||||
[mk_reset_equation (ns_eq::b.b_equs) (boolvar resetname)];
|
||||
(* (or_op (boolvar pre_next_resetname) (boolvar resetname))]; *)
|
||||
b_defnames = defnames;
|
||||
}
|
||||
in
|
||||
|
||||
let v =
|
||||
(mk_var_dec next_statename (Tid(statetype))) ::
|
||||
(mk_var_dec resetname (Tid Initial.pbool)) ::
|
||||
(mk_var_dec next_resetname (Tid Initial.pbool)) ::
|
||||
(mk_var_dec pre_next_resetname (Tid Initial.pbool)) :: v in
|
||||
(* we optimise the case of an only strong automaton *)
|
||||
(* or only weak automaton *)
|
||||
match has_until, has_unless with
|
||||
| true, false ->
|
||||
let switch_e = mk_exp_fby_state initial (statevar next_statename) in
|
||||
let switch_handlers = (List.map
|
||||
(fun ({ s_state = n } as case) ->
|
||||
{ w_name = name n; w_block = weak case })
|
||||
handlers) in
|
||||
let switch_eq = mk_switch_equation switch_e switch_handlers in
|
||||
let nr_eq = mk_simple_equation (Evarpat pre_next_resetname)
|
||||
(mk_exp_fby_false (boolvar (next_resetname))) in
|
||||
let pnr_eq = mk_simple_equation (Evarpat resetname)
|
||||
(boolvar pre_next_resetname) in
|
||||
(* a Moore automaton with only weak transitions *)
|
||||
v, switch_eq :: nr_eq :: pnr_eq :: eq_list
|
||||
| _ ->
|
||||
(* the general case; two switch to generate,
|
||||
statename variable used and defined *)
|
||||
let v = (mk_var_dec statename (Tid statetype)) :: v in
|
||||
|
||||
let ns_switch_e = mk_exp_fby_state initial (statevar next_statename) in
|
||||
let ns_switch_handlers = List.map
|
||||
(fun ({ s_state = n } as case) ->
|
||||
{ w_name = name n; w_block = strong case })
|
||||
handlers in
|
||||
let ns_switch_eq = mk_switch_equation ns_switch_e ns_switch_handlers in
|
||||
|
||||
let switch_e = statevar statename in
|
||||
let switch_handlers = List.map
|
||||
(fun ({ s_state = n } as case) ->
|
||||
{ w_name = name n; w_block = weak case })
|
||||
handlers in
|
||||
let switch_eq = mk_switch_equation switch_e switch_handlers in
|
||||
|
||||
let pnr_eq = mk_simple_equation (Evarpat pre_next_resetname)
|
||||
(mk_exp_fby_false (boolvar (next_resetname))) in
|
||||
v, ns_switch_eq :: switch_eq :: pnr_eq :: eq_list
|
||||
|
||||
let translate_contract ({ c_local = v; c_eq = eq_list} as c) =
|
||||
let v, eq_list = translate_eqs v eq_list in
|
||||
{ c with c_local = v; c_eq = eq_list }
|
||||
|
||||
let node ({ n_local = v; n_equs = eq_list; n_contract = contract } as n) =
|
||||
let v, eq_list = translate_eqs v eq_list in
|
||||
let contract = optional translate_contract contract in
|
||||
{ n with n_local = v; n_equs = eq_list; n_contract = contract }
|
||||
|
||||
let program ({ p_types = pt_list; p_nodes = n_list } as p) =
|
||||
let n_list = List.map node n_list in
|
||||
{ p with p_types = !state_type_dec_list @ pt_list;
|
||||
p_nodes = n_list }
|
||||
|
||||
(*
|
||||
A -> do ... unless c1 then A1 ... until c'1 then A'1 ...
|
||||
|
||||
match A fby next_state with
|
||||
A -> resA = pre_next_res or (if c1 then ... else ..
|
||||
|
||||
match state with
|
||||
A -> reset
|
||||
next_res = if c'1 then true else ... else false
|
||||
every resA
|
||||
|
||||
if faut donc: - une memoire pour pre(next_res) + n memoires (pre(resA),...)
|
||||
|
||||
merge state
|
||||
(A -> reset ... when A(state) every pre_next_res or res)
|
||||
*)
|
||||
|
|
@ -1,80 +0,0 @@
|
|||
(**************************************************************************)
|
||||
(* *)
|
||||
(* Heptagon *)
|
||||
(* *)
|
||||
(* Author : Marc Pouzet *)
|
||||
(* Organization : Demons, LRI, University of Paris-Sud, Orsay *)
|
||||
(* *)
|
||||
(**************************************************************************)
|
||||
(* complete partial definitions with [x = last(x)] *)
|
||||
|
||||
open Misc
|
||||
open Heptagon
|
||||
open Idents
|
||||
|
||||
(* adds an equation [x = last(x)] for every partially defined variable *)
|
||||
(* in a control structure *)
|
||||
let complete_with_last defined_names local_defined_names eq_list =
|
||||
let last n ty = mk_exp (Elast n) ty in
|
||||
let equation n ty eq_list =
|
||||
(mk_equation (Eeq(Evarpat n, last n ty)))::eq_list
|
||||
in
|
||||
let d = Env.diff defined_names local_defined_names in
|
||||
Env.fold equation d eq_list
|
||||
|
||||
let rec translate_eq eq =
|
||||
match eq.eq_desc with
|
||||
| Ereset(eq_list, e) ->
|
||||
{ eq with eq_desc = Ereset(translate_eqs eq_list, e) }
|
||||
| Eeq(pat, e) ->
|
||||
{ eq with eq_desc = Eeq(pat, e) }
|
||||
| Eswitch(e, switch_handlers) ->
|
||||
let defnames =
|
||||
List.fold_left
|
||||
(fun acc { w_block = { b_defnames = d } } -> Env.union acc d)
|
||||
Env.empty switch_handlers in
|
||||
let switch_handlers =
|
||||
List.map (fun ({ w_block = b } as handler) ->
|
||||
{ handler with w_block = translate_block defnames b })
|
||||
switch_handlers in
|
||||
{ eq with eq_desc = Eswitch(e, switch_handlers) }
|
||||
| Epresent(present_handlers, b) ->
|
||||
let defnames =
|
||||
List.fold_left
|
||||
(fun acc { p_block = { b_defnames = d } } -> Env.union acc d)
|
||||
b.b_defnames present_handlers in
|
||||
let present_handlers =
|
||||
List.map (fun ({ p_block = b } as handler) ->
|
||||
{ handler with p_block = translate_block defnames b })
|
||||
present_handlers in
|
||||
let b = translate_block defnames b in
|
||||
{eq with eq_desc = Epresent(present_handlers, b)}
|
||||
| Eautomaton(state_handlers) ->
|
||||
let defnames =
|
||||
List.fold_left
|
||||
(fun acc { s_block = { b_defnames = d } } -> Env.union acc d)
|
||||
Env.empty state_handlers in
|
||||
let state_handlers =
|
||||
List.map (fun ({ s_block = b } as handler) ->
|
||||
{ handler with s_block = translate_block defnames b })
|
||||
state_handlers in
|
||||
{ eq with eq_desc = Eautomaton(state_handlers) }
|
||||
|
||||
and translate_eqs eq_list = List.map translate_eq eq_list
|
||||
|
||||
and translate_block defnames
|
||||
({ b_defnames = bdefnames; b_equs = eq_list } as b) =
|
||||
let eq_list = translate_eqs eq_list in
|
||||
let eq_list = complete_with_last defnames bdefnames eq_list in
|
||||
{ b with b_equs = eq_list; b_defnames = defnames }
|
||||
|
||||
let translate_contract ({ c_eq = eqs } as c) =
|
||||
{ c with c_eq = translate_eqs eqs }
|
||||
|
||||
let node ({ n_equs = eq_list; n_contract = contract } as n) =
|
||||
{ n with
|
||||
n_equs = translate_eqs eq_list;
|
||||
n_contract = optional translate_contract contract }
|
||||
|
||||
let program ({ p_types = pt_list; p_nodes = n_list } as p) =
|
||||
{ p with p_types = pt_list; p_nodes = List.map node n_list }
|
||||
|
|
@ -1,58 +0,0 @@
|
|||
(**************************************************************************)
|
||||
(* *)
|
||||
(* Heptagon *)
|
||||
(* *)
|
||||
(* Author : Marc Pouzet *)
|
||||
(* Organization : Demons, LRI, University of Paris-Sud, Orsay *)
|
||||
(* *)
|
||||
(**************************************************************************)
|
||||
(* complete partial definitions with [x = last(x)] *)
|
||||
|
||||
open Misc
|
||||
open Heptagon
|
||||
open Global_mapfold
|
||||
open Hept_mapfold
|
||||
open Idents
|
||||
|
||||
(* adds an equation [x = last(x)] for every partially defined variable *)
|
||||
(* in a control structure *)
|
||||
let complete_with_last defined_names local_defined_names eq_list =
|
||||
let last n ty = mk_exp (Elast n) ty in
|
||||
let equation n ty eq_list =
|
||||
(mk_equation (Eeq(Evarpat n, last n ty)))::eq_list
|
||||
in
|
||||
let d = Env.diff defined_names local_defined_names in
|
||||
Env.fold equation d eq_list
|
||||
|
||||
let block funs (defnames,collect) b =
|
||||
if collect then
|
||||
b, (b.b_defnames, collect)
|
||||
else
|
||||
let b, _ = Hept_mapfold.block funs (Env.empty, false) b in
|
||||
let added_eq = complete_with_last defnames b.b_defnames [] in
|
||||
{ b with b_equs = b.b_equs @ added_eq; b_defnames = defnames },
|
||||
(Env.empty, false)
|
||||
|
||||
let eqdesc funs _ ed =
|
||||
match ed with
|
||||
| Epresent _ | Eautomaton _ | Eswitch _ ->
|
||||
(* collect defined names *)
|
||||
let ed, (defnames, _) = Hept_mapfold.eqdesc funs (Env.empty, true) ed in
|
||||
(* add missing defnames *)
|
||||
Hept_mapfold.eqdesc funs (defnames, false) ed
|
||||
|
||||
| _ -> raise Misc.Fallback
|
||||
|
||||
let gather (acc, collect) (local_acc, collect) =
|
||||
Env.union local_acc acc, collect
|
||||
|
||||
let program p =
|
||||
let funs =
|
||||
{ Hept_mapfold.defaults
|
||||
with eqdesc = eqdesc; block = block;
|
||||
switch_handler = it_gather gather Hept_mapfold.switch_handler;
|
||||
present_handler = it_gather gather Hept_mapfold.present_handler;
|
||||
state_handler = it_gather gather Hept_mapfold.state_handler; } in
|
||||
let p, _ = program_it funs (Env.empty, false) p in
|
||||
p
|
||||
|
||||
|
|
@ -1,131 +0,0 @@
|
|||
(**************************************************************************)
|
||||
(* *)
|
||||
(* Heptagon *)
|
||||
(* *)
|
||||
(* Author : Marc Pouzet *)
|
||||
(* Organization : Demons, LRI, University of Paris-Sud, Orsay *)
|
||||
(* *)
|
||||
(**************************************************************************)
|
||||
|
||||
(* removing complex reset expressions :
|
||||
equations
|
||||
x = (f every e) e'
|
||||
-->
|
||||
r = e;
|
||||
x = (f every r) e'
|
||||
*)
|
||||
|
||||
open Misc
|
||||
open Idents
|
||||
open Heptagon
|
||||
open Reset
|
||||
|
||||
(*
|
||||
let defnames m n d =
|
||||
let rec loop acc k = if k < n then loop (S.add m.(k) acc) (k+1) else acc in
|
||||
loop d 0
|
||||
*)
|
||||
|
||||
let statefull eq_list = List.exists (fun eq -> eq.eq_statefull) eq_list
|
||||
|
||||
let is_var = function
|
||||
| { e_desc = Evar _ } -> true
|
||||
| _ -> false
|
||||
|
||||
let rec translate_eq v acc_eq_list eq =
|
||||
match eq.eq_desc with
|
||||
| Eeq(pat, e) ->
|
||||
let v,acc_eq_list,e = translate v acc_eq_list e in
|
||||
v, { eq with eq_desc = Eeq(pat, e) } :: acc_eq_list
|
||||
| Eswitch(e, tag_block_list) ->
|
||||
let v,acc_eq_list,e = translate v acc_eq_list e in
|
||||
let tag_block_list, acc_eq_list =
|
||||
translate_switch acc_eq_list tag_block_list in
|
||||
v, { eq with eq_desc = Eswitch(e, tag_block_list) } :: acc_eq_list
|
||||
| Ereset _ | Epresent _ | Eautomaton _ -> assert false
|
||||
|
||||
and translate_eqs v acc_eq_list eq_list =
|
||||
List.fold_left
|
||||
(fun (v,acc_eq_list) eq ->
|
||||
translate_eq v acc_eq_list eq) (v,acc_eq_list) eq_list
|
||||
|
||||
and translate_switch acc_eq_list switch_handlers =
|
||||
|
||||
let body {w_name = c;
|
||||
w_block = ({ b_local = lv; b_defnames = d; b_equs = eqs } as b)} =
|
||||
let lv,eqs = translate_eqs lv [] eqs in
|
||||
{ w_name = c;
|
||||
w_block = { b with b_local = lv; b_defnames = d; b_equs = eqs } } in
|
||||
|
||||
let rec loop switch_handlers =
|
||||
match switch_handlers with
|
||||
[] -> []
|
||||
| handler :: switch_handlers ->
|
||||
(body handler) :: (loop switch_handlers) in
|
||||
|
||||
loop switch_handlers, acc_eq_list
|
||||
|
||||
and translate v acc_eq_list e =
|
||||
match e.e_desc with
|
||||
Econst _ | Evar _ | Elast _ | Efby _ | Epre _ -> v,acc_eq_list,e
|
||||
| Eapp (op, e_list, Some re) when not (is_var re) ->
|
||||
let v, acc_eq_list,re = translate v acc_eq_list re in
|
||||
let n, v, acc_eq_list = equation v acc_eq_list re in
|
||||
let v, acc_eq_list, e_list = translate_list v acc_eq_list e_list in
|
||||
let re = { re with e_desc = Evar(n) } in
|
||||
v,acc_eq_list,
|
||||
{ e with e_desc = Eapp (op, e_list, Some re) }
|
||||
| Eiterator(it, op, n, e_list, Some re) when not (is_var re) ->
|
||||
let v, acc_eq_list,re = translate v acc_eq_list re in
|
||||
let x, v, acc_eq_list = equation v acc_eq_list re in
|
||||
let v, acc_eq_list, e_list = translate_list v acc_eq_list e_list in
|
||||
let re = { re with e_desc = Evar x } in
|
||||
v,acc_eq_list,
|
||||
{ e with e_desc = Eiterator(it, op, n, e_list, Some re) }
|
||||
| Eapp(op, e_list, r) ->
|
||||
let v, acc_eq_list, e_list = translate_list v acc_eq_list e_list in
|
||||
v, acc_eq_list,
|
||||
{ e with e_desc = Eapp(op, e_list, r) }
|
||||
| Eiterator(it, op, n, e_list, r) ->
|
||||
let v, acc_eq_list, e_list = translate_list v acc_eq_list e_list in
|
||||
v, acc_eq_list,
|
||||
{ e with e_desc = Eiterator(it, op, n, e_list, r) }
|
||||
| Estruct(e_f_list) ->
|
||||
let v,acc_eq_list,e_f_list =
|
||||
List.fold_left
|
||||
(fun (v,acc_eq_list,acc_e_f) (f,e) ->
|
||||
let v,acc_eq_list,e = translate v acc_eq_list e in
|
||||
(v,acc_eq_list,(f,e)::acc_e_f))
|
||||
(v,acc_eq_list,[]) e_f_list in
|
||||
v,acc_eq_list,
|
||||
{ e with e_desc = Estruct(List.rev e_f_list) }
|
||||
|
||||
and translate_list v acc_eq_list e_list =
|
||||
let v,acc_eq_list,acc_e =
|
||||
List.fold_left
|
||||
(fun (v,acc_eq_list,acc_e) e ->
|
||||
let v,acc_eq_list,e = translate v acc_eq_list e in
|
||||
(v,acc_eq_list,e::acc_e))
|
||||
(v,acc_eq_list,[]) e_list in
|
||||
v,acc_eq_list,List.rev acc_e
|
||||
|
||||
let translate_contract ({ c_local = v;
|
||||
c_eq = eq_list;
|
||||
c_assume = e_a;
|
||||
c_enforce = e_g } as c) =
|
||||
let v,acc_eq,e_a = translate v [] e_a in
|
||||
let v,acc_eq,e_g = translate v acc_eq e_g in
|
||||
let v, eq_list = translate_eqs v acc_eq eq_list in
|
||||
{ c with
|
||||
c_local = v;
|
||||
c_eq = eq_list;
|
||||
c_assume = e_a;
|
||||
c_enforce = e_g }
|
||||
|
||||
let node ({ n_local = v; n_equs = eq_list; n_contract = contract } as n) =
|
||||
let contract = optional translate_contract contract in
|
||||
let v, eq_list = translate_eqs v [] eq_list in
|
||||
{ n with n_local = v; n_equs = eq_list; n_contract = contract }
|
||||
|
||||
let program ({ p_types = pt_list; p_nodes = n_list } as p) =
|
||||
{ p with p_types = pt_list; p_nodes = List.map node n_list }
|
||||
|
|
@ -1,102 +0,0 @@
|
|||
(**************************************************************************)
|
||||
(* *)
|
||||
(* Heptagon *)
|
||||
(* *)
|
||||
(* Author : Marc Pouzet *)
|
||||
(* Organization : Demons, LRI, University of Paris-Sud, Orsay *)
|
||||
(* *)
|
||||
(**************************************************************************)
|
||||
(* removing accessed to shared variables (last x) *)
|
||||
|
||||
open Misc
|
||||
open Heptagon
|
||||
open Idents
|
||||
|
||||
(* introduce a fresh equation [last_x = pre(x)] for every *)
|
||||
(* variable declared with a last *)
|
||||
let last (eq_list, env, v) { v_ident = n; v_type = t; v_last = last } =
|
||||
match last with
|
||||
| Var -> (eq_list, env, v)
|
||||
| Last(default) ->
|
||||
let lastn = Idents.fresh ("last" ^ (sourcename n)) in
|
||||
let eq = mk_equation (Eeq (Evarpat lastn,
|
||||
mk_exp (Epre (default,
|
||||
mk_exp (Evar n) t)) t)) in
|
||||
eq:: eq_list,
|
||||
Env.add n lastn env,
|
||||
(mk_var_dec lastn t) :: v
|
||||
|
||||
let extend_env env v = List.fold_left last ([], env, []) v
|
||||
|
||||
let rec translate_eq env eq =
|
||||
match eq.eq_desc with
|
||||
| Ereset(eq_list, e) ->
|
||||
{ eq with eq_desc = Ereset(translate_eqs env eq_list, translate env e) }
|
||||
| Eeq(pat, e) ->
|
||||
{ eq with eq_desc = Eeq(pat, translate env e) }
|
||||
| Eswitch(e, handler_list) ->
|
||||
let handler_list =
|
||||
List.map (fun ({ w_block = b } as handler) ->
|
||||
{ handler with w_block = translate_block env b })
|
||||
handler_list in
|
||||
{ eq with eq_desc = Eswitch(translate env e, handler_list) }
|
||||
| Epresent _ | Eautomaton _ -> assert false
|
||||
|
||||
and translate_eqs env eq_list = List.map (translate_eq env) eq_list
|
||||
|
||||
and translate_block env ({ b_local = v; b_equs = eq_list } as b) =
|
||||
let eq_lastn_n_list, env, last_v = extend_env env v in
|
||||
let eq_list = translate_eqs env eq_list in
|
||||
{ b with b_local = v @ last_v; b_equs = eq_lastn_n_list @ eq_list }
|
||||
|
||||
and translate env e =
|
||||
match e.e_desc with
|
||||
| Econst _ | Evar _ -> e
|
||||
| Elast(x) ->
|
||||
let lx = Env.find x env in { e with e_desc = Evar(lx) }
|
||||
| Epre(c, e) ->
|
||||
{ e with e_desc = Epre(c, translate env e) }
|
||||
| Efby (e1, e2) ->
|
||||
{ e with e_desc = Efby(translate env e1, translate env e2) }
|
||||
| Eapp(op, e_list, r) ->
|
||||
{ e with e_desc = Eapp(op, List.map (translate env) e_list, r) }
|
||||
| Estruct(e_f_list) ->
|
||||
{ e with e_desc =
|
||||
Estruct(List.map (fun (f, e) -> (f, translate env e)) e_f_list) }
|
||||
| Eiterator(it, app, n, e_list, r) ->
|
||||
{ e with e_desc = Eiterator(it, app, n,
|
||||
List.map (translate env) e_list, r) }
|
||||
|
||||
let translate_contract env contract =
|
||||
match contract with
|
||||
| None -> None, env
|
||||
| Some { c_local = v;
|
||||
c_eq = eq_list;
|
||||
c_assume = e_a;
|
||||
c_enforce = e_g } ->
|
||||
let eq_lastn_n_list, env', last_v = extend_env env v in
|
||||
let eq_list = translate_eqs env' eq_list in
|
||||
let e_a = translate env' e_a in
|
||||
let e_g = translate env' e_g in
|
||||
Some { c_local = v @ last_v;
|
||||
c_eq = eq_lastn_n_list @ eq_list;
|
||||
c_assume = e_a;
|
||||
c_enforce = e_g },
|
||||
env
|
||||
|
||||
let node ({ n_input = i; n_local = v; n_output = o;
|
||||
n_equs = eq_list; n_contract = contract } as n) =
|
||||
let _, env, _ = extend_env Env.empty i in
|
||||
let eq_lasto_list, env, last_o = extend_env env o in
|
||||
let contract, env = translate_contract env contract in
|
||||
let eq_lastn_n_list, env, last_v = extend_env env v in
|
||||
let eq_list = translate_eqs env eq_list in
|
||||
{ n with
|
||||
n_input = i;
|
||||
n_output = o;
|
||||
n_local = v @ last_o @ last_v;
|
||||
n_contract = contract;
|
||||
n_equs = eq_lasto_list @ eq_lastn_n_list @ eq_list }
|
||||
|
||||
let program ({ p_types = pt_list; p_nodes = n_list } as p) =
|
||||
{ p with p_types = pt_list; p_nodes = List.map node n_list }
|
||||
|
|
@ -1,68 +0,0 @@
|
|||
(**************************************************************************)
|
||||
(* *)
|
||||
(* Heptagon *)
|
||||
(* *)
|
||||
(* Author : Marc Pouzet *)
|
||||
(* Organization : Demons, LRI, University of Paris-Sud, Orsay *)
|
||||
(* *)
|
||||
(**************************************************************************)
|
||||
(* removing present statements *)
|
||||
|
||||
(* $Id$ *)
|
||||
|
||||
open Misc
|
||||
open Location
|
||||
open Heptagon
|
||||
open Initial
|
||||
|
||||
let rec translate_eq v eq =
|
||||
match eq.eq_desc with
|
||||
| Eswitch(e, switch_handlers) ->
|
||||
v, { eq with eq_desc =
|
||||
Eswitch(e, translate_switch_handlers switch_handlers) }
|
||||
| Epresent(present_handlers, block) ->
|
||||
v,
|
||||
translate_present_handlers present_handlers (translate_block block)
|
||||
| Ereset(eq_list, e) ->
|
||||
let v, eq_list = translate_eqs v eq_list in
|
||||
v, { eq with eq_desc = Ereset(eq_list, e) }
|
||||
| Eeq _ -> v, eq
|
||||
| Eautomaton _ -> assert false
|
||||
|
||||
and translate_eqs v eq_list =
|
||||
List.fold_left
|
||||
(fun (v, eq_list) eq ->
|
||||
let v, eq = translate_eq v eq in v, eq :: eq_list)
|
||||
(v, []) eq_list
|
||||
|
||||
and translate_block ({ b_local = v; b_equs = eq_list } as b) =
|
||||
let v, eq_list = translate_eqs v eq_list in
|
||||
{ b with b_local = v; b_equs = eq_list }
|
||||
|
||||
and translate_switch_handlers handlers =
|
||||
let translate_switch_handler { w_name = n; w_block = b } =
|
||||
{ w_name = n; w_block = translate_block b } in
|
||||
List.map translate_switch_handler handlers
|
||||
|
||||
and translate_present_handlers handlers cont =
|
||||
let translate_present_handler { p_cond = e; p_block = b } cont =
|
||||
let statefull = b.b_statefull or cont.b_statefull in
|
||||
mk_block ~statefull:statefull b.b_defnames
|
||||
[mk_switch_equation
|
||||
~statefull:statefull e
|
||||
[{ w_name = ptrue; w_block = b };
|
||||
{ w_name = pfalse; w_block = cont }]] in
|
||||
let b = List.fold_right translate_present_handler handlers cont in
|
||||
List.hd (b.b_equs)
|
||||
|
||||
let translate_contract ({ c_local = v; c_eq = eq_list} as c) =
|
||||
let v, eq_list = translate_eqs v eq_list in
|
||||
{ c with c_local = v; c_eq = eq_list }
|
||||
|
||||
let node ({ n_local = v; n_equs = eq_list; n_contract = contract } as n) =
|
||||
let v, eq_list = translate_eqs v eq_list in
|
||||
let contract = optional translate_contract contract in
|
||||
{ n with n_local = v; n_equs = eq_list; n_contract = contract }
|
||||
|
||||
let program ({ p_types = pt_list; p_nodes = n_list } as p) =
|
||||
{ p with p_types = pt_list; p_nodes = List.map node n_list }
|
||||
|
|
@ -1,271 +0,0 @@
|
|||
(**************************************************************************)
|
||||
(* *)
|
||||
(* Heptagon *)
|
||||
(* *)
|
||||
(* Author : Marc Pouzet *)
|
||||
(* Organization : Demons, LRI, University of Paris-Sud, Orsay *)
|
||||
(* *)
|
||||
(**************************************************************************)
|
||||
(* removing reset statements *)
|
||||
|
||||
|
||||
open Misc
|
||||
open Idents
|
||||
open Heptagon
|
||||
open Types
|
||||
|
||||
(* We introduce an initialization variable for each block *)
|
||||
(* Using an asynchronous reset would allow to produce *)
|
||||
(* better code avoiding to introduce n local variables and *)
|
||||
(* n state variables *)
|
||||
(* reset
|
||||
switch e with
|
||||
case C1 do ...
|
||||
| case C2 do ...
|
||||
| case C3 do ...
|
||||
end
|
||||
every r
|
||||
|
||||
switch e with
|
||||
case C1 do ... (* l_m1 *)
|
||||
m1 = false; m2 = l_m2; m3 = l_m3
|
||||
| case C2 do ... (* l_m2 *)
|
||||
m1 = l_m1; m2 = false; m3 = l_m3
|
||||
| case C3 do ... (* l_m3 *)
|
||||
m1 = l_m1; m2 = l_m2; m3 = false
|
||||
end;
|
||||
l_m1 = if res then true else true fby m1;...;
|
||||
l_m3 = if res then true else true fby m3
|
||||
|
||||
e1 -> e2 is translated into if (true fby false) then e1 else e2
|
||||
*)
|
||||
|
||||
let mk_bool_var n =
|
||||
mk_exp (Evar n) (Tid Initial.pbool)
|
||||
let mk_bool_param n =
|
||||
mk_var_dec n (Tid Initial.pbool)
|
||||
|
||||
let or_op_call = mk_op (Efun Initial.por)
|
||||
|
||||
let pre_true e =
|
||||
{ e with e_desc = Epre (Some (mk_static_exp ~ty:(Tid Initial.pbool)
|
||||
(Sconstructor Initial.ptrue)), e) }
|
||||
let init e = pre_true { dfalse with e_loc = e.e_loc }
|
||||
|
||||
(* the boolean condition for a structural reset *)
|
||||
type reset =
|
||||
| Rfalse
|
||||
| Rorthen of reset * ident
|
||||
|
||||
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 =
|
||||
match e.e_desc with
|
||||
| Econst c -> Some c
|
||||
| _ -> 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 =
|
||||
match res with
|
||||
| Rfalse -> mk_ifthenelse (init e3) e2 e3
|
||||
| _ -> (* a reset occurs *)
|
||||
mk_ifthenelse (exp_of_res res) e2 e3
|
||||
|
||||
(* add an equation *)
|
||||
let equation v acc_eq_list e =
|
||||
let n = Idents.fresh "r" in
|
||||
n,
|
||||
(mk_bool_param n) :: v,
|
||||
(mk_equation (Eeq(Evarpat n, e))) ::acc_eq_list
|
||||
|
||||
let orthen v acc_eq_list res e =
|
||||
match e.e_desc with
|
||||
| Evar(n) -> v, acc_eq_list, Rorthen(res, n)
|
||||
| _ ->
|
||||
let n, v, acc_eq_list = equation v acc_eq_list e in
|
||||
v, acc_eq_list, Rorthen(res, n)
|
||||
|
||||
let add_locals m n locals =
|
||||
let rec loop locals i n =
|
||||
if i < n then
|
||||
loop ((mk_bool_param m.(i)) :: locals) (i+1) n
|
||||
else locals in
|
||||
loop locals 0 n
|
||||
|
||||
let add_local_equations i n m lm acc =
|
||||
(* [mi = false;...; m1 = l_m1;...; mn = l_mn] *)
|
||||
let rec loop acc k =
|
||||
if k < n then
|
||||
if k = i
|
||||
then loop ((mk_simple_equation (Evarpat (m.(k))) dfalse) :: acc) (k+1)
|
||||
else
|
||||
loop
|
||||
((mk_simple_equation (Evarpat (m.(k))) (mk_bool_var lm.(k))) :: acc)
|
||||
(k+1)
|
||||
else acc
|
||||
in loop acc 0
|
||||
|
||||
let add_global_equations n m lm res acc =
|
||||
(* [ l_m1 = if res then true else true fby m1;...;
|
||||
l_mn = if res then true else true fby mn ] *)
|
||||
let rec loop acc k =
|
||||
if k < n then
|
||||
let exp =
|
||||
(match res with
|
||||
| Rfalse -> pre_true (mk_bool_var m.(k))
|
||||
| _ -> ifres res dtrue (pre_true (mk_bool_var m.(k)))
|
||||
) in
|
||||
loop
|
||||
((mk_equation (Eeq (Evarpat (lm.(k)), exp))) :: acc) (k+1)
|
||||
else acc in
|
||||
loop acc 0
|
||||
|
||||
let defnames m n d =
|
||||
let rec loop acc k =
|
||||
if k < n
|
||||
then loop (Env.add m.(k) (Tid Initial.pbool) acc) (k+1)
|
||||
else acc in
|
||||
loop d 0
|
||||
|
||||
let statefull eq_list = List.exists (fun eq -> eq.eq_statefull) eq_list
|
||||
|
||||
let rec translate_eq res v acc_eq_list eq =
|
||||
match eq.eq_desc with
|
||||
| Ereset(eq_list, e) ->
|
||||
let e = translate res e in
|
||||
if statefull eq_list then
|
||||
let v, acc_eq_list, res = orthen v acc_eq_list res e in
|
||||
translate_eqs res v acc_eq_list eq_list
|
||||
else
|
||||
let _, v, acc_eq_list = equation v acc_eq_list e in
|
||||
translate_eqs res v acc_eq_list eq_list
|
||||
| Eeq(pat, e) ->
|
||||
v, { eq with eq_desc = Eeq(pat, translate res e) } :: acc_eq_list
|
||||
| Eswitch(e, tag_block_list) ->
|
||||
let e = translate res e in
|
||||
let v, tag_block_list, acc_eq_list =
|
||||
translate_switch res v acc_eq_list tag_block_list in
|
||||
v, { eq with eq_desc = Eswitch(e, tag_block_list) } :: acc_eq_list
|
||||
| Epresent _ | Eautomaton _ -> assert false
|
||||
|
||||
and translate_eqs res v acc_eq_list eq_list =
|
||||
List.fold_left
|
||||
(fun (v, acc_eq_list) eq ->
|
||||
translate_eq res v acc_eq_list eq) (v, acc_eq_list) eq_list
|
||||
|
||||
and translate_switch res locals acc_eq_list switch_handlers =
|
||||
(* introduce a reset bit for each branch *)
|
||||
let tab_of_vars n = Array.init n (fun _ -> Idents.fresh "r") in
|
||||
let n = List.length switch_handlers in
|
||||
let m = tab_of_vars n in
|
||||
let lm = tab_of_vars n in
|
||||
|
||||
let locals = add_locals m n locals in
|
||||
let locals = add_locals lm n locals in
|
||||
|
||||
let body i {w_name = ci;
|
||||
w_block = ({ b_local = li; b_defnames = d; b_equs = eqi } as b)} =
|
||||
let d = defnames m n d in
|
||||
let li, eqi = translate_eqs (rvar (lm.(i))) li [] eqi in
|
||||
let eqi = add_local_equations i n m lm eqi in
|
||||
{ w_name = ci;
|
||||
w_block = { b with b_local = li; b_defnames = d; b_equs = eqi } } in
|
||||
|
||||
let rec loop i switch_handlers =
|
||||
match switch_handlers with
|
||||
[] -> []
|
||||
| handler :: switch_handlers ->
|
||||
(body i handler) :: (loop (i+1) switch_handlers) in
|
||||
|
||||
let acc_eq_list = add_global_equations n m lm res acc_eq_list in
|
||||
|
||||
locals, loop 0 switch_handlers, acc_eq_list
|
||||
|
||||
and translate res e =
|
||||
match e.e_desc with
|
||||
| Econst _ | Evar _ | Elast _ -> e
|
||||
| Efby (e1, e2) ->
|
||||
let e1 = translate res e1 in
|
||||
let e2 = translate res e2 in
|
||||
begin
|
||||
match res, e1 with
|
||||
| Rfalse, { e_desc = Econst c } ->
|
||||
(* no reset *)
|
||||
{ e with e_desc = Epre(Some c, e2) }
|
||||
| _ ->
|
||||
ifres res e1
|
||||
{ e with e_desc = Epre(default e1, e2) }
|
||||
end
|
||||
| Eapp({ a_op = Earrow }, [e1;e2], _) ->
|
||||
let e1 = translate res e1 in
|
||||
let e2 = translate res e2 in
|
||||
ifres res e1 e2
|
||||
| Epre (c, e1) ->
|
||||
{ e with e_desc = Epre (c, translate res e1)}
|
||||
|
||||
(* add reset to the current reset exp. *)
|
||||
| Eapp({ a_op = Enode _ } as op, e_list, Some re) ->
|
||||
let re = translate res re in
|
||||
let e_list = List.map (translate res) e_list in
|
||||
{ e with e_desc = Eapp(op, e_list, Some (or_op res re)) }
|
||||
(* create a new reset exp if necessary *)
|
||||
| Eapp({ a_op = Enode _ } as op, e_list, None) ->
|
||||
let e_list = List.map (translate res) e_list in
|
||||
if true_reset res then
|
||||
{ e with e_desc = Eapp(op, e_list, Some (exp_of_res res)) }
|
||||
else
|
||||
{ e with e_desc = Eapp(op, e_list, None) }
|
||||
(* add reset to the current reset exp. *)
|
||||
| Eiterator(it, ({ a_op = Enode _ } as op), n, e_list, Some re) ->
|
||||
let re = translate res re in
|
||||
let e_list = List.map (translate res) e_list in
|
||||
{ e with e_desc = Eiterator(it, op, n, e_list, Some (or_op res re)) }
|
||||
(* create a new reset exp if necessary *)
|
||||
| Eiterator(it, ({ a_op = Enode _ } as op), n, e_list, None) ->
|
||||
let e_list = List.map (translate res) e_list in
|
||||
if true_reset res then
|
||||
{ e
|
||||
with e_desc = Eiterator(it, op, n, e_list, Some (exp_of_res res)) }
|
||||
else
|
||||
{ e with e_desc = Eiterator(it, op, n, e_list, None) }
|
||||
| Eiterator(it, op, n, e_list, r) ->
|
||||
let e_list = List.map (translate res) e_list in
|
||||
{ e with e_desc = Eiterator(it, op, n, e_list, None) }
|
||||
|
||||
| Eapp(op, e_list, _) ->
|
||||
{ e with e_desc = Eapp(op, List.map (translate res) e_list, None) }
|
||||
| Estruct(e_f_list) ->
|
||||
{ e with e_desc =
|
||||
Estruct(List.map (fun (f, e) -> (f, translate res e)) e_f_list) }
|
||||
|
||||
let translate_contract ({ c_local = v;
|
||||
c_eq = eq_list;
|
||||
c_assume = e_a;
|
||||
c_enforce = e_g } as c) =
|
||||
let v, eq_list = translate_eqs rfalse v [] eq_list in
|
||||
let e_a = translate rfalse e_a in
|
||||
let e_g = translate rfalse e_g in
|
||||
{ c with c_local = v; c_eq = eq_list; c_assume = e_a; c_enforce = e_g }
|
||||
|
||||
let node n =
|
||||
let c = optional translate_contract n.n_contract in
|
||||
let var, eqs = translate_eqs rfalse n.n_local [] n.n_equs in
|
||||
{ n with n_local = var; n_equs = eqs; n_contract = c }
|
||||
|
||||
let program p =
|
||||
{ p with p_nodes = List.map node p.p_nodes }
|
||||
Loading…
Reference in a new issue