Hept2mls ported and very simplified
Does not compile yet
This commit is contained in:
Cédric Pasteur
parent
d2c4f09aa2
commit
e2e8a93656
1 changed files with 69 additions and 280 deletions
|
|
@ -36,153 +36,24 @@ struct
|
|||
| Eunsupported_language_construct ->
|
||||
eprintf "%aThis construct is not supported by MiniLS.@."
|
||||
print_location loc
|
||||
| Enormalization ->
|
||||
eprintf "%aThis construct should have been normalized.@."
|
||||
print_location loc
|
||||
end;
|
||||
raise Errors.Error
|
||||
end
|
||||
|
||||
module Env =
|
||||
(* associate a clock level [base on C1(x1) on ... Cn(xn)] to every *)
|
||||
(* local name [x] *)
|
||||
(* then [x] is translated into [x when C1(x1) ... when Cn(xn)] *)
|
||||
struct
|
||||
type env =
|
||||
| Eempty
|
||||
| Ecomp of env * IdentSet.t
|
||||
| Eon of env * constructor_name * ident
|
||||
|
||||
let empty = Eempty
|
||||
|
||||
let push env tag c = Eon(env, tag, c)
|
||||
|
||||
let add l env =
|
||||
Ecomp(env,
|
||||
List.fold_left
|
||||
(fun acc { Heptagon.v_ident = n } ->
|
||||
IdentSet.add n acc) IdentSet.empty l)
|
||||
|
||||
(* sample e according to the clock [base on C1(x1) on ... on Cn(xn)] *)
|
||||
let con env x e =
|
||||
let rec conrec env =
|
||||
match env with
|
||||
| Eempty -> Format.eprintf "%s@." (name x); assert false
|
||||
| Eon(env, tag, name) ->
|
||||
let e, ck = conrec env in
|
||||
let ck_tag_name = Con(ck, tag, name) in
|
||||
{ e with e_desc = Ewhen(e, tag, name); e_ck = ck_tag_name },
|
||||
ck_tag_name
|
||||
| Ecomp(env, l) ->
|
||||
if IdentSet.mem x l then (e, Cbase) else conrec env in
|
||||
let e, _ = conrec env in e
|
||||
|
||||
(* a constant [c] is translated into [c when C1(x1) on ... on Cn(xn)] *)
|
||||
let const env e =
|
||||
let rec constrec env =
|
||||
match env with
|
||||
| Eempty -> e, Cbase
|
||||
| Eon(env, tag, name) ->
|
||||
let e, ck = constrec env in
|
||||
let ck_tag_name = Con(ck, tag, name) in
|
||||
{ e with e_desc = Ewhen(e, tag, name); e_ck = ck_tag_name },
|
||||
ck_tag_name
|
||||
| Ecomp(env, _) -> constrec env in
|
||||
let e, _ = constrec env in e
|
||||
end
|
||||
|
||||
(* add an equation *)
|
||||
let equation locals l_eqs e =
|
||||
let equation locals eqs e =
|
||||
let n = Idents.gen_var "hept2mls" "ck" in
|
||||
n,
|
||||
(mk_var_dec n e.e_ty) :: locals,
|
||||
(mk_equation (Evarpat n) e):: l_eqs
|
||||
|
||||
(* inserts the definition [x,e] into the set of shared equations *)
|
||||
let rec add x e shared =
|
||||
match shared with
|
||||
| [] -> [x, e]
|
||||
| (y, e_y) :: s ->
|
||||
if x < y then (x, e) :: shared else (y, e_y) :: add x e s
|
||||
|
||||
let add_locals ni l_eqs s_eqs s_handlers =
|
||||
let rec addrec l_eqs s_eqs s_handlers =
|
||||
match s_handlers with
|
||||
| [] -> l_eqs, s_eqs
|
||||
| (x, e) :: s_handlers ->
|
||||
if IdentSet.mem x ni then addrec l_eqs (add x e s_eqs) s_handlers
|
||||
else
|
||||
addrec ((mk_equation (Evarpat x) e) :: l_eqs)
|
||||
s_eqs s_handlers in
|
||||
addrec l_eqs s_eqs s_handlers
|
||||
(mk_equation (Evarpat n) e):: eqs
|
||||
|
||||
let translate_var { Heptagon.v_ident = n; Heptagon.v_type = ty;
|
||||
Heptagon.v_loc = loc } =
|
||||
mk_var_dec ~loc:loc n ty
|
||||
|
||||
let translate_locals locals l =
|
||||
List.fold_left (fun locals v -> translate_var v :: locals) locals l
|
||||
|
||||
(*transforms [c1, [(x1, e11);...;(xn, e1n)];...;ck, [(x1,ek1);...;(xn,ekn)]] *)
|
||||
(*into [x1=merge x (c1, e11)...(ck, ek1);...;xn=merge x (c1, e1n)...(ck,ekn)]*)
|
||||
let switch x ci_eqs_list =
|
||||
(* Defensive coherence check *)
|
||||
let check ci_eqs_list =
|
||||
let rec unique = function
|
||||
[] -> true
|
||||
| x :: h -> not (List.mem x h) && (unique h) in
|
||||
|
||||
let rec extract eqs_lists =
|
||||
match eqs_lists with
|
||||
| [] -> [],[]
|
||||
| []::eqs_lists' ->
|
||||
(* check length *)
|
||||
assert (List.for_all (function [] -> true | _ -> false) eqs_lists');
|
||||
[],[]
|
||||
| ((x,e)::eqs)::eqs_lists' ->
|
||||
let firsts,nexts = extract eqs_lists' in
|
||||
(x,e)::firsts,eqs::nexts in
|
||||
|
||||
let rec check_eqs eqs_lists =
|
||||
match eqs_lists with
|
||||
| [] -> ()
|
||||
| []::eqs_lists' ->
|
||||
(* check length *)
|
||||
assert (List.for_all (function [] -> true | _ -> false) eqs_lists')
|
||||
| _ ->
|
||||
let firsts,nexts = extract eqs_lists in
|
||||
(* check all firsts defining same name *)
|
||||
if (List.for_all (fun (x,_) -> x = (fst (List.hd firsts))) firsts)
|
||||
then ()
|
||||
else
|
||||
begin
|
||||
List.iter
|
||||
(fun (x,_) -> Format.eprintf "|%s|, " (name x))
|
||||
firsts;
|
||||
assert false
|
||||
end;
|
||||
check_eqs nexts in
|
||||
|
||||
let ci,eqs = List.split ci_eqs_list in
|
||||
(* constructors uniqueness *)
|
||||
assert (unique ci);
|
||||
check_eqs eqs in
|
||||
|
||||
let rec split ci_eqs_list =
|
||||
match ci_eqs_list with
|
||||
| [] | (_, []) :: _ -> [], []
|
||||
| (ci, (_, e) :: shared_eq_list) :: ci_eqs_list ->
|
||||
let ci_e_list, ci_eqs_list = split ci_eqs_list in
|
||||
(ci, e) :: ci_e_list, (ci, shared_eq_list) :: ci_eqs_list in
|
||||
|
||||
let rec distribute ci_eqs_list =
|
||||
match ci_eqs_list with
|
||||
| [] | (_, []) :: _ -> []
|
||||
| (_, (y, { e_ty = ty; e_loc = loc }) :: _) :: _ ->
|
||||
let ci_e_list, ci_eqs_list = split ci_eqs_list in
|
||||
(y, mk_exp ~ty:ty ~loc:loc (Emerge(x, ci_e_list))) ::
|
||||
distribute ci_eqs_list in
|
||||
|
||||
check ci_eqs_list;
|
||||
distribute ci_eqs_list
|
||||
|
||||
let translate_reset = function
|
||||
| Some { Heptagon.e_desc = Heptagon.Evar n } -> Some n
|
||||
| Some re -> Error.message re.Heptagon.e_loc Error.Ereset_not_var
|
||||
|
|
@ -211,197 +82,115 @@ let rec translate_op = function
|
|||
| Heptagon.Econcat -> Econcat
|
||||
| Heptagon.Earray -> Earray
|
||||
| Heptagon.Etuple -> Etuple
|
||||
| Heptagon.Earrow -> Error.message no_location Error.Eunsupported_language_construct
|
||||
| Heptagon.Earrow -> assert false
|
||||
|
||||
let translate_app app =
|
||||
mk_app ~params:app.Heptagon.a_params
|
||||
~unsafe:app.Heptagon.a_unsafe (translate_op app.Heptagon.a_op)
|
||||
|
||||
let rec translate env
|
||||
let translate_extvalue
|
||||
{ Heptagon.e_desc = desc; Heptagon.e_ty = ty;
|
||||
Heptagon.e_loc = loc } =
|
||||
let mk_extvalue = mk_extvalue ~loc:loc ~ty:ty in
|
||||
match desc with
|
||||
| Heptagon.Econst c ->
|
||||
Env.const env (mk_extvalue (Wconst c))
|
||||
| Heptagon.Evar x ->
|
||||
Env.con env x (mk_extvalue (Wvar x))
|
||||
| Heptagon.Ewhen (e, c, ce) ->
|
||||
(match ce.Heptagon.e_desc with
|
||||
| Heptagon.Evar x ->
|
||||
mk_exp (Wwhen (translate_ext_value e, c, x))
|
||||
| _ -> Error.message loc Error.Enormalization)
|
||||
| Heptagon.Eapp({ a_op = Efield; a_params = params }, e_list, reset) ->
|
||||
let e = assert_1 e_list in
|
||||
let f = assert_1 params in
|
||||
let fn = match f with Sfield fn -> fn | _ -> asssert false in
|
||||
mk_extvalue (Wfield (translate_ext_value e, fn))
|
||||
| _ -> Error.message loc Error.Enormalization
|
||||
|
||||
let translate
|
||||
{ Heptagon.e_desc = desc; Heptagon.e_ty = ty;
|
||||
Heptagon.e_loc = loc } =
|
||||
match desc with
|
||||
| Heptagon.Econst c ->
|
||||
Env.const env (mk_exp ~loc:loc ~ty:ty (Econst c))
|
||||
| Heptagon.Evar x ->
|
||||
Env.con env x (mk_exp ~loc:loc ~ty:ty (Evar x))
|
||||
| Heptagon.Econst _
|
||||
| Heptagon.Evar _
|
||||
| Heptagon.Ewhen _
|
||||
| Heptagon.Eapp({ a_op = Efield }, _, _) ->
|
||||
let w = translate_extvalue e in
|
||||
mk_exp ~loc:loc ~ty:ty (Eextvalue w)
|
||||
| Heptagon.Epre(None, e) ->
|
||||
mk_exp ~loc:loc ~ty:ty (Efby(None, translate env e))
|
||||
mk_exp ~loc:loc ~ty:ty (Efby(None, translate_ext_value e))
|
||||
| Heptagon.Epre(Some c, e) ->
|
||||
mk_exp ~loc:loc ~ty:ty (Efby(Some c, translate env e))
|
||||
mk_exp ~loc:loc ~ty:ty (Efby(Some c, translate_extvalue e))
|
||||
| Heptagon.Efby ({ Heptagon.e_desc = Heptagon.Econst c }, e) ->
|
||||
mk_exp ~loc:loc ~ty:ty (Efby(Some c, translate env e))
|
||||
mk_exp ~loc:loc ~ty:ty (Efby(Some c, translate_extvalue e))
|
||||
| Heptagon.Estruct f_e_list ->
|
||||
let f_e_list = List.map
|
||||
(fun (f, e) -> (f, translate env e)) f_e_list in
|
||||
(fun (f, e) -> (f, translate_extvalue e)) f_e_list in
|
||||
mk_exp ~loc:loc ~ty:ty (Estruct f_e_list)
|
||||
| Heptagon.Eapp({ a_op = Earrow }, _, _) ->
|
||||
Error.message loc Error.Eunsupported_language_construct
|
||||
| Heptagon.Eapp(app, e_list, reset) ->
|
||||
mk_exp ~loc:loc ~ty:ty (Eapp (translate_app app,
|
||||
List.map (translate env) e_list,
|
||||
translate_reset reset))
|
||||
List.map translate_extvalue e_list,
|
||||
translate_reset reset))
|
||||
| Heptagon.Eiterator(it, app, n, pe_list, e_list, reset) ->
|
||||
mk_exp ~loc:loc ~ty:ty
|
||||
(Eiterator (translate_iterator_type it,
|
||||
translate_app app, n,
|
||||
List.map (translate env) pe_list,
|
||||
List.map (translate env) e_list,
|
||||
List.map translate_extvalue pe_list,
|
||||
List.map translate_extvalue e_list,
|
||||
translate_reset reset))
|
||||
| Heptagon.Efby _
|
||||
| Heptagon.Elast _ ->
|
||||
Error.message loc Error.Eunsupported_language_construct
|
||||
| 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)
|
||||
(Emerge (x, List.map (fun (c,e)->c,
|
||||
translate_extvalue e) c_e_list))
|
||||
| _ -> Error.message loc Error.Enormalization)
|
||||
|
||||
let rec translate_pat = function
|
||||
| Heptagon.Evarpat(n) -> Evarpat n
|
||||
| Heptagon.Etuplepat(l) -> Etuplepat (List.map translate_pat l)
|
||||
|
||||
let rec rename_pat ni locals s_eqs = function
|
||||
| Heptagon.Evarpat(n), ty ->
|
||||
if IdentSet.mem n ni then (
|
||||
let n_copy = Idents.gen_var "hept2mls" (name n) in
|
||||
Evarpat n_copy,
|
||||
(mk_var_dec n_copy ty) :: locals,
|
||||
add n (mk_exp ~ty:ty (Evar n_copy)) s_eqs
|
||||
) else
|
||||
Evarpat n, locals, s_eqs
|
||||
| Heptagon.Etuplepat(l), Tprod l_ty ->
|
||||
let l, locals, s_eqs =
|
||||
List.fold_right2
|
||||
(fun pat ty (p_list, locals, s_eqs) ->
|
||||
let pat, locals, s_eqs = rename_pat ni locals s_eqs (pat,ty) in
|
||||
pat :: p_list, locals, s_eqs) l l_ty
|
||||
([], locals, s_eqs) in
|
||||
Etuplepat(l), locals, s_eqs
|
||||
| _ -> assert false
|
||||
|
||||
let all_locals ni p =
|
||||
IdentSet.is_empty (IdentSet.inter (Heptagon.vars_pat p) ni)
|
||||
|
||||
let rec translate_eq env ni (locals, l_eqs, s_eqs)
|
||||
let rec translate_eq env
|
||||
{ Heptagon.eq_desc = desc; Heptagon.eq_loc = loc } =
|
||||
match desc with
|
||||
| Heptagon.Eswitch(e, switch_handlers) ->
|
||||
translate_switch_handlers env ni (locals,l_eqs,s_eqs) e switch_handlers
|
||||
| Heptagon.Eeq(Heptagon.Evarpat n, e) when IdentSet.mem n ni ->
|
||||
locals,
|
||||
l_eqs,
|
||||
add n (translate env e) s_eqs
|
||||
| Heptagon.Eeq(p, e) when all_locals ni p ->
|
||||
(* all vars from [p] are local *)
|
||||
locals,
|
||||
(mk_equation ~loc:loc (translate_pat p) (translate env e)) :: l_eqs,
|
||||
s_eqs
|
||||
| Heptagon.Eeq(p, e) (* some are local *) ->
|
||||
(* transforms [p = e] into [p' = e; p = p'] *)
|
||||
let p', locals, s_eqs =
|
||||
rename_pat ni locals s_eqs (p, e.Heptagon.e_ty) in
|
||||
locals,
|
||||
(mk_equation ~loc:loc p' (translate env e)) :: l_eqs,
|
||||
s_eqs
|
||||
| Heptagon.Eblock _
|
||||
| Heptagon.Eeq(p, e) ->
|
||||
mk_equation ~loc:loc (translate_pat p) (translate env e)
|
||||
| Heptagon.Eblock _ | Heptagon.Eswitch
|
||||
| Heptagon.Epresent _ | Heptagon.Eautomaton _ | Heptagon.Ereset _ ->
|
||||
Error.message loc Error.Eunsupported_language_construct
|
||||
|
||||
and translate_eqs env ni (locals, local_eqs, shared_eqs) eq_list =
|
||||
List.fold_left
|
||||
(fun (locals, local_eqs, shared_eqs) eq ->
|
||||
translate_eq env ni (locals, local_eqs, shared_eqs) eq)
|
||||
(locals, local_eqs, shared_eqs) eq_list
|
||||
|
||||
and translate_block env ni (locals, l_eqs)
|
||||
{ Heptagon.b_local = l; Heptagon.b_equs = eq_list} =
|
||||
let env = Env.add l env in
|
||||
let locals = translate_locals locals l in
|
||||
let locals, local_eqs, shared_eqs =
|
||||
translate_eqs env ni (locals, l_eqs, []) eq_list in
|
||||
locals, local_eqs, shared_eqs
|
||||
|
||||
and translate_switch_handlers env ni (locals, l_eqs, s_eqs) e handlers =
|
||||
let rec transrec x ni_handlers (locals, l_eqs, ci_s_eqs_list) handlers =
|
||||
match handlers with
|
||||
[] -> locals, l_eqs, ci_s_eqs_list
|
||||
| { Heptagon.w_name = ci; Heptagon.w_block = b } :: handlers ->
|
||||
let locals, l_eqs, s_eqs =
|
||||
translate_block (Env.push env ci x) ni_handlers (locals, l_eqs) b in
|
||||
transrec x ni_handlers (locals, l_eqs, (ci, s_eqs) :: ci_s_eqs_list)
|
||||
handlers in
|
||||
|
||||
let def = function
|
||||
[] -> IdentSet.empty
|
||||
| { Heptagon.w_block = { Heptagon.b_defnames = env } } :: _ ->
|
||||
(* Create set from env *)
|
||||
(Idents.Env.fold
|
||||
(fun name _ set -> IdentSet.add name set)
|
||||
env
|
||||
IdentSet.empty) in
|
||||
|
||||
let ni_handlers = def handlers in
|
||||
let x, locals, l_eqs = equation locals l_eqs (translate env e) in
|
||||
let locals, l_eqs, ci_s_eqs_list =
|
||||
transrec x ni_handlers (locals, l_eqs, []) handlers in
|
||||
let s_handlers = switch x ci_s_eqs_list in
|
||||
let l_eqs, s_eqs = add_locals ni l_eqs s_eqs s_handlers in
|
||||
locals, l_eqs, s_eqs
|
||||
|
||||
let translate_contract env contract =
|
||||
let translate_contract contract =
|
||||
match contract with
|
||||
| None -> None, env
|
||||
| None -> None
|
||||
| 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_controllables = l_c } ->
|
||||
let env' = Env.add v env in
|
||||
let locals = translate_locals [] v in
|
||||
let locals, l_eqs, s_eqs =
|
||||
translate_eqs env' IdentSet.empty (locals, [], []) eq_list in
|
||||
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_controllables = List.map translate_var l_c },
|
||||
env
|
||||
Some { c_local = List.map translate_var v;
|
||||
c_eq = List.map translate_eq eq_list;
|
||||
c_assume = translate e_a;
|
||||
c_enforce = translate e_g;
|
||||
c_controllables = List.map translate_var l_c }
|
||||
|
||||
|
||||
let node
|
||||
{ Heptagon.n_name = n; Heptagon.n_input = i; Heptagon.n_output = o;
|
||||
Heptagon.n_contract = contract; Heptagon.n_stateful = stateful;
|
||||
Heptagon.n_block = { Heptagon.b_local = v; Heptagon.b_equs = eq_list };
|
||||
Heptagon.n_loc = loc;
|
||||
Heptagon.n_params = params;
|
||||
Heptagon.n_params_constraints = params_constr } =
|
||||
let env = Env.add o (Env.add i Env.empty) in
|
||||
let contract, env = translate_contract env contract in
|
||||
let env = Env.add v env in
|
||||
let locals = translate_locals [] v in
|
||||
let locals, l_eqs, s_eqs =
|
||||
translate_eqs env IdentSet.empty (locals, [], []) eq_list in
|
||||
let l_eqs, _ = add_locals IdentSet.empty l_eqs [] s_eqs in
|
||||
{ n_name = n;
|
||||
n_stateful = stateful;
|
||||
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 ;
|
||||
n_params = params;
|
||||
n_params_constraints = params_constr }
|
||||
let node n =
|
||||
{ n_name = n.Heptagon.n_name;
|
||||
n_stateful = n.Heptagon.n_stateful;
|
||||
n_input = List.map translate_var n.Heptagon.n_inputs;
|
||||
n_output = List.map translate_var n.Heptagon.n_outputs;
|
||||
n_contract = translate_contract n.Heptagon.n_contract;
|
||||
n_local = List.map translate_var n.Heptagon.n_block.Heptagon.n_locals;
|
||||
n_equs = List.map translate_eq n.Heptagon.n_block.Heptagon.n_equs;
|
||||
n_loc = n.Heptagon.n_loc ;
|
||||
n_params = n.Heptagon.n_params;
|
||||
n_params_constraints = n.Heptagon.n_params_constraints }
|
||||
|
||||
let typedec
|
||||
{Heptagon.t_name = n; Heptagon.t_desc = tdesc; Heptagon.t_loc = loc} =
|
||||
|
|
|
|||
Loading…
Reference in a new issue