Updated version of Hept_printer
The code is much clearer but it should print mostly the same thing.
This commit is contained in:
Cédric Pasteur
parent
d8dffe15d8
commit
4a5c9130e7
|
|
@ -32,329 +32,238 @@ let print_iterator ff it =
|
||||||
fprintf ff "%s" (iterator_to_string it)
|
fprintf ff "%s" (iterator_to_string it)
|
||||||
|
|
||||||
let rec print_pat ff = function
|
let rec print_pat ff = function
|
||||||
| Evarpat(n) -> print_ident ff n
|
| Evarpat n -> print_ident ff n
|
||||||
| Etuplepat(pat_list) ->
|
| Etuplepat pat_list ->
|
||||||
print_list_r print_pat "(" "," ")" ff pat_list
|
fprintf ff "@[<2>(%a)@]" (print_list_r print_pat """,""") pat_list
|
||||||
|
|
||||||
and print_vd ff { v_ident = n; v_type = ty; v_last = last } =
|
let rec print_vd ff { v_ident = n; v_type = ty; v_last = last } =
|
||||||
fprintf ff "@[<v>";
|
fprintf ff "%a%a : %a%a"
|
||||||
begin match last with Last _ -> fprintf ff "last " | _ -> () end;
|
print_last last print_ident n
|
||||||
print_ident ff n;
|
print_type ty print_last_value last
|
||||||
fprintf ff ": ";
|
|
||||||
print_type ff ty;
|
and print_last ff = function
|
||||||
begin
|
| Last _ -> fprintf ff "last "
|
||||||
match last with Last(Some(v)) -> fprintf ff "= ";print_static_exp ff v
|
| _ -> ()
|
||||||
| _ -> ()
|
|
||||||
end;
|
and print_last_value ff = function
|
||||||
fprintf ff "@]"
|
| Last (Some v) -> fprintf ff " = %a" print_static_exp v
|
||||||
|
| _ -> ()
|
||||||
|
|
||||||
|
let print_local_vars ff = function
|
||||||
|
| [] -> ()
|
||||||
|
| l -> fprintf ff "@[<4>%a@]@\n" (print_list_r print_vd "var "";"";") l
|
||||||
|
|
||||||
|
let print_const_dec ff c =
|
||||||
|
if !Misc.full_type_info then
|
||||||
|
fprintf ff "const %a : %a = %a"
|
||||||
|
print_qualname c.c_name print_type c.c_type print_static_exp c.c_value
|
||||||
|
else
|
||||||
|
fprintf ff "const %a = %a"
|
||||||
|
print_qualname c.c_name print_static_exp c.c_value;
|
||||||
|
fprintf ff "@."
|
||||||
|
|
||||||
|
|
||||||
|
let rec print_params ff l =
|
||||||
|
fprintf ff "@[<2>%a@]" (print_list_r print_static_exp "<<"","">>") l
|
||||||
|
|
||||||
|
and print_node_params ff l =
|
||||||
|
fprintf ff "@[<2>%a@]" (print_list_r print_param "<<"","">>") l
|
||||||
|
|
||||||
|
and print_exp_tuple ff l =
|
||||||
|
fprintf ff "@[<2>(%a)@]" (print_list_r print_exp """,""") l
|
||||||
|
|
||||||
|
and print_vd_tuple ff l =
|
||||||
|
fprintf ff "@[<2>%a@]" (print_list_r print_vd "("";"")") l
|
||||||
|
|
||||||
|
and print_index ff idx =
|
||||||
|
fprintf ff "@[<2>%a@]" (print_list print_static_exp "[""][""]") idx
|
||||||
|
|
||||||
|
and print_dyn_index ff idx =
|
||||||
|
fprintf ff "@[<2>%a@]" (print_list print_exp "[""][""]") idx
|
||||||
|
|
||||||
and print_exps ff e_list =
|
and print_exps ff e_list =
|
||||||
print_list_r print_exp "(" "," ")" ff e_list
|
print_list_r print_exp "(" "," ")" ff e_list
|
||||||
|
|
||||||
and print_exp ff e =
|
and print_exp ff e =
|
||||||
if !Misc.full_type_info then fprintf ff "(";
|
if !Misc.full_type_info then
|
||||||
begin match e.e_desc with
|
fprintf ff "(%a : %a)"
|
||||||
| Evar x -> print_ident ff x
|
print_exp_desc e.e_desc print_type e.e_ty
|
||||||
| Elast x -> fprintf ff "last "; print_ident ff x
|
else fprintf ff "%a" print_exp_desc e.e_desc
|
||||||
| Econst c -> print_static_exp ff c
|
|
||||||
| Epre(None, e) -> fprintf ff "pre "; print_exp ff e
|
|
||||||
| Epre(Some c, e) ->
|
|
||||||
print_static_exp ff c; fprintf ff " fby "; print_exp ff e
|
|
||||||
| Efby(e1, e2) -> print_exp ff e1; fprintf ff " fby "; print_exp ff e2
|
|
||||||
| Eapp({ a_op = op; a_params = params }, e_list, r) ->
|
|
||||||
print_op ff op params e_list;
|
|
||||||
(match r with
|
|
||||||
| None -> ()
|
|
||||||
| Some r -> fprintf ff " every %a" print_exp r
|
|
||||||
)
|
|
||||||
| Estruct(f_e_list) ->
|
|
||||||
print_list_r
|
|
||||||
(fun ff (field, e) -> print_qualname ff field;fprintf ff " = ";
|
|
||||||
print_exp ff e)
|
|
||||||
"{" ";" "}" ff f_e_list;
|
|
||||||
fprintf ff "}@]"
|
|
||||||
| Eiterator (it, { a_op = (Efun ln|Enode ln); a_params = params },
|
|
||||||
n, e_list, reset) ->
|
|
||||||
fprintf ff "(";
|
|
||||||
print_iterator ff it;
|
|
||||||
fprintf ff " ";
|
|
||||||
(match params with
|
|
||||||
| [] -> print_qualname ff ln
|
|
||||||
| l ->
|
|
||||||
fprintf ff "(";
|
|
||||||
print_qualname ff ln;
|
|
||||||
print_call_params ff params;
|
|
||||||
fprintf ff ")"
|
|
||||||
);
|
|
||||||
fprintf ff " <<";
|
|
||||||
print_static_exp ff n;
|
|
||||||
fprintf ff ">>) ";
|
|
||||||
print_exps ff e_list;
|
|
||||||
(match reset with
|
|
||||||
| None -> ()
|
|
||||||
| Some r -> fprintf ff " every %a" print_exp r
|
|
||||||
)
|
|
||||||
| Eiterator _ -> assert false
|
|
||||||
end;
|
|
||||||
if !Misc.full_type_info then fprintf ff " : %a)" print_type e.e_ty
|
|
||||||
|
|
||||||
and print_call_params ff = function
|
and print_exp_desc ff = function
|
||||||
| [] -> ()
|
| Evar x -> print_ident ff x
|
||||||
| l -> print_list_r print_static_exp "<<" "," ">>" ff l
|
| Elast x -> fprintf ff "last %a" print_ident x
|
||||||
|
| Econst c -> print_static_exp ff c
|
||||||
|
| Epre(None, e) -> fprintf ff "pre %a" print_exp e
|
||||||
|
| Epre(Some c, e) ->
|
||||||
|
fprintf ff "@[<2>%a fby@ %a@]" print_static_exp c print_exp e
|
||||||
|
| Efby(e1, e2) ->
|
||||||
|
fprintf ff "@[<2>%a fby@ %a@]" print_exp e1 print_exp e2
|
||||||
|
| Eapp(app, args, reset) ->
|
||||||
|
fprintf ff "@[<2>%a@,%a@]"
|
||||||
|
print_app (app, args) print_every reset
|
||||||
|
| Estruct(f_e_list) ->
|
||||||
|
print_record (print_couple print_qualname print_exp """ = """) ff f_e_list
|
||||||
|
| Eiterator (it, f, param, args, reset) ->
|
||||||
|
fprintf ff "@[<2>(%s (%a)<<%a>>)@,%a@]%a"
|
||||||
|
(iterator_to_string it)
|
||||||
|
print_app (f, [])
|
||||||
|
print_static_exp param
|
||||||
|
print_exp_tuple args
|
||||||
|
print_every reset
|
||||||
|
| Eiterator _ -> assert false
|
||||||
|
|
||||||
and print_op ff op params e_list =
|
and print_every ff reset =
|
||||||
match op with
|
print_opt (fun ff id -> fprintf ff " every %a" print_exp id) ff reset
|
||||||
| Eequal ->
|
|
||||||
let e1, e2 = assert_2 e_list in
|
and print_app ff (app, args) = match app.a_op with
|
||||||
fprintf ff "@[<2>%a@ = %a@]" print_exp e1 print_exp e2
|
| Eequal ->
|
||||||
| Earrow ->
|
let e1, e2 = assert_2 args in
|
||||||
let e1, e2 = assert_2 e_list in
|
fprintf ff "@[<2>%a@ = %a@]" print_exp e1 print_exp e2
|
||||||
print_exp ff e1; fprintf ff " -> "; print_exp ff e2
|
| Etuple -> print_exp_tuple ff args
|
||||||
| Eifthenelse ->
|
| Efun f | Enode f ->
|
||||||
let e1, e2, e3 = assert_3 e_list in
|
fprintf ff "@[%a@,%a@,%a@]"
|
||||||
fprintf ff "@["; fprintf ff "if "; print_exp ff e1;
|
print_qualname f print_params app.a_params print_exp_tuple args
|
||||||
fprintf ff "@ then@ "; print_exp ff e2;
|
| Eifthenelse ->
|
||||||
fprintf ff "@ else@ "; print_exp ff e3;
|
let e1, e2, e3 = assert_3 args in
|
||||||
fprintf ff "@]"
|
fprintf ff "@[<hv>if %a@ then %a@ else %a@]"
|
||||||
| Etuple -> print_exps ff e_list
|
print_exp e1 print_exp e2 print_exp e3
|
||||||
| Earray ->
|
| Efield ->
|
||||||
print_list_r print_exp "[" "," "]" ff e_list
|
let r = assert_1 args in
|
||||||
| (Efun f|Enode f) ->
|
let f = assert_1 app.a_params in
|
||||||
print_qualname ff f;
|
fprintf ff "%a.%a" print_exp r print_static_exp f
|
||||||
print_call_params ff params;
|
| Efield_update ->
|
||||||
print_exps ff e_list
|
let r,e = assert_2 args in
|
||||||
| Efield ->
|
let f = assert_1 app.a_params in
|
||||||
let e = assert_1 e_list in
|
fprintf ff "@[<2>{%a with .%a =@ %a}@]"
|
||||||
let field = assert_1 params in
|
print_exp r print_static_exp f print_exp e
|
||||||
print_exp ff e; fprintf ff ".";
|
| Earray -> fprintf ff "@[<2>%a@]" (print_list_r print_exp "["";""]") args
|
||||||
print_static_exp ff field
|
| Earray_fill ->
|
||||||
| Efield_update ->
|
let e = assert_1 args in
|
||||||
let e1, e2 = assert_2 e_list in
|
let n = assert_1 app.a_params in
|
||||||
let se = assert_1 params in
|
fprintf ff "%a^%a" print_exp e print_static_exp n
|
||||||
fprintf ff "(@[";
|
| Eselect ->
|
||||||
print_exp ff e1;
|
let e = assert_1 args in
|
||||||
fprintf ff " with .";
|
fprintf ff "%a%a" print_exp e print_index app.a_params
|
||||||
print_static_exp ff se;
|
| Eselect_slice ->
|
||||||
fprintf ff " = ";
|
let e = assert_1 args in
|
||||||
print_exp ff e2;
|
let idx1, idx2 = assert_2 app.a_params in
|
||||||
fprintf ff ")@]"
|
fprintf ff "%a[%a..%a]"
|
||||||
| Earray_fill ->
|
print_exp e print_static_exp idx1 print_static_exp idx2
|
||||||
let e = assert_1 e_list in
|
| Eselect_dyn ->
|
||||||
let se = assert_1 params in
|
let r, d, e = assert_2min args in
|
||||||
print_exp ff e;
|
fprintf ff "%a%a default %a"
|
||||||
fprintf ff "^";
|
print_exp r print_dyn_index e print_exp d
|
||||||
print_static_exp ff se
|
| Eupdate ->
|
||||||
| Eselect ->
|
let e1, e2, idx = assert_2min args in
|
||||||
let e = assert_1 e_list in
|
fprintf ff "@[<2>(%a with %a =@ %a)@]"
|
||||||
print_exp ff e;
|
print_exp e1 print_dyn_index idx print_exp e2
|
||||||
print_list_r print_static_exp "[" "][" "]" ff params
|
| Econcat ->
|
||||||
| Eselect_dyn ->
|
let e1, e2 = assert_2 args in
|
||||||
let e, defe, idx_list = assert_2min e_list in
|
fprintf ff "@[<2>%a@ @@ %a@]" print_exp e1 print_exp e2
|
||||||
fprintf ff "@[(";
|
| Earrow ->
|
||||||
print_exp ff e;
|
let e1, e2 = assert_2 args in
|
||||||
print_list_r print_exp "[" "][" "] default " ff idx_list;
|
fprintf ff "@[<2>%a ->@ %a@]" print_exp e1 print_exp e2
|
||||||
print_exp ff defe;
|
|
||||||
fprintf ff ")@]"
|
|
||||||
| Eupdate ->
|
|
||||||
let e1, e2, idx_list = assert_2min e_list in
|
|
||||||
fprintf ff "(@[";
|
|
||||||
print_exp ff e1;
|
|
||||||
fprintf ff " with ";
|
|
||||||
print_list_r print_exp "[" "][" "]" ff idx_list;
|
|
||||||
fprintf ff " = ";
|
|
||||||
print_exp ff e2;
|
|
||||||
fprintf ff ")@]"
|
|
||||||
| Eselect_slice ->
|
|
||||||
let e = assert_1 e_list in
|
|
||||||
let idx1, idx2 = assert_2 params in
|
|
||||||
print_exp ff e;
|
|
||||||
fprintf ff "[";
|
|
||||||
print_static_exp ff idx1;
|
|
||||||
fprintf ff "..";
|
|
||||||
print_static_exp ff idx2;
|
|
||||||
fprintf ff "]"
|
|
||||||
| Econcat ->
|
|
||||||
let e1, e2 = assert_2 e_list in
|
|
||||||
fprintf ff "@[";
|
|
||||||
print_exp ff e1;
|
|
||||||
fprintf ff " @@ ";
|
|
||||||
print_exp ff e2;
|
|
||||||
fprintf ff "@]"
|
|
||||||
|
|
||||||
let rec print_eq ff eq =
|
let rec print_eq ff eq =
|
||||||
match eq.eq_desc with
|
match eq.eq_desc with
|
||||||
| Eeq(p, e) ->
|
| Eeq(p, e) ->
|
||||||
fprintf ff "@[<hov 2>";
|
fprintf ff "@[<2>%a =@ %a@]" print_pat p print_exp e
|
||||||
print_pat ff p;
|
|
||||||
fprintf ff " =@ ";
|
|
||||||
print_exp ff e;
|
|
||||||
fprintf ff "@]"
|
|
||||||
| Eautomaton(state_handler_list) ->
|
| Eautomaton(state_handler_list) ->
|
||||||
fprintf ff "@[<v>automaton@,";
|
fprintf ff "@[<v>@[<hv 2>automaton @ %a@]@,end@]"
|
||||||
fprintf ff "@[<v>";
|
print_state_handler_list state_handler_list
|
||||||
print_list print_state_handler "" "" "" ff state_handler_list;
|
|
||||||
fprintf ff "@]@,";
|
|
||||||
fprintf ff "end@]"
|
|
||||||
| Eswitch(e, switch_handler_list) ->
|
| Eswitch(e, switch_handler_list) ->
|
||||||
fprintf ff "@[<v>switch ";
|
fprintf ff "@[<v>@[<hv 2>switch (%a) {@ %a@]@,}@]"
|
||||||
print_exp ff e;
|
print_exp e
|
||||||
fprintf ff "@,@[<v>";
|
print_switch_handler_list switch_handler_list
|
||||||
print_list print_switch_handler "" "" "" ff switch_handler_list;
|
|
||||||
fprintf ff "@]@,";
|
|
||||||
fprintf ff "end@]"
|
|
||||||
| Epresent(present_handler_list, b) ->
|
| Epresent(present_handler_list, b) ->
|
||||||
fprintf ff "@[<v>present@,";
|
fprintf ff "@[<v>@[<hv 2>present @ %a%a@]@,end@]"
|
||||||
print_list print_present_handler "" "" "" ff present_handler_list;
|
print_present_handler_list present_handler_list
|
||||||
if b.b_equs <> [] then begin
|
print_default b
|
||||||
fprintf ff " @[<v 2>default@,";
|
|
||||||
print_block ff b;
|
|
||||||
fprintf ff "@]"
|
|
||||||
end;
|
|
||||||
fprintf ff "@,end@]"
|
|
||||||
| Ereset(b, e) ->
|
| Ereset(b, e) ->
|
||||||
fprintf ff "@[<v>reset@,";
|
fprintf ff "@[<v>@[<hv 2>reset @ %a@]@,every %a@]"
|
||||||
fprintf ff " @[<v>";
|
print_block b print_exp e
|
||||||
print_block ff b;
|
|
||||||
fprintf ff "@]";
|
and print_state_handler_list ff tag_act_list =
|
||||||
fprintf ff "@,every ";
|
print_list
|
||||||
print_exp ff e;
|
(fun ff sh ->
|
||||||
fprintf ff "@]"
|
fprintf ff "@[<v 2>state %a:@ %a%a%a@]"
|
||||||
|
print_name sh.s_state
|
||||||
|
print_block sh.s_block
|
||||||
|
(print_escape_list "until") sh.s_until
|
||||||
|
(print_escape_list "unless") sh.s_unless)
|
||||||
|
"" "" "" ff tag_act_list
|
||||||
|
|
||||||
|
and print_escape_list unless ff esc_list = match esc_list with
|
||||||
|
| [] -> ()
|
||||||
|
| _ ->
|
||||||
|
fprintf ff "@,%s %a" unless
|
||||||
|
(print_list
|
||||||
|
(fun ff esc ->
|
||||||
|
let cont = if esc.e_reset then "then" else "continue" in
|
||||||
|
fprintf ff "@,| %a %s %a"
|
||||||
|
print_exp esc.e_cond cont print_name esc.e_next_state)
|
||||||
|
"" "" "") esc_list
|
||||||
|
|
||||||
|
and print_switch_handler_list ff tag_act_list =
|
||||||
|
print_list
|
||||||
|
(fun ff sh ->
|
||||||
|
fprintf ff "@[<v 2>| %a:@ %a@]"
|
||||||
|
print_qualname sh.w_name
|
||||||
|
print_block sh.w_block)
|
||||||
|
"" "" "" ff tag_act_list
|
||||||
|
|
||||||
|
and print_present_handler_list ff present_act_list =
|
||||||
|
print_list
|
||||||
|
(fun ff ph ->
|
||||||
|
fprintf ff "@[<v 2>| %a:@ %a@]"
|
||||||
|
print_exp ph.p_cond
|
||||||
|
print_block ph.p_block)
|
||||||
|
"" "" "" ff present_act_list
|
||||||
|
|
||||||
|
and print_default ff b =
|
||||||
|
match b.b_equs with
|
||||||
|
| [] -> ()
|
||||||
|
| _ -> fprintf ff "@[<v 2>default@,%a@]" print_block b
|
||||||
|
|
||||||
and print_eq_list ff = function
|
and print_eq_list ff = function
|
||||||
| [] -> ()
|
| [] -> ()
|
||||||
| [eq] -> print_eq ff eq;fprintf ff ";"
|
| l -> print_list_r print_eq """;""" ff l
|
||||||
| eq :: l -> print_eq ff eq;fprintf ff ";@,";print_eq_list ff l
|
|
||||||
|
|
||||||
and print_state_handler ff
|
|
||||||
{ s_state = s; s_block = b; s_until = until; s_unless = unless } =
|
|
||||||
fprintf ff " @[<v 2>state ";
|
|
||||||
fprintf ff "%a@," print_name s;
|
|
||||||
print_block ff b;
|
|
||||||
if until <> [] then
|
|
||||||
begin
|
|
||||||
fprintf ff "@,@[<v 2>until ";
|
|
||||||
print_list print_escape "" "" "" ff until;
|
|
||||||
fprintf ff "@]"
|
|
||||||
end;
|
|
||||||
if unless <> [] then
|
|
||||||
begin
|
|
||||||
fprintf ff "@,@[<v 2>unless ";
|
|
||||||
print_list_r print_escape "" " " "" ff unless;
|
|
||||||
fprintf ff "@]"
|
|
||||||
end;
|
|
||||||
fprintf ff "@]"
|
|
||||||
|
|
||||||
and print_switch_handler ff { w_name = tag; w_block = b } =
|
|
||||||
fprintf ff " @[<v 2>| ";
|
|
||||||
print_qualname ff tag;
|
|
||||||
fprintf ff "@,";
|
|
||||||
print_block ff b;
|
|
||||||
fprintf ff "@]"
|
|
||||||
|
|
||||||
and print_present_handler ff { p_cond = e; p_block = b } =
|
|
||||||
fprintf ff " @[<v 2>| ";
|
|
||||||
print_exp ff e;
|
|
||||||
fprintf ff "@,";
|
|
||||||
print_block ff b;
|
|
||||||
fprintf ff "@]"
|
|
||||||
|
|
||||||
and print_escape ff { e_cond = e; e_reset = r; e_next_state = ns} =
|
|
||||||
fprintf ff "@,| ";
|
|
||||||
print_exp ff e;
|
|
||||||
if r then fprintf ff " then " else fprintf ff " continue ";
|
|
||||||
print_name ff ns
|
|
||||||
|
|
||||||
and print_block ff { b_local = v_list; b_equs = eqs; b_defnames = defnames } =
|
and print_block ff { b_local = v_list; b_equs = eqs; b_defnames = defnames } =
|
||||||
if v_list <> [] then
|
fprintf ff "%a@[<v2>do@ %a@]" print_local_vars v_list print_eq_list eqs
|
||||||
begin
|
|
||||||
fprintf ff "@[<v 2>var ";
|
|
||||||
print_list_r print_vd "" ";" "" ff v_list;
|
|
||||||
fprintf ff "@]@,"
|
|
||||||
end;
|
|
||||||
(* (\* DEBUG *\) *)
|
|
||||||
(* fprintf ff "@[<hov 2>defines @,"; *)
|
|
||||||
(* Env.iter (fun n t -> fprintf ff "%s," n) defnames; *)
|
|
||||||
(* fprintf ff "@]@\n"; *)
|
|
||||||
(* (\* END DEBUG *\) *)
|
|
||||||
fprintf ff "@[<v 2>do@,";
|
|
||||||
print_eq_list ff eqs;
|
|
||||||
fprintf ff "@]"
|
|
||||||
|
|
||||||
let print_type_def ff { t_name = name; t_desc = tdesc } =
|
let rec print_type_def ff { t_name = name; t_desc = tdesc } =
|
||||||
match tdesc with
|
let print_type_desc ff = function
|
||||||
| Type_abs -> fprintf ff "@[type %a@.@]" print_qualname name
|
| Type_abs -> ()
|
||||||
| Type_alias ty ->
|
| Type_alias ty -> fprintf ff " =@ %a" print_type ty
|
||||||
fprintf ff "@[type %a@ = %a@.@]" print_qualname name print_type ty
|
| Type_enum tag_name_list ->
|
||||||
| Type_enum(tag_name_list) ->
|
fprintf ff " =@ %a" (print_list print_qualname """|""") tag_name_list
|
||||||
fprintf ff "@[<2>type %a = " print_qualname name;
|
| Type_struct f_ty_list ->
|
||||||
print_list_r print_qualname "" "| " "" ff tag_name_list;
|
fprintf ff " =@ %a" (print_record print_field) f_ty_list in
|
||||||
fprintf ff "@.@]"
|
fprintf ff "@[<2>type %a%a@]@." print_qualname name print_type_desc tdesc
|
||||||
| Type_struct(f_ty_list) ->
|
|
||||||
fprintf ff "@[type %a = " print_qualname name;
|
|
||||||
print_list_r
|
|
||||||
(fun ff { f_name = field; f_type = ty } ->
|
|
||||||
print_qualname ff field;
|
|
||||||
fprintf ff ": ";
|
|
||||||
print_type ff ty) "{" ";" "}" ff f_ty_list;
|
|
||||||
fprintf ff "@.@]"
|
|
||||||
|
|
||||||
let print_const_dec ff c =
|
let print_contract ff { c_block = b;
|
||||||
fprintf ff "@[const ";
|
c_assume = e_a; c_enforce = e_g; } =
|
||||||
print_qualname ff c.c_name;
|
fprintf ff "@[<v2>contract@\n%a@ assume %a;@ enforce %a@]"
|
||||||
fprintf ff " : ";
|
print_block b
|
||||||
print_type ff c.c_type;
|
|
||||||
fprintf ff " = ";
|
|
||||||
print_static_exp ff c.c_value;
|
|
||||||
fprintf ff "@.@]"
|
|
||||||
|
|
||||||
let print_contract ff {c_block = b;
|
|
||||||
c_assume = e_a;
|
|
||||||
c_enforce = e_g } =
|
|
||||||
if b.b_local <> [] then begin
|
|
||||||
fprintf ff "@[<v 2>contract@\n";
|
|
||||||
fprintf ff "@[<hov 4>var ";
|
|
||||||
print_list_r print_vd "" ";" "" ff b.b_local;
|
|
||||||
fprintf ff ";@]@\n"
|
|
||||||
end;
|
|
||||||
if b.b_equs <> [] then begin
|
|
||||||
fprintf ff "@[<v 2>let @,";
|
|
||||||
print_eq_list ff b.b_equs;
|
|
||||||
fprintf ff "@]"; fprintf ff "tel@\n"
|
|
||||||
end;
|
|
||||||
fprintf ff "assume %a@;enforce %a@;with (@[<hov>"
|
|
||||||
print_exp e_a
|
print_exp e_a
|
||||||
print_exp e_g;
|
print_exp e_g
|
||||||
fprintf ff "@])@]@."
|
|
||||||
|
|
||||||
let print_node_params ff = function
|
|
||||||
| [] -> ()
|
|
||||||
| l -> print_list_r print_param "<<" "," ">>" ff l
|
|
||||||
|
|
||||||
let print_node ff
|
let print_node ff
|
||||||
{ n_name = n; n_input = ni;
|
{ n_name = n; n_input = ni;
|
||||||
n_block = nb; n_output = no; n_contract = contract;
|
n_block = nb; n_output = no; n_contract = contract;
|
||||||
n_params = params; } =
|
n_params = params } =
|
||||||
fprintf ff "@[<v 2>node ";
|
fprintf ff "@[node %a%a%a@ returns %a@]@\n%a%a@[<v2>let@ %a@]@\ntel@]@\n@."
|
||||||
print_qualname ff n;
|
print_qualname n
|
||||||
fprintf ff "@[%a@]" print_node_params params;
|
print_node_params params
|
||||||
fprintf ff "@[%a@]" (print_list_r print_vd "(" ";" ")") ni;
|
print_vd_tuple ni
|
||||||
fprintf ff " returns ";
|
print_vd_tuple no
|
||||||
fprintf ff "@[%a@]" (print_list_r print_vd "(" ";" ")") no;
|
(print_opt print_contract) contract
|
||||||
fprintf ff "@,";
|
print_local_vars nb.b_local
|
||||||
optunit (print_contract ff) contract;
|
print_eq_list nb.b_equs
|
||||||
if nb.b_local <> [] then begin
|
|
||||||
fprintf ff "@[<hov 4>var ";
|
|
||||||
print_list_r print_vd "" ";" "" ff nb.b_local;
|
|
||||||
fprintf ff ";@]@,"
|
|
||||||
end;
|
|
||||||
fprintf ff "@[<v 2>let @,";
|
|
||||||
print_eq_list ff nb.b_equs;
|
|
||||||
fprintf ff "@]@;"; fprintf ff "tel";fprintf ff "@.@]"
|
|
||||||
|
|
||||||
let print_open_module ff name =
|
let print_open_module ff name = fprintf ff "open %a@." print_name name
|
||||||
fprintf ff "@[open ";
|
|
||||||
print_name ff name;
|
|
||||||
fprintf ff "@.@]"
|
|
||||||
|
|
||||||
let print oc { p_opened = po; p_types = pt; p_nodes = pn; p_consts = pc } =
|
let print oc { p_opened = po; p_types = pt; p_nodes = pn; p_consts = pc } =
|
||||||
let ff = Format.formatter_of_out_channel oc in
|
let ff = Format.formatter_of_out_channel oc in
|
||||||
|
|
|
||||||
Loading…
Reference in a new issue