Fix typing of attributes in nested binders + tests

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); _ }

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

tests/typing/pass/smtlib/v2.6/attribute/flags.dune

@@ -0,0 +1 @@
+--debug

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
+

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

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

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

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

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