diff --git a/global/static.ml b/global/static.ml index 8366eb1..622d46f 100644 --- a/global/static.ml +++ b/global/static.ml @@ -130,7 +130,7 @@ let rec print_size_exp ff = | SConst i -> fprintf ff "%d" i | SVar id -> fprintf ff "%s" id | SOp (op, e1, e2) -> - fprintf ff "@[(%a %s %a@]" + fprintf ff "@[(%a %s %a)@]" print_size_exp e1 (op_to_string op) print_size_exp e2 let print_size_constr ff = function diff --git a/global/types.ml b/global/types.ml index fcceceb..4bf999e 100644 --- a/global/types.ml +++ b/global/types.ml @@ -16,7 +16,7 @@ let invalid_type = Tprod [] let const_array_of ty n = Tarray (ty, SConst n) - + open Pp_tools open Format diff --git a/heptagon/printer.ml b/heptagon/printer.ml index aa68564..bc999d9 100644 --- a/heptagon/printer.ml +++ b/heptagon/printer.ml @@ -6,9 +6,7 @@ (* Organization : Demons, LRI, University of Paris-Sud, Orsay *) (* *) (**************************************************************************) -(* the printer *) - -(* $Id$ *) +(* The Heptagon printer *) open Location open Misc @@ -329,11 +327,11 @@ let print_node ff n_local = nl; n_output = no; n_contract = contract; n_equs = ne; n_params = params; } = fprintf ff "@[node "; - print_name ff n; - print_node_params ff params; - print_list_r print_vd "(" ";" ")" ff ni; + print_name ff n; + fprintf ff "@[%a@]" print_node_params params; + fprintf ff "@[%a@]" (print_list_r print_vd "(" ";" ")") ni; fprintf ff " returns "; - print_list_r print_vd "(" ";" ")" ff no; + fprintf ff "@[%a@]" (print_list_r print_vd "(" ";" ")") no; fprintf ff "@,"; optunit (print_contract ff) contract; if nl <> [] then begin diff --git a/minils/minils_printer.ml b/minils/minils_printer.ml index 800f058..8b90a86 100644 --- a/minils/minils_printer.ml +++ b/minils/minils_printer.ml @@ -7,6 +7,13 @@ open Format open Signature open Pp_tools +(* Every print_ function is boxed, that is it doesn't export break points, + Exceptions are print_list* print_type_desc *) + +(* Every print_ function is without heading white space, + except for print_type_desc *) + +(* Every print_ function is without heading carry return *) let iterator_to_string i = match i with @@ -14,11 +21,10 @@ let iterator_to_string i = | Ifold -> "fold" | Imapfold -> "mapfold" - let rec print_pat ff = function | Evarpat n -> print_ident ff n | Etuplepat pat_list -> - fprintf ff "@[%a@]" (print_list_r print_pat "("","")") pat_list + fprintf ff "@[<2>%a@]" (print_list_r print_pat "("","")") pat_list let rec print_ck ff = function | Cbase -> fprintf ff "base" @@ -30,38 +36,49 @@ let rec print_ck ff = function let rec print_clock ff = function | Ck ck -> print_ck ff ck | Cprod ct_list -> - fprintf ff "@[%a@]" (print_list_r print_clock "("" *"")") ct_list + fprintf ff "@[<2>%a@]" (print_list_r print_clock "("" *"")") ct_list let print_vd ff { v_name = n; v_type = ty; v_clock = ck } = - fprintf ff "@[%a : %a :: %a@]" print_ident n print_type ty print_ck ck + if !Misc.full_type_info then + fprintf ff "%a : %a :: %a" print_ident n print_type ty print_ck ck + else fprintf ff "%a : %a" print_ident n print_type ty + +let print_local_vars ff = function + | [] -> () + | l -> fprintf ff "@[<4>%a@]@\n" (print_list_r print_vd "var "";"";") l let rec print_c ff = function | Cint i -> fprintf ff "%d" i | Cfloat f -> fprintf ff "%f" f | Cconstr tag -> print_longname ff tag - | Carray (n, c) -> fprintf ff "@[%a^%a@]" print_c c print_size_exp n + | Carray (n, c) -> fprintf ff "%a^%a" print_c c print_size_exp n -let print_params ff l = print_list_l print_size_exp "<<"","">>" ff l +let rec print_params ff l = + fprintf ff "@[<2>%a@]" (print_list_r print_size_exp "<<"","">>") l -let print_node_params ff l = print_list_l print_param "<<"","">>" ff l +and print_node_params ff l = + fprintf ff "@[<2>%a@]" (print_list_r print_param "<<"","">>") l + +and print_args ff l = + fprintf ff "@[<2>%a@]" (print_list_r print_exp "("","")") l -let print_node_args ff l = print_list_l print_vd "("","")" ff l +and print_node_args ff l = + fprintf ff "@[<2>%a@]" (print_list_r print_vd "("","")") l -let print_index ff idx = print_list print_size_exp "[""][""]" ff idx - -let rec print_dyn_index ff idx = print_list print_exp "[""][""]" ff idx - -and print_args ff e_list = - fprintf ff "@[%a@]" (print_list_r print_exp "("","")") e_list +and print_index ff idx = + fprintf ff "@[<2>%a@]" (print_list print_size_exp "[""][""]") idx +and print_dyn_index ff idx = + fprintf ff "@[<2>%a@]" (print_list print_exp "[""][""]") idx + and print_op ff op = - fprintf ff "%a %a" print_longname op.op_name print_params op.op_params + fprintf ff "%a%a" print_longname op.op_name print_params op.op_params and print_exp ff e = if !Misc.full_type_info then - fprintf ff "@[(%a@ : %a)@]" print_exp_desc e.e_desc print_type e.e_ty + fprintf ff "%a : %a" print_exp_desc e.e_desc print_type e.e_ty else fprintf ff "%a" print_exp_desc e.e_desc - + and print_every ff reset = print_opt (fun ff id -> fprintf ff " every %a" print_ident id) ff reset @@ -69,50 +86,49 @@ and print_exp_desc ff = function | Evar x -> print_ident ff x | Econstvar x -> print_name ff x | Econst c -> print_c ff c - | Efby ((Some c), e) -> - (print_c ff c; fprintf ff " fby "; print_exp ff e) - | Efby (None, e) -> (fprintf ff "pre "; print_exp ff e) + | Efby ((Some c), e) -> fprintf ff "@[<2>%a fby@ %a@]" print_c c print_exp e + | Efby (None, e) -> fprintf ff "pre %a" print_exp e | Ecall (op, args, reset) -> - fprintf ff "%a %a%a" + fprintf ff "@[<2>%a@,%a%a@]" print_op op print_args args print_every reset | Ewhen (e, c, n) -> - fprintf ff "@[(%a when %a(%a))@]" + fprintf ff "@[<2>(%a@ when %a(%a))@]" print_exp e print_longname c print_ident n | Eifthenelse (e1, e2, e3) -> fprintf ff "@[if %a@ then %a@ else %a@]" print_exp e1 print_exp e2 print_exp e3 | Emerge (x, tag_e_list) -> - fprintf ff "@[merge %a@ @[%a@]@]" + fprintf ff "@[<2>merge %a@ %a@]" print_ident x print_tag_e_list tag_e_list | Etuple e_list -> - fprintf ff "@[%a@]" (print_list_r print_exp "("","")") e_list + fprintf ff "@[<2>%a@]" (print_list_r print_exp "("","")") e_list | Efield (e, field) -> fprintf ff "%a.%a" print_exp e print_longname field | Estruct f_e_list -> print_record (print_couple print_longname print_exp """ =""") ff f_e_list | Earray e_list -> - fprintf ff "@[%a@]" (print_list_r print_exp "["";""]") e_list - | Earray_op(array_op) -> - print_array_op ff array_op + fprintf ff "@[<2>%a@]" (print_list_r print_exp "["";""]") e_list + | Earray_op(array_op) -> print_array_op ff array_op | Efield_update (f, e1, e2) -> - fprintf ff "@[%a@ with .%a =@ %a@]" + fprintf ff "@[<2>(%a with .%a =@ %a)@]" print_exp e1 print_longname f print_exp e2 and print_array_op ff = function - | Erepeat (n, e) -> (print_exp ff e; fprintf ff "^"; print_size_exp ff n) - | Eselect (idx, e) -> fprintf ff "@[%a%a@]" print_exp e print_index idx + | Erepeat (n, e) -> fprintf ff "%a^%a" print_exp e print_size_exp n + | Eselect (idx, e) -> fprintf ff "%a%a" print_exp e print_index idx | Eselect_dyn (idx, _, e1, e2) -> - fprintf ff "@[%a%a default %a@]" + fprintf ff "%a%a default %a" print_exp e1 print_dyn_index idx print_exp e2 | Eupdate (idx, e1, e2) -> - fprintf ff "@[%a with %a = %a@]" print_exp e1 print_index idx print_exp e2 + fprintf ff "@[<2>(%a with %a =@ %a)@]" + print_exp e1 print_index idx print_exp e2 | Eselect_slice (idx1, idx2, e) -> - fprintf ff "@[%a[%a..%a]@]" + fprintf ff "%a[%a..%a]" print_exp e print_size_exp idx1 print_size_exp idx2 - | Econcat (e1, e2) -> fprintf ff "%a @@ %a" print_exp e1 print_exp e2 + | Econcat (e1, e2) -> fprintf ff "@[<2>%a@ @@ %a@]" print_exp e1 print_exp e2 | Eiterator (it, f, n, e_list, r) -> - fprintf ff "(%s (%a)<<%a>>)@ @[%a@]%a" + fprintf ff "@[<2>(%s (%a)<<%a>>)@ @[<2>%a@]@]%a" (iterator_to_string it) print_op f print_size_exp n @@ -127,63 +143,54 @@ and print_tag_e_list ff tag_e_list = let print_eq ff { eq_lhs = p; eq_rhs = e } = if !Misc.full_type_info - then fprintf ff "@[%a :: %a =@ %a;@]" + then fprintf ff "@[<2>%a :: %a =@ %a@]" print_pat p print_ck e.e_ck print_exp e - else fprintf ff "@[%a =@ %a;@]" print_pat p print_exp e + else fprintf ff "@[<2>%a =@ %a@]" print_pat p print_exp e -let print_eqs ff l = - fprintf ff "@\n@[let@ %a@]@ tel" (print_list print_eq """""") l +let print_eqs ff = function + | [] -> () + | l -> fprintf ff "@[let@ %a@]@\ntel" (print_list_r print_eq """;""") l -let print_open_module ff name = fprintf ff "@[open %a@]@." print_name name +let print_open_module ff name = fprintf ff "open %a@." print_name name let rec print_type_def ff { t_name = name; t_desc = tdesc } = - fprintf ff "@[type %s%a@]@." name print_type_desc tdesc - -and print_field ff field = - fprintf ff "%a:@ %a" print_name field.f_name print_type field.f_type + fprintf ff "@[<2>type %s%a@]@." name print_type_desc tdesc +(** Small exception to the rule, + adding a heading space itself when needed and exporting a break*) and print_type_desc ff = function - | Type_abs -> () + | Type_abs -> () (* that's the reason of the exception *) | Type_enum tag_name_list -> fprintf ff " =@ %a" (print_list print_name """|""") tag_name_list | Type_struct f_ty_list -> fprintf ff " =@ %a" (print_record print_field) f_ty_list +and print_field ff field = + fprintf ff "@[%a: %a@]" print_name field.f_name print_type field.f_type + let print_contract ff { c_local = l; c_eq = eqs; c_assume = e_a; c_enforce = e_g; c_controllables = cl } = - fprintf ff "@\n@["; - (if l <> [] - then - (fprintf ff "contract\n"; - fprintf ff "@[var "; - print_list_l print_vd """;""" ff l; - fprintf ff ";@]\n") - else (); - if eqs <> [] - then - (fprintf ff "@[let @,"; - print_eqs ff eqs; - fprintf ff "@]"; - fprintf ff "tel\n") - else (); - fprintf ff "assume@ %a@;enforce@ %a with (" print_exp e_a print_exp e_g; - print_list_l print_vd """;""" ff cl; - fprintf ff ")@]") - - + fprintf ff "@[contract@\n%a%a@ assume %a;@ enforce %a@ with %a@]" + print_local_vars l + print_eqs eqs + print_exp e_a + print_exp e_g + print_node_args cl + + 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 } = - fprintf ff "@[node %s%a%a@ returns %a%a@\n%a%a@]@." + fprintf ff "@[node %s%a%a@ returns %a@]@\n%a%a%a@]@\n@." n print_node_params params print_node_args ni print_node_args no (print_opt print_contract) contract - (print_list_l print_vd "var "";"";") nl + print_local_vars nl print_eqs ne diff --git a/utilities/pp_tools.ml b/utilities/pp_tools.ml index 0e7fc19..5bf0e68 100644 --- a/utilities/pp_tools.ml +++ b/utilities/pp_tools.ml @@ -15,27 +15,27 @@ open Format let rec print_list print lp sep rp ff = function | [] -> () | x::l -> - fprintf ff "@[%s%a" lp print x; - List.iter (fprintf ff "@]%s@,@[%a" sep print) l; - fprintf ff "%s@]" rp + fprintf ff "%s%a" lp print x; + List.iter (fprintf ff "%s@,%a" sep print) l; + fprintf ff "%s" rp (** print the list x1...xn : \@\[[lp][x1][sep] [x2]...[sep] [xn][rp]\]\@ and nothing if the list is empty *) let rec print_list_r print lp sep rp ff = function | [] -> () | x :: l -> - fprintf ff "@[%s%a" lp print x; - List.iter (fprintf ff "%s@]@ @[%a" sep print) l; - fprintf ff "%s@]" rp + fprintf ff "%s%a" lp print x; + List.iter (fprintf ff "%s@ %a" sep print) l; + fprintf ff "%s" rp (** print the list x1...xn : \@\[[lp][x1] [sep][x2]... [sep][xn][rp]\]\@ and nothing if the list is empty *) let rec print_list_l print lp sep rp ff = function | [] -> () | x :: l -> - fprintf ff "@[%s%a" lp print x; - List.iter (fprintf ff "@]@ @[%s%a" sep print) l; - fprintf ff "%s@]" rp + fprintf ff "%s%a" lp print x; + List.iter (fprintf ff "@ %s%a" sep print) l; + fprintf ff "%s" rp (* let rec print_list_rb print lp sep rp ff = function | [] -> ()