aboutsummaryrefslogtreecommitdiffhomepage
diff options
context:
space:
mode:
Diffstat
-rw-r--r--grammar/argextend.ml411
-rw-r--r--grammar/q_util.ml426
-rw-r--r--grammar/q_util.mli2
-rw-r--r--grammar/tacextend.ml43
-rw-r--r--grammar/vernacextend.ml48
-rw-r--r--parsing/highparsing.mllib1
-rw-r--r--parsing/pcoq.ml51
-rw-r--r--parsing/pcoq.mli2
-rw-r--r--plugins/funind/g_indfun.ml42
-rw-r--r--tactics/coretactics.ml41
-rw-r--r--tactics/extraargs.ml418
-rw-r--r--tactics/extraargs.mli7
-rw-r--r--tactics/extratactics.ml412
-rw-r--r--tactics/g_obligations.ml4 (renamed from toplevel/g_obligations.ml4)4
-rw-r--r--tactics/hightactics.mllib1
15 files changed, 105 insertions, 44 deletions
diff --git a/grammar/argextend.ml4 b/grammar/argextend.ml4
index 41e94914e..82bc09519 100644
--- a/grammar/argextend.ml4
+++ b/grammar/argextend.ml4
@@ -46,18 +46,16 @@ let has_extraarg l =
let make_act loc act pil =
let rec make = function
| [] -> <:expr< (fun loc -> $act$) >>
- | ExtNonTerminal (t, _, p) :: tl ->
- <:expr<
- (fun $lid:p$ ->
- let _ = Genarg.in_gen $make_rawwit loc t$ $lid:p$ in $make tl$)
- >>
+ | ExtNonTerminal (t, _, p) :: tl -> <:expr< (fun $lid:p$ -> $make tl$) >>
| ExtTerminal _ :: tl ->
<:expr< (fun _ -> $make tl$) >> in
make (List.rev pil)
let make_prod_item = function
| ExtTerminal s -> <:expr< Pcoq.Atoken (Lexer.terminal $mlexpr_of_string s$) >>
- | ExtNonTerminal (_, g, _) -> mlexpr_of_prod_entry_key g
+ | ExtNonTerminal (_, g, _) ->
+ let base s = <:expr< Pcoq.name_of_entry $lid:s$ >> in
+ mlexpr_of_prod_entry_key base g
let rec make_prod = function
| [] -> <:expr< Extend.Stop >>
@@ -174,7 +172,6 @@ let declare_vernac_argument loc s pr cl =
(fun _ _ _ _ -> Errors.anomaly (Pp.str "vernac argument needs not wit printer")) }
>> ]
-open Pcoq
open Pcaml
open PcamlSig (* necessary for camlp4 *)
diff --git a/grammar/q_util.ml4 b/grammar/q_util.ml4
index 3946d5d2b..c43ce15be 100644
--- a/grammar/q_util.ml4
+++ b/grammar/q_util.ml4
@@ -47,31 +47,23 @@ let mlexpr_of_option f = function
let mlexpr_of_ident id =
<:expr< Names.Id.of_string $str:id$ >>
-let rec mlexpr_of_prod_entry_key = function
- | Extend.Ulist1 s -> <:expr< Pcoq.Alist1 $mlexpr_of_prod_entry_key s$ >>
- | Extend.Ulist1sep (s,sep) -> <:expr< Pcoq.Alist1sep $mlexpr_of_prod_entry_key s$ $str:sep$ >>
- | Extend.Ulist0 s -> <:expr< Pcoq.Alist0 $mlexpr_of_prod_entry_key s$ >>
- | Extend.Ulist0sep (s,sep) -> <:expr< Pcoq.Alist0sep $mlexpr_of_prod_entry_key s$ $str:sep$ >>
- | Extend.Uopt s -> <:expr< Pcoq.Aopt $mlexpr_of_prod_entry_key s$ >>
- | Extend.Umodifiers s -> <:expr< Pcoq.Amodifiers $mlexpr_of_prod_entry_key s$ >>
- | Extend.Uentry e -> <:expr< Pcoq.Aentry (Pcoq.name_of_entry $lid:e$) >>
+let rec mlexpr_of_prod_entry_key f = function
+ | Extend.Ulist1 s -> <:expr< Pcoq.Alist1 $mlexpr_of_prod_entry_key f s$ >>
+ | Extend.Ulist1sep (s,sep) -> <:expr< Pcoq.Alist1sep $mlexpr_of_prod_entry_key f s$ $str:sep$ >>
+ | Extend.Ulist0 s -> <:expr< Pcoq.Alist0 $mlexpr_of_prod_entry_key f s$ >>
+ | Extend.Ulist0sep (s,sep) -> <:expr< Pcoq.Alist0sep $mlexpr_of_prod_entry_key f s$ $str:sep$ >>
+ | Extend.Uopt s -> <:expr< Pcoq.Aopt $mlexpr_of_prod_entry_key f s$ >>
+ | Extend.Umodifiers s -> <:expr< Pcoq.Amodifiers $mlexpr_of_prod_entry_key f s$ >>
+ | Extend.Uentry e -> <:expr< Pcoq.Aentry $f e$ >>
| Extend.Uentryl (e, l) ->
(** Keep in sync with Pcoq! *)
assert (CString.equal e "tactic");
if l = 5 then <:expr< Pcoq.Aentry (Pcoq.name_of_entry Pcoq.Tactic.binder_tactic) >>
else <:expr< Pcoq.Aentryl (Pcoq.name_of_entry Pcoq.Tactic.tactic_expr) $mlexpr_of_int l$ >>
-let type_entry u e =
- let Pcoq.TypedEntry (t, _) = Pcoq.get_entry u e in
- Genarg.unquote t
-
let rec type_of_user_symbol = function
| Ulist1 s | Ulist1sep (s, _) | Ulist0 s | Ulist0sep (s, _) | Umodifiers s ->
Genarg.ListArgType (type_of_user_symbol s)
| Uopt s ->
Genarg.OptArgType (type_of_user_symbol s)
-| Uentry e | Uentryl (e, _) ->
- try type_entry Pcoq.uprim e with Not_found ->
- try type_entry Pcoq.uconstr e with Not_found ->
- try type_entry Pcoq.utactic e with Not_found ->
- Genarg.ExtraArgType e
+| Uentry e | Uentryl (e, _) -> Genarg.ExtraArgType e
diff --git a/grammar/q_util.mli b/grammar/q_util.mli
index 837ec6fb0..712aa8509 100644
--- a/grammar/q_util.mli
+++ b/grammar/q_util.mli
@@ -28,6 +28,6 @@ val mlexpr_of_option : ('a -> MLast.expr) -> 'a option -> MLast.expr
val mlexpr_of_ident : string -> MLast.expr
-val mlexpr_of_prod_entry_key : Extend.user_symbol -> MLast.expr
+val mlexpr_of_prod_entry_key : (string -> MLast.expr) -> Extend.user_symbol -> MLast.expr
val type_of_user_symbol : Extend.user_symbol -> Genarg.argument_type
diff --git a/grammar/tacextend.ml4 b/grammar/tacextend.ml4
index c35fa00d2..8c85d0162 100644
--- a/grammar/tacextend.ml4
+++ b/grammar/tacextend.ml4
@@ -85,8 +85,9 @@ let make_fun_clauses loc s l =
let make_prod_item = function
| ExtTerminal s -> <:expr< Egramml.GramTerminal $str:s$ >>
| ExtNonTerminal (nt, g, id) ->
+ let base s = <:expr< Pcoq.genarg_grammar $mk_extraarg loc s$ >> in
<:expr< Egramml.GramNonTerminal $default_loc$ $make_rawwit loc nt$
- $mlexpr_of_prod_entry_key g$ >>
+ $mlexpr_of_prod_entry_key base g$ >>
let mlexpr_of_clause cl =
mlexpr_of_list (fun (a,_,_) -> mlexpr_of_list make_prod_item a) cl
diff --git a/grammar/vernacextend.ml4 b/grammar/vernacextend.ml4
index 3bb1e0907..d8c885088 100644
--- a/grammar/vernacextend.ml4
+++ b/grammar/vernacextend.ml4
@@ -42,7 +42,7 @@ let rec make_let e = function
let make_clause { r_patt = pt; r_branch = e; } =
(make_patt pt,
- vala (Some (make_when (MLast.loc_of_expr e) pt)),
+ vala None,
make_let e pt)
(* To avoid warnings *)
@@ -58,11 +58,11 @@ let make_clause_classifier cg s { r_patt = pt; r_class = c; } =
match c ,cg with
| Some c, _ ->
(make_patt pt,
- vala (Some (make_when (MLast.loc_of_expr c) pt)),
+ vala None,
make_let (mk_ignore c pt) pt)
| None, Some cg ->
(make_patt pt,
- vala (Some (make_when (MLast.loc_of_expr cg) pt)),
+ vala None,
<:expr< fun () -> $cg$ $str:s$ >>)
| None, None -> msg_warning
(strbrk("Vernac entry \""^s^"\" misses a classifier. "^
@@ -85,7 +85,7 @@ let make_clause_classifier cg s { r_patt = pt; r_class = c; } =
strbrk("Specific classifiers have precedence over global "^
"classifiers. Only one classifier is called.")++fnl());
(make_patt pt,
- vala (Some (make_when loc pt)),
+ vala None,
<:expr< fun () -> (Vernacexpr.VtUnknown, Vernacexpr.VtNow) >>)
let make_fun_clauses loc s l =
diff --git a/parsing/highparsing.mllib b/parsing/highparsing.mllib
index 13ed80464..eed6caea3 100644
--- a/parsing/highparsing.mllib
+++ b/parsing/highparsing.mllib
@@ -4,4 +4,3 @@ G_prim
G_proofs
G_tactic
G_ltac
-G_obligations
diff --git a/parsing/pcoq.ml b/parsing/pcoq.ml
index 1b1ecaf91..05fd9f9d8 100644
--- a/parsing/pcoq.ml
+++ b/parsing/pcoq.ml
@@ -229,12 +229,23 @@ let get_typed_entry e =
let new_entry etyp u s =
let utab = get_utable u in
let uname = Entry.univ_name u in
- let _ = Entry.create u s in
+ let entry = Entry.create u s in
let ename = uname ^ ":" ^ s in
let e = Gram.entry_create ename in
- Hashtbl.add utab s (TypedEntry (etyp, e)); e
+ Hashtbl.add utab s (TypedEntry (etyp, e)); (entry, e)
-let make_gen_entry u rawwit s = new_entry rawwit u s
+let make_gen_entry u rawwit s = snd (new_entry rawwit u s)
+
+module GrammarObj =
+struct
+ type ('r, _, _) obj = 'r Entry.t
+ let name = "grammar"
+ let default _ = None
+end
+
+module Grammar = Register(GrammarObj)
+
+let genarg_grammar wit = Grammar.obj wit
let create_generic_entry (type a) u s (etyp : a raw_abstract_argument_type) : a Gram.entry =
let utab = get_utable u in
@@ -242,7 +253,10 @@ let create_generic_entry (type a) u s (etyp : a raw_abstract_argument_type) : a
let u = Entry.univ_name u in
failwith ("Entry " ^ u ^ ":" ^ s ^ " already exists");
else
- new_entry etyp u s
+ let (entry, e) = new_entry etyp u s in
+ let Rawwit t = etyp in
+ let () = Grammar.register0 t entry in
+ e
(* Initial grammar entries *)
@@ -841,3 +855,32 @@ let epsilon_value f e =
let entry = G.entry_create "epsilon" in
let () = maybe_uncurry (Gram.extend entry) ext in
try Some (parse_string entry "") with _ -> None
+
+(** Registering grammar of generic arguments *)
+
+let () =
+ let open Stdarg in
+ let open Constrarg in
+(* Grammar.register0 wit_unit; *)
+(* Grammar.register0 wit_bool; *)
+ Grammar.register0 wit_int (name_of_entry Prim.integer);
+ Grammar.register0 wit_string (name_of_entry Prim.string);
+ Grammar.register0 wit_pre_ident (name_of_entry Prim.preident);
+ Grammar.register0 wit_int_or_var (name_of_entry Tactic.int_or_var);
+ Grammar.register0 wit_intro_pattern (name_of_entry Tactic.simple_intropattern);
+ Grammar.register0 wit_ident (name_of_entry Prim.ident);
+ Grammar.register0 wit_var (name_of_entry Prim.var);
+ Grammar.register0 wit_ref (name_of_entry Prim.reference);
+ Grammar.register0 wit_quant_hyp (name_of_entry Tactic.quantified_hypothesis);
+ Grammar.register0 wit_sort (name_of_entry Constr.sort);
+ Grammar.register0 wit_constr (name_of_entry Constr.constr);
+ Grammar.register0 wit_constr_may_eval (name_of_entry Tactic.constr_may_eval);
+ Grammar.register0 wit_uconstr (name_of_entry Tactic.uconstr);
+ Grammar.register0 wit_open_constr (name_of_entry Tactic.open_constr);
+ Grammar.register0 wit_constr_with_bindings (name_of_entry Tactic.constr_with_bindings);
+ Grammar.register0 wit_bindings (name_of_entry Tactic.bindings);
+(* Grammar.register0 wit_hyp_location_flag; *)
+ Grammar.register0 wit_red_expr (name_of_entry Tactic.red_expr);
+ Grammar.register0 wit_tactic (name_of_entry Tactic.tactic);
+ Grammar.register0 wit_clause_dft_concl (name_of_entry Tactic.clause_dft_concl);
+ ()
diff --git a/parsing/pcoq.mli b/parsing/pcoq.mli
index 625f0370e..b1353ef8a 100644
--- a/parsing/pcoq.mli
+++ b/parsing/pcoq.mli
@@ -160,6 +160,8 @@ val uconstr : gram_universe
val utactic : gram_universe
val uvernac : gram_universe
+val genarg_grammar : ('raw, 'glb, 'top) genarg_type -> 'raw Entry.t
+
val get_entry : gram_universe -> string -> typed_entry
val create_generic_entry : gram_universe -> string ->
diff --git a/plugins/funind/g_indfun.ml4 b/plugins/funind/g_indfun.ml4
index 4bd69b9fe..e93c395e3 100644
--- a/plugins/funind/g_indfun.ml4
+++ b/plugins/funind/g_indfun.ml4
@@ -94,7 +94,7 @@ let out_disjunctive = function
| loc, IntroAction (IntroOrAndPattern l) -> (loc,l)
| _ -> Errors.error "Disjunctive or conjunctive intro pattern expected."
-ARGUMENT EXTEND with_names TYPED AS simple_intropattern_opt PRINTED BY pr_intro_as_pat
+ARGUMENT EXTEND with_names TYPED AS intropattern_opt PRINTED BY pr_intro_as_pat
| [ "as" simple_intropattern(ipat) ] -> [ Some ipat ]
| [] ->[ None ]
END
diff --git a/tactics/coretactics.ml4 b/tactics/coretactics.ml4
index 73b7bde9d..6c02a7202 100644
--- a/tactics/coretactics.ml4
+++ b/tactics/coretactics.ml4
@@ -15,6 +15,7 @@ open Misctypes
open Genredexpr
open Stdarg
open Constrarg
+open Extraargs
open Pcoq.Constr
open Pcoq.Prim
open Pcoq.Tactic
diff --git a/tactics/extraargs.ml4 b/tactics/extraargs.ml4
index 8215e785a..d33ec91f9 100644
--- a/tactics/extraargs.ml4
+++ b/tactics/extraargs.ml4
@@ -55,6 +55,14 @@ ARGUMENT EXTEND orient TYPED AS bool PRINTED BY pr_orient
| [ ] -> [ true ]
END
+let pr_int _ _ _ i = Pp.int i
+
+let _natural = Pcoq.Prim.natural
+
+ARGUMENT EXTEND natural TYPED AS int PRINTED BY pr_int
+| [ _natural(i) ] -> [ i ]
+END
+
let pr_orient = pr_orient () () ()
@@ -122,6 +130,8 @@ let interp_glob ist gl (t,_) = Tacmach.project gl , (ist,t)
let glob_glob = Tacintern.intern_constr
+let pr_lconstr _ prc _ c = prc c
+
let subst_glob = Tacsubst.subst_glob_constr_and_expr
ARGUMENT EXTEND glob
@@ -139,6 +149,14 @@ ARGUMENT EXTEND glob
[ constr(c) ] -> [ c ]
END
+let l_constr = Pcoq.Constr.lconstr
+
+ARGUMENT EXTEND lconstr
+ TYPED AS constr
+ PRINTED BY pr_lconstr
+ [ l_constr(c) ] -> [ c ]
+END
+
ARGUMENT EXTEND lglob
PRINTED BY pr_globc
diff --git a/tactics/extraargs.mli b/tactics/extraargs.mli
index f7b379e69..14aa69875 100644
--- a/tactics/extraargs.mli
+++ b/tactics/extraargs.mli
@@ -21,6 +21,8 @@ val wit_occurrences : (int list or_var, int list or_var, int list) Genarg.genarg
val pr_occurrences : int list or_var -> Pp.std_ppcmds
val occurrences_of : int list -> Locus.occurrences
+val wit_natural : int Genarg.uniform_genarg_type
+
val wit_glob :
(constr_expr,
Tacexpr.glob_constr_and_expr,
@@ -31,6 +33,11 @@ val wit_lglob :
Tacexpr.glob_constr_and_expr,
Tacinterp.interp_sign * glob_constr) Genarg.genarg_type
+val wit_lconstr :
+ (constr_expr,
+ Tacexpr.glob_constr_and_expr,
+ Constr.t) Genarg.genarg_type
+
val glob : constr_expr Pcoq.Gram.entry
val lglob : constr_expr Pcoq.Gram.entry
diff --git a/tactics/extratactics.ml4 b/tactics/extratactics.ml4
index 52419497d..0cc796886 100644
--- a/tactics/extratactics.ml4
+++ b/tactics/extratactics.ml4
@@ -154,23 +154,23 @@ TACTIC EXTEND einjection
| [ "einjection" quantified_hypothesis(h) ] -> [ injClause None true (Some (induction_arg_of_quantified_hyp h)) ]
END
TACTIC EXTEND injection_as_main
-| [ "injection" constr_with_bindings(c) "as" simple_intropattern_list(ipat)] ->
+| [ "injection" constr_with_bindings(c) "as" intropattern_list(ipat)] ->
[ elimOnConstrWithHoles (injClause (Some ipat)) false c ]
END
TACTIC EXTEND injection_as
-| [ "injection" "as" simple_intropattern_list(ipat)] ->
+| [ "injection" "as" intropattern_list(ipat)] ->
[ injClause (Some ipat) false None ]
-| [ "injection" quantified_hypothesis(h) "as" simple_intropattern_list(ipat) ] ->
+| [ "injection" quantified_hypothesis(h) "as" intropattern_list(ipat) ] ->
[ injClause (Some ipat) false (Some (induction_arg_of_quantified_hyp h)) ]
END
TACTIC EXTEND einjection_as_main
-| [ "einjection" constr_with_bindings(c) "as" simple_intropattern_list(ipat)] ->
+| [ "einjection" constr_with_bindings(c) "as" intropattern_list(ipat)] ->
[ elimOnConstrWithHoles (injClause (Some ipat)) true c ]
END
TACTIC EXTEND einjection_as
-| [ "einjection" "as" simple_intropattern_list(ipat)] ->
+| [ "einjection" "as" intropattern_list(ipat)] ->
[ injClause (Some ipat) true None ]
-| [ "einjection" quantified_hypothesis(h) "as" simple_intropattern_list(ipat) ] ->
+| [ "einjection" quantified_hypothesis(h) "as" intropattern_list(ipat) ] ->
[ injClause (Some ipat) true (Some (induction_arg_of_quantified_hyp h)) ]
END
diff --git a/toplevel/g_obligations.ml4 b/tactics/g_obligations.ml4
index dd11efebd..e67d70121 100644
--- a/toplevel/g_obligations.ml4
+++ b/tactics/g_obligations.ml4
@@ -63,11 +63,11 @@ open Obligations
let classify_obbl _ = Vernacexpr.(VtStartProof ("Classic",Doesn'tGuaranteeOpacity,[]), VtLater)
VERNAC COMMAND EXTEND Obligations CLASSIFIED BY classify_obbl
-| [ "Obligation" integer(num) "of" ident(name) ":" lconstr(t) withtac(tac) ] ->
+| [ "Obligation" integer(num) "of" ident(name) ":" lglob(t) withtac(tac) ] ->
[ obligation (num, Some name, Some t) tac ]
| [ "Obligation" integer(num) "of" ident(name) withtac(tac) ] ->
[ obligation (num, Some name, None) tac ]
-| [ "Obligation" integer(num) ":" lconstr(t) withtac(tac) ] ->
+| [ "Obligation" integer(num) ":" lglob(t) withtac(tac) ] ->
[ obligation (num, None, Some t) tac ]
| [ "Obligation" integer(num) withtac(tac) ] ->
[ obligation (num, None, None) tac ]
diff --git a/tactics/hightactics.mllib b/tactics/hightactics.mllib
index 73f11d0be..5c5946542 100644
--- a/tactics/hightactics.mllib
+++ b/tactics/hightactics.mllib
@@ -1,4 +1,5 @@
Extraargs
+G_obligations
Coretactics
Autorewrite
Extratactics
generated by cgit v1.2.3 (git 2.39.1) at 2024-06-01 21:28:23 +0000