diff --git a/compiler/global/idents.ml b/compiler/global/idents.ml index 9fdddab..2f2686d 100644 --- a/compiler/global/idents.ml +++ b/compiler/global/idents.ml @@ -101,6 +101,7 @@ struct to variables defined in the source file have the same name unless there is a collision. *) let assign_name n = + let num = ref 1 in let fresh s = num := !num + 1; s ^ "_" ^ (string_of_int !num) in @@ -118,7 +119,8 @@ struct end let gen_fresh pass_name kind_to_string kind = - let s = "__" ^ pass_name ^ "_" ^ (kind_to_string kind) in + let s = kind_to_string kind in + let s = if !Compiler_options.full_name then "__"^pass_name ^ "_" ^ s else s in num := !num + 1; let id = { num = !num; source = s; is_generated = true } in UniqueNames.assign_name id; id diff --git a/compiler/global/modules.ml b/compiler/global/modules.ml index 26762d6..66f8437 100644 --- a/compiler/global/modules.ml +++ b/compiler/global/modules.ml @@ -226,33 +226,53 @@ let current_qual n = { qual = g_env.current_mod; name = n } (** { 3 Fresh functions return a fresh qualname for the current module } *) let rec fresh_value pass_name name = - let q = current_qual ("__"^ pass_name ^"_"^ name) in + let fname = + if !Compiler_options.full_name + then ("__"^ pass_name ^"_"^ name) + else name in + let q = current_qual fname in if QualEnv.mem q g_env.values - then fresh_value pass_name (name ^"_"^ Misc.gen_symbol()) + then fresh_value pass_name (name ^ Misc.gen_symbol()) else q let rec fresh_value_in pass_name name qualifier = - let q = { qual = qualifier; name = "__"^ pass_name ^"_"^ name } in + let fname = + if !Compiler_options.full_name + then ("__"^ pass_name ^"_"^ name) + else name in + let q = { qual = qualifier; name = fname } in if QualEnv.mem q g_env.values - then fresh_value_in pass_name (name ^"_"^ Misc.gen_symbol()) qualifier + then fresh_value_in pass_name (name ^ Misc.gen_symbol()) qualifier else q let rec fresh_type pass_name name = - let q = current_qual ("__"^ pass_name ^"_"^ name) in + let fname = + if !Compiler_options.full_name + then ("__"^ pass_name ^"_"^ name) + else name in + let q = current_qual fname in if QualEnv.mem q g_env.types - then fresh_type pass_name (name ^"_"^ Misc.gen_symbol()) + then fresh_type pass_name (name ^ Misc.gen_symbol()) else q let rec fresh_const pass_name name = - let q = current_qual ("__"^ pass_name ^"_"^ name) in + let fname = + if !Compiler_options.full_name + then ("__"^ pass_name ^"_"^ name) + else name in + let q = current_qual fname in if QualEnv.mem q g_env.consts - then fresh_const pass_name (name ^"_"^ Misc.gen_symbol()) + then fresh_const pass_name (name ^ Misc.gen_symbol()) else q let rec fresh_constr pass_name name = - let q = current_qual ("__"^ pass_name ^"_"^ name) in + let fname = + if !Compiler_options.full_name + then ("__"^ pass_name ^"_"^ name) + else name in + let q = current_qual fname in if QualEnv.mem q g_env.constrs - then fresh_constr pass_name (name ^"_"^ Misc.gen_symbol()) + then fresh_constr pass_name (name ^ Misc.gen_symbol()) else q diff --git a/compiler/heptagon/hept_printer.ml b/compiler/heptagon/hept_printer.ml index 1391eac..1af1988 100644 --- a/compiler/heptagon/hept_printer.ml +++ b/compiler/heptagon/hept_printer.ml @@ -49,9 +49,10 @@ and print_last_value ff = function | Last (Some v) -> fprintf ff " = %a" print_static_exp v | _ -> () -let print_local_vars ff = function +let print_local_vars s ff l = match l with | [] -> () - | l -> fprintf ff "@[<4>%a@]@\n" (print_list_r print_vd "var "";"";") l + | l -> + fprintf ff "@[<4>%a@]%s@\n" (print_list_r print_vd "var "";"";") l s let print_const_dec ff c = if !Compiler_options.full_type_info then @@ -193,16 +194,16 @@ let rec print_eq ff eq = print_default b | Ereset(b, e) -> fprintf ff "@[@[reset @ %a@]@,every %a@]" - (print_block "in") b print_exp e + print_block b print_exp e | Eblock b -> - fprintf ff "@[do@[@ @[%a@]@]@ done@]" (print_block "in") b + fprintf ff "@[do@[@ @[%a@]@]@ done@]" print_block b and print_state_handler_list ff tag_act_list = print_list (fun ff sh -> fprintf ff "@[state %a:@ %a%a%a@]" print_name sh.s_state - (print_block "do") sh.s_block + print_block sh.s_block (print_escape_list "until") sh.s_until (print_escape_list "unless") sh.s_unless) "" "" "" ff tag_act_list @@ -223,7 +224,7 @@ and print_switch_handler_list ff tag_act_list = (fun ff sh -> fprintf ff "@[| %a:@ %a@]" print_qualname sh.w_name - (print_block "do") sh.w_block) + print_block sh.w_block) "" "" "" ff tag_act_list and print_present_handler_list ff present_act_list = @@ -231,24 +232,22 @@ and print_present_handler_list ff present_act_list = (fun ff ph -> fprintf ff "@[| %a:@ %a@]" print_exp ph.p_cond - (print_block "do") ph.p_block) + print_block ph.p_block) "" "" "" ff present_act_list and print_default ff b = match b.b_equs with | [] -> () - | _ -> fprintf ff "@[default@,%a@]" (print_block "do") b + | _ -> fprintf ff "@[default@,%a@]" print_block b and print_eq_list ff = function | [] -> () | l -> print_list_r print_eq """;""" ff l -and print_block s ff { b_local = v_list; b_equs = eqs } = - fprintf ff "%a@[%s@ %a@]" print_local_vars v_list s print_eq_list eqs +and print_block ff { b_local = v_list; b_equs = eqs } = + fprintf ff "@[%a%a@]" (print_local_vars " in") v_list print_eq_list eqs -let print_inblock = print_block "in" - let rec print_type_def ff { t_name = name; t_desc = tdesc } = let print_type_desc ff = function @@ -264,7 +263,7 @@ let print_contract ff { c_block = b; c_assume = e_a; c_enforce = e_g; c_controllables = c} = fprintf ff "@[contract@\n%a@ assume %a@ enforce %a@ with (%a)@]" - (print_block "let") b + print_block b print_exp e_a print_exp e_g print_vd_tuple c @@ -279,7 +278,7 @@ let print_node ff print_vd_tuple ni print_vd_tuple no (print_opt print_contract) contract - print_local_vars nb.b_local + (print_local_vars "") nb.b_local print_eq_list nb.b_equs let print_open_module ff name = fprintf ff "open %a@." print_name name diff --git a/compiler/main/heptc.ml b/compiler/main/heptc.ml index a7a8878..c06bb92 100644 --- a/compiler/main/heptc.ml +++ b/compiler/main/heptc.ml @@ -93,6 +93,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; + "-fname", Arg.Set full_name, doc_full_name; "-itfusion", Arg.Set do_iterator_fusion, doc_itfusion; ] (compile compile_impl) diff --git a/compiler/obc/obc_printer.ml b/compiler/obc/obc_printer.ml index 18d4f4c..3c1af7e 100644 --- a/compiler/obc/obc_printer.ml +++ b/compiler/obc/obc_printer.ml @@ -80,7 +80,7 @@ let rec print_act ff a = match a with | Aassgn (x, e) -> print_asgn ff "" x e | Acase(e, tag_act_list) -> - fprintf ff "@[@[switch ("; + fprintf ff "@[@[switch ("; print_exp ff e; fprintf ff ") {@ "; print_tag_act_list ff tag_act_list; fprintf ff "@]@,}@]" diff --git a/compiler/utilities/global/compiler_options.ml b/compiler/utilities/global/compiler_options.ml index 837c923..78b5f29 100644 --- a/compiler/utilities/global/compiler_options.ml +++ b/compiler/utilities/global/compiler_options.ml @@ -75,6 +75,8 @@ let set_target_path path = let full_type_info = ref false +let full_name = ref false + let causality = ref true let init = ref true @@ -109,6 +111,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_full_name = "\t\t\tPrint full variable name information" and doc_target_path = "\tGenerated files will be placed in \n\t\t\t(the directory is" ^ " cleaned)"