aboutsummaryrefslogtreecommitdiff
diff options
context:
space:
mode:
Diffstat
-rw-r--r--grammar/q_util.mli2
-rw-r--r--grammar/q_util.mlp14
-rw-r--r--grammar/tacextend.mlp14
-rw-r--r--grammar/vernacextend.mlp123
-rw-r--r--plugins/ltac/tacentries.ml11
-rw-r--r--vernac/egramml.ml9
-rw-r--r--vernac/egramml.mli2
-rw-r--r--vernac/vernacentries.ml79
-rw-r--r--vernac/vernacentries.mli15
9 files changed, 140 insertions, 129 deletions
diff --git a/grammar/q_util.mli b/grammar/q_util.mli
index 323a12357d..f3af318b60 100644
--- a/grammar/q_util.mli
+++ b/grammar/q_util.mli
@@ -48,3 +48,5 @@ val mlexpr_of_prod_entry_key : (string -> MLast.expr) -> user_symbol -> MLast.ex
val type_of_user_symbol : user_symbol -> argument_type
val parse_user_entry : string -> string -> user_symbol
+
+val mlexpr_of_symbol : user_symbol -> MLast.expr
diff --git a/grammar/q_util.mlp b/grammar/q_util.mlp
index 0b8d7fda7a..0e2bf55d86 100644
--- a/grammar/q_util.mlp
+++ b/grammar/q_util.mlp
@@ -128,3 +128,17 @@ let rec parse_user_entry s sep =
let s = match s with "hyp" -> "var" | _ -> s in
check_separator sep;
Uentry s
+
+let rec mlexpr_of_symbol = function
+| Ulist1 s -> <:expr< Extend.TUlist1 $mlexpr_of_symbol s$ >>
+| Ulist1sep (s,sep) -> <:expr< Extend.TUlist1sep $mlexpr_of_symbol s$ $str:sep$ >>
+| Ulist0 s -> <:expr< Extend.TUlist0 $mlexpr_of_symbol s$ >>
+| Ulist0sep (s,sep) -> <:expr< Extend.TUlist0sep $mlexpr_of_symbol s$ $str:sep$ >>
+| Uopt s -> <:expr< Extend.TUopt $mlexpr_of_symbol s$ >>
+| Uentry e ->
+ let wit = <:expr< $lid:"wit_"^e$ >> in
+ <:expr< Extend.TUentry (Genarg.get_arg_tag $wit$) >>
+| Uentryl (e, l) ->
+ assert (e = "tactic");
+ let wit = <:expr< $lid:"wit_"^e$ >> in
+ <:expr< Extend.TUentryl (Genarg.get_arg_tag $wit$) $mlexpr_of_int l$>>
diff --git a/grammar/tacextend.mlp b/grammar/tacextend.mlp
index cea0bed599..07a9a76139 100644
--- a/grammar/tacextend.mlp
+++ b/grammar/tacextend.mlp
@@ -15,20 +15,6 @@ open Argextend
let plugin_name = <:expr< __coq_plugin_name >>
-let rec mlexpr_of_symbol = function
-| Ulist1 s -> <:expr< Extend.TUlist1 $mlexpr_of_symbol s$ >>
-| Ulist1sep (s,sep) -> <:expr< Extend.TUlist1sep $mlexpr_of_symbol s$ $str:sep$ >>
-| Ulist0 s -> <:expr< Extend.TUlist0 $mlexpr_of_symbol s$ >>
-| Ulist0sep (s,sep) -> <:expr< Extend.TUlist0sep $mlexpr_of_symbol s$ $str:sep$ >>
-| Uopt s -> <:expr< Extend.TUopt $mlexpr_of_symbol s$ >>
-| Uentry e ->
- let wit = <:expr< $lid:"wit_"^e$ >> in
- <:expr< Extend.TUentry (Genarg.get_arg_tag $wit$) >>
-| Uentryl (e, l) ->
- assert (e = "tactic");
- let wit = <:expr< $lid:"wit_"^e$ >> in
- <:expr< Extend.TUentryl (Genarg.get_arg_tag $wit$) $mlexpr_of_int l$>>
-
let rec mlexpr_of_clause = function
| [] -> <:expr< TyNil >>
| ExtTerminal s :: cl -> <:expr< TyIdent($str:s$, $mlexpr_of_clause cl$) >>
diff --git a/grammar/vernacextend.mlp b/grammar/vernacextend.mlp
index f344f3c573..f30c96a7f5 100644
--- a/grammar/vernacextend.mlp
+++ b/grammar/vernacextend.mlp
@@ -14,98 +14,42 @@ open Q_util
open Argextend
type rule = {
- r_head : string option;
- (** The first terminal grammar token *)
r_patt : extend_token list;
(** The remaining tokens of the parsing rule *)
r_class : MLast.expr option;
(** An optional classifier for the STM *)
r_branch : MLast.expr;
(** The action performed by this rule. *)
- r_depr : unit option;
+ r_depr : bool;
(** Whether this entry is deprecated *)
}
-(** Quotation difference for match clauses *)
+let rec make_patt r = function
+| [] -> r
+| ExtNonTerminal (_, Some p) :: l -> <:expr< fun $lid:p$ -> $make_patt r l$ >>
+| ExtNonTerminal (_, None) :: l -> <:expr< fun _ -> $make_patt r l$ >>
+| ExtTerminal _ :: l -> make_patt r l
-let default_patt loc =
- (<:patt< _ >>, ploc_vala None, <:expr< failwith "Extension: cannot occur" >>)
-
-let make_fun loc cl =
- let l = cl @ [default_patt loc] in
- MLast.ExFun (loc, ploc_vala l) (* correspond to <:expr< fun [ $list:l$ ] >> *)
-
-let rec make_patt = function
- | [] -> <:patt< [] >>
- | ExtNonTerminal (_, Some p) :: l ->
- <:patt< [ $lid:p$ :: $make_patt l$ ] >>
- | _::l -> make_patt l
-
-let rec make_let e = function
- | [] -> e
- | ExtNonTerminal (g, Some p) :: l ->
- let t = type_of_user_symbol g in
- let loc = MLast.loc_of_expr e in
- let e = make_let e l in
- <:expr< let $lid:p$ = Genarg.out_gen $make_rawwit loc t$ $lid:p$ in $e$ >>
- | _::l -> make_let e l
-
-let make_clause { r_patt = pt; r_branch = e; } =
- (make_patt pt,
- ploc_vala None,
- make_let e pt)
-
-(* To avoid warnings *)
-let mk_ignore c pt =
- let fold accu = function
- | ExtNonTerminal (_, Some p) -> p :: accu
- | _ -> accu
- in
- let names = List.fold_left fold [] pt in
- let fold accu id = <:expr< let _ = $lid:id$ in $accu$ >> in
- let names = List.fold_left fold <:expr< () >> names in
- <:expr< do { let _ = $names$ in $c$ } >>
-
-let make_clause_classifier { r_patt = pt; r_class = c; } =
- let map c =
- make_fun loc [(make_patt pt,
- ploc_vala None,
- make_let (mk_ignore c pt) pt)]
- in
- mlexpr_of_option map c
-
-let make_prod_item = function
- | ExtTerminal s -> <:expr< Egramml.GramTerminal $str:s$ >>
- | ExtNonTerminal (g, ido) ->
- let nt = type_of_user_symbol g in
- let base s = <:expr< Pcoq.genarg_grammar ($mk_extraarg loc s$) >> in
- let typ = match ido with None -> None | Some _ -> Some nt in
- <:expr< Egramml.GramNonTerminal ( Loc.tag ( $mlexpr_of_option (make_rawwit loc) typ$ ,
- $mlexpr_of_prod_entry_key base g$ ) ) >>
-
-let mlexpr_of_clause { r_head = a; r_patt = b; } = match a with
-| None -> mlexpr_of_list make_prod_item b
-| Some a -> mlexpr_of_list make_prod_item (ExtTerminal a :: b)
+let rec mlexpr_of_clause = function
+| [] -> <:expr< Vernacentries.TyNil >>
+| ExtTerminal s :: cl -> <:expr< Vernacentries.TyTerminal ($str:s$, $mlexpr_of_clause cl$) >>
+| ExtNonTerminal (g, id) :: cl ->
+ let id = mlexpr_of_option mlexpr_of_string id in
+ <:expr< Vernacentries.TyNonTerminal ($id$, $mlexpr_of_symbol g$, $mlexpr_of_clause cl$) >>
let make_rule r =
- let depr = match r.r_depr with
- | None -> false
- | Some () -> true
- in
- let gram = mlexpr_of_clause r in
- let cmd = make_fun loc [make_clause r] in
- let classif = make_clause_classifier r in
- <:expr< ($mlexpr_of_bool depr$, $cmd$, $classif$, $gram$) >>
+ let ty = mlexpr_of_clause r.r_patt in
+ let cmd = make_patt r.r_branch r.r_patt in
+ let make_classifier c = make_patt c r.r_patt in
+ let classif = mlexpr_of_option make_classifier r.r_class in
+ <:expr< Vernacentries.TyML ($mlexpr_of_bool r.r_depr$, $ty$, $cmd$, $classif$) >>
let declare_command loc s c nt cl =
let se = mlexpr_of_string s in
let c = mlexpr_of_option (fun x -> x) c in
let rules = mlexpr_of_list make_rule cl in
declare_str_items loc
- [ <:str_item< do {
- Vernacentries.vernac_extend ?{ classifier = $c$ }
- ~{ command = $se$ } ?{ entry = $nt$ } $rules$;
- } >> ]
+ [ <:str_item< Vernacentries.vernac_extend ?{ classifier = $c$ } ~{ command = $se$ } ?{ entry = $nt$ } $rules$ >> ]
open Pcaml
@@ -140,34 +84,21 @@ EXTEND
] ]
;
deprecation:
- [ [ "DEPRECATED" -> () ] ]
+ [ [ -> false | "DEPRECATED" -> true ] ]
;
- (* spiwack: comment-by-guessing: it seems that the isolated string
- (which otherwise could have been another argument) is not passed
- to the VernacExtend interpreter function to discriminate between
- the clauses. *)
rule:
- [ [ "["; s = STRING; l = LIST0 args; "]";
- d = OPT deprecation; c = OPT classifier; "->"; "["; e = Pcaml.expr; "]" ->
- let () = if s = "" then failwith "Command name is empty." in
- let b = <:expr< fun ~{atts} ~{st} -> ( let () = $e$ in st ) >> in
- { r_head = Some s; r_patt = l; r_class = c; r_branch = b; r_depr = d; }
- | "[" ; "-" ; l = LIST1 args ; "]" ;
- d = OPT deprecation; c = OPT classifier; "->"; "["; e = Pcaml.expr; "]" ->
+ [ [ "["; OPT "-"; l = LIST1 args; "]";
+ d = deprecation; c = OPT classifier; "->"; "["; e = Pcaml.expr; "]" ->
let b = <:expr< fun ~{atts} ~{st} -> ( let () = $e$ in st ) >> in
- { r_head = None; r_patt = l; r_class = c; r_branch = b; r_depr = d; }
+ { r_patt = l; r_class = c; r_branch = b; r_depr = d; }
] ]
;
+ (** The [OPT "-"] argument serves no purpose nowadays, it is left here for
+ backward compatibility. *)
fun_rule:
- [ [ "["; s = STRING; l = LIST0 args; "]";
- d = OPT deprecation; c = OPT classifier; "->"; "["; e = Pcaml.expr; "]" ->
- let () = if s = "" then failwith "Command name is empty." in
- let b = <:expr< $e$ >> in
- { r_head = Some s; r_patt = l; r_class = c; r_branch = b; r_depr = d; }
- | "[" ; "-" ; l = LIST1 args ; "]" ;
- d = OPT deprecation; c = OPT classifier; "->"; "["; e = Pcaml.expr; "]" ->
- let b = <:expr< $e$ >> in
- { r_head = None; r_patt = l; r_class = c; r_branch = b; r_depr = d; }
+ [ [ "["; OPT "-"; l = LIST1 args; "]";
+ d = deprecation; c = OPT classifier; "->"; "["; e = Pcaml.expr; "]" ->
+ { r_patt = l; r_class = c; r_branch = e; r_depr = d; }
] ]
;
classifier:
diff --git a/plugins/ltac/tacentries.ml b/plugins/ltac/tacentries.ml
index fac464a628..463d8633cf 100644
--- a/plugins/ltac/tacentries.ml
+++ b/plugins/ltac/tacentries.ml
@@ -592,15 +592,6 @@ let rec clause_of_sign : type a. a ty_sig -> Genarg.ArgT.any Extend.user_symbol
let clause_of_ty_ml = function
| TyML (t,_) -> clause_of_sign t
-let rec prj : type a b c. (a,b,c) Extend.ty_user_symbol -> (a,b,c) genarg_type = function
- | TUentry a -> ExtraArg a
- | TUentryl (a,l) -> ExtraArg a
- | TUopt(o) -> OptArg (prj o)
- | TUlist1 l -> ListArg (prj l)
- | TUlist1sep (l,_) -> ListArg (prj l)
- | TUlist0 l -> ListArg (prj l)
- | TUlist0sep (l,_) -> ListArg (prj l)
-
let rec eval_sign : type a. a ty_sig -> a -> Geninterp.Val.t list -> Geninterp.interp_sign -> unit Proofview.tactic =
fun sign tac ->
match sign with
@@ -615,7 +606,7 @@ let rec eval_sign : type a. a ty_sig -> a -> Geninterp.Val.t list -> Geninterp.i
begin fun tac vals ist -> match vals with
| [] -> assert false
| v :: vals ->
- let v' = Taccoerce.Value.cast (topwit (prj a)) v in
+ let v' = Taccoerce.Value.cast (topwit (Egramml.proj_symbol a)) v in
f (tac v') vals ist
end tac
| TyAnonArg (a, sig') -> eval_sign sig' tac
diff --git a/vernac/egramml.ml b/vernac/egramml.ml
index 048d4d93a0..c5dedc880e 100644
--- a/vernac/egramml.ml
+++ b/vernac/egramml.ml
@@ -64,6 +64,15 @@ let make_rule f prod =
let act = ty_eval ty_rule f in
Extend.Rule (symb, act)
+let rec proj_symbol : type a b c. (a, b, c) ty_user_symbol -> (a, b, c) genarg_type = function
+| TUentry a -> ExtraArg a
+| TUentryl (a,l) -> ExtraArg a
+| TUopt(o) -> OptArg (proj_symbol o)
+| TUlist1 l -> ListArg (proj_symbol l)
+| TUlist1sep (l,_) -> ListArg (proj_symbol l)
+| TUlist0 l -> ListArg (proj_symbol l)
+| TUlist0sep (l,_) -> ListArg (proj_symbol l)
+
(** Vernac grammar extensions *)
let vernac_exts = ref []
diff --git a/vernac/egramml.mli b/vernac/egramml.mli
index a5ee036db5..c4f4fcfaa4 100644
--- a/vernac/egramml.mli
+++ b/vernac/egramml.mli
@@ -26,6 +26,8 @@ val extend_vernac_command_grammar :
val get_extend_vernac_rule : Vernacexpr.extend_name -> vernac_expr grammar_prod_item list
+val proj_symbol : ('a, 'b, 'c) Extend.ty_user_symbol -> ('a, 'b, 'c) Genarg.genarg_type
+
(** Utility function reused in Egramcoq : *)
val make_rule :
diff --git a/vernac/vernacentries.ml b/vernac/vernacentries.ml
index 08dd6bec18..653f8b26e0 100644
--- a/vernac/vernacentries.ml
+++ b/vernac/vernacentries.ml
@@ -2437,8 +2437,75 @@ let interp ?verbosely ?proof ~st cmd =
Vernacstate.invalidate_cache ();
iraise exn
+(** VERNAC EXTEND registering *)
+
+open Genarg
+open Extend
+
type classifier = Genarg.raw_generic_argument list -> vernac_classification
+type (_, _) ty_sig =
+| TyNil : (atts:atts -> st:Vernacstate.t -> Vernacstate.t, Vernacexpr.vernac_classification) ty_sig
+| TyTerminal : string * ('r, 's) ty_sig -> ('r, 's) ty_sig
+| TyNonTerminal :
+ string option * ('a, 'b, 'c) Extend.ty_user_symbol * ('r, 's) ty_sig -> ('a -> 'r, 'a -> 's) ty_sig
+
+type ty_ml = TyML : bool * ('r, 's) ty_sig * 'r * 's option -> ty_ml
+
+let type_error () = CErrors.anomaly (Pp.str "Ill-typed VERNAC EXTEND")
+
+let rec untype_classifier : type r s. (r, s) ty_sig -> s -> classifier = function
+| TyNil -> fun f args ->
+ begin match args with
+ | [] -> f
+ | _ :: _ -> type_error ()
+ end
+| TyTerminal (_, ty) -> fun f args -> untype_classifier ty f args
+| TyNonTerminal (_, tu, ty) -> fun f args ->
+ begin match args with
+ | [] -> type_error ()
+ | Genarg.GenArg (Rawwit tag, v) :: args ->
+ match Genarg.genarg_type_eq tag (Egramml.proj_symbol tu) with
+ | None -> type_error ()
+ | Some Refl -> untype_classifier ty (f v) args
+ end
+
+(** Stupid GADTs forces us to duplicate the definition just for typing *)
+let rec untype_command : type r s. (r, s) ty_sig -> r -> plugin_args vernac_command = function
+| TyNil -> fun f args ->
+ begin match args with
+ | [] -> f
+ | _ :: _ -> type_error ()
+ end
+| TyTerminal (_, ty) -> fun f args -> untype_command ty f args
+| TyNonTerminal (_, tu, ty) -> fun f args ->
+ begin match args with
+ | [] -> type_error ()
+ | Genarg.GenArg (Rawwit tag, v) :: args ->
+ match Genarg.genarg_type_eq tag (Egramml.proj_symbol tu) with
+ | None -> type_error ()
+ | Some Refl -> untype_command ty (f v) args
+ end
+
+let rec untype_user_symbol : type s a b c. (a, b, c) Extend.ty_user_symbol -> (s, a) Extend.symbol = function
+| TUlist1 l -> Alist1 (untype_user_symbol l)
+| TUlist1sep (l, s) -> Alist1sep (untype_user_symbol l, Atoken (CLexer.terminal s))
+| TUlist0 l -> Alist0 (untype_user_symbol l)
+| TUlist0sep (l, s) -> Alist0sep (untype_user_symbol l, Atoken (CLexer.terminal s))
+| TUopt o -> Aopt (untype_user_symbol o)
+| TUentry a -> Aentry (Pcoq.genarg_grammar (ExtraArg a))
+| TUentryl (a, i) -> Aentryl (Pcoq.genarg_grammar (ExtraArg a), string_of_int i)
+
+let rec untype_grammar : type r s. (r, s) ty_sig -> vernac_expr Egramml.grammar_prod_item list = function
+| TyNil -> []
+| TyTerminal (tok, ty) -> Egramml.GramTerminal tok :: untype_grammar ty
+| TyNonTerminal (id, tu, ty) ->
+ let t = Option.map (fun _ -> rawwit (Egramml.proj_symbol tu)) id in
+ let symb = untype_user_symbol tu in
+ Egramml.GramNonTerminal (Loc.tag (t, symb)) :: untype_grammar ty
+
+let _ = untype_classifier, untype_command, untype_grammar, untype_user_symbol
+
let classifiers : classifier array String.Map.t ref = ref String.Map.empty
let get_vernac_classifier (name, i) args =
@@ -2448,8 +2515,8 @@ let declare_vernac_classifier name f =
classifiers := String.Map.add name f !classifiers
let vernac_extend ~command ?classifier ?entry ext =
- let get_classifier = function
- | Some cl -> cl
+ let get_classifier (TyML (_, ty, _, cl)) = match cl with
+ | Some cl -> untype_classifier ty cl
| None ->
match classifier with
| Some cl -> fun _ -> cl command
@@ -2478,9 +2545,11 @@ let vernac_extend ~command ?classifier ?entry ext =
in
CErrors.user_err (Pp.strbrk msg)
in
- let cl = Array.map_of_list (fun (_, _, cl, _) -> get_classifier cl) ext in
- let iter i (depr, f, cl, r) =
- let () = Vernacinterp.vinterp_add depr (command, i) f in
+ let cl = Array.map_of_list get_classifier ext in
+ let iter i (TyML (depr, ty, f, _)) =
+ let f = untype_command ty f in
+ let r = untype_grammar ty in
+ let () = vinterp_add depr (command, i) f in
Egramml.extend_vernac_command_grammar (command, i) entry r
in
let () = declare_vernac_classifier command cl in
diff --git a/vernac/vernacentries.mli b/vernac/vernacentries.mli
index 102f996cf2..fb2a30bac7 100644
--- a/vernac/vernacentries.mli
+++ b/vernac/vernacentries.mli
@@ -47,15 +47,22 @@ val attributes_of_flags : Vernacexpr.vernac_flags -> Vernacinterp.atts -> bool o
type classifier = Genarg.raw_generic_argument list -> Vernacexpr.vernac_classification
+type (_, _) ty_sig =
+| TyNil : (atts:Vernacinterp.atts -> st:Vernacstate.t -> Vernacstate.t, Vernacexpr.vernac_classification) ty_sig
+| TyTerminal : string * ('r, 's) ty_sig -> ('r, 's) ty_sig
+| TyNonTerminal :
+ string option *
+ ('a, 'b, 'c) Extend.ty_user_symbol * ('r, 's) ty_sig ->
+ ('a -> 'r, 'a -> 's) ty_sig
+
+type ty_ml = TyML : bool (** deprecated *) * ('r, 's) ty_sig * 'r * 's option -> ty_ml
+
(** Wrapper to dynamically extend vernacular commands. *)
val vernac_extend :
command:string ->
?classifier:(string -> Vernacexpr.vernac_classification) ->
?entry:Vernacexpr.vernac_expr Pcoq.Entry.t ->
- (bool *
- Vernacinterp.plugin_args Vernacinterp.vernac_command *
- classifier option *
- Vernacexpr.vernac_expr Egramml.grammar_prod_item list) list -> unit
+ ty_ml list -> unit
(** {5 STM classifiers} *)
generated by cgit v1.2.3 (git 2.25.1) at 2026-01-31 16:59:40 +0000