diff --git a/compiler/heptagon/hept_printer.ml b/compiler/heptagon/hept_printer.ml index 6688901..c97fe73 100644 --- a/compiler/heptagon/hept_printer.ml +++ b/compiler/heptagon/hept_printer.ml @@ -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 "@[%s@,%a@]" sep print_eq_list eqs - | _ -> - fprintf ff "@[%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@[%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 diff --git a/compiler/main/heptc.ml b/compiler/main/heptc.ml index 5032857..6a31363 100644 --- a/compiler/main/heptc.ml +++ b/compiler/main/heptc.ml @@ -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; diff --git a/compiler/utilities/global/compiler_options.ml b/compiler/utilities/global/compiler_options.ml index 686afaf..c6ad7ff 100644 --- a/compiler/utilities/global/compiler_options.ml +++ b/compiler/utilities/global/compiler_options.ml @@ -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 = "\tGenerate code in language \n\t\t\t(with =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 = "\tGenerated files will be placed in \n\t\t\t(the directory is"