printer.mli 6.26 KB
Newer Older
1 2 3
(********************************************************************)
(*                                                                  *)
(*  The Why3 Verification Platform   /   The Why3 Development Team  *)
Guillaume Melquiond's avatar
Guillaume Melquiond committed
4
(*  Copyright 2010-2019   --   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
open Wstdlib
13 14 15 16 17 18 19 20 21 22 23
open Ident
open Ty
open Term
open Decl
open Theory
open Task

(** Register printers *)

type prelude = string list
type prelude_map = prelude Mid.t
24 25
type interface = string list
type interface_map = interface Mid.t
26
type blacklist = string list
27

28 29 30 31
(* 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;
32
  vc_term_loc   : Loc.position option;
33
  (* The position of the term that triggers the VC *)
34
  queried_terms : Term.term Mstr.t;
35 36
  (* The list of terms that were queried for the counter-example
     by the printer *)
37 38 39
  list_projections: Ident.ident Mstr.t;
  (* List of projections as printed in the model. They corresponds to an ident
     which is kept so that we can approximate its used name in task. *)
DAILLER Sylvain's avatar
DAILLER Sylvain committed
40 41 42 43
  list_fields: Ident.ident Mstr.t;
  (* These corresponds to meta_record_def (tagged on field function definition).
     The difference with projections is that you are not allowed to reconstruct
     two projections into a record (at counterexample parsing level). *)
44
  list_records: ((string * string) list) Mstr.t;
45 46
  (* List of constructors with no arguments that can be confused for variables
     during parsing. *)
47 48 49 50 51
  noarg_constructors: string list;
  (* List of attributes corresponding to a printed constants (that was on the
     immediate term, not inside the ident) *)
  set_str: Sattr.t Mstr.t

52 53
}

54 55 56 57 58
type printer_args = {
  env        : Env.env;
  prelude    : prelude;
  th_prelude : prelude_map;
  blacklist  : blacklist;
59
  mutable printer_mapping : printer_mapping;
60 61
}

62
type printer = printer_args -> ?old:in_channel -> task Pp.pp
63

64 65
val get_default_printer_mapping : printer_mapping

66
val register_printer : desc:Pp.formatted -> string -> printer -> unit
67 68 69

val lookup_printer : string -> printer

70
val list_printers : unit -> (string * Pp.formatted) list
71

Piotr Trojanek's avatar
Piotr Trojanek committed
72
(** {2 Use printers} *)
73

74 75
val print_prelude : prelude Pp.pp
val print_th_prelude : task -> prelude_map Pp.pp
76
val print_interface : interface Pp.pp
77

78 79
val meta_syntax_type : meta
val meta_syntax_logic : meta
Clément Fumex's avatar
Clément Fumex committed
80
val meta_syntax_literal : meta
81
val meta_remove_prop : meta
82
val meta_remove_logic : meta
Andrei Paskevich's avatar
Andrei Paskevich committed
83 84
val meta_remove_type : meta
val meta_realized_theory : meta
85

86 87
val syntax_type : tysymbol -> string -> bool -> tdecl
val syntax_logic : lsymbol -> string -> bool -> tdecl
Clément Fumex's avatar
Clément Fumex committed
88
val syntax_literal : tysymbol -> string -> bool -> tdecl
89 90
val remove_prop : prsymbol -> tdecl

91 92 93
val check_syntax_type: tysymbol -> string -> unit
val check_syntax_logic: lsymbol -> string -> unit

94
type syntax_map = (string*int) Mid.t
95
(* [syntax_map] maps the idents of removed props to "" *)
96

97
val get_syntax_map : task -> syntax_map
98
val add_syntax_map : tdecl -> syntax_map -> syntax_map
99 100
(* interprets a declaration as a syntax rule, if any *)

Clément Fumex's avatar
Clément Fumex committed
101 102
val get_rliteral_map : task -> syntax_map
val add_rliteral_map : tdecl -> syntax_map -> syntax_map
103

104
val query_syntax : syntax_map -> ident -> string option
105

106 107 108 109 110
val syntax_arguments_prec : string -> (int -> 'a Pp.pp) -> int list -> 'a list Pp.pp
(** (syntax_arguments_prec templ print_arg prec_list fmt l) prints in the formatter
     fmt the list l using the template templ, the printer print_arg, and the
     precedence list prec_list *)

111
val syntax_arguments : string -> 'a Pp.pp -> 'a list Pp.pp
112

113 114 115 116 117 118 119 120 121
val gen_syntax_arguments_typed_prec :
  ('a -> 'b) -> ('a -> 'b array) -> string -> (int -> 'a Pp.pp)
  -> 'b Pp.pp -> 'a -> int list -> 'a list Pp.pp

val syntax_arguments_typed_prec :
  string -> (int -> term Pp.pp) -> ty Pp.pp -> term -> int list -> term list Pp.pp
(** (syntax_arguments_typed templ print_arg prec_list fmt l) prints in the
    formatter fmt the list l using the template templ, the printer print_arg
    and the precedence list prec_list  *)
122

123
val syntax_arguments_typed :
124
  string -> term Pp.pp -> ty Pp.pp -> term -> term list Pp.pp
125

Clément Fumex's avatar
Clément Fumex committed
126
val syntax_range_literal :
127
  string -> Number.int_constant Pp.pp
Clément Fumex's avatar
Clément Fumex committed
128 129

val syntax_float_literal :
130
  string -> Number.float_format -> Number.real_constant Pp.pp
Clément Fumex's avatar
Clément Fumex committed
131 132

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

134
val on_syntax_map : (syntax_map -> 'a Trans.trans) -> 'a Trans.trans
135

136
val sprint_tdecl :
137
  ('a -> Format.formatter -> Theory.tdecl -> 'a * string list) ->
138 139 140
    Theory.tdecl -> 'a * string list -> 'a * string list

val sprint_decl :
141
  ('a -> Format.formatter -> Decl.decl -> 'a * string list) ->
142
    Theory.tdecl -> 'a * string list -> 'a * string list
143

Piotr Trojanek's avatar
Piotr Trojanek committed
144
(** {2 Exceptions to use in transformations and printers} *)
145 146

exception UnsupportedType of ty   * string
147
exception UnsupportedTerm of term * string
148 149 150
exception UnsupportedDecl of decl * string
exception NotImplemented  of        string

151 152
val unsupportedType : ty   -> string -> 'a
val unsupportedTerm : term -> string -> 'a
153
val unsupportedPattern : pattern -> string -> 'a
154 155
val unsupportedDecl : decl -> string -> 'a
val notImplemented  :         string -> 'a
156

Piotr Trojanek's avatar
Piotr Trojanek committed
157
(** {3 Functions that catch inner error} *)
158 159 160 161 162

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

163
val unsupported : string -> 'a
164 165 166 167 168 169 170 171 172 173 174 175 176

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