From e9aa3e6b70b1bab7138187733f6647b655a81b0b Mon Sep 17 00:00:00 2001 From: Pierre-Marie Pédrot Date: Mon, 11 Apr 2016 13:45:57 +0200 Subject: 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. --- grammar/argextend.ml4 | 21 +++++++++++---------- 1 file 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" -- cgit v1.2.3 From 116f8338b6fd60fdcf0f244772bcd6c82af5e333 Mon Sep 17 00:00:00 2001 From: Pierre-Marie Pédrot Date: Mon, 11 Apr 2016 13:57:32 +0200 Subject: Allowing simple ARGUMENT EXTEND not to mention their self type. The TYPED AS clause was useless when defining a fresh generic argument. Instead of having to write it mandatorily, we simply make it optional. --- grammar/argextend.ml4 | 31 +++++++++++++++++-------------- 1 file changed, 17 insertions(+), 14 deletions(-) diff --git a/grammar/argextend.ml4 b/grammar/argextend.ml4 index c0be4598e1..52119a963a 100644 --- a/grammar/argextend.ml4 +++ b/grammar/argextend.ml4 @@ -75,8 +75,9 @@ let make_extend loc s cl wit = match cl with 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 + | `Uniform (otyp, pr) -> + let typ = match otyp with Some typ -> typ | None -> ExtraArgType s in + typ, pr, typ, pr, otyp, pr | `Specialized (a, b, c, d, e, f) -> a, b, c, d, e, f in let glob = match g with @@ -180,23 +181,25 @@ EXTEND "END" -> declare_vernac_argument loc s pr l ] ] ; + argextend_specialized: + [ [ "RAW_TYPED"; "AS"; rawtyp = argtype; + "RAW_PRINTED"; "BY"; rawpr = LIDENT; + "GLOB_TYPED"; "AS"; globtyp = argtype; + "GLOB_PRINTED"; "BY"; globpr = LIDENT -> + (rawtyp, rawpr, globtyp, globpr) ] ] + ; argextend_header: - [ [ "TYPED"; "AS"; typ = argtype; - "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 ] -> - (`Uniform (typ, pr), f, g, h) - | typ = OPT [ "TYPED"; "AS"; typ = argtype -> typ ]; + [ [ 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 ]; - "RAW_TYPED"; "AS"; rawtyp = argtype; - "RAW_PRINTED"; "BY"; rawpr = LIDENT; - "GLOB_TYPED"; "AS"; globtyp = argtype; - "GLOB_PRINTED"; "BY"; globpr = LIDENT -> - (`Specialized (rawtyp, rawpr, globtyp, globpr, typ, pr), f, g, h) ] ] + special = OPT argextend_specialized -> + let repr = match special with + | None -> `Uniform (typ, pr) + | Some (rtyp, rpr, gtyp, gpr) -> `Specialized (rtyp, rpr, gtyp, gpr, typ, pr) + in + (repr, f, g, h) ] ] ; argtype: [ "2" -- cgit v1.2.3 From 5ecdba3505a1dd8e713503657c1a0acbef0796a7 Mon Sep 17 00:00:00 2001 From: Pierre-Marie Pédrot Date: Mon, 11 Apr 2016 14:10:07 +0200 Subject: Warning for redundant TYPED AS clauses. --- grammar/argextend.ml4 | 7 ++++++- 1 file changed, 6 insertions(+), 1 deletion(-) diff --git a/grammar/argextend.ml4 b/grammar/argextend.ml4 index 52119a963a..33cd62e3a9 100644 --- a/grammar/argextend.ml4 +++ b/grammar/argextend.ml4 @@ -76,7 +76,12 @@ let make_extend loc s cl wit = match cl with let declare_tactic_argument loc s (typ, f, g, h) cl = let rawtyp, rawpr, globtyp, globpr, typ, pr = match typ with | `Uniform (otyp, pr) -> - let typ = match otyp with Some typ -> typ | None -> ExtraArgType s in + let typ = match otyp with + | None -> ExtraArgType s + | Some typ -> + let () = if is_self s typ then Printf.eprintf "Redundant [TYPED AS %s] clause.\n%!" s in + typ + in typ, pr, typ, pr, otyp, pr | `Specialized (a, b, c, d, e, f) -> a, b, c, d, e, f in -- cgit v1.2.3 From 9719ac37ed51ccadaf81712793057d5c0c3235cf Mon Sep 17 00:00:00 2001 From: Pierre-Marie Pédrot Date: Mon, 11 Apr 2016 15:45:52 +0200 Subject: Allowing optional RAW_TYPED and GLOB_TYPED clauses in ARGUMENT EXTEND. --- grammar/argextend.ml4 | 53 ++++++++++++++++++++++++++++++--------------------- 1 file changed, 31 insertions(+), 22 deletions(-) diff --git a/grammar/argextend.ml4 b/grammar/argextend.ml4 index 33cd62e3a9..4fd9cd9da0 100644 --- a/grammar/argextend.ml4 +++ b/grammar/argextend.ml4 @@ -73,40 +73,48 @@ 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 warning_redundant prefix s = + Printf.eprintf "Redundant [%sTYPED AS %s] clause.\n%!" prefix s + +let get_type prefix s = function +| None -> None +| Some typ -> + if is_self s typ then + let () = warning_redundant prefix s in None + else Some typ + let declare_tactic_argument loc s (typ, f, g, h) cl = let rawtyp, rawpr, globtyp, globpr, typ, pr = match typ with - | `Uniform (otyp, pr) -> - let typ = match otyp with - | None -> ExtraArgType s - | Some typ -> - let () = if is_self s typ then Printf.eprintf "Redundant [TYPED AS %s] clause.\n%!" s in - typ - in - typ, pr, typ, pr, otyp, pr - | `Specialized (a, b, c, d, e, f) -> a, b, c, d, e, f + | `Uniform (typ, pr) -> + let typ = get_type "" s typ in + typ, pr, typ, pr, typ, pr + | `Specialized (a, b, c, d, e, f) -> + get_type "RAW_" s a, b, get_type "GLOB_" s c, d, e, f in let glob = match g with | None -> - if is_self s rawtyp then - <:expr< fun ist v -> (ist, v) >> - else + begin match rawtyp with + | None -> <:expr< fun ist v -> (ist, v) >> + | Some rawtyp -> <:expr< fun ist v -> let ans = out_gen $make_globwit loc rawtyp$ (Tacintern.intern_genarg ist (Genarg.in_gen $make_rawwit loc rawtyp$ v)) in (ist, ans) >> + end | Some f -> <:expr< fun ist v -> (ist, $lid:f$ ist v) >> in let interp = match f with | None -> - if is_self s globtyp then - <:expr< fun ist v -> Ftactic.return v >> - else - <:expr< fun ist x -> + begin match globtyp with + | None -> <:expr< fun ist v -> Ftactic.return v >> + | Some globtyp -> + <:expr< fun ist x -> Ftactic.bind - (Tacinterp.interp_genarg ist (Genarg.in_gen $make_globwit loc globtyp$ x)) + (Tacinterp.interp_genarg ist (Genarg.in_gen $make_globwit loc globtyp$ x)) (fun v -> Ftactic.return (Tacinterp.Value.cast $make_topwit loc globtyp$ v)) >> + end | Some f -> (** Compatibility layer, TODO: remove me *) <:expr< @@ -118,13 +126,14 @@ let declare_tactic_argument loc s (typ, f, g, h) cl = >> in let subst = match h with | None -> - if is_self s globtyp then - <:expr< fun s v -> v >> - else + begin match globtyp with + | None -> <:expr< fun s v -> v >> + | Some globtyp -> <:expr< fun s x -> out_gen $make_globwit loc globtyp$ (Tacsubst.subst_genarg s (Genarg.in_gen $make_globwit loc globtyp$ x)) >> + end | Some f -> <:expr< $lid:f$>> in let dyn = match typ with | None -> <:expr< None >> @@ -187,9 +196,9 @@ EXTEND declare_vernac_argument loc s pr l ] ] ; argextend_specialized: - [ [ "RAW_TYPED"; "AS"; rawtyp = argtype; + [ [ rawtyp = OPT [ "RAW_TYPED"; "AS"; rawtyp = argtype -> rawtyp ]; "RAW_PRINTED"; "BY"; rawpr = LIDENT; - "GLOB_TYPED"; "AS"; globtyp = argtype; + globtyp = OPT [ "GLOB_TYPED"; "AS"; globtyp = argtype -> globtyp ]; "GLOB_PRINTED"; "BY"; globpr = LIDENT -> (rawtyp, rawpr, globtyp, globpr) ] ] ; -- cgit v1.2.3 From 137888c3aaab15bc26f7b4ffac7e53469fb1bb3e Mon Sep 17 00:00:00 2001 From: Pierre-Marie Pédrot Date: Mon, 11 Apr 2016 16:22:19 +0200 Subject: Adding warnings for inferrable *_TYPED AS clauses. --- grammar/argextend.ml4 | 16 +++++++++++++--- 1 file changed, 13 insertions(+), 3 deletions(-) diff --git a/grammar/argextend.ml4 b/grammar/argextend.ml4 index 4fd9cd9da0..dca3e1656f 100644 --- a/grammar/argextend.ml4 +++ b/grammar/argextend.ml4 @@ -74,7 +74,7 @@ let make_extend loc s cl wit = match cl with $lid:s$ >> let warning_redundant prefix s = - Printf.eprintf "Redundant [%sTYPED AS %s] clause.\n%!" prefix s + Printf.eprintf "Redundant [%sTYPED AS] clause in [ARGUMENT EXTEND %s].\n%!" prefix s let get_type prefix s = function | None -> None @@ -83,13 +83,23 @@ let get_type prefix s = function let () = warning_redundant prefix s in None else Some typ +let check_type prefix s = function +| None -> () +| Some _ -> warning_redundant prefix s + let declare_tactic_argument loc s (typ, f, g, h) cl = let rawtyp, rawpr, globtyp, globpr, typ, pr = match typ with | `Uniform (typ, pr) -> let typ = get_type "" s typ in typ, pr, typ, pr, typ, pr - | `Specialized (a, b, c, d, e, f) -> - get_type "RAW_" s a, b, get_type "GLOB_" s c, d, e, f + | `Specialized (a, rpr, c, gpr, e, tpr) -> + (** Check that we actually need the TYPED AS arguments *) + let rawtyp = get_type "RAW_" s a in + let glbtyp = get_type "GLOB_" s c in + let toptyp = get_type "" s e in + let () = match g with None -> () | Some _ -> check_type "RAW_" s rawtyp in + let () = match f, h with Some _, Some _ -> check_type "GLOB_" s glbtyp | _ -> () in + rawtyp, rpr, glbtyp, gpr, toptyp, tpr in let glob = match g with | None -> -- cgit v1.2.3 From fa9c33e37ca609981aca88d6f92b07882bd2f4f4 Mon Sep 17 00:00:00 2001 From: Pierre-Marie Pédrot Date: Mon, 11 Apr 2016 16:05:15 +0200 Subject: Removing redundant *_TYPED AS clauses in EXTEND statements. --- ltac/extraargs.ml4 | 17 ----------------- ltac/extratactics.ml4 | 2 -- ltac/g_auto.ml4 | 2 -- ltac/g_rewrite.ml4 | 6 ------ plugins/extraction/g_extraction.ml4 | 1 - 5 files changed, 28 deletions(-) diff --git a/ltac/extraargs.ml4 b/ltac/extraargs.ml4 index 4d3507cbc4..f2dc024c71 100644 --- a/ltac/extraargs.ml4 +++ b/ltac/extraargs.ml4 @@ -110,10 +110,7 @@ ARGUMENT EXTEND occurrences GLOBALIZED BY glob_occs SUBSTITUTED BY subst_occs - RAW_TYPED AS occurrences_or_var RAW_PRINTED BY pr_occurrences - - GLOB_TYPED AS occurrences_or_var GLOB_PRINTED BY pr_occurrences | [ ne_integer_list(l) ] -> [ ArgArg l ] @@ -141,10 +138,7 @@ ARGUMENT EXTEND glob GLOBALIZED BY glob_glob SUBSTITUTED BY subst_glob - RAW_TYPED AS constr_expr RAW_PRINTED BY pr_gen - - GLOB_TYPED AS glob_constr_and_expr GLOB_PRINTED BY pr_gen [ constr(c) ] -> [ c ] END @@ -164,10 +158,7 @@ ARGUMENT EXTEND lglob GLOBALIZED BY glob_glob SUBSTITUTED BY subst_glob - RAW_TYPED AS constr_expr RAW_PRINTED BY pr_gen - - GLOB_TYPED AS glob_constr_and_expr GLOB_PRINTED BY pr_gen [ lconstr(c) ] -> [ c ] END @@ -207,9 +198,7 @@ ARGUMENT EXTEND hloc INTERPRETED BY interp_place GLOBALIZED BY intern_place SUBSTITUTED BY subst_place - RAW_TYPED AS loc_place RAW_PRINTED BY pr_loc_place - GLOB_TYPED AS loc_place GLOB_PRINTED BY pr_loc_place [ ] -> [ ConclLocation () ] @@ -224,12 +213,6 @@ ARGUMENT EXTEND hloc END - - - - - - (* Julien: Mise en commun des differentes version de replace with in by *) let pr_by_arg_tac _prc _prlc prtac opt_c = diff --git a/ltac/extratactics.ml4 b/ltac/extratactics.ml4 index ba9f82fb96..0b475340e2 100644 --- a/ltac/extratactics.ml4 +++ b/ltac/extratactics.ml4 @@ -980,9 +980,7 @@ let interp_test ist gls = function ARGUMENT EXTEND test PRINTED BY pr_itest' INTERPRETED BY interp_test - RAW_TYPED AS test RAW_PRINTED BY pr_test' - GLOB_TYPED AS test GLOB_PRINTED BY pr_test' | [ int_or_var(x) comparison(c) int_or_var(y) ] -> [ Test(c,x,y) ] END diff --git a/ltac/g_auto.ml4 b/ltac/g_auto.ml4 index bc98b7d6d4..d4fd8a1df3 100644 --- a/ltac/g_auto.ml4 +++ b/ltac/g_auto.ml4 @@ -174,7 +174,6 @@ END let pr_hints_path_atom _ _ _ = Hints.pp_hints_path_atom ARGUMENT EXTEND hints_path_atom - TYPED AS hints_path_atom PRINTED BY pr_hints_path_atom | [ global_list(g) ] -> [ Hints.PathHints (List.map Nametab.global g) ] | [ "*" ] -> [ Hints.PathAny ] @@ -183,7 +182,6 @@ END let pr_hints_path prc prx pry c = Hints.pp_hints_path c ARGUMENT EXTEND hints_path - TYPED AS hints_path PRINTED BY pr_hints_path | [ "(" hints_path(p) ")" ] -> [ p ] | [ "!" hints_path(p) ] -> [ Hints.PathStar p ] diff --git a/ltac/g_rewrite.ml4 b/ltac/g_rewrite.ml4 index c4ef1f297e..395c2cd1b6 100644 --- a/ltac/g_rewrite.ml4 +++ b/ltac/g_rewrite.ml4 @@ -47,10 +47,7 @@ ARGUMENT EXTEND glob_constr_with_bindings GLOBALIZED BY glob_glob_constr_with_bindings SUBSTITUTED BY subst_glob_constr_with_bindings - RAW_TYPED AS constr_expr_with_bindings RAW_PRINTED BY pr_constr_expr_with_bindings - - GLOB_TYPED AS glob_constr_with_bindings GLOB_PRINTED BY pr_glob_constr_with_bindings [ constr_with_bindings(bl) ] -> [ bl ] @@ -76,10 +73,7 @@ ARGUMENT EXTEND rewstrategy GLOBALIZED BY glob_strategy SUBSTITUTED BY subst_strategy - RAW_TYPED AS raw_strategy RAW_PRINTED BY pr_raw_strategy - - GLOB_TYPED AS glob_strategy GLOB_PRINTED BY pr_glob_strategy [ glob(c) ] -> [ StratConstr (c, true) ] diff --git a/plugins/extraction/g_extraction.ml4 b/plugins/extraction/g_extraction.ml4 index 7bd07f6255..ca4e13e125 100644 --- a/plugins/extraction/g_extraction.ml4 +++ b/plugins/extraction/g_extraction.ml4 @@ -35,7 +35,6 @@ let pr_int_or_id _ _ _ = function | ArgId id -> pr_id id ARGUMENT EXTEND int_or_id - TYPED AS int_or_id PRINTED BY pr_int_or_id | [ preident(id) ] -> [ ArgId (Id.of_string id) ] | [ integer(i) ] -> [ ArgInt i ] -- cgit v1.2.3 From d632f64403da813e240973a9caf06c79e262a7ec Mon Sep 17 00:00:00 2001 From: Pierre-Marie Pédrot Date: Mon, 11 Apr 2016 16:41:49 +0200 Subject: Adding toplevel representation sharing for some generic arguments. --- ltac/extraargs.ml4 | 2 ++ 1 file changed, 2 insertions(+) diff --git a/ltac/extraargs.ml4 b/ltac/extraargs.ml4 index f2dc024c71..fbae17bafc 100644 --- a/ltac/extraargs.ml4 +++ b/ltac/extraargs.ml4 @@ -104,6 +104,7 @@ let glob_occs ist l = l let subst_occs evm l = l ARGUMENT EXTEND occurrences + TYPED AS int list PRINTED BY pr_int_list_full INTERPRETED BY interp_occs @@ -152,6 +153,7 @@ ARGUMENT EXTEND lconstr END ARGUMENT EXTEND lglob + TYPED AS glob PRINTED BY pr_globc INTERPRETED BY interp_glob -- cgit v1.2.3