diff options
| author | Maxime Dénès | 2020-02-27 11:15:02 +0100 |
|---|---|---|
| committer | Maxime Dénès | 2020-03-01 20:33:27 +0100 |
| commit | 38e57715c086183250dd6176f9eaad01bfcde4c5 (patch) | |
| tree | bb6d61b021082fdd17fbcc6c625d4a29550c0b4a /vernac | |
| parent | fd38386b2aa19edf2df05f7b935d2273d9de8b00 (diff) | |
Refactor lookaheads using DSL
Diffstat (limited to 'vernac')
| -rw-r--r-- | vernac/g_vernac.mlg | 23 |
1 files changed, 9 insertions, 14 deletions
diff --git a/vernac/g_vernac.mlg b/vernac/g_vernac.mlg index def4ed942a..8486de3aed 100644 --- a/vernac/g_vernac.mlg +++ b/vernac/g_vernac.mlg @@ -22,7 +22,6 @@ open Extend open Decls open Declaremods open Namegen -open Tok (* necessary for camlp5 *) open Pcoq open Pcoq.Prim @@ -531,16 +530,12 @@ END { -let only_starredidentrefs = - Pcoq.Entry.of_parser "test_only_starredidentrefs" - (fun _ strm -> - let rec aux n = - match Util.stream_nth n strm with - | KEYWORD "." -> () - | KEYWORD ")" -> () - | (IDENT _ | KEYWORD "Type" | KEYWORD "*") -> aux (n+1) - | _ -> raise Stream.Failure in - aux 0) +let test_only_starredidentrefs = + let open Pcoq.Lookahead in + to_entry "test_only_starredidentrefs" begin + lk_list (lk_ident <+> lk_kws ["Type"; "*"]) >> (lk_kws [".";")"]) + end + let starredidentreflist_to_expr l = match l with | [] -> SsEmpty @@ -670,7 +665,7 @@ GRAMMAR EXTEND Gram ; (* Proof using *) section_subset_expr: - [ [ only_starredidentrefs; l = LIST0 starredidentref -> + [ [ test_only_starredidentrefs; l = LIST0 starredidentref -> { starredidentreflist_to_expr l } | e = ssexpr -> { e } ]] ; @@ -688,9 +683,9 @@ GRAMMAR EXTEND Gram | e1 = ssexpr; "+"; e2 = ssexpr-> { SsUnion(e1,e2) } ] | "0" [ i = starredidentref -> { i } - | "("; only_starredidentrefs; l = LIST0 starredidentref; ")"-> + | "("; test_only_starredidentrefs; l = LIST0 starredidentref; ")"-> { starredidentreflist_to_expr l } - | "("; only_starredidentrefs; l = LIST0 starredidentref; ")"; "*" -> + | "("; test_only_starredidentrefs; l = LIST0 starredidentref; ")"; "*" -> { SsFwdClose(starredidentreflist_to_expr l) } | "("; e = ssexpr; ")"-> { e } | "("; e = ssexpr; ")"; "*" -> { SsFwdClose e } ] ] |