Fix attributes in nested binders (Gbury#210)

* Change Hmap implementation, and use that to add tag printing
* Fix typing of attributes in nested binders + tests

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
 

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 }

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;

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)
 )

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
+

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

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 *)
 (* ************************************************************************* *)

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

src/standard/expr.ml

@@ -119,48 +119,56 @@ 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 *)
 (* ************************************************************************* *)
 
 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 *)
 (* ************************************************************************* *)

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. *)