diff options
| author | Pierre-Marie Pédrot | 2016-04-11 13:45:57 +0200 |
|---|---|---|
| committer | Pierre-Marie Pédrot | 2016-04-12 20:49:12 +0200 |
| commit | e9aa3e6b70b1bab7138187733f6647b655a81b0b (patch) | |
| tree | 19d81b01d3ee39cf3b9e760e00fb636b5b5f5225 | |
| parent | d78784bd86d3d571bb2891356e9e9718c69976ba (diff) | |
Allowing the presence of TYPED AS in specialized ARGUMENT EXTEND.
This allows to use the ARGUMENT EXTEND macro while sharing the same
toplevel dynamic representation as another argument.
| -rw-r--r-- | grammar/argextend.ml4 | 21 |
1 files changed, 11 insertions, 10 deletions
diff --git a/grammar/argextend.ml4 b/grammar/argextend.ml4 index adfbd8cfde..c0be4598e1 100644 --- a/grammar/argextend.ml4 +++ b/grammar/argextend.ml4 @@ -73,11 +73,11 @@ let make_extend loc s cl wit = match cl with let () = Pcoq.grammar_extend $lid:s$ None (None, [(None, None, $rules$)]) in $lid:s$ >> -let declare_tactic_argument loc s (typ, pr, f, g, h) cl = - let rawtyp, rawpr, globtyp, globpr = match typ with - | `Uniform typ -> - typ, pr, typ, pr - | `Specialized (a, b, c, d) -> a, b, c, d +let declare_tactic_argument loc s (typ, f, g, h) cl = + let rawtyp, rawpr, globtyp, globpr, typ, pr = match typ with + | `Uniform (typ, pr) -> + typ, pr, typ, pr, Some typ, pr + | `Specialized (a, b, c, d, e, f) -> a, b, c, d, e, f in let glob = match g with | None -> @@ -121,10 +121,10 @@ let declare_tactic_argument loc s (typ, pr, f, g, h) cl = (Genarg.in_gen $make_globwit loc globtyp$ x)) >> | Some f -> <:expr< $lid:f$>> in let dyn = match typ with - | `Uniform typ -> + | None -> <:expr< None >> + | Some typ -> if is_self s typ then <:expr< None >> else <:expr< Some (Genarg.val_tag $make_topwit loc typ$) >> - | `Specialized _ -> <:expr< None >> in let se = mlexpr_of_string s in let wit = <:expr< $lid:"wit_"^s$ >> in @@ -186,8 +186,9 @@ EXTEND f = OPT [ "INTERPRETED"; "BY"; f = LIDENT -> f ]; g = OPT [ "GLOBALIZED"; "BY"; f = LIDENT -> f ]; h = OPT [ "SUBSTITUTED"; "BY"; f = LIDENT -> f ] -> - (`Uniform typ, pr, f, g, h) - | "PRINTED"; "BY"; pr = LIDENT; + (`Uniform (typ, pr), f, g, h) + | typ = OPT [ "TYPED"; "AS"; typ = argtype -> typ ]; + "PRINTED"; "BY"; pr = LIDENT; f = OPT [ "INTERPRETED"; "BY"; f = LIDENT -> f ]; g = OPT [ "GLOBALIZED"; "BY"; f = LIDENT -> f ]; h = OPT [ "SUBSTITUTED"; "BY"; f = LIDENT -> f ]; @@ -195,7 +196,7 @@ EXTEND "RAW_PRINTED"; "BY"; rawpr = LIDENT; "GLOB_TYPED"; "AS"; globtyp = argtype; "GLOB_PRINTED"; "BY"; globpr = LIDENT -> - (`Specialized (rawtyp, rawpr, globtyp, globpr), pr, f, g, h) ] ] + (`Specialized (rawtyp, rawpr, globtyp, globpr, typ, pr), f, g, h) ] ] ; argtype: [ "2" |