Commit b0cef7e3 authored by Andrei Paskevich's avatar Andrei Paskevich

s/label/attribute/g

parent 87e9ce01
......@@ -27,7 +27,7 @@ open Ptree
(* start a module *)
(* BEGIN{openmodule} *)
let () = Typing.open_file env [] (* empty pathname *)
let mk_ident s = { id_str = s; id_lab=[]; id_loc = Loc.dummy_position }
let mk_ident s = { id_str = s; id_ats=[]; id_loc = Loc.dummy_position }
let m = Typing.open_module (mk_ident "Program")
(* END{openmodule} *)
......
......@@ -25,7 +25,7 @@ let () = Debug.set_flag Dterm.debug_ignore_unused_var
*)
let mk_id ~loc name =
{ id_str = name; id_lab = []; id_loc = loc }
{ id_str = name; id_ats = []; id_loc = loc }
let infix ~loc s = Qident (mk_id ~loc (Ident.infix s))
let prefix ~loc s = Qident (mk_id ~loc (Ident.prefix s))
......@@ -286,7 +286,7 @@ and block env ~loc = function
| [] ->
mk_unit ~loc
| Dstmt { stmt_loc = loc; stmt_desc = Slabel id } :: sl ->
mk_expr ~loc (Emark (id, block env ~loc sl))
mk_expr ~loc (Elabel (id, block env ~loc sl))
| Dstmt { Py_ast.stmt_loc = loc; stmt_desc = Py_ast.Sassign (id, e) } :: sl
when not (Mstr.mem id.id_str env.vars) ->
let e = expr env e in (* check e *before* adding id to environment *)
......@@ -325,7 +325,7 @@ and block env ~loc = function
let fresh_type_var =
let r = ref 0 in
fun loc -> incr r;
PTtyvar { id_str = "a" ^ string_of_int !r; id_loc = loc; id_lab = [] }
PTtyvar { id_str = "a" ^ string_of_int !r; id_loc = loc; id_ats = [] }
let logic_param id =
id.id_loc, Some id, false, fresh_type_var id.id_loc
......
......@@ -19,7 +19,7 @@
| _ -> raise exn)
let floc s e = Loc.extract (s,e)
let mk_id id s e = { id_str = id; id_lab = []; id_loc = floc s e }
let mk_id id s e = { id_str = id; id_ats = []; id_loc = floc s e }
let mk_pat d s e = { pat_desc = d; pat_loc = floc s e }
let mk_term d s e = { term_desc = d; term_loc = floc s e }
let mk_expr loc d = { expr_desc = d; expr_loc = loc }
......
......@@ -219,7 +219,7 @@ and dterm_node =
| DTfalse
| DTcast of dterm * dty
| DTuloc of dterm * Loc.position
| DTlabel of dterm * Slab.t
| DTattr of dterm * Sattr.t
(** Unification tools *)
......@@ -330,14 +330,14 @@ let dpattern ?loc node =
let dty, vars = Loc.try1 ?loc get_dty node in
{ dp_node = node; dp_dty = dty; dp_vars = vars; dp_loc = loc }
let slab_coercion = Slab.singleton Pretty.label_coercion
let coercion_attrs = Sattr.singleton Pretty.coercion_attr
let apply_coercion l ({dt_loc = loc} as dt) =
let apply dt ls =
let dtyl, dty = specialize_ls ls in
dterm_expected_type dt (List.hd dtyl);
let dt = { dt_node = DTapp (ls, [dt]); dt_dty = dty; dt_loc = loc } in
{ dt with dt_node = DTlabel (dt, slab_coercion) } in
{ dt with dt_node = DTattr (dt, coercion_attrs) } in
List.fold_left apply dt l
(* coercions using just head tysymbols without type arguments: *)
......@@ -491,7 +491,7 @@ let dterm crcmap ?loc node =
| DTcast (dt,dty) ->
dterm_expected_dterm crcmap dt dty
| DTuloc (dt,_)
| DTlabel (dt,_) ->
| DTattr (dt,_) ->
mk_dty (dt.dt_dty)
in Loc.try1 ?loc (dterm_node loc) node
......@@ -569,32 +569,32 @@ let check_used_var t vs =
let check_exists_implies f = match f.t_node with
| Tbinop (Timplies,{ t_node = Tbinop (Tor,f,{ t_node = Ttrue }) },_)
when Slab.mem Term.asym_split f.t_label -> ()
when Sattr.mem Term.asym_split f.t_attrs -> ()
| Tbinop (Timplies,_,_) -> Warning.emit ?loc:f.t_loc
"form \"exists x. P -> Q\" is likely an error (use \"not P \\/ Q\" if not)"
| _ -> ()
let t_label loc labs t =
if loc = None && Slab.is_empty labs
then t else t_label ?loc labs t
let t_attr_set loc attrs t =
if loc = None && Sattr.is_empty attrs
then t else t_attr_set ?loc attrs t
let rec strip uloc labs dt = match dt.dt_node with
| DTcast (dt,_) -> strip uloc labs dt
| DTuloc (dt,loc) -> strip (Some loc) labs dt
| DTlabel (dt,s) -> strip uloc (Slab.union labs s) dt
| _ -> uloc, labs, dt
let rec strip uloc attrs dt = match dt.dt_node with
| DTcast (dt,_) -> strip uloc attrs dt
| DTuloc (dt,loc) -> strip (Some loc) attrs dt
| DTattr (dt,s) -> strip uloc (Sattr.union attrs s) dt
| _ -> uloc, attrs, dt
let rec term ~strict ~keep_loc uloc env prop dt =
let uloc, labs, dt = strip uloc Slab.empty dt in
let uloc, attrs, dt = strip uloc Sattr.empty dt in
let tloc = if keep_loc then dt.dt_loc else None in
let tloc = if uloc <> None then uloc else tloc in
let t = Loc.try7 ?loc:dt.dt_loc
try_term strict keep_loc uloc env prop dt.dt_dty dt.dt_node in
let t = t_label tloc labs t in
let t = t_attr_set tloc attrs t in
match t.t_ty with
| Some _ when prop -> t_label tloc Slab.empty
| Some _ when prop -> t_attr_set tloc Sattr.empty
(Loc.try2 ?loc:dt.dt_loc t_equ t t_bool_true)
| None when not prop -> t_label tloc Slab.empty
| None when not prop -> t_attr_set tloc Sattr.empty
(t_if t t_bool_true t_bool_false)
| _ -> t
......@@ -677,13 +677,13 @@ and try_term strict keep_loc uloc env prop dty node =
t_iff (get env true df1) (get env true df2)
| DTbinop (DTby,df1,df2) ->
let t2 = get env true df2 in
let tt = t_label t2.t_loc Slab.empty t_true in
let t2 = t_label t2.t_loc Slab.empty (t_or_asym t2 tt) in
let tt = t_attr_set t2.t_loc Sattr.empty t_true in
let t2 = t_attr_set t2.t_loc Sattr.empty (t_or_asym t2 tt) in
t_implies t2 (get env true df1)
| DTbinop (DTso,df1,df2) ->
let t2 = get env true df2 in
let tt = t_label t2.t_loc Slab.empty t_true in
let t2 = t_label t2.t_loc Slab.empty (t_or_asym t2 tt) in
let tt = t_attr_set t2.t_loc Sattr.empty t_true in
let t2 = t_attr_set t2.t_loc Sattr.empty (t_or_asym t2 tt) in
t_and (get env true df1) t2
| DTnot df ->
t_not (get env true df)
......@@ -691,7 +691,7 @@ and try_term strict keep_loc uloc env prop dty node =
if prop then t_true else t_bool_true
| DTfalse ->
if prop then t_false else t_bool_false
| DTcast _ | DTuloc _ | DTlabel _ ->
| DTcast _ | DTuloc _ | DTattr _ ->
assert false (* already stripped *)
let fmla ?(strict=true) ?(keep_loc=true) dt =
......
......@@ -83,7 +83,7 @@ and dterm_node =
| DTfalse
| DTcast of dterm * dty
| DTuloc of dterm * Loc.position
| DTlabel of dterm * Slab.t
| DTattr of dterm * Sattr.t
(** Environment *)
......
......@@ -11,41 +11,41 @@
open Wstdlib
(** Labels *)
(** Attributes *)
type label = {
lab_string : string;
lab_tag : int;
type attribute = {
attr_string : string;
attr_tag : int;
}
module Lab = MakeMSH (struct
type t = label
let tag lab = lab.lab_tag
module Attr = MakeMSH (struct
type t = attribute
let tag a = a.attr_tag
end)
module Slab = Lab.S
module Mlab = Lab.M
module Sattr = Attr.S
module Mattr = Attr.M
module Hslab = Hashcons.Make (struct
type t = label
let equal lab1 lab2 = lab1.lab_string = lab2.lab_string
let hash lab = Hashtbl.hash lab.lab_string
let tag n lab = { lab with lab_tag = n }
module Hsattr = Hashcons.Make (struct
type t = attribute
let equal a1 a2 = a1.attr_string = a2.attr_string
let hash a = Hashtbl.hash a.attr_string
let tag n a = { a with attr_tag = n }
end)
let create_label s = Hslab.hashcons {
lab_string = s;
lab_tag = -1
let create_attribute s = Hsattr.hashcons {
attr_string = s;
attr_tag = -1
}
let list_label () =
let list_attributes () =
let acc = ref [] in
Hslab.iter (fun label -> acc := label.lab_string :: !acc);
Hsattr.iter (fun a -> acc := a.attr_string :: !acc);
!acc
let lab_equal : label -> label -> bool = (==)
let lab_hash lab = lab.lab_tag
let lab_compare l1 l2 = Pervasives.compare l1.lab_tag l2.lab_tag
let attr_equal : attribute -> attribute -> bool = (==)
let attr_hash a = a.attr_tag
let attr_compare a1 a2 = Pervasives.compare a1.attr_tag a2.attr_tag
(** Naming convention *)
......@@ -69,7 +69,7 @@ let kind_of_fix s =
type ident = {
id_string : string; (* non-unique name *)
id_label : Slab.t; (* identifier labels *)
id_attrs : Sattr.t; (* identifier attributes *)
id_loc : Loc.position option; (* optional location *)
id_tag : Weakhtbl.tag; (* unique magical tag *)
}
......@@ -86,7 +86,7 @@ module Wid = Id.W
type preid = {
pre_name : string;
pre_label : Slab.t;
pre_attrs : Sattr.t;
pre_loc : Loc.position option;
}
......@@ -98,33 +98,33 @@ let id_compare id1 id2 = Pervasives.compare (id_hash id1) (id_hash id2)
let id_register = let r = ref 0 in fun id -> {
id_string = id.pre_name;
id_label = id.pre_label;
id_attrs = id.pre_attrs;
id_loc = id.pre_loc;
id_tag = (incr r; Weakhtbl.create_tag !r);
}
let create_ident name labels loc = {
let create_ident name attrs loc = {
pre_name = name;
pre_label = labels;
pre_attrs = attrs;
pre_loc = loc;
}
let id_fresh ?(label = Slab.empty) ?loc nm =
create_ident nm label loc
let id_fresh ?(attrs = Sattr.empty) ?loc nm =
create_ident nm attrs loc
let id_user ?(label = Slab.empty) nm loc =
create_ident nm label (Some loc)
let id_user ?(attrs = Sattr.empty) nm loc =
create_ident nm attrs (Some loc)
let id_lab label id =
create_ident id.id_string label id.id_loc
let id_attr id attrs =
create_ident id.id_string attrs id.id_loc
let id_clone ?(label = Slab.empty) id =
let ll = Slab.union label id.id_label in
create_ident id.id_string ll id.id_loc
let id_clone ?(attrs = Sattr.empty) id =
let aa = Sattr.union attrs id.id_attrs in
create_ident id.id_string aa id.id_loc
let id_derive ?(label = Slab.empty) nm id =
let ll = Slab.union label id.id_label in
create_ident nm ll id.id_loc
let id_derive ?(attrs = Sattr.empty) nm id =
let aa = Sattr.union attrs id.id_attrs in
create_ident nm aa id.id_loc
let preid_name id = id.pre_name
......@@ -261,54 +261,54 @@ let sanitizer' head rest last n =
let sanitizer head rest n = sanitizer' head rest rest n
(** {2 functions for working with counterexample model labels} *)
(** {2 functions for working with counterexample attributes} *)
let model_label = create_label "model"
let model_projected_label = create_label "model_projected"
let model_vc_label = create_label "model_vc"
let model_vc_post_label = create_label "model_vc_post"
let model_vc_havoc_label = create_label "model_vc_havoc"
let model_attr = create_attribute "model"
let model_projected_attr = create_attribute "model_projected"
let model_vc_attr = create_attribute "model_vc"
let model_vc_post_attr = create_attribute "model_vc_post"
let model_vc_havoc_attr = create_attribute "model_vc_havoc"
let create_model_trace_label s = create_label ("model_trace:" ^ s)
let create_model_trace_attr s = create_attribute ("model_trace:" ^ s)
let is_counterexample_label l =
l = model_label || l = model_projected_label
let is_counterexample_attr l =
l = model_attr || l = model_projected_attr
let has_a_model_label id =
Slab.exists is_counterexample_label id.id_label
let has_a_model_attr id =
Sattr.exists is_counterexample_attr id.id_attrs
let remove_model_labels ~labels =
Slab.filter (fun l -> not (is_counterexample_label l)) labels
let remove_model_attrs ~attrs =
Sattr.filter (fun l -> not (is_counterexample_attr l)) attrs
let is_model_trace_label label =
Strings.has_prefix "model_trace:" label.lab_string
let is_model_trace_attr a =
Strings.has_prefix "model_trace:" a.attr_string
let get_model_trace_label ~labels =
Slab.choose (Slab.filter is_model_trace_label labels)
let get_model_trace_attr ~attrs =
Sattr.choose (Sattr.filter is_model_trace_attr attrs)
let transform_model_trace_label labels trans_fun =
let transform_model_trace_attr attrs trans_fun =
try
let trace_label = get_model_trace_label ~labels in
let labels_without_trace = Slab.remove trace_label labels in
let new_trace_label = create_label (trans_fun trace_label.lab_string) in
Slab.add new_trace_label labels_without_trace
with Not_found -> labels
let append_to_model_element_name ~labels ~to_append =
let trans lab_str =
let splitted = Strings.bounded_split '@' lab_str 2 in
let trace_attr = get_model_trace_attr ~attrs in
let attrs_without_trace = Sattr.remove trace_attr attrs in
let new_trace_attr = create_attribute (trans_fun trace_attr.attr_string) in
Sattr.add new_trace_attr attrs_without_trace
with Not_found -> attrs
let append_to_model_element_name ~attrs ~to_append =
let trans attr_str =
let splitted = Strings.bounded_split '@' attr_str 2 in
match splitted with
| [before; after] -> before ^ to_append ^ "@" ^ after
| _ -> lab_str^to_append in
transform_model_trace_label labels trans
| _ -> attr_str^to_append in
transform_model_trace_attr attrs trans
let append_to_model_trace_label ~labels ~to_append =
let trans lab_str = lab_str ^ to_append in
transform_model_trace_label labels trans
let append_to_model_trace_attr ~attrs ~to_append =
let trans attr_str = attr_str ^ to_append in
transform_model_trace_attr attrs trans
let get_model_element_name ~labels =
let trace_label = get_model_trace_label ~labels in
let splitted1 = Strings.bounded_split ':' trace_label.lab_string 2 in
let get_model_element_name ~attrs =
let trace_attr = get_model_trace_attr ~attrs in
let splitted1 = Strings.bounded_split ':' trace_attr.attr_string 2 in
match splitted1 with
| [_; content] ->
begin
......@@ -321,41 +321,41 @@ let get_model_element_name ~labels =
| [_] -> ""
| _ -> assert false
let get_model_trace_string ~labels =
let tl = get_model_trace_label ~labels in
let splitted = Strings.bounded_split ':' tl.lab_string 2 in
let get_model_trace_string ~attrs =
let tl = get_model_trace_attr ~attrs in
let splitted = Strings.bounded_split ':' tl.attr_string 2 in
match splitted with
| [_; t_str] -> t_str
| _ -> ""
(* Functions for working with ITP labels *)
(* Functions for working with ITP attributes *)
let is_name_label label =
Strings.has_prefix "name:" label.lab_string
let is_name_attr a =
Strings.has_prefix "name:" a.attr_string
let get_name_label ~labels =
try Some (Slab.choose (Slab.filter is_name_label labels))
let get_name_attr ~attrs =
try Some (Sattr.choose (Sattr.filter is_name_attr attrs))
with Not_found -> None
let get_element_name ~labels =
match get_name_label ~labels with
let get_element_name ~attrs =
match get_name_attr ~attrs with
| None -> None
| Some name_label ->
let splitted1 = Strings.bounded_split ':' name_label.lab_string 2 in
| Some name_attr ->
let splitted1 = Strings.bounded_split ':' name_attr.attr_string 2 in
let correct_word = Str.regexp "^\\([A-Za-z]+\\)\\([A-Za-z0-9_']*\\)$" in
match splitted1 with
| ["name"; content] when Str.string_match correct_word content 0 ->
Some content
| _ -> None
let id_unique_label printer ?(sanitizer = same) id =
let id_unique_attr printer ?(sanitizer = same) id =
try
Hid.find printer.values id
with Not_found ->
let labels = id.id_label in
let attrs = id.id_attrs in
let name =
match (get_element_name ~labels) with
match (get_element_name ~attrs) with
| Some x -> x
| None -> printer.sanitizer id.id_string
in
......
......@@ -11,23 +11,23 @@
(** Identifiers *)
(** {2 Labels} *)
(** {2 Attributes} *)
type label = private {
lab_string : string;
lab_tag : int;
type attribute = private {
attr_string : string;
attr_tag : int;
}
module Mlab : Extmap.S with type key = label
module Slab : Extset.S with module M = Mlab
module Mattr : Extmap.S with type key = attribute
module Sattr : Extset.S with module M = Mattr
val lab_compare : label -> label -> int
val lab_equal : label -> label -> bool
val lab_hash : label -> int
val attr_compare : attribute -> attribute -> int
val attr_equal : attribute -> attribute -> bool
val attr_hash : attribute -> int
val create_label : string -> label
val create_attribute : string -> attribute
val list_label: unit -> string list
val list_attributes : unit -> string list
(** {2 Naming convention } *)
......@@ -49,7 +49,7 @@ val kind_of_fix: string -> [ `None
type ident = private {
id_string : string; (** non-unique name *)
id_label : Slab.t; (** identifier labels *)
id_attrs : Sattr.t; (** identifier attributes *)
id_loc : Loc.position option; (** optional location *)
id_tag : Weakhtbl.tag; (** unique magical tag *)
}
......@@ -66,7 +66,7 @@ val id_hash : ident -> int
(** a user-created type of unregistered identifiers *)
type preid = {
pre_name : string;
pre_label : Slab.t;
pre_attrs : Sattr.t;
pre_loc : Loc.position option;
}
......@@ -74,19 +74,19 @@ type preid = {
val id_register : preid -> ident
(** create a fresh pre-ident *)
val id_fresh : ?label:Slab.t -> ?loc:Loc.position -> string -> preid
val id_fresh : ?attrs:Sattr.t -> ?loc:Loc.position -> string -> preid
(** create a localized pre-ident *)
val id_user : ?label:Slab.t -> string -> Loc.position -> preid
val id_user : ?attrs:Sattr.t -> string -> Loc.position -> preid
(** create a duplicate pre-ident with given labels *)
val id_lab : Slab.t -> ident -> preid
(** create a duplicate pre-ident with given attributes *)
val id_attr : ident -> Sattr.t -> preid
(** create a duplicate pre-ident *)
val id_clone : ?label:Slab.t -> ident -> preid
val id_clone : ?attrs:Sattr.t -> ident -> preid
(** create a derived pre-ident (inherit labels and location) *)
val id_derive : ?label:Slab.t -> string -> ident -> preid
(** create a derived pre-ident (inherit attributes and location) *)
val id_derive : ?attrs:Sattr.t -> string -> ident -> preid
(* DEPRECATED : retrieve preid name without registering *)
val preid_name : preid -> string
......@@ -136,54 +136,51 @@ val char_to_lalnumus : char -> string
(** {2 Name handling for ITP} *)
val id_unique_label :
(* TODO: integrate this functionality into id_unique *)
val id_unique_attr :
ident_printer -> ?sanitizer : (string -> string) -> ident -> string
(** Do the same as id_unique except that it tries first to
use the "name:" label to generate the name instead of id.id_string *)
(** Do the same as id_unique except that it tries first to use
the "name:" attribute to generate the name instead of id.id_string *)
(** {2 labels for handling counterexamples} *)
(** {2 Attributes for handling counterexamples} *)
val model_label : label
val model_projected_label : label
val model_attr : attribute
val model_projected_attr : attribute
val model_vc_label : label
val model_vc_post_label : label
val model_vc_havoc_label : label
val model_vc_attr : attribute
val model_vc_post_attr : attribute
val model_vc_havoc_attr : attribute
val has_a_model_label : ident -> bool
(** [true] when [ident] has one of the labels above. *)
val has_a_model_attr : ident -> bool
(** [true] when [ident] has one of the attributes above *)
val remove_model_labels : labels : Slab.t -> Slab.t
(** Returns a copy of labels without [model_label] and [model_projected_label]. *)
val remove_model_attrs : attrs:Sattr.t -> Sattr.t
(** Remove the counter-example attributes from an attribute set *)
val create_model_trace_label : string -> label
val create_model_trace_attr : string -> attribute
val is_model_trace_label : label -> bool
val is_model_trace_attr : attribute -> bool
val append_to_model_trace_label : labels : Slab.t ->
to_append : string ->
Slab.t
(** The returned set of labels will contain the same set of labels
as argument labels except that a label of the form ["model_trace:*"]
val append_to_model_trace_attr : attrs:Sattr.t -> to_append:string -> Sattr.t
(** The returned set of attributes will contain the same set of attributes
as argument attrs except that an attribute of the form ["model_trace:*"]
will be ["model_trace:*to_append"]. *)
val append_to_model_element_name : labels : Slab.t ->
to_append : string ->
Slab.t
(** The returned set of labels will contain the same set of labels
as argument labels except that a label of the form ["model_trace:*@*"]
val append_to_model_element_name : attrs:Sattr.t -> to_append:string -> Sattr.t
(** The returned set of attributes will contain the same set of attributes
as argument attrs except that an attribute of the form ["model_trace:*@*"]
will be ["model_trace:*to_append@*"]. *)
val get_model_element_name : labels : Slab.t -> string
(** If labels contain a label of the form ["model_trace:name@*"],
return ["name"].
Throws [Not_found] if there is no label of the form ["model_trace:*"]. *)
val get_model_element_name : attrs:Sattr.t -> string
(** If attributes contain an attribute of the form ["model_trace:name@*"],
return ["name"]. Raises [Not_found] if there is no attribute of
the form ["model_trace:*"]. *)
val get_model_trace_string : labels : Slab.t -> string
(** If labels contain a label of the form ["model_trace:mt_string"],
return ["mt_string"].
Throws [Not_found] if there is no label of the form ["model_trace:*"]. *)
val get_model_trace_string : attrs:Sattr.t -> string
(** If attrs contain an attribute of the form ["model_trace:mt_string"],
return ["mt_string"]. Raises [Not_found] if there is no attribute of
the form ["model_trace:*"]. *)
val get_model_trace_label : labels : Slab.t -> Slab.elt
(** Return a label of the form ["model_trace:*"].
Throws [Not_found] if there is no such label. *)
val get_model_trace_attr : attrs:Sattr.t -> attribute
(** Return an attribute of the form ["model_trace:*"].
Raises [Not_found] if there is no such attribute. *)
......@@ -674,7 +674,7 @@ let build_model_rec (raw_model: model_element list) (term_map: Term.term Mstr.t)
try
(
let t = Mstr.find raw_element_name term_map in
let real_model_trace = construct_name (get_model_trace_string ~labels:t.t_label) in
let real_model_trace = construct_name (get_model_trace_string ~attrs:t.t_attrs) in
let model_element = {
me_name = real_model_trace;
me_value = raw_element.me_value;
......
......@@ -26,7 +26,7 @@ let why3_keywords =
"forall"; "exists"; "not"; "true"; "false"; "if"; "then"; "else";
"let"; "in"; "match"; "with"; "as"; "epsilon" ]
let label_coercion = create_label "coercion"
let coercion_attr = create_attribute "coercion"
module type Printer = sig
......@@ -34,7 +34,7 @@ module type Printer = sig
val forget_tvs : unit -> unit (* flush id_unique for type vars *)
val forget_var : vsymbol -> unit (* flush id_unique for a variable *)
val print_id_labels : formatter -> ident -> unit (* labels and location *)
val print_id_attrs : formatter -> ident -> unit (* attributes and location *)
val print_tv : formatter -> tvsymbol -> unit (* type variable *)
val print_vs : formatter -> vsymbol -> unit (* variable *)
......@@ -53,7 +53,7 @@ module type Printer = sig
val print_pat : formatter -> pattern -> unit (* pattern *)
val print_term : formatter -> term -> unit (* term *)
val print_label : formatter -> label -> unit
val print_attr : formatter -> attribute -> unit
val print_loc : formatter -> Loc.position -> unit
val print_pkind : formatter -> prop_kind -> unit
val print_meta_arg : formatter -> meta_arg -> unit
......@@ -82,10 +82,10 @@ module type Printer = sig
end
let debug_print_labels =
let debug_print_attrs =
Debug.register_info_flag
"print_labels"
~desc:"Print@ labels@ of@ identifiers@ and@ expressions."
"print_attributes"
~desc:"Print@ attributes@ of@ identifiers@ and@ expressions."
let debug_print_locs = Debug.register_info_flag "print_locs"
~desc:"Print@ locations@ of@ identifiers@ and@ expressions."
......@@ -106,17 +106,17 @@ let forget_all () =
if do_forget_all then forget_all tprinter;
if do_forget_all then forget_all pprinter
let print_label fmt l = fprintf fmt "[@%s]" l.lab_string
let print_labels = print_iter1 Slab.iter space print_label
let print_attr fmt a = fprintf fmt "[@%s]" a.attr_string
let print_attrs = print_iter1 Sattr.iter space print_attr
let print_loc fmt l =
let (f,l,b,e) = Loc.get l in
fprintf fmt "#\"%s\" %d %d %d#" f l b e
let print_id_labels fmt id =
if Debug.test_flag debug_print_labels &&
not (Slab.is_empty id.id_label) then
fprintf fmt "@ %a" print_labels id.id_label;
let print_id_attrs fmt id =
if Debug.test_flag debug_print_attrs &&
not (Sattr.is_empty id.id_attrs) then
fprintf fmt "@ %a" print_attrs id.id_attrs;
if Debug.test_flag debug_print_locs then