diff options
40 files changed, 237 insertions, 190 deletions
diff --git a/clib/exninfo.ml b/clib/exninfo.ml index ee998c2f17..34a4555a9a 100644 --- a/clib/exninfo.ml +++ b/clib/exninfo.ml @@ -81,16 +81,6 @@ let iraise (e,i) = | Some bt -> Printexc.raise_with_backtrace e bt -let raise ?info e = match info with -| None -> - let () = Mutex.lock lock in - let id = Thread.id (Thread.self ()) in - let () = current := remove_assoc id !current in - let () = Mutex.unlock lock in - raise e -| Some i -> - iraise (e,i) - let find_and_remove () = let () = Mutex.lock lock in let id = Thread.id (Thread.self ()) in diff --git a/clib/exninfo.mli b/clib/exninfo.mli index 36cc44cf82..725cd82809 100644 --- a/clib/exninfo.mli +++ b/clib/exninfo.mli @@ -79,6 +79,3 @@ val capture : exn -> iexn val iraise : iexn -> 'a (** Raise the given enriched exception. *) - -val raise : ?info:info -> exn -> 'a -(** Raise the given exception with additional information. *) diff --git a/configure.ml b/configure.ml index 89d9ed9d2a..6e15cdbe4e 100644 --- a/configure.ml +++ b/configure.ml @@ -923,7 +923,7 @@ let datadir,datadirsuffix = let (_,_,d,s) = select "DATADIR" in d,s (** * CC runtime flags *) -let cflags_dflt = "-Wall -Wno-unused -g -O2 -fexcess-precision=standard" +let cflags_dflt = "-Wall -Wno-unused -g -O2 -std=c99 -fasm" let cflags_sse2 = "-msse2 -mfpmath=sse" diff --git a/coqpp/coqpp_main.ml b/coqpp/coqpp_main.ml index 72b7cb2f84..e723d4ea1b 100644 --- a/coqpp/coqpp_main.ml +++ b/coqpp/coqpp_main.ml @@ -266,7 +266,7 @@ let print_rule fmt r = let print_entry fmt e = let print_position_opt fmt pos = print_opt fmt print_position pos in let print_rules fmt rules = print_list fmt print_rule rules in - fprintf fmt "let () =@ @[Pcoq.grammar_extend@ %s@ None@ @[(%a, %a)@]@]@ in@ " + fprintf fmt "let () =@ @[Pcoq.grammar_extend@ %s@ @[(%a, %a)@]@]@ in@ " e.gentry_name print_position_opt e.gentry_pos print_rules e.gentry_rules let print_ast fmt ext = diff --git a/dev/ci/ci-coquelicot.sh b/dev/ci/ci-coquelicot.sh index 6cb8dad604..ffe92dcecf 100755 --- a/dev/ci/ci-coquelicot.sh +++ b/dev/ci/ci-coquelicot.sh @@ -7,4 +7,4 @@ install_ssreflect git_download coquelicot -( cd "${CI_BUILD_DIR}/coquelicot" && ./autogen.sh && ./configure && ./remake "-j${NJOBS}" ) +( cd "${CI_BUILD_DIR}/coquelicot" && autoreconf -i -s && ./configure && ./remake "-j${NJOBS}" ) diff --git a/dev/doc/changes.md b/dev/doc/changes.md index 42dd2dd052..d5938713d6 100644 --- a/dev/doc/changes.md +++ b/dev/doc/changes.md @@ -15,6 +15,12 @@ Exception handling: `Exninfo.capture` and `iraise` when re-raising inside an exception handler. +- Registration of exception printers now follows more closely OCaml's + API, thus: + + + printers are of type `exn -> Pp.t option` [`None` == not handled] + + it is forbidden for exception printers to raise. + Printers: - Functions such as Printer.pr_lconstr_goal_style_env have been diff --git a/doc/sphinx/proof-engine/ltac2.rst b/doc/sphinx/proof-engine/ltac2.rst index b722b1af74..9362a7729e 100644 --- a/doc/sphinx/proof-engine/ltac2.rst +++ b/doc/sphinx/proof-engine/ltac2.rst @@ -3,10 +3,6 @@ Ltac2 ===== -.. coqtop:: none - - From Ltac2 Require Import Ltac2. - The Ltac tactic language is probably one of the ingredients of the success of Coq, yet it is at the same time its Achilles' heel. Indeed, Ltac: @@ -88,6 +84,12 @@ which allows to ensure that Ltac2 satisfies the same equations as a generic ML with unspecified effects would do, e.g. function reduction is substitution by a value. +To import Ltac2, use the following command: + +.. coqtop:: in + + From Ltac2 Require Import Ltac2. + Type Syntax ~~~~~~~~~~~ diff --git a/engine/logic_monad.ml b/engine/logic_monad.ml index 3c383b2e00..1caf2c2722 100644 --- a/engine/logic_monad.ml +++ b/engine/logic_monad.ml @@ -38,9 +38,9 @@ exception Tac_Timeout exception TacticFailure of exn let _ = CErrors.register_handler begin function - | Exception e -> CErrors.print e - | TacticFailure e -> CErrors.print e - | _ -> raise CErrors.Unhandled + | Exception e -> Some (CErrors.print e) + | TacticFailure e -> Some (CErrors.print e) + | _ -> None end (** {6 Non-logical layer} *) @@ -83,7 +83,7 @@ struct (** [Pervasives.raise]. Except that exceptions are wrapped with {!Exception}. *) - let raise ?info = fun e -> (); fun () -> Exninfo.raise ?info (Exception e) + let raise (e, info) () = Exninfo.iraise (Exception e, info) (** [try ... with ...] but restricted to {!Exception}. *) let catch = fun s h -> (); @@ -93,7 +93,8 @@ struct h (e, info) () let read_line = fun () -> try read_line () with e -> - let (e, info) = CErrors.push e in raise ~info e () + let (e, info) = CErrors.push e in + raise (e, info) () let print_char = fun c -> (); fun () -> print_char c diff --git a/engine/logic_monad.mli b/engine/logic_monad.mli index 75920455ce..5002d24af0 100644 --- a/engine/logic_monad.mli +++ b/engine/logic_monad.mli @@ -70,7 +70,7 @@ module NonLogical : sig (** [Pervasives.raise]. Except that exceptions are wrapped with {!Exception}. *) - val raise : ?info:Exninfo.info -> exn -> 'a t + val raise : Exninfo.iexn -> 'a t (** [try ... with ...] but restricted to {!Exception}. *) val catch : 'a t -> (Exninfo.iexn -> 'a t) -> 'a t diff --git a/engine/proofview.ml b/engine/proofview.ml index b0ea75ac60..a26ce71141 100644 --- a/engine/proofview.ml +++ b/engine/proofview.ml @@ -303,8 +303,8 @@ let tclONCE = Proof.once exception MoreThanOneSuccess let _ = CErrors.register_handler begin function | MoreThanOneSuccess -> - Pp.str "This tactic has more than one success." - | _ -> raise CErrors.Unhandled + Some (Pp.str "This tactic has more than one success.") + | _ -> None end (** [tclEXACTLY_ONCE e t] succeeds as [t] if [t] has exactly one @@ -348,8 +348,8 @@ exception NoSuchGoals of int let _ = CErrors.register_handler begin function | NoSuchGoals n -> - str "No such " ++ str (String.plural n "goal") ++ str "." - | _ -> raise CErrors.Unhandled + Some (str "No such " ++ str (String.plural n "goal") ++ str ".") + | _ -> None end (** [tclFOCUS ?nosuchgoal i j t] applies [t] in a context where @@ -421,9 +421,10 @@ exception SizeMismatch of int*int let _ = CErrors.register_handler begin function | SizeMismatch (i,j) -> let open Pp in - str"Incorrect number of goals" ++ spc() ++ - str"(expected "++int i++str(String.plural i " tactic") ++ str", was given "++ int j++str")." - | _ -> raise CErrors.Unhandled + Some ( + str"Incorrect number of goals" ++ spc() ++ + str"(expected "++int i++str(String.plural i " tactic") ++ str", was given "++ int j++str").") + | _ -> None end (** A variant of [Monad.List.iter] where we iter over the focused list @@ -908,8 +909,8 @@ let tclPROGRESS t = let _ = CErrors.register_handler begin function | Logic_monad.Tac_Timeout -> - Pp.str "[Proofview.tclTIMEOUT] Tactic timeout!" - | _ -> raise CErrors.Unhandled + Some (Pp.str "[Proofview.tclTIMEOUT] Tactic timeout!") + | _ -> None end let tclTIMEOUT n t = @@ -937,7 +938,7 @@ let tclTIMEOUT n t = return (Util.Inr (Logic_monad.Tac_Timeout, info)) | Logic_monad.TacticFailure e -> return (Util.Inr (e, info)) - | e -> Logic_monad.NonLogical.raise ~info e + | e -> Logic_monad.NonLogical.raise (e, info) end end >>= function | Util.Inl (res,s,m,i) -> diff --git a/ide/idetop.ml b/ide/idetop.ml index ae2301a0a7..60036ef876 100644 --- a/ide/idetop.ml +++ b/ide/idetop.ml @@ -70,7 +70,7 @@ let ide_cmd_checks ~last_valid { CAst.loc; v } = with e -> let (e, info) = CErrors.push e in let info = Stateid.add info ~valid:last_valid Stateid.dummy in - Exninfo.raise ~info e + Exninfo.iraise (e, info) in if is_debug v.expr then user_error "Debug mode not available in the IDE" diff --git a/kernel/term_typing.ml b/kernel/term_typing.ml index faa601e277..2ecd4880f7 100644 --- a/kernel/term_typing.ml +++ b/kernel/term_typing.ml @@ -61,7 +61,7 @@ let feedback_completion_typecheck = Feedback.feedback ~id:state_id Feedback.Complete) type typing_context = -| MonoTyCtx of Environ.env * unsafe_type_judgment * Univ.ContextSet.t * Id.Set.t * Stateid.t option +| MonoTyCtx of Environ.env * unsafe_type_judgment * Id.Set.t * Stateid.t option | PolyTyCtx of Environ.env * unsafe_type_judgment * Univ.universe_level_subst * Univ.AUContext.t * Id.Set.t * Stateid.t option let infer_declaration env (dcl : constant_entry) = @@ -155,7 +155,7 @@ let infer_opaque env = function let env = push_context_set ~strict:true univs env in let { opaque_entry_feedback = feedback_id; _ } = c in let tyj = Typeops.infer_type env typ in - let context = MonoTyCtx (env, tyj, univs, c.opaque_entry_secctx, feedback_id) in + let context = MonoTyCtx (env, tyj, c.opaque_entry_secctx, feedback_id) in let def = OpaqueDef () in { Cooking.cook_body = def; @@ -257,10 +257,8 @@ let build_constant_declaration env result = const_typing_flags = Environ.typing_flags env } let check_delayed (type a) (handle : a effect_handler) tyenv (body : a proof_output) = match tyenv with -| MonoTyCtx (env, tyj, univs, declared, feedback_id) -> +| MonoTyCtx (env, tyj, declared, feedback_id) -> let ((body, uctx), side_eff) = body in - (* don't redeclare universes which are declared for the type *) - let uctx = Univ.ContextSet.diff uctx univs in let (body, uctx', valid_signatures) = handle env body side_eff in let uctx = Univ.ContextSet.union uctx uctx' in let env = push_context_set uctx env in diff --git a/lib/cErrors.ml b/lib/cErrors.ml index 9f496f5845..323dc8c1a4 100644 --- a/lib/cErrors.ml +++ b/lib/cErrors.ml @@ -66,12 +66,10 @@ let print_anomaly askreport e = let handle_stack = ref [] -exception Unhandled - let register_handler h = handle_stack := h::!handle_stack let is_handled e = - let is_handled_by h = (try let _ = h e in true with | Unhandled -> false) in + let is_handled_by h = Option.has_some (h e) in List.exists is_handled_by !handle_stack let is_anomaly = function @@ -88,30 +86,31 @@ let register_additional_error_info (f : Exninfo.info -> (Pp.t option Loc.located all the handlers of a list, and finally a [bottom] handler if all others have failed *) -let rec print_gen ~anomaly ~extra_msg stk (e, info) = +let rec print_gen ~anomaly ~extra_msg stk e = match stk with | [] -> print_anomaly anomaly e | h::stk' -> - try - let err_msg = h e in + match h e with + | Some err_msg -> Option.cata (fun msg -> msg ++ err_msg) err_msg extra_msg - with - | Unhandled -> print_gen ~anomaly ~extra_msg stk' (e,info) - | any -> print_gen ~anomaly ~extra_msg stk' (any,info) + | None -> + print_gen ~anomaly ~extra_msg stk' e let print_gen ~anomaly (e, info) = let extra_info = try CList.find_map (fun f -> Some (f info)) !additional_error_info_handler with Not_found -> None in - let extra_msg, info = match extra_info with - | None -> None, info - | Some (loc, msg) -> - let info = Option.cata (fun l -> Loc.add_loc info l) info loc in - msg, info + let extra_msg = match extra_info with + | None -> None + | Some (loc, msg) -> msg in - print_gen ~anomaly ~extra_msg !handle_stack (e,info) + try + print_gen ~anomaly ~extra_msg !handle_stack e + with exn -> + (* exception in error printer *) + str "<in exception printer>" ++ fnl () ++ print_anomaly anomaly exn (** The standard exception printer *) let iprint (e, info) = @@ -130,8 +129,8 @@ let print_no_report e = iprint_no_report (e, Exninfo.info e) let _ = register_handler begin function | UserError(s, pps) -> - where s ++ pps - | _ -> raise Unhandled + Some (where s ++ pps) + | _ -> None end (** Critical exceptions should not be caught and ignored by mistake diff --git a/lib/cErrors.mli b/lib/cErrors.mli index 02eaf6bd0b..1660a00244 100644 --- a/lib/cErrors.mli +++ b/lib/cErrors.mli @@ -46,19 +46,14 @@ exception Timeout recent first) until a handle deals with it. Handles signal that they don't deal with some exception - by raising [Unhandled]. + by returning None. Raising any other exception is + forbidden and will result in an anomaly. - Handles can raise exceptions themselves, in which - case, the exception is passed to the handles which - were registered before. - - The exception that are considered anomalies should not be + Exceptions that are considered anomalies should not be handled by registered handlers. *) -exception Unhandled - -val register_handler : (exn -> Pp.t) -> unit +val register_handler : (exn -> Pp.t option) -> unit (** The standard exception printer *) val print : exn -> Pp.t diff --git a/lib/future.ml b/lib/future.ml index 5cccd2038d..ddf841b7fc 100644 --- a/lib/future.ml +++ b/lib/future.ml @@ -28,9 +28,9 @@ exception NotReady of string exception NotHere of string let _ = CErrors.register_handler (function - | NotReady name -> !not_ready_msg name - | NotHere name -> !not_here_msg name - | _ -> raise CErrors.Unhandled) + | NotReady name -> Some (!not_ready_msg name) + | NotHere name -> Some (!not_here_msg name) + | _ -> None) type fix_exn = Exninfo.iexn -> Exninfo.iexn let id x = x diff --git a/parsing/pcoq.ml b/parsing/pcoq.ml index 26afdcb9d5..92c3b7c6e8 100644 --- a/parsing/pcoq.ml +++ b/parsing/pcoq.ml @@ -212,7 +212,8 @@ type 'a extend_statement = 'a single_extend_statement list type extend_rule = -| ExtendRule : 'a G.Entry.e * gram_reinit option * 'a extend_statement -> extend_rule +| ExtendRule : 'a Entry.t * 'a extend_statement -> extend_rule +| ExtendRuleReinit : 'a Entry.t * gram_reinit * 'a extend_statement -> extend_rule module EntryCommand = Dyn.Make () module EntryData = struct type _ t = Ex : 'b G.Entry.e String.Map.t -> ('a * 'b) t end @@ -231,33 +232,39 @@ let camlp5_entries = ref EntryDataMap.empty (** Deletion *) -let grammar_delete e reinit (pos,rls) = +let grammar_delete e (pos,rls) = List.iter (fun (n,ass,lev) -> List.iter (fun (AnyProduction (pil,_)) -> G.safe_delete_rule e pil) (List.rev lev)) - (List.rev rls); - match reinit with - | Some (a,ext) -> - let lev = match pos with + (List.rev rls) + +let grammar_delete_reinit e reinit (pos, rls) = + grammar_delete e (pos, rls); + let a, ext = reinit in + let lev = match pos with | Some (Gramext.Level n) -> n | _ -> assert false - in - let warning msg = Feedback.msg_warning Pp.(str msg) in - (G.safe_extend ~warning:(Some warning) e) (Some ext) [Some lev,Some a,[]] - | None -> () + in + let warning msg = Feedback.msg_warning Pp.(str msg) in + (G.safe_extend ~warning:(Some warning) e) (Some ext) [Some lev,Some a,[]] (** Extension *) -let grammar_extend e reinit ext = +let grammar_extend e ext = let ext = of_coq_extend_statement ext in - let undo () = grammar_delete e reinit ext in + let undo () = grammar_delete e ext in let pos, ext = fix_extend_statement ext in let redo () = G.safe_extend ~warning:None e pos ext in camlp5_state := ByEXTEND (undo, redo) :: !camlp5_state; redo () -let grammar_extend_sync e reinit ext = - camlp5_state := ByGrammar (ExtendRule (e, reinit, ext)) :: !camlp5_state; +let grammar_extend_sync e ext = + camlp5_state := ByGrammar (ExtendRule (e, ext)) :: !camlp5_state; + let pos, ext = fix_extend_statement (of_coq_extend_statement ext) in + G.safe_extend ~warning:None e pos ext + +let grammar_extend_sync_reinit e reinit ext = + camlp5_state := ByGrammar (ExtendRuleReinit (e, reinit, ext)) :: !camlp5_state; let pos, ext = fix_extend_statement (of_coq_extend_statement ext) in G.safe_extend ~warning:None e pos ext @@ -278,8 +285,12 @@ let rec remove_grammars n = if n>0 then match !camlp5_state with | [] -> anomaly ~label:"Pcoq.remove_grammars" (Pp.str "too many rules to remove.") - | ByGrammar (ExtendRule (g, reinit, ext)) :: t -> - grammar_delete g reinit (of_coq_extend_statement ext); + | ByGrammar (ExtendRuleReinit (g, reinit, ext)) :: t -> + grammar_delete_reinit g reinit (of_coq_extend_statement ext); + camlp5_state := t; + remove_grammars (n-1) + | ByGrammar (ExtendRule (g, ext)) :: t -> + grammar_delete g (of_coq_extend_statement ext); camlp5_state := t; remove_grammars (n-1) | ByEXTEND (undo,redo)::t -> @@ -507,6 +518,12 @@ let create_entry_command name (interp : ('a, 'b) entry_extension) : ('a, 'b) ent let () = entry_interp := EntryInterpMap.add obj (EntryInterp.Ex interp) !entry_interp in obj +let iter_extend_sync = function + | ExtendRule (e, ext) -> + grammar_extend_sync e ext + | ExtendRuleReinit (e, reinit, ext) -> + grammar_extend_sync_reinit e reinit ext + let extend_grammar_command tag g = let modify = GrammarInterpMap.find tag !grammar_interp in let grammar_state = match !grammar_stack with @@ -514,8 +531,7 @@ let extend_grammar_command tag g = | (_, st) :: _ -> st in let (rules, st) = modify g grammar_state in - let iter (ExtendRule (e, reinit, ext)) = grammar_extend_sync e reinit ext in - let () = List.iter iter rules in + let () = List.iter iter_extend_sync rules in let nb = List.length rules in grammar_stack := (GramExt (nb, GrammarCommand.Dyn (tag, g)), st) :: !grammar_stack diff --git a/parsing/pcoq.mli b/parsing/pcoq.mli index 404fbdb4fd..f2fc007a7b 100644 --- a/parsing/pcoq.mli +++ b/parsing/pcoq.mli @@ -225,7 +225,7 @@ type 'a extend_statement = Gramlib.Gramext.position option * 'a single_extend_statement list -val grammar_extend : 'a Entry.t -> gram_reinit option -> 'a extend_statement -> unit +val grammar_extend : 'a Entry.t -> 'a extend_statement -> unit (** Extend the grammar of Coq, without synchronizing it with the backtracking mechanism. This means that grammar extensions defined this way will survive an undo. *) @@ -242,7 +242,8 @@ type 'a grammar_command marshallable. *) type extend_rule = -| ExtendRule : 'a Entry.t * gram_reinit option * 'a extend_statement -> extend_rule +| ExtendRule : 'a Entry.t * 'a extend_statement -> extend_rule +| ExtendRuleReinit : 'a Entry.t * gram_reinit * 'a extend_statement -> extend_rule type 'a grammar_extension = 'a -> GramState.t -> extend_rule list * GramState.t (** Grammar extension entry point. Given some ['a] and a current grammar state, diff --git a/plugins/ltac/tacentries.ml b/plugins/ltac/tacentries.ml index 13a2f3b8c0..8b4520947b 100644 --- a/plugins/ltac/tacentries.ml +++ b/plugins/ltac/tacentries.ml @@ -191,7 +191,7 @@ let add_tactic_entry (kn, ml, tg) state = in let prods = List.map map tg.tacgram_prods in let rules = make_rule mkact prods in - let r = ExtendRule (entry, None, (pos, [(None, None, [rules])])) in + let r = ExtendRule (entry, (pos, [(None, None, [rules])])) in ([r], state) let tactic_grammar = @@ -415,7 +415,7 @@ let create_ltac_quotation name cast (e, l) = in let action _ v _ _ _ loc = cast (Some loc, v) in let gram = (level, assoc, [Rule (rule, action)]) in - Pcoq.grammar_extend Pltac.tactic_arg None (None, [gram]) + Pcoq.grammar_extend Pltac.tactic_arg (None, [gram]) (** Command *) @@ -759,7 +759,7 @@ let argument_extend (type a b c) ~name (arg : (a, b, c) tactic_argument) = e | Vernacextend.Arg_rules rules -> let e = Pcoq.create_generic_entry Pcoq.utactic name (Genarg.rawwit wit) in - let () = Pcoq.grammar_extend e None (None, [(None, None, rules)]) in + let () = Pcoq.grammar_extend e (None, [(None, None, rules)]) in e in let (rpr, gpr, tpr) = arg.arg_printer in diff --git a/plugins/ltac/tactic_debug.ml b/plugins/ltac/tactic_debug.ml index 0e9465839a..392f9b2ffd 100644 --- a/plugins/ltac/tactic_debug.ml +++ b/plugins/ltac/tactic_debug.ml @@ -107,13 +107,29 @@ let db_initialize = let int_of_string s = try Proofview.NonLogical.return (int_of_string s) - with e -> Proofview.NonLogical.raise e + with e -> + let e = Exninfo.capture e in + Proofview.NonLogical.raise e let string_get s i = try Proofview.NonLogical.return (String.get s i) - with e -> Proofview.NonLogical.raise e + with e -> + let e = Exninfo.capture e in + Proofview.NonLogical.raise e + +let check_positive n = + try + if n < 0 then + raise (Invalid_argument "number must be positive") + else + Proofview.NonLogical.return () + with e -> + let e = Exninfo.capture e in + Proofview.NonLogical.raise e -let run_invalid_arg () = Proofview.NonLogical.raise (Invalid_argument "run_com") +let run_invalid_arg () = + let info = Exninfo.null in + Proofview.NonLogical.raise (Invalid_argument "run_com", info) (* Gives the number of steps or next breakpoint of a run command *) let run_com inst = @@ -125,7 +141,7 @@ let run_com inst = let s = String.sub inst i (String.length inst - i) in if inst.[0] >= '0' && inst.[0] <= '9' then int_of_string s >>= fun num -> - (if num<0 then run_invalid_arg () else return ()) >> + check_positive num >> (skip:=num) >> (skipped:=0) else breakpoint:=Some (possibly_unquote s) @@ -156,11 +172,11 @@ let rec prompt level = let open Proofview.NonLogical in Proofview.NonLogical.print_notice (fnl () ++ str "TcDebug (" ++ int level ++ str ") > ") >> if Util.(!batch) then return (DebugOn (level+1)) else - let exit = (skip:=0) >> (skipped:=0) >> raise Sys.Break in + let exit = (skip:=0) >> (skipped:=0) >> raise (Sys.Break, Exninfo.null) in Proofview.NonLogical.catch Proofview.NonLogical.read_line begin function (e, info) -> match e with | End_of_file -> exit - | e -> raise ~info e + | e -> raise (e, info) end >>= fun inst -> match inst with @@ -176,7 +192,7 @@ let rec prompt level = Proofview.NonLogical.catch (run_com inst >> runtrue >> return (DebugOn (level+1))) begin function (e, info) -> match e with | Failure _ | Invalid_argument _ -> prompt level - | e -> raise ~info e + | e -> raise (e, info) end end diff --git a/plugins/ltac/tactic_matching.ml b/plugins/ltac/tactic_matching.ml index eabfe2f540..2d5e9e53ce 100644 --- a/plugins/ltac/tactic_matching.ml +++ b/plugins/ltac/tactic_matching.ml @@ -227,11 +227,9 @@ module PatternMatching (E:StaticEnvironment) = struct substitution. *) let wildcard_match_term = return - (** [pattern_match_term refresh pat term lhs] returns the possible - matchings of [term] with the pattern [pat => lhs]. If refresh is - true, refreshes the universes of [term]. *) - let pattern_match_term refresh pat term lhs = -(* let term = if refresh then Termops.refresh_universes_strict term else term in *) + (** [pattern_match_term pat term lhs] returns the possible + matchings of [term] with the pattern [pat => lhs]. *) + let pattern_match_term pat term lhs = match pat with | Term p -> begin @@ -262,7 +260,7 @@ module PatternMatching (E:StaticEnvironment) = struct matching rule [rule]. *) let rule_match_term term = function | All lhs -> wildcard_match_term lhs - | Pat ([],pat,lhs) -> pattern_match_term false pat term lhs + | Pat ([],pat,lhs) -> pattern_match_term pat term lhs | Pat _ -> (* Rules with hypotheses, only work in match goal. *) fail @@ -286,8 +284,7 @@ module PatternMatching (E:StaticEnvironment) = struct let hyp_match_type hypname pat hyps = pick hyps >>= fun decl -> let id = NamedDecl.get_id decl in - let refresh = is_local_def decl in - pattern_match_term refresh pat (NamedDecl.get_type decl) () <*> + pattern_match_term pat (NamedDecl.get_type decl) () <*> put_terms (id_map_try_add_name hypname (EConstr.mkVar id) empty_term_subst) <*> return id @@ -298,8 +295,8 @@ module PatternMatching (E:StaticEnvironment) = struct let hyp_match_body_and_type hypname bodypat typepat hyps = pick hyps >>= function | LocalDef (id,body,hyp) -> - pattern_match_term false bodypat body () <*> - pattern_match_term true typepat hyp () <*> + pattern_match_term bodypat body () <*> + pattern_match_term typepat hyp () <*> put_terms (id_map_try_add_name hypname (EConstr.mkVar id.binder_name) empty_term_subst) <*> return id.binder_name | LocalAssum (id,hyp) -> fail @@ -337,7 +334,7 @@ module PatternMatching (E:StaticEnvironment) = struct (* the rules are applied from the topmost one (in the concrete syntax) to the bottommost. *) let hyppats = List.rev hyppats in - pattern_match_term false conclpat concl () <*> + pattern_match_term conclpat concl () <*> hyp_pattern_list_match hyppats hyps lhs (** [match_goal hyps concl rules] matches the goal [hyps|-concl] diff --git a/pretyping/typing.mli b/pretyping/typing.mli index fd2dc7c2fc..e85f6327f8 100644 --- a/pretyping/typing.mli +++ b/pretyping/typing.mli @@ -19,6 +19,7 @@ open Evd (** Typecheck a term and return its type. May trigger an evarmap leak. *) val unsafe_type_of : env -> evar_map -> constr -> types +[@@ocaml.deprecated "Use [type_of] or retyping according to your needs."] (** Typecheck a term and return its type + updated evars, optionally refreshing universes *) diff --git a/proofs/proof.ml b/proofs/proof.ml index e2ee5426b5..7d0b31734e 100644 --- a/proofs/proof.ml +++ b/proofs/proof.ml @@ -69,16 +69,16 @@ exception FullyUnfocused let _ = CErrors.register_handler begin function | CannotUnfocusThisWay -> - Pp.str "This proof is focused, but cannot be unfocused this way" + Some (Pp.str "This proof is focused, but cannot be unfocused this way") | NoSuchGoals (i,j) when Int.equal i j -> - Pp.(str "[Focus] No such goal (" ++ int i ++ str").") + Some Pp.(str "[Focus] No such goal (" ++ int i ++ str").") | NoSuchGoals (i,j) -> - Pp.(str "[Focus] Not every goal in range ["++ int i ++ str","++int j++str"] exist.") + Some Pp.(str "[Focus] Not every goal in range ["++ int i ++ str","++int j++str"] exist.") | NoSuchGoal id -> - Pp.(str "[Focus] No such goal: " ++ str (Names.Id.to_string id) ++ str ".") + Some Pp.(str "[Focus] No such goal: " ++ str (Names.Id.to_string id) ++ str ".") | FullyUnfocused -> - Pp.str "The proof is not focused" - | _ -> raise CErrors.Unhandled + Some (Pp.str "The proof is not focused") + | _ -> None end let check_cond_kind c k = @@ -325,9 +325,9 @@ exception OpenProof of Names.Id.t option * open_error_reason let _ = CErrors.register_handler begin function | OpenProof (pid, reason) -> let open Pp in - Option.cata (fun pid -> - str " (in proof " ++ Names.Id.print pid ++ str "): ") (mt()) pid ++ print_open_error_reason reason - | _ -> raise CErrors.Unhandled + Some (Option.cata (fun pid -> + str " (in proof " ++ Names.Id.print pid ++ str "): ") (mt()) pid ++ print_open_error_reason reason) + | _ -> None end let warn_remaining_shelved_goals = diff --git a/proofs/proof_bullet.ml b/proofs/proof_bullet.ml index 3ff0533b6b..d978885d62 100644 --- a/proofs/proof_bullet.ml +++ b/proofs/proof_bullet.ml @@ -79,8 +79,8 @@ module Strict = struct (function | FailedBullet (b,sugg) -> let prefix = Pp.(str"Wrong bullet " ++ pr_bullet b ++ str": ") in - Pp.(str "[Focus]" ++ spc () ++ prefix ++ suggest_on_error sugg) - | _ -> raise CErrors.Unhandled) + Some Pp.(str "[Focus]" ++ spc () ++ prefix ++ suggest_on_error sugg) + | _ -> None) (* spiwack: we need only one focus kind as we keep a stack of (distinct!) bullets *) @@ -203,7 +203,7 @@ exception SuggestNoSuchGoals of int * Proof.t let _ = CErrors.register_handler begin function | SuggestNoSuchGoals(n,proof) -> let suffix = suggest proof in - Pp.(str "No such " ++ str (CString.plural n "goal") ++ str "." ++ - pr_non_empty_arg (fun x -> x) suffix) - | _ -> raise CErrors.Unhandled + Some (Pp.(str "No such " ++ str (CString.plural n "goal") ++ str "." ++ + pr_non_empty_arg (fun x -> x) suffix)) + | _ -> None end diff --git a/proofs/tacmach.ml b/proofs/tacmach.ml index d3bce07814..3e4549f92c 100644 --- a/proofs/tacmach.ml +++ b/proofs/tacmach.ml @@ -76,7 +76,6 @@ let pf_nf = pf_reduce simpl let pf_nf_betaiota = pf_reduce nf_betaiota let pf_compute = pf_reduce compute let pf_unfoldn ubinds = pf_reduce (unfoldn ubinds) -let pf_unsafe_type_of = pf_reduce unsafe_type_of let pf_type_of = pf_reduce type_of let pf_get_type_of = pf_reduce Retyping.get_type_of @@ -117,9 +116,6 @@ module New = struct let pf_env = Proofview.Goal.env let pf_concl = Proofview.Goal.concl - let pf_unsafe_type_of gl t = - pf_apply unsafe_type_of gl t - let pf_type_of gl t = pf_apply type_of gl t @@ -182,4 +178,12 @@ module New = struct let pf_compute gl t = pf_apply compute gl t let pf_nf_evar gl t = nf_evar (project gl) t + + (* deprecated *) + let pf_unsafe_type_of gl t = + pf_apply (unsafe_type_of[@warning "-3"]) gl t + end + +(* deprecated *) +let pf_unsafe_type_of = pf_reduce unsafe_type_of[@warning "-3"] diff --git a/proofs/tacmach.mli b/proofs/tacmach.mli index aed1c89bfe..b4247f39b9 100644 --- a/proofs/tacmach.mli +++ b/proofs/tacmach.mli @@ -34,6 +34,7 @@ val pf_nth_hyp_id : Goal.goal sigma -> int -> Id.t val pf_last_hyp : Goal.goal sigma -> named_declaration val pf_ids_of_hyps : Goal.goal sigma -> Id.t list val pf_unsafe_type_of : Goal.goal sigma -> constr -> types +[@@ocaml.deprecated "Use [type_of] or retyping according to your needs."] val pf_type_of : Goal.goal sigma -> constr -> evar_map * types val pf_hnf_type_of : Goal.goal sigma -> constr -> types @@ -83,6 +84,7 @@ module New : sig (** WRONG: To be avoided at all costs, it typechecks the term entirely but forgets the universe constraints necessary to retypecheck it *) val pf_unsafe_type_of : Proofview.Goal.t -> constr -> types + [@@ocaml.deprecated "Use [type_of] or retyping according to your needs."] (** This function does no type inference and expects an already well-typed term. It recomputes its type in the fastest way possible (no conversion is ever involved) *) diff --git a/stm/stm.ml b/stm/stm.ml index a521f9001d..c79a1eed3d 100644 --- a/stm/stm.ml +++ b/stm/stm.ml @@ -1273,8 +1273,8 @@ let record_pb_time ?loc proof_name time = exception RemoteException of Pp.t let _ = CErrors.register_handler (function - | RemoteException ppcmd -> ppcmd - | _ -> raise Unhandled) + | RemoteException ppcmd -> Some ppcmd + | _ -> None) (****************** proof structure for error recovery ************************) (******************************************************************************) diff --git a/tactics/declare.ml b/tactics/declare.ml index ce2f3ec2c5..5655bdfd4d 100644 --- a/tactics/declare.ml +++ b/tactics/declare.ml @@ -24,10 +24,11 @@ exception AlreadyDeclared of (string option * Id.t) let _ = CErrors.register_handler (function | AlreadyDeclared (kind, id) -> - seq [ Pp.pr_opt_no_spc (fun s -> str s ++ spc ()) kind - ; Id.print id; str " already exists."] + Some + (seq [ Pp.pr_opt_no_spc (fun s -> str s ++ spc ()) kind + ; Id.print id; str " already exists."]) | _ -> - raise CErrors.Unhandled) + None) module NamedDecl = Context.Named.Declaration diff --git a/tactics/pfedit.ml b/tactics/pfedit.ml index 72204e1d24..dbabc4e4e0 100644 --- a/tactics/pfedit.ml +++ b/tactics/pfedit.ml @@ -26,8 +26,8 @@ let use_unification_heuristics () = !use_unification_heuristics_ref exception NoSuchGoal let () = CErrors.register_handler begin function - | NoSuchGoal -> Pp.(str "No such goal.") - | _ -> raise CErrors.Unhandled + | NoSuchGoal -> Some Pp.(str "No such goal.") + | _ -> None end let get_nth_V82_goal p i = diff --git a/test-suite/bugs/closed/bug_11549.v b/test-suite/bugs/closed/bug_11549.v new file mode 100644 index 0000000000..7608e1c4d8 --- /dev/null +++ b/test-suite/bugs/closed/bug_11549.v @@ -0,0 +1,5 @@ +From Ltac2 Require Ltac2. + +Notation "t $ r" := (t r) + (at level 65, right associativity, only parsing). +Check S $ O. diff --git a/topbin/coqtop_byte_bin.ml b/topbin/coqtop_byte_bin.ml index 604c6e251a..7e977ca0f2 100644 --- a/topbin/coqtop_byte_bin.ml +++ b/topbin/coqtop_byte_bin.ml @@ -11,9 +11,9 @@ (* We register this handler for lower-level toplevel loading code *) let _ = CErrors.register_handler (function | Symtable.Error e -> - Pp.str (Format.asprintf "%a" Symtable.report_error e) + Some (Pp.str (Format.asprintf "%a" Symtable.report_error e)) | _ -> - raise CErrors.Unhandled + None ) let drop_setup () = diff --git a/user-contrib/Ltac2/g_ltac2.mlg b/user-contrib/Ltac2/g_ltac2.mlg index d05640f22d..e95ac3b02b 100644 --- a/user-contrib/Ltac2/g_ltac2.mlg +++ b/user-contrib/Ltac2/g_ltac2.mlg @@ -25,6 +25,10 @@ let err () = raise Stream.Failure type lookahead = Gramlib.Plexing.location_function -> int -> Tok.t Stream.t -> int option +let check_no_space tok m strm = + let n = Stream.count strm in + if G_prim.contiguous tok n (n+m-1) then Some m else None + let entry_of_lookahead s (lk : lookahead) = let run tok strm = match lk tok 0 strm with None -> err () | Some _ -> () in Pcoq.Entry.of_parser s run @@ -51,7 +55,7 @@ let lk_int tok n strm = match stream_nth n strm with | NUMERAL { NumTok.int = _; frac = ""; exp = "" } -> Some (n + 1) | _ -> None -let lk_ident_or_anti = lk_ident <+> (lk_kw "$" >> lk_ident) +let lk_ident_or_anti = lk_ident <+> (lk_kw "$" >> lk_ident >> check_no_space) let rec lk_ident_list n strm = ((lk_ident >> lk_ident_list) <+> lk_empty) n strm @@ -80,10 +84,6 @@ let test_lpar_id_rpar = lk_kw "(" >> lk_ident >> lk_kw ")" end -let check_no_space tok m strm = - let n = Stream.count strm in - if G_prim.contiguous tok n (n+m-1) then Some m else None - let test_ampersand_ident = entry_of_lookahead "test_ampersand_ident" begin lk_kw "&" >> lk_ident >> check_no_space @@ -91,7 +91,7 @@ let test_ampersand_ident = let test_dollar_ident = entry_of_lookahead "test_dollar_ident" begin - lk_kw "$" >> lk_ident + lk_kw "$" >> lk_ident >> check_no_space end let test_ltac1_env = @@ -889,7 +889,7 @@ let rules = [ ] in Hook.set Tac2entries.register_constr_quotations begin fun () -> - Pcoq.grammar_extend Pcoq.Constr.operconstr None (Some (Gramlib.Gramext.Level "0"), [(None, None, rules)]) + Pcoq.grammar_extend Pcoq.Constr.operconstr (Some (Gramlib.Gramext.Level "0"), [(None, None, rules)]) end } diff --git a/user-contrib/Ltac2/tac2core.ml b/user-contrib/Ltac2/tac2core.ml index 431589aa30..196b28b274 100644 --- a/user-contrib/Ltac2/tac2core.ml +++ b/user-contrib/Ltac2/tac2core.ml @@ -161,7 +161,7 @@ let set_bt info = let throw ?(info = Exninfo.null) e = set_bt info >>= fun info -> let info = Exninfo.add info fatal_flag () in - Proofview.tclLIFT (Proofview.NonLogical.raise ~info e) + Proofview.tclLIFT (Proofview.NonLogical.raise (e, info)) let fail ?(info = Exninfo.null) e = set_bt info >>= fun info -> diff --git a/user-contrib/Ltac2/tac2entries.ml b/user-contrib/Ltac2/tac2entries.ml index d6db4a735c..2a0c109a42 100644 --- a/user-contrib/Ltac2/tac2entries.ml +++ b/user-contrib/Ltac2/tac2entries.ml @@ -643,7 +643,7 @@ let perform_notation syn st = | Some lev -> Some (string_of_int lev) in let rule = (lev, None, [rule]) in - ([Pcoq.ExtendRule (Pltac.tac2expr, None, (None, [rule]))], st) + ([Pcoq.ExtendRule (Pltac.tac2expr, (None, [rule]))], st) let ltac2_notation = Pcoq.create_grammar_command "ltac2-notation" perform_notation @@ -848,8 +848,8 @@ let () = register_handler begin function let v = Tac2ffi.of_open (kn, args) in let t = GTypRef (Other t_exn, []) in let c = Tac2print.pr_valexpr (Global.env ()) Evd.empty v t in - hov 0 (str "Uncaught Ltac2 exception:" ++ spc () ++ hov 0 c) -| _ -> raise Unhandled + Some (hov 0 (str "Uncaught Ltac2 exception:" ++ spc () ++ hov 0 c)) +| _ -> None end let () = CErrors.register_additional_error_info begin fun info -> diff --git a/vernac/egramcoq.ml b/vernac/egramcoq.ml index 72e6d41969..ead86bd12f 100644 --- a/vernac/egramcoq.ml +++ b/vernac/egramcoq.ml @@ -96,38 +96,38 @@ let create_pos = function let find_position_gen current ensure assoc lev = match lev with | None -> - current, (None, None, None, None) + current, (None, None, None, None) | Some n -> - let after = ref None in - let init = ref None in - let rec add_level q = function - | (p,_,_ as pa)::l when p > n -> pa :: add_level (Some p) l - | (p,a,reinit)::l when Int.equal p n -> - if reinit then - let a' = create_assoc assoc in - (init := Some (a',create_pos q); (p,a',false)::l) - else if admissible_assoc (a,assoc) then - raise Exit - else - error_level_assoc p a (Option.get assoc) - | l -> after := q; (n,create_assoc assoc,ensure)::l - in - try - let updated = add_level None current in - let assoc = create_assoc assoc in - begin match !init with + let after = ref None in + let init = ref None in + let rec add_level q = function + | (p,_,_ as pa)::l when p > n -> pa :: add_level (Some p) l + | (p,a,reinit)::l when Int.equal p n -> + if reinit then + let a' = create_assoc assoc in + (init := Some (a',create_pos q); (p,a',false)::l) + else if admissible_assoc (a,assoc) then + raise Exit + else + error_level_assoc p a (Option.get assoc) + | l -> after := q; (n,create_assoc assoc,ensure)::l + in + try + let updated = add_level None current in + let assoc = create_assoc assoc in + begin match !init with | None -> (* Create the entry *) - updated, (Some (create_pos !after), Some assoc, Some (constr_level n), None) + updated, (Some (create_pos !after), Some assoc, Some (constr_level n), None) | _ -> (* The reinit flag has been updated *) - updated, (Some (Gramlib.Gramext.Level (constr_level n)), None, None, !init) - end - with - (* Nothing has changed *) - Exit -> - (* Just inherit the existing associativity and name (None) *) - current, (Some (Gramlib.Gramext.Level (constr_level n)), None, None, None) + updated, (Some (Gramlib.Gramext.Level (constr_level n)), None, None, !init) + end + with + (* Nothing has changed *) + Exit -> + (* Just inherit the existing associativity and name (None) *) + current, (Some (Gramlib.Gramext.Level (constr_level n)), None, None, None) let rec list_mem_assoc_triple x = function | [] -> false @@ -505,7 +505,11 @@ let target_to_bool : type r. r target -> bool = function let prepare_empty_levels forpat (where,(pos,p4assoc,name,reinit)) = let empty = (pos, [(name, p4assoc, [])]) in - ExtendRule (target_entry where forpat, reinit, empty) + match reinit with + | None -> + ExtendRule (target_entry where forpat, empty) + | Some reinit -> + ExtendRuleReinit (target_entry where forpat, reinit, empty) let different_levels (custom,opt_level) (custom',string_level) = match opt_level with @@ -552,7 +556,12 @@ let extend_constr state forpat ng = | MayRecRNo symbs -> Rule (symbs, act) | MayRecRMay symbs -> Rule (symbs, act) in name, p4assoc, [r] in - let r = ExtendRule (entry, reinit, (pos, [rule])) in + let r = match reinit with + | None -> + ExtendRule (entry, (pos, [rule])) + | Some reinit -> + ExtendRuleReinit (entry, reinit, (pos, [rule])) + in (accu @ empty_rules @ [r], state) in List.fold_left fold ([], state) ng.notgram_prods diff --git a/vernac/egramml.ml b/vernac/egramml.ml index 62eb561f3c..2b1d99c7a9 100644 --- a/vernac/egramml.ml +++ b/vernac/egramml.ml @@ -90,4 +90,4 @@ let extend_vernac_command_grammar s nt gl = vernac_exts := (s,gl) :: !vernac_exts; let mkact loc l = VernacExtend (s, l) in let rules = [make_rule mkact gl] in - grammar_extend nt None (None, [None, None, rules]) + grammar_extend nt (None, [None, None, rules]) diff --git a/vernac/himsg.ml b/vernac/himsg.ml index f6f6c4f1eb..07ec6ca1ba 100644 --- a/vernac/himsg.ml +++ b/vernac/himsg.ml @@ -1356,6 +1356,12 @@ let explain_prim_token_notation_error kind env sigma = function Nota: explain_exn does NOT end with a newline anymore! *) +exception Unhandled + +let wrap_unhandled f e = + try Some (f e) + with Unhandled -> None + let explain_exn_default = function (* Basic interaction exceptions *) | Stream.Error txt -> hov 0 (str "Syntax error: " ++ str txt ++ str ".") @@ -1366,9 +1372,9 @@ let explain_exn_default = function | CErrors.Timeout -> hov 0 (str "Timeout!") | Sys.Break -> hov 0 (fnl () ++ str "User interrupt.") (* Otherwise, not handled here *) - | _ -> raise CErrors.Unhandled + | _ -> raise Unhandled -let _ = CErrors.register_handler explain_exn_default +let _ = CErrors.register_handler (wrap_unhandled explain_exn_default) let rec vernac_interp_error_handler = function | Univ.UniverseInconsistency i -> @@ -1409,6 +1415,6 @@ let rec vernac_interp_error_handler = function | Logic_monad.TacticFailure e -> vernac_interp_error_handler e | _ -> - raise CErrors.Unhandled + raise Unhandled -let _ = CErrors.register_handler vernac_interp_error_handler +let _ = CErrors.register_handler (wrap_unhandled vernac_interp_error_handler) diff --git a/vernac/mltop.ml b/vernac/mltop.ml index ab9d008659..5046248e11 100644 --- a/vernac/mltop.ml +++ b/vernac/mltop.ml @@ -99,9 +99,9 @@ let ocaml_toploop () = *) let _ = CErrors.register_handler (function | Dynlink.Error e -> - hov 0 (str "Dynlink error: " ++ str Dynlink.(error_message e)) + Some (hov 0 (str "Dynlink error: " ++ str Dynlink.(error_message e))) | _ -> - raise CErrors.Unhandled + None ) let ml_load s = diff --git a/vernac/pvernac.ml b/vernac/pvernac.ml index 826e88cabf..2425f3d6c1 100644 --- a/vernac/pvernac.ml +++ b/vernac/pvernac.ml @@ -58,7 +58,7 @@ module Vernac_ = Rule (Next (Stop, Atoken Tok.PEOI), act_eoi); Rule (Next (Stop, Aentry vernac_control), act_vernac); ] in - Pcoq.grammar_extend main_entry None (None, [None, None, rule]) + Pcoq.grammar_extend main_entry (None, [None, None, rule]) let select_tactic_entry spec = match spec with diff --git a/vernac/vernacextend.ml b/vernac/vernacextend.ml index e29086d726..f41df06f85 100644 --- a/vernac/vernacextend.ml +++ b/vernac/vernacextend.ml @@ -254,7 +254,7 @@ let vernac_argument_extend ~name arg = e | Arg_rules rules -> let e = Pcoq.create_generic_entry Pcoq.utactic name (Genarg.rawwit wit) in - let () = Pcoq.grammar_extend e None (None, [(None, None, rules)]) in + let () = Pcoq.grammar_extend e (None, [(None, None, rules)]) in e in let pr = arg.arg_printer in diff --git a/vernac/vernacstate.ml b/vernac/vernacstate.ml index 80b72225f0..3c70961e06 100644 --- a/vernac/vernacstate.ml +++ b/vernac/vernacstate.ml @@ -124,8 +124,8 @@ module Proof_global = struct let () = CErrors.register_handler begin function | NoCurrentProof -> - Pp.(str "No focused proof (No proof-editing in progress).") - | _ -> raise CErrors.Unhandled + Some (Pp.(str "No focused proof (No proof-editing in progress).")) + | _ -> None end open Lemmas |