Commit 32712471 authored by MARCHE Claude's avatar MARCHE Claude

Resurrection of extraction drivers

Attempt to make it generic, using registered extraction functions

Compiles but not working yet
parent 8a4809cc
......@@ -176,7 +176,8 @@ LIB_DRIVER = prove_client call_provers driver_ast driver_parser driver_lexer dri
whyconf autodetection \
parse_smtv2_model_parser parse_smtv2_model_lexer parse_smtv2_model
LIB_MLW = ity expr dexpr pdecl eval_match vc pmodule pinterp
LIB_MLW = ity expr dexpr pdecl eval_match vc pmodule \
pinterp pdriver
LIB_PARSER = ptree glob typing parser lexer
......@@ -469,10 +470,7 @@ install_no_local::
TOOLSGENERATED = src/tools/why3wc.ml
# TODO
#TOOLS_BIN = why3config why3execute why3extract why3prove \
# why3realize why3replay why3wc
TOOLS_BIN = why3config why3execute why3prove \
TOOLS_BIN = why3config why3execute why3extract why3prove \
why3realize why3replay why3wc
TOOLS_FILES = main $(TOOLS_BIN)
......
......@@ -22,8 +22,6 @@ type prelude = string list
type prelude_map = prelude Mid.t
type blacklist = string list
type 'a pp = Format.formatter -> 'a -> unit
(* Makes it possible to estabilish traceability from names
in the output of the printer to elements of AST in its input. *)
type printer_mapping = {
......@@ -43,7 +41,7 @@ type printer_args = {
mutable printer_mapping : printer_mapping;
}
type printer = printer_args -> ?old:in_channel -> task pp
type printer = printer_args -> ?old:in_channel -> task Pp.pp
val get_default_printer_mapping : printer_mapping
......@@ -55,8 +53,8 @@ val list_printers : unit -> (string * Pp.formatted) list
(** {2 Use printers} *)
val print_prelude : prelude pp
val print_th_prelude : task -> prelude_map pp
val print_prelude : prelude Pp.pp
val print_th_prelude : task -> prelude_map Pp.pp
val meta_syntax_type : meta
val meta_syntax_logic : meta
......@@ -88,15 +86,15 @@ val add_converter_map : tdecl -> converter_map -> converter_map
val query_syntax : syntax_map -> ident -> string option
val query_converter : converter_map -> lsymbol -> string option
val syntax_arguments : string -> 'a pp -> 'a list pp
val syntax_arguments : string -> 'a Pp.pp -> 'a list Pp.pp
(** (syntax_arguments templ print_arg fmt l) prints in the formatter fmt
the list l using the template templ and the printer print_arg *)
val gen_syntax_arguments_typed :
('a -> 'b) -> ('a -> 'b array) -> string -> 'a pp -> 'b pp -> 'a -> 'a list pp
('a -> 'b) -> ('a -> 'b array) -> string -> 'a Pp.pp -> 'b Pp.pp -> 'a -> 'a list Pp.pp
val syntax_arguments_typed :
string -> term pp -> ty pp -> term -> term list pp
string -> term Pp.pp -> ty Pp.pp -> term -> term list Pp.pp
(** (syntax_arguments templ print_arg fmt l) prints in the formatter fmt
the list l using the template templ and the printer print_arg *)
......
(********************************************************************)
(* *)
(* The Why3 Verification Platform / The Why3 Development Team *)
(* Copyright 2010-2016 -- 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. *)
(* *)
(********************************************************************)
open Ident
open Ty
open Term
open Theory
open Driver_ast
type driver = {
drv_env : Env.env;
drv_printer : string option;
drv_prelude : Printer.prelude;
drv_thprelude : Printer.prelude_map;
drv_blacklist : Printer.blacklist;
drv_syntax : Printer.syntax_map;
drv_converter : Printer.syntax_map;
}
type printer_args = {
env : Env.env;
prelude : Printer.prelude;
thprelude : Printer.prelude_map;
blacklist : Printer.blacklist;
syntax : Printer.syntax_map;
converter : Printer.syntax_map;
}
let load_file file =
let c = open_in file in
let lb = Lexing.from_channel c in
Loc.set_file file lb;
let to_close = Stack.create () in
Stack.push c to_close;
let input_lexer filename =
let c = open_in filename in
Stack.push c to_close;
let lb = Lexing.from_channel c in
Loc.set_file filename lb;
lb
in
let f = Driver_lexer.parse_file_extract input_lexer lb in
Stack.iter close_in to_close;
f
exception Duplicate of string
exception UnknownType of (string list * string list)
exception UnknownLogic of (string list * string list)
exception UnknownProp of (string list * string list)
exception UnknownVal of (string list * string list)
exception UnknownExn of (string list * string list)
exception FSymExpected of lsymbol
exception PSymExpected of lsymbol
let load_driver env file extra_files =
let prelude = ref [] in
let printer = ref None in
let blacklist = Queue.create () in
let set_or_raise loc r v error = match !r with
| Some _ -> raise (Loc.Located (loc, Duplicate error))
| None -> r := Some v
in
let add_to_list r v = (r := v :: !r) in
let add_global (loc, g) = match g with
| EPrelude s -> add_to_list prelude s
| EPrinter s -> set_or_raise loc printer s "printer"
| EBlacklist sl -> List.iter (fun s -> Queue.add s blacklist) sl
in
let f = load_file file in
List.iter add_global f.fe_global;
let thprelude = ref Mid.empty in
let syntax_map = ref Mid.empty in
let converter_map = ref Mid.empty in
let qualid = ref [] in
let find_pr th (loc,q) = try Theory.ns_find_pr th.th_export q
with Not_found -> raise (Loc.Located (loc, UnknownProp (!qualid,q)))
in
let find_ls th (loc,q) = try Theory.ns_find_ls th.th_export q
with Not_found -> raise (Loc.Located (loc, UnknownLogic (!qualid,q)))
in
let find_ts th (loc,q) = try Theory.ns_find_ts th.th_export q
with Not_found -> raise (Loc.Located (loc, UnknownType (!qualid,q)))
in
let find_fs th q =
let ls = find_ls th q in
if ls.ls_value = None then raise (FSymExpected ls) else ls in
let find_ps th q =
let ls = find_ls th q in
if ls.ls_value <> None then raise (PSymExpected ls) else ls in
let add_syntax id s b =
syntax_map := Mid.add id (s,if b then 1 else 0) !syntax_map in
let add_converter id s b =
converter_map := Mid.add id (s,if b then 1 else 0) !converter_map in
let add_local th = function
| Rprelude s ->
let l = Mid.find_def [] th.th_name !thprelude in
thprelude := Mid.add th.th_name (s::l) !thprelude
| Rsyntaxts (q,s,b) ->
let ts = find_ts th q in
Printer.check_syntax_type ts s;
add_syntax ts.ts_name s b
| Rsyntaxfs (q,s,b) ->
let fs = find_fs th q in
Printer.check_syntax_logic fs s;
add_syntax fs.ls_name s b
| Rsyntaxps (q,s,b) ->
let ps = find_ps th q in
Printer.check_syntax_logic ps s;
add_syntax ps.ls_name s b
| Rconverter _ ->
Loc.errorm "Syntax converter cannot be used in pure theories"
| Rremovepr (q) ->
ignore (find_pr th q)
| Rremoveall ->
let it key _ = match (Mid.find key th.th_known).Decl.d_node with
| Decl.Dprop (_,symb,_) -> ignore symb
| _ -> ()
in
Mid.iter it th.th_local
| Rmeta (s,al) ->
let rec ty_of_pty = function
| PTyvar x ->
Ty.ty_var (Ty.tv_of_string x)
| PTyapp ((loc,_) as q,tyl) ->
let ts = find_ts th q in
let tyl = List.map ty_of_pty tyl in
Loc.try2 ~loc Ty.ty_app ts tyl
| PTuple tyl ->
let ts = Ty.ts_tuple (List.length tyl) in
Ty.ty_app ts (List.map ty_of_pty tyl)
in
let convert = function
| PMAty (PTyapp (q,[]))
-> MAts (find_ts th q)
| PMAty ty -> MAty (ty_of_pty ty)
| PMAfs q -> MAls (find_fs th q)
| PMAps q -> MAls (find_ps th q)
| PMApr q -> MApr (find_pr th q)
| PMAstr s -> MAstr s
| PMAint i -> MAint i
in
let m = lookup_meta s in
ignore (create_meta m (List.map convert al))
in
let add_local th (loc,rule) = Loc.try2 ~loc add_local th rule in
let open Pmodule in
let find_val m (loc,q) =
try match ns_find_prog_symbol m.mod_export q with
| PV pv -> pv.Ity.pv_vs.vs_name
| RS rs -> rs.Expr.rs_name
with Not_found -> raise (Loc.Located (loc, UnknownVal (!qualid,q)))
in
let find_xs m (loc,q) =
try ns_find_xs m.mod_export q
with Not_found -> raise (Loc.Located (loc, UnknownExn (!qualid,q)))
in
let add_local_module loc m = function
| MRexception (q,s) ->
let xs = find_xs m q in
add_syntax xs.Ity.xs_name s false
| MRval (q,s) ->
let id = find_val m q in
add_syntax id s false
| MRtheory (Rconverter (q,s,b)) ->
let id = find_val m q in
add_converter id s b
| MRtheory trule ->
add_local m.mod_theory (loc,trule)
in
let add_local_module m (loc,rule) =
Loc.try3 ~loc add_local_module loc m rule
in
let add_theory { thr_name = (loc,q); thr_rules = trl } =
let f,id = let l = List.rev q in List.rev (List.tl l),List.hd l in
let th = Loc.try3 ~loc Env.read_theory env f id in
qualid := q;
List.iter (add_local th) trl
in
let add_module { mor_name = (loc,q); mor_rules = mrl } =
let f,id = let l = List.rev q in List.rev (List.tl l),List.hd l in
let m = Loc.try3 ~loc read_module env f id in
qualid := q;
List.iter (add_local_module m) mrl
in
List.iter add_theory f.fe_th_rules;
List.iter add_module f.fe_mo_rules;
List.iter (fun f ->
let fe = load_file f in
List.iter add_theory fe.fe_th_rules;
List.iter add_module fe.fe_mo_rules)
extra_files;
{
drv_env = env;
drv_printer = !printer;
drv_prelude = List.rev !prelude;
drv_thprelude = Mid.map List.rev !thprelude;
drv_blacklist = Queue.fold (fun l s -> s :: l) [] blacklist;
drv_syntax = !syntax_map;
drv_converter = !converter_map;
}
(* registering printers for programs *)
open Stdlib
type printer = printer_args -> ?old:in_channel -> Pmodule.pmodule Pp.pp
type reg_printer = Pp.formatted * printer
let printers : reg_printer Hstr.t = Hstr.create 17
exception KnownPrinter of string
exception UnknownPrinter of string
exception NoPrinter
let register_printer ~desc s p =
if Hstr.mem printers s then raise (KnownPrinter s);
Hstr.replace printers s (desc, p)
let lookup_printer s =
try snd (Hstr.find printers s)
with Not_found -> raise (UnknownPrinter s)
let list_printers () =
Hstr.fold (fun k (desc,_) acc -> (k,desc)::acc) printers []
let extract_module ?old drv fmt m =
let p = match drv.drv_printer with
| None -> raise NoPrinter
| Some p -> p
in
let printer_args = {
env = drv.drv_env;
prelude = drv.drv_prelude;
thprelude = drv.drv_thprelude;
blacklist = drv.drv_blacklist;
syntax = drv.drv_syntax;
converter = drv.drv_converter;
} in
let printer = lookup_printer p printer_args in
Format.fprintf fmt "@[%a@]@?" (printer ?old) m
(* exception report *)
let string_of_qualid thl idl =
String.concat "." thl ^ "." ^ String.concat "." idl
let () = Exn_printer.register (fun fmt exn ->
let open Format in
match exn with
| Duplicate s -> fprintf fmt
"Duplicate %s specification" s
| UnknownType (thl,idl) -> fprintf fmt
"Unknown type symbol %s" (string_of_qualid thl idl)
| UnknownLogic (thl,idl) -> fprintf fmt
"Unknown logical symbol %s" (string_of_qualid thl idl)
| UnknownProp (thl,idl) -> fprintf fmt
"Unknown proposition %s" (string_of_qualid thl idl)
| UnknownVal (thl,idl) -> fprintf fmt
"Unknown val %s" (string_of_qualid thl idl)
| UnknownExn (thl,idl) -> fprintf fmt
"Unknown exception %s" (string_of_qualid thl idl)
| FSymExpected ls -> fprintf fmt
"%a is not a function symbol" Pretty.print_ls ls
| PSymExpected ls -> fprintf fmt
"%a is not a predicate symbol" Pretty.print_ls ls
| KnownPrinter s ->
fprintf fmt "Program printer '%s' is already registered" s
| UnknownPrinter s ->
fprintf fmt "Unknown program printer '%s'" s
| e -> raise e)
(********************************************************************)
(* *)
(* The Why3 Verification Platform / The Why3 Development Team *)
(* Copyright 2010-2016 -- 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. *)
(* *)
(********************************************************************)
type driver = private {
drv_env : Env.env;
drv_printer : string option;
drv_prelude : Printer.prelude;
drv_thprelude : Printer.prelude_map;
drv_blacklist : Printer.blacklist;
drv_syntax : Printer.syntax_map;
drv_converter : Printer.syntax_map;
}
type printer_args = private {
env : Env.env;
prelude : Printer.prelude;
thprelude : Printer.prelude_map;
blacklist : Printer.blacklist;
syntax : Printer.syntax_map;
converter : Printer.syntax_map;
}
val load_driver : Env.env -> string -> string list -> driver
(** loads a driver from a file
@param env environment to interpret theories and modules
@param string driver file name
@param string list additional drivers containing only theories/modules *)
type printer = printer_args -> ?old:in_channel -> Pmodule.pmodule Pp.pp
val register_printer : desc:Pp.formatted -> string -> printer -> unit
val lookup_printer : string -> printer
val list_printers : unit -> (string * Pp.formatted) list
val extract_module : ?old:in_channel ->
driver -> Format.formatter -> Pmodule.pmodule -> unit
......@@ -94,13 +94,13 @@ let opt_driver =
eprintf "Extraction driver (-D) is required.@.";
exit 1
| f::ef ->
Mlw_driver.load_driver env f ef
Pdriver.load_driver env f ef
with e when not (Debug.test_flag Debug.stack_trace) ->
eprintf "%a@." Exn_printer.exn_printer e;
exit 1
let extract_to ?fname th extract =
let file = Filename.concat opt_output (Mlw_ocaml.extract_filename ?fname th) in
let extract_to ?fname:string th extract =
let file = Filename.concat opt_output (assert false (*Mlw_ocaml.extract_filename ?fname th *)) in
let old =
if Sys.file_exists file then begin
let backup = file ^ ".bak" in
......@@ -111,30 +111,23 @@ let extract_to ?fname th extract =
extract file ?old (formatter_of_out_channel cout);
close_out cout
let extract_to =
let extract_to _ =
assert false
(*
let visited = Ident.Hid.create 17 in
fun ?fname th extract ->
if not (Ident.Hid.mem visited th.th_name) then begin
Ident.Hid.add visited th.th_name ();
extract_to ?fname th extract
end
*)
let use_iter f th =
List.iter (fun d -> match d.td_node with Use t -> f t | _ -> ()) th.th_decls
let rec do_extract_theory ?fname th =
let extract file ?old fmt = ignore (old);
let tname = th.th_name.Ident.id_string in
Debug.dprintf Mlw_ocaml.debug "extract theory %s to file %s@." tname file;
Mlw_ocaml.extract_theory opt_driver ?old ?fname fmt th
in
extract_to ?fname th extract;
let extract_use th' =
let fname = if th'.th_path = [] then fname else None in
do_extract_theory ?fname th' in
use_iter extract_use th
let rec do_extract_module ?fname m =
let do_extract_module ?fname m =
assert false
(*
let extract file ?old fmt = ignore (old);
let tname = m.Mlw_module.mod_theory.th_name.Ident.id_string in
Debug.dprintf Mlw_ocaml.debug "extract module %s to file %s@." tname file;
......@@ -149,49 +142,31 @@ let rec do_extract_module ?fname m =
| Some m' -> do_extract_module ?fname m'
| None -> do_extract_theory ?fname th' in
use_iter extract_use m.Mlw_module.mod_theory
*)
let do_global_extract (_,p,t) =
let env = opt_driver.Mlw_driver.drv_env in
match Mlw_module.read_module_or_theory env p t with
| Mlw_module.Module m -> do_extract_module m
| Mlw_module.Theory t -> do_extract_theory t
let do_extract_theory_from fname m (tname,_,t) =
let th = try Mstr.find t m with Not_found ->
eprintf "Theory '%s' not found in file '%s'.@." tname fname;
exit 1
in
do_extract_theory ~fname th
let env = opt_driver.Pdriver.drv_env in
let m = Pmodule.read_module env p t in
assert false (* TODO *)
let do_extract_module_from fname mm thm (tname,_,t) =
let do_extract_module_from fname mm (tname,_,t) =
try
let m = Mstr.find t mm in do_extract_module ~fname m
with Not_found -> try
let th = Mstr.find t thm in do_extract_theory ~fname th
with Not_found ->
eprintf "Theory/module '%s' not found in file '%s'.@." tname fname;
eprintf "Module '%s' not found in file '%s'.@." tname fname;
exit 1
let do_local_extract fname cin tlist =
let env = opt_driver.Mlw_driver.drv_env in
let env = opt_driver.Pdriver.drv_env in
let format = !opt_parser in
try
let mm, thm =
Env.read_channel ?format Mlw_module.mlw_language env fname cin in
if Queue.is_empty tlist then
let do_m t m thm = do_extract_module ~fname m; Mstr.remove t thm in
let thm = Mstr.fold do_m mm thm in
Mstr.iter (fun _ th -> do_extract_theory ~fname th) thm
else
Queue.iter (do_extract_module_from fname mm thm) tlist
with Env.InvalidFormat _ ->
let m = Env.read_channel ?format Env.base_language env fname cin in
if Queue.is_empty tlist then
let add_th t th mi = Ident.Mid.add th.th_name (t,th) mi in
let do_th _ (_,th) = do_extract_theory ~fname th in
Ident.Mid.iter do_th (Mstr.fold add_th m Ident.Mid.empty)
else
Queue.iter (do_extract_theory_from fname m) tlist
let mm =
Env.read_channel ?format Pmodule.mlw_language env fname cin in
if Queue.is_empty tlist then
let do_m m = do_extract_module ~fname m in
Mstr.iter do_m mm
else
Queue.iter (do_extract_module_from fname mm) tlist
let do_input = function
| None, tlist ->
......@@ -209,9 +184,3 @@ let () =
with e when not (Debug.test_flag Debug.stack_trace) ->
eprintf "%a@." Exn_printer.exn_printer e;
exit 1
(*
Local Variables:
compile-command: "unset LANG; make -C ../.. byte"
End:
*)
......@@ -15,6 +15,8 @@
open Format
type 'a pp = formatter -> 'a -> unit
let print_option f fmt = function
| None -> ()
| Some x -> f fmt x
......
......@@ -13,57 +13,29 @@
open Format
val print_option : (formatter -> 'a -> unit) -> formatter -> 'a option -> unit
val print_option_or_default :
string -> (formatter -> 'a -> unit) -> formatter -> 'a option -> unit
val print_list_pre :
(formatter -> unit -> unit) ->
(formatter -> 'a -> unit) -> formatter -> 'a list -> unit
val print_list_suf :
(formatter -> unit -> unit) ->
(formatter -> 'a -> unit) -> formatter -> 'a list -> unit
val print_list :
(formatter -> unit -> unit) ->
(formatter -> 'a -> unit) -> formatter -> 'a list -> unit
val print_list_or_default :
string -> (formatter -> unit -> unit) ->
(formatter -> 'a -> unit) -> formatter -> 'a list -> unit
val print_list_par :
(Format.formatter -> unit -> 'a) ->
(Format.formatter -> 'b -> unit) -> Format.formatter -> 'b list -> unit
val print_list_next :
(Format.formatter -> unit -> unit) ->
(bool -> Format.formatter -> 'a -> unit) ->
Format.formatter -> 'a list -> unit
type 'a pp = formatter -> 'a -> unit
val print_option : 'a pp -> 'a option pp
val print_option_or_default : string -> 'a pp -> 'a option pp
val print_list_pre : unit pp -> 'a pp -> 'a list pp
val print_list_suf : unit pp -> 'a pp -> 'a list pp
val print_list : unit pp -> 'a pp -> 'a list pp
val print_list_or_default : string -> unit pp -> 'a pp -> 'a list pp
val print_list_par : (formatter -> unit -> 'a) -> 'b pp -> 'b list pp
val print_list_next : unit pp -> (bool -> 'a pp) -> 'a list pp
val print_list_delim :
start:(Format.formatter -> unit -> unit) ->
stop:(Format.formatter -> unit -> unit) ->
sep:(Format.formatter -> unit -> unit) ->
(Format.formatter -> 'b -> unit) -> Format.formatter -> 'b list -> unit
start:unit pp -> stop:unit pp -> sep:unit pp -> 'b pp -> 'b list pp
val print_pair_delim :
(Format.formatter -> unit -> unit) ->
(Format.formatter -> unit -> unit) ->
(Format.formatter -> unit -> unit) ->
(Format.formatter -> 'a -> unit) ->
(Format.formatter -> 'b -> unit) -> Format.formatter -> 'a * 'b -> unit
val print_pair :
(Format.formatter -> 'a -> unit) ->
(Format.formatter -> 'b -> unit) -> Format.formatter -> 'a * 'b -> unit
unit pp -> unit pp -> unit pp -> 'a pp -> 'b pp -> ('a * 'b) pp
val print_pair : 'a pp -> 'b pp -> ('a * 'b) pp
val print_iter1 :
(('a -> unit) -> 'b -> unit) ->
(Format.formatter -> unit -> unit) ->
(Format.formatter -> 'a -> unit) ->
Format.formatter -> 'b -> unit
(('a -> unit) -> 'b -> unit) -> unit pp -> 'a pp -> 'b pp
val print_iter2:
(('a -> 'b -> unit) -> 'c -> unit) ->
(Format.formatter -> unit -> unit) ->
(Format.formatter -> unit -> unit) ->
(Format.formatter -> 'a -> unit) ->
(Format.formatter -> 'b -> unit) ->
Format.formatter -> 'c -> unit
unit pp -> unit pp -> 'a pp -> 'b pp -> 'c pp
(** [print_iter2 iter sep1 sep2 print1 print2 fmt t]
iter iterator on [t : 'c]
print1 k sep2 () print2 v sep1 () print1 sep2 () ...
......@@ -71,9 +43,9 @@ val print_iter2:
val print_iter22:
(('a -> 'b -> unit) -> 'c -> unit) ->
(Format.formatter -> unit -> unit) ->
(Format.formatter -> 'a -> 'b -> unit) ->
Format.formatter -> 'c -> unit
unit pp ->
(formatter -> 'a -> 'b -> unit) ->
'c pp
(** [print_iter22 iter sep print fmt t]
iter iterator on [t : 'c]
print k v sep () print k v sep () ...
......@@ -84,43 +56,43 @@ val print_iter22:
type formatted = (unit, unit, unit, unit, unit, unit) format6
val empty_formatted : formatted
val space : formatter -> unit -> unit
val alt : formatter -> unit -> unit
val alt2 : formatter -> unit -> unit
val newline : formatter -> unit -> unit
val newline2 : formatter -> unit -> unit
val dot : formatter -> unit -> unit
val comma : formatter -> unit -> unit
val star : formatter -> unit -> unit
val simple_comma : formatter -> unit -> unit
val semi : formatter -> unit -> unit
val colon : formatter -> unit -> unit
val underscore : formatter -> unit -> unit
val equal : formatter -> unit -> unit
val arrow : formatter -> unit -> unit
val lbrace : formatter -> unit -> unit
val rbrace : formatter -> unit -> unit
val lsquare : formatter -> unit -> unit
val rsquare : formatter -> unit -> unit
val lparen : formatter -> unit -> unit
val rparen : formatter -> unit -> unit
val lchevron : formatter -> unit -> unit
val rchevron : formatter -> unit -> unit
val nothing : formatter -> 'a -> unit
val string : formatter -> string -> unit
val float : formatter -> float -> unit
val int : formatter -> int -> unit
val constant_string : string -> formatter -> unit -> unit
val space : unit pp
val alt : unit pp
val alt2 : unit pp
val newline : unit pp
val newline2 : unit pp
val dot : unit pp
val comma : unit pp
val star : unit pp
val simple_comma : unit pp
val semi : unit pp
val colon : unit pp
val underscore : unit pp
val equal : unit pp
val arrow : unit pp
val lbrace : unit pp
val rbrace : unit pp
val lsquare : unit pp
val rsquare : unit pp
val lparen : unit pp
val rparen : unit pp
val lchevron : unit pp
val rchevron : unit pp
val nothing : 'a pp
val string : string pp
val float : float pp
val int : int pp
val constant_string : string -> unit pp
val formatted : formatter -> formatted -> unit
val constant_formatted : formatted -> formatter -> unit -> unit
val print0 : formatter -> unit -> unit
val hov : int -> (formatter -> 'a -> unit) -> formatter -> 'a -> unit
val indent : int -> (formatter -> 'a -> unit) -> formatter -> 'a -> unit
val constant_formatted : formatted -> unit pp
val print0 : unit pp
val hov : int -> 'a pp -> 'a pp
val indent : int -> 'a pp -> 'a pp
(** add the indentation at the first line *)
val add_flush : (formatter -> 'a -> unit) -> formatter -> 'a -> unit
val add_flush : 'a pp -> 'a pp
val asd : (formatter -> 'a -> unit) -> (formatter -> 'a -> unit)
val asd : 'a pp -> 'a pp
(** add string delimiter " " *)