Add warning for unknown attribute (#207)

* Add warning for unknown attribute

* Changes

CHANGES.md

@@ -39,6 +39,13 @@ next
   typechecking (PR#199)
 - Treat smtlib `:named` annotations as implicit definitions as
   required by the spec (PR#199)
+- 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)
 
 ### Loop
 

src/loop/typer.ml

@@ -361,13 +361,12 @@ let unused_term_variable =
           print_var_kind kind Dolmen.Std.Expr.Print.id v)
     ~name:"Unused bound term variable" ()
 
-let error_in_attribute =
-  Report.Warning.mk ~code ~mnemonic:"error-in-attr"
-    ~message:(fun fmt exn ->
-        Format.fprintf fmt
-          "Exception while typing attribute:@ %s"
-          (Printexc.to_string exn))
-    ~name:"Exception while typing an attribute" ()
+let unknown_attribute =
+  Report.Warning.mk ~code ~mnemonic:"unknown-attribute"
+    ~message:(fun fmt id ->
+        Format.fprintf fmt "Unknown attribute (the attribtue was ignored): %a"
+          (pp_wrap Dolmen.Std.Id.print) id)
+    ~name:"Unknown attribute" ()
 
 let superfluous_destructor =
   Report.Warning.mk ~code:Code.bug ~mnemonic:"extra-dstr"
@@ -1228,20 +1227,24 @@ module Typer(State : State.S) = struct
       else warn ~input ~loc st unused_term_variable (kind, v)
 
     (* *)
-    | T.Error_in_attribute exn ->
-      warn ~input ~loc st error_in_attribute exn
     | T.Superfluous_destructor _ ->
       warn ~input ~loc st superfluous_destructor ()
     | T.Shadowing (id, old, _cur) ->
       warn ~input ~loc st shadowing (id, old)
     | T.Redundant_pattern pattern ->
       warn ~input ~loc st redundant_pattern pattern
+
+    (* smtlib2 *)
+    | Smtlib2_Core.Unknown_attribute id ->
+      warn ~input ~loc st unknown_attribute id
     | Smtlib2_Arrays.Extension id ->
       warn ~input ~loc st array_extension id
     | Smtlib2_Ints.Restriction (config, msg)
     | Smtlib2_Reals.Restriction (config, msg)
     | Smtlib2_Reals_Ints.Restriction (config, msg) ->
       warn ~input ~loc st bad_arith_expr (config, msg)
+
+    (* catch-all *)
     | _ ->
       warn ~input ~loc st unknown_warning
         (Obj.Extension_constructor.(name (of_val w)))

src/typecheck/core.ml

@@ -499,6 +499,9 @@ module Smtlib2 = struct
       (T : Dolmen.Intf.Term.Smtlib_Base with type t = Type.T.t
                                          and type cstr := Type.T.Cstr.t) = struct
 
+    type _ Type.warn +=
+      | Unknown_attribute : Dolmen.Std.Id.t -> Dolmen.Std.Term.t Type.warn
+
     type _ Type.err +=
       | Incorrect_sexpression : Dolmen.Intf.Msg.t -> Dolmen.Std.Term.t Type.err
       | Non_closed_named_term : Type.Ty.Var.t list * Type.T.Var.t list -> Dolmen.Std.Term.t Type.err
@@ -641,6 +644,14 @@ module Smtlib2 = struct
             [Type.Add (Tag.triggers, t)]
           ))
 
+      (* Unknown attributes *)
+      | Type.Id ({ name = Simple annot; ns = Attr } as id)
+        when String.length annot > 0 && annot.[0] = ':' ->
+        Type.builtin_tags (fun ast _args ->
+            Type._warn env (Ast ast) (Unknown_attribute id);
+            []
+          )
+
       (* Rewrite rules *)
       | Type.Id id when Id.equal id Id.rwrt_rule ->
         Type.builtin_tags (fun _ast _args -> [Type.Set (Tag.rwrt, ())])

src/typecheck/core.mli

@@ -77,6 +77,9 @@ module Smtlib2 : sig
       (T : Dolmen.Intf.Term.Smtlib_Base with type t = Type.T.t
                                          and type cstr := Type.T.Cstr.t) : sig
 
+    type _ Type.warn +=
+      | Unknown_attribute : Dolmen.Std.Id.t -> Dolmen.Std.Term.t Type.warn
+
     type _ Type.err +=
       | Incorrect_sexpression : Dolmen.Intf.Msg.t -> Dolmen.Std.Term.t Type.err
       | Non_closed_named_term : Type.Ty.Var.t list * Type.T.Var.t list -> Dolmen.Std.Term.t Type.err

src/typecheck/intf.ml

