Commit bb20ba6d authored by MARCHE Claude's avatar MARCHE Claude

fix module Pretty

removed interface-only module pretty_sig because does break make -j

Too bad the sig Printer needs now to be duplicated.
parent 8cf28b45
......@@ -1900,7 +1900,7 @@ MODULESTODOC = \
util/weakhtbl util/stdlib util/rc util/debug \
util/loc util/pp util/bigInt util/number \
core/ident core/ty core/term core/decl core/theory \
core/env core/task core/trans core/pretty_sig core/pretty core/printer \
core/env core/task core/trans core/pretty core/printer \
driver/whyconf driver/call_provers driver/driver \
transform/args_wrapper \
session/session_itp session/controller_itp \
......
......@@ -26,6 +26,60 @@ let why3_keywords =
"forall"; "exists"; "not"; "true"; "false"; "if"; "then"; "else";
"let"; "in"; "match"; "with"; "as"; "epsilon" ]
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
let debug_print_labels =
Debug.register_info_flag
"print_labels"
......@@ -568,7 +622,7 @@ let print_sequent fmt task =
end) : Pretty_sig.Printer) (* end of the first class module *)
end) : Printer) (* end of the first class module *)
......
......@@ -13,10 +13,71 @@
val why3_keywords : string list
include 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
include Printer
val meta_introduced_hypotheses : Theory.meta
val create : Ident.ident_printer ->Ident.ident_printer ->
Ident.ident_printer -> Ident.ident_printer ->
bool -> (module Pretty_sig.Printer)
bool -> (module Printer)
(********************************************************************)
(* *)
(* The Why3 Verification Platform / The Why3 Development Team *)
(* Copyright 2010-2018 -- Inria - CNRS - Paris-Sud University *)
(* *)
(* This software is distributed under the terms of the GNU Lesser *)
(* General Public License version 2.1, with the special exception *)
(* on linking described in file LICENSE. *)
(* *)
(********************************************************************)
(** Pretty-printing various objects from Why3's core logic (signature)
signature only, see module [Pretty] for implementation
*)
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
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