Commit ee3a0d4d authored by Andrei Paskevich's avatar Andrei Paskevich

add a module for printers (borrow the code from Driver and Register)

parent 03e9767e
......@@ -95,7 +95,7 @@ LIBGENERATED = src/util/rc.ml \
LIB_UTIL = exn_printer pp loc print_tree hashweak hashcons util sysutil rc
LIB_CORE = ident ty term pattern decl theory task pretty trans env
LIB_CORE = ident ty term pattern decl theory task pretty env printer trans
LIB_PARSER = ptree parser lexer denv typing
......
......@@ -339,13 +339,6 @@ let print_inst fmt (id1,id2) =
else
fprintf fmt "ident %s = %s" id1.id_string id2.id_string
let print_meta_arg_type fmt = function
| MTtysymbol -> fprintf fmt "type_symbol"
| MTlsymbol -> fprintf fmt "logic_symbol"
| MTprsymbol -> fprintf fmt "proposition"
| MTstring -> fprintf fmt "string"
| MTint -> fprintf fmt "int"
let print_meta_arg fmt = function
| MARid id ->
if Hid.mem thash id then
......
......@@ -48,7 +48,6 @@ val print_expr : formatter -> expr -> unit (* term or formula *)
val print_pkind : formatter -> prop_kind -> unit
val print_meta_arg : formatter -> meta_arg_real -> unit
val print_meta_arg_type : formatter -> meta_arg_type -> unit
val print_type_decl : formatter -> ty_decl -> unit
val print_logic_decl : formatter -> logic_decl -> unit
......
(**************************************************************************)
(* *)
(* 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
type printer = prelude -> prelude_map -> task pp
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} *)
let print_prelude = print_list newline pp_print_string
let print_th_prelude task fmt pm =
let th_used = task_fold (fun acc -> function
| { td_node = Clone (th,cl) } when Mid.is_empty cl -> th::acc
| _ -> acc) [] task
in
List.iter (fun th ->
let prel = try Mid.find th.th_name pm with Not_found -> [] in
print_prelude fmt prel) th_used
let meta_remove_type = "remove_type"
let meta_remove_logic = "remove_logic"
let meta_remove_prop = "remove_prop"
let meta_syntax_type = "syntax_type"
let meta_syntax_logic = "syntax_logic"
let () =
register_meta meta_remove_type [MTtysymbol];
register_meta meta_remove_logic [MTlsymbol];
register_meta meta_remove_prop [MTprsymbol];
register_meta meta_syntax_type [MTtysymbol; MTstring];
register_meta meta_syntax_logic [MTlsymbol; MTstring]
let remove_type ts = create_meta meta_remove_type [MAts ts]
let remove_logic ls = create_meta meta_remove_logic [MAls ls]
let remove_prop pr = create_meta meta_remove_prop [MApr pr]
let syntax_type ts s =
check_syntax s (List.length ts.ts_args);
create_meta meta_syntax_type [MAts ts; MAstr s]
let syntax_logic ls s =
check_syntax s (List.length ls.ls_args);
create_meta meta_syntax_logic [MAls ls; MAstr s]
let get_remove_set task =
let add td s = match td.td_node with
| Meta (_,[MARid id]) -> Sid.add id s
| _ -> assert false
in
let s = Sid.empty in
let s = Stdecl.fold add (find_meta task meta_remove_type) s in
let s = Stdecl.fold add (find_meta task meta_remove_logic) s in
let s = Stdecl.fold add (find_meta task meta_remove_prop) s in
s
let get_syntax_map task =
let add td m = match td.td_node with
| Meta (_,[MARid id; MARstr s]) -> Mid.add id s m
| _ -> assert false
in
let m = Mid.empty in
let m = Stdecl.fold add (find_meta task meta_syntax_type) m in
let m = Stdecl.fold add (find_meta task meta_syntax_logic) m in
m
(** {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
| 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)
(**************************************************************************)
(* *)
(* 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 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
type printer = prelude -> prelude_map -> task pp
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
val meta_remove_type : string
val meta_remove_logic : string
val meta_remove_prop : string
val meta_syntax_type : string
val meta_syntax_logic : string
val remove_type : tysymbol -> tdecl
val remove_logic : lsymbol -> tdecl
val remove_prop : prsymbol -> tdecl
val syntax_type : tysymbol -> string -> tdecl
val syntax_logic : lsymbol -> string -> tdecl
val get_remove_set : task -> Sid.t
val get_syntax_map : task -> string Mid.t
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 *)
(** {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
val unsupportedType : ty -> string -> unit
val unsupportedTerm : term -> string -> unit
val unsupportedFmla : fmla -> string -> unit
val unsupportedExpr : expr -> string -> unit
val unsupportedDecl : decl -> string -> unit
val notImplemented : string -> unit
(** {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 *)
val unsupported : string -> unit
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_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] *)
......@@ -47,6 +47,9 @@ val task_known : task -> known_map
val task_clone : task -> clone_map
val task_meta : task -> meta_map
val find_clone : task -> theory -> Stdecl.t
val find_meta : task -> string -> Stdecl.t
(** {2 constructors} *)
val add_decl : task -> decl -> task
......
......@@ -112,7 +112,9 @@ let register_meta s al =
if Hashtbl.mem meta_table s then raise (KnownMeta s);
Hashtbl.add meta_table s al
let lookup_meta s = Hashtbl.find meta_table s
let lookup_meta s =
try Hashtbl.find meta_table s
with Not_found -> raise (UnknownMeta s)
let list_meta () = Hashtbl.fold (fun k _ acc -> k::acc) meta_table []
......@@ -682,6 +684,13 @@ let tuple_theory = Util.memo tuple_theory
(* Exception reporting *)
let print_meta_arg_type fmt = function
| MTtysymbol -> fprintf fmt "type_symbol"
| MTlsymbol -> fprintf fmt "logic_symbol"
| MTprsymbol -> fprintf fmt "proposition"
| MTstring -> fprintf fmt "string"
| MTint -> fprintf fmt "int"
let () = Exn_printer.register
begin fun fmt exn -> match exn with
| NonLocal id ->
......@@ -697,6 +706,17 @@ let () = Exn_printer.register
Format.fprintf fmt "No opened namespaces"
| ClashSymbol s ->
Format.fprintf fmt "Symbol %s is already defined in the current scope" s
| UnknownMeta s ->
Format.fprintf fmt "Unknown metaproperty %s" s
| KnownMeta s ->
Format.fprintf fmt "Metaproperty %s is already registered with \
a conflicting signature" s
| BadMetaArity (s,i1,i2) ->
Format.fprintf fmt "Metaproperty %s requires %d arguments but \
is applied to %d" s i1 i2
| MetaTypeMismatch (s,t1,t2) ->
Format.fprintf fmt "Metaproperty %s expects %a argument but \
is applied to %a" s print_meta_arg_type t1 print_meta_arg_type t2
| _ -> raise exn
end
Markdown is supported
0% or
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment