aboutsummaryrefslogtreecommitdiffhomepage
diff options
context:
space:
mode:
Diffstat
-rw-r--r--doc/refman/RefMan-pro.tex19
-rw-r--r--intf/vernacexpr.mli1
-rw-r--r--parsing/g_proofs.ml436
-rw-r--r--parsing/g_vernac.ml434
-rw-r--r--printing/ppvernac.ml9
-rw-r--r--proofs/proof_using.ml30
-rw-r--r--proofs/proof_using.mli2
-rw-r--r--stm/texmacspp.ml1
-rw-r--r--stm/vernac_classifier.ml1
-rw-r--r--test-suite/success/proof_using.v31
-rw-r--r--toplevel/vernacentries.ml4
11 files changed, 126 insertions, 42 deletions
diff --git a/doc/refman/RefMan-pro.tex b/doc/refman/RefMan-pro.tex
index 8d69f1682..789297fb4 100644
--- a/doc/refman/RefMan-pro.tex
+++ b/doc/refman/RefMan-pro.tex
@@ -177,6 +177,25 @@ The following options modify the behavior of {\tt Proof using}.
When {\tt Qed} is performed, suggest a {\tt using} annotation if
the user did not provide one.
+\subsubsection[\tt Package]{Name a set of section hypotheses for {\tt Proof using}}
+\comindex{Package}
+
+The command {\tt Package} can be used to name a set of section hypotheses,
+with the purpose of making {\tt Proof using} annotations more compat.
+
+\variant {\tt Package Some := x y z.}
+
+ Define the package named "Some" containing {\tt x y} and {\tt z}
+
+\variant {\tt Package Fewer := Some - x.}
+
+ Define the package named "Fewer" containing only {\tt x y}
+
+\variant {\tt Package Many := Fewer + Some.}
+
+ Define the package named "Many" containing the union of the elements
+ of "Fewer" and "Some", namely {\tt x y z}.
+
\subsection[\tt Abort.]{\tt Abort.\comindex{Abort}}
This command cancels the current proof development, switching back to
diff --git a/intf/vernacexpr.mli b/intf/vernacexpr.mli
index bc167d94a..f66b1c124 100644
--- a/intf/vernacexpr.mli
+++ b/intf/vernacexpr.mli
@@ -323,6 +323,7 @@ type vernac_expr =
class_rawexpr * class_rawexpr
| VernacIdentityCoercion of obsolete_locality * lident *
class_rawexpr * class_rawexpr
+ | VernacNameSectionHypSet of lident * section_subset_descr
(* Type classes *)
| VernacInstance of
diff --git a/parsing/g_proofs.ml4 b/parsing/g_proofs.ml4
index 2c8eb85b8..60313d749 100644
--- a/parsing/g_proofs.ml4
+++ b/parsing/g_proofs.ml4
@@ -20,17 +20,6 @@ open Pcoq.Vernac_
let thm_token = G_vernac.thm_token
-let only_identrefs =
- Gram.Entry.of_parser "test_only_identrefs"
- (fun strm ->
- let rec aux n =
- match get_tok (Util.stream_nth n strm) with
- | KEYWORD "." -> ()
- | KEYWORD ")" -> ()
- | IDENT _ -> aux (n+1)
- | _ -> raise Stream.Failure in
- aux 0)
-
let hint_proof_using e = function
| Some _ as x -> x
| None -> match Proof_using.get_default_proof_using () with
@@ -48,12 +37,12 @@ GEXTEND Gram
command:
[ [ IDENT "Goal"; c = lconstr -> VernacGoal c
| IDENT "Proof" ->
- VernacProof (None,hint_proof_using section_subset_descr None)
+ VernacProof (None,hint_proof_using G_vernac.section_subset_descr None)
| IDENT "Proof" ; IDENT "Mode" ; mn = string -> VernacProofMode mn
| IDENT "Proof"; "with"; ta = tactic;
- l = OPT [ "using"; l = section_subset_descr -> l ] ->
- VernacProof (Some ta, hint_proof_using section_subset_descr l)
- | IDENT "Proof"; "using"; l = section_subset_descr;
+ l = OPT [ "using"; l = G_vernac.section_subset_descr -> l ] ->
+ VernacProof (Some ta,hint_proof_using G_vernac.section_subset_descr l)
+ | IDENT "Proof"; "using"; l = G_vernac.section_subset_descr;
ta = OPT [ "with"; ta = tactic -> ta ] ->
VernacProof (ta,Some l)
| IDENT "Proof"; c = lconstr -> VernacExactProof c
@@ -115,23 +104,6 @@ GEXTEND Gram
VernacHints (false,dbnames,
HintsResolve (List.map (fun x -> (pri, true, x)) lc))
] ];
- section_subset_descr:
- [ [ IDENT "All" -> SsAll
- | "Type" -> SsType
- | only_identrefs; l = LIST0 identref -> SsExpr (SsSet l)
- | e = section_subset_expr -> SsExpr e ] ]
- ;
- section_subset_expr:
- [ "35"
- [ "-"; e = section_subset_expr -> SsCompl e ]
- | "50"
- [ e1 = section_subset_expr; "-"; e2 = section_subset_expr->SsSubstr(e1,e2)
- | e1 = section_subset_expr; "+"; e2 = section_subset_expr->SsUnion(e1,e2)]
- | "0"
- [ i = identref -> SsSet [i]
- | "("; only_identrefs; l = LIST0 identref; ")"-> SsSet l
- | "("; e = section_subset_expr; ")"-> e ] ]
- ;
obsolete_locality:
[ [ IDENT "Local" -> true | -> false ] ]
;
diff --git a/parsing/g_vernac.ml4 b/parsing/g_vernac.ml4
index ce731a5f5..77ba41f4e 100644
--- a/parsing/g_vernac.ml4
+++ b/parsing/g_vernac.ml4
@@ -46,6 +46,7 @@ let record_field = Gram.entry_create "vernac:record_field"
let of_type_with_opt_coercion = Gram.entry_create "vernac:of_type_with_opt_coercion"
let subgoal_command = Gram.entry_create "proof_mode:subgoal_command"
let instance_name = Gram.entry_create "vernac:instance_name"
+let section_subset_descr = Gram.entry_create "vernac:section_subset_descr"
let command_entry = ref noedit_mode
let set_command_entry e = command_entry := e
@@ -423,10 +424,20 @@ GEXTEND Gram
;
END
+let only_identrefs =
+ Gram.Entry.of_parser "test_only_identrefs"
+ (fun strm ->
+ let rec aux n =
+ match get_tok (Util.stream_nth n strm) with
+ | KEYWORD "." -> ()
+ | KEYWORD ")" -> ()
+ | IDENT _ -> aux (n+1)
+ | _ -> raise Stream.Failure in
+ aux 0)
(* Modules and Sections *)
GEXTEND Gram
- GLOBAL: gallina_ext module_expr module_type;
+ GLOBAL: gallina_ext module_expr module_type section_subset_descr;
gallina_ext:
[ [ (* Interactive module declaration *)
@@ -448,6 +459,10 @@ GEXTEND Gram
(* This end a Section a Module or a Module Type *)
| IDENT "End"; id = identref -> VernacEndSegment id
+ (* Naming a set of section hyps *)
+ | IDENT "Package"; id = identref; ":="; expr = section_subset_descr ->
+ VernacNameSectionHypSet (id, expr)
+
(* Requiring an already compiled module *)
| IDENT "Require"; export = export_token; qidl = LIST1 global ->
VernacRequire (export, qidl)
@@ -537,6 +552,23 @@ GEXTEND Gram
CMwith (!@loc,mty,decl)
] ]
;
+ section_subset_descr:
+ [ [ IDENT "All" -> SsAll
+ | "Type" -> SsType
+ | only_identrefs; l = LIST0 identref -> SsExpr (SsSet l)
+ | e = section_subset_expr -> SsExpr e ] ]
+ ;
+ section_subset_expr:
+ [ "35"
+ [ "-"; e = section_subset_expr -> SsCompl e ]
+ | "50"
+ [ e1 = section_subset_expr; "-"; e2 = section_subset_expr->SsSubstr(e1,e2)
+ | e1 = section_subset_expr; "+"; e2 = section_subset_expr->SsUnion(e1,e2)]
+ | "0"
+ [ i = identref -> SsSet [i]
+ | "("; only_identrefs; l = LIST0 identref; ")"-> SsSet l
+ | "("; e = section_subset_expr; ")"-> e ] ]
+ ;
END
(* Extensions: implicits, coercions, etc. *)
diff --git a/printing/ppvernac.ml b/printing/ppvernac.ml
index eca67ad86..993f9fd91 100644
--- a/printing/ppvernac.ml
+++ b/printing/ppvernac.ml
@@ -855,6 +855,9 @@ module Make
return (hov 2 (keyword "Section" ++ spc () ++ pr_lident id))
| VernacEndSegment id ->
return (hov 2 (keyword "End" ++ spc() ++ pr_lident id))
+ | VernacNameSectionHypSet (id,set) ->
+ return (hov 2 (keyword "Package" ++ spc() ++ pr_lident id ++ spc()++
+ str ":="++spc()++pr_using set))
| VernacRequire (exp, l) ->
return (
hov 2
@@ -1208,12 +1211,14 @@ module Make
| VernacProof (None, None) ->
return (keyword "Proof")
| VernacProof (None, Some e) ->
- return (keyword "Proof " ++ pr_using e)
+ return (keyword "Proof " ++ spc () ++
+ keyword "using" ++ spc() ++ pr_using e)
| VernacProof (Some te, None) ->
return (keyword "Proof with" ++ spc() ++ pr_raw_tactic te)
| VernacProof (Some te, Some e) ->
return (
- keyword "Proof" ++ spc () ++ pr_using e ++ spc() ++
+ keyword "Proof" ++ spc () ++
+ keyword "using" ++ spc() ++ pr_using e ++ spc() ++
keyword "with" ++ spc() ++pr_raw_tactic te
)
| VernacProofMode s ->
diff --git a/proofs/proof_using.ml b/proofs/proof_using.ml
index 746daf273..f326548d1 100644
--- a/proofs/proof_using.ml
+++ b/proofs/proof_using.ml
@@ -26,25 +26,41 @@ let to_string = function
| SsSubstr(e1,e2) -> "("^aux e1 ^" - "^ aux e2^")"
in aux e
-let set_of_list l = List.fold_right Id.Set.add l Id.Set.empty
+let known_names = Summary.ref [] ~name:"proofusing-nameset"
-let full_set env = set_of_list (List.map pi1 (named_context env))
+let in_nameset =
+ let open Libobject in
+ declare_object { (default_object "proofusing-nameset") with
+ cache_function = (fun (_,x) -> known_names := x :: !known_names);
+ classify_function = (fun _ -> Dispose);
+ discharge_function = (fun _ -> None)
+ }
-let process_expr env e ty =
+let rec process_expr env e ty =
match e with
- | SsAll -> List.map pi1 (named_context env)
+ | SsAll ->
+ List.fold_right Id.Set.add (List.map pi1 (named_context env)) Id.Set.empty
| SsExpr e ->
let rec aux = function
- | SsSet l -> set_of_list (List.map snd l)
+ | SsSet l -> set_of_list env (List.map snd l)
| SsUnion(e1,e2) -> Id.Set.union (aux e1) (aux e2)
| SsSubstr(e1,e2) -> Id.Set.diff (aux e1) (aux e2)
| SsCompl e -> Id.Set.diff (full_set env) (aux e)
in
- Id.Set.elements (aux e)
+ aux e
| SsType ->
match ty with
- | [ty] -> Id.Set.elements (global_vars_set env ty)
+ | [ty] -> global_vars_set env ty
| _ -> Errors.error"Proof using on a multiple lemma is not supported"
+and set_of_list env = function
+ | [x] when CList.mem_assoc_f Id.equal x !known_names ->
+ process_expr env (CList.assoc_f Id.equal x !known_names) []
+ | l -> List.fold_right Id.Set.add l Id.Set.empty
+and full_set env = set_of_list env (List.map pi1 (named_context env))
+
+let process_expr env e ty = Id.Set.elements (process_expr env e ty)
+
+let name_set id expr = Lib.add_anonymous_leaf (in_nameset (id,expr))
let minimize_hyps env ids =
let rec aux ids =
diff --git a/proofs/proof_using.mli b/proofs/proof_using.mli
index f1731621d..ccda82c60 100644
--- a/proofs/proof_using.mli
+++ b/proofs/proof_using.mli
@@ -19,6 +19,8 @@ val process_expr :
Environ.env -> Vernacexpr.section_subset_descr -> Constr.types list ->
Names.Id.t list
+val name_set : Names.Id.t -> Vernacexpr.section_subset_descr -> unit
+
val to_string : Vernacexpr.section_subset_descr -> string
val get_default_proof_using : unit -> string option
diff --git a/stm/texmacspp.ml b/stm/texmacspp.ml
index fb103b782..1880a63a5 100644
--- a/stm/texmacspp.ml
+++ b/stm/texmacspp.ml
@@ -617,6 +617,7 @@ let rec tmpp v loc =
(* Gallina extensions *)
| VernacBeginSection (_, id) -> xmlBeginSection loc (Id.to_string id)
| VernacEndSegment (_, id) -> xmlEndSegment loc (Id.to_string id)
+ | VernacNameSectionHypSet _ as x -> xmlTODO loc x
| VernacRequire (None,l) ->
xmlRequire loc (List.map (fun ref ->
xmlReference ref) l)
diff --git a/stm/vernac_classifier.ml b/stm/vernac_classifier.ml
index cc960a267..4ad165a4c 100644
--- a/stm/vernac_classifier.ml
+++ b/stm/vernac_classifier.ml
@@ -169,6 +169,7 @@ let rec classify_vernac e =
| VernacDeclareClass _ | VernacDeclareInstances _
| VernacRegister _
| VernacDeclareTacticDefinition _
+ | VernacNameSectionHypSet _
| VernacComments _ -> VtSideff [], VtLater
(* Who knows *)
| VernacLoad _ -> VtSideff [], VtNow
diff --git a/test-suite/success/proof_using.v b/test-suite/success/proof_using.v
index bf302df44..d2691e763 100644
--- a/test-suite/success/proof_using.v
+++ b/test-suite/success/proof_using.v
@@ -65,3 +65,34 @@ End S1.
Check (deep 3 4 : 3 = 4).
Check (deep2 3 4 : 3 = 4).
+
+Section P1.
+
+Variable x : nat.
+Variable y : nat.
+Variable z : nat.
+
+
+Package TOTO := x y.
+
+Package TITI := TOTO - x.
+
+Lemma t1 : True. Proof using TOTO. trivial. Qed.
+Lemma t2 : True. Proof using TITI. trivial. Qed.
+
+ Section P2.
+ Package TOTO := x.
+ Lemma t3 : True. Proof using TOTO. trivial. Qed.
+ End P2.
+
+Lemma t4 : True. Proof using TOTO. trivial. Qed.
+
+End P1.
+
+Lemma t5 : True. Fail Proof using TOTO. trivial. Qed.
+
+Check (t1 1 2 : True).
+Check (t2 1 : True).
+Check (t3 1 : True).
+Check (t4 1 2 : True).
+
diff --git a/toplevel/vernacentries.ml b/toplevel/vernacentries.ml
index 809f3a07f..29ba18307 100644
--- a/toplevel/vernacentries.ml
+++ b/toplevel/vernacentries.ml
@@ -738,6 +738,8 @@ let vernac_end_section (loc,_) =
(DirPath.to_string (Lib.current_dirpath true)) "<>" "sec";
Lib.close_section ()
+let vernac_name_sec_hyp (_,id) set = Proof_using.name_set id set
+
(* Dispatcher of the "End" command *)
let vernac_end_segment (_,id as lid) =
@@ -1864,6 +1866,8 @@ let interp ?proof locality poly c =
| VernacEndSegment lid -> vernac_end_segment lid
+ | VernacNameSectionHypSet (lid, set) -> vernac_name_sec_hyp lid set
+
| VernacRequire (export, qidl) -> vernac_require export qidl
| VernacImport (export,qidl) -> vernac_import export qidl
| VernacCanonical qid -> vernac_canonical qid
generated by cgit v1.2.3 (git 2.39.1) at 2024-07-06 13:14:43 +0000