Commit 9b0ac0fc authored by Robbert Krebbers's avatar Robbert Krebbers
Browse files

Improve intro and spec pattern parsers.

- Better error messages
- Handle more inputs
parent 45b378c1
...@@ -128,11 +128,11 @@ Ltac parse s := ...@@ -128,11 +128,11 @@ Ltac parse s :=
| intro_pat => constr:([s]) | intro_pat => constr:([s])
| list string => | list string =>
lazymatch eval vm_compute in (mjoin <$> mapM parse s) with 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 end
| string => | string =>
lazymatch eval vm_compute in (parse s) with 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 end
| ident => constr:([IIdent s]) | ident => constr:([IIdent s])
| ?X => fail "intro_pat.parse:" s "has unexpected type" X | ?X => fail "intro_pat.parse:" s "has unexpected type" X
...@@ -142,7 +142,7 @@ Ltac parse_one s := ...@@ -142,7 +142,7 @@ Ltac parse_one s :=
| intro_pat => s | intro_pat => s
| string => | string =>
lazymatch eval vm_compute in (parse s) with 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 end
| ?X => fail "intro_pat.parse_one:" s "has unexpected type" X | ?X => fail "intro_pat.parse_one:" s "has unexpected type" X
end. end.
......
...@@ -72,8 +72,11 @@ Definition parse (s : string) : option (list spec_pat) := ...@@ -72,8 +72,11 @@ Definition parse (s : string) : option (list spec_pat) :=
Ltac parse s := Ltac parse s :=
lazymatch type of s with lazymatch type of s with
| list spec_pat => s | list spec_pat => s
| spec_pat => constr:([s])
| string => lazymatch eval vm_compute in (parse s) with | 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 end
| ident => constr:([SIdent s])
| ?X => fail "spec_pat.parse:" s "has unexpected type" X
end. end.
End spec_pat. End spec_pat.
Markdown is supported
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