printer.ml 8.29 KB
Newer Older
1 2 3 4 5 6 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 34 35
(**************************************************************************)
(*                                                                        *)
(*  Copyright (C) 2010-                                                   *)
(*    Francois Bobot                                                      *)
(*    Jean-Christophe Filliatre                                           *)
(*    Johannes Kanig                                                      *)
(*    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 Format
open Pp
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 = formatter -> 'a -> unit

MARCHE Claude's avatar
MARCHE Claude committed
36
type printer = Env.env -> prelude -> prelude_map -> ?old:in_channel -> task pp
37 38 39 40 41 42 43 44 45 46 47 48 49 50 51 52 53 54 55 56 57 58 59 60 61 62 63 64 65 66 67 68 69 70 71 72 73 74 75 76 77 78 79 80 81 82 83 84 85 86 87 88 89 90 91 92 93 94 95 96 97 98 99 100 101 102 103 104 105 106 107 108 109

let printers : (string, printer) Hashtbl.t = Hashtbl.create 17

exception KnownPrinter of string
exception UnknownPrinter of string

let register_printer s p =
  if Hashtbl.mem printers s then raise (KnownPrinter s);
  Hashtbl.replace printers s p

let lookup_printer s =
  try Hashtbl.find printers s
  with Not_found -> raise (UnknownPrinter s)

let list_printers ()  = Hashtbl.fold (fun k _ acc -> k::acc) printers []

(** Syntax substitutions *)

let opt_search_forward re s pos =
  try Some (Str.search_forward re s pos) with Not_found -> None

let global_substitute_fmt expr repl_fun text fmt =
  let rec replace start last_was_empty =
    let startpos = if last_was_empty then start + 1 else start in
    if startpos > String.length text then
      pp_print_string fmt (Str.string_after text start)
    else
      match opt_search_forward expr text startpos with
      | None ->
          pp_print_string fmt (Str.string_after text start)
      | Some pos ->
          let end_pos = Str.match_end () in
          pp_print_string fmt (String.sub text start (pos - start));
          repl_fun text fmt;
          replace end_pos (end_pos = pos)
  in
  replace 0 false

let iter_group expr iter_fun text =
  let rec iter start last_was_empty =
    let startpos = if last_was_empty then start + 1 else start in
    if startpos < String.length text then
      match opt_search_forward expr text startpos with
      | None -> ()
      | Some pos ->
          let end_pos = Str.match_end () in
          iter_fun text;
          iter end_pos (end_pos = pos)
  in
  iter 0 false

let regexp_arg_pos = Str.regexp "%\\([0-9]+\\)"

exception BadSyntaxIndex of int
exception BadSyntaxArity of int * int

let check_syntax s len =
  let arg s =
    let i = int_of_string (Str.matched_group 1 s) in
    if i <= 0 then raise (BadSyntaxIndex i);
    if i > len then raise (BadSyntaxArity (len,i));
  in
  iter_group regexp_arg_pos arg s

let syntax_arguments s print fmt l =
  let args = Array.of_list l in
  let repl_fun s fmt =
    let i = int_of_string (Str.matched_group 1 s) in
    print fmt args.(i-1) in
  global_substitute_fmt regexp_arg_pos repl_fun s fmt

(** {2 use printers} *)

110
let print_prelude fmt pl =
111 112
  let println fmt s = fprintf fmt "%s@\n" s in
  print_list nothing println fmt pl
113 114 115

let print_th_prelude task fmt pm =
  let th_used = task_fold (fun acc -> function
116 117
    | { td_node = Clone (th,tm,lm,pm) }
      when Mts.is_empty tm && Mls.is_empty lm && Mpr.is_empty pm -> th::acc
118 119 120
    | _ -> acc) [] task
  in
  List.iter (fun th ->
121
    let prel = Mid.find_default th.th_name [] pm in
122 123
    print_prelude fmt prel) th_used

124 125 126
exception KnownTypeSyntax of tysymbol
exception KnownLogicSyntax of lsymbol

Andrei Paskevich's avatar
Andrei Paskevich committed
127 128 129 130 131
let meta_syntax_type  = register_meta "syntax_type" [MTtysymbol; MTstring]
let meta_syntax_logic = register_meta "syntax_logic" [MTlsymbol; MTstring]
let meta_remove_prop  = register_meta "remove_prop" [MTprsymbol]

let syntax_type ts s =
132
  check_syntax s (List.length ts.ts_args);
Andrei Paskevich's avatar
Andrei Paskevich committed
133
  create_meta meta_syntax_type [MAts ts; MAstr s]
134

Andrei Paskevich's avatar
Andrei Paskevich committed
135
let syntax_logic ls s =
136
  check_syntax s (List.length ls.ls_args);
Andrei Paskevich's avatar
Andrei Paskevich committed
137
  create_meta meta_syntax_logic [MAls ls; MAstr s]
138

Andrei Paskevich's avatar
Andrei Paskevich committed
139 140
let remove_prop pr =
  create_meta meta_remove_prop [MApr pr]
141

Andrei Paskevich's avatar
Andrei Paskevich committed
142 143 144
let get_syntax_map task =
  let add_ts td m = match td.td_node with
    | Meta (_,[MAts ts; MAstr s]) ->
145
        Mid.add_new ts.ts_name s (KnownTypeSyntax ts) m
Andrei Paskevich's avatar
Andrei Paskevich committed
146 147 148 149
    | _ -> assert false
  in
  let add_ls td m = match td.td_node with
    | Meta (_,[MAls ls; MAstr s]) ->
150
        Mid.add_new ls.ls_name s (KnownLogicSyntax ls) m
Andrei Paskevich's avatar
Andrei Paskevich committed
151 152 153 154 155 156
    | _ -> assert false
  in
  let m = Mid.empty in
  let m = Stdecl.fold add_ts (find_meta task meta_syntax_type).tds_set m in
  let m = Stdecl.fold add_ls (find_meta task meta_syntax_logic).tds_set m in
  m
157 158

let get_remove_set task =
159
  let add_ts td s = match td.td_node with
Andrei Paskevich's avatar
Andrei Paskevich committed
160
    | Meta (_,[MAts ts; _]) -> Sid.add ts.ts_name s
161 162 163
    | _ -> assert false
  in
  let add_ls td s = match td.td_node with
Andrei Paskevich's avatar
Andrei Paskevich committed
164
    | Meta (_,[MAls ls; _]) -> Sid.add ls.ls_name s
165 166 167 168
    | _ -> assert false
  in
  let add_pr td s = match td.td_node with
    | Meta (_,[MApr pr]) -> Sid.add pr.pr_name s
169 170 171
    | _ -> assert false
  in
  let s = Sid.empty in
Andrei Paskevich's avatar
Andrei Paskevich committed
172 173
  let s = Stdecl.fold add_ts (find_meta task meta_syntax_type).tds_set s in
  let s = Stdecl.fold add_ls (find_meta task meta_syntax_logic).tds_set s in
174
  let s = Stdecl.fold add_pr (find_meta task meta_remove_prop).tds_set s in
175 176
  s

177
let query_syntax sm id = Mid.find_option id sm
Andrei Paskevich's avatar
Andrei Paskevich committed
178

179 180 181 182 183 184 185 186 187 188 189 190 191 192 193 194 195 196 197 198 199 200 201 202 203 204 205 206 207 208 209 210 211 212 213 214 215 216
(** {2 exceptions to use in transformations and printers} *)

exception UnsupportedType of ty   * string
exception UnsupportedExpr of expr * string
exception UnsupportedDecl of decl * string
exception NotImplemented  of        string
exception Unsupported     of        string

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

let unsupportedType e s = raise (UnsupportedType (e,s))
let unsupportedTerm e s = raise (UnsupportedExpr (Term e,s))
let unsupportedFmla e s = raise (UnsupportedExpr (Fmla e,s))
let unsupportedExpr e s = raise (UnsupportedExpr (e,s))
let unsupportedDecl e s = raise (UnsupportedDecl (e,s))
let notImplemented    s = raise (NotImplemented s)
let unsupported       s = raise (Unsupported s)

let catch_unsupportedType f e =
  try f e with Unsupported s -> unsupportedType e s

let catch_unsupportedTerm f e =
  try f e with Unsupported s -> unsupportedTerm e s

let catch_unsupportedFmla f e =
  try f e with Unsupported s -> unsupportedFmla e s

let catch_unsupportedExpr f e =
  try f e with Unsupported s -> unsupportedExpr e s

let catch_unsupportedDecl f e =
  try f e with Unsupported s -> unsupportedDecl e s

let () = Exn_printer.register (fun fmt exn -> match exn with
  | KnownPrinter s ->
      fprintf fmt "Printer '%s' is already registered" s
  | UnknownPrinter s ->
      fprintf fmt "Unknown printer '%s'" s
217 218 219 220 221 222
  | KnownTypeSyntax ts ->
      fprintf fmt "Syntax for type symbol %a is already defined"
        Pretty.print_ts ts
  | KnownLogicSyntax ls ->
      fprintf fmt "Syntax for logical symbol %a is already defined"
        Pretty.print_ls ls
223 224 225 226 227 228 229 230 231 232 233 234 235 236 237 238 239 240 241
  | BadSyntaxIndex i ->
      fprintf fmt "Bad argument index %d, must start with 1" i
  | BadSyntaxArity (i1,i2) ->
      fprintf fmt "Bad argument index %d, must end with %d" i2 i1
  | Unsupported s ->
      fprintf fmt "@[<hov 3> Uncatched exception 'Unsupported %s'@]" s
  | UnsupportedType (e,s) ->
      fprintf fmt "@[<hov 3> This type isn't supported:@\n%a@\n%s@]"
        Pretty.print_ty e s
  | UnsupportedExpr (e,s) ->
      fprintf fmt "@[<hov 3> This expression isn't supported:@\n%a@\n%s@]"
        Pretty.print_expr e s
  | UnsupportedDecl (d,s) ->
      fprintf fmt "@[<hov 3> This declaration isn't supported:@\n%a@\n%s@]"
        Pretty.print_decl d s
  | NotImplemented (s) ->
      fprintf fmt "@[<hov 3> Unimplemented feature:@\n%s@]" s
  | e -> raise e)