Commit c93646f0 authored by Ralf Jung's avatar Ralf Jung
Browse files

Merge branch 'robbert/sel_pat_parse' into 'master'

Let `sel_pat.parse` fail with proper error when type is incorrect

Closes #421

See merge request iris/iris!704
parents 90492593 52547f53
......@@ -136,23 +136,32 @@ Ltac parse s :=
| intro_pat => constr:([s])
| list string =>
lazymatch eval vm_compute in (mjoin <$> mapM parse s) with
| Some ?pats => pats | _ => fail "intro_pat.parse: cannot parse" s
| Some ?pats => pats
| _ => fail "intro_pat.parse: cannot parse" s "as an introduction pattern"
end
| string =>
lazymatch eval vm_compute in (parse s) with
| Some ?pats => pats | _ => fail "intro_pat.parse: cannot parse" s
| Some ?pats => pats
| _ => fail "intro_pat.parse: cannot parse" s "as an introduction pattern"
end
| ident => constr:([IIdent s])
| ?X => fail "intro_pat.parse:" s "has unexpected type" X
| ?X => fail "intro_pat.parse: the term" s
"is expected to be an introduction pattern"
"(usually a string),"
"but has unexpected type" X
end.
Ltac parse_one s :=
lazymatch type of s with
| intro_pat => s
| string =>
lazymatch eval vm_compute in (parse s) with
| Some [?pat] => pat | _ => fail "intro_pat.parse_one: cannot parse" s
| Some [?pat] => pat
| _ => fail "intro_pat.parse_one: cannot parse" s "as an introduction pattern"
end
| ?X => fail "intro_pat.parse_one:" s "has unexpected type" X
| ?X => fail "intro_pat.parse_one: the term" s
"is expected to be an introduction pattern"
"(usually a string),"
"but has unexpected type" X
end.
End intro_pat.
......@@ -176,5 +185,8 @@ Ltac intro_pat_intuitionistic p :=
eval cbv in (forallb intro_pat_intuitionistic pat)
| ident => false
| bool => p
| ?X => fail "intro_pat_intuitionistic:" p "has unexpected type" X
| ?X => fail "intro_pat_intuitionistic: the term" p
"is expected to be an introduction pattern"
"(usually a string),"
"but has unexpected type" X
end.
......@@ -37,7 +37,12 @@ Ltac parse s :=
| list string => eval vm_compute in (SelIdent INamed <$> s)
| string =>
lazymatch eval vm_compute in (parse s) with
| Some ?pats => pats | _ => fail "invalid sel_pat" s
| Some ?pats => pats
| _ => fail "sel_pat.parse: cannot parse" s "as a selection pattern"
end
| ?X => fail "sel_pat.parse: the term" s
"is expected to be a selection pattern"
"(usually a string),"
"but has unexpected type" X
end.
End sel_pat.
......@@ -92,10 +92,15 @@ Ltac parse s :=
lazymatch type of s with
| list spec_pat => s
| spec_pat => constr:([s])
| string => lazymatch eval vm_compute in (parse s) with
| Some ?pats => pats | _ => fail "spec_pat.parse: cannot parse" s
end
| string =>
lazymatch eval vm_compute in (parse s) with
| Some ?pats => pats
| _ => fail "spec_pat.parse: cannot parse" s "as a specialization pattern"
end
| ident => constr:([SIdent s []])
| ?X => fail "spec_pat.parse:" s "has unexpected type" X
| ?X => fail "spec_pat.parse: the term" s
"is expected to be a specialization pattern"
"(usually a string),"
"but has unexpected type" X
end.
End spec_pat.
......@@ -727,6 +727,18 @@ The command has indeed failed with message:
Tactic failure:
"Only non-mask-changing update modalities can be introduced directly.
Use [iApply fupd_mask_intro] to introduce mask-changing update modalities".
"iRevert_wrong_sel_pat"
: string
The command has indeed failed with message:
Tactic failure: sel_pat.parse: the term n
is expected to be a selection pattern (usually a string),
but has unexpected type nat.
"iInduction_wrong_sel_pat"
: string
The command has indeed failed with message:
Tactic failure: sel_pat.parse: the term m
is expected to be a selection pattern (usually a string),
but has unexpected type nat.
"test_pure_name"
: string
1 goal
......
......@@ -1435,6 +1435,20 @@ Proof.
Fail iIntros "!>".
Abort.
Check "iRevert_wrong_sel_pat".
Lemma iRevert_wrong_sel_pat (n m : nat) (P Q : nat PROP) :
n = m - P n - P m.
Proof.
Fail iRevert n.
Abort.
Check "iInduction_wrong_sel_pat".
Lemma iInduction_wrong_sel_pat (n m : nat) (P Q : nat PROP) :
n = m - P n - P m.
Proof.
Fail iInduction n as [|n] "IH" forall m.
Abort.
End error_tests.
Section pure_name_tests.
......
Supports Markdown
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment