From 9b0ac0fc0730e7ce4fe2ea0bb75f083aa1e3f8e9 Mon Sep 17 00:00:00 2001
From: Robbert Krebbers <mail@robbertkrebbers.nl>
Date: Tue, 27 Feb 2018 20:13:51 +0100
Subject: [PATCH] Improve intro and spec pattern parsers.
- Better error messages
- Handle more inputs
---
theories/proofmode/intro_patterns.v | 6 +++---
theories/proofmode/spec_patterns.v | 5 ++++-
2 files changed, 7 insertions(+), 4 deletions(-)
diff --git a/theories/proofmode/intro_patterns.v b/theories/proofmode/intro_patterns.v
index cc8feb04a..e24ab1e67 100644
--- a/theories/proofmode/intro_patterns.v
+++ b/theories/proofmode/intro_patterns.v
@@ -128,11 +128,11 @@ Ltac parse s :=
| intro_pat => constr:([s])
| list string =>
lazymatch eval vm_compute in (mjoin <$> mapM parse s) with
- | Some ?pats => pats | _ => fail "invalid list intro_pat" s
+ | Some ?pats => pats | _ => fail "intro_pat.parse: cannot parse" s
end
| string =>
lazymatch eval vm_compute in (parse s) with
- | Some ?pats => pats | _ => fail "invalid list intro_pat" s
+ | Some ?pats => pats | _ => fail "intro_pat.parse: cannot parse" s
end
| ident => constr:([IIdent s])
| ?X => fail "intro_pat.parse:" s "has unexpected type" X
@@ -142,7 +142,7 @@ Ltac parse_one s :=
| intro_pat => s
| string =>
lazymatch eval vm_compute in (parse s) with
- | Some [?pat] => pat | _ => fail "invalid intro_pat" s
+ | Some [?pat] => pat | _ => fail "intro_pat.parse_one: cannot parse" s
end
| ?X => fail "intro_pat.parse_one:" s "has unexpected type" X
end.
diff --git a/theories/proofmode/spec_patterns.v b/theories/proofmode/spec_patterns.v
index 64201daf2..dd93c0ebe 100644
--- a/theories/proofmode/spec_patterns.v
+++ b/theories/proofmode/spec_patterns.v
@@ -72,8 +72,11 @@ Definition parse (s : string) : option (list spec_pat) :=
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 "invalid list spec_pat" s
+ | Some ?pats => pats | _ => fail "spec_pat.parse: cannot parse" s
end
+ | ident => constr:([SIdent s])
+ | ?X => fail "spec_pat.parse:" s "has unexpected type" X
end.
End spec_pat.
--
GitLab