Unclutter ident printing.

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

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
 
 

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 "@[<v>@[<hv 2>reset @ %a@]@,every %a@]"
-        (print_block "in") b   print_exp e
+        print_block b   print_exp e
     | Eblock b ->
-      fprintf ff "@[<v>do@[<v>@ @[%a@]@]@ done@]" (print_block "in") b
+      fprintf ff "@[<v>do@[<v>@ @[%a@]@]@ done@]" print_block b
 
 and print_state_handler_list ff tag_act_list =
   print_list
     (fun ff sh ->
        fprintf ff "@[<v 2>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 "@[<v 2>| %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 "@[<v 2>| %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 "@[<v 2>default@,%a@]" (print_block "do") b
+    | _ -> fprintf ff "@[<v 2>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@[<v2>%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 "@[<v>%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 "@[<v2>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

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)

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 "@[<v>@[<hv 2>switch (";
+        fprintf ff "@[<v>@[<v 2>switch (";
         print_exp ff e; fprintf ff ") {@ ";
         print_tag_act_list ff tag_act_list;
         fprintf ff "@]@,}@]"

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 =
   "<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_full_name = "\t\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"
   ^ " cleaned)"