From 1722c57195c1cb07b0f780b62e3597cbae9abf26 Mon Sep 17 00:00:00 2001 From: Guillaume Bury Date: Fri, 8 Mar 2024 17:27:41 +0100 Subject: [PATCH 1/5] Change Hmap implementation, and use that to add tag printing --- 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 +++++++++-- 14 files changed, 227 insertions(+), 337 deletions(-) create mode 100644 src/interface/pretty.ml delete mode 100644 src/standard/hmap.ml delete mode 100644 src/standard/hmap.mli 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 "@[{ "; + 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. *) From 835d63b6491e0b9b8c31f024966fd92aebb5d6a0 Mon Sep 17 00:00:00 2001 From: Guillaume Bury Date: Fri, 8 Mar 2024 17:28:08 +0100 Subject: [PATCH 2/5] Fix typing of attributes in nested binders + tests --- src/typecheck/thf.ml | 40 ++++--- tests/typing/pass/smtlib/v2.6/attribute/dune | 100 ++++++++++++++++++ .../pass/smtlib/v2.6/attribute/flags.dune | 1 + .../smtlib/v2.6/attribute/let_seq.expected | 20 ++++ .../pass/smtlib/v2.6/attribute/let_seq.smt2 | 8 ++ .../v2.6/attribute/nest_pattern.expected | 21 ++++ .../smtlib/v2.6/attribute/nest_pattern.smt2 | 10 ++ .../v2.6/attribute/simple_pattern.expected | 20 ++++ .../smtlib/v2.6/attribute/simple_pattern.smt2 | 8 ++ 9 files changed, 214 insertions(+), 14 deletions(-) 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/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..2a8c27d47 --- /dev/null +++ b/tests/typing/pass/smtlib/v2.6/attribute/flags.dune @@ -0,0 +1 @@ +--debug 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..e3315b8fc --- /dev/null +++ b/tests/typing/pass/smtlib/v2.6/attribute/let_seq.expected @@ -0,0 +1,20 @@ +[logic][parsed][0-15] set-logic: ALL +[logic][typed][0-15] other_1[0-15]: + set-logic: ALL = + { theories: core, arrays, bitv, floats, string, + int+real; + features: { free_sorts : true; + free_functions : true; + datatypes : true; + quantifiers : true; + arithmetic : regular; + arrays : all; }; }]} + +[logic][parsed][16-79] antecedent: (let (x : 5) in (= x x){(:foo bar)}) +File "tests/typing/pass/smtlib/v2.6/attribute/let_seq.smt2", line 5, character 5-13: +5 | :foo bar + ^^^^^^^^ +Warning Unknown attribute (the attribtue was ignored): `:foo` +[logic][typed][16-79] hyp_1[16-79]: + hyp: let x/160 = 5/159 in x/160 = x/160 + 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..0d7e30640 --- /dev/null +++ b/tests/typing/pass/smtlib/v2.6/attribute/let_seq.smt2 @@ -0,0 +1,8 @@ +(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..e2785f50e --- /dev/null +++ b/tests/typing/pass/smtlib/v2.6/attribute/nest_pattern.expected @@ -0,0 +1,21 @@ +[logic][parsed][0-15] set-logic: ALL +[logic][typed][0-15] other_1[0-15]: + set-logic: ALL = + { theories: core, arrays, bitv, floats, string, + int+real; + features: { free_sorts : true; + free_functions : true; + datatypes : true; + quantifiers : true; + arithmetic : regular; + arrays : all; }; }]} + +[logic][parsed][16-125] antecedent: + (∀ (x : Int) . + (∀ (y : Int) . (= x y)){(:pattern (sexpr x))}) +[logic][typed][16-125] hyp_1[16-125]: + hyp: + ∀ x/159 : int/4. + { multi-trigger int/4 x/159; } + (∀ y/160 : int/4. x/159 = y/160) + 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..e86225bb8 --- /dev/null +++ b/tests/typing/pass/smtlib/v2.6/attribute/nest_pattern.smt2 @@ -0,0 +1,10 @@ +(set-logic ALL) +(assert + (forall ((x Int)) + (! (forall ((y Int)) + (= x y) + ) + :pattern (x) + ) + ) +) 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..69b8c86cf --- /dev/null +++ b/tests/typing/pass/smtlib/v2.6/attribute/simple_pattern.expected @@ -0,0 +1,20 @@ +[logic][parsed][0-15] set-logic: ALL +[logic][typed][0-15] other_1[0-15]: + set-logic: ALL = + { theories: core, arrays, bitv, floats, string, + int+real; + features: { free_sorts : true; + free_functions : true; + datatypes : true; + quantifiers : true; + arithmetic : regular; + arrays : all; }; }]} + +[logic][parsed][16-88] antecedent: + (∀ (x : Int) . (= x x){(:pattern (sexpr x))}) +[logic][typed][16-88] hyp_1[16-88]: + hyp: + ∀ x/159 : int/4. + { multi-trigger int/4 x/159; } + (x/159 = x/159) + 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..e0bd7048b --- /dev/null +++ b/tests/typing/pass/smtlib/v2.6/attribute/simple_pattern.smt2 @@ -0,0 +1,8 @@ +(set-logic ALL) +(assert + (forall ((x Int)) + (! (= x x) + :pattern (x) + ) + ) +) From 4ba8aa36d62307235a0101a9b3cad6fbec5a6158 Mon Sep 17 00:00:00 2001 From: Guillaume Bury Date: Fri, 8 Mar 2024 17:55:52 +0100 Subject: [PATCH 3/5] changes --- CHANGES.md | 10 ++++++---- 1 file changed, 6 insertions(+), 4 deletions(-) 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 From f564237564f15c5e419b94674c10f1064198da5e Mon Sep 17 00:00:00 2001 From: Guillaume Bury Date: Fri, 8 Mar 2024 17:57:20 +0100 Subject: [PATCH 4/5] Add one more test --- tests/typing/pass/smtlib/v2.6/attribute/dune | 32 +++++++++++++++++++ .../v2.6/attribute/nested_quant.expected | 17 ++++++++++ .../smtlib/v2.6/attribute/nested_quant.smt2 | 8 +++++ 3 files changed, 57 insertions(+) create mode 100644 tests/typing/pass/smtlib/v2.6/attribute/nested_quant.expected create mode 100644 tests/typing/pass/smtlib/v2.6/attribute/nested_quant.smt2 diff --git a/tests/typing/pass/smtlib/v2.6/attribute/dune b/tests/typing/pass/smtlib/v2.6/attribute/dune index e903dde2c..51cc525e6 100644 --- a/tests/typing/pass/smtlib/v2.6/attribute/dune +++ b/tests/typing/pass/smtlib/v2.6/attribute/dune @@ -65,6 +65,38 @@ (action (diff nest_pattern.expected nest_pattern.full))) +; Test for nested_quant.smt2 +; Incremental test + +(rule + (target nested_quant.incremental) + (deps (:input nested_quant.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 nested_quant.expected nested_quant.incremental))) + +; Full mode test + +(rule + (target nested_quant.full) + (deps (:input nested_quant.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 nested_quant.expected nested_quant.full))) + + ; Test for simple_pattern.smt2 ; Incremental test diff --git a/tests/typing/pass/smtlib/v2.6/attribute/nested_quant.expected b/tests/typing/pass/smtlib/v2.6/attribute/nested_quant.expected new file mode 100644 index 000000000..64f207fa4 --- /dev/null +++ b/tests/typing/pass/smtlib/v2.6/attribute/nested_quant.expected @@ -0,0 +1,17 @@ +[logic][parsed][0-15] set-logic: ALL +[logic][typed][0-15] other_1[0-15]: + set-logic: ALL = + { theories: core, arrays, bitv, floats, string, + int+real; + features: { free_sorts : true; + free_functions : true; + datatypes : true; + quantifiers : true; + arithmetic : regular; + arrays : all; }; }]} + +[logic][parsed][16-95] antecedent: + (∀ (x : Int) . (∀ (y : Int) . (= x y))) +[logic][typed][16-95] hyp_1[16-95]: + hyp: ∀ x/159 : int/4, y/160 : int/4. x/159 = y/160 + diff --git a/tests/typing/pass/smtlib/v2.6/attribute/nested_quant.smt2 b/tests/typing/pass/smtlib/v2.6/attribute/nested_quant.smt2 new file mode 100644 index 000000000..866b05c6e --- /dev/null +++ b/tests/typing/pass/smtlib/v2.6/attribute/nested_quant.smt2 @@ -0,0 +1,8 @@ +(set-logic ALL) +(assert + (forall ((x Int)) + (forall ((y Int)) + (= x y) + ) + ) +) From b72a52eebfe6fb7565d88a9324e3bf90879fbf41 Mon Sep 17 00:00:00 2001 From: Guillaume Bury Date: Mon, 11 Mar 2024 10:59:07 +0100 Subject: [PATCH 5/5] Adjust tests for windows --- tests/typing/pass/smtlib/v2.6/attribute/dune | 32 ------------------- .../pass/smtlib/v2.6/attribute/flags.dune | 1 - .../smtlib/v2.6/attribute/let_seq.expected | 20 ++---------- .../pass/smtlib/v2.6/attribute/let_seq.smt2 | 2 ++ .../v2.6/attribute/nest_pattern.expected | 25 +++------------ .../smtlib/v2.6/attribute/nest_pattern.smt2 | 4 ++- .../v2.6/attribute/nested_quant.expected | 17 ---------- .../smtlib/v2.6/attribute/nested_quant.smt2 | 8 ----- .../v2.6/attribute/simple_pattern.expected | 24 +++----------- .../smtlib/v2.6/attribute/simple_pattern.smt2 | 4 ++- 10 files changed, 18 insertions(+), 119 deletions(-) delete mode 100644 tests/typing/pass/smtlib/v2.6/attribute/nested_quant.expected delete mode 100644 tests/typing/pass/smtlib/v2.6/attribute/nested_quant.smt2 diff --git a/tests/typing/pass/smtlib/v2.6/attribute/dune b/tests/typing/pass/smtlib/v2.6/attribute/dune index 51cc525e6..e903dde2c 100644 --- a/tests/typing/pass/smtlib/v2.6/attribute/dune +++ b/tests/typing/pass/smtlib/v2.6/attribute/dune @@ -65,38 +65,6 @@ (action (diff nest_pattern.expected nest_pattern.full))) -; Test for nested_quant.smt2 -; Incremental test - -(rule - (target nested_quant.incremental) - (deps (:input nested_quant.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 nested_quant.expected nested_quant.incremental))) - -; Full mode test - -(rule - (target nested_quant.full) - (deps (:input nested_quant.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 nested_quant.expected nested_quant.full))) - - ; Test for simple_pattern.smt2 ; Incremental test diff --git a/tests/typing/pass/smtlib/v2.6/attribute/flags.dune b/tests/typing/pass/smtlib/v2.6/attribute/flags.dune index 2a8c27d47..e69de29bb 100644 --- a/tests/typing/pass/smtlib/v2.6/attribute/flags.dune +++ b/tests/typing/pass/smtlib/v2.6/attribute/flags.dune @@ -1 +0,0 @@ ---debug diff --git a/tests/typing/pass/smtlib/v2.6/attribute/let_seq.expected b/tests/typing/pass/smtlib/v2.6/attribute/let_seq.expected index e3315b8fc..9c67551f9 100644 --- a/tests/typing/pass/smtlib/v2.6/attribute/let_seq.expected +++ b/tests/typing/pass/smtlib/v2.6/attribute/let_seq.expected @@ -1,20 +1,4 @@ -[logic][parsed][0-15] set-logic: ALL -[logic][typed][0-15] other_1[0-15]: - set-logic: ALL = - { theories: core, arrays, bitv, floats, string, - int+real; - features: { free_sorts : true; - free_functions : true; - datatypes : true; - quantifiers : true; - arithmetic : regular; - arrays : all; }; }]} - -[logic][parsed][16-79] antecedent: (let (x : 5) in (= x x){(:foo bar)}) -File "tests/typing/pass/smtlib/v2.6/attribute/let_seq.smt2", line 5, character 5-13: -5 | :foo bar +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` -[logic][typed][16-79] hyp_1[16-79]: - hyp: let x/160 = 5/159 in x/160 = x/160 - diff --git a/tests/typing/pass/smtlib/v2.6/attribute/let_seq.smt2 b/tests/typing/pass/smtlib/v2.6/attribute/let_seq.smt2 index 0d7e30640..df38363ed 100644 --- a/tests/typing/pass/smtlib/v2.6/attribute/let_seq.smt2 +++ b/tests/typing/pass/smtlib/v2.6/attribute/let_seq.smt2 @@ -1,3 +1,5 @@ +; 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)) diff --git a/tests/typing/pass/smtlib/v2.6/attribute/nest_pattern.expected b/tests/typing/pass/smtlib/v2.6/attribute/nest_pattern.expected index e2785f50e..80f8eaf22 100644 --- a/tests/typing/pass/smtlib/v2.6/attribute/nest_pattern.expected +++ b/tests/typing/pass/smtlib/v2.6/attribute/nest_pattern.expected @@ -1,21 +1,4 @@ -[logic][parsed][0-15] set-logic: ALL -[logic][typed][0-15] other_1[0-15]: - set-logic: ALL = - { theories: core, arrays, bitv, floats, string, - int+real; - features: { free_sorts : true; - free_functions : true; - datatypes : true; - quantifiers : true; - arithmetic : regular; - arrays : all; }; }]} - -[logic][parsed][16-125] antecedent: - (∀ (x : Int) . - (∀ (y : Int) . (= x y)){(:pattern (sexpr x))}) -[logic][typed][16-125] hyp_1[16-125]: - hyp: - ∀ x/159 : int/4. - { multi-trigger int/4 x/159; } - (∀ y/160 : int/4. x/159 = y/160) - +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 index e86225bb8..27aa5ab8a 100644 --- a/tests/typing/pass/smtlib/v2.6/attribute/nest_pattern.smt2 +++ b/tests/typing/pass/smtlib/v2.6/attribute/nest_pattern.smt2 @@ -1,10 +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) ) - :pattern (x) + :foo bar ) ) ) diff --git a/tests/typing/pass/smtlib/v2.6/attribute/nested_quant.expected b/tests/typing/pass/smtlib/v2.6/attribute/nested_quant.expected deleted file mode 100644 index 64f207fa4..000000000 --- a/tests/typing/pass/smtlib/v2.6/attribute/nested_quant.expected +++ /dev/null @@ -1,17 +0,0 @@ -[logic][parsed][0-15] set-logic: ALL -[logic][typed][0-15] other_1[0-15]: - set-logic: ALL = - { theories: core, arrays, bitv, floats, string, - int+real; - features: { free_sorts : true; - free_functions : true; - datatypes : true; - quantifiers : true; - arithmetic : regular; - arrays : all; }; }]} - -[logic][parsed][16-95] antecedent: - (∀ (x : Int) . (∀ (y : Int) . (= x y))) -[logic][typed][16-95] hyp_1[16-95]: - hyp: ∀ x/159 : int/4, y/160 : int/4. x/159 = y/160 - diff --git a/tests/typing/pass/smtlib/v2.6/attribute/nested_quant.smt2 b/tests/typing/pass/smtlib/v2.6/attribute/nested_quant.smt2 deleted file mode 100644 index 866b05c6e..000000000 --- a/tests/typing/pass/smtlib/v2.6/attribute/nested_quant.smt2 +++ /dev/null @@ -1,8 +0,0 @@ -(set-logic ALL) -(assert - (forall ((x Int)) - (forall ((y Int)) - (= x y) - ) - ) -) diff --git a/tests/typing/pass/smtlib/v2.6/attribute/simple_pattern.expected b/tests/typing/pass/smtlib/v2.6/attribute/simple_pattern.expected index 69b8c86cf..1c03451da 100644 --- a/tests/typing/pass/smtlib/v2.6/attribute/simple_pattern.expected +++ b/tests/typing/pass/smtlib/v2.6/attribute/simple_pattern.expected @@ -1,20 +1,4 @@ -[logic][parsed][0-15] set-logic: ALL -[logic][typed][0-15] other_1[0-15]: - set-logic: ALL = - { theories: core, arrays, bitv, floats, string, - int+real; - features: { free_sorts : true; - free_functions : true; - datatypes : true; - quantifiers : true; - arithmetic : regular; - arrays : all; }; }]} - -[logic][parsed][16-88] antecedent: - (∀ (x : Int) . (= x x){(:pattern (sexpr x))}) -[logic][typed][16-88] hyp_1[16-88]: - hyp: - ∀ x/159 : int/4. - { multi-trigger int/4 x/159; } - (x/159 = x/159) - +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 index e0bd7048b..c2d868bf6 100644 --- a/tests/typing/pass/smtlib/v2.6/attribute/simple_pattern.smt2 +++ b/tests/typing/pass/smtlib/v2.6/attribute/simple_pattern.smt2 @@ -1,8 +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) - :pattern (x) + :foo bar ) ) )