jeltz/heptagon
1
0
Fork 0
Code Issues Pull requests Releases Activity

Printing fixes, minils_printer seems ok.

Browse source
This commit is contained in:
Léonard Gérard 2010-06-19 18:28:52 +02:00
parent 29b4dea3b6
commit c549b150e8
5 changed files with 90 additions and 85 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

2
global/static.ml
View file

@ -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

2
global/types.ml
View file

@ -16,7 +16,7 @@ let invalid_type = Tprod []
let const_array_of ty n = Tarray (ty, SConst n)
open Pp_tools
open Format

12
heptagon/printer.ml
View file

@ -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 "@[<v 2>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

141
minils/minils_printer.ml
View file

@ -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 "@[<v>%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 "@[<hov2>(%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 "@[<hv>if %a@ then %a@ else %a@]"
print_exp e1 print_exp e2 print_exp e3
| Emerge (x, tag_e_list) ->
fprintf ff "@[<hov2>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 "@[<hov2>%a :: %a =@ %a;@]"
then fprintf ff "@[<2>%a :: %a =@ %a@]"
print_pat p print_ck e.e_ck print_exp e
else fprintf ff "@[<hov2>%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@[<hv2>let@ %a@]@ tel" (print_list print_eq """""") l
let print_eqs ff = function
| [] -> ()
| l -> fprintf ff "@[<v2>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@[<v2>";
(if l <> []
then
(fprintf ff "contract\n";
fprintf ff "@[<hov 4>var ";
print_list_l print_vd """;""" ff l;
fprintf ff ";@]\n")
else ();
if eqs <> []
then
(fprintf ff "@[<v 2>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 "@[<v2>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 "@[<hov2>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

18
utilities/pp_tools.ml
View file

@ -15,27 +15,27 @@ open Format
let rec print_list print lp sep rp ff = function
| [] -> ()
| x::l ->
fprintf ff "@[<hov2>%s%a" lp print x;
List.iter (fprintf ff "@]%s@,@[<hv2>%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 "@[<hov2>%s%a" lp print x;
List.iter (fprintf ff "%s@]@ @[<hv2>%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 "@[<hov2>%s%a" lp print x;
List.iter (fprintf ff "@]@ @[<hv2>%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
| [] -> ()