2010-09-13 13:32:35 +02:00
|
|
|
open Misc
|
2010-06-16 19:31:51 +02:00
|
|
|
open Names
|
2010-07-23 19:45:19 +02:00
|
|
|
open Idents
|
2010-06-16 19:31:51 +02:00
|
|
|
open Types
|
2010-07-23 22:06:06 +02:00
|
|
|
open Clocks
|
2010-06-16 19:31:51 +02:00
|
|
|
open Static
|
|
|
|
open Format
|
2010-06-17 16:09:32 +02:00
|
|
|
open Signature
|
2010-09-09 00:35:06 +02:00
|
|
|
open Global_printer
|
2010-06-16 19:31:51 +02:00
|
|
|
open Pp_tools
|
2010-07-13 14:03:39 +02:00
|
|
|
open Minils
|
2010-06-16 19:31:51 +02:00
|
|
|
|
2010-06-21 18:19:58 +02:00
|
|
|
(** Every print_ function is boxed, that is it doesn't export break points,
|
2010-08-24 17:13:28 +02:00
|
|
|
Exceptions are [list] class functions *)
|
2010-06-19 18:28:52 +02:00
|
|
|
|
2010-08-24 17:13:28 +02:00
|
|
|
(** Every print_ function is without heading carry return or white space *)
|
2010-06-16 19:31:51 +02:00
|
|
|
|
2010-06-26 16:53:25 +02:00
|
|
|
let iterator_to_string i =
|
|
|
|
match i with
|
2010-06-17 16:09:32 +02:00
|
|
|
| Imap -> "map"
|
|
|
|
| Ifold -> "fold"
|
2010-07-26 09:33:22 +02:00
|
|
|
| Ifoldi -> "foldi"
|
2010-06-17 16:09:32 +02:00
|
|
|
| Imapfold -> "mapfold"
|
|
|
|
|
2010-06-16 19:31:51 +02:00
|
|
|
let rec print_pat ff = function
|
|
|
|
| Evarpat n -> print_ident ff n
|
|
|
|
| Etuplepat pat_list ->
|
2010-08-18 16:16:50 +02:00
|
|
|
fprintf ff "@[<2>(%a)@]" (print_list_r print_pat """,""") pat_list
|
2010-06-16 19:31:51 +02:00
|
|
|
|
|
|
|
let rec print_ck ff = function
|
|
|
|
| Cbase -> fprintf ff "base"
|
|
|
|
| Con (ck, c, n) ->
|
2010-09-09 00:35:06 +02:00
|
|
|
fprintf ff "%a on %a(%a)" print_ck ck print_qualname c print_ident n
|
2010-09-14 09:39:02 +02:00
|
|
|
| Cvar { contents = Cindex _ } -> fprintf ff "base"
|
2010-06-16 19:31:51 +02:00
|
|
|
| Cvar { contents = Clink ck } -> print_ck ff ck
|
|
|
|
|
|
|
|
let rec print_clock ff = function
|
|
|
|
| Ck ck -> print_ck ff ck
|
|
|
|
| Cprod ct_list ->
|
2010-08-18 16:16:50 +02:00
|
|
|
fprintf ff "@[<2>(%a)@]" (print_list_r print_clock """ *""") ct_list
|
2010-06-16 19:31:51 +02:00
|
|
|
|
2010-06-27 17:24:31 +02:00
|
|
|
let print_vd ff { v_ident = n; v_type = ty; v_clock = ck } =
|
2010-09-15 09:38:52 +02:00
|
|
|
if !Compiler_options.full_type_info then
|
2010-06-26 16:53:25 +02:00
|
|
|
fprintf ff "%a : %a :: %a" print_ident n print_type ty print_ck ck
|
2010-06-19 18:28:52 +02:00
|
|
|
else fprintf ff "%a : %a" print_ident n print_type ty
|
2010-06-26 16:53:25 +02:00
|
|
|
|
2010-06-19 18:28:52 +02:00
|
|
|
let print_local_vars ff = function
|
|
|
|
| [] -> ()
|
|
|
|
| l -> fprintf ff "@[<4>%a@]@\n" (print_list_r print_vd "var "";"";") l
|
2010-06-26 16:53:25 +02:00
|
|
|
|
2010-07-14 02:30:48 +02:00
|
|
|
let print_const_dec ff c =
|
2010-09-15 09:38:52 +02:00
|
|
|
if !Compiler_options.full_type_info then
|
2010-07-14 02:30:48 +02:00
|
|
|
fprintf ff "const %a : %a = %a"
|
2010-09-09 00:35:06 +02:00
|
|
|
print_qualname c.c_name print_type c.c_type print_static_exp c.c_value
|
2010-07-14 02:30:48 +02:00
|
|
|
else
|
|
|
|
fprintf ff "const %a = %a"
|
2010-09-09 00:35:06 +02:00
|
|
|
print_qualname c.c_name print_static_exp c.c_value;
|
2010-08-17 12:21:21 +02:00
|
|
|
fprintf ff "@."
|
2010-07-14 02:30:48 +02:00
|
|
|
|
|
|
|
|
2010-06-19 18:28:52 +02:00
|
|
|
let rec print_params ff l =
|
2010-06-30 17:20:56 +02:00
|
|
|
fprintf ff "@[<2>%a@]" (print_list_r print_static_exp "<<"","">>") l
|
2010-06-17 16:09:32 +02:00
|
|
|
|
2010-06-19 18:28:52 +02:00
|
|
|
and print_node_params ff l =
|
|
|
|
fprintf ff "@[<2>%a@]" (print_list_r print_param "<<"","">>") l
|
2010-06-26 16:53:25 +02:00
|
|
|
|
2010-06-21 01:45:23 +02:00
|
|
|
and print_exp_tuple ff l =
|
2010-08-18 16:16:50 +02:00
|
|
|
fprintf ff "@[<2>(%a)@]" (print_list_r print_exp """,""") l
|
2010-06-16 19:31:51 +02:00
|
|
|
|
2010-06-21 01:45:23 +02:00
|
|
|
and print_vd_tuple ff l =
|
2010-07-27 13:31:13 +02:00
|
|
|
fprintf ff "@[<2>%a@]" (print_list_r print_vd "("";"")") l
|
2010-06-17 16:09:32 +02:00
|
|
|
|
2010-06-19 18:28:52 +02:00
|
|
|
and print_index ff idx =
|
2010-06-30 17:20:56 +02:00
|
|
|
fprintf ff "@[<2>%a@]" (print_list print_static_exp "[""][""]") idx
|
2010-06-16 19:31:51 +02:00
|
|
|
|
2010-06-19 18:28:52 +02:00
|
|
|
and print_dyn_index ff idx =
|
|
|
|
fprintf ff "@[<2>%a@]" (print_list print_exp "[""][""]") idx
|
2010-06-26 16:53:25 +02:00
|
|
|
|
2010-06-16 19:31:51 +02:00
|
|
|
and print_exp ff e =
|
2010-09-15 09:38:52 +02:00
|
|
|
if !Compiler_options.full_type_info then
|
2010-07-27 13:31:13 +02:00
|
|
|
fprintf ff "(%a : %a :: %a)"
|
|
|
|
print_exp_desc e.e_desc print_type e.e_ty print_ck e.e_ck
|
2010-06-17 16:09:32 +02:00
|
|
|
else fprintf ff "%a" print_exp_desc e.e_desc
|
2010-06-19 18:28:52 +02:00
|
|
|
|
2010-06-17 16:09:32 +02:00
|
|
|
and print_every ff reset =
|
2010-06-26 16:53:25 +02:00
|
|
|
print_opt (fun ff id -> fprintf ff " every %a" print_ident id) ff reset
|
2010-06-17 16:09:32 +02:00
|
|
|
|
|
|
|
and print_exp_desc ff = function
|
2010-07-13 14:03:39 +02:00
|
|
|
| Econst c -> print_static_exp ff c
|
2010-07-14 02:30:48 +02:00
|
|
|
| Evar x -> print_ident ff x
|
2010-07-13 14:03:39 +02:00
|
|
|
| Efby ((Some c), e) ->
|
|
|
|
fprintf ff "@[<2>%a fby@ %a@]" print_static_exp c print_exp e
|
2010-06-19 18:28:52 +02:00
|
|
|
| Efby (None, e) -> fprintf ff "pre %a" print_exp e
|
2010-07-13 14:03:39 +02:00
|
|
|
| Eapp (app, args, reset) ->
|
2010-07-14 02:30:48 +02:00
|
|
|
fprintf ff "@[<2>%a@,%a@]"
|
|
|
|
print_app (app, args) print_every reset
|
2010-06-17 16:09:32 +02:00
|
|
|
| Ewhen (e, c, n) ->
|
2010-06-19 18:28:52 +02:00
|
|
|
fprintf ff "@[<2>(%a@ when %a(%a))@]"
|
2010-09-09 00:35:06 +02:00
|
|
|
print_exp e print_qualname c print_ident n
|
2010-06-17 16:09:32 +02:00
|
|
|
| Emerge (x, tag_e_list) ->
|
2010-06-19 18:28:52 +02:00
|
|
|
fprintf ff "@[<2>merge %a@ %a@]"
|
2010-06-17 16:09:32 +02:00
|
|
|
print_ident x print_tag_e_list tag_e_list
|
|
|
|
| Estruct f_e_list ->
|
2010-09-09 00:35:06 +02:00
|
|
|
print_record (print_couple print_qualname print_exp """ = """) ff f_e_list
|
2010-07-14 02:30:48 +02:00
|
|
|
| Eiterator (it, f, param, args, reset) ->
|
2010-06-26 16:53:25 +02:00
|
|
|
fprintf ff "@[<2>(%s (%a)<<%a>>)@,%a@]%a"
|
|
|
|
(iterator_to_string it)
|
2010-07-13 14:03:39 +02:00
|
|
|
print_app (f, [])
|
2010-07-14 02:30:48 +02:00
|
|
|
print_static_exp param
|
|
|
|
print_exp_tuple args
|
|
|
|
print_every reset
|
|
|
|
|
2010-09-13 13:32:35 +02:00
|
|
|
and print_app ff (app, args) = match app.a_op with
|
|
|
|
| Eequal ->
|
|
|
|
let e1, e2 = assert_2 args in
|
2010-07-27 17:16:35 +02:00
|
|
|
fprintf ff "@[<2>%a@ = %a@]" print_exp e1 print_exp e2
|
2010-09-13 13:32:35 +02:00
|
|
|
| Etuple -> print_exp_tuple ff args
|
|
|
|
| Efun f | Enode f ->
|
2010-07-14 02:30:48 +02:00
|
|
|
fprintf ff "@[%a@,%a@,%a@]"
|
2010-09-13 13:32:35 +02:00
|
|
|
print_qualname f print_params app.a_params print_exp_tuple args
|
|
|
|
| Eifthenelse ->
|
|
|
|
let e1, e2, e3 = assert_3 args in
|
2010-07-14 02:30:48 +02:00
|
|
|
fprintf ff "@[<hv>if %a@ then %a@ else %a@]"
|
|
|
|
print_exp e1 print_exp e2 print_exp e3
|
2010-09-13 13:32:35 +02:00
|
|
|
| Efield ->
|
|
|
|
let r = assert_1 args in
|
|
|
|
let f = assert_1 app.a_params in
|
|
|
|
fprintf ff "%a.%a" print_exp r print_static_exp f
|
|
|
|
| Efield_update ->
|
|
|
|
let r,e = assert_2 args in
|
|
|
|
let f = assert_1 app.a_params in
|
2010-07-14 02:30:48 +02:00
|
|
|
fprintf ff "@[<2>{%a with .%a =@ %a}@]"
|
|
|
|
print_exp r print_static_exp f print_exp e
|
2010-09-13 13:32:35 +02:00
|
|
|
| Earray -> fprintf ff "@[<2>%a@]" (print_list_r print_exp "["";""]") args
|
|
|
|
| Earray_fill ->
|
|
|
|
let e = assert_1 args in
|
|
|
|
let n = assert_1 app.a_params in
|
|
|
|
fprintf ff "%a^%a" print_exp e print_static_exp n
|
|
|
|
| Eselect ->
|
|
|
|
let e = assert_1 args in
|
|
|
|
fprintf ff "%a%a" print_exp e print_index app.a_params
|
|
|
|
| Eselect_slice ->
|
|
|
|
let e = assert_1 args in
|
|
|
|
let idx1, idx2 = assert_2 app.a_params in
|
2010-07-14 02:30:48 +02:00
|
|
|
fprintf ff "%a[%a..%a]"
|
|
|
|
print_exp e print_static_exp idx1 print_static_exp idx2
|
2010-09-13 13:32:35 +02:00
|
|
|
| Eselect_dyn ->
|
|
|
|
let r, d, e = assert_2min args in
|
2010-07-14 02:30:48 +02:00
|
|
|
fprintf ff "%a%a default %a"
|
|
|
|
print_exp r print_dyn_index e print_exp d
|
2010-09-13 13:32:35 +02:00
|
|
|
| Eupdate ->
|
|
|
|
let e1, e2, idx = assert_2min args in
|
2010-07-13 14:03:39 +02:00
|
|
|
fprintf ff "@[<2>(%a with %a =@ %a)@]"
|
2010-07-28 12:34:07 +02:00
|
|
|
print_exp e1 print_dyn_index idx print_exp e2
|
2010-09-13 13:32:35 +02:00
|
|
|
| Econcat ->
|
|
|
|
let e1, e2 = assert_2 args in
|
2010-07-14 02:30:48 +02:00
|
|
|
fprintf ff "@[<2>%a@ @@ %a@]" print_exp e1 print_exp e2
|
2010-07-13 14:03:39 +02:00
|
|
|
|
2010-06-29 19:04:40 +02:00
|
|
|
and print_handler ff c =
|
2010-09-09 00:35:06 +02:00
|
|
|
fprintf ff "@[<2>%a@]" (print_couple print_qualname print_exp "("" -> "")") c
|
2010-06-29 19:04:40 +02:00
|
|
|
|
2010-06-16 19:31:51 +02:00
|
|
|
and print_tag_e_list ff tag_e_list =
|
2010-08-18 16:16:50 +02:00
|
|
|
fprintf ff "@[%a@]" (print_list print_handler """""") tag_e_list
|
2010-06-17 16:09:32 +02:00
|
|
|
|
|
|
|
|
2010-07-21 16:00:06 +02:00
|
|
|
and print_eq ff { eq_lhs = p; eq_rhs = e } =
|
2010-09-15 09:38:52 +02:00
|
|
|
if !Compiler_options.full_type_info
|
2010-06-19 18:28:52 +02:00
|
|
|
then fprintf ff "@[<2>%a :: %a =@ %a@]"
|
2010-06-26 16:53:25 +02:00
|
|
|
print_pat p print_ck e.e_ck print_exp e
|
2010-06-21 01:45:23 +02:00
|
|
|
else fprintf ff "@[<2>%a =@ %a@]" print_pat p print_exp e
|
2010-06-17 16:09:32 +02:00
|
|
|
|
2010-06-16 19:31:51 +02:00
|
|
|
|
2010-07-21 16:00:06 +02:00
|
|
|
and print_eqs ff = function
|
2010-06-19 18:28:52 +02:00
|
|
|
| [] -> ()
|
|
|
|
| l -> fprintf ff "@[<v2>let@ %a@]@\ntel" (print_list_r print_eq """;""") l
|
2010-06-17 16:09:32 +02:00
|
|
|
|
2010-06-19 18:28:52 +02:00
|
|
|
let print_open_module ff name = fprintf ff "open %a@." print_name name
|
2010-06-16 19:31:51 +02:00
|
|
|
|
2010-07-14 02:30:48 +02:00
|
|
|
let rec print_type_dec ff { t_name = name; t_desc = tdesc } =
|
2010-08-24 17:13:28 +02:00
|
|
|
let print_type_desc ff = function
|
|
|
|
| Type_abs -> ()
|
|
|
|
| Type_alias ty -> fprintf ff " =@ %a" print_type ty
|
|
|
|
| Type_enum tag_name_list ->
|
2010-09-09 00:35:06 +02:00
|
|
|
fprintf ff " =@ %a" (print_list print_qualname """|""") tag_name_list
|
2010-08-24 17:13:28 +02:00
|
|
|
| Type_struct f_ty_list ->
|
|
|
|
fprintf ff " =@ %a" (print_record print_field) f_ty_list in
|
2010-09-09 00:35:06 +02:00
|
|
|
fprintf ff "@[<2>type %a%a@]@." print_qualname name print_type_desc tdesc
|
2010-06-26 16:53:25 +02:00
|
|
|
|
2010-06-16 19:31:51 +02:00
|
|
|
|
2010-08-18 16:16:50 +02:00
|
|
|
let print_contract ff { c_local = l; c_eq = eqs;
|
2010-12-06 18:13:15 +01:00
|
|
|
c_assume = e_a; c_enforce = e_g;
|
|
|
|
c_controllables = c;} =
|
|
|
|
fprintf ff "@[<v2>contract@\n%a%a@ assume %a@ enforce %a@ with (%a)@]"
|
2010-06-26 16:53:25 +02:00
|
|
|
print_local_vars l
|
|
|
|
print_eqs eqs
|
|
|
|
print_exp e_a
|
|
|
|
print_exp e_g
|
2010-12-06 18:13:15 +01:00
|
|
|
print_vd_tuple c
|
2010-06-26 16:53:25 +02:00
|
|
|
|
|
|
|
|
2010-08-18 16:16:50 +02:00
|
|
|
let print_node ff { n_name = n; n_input = ni; n_output = no;
|
|
|
|
n_contract = contract; n_local = nl;
|
|
|
|
n_equs = ne; n_params = params } =
|
2010-09-09 00:35:06 +02:00
|
|
|
fprintf ff "@[node %a%a%a@ returns %a@]@\n%a%a%a@]@\n@."
|
|
|
|
print_qualname n
|
2010-06-17 16:09:32 +02:00
|
|
|
print_node_params params
|
2010-06-21 01:45:23 +02:00
|
|
|
print_vd_tuple ni
|
|
|
|
print_vd_tuple no
|
2010-06-17 16:09:32 +02:00
|
|
|
(print_opt print_contract) contract
|
2010-06-19 18:28:52 +02:00
|
|
|
print_local_vars nl
|
2010-06-17 16:09:32 +02:00
|
|
|
print_eqs ne
|
|
|
|
|
2010-06-16 19:31:51 +02:00
|
|
|
|
2010-06-22 13:47:00 +02:00
|
|
|
let print oc { p_opened = pm; p_types = pt; p_nodes = pn; p_consts = pc } =
|
2010-09-09 00:35:06 +02:00
|
|
|
let ff = formatter_of_out_channel oc in
|
2010-08-29 22:30:51 +02:00
|
|
|
List.iter (print_open_module ff) pm;
|
|
|
|
List.iter (print_const_dec ff) pc;
|
|
|
|
List.iter (print_type_dec ff) pt;
|
|
|
|
List.iter (print_node ff) pn;
|
2010-09-09 00:35:06 +02:00
|
|
|
fprintf ff "@?"
|