printer.mli 5.37 KB
Newer Older
1 2 3
(********************************************************************)
(*                                                                  *)
(*  The Why3 Verification Platform   /   The Why3 Development Team  *)
MARCHE Claude's avatar
MARCHE Claude committed
4
(*  Copyright 2010-2017   --   INRIA - CNRS - Paris-Sud University  *)
5 6 7 8 9 10
(*                                                                  *)
(*  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 28 29 30
(* Makes it possible to estabilish traceability from names
in the output of the printer to elements of AST in its input. *)
type printer_mapping = {
  lsymbol_m     : string -> Term.lsymbol;
31
  vc_term_loc   : Loc.position option;
32
  (* The position of the term that triggers the VC *)
33
  queried_terms : Term.term Stdlib.Mstr.t;
34 35
  (* The list of terms that were queried for the counter-example
     by the printer *)
36 37
}

38 39 40 41 42
type printer_args = {
  env        : Env.env;
  prelude    : prelude;
  th_prelude : prelude_map;
  blacklist  : blacklist;
43
  mutable printer_mapping : printer_mapping;
44 45 46
}

type printer = printer_args -> ?old:in_channel -> task pp
47

48 49
val get_default_printer_mapping : printer_mapping

50
val register_printer : desc:Pp.formatted -> string -> printer -> unit
51 52 53

val lookup_printer : string -> printer

54
val list_printers : unit -> (string * Pp.formatted) list
55

Piotr Trojanek's avatar
Piotr Trojanek committed
56
(** {2 Use printers} *)
57 58 59 60

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

61 62
val meta_syntax_type : meta
val meta_syntax_logic : meta
63
val meta_syntax_converter : meta
Clément Fumex's avatar
Clément Fumex committed
64
val meta_syntax_literal : meta
65
val meta_remove_prop : meta
66
val meta_remove_logic : meta
Andrei Paskevich's avatar
Andrei Paskevich committed
67 68
val meta_remove_type : meta
val meta_realized_theory : meta
69

70 71 72
val syntax_type : tysymbol -> string -> bool -> tdecl
val syntax_logic : lsymbol -> string -> bool -> tdecl
val syntax_converter : lsymbol -> string -> bool -> tdecl
Clément Fumex's avatar
Clément Fumex committed
73
val syntax_literal : tysymbol -> string -> bool -> tdecl
74 75
val remove_prop : prsymbol -> tdecl

76 77 78
val check_syntax_type: tysymbol -> string -> unit
val check_syntax_logic: lsymbol -> string -> unit

79
type syntax_map = (string*int) Mid.t
80
(* [syntax_map] maps the idents of removed props to "" *)
81
type converter_map = (string*int) Mls.t
82

83
val get_syntax_map : task -> syntax_map
84
val add_syntax_map : tdecl -> syntax_map -> syntax_map
85 86 87
(* interprets a declaration as a syntax rule, if any *)

val get_converter_map : task -> converter_map
Clément Fumex's avatar
Clément Fumex committed
88 89 90

val get_rliteral_map : task -> syntax_map
val add_rliteral_map : tdecl -> syntax_map -> syntax_map
91

92
val query_syntax : syntax_map -> ident -> string option
93
val query_converter : converter_map -> lsymbol -> string option
94

95 96 97 98
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 *)

99 100 101
val gen_syntax_arguments_typed :
  ('a -> 'b) -> ('a -> 'b array) -> string -> 'a pp -> 'b pp -> 'a -> 'a list pp

102
val syntax_arguments_typed :
103
  string -> term pp -> ty pp -> term -> term list pp
104 105 106
(** (syntax_arguments templ print_arg fmt l) prints in the formatter fmt
     the list l using the template templ and the printer print_arg *)

Clément Fumex's avatar
Clément Fumex committed
107 108 109 110 111 112 113
val syntax_range_literal :
  string -> Number.integer_constant pp

val syntax_float_literal :
  string -> Number.float_format -> Number.real_constant pp

(** {2 pretty-printing transformations (useful for caching)} *)
114

115
val on_syntax_map : (syntax_map -> 'a Trans.trans) -> 'a Trans.trans
116

117 118
val on_converter_map : (converter_map -> 'a Trans.trans) -> 'a Trans.trans

119
val sprint_tdecl :
120
  ('a -> Format.formatter -> Theory.tdecl -> 'a * string list) ->
121 122 123
    Theory.tdecl -> 'a * string list -> 'a * string list

val sprint_decl :
124
  ('a -> Format.formatter -> Decl.decl -> 'a * string list) ->
125
    Theory.tdecl -> 'a * string list -> 'a * string list
126

Piotr Trojanek's avatar
Piotr Trojanek committed
127
(** {2 Exceptions to use in transformations and printers} *)
128 129

exception UnsupportedType of ty   * string
Andrei Paskevich's avatar
Andrei Paskevich committed
130
exception UnsupportedTerm of term * string
131 132 133
exception UnsupportedDecl of decl * string
exception NotImplemented  of        string

134 135
val unsupportedType : ty   -> string -> 'a
val unsupportedTerm : term -> string -> 'a
136
val unsupportedPattern : pattern -> string -> 'a
137 138
val unsupportedDecl : decl -> string -> 'a
val notImplemented  :         string -> 'a
139

Piotr Trojanek's avatar
Piotr Trojanek committed
140
(** {3 Functions that catch inner error} *)
141 142 143 144 145

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

146
val unsupported : string -> 'a
147 148 149 150 151 152 153 154 155 156 157 158 159

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] *)