heptagon/compiler/main/hept2mls.ml

223 lines
8 KiB
OCaml
Raw Normal View History

2010-06-15 10:49:03 +02:00
(**************************************************************************)
(* *)
(* Heptagon *)
(* *)
(* Author : Marc Pouzet *)
(* Organization : Demons, LRI, University of Paris-Sud, Orsay *)
(* *)
(**************************************************************************)
(* removing switch statements and translation into Minils *)
open Location
open Misc
open Names
open Idents
2010-06-15 10:49:03 +02:00
open Static
2010-06-18 14:59:10 +02:00
open Types
2010-07-23 22:06:06 +02:00
open Clocks
2010-06-18 14:59:10 +02:00
open Format
2010-06-15 10:49:03 +02:00
open Minils
open Mls_utils
2010-06-18 14:59:10 +02:00
open Signature
module Error =
struct
type error =
| Ereset_not_var
| Eunsupported_language_construct
| Enormalization
2010-06-18 14:59:10 +02:00
let message loc kind =
begin match kind with
| Ereset_not_var ->
eprintf "%aOnly variables can be used for resets.@."
print_location loc
2010-06-18 14:59:10 +02:00
| 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
2010-06-18 14:59:10 +02:00
end;
raise Errors.Error
2010-06-18 14:59:10 +02:00
end
2010-06-15 10:49:03 +02:00
(* add an equation *)
let equation locals eqs e =
let n = Idents.gen_var "hept2mls" "ck" in
2010-06-15 10:49:03 +02:00
n,
2010-06-18 14:59:10 +02:00
(mk_var_dec n e.e_ty) :: locals,
(mk_equation (Evarpat n) e):: eqs
2010-06-15 10:49:03 +02:00
2010-07-15 10:02:42 +02:00
let translate_var { Heptagon.v_ident = n; Heptagon.v_type = ty;
Heptagon.v_loc = loc } =
mk_var_dec ~loc:loc n ty
2010-06-15 10:49:03 +02:00
2010-06-18 14:59:10 +02:00
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
| None -> None
2010-06-15 10:49:03 +02:00
2010-06-18 14:59:10 +02:00
let translate_iterator_type = function
| Heptagon.Imap -> Imap
| Heptagon.Imapi -> Imapi
| Heptagon.Ifold -> Ifold
| Heptagon.Ifoldi -> Ifoldi
| Heptagon.Imapfold -> Imapfold
2010-06-18 14:59:10 +02:00
let rec translate_op = function
| Heptagon.Eequal -> Eequal
2010-07-13 08:38:51 +02:00
| Heptagon.Eifthenelse -> Eifthenelse
| Heptagon.Efun f -> Efun f
| Heptagon.Enode f -> Enode f
| Heptagon.Efield -> assert false
2010-07-13 08:38:51 +02:00
| Heptagon.Efield_update -> Efield_update
| Heptagon.Earray_fill -> Earray_fill
| Heptagon.Eselect -> Eselect
| Heptagon.Eselect_dyn -> Eselect_dyn
| Heptagon.Eupdate -> Eupdate
| Heptagon.Eselect_slice -> Eselect_slice
| Heptagon.Eselect_trunc -> Eselect_trunc
2010-07-13 08:38:51 +02:00
| Heptagon.Econcat -> Econcat
| Heptagon.Earray -> Earray
2011-04-18 16:09:07 +02:00
| Heptagon.Etuple -> Misc.internal_error "hept2mls Etuple" 1
| Heptagon.Earrow -> assert false
2010-07-13 08:38:51 +02:00
let translate_app app =
2011-03-09 00:02:30 +01:00
mk_app ~params:app.Heptagon.a_params
~unsafe:app.Heptagon.a_unsafe (translate_op app.Heptagon.a_op)
let rec translate_extvalue e =
let mk_extvalue = mk_extvalue ~loc:e.Heptagon.e_loc ~ty:e.Heptagon.e_ty in
match e.Heptagon.e_desc with
| Heptagon.Econst c -> mk_extvalue (Wconst c)
| Heptagon.Evar x -> mk_extvalue (Wvar x)
| Heptagon.Ewhen (e, c, ce) ->
(match ce.Heptagon.e_desc with
| Heptagon.Evar x ->
mk_extvalue (Wwhen (translate_extvalue e, c, x))
| _ -> Error.message e.Heptagon.e_loc Error.Enormalization)
| Heptagon.Eapp({ Heptagon.a_op = Heptagon.Efield;
Heptagon.a_params = params }, e_list, reset) ->
let e = assert_1 e_list in
let f = assert_1 params in
let fn = match f.se_desc with Sfield fn -> fn | _ -> assert false in
mk_extvalue (Wfield (translate_extvalue e, fn))
| _ -> Error.message e.Heptagon.e_loc Error.Enormalization
let translate
({ Heptagon.e_desc = desc; Heptagon.e_ty = ty;
Heptagon.e_loc = loc } as e) =
let mk_exp = mk_exp ~loc:loc in
match desc with
| Heptagon.Econst _
| Heptagon.Evar _
| Heptagon.Ewhen _
| Heptagon.Eapp({ Heptagon.a_op = Heptagon.Efield }, _, _) ->
let w = translate_extvalue e in
mk_exp ty (Eextvalue w)
| Heptagon.Epre(None, e) ->
mk_exp ty (Efby(None, translate_extvalue e))
2010-07-13 08:38:51 +02:00
| Heptagon.Epre(Some c, e) ->
mk_exp ty (Efby(Some c, translate_extvalue e))
| Heptagon.Efby ({ Heptagon.e_desc = Heptagon.Econst c }, e) ->
mk_exp ty (Efby(Some c, translate_extvalue e))
| Heptagon.Estruct f_e_list ->
let f_e_list = List.map
(fun (f, e) -> (f, translate_extvalue e)) f_e_list in
mk_exp ty (Estruct f_e_list)
| Heptagon.Eapp({ Heptagon.a_op = Heptagon.Earrow }, _, _) ->
Error.message loc Error.Eunsupported_language_construct
2010-07-13 08:38:51 +02:00
| Heptagon.Eapp(app, e_list, reset) ->
mk_exp ty (Eapp (translate_app app,
List.map translate_extvalue e_list,
translate_reset reset))
| Heptagon.Eiterator(it, app, n, pe_list, e_list, reset) ->
mk_exp ty
(Eiterator (translate_iterator_type it,
translate_app app, n,
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
2010-12-14 18:34:06 +01:00
| Heptagon.Emerge (e, c_e_list) ->
(match e.Heptagon.e_desc with
| Heptagon.Evar x ->
mk_exp ty
(Emerge (x, List.map (fun (c,e)->c,
translate_extvalue e) c_e_list))
| _ -> Error.message loc Error.Enormalization)
2010-06-15 10:49:03 +02:00
let rec translate_pat = function
| Heptagon.Evarpat(n) -> Evarpat n
| Heptagon.Etuplepat(l) -> Etuplepat (List.map translate_pat l)
let rec translate_eq
2010-06-18 14:59:10 +02:00
{ Heptagon.eq_desc = desc; Heptagon.eq_loc = loc } =
match desc with
| Heptagon.Eeq(p, e) ->
mk_equation ~loc:loc (translate_pat p) (translate e)
| Heptagon.Eblock _ | Heptagon.Eswitch _
2010-06-15 10:49:03 +02:00
| Heptagon.Epresent _ | Heptagon.Eautomaton _ | Heptagon.Ereset _ ->
2010-06-18 14:59:10 +02:00
Error.message loc Error.Eunsupported_language_construct
2010-06-15 10:49:03 +02:00
let translate_contract contract =
2010-06-15 10:49:03 +02:00
match contract with
| None -> None
| Some { Heptagon.c_block = { Heptagon.b_local = v;
Heptagon.b_equs = eq_list };
2010-06-15 10:49:03 +02:00
Heptagon.c_assume = e_a;
2010-12-08 17:32:24 +01:00
Heptagon.c_enforce = e_g;
Heptagon.c_controllables = l_c } ->
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 n =
{ n_name = n.Heptagon.n_name;
n_stateful = n.Heptagon.n_stateful;
n_input = List.map translate_var n.Heptagon.n_input;
n_output = List.map translate_var n.Heptagon.n_output;
n_contract = translate_contract n.Heptagon.n_contract;
n_local = List.map translate_var n.Heptagon.n_block.Heptagon.b_local;
n_equs = List.map translate_eq n.Heptagon.n_block.Heptagon.b_equs;
n_loc = n.Heptagon.n_loc ;
n_params = n.Heptagon.n_params;
n_params_constraints = n.Heptagon.n_params_constraints }
2010-06-15 10:49:03 +02:00
let typedec
{Heptagon.t_name = n; Heptagon.t_desc = tdesc; Heptagon.t_loc = loc} =
let onetype = function
| Heptagon.Type_abs -> Type_abs
| Heptagon.Type_alias ln -> Type_alias ln
2010-06-18 14:59:10 +02:00
| Heptagon.Type_enum tag_list -> Type_enum tag_list
| Heptagon.Type_struct field_ty_list -> Type_struct field_ty_list
2010-06-15 10:49:03 +02:00
in
{ t_name = n; t_desc = onetype tdesc; t_loc = loc }
let const_dec cd =
{ Minils.c_name = cd.Heptagon.c_name;
Minils.c_value = cd.Heptagon.c_value;
Minils.c_type = cd.Heptagon.c_type;
Minils.c_loc = cd.Heptagon.c_loc; }
2010-06-15 10:49:03 +02:00
let program_desc pd = match pd with
| Heptagon.Ptype td -> Ptype (typedec td)
| Heptagon.Pnode nd -> Pnode (node nd)
| Heptagon.Pconst cd -> Pconst (const_dec cd)
let program
{ Heptagon.p_modname = modname;
Heptagon.p_opened = modules;
Heptagon.p_desc = desc_list } =
{ p_modname = modname;
p_format_version = minils_format_version;
2010-06-15 10:49:03 +02:00
p_opened = modules;
p_desc = List.map program_desc desc_list }