Merge branch 'gen_proofmode' of https://gitlab.mpi-sws.org/FP/iris-coq into gen_proofmode

339b0438 · Ralf Jung · 4526990e · 5e7a9f2a · 339b0438 · 339b0438
Commit 339b0438 authored Jun 14, 2018 by Ralf Jung
--- a/Makefile.coq.local
+++ b/Makefile.coq.local
@@ -7,11 +7,13 @@ TESTFILES=$(wildcard tests/*.v)
 test: $(TESTFILES:.v=.vo)
 .PHONY: test

+COQ_TEST=$(COQTOP) $(COQDEBUG) -batch -test-mode
+
 $(TESTFILES:.v=.vo): %.vo: %.v $(VFILES:.v=.vo)
-	$(SHOW)COQC [test] $<
+	$(SHOW)COQTOP [test] $<
 	$(HIDE)TEST="$$(basename -s .v $<)" && \
 	  TMPFILE="$$(mktemp)" && \
-	  $(TIMER) $(COQC) $(COQDEBUG) $(TIMING_ARG) $(COQFLAGS) $(COQLIBS) $< $(TIMING_EXTRA) > "$$TMPFILE" && \
+	  $(TIMER) $(COQ_TEST) $(TIMING_ARG) $(COQFLAGS) $(COQLIBS) -load-vernac-source $< $(TIMING_EXTRA) > "$$TMPFILE" && \
 	  (diff -u "tests/$$TEST.ref" "$$TMPFILE" || (rm "tests/$$TEST.vo" "$$TMPFILE" && exit 1)) && \
 	  rm "$$TMPFILE"

@@ -20,6 +22,6 @@ ref: $(TESTFILES:.v=.ref)
 .PHONY: ref

 tests/%.ref: tests/%.v $(VFILES:.v=.vo)
-	$(SHOW)COQC [ref] $<
+	$(SHOW)COQTOP [ref] $<
 	$(HIDE)TEST="$$(basename -s .v $<)" && \
-	  $(TIMER) $(COQC) $(COQDEBUG) $(TIMING_ARG) $(COQFLAGS) $(COQLIBS) $< $(TIMING_EXTRA) > "tests/$$TEST.ref"
+	  $(TIMER) $(COQ_TEST) $(TIMING_ARG) $(COQFLAGS) $(COQLIBS) -load-vernac-source $< $(TIMING_EXTRA) > "tests/$$TEST.ref"
--- a/tests/proofmode.ref
+++ b/tests/proofmode.ref
@@ -31,6 +31,39 @@
  --------------------------------------□
  <affine> (P ∗ Q)
  
+The command has indeed failed with message:
+Ltac call to "done" failed.
+No applicable tactic.
+The command has indeed failed with message:
+In nested Ltac calls to "iClear (constr)", "iElaborateSelPat" and
+"iElaborateSelPat_go", last call failed.
+Tactic failure: iElaborateSelPat: (INamed "HQ") not found.
+The command has indeed failed with message:
+In nested Ltac calls to "iClear (constr)", "iElaborateSelPat" and
+"iElaborateSelPat_go", last call failed.
+Tactic failure: iElaborateSelPat: (INamed "HQ") not found.
+The command has indeed failed with message:
+In nested Ltac calls to "iSpecialize (open_constr)",
+"iSpecializeCore (open_constr) as (constr)",
+"iSpecializeCore (open_constr) as (constr)",
+"iSpecializeCore (open_constr) with (open_constr) (open_constr) as (constr)",
+"iSpecializePat (open_constr) (constr)" and "iSpecializePat_go", last call
+failed.
+Tactic failure: iSpecialize: cannot instantiate (∀ _ : φ, P -∗ False)%I with
+P.
+The command has indeed failed with message:
+In nested Ltac calls to "iSpecialize (open_constr)",
+"iSpecializeCore (open_constr) as (constr)",
+"iSpecializeCore (open_constr) as (constr)",
+"iSpecializeCore (open_constr) with (open_constr) (open_constr) as (constr)",
+"iSpecializePat (open_constr) (constr)" and "iSpecializePat_go", last call
+failed.
+Tactic failure: iSpecialize: cannot instantiate (⌜φ⌝ → P -∗ False)%I with P.
+The command has indeed failed with message:
+In nested Ltac calls to "iFrame (constr)",
+"<iris.proofmode.ltac_tactics.iFrame_go>" and
+"<iris.proofmode.ltac_tactics.iFrameHyp>", last call failed.
+Tactic failure: iFrame: cannot frame Q.
 1 subgoal
  
  PROP : sbi
@@ -151,3 +184,22 @@
  ={E1,E2}=∗ QQQQQQQQQQQQQQQQQQ ∗ QQQQQQQQQQQQQQQQQQ ∗ QQQQQQQQQQQQQQQQQQ
             ={E1,E2}=∗ QQQQQQQQQQQQQQQQQQ ∗ QQQQQQQQQQQQQQQQQQ
  
+The command has indeed failed with message:
+In nested Ltac calls to "iAlways", "iModIntro" and 
+"iModIntro (uconstr)", last call failed.
+Tactic failure: iModIntro: spatial context is non-empty.
+The command has indeed failed with message:
+In nested Ltac calls to "iDestruct (open_constr) as (constr)",
+"iDestructCore (open_constr) as (constr) (tactic)" and
+"iDestructCore (open_constr) as (constr) (tactic)", last call failed.
+Tactic failure: iDestruct: (INamed "HQ") not found.
+The command has indeed failed with message:
+In nested Ltac calls to "iIntros ( (intropattern) )",
+"iIntro ( (intropattern) )" and "intros x", last call failed.
+x is already used.
+The command has indeed failed with message:
+Ltac call to "iSplitL (constr)" failed.
+Tactic failure: iSplitL: hypotheses ["HPx"] not found.
+The command has indeed failed with message:
+Ltac call to "iSplitL (constr)" failed.
+Tactic failure: iSplitL: hypotheses ["HPx"] not found.
--- a/tests/proofmode.v
+++ b/tests/proofmode.v
@@ -499,14 +499,7 @@ Lemma print_long_line (P_P_P_P_P_P_P_P_P_P_P_P_P_P_P_P_P_P_P_P_P_P_P_P_P_P : PRO
  P_P_P_P_P_P_P_P_P_P_P_P_P_P_P_P_P_P_P_P_P_P_P_P_P_P
  -∗ True.
 Proof.
-  iIntros "HP". Show.
-Abort.
-Lemma print_long_line_anon (P_P_P_P_P_P_P_P_P_P_P_P_P_P_P_P_P_P_P_P_P_P_P_P_P_P : PROP) :
-  P_P_P_P_P_P_P_P_P_P_P_P_P_P_P_P_P_P_P_P_P_P_P_P_P_P ∗
-  P_P_P_P_P_P_P_P_P_P_P_P_P_P_P_P_P_P_P_P_P_P_P_P_P_P
-  -∗ True.
-Proof.
-  iIntros "?". Show.
+  iIntros "HP". Show. Undo. iIntros "?". Show.
 Abort.

 (* This is specifically crafted such that not having the printing box in
@@ -517,13 +510,7 @@ Lemma print_long_line (P_P_P_P_P_P_P_P_P_P_P_P_P_P_P_P_P_P_P_P_P_P_P_P_P : PROP)
  TESTNOTATION {{ P_P_P_P_P_P_P_P_P_P_P_P_P_P_P_P_P_P_P_P_P_P_P_P_P | P_P_P_P_P_P_P_P_P_P_P_P_P_P_P_P_P_P_P_P_P_P_P_P_P }}
  -∗ True.
 Proof.
-  iIntros "HP". Show.
-Abort.
-Lemma print_long_line_anon (P_P_P_P_P_P_P_P_P_P_P_P_P_P_P_P_P_P_P_P_P_P_P_P_P : PROP) :
-  TESTNOTATION {{ P_P_P_P_P_P_P_P_P_P_P_P_P_P_P_P_P_P_P_P_P_P_P_P_P | P_P_P_P_P_P_P_P_P_P_P_P_P_P_P_P_P_P_P_P_P_P_P_P_P }}
-  -∗ True.
-Proof.
-  iIntros "?". Show.
+  iIntros "HP". Show. Undo. iIntros "?". Show.
 Abort.

 Lemma long_impl (PPPPPPPPPPPPPPPPP QQQQQQQQQQQQQQQQQQ : PROP) :
@@ -560,3 +547,28 @@ Abort.
 End linebreaks.

 End printing_tests.
+
+(** Test error messages *)
+Section error_tests.
+Context {PROP : sbi}.
+Implicit Types P Q R : PROP.
+
+Lemma iAlways_spatial_non_empty P :
+  P -∗ □ emp.
+Proof. iIntros "HP". Fail iAlways. Abort.
+
+Lemma iDestruct_bad_name P :
+  P -∗ P.
+Proof. iIntros "HP". Fail iDestruct "HQ" as "HP". Abort.
+
+Lemma iIntros_dup_name P :
+  P -∗ ∀ x y : (), P.
+Proof. iIntros "HP" (x). Fail iIntros (x). Abort.
+
+Lemma iSplit_one_of_many P :
+  P -∗ P -∗ P ∗ P.
+Proof.
+  iIntros "HP1 HP2". Fail iSplitL "HP1 HPx". Fail iSplitL "HPx HP1".
+Abort.
+
+End error_tests.
--- a/tests/proofmode_iris.ref
+++ b/tests/proofmode_iris.ref
@@ -107,6 +107,24 @@
  --------------------------------------∗
  |={⊤}=> na_own t E1 ∗ na_own t E2 ∗ ▷ P
  
+The command has indeed failed with message:
+In nested Ltac calls to "iInv (constr) as (constr)",
+"iInvCore (constr) in (tactic)" and
+"iInvCore (constr) with (constr) as (open_constr) in (tactic)", last call
+failed.
+Tactic failure: iInv: selector 34 is not of the right type .
+The command has indeed failed with message:
+In nested Ltac calls to "iInv (constr) as (constr)",
+"iInvCore (constr) in (tactic)" and
+"iInvCore (constr) with (constr) as (open_constr) in (tactic)", last call
+failed.
+Tactic failure: iInv: invariant nroot not found.
+The command has indeed failed with message:
+In nested Ltac calls to "iInv (constr) as (constr)",
+"iInvCore (constr) in (tactic)" and
+"iInvCore (constr) with (constr) as (open_constr) in (tactic)", last call
+failed.
+Tactic failure: iInv: invariant "H2" not found.
 1 subgoal
  
  Σ : gFunctors

--- a/tests/proofmode_monpred.ref
+++ b/tests/proofmode_monpred.ref
@@ -57,3 +57,8 @@
  --------------------------------------∗
  ∀ _ : (), ∃ _ : (), emp
  
+The command has indeed failed with message:
+In nested Ltac calls to "iFrame (constr)",
+"<iris.proofmode.ltac_tactics.iFrame_go>" and
+"<iris.proofmode.ltac_tactics.iFrameHyp>", last call failed.
+Tactic failure: iFrame: cannot frame (P i).
--- a/theories/proofmode/ltac_tactics.v
+++ b/theories/proofmode/ltac_tactics.v
@@ -149,28 +149,28 @@ Local Inductive esel_pat :=
  | ESelPure
  | ESelIdent : bool → ident → esel_pat.

+Ltac iElaborateSelPat_go pat Δ Hs :=
+  lazymatch pat with
+  | [] => eval cbv in Hs
+  | SelPure :: ?pat =>  iElaborateSelPat_go pat Δ (ESelPure :: Hs)
+  | SelPersistent :: ?pat =>
+    let Hs' := eval env_cbv in (env_dom (env_intuitionistic Δ)) in
+    let Δ' := eval env_cbv in (envs_clear_persistent Δ) in
+    iElaborateSelPat_go pat Δ' ((ESelIdent true <$> Hs') ++ Hs)
+  | SelSpatial :: ?pat =>
+    let Hs' := eval env_cbv in (env_dom (env_spatial Δ)) in
+    let Δ' := eval env_cbv in (envs_clear_spatial Δ) in
+    iElaborateSelPat_go pat Δ' ((ESelIdent false <$> Hs') ++ Hs)
+  | SelIdent ?H :: ?pat =>
+    lazymatch eval env_cbv in (envs_lookup_delete false H Δ) with
+    | Some (?p,_,?Δ') =>  iElaborateSelPat_go pat Δ' (ESelIdent p H :: Hs)
+    | None => fail "iElaborateSelPat:" H "not found"
+    end
+  end.
 Ltac iElaborateSelPat pat :=
-  let rec go pat Δ Hs :=
-    lazymatch pat with
-    | [] => eval cbv in Hs
-    | SelPure :: ?pat => go pat Δ (ESelPure :: Hs)
-    | SelPersistent :: ?pat =>
-       let Hs' := eval env_cbv in (env_dom (env_intuitionistic Δ)) in
-       let Δ' := eval env_cbv in (envs_clear_persistent Δ) in
-       go pat Δ' ((ESelIdent true <$> Hs') ++ Hs)
-    | SelSpatial :: ?pat =>
-       let Hs' := eval env_cbv in (env_dom (env_spatial Δ)) in
-       let Δ' := eval env_cbv in (envs_clear_spatial Δ) in
-       go pat Δ' ((ESelIdent false <$> Hs') ++ Hs)
-    | SelIdent ?H :: ?pat =>
-       lazymatch eval env_cbv in (envs_lookup_delete false H Δ) with
-       | Some (?p,_,?Δ') => go pat Δ' (ESelIdent p H :: Hs)
-       | None => fail "iElaborateSelPat:" H "not found"
-       end
-    end in
  lazymatch goal with
  | |- envs_entails ?Δ _ =>
-    let pat := sel_pat.parse pat in go pat Δ (@nil esel_pat)
+    let pat := sel_pat.parse pat in iElaborateSelPat_go pat Δ (@nil esel_pat)
  end.

 Local Ltac iClearHyp H :=
@@ -351,16 +351,17 @@ Tactic Notation "iFrame" "(" constr(t1) constr(t2) constr(t3) constr(t4)
    constr(t5) constr(t6) constr(t7) constr(t8)")" :=
  iFramePure t1; iFrame ( t2 t3 t4 t5 t6 t7 t8 ).

+Local Ltac iFrame_go Hs :=
+  lazymatch Hs with
+  | [] => idtac
+  | SelPure :: ?Hs => iFrameAnyPure; iFrame_go Hs
+  | SelPersistent :: ?Hs => iFrameAnyPersistent; iFrame_go Hs
+  | SelSpatial :: ?Hs => iFrameAnySpatial; iFrame_go Hs
+  | SelIdent ?H :: ?Hs => iFrameHyp H; iFrame_go Hs
+  end.
+
 Tactic Notation "iFrame" constr(Hs) :=
-  let rec go Hs :=
-    lazymatch Hs with
-    | [] => idtac
-    | SelPure :: ?Hs => iFrameAnyPure; go Hs
-    | SelPersistent :: ?Hs => iFrameAnyPersistent; go Hs
-    | SelSpatial :: ?Hs => iFrameAnySpatial; go Hs
-    | SelIdent ?H :: ?Hs => iFrameHyp H; go Hs
-    end
-  in let Hs := sel_pat.parse Hs in go Hs.
+  let Hs := sel_pat.parse Hs in iFrame_go Hs.
 Tactic Notation "iFrame" "(" constr(t1) ")" constr(Hs) :=
  iFramePure t1; iFrame Hs.
 Tactic Notation "iFrame" "(" constr(t1) constr(t2) ")" constr(Hs) :=
@@ -514,7 +515,7 @@ Local Tactic Notation "iSpecializeArgs" constr(H) open_constr(xs) :=
    end in
  go xs.

-Local Tactic Notation "iSpecializePat" open_constr(H) constr(pat) :=
+Ltac iSpecializePat_go H1 pats :=
  let solve_to_wand H1 :=
    iSolveTC ||
    let P := match goal with |- IntoWand _ _ ?P _ _ => P end in
@@ -527,12 +528,11 @@ Local Tactic Notation "iSpecializePat" open_constr(H) constr(pat) :=
       fail "iSpecialize: cannot solve" Q "using done"
    | false => idtac
    end in
-  let rec go H1 pats :=
-    lazymatch pats with
+  lazymatch pats with
    | [] => idtac
    | SForall :: ?pats =>
       idtac "[IPM] The * specialization pattern is deprecated because it is applied implicitly.";
-       go H1 pats
+       iSpecializePat_go H1 pats
    | SIdent ?H2 :: ?pats =>
       notypeclasses refine (tac_specialize _ _ _ H2 _ H1 _ _ _ _ _ _ _ _ _ _);
         [env_reflexivity || fail "iSpecialize:" H2 "not found"
@@ -541,7 +541,7 @@ Local Tactic Notation "iSpecializePat" open_constr(H) constr(pat) :=
          let P := match goal with |- IntoWand _ _ ?P ?Q _ => P end in
          let Q := match goal with |- IntoWand _ _ ?P ?Q _ => Q end in
          fail "iSpecialize: cannot instantiate" P "with" Q
-         |env_reflexivity|go H1 pats]
+         |env_reflexivity|iSpecializePat_go H1 pats]
    | SPureGoal ?d :: ?pats =>
       notypeclasses refine (tac_specialize_assert_pure _ _ H1 _ _ _ _ _ _ _ _ _ _ _ _);
         [env_reflexivity || fail "iSpecialize:" H1 "not found"
@@ -551,7 +551,7 @@ Local Tactic Notation "iSpecializePat" open_constr(H) constr(pat) :=
          fail "iSpecialize:" Q "not pure"
         |env_reflexivity
         |solve_done d (*goal*)
-         |go H1 pats]
+         |iSpecializePat_go H1 pats]
    | SGoal (SpecGoal GPersistent false ?Hs_frame [] ?d) :: ?pats =>
       notypeclasses refine (tac_specialize_assert_persistent _ _ _ H1 _ _ _ _ _ _ _ _ _ _ _ _ _);
         [env_reflexivity || fail "iSpecialize:" H1 "not found"
@@ -562,7 +562,7 @@ Local Tactic Notation "iSpecializePat" open_constr(H) constr(pat) :=
         |iSolveTC
         |env_reflexivity
         |iFrame Hs_frame; solve_done d (*goal*)
-         |go H1 pats]
+         |iSpecializePat_go H1 pats]
    | SGoal (SpecGoal GPersistent _ _ _ _) :: ?pats =>
       fail "iSpecialize: cannot select hypotheses for persistent premise"
    | SGoal (SpecGoal ?m ?lr ?Hs_frame ?Hs ?d) :: ?pats =>
@@ -578,7 +578,7 @@ Local Tactic Notation "iSpecializePat" open_constr(H) constr(pat) :=
          let Hs' := iMissingHyps Hs' in
          fail "iSpecialize: hypotheses" Hs' "not found"
         |iFrame Hs_frame; solve_done d (*goal*)
-         |go H1 pats]
+         |iSpecializePat_go H1 pats]
    | SAutoFrame GPersistent :: ?pats =>
       notypeclasses refine (tac_specialize_assert_persistent _ _ _ H1 _ _ _ _ _ _ _ _ _ _ _ _ _);
         [env_reflexivity || fail "iSpecialize:" H1 "not found"
@@ -588,7 +588,7 @@ Local Tactic Notation "iSpecializePat" open_constr(H) constr(pat) :=
          fail "iSpecialize:" Q "not persistent"
         |env_reflexivity
         |solve [iFrame "∗ #"]
-         |go H1 pats]
+         |iSpecializePat_go H1 pats]
    | SAutoFrame ?m :: ?pats =>
       notypeclasses refine (tac_specialize_frame _ _ H1 _ _ _ _ _ _ _ _ _ _ _ _);
         [env_reflexivity || fail "iSpecialize:" H1 "not found"
@@ -602,8 +602,11 @@ Local Tactic Notation "iSpecializePat" open_constr(H) constr(pat) :=
            |notypeclasses refine (tac_unlock_True _ _ _)
            |iFrame "∗ #"; notypeclasses refine (tac_unlock _ _ _)
            |fail "iSpecialize: premise cannot be solved by framing"]
-         |exact eq_refl]; iIntro H1; go H1 pats
-    end in let pats := spec_pat.parse pat in go H pats.
+         |exact eq_refl]; iIntro H1; iSpecializePat_go H1 pats
+    end.
+
+Local Tactic Notation "iSpecializePat" open_constr(H) constr(pat) :=
+  let pats := spec_pat.parse pat in iSpecializePat_go H pats.

 (* The argument [p] denotes whether the conclusion of the specialized term is
 persistent. If so, one can use all spatial hypotheses for both proving the