aboutsummaryrefslogtreecommitdiff
path: root/coqpp
diff options
context:
space:
mode:
Diffstat (limited to 'coqpp')
-rw-r--r--coqpp/coqpp_ast.mli21
-rw-r--r--coqpp/coqpp_lex.mll5
-rw-r--r--coqpp/coqpp_main.ml138
-rw-r--r--coqpp/coqpp_parse.mly47
4 files changed, 164 insertions, 47 deletions
diff --git a/coqpp/coqpp_ast.mli b/coqpp/coqpp_ast.mli
index 956a916792..6f697f5d49 100644
--- a/coqpp/coqpp_ast.mli
+++ b/coqpp/coqpp_ast.mli
@@ -85,12 +85,31 @@ type tactic_ext = {
tacext_rules : tactic_rule list;
}
+type classification =
+| ClassifDefault
+| ClassifCode of code
+| ClassifName of string
+
+type vernac_rule = {
+ vernac_toks : ext_token list;
+ vernac_class : code option;
+ vernac_depr : bool;
+ vernac_body : code;
+}
+
+type vernac_ext = {
+ vernacext_name : string;
+ vernacext_entry : code option;
+ vernacext_class : classification;
+ vernacext_rules : vernac_rule list;
+}
+
type node =
| Code of code
| Comment of string
| DeclarePlugin of string
| GramExt of grammar_ext
-| VernacExt
+| VernacExt of vernac_ext
| TacticExt of tactic_ext
type t = node list
diff --git a/coqpp/coqpp_lex.mll b/coqpp/coqpp_lex.mll
index 81a53e887b..d809b824df 100644
--- a/coqpp/coqpp_lex.mll
+++ b/coqpp/coqpp_lex.mll
@@ -95,12 +95,16 @@ rule extend = parse
| "{" { start_ocaml lexbuf; ocaml lexbuf }
| "GRAMMAR" { GRAMMAR }
| "VERNAC" { VERNAC }
+| "COMMAND" { COMMAND }
| "TACTIC" { TACTIC }
| "EXTEND" { EXTEND }
| "END" { END }
| "DECLARE" { DECLARE }
| "PLUGIN" { PLUGIN }
| "DEPRECATED" { DEPRECATED }
+| "CLASSIFIED" { CLASSIFIED }
+| "BY" { BY }
+| "AS" { AS }
(** Camlp5 specific keywords *)
| "GLOBAL" { GLOBAL }
| "FIRST" { FIRST }
@@ -122,6 +126,7 @@ rule extend = parse
| ']' { RBRACKET }
| '|' { PIPE }
| "->" { ARROW }
+| "=>" { FUN }
| ',' { COMMA }
| ':' { COLON }
| ';' { SEMICOLON }
diff --git a/coqpp/coqpp_main.ml b/coqpp/coqpp_main.ml
index 42d8528a8c..602620968d 100644
--- a/coqpp/coqpp_main.ml
+++ b/coqpp/coqpp_main.ml
@@ -64,6 +64,39 @@ let string_split s =
let plugin_name = "__coq_plugin_name"
+let print_list fmt pr l =
+ let rec prl fmt = function
+ | [] -> ()
+ | [x] -> fprintf fmt "%a" pr x
+ | x :: l -> fprintf fmt "%a;@ %a" pr x prl l
+ in
+ fprintf fmt "@[<hv>[%a]@]" prl l
+
+let rec print_binders fmt = function
+| [] -> ()
+| ExtTerminal _ :: rem -> print_binders fmt rem
+| ExtNonTerminal (_, TokNone) :: rem ->
+ fprintf fmt "_@ %a" print_binders rem
+| ExtNonTerminal (_, TokName id) :: rem ->
+ fprintf fmt "%s@ %a" id print_binders rem
+
+let rec print_symbol fmt = function
+| Ulist1 s ->
+ fprintf fmt "@[Extend.TUlist1 (%a)@]" print_symbol s
+| Ulist1sep (s, sep) ->
+ fprintf fmt "@[Extend.TUlist1sep (%a, \"%s\")@]" print_symbol s sep
+| Ulist0 s ->
+ fprintf fmt "@[Extend.TUlist0 (%a)@]" print_symbol s
+| Ulist0sep (s, sep) ->
+ fprintf fmt "@[Extend.TUlist0sep (%a, \"%s\")@]" print_symbol s sep
+| Uopt s ->
+ fprintf fmt "@[Extend.TUopt (%a)@]" print_symbol s
+| Uentry e ->
+ fprintf fmt "@[Extend.TUentry (Genarg.get_arg_tag wit_%s)@]" e
+| Uentryl (e, l) ->
+ assert (e = "tactic");
+ fprintf fmt "@[Extend.TUentryl (Genarg.get_arg_tag wit_%s, %i)@]" e l
+
module GramExt :
sig
@@ -104,14 +137,6 @@ let print_local fmt ext =
let print_string fmt s = fprintf fmt "\"%s\"" s
-let print_list fmt pr l =
- let rec prl fmt = function
- | [] -> ()
- | [x] -> fprintf fmt "%a" pr x
- | x :: l -> fprintf fmt "%a;@ %a" pr x prl l
- in
- fprintf fmt "@[<hv>[%a]@]" prl l
-
let print_opt fmt pr = function
| None -> fprintf fmt "None"
| Some x -> fprintf fmt "Some@ (%a)" pr x
@@ -268,6 +293,61 @@ let print_ast fmt ext =
end
+module VernacExt :
+sig
+
+val print_ast : Format.formatter -> vernac_ext -> unit
+
+end =
+struct
+
+let print_rule_classifier fmt r = match r.vernac_class with
+| None -> fprintf fmt "None"
+| Some f -> fprintf fmt "Some @[(fun %a-> %s)@]" print_binders r.vernac_toks f.code
+
+let print_body fmt r =
+ fprintf fmt "@[(fun %a~atts@ ~st@ -> %s)@]"
+ print_binders r.vernac_toks r.vernac_body.code
+
+let rec print_sig fmt = function
+| [] -> fprintf fmt "@[Vernacentries.TyNil@]"
+| ExtTerminal s :: rem ->
+ fprintf fmt "@[Vernacentries.TyTerminal (\"%s\", %a)@]" s print_sig rem
+| ExtNonTerminal (symb, _) :: rem ->
+ fprintf fmt "@[Vernacentries.TyNonTerminal (%a, %a)@]"
+ print_symbol symb print_sig rem
+
+let print_rule fmt r =
+ fprintf fmt "Vernacentries.TyML (%b, %a, %a, %a)"
+ r.vernac_depr print_sig r.vernac_toks print_body r print_rule_classifier r
+
+let print_rules fmt rules =
+ print_list fmt (fun fmt r -> fprintf fmt "(%a)" print_rule r) rules
+
+let print_classifier fmt = function
+| ClassifDefault -> fprintf fmt ""
+| ClassifName "QUERY" ->
+ fprintf fmt "~classifier:(fun _ -> Vernac_classifier.classify_as_query)"
+| ClassifName "SIDEFF" ->
+ fprintf fmt "~classifier:(fun _ -> Vernac_classifier.classify_as_sideeff)"
+| ClassifName s -> fatal (Printf.sprintf "Unknown classifier %s" s)
+| ClassifCode c -> fprintf fmt "~classifier:(%s)" c.code
+
+let print_entry fmt = function
+| None -> fprintf fmt "None"
+| Some e -> fprintf fmt "Some (%s)" e.code
+
+let print_ast fmt ext =
+ let pr fmt () =
+ fprintf fmt "Vernacentries.vernac_extend ~command:\"%s\" %a ?entry:%a %a"
+ ext.vernacext_name print_classifier ext.vernacext_class
+ print_entry ext.vernacext_entry print_rules ext.vernacext_rules
+ in
+ let () = fprintf fmt "let () = @[%a@]@\n" pr () in
+ ()
+
+end
+
module TacticExt :
sig
@@ -276,49 +356,19 @@ val print_ast : Format.formatter -> tactic_ext -> unit
end =
struct
-let rec print_symbol fmt = function
-| Ulist1 s ->
- fprintf fmt "@[Extend.TUlist1 (%a)@]" print_symbol s
-| Ulist1sep (s, sep) ->
- fprintf fmt "@[Extend.TUlist1sep (%a, \"%s\")@]" print_symbol s sep
-| Ulist0 s ->
- fprintf fmt "@[Extend.TUlist0 (%a)@]" print_symbol s
-| Ulist0sep (s, sep) ->
- fprintf fmt "@[Extend.TUlist0sep (%a, \"%s\")@]" print_symbol s sep
-| Uopt s ->
- fprintf fmt "@[Extend.TUopt (%a)@]" print_symbol s
-| Uentry e ->
- fprintf fmt "@[Extend.TUentry (Genarg.get_arg_tag wit_%s)@]" e
-| Uentryl (e, l) ->
- assert (e = "tactic");
- fprintf fmt "@[Extend.TUentryl (Genarg.get_arg_tag wit_%s, %i)@]" e l
-
let rec print_clause fmt = function
-| [] -> fprintf fmt "@[TyNil@]"
-| ExtTerminal s :: cl -> fprintf fmt "@[TyIdent (\"%s\", %a)@]" s print_clause cl
+| [] -> fprintf fmt "@[Tacentries.TyNil@]"
+| ExtTerminal s :: cl -> fprintf fmt "@[Tacentries.TyIdent (\"%s\", %a)@]" s print_clause cl
| ExtNonTerminal (g, _) :: cl ->
- fprintf fmt "@[TyArg (%a, %a)@]"
+ fprintf fmt "@[Tacentries.TyArg (%a, %a)@]"
print_symbol g print_clause cl
-let rec print_binders fmt = function
-| [] -> fprintf fmt "ist@ "
-| ExtTerminal _ :: rem -> print_binders fmt rem
-| ExtNonTerminal (_, TokNone) :: rem ->
- fprintf fmt "_@ %a" print_binders rem
-| ExtNonTerminal (_, TokName id) :: rem ->
- fprintf fmt "%s@ %a" id print_binders rem
-
let print_rule fmt r =
- fprintf fmt "@[TyML (%a, @[fun %a -> %a@])@]"
+ fprintf fmt "@[Tacentries.TyML (%a, @[fun %aist@ -> %a@])@]"
print_clause r.tac_toks print_binders r.tac_toks print_code r.tac_body
-let rec print_rules fmt = function
-| [] -> ()
-| [r] -> fprintf fmt "(%a)@\n" print_rule r
-| r :: rem -> fprintf fmt "(%a);@\n%a" print_rule r print_rules rem
-
let print_rules fmt rules =
- fprintf fmt "Tacentries.([@[<v>%a@]])" print_rules rules
+ print_list fmt (fun fmt r -> fprintf fmt "(%a)" print_rule r) rules
let print_ast fmt ext =
let deprecation fmt =
@@ -347,7 +397,7 @@ let pr_ast fmt = function
| Comment s -> fprintf fmt "%s@\n" s
| DeclarePlugin name -> declare_plugin fmt name
| GramExt gram -> fprintf fmt "%a@\n" GramExt.print_ast gram
-| VernacExt -> fprintf fmt "VERNACEXT@\n"
+| VernacExt vernac -> fprintf fmt "%a@\n" VernacExt.print_ast vernac
| TacticExt tac -> fprintf fmt "%a@\n" TacticExt.print_ast tac
let () =
diff --git a/coqpp/coqpp_parse.mly b/coqpp/coqpp_parse.mly
index bf435fd247..31f234c37f 100644
--- a/coqpp/coqpp_parse.mly
+++ b/coqpp/coqpp_parse.mly
@@ -63,7 +63,8 @@ let parse_user_entry s sep =
%token <string> STRING
%token <int> INT
%token VERNAC TACTIC GRAMMAR EXTEND END DECLARE PLUGIN DEPRECATED
-%token LBRACKET RBRACKET PIPE ARROW COMMA EQUAL
+%token COMMAND CLASSIFIED BY AS
+%token LBRACKET RBRACKET PIPE ARROW FUN COMMA EQUAL
%token LPAREN RPAREN COLON SEMICOLON
%token GLOBAL FIRST LAST BEFORE AFTER LEVEL LEFTA RIGHTA NONA
%token EOF
@@ -104,7 +105,49 @@ grammar_extend:
;
vernac_extend:
-| VERNAC EXTEND IDENT END { VernacExt }
+| VERNAC vernac_entry EXTEND IDENT vernac_classifier vernac_rules END
+ { VernacExt {
+ vernacext_name = $4;
+ vernacext_entry = $2;
+ vernacext_class = $5;
+ vernacext_rules = $6;
+ } }
+;
+
+vernac_entry:
+| COMMAND { None }
+| CODE { Some $1 }
+;
+
+vernac_classifier:
+| { ClassifDefault }
+| CLASSIFIED BY CODE { ClassifCode $3 }
+| CLASSIFIED AS IDENT { ClassifName $3 }
+;
+
+vernac_rules:
+| vernac_rule { [$1] }
+| vernac_rule vernac_rules { $1 :: $2 }
+;
+
+vernac_rule:
+| PIPE LBRACKET ext_tokens RBRACKET rule_deprecation rule_classifier ARROW CODE
+ { {
+ vernac_toks = $3;
+ vernac_depr = $5;
+ vernac_class= $6;
+ vernac_body = $8;
+ } }
+;
+
+rule_deprecation:
+| { false }
+| DEPRECATED { true }
+;
+
+rule_classifier:
+| { None }
+| FUN CODE { Some $2 }
;
tactic_extend:
generated by cgit v1.2.3 (git 2.25.1) at 2026-01-31 14:52:17 +0000