Switch removing.
This commit is contained in:
Léonard Gérard
parent
ac9f805446
commit
ac6dab15ee
|
|
@ -108,12 +108,14 @@ let rec typing e =
|
|||
candlist l
|
||||
| Eiterator (_, _, _, e_list, _) ->
|
||||
ctuplelist (List.map typing e_list)
|
||||
| Ewhen (e, c, n) ->
|
||||
| Ewhen (e, c, ce) ->
|
||||
let t = typing e in
|
||||
let tc = typing ce in
|
||||
cseq tc t
|
||||
| Emerge (e, c_e_list) ->
|
||||
let t = typing e in
|
||||
cseq (read n) t
|
||||
| Emerge (n, c_e_list) ->
|
||||
let tl = List.map (fun (_,e) -> typing e) c_e_list in
|
||||
cseq (read n) (candlist tl)
|
||||
cseq t (candlist tl)
|
||||
|
||||
|
||||
(** Typing an application *)
|
||||
|
|
|
|||
|
|
@ -249,14 +249,14 @@ let rec typing h e =
|
|||
| Eiterator (_, _, _, e_list, _) ->
|
||||
List.iter (fun e -> initialized_exp h e) e_list;
|
||||
skeleton izero e.e_ty
|
||||
| Ewhen (e, _, n) ->
|
||||
let i = imax (itype (IEnv.find_var_typ n h)) (itype (typing h e)) in
|
||||
| Ewhen (e, _, ce) ->
|
||||
let i = imax (itype (typing h ce)) (itype (typing h e)) in
|
||||
skeleton i e.e_ty
|
||||
| Emerge (n, c_e_list) ->
|
||||
| Emerge (e, c_e_list) ->
|
||||
let i =
|
||||
List.fold_left
|
||||
(fun acc (_, e) -> imax acc (itype (typing h e))) izero c_e_list in
|
||||
let i = imax (itype (IEnv.find_var_typ n h)) i in
|
||||
let i = imax (itype (typing h e)) i in
|
||||
skeleton i e.e_ty
|
||||
|
||||
|
||||
|
|
@ -367,10 +367,10 @@ let build_initialized h vdecs =
|
|||
let typing_contract h contract =
|
||||
match contract with
|
||||
| None -> h
|
||||
| Some { c_block = b;
|
||||
c_assume = e_a;
|
||||
| Some { c_block = b;
|
||||
c_assume = e_a;
|
||||
c_enforce = e_g;
|
||||
c_controllables = c } ->
|
||||
c_controllables = c } ->
|
||||
let h' = build h b.b_local in
|
||||
typing_eqs h' b.b_equs;
|
||||
(* assumption *)
|
||||
|
|
|
|||
|
|
@ -543,14 +543,14 @@ let rec typing const_env h e =
|
|||
, typed_n, typed_e_list, reset), ty
|
||||
| Eiterator _ -> assert false
|
||||
|
||||
| Ewhen (e, c, n) ->
|
||||
| Ewhen (e, c, ce) ->
|
||||
let typed_e, t = typing const_env h e in
|
||||
let tn_expected = find_constrs c in
|
||||
let tn_actual = typ_of_name h n in
|
||||
let typed_ce, tn_actual = typing const_env h ce in
|
||||
unify tn_actual tn_expected;
|
||||
Ewhen (typed_e, c, n), t
|
||||
Ewhen (typed_e, c, typed_ce), t
|
||||
|
||||
| Emerge (n, (c1,e1)::c_e_list) ->
|
||||
| Emerge (e, (c1,e1)::c_e_list) ->
|
||||
(* verify the constructors : they should be unique,
|
||||
all of the same type and cover all the possibilities *)
|
||||
let c_type = find_constrs c1 in
|
||||
|
|
@ -575,13 +575,13 @@ let rec typing const_env h e =
|
|||
if not (QualSet.is_empty c_set_diff)
|
||||
then message e.e_loc (Emerge_missing_constrs c_set_diff);
|
||||
(* verify [n] is of the right type *)
|
||||
let n_type = typ_of_name h n in
|
||||
unify n_type c_type;
|
||||
let typed_e, e_type = typing const_env h e in
|
||||
unify e_type c_type;
|
||||
(* type *)
|
||||
let typed_e1, t = typing const_env h e1 in
|
||||
let typed_c_e_list =
|
||||
List.map (fun (c, e) -> (c, expect const_env h t e)) c_e_list in
|
||||
Emerge (n, (c1,typed_e1)::typed_c_e_list), t
|
||||
Emerge (typed_e, (c1,typed_e1)::typed_c_e_list), t
|
||||
| Emerge (_, []) -> assert false
|
||||
in
|
||||
{ e with e_desc = typed_desc; e_ty = ty; }, ty
|
||||
|
|
|
|||
|
|
@ -111,12 +111,12 @@ and print_exp_desc ff = function
|
|||
print_static_exp param
|
||||
print_exp_tuple args
|
||||
print_every reset
|
||||
| Ewhen (e, c, n) ->
|
||||
| Ewhen (e, c, ec) ->
|
||||
fprintf ff "@[<2>(%a@ when %a(%a))@]"
|
||||
print_exp e print_qualname c print_ident n
|
||||
| Emerge (x, tag_e_list) ->
|
||||
print_exp e print_qualname c print_exp ec
|
||||
| Emerge (e, tag_e_list) ->
|
||||
fprintf ff "@[<2>merge %a@ %a@]"
|
||||
print_ident x print_tag_e_list tag_e_list
|
||||
print_exp e print_tag_e_list tag_e_list
|
||||
|
||||
and print_handler ff c =
|
||||
fprintf ff "@[<2>%a@]" (print_couple print_qualname print_exp "("" -> "")") c
|
||||
|
|
@ -262,7 +262,7 @@ let rec print_type_def ff { t_name = name; t_desc = tdesc } =
|
|||
|
||||
let print_contract ff { c_block = b;
|
||||
c_assume = e_a; c_enforce = e_g;
|
||||
c_controllables = c} =
|
||||
c_controllables = c} =
|
||||
fprintf ff "@[<v2>contract@\n%a@ assume %a@ enforce %a@ with (%a)@]"
|
||||
(print_block "let") b
|
||||
print_exp e_a
|
||||
|
|
|
|||
|
|
@ -39,9 +39,9 @@ and desc =
|
|||
| Epre of static_exp option * exp
|
||||
| Efby of exp * exp
|
||||
| Estruct of (field_name * exp) list
|
||||
| Ewhen of exp * constructor_name * var_ident
|
||||
| Ewhen of exp * constructor_name * exp
|
||||
(** exp when Constructor(ident) *)
|
||||
| Emerge of var_ident * (constructor_name * exp) list
|
||||
| Emerge of exp * (constructor_name * exp) list
|
||||
(** merge ident (Constructor -> exp)+ *)
|
||||
| Eapp of app * exp list * exp option
|
||||
| Eiterator of iterator_type * app * static_exp * exp list * exp option
|
||||
|
|
@ -202,8 +202,8 @@ let mk_var_dec ?(last = Var) ?(ck = fresh_clock()) name ty =
|
|||
{ v_ident = name; v_type = ty; v_clock = ck;
|
||||
v_last = last; v_loc = no_location }
|
||||
|
||||
let mk_block ?(statefull = true) ?(defnames = Env.empty) eqs =
|
||||
{ b_local = []; b_equs = eqs; b_defnames = defnames;
|
||||
let mk_block ?(statefull = true) ?(defnames = Env.empty) ?(locals = []) eqs =
|
||||
{ b_local = locals; b_equs = eqs; b_defnames = defnames;
|
||||
b_statefull = statefull; b_loc = no_location }
|
||||
|
||||
let dfalse =
|
||||
|
|
|
|||
|
|
@ -64,6 +64,9 @@ let compile_impl pp p =
|
|||
(* Shared variables (last) *)
|
||||
let p = pass "Last" true Last.program p pp in
|
||||
|
||||
(* Remove switch statements *)
|
||||
let p = pass "switch" true Switch.program p pp in
|
||||
|
||||
(* Reset *)
|
||||
let p = pass "Reset" true Reset.program p pp in
|
||||
|
||||
|
|
|
|||
|
|
@ -254,20 +254,20 @@ and translate_desc loc env = function
|
|||
let app = Heptagon.mk_op ~params:params (translate_op op) in
|
||||
Heptagon.Eiterator (translate_iterator_type it,
|
||||
app, n, e_list, None)
|
||||
| Ewhen (e, c, n) ->
|
||||
| Ewhen (e, c, ce) ->
|
||||
let e = translate_exp env e in
|
||||
let c = qualify_constrs c in
|
||||
let n = Rename.var loc env n in
|
||||
Heptagon.Ewhen (e, c, n)
|
||||
| Emerge (n, c_e_list) ->
|
||||
let n = Rename.var loc env n in
|
||||
let ce = translate_exp env (mk_exp (Evar ce) loc) in
|
||||
Heptagon.Ewhen (e, c, ce)
|
||||
| Emerge (e, c_e_list) ->
|
||||
let e = translate_exp env (mk_exp (Evar e) loc) in
|
||||
let c_e_list =
|
||||
let fun_c_e (c, e) =
|
||||
let e = translate_exp env e in
|
||||
let c = qualify_constrs c in
|
||||
(c, e) in
|
||||
List.map fun_c_e c_e_list in
|
||||
Heptagon.Emerge (n, c_e_list)
|
||||
Heptagon.Emerge (e, c_e_list)
|
||||
|
||||
and translate_op = function
|
||||
| Eequal -> Heptagon.Eequal
|
||||
|
|
|
|||
|
|
@ -0,0 +1,222 @@
|
|||
(**************************************************************************)
|
||||
(* *)
|
||||
(* Heptagon *)
|
||||
(* *)
|
||||
(* Author : Marc Pouzet *)
|
||||
(* Organization : Demons, LRI, University of Paris-Sud, Orsay *)
|
||||
(* *)
|
||||
(**************************************************************************)
|
||||
|
||||
(* ASSUMES no automaton, no present, no last *)
|
||||
|
||||
(* Removing switch statements *)
|
||||
|
||||
(* sketch of the transformation :
|
||||
Eswitch is translated into an Eblock in the following way :
|
||||
|
||||
switch (e)
|
||||
up : block_up
|
||||
down : block_down
|
||||
|
||||
with one defined var y ( defnames = {y} ) and used var x
|
||||
(example : block_up = block : { var t in t = x + 3; y = t + 2; }
|
||||
|
||||
becomes :
|
||||
|
||||
block : {
|
||||
var ck, y_up, y_down in
|
||||
ck = e
|
||||
block_up[x when up(ck) /x][y_up /y]
|
||||
block_down[x when up(ck) /x][y_down /y]
|
||||
y = merge ck (up -> y_up) (down -> y_down)
|
||||
}
|
||||
*)
|
||||
|
||||
(* base_ck is used to have correct behavior for side effects :
|
||||
it keep track of the fact that a call
|
||||
without interaction with the dataflow was in a case of the switch *)
|
||||
|
||||
|
||||
|
||||
|
||||
open Misc
|
||||
open Heptagon
|
||||
open Hept_mapfold
|
||||
|
||||
(** Give the var [name] and a [constructor], returns fresh [name_constr] *)
|
||||
let fresh_case_var name constr =
|
||||
let tmp (n,c) =
|
||||
n^"_"^(Names.print_pp_to_name Global_printer.print_qualname c) in
|
||||
Idents.gen_fresh "switch" tmp (name,constr)
|
||||
|
||||
let fresh_clock_id () =
|
||||
Idents.gen_var "switch" "ck"
|
||||
|
||||
|
||||
|
||||
(** Environment [env]
|
||||
used to sample the shared variables : x ==> x when Up(ck)... *)
|
||||
module Env = struct
|
||||
|
||||
|
||||
open Idents
|
||||
open Names
|
||||
open Clocks
|
||||
|
||||
type t = Base | Level of ck * IdentSet.t * t
|
||||
|
||||
let level_up constr ckid env = match env with
|
||||
| Base -> Level(Con(Cbase, constr, ckid), IdentSet.empty, env)
|
||||
| Level (ck, _,_) -> Level(Con(ck, constr, ckid), IdentSet.empty, env)
|
||||
|
||||
let level_down env = match env with
|
||||
| Base -> Format.eprintf "Internal Error : wrong switch level"; assert false
|
||||
| Level(_,_, env_down) -> env_down
|
||||
|
||||
let add_var x env = match env with
|
||||
| Base -> Base
|
||||
| Level (ck, h, ed) ->
|
||||
Level(ck, IdentSet.add x h, ed)
|
||||
|
||||
(** Wraps [Evar]s with the needed [when]
|
||||
corresponding to their definition level *)
|
||||
let rec sample_var e env = match env with
|
||||
| Base -> e
|
||||
| Level (Con(_, constr, ck), h, env_d) ->
|
||||
(match e.e_desc with
|
||||
| Evar x ->
|
||||
if IdentSet.mem x h
|
||||
then e (* the var is declared at this level, nothing to do *)
|
||||
else (*sample to lower level*)
|
||||
{e with e_desc =
|
||||
Ewhen ((sample_var e env_d), constr, {e with e_desc = Evar ck})}
|
||||
| _ ->
|
||||
(Format.eprintf "'sample_var' called on full exp : %a@."
|
||||
Hept_printer.print_exp e;
|
||||
assert false))
|
||||
| Level _ -> assert false
|
||||
|
||||
|
||||
(** Gives back the current level clock *)
|
||||
let current_level env = match env with
|
||||
| Base -> Cbase
|
||||
| Level (ck, _,_) -> ck
|
||||
|
||||
(** Set the base clock of an expression to the current level of the [env] *)
|
||||
let annot_exp e env =
|
||||
{ e with e_base_ck = current_level env }
|
||||
|
||||
end
|
||||
|
||||
(** Renaming environment [h]
|
||||
to rename the defined shared variables : x = ... ==> x_up = ... *)
|
||||
module Rename = struct
|
||||
include Idents.Env
|
||||
|
||||
let rename n h =
|
||||
try find n h with _ -> n
|
||||
|
||||
let rename_defnames defnames h =
|
||||
fold (fun n ty acc -> add (rename n h) ty acc) defnames empty
|
||||
|
||||
let level_up defnames constr h =
|
||||
let ident_level_up n new_h =
|
||||
let old_n = rename n h in
|
||||
let new_n = fresh_case_var (Idents.name old_n) constr in
|
||||
add n new_n new_h in
|
||||
fold (fun n _ new_h -> ident_level_up n new_h) defnames empty
|
||||
|
||||
let add_to_vds defnames h vds =
|
||||
fold (fun n nn acc -> (Heptagon.mk_var_dec nn (find n defnames))::acc) vds h
|
||||
|
||||
end
|
||||
|
||||
(** Mapfold *)
|
||||
|
||||
|
||||
(* apply the renaming for shared defined variables *)
|
||||
let pattern _ (env,h) pat = match pat with
|
||||
| Evarpat x -> Evarpat (Rename.rename x h), (env,h)
|
||||
| _ -> raise Errors.Fallback
|
||||
|
||||
let var_dec _ (env,h) vd =
|
||||
let env = Env.add_var vd.v_ident env in
|
||||
vd, (env,h)
|
||||
|
||||
(* apply the renaming to the defnames *)
|
||||
let block funs (env,h) b =
|
||||
let b = { b with b_defnames = Rename.rename_defnames b.b_defnames h } in
|
||||
Hept_mapfold.block funs (env,h) b
|
||||
|
||||
(* apply the sampling on shared vars *)
|
||||
let exp funs (env,h) e =
|
||||
let e = Env.annot_exp e env in
|
||||
match e.e_desc with
|
||||
| Evar _ -> Env.sample_var e env, (env,h)
|
||||
| _ -> Hept_mapfold.exp funs (env,h) e
|
||||
|
||||
(* update statefull and loc *)
|
||||
let eq funs (env,h) eq =
|
||||
let eqd = match eq.eq_desc with
|
||||
| Eblock b -> (* probably created by eqdesc, so update statefull and loc *)
|
||||
Eblock { b with b_statefull = eq.eq_statefull; b_loc = eq.eq_loc }
|
||||
| _ -> eq.eq_desc in
|
||||
Hept_mapfold.eq funs (env,h) {eq with eq_desc = eqd}
|
||||
|
||||
(* remove the Eswitch *)
|
||||
let eqdesc funs (env,h) eqd = match eqd with
|
||||
| Eswitch (e, sw_h_l) ->
|
||||
(* create a clock var corresponding to the switch condition [e] *)
|
||||
let ck = fresh_clock_id () in
|
||||
let e, (env,h) = exp_it funs (env,h) e in
|
||||
let ck_e = { e with e_desc = Evar ck } in
|
||||
let locals = [Heptagon.mk_var_dec ck e.e_ty] in
|
||||
let equs = [Heptagon.mk_equation (Eeq (Evarpat ck, e))] in
|
||||
|
||||
(* typing have proved that defined variables are the same among states *)
|
||||
let defnames = (List.hd sw_h_l).w_block.b_defnames in
|
||||
let defnames = Rename.rename_defnames defnames h in
|
||||
|
||||
(* deal with the handlers *)
|
||||
let switch_handler (c_h_l, locals, equs) sw_h =
|
||||
let constr = sw_h.w_name in
|
||||
(* level up *)
|
||||
let h = Rename.level_up defnames constr h in
|
||||
let env = Env.level_up constr ck env in
|
||||
(* mapfold with updated envs *)
|
||||
let b_eq, (_,h) = block_it funs (env,h) sw_h.w_block in
|
||||
(* inline the handler as a block *)
|
||||
let equs = (Heptagon.mk_equation (Eblock b_eq))::equs in
|
||||
(* add to the locals the new vars from leveling_up *)
|
||||
let locals = Rename.add_to_vds defnames locals h in
|
||||
((constr,h)::c_h_l, locals, equs) in
|
||||
let (c_h_l, locals, equs) =
|
||||
List.fold_left switch_handler ([], locals, equs) sw_h_l in
|
||||
|
||||
(* create a merge equation for each defnames *)
|
||||
let new_merge n equs =
|
||||
let ty = (Idents.Env.find n defnames) in
|
||||
let c_h_to_c_e (constr,h) =
|
||||
constr, Heptagon.mk_exp (Evar (Rename.rename n h)) ty in
|
||||
let c_e_l = List.map c_h_to_c_e c_h_l in
|
||||
let merge = Heptagon.mk_exp (Emerge (ck_e, c_e_l)) ty in
|
||||
(Heptagon.mk_equation (Eeq (Evarpat n, merge))) :: equs in
|
||||
let equs =
|
||||
Idents.Env.fold (fun n _ equs -> new_merge n equs) defnames equs in
|
||||
|
||||
(* return the transformation in a block *)
|
||||
let b = Heptagon.mk_block ~defnames:defnames ~locals:locals equs in
|
||||
Eblock b, (env,h)
|
||||
| _ -> raise Errors.Fallback
|
||||
|
||||
let program p =
|
||||
let funs = { Hept_mapfold.defaults
|
||||
with pat = pattern; var_dec = var_dec; block = block;
|
||||
exp = exp; eq = eq; eqdesc = eqdesc } in
|
||||
let p, _ = program_it funs (Env.Base,Rename.empty) p in
|
||||
p
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
|
@ -247,11 +247,17 @@ let rec translate env
|
|||
| Heptagon.Efby _
|
||||
| Heptagon.Elast _ ->
|
||||
Error.message loc Error.Eunsupported_language_construct
|
||||
| Heptagon.Ewhen (e, c, n) ->
|
||||
mk_exp ~loc:loc ~ty:ty (Ewhen (translate env e, c, n))
|
||||
| Heptagon.Emerge (n, c_e_list) ->
|
||||
mk_exp ~loc:loc ~ty:ty
|
||||
(Emerge (n, List.map (fun (c,e) -> c, translate env e) c_e_list))
|
||||
| Heptagon.Ewhen (e, c, ce) ->
|
||||
(match ce.Heptagon.e_desc with
|
||||
| Heptagon.Evar x ->
|
||||
mk_exp ~loc:loc ~ty:ty (Ewhen (translate env e, c, x))
|
||||
| _ -> Format.eprintf "when with a nonvar condition.@."; assert false)
|
||||
| Heptagon.Emerge (e, c_e_list) ->
|
||||
(match e.Heptagon.e_desc with
|
||||
| Heptagon.Evar x ->
|
||||
mk_exp ~loc:loc ~ty:ty
|
||||
(Emerge (x, List.map (fun (c,e)->c, translate env e) c_e_list))
|
||||
| _ -> Format.eprintf "merge with a nonvar condition.@.";assert false)
|
||||
|
||||
let rec translate_pat = function
|
||||
| Heptagon.Evarpat(n) -> Evarpat n
|
||||
|
|
|
|||
Loading…
Reference in New Issue