diff options
-rw-r--r-- | ide/texmacspp.ml | 1 | ||||
-rw-r--r-- | intf/vernacexpr.mli | 7 | ||||
-rw-r--r-- | parsing/g_vernac.ml4 | 35 | ||||
-rw-r--r-- | plugins/ltac/g_ltac.ml4 | 2 | ||||
-rw-r--r-- | printing/ppvernac.ml | 9 | ||||
-rw-r--r-- | proofs/proof_global.ml | 27 | ||||
-rw-r--r-- | proofs/proof_global.mli | 1 | ||||
-rw-r--r-- | stm/vernac_classifier.ml | 3 | ||||
-rw-r--r-- | test-suite/output/Search.out | 8 | ||||
-rw-r--r-- | test-suite/output/Search.v | 10 | ||||
-rw-r--r-- | vernac/vernacentries.ml | 32 |
11 files changed, 75 insertions, 60 deletions
diff --git a/ide/texmacspp.ml b/ide/texmacspp.ml index e787e48bf..e20704b7f 100644 --- a/ide/texmacspp.ml +++ b/ide/texmacspp.ml @@ -504,7 +504,6 @@ let rec tmpp v loc = xmlApply loc (Element("timeout",["val",string_of_int s],[]) :: [tmpp e loc]) | VernacFail e -> xmlApply loc (Element("fail",[],[]) :: [tmpp e loc]) - | VernacError _ -> xmlWithLoc loc "error" [] [] (* Syntax *) | VernacSyntaxExtension (_, ((_, name), sml)) -> diff --git a/intf/vernacexpr.mli b/intf/vernacexpr.mli index 25d3c705f..f018d59e6 100644 --- a/intf/vernacexpr.mli +++ b/intf/vernacexpr.mli @@ -71,7 +71,7 @@ type printable = | PrintScopes | PrintScope of string | PrintVisibility of string option - | PrintAbout of reference or_by_notation*int option + | PrintAbout of reference or_by_notation * goal_selector option | PrintImplicit of reference or_by_notation | PrintAssumptions of bool * bool * reference or_by_notation | PrintStrategy of reference or_by_notation option @@ -316,7 +316,6 @@ type vernac_expr = | VernacRedirect of string * vernac_expr located | VernacTimeout of int * vernac_expr | VernacFail of vernac_expr - | VernacError of exn (* always fails *) (* Syntax *) | VernacSyntaxExtension of @@ -436,11 +435,11 @@ type vernac_expr = | VernacRemoveOption of Goptions.option_name * option_ref_value list | VernacMemOption of Goptions.option_name * option_ref_value list | VernacPrintOption of Goptions.option_name - | VernacCheckMayEval of Genredexpr.raw_red_expr option * int option * constr_expr + | VernacCheckMayEval of Genredexpr.raw_red_expr option * goal_selector option * constr_expr | VernacGlobalCheck of constr_expr | VernacDeclareReduction of string * Genredexpr.raw_red_expr | VernacPrint of printable - | VernacSearch of searchable * int option * search_restriction + | VernacSearch of searchable * goal_selector option * search_restriction | VernacLocate of locatable | VernacRegister of lident * register_kind | VernacComments of comment list diff --git a/parsing/g_vernac.ml4 b/parsing/g_vernac.ml4 index 4fd316119..011565d86 100644 --- a/parsing/g_vernac.ml4 +++ b/parsing/g_vernac.ml4 @@ -40,7 +40,6 @@ let def_body = Gram.entry_create "vernac:def_body" let decl_notation = Gram.entry_create "vernac:decl_notation" 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_expr = Gram.entry_create "vernac:section_subset_expr" @@ -53,7 +52,7 @@ let make_bullet s = | _ -> assert false GEXTEND Gram - GLOBAL: vernac gallina_ext noedit_mode subprf subgoal_command; + GLOBAL: vernac gallina_ext noedit_mode subprf; vernac: FIRST [ [ IDENT "Time"; c = located_vernac -> VernacTime c | IDENT "Redirect"; s = ne_string; c = located_vernac -> VernacRedirect (s, c) @@ -92,7 +91,7 @@ GEXTEND Gram [ [ prfcom = command_entry -> prfcom ] ] ; noedit_mode: - [ [ c = subgoal_command -> c None] ] + [ [ c = query_command -> c None] ] ; subprf: @@ -102,15 +101,6 @@ GEXTEND Gram ] ] ; - subgoal_command: - [ [ c = query_command; "." -> - begin function - | Some (SelectNth g) -> c (Some g) - | None -> c None - | _ -> - VernacError (UserError (None,str"Typing and evaluation commands, cannot be used with the \"all:\" selector.")) - end ] ] - ; located_vernac: [ [ v = vernac -> !@loc, v ] ] ; @@ -918,29 +908,30 @@ GEXTEND Gram VernacRemoveOption ([table], v) ]] ; query_command: (* TODO: rapprocher Eval et Check *) - [ [ IDENT "Eval"; r = red_expr; "in"; c = lconstr -> + [ [ IDENT "Eval"; r = red_expr; "in"; c = lconstr; "." -> fun g -> VernacCheckMayEval (Some r, g, c) - | IDENT "Compute"; c = lconstr -> + | IDENT "Compute"; c = lconstr; "." -> fun g -> VernacCheckMayEval (Some (Genredexpr.CbvVm None), g, c) - | IDENT "Check"; c = lconstr -> + | IDENT "Check"; c = lconstr; "." -> fun g -> VernacCheckMayEval (None, g, c) (* Searching the environment *) - | IDENT "About"; qid = smart_global -> + | IDENT "About"; qid = smart_global; "." -> fun g -> VernacPrint (PrintAbout (qid,g)) - | IDENT "SearchHead"; c = constr_pattern; l = in_or_out_modules -> + | IDENT "SearchHead"; c = constr_pattern; l = in_or_out_modules; "." -> fun g -> VernacSearch (SearchHead c,g, l) - | IDENT "SearchPattern"; c = constr_pattern; l = in_or_out_modules -> + | IDENT "SearchPattern"; c = constr_pattern; l = in_or_out_modules; "." -> fun g -> VernacSearch (SearchPattern c,g, l) - | IDENT "SearchRewrite"; c = constr_pattern; l = in_or_out_modules -> + | IDENT "SearchRewrite"; c = constr_pattern; l = in_or_out_modules; "." -> fun g -> VernacSearch (SearchRewrite c,g, l) - | IDENT "Search"; s = searchabout_query; l = searchabout_queries -> + | IDENT "Search"; s = searchabout_query; l = searchabout_queries; "." -> let (sl,m) = l in fun g -> VernacSearch (SearchAbout (s::sl),g, m) (* compatibility: SearchAbout *) - | IDENT "SearchAbout"; s = searchabout_query; l = searchabout_queries -> + | IDENT "SearchAbout"; s = searchabout_query; l = searchabout_queries; "." -> fun g -> let (sl,m) = l in VernacSearch (SearchAbout (s::sl),g, m) (* compatibility: SearchAbout with "[ ... ]" *) | IDENT "SearchAbout"; "["; sl = LIST1 searchabout_query; "]"; - l = in_or_out_modules -> fun g -> VernacSearch (SearchAbout sl,g, l) + l = in_or_out_modules; "." -> + fun g -> VernacSearch (SearchAbout sl,g, l) ] ] ; printable: diff --git a/plugins/ltac/g_ltac.ml4 b/plugins/ltac/g_ltac.ml4 index ece0adb07..ca5d198c2 100644 --- a/plugins/ltac/g_ltac.ml4 +++ b/plugins/ltac/g_ltac.ml4 @@ -335,7 +335,7 @@ GEXTEND Gram | IDENT "all"; ":" -> SelectAll ] ] ; tactic_mode: - [ [ g = OPT toplevel_selector; tac = G_vernac.subgoal_command -> tac g ] ] + [ [ g = OPT toplevel_selector; tac = G_vernac.query_command -> tac g ] ] ; command: [ [ IDENT "Proof"; "with"; ta = Pltac.tactic; diff --git a/printing/ppvernac.ml b/printing/ppvernac.ml index cfc2e48d1..5af0e1d9b 100644 --- a/printing/ppvernac.ml +++ b/printing/ppvernac.ml @@ -107,7 +107,7 @@ open Decl_kinds | SearchString (s,sc) -> qs s ++ pr_opt (fun sc -> str "%" ++ str sc) sc let pr_search a gopt b pr_p = - pr_opt (fun g -> int g ++ str ":"++ spc()) gopt + pr_opt (fun g -> Proof_global.pr_goal_selector g ++ str ":"++ spc()) gopt ++ match a with | SearchHead c -> keyword "SearchHead" ++ spc() ++ pr_p c ++ pr_in_out_modules b @@ -497,7 +497,7 @@ open Decl_kinds | PrintVisibility s -> keyword "Print Visibility" ++ pr_opt str s | PrintAbout (qid,gopt) -> - pr_opt (fun g -> int g ++ str ":"++ spc()) gopt + pr_opt (fun g -> Proof_global.pr_goal_selector g ++ str ":"++ spc()) gopt ++ keyword "About" ++ spc() ++ pr_smart_global qid | PrintImplicit qid -> keyword "Print Implicit" ++ spc() ++ pr_smart_global qid @@ -619,8 +619,6 @@ open Decl_kinds return (keyword "Timeout " ++ int n ++ spc() ++ pr_vernac_body v) | VernacFail v -> return (keyword "Fail" ++ spc() ++ pr_vernac_body v) - | VernacError _ -> - return (keyword "No-parsing-rule for VernacError") (* Syntax *) | VernacOpenCloseScope (_,(opening,sc)) -> @@ -1140,7 +1138,8 @@ open Decl_kinds spc() ++ keyword "in" ++ spc () ++ pr_lconstr c) | None -> hov 2 (keyword "Check" ++ spc() ++ pr_lconstr c) in - let pr_i = match io with None -> mt () | Some i -> int i ++ str ": " in + let pr_i = match io with None -> mt () + | Some i -> Proof_global.pr_goal_selector i ++ str ": " in return (pr_i ++ pr_mayeval r c) | VernacGlobalCheck c -> return (hov 2 (keyword "Type" ++ pr_constrarg c)) diff --git a/proofs/proof_global.ml b/proofs/proof_global.ml index e4cba6f07..61b776f24 100644 --- a/proofs/proof_global.ml +++ b/proofs/proof_global.ml @@ -671,16 +671,18 @@ let _ = let default_goal_selector = ref (Vernacexpr.SelectNth 1) let get_default_goal_selector () = !default_goal_selector -let print_range_selector (i, j) = - if i = j then string_of_int i - else string_of_int i ^ "-" ^ string_of_int j - -let print_goal_selector = function - | Vernacexpr.SelectAll -> "all" - | Vernacexpr.SelectNth i -> string_of_int i - | Vernacexpr.SelectList l -> "[" ^ - String.concat ", " (List.map print_range_selector l) ^ "]" - | Vernacexpr.SelectId id -> Id.to_string id +let pr_range_selector (i, j) = + if i = j then int i + else int i ++ str "-" ++ int j + +let pr_goal_selector = function + | Vernacexpr.SelectAll -> str "all" + | Vernacexpr.SelectNth i -> int i + | Vernacexpr.SelectList l -> + str "[" + ++ prlist_with_sep pr_comma pr_range_selector l + ++ str "]" + | Vernacexpr.SelectId id -> Id.print id let parse_goal_selector = function | "all" -> Vernacexpr.SelectAll @@ -699,7 +701,10 @@ let _ = optdepr = false; optname = "default goal selector" ; optkey = ["Default";"Goal";"Selector"] ; - optread = begin fun () -> print_goal_selector !default_goal_selector end; + optread = begin fun () -> + string_of_ppcmds + (pr_goal_selector !default_goal_selector) + end; optwrite = begin fun n -> default_goal_selector := parse_goal_selector n end diff --git a/proofs/proof_global.mli b/proofs/proof_global.mli index 3b2cc6b23..6bb6f5e2c 100644 --- a/proofs/proof_global.mli +++ b/proofs/proof_global.mli @@ -198,6 +198,7 @@ end (* *) (**********************************************************) +val pr_goal_selector : Vernacexpr.goal_selector -> Pp.std_ppcmds val get_default_goal_selector : unit -> Vernacexpr.goal_selector module V82 : sig diff --git a/stm/vernac_classifier.ml b/stm/vernac_classifier.ml index fb6adaec5..c4f392f20 100644 --- a/stm/vernac_classifier.ml +++ b/stm/vernac_classifier.ml @@ -202,8 +202,7 @@ let rec classify_vernac e = (* What are these? *) | VernacToplevelControl _ | VernacRestoreState _ - | VernacWriteState _ - | VernacError _ -> VtUnknown, VtNow + | VernacWriteState _ -> VtUnknown, VtNow (* Plugins should classify their commands *) | VernacExtend (s,l) -> try List.assoc s !classifiers l () diff --git a/test-suite/output/Search.out b/test-suite/output/Search.out index 81fda176e..7446c17d9 100644 --- a/test-suite/output/Search.out +++ b/test-suite/output/Search.out @@ -98,6 +98,14 @@ h: n <> newdef n h': newdef n <> n h: n <> newdef n h: n <> newdef n +h: n <> newdef n +h': newdef n <> n +The command has indeed failed with message: +No such goal. +The command has indeed failed with message: +Query commands only support the single numbered goal selector. +The command has indeed failed with message: +Query commands only support the single numbered goal selector. h: P n h': ~ P n h: P n diff --git a/test-suite/output/Search.v b/test-suite/output/Search.v index 2a0f0b407..82096f29b 100644 --- a/test-suite/output/Search.v +++ b/test-suite/output/Search.v @@ -10,11 +10,19 @@ Search (@eq _ _ _) true -false "prop" -"intro". (* andb_prop *) Definition newdef := fun x:nat => x. Goal forall n:nat, n <> newdef n -> newdef n <> n -> False. - intros n h h'. + cut False. + intros _ n h h'. Search n. (* search hypothesis *) Search newdef. (* search hypothesis *) Search ( _ <> newdef _). (* search hypothesis, pattern *) Search ( _ <> newdef _) -"h'". (* search hypothesis, pattern *) + + 1:Search newdef. + 2:Search newdef. + + Fail 3:Search newdef. + Fail 1-2:Search newdef. + Fail all:Search newdef. Abort. Goal forall n (P:nat -> Prop), P n -> ~P n -> False. diff --git a/vernac/vernacentries.ml b/vernac/vernacentries.ml index 92b1a5956..52136a70e 100644 --- a/vernac/vernacentries.ml +++ b/vernac/vernacentries.ml @@ -1533,7 +1533,14 @@ let get_current_context_of_args = function | Some n -> get_goal_context n | None -> get_current_context () -let vernac_check_may_eval redexp glopt rc = +let query_command_selector ~loc = function + | None -> None + | Some (SelectNth n) -> Some n + | _ -> user_err ~loc ~hdr:"query_command_selector" + (str "Query commands only support the single numbered goal selector.") + +let vernac_check_may_eval ~loc redexp glopt rc = + let glopt = query_command_selector ~loc glopt in let (sigma, env) = get_current_context_of_args glopt in let sigma', c = interp_open_constr env sigma rc in let c = EConstr.Unsafe.to_constr c in @@ -1595,9 +1602,10 @@ exception NoHyp (* Printing "About" information of a hypothesis of the current goal. We only print the type and a small statement to this comes from the goal. Precondition: there must be at least one current goal. *) -let print_about_hyp_globs ref_or_by_not glnumopt = +let print_about_hyp_globs ~loc ref_or_by_not glopt = let open Context.Named.Declaration in try + let glnumopt = query_command_selector ~loc glopt in let gl,id = match glnumopt,ref_or_by_not with | None,AN (Ident (_loc,id)) -> (* goal number not given, catch any failure *) @@ -1605,8 +1613,8 @@ let print_about_hyp_globs ref_or_by_not glnumopt = | Some n,AN (Ident (_loc,id)) -> (* goal number given, catch if wong *) (try get_nth_goal n,id with - Failure _ -> user_err ~hdr:"print_about_hyp_globs" - (str "No such goal: " ++ int n ++ str ".")) + Failure _ -> user_err ~loc ~hdr:"print_about_hyp_globs" + (str "No such goal: " ++ int n ++ str ".")) | _ , _ -> raise NoHyp in let hyps = pf_hyps gl in let decl = Context.Named.lookup id hyps in @@ -1619,7 +1627,7 @@ let print_about_hyp_globs ref_or_by_not glnumopt = | NoHyp | Not_found -> print_about ref_or_by_not -let vernac_print = let open Feedback in function +let vernac_print ~loc = let open Feedback in function | PrintTables -> msg_notice (print_tables ()) | PrintFullContext-> msg_notice (print_full_context_typ ()) | PrintSectionContext qid -> msg_notice (print_sec_context_typ qid) @@ -1664,7 +1672,7 @@ let vernac_print = let open Feedback in function | PrintVisibility s -> msg_notice (Notation.pr_visibility (Constrextern.without_symbols pr_lglob_constr) s) | PrintAbout (ref_or_by_not,glnumopt) -> - msg_notice (print_about_hyp_globs ref_or_by_not glnumopt) + msg_notice (print_about_hyp_globs ~loc ref_or_by_not glnumopt) | PrintImplicit qid -> dump_global qid; msg_notice (print_impargs qid) | PrintAssumptions (o,t,r) -> @@ -1729,7 +1737,8 @@ let _ = optread = (fun () -> !search_output_name_only); optwrite = (:=) search_output_name_only } -let vernac_search s gopt r = +let vernac_search ~loc s gopt r = + let gopt = query_command_selector ~loc gopt in let r = interp_search_restriction r in let env,gopt = match gopt with | None -> @@ -1935,9 +1944,6 @@ let interp ?proof ~loc locality poly c = | VernacBack _ -> anomaly (str "VernacBack not handled by Stm") | VernacBackTo _ -> anomaly (str "VernacBackTo not handled by Stm") - (* Horrible Hack that should die. *) - | VernacError e -> raise e - (* This one is possible to handle here *) | VernacAbort id -> CErrors.user_err (str "Abort cannot be used through the Load command") @@ -2039,11 +2045,11 @@ let interp ?proof ~loc locality poly c = | VernacAddOption (key,v) -> vernac_add_option key v | VernacMemOption (key,v) -> vernac_mem_option key v | VernacPrintOption key -> vernac_print_option key - | VernacCheckMayEval (r,g,c) -> vernac_check_may_eval r g c + | VernacCheckMayEval (r,g,c) -> vernac_check_may_eval ~loc r g c | VernacDeclareReduction (s,r) -> vernac_declare_reduction locality s r | VernacGlobalCheck c -> vernac_global_check c - | VernacPrint p -> vernac_print p - | VernacSearch (s,g,r) -> vernac_search s g r + | VernacPrint p -> vernac_print ~loc p + | VernacSearch (s,g,r) -> vernac_search ~loc s g r | VernacLocate l -> vernac_locate l | VernacRegister (id, r) -> vernac_register id r | VernacComments l -> if_verbose Feedback.msg_info (str "Comments ok\n") |