Added controllables in every pass

This commit is contained in:
Gwenal Delaval 2010-12-08 17:32:24 +01:00
parent b7cba3315a
commit ed2642f847
7 changed files with 35 additions and 17 deletions

View file

@ -365,15 +365,17 @@ let build_initialized h vdecs =
let typing_contract h contract =
match contract with
| None -> h
| Some { c_block = b; c_assume = e_a;
c_enforce = e_g } ->
| Some { c_block = b;
c_assume = e_a;
c_enforce = e_g;
c_controllables = c } ->
let h' = build h b.b_local in
typing_eqs h' b.b_equs;
(* assumption *)
expect h' e_a (skeleton izero e_a.e_ty);
(* property *)
expect h' e_g (skeleton izero e_g.e_ty);
h
build_initialized h c
let typing_node { n_input = i_list; n_output = o_list;
n_contract = contract; n_block = b } =

View file

@ -990,7 +990,8 @@ let typing_contract const_env h contract =
| None -> None,h
| Some ({ c_block = b;
c_assume = e_a;
c_enforce = e_g }) ->
c_enforce = e_g;
c_controllables = c }) ->
let typed_b, defined_names, _ = typing_block const_env h b in
(* check that the equations do not define other unexpected names *)
included_env defined_names Env.empty;
@ -1000,9 +1001,12 @@ let typing_contract const_env h contract =
(* property *)
let typed_e_g = expect const_env h (Tid Initial.pbool) e_g in
Some { c_block = typed_b;
c_assume = typed_e_a;
c_enforce = typed_e_g }, h
let typed_c, (c_names, h) = build const_env h c in
Some { c_block = typed_b;
c_assume = typed_e_a;
c_enforce = typed_e_g;
c_controllables = typed_c }, h
let solve loc cl =
try

View file

@ -254,9 +254,13 @@ and contract funs acc c =
let c_assume, acc = exp_it funs acc c.c_assume in
let c_enforce, acc = exp_it funs acc c.c_enforce in
let c_block, acc = block_it funs acc c.c_block in
let c_controllables, acc = mapfold (var_dec_it funs) acc c.c_controllables in
{ c with
c_assume = c_assume; c_enforce = c_enforce; c_block = c_block }
, acc
c_assume = c_assume;
c_enforce = c_enforce;
c_block = c_block;
c_controllables = c_controllables },
acc
and param_it funs acc vd = funs.param funs acc vd
and param funs acc vd =

View file

@ -364,6 +364,7 @@ let translate_contract env ct =
let b, _ = translate_block env ct.c_block in
{ Heptagon.c_assume = translate_exp env ct.c_assume;
Heptagon.c_enforce = translate_exp env ct.c_enforce;
Heptagon.c_controllables = translate_vd_list env ct.c_controllables;
Heptagon.c_block = b }
let params_of_var_decs =

View file

@ -350,7 +350,8 @@ let translate_contract env contract =
| Some { Heptagon.c_block = { Heptagon.b_local = v;
Heptagon.b_equs = eq_list };
Heptagon.c_assume = e_a;
Heptagon.c_enforce = e_g} ->
Heptagon.c_enforce = e_g;
Heptagon.c_controllables = l_c } ->
let env' = Env.add v env in
let locals = translate_locals [] v in
let locals, l_eqs, s_eqs =
@ -358,10 +359,12 @@ let translate_contract env contract =
let l_eqs, _ = add_locals IdentSet.empty l_eqs [] s_eqs in
let e_a = translate env' e_a in
let e_g = translate env' e_g in
let env = Env.add l_c env in
Some { c_local = locals;
c_eq = l_eqs;
c_assume = e_a;
c_enforce = e_g },
c_enforce = e_g;
c_controllables = List.map translate_var l_c },
env
@ -383,6 +386,7 @@ let node
n_input = List.map translate_var i;
n_output = List.map translate_var o;
n_contract = contract;
n_controller_call = ([],[]);
n_local = locals;
n_equs = l_eqs;
n_loc = loc ;

View file

@ -139,14 +139,15 @@ let typing_contract h contract base =
| Some { c_local = l_list;
c_eq = eq_list;
c_assume = e_a;
c_enforce = e_g; } ->
c_enforce = e_g;
c_controllables = c_list } ->
let h' = build h l_list in
(* assumption *)
(* property *)
(typing_eqs h' eq_list;
expect h' (Ck base) e_a;
expect h' (Ck base) e_g;
h)
typing_eqs h' eq_list;
expect h' (Ck base) e_a;
expect h' (Ck base) e_g;
sbuild h c_list base
let typing_node ({ n_input = i_list;
n_output = o_list;

View file

@ -144,11 +144,13 @@ let mk_equation ?(loc = no_location) pat exp =
let mk_node
?(input = []) ?(output = []) ?(contract = None) ?(local = []) ?(eq = [])
?(loc = no_location) ?(param = []) ?(constraints = []) ?(pinst = []) name =
?(loc = no_location) ?(param = []) ?(constraints = [])
?(pinst = ([],[])) name =
{ n_name = name;
n_input = input;
n_output = output;
n_contract = contract;
n_controller_call = pinst;
n_local = local;
n_equs = eq;
n_loc = loc;