Commit 6fbfa827 authored by Andrei Paskevich's avatar Andrei Paskevich
Browse files

rename Ident.printer to ident_printer and Theory.Theory to TheoryUC

parent 6dfe0744
...@@ -70,7 +70,7 @@ let id_dup id = { id with id_tag = -1 } ...@@ -70,7 +70,7 @@ let id_dup id = { id with id_tag = -1 }
(** Unique names for pretty printing *) (** Unique names for pretty printing *)
type printer = type ident_printer =
(string, int) Hashtbl.t * (int, string) Hashtbl.t * (string -> string) (string, int) Hashtbl.t * (int, string) Hashtbl.t * (string -> string)
let rec find_index indices name ind = let rec find_index indices name ind =
...@@ -89,7 +89,7 @@ let find_unique indices name = ...@@ -89,7 +89,7 @@ let find_unique indices name =
let same x = x let same x = x
let create_printer ?(sanitizer = same) sl = let create_ident_printer ?(sanitizer = same) sl =
let indices = Hashtbl.create 1997 in let indices = Hashtbl.create 1997 in
let block n = ignore (find_unique indices n) in let block n = ignore (find_unique indices n) in
List.iter block sl; List.iter block sl;
......
...@@ -61,17 +61,19 @@ val id_dup : ident -> preid ...@@ -61,17 +61,19 @@ val id_dup : ident -> preid
(** Unique persistent names for pretty printing *) (** Unique persistent names for pretty printing *)
type printer type ident_printer
(* create new printing session with a sanitizing function and a blacklist *) (* start a new printer with a sanitizing function and a blacklist *)
val create_printer : ?sanitizer : (string -> string) -> string list -> printer val create_ident_printer :
?sanitizer : (string -> string) -> string list -> ident_printer
(* generate a unique name for ident in the printing session *) (* use ident_printer to generate a unique name for ident *)
(* an optional sanitizer is applied over the printer's sanitizer *) (* an optional sanitizer is applied over the printer's sanitizer *)
val id_unique : printer -> ?sanitizer : (string -> string) -> ident -> string val id_unique :
ident_printer -> ?sanitizer : (string -> string) -> ident -> string
(* forget an ident *) (* forget an ident *)
val forget_id : printer -> ident -> unit val forget_id : ident_printer -> ident -> unit
(* generic sanitizer taking a separate encoder for the first letter *) (* generic sanitizer taking a separate encoder for the first letter *)
val sanitizer : (char -> string) -> (char -> string) -> string -> string val sanitizer : (char -> string) -> (char -> string) -> string -> string
......
...@@ -34,7 +34,7 @@ let printer = ...@@ -34,7 +34,7 @@ let printer =
"let"; "in"; "match"; "with"; "as"; "epsilon" ] "let"; "in"; "match"; "with"; "as"; "epsilon" ]
in in
let sanitize = sanitizer char_to_alpha char_to_alnumus in let sanitize = sanitizer char_to_alpha char_to_alnumus in
create_printer bl ~sanitizer:sanitize create_ident_printer bl ~sanitizer:sanitize
let print_id fmt id = Format.fprintf fmt "%s" (id_unique printer id) let print_id fmt id = Format.fprintf fmt "%s" (id_unique printer id)
......
...@@ -727,7 +727,7 @@ type theory_uc = { ...@@ -727,7 +727,7 @@ type theory_uc = {
uc_local : Sid.t; uc_local : Sid.t;
} }
module Theory = struct module TheoryUC = struct
exception CloseTheory exception CloseTheory
exception NoOpenedNamespace exception NoOpenedNamespace
...@@ -888,7 +888,7 @@ end ...@@ -888,7 +888,7 @@ end
(** Debugging *) (** Debugging *)
let print_ident = let print_ident =
let printer = create_printer [] in let printer = create_ident_printer [] in
let print fmt id = Format.fprintf fmt "%s" (id_unique printer id) in let print fmt id = Format.fprintf fmt "%s" (id_unique printer id) in
print print
...@@ -904,7 +904,7 @@ let rec print_namespace fmt ns = ...@@ -904,7 +904,7 @@ let rec print_namespace fmt ns =
ns.ns_ns; ns.ns_ns;
fprintf fmt "@]" fprintf fmt "@]"
let print_uc fmt uc = print_namespace fmt (Theory.get_namespace uc) let print_uc fmt uc = print_namespace fmt (TheoryUC.get_namespace uc)
let print_ctxt fmt ctxt = let print_ctxt fmt ctxt =
fprintf fmt "@[<hov 2>ctxt : cloned : %a@]" fprintf fmt "@[<hov 2>ctxt : cloned : %a@]"
......
...@@ -176,7 +176,7 @@ val builtin_theory : theory ...@@ -176,7 +176,7 @@ val builtin_theory : theory
type theory_uc (* a theory under construction *) type theory_uc (* a theory under construction *)
module Theory : sig module TheoryUC : sig
val create_theory : preid -> theory_uc val create_theory : preid -> theory_uc
val close_theory : theory_uc -> theory val close_theory : theory_uc -> theory
......
...@@ -27,7 +27,7 @@ open Theory ...@@ -27,7 +27,7 @@ open Theory
let ident_printer = let ident_printer =
let bls = ["let"; "forall"; "exists"; "and"; "or"] in let bls = ["let"; "forall"; "exists"; "and"; "or"] in
let san = sanitizer char_to_alpha char_to_alnumus in let san = sanitizer char_to_alpha char_to_alnumus in
create_printer bls ~sanitizer:san create_ident_printer bls ~sanitizer:san
let print_ident fmt id = let print_ident fmt id =
fprintf fmt "%s" (id_unique ident_printer id) fprintf fmt "%s" (id_unique ident_printer id)
......
...@@ -25,8 +25,7 @@ open Ty ...@@ -25,8 +25,7 @@ open Ty
open Term open Term
open Ptree open Ptree
open Theory open Theory
open TheoryUC
open Theory
(** errors *) (** errors *)
...@@ -1153,7 +1152,7 @@ and add_decl env th = function ...@@ -1153,7 +1152,7 @@ and add_decl env th = function
close_namespace th true n close_namespace th true n
| Export -> | Export ->
use_or_clone th use_or_clone th
with Theory.ClashSymbol s -> with ClashSymbol s ->
error ~loc (Clash s) error ~loc (Clash s)
end end
| Namespace (_, import, name, dl) -> | Namespace (_, import, name, dl) ->
......
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