aboutsummaryrefslogtreecommitdiff
path: root/grammar/argextend.mlp
diff options
context:
space:
mode:
Diffstat (limited to 'grammar/argextend.mlp')
-rw-r--r--grammar/argextend.mlp221
1 files changed, 0 insertions, 221 deletions
diff --git a/grammar/argextend.mlp b/grammar/argextend.mlp
deleted file mode 100644
index 715b8cd23f..0000000000
--- a/grammar/argextend.mlp
+++ /dev/null
@@ -1,221 +0,0 @@
-(************************************************************************)
-(* * The Coq Proof Assistant / The Coq Development Team *)
-(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *)
-(* <O___,, * (see CREDITS file for the list of authors) *)
-(* \VV/ **************************************************************)
-(* // * This file is distributed under the terms of the *)
-(* * GNU Lesser General Public License Version 2.1 *)
-(* * (see LICENSE file for the text of the license) *)
-(************************************************************************)
-
-open Q_util
-
-let loc = Ploc.dummy
-
-IFDEF STRICT THEN
- let ploc_vala x = Ploc.VaVal x
-ELSE
- let ploc_vala x = x
-END
-
-let declare_str_items loc l =
- MLast.StDcl (loc, ploc_vala l) (* correspond to <:str_item< declare $list:l'$ end >> *)
-
-let declare_arg loc s e =
- declare_str_items loc [
- <:str_item< value ($lid:"wit_"^s$, $lid:s$) = $e$ >>;
- (** Prevent the unused variable warning *)
- <:str_item< value _ = ($lid:"wit_"^s$, $lid:s$) >>;
- ]
-
-let mk_extraarg loc s = <:expr< $lid:"wit_"^s$ >>
-
-let rec make_wit loc = function
- | ListArgType t -> <:expr< Genarg.wit_list $make_wit loc t$ >>
- | OptArgType t -> <:expr< Genarg.wit_opt $make_wit loc t$ >>
- | PairArgType (t1,t2) ->
- <:expr< Genarg.wit_pair $make_wit loc t1$ $make_wit loc t2$ >>
- | ExtraArgType s -> mk_extraarg loc s
-
-let is_self s = function
-| ExtraArgType s' -> s = s'
-| _ -> false
-
-let make_rawwit loc arg = <:expr< Genarg.rawwit $make_wit loc arg$ >>
-let make_globwit loc arg = <:expr< Genarg.glbwit $make_wit loc arg$ >>
-let make_topwit loc arg = <:expr< Genarg.topwit $make_wit loc arg$ >>
-
-let make_act loc act pil =
- let rec make = function
- | [] -> <:expr< (fun loc -> $act$) >>
- | ExtNonTerminal (_, None) :: tl -> <:expr< (fun $lid:"_"$ -> $make tl$) >>
- | ExtNonTerminal (_, Some p) :: tl -> <:expr< (fun $lid:p$ -> $make tl$) >>
- | ExtTerminal _ :: tl ->
- <:expr< (fun _ -> $make tl$) >> in
- make (List.rev pil)
-
-let make_prod_item self = function
- | ExtTerminal s -> <:expr< Extend.Atoken (CLexer.terminal $mlexpr_of_string s$) >>
- | ExtNonTerminal (Uentry e, _) when e = self -> <:expr< Extend.Aself >>
- | ExtNonTerminal (g, _) ->
- let base s = <:expr< $lid:s$ >> in
- mlexpr_of_prod_entry_key base g
-
-let rec make_prod self = function
-| [] -> <:expr< Extend.Stop >>
-| item :: prods -> <:expr< Extend.Next $make_prod self prods$ $make_prod_item self item$ >>
-
-let make_rule loc self (prods,act) =
- <:expr< Extend.Rule $make_prod self (List.rev prods)$ $make_act loc act prods$ >>
-
-let is_ident x = function
-| <:expr< $lid:s$ >> -> (s : string) = x
-| _ -> false
-
-let make_extend loc self cl = match cl with
-| [[ExtNonTerminal (Uentry e, Some id)], act] when is_ident id act ->
- (** Special handling of identity arguments by not redeclaring an entry *)
- <:expr< Vernacextend.Arg_alias $lid:e$ >>
-| _ ->
- <:expr< Vernacextend.Arg_rules $mlexpr_of_list (make_rule loc self) (List.rev cl)$ >>
-
-let warning_deprecated prefix s = function
-| None -> ()
-| Some _ ->
- Printf.eprintf "Deprecated [%sTYPED AS] clause in [ARGUMENT EXTEND %s]. \
- Use [TYPED AS] instead.\n%!" prefix s
-
-let get_type s = function
-| None -> None
-| Some typ ->
- if is_self s typ then
- let () = Printf.eprintf "Redundant [TYPED AS] clause in [ARGUMENT EXTEND %s].\n%!" s in
- None
- else Some typ
-
-let declare_tactic_argument loc s (typ, f, g, h) cl =
- let se = mlexpr_of_string s in
- let typ, pr = match typ with
- | `Uniform (typ, pr) ->
- let typ = get_type s typ in
- typ, <:expr< ($lid:pr$, $lid:pr$, $lid:pr$) >>
- | `Specialized (a, rpr, c, gpr, e, tpr) ->
- let () = warning_deprecated "RAW_" s a in
- let () = warning_deprecated "GLOB_" s c in
- let typ = get_type s e in
- typ, <:expr< ($lid:rpr$, $lid:gpr$, $lid:tpr$) >>
- in
- let glob = match g, typ with
- | Some f, (None | Some _) ->
- <:expr< Tacentries.ArgInternFun (fun ist v -> (ist, $lid:f$ ist v)) >>
- | None, Some typ ->
- <:expr< Tacentries.ArgInternWit $make_wit loc typ$ >>
- | None, None ->
- <:expr< Tacentries.ArgInternFun (fun ist v -> (ist, v)) >>
- in
- let interp = match f, typ with
- | Some f, (None | Some _) ->
- <:expr< Tacentries.ArgInterpLegacy $lid:f$ >>
- | None, Some typ ->
- <:expr< Tacentries.ArgInterpWit $make_wit loc typ$ >>
- | None, None ->
- <:expr< Tacentries.ArgInterpRet >>
- in
- let subst = match h, typ with
- | Some f, (None | Some _) ->
- <:expr< Tacentries.ArgSubstFun $lid:f$ >>
- | None, Some typ ->
- <:expr< Tacentries.ArgSubstWit $make_wit loc typ$ >>
- | None, None ->
- <:expr< Tacentries.ArgSubstFun (fun s v -> v) >>
- in
- let dyn = mlexpr_of_option (fun typ -> <:expr< Geninterp.val_tag $make_topwit loc typ$ >>) typ in
- declare_arg loc s <:expr< Tacentries.argument_extend ~{ name = $se$ } {
- Tacentries.arg_parsing = $make_extend loc s cl$;
- Tacentries.arg_tag = $dyn$;
- Tacentries.arg_intern = $glob$;
- Tacentries.arg_subst = $subst$;
- Tacentries.arg_interp = $interp$;
- Tacentries.arg_printer = $pr$
- } >>
-
-let declare_vernac_argument loc s pr cl =
- let se = mlexpr_of_string s in
- let pr_rules = match pr with
- | None -> <:expr< fun _ -> Pp.str $str:"[No printer for "^s^"]"$ >>
- | Some pr -> <:expr< $lid:pr$ >> in
- declare_arg loc s <:expr< Vernacextend.vernac_argument_extend ~{ name = $se$ } {
- Vernacextend.arg_printer = $pr_rules$;
- Vernacextend.arg_parsing = $make_extend loc s cl$
- } >>
-
-open Pcaml
-
-EXTEND
- GLOBAL: str_item;
- str_item:
- [ [ "ARGUMENT"; "EXTEND"; s = entry_name;
- header = argextend_header;
- OPT "|"; l = LIST1 argrule SEP "|";
- "END" ->
- declare_tactic_argument loc s header l
- | "VERNAC"; "ARGUMENT"; "EXTEND"; s = entry_name;
- pr = OPT ["PRINTED"; "BY"; pr = LIDENT -> pr];
- OPT "|"; l = LIST1 argrule SEP "|";
- "END" ->
- declare_vernac_argument loc s pr l ] ]
- ;
- argextend_specialized:
- [ [ rawtyp = OPT [ "RAW_TYPED"; "AS"; rawtyp = argtype -> rawtyp ];
- "RAW_PRINTED"; "BY"; rawpr = LIDENT;
- globtyp = OPT [ "GLOB_TYPED"; "AS"; globtyp = argtype -> globtyp ];
- "GLOB_PRINTED"; "BY"; globpr = LIDENT ->
- (rawtyp, rawpr, globtyp, globpr) ] ]
- ;
- argextend_header:
- [ [ 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 ];
- 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"
- [ e1 = argtype; "*"; e2 = argtype -> PairArgType (e1, e2) ]
- | "1"
- [ e = argtype; LIDENT "list" -> ListArgType e
- | e = argtype; LIDENT "option" -> OptArgType e ]
- | "0"
- [ e = LIDENT ->
- let e = parse_user_entry e "" in
- type_of_user_symbol e
- | "("; e = argtype; ")" -> e ] ]
- ;
- argrule:
- [ [ "["; l = LIST0 genarg; "]"; "->"; "["; e = Pcaml.expr; "]" -> (l,e) ] ]
- ;
- genarg:
- [ [ e = LIDENT; "("; s = LIDENT; ")" ->
- let e = parse_user_entry e "" in
- ExtNonTerminal (e, Some s)
- | e = LIDENT; "("; s = LIDENT; ","; sep = STRING; ")" ->
- let e = parse_user_entry e sep in
- ExtNonTerminal (e, Some s)
- | e = LIDENT ->
- let e = parse_user_entry e "" in
- ExtNonTerminal (e, None)
- | s = STRING -> ExtTerminal s
- ] ]
- ;
- entry_name:
- [ [ s = LIDENT -> s
- | UIDENT -> failwith "Argument entry names must be lowercase"
- ] ]
- ;
- END
generated by cgit v1.2.3 (git 2.25.1) at 2026-04-27 09:14:09 +0000