From 5e22e653ec376336bbbed50aca4946db8edbc90f Mon Sep 17 00:00:00 2001
From: Guillaume Bury <guillaume.bury@gmail.com>
Date: Mon, 11 Mar 2024 11:48:40 +0100
Subject: [PATCH] Fix attributes in nested binders (#210)

* Change Hmap implementation, and use that to add tag printing
* Fix typing of attributes in nested binders + tests
---
 CHANGES.md                                    |  10 +-
 dolmen.opam                                   |   1 +
 src/bin/main.ml                               |   1 +
 src/interface/dune                            |   2 +-
 src/interface/pretty.ml                       |  29 ++++
 src/interface/tag.ml                          |   4 +-
 src/loop/state.ml                             |  46 ++---
 src/standard/dune                             |   4 +-
 src/standard/expr.ml                          | 117 +++++++++----
 src/standard/expr.mli                         |   3 +
 src/standard/hmap.ml                          | 161 ------------------
 src/standard/hmap.mli                         |  83 ---------
 src/standard/pretty.ml                        |  10 +-
 src/standard/tag.ml                           |  60 ++++---
 src/standard/tag.mli                          |  43 ++++-
 src/typecheck/thf.ml                          |  40 +++--
 tests/typing/pass/smtlib/v2.6/attribute/dune  | 100 +++++++++++
 .../pass/smtlib/v2.6/attribute/flags.dune     |   0
 .../smtlib/v2.6/attribute/let_seq.expected    |   4 +
 .../pass/smtlib/v2.6/attribute/let_seq.smt2   |  10 ++
 .../v2.6/attribute/nest_pattern.expected      |   4 +
 .../smtlib/v2.6/attribute/nest_pattern.smt2   |  12 ++
 .../v2.6/attribute/simple_pattern.expected    |   4 +
 .../smtlib/v2.6/attribute/simple_pattern.smt2 |  10 ++
 24 files changed, 403 insertions(+), 355 deletions(-)
 create mode 100644 src/interface/pretty.ml
 delete mode 100644 src/standard/hmap.ml
 delete mode 100644 src/standard/hmap.mli
 create mode 100644 tests/typing/pass/smtlib/v2.6/attribute/dune
 create mode 100644 tests/typing/pass/smtlib/v2.6/attribute/flags.dune
 create mode 100644 tests/typing/pass/smtlib/v2.6/attribute/let_seq.expected
 create mode 100644 tests/typing/pass/smtlib/v2.6/attribute/let_seq.smt2
 create mode 100644 tests/typing/pass/smtlib/v2.6/attribute/nest_pattern.expected
 create mode 100644 tests/typing/pass/smtlib/v2.6/attribute/nest_pattern.smt2
 create mode 100644 tests/typing/pass/smtlib/v2.6/attribute/simple_pattern.expected
 create mode 100644 tests/typing/pass/smtlib/v2.6/attribute/simple_pattern.smt2

diff --git a/CHANGES.md b/CHANGES.md
index 510c655fe..1f181e71c 100644
--- a/CHANGES.md
+++ b/CHANGES.md
@@ -26,6 +26,8 @@ next
 ### Printing
 
 - Add printers for smtlib identifiers (PR#198)
+- Printing of typed expressions (i.e. the Std.Expr module)
+  can now print the tags (PR#210)
 
 ### Typing
 
@@ -42,10 +44,10 @@ next
 - Add a warning for unknown attributes in smtlib2. This replaces
   the `unbound id` error that some files could raise before when
   using non-standard attribtues (PR#207)
-- Only type annotations on quantified formulas once. Previously,
-  these were typed twice so that they can be attached to both the
-  body of the quantified formula and the quantified formula itself.
-  (PR#207)
+- Only type annotations on quantified formulas and binders once.
+  Previously, these were typed twice so that they can be attached to
+  both the body of the bound formula and the quantified formula itself.
+  (PR#207, PR#210)
 
 ### Loop
 
diff --git a/dolmen.opam b/dolmen.opam
index fe670fa17..341d17c58 100644
--- a/dolmen.opam
+++ b/dolmen.opam
@@ -13,6 +13,7 @@ depends: [
   "menhir" {>= "20211230" }
   "dune" { >= "3.0" }
   "fmt" { >= "0.8.7" }
+  "hmap" { >= "0.8.1" }
   "seq"
   "odoc" { with-doc }
   "qcheck" { with-test }
diff --git a/src/bin/main.ml b/src/bin/main.ml
index 51eb745d8..cb2ee8070 100644
--- a/src/bin/main.ml
+++ b/src/bin/main.ml
@@ -38,6 +38,7 @@ let finally st e =
 
 let run st preludes logic_file =
   if Loop.State.get Loop.State.debug st then begin
+    Dolmen.Std.Expr.Print.print_tags := true;
     Dolmen.Std.Expr.Print.print_index := true;
     ()
   end;
diff --git a/src/interface/dune b/src/interface/dune
index 50b91d610..017f1b4db 100644
--- a/src/interface/dune
+++ b/src/interface/dune
@@ -4,5 +4,5 @@
   (instrumentation (backend bisect_ppx))
   (libraries      menhirLib)
   (modules        Map Msg Tok Lex Parse Location
-                  Id Tag Ty Term Stmt Ext Language)
+                  Pretty Tag Id Ty Term Stmt Ext Language)
 )
diff --git a/src/interface/pretty.ml b/src/interface/pretty.ml
new file mode 100644
index 000000000..d295ed807
--- /dev/null
+++ b/src/interface/pretty.ml
@@ -0,0 +1,29 @@
+
+(* This file is free software, part of Dolmen. See file "LICENSE" for more details. *)
+
+(** Pretty printing annotations
+
+    This module defines types to specify pretty printing annotations
+    (such as associtativity, infix notations, etc...).
+*)
+
+
+(* Pretty types *)
+(* ************************************************************************ *)
+
+type name =
+  | Exact of string
+  | Renamed of string
+
+type pos =
+  | Infix
+  | Prefix
+
+type assoc =
+  | Left
+  | Right
+
+type 'a print =
+  | Ignore : _ print
+  | P : (Format.formatter -> 'a -> unit) -> 'a print
+
diff --git a/src/interface/tag.ml b/src/interface/tag.ml
index 0dd048157..775ea4b9d 100644
--- a/src/interface/tag.ml
+++ b/src/interface/tag.ml
@@ -10,7 +10,9 @@ module type S = sig
   type 'a t
   (** Polymorphic tags *)
 
-  val create : unit -> 'a t
+  val create :
+    ?print:('a Pretty.print) ->
+    unit -> 'a t
   (** Create a new tag. *)
 
 end
diff --git a/src/loop/state.ml b/src/loop/state.ml
index ec8d0b0e1..1083cbd0a 100644
--- a/src/loop/state.ml
+++ b/src/loop/state.ml
@@ -4,20 +4,16 @@
 (* Type definition *)
 (* ************************************************************************* *)
 
-module M = Dolmen.Std.Hmap.Make(struct
-    type t = int
-    let compare (a: int) (b: int) = compare a b
-  end)
-
-type t = M.t
-
-type 'a key = {
-  id : int;
+type 'a info = {
   name : string;
   pipe : string;
-  inj : 'a Dolmen.Std.Hmap.injection;
 }
 
+module M = Hmap.Make(struct type 'a t = 'a info end)
+
+type t = M.t
+type 'a key = 'a M.key
+
 type report_style =
   | Minimal
   | Regular
@@ -146,34 +142,38 @@ end
 
 let empty : t = M.empty
 
-let key_counter = ref 0
 let create_key ~pipe name =
-  incr key_counter;
-  { id = !key_counter; pipe; name;
-    inj = Dolmen.Std.Hmap.create_inj ();}
+  let info = { name; pipe; } in
+  M.Key.create info
 
 let get k t =
-  match M.get ~inj:k.inj k.id t with
+  match M.find k t with
   | Some v -> v
-  | None -> raise (Key_not_found (t, k.name, k.pipe))
+  | None ->
+    let info = M.Key.info k in
+    raise (Key_not_found (t, info.name, info.pipe))
 
 let get_or ~default k t =
-  match M.get ~inj:k.inj k.id t with
+  match M.find k t with
   | Some v -> v
   | None -> default
 
 let set k v t =
-  M.add ~inj:k.inj k.id v t
+  M.add k v t
 
 let update_opt k f t =
-  M.update ~inj:k.inj k.id f t
+  let old_value = M.find k t in
+  match f old_value with
+  | Some new_value -> M.add k new_value t
+  | None -> M.rem k t
 
 let update k f t =
   update_opt k (function
-    | None -> raise (Key_not_found (t, k.name, k.pipe))
-    | Some v -> Some (f v)) t
-
-let key_name { name; _ } = name
+    | Some v -> Some (f v)
+    | None ->
+      let info = M.Key.info k in
+      raise (Key_not_found (t, info.name, info.pipe))
+    ) t
 
 (* Some common keys *)
 (* ************************************************************************* *)
diff --git a/src/standard/dune b/src/standard/dune
index f3f227a3e..9574d440d 100644
--- a/src/standard/dune
+++ b/src/standard/dune
@@ -1,12 +1,12 @@
 (library
   (name           dolmen_std)
   (public_name    dolmen.std)
-  (libraries      dolmen_intf dolmen_line unix fmt)
+  (libraries      dolmen_intf dolmen_line hmap unix fmt)
   (instrumentation (backend bisect_ppx))
   (flags :standard -warn-error -3)
   (modules
     ; Maps & Utils % TODO: split this into a dedicated sub-library ?
-    Timer Stats Hmap Maps Maps_string
+    Timer Stats Maps Maps_string
     ; Parsing structures
     Loc Name Namespace Id Term Statement Answer Normalize Extensions
     ; Typing & Loop stuff
diff --git a/src/standard/expr.ml b/src/standard/expr.ml
index cbe5d1484..440c3644c 100644
--- a/src/standard/expr.ml
+++ b/src/standard/expr.ml
@@ -119,34 +119,6 @@ exception Record_type_expected of ty_cst
 exception Wildcard_already_set of ty_var
 
 
-(* Tags *)
-(* ************************************************************************* *)
-
-module Tags = struct
-
-  type 'a t = 'a tag
-  type pos = Pretty.pos
-  type name = Pretty.name
-
-  let pos = Tag.create ()
-  let name = Tag.create ()
-  let rwrt = Tag.create ()
-  let ac = Tag.create ()
-  let predicate = Tag.create ()
-
-  let exact s = Pretty.Exact s
-  let infix = Pretty.Infix
-  let prefix = Pretty.Prefix
-
-  let named = Tag.create ()
-  let triggers = Tag.create ()
-  let filters = Tag.create ()
-
-  let bound = Tag.create ()
-
-end
-
-
 (* Printing *)
 (* ************************************************************************* *)
 
@@ -154,13 +126,49 @@ module Print = struct
 
   type 'a t = Format.formatter -> 'a -> unit
 
+  let print_tags = ref false
   let print_index = ref false
 
-  let pos : Pretty.pos tag = Tags.pos
-  let name : Pretty.name tag = Tags.name
+  let pos : Pretty.pos tag = Tag.create ()
+  let name : Pretty.name tag = Tag.create ()
 
   let return fmt_str out () = Format.fprintf out "%(%)" fmt_str
 
+  (* Tag printing *)
+
+  let pp_tags_aux k fmt map =
+    if not !print_tags then
+      k false
+    else begin
+      let l = Tag.fold map [] (fun (Tag.B (k, v)) acc ->
+          let info = Tag.info k in
+          match info.print with
+          | Pretty.Ignore -> acc
+          | Pretty.P pp ->
+            let msg = Format.dprintf "%a" pp v in
+            msg :: acc)
+      in
+      match l with
+      | [] -> k false
+      | _ :: _ ->
+        Format.fprintf fmt "@[<hov>{ ";
+        List.iter (fun msg ->
+            Format.fprintf fmt "%t;@ " msg
+          ) l;
+        Format.fprintf fmt "}@]";
+        k true
+    end
+
+  let pp_tags =
+    pp_tags_aux (fun _ -> ())
+
+  let wrap_tags tags pp fmt t =
+    let k = function
+      | false -> pp fmt t
+      | true -> Format.fprintf fmt "@,(%a)" pp t
+    in
+    pp_tags_aux k fmt tags
+
 
   (* Id printing *)
 
@@ -171,12 +179,12 @@ module Print = struct
   let id fmt (v : _ id) =
     match Tag.get v.tags name with
     | Some (Pretty.Exact s | Pretty.Renamed s) ->
-      Format.fprintf fmt "%s" s
+      Format.fprintf fmt "%s%a" s pp_tags v.tags
     | None ->
       if !print_index then
-        Format.fprintf fmt "%a%a" Path.print v.path pp_index v
+        Format.fprintf fmt "%a%a%a" Path.print v.path pp_index v pp_tags v.tags
       else
-        Format.fprintf fmt "%a" Path.print v.path
+        Format.fprintf fmt "%a%a" Path.print v.path pp_tags v.tags
 
   let id_pretty fmt (v : _ id) =
     match Tag.get v.tags pos with
@@ -234,7 +242,7 @@ module Print = struct
     | _ -> Format.fprintf fmt "( %a )" ty t
 
   and ty fmt t =
-    ty_descr fmt t.ty_descr
+    wrap_tags t.ty_tags ty_descr fmt t.ty_descr
 
   let term_var fmt var = id_type ty fmt var
   let term_cst fmt cst = id_type ty fmt cst
@@ -279,9 +287,9 @@ module Print = struct
         (Format.pp_print_list ~pp_sep:(return "@ ") subterm) args
 
   and binder_sep fmt = function
-    | Lambda _ -> Format.fprintf fmt "=>"
+    | Lambda _ -> Format.fprintf fmt " =>"
     | Let_seq _
-    | Let_par _ -> Format.fprintf fmt "in"
+    | Let_par _ -> Format.fprintf fmt " in"
     | Exists _
     | Forall _ -> Format.fprintf fmt "."
 
@@ -334,7 +342,7 @@ module Print = struct
     | _ -> Format.fprintf fmt "(%a)" term t
 
   and term fmt t =
-    term_descr fmt t.term_descr
+    wrap_tags t.term_tags term_descr fmt t.term_descr
 
   let formula = term
 
@@ -362,6 +370,41 @@ module Print = struct
       )
 end
 
+(* Tags *)
+(* ************************************************************************* *)
+
+module Tags = struct
+
+  type 'a t = 'a tag
+  type pos = Pretty.pos
+  type name = Pretty.name
+
+  let exact s = Pretty.Exact s
+  let infix = Pretty.Infix
+  let prefix = Pretty.Prefix
+
+  let pos = Print.pos
+  let name = Print.name
+
+  let rwrt = Tag.create ()
+  let ac = Tag.create ()
+  let predicate = Tag.create ()
+
+  let named = Tag.create ()
+  let filters = Tag.create ()
+
+  let triggers =
+    Tag.create ()
+      ~print:(Pretty.P (fun fmt triggers ->
+          let pp_sep fmt () = Format.fprintf fmt "@ | " in
+          Format.fprintf fmt "%a"
+            (Format.pp_print_list ~pp_sep Print.term) triggers))
+
+  let bound = Tag.create ()
+
+end
+
+
 
 (* Helpers *)
 (* ************************************************************************* *)
diff --git a/src/standard/expr.mli b/src/standard/expr.mli
index 09eb0e541..46e44b651 100644
--- a/src/standard/expr.mli
+++ b/src/standard/expr.mli
@@ -192,6 +192,9 @@ module Print : sig
   type 'a t = Format.formatter -> 'a -> unit
   (** Alias for the type printing functions. *)
 
+  val print_tags : bool ref
+  (** Determine whether to print the map of tags for each id/type/term or not. *)
+
   val print_index : bool ref
   (** Determines whether to print the unique index of each identifier or not. *)
 
diff --git a/src/standard/hmap.ml b/src/standard/hmap.ml
deleted file mode 100644
index cbb8b2e96..000000000
--- a/src/standard/hmap.ml
+++ /dev/null
@@ -1,161 +0,0 @@
-
-(* This file is free software, part of Archsat. See file "LICENSE" for more details. *)
-
-(* Heterogeneous Maps,
-   implementation taken from containers, see data.CCMixmap *)
-
-(* Mixmap Implementation (from containers) *)
-(* ************************************************************************ *)
-
-(* Implementation taken from containers. *)
-
-
-type 'b injection = {
-  get : (unit -> unit) -> 'b option;
-  set : 'b -> (unit -> unit);
-}
-
-let create_inj () =
-  let r = ref None in
-  let get f =
-    r := None;
-    f ();
-    !r
-  and set v =
-    (fun () -> r := Some v)
-  in
-  {get;set}
-
-module type S = sig
-  type key
-
-  type t
-  (** A map containing values of different types, indexed by {!key}. *)
-
-  val empty : t
-  (** Empty map *)
-
-  val get : inj:'a injection -> key -> t -> 'a option
-  (** Get the value corresponding to this key, if it exists and
-      belongs to the same key *)
-
-  val add : inj:'a injection -> key -> 'a -> t -> t
-  (** Bind the key to the value, using [inj] *)
-
-  val update : inj:'a injection -> key -> ('a option -> 'a option) -> t -> t
-  (** [update ~inj k f m] updates the value associated with [k] in [m] according
-      to [f (get ~inj k m)]. If the result is [None], the binding associated
-      with [k] is removed. *)
-
-  val find : inj:'a injection -> key -> t -> 'a
-  (** Find the value for the given key, which must be of the right type.
-      @raise Not_found if either the key is not found, or if its value
-        doesn't belong to the right type *)
-
-  val cardinal : t -> int
-  (** Number of bindings *)
-
-  val remove : key -> t -> t
-  (** Remove the binding for this key *)
-
-  val mem : inj:_ injection-> key -> t -> bool
-  (** Is the given key in the map, with the right type? *)
-
-  val iter_keys : f:(key -> unit) -> t -> unit
-  (** Iterate on the keys of this map *)
-
-  val fold_keys : f:('a -> key -> 'a) -> x:'a -> t -> 'a
-  (** Fold over the keys *)
-
-  (** {2 Iterators} *)
-
-  type 'a iter = ('a -> unit) -> unit
-
-  val keys_iter : t -> key iter
-  (** All the keys *)
-
-  val bindings_of : inj:'a injection -> t -> (key * 'a) iter
-  (** All the bindings that come from the corresponding injection *)
-
-  type value =
-    | Value : ('a injection -> 'a option) -> value
-
-  val bindings : t -> (key * value) iter
-  (** Iterate on all bindings *)
-end
-
-module type ORD = sig
-  type t
-  val compare : t -> t -> int
-end
-
-module Make(X : ORD) : S with type key = X.t = struct
-  module M = Map.Make(X)
-
-  type key = X.t
-  type t = (unit -> unit) M.t
-
-  let empty = M.empty
-
-  let find ~inj x map =
-    match inj.get (M.find x map) with
-      | None -> raise Not_found
-      | Some v -> v
-
-  let get ~inj x map =
-    try inj.get (M.find x map)
-    with Not_found -> None
-
-  let update ~inj x f map =
-    M.update x (fun y ->
-      Option.map inj.set @@ f (Option.bind y inj.get))
-      map
-
-  let add ~inj x y map =
-    M.add x (inj.set y) map
-
-  let cardinal = M.cardinal
-
-  let remove = M.remove
-
-  let is_some = function
-    | None -> false
-    | Some _ -> true
-
-  let mem ~inj x map =
-    try
-      is_some (inj.get (M.find x map))
-    with Not_found -> false
-
-  let iter_keys ~f map =
-    M.iter (fun x _ -> f x) map
-
-  let fold_keys ~f ~x map =
-    M.fold (fun x _ acc -> f acc x) map x
-
-  (** {2 Iterators} *)
-
-  type 'a iter = ('a -> unit) -> unit
-
-  let keys_iter map yield =
-    M.iter
-      (fun x _ -> yield x)
-      map
-
-  let bindings_of ~inj map yield =
-    M.iter
-      (fun k value ->
-         match inj.get value with
-           | None -> ()
-           | Some v -> yield (k, v)
-      ) map
-
-  type value =
-    | Value : ('b injection -> 'b option) -> value
-
-  let bindings map yield =
-    M.iter
-      (fun x y -> yield (x, Value (fun inj -> inj.get y)))
-      map
-end
-
diff --git a/src/standard/hmap.mli b/src/standard/hmap.mli
deleted file mode 100644
index 7c12ab9d9..000000000
--- a/src/standard/hmap.mli
+++ /dev/null
@@ -1,83 +0,0 @@
-
-(* This file is free software, part of Dolmen. See file "LICENSE" for more details. *)
-
-(** {2 Heterogeneous Maps} *)
-
-type 'a injection
-(** An accessor for values of type 'a in any map. Values put
-    in the map using a key can only be retrieved using this
-    very same key. *)
-
-val create_inj : unit -> 'a injection
-(** Return a value that works for a given type of values.  This function is
-    normally called once for each type of value. Several keys may be
-    created for the same type, but a value set with a given setter can only be
-    retrieved with the matching getter. The same key can be reused
-    across multiple maps (although not in a thread-safe way). *)
-
-module type S = sig
-  type key
-
-  type t
-  (** A map containing values of different types, indexed by {!key}. *)
-
-  val empty : t
-  (** Empty map. *)
-
-  val get : inj:'a injection -> key -> t -> 'a option
-  (** Get the value corresponding to this key, if it exists and
-      belongs to the same key. *)
-
-  val add : inj:'a injection -> key -> 'a -> t -> t
-  (** Bind the key to the value, using [inj]. *)
-
-  val update : inj:'a injection -> key -> ('a option -> 'a option) -> t -> t
-  (** [update ~inj k f m] updates the value associated with [k] in [m] according
-      to [f (get ~inj k m)]. If the result is [None], the binding associated
-      with [k] is removed.
-
-      @since 0.9 *)
-
-  val find : inj:'a injection -> key -> t -> 'a
-  (** Find the value for the given key, which must be of the right type.
-      @raise Not_found if either the key is not found, or if its value
-        doesn't belong to the right type. *)
-
-  val cardinal : t -> int
-  (** Number of bindings. *)
-
-  val remove : key -> t -> t
-  (** Remove the binding for this key. *)
-
-  val mem : inj:_ injection-> key -> t -> bool
-  (** Is the given key in the map, with the right type? *)
-
-  val iter_keys : f:(key -> unit) -> t -> unit
-  (** Iterate on the keys of this map. *)
-
-  val fold_keys : f:('a -> key -> 'a) -> x:'a -> t -> 'a
-  (** Fold over the keys. *)
-
-  (** {2 Iterators} *)
-
-  type 'a iter = ('a -> unit) -> unit
-
-  val keys_iter : t -> key iter
-  (** All the keys. *)
-
-  val bindings_of : inj:'a injection -> t -> (key * 'a) iter
-  (** All the bindings that come from the corresponding injection. *)
-
-  type value =
-    | Value : ('a injection -> 'a option) -> value
-
-  val bindings : t -> (key * value) iter
-  (** Iterate on all bindings. *)
-end
-
-module type ORD = sig
-  type t
-  val compare : t -> t -> int
-end
-
-module Make(X : ORD) : S with type key = X.t
diff --git a/src/standard/pretty.ml b/src/standard/pretty.ml
index 8caa45786..d34f34ddb 100644
--- a/src/standard/pretty.ml
+++ b/src/standard/pretty.ml
@@ -11,15 +11,19 @@
 (* Pretty types *)
 (* ************************************************************************ *)
 
-type name =
+type name = Dolmen_intf.Pretty.name =
   | Exact of string
   | Renamed of string
 
-type pos =
+type pos = Dolmen_intf.Pretty.pos =
   | Infix
   | Prefix
 
-type assoc =
+type assoc = Dolmen_intf.Pretty.assoc =
   | Left
   | Right
 
+type 'a print = 'a Dolmen_intf.Pretty.print =
+  | Ignore : _ print
+  | P : (Format.formatter -> 'a -> unit) -> 'a print
+
diff --git a/src/standard/tag.ml b/src/standard/tag.ml
index 15035f4fb..908a8419d 100644
--- a/src/standard/tag.ml
+++ b/src/standard/tag.ml
@@ -7,32 +7,56 @@
 (* Functor instantiation *)
 (* ************************************************************************ *)
 
-module M = Hmap.Make(struct
-    type t = int
-    let compare (a: int) (b: int) = compare a b
-  end)
+(* Key info *)
+type 'a info = {
+  print : 'a Pretty.print;
+}
+
+module M = Hmap.Make(struct type 'a t = 'a info end)
+
+(* Types and key creation *)
+(* ************************************************************************ *)
 
 type map = M.t
+type 'a t = 'a M.key
 
-type 'a t = {
-  id : int;
-  inj : 'a Hmap.injection;
-}
+let info k =
+  M.Key.info k
+
+let create ?(print=Pretty.Ignore) () =
+  let info = { print; } in
+  M.Key.create info
 
-let equal k k' = k.id = k'.id
 
-let mk_key id = { id; inj = Hmap.create_inj (); }
+(* Iteration *)
+(* ************************************************************************ *)
+
+type binding = M.binding = B : 'a t * 'a -> binding
+
+let iter m f = M.iter f m
 
-let max_id = ref 0
+let fold m acc f = M.fold f m acc
 
-let create () =
-  incr max_id;
-  mk_key !max_id
+
+(* small wrappers *)
+(* ************************************************************************ *)
 
 let empty = M.empty
 
+let is_empty = M.is_empty
+
 let get m k =
-  M.get ~inj:k.inj k.id m
+  M.find k m
+
+let unset m k =
+  M.rem k m
+
+let set m k l =
+  M.add k l m
+
+
+(* convenient wrappers for advanced tags *)
+(* ************************************************************************ *)
 
 let get_list m k =
   match get m k with
@@ -45,12 +69,6 @@ let get_last m k =
   | Some [] -> None
   | Some (x :: _) -> Some x
 
-let unset m k =
-  M.remove k.id m
-
-let set m k l =
-  M.add ~inj:k.inj k.id l m
-
 let set_opt m k = function
   | None -> m
   | Some v -> set m k v
diff --git a/src/standard/tag.mli b/src/standard/tag.mli
index c731de2d5..4eeb06943 100644
--- a/src/standard/tag.mli
+++ b/src/standard/tag.mli
@@ -11,17 +11,47 @@ type map
 type 'a t
 (** A tag containing values of type ['a]. *)
 
-val equal : _ t -> _ t -> bool
-(** Are two tag keys equal ? *)
+type 'a info = {
+  print : 'a Pretty.print;
+}
+(** The type for information carried by each tag. *)
 
 
-(** {2 Creating and accessing tags} *)
+(** {2 Creating tags} *)
+
+val create :
+  ?print:'a Pretty.print ->
+  unit -> 'a t
+(** Create a new tag. *)
+
+val info : 'a t -> 'a info
+(** Access the info of a tag. *)
+
+
+(** {2 Creating maps} *)
 
 val empty : map
 (** The empty map. *)
 
-val create : unit -> 'a t
-(** Create a new tag. *)
+val is_empty : map -> bool
+(** Is the map empty ? *)
+
+
+(** {2 Iterators} *)
+
+
+type binding = B : 'a t * 'a -> binding (**)
+(** Existencial type to wrap a binding. *)
+
+val iter : map -> (binding -> unit) -> unit
+(** [iter f m] applies [f] to all bindings of [m]. *)
+
+val fold : map -> 'a -> (binding -> 'a -> 'a) -> 'a
+(** [fold f m acc] folds over the bindings of [m] with [f], starting with
+    [acc] *)
+
+
+(** {2 Getters} *)
 
 val get : map -> 'a t -> 'a option
 (** Get the value associated to a tag. *)
@@ -34,6 +64,9 @@ val get_last : map -> 'a list t -> 'a option
 (** Return the last value associated to a list tag (i.e. the head of the
     list returned by {get_list} if it exists). *)
 
+
+(** {2 Setters} *)
+
 val set : map -> 'a t -> 'a -> map
 (** Set the value bound to a tag. *)
 
diff --git a/src/typecheck/thf.ml b/src/typecheck/thf.ml
index 1aedda4c1..8995bd854 100644
--- a/src/typecheck/thf.ml
+++ b/src/typecheck/thf.ml
@@ -1619,14 +1619,21 @@ module Make
       ) ([], [], env) l in
     List.rev ttype_vars, List.rev typed_vars, env'
 
-  and parse_binder parse_inner mk b env ast ttype_acc ty_acc body_ast =
-    parse_binder_aux parse_inner mk b env ast ttype_acc ty_acc body_ast
-
-  and parse_binder_aux parse_inner mk b env ast ttype_acc ty_acc = function
+  and parse_binder parse_inner mk b env ast ttype_acc ty_acc = function
     | { Ast.term = Ast.Binder (b', vars, f); _ } when b = b' ->
-      let ttype_vars, ty_vars, env' = parse_binder_vars env vars in
-      parse_binder parse_inner mk b env' ast (ttype_acc @ ttype_vars) (ty_acc @ ty_vars) f
+      let ttype_vars, ty_vars, env = parse_binder_vars env vars in
+      let ttype_acc = ttype_acc @ ttype_vars in
+      let ty_acc = ty_acc @ ty_vars in
+      (* if there are any attributes, do **not** try and collapse successive
+         binders into a single one. *)
+      begin match f.attr with
+        | [] -> parse_binder parse_inner mk b env ast ttype_acc ty_acc f
+        | _ :: _ -> parse_binder_end parse_inner mk b env ast ttype_acc ty_acc f
+      end
     | body_ast ->
+      parse_binder_end parse_inner mk b env ast ttype_acc ty_acc body_ast
+
+  and parse_binder_end parse_inner mk b env ast ttype_acc ty_acc body_ast =
       let body = parse_inner env body_ast in
       let f = mk_binder env b ast mk (ttype_acc, ty_acc) body in
       Term f
@@ -1698,21 +1705,26 @@ module Make
     in
     List.rev l, env
 
-  and parse_let_seq_end env ast acc = function
+  and parse_let_seq_collapse env ast acc = function
     | ({ Ast.term = Ast.Binder (Ast.Let_seq, vars, f'); _ } as f)
     | ({ Ast.term = Ast.Binder (Ast.Let_par, ([_] as vars), f'); _ } as f)->
       parse_let_seq env f acc f' vars
     | f ->
-      let l = List.rev acc in
-      begin match parse_expr env f with
-        | Term t -> Term (mk_let env ast T.letin l t)
-        | res -> _expected env "term of formula" f (Some res)
-      end
+      parse_let_seq_end env ast acc f
+
+  and parse_let_seq_end env ast acc f =
+    let l = List.rev acc in
+    begin match parse_expr env f with
+      | Term t -> Term (mk_let env ast T.letin l t)
+      | res -> _expected env "term of formula" f (Some res)
+    end
 
   and parse_let_seq env ast acc f = function
     | [] ->
-      let[@inline] aux t = parse_let_seq_end env ast acc t in
-      (wrap_attr[@inlined]) apply_attr env f aux
+      begin match f.attr with
+        | [] -> parse_let_seq_collapse env ast acc f
+        | _ :: _ -> parse_let_seq_end env ast acc f
+      end
     | x :: r ->
       begin match x with
         | { Ast.term = Ast.Colon ({ Ast.term = Ast.Symbol s; _ } as w, e); _ }
diff --git a/tests/typing/pass/smtlib/v2.6/attribute/dune b/tests/typing/pass/smtlib/v2.6/attribute/dune
new file mode 100644
index 000000000..e903dde2c
--- /dev/null
+++ b/tests/typing/pass/smtlib/v2.6/attribute/dune
@@ -0,0 +1,100 @@
+; File auto-generated by gentests.ml
+
+; Auto-generated part begin
+; Test for let_seq.smt2
+; Incremental test
+
+(rule
+   (target  let_seq.incremental)
+   (deps    (:input let_seq.smt2))
+   (package dolmen_bin)
+   (action (chdir %{workspace_root}
+            (with-outputs-to %{target}
+             (with-accepted-exit-codes (or 0 (not 0))
+              (run dolmen --mode=incremental --color=never %{input} %{read-lines:flags.dune}))))))
+(rule
+  (alias runtest)
+  (package dolmen_bin)
+  (action (diff let_seq.expected let_seq.incremental)))
+
+; Full mode test
+
+(rule
+   (target  let_seq.full)
+   (deps    (:input let_seq.smt2))
+   (package dolmen_bin)
+   (action (chdir %{workspace_root}
+            (with-outputs-to %{target}
+             (with-accepted-exit-codes (or 0 (not 0))
+              (run dolmen --mode=full --color=never %{input} %{read-lines:flags.dune}))))))
+(rule
+  (alias runtest)
+  (package dolmen_bin)
+  (action (diff let_seq.expected let_seq.full)))
+
+
+; Test for nest_pattern.smt2
+; Incremental test
+
+(rule
+   (target  nest_pattern.incremental)
+   (deps    (:input nest_pattern.smt2))
+   (package dolmen_bin)
+   (action (chdir %{workspace_root}
+            (with-outputs-to %{target}
+             (with-accepted-exit-codes (or 0 (not 0))
+              (run dolmen --mode=incremental --color=never %{input} %{read-lines:flags.dune}))))))
+(rule
+  (alias runtest)
+  (package dolmen_bin)
+  (action (diff nest_pattern.expected nest_pattern.incremental)))
+
+; Full mode test
+
+(rule
+   (target  nest_pattern.full)
+   (deps    (:input nest_pattern.smt2))
+   (package dolmen_bin)
+   (action (chdir %{workspace_root}
+            (with-outputs-to %{target}
+             (with-accepted-exit-codes (or 0 (not 0))
+              (run dolmen --mode=full --color=never %{input} %{read-lines:flags.dune}))))))
+(rule
+  (alias runtest)
+  (package dolmen_bin)
+  (action (diff nest_pattern.expected nest_pattern.full)))
+
+
+; Test for simple_pattern.smt2
+; Incremental test
+
+(rule
+   (target  simple_pattern.incremental)
+   (deps    (:input simple_pattern.smt2))
+   (package dolmen_bin)
+   (action (chdir %{workspace_root}
+            (with-outputs-to %{target}
+             (with-accepted-exit-codes (or 0 (not 0))
+              (run dolmen --mode=incremental --color=never %{input} %{read-lines:flags.dune}))))))
+(rule
+  (alias runtest)
+  (package dolmen_bin)
+  (action (diff simple_pattern.expected simple_pattern.incremental)))
+
+; Full mode test
+
+(rule
+   (target  simple_pattern.full)
+   (deps    (:input simple_pattern.smt2))
+   (package dolmen_bin)
+   (action (chdir %{workspace_root}
+            (with-outputs-to %{target}
+             (with-accepted-exit-codes (or 0 (not 0))
+              (run dolmen --mode=full --color=never %{input} %{read-lines:flags.dune}))))))
+(rule
+  (alias runtest)
+  (package dolmen_bin)
+  (action (diff simple_pattern.expected simple_pattern.full)))
+
+
+; Auto-generated part end
diff --git a/tests/typing/pass/smtlib/v2.6/attribute/flags.dune b/tests/typing/pass/smtlib/v2.6/attribute/flags.dune
new file mode 100644
index 000000000..e69de29bb
diff --git a/tests/typing/pass/smtlib/v2.6/attribute/let_seq.expected b/tests/typing/pass/smtlib/v2.6/attribute/let_seq.expected
new file mode 100644
index 000000000..9c67551f9
--- /dev/null
+++ b/tests/typing/pass/smtlib/v2.6/attribute/let_seq.expected
@@ -0,0 +1,4 @@
+File "tests/typing/pass/smtlib/v2.6/attribute/let_seq.smt2", line 7, character 5-13:
+7 |      :foo bar
+         ^^^^^^^^
+Warning Unknown attribute (the attribtue was ignored): `:foo`
diff --git a/tests/typing/pass/smtlib/v2.6/attribute/let_seq.smt2 b/tests/typing/pass/smtlib/v2.6/attribute/let_seq.smt2
new file mode 100644
index 000000000..df38363ed
--- /dev/null
+++ b/tests/typing/pass/smtlib/v2.6/attribute/let_seq.smt2
@@ -0,0 +1,10 @@
+; This tests that attributes are correctly taken into account
+; To do that, we rely on the unknown attribute warning
+(set-logic ALL)
+(assert
+  (let ((x 5))
+    (! (= x x)
+     :foo bar
+    )
+  )
+)
diff --git a/tests/typing/pass/smtlib/v2.6/attribute/nest_pattern.expected b/tests/typing/pass/smtlib/v2.6/attribute/nest_pattern.expected
new file mode 100644
index 000000000..80f8eaf22
--- /dev/null
+++ b/tests/typing/pass/smtlib/v2.6/attribute/nest_pattern.expected
@@ -0,0 +1,4 @@
+File "tests/typing/pass/smtlib/v2.6/attribute/nest_pattern.smt2", line 9, character 5-13:
+9 |      :foo bar
+         ^^^^^^^^
+Warning Unknown attribute (the attribtue was ignored): `:foo`
diff --git a/tests/typing/pass/smtlib/v2.6/attribute/nest_pattern.smt2 b/tests/typing/pass/smtlib/v2.6/attribute/nest_pattern.smt2
new file mode 100644
index 000000000..27aa5ab8a
--- /dev/null
+++ b/tests/typing/pass/smtlib/v2.6/attribute/nest_pattern.smt2
@@ -0,0 +1,12 @@
+; This tests that attributes are correctly taken into account
+; To do that, we rely on the unknown attribute warning
+(set-logic ALL)
+(assert
+  (forall ((x Int))
+    (! (forall ((y Int))
+          (= x y)
+       )
+     :foo bar
+    )
+  )
+)
diff --git a/tests/typing/pass/smtlib/v2.6/attribute/simple_pattern.expected b/tests/typing/pass/smtlib/v2.6/attribute/simple_pattern.expected
new file mode 100644
index 000000000..1c03451da
--- /dev/null
+++ b/tests/typing/pass/smtlib/v2.6/attribute/simple_pattern.expected
@@ -0,0 +1,4 @@
+File "tests/typing/pass/smtlib/v2.6/attribute/simple_pattern.smt2", line 7, character 5-13:
+7 |      :foo bar
+         ^^^^^^^^
+Warning Unknown attribute (the attribtue was ignored): `:foo`
diff --git a/tests/typing/pass/smtlib/v2.6/attribute/simple_pattern.smt2 b/tests/typing/pass/smtlib/v2.6/attribute/simple_pattern.smt2
new file mode 100644
index 000000000..c2d868bf6
--- /dev/null
+++ b/tests/typing/pass/smtlib/v2.6/attribute/simple_pattern.smt2
@@ -0,0 +1,10 @@
+; This tests that attributes are correctly taken into account
+; To do that, we rely on the unknown attribute warning
+(set-logic ALL)
+(assert
+  (forall ((x Int))
+    (! (= x x)
+     :foo bar
+    )
+  )
+)