Commit d3e8e475 authored by MARCHE Claude's avatar MARCHE Claude

ITP does not use drivers anymore for printing task

it now uses the module core/Pretty, that is generalized so as
to take ident_printer as arguments.
Notice the very nice use of first-class modules !

TODO: a bug remain when printing ident with space in them
TODO: remove the tables in printer_args

We need to discuss with Andrei about the use of "infix " in
infix identifiers which appears to be a problem for parsing
transformation arguments.
Anyway, we don't understand the specific hacks for "mixfix []"
and "mixfix [<-]" in Pretty.ml. Why not similar hacks for "mixfix [..]"
for example?
parent 3a923a0f
......@@ -175,7 +175,7 @@ LIB_UTIL = config bigInt util opt lists strings \
lexlib print_tree cmdline warning sysutil rc plugin bigInt number pqueue
LIB_CORE = ident ty term pattern decl theory \
task pretty dterm env trans printer model_parser
task pretty_sig pretty dterm env trans printer model_parser
LIB_DRIVER = prove_client call_provers driver_ast driver_parser driver_lexer driver \
whyconf autodetection \
......
......@@ -34,22 +34,20 @@ let debug_print_labels =
let debug_print_locs = Debug.register_info_flag "print_locs"
~desc:"Print@ locations@ of@ identifiers@ and@ expressions."
let iprinter,aprinter,tprinter,pprinter =
let isanitize = sanitizer char_to_alpha char_to_alnumus in
let lsanitize = sanitizer char_to_lalpha char_to_alnumus in
create_ident_printer why3_keywords ~sanitizer:isanitize,
create_ident_printer why3_keywords ~sanitizer:lsanitize,
create_ident_printer why3_keywords ~sanitizer:lsanitize,
create_ident_printer why3_keywords ~sanitizer:isanitize
let create iprinter aprinter tprinter pprinter do_forget_all =
(module (struct
let forget_tvs () =
forget_all aprinter
(* we always forget type variables between each declaration *)
(* if do_forget_all then *) forget_all aprinter
let forget_all () =
forget_all iprinter;
forget_all aprinter;
forget_all tprinter;
forget_all pprinter
if do_forget_all then forget_all iprinter;
if do_forget_all then forget_all aprinter;
if do_forget_all then forget_all tprinter;
if do_forget_all then forget_all pprinter
let print_label fmt l = fprintf fmt "\"%s\"" l.lab_string
let print_labels = print_iter1 Slab.iter space print_label
......@@ -508,6 +506,51 @@ let print_namespace fmt name th =
fprintf fmt "@[<hov>%a@]@." P.print
(NsTree.Namespace (name, th.th_export, th.th_known))
(* print task under the form of a sequent, with only local context, for the IDE *)
let print_goal fmt d =
match d.d_node with
| Dprop (Pgoal,_pr,f) -> fprintf fmt "@[%a@]@\n" print_term f
| _ -> assert false
let print_sequent fmt task =
let ut = Task.used_symbols (Task.used_theories task) in
let ld = Task.local_decls task ut in
let rec aux fmt l =
match l with
| [] -> assert false
| [g] ->
fprintf fmt "----------------------------- Goal ---------------------------@\n@\n";
print_goal fmt g
| d :: r ->
fprintf fmt "@[%a@]@\n@\n" print_decl d;
aux fmt r
in
fprintf fmt "----------------------------- Local context ---------------------------@\n@\n";
fprintf fmt "@[<v 0>%a@]" aux ld
end) : Pretty_sig.Printer) (* end of the first class module *)
module LegacyPrinter =
(val (let iprinter,aprinter,tprinter,pprinter =
let isanitize = sanitizer char_to_alpha char_to_alnumus in
let lsanitize = sanitizer char_to_lalpha char_to_alnumus in
create_ident_printer why3_keywords ~sanitizer:isanitize,
create_ident_printer why3_keywords ~sanitizer:lsanitize,
create_ident_printer why3_keywords ~sanitizer:lsanitize,
create_ident_printer why3_keywords ~sanitizer:isanitize
in
create iprinter aprinter tprinter pprinter true))
include LegacyPrinter
(* Exception reporting *)
let () = Exn_printer.register
......
......@@ -9,59 +9,11 @@
(* *)
(********************************************************************)
open Format
open Ident
open Ty
open Term
open Decl
open Theory
open Task
val why3_keywords : string list
val forget_all : unit -> unit (* flush id_unique *)
val forget_tvs : unit -> unit (* flush id_unique for type vars *)
val forget_var : vsymbol -> unit (* flush id_unique for a variable *)
include Pretty_sig.Printer
val print_id_labels : formatter -> ident -> unit (* labels and location *)
val print_tv : formatter -> tvsymbol -> unit (* type variable *)
val print_vs : formatter -> vsymbol -> unit (* variable *)
val print_ts : formatter -> tysymbol -> unit (* type symbol *)
val print_ls : formatter -> lsymbol -> unit (* logic symbol *)
val print_cs : formatter -> lsymbol -> unit (* constructor symbol *)
val print_pr : formatter -> prsymbol -> unit (* proposition name *)
val print_th : formatter -> theory -> unit (* theory name *)
val print_ty : formatter -> ty -> unit (* type *)
val print_vsty : formatter -> vsymbol -> unit (* variable : type *)
val print_quant : formatter -> quant -> unit (* quantifier *)
val print_binop : asym:bool -> formatter -> binop -> unit (* binary operator *)
val print_pat : formatter -> pattern -> unit (* pattern *)
val print_term : formatter -> term -> unit (* term *)
val print_label : formatter -> label -> unit
val print_loc : formatter -> Loc.position -> unit
val print_pkind : formatter -> prop_kind -> unit
val print_meta_arg : formatter -> meta_arg -> unit
val print_meta_arg_type : formatter -> meta_arg_type -> unit
val print_ty_decl : formatter -> tysymbol -> unit
val print_data_decl : formatter -> data_decl -> unit
val print_param_decl : formatter -> lsymbol -> unit
val print_logic_decl : formatter -> logic_decl -> unit
val print_ind_decl : formatter -> ind_sign -> ind_decl -> unit
val print_next_data_decl : formatter -> data_decl -> unit
val print_next_logic_decl : formatter -> logic_decl -> unit
val print_next_ind_decl : formatter -> ind_decl -> unit
val print_prop_decl : formatter -> prop_decl -> unit
val print_decl : formatter -> decl -> unit
val print_tdecl : formatter -> tdecl -> unit
val print_task : formatter -> task -> unit
val print_theory : formatter -> theory -> unit
val print_namespace : formatter -> string -> theory -> unit
val create : Ident.ident_printer ->Ident.ident_printer ->
Ident.ident_printer -> Ident.ident_printer ->
bool -> (module Pretty_sig.Printer)
open Format
open Ident
open Ty
open Term
open Decl
open Theory
open Task
module type Printer = sig
val forget_all : unit -> unit (* flush id_unique *)
val forget_tvs : unit -> unit (* flush id_unique for type vars *)
val forget_var : vsymbol -> unit (* flush id_unique for a variable *)
val print_id_labels : formatter -> ident -> unit (* labels and location *)
val print_tv : formatter -> tvsymbol -> unit (* type variable *)
val print_vs : formatter -> vsymbol -> unit (* variable *)
val print_ts : formatter -> tysymbol -> unit (* type symbol *)
val print_ls : formatter -> lsymbol -> unit (* logic symbol *)
val print_cs : formatter -> lsymbol -> unit (* constructor symbol *)
val print_pr : formatter -> prsymbol -> unit (* proposition name *)
val print_th : formatter -> theory -> unit (* theory name *)
val print_ty : formatter -> ty -> unit (* type *)
val print_vsty : formatter -> vsymbol -> unit (* variable : type *)
val print_quant : formatter -> quant -> unit (* quantifier *)
val print_binop : asym:bool -> formatter -> binop -> unit (* binary operator *)
val print_pat : formatter -> pattern -> unit (* pattern *)
val print_term : formatter -> term -> unit (* term *)
val print_label : formatter -> label -> unit
val print_loc : formatter -> Loc.position -> unit
val print_pkind : formatter -> prop_kind -> unit
val print_meta_arg : formatter -> meta_arg -> unit
val print_meta_arg_type : formatter -> meta_arg_type -> unit
val print_ty_decl : formatter -> tysymbol -> unit
val print_data_decl : formatter -> data_decl -> unit
val print_param_decl : formatter -> lsymbol -> unit
val print_logic_decl : formatter -> logic_decl -> unit
val print_ind_decl : formatter -> ind_sign -> ind_decl -> unit
val print_next_data_decl : formatter -> data_decl -> unit
val print_next_logic_decl : formatter -> logic_decl -> unit
val print_next_ind_decl : formatter -> ind_decl -> unit
val print_prop_decl : formatter -> prop_decl -> unit
val print_decl : formatter -> decl -> unit
val print_tdecl : formatter -> tdecl -> unit
val print_task : formatter -> task -> unit
val print_sequent : formatter -> task -> unit
val print_theory : formatter -> theory -> unit
val print_namespace : formatter -> string -> theory -> unit
end
......@@ -342,6 +342,7 @@ type naming_table = {
namespace : namespace;
known_map : known_map;
printer : Ident.ident_printer;
aprinter : Ident.ident_printer;
}
exception Bad_name_table of string
......
......@@ -171,6 +171,7 @@ type naming_table = {
namespace : namespace;
known_map : known_map;
printer : Ident.ident_printer;
aprinter : Ident.ident_printer;
}
(** In order to interpret, that is type, string arguments as symbols or
terms, a transformation may need a [naming_table]. Typing arguments
......
......@@ -80,6 +80,7 @@ let rec print_ty_node inn tables fmt ty = match ty.ty_node with
let print_ty = print_ty_node false
(** Forgetting function for stability of errors *)
(*
let print_forget_vsty tables fmt v =
if (Ident.known_id tables.Trans.printer v.vs_name) then
fprintf fmt "%a: %a" (print_vs tables) v (print_ty tables) v.vs_ty
......@@ -88,7 +89,7 @@ let print_forget_vsty tables fmt v =
fprintf fmt "%a: %a" (print_vs tables) v (print_ty tables) v.vs_ty;
forget_var tables v
end
*)
(* can the type of a value be derived from the type of the arguments? *)
let unambig_fs fs =
......@@ -409,11 +410,14 @@ let print_tdecls tables =
let empty_naming_table () =
let sanitizer = Ident.(sanitizer char_to_alpha char_to_alnumus) in
let lsanitizer = Ident.(sanitizer char_to_lalpha char_to_alnumus) in
let pr = create_ident_printer Pretty.why3_keywords ~sanitizer in
let apr = create_ident_printer Pretty.why3_keywords ~sanitizer:lsanitizer in
Trans.{
namespace = empty_ns;
known_map = Ident.Mid.empty;
printer = pr;
aprinter = apr;
}
let print_task args ?old:_ fmt task =
......
......@@ -30,6 +30,7 @@
*)
(*
val print_ls : Trans.naming_table -> Format.formatter -> Term.lsymbol -> unit
val print_tv : Trans.naming_table -> Format.formatter -> Ty.tvsymbol -> unit
val print_ts : Trans.naming_table -> Format.formatter -> Ty.tysymbol -> unit
......@@ -39,3 +40,4 @@ val print_pat : Trans.naming_table -> Format.formatter -> Term.pattern -> unit
val print_ty : Trans.naming_table -> Format.formatter -> Ty.ty -> unit
val print_term : Trans.naming_table -> Format.formatter -> Term.term -> unit
val print_decl : Trans.naming_table -> Format.formatter -> Decl.decl -> unit
*)
......@@ -82,53 +82,37 @@ let loaded_strategies = ref []
(****** Exception handling *********)
let print_term s id fmt t =
let p s id =
let tables = match (Session_itp.get_table s id) with
| None -> Args_wrapper.build_naming_tables (Session_itp.get_task s id)
| Some tables -> tables in
Why3printer.print_term tables fmt t
let pr = tables.Trans.printer in
let apr = tables.Trans.aprinter in
(Pretty.create pr apr pr pr false)
let print_term s id fmt t =
let module P = (val (p s id)) in P.print_term fmt t
let print_type s id fmt t =
let tables = match (Session_itp.get_table s id) with
| None -> Args_wrapper.build_naming_tables (Session_itp.get_task s id)
| Some tables -> tables in
Why3printer.print_ty tables fmt t
let module P = (val (p s id)) in P.print_ty fmt t
let print_ts s id fmt t =
let tables = match (Session_itp.get_table s id) with
| None -> Args_wrapper.build_naming_tables (Session_itp.get_task s id)
| Some tables -> tables in
Why3printer.print_ts tables fmt t
let module P = (val (p s id)) in P.print_ts fmt t
let print_ls s id fmt t =
let tables = match (Session_itp.get_table s id) with
| None -> Args_wrapper.build_naming_tables (Session_itp.get_task s id)
| Some tables -> tables in
Why3printer.print_ls tables fmt t
let module P = (val (p s id)) in P.print_ls fmt t
let print_tv s id fmt t =
let tables = match (Session_itp.get_table s id) with
| None -> Args_wrapper.build_naming_tables (Session_itp.get_task s id)
| Some tables -> tables in
Why3printer.print_tv tables fmt t
let module P = (val (p s id)) in P.print_tv fmt t
let print_vsty s id fmt t =
let tables = match (Session_itp.get_table s id) with
| None -> Args_wrapper.build_naming_tables (Session_itp.get_task s id)
| Some tables -> tables in
Why3printer.print_forget_vsty tables fmt t
let module P = (val (p s id)) in P.print_vsty fmt t
let print_pr s id fmt t =
let tables = match (Session_itp.get_table s id) with
| None -> Args_wrapper.build_naming_tables (Session_itp.get_task s id)
| Some tables -> tables in
Why3printer.print_pr tables fmt t
let module P = (val (p s id)) in P.print_pr fmt t
let print_pat s id fmt t =
let tables = match (Session_itp.get_table s id) with
| None -> Args_wrapper.build_naming_tables (Session_itp.get_task s id)
| Some tables -> tables in
Why3printer.print_pat tables fmt t
let module P = (val (p s id)) in P.print_pat fmt t
(* Exception reporting *)
......@@ -912,9 +896,16 @@ end
let tables = get_table d.cont.controller_session id in
(* This function also send source locations associated to the task *)
let loc_color_list = get_locations task in
Pp.string_of
(Driver.print_task ~cntexample:false ?name_table:tables ~do_intros d.task_driver)
task, loc_color_list
let task_text =
match tables with
| None -> assert false
| Some t ->
let pr = t.Trans.printer in
let apr = t.Trans.aprinter in
let module P = (val Pretty.create pr apr pr pr false) in
Pp.string_of P.print_sequent task
in
task_text, loc_color_list
let send_task nid do_intros =
let d = get_server_data () in
......
......@@ -157,7 +157,10 @@ let print_id s tables =
try Ident.Mid.find (symbol_name id) km with
| Not_found -> raise Not_found (* Should not happen *)
in
Pp.string_of (Why3printer.print_decl tables) d
let pr = tables.Trans.printer in
let apr = tables.Trans.aprinter in
let module P = (val Pretty.create pr apr pr pr false) in
Pp.string_of P.print_decl d
......@@ -212,7 +215,10 @@ let search s tables =
(Pp.print_list Pp.space (fun fmt id -> Pp.string fmt id.Ident.id_string))
ids
else let l = Decl.Sdecl.elements l in
Pp.string_of (Pp.print_list Pp.newline2 (Why3printer.print_decl tables)) l
let pr = tables.Trans.printer in
let apr = tables.Trans.aprinter in
let module P = (val Pretty.create pr apr pr pr false) in
Pp.string_of (Pp.print_list Pp.newline2 P.print_decl) l
let print_id _cont task args =
match args with
......
......@@ -144,16 +144,19 @@ let add (d: decl) (tables: naming_table): naming_table =
add_unsafe s (Pr pr) tables
let build_naming_tables task : naming_table =
(* TODO this sanitizer makes it impossible to reparse '=' but not only it.
Also other stuff like ident followed by number generated by intros. *)
let sanitizer = sanitizer char_to_alpha char_to_alnumus in
(* TODO sanitizer breaks the naming of infix symbol. *)
let pr = create_ident_printer Pretty.why3_keywords (*~sanitizer*) in
(** FIXME: using sanitizer here breaks the printing of infix symbols
because it replaces "infix +" by "infix_+", which forbids to
parse transformation arguments containing "+" such as "cut 1+2=3" *)
let isanitizer = sanitizer char_to_alpha char_to_alnumus in
let lsanitize = sanitizer char_to_lalpha char_to_alnumus in
let pr = create_ident_printer Pretty.why3_keywords (* ~sanitizer:isanitizer*) in
let apr = create_ident_printer [] ~sanitizer:lsanitize in
let km = Task.task_known task in
let tables = {
namespace = empty_ns;
known_map = km;
printer = pr;
aprinter = apr;
} in
(* We want conflicting names to be named as follows:
names closer to the goal should be named with lowest
......
module M
use import int.Int
function (++) (x:int) (y:int) : int = x * y
end
module TestTaskPrinting
use import int.Int
......@@ -20,6 +28,16 @@ module TestTaskPrinting
goal g6: let x = averyveryveryveryveryverylongname 1 + averyveryveryveryveryverylongname 2
in averyveryveryveryveryverylongname x + averyveryveryveryveryverylongname 1 >= 0
function (+) (x:int) (y:int) : int = x * y
goal g7: 2 + 3 = Int.(+) 3 3
use import M
function (++) (x:int) (y:int) : int = x * y
goal g8: 2 ++ 3 = M.(++) 3 3
end
module TestAutomaticIntro
......
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