Commit 6174ead2 authored by MARCHE Claude's avatar MARCHE Claude

move empty_name_table where it is used

parent 5f88d5fa
......@@ -345,14 +345,6 @@ type naming_table = {
exception Bad_name_table of string
let empty_naming_table =
let sanitizer = Ident.(sanitizer char_to_alpha char_to_alnumus) in
{
namespace = empty_ns;
known_map = Ident.Mid.empty;
printer = Ident.create_ident_printer ~sanitizer [];
}
type trans_with_args = string list -> Env.env -> naming_table -> task trans
type trans_with_args_l = string list -> Env.env -> naming_table -> task tlist
......
......@@ -187,8 +187,6 @@ type naming_table = {
exception Bad_name_table of string
val empty_naming_table : naming_table
type trans_with_args = string list -> Env.env -> naming_table -> task trans
type trans_with_args_l = string list -> Env.env -> naming_table -> task tlist
......
......@@ -407,13 +407,18 @@ let print_tdecls tables =
Discriminate.on_syntax_map (fun sm -> Trans.fold (print_tdecl tables) (sm,[]))
*)
(* TODO print_task and print_sequent recompute a table every time they are called.
Do we want that? *)
let empty_naming_table () =
let sanitizer = Ident.(sanitizer char_to_alpha char_to_alnumus) in
let pr = create_ident_printer Pretty.why3_keywords ~sanitizer in
Trans.{
namespace = empty_ns;
known_map = Ident.Mid.empty;
printer = pr;
}
let print_task args ?old:_ fmt task =
(* In trans-based p-printing [forget_all] IST STRENG VERBOTEN *)
(* forget_all (); *)
let tables = match args.name_table with
| None -> Trans.empty_naming_table (* raise (Bad_name_table "Why3printer.print_task")*)
| None -> empty_naming_table ()
| Some tables -> tables in
print_prelude fmt args.prelude;
fprintf fmt "theory Task@\n";
......@@ -471,9 +476,10 @@ let print_goal tables do_intros fmt d =
let print_sequent args ?old:_ fmt task =
info := {info_syn = Discriminate.get_syntax_map task;
itp = true};
let tables = match args.name_table with
| None -> Trans.empty_naming_table (* raise (Bad_name_table "Why3printer.print_sequent") *)
| Some tables -> tables in
let tables,do_intros = match args.name_table with
| None -> empty_naming_table (), false
| Some tables -> tables,args.do_intros
in
(* let tables = build_name_tables task in *)
let ut = Task.used_symbols (Task.used_theories task) in
let ld = Task.local_decls task ut in
......@@ -482,7 +488,7 @@ let print_sequent args ?old:_ fmt task =
| [] -> assert false
| [g] ->
fprintf fmt "----------------------------- Goal ---------------------------@\n@\n";
print_goal tables args.do_intros fmt g
print_goal tables do_intros fmt g
| d :: r ->
fprintf fmt "@[%a@]@\n" (print_decl tables) d;
aux fmt r
......
......@@ -91,6 +91,8 @@ let ind_decl_add il tables =
il
tables
(* [add d printer tables] Adds all new declaration of symbol inside d to tables.
It uses printer to give them a unique name and also register these new names in printer *)
let add (d: decl) (tables: naming_table): naming_table =
......@@ -135,7 +137,7 @@ let add (d: decl) (tables: naming_table): naming_table =
ind_decl_add tables ind)
tables
il
| Dprop (_, pr, _t) ->
| Dprop (_, pr, _) ->
(* Only pr is new in Dprop (see create_prop_decl) *)
let id = pr.pr_name in
let s = id_unique tables id in
......
......@@ -22,6 +22,15 @@ module TestTaskPrinting
end
module TestAutomaticIntro
use import int.Int
goal g : forall x:int. x > 0 -> forall y z:int. y = z -> x=y
end
module TestInfixSymbols
......
Markdown is supported
0%
or
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment