Merge pull request #516 from FStarLang/gebner_impure_spec_prover

Use default prover for impure specs too.

Author: gebner

src/checker/Pulse.Checker.ImpureSpec.fst

@@ -60,63 +60,10 @@ let rec get_rewrites_to_from_post (g: env) xres (post: slprop) : T.Tac (option R
       | _ -> None)
   | _ -> None
 
-let prove_this (g: env) (goal: slprop) (ctxt: list slprop) : T.Tac (option (list slprop)) =
-  match inspect_term goal with
-  | Tm_Pure p ->
-    // TODO: pure (x == ?u)
-    Some []
-  | Tm_ExistsSL u b body ->
-    let uv = RU.new_implicit_var "witness for exists*" (RU.range_of_term goal) (elab_env g) b.binder_ty false in
-    Some (slprop_as_list (open_term' body uv 0))
-  | Tm_WithPure p _ body ->
-    Some (tm_pure p :: slprop_as_list (open_term' body unit_const 0))
-  | Tm_Star a b ->
-    Some [a; b]
-  | _ ->
-    let rec try_match (ctxt: list slprop) : Dv bool =
-      match ctxt with
-      | [] -> false
-      | c::ctxt ->
-        if RU.teq_nosmt_force_phase1 (elab_env g) goal c then
-          true
-        else
-          try_match ctxt
-      in
-    if try_match ctxt then
-      Some []
-    else
-      None
-
-let rec prove_step (g: env) (goals: list slprop) (ctxt: list slprop) : T.Tac (option (list slprop)) =
-  match goals with
-  | [] -> None
-  | goal::goals ->
-    match prove_this g goal ctxt with
-    | Some new_goals -> Some (new_goals @ goals)
-    | None ->
-      match prove_step g goals ctxt with
-      | Some stepped -> Some (goal :: stepped)
-      | None -> None
-
-let rec prove_loop (g: env) (goals: list slprop) (ctxt: list slprop) : T.Tac (list slprop) =
-  match prove_step g goals ctxt with
-  | Some new_goals -> prove_loop g new_goals ctxt
-  | None -> goals
-
 let prove (g: env) (goal: slprop) (ctxt: slprop) (r: range) : T.Tac unit =
-  let (| goal, _ |) = normalize_slprop g goal true in
-  let goal = slprop_as_list goal in
-  let (| ctxt, _ |) = normalize_slprop g ctxt true in
-  let ctxt = slprop_as_list ctxt in
-  match prove_loop g goal ctxt with
-  | [] -> ()
-  | unsolved_goals ->
-    T.fail_doc_at [
-      text "Cannot prove remaining precondition:";
-      separate hardline (T.map pp unsolved_goals);
-      text "from context:";
-      separate hardline (T.map pp ctxt);
-    ] (Some r)
+  let allow_amb = true in
+  let (| g', ctxt', _ |) = Pulse.Checker.Prover.prove r g ctxt goal allow_amb in
+  ()
 
 let symb_eval_stateful_app (g: env) (ctxt: slprop) (t: term) : T.Tac R.term =
   let t, ty, _ = tc_term_phase1 g t in

src/checker/Pulse.Checker.Prover.fst

@@ -535,7 +535,7 @@ let check_slprop_equiv_ext r (g:env) (p q:slprop)
   match res with
   | None -> 
     fail_doc_with_subissues g (Some r) issues [
-      text "rewrite: could not prove equality of";
+      text "Could not prove equality of:";
       pp p;
       pp q;
     ]
@@ -1097,11 +1097,12 @@ let prove rng (g: env) (ctxt goals: slprop) allow_amb :
       ] else []))
     (Some rng)
   else
-    let before, after = k g' in
-    let h: slprop_equiv g' (elab_slprops (solved' @ ctxt')) (elab_slprops (ctxt' @ solved' @ goals')) = RU.magic () in
-    let k = cont_elab_trans before (cont_elab_frame after ctxt') h [] in
-    let h: slprop_equiv g' (elab_slprops (ctxt' @ [Unknown goals])) (tm_star goals (elab_slprops ctxt')) = RU.magic () in
-    (| g', RU.deep_compress_safe (elab_slprops ctxt'), k_elab_equiv k (VE_Refl _ _) h |)
+    (| g', RU.deep_compress_safe (elab_slprops ctxt'), fun post_hint post_hint_typ ->
+      let before, after = k g' in
+      let h: slprop_equiv g' (elab_slprops (solved' @ ctxt')) (elab_slprops (ctxt' @ solved' @ goals')) = RU.magic () in
+      let k = cont_elab_trans before (cont_elab_frame after ctxt') h [] in
+      let h: slprop_equiv g' (elab_slprops (ctxt' @ [Unknown goals])) (tm_star goals (elab_slprops ctxt')) = RU.magic () in
+      k_elab_equiv k (VE_Refl _ _) h post_hint post_hint_typ |)
 
 #restart-solver
 #push-options "--z3rlimit_factor 2"
@@ -1195,10 +1196,10 @@ let elim_exists_and_pure (#g:env) (#ctxt:slprop)
   let ctxt' = Pulse.Checker.Prover.Substs.ss_term ctxt ss in
   let (| g', ctxt'', goals'', solved, k |) = try_elim_core g [Unknown ctxt'] in
   let h: tot_typing g' (elab_slprops ctxt'') tm_slprop = RU.magic () in // TODO thread through prover
-  let h1: slprop_equiv g (elab_slprops ([] @ [Unknown ctxt'])) ctxt = (RU.magic() <: slprop_equiv g ctxt' ctxt) in
-  let h2: slprop_equiv g' (elab_slprops (ctxt'' @ solved @ goals'')) (elab_slprops ([] @ solved @ ctxt'')) = RU.magic () in
-  let h3: slprop_equiv g' (elab_slprops (ctxt'' @ [])) (elab_slprops ctxt'') = RU.magic () in
-  let before, after = k g' in
-  (| g', elab_slprops ctxt'', h,
+  (| g', elab_slprops ctxt'', h, fun post_hint post_hint_typ ->
+    let h1: slprop_equiv g (elab_slprops ([] @ [Unknown ctxt'])) ctxt = (RU.magic() <: slprop_equiv g ctxt' ctxt) in
+    let h2: slprop_equiv g' (elab_slprops (ctxt'' @ solved @ goals'')) (elab_slprops ([] @ solved @ ctxt'')) = RU.magic () in
+    let h3: slprop_equiv g' (elab_slprops (ctxt'' @ [])) (elab_slprops ctxt'') = RU.magic () in
+    let before, after = k g' in
     k_elab_trans (k_elab_equiv (before []) h1 (VE_Refl _ _))
-      (k_elab_equiv (after ctxt'') h2 h3) |)
+      (k_elab_equiv (after ctxt'') h2 h3) post_hint post_hint_typ |)

test/LoopInvariants.fst.output.expected

@@ -2,23 +2,23 @@
   - Expected failure:
   - When using multiple invariants, they must all be in the "new" style without a binder.
 
-* Info at LoopInvariants.fst(77,4-77,8):
+* Info at LoopInvariants.fst(76,20-77,8):
   - Expected failure:
-  - rewrite: could not prove equality of
+  - Could not prove equality of:
   - Pulse.Lib.Reference.pts_to s 3
   - Pulse.Lib.Reference.pts_to s 2
   - Assertion failed
   - The SMT solver could not prove the query. Use --query_stats for more
     details.
-  - See also LoopInvariants.fst(77,4-77,10)
+  - See also LoopInvariants.fst(76,20-77,10)
 
-* Info at LoopInvariants.fst(88,4-88,8):
+* Info at LoopInvariants.fst(86,2-88,8):
   - Expected failure:
-  - rewrite: could not prove equality of
+  - Could not prove equality of:
   - Pulse.Lib.Reference.pts_to s 3
   - Pulse.Lib.Reference.pts_to s 2
   - Assertion failed
   - The SMT solver could not prove the query. Use --query_stats for more
     details.
-  - See also LoopInvariants.fst(88,4-88,10)
+  - See also LoopInvariants.fst(86,2-88,10)
 

test/bug-reports/Bug174.fst.output.expected

@@ -1,9 +1,14 @@
-* Info at Bug174.fst(15,1-16,42):
+* Info at Bug174.fst(16,30-16,42):
   - Expected failure:
-  - rewrite: could not prove equality of
-  - Pulse.Lib.Reference.pts_to r v
-  - Pulse.Lib.Reference.pts_to r v
+  - Ill-typed term: !r
+  - Expected a term of type
+      Pulse.Lib.Core.stt FStar.SizeT.t
+        (r |-> Pulse.Class.PtsTo.Frac 1.0R v)
+        (fun x ->
+            r |-> Pulse.Class.PtsTo.Frac 1.0R v **
+            Pulse.Lib.Core.rewrites_to x v)
   - Assertion failed
   - The SMT solver could not prove the query. Use --query_stats for more
     details.
+  - See also Bug174.fst(15,1-16,40)
 

test/bug-reports/ExistsErasedAndPureEqualities.fst.output.expected

@@ -9,9 +9,9 @@
       v#269 : FStar.Ghost.erased Prims.int,
       x#263 : Pulse.Lib.Reference.ref Prims.int
 
-* Info at ExistsErasedAndPureEqualities.fst(70,4-71,21):
+* Info at ExistsErasedAndPureEqualities.fst(70,32-72,5):
   - Expected failure:
-  - Failed to prove pure property: v == (*?u102*)_
+  - Ill-typed term: pure (v == (*?u102*)_)
+  - Expected a term of type slprop
   - Cannot check relation with uvars.
-  - See also ExistsErasedAndPureEqualities.fst(70,23-71,15)