aboutsummaryrefslogtreecommitdiffhomepage
path: root/parsing
diff options
context:
space:
mode:
authorGravatar Matthieu Sozeau <mattam@mattam.org>2016-10-24 18:18:33 +0200
committerGravatar Matthieu Sozeau <mattam@mattam.org>2016-11-03 16:26:27 +0100
commitd6fe6773c959493ed97108e1032b1bd8c1e78081 (patch)
tree69d1cb3e8aaf0b1800c0c09b22f70c162948f7d7 /parsing
parent6ec511721efc9235f6c2fa922a21dcb9b041bbfd (diff)
Lets Hints/Instances take an optional pattern
In addition to a priority, cleanup the interfaces for passing this information as well. The pattern, if given, takes priority over the inferred one. We only allow Existing Instances gr ... gr | pri. for now, without pattern, as before. Make the API compatible to 8.5 as well.
Diffstat (limited to 'parsing')
-rw-r--r--parsing/g_proofs.ml410
-rw-r--r--parsing/g_vernac.ml426
-rw-r--r--parsing/pcoq.ml1
-rw-r--r--parsing/pcoq.mli1
4 files changed, 23 insertions, 15 deletions
diff --git a/parsing/g_proofs.ml4 b/parsing/g_proofs.ml4
index 1e3c4b880..70c5d5d88 100644
--- a/parsing/g_proofs.ml4
+++ b/parsing/g_proofs.ml4
@@ -103,10 +103,9 @@ GEXTEND Gram
(* Declare "Resolve" explicitly so as to be able to later extend with
"Resolve ->" and "Resolve <-" *)
| IDENT "Hint"; IDENT "Resolve"; lc = LIST1 reference_or_constr;
- pri = OPT [ "|"; i = natural -> i ];
- dbnames = opt_hintbases ->
+ info = hint_info; dbnames = opt_hintbases ->
VernacHints (false,dbnames,
- HintsResolve (List.map (fun x -> (pri, true, x)) lc))
+ HintsResolve (List.map (fun x -> (info, true, x)) lc))
] ];
obsolete_locality:
[ [ IDENT "Local" -> true | -> false ] ]
@@ -116,9 +115,8 @@ GEXTEND Gram
| c = constr -> HintsConstr c ] ]
;
hint:
- [ [ IDENT "Resolve"; lc = LIST1 reference_or_constr;
- pri = OPT [ "|"; i = natural -> i ] ->
- HintsResolve (List.map (fun x -> (pri, true, x)) lc)
+ [ [ IDENT "Resolve"; lc = LIST1 reference_or_constr; info = hint_info ->
+ HintsResolve (List.map (fun x -> (info, true, x)) lc)
| IDENT "Immediate"; lc = LIST1 reference_or_constr -> HintsImmediate lc
| IDENT "Transparent"; lc = LIST1 global -> HintsTransparency (lc, true)
| IDENT "Opaque"; lc = LIST1 global -> HintsTransparency (lc, false)
diff --git a/parsing/g_vernac.ml4 b/parsing/g_vernac.ml4
index e0d836df8..ffc27d605 100644
--- a/parsing/g_vernac.ml4
+++ b/parsing/g_vernac.ml4
@@ -582,7 +582,7 @@ let warn_deprecated_implicit_arguments =
(* Extensions: implicits, coercions, etc. *)
GEXTEND Gram
- GLOBAL: gallina_ext instance_name;
+ GLOBAL: gallina_ext instance_name hint_info;
gallina_ext:
[ [ (* Transparent and Opaque *)
@@ -635,17 +635,20 @@ GEXTEND Gram
| IDENT "Instance"; namesup = instance_name; ":";
expl = [ "!" -> Decl_kinds.Implicit | -> Decl_kinds.Explicit ] ; t = operconstr LEVEL "200";
- pri = OPT [ "|"; i = natural -> i ] ;
+ info = hint_info ;
props = [ ":="; "{"; r = record_declaration; "}" -> Some (true,r) |
":="; c = lconstr -> Some (false,c) | -> None ] ->
- VernacInstance (false,snd namesup,(fst namesup,expl,t),props,pri)
+ VernacInstance (false,snd namesup,(fst namesup,expl,t),props,info)
| IDENT "Existing"; IDENT "Instance"; id = global;
- pri = OPT [ "|"; i = natural -> i ] ->
- VernacDeclareInstances ([id], pri)
+ info = hint_info ->
+ VernacDeclareInstances [id, info]
+
| IDENT "Existing"; IDENT "Instances"; ids = LIST1 global;
- pri = OPT [ "|"; i = natural -> i ] ->
- VernacDeclareInstances (ids, pri)
+ pri = OPT [ "|"; i = natural -> i ] ->
+ let info = { hint_priority = pri; hint_pattern = None } in
+ let insts = List.map (fun i -> (i, info)) ids in
+ VernacDeclareInstances insts
| IDENT "Existing"; IDENT "Class"; is = global -> VernacDeclareClass is
@@ -786,6 +789,11 @@ GEXTEND Gram
(Option.default [] sup)
| -> ((!@loc, Anonymous), None), [] ] ]
;
+ hint_info:
+ [ [ "|"; i = OPT natural; pat = OPT constr_pattern ->
+ { hint_priority = i; hint_pattern = pat }
+ | -> { hint_priority = None; hint_pattern = None } ] ]
+ ;
reserv_list:
[ [ bl = LIST1 reserv_tuple -> bl | b = simple_reserv -> [b] ] ]
;
@@ -807,8 +815,8 @@ GEXTEND Gram
(* Hack! Should be in grammar_ext, but camlp4 factorize badly *)
| IDENT "Declare"; IDENT "Instance"; namesup = instance_name; ":";
expl = [ "!" -> Decl_kinds.Implicit | -> Decl_kinds.Explicit ] ; t = operconstr LEVEL "200";
- pri = OPT [ "|"; i = natural -> i ] ->
- VernacInstance (true, snd namesup, (fst namesup, expl, t), None, pri)
+ info = hint_info ->
+ VernacInstance (true, snd namesup, (fst namesup, expl, t), None, info)
(* System directory *)
| IDENT "Pwd" -> VernacChdir None
diff --git a/parsing/pcoq.ml b/parsing/pcoq.ml
index 9e9a7e723..7dc02190e 100644
--- a/parsing/pcoq.ml
+++ b/parsing/pcoq.ml
@@ -379,6 +379,7 @@ module Vernac_ =
let vernac = gec_vernac "Vernac.vernac"
let vernac_eoi = eoi_entry vernac
let rec_definition = gec_vernac "Vernac.rec_definition"
+ let hint_info = gec_vernac "hint_info"
(* Main vernac entry *)
let main_entry = Gram.entry_create "vernac"
let noedit_mode = gec_vernac "noedit_command"
diff --git a/parsing/pcoq.mli b/parsing/pcoq.mli
index 7f6caf63f..ec8dac821 100644
--- a/parsing/pcoq.mli
+++ b/parsing/pcoq.mli
@@ -213,6 +213,7 @@ module Vernac_ :
val vernac_eoi : vernac_expr Gram.entry
val noedit_mode : vernac_expr Gram.entry
val command_entry : vernac_expr Gram.entry
+ val hint_info : Vernacexpr.hint_info_expr Gram.entry
end
(** The main entry: reads an optional vernac command *)