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

Print stateful in heptagon. 

Conflicts:

	compiler/heptagon/hept_printer.ml
This commit is contained in:
Léonard Gérard 2011-11-02 13:14:07 +01:00
parent 5593ffdc91
commit 33021aaa90
3 changed files with 16 additions and 7 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

19
compiler/heptagon/hept_printer.ml
View File

@ -104,6 +104,9 @@ and print_trunc_index ff idx =
and print_exps ff e_list =
print_list_r print_exp "(" "," ")" ff e_list
and print_stateful ff s =
if !Compiler_options.stateful_info && s then fprintf ff "$"
and print_exp ff e =
if !Compiler_options.full_type_info then
fprintf ff "(%a : %a%a%a)"
@ -171,7 +174,11 @@ and print_app ff (app, args) =
| Efun { name = n } when (n = "*" or n = "*.") ->
let a1, a2 = assert_2 args in
fprintf ff "@[%a@, %s@, %a@]" print_exp a1 n print_exp a2
| Efun f | Enode f ->
| Efun f ->
fprintf ff "@[%a@,%a@,%a@]"
print_qualname f print_params app.a_params print_exp_tuple args
| Enode f ->
print_stateful ff true;
fprintf ff "@[%a@,%a@,%a@]"
print_qualname f print_params app.a_params print_exp_tuple args
| Eifthenelse ->
@ -220,6 +227,7 @@ and print_app ff (app, args) =
fprintf ff "@[split@,%a@]" print_exp_tuple args
let rec print_eq ff eq =
print_stateful ff eq.eq_stateful;
match eq.eq_desc with
| Eeq(p, e) ->
fprintf ff "@[<2>%a =@ %a@]" print_pat_init (p, eq.eq_inits) print_exp e
@ -286,12 +294,9 @@ and print_eq_list ff = function
| [] -> ()
| l -> print_list_r print_eq """;""" ff l
and print_block sep ff { b_local = v_list; b_equs = eqs } =
match v_list with
| [] ->
fprintf ff "@[<v>%s@,%a@]" sep print_eq_list eqs
| _ ->
fprintf ff "@[<v>%a@,%a@]" (print_local_vars sep) v_list print_eq_list eqs
and print_block sep ff { b_local = v_list; b_equs = eqs; b_stateful = s } =
fprintf ff "%a@[<v>%a%a@]" print_stateful s (print_local_vars sep) v_list print_eq_list eqs
and print_sblock sep ff { b_local = v_list; b_equs = eqs } =
match v_list with

1
compiler/main/heptc.ml
View File

@ -121,6 +121,7 @@ let main () =
"-nocaus", Arg.Clear causality, doc_nocaus;
"-noinit", Arg.Clear init, doc_noinit;
"-fti", Arg.Set full_type_info, doc_full_type_info;
"-statefuli", Arg.Set stateful_info, doc_stateful_info;
"-fname", Arg.Set full_name, doc_full_name;
"-itfusion", Arg.Set do_iterator_fusion, doc_itfusion;
"-memalloc", Arg.Unit do_mem_alloc_and_typing, doc_memalloc;

3
compiler/utilities/global/compiler_options.ml
View File

@ -77,6 +77,8 @@ let set_target_path path =
let full_type_info = ref false
let stateful_info = ref false
let full_name = ref false
let causality = ref true
@ -127,6 +129,7 @@ and doc_target =
"<lang>\tGenerate code in language <lang>\n\t\t\t(with <lang>=c,"
^ " java or z3z)"
and doc_full_type_info = "\t\t\tPrint full type information"
and doc_stateful_info = "\t\t\tPrint stateful information"
and doc_full_name = "\t\tPrint full variable name information"
and doc_target_path =
"<path>\tGenerated files will be placed in <path>\n\t\t\t(the directory is"