Merge pull request #312 from mtzguido/errors

More error improvements, failing on partial applications and sequencing with informative values

lib/pulse/lib/Pulse.Lib.DequeRef.fst

@@ -110,10 +110,10 @@ ensures
   push_front x3 v;
   push_front x4 v;
 
-  pop_front x1;
-  pop_front x2;
-  pop_front x3;
-  pop_front x4;
+  let _ = pop_front x1;
+  let _ = pop_front x2;
+  let _ = pop_front x3;
+  let _ = pop_front x4;
   ()
 }
-#pop-options
+#pop-options

lib/pulse/lib/Pulse.Lib.HashTable.fst

@@ -143,7 +143,7 @@ fn lookup
           {
             cont := false;
             ret := Some idx;
-            V.replace_i_ref contents idx (Used k' v');
+            let _ = V.replace_i_ref contents idx (Used k' v');
             with vcontents. assert (pts_to contents vcontents);
             with s. assert (pts_to vcontents s);
             assert (pure (Seq.equal s pht.repr.seq));
@@ -152,7 +152,7 @@ fn lookup
           } else
           {
             off := voff +^ 1sz;
-            V.replace_i_ref contents idx (Used k' v');
+            let _ = V.replace_i_ref contents idx (Used k' v');
             with vcontents. assert (pts_to contents vcontents);
             with s. assert (pts_to vcontents s);
             assert (pure (Seq.equal s pht.repr.seq));
@@ -163,7 +163,7 @@ fn lookup
         Clean ->
         {
           cont := false;
-          V.replace_i_ref contents idx c;
+          let _ = V.replace_i_ref contents idx c;
           with vcontents. assert (pts_to contents vcontents);
           with s. assert (pts_to vcontents s);
           assert (pure (Seq.equal s pht.repr.seq));
@@ -173,7 +173,7 @@ fn lookup
         Zombie ->
         {
           off := voff +^ 1sz;
-          V.replace_i_ref contents idx c;
+          let _ = V.replace_i_ref contents idx c;
           with vcontents. assert (pts_to contents vcontents);
           with s. assert (pts_to vcontents s);
           assert (pure (Seq.equal s pht.repr.seq));
@@ -447,7 +447,7 @@ fn not_full
     {
       let c = V.replace_i_ref contents vi Zombie;
       let b = is_used c;
-      V.replace_i_ref contents vi (snd b);
+      let _ = V.replace_i_ref contents vi (snd b);
       with vcontents. assert (pts_to contents vcontents);
       with s. assert (V.pts_to vcontents s);
       assert (pure (Seq.equal s pht.repr.seq));

lib/pulse/lib/Pulse.Lib.Pervasives.fst

@@ -209,4 +209,4 @@ fn dup_inames_live (is:inames)
   GhostSet.lemma_equal_intro is (GhostSet.union is is);
   rewrite inames_live is as inames_live (GhostSet.union is is);
   share_inames_live is is;
-}
+}

lib/pulse/lib/Pulse.fst

@@ -1,3 +1,4 @@
 module Pulse
 
 include Pulse.Lib.Pervasives
+include FStar.Mul

share/pulse/examples/Pulse.fst.config.json

@@ -12,7 +12,7 @@
     "4.13.3"
   ],
   "include_dirs": [
-    "../../../lib/pulse",
+    "../../../out/lib/pulse",
     "bug-reports",
     "by-example",
     "parallel",

src/checker/Pulse.Checker.AssertWithBinders.fst

@@ -488,30 +488,18 @@ let check
       ] in
       info_doc_env g (Some st.range) msg
     end;
-    let rw = { term = Tm_Rewrite { t1 = lhs;
-                                   t2 = rhs;
-                                   tac_opt = Some Pulse.Reflection.Util.slprop_equiv_norm_tm };
-               range = st.range;
-               effect_tag = as_effect_hint STT_Ghost;
-               source = Sealed.seal false;
-    } in
-    let st = { term = Tm_Bind { binder = as_binder (wr (`unit) st.range);
-                                head = rw; body };
-               range = st.range;
-               effect_tag = body.effect_tag;
-               source = Sealed.seal false;
-    } in
+
+    let rw = mk_term (Tm_Rewrite { t1 = lhs; t2 = rhs; tac_opt = Some Pulse.Reflection.Util.slprop_equiv_norm_tm }) st.range in
+    let rw = { rw with effect_tag = as_effect_hint STT_Ghost } in
+
+    let st = mk_term (Tm_Bind { binder = as_binder (wr (`unit) st.range); head = rw; body }) st.range in
+    let st = { st with effect_tag = body.effect_tag } in
 
     let st =
       match bs with
       | [] -> st
       | _ ->
-        { term = Tm_ProofHintWithBinders { hint_type = ASSERT { p = lhs };
-                                           binders = bs;
-                                           t = st };
-          range = st.range;
-          effect_tag = st.effect_tag;
-          source = Sealed.seal false;
-        }
+        let t = mk_term (Tm_ProofHintWithBinders { hint_type = ASSERT { p = lhs }; binders = bs; t = st }) st.range in
+        { t with effect_tag = st.effect_tag }
     in
     check g pre pre_typing post_hint res_ppname st

src/checker/Pulse.Checker.Base.fst

@@ -635,13 +635,14 @@ let match_comp_res_with_post_hint (#g:env) (#t:st_term) (#c:comp_st)
     let cres = comp_res c in
     if eq_tm cres ret_ty
     then (| t, c, d |)
-    else match Pulse.Checker.Pure.check_equiv g cres ret_ty with
-         | None ->
-           fail g (Some t.range)
-             (Printf.sprintf "Could not prove equiv for computed type %s and expected type %s"
-                (P.term_to_string cres)
-                (P.term_to_string ret_ty))
-         | Some tok ->
+    else match Pulse.Typing.Util.check_equiv_now (elab_env g) cres ret_ty with
+         | None, issues ->
+           let open Pulse.PP in
+           fail_doc_with_subissues g (Some t.range) issues [
+            prefix 2 1 (text "Could not prove equality between computed type") (pp cres) ^/^
+            prefix 2 1 (text "and expected type") (pp ret_ty);
+           ]
+         | Some tok, _ ->
            let d_equiv
              : RT.equiv _ cres ret_ty =
              RT.Rel_eq_token _ _ _ (FStar.Squash.return_squash tok) in
@@ -807,7 +808,7 @@ let is_stateful_application (g:env) (e:term)
         | _ -> None
       in
       let st_app = Tm_STApp { head; arg=last_arg; arg_qual=qual} in
-      let st_app = { term = st_app; range=RU.range_of_term e; effect_tag=default_effect_hint; source=Sealed.seal false } in
+      let st_app = mk_term st_app (RU.range_of_term e) in
       Some st_app
     | _ -> None
 

src/checker/Pulse.Checker.Bind.fst

@@ -63,7 +63,59 @@ let check_bind_fn
   | _ -> fail g (Some t.range) "check_bind_fn: head is not an abstraction"
 #pop-options
 
-#push-options "--z3rlimit_factor 4 --fuel 1 --ifuel 1"
+let check_if_seq_lhs
+  (g:env) (ctxt : slprop) (post_hint : post_hint_opt g)
+  (r:checker_result_t g ctxt post_hint) (e1:st_term)
+  : T.Tac unit
+=
+  if T.unseal e1.seq_lhs then begin
+    let (| _x, g, (| u, ty, ty_wf |), _ctxt', _k |) = r in
+    let open Pulse.PP in
+    if T.Tv_Arrow? ty then
+      fail_doc g (Some e1.range) [
+        prefix 2 1 (text "This function is partially applied. Remaining type:") (pp ty);
+        text "Did you forget to apply some arguments?";
+      ]
+    else if None? (fst <| T.is_non_informative (elab_env g) ty) then (
+      if None? (Pulse.Checker.Pure.try_get_non_informative_witness g u ty ty_wf) then
+        fail_doc g (Some e1.range) [
+          prefix 2 1 (text "This statement returns a value of type:") (pp ty);
+          text "Did you forget to assign it or ignore it?";
+        ]
+    ) else
+      () (* ok *)
+  end
+
+let check_binder_typ
+  (g:env) (ctxt : slprop) (post_hint : post_hint_opt g)
+  (r:checker_result_t g ctxt post_hint)
+  (b:binder) (e1:st_term)
+  : T.Tac unit
+=
+  (* Check that the type matches the annotation, if any *)
+  let ty = b.binder_ty in
+  begin match inspect_term ty with
+  | Tm_Unknown -> ()
+  | _ ->
+    let (| ty, _, _ |) = compute_tot_term_type g ty in //elaborate it first
+    let (| _, _, (| _, t, _ |), _, _ |) = r in
+    // TODO: once we have the rename operation then we should
+    // ditch this check and just elaborate the bind
+    //   let x : ty = stapp in ...
+    // to
+    //   let x0 = stapp in
+    //   let x : t = x0 in
+    //   rename x0 x; ...
+    // to leverage the pure case
+    if not (eq_tm ty t) then
+      let open Pulse.PP in
+      fail_doc g (Some e1.range) [
+        text "Type mismatch (NB: this is a syntactic check)";
+        prefix 2 1 (text "Expected:") (pp ty);
+        prefix 2 1 (text "Got:") (pp t);
+      ]
+  end
+
 let check_bind
   (g:env)
   (ctxt:slprop)
@@ -94,29 +146,8 @@ let check_bind
   else (
     let (| x, g1, _, (| ctxt', ctxt'_typing |), k1 |) =
       let r = check g ctxt ctxt_typing None binder.binder_ppname e1 in
-      (* Check that the type matches the annotation, if any *)
-      let ty = binder.binder_ty in
-      begin match inspect_term ty with
-      | Tm_Unknown -> ()
-      | _ ->
-        let (| ty, _, _ |) = compute_tot_term_type g ty in //elaborate it first
-        let (| _, _, (| _, t, _ |), _, _ |) = r in
-        // TODO: once we have the rename operation then we should
-        // ditch this check and just elaborate the bind
-        //   let x : ty = stapp in ...
-        // to
-        //   let x0 = stapp in
-        //   let x : t = x0 in
-        //   rename x0 x; ...
-        // to leverage the pure case
-        if not (eq_tm ty t) then
-          let open Pulse.PP in
-          fail_doc g (Some e1.range) [
-            text "Type mismatch (NB: this is a syntactic check)";
-            prefix 2 1 (text "Expected:") (pp ty);
-            prefix 2 1 (text "Got:") (pp t);
-          ]
-      end;
+      check_if_seq_lhs g ctxt None r e1;
+      check_binder_typ g ctxt None r binder e1;
       r
     in
     let g1 = reset_context g1 g in
@@ -156,7 +187,7 @@ let check_tot_bind
 
   | None -> (
     let head = Tm_Return { expected_type = b.binder_ty; term = e1; insert_eq = true } in
-    let head = { term = head; range = Pulse.RuntimeUtils.range_of_term e1; effect_tag = default_effect_hint; source = Sealed.seal false } in
+    let head = mk_term head (Pulse.RuntimeUtils.range_of_term e1) in
     let t = { t with term = Tm_Bind { binder=b; head; body=e2 } } in
     check_bind g pre pre_typing post_hint res_ppname t check
   )

src/checker/Pulse.Checker.If.fst

@@ -65,19 +65,17 @@ let check
         (mk_eq2 u0 tm_bool b eq_v)
     in
 
-    let br = {
-        term =
-          Tm_ProofHintWithBinders {
-            binders = [];
-            hint_type = RENAME { pairs = [(b, eq_v)]; goal=None; tac_opt=None; };
-            t = br;
-          };
-        range = br.range;
-        effect_tag = br.effect_tag;
-        source = Sealed.seal false;
-      }
+    let br =
+      let t =
+        mk_term (Tm_ProofHintWithBinders {
+          binders = [];
+          hint_type = RENAME { pairs = [(b, eq_v)]; goal=None; tac_opt=None; };
+          t = br;
+        }) br.range
+      in
+      { t with effect_tag = br.effect_tag }
     in
-    
+
     let (| br, c, d |) =
       let ppname = mk_ppname_no_range "_if_br" in
       let r =

src/checker/Pulse.Checker.Match.fst

@@ -250,19 +250,16 @@ let check_branch
   let g' = push_binding g' hyp_var ({name = Sealed.seal "branch equality"; range = Range.range_0 }) eq_typ in
   let e = open_st_term_bs e pulse_bs in
   let e =
-    {
-      term =
-        Tm_ProofHintWithBinders {
-          binders = [];
-          hint_type = RENAME { pairs = [(sc, elab_p_tm)];
-                               goal = None;
-                               tac_opt = Some Pulse.Reflection.Util.match_rewrite_tac_tm; };
-          t = e;
-        };
-      range = e.range;
-      effect_tag = e.effect_tag;
-      source = Sealed.seal false;
-    }
+    let t =
+      mk_term (Tm_ProofHintWithBinders {
+                 binders = [];
+                 hint_type = RENAME { pairs = [(sc, elab_p_tm)];
+                                      goal = None;
+                                      tac_opt = Some Pulse.Reflection.Util.match_rewrite_tac_tm; };
+                 t = e; })
+              e.range
+    in
+    { t with effect_tag = e.effect_tag }
   in
   let pre_typing = tot_typing_weakening_n pulse_bs pre_typing in // weaken w/ binders
   let pre_typing = Pulse.Typing.Metatheory.tot_typing_weakening_single pre_typing hyp_var eq_typ in // weaken w/ branch eq

src/checker/Pulse.Checker.Pure.fst

@@ -162,6 +162,7 @@ let readback_failure (s:R.term) =
   Printf.sprintf "Internal error: failed to readback F* term %s"
                  (T.term_to_string s)
 
+(* Set got_typ = None if we don't have a good type for `t`. *)
 let ill_typed_term (t:term) (expected_typ:option term) (got_typ:option term) : Tac (list document) =
   let open Pulse.PP in
   match expected_typ, got_typ with
@@ -170,8 +171,7 @@ let ill_typed_term (t:term) (expected_typ:option term) (got_typ:option term) : T
   ]
   | Some ty, None -> [
     prefix 2 1 (text "Expected term of type") (pp ty) ^/^
-    prefix 2 1 (text "got term") (pp t) ^/^
-    text "of unknown type"
+    prefix 2 1 (text "got term") (pp t)
   ]
   | Some ty, Some ty' -> [
     prefix 2 1 (text "Expected term of type") (pp ty) ^/^

src/checker/Pulse.Checker.STApp.fst

@@ -77,11 +77,9 @@ let rec intro_uvars_for_logical_implicits (g:env) (uvs:env { disjoint g uvs }) (
        | C_ST _
        | C_STAtomic _ _ _
        | C_STGhost _ _ ->
-         (| uvs', push_env g uvs', {term=Tm_STApp {head=t;arg_qual=Some Implicit;arg=t_var};
-                                    range=Pulse.RuntimeUtils.range_of_term t;
-                                    effect_tag=as_effect_hint (ctag_of_comp_st c_rest);
-                                    source = Sealed.seal false;
-                                   }|)
+         let term = mk_term (Tm_STApp {head=t;arg_qual=Some Implicit;arg=t_var}) (RU.range_of_term t) in
+         let term = { term with effect_tag = as_effect_hint (ctag_of_comp_st c_rest) } in
+         (| uvs', push_env g uvs', term |)
        | C_Tot ty ->
          intro_uvars_for_logical_implicits g uvs' (tm_pureapp t (Some Implicit) t_var) ty
     end
@@ -107,7 +105,8 @@ let instantiate_implicits (g:env) (t:st_term { Tm_STApp? t.term })
   | _ ->
     match is_pure_app t with
     | Some (head, q, arg) ->
-      (| uvs, push_env g uvs, {term=Tm_STApp {head;arg_qual=q;arg}; range=Pulse.RuntimeUtils.range_of_term t; effect_tag=default_effect_hint; source = Sealed.seal false } |)
+      let term = mk_term (Tm_STApp {head;arg_qual=q;arg}) range in
+      (| uvs, push_env g uvs, term |)
     | _ ->
       fail g (Some (Pulse.RuntimeUtils.range_of_term t))
         (Printf.sprintf "check_stapp.instantiate_implicits: expected an application term, found: %s"
@@ -189,7 +188,8 @@ let apply_impure_function
           let d : st_typing _ _ (open_comp_with comp_typ arg) =
             T_STApp g head formal bqual comp_typ arg dhead darg in
           let d = canonicalize_st_typing d in
-          let t = { term = Tm_STApp {head; arg_qual=bqual; arg}; range; effect_tag=as_effect_hint (ctag_of_comp_st comp_typ); source=Sealed.seal false } in
+          let t = mk_term (Tm_STApp {head; arg_qual=bqual; arg}) range in
+          let t = { t with effect_tag=as_effect_hint (ctag_of_comp_st comp_typ) } in
           let c = (canon_comp (open_comp_with comp_typ arg)) in
           (| t, c, d |)
         | C_STGhost _ res ->
@@ -220,7 +220,8 @@ let apply_impure_function
               (E d_non_info)
               (lift_typing_to_ghost_typing darg) in
           let d = canonicalize_st_typing d in
-          let t = { term = Tm_STApp {head; arg_qual=bqual; arg}; range; effect_tag=as_effect_hint STT_Ghost; source=Sealed.seal false; } in
+          let t = mk_term (Tm_STApp {head; arg_qual=bqual; arg}) range in
+          let t = { t with effect_tag=as_effect_hint STT_Ghost } in
           let c = (canon_comp (open_comp_with comp_typ arg)) in
           (| t, c, d |)
         | _ ->

src/checker/Pulse.Checker.fst

@@ -96,7 +96,9 @@ let instantiate_unknown_witnesses (g:env) (t:st_term { Tm_IntroExists? t.term })
     let e1 =
       let hint_type = ASSERT { p = opened_p } in
       let binders = [] in
-      {term=Tm_ProofHintWithBinders { hint_type;binders;t=e2 }; range=t.range; effect_tag=as_effect_hint STT_Ghost; source = Sealed.seal false } in
+      let t = mk_term (Tm_ProofHintWithBinders { hint_type;binders;t=e2 }) t.range in
+      { t with effect_tag = as_effect_hint STT_Ghost }
+     in
 
     let t = 
       L.fold_right