pretty.mli 2.82 KB
Newer Older
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
1 2
(**************************************************************************)
(*                                                                        *)
Jean-Christophe Filliâtre's avatar
headers  
Jean-Christophe Filliâtre committed
3 4 5 6 7
(*  Copyright (C) 2010-                                                   *)
(*    Francois Bobot                                                      *)
(*    Jean-Christophe Filliatre                                           *)
(*    Johannes Kanig                                                      *)
(*    Andrei Paskevich                                                    *)
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
8 9 10 11 12 13 14 15 16 17 18 19 20
(*                                                                        *)
(*  This software is free software; you can redistribute it and/or        *)
(*  modify it under the terms of the GNU Library General Public           *)
(*  License version 2.1, with the special exception on linking            *)
(*  described in file LICENSE.                                            *)
(*                                                                        *)
(*  This software is distributed in the hope that it will be useful,      *)
(*  but WITHOUT ANY WARRANTY; without even the implied warranty of        *)
(*  MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE.                  *)
(*                                                                        *)
(**************************************************************************)

open Format
21
open Ident
22
open Ty
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
23
open Term
24
open Theory
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
25

26 27 28
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 *)
29

30 31 32 33 34 35 36 37 38
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_pr : formatter -> prop -> unit          (* proposition name *)

val print_ty : formatter -> ty -> unit            (* type *)
val print_vsty : formatter -> vsymbol -> unit     (* variable : type *)
39

40
val print_const : formatter -> constant -> unit   (* int/real constant *)
41 42 43
val print_pat : formatter -> pattern -> unit      (* pattern *)
val print_term : formatter -> term -> unit        (* term *)
val print_fmla : formatter -> fmla -> unit        (* formula *)
44

45 46 47
val print_type_decl : formatter -> ty_decl -> unit
val print_logic_decl : formatter -> logic_decl -> unit
val print_ind_decl : formatter -> ind_decl -> unit
48 49

val print_pkind : formatter -> prop_kind -> unit
50
val print_prop : formatter -> prop -> unit
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
51

52 53 54 55
val print_decl : formatter -> decl -> unit
val print_decls : formatter -> decl list -> unit
val print_context : formatter -> context -> unit
val print_theory : formatter -> theory -> unit
56

57
val print_named_context : formatter -> string -> context -> unit
58