Merge pull request #4261 from mtzguido/smtpat-on-fields

Allow SMT patterns in record fields and typeclass methods

Author: mtzguido

src/typechecker/FStarC.TypeChecker.TcTerm.fst

@@ -484,13 +484,16 @@ let check_no_smt_theory_symbols (en:env) (t:term) : ML unit =
           (group <| separate_map (comma ^^ break_ 1) pp tlist)
       ]
 
-let check_smt_pat env t bs c : ML unit =
-    if U.is_smt_lemma t //check patterns cover the bound vars
-    then match c.n with
-        | Comp ({effect_args=[_pre; _post; (pats, _)]}) ->
-            check_pat_fvs t.pos env pats bs;
-            check_no_smt_theory_symbols env pats
-        | _ -> failwith "Impossible: check_smt_pat: not Comp"
+let check_smt_pat env t : ML unit =
+    // Check patterns cover the bound vars
+    if U.is_smt_lemma t then
+      let bs, c = U.arrow_formals_comp t in
+      match c.n with
+      | Comp ({effect_args=[_pre; _post; (pats, _)]}) ->
+          check_pat_fvs t.pos env pats bs;
+          check_no_smt_theory_symbols env pats
+      | _ ->
+        failwith "Impossible: check_smt_pat: not Comp"
 
 (************************************************************************************************************)
 (* Building the environment for the body of a let rec;                                                      *)
@@ -1860,7 +1863,7 @@ and tc_value env (e:term) : ML (term
     let e = {U.arrow bs c with pos=top.pos} in
     (* checks the SMT pattern associated with this function is properly defined with regard to context *)
     if not env.phase1 then
-      check_smt_pat env e bs c;
+      check_smt_pat env e;
     (* taking the maximum of the universes of the computation and of all binders *)
     let u = S.U_max (uc::us) in
     (* create a universe of level u *)

tests/error-messages/Bug1918.fst.json_output.expected

@@ -1 +1 @@
-{"msg":["Expected failure:","Tactic failed","Could not solve typeclass constraint `mon`"],"level":"Info","range":{"def":{"file_name":"Bug1918.fst","start_pos":{"line":11,"col":13},"end_pos":{"line":11,"col":14}},"use":{"file_name":"Bug1918.fst","start_pos":{"line":11,"col":13},"end_pos":{"line":11,"col":14}}},"number":228,"ctx":["While synthesizing term with a tactic","Running tactic for meta-arg","While typechecking the top-level declaration `let comp2`","While typechecking the top-level declaration `[@@expect_failure] let comp2`"]}
+{"msg":["Expected failure:","Tactic failed","Could not solve typeclass constraint `mon`"],"level":"Info","range":{"def":{"file_name":"Bug1918.fst","start_pos":{"line":11,"col":13},"end_pos":{"line":11,"col":14}},"use":{"file_name":"Bug1918.fst","start_pos":{"line":11,"col":13},"end_pos":{"line":11,"col":14}}},"number":228,"ctx":["While synthesizing term with a tactic","Running tactic for meta-arg","While trying to get a subtyping predicate","While typechecking the top-level declaration `let comp2`","While typechecking the top-level declaration `[@@expect_failure] let comp2`"]}

tests/micro-benchmarks/RecordPat1.fst

@@ -0,0 +1,22 @@
+module RecordPat1
+
+noeq
+type deq (a:Type) = {
+  ( =? ) : a -> a -> bool;
+
+  eq_sound :
+    (x:a) -> (y:a) ->
+      Lemma (requires x =? y)
+            (ensures x == y)
+            [SMTPat (x =? y)]
+}
+
+let test0 #t (d : deq t) (x y : t) =
+  if d.op_Equals_Question x y then (
+    d.eq_sound x y;
+    assert (x == y)
+  )
+
+let test1 #t (d : deq t) (x y : t) =
+  if d.op_Equals_Question x y then
+    assert (x == y)

tests/micro-benchmarks/RecordPat2.fst

@@ -0,0 +1,30 @@
+module RecordPat2
+
+class deq (a:Type) = {
+  ( =? ) : a -> a -> bool;
+
+  eq_sound :
+    (x:a) -> (y:a) ->
+      Lemma (requires x =? y)
+            (ensures x == y)
+            [SMTPat (x =? y)]
+}
+
+let test0 #t {| deq t |} (x y : t) =
+  if x =? y then (
+    eq_sound x y;
+    assert (x == y)
+  )
+
+let test1 #t {| d : deq t |} (x y : t) =
+  if d.op_Equals_Question x y then
+    assert (x == y)
+
+let test2 #t {| d : deq t |} (x y : t) =
+  let _ = d.op_Equals_Question x y in
+  if x =? y then
+    assert (x == y)
+
+let test3 #t {| d : deq t |} (x y : t) =
+  if x =? y then
+    assert (x == y)

ulib/FStar.Tactics.Typeclasses.fst

@@ -578,13 +578,25 @@ let mk_class (nm:string) : Tac decls =
             mk_arr (ps@(b1::bs')) cod
       in
       let def =
-        let bs, body = collect_abs proj_lb.lb_def in
-        let ps, bs = List.Tot.Base.splitAt (List.Tot.Base.length params) bs in
-        match bs with
-        | [] -> fail "mk_class: impossible, no binders"
-        | b1::bs' ->
+        if false then
+          let bs, body = collect_abs proj_lb.lb_def in
+          let ps, bs = List.Tot.Base.splitAt (List.Tot.Base.length params) bs in
+          match bs with
+          | [] -> fail "mk_class: impossible, no binders"
+          | b1::bs' ->
+              let b1 = binder_set_meta b1 tcr in
+              mk_abs (ps@(b1::bs')) body
+        else
+          let bs, _cod = collect_arr_bs proj_lb.lb_typ in
+          let ps, bs = List.Tot.Base.splitAt (List.Tot.Base.length params) bs in
+          match bs with
+          | [] -> fail "mk_class: impossible, no binders"
+          | b1::bs' ->
             let b1 = binder_set_meta b1 tcr in
-            mk_abs (ps@(b1::bs')) body
+            mk_abs (ps@[b1]) <|
+              mk_app (Tv_FVar proj_lb.lb_fv)
+                (L.map (fun p -> (binder_to_term p, Q_Implicit)) ps
+                @ [binder_to_term b1, Q_Explicit])
       in
       debug' (fun () -> "def = " ^ term_to_string def);
       debug' (fun () -> "ty  = " ^ term_to_string ty);
@@ -597,7 +609,7 @@ let mk_class (nm:string) : Tac decls =
       let se = pack_sigelt (Sg_Let {isrec=false; lbs=[lb]}) in
       let se = set_sigelt_quals to_propagate se in
       let se = set_sigelt_attrs ((`tcmethod) :: proj_attrs @ b.attrs) se in
-      //debug' (fun () -> "trying to return : " ^ term_to_string (quote se));
+      // debug' (fun () -> "trying to return : " ^ term_to_string (quote se));
       se
     )
-#pop-options
+#pop-options