@@ -275,8 +275,6 @@ module type Formulas = sig
     (** Unused quantified type variable *)
     | Unused_term_variable : var_kind * term_var -> Dolmen.Std.Term.t warn
     (** Unused quantified term variable *)
-    | Error_in_attribute : exn -> Dolmen.Std.Term.t warn
-    (** An error occurred wile parsing an attribute *)
     | Superfluous_destructor :
         Dolmen.Std.Id.t * Dolmen.Std.Id.t * term_cst -> Dolmen.Std.Term.t warn
     (** The user implementation of typed terms returned a destructor where

src/typecheck/thf.ml

@@ -333,8 +333,6 @@ module Make
     (* Unused bound type variable *)
     | Unused_term_variable : var_kind * T.Var.t -> Ast.t warn
     (* Unused bound term variable *)
-    | Error_in_attribute : exn -> Ast.t warn
-    (* An error occurred wile parsing an attribute *)
     | Superfluous_destructor : Id.t * Id.t * T.Const.t -> Ast.t warn
     (* The user implementation of typed terms returned a destructor where
        was asked for. This warning can very safely be ignored. *)
@@ -674,6 +672,9 @@ module Make
   (* Convenience functions *)
   (* ************************************************************************ *)
 
+  let _redundant_pattern env ast pat =
+    _warn env (Ast ast) (Redundant_pattern pat)
+
   let _expected env s t res =
     _error env (Ast t) (Expected (s, res))
 
@@ -692,9 +693,6 @@ module Make
   let _bad_poly_arity env ast ty_vars tys =
     _error env (Ast ast) (Bad_poly_arity (ty_vars, tys))
 
-  let _redundant_pattern env ast pat =
-    _warn env (Ast ast) (Redundant_pattern pat)
-
   let _partial_pattern_match env ast missing =
     _error env (Ast ast) (Partial_pattern_match missing)
 
@@ -1571,16 +1569,16 @@ module Make
         | Hook f -> f ast res
       ) res (parse_attrs env [] l)
 
-  and parse_attr env ast =
-    match parse_expr (expect_anything env) ast with
-    | Tags l -> List.map (fun tag -> ast, tag) l
-    | res -> _expected env "tag" ast (Some res)
-
   and parse_attrs env acc = function
     | [] -> acc
     | a :: r ->
       parse_attrs env (parse_attr env a @ acc) r
 
+  and parse_attr env ast =
+    match parse_expr (expect_anything env) ast with
+    | Tags l -> List.map (fun tag -> ast, tag) l
+    | res -> _expected env "tag" ast (Some res)
+
   and parse_var_in_binding_pos env = function
     | { Ast.term = Ast.Symbol s; _ } as t ->
       infer_var_in_binding_pos env t s
@@ -1622,10 +1620,7 @@ module Make
     List.rev ttype_vars, List.rev typed_vars, env'
 
   and parse_binder parse_inner mk b env ast ttype_acc ty_acc body_ast =
-    let [@inline] aux t =
-      parse_binder_aux parse_inner mk b env ast ttype_acc ty_acc t
-    in
-    (wrap_attr[@inlined]) apply_attr env body_ast aux
+    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
     | { Ast.term = Ast.Binder (b', vars, f); _ } when b = b' ->

tests/typing/warnings/unknown_attribute/dune

@@ -0,0 +1,36 @@
+; File auto-generated by gentests.ml
+
+; Auto-generated part begin
+; Test for unknown_attr.smt2
+; Incremental test
+
+(rule
+   (target  unknown_attr.incremental)
+   (deps    (:input unknown_attr.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 unknown_attr.expected unknown_attr.incremental)))
+
+; Full mode test
+
+(rule
+   (target  unknown_attr.full)
+   (deps    (:input unknown_attr.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 unknown_attr.expected unknown_attr.full)))
+
+
+; Auto-generated part end

tests/typing/warnings/unknown_attribute/unknown_attr.expected

@@ -0,0 +1,8 @@
+File "tests/typing/warnings/unknown_attribute/unknown_attr.smt2", line 5, character 6-32:
+5 |       :qid |somefile.ext.161:23|
+          ^^^^^^^^^^^^^^^^^^^^^^^^^^
+Warning Unknown attribute (the attribtue was ignored): `:qid`
+File "tests/typing/warnings/unknown_attribute/unknown_attr.smt2", line 6, character 6-19:
+6 |       :skolemid |0|
+          ^^^^^^^^^^^^^
+Warning Unknown attribute (the attribtue was ignored): `:skolemid`

tests/typing/warnings/unknown_attribute/unknown_attr.smt2

@@ -0,0 +1,10 @@
+(set-logic ALL)
+(assert
+  (forall ((v Int))
+    (! (= v v)
+      :qid |somefile.ext.161:23|
+      :skolemid |0|
+      :pattern (v)
+    )
+  )
+)