printer.mli 3.83 KB
Newer Older
1 2 3 4 5 6 7 8 9 10
(********************************************************************)
(*                                                                  *)
(*  The Why3 Verification Platform   /   The Why3 Development Team  *)
(*  Copyright 2010-2012   --   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.                           *)
(*                                                                  *)
(********************************************************************)
11 12 13 14 15 16 17 18 19 20 21 22

open Ident
open Ty
open Term
open Decl
open Theory
open Task

(** Register printers *)

type prelude = string list
type prelude_map = prelude Mid.t
23
type blacklist = string list
24 25 26

type 'a pp = Format.formatter -> 'a -> unit

27
type printer =
28
  Env.env -> prelude -> prelude_map -> blacklist -> ?old:in_channel -> task pp
29

30
val register_printer : desc:Pp.formatted -> string -> printer -> unit
31 32 33

val lookup_printer : string -> printer

34
val list_printers : unit -> (string * Pp.formatted) list
35 36 37 38 39 40

(** {2 use printers} *)

val print_prelude : prelude pp
val print_th_prelude : task -> prelude_map pp

41 42
val meta_syntax_type : meta
val meta_syntax_logic : meta
43
val meta_remove_prop : meta
44
val meta_remove_logic : meta
Andrei Paskevich's avatar
Andrei Paskevich committed
45 46
val meta_remove_type : meta
val meta_realized_theory : meta
47

48 49
val syntax_type : tysymbol -> string -> tdecl
val syntax_logic : lsymbol -> string -> tdecl
50 51
val remove_prop : prsymbol -> tdecl

52 53 54
val check_syntax_type: tysymbol -> string -> unit
val check_syntax_logic: lsymbol -> string -> unit

55 56
type syntax_map = string Mid.t
(* [syntax_map] maps the idents of removed props to "" *)
57

58
val get_syntax_map : task -> syntax_map
59 60
val add_syntax_map : tdecl -> syntax_map -> syntax_map
  (* interprets a declaration as a syntax rule, if any *)
61

62
val query_syntax : syntax_map -> ident -> string option
63

64 65 66 67
val syntax_arguments : string -> 'a pp -> 'a list 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 *)

68
val syntax_arguments_typed :
69
  string -> term pp -> ty pp -> term -> term list pp
70 71 72
(** (syntax_arguments templ print_arg fmt l) prints in the formatter fmt
     the list l using the template templ and the printer print_arg *)

73 74 75 76 77 78
(** {2 pretty-printing transformations (useful for caching)} *)

val fold_tdecls : (syntax_map -> tdecl -> 'a -> 'a) -> 'a -> 'a Trans.trans

val sprint_tdecls : (syntax_map -> tdecl pp) -> string list Trans.trans
val sprint_decls  : (syntax_map -> decl  pp) -> string list Trans.trans
79

80 81 82
(** {2 exceptions to use in transformations and printers} *)

exception UnsupportedType of ty   * string
Andrei Paskevich's avatar
Andrei Paskevich committed
83
exception UnsupportedTerm of term * string
84 85 86
exception UnsupportedDecl of decl * string
exception NotImplemented  of        string

87 88 89 90
val unsupportedType : ty   -> string -> 'a
val unsupportedTerm : term -> string -> 'a
val unsupportedDecl : decl -> string -> 'a
val notImplemented  :         string -> 'a
91 92 93 94 95 96 97

(** {3 functions that catch inner error} *)

exception Unsupported of string
(** This exception must be raised only inside a call
    of one of the catch_* functions below *)

98
val unsupported : string -> 'a
99 100 101 102 103 104 105 106 107 108 109 110 111 112

val catch_unsupportedType : (ty -> 'a) -> (ty -> 'a)
(** [catch_unsupportedType f] return a function which applied on [arg]:
    - return [f arg] if [f arg] does not raise {!Unsupported} exception
    - raise [UnsupportedType (arg,s)] if [f arg] raises [Unsupported s]*)

val catch_unsupportedTerm : (term -> 'a) -> (term -> 'a)
(** same as {! catch_unsupportedType} but use [UnsupportedExpr]
    instead of [UnsupportedType]*)

val catch_unsupportedDecl : (decl -> 'a) -> (decl -> 'a)
(** same as {! catch_unsupportedType} but use [UnsupportedDecl]
    instead of [UnsupportedType] *)