diff options
| author | herbelin | 2002-11-07 14:14:56 +0000 |
|---|---|---|
| committer | herbelin | 2002-11-07 14:14:56 +0000 |
| commit | 10e75ab2885f8c55c3df8628db2780ffb8482f90 (patch) | |
| tree | 093913ed48d2eb66b744f6c778d1dbcadf23e789 /parsing | |
| parent | ca90f1c666f9ab936adc5c9c3965dfd1b1d5cdf1 (diff) | |
Un hack camlp4 qui marche à tous les coups pour continuer à parser '(n)' comme un entier de nat
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3222 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'parsing')
| -rw-r--r-- | parsing/g_cases.ml4 | 4 | ||||
| -rw-r--r-- | parsing/g_constr.ml4 | 21 |
2 files changed, 24 insertions, 1 deletions
diff --git a/parsing/g_cases.ml4 b/parsing/g_cases.ml4 index 6bee39b122..e84a890920 100644 --- a/parsing/g_cases.ml4 +++ b/parsing/g_cases.ml4 @@ -18,6 +18,10 @@ GEXTEND Gram pattern: [ [ qid = global -> qid + (* Hack to parse syntax "(n)" as a natural number *) + | "("; G_constr.test_int_rparen; n = INT; ")" -> + let n = Coqast.Str (loc,n) in + <:ast< (PATTDELIMITERS "nat_scope" (PATTNUMERAL $n)) >> | "("; p = compound_pattern; ")" -> p | n = INT -> let n = Coqast.Str (loc,n) in <:ast< (PATTNUMERAL $n) >> diff --git a/parsing/g_constr.ml4 b/parsing/g_constr.ml4 index df8c7bbeef..620b6a8002 100644 --- a/parsing/g_constr.ml4 +++ b/parsing/g_constr.ml4 @@ -13,6 +13,20 @@ open Pcoq open Constr +(* Hack to parse "(n)" as nat without conflicts with the (useless) *) +(* admissible notation "(n)" *) +let test_int_rparen = + Gram.Entry.of_parser "test_int_rparen" + (fun strm -> + match Stream.npeek 1 strm with + | [("INT", _)] -> + begin match Stream.npeek 2 strm with + | [_; ("", ")")] -> () + | _ -> raise Stream.Failure + end + | _ -> raise Stream.Failure) + + GEXTEND Gram GLOBAL: constr0 constr1 constr2 constr3 lassoc_constr4 constr5 constr6 constr7 constr8 constr9 constr10 lconstr constr @@ -71,6 +85,10 @@ GEXTEND Gram | "?"; n = Prim.natural -> let n = Coqast.Num (loc,n) in <:ast< (META $n) >> | bl = binders; c = constr -> <:ast< ($ABSTRACT "LAMBDALIST" $bl $c) >> + (* Hack to parse syntax "(n)" as a natural number *) + | "("; test_int_rparen; n = INT; ")" -> + let n = Coqast.Str (loc,n) in + <:ast< (DELIMITERS "nat_scope" (NUMERAL $n)) >> | "("; lc1 = lconstr; ":"; c = constr; body = product_tail -> let id = Ast.coerce_to_var lc1 in <:ast< (PROD $c [$id]$body) >> @@ -147,7 +165,8 @@ GEXTEND Gram IDENT "if"; c1 = constr; IDENT "then"; c2 = constr; IDENT "else"; c3 = constr -> <:ast< (IF $l1 $c1 $c2 $c3) >> - | c = constr0 -> c ] ] + | c = constr0 -> c + ] ] ; constr2: (* ~ will be here *) [ [ c = constr1 -> c ] ] |