printer.mli 4.57 KB
Newer Older
1 2 3
(**************************************************************************)
(*                                                                        *)
(*  Copyright (C) 2010-                                                   *)
MARCHE Claude's avatar
MARCHE Claude committed
4 5 6
(*    François Bobot                                                     *)
(*    Jean-Christophe Filliâtre                                          *)
(*    Claude Marché                                                      *)
7 8 9 10 11 12 13 14 15 16 17 18 19 20 21 22 23 24 25 26 27 28 29 30 31 32 33
(*    Andrei Paskevich                                                    *)
(*                                                                        *)
(*  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 Ident
open Ty
open Term
open Decl
open Theory
open Task

(** Register printers *)

type prelude = string list
type prelude_map = prelude Mid.t

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

MARCHE Claude's avatar
MARCHE Claude committed
34
type printer = Env.env -> prelude -> prelude_map -> ?old:in_channel -> task pp
35 36 37 38 39 40 41 42 43 44 45

val register_printer : string -> printer -> unit

val lookup_printer : string -> printer

val list_printers : unit -> string list

(** {2 use printers} *)

val print_prelude : prelude pp
val print_th_prelude : task -> prelude_map pp
46
val print_prelude_for_theory : theory -> prelude_map pp
47

48 49
val meta_syntax_type : meta
val meta_syntax_logic : meta
50
val meta_remove_prop : meta
51

52 53
val syntax_type : tysymbol -> string -> tdecl
val syntax_logic : lsymbol -> string -> tdecl
54 55
val remove_prop : prsymbol -> tdecl

56
val get_syntax_map : task -> string Mid.t
57
val get_remove_set : task -> Sid.t
58

59 60
val get_syntax_map_of_theory : theory -> string Mid.t

61
val query_syntax : string Mid.t -> ident -> string option
62

63 64 65 66
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 *)

67 68 69 70 71 72
val syntax_arguments_typed : string -> term pp -> ty pp ->
  term option -> term 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 *)


73 74
(** {2 exceptions to use in transformations and printers} *)

75
exception UnsupportedTysymbol   of tysymbol   * string
76 77 78 79 80
exception UnsupportedType of ty   * string
exception UnsupportedExpr of expr * string
exception UnsupportedDecl of decl * string
exception NotImplemented  of        string

81
val unsupportedTysymbol   : tysymbol   -> string -> 'a
82 83 84 85 86 87
val unsupportedType : ty   -> string -> 'a
val unsupportedTerm : term -> string -> 'a
val unsupportedFmla : fmla -> string -> 'a
val unsupportedExpr : expr -> string -> 'a
val unsupportedDecl : decl -> string -> 'a
val notImplemented  :         string -> 'a
88 89 90 91 92 93 94

(** {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 *)

95
val unsupported : string -> 'a
96 97 98 99 100 101

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

102 103 104 105 106

val catch_unsupportedTysymbol : (tysymbol -> 'a) -> (tysymbol -> 'a)
(** same as {! catch_unsupportedType} but use [UnsupportedTysymbol]
    instead of [UnsupportedType]*)

107 108 109 110 111 112 113 114 115 116 117 118 119 120 121 122
val catch_unsupportedTerm : (term -> 'a) -> (term -> 'a)
(** same as {! catch_unsupportedType} but use [UnsupportedExpr]
    instead of [UnsupportedType]*)

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

val catch_unsupportedExpr : (expr -> 'a) -> (expr -> '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] *)