diff options
79 files changed, 688 insertions, 510 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/dev/tools/merge-pr.sh b/dev/tools/merge-pr.sh index d8d835d9b8..ce64aebdc7 100755 --- a/dev/tools/merge-pr.sh +++ b/dev/tools/merge-pr.sh @@ -22,7 +22,6 @@ fi RED="\033[31m" RESET="\033[0m" GREEN="\033[32m" -BLUE="\033[34m" YELLOW="\033[33m" info() { echo -e "${GREEN}info:${RESET} $1 ${RESET}" @@ -74,17 +73,17 @@ fi PRDATA=$(curl -s "$API/pulls/$PR") TITLE=$(echo "$PRDATA" | jq -r '.title') -info "title for PR $PR is ${BLUE}$TITLE" +info "title for PR $PR is $TITLE" BASE_BRANCH=$(echo "$PRDATA" | jq -r '.base.label') -info "PR $PR targets branch ${BLUE}$BASE_BRANCH" +info "PR $PR targets branch $BASE_BRANCH" CURRENT_LOCAL_BRANCH=$(git rev-parse --abbrev-ref HEAD) -info "you are merging in ${BLUE}$CURRENT_LOCAL_BRANCH" +info "you are merging in $CURRENT_LOCAL_BRANCH" REMOTE=$(git config --get "branch.$CURRENT_LOCAL_BRANCH.remote") if [ -z "$REMOTE" ]; then - error "branch ${BLUE}$CURRENT_LOCAL_BRANCH${RESET} has not associated remote" + error "branch $CURRENT_LOCAL_BRANCH has not associated remote" error "don't know where to fetch the PR from" error "please run: git branch --set-upstream-to=THE_REMOTE/$CURRENT_LOCAL_BRANCH" exit 1 @@ -96,12 +95,12 @@ if [ "$REMOTE_URL" != "${OFFICIAL_REMOTE_GIT_URL}" ] && \ [ "$REMOTE_URL" != "https://${OFFICIAL_REMOTE_HTTPS_URL}.git" ] && \ [[ "$REMOTE_URL" != "https://"*"@${OFFICIAL_REMOTE_HTTPS_URL}" ]] && \ [[ "$REMOTE_URL" != "https://"*"@${OFFICIAL_REMOTE_HTTPS_URL}.git" ]] ; then - error "remote ${BLUE}$REMOTE${RESET} does not point to the official Coq repo" - error "that is ${BLUE}$OFFICIAL_REMOTE_GIT_URL" - error "it points to ${BLUE}$REMOTE_URL${RESET} instead" + error "remote $REMOTE does not point to the official Coq repo" + error "that is $OFFICIAL_REMOTE_GIT_URL" + error "it points to $REMOTE_URL instead" ask_confirmation fi -info "remote for $CURRENT_LOCAL_BRANCH is ${BLUE}$REMOTE" +info "remote for $CURRENT_LOCAL_BRANCH is $REMOTE" info "fetching from $REMOTE the PR" git remote update "$REMOTE" @@ -112,12 +111,12 @@ if ! git ls-remote "$REMOTE" | grep pull >/dev/null; then fi git fetch "$REMOTE" "refs/pull/$PR/head" COMMIT=$(git rev-parse FETCH_HEAD) -info "commit for PR $PR is ${BLUE}$COMMIT" +info "commit for PR $PR is $COMMIT" # Sanity check: merge to a different branch if [ "$BASE_BRANCH" != "coq:$CURRENT_LOCAL_BRANCH" ]; then - error "PR requests merge in ${BLUE}$BASE_BRANCH${RESET} but you are merging in ${BLUE}$CURRENT_LOCAL_BRANCH" + error "PR requests merge in $BASE_BRANCH but you are merging in $CURRENT_LOCAL_BRANCH" ask_confirmation fi; @@ -166,7 +165,7 @@ fi STATUS=$(curl -s "$API/commits/$COMMIT/status") if [ "$(echo "$STATUS" | jq -r '.state')" != "success" ]; then - error "CI unsuccessful on ${BLUE}$(echo "$STATUS" | + error "CI unsuccessful on $(echo "$STATUS" | jq -r -c '.statuses|map(select(.state != "success"))|map(.context)')" ask_confirmation fi; @@ -175,7 +174,7 @@ fi; NEEDS_LABELS=$(echo "$PRDATA" | jq -rc '.labels | map(select(.name | match("needs:"))) | map(.name)') if [ "$NEEDS_LABELS" != "[]" ]; then - error "needs:something labels still present: ${BLUE}$NEEDS_LABELS" + error "needs:something labels still present: $NEEDS_LABELS" ask_confirmation fi diff --git a/doc/changelog/03-notations/11650-parensNew.rst b/doc/changelog/03-notations/11650-parensNew.rst new file mode 100644 index 0000000000..5e2da594c6 --- /dev/null +++ b/doc/changelog/03-notations/11650-parensNew.rst @@ -0,0 +1,4 @@ +- **Added:** + added option Set Printing Parentheses to print parentheses even when implied by associativity or precedence. + (`#11650 <https://github.com/coq/coq/pull/11650>`_, + by Hugo Herbelin and Abhishek Anand). diff --git a/doc/changelog/07-commands-and-options/11663-remove-polymorphic-unqualified.rst b/doc/changelog/07-commands-and-options/11663-remove-polymorphic-unqualified.rst new file mode 100644 index 0000000000..1f8dcd3992 --- /dev/null +++ b/doc/changelog/07-commands-and-options/11663-remove-polymorphic-unqualified.rst @@ -0,0 +1,5 @@ +- **Removed:** + Unqualified ``polymorphic``, ``monomorphic``, ``template``, + ``notemplate`` attributes (they were deprecated since Coq 8.10). + Use them as sub-attributes of the ``universes`` attribute (`#11663 + <https://github.com/coq/coq/pull/11663>`_, by Théo Zimmermann). diff --git a/doc/changelog/10-standard-library/11686-fix-int-notations.rst b/doc/changelog/10-standard-library/11686-fix-int-notations.rst new file mode 100644 index 0000000000..cc820c5a25 --- /dev/null +++ b/doc/changelog/10-standard-library/11686-fix-int-notations.rst @@ -0,0 +1,6 @@ +- **Changed:** + Notations :n:`[|@term|]` and :n:`[||@term||]` for morphisms from 63-bit + integers to :g:`Z` and :g:`zn2z int` have been removed in favor of + :n:`φ(@term)` and :n:`Φ(@term)` respectively. These notations were + breaking Ltac parsing. (`#11686 <https://github.com/coq/coq/pull/11686>`_, + by Maxime Dénès). diff --git a/doc/sphinx/proof-engine/ltac2.rst b/doc/sphinx/proof-engine/ltac2.rst index 56e33b9ea5..06106a6b4c 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/doc/sphinx/user-extensions/syntax-extensions.rst b/doc/sphinx/user-extensions/syntax-extensions.rst index e1545bdc2b..9b4d7cf5fa 100644 --- a/doc/sphinx/user-extensions/syntax-extensions.rst +++ b/doc/sphinx/user-extensions/syntax-extensions.rst @@ -396,6 +396,11 @@ Displaying information about notations Controls whether to use notations for printing terms wherever possible. Default is on. +.. flag:: Printing Parentheses + + If on, parentheses are printed even if implied by associativity and precedence + Default is off. + .. seealso:: :flag:`Printing All` 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/coq.ml b/ide/coq.ml index 0c6aef0305..5b66cb745e 100644 --- a/ide/coq.ml +++ b/ide/coq.ml @@ -558,6 +558,7 @@ struct { opts = [raw_matching]; init = true; label = "Display raw _matching expressions" }; { opts = [notations]; init = true; label = "Display _notations" }; + { opts = [notations]; init = true; label = "Display _parentheses" }; { opts = [all_basic]; init = false; label = "Display _all basic low-level contents" }; { opts = [existential]; init = false; diff --git a/ide/coqide_ui.ml b/ide/coqide_ui.ml index f22821c6ea..e9ff1bbba1 100644 --- a/ide/coqide_ui.ml +++ b/ide/coqide_ui.ml @@ -79,6 +79,7 @@ let init () = \n <menuitem action='Display coercions' />\ \n <menuitem action='Display raw matching expressions' />\ \n <menuitem action='Display notations' />\ +\n <menuitem action='Display parentheses' />\ \n <menuitem action='Display all basic low-level contents' />\ \n <menuitem action='Display existential variable instances' />\ \n <menuitem action='Display universe levels' />\ diff --git a/ide/idetop.ml b/ide/idetop.ml index ae2301a0a7..9eb0b972b6 100644 --- a/ide/idetop.ml +++ b/ide/idetop.ml @@ -49,6 +49,7 @@ let coqide_known_option table = List.mem table [ ["Printing";"Matching"]; ["Printing";"Synth"]; ["Printing";"Notations"]; + ["Printing";"Parentheses"]; ["Printing";"All"]; ["Printing";"Records"]; ["Printing";"Existential";"Instances"]; @@ -70,7 +71,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/interp/constrextern.ml b/interp/constrextern.ml index 4ec9f17c71..44aacd62d8 100644 --- a/interp/constrextern.ml +++ b/interp/constrextern.ml @@ -57,6 +57,10 @@ let print_implicits_defensive = ref true (* This forces printing of coercions *) let print_coercions = ref false +(* This forces printing of parentheses even when + it is implied by associativity/precedence *) +let print_parentheses = Notation_ops.print_parentheses + (* This forces printing universe names of Type{.} *) let print_universes = Detyping.print_universes diff --git a/interp/constrextern.mli b/interp/constrextern.mli index fa263cbeb7..0eca287c1d 100644 --- a/interp/constrextern.mli +++ b/interp/constrextern.mli @@ -53,6 +53,7 @@ val print_implicits_defensive : bool ref val print_arguments : bool ref val print_evar_arguments : bool ref val print_coercions : bool ref +val print_parentheses : bool ref val print_universes : bool ref val print_no_symbol : bool ref val print_projections : bool ref diff --git a/interp/constrintern.ml b/interp/constrintern.ml index c39e61083d..8a820293a0 100644 --- a/interp/constrintern.ml +++ b/interp/constrintern.ml @@ -2057,7 +2057,9 @@ let internalize globalenv env pattern_mode (_, ntnvars as lvar) c = intern env (CAst.make ?loc @@ CPrim (Numeral (SMinus,p))) | CNotation (_,(InConstrEntrySomeLevel,"( _ )"),([a],[],[],[])) -> intern env a | CNotation (_,ntn,args) -> - intern_notation intern env ntnvars loc ntn args + let c = intern_notation intern env ntnvars loc ntn args in + let x, impl, scopes, l = find_appl_head_data c in + apply_impargs x env impl scopes l loc | CGeneralization (b,a,c) -> intern_generalization intern env ntnvars loc b a c | CPrim p -> diff --git a/interp/notation_ops.ml b/interp/notation_ops.ml index 59a58d643c..8f47e9276b 100644 --- a/interp/notation_ops.ml +++ b/interp/notation_ops.ml @@ -258,6 +258,8 @@ let glob_constr_of_notation_constr ?loc x = (******************************************************************************) (* Translating a glob_constr into a notation, interpreting recursive patterns *) +let print_parentheses = ref false + type found_variables = { vars : Id.t list; recursive_term_vars : (Id.t * Id.t) list; @@ -1092,6 +1094,7 @@ let match_termlist match_fun alp metas sigma rest x y iter termin revert = let rest = Id.List.assoc ldots_var terms in let t = Id.List.assoc y terms in let sigma = remove_sigma y (remove_sigma ldots_var sigma) in + if !print_parentheses && not (List.is_empty acc) then raise No_match; aux sigma (t::acc) rest with No_match when not (List.is_empty acc) -> acc, match_fun metas sigma rest termin in diff --git a/interp/notation_ops.mli b/interp/notation_ops.mli index 2ab8b620df..0ef51b65a2 100644 --- a/interp/notation_ops.mli +++ b/interp/notation_ops.mli @@ -61,6 +61,8 @@ val glob_constr_of_notation_constr : ?loc:Loc.t -> notation_constr -> glob_const exception No_match +val print_parentheses : bool ref + val match_notation_constr : bool -> 'a glob_constr_g -> interpretation -> ('a glob_constr_g * extended_subscopes) list * ('a glob_constr_g list * extended_subscopes) list * ('a cases_pattern_disjunction_g * extended_subscopes) list * diff --git a/kernel/nativelib.ml b/kernel/nativelib.ml index a62b51e8aa..86eaaddc90 100644 --- a/kernel/nativelib.ml +++ b/kernel/nativelib.ml @@ -25,7 +25,7 @@ let open_header = ["Nativevalues"; let open_header = List.map mk_open open_header (* Directory where compiled files are stored *) -let output_dir = ".coq-native" +let output_dir = ref ".coq-native" (* Extension of generated ml files, stored for debugging purposes *) let source_ext = ".native" @@ -51,8 +51,13 @@ let () = at_exit (fun () -> be guessed until flags have been properly initialized. It also lets us avoid forcing [my_temp_dir] if we don't need it (eg stdlib file without native compute or native conv uses). *) -let include_dirs () = - let base = [Envars.coqlib () / "kernel"; Envars.coqlib () / "library"] in +let include_dirs = ref [] +let get_include_dirs () = + let base = match !include_dirs with + | [] -> + [Envars.coqlib () / "kernel"; Envars.coqlib () / "library"] + | _::_ as l -> l + in if Lazy.is_val my_temp_dir then (Lazy.force my_temp_dir) :: base else base @@ -88,8 +93,8 @@ let error_native_compiler_failed e = let call_compiler ?profile:(profile=false) ml_filename = let load_path = !get_load_paths () in - let load_path = List.map (fun dn -> dn / output_dir) load_path in - let include_dirs = List.flatten (List.map (fun x -> ["-I"; x]) (include_dirs () @ load_path)) in + let load_path = List.map (fun dn -> dn / !output_dir) load_path in + let include_dirs = List.flatten (List.map (fun x -> ["-I"; x]) (get_include_dirs () @ load_path)) in let f = Filename.chop_extension ml_filename in let link_filename = f ^ ".cmo" in let link_filename = Dynlink.adapt_filename link_filename in @@ -139,7 +144,7 @@ let compile_library dir code fn = let fn = fn ^ source_ext in let basename = Filename.basename fn in let dirname = Filename.dirname fn in - let dirname = dirname / output_dir in + let dirname = dirname / !output_dir in let () = try Unix.mkdir dirname 0o755 with Unix.Unix_error (Unix.EEXIST, _, _) -> () @@ -181,5 +186,5 @@ let call_linker ?(fatal=true) env ~prefix f upds = match upds with Some upds -> update_locations upds | _ -> () let link_library env ~prefix ~dirname ~basename = - let f = dirname / output_dir / basename in + let f = dirname / !output_dir / basename in call_linker env ~fatal:false ~prefix f None diff --git a/kernel/nativelib.mli b/kernel/nativelib.mli index 52d18acca6..155fde54e9 100644 --- a/kernel/nativelib.mli +++ b/kernel/nativelib.mli @@ -13,7 +13,8 @@ open Nativecode used by the native compiler. *) (* Directory where compiled files are stored *) -val output_dir : string +val output_dir : CUnix.physical_path ref +val include_dirs : CUnix.physical_path list ref val get_load_paths : (unit -> string list) ref 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/parsing/ppextend.ml b/parsing/ppextend.ml index 393ab8a302..bb6693a239 100644 --- a/parsing/ppextend.ml +++ b/parsing/ppextend.ml @@ -38,9 +38,9 @@ let ppcmd_of_cut = function | PpBrk(n1,n2) -> brk(n1,n2) type unparsing = - | UnpMetaVar of entry_relative_level + | UnpMetaVar of entry_relative_level * Extend.side option | UnpBinderMetaVar of entry_relative_level - | UnpListMetaVar of entry_relative_level * unparsing list + | UnpListMetaVar of entry_relative_level * unparsing list * Extend.side option | UnpBinderListMetaVar of bool * unparsing list | UnpTerminal of string | UnpBox of ppbox * unparsing Loc.located list @@ -50,9 +50,9 @@ type unparsing_rule = unparsing list * entry_level type extra_unparsing_rules = (string * string) list let rec unparsing_eq unp1 unp2 = match (unp1,unp2) with - | UnpMetaVar p1, UnpMetaVar p2 -> entry_relative_level_eq p1 p2 + | UnpMetaVar (p1,s1), UnpMetaVar (p2,s2) -> entry_relative_level_eq p1 p2 && s1 = s2 | UnpBinderMetaVar p1, UnpBinderMetaVar p2 -> entry_relative_level_eq p1 p2 - | UnpListMetaVar (p1,l1), UnpListMetaVar (p2,l2) -> entry_relative_level_eq p1 p2 && List.for_all2eq unparsing_eq l1 l2 + | UnpListMetaVar (p1,l1,s1), UnpListMetaVar (p2,l2,s2) -> entry_relative_level_eq p1 p2 && List.for_all2eq unparsing_eq l1 l2 && s1 = s2 | UnpBinderListMetaVar (b1,l1), UnpBinderListMetaVar (b2,l2) -> b1 = b2 && List.for_all2eq unparsing_eq l1 l2 | UnpTerminal s1, UnpTerminal s2 -> String.equal s1 s2 | UnpBox (b1,l1), UnpBox (b2,l2) -> b1 = b2 && List.for_all2eq unparsing_eq (List.map snd l1) (List.map snd l2) diff --git a/parsing/ppextend.mli b/parsing/ppextend.mli index 346fc83f5f..18e48942c6 100644 --- a/parsing/ppextend.mli +++ b/parsing/ppextend.mli @@ -30,9 +30,9 @@ val ppcmd_of_cut : ppcut -> Pp.t (** Declare and look for the printing rule for symbolic notations *) type unparsing = - | UnpMetaVar of entry_relative_level + | UnpMetaVar of entry_relative_level * Extend.side option | UnpBinderMetaVar of entry_relative_level - | UnpListMetaVar of entry_relative_level * unparsing list + | UnpListMetaVar of entry_relative_level * unparsing list * Extend.side option | UnpBinderListMetaVar of bool * unparsing list | UnpTerminal of string | UnpBox of ppbox * unparsing Loc.located list 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/printing/ppconstr.ml b/printing/ppconstr.ml index c2d760ae08..59972f8bdb 100644 --- a/printing/ppconstr.ml +++ b/printing/ppconstr.ml @@ -85,6 +85,7 @@ let tag_var = tag Tag.variable let env = ref terms and envlist = ref termlists and bl = ref binders and bll = ref binderlists in let pop r = let a = List.hd !r in r := List.tl !r; a in let return unp pp1 pp2 = (tag_unparsing unp pp1) ++ pp2 in + let parens = !Constrextern.print_parentheses in (* Warning: The following function enforces a very precise order of evaluation of sub-components. @@ -92,19 +93,19 @@ let tag_var = tag Tag.variable let rec aux = function | [] -> mt () - | UnpMetaVar prec as unp :: l -> + | UnpMetaVar (prec, side) as unp :: l -> let c = pop env in let pp2 = aux l in - let pp1 = pr prec c in + let pp1 = pr (if parens && side <> None then LevelLe 0 else prec) c in return unp pp1 pp2 | UnpBinderMetaVar prec as unp :: l -> let c = pop bl in let pp2 = aux l in let pp1 = pr_patt prec c in return unp pp1 pp2 - | UnpListMetaVar (prec, sl) as unp :: l -> + | UnpListMetaVar (prec, sl, side) as unp :: l -> let cl = pop envlist in - let pp1 = prlist_with_sep (fun () -> aux sl) (pr prec) cl in + let pp1 = prlist_with_sep (fun () -> aux sl) (pr (if parens && side <> None then LevelLe 0 else prec)) cl in let pp2 = aux l in return unp pp1 pp2 | UnpBinderListMetaVar (isopen, sl) as unp :: l -> 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/stm/stm.ml b/stm/stm.ml index a521f9001d..95c58b9043 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 ************************) (******************************************************************************) @@ -2157,22 +2157,23 @@ let collect_proof keep cur hd brkind id = let has_default_proof_using = Option.has_some (Proof_using.get_default_proof_using ()) in let proof_using_ast = function | VernacProof(_,Some _) -> true + | VernacProof(_,None) -> has_default_proof_using | _ -> false in let proof_using_ast = function | Some (_, v) when proof_using_ast v.expr.CAst.v.expr && (not (Vernacprop.has_Fail v.expr)) -> Some v | _ -> None in - let has_proof_using x = has_default_proof_using || (proof_using_ast x <> None) in + let has_proof_using x = proof_using_ast x <> None in let proof_no_using = function - | VernacProof(t,None) -> t + | VernacProof(t,None) -> if has_default_proof_using then None else t | _ -> assert false in let proof_no_using = function | Some (_, v) -> proof_no_using v.expr.CAst.v.expr, v | _ -> assert false in let has_proof_no_using = function - | VernacProof(_,None) -> true + | VernacProof(_,None) -> not has_default_proof_using | _ -> false in let has_proof_no_using = function 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_10031.v b/test-suite/bugs/closed/bug_10031.v index 15b53de00d..b76ea7d337 100644 --- a/test-suite/bugs/closed/bug_10031.v +++ b/test-suite/bugs/closed/bug_10031.v @@ -3,7 +3,7 @@ Require Import Int63 ZArith. Open Scope int63_scope. Goal False. -cut (let (q, r) := (0, 0) in ([|q|], [|r|]) = (9223372036854775808%Z, 0%Z)); +cut (let (q, r) := (0, 0) in (φ q, φ r) = (9223372036854775808%Z, 0%Z)); [discriminate| ]. Fail (change (0, 0) with (diveucl_21 1 0 1); apply diveucl_21_spec). Abort. diff --git a/test-suite/bugs/closed/bug_11342.v b/test-suite/bugs/closed/bug_11342.v new file mode 100644 index 0000000000..3c163fb772 --- /dev/null +++ b/test-suite/bugs/closed/bug_11342.v @@ -0,0 +1,19 @@ +(* -*- mode: coq; coq-prog-args: ("-vos") -*- *) + +Section foo. + Context {H:True}. + Set Default Proof Using "Type". + Theorem test2 : True. + Proof. + (* BUG: this gets run when compiling with -vos *) + fail "proof with default using". + exact I. + Qed. + + Theorem test3 : True. + Proof using Type. + (* this isn't run with -vos *) + fail "using". + exact I. + Qed. +End foo. diff --git a/test-suite/output-coqtop/ShowGoal.out b/test-suite/output-coqtop/ShowGoal.out index 2eadd22db8..42d9ff31e9 100644 --- a/test-suite/output-coqtop/ShowGoal.out +++ b/test-suite/output-coqtop/ShowGoal.out @@ -52,19 +52,19 @@ x < 1 subgoal ============================
i = i
-x < goal ID 16 at state 5
+x < goal ID 13 at state 5
i : nat
============================
i = ?j /\ ?j = ?k /\ i = ?k
-x < goal ID 16 at state 7
+x < goal ID 13 at state 7
i : nat
============================
i = i /\ i = ?k /\ i = ?k
-x < goal ID 16 at state 9
+x < goal ID 13 at state 9
i : nat
============================
diff --git a/test-suite/output-coqtop/ShowGoal.v b/test-suite/output-coqtop/ShowGoal.v index 9545254770..80996eb169 100644 --- a/test-suite/output-coqtop/ShowGoal.v +++ b/test-suite/output-coqtop/ShowGoal.v @@ -6,6 +6,6 @@ Proof using. trivial. split. trivial. -Show Goal 16 at 5. -Show Goal 16 at 7. -Show Goal 16 at 9. +Show Goal 13 at 5. +Show Goal 13 at 7. +Show Goal 13 at 9. diff --git a/test-suite/output/EqNotation.out b/test-suite/output/EqNotation.out new file mode 100644 index 0000000000..41500a75b9 --- /dev/null +++ b/test-suite/output/EqNotation.out @@ -0,0 +1,3 @@ +The command has indeed failed with message: +Cannot infer the implicit parameter A of eq whose type is +"Type". diff --git a/test-suite/output/EqNotation.v b/test-suite/output/EqNotation.v new file mode 100644 index 0000000000..21076472b8 --- /dev/null +++ b/test-suite/output/EqNotation.v @@ -0,0 +1,2 @@ +(* should mention "the implicit parameter A of eq" *) +Fail Type (forall x, x = x). diff --git a/test-suite/output/PrintingParentheses.out b/test-suite/output/PrintingParentheses.out new file mode 100644 index 0000000000..a5874f09a7 --- /dev/null +++ b/test-suite/output/PrintingParentheses.out @@ -0,0 +1,28 @@ +((1 + (2 * 3), 4), 5) + : (nat * nat) * nat +mult_n_Sm = +fun n m : nat => +nat_ind (fun n0 : nat => ((n0 * m) + n0) = (n0 * (S m))) eq_refl + (fun (p : nat) (H : ((p * m) + p) = (p * (S m))) => + let n0 := p * (S m) in + match H in (_ = y) return (((m + (p * m)) + (S p)) = (S (m + y))) with + | eq_refl => + eq_ind (S ((m + (p * m)) + p)) + (fun n1 : nat => n1 = (S (m + ((p * m) + p)))) + (eq_S ((m + (p * m)) + p) (m + ((p * m) + p)) + (nat_ind + (fun n1 : nat => ((n1 + (p * m)) + p) = (n1 + ((p * m) + p))) + eq_refl + (fun (n1 : nat) + (H0 : ((n1 + (p * m)) + p) = (n1 + ((p * m) + p))) => + f_equal_nat nat S ((n1 + (p * m)) + p) + (n1 + ((p * m) + p)) H0) m)) ((m + (p * m)) + (S p)) + (plus_n_Sm (m + (p * m)) p) + end) n + : forall n m : nat, ((n * m) + n) = (n * (S m)) + +Arguments mult_n_Sm (_ _)%nat_scope +1 :: (2 :: [3; 4]) + : list nat +{0 = 1} + {2 <= (4 + 5)} + : Set diff --git a/test-suite/output/PrintingParentheses.v b/test-suite/output/PrintingParentheses.v new file mode 100644 index 0000000000..190e122e2f --- /dev/null +++ b/test-suite/output/PrintingParentheses.v @@ -0,0 +1,10 @@ +Set Printing Parentheses. + +Check (1+2*3,4,5). +Print mult_n_Sm. + +Require Import List. +Import ListNotations. +Check [1;2;3;4]. + +Check {0=1}+{2<=4+5}. diff --git a/test-suite/output/Show.out b/test-suite/output/Show.out index ca56f032ff..f02e442be5 100644 --- a/test-suite/output/Show.out +++ b/test-suite/output/Show.out @@ -1,10 +1,10 @@ -3 subgoals (ID 31) +3 subgoals (ID 29) H : 0 = 0 ============================ 1 = 1 -subgoal 2 (ID 35) is: +subgoal 2 (ID 33) is: 1 = S (S m') -subgoal 3 (ID 22) is: +subgoal 3 (ID 20) is: S (S n') = S m diff --git a/test-suite/output/bug_11342.out b/test-suite/output/bug_11342.out new file mode 100644 index 0000000000..9aac16de0d --- /dev/null +++ b/test-suite/output/bug_11342.out @@ -0,0 +1 @@ +without using diff --git a/test-suite/output/bug_11342.v b/test-suite/output/bug_11342.v new file mode 100644 index 0000000000..73131a3190 --- /dev/null +++ b/test-suite/output/bug_11342.v @@ -0,0 +1,12 @@ +(* -*- mode: coq; coq-prog-args: ("-vos") -*- *) + +Section foo. + Context {H:True}. + Theorem test1 : True. + Proof. + (* this gets printed with -vos because there's no annotation (either [Set + Default Proof Using ...] or an explicit [Proof using ...]) *) + idtac "without using". + exact I. + Qed. +End foo. diff --git a/test-suite/output/bug_11608.out b/test-suite/output/bug_11608.out new file mode 100644 index 0000000000..793ff768d4 --- /dev/null +++ b/test-suite/output/bug_11608.out @@ -0,0 +1 @@ +creating x without [Proof.] diff --git a/test-suite/output/bug_11608.v b/test-suite/output/bug_11608.v new file mode 100644 index 0000000000..3929082913 --- /dev/null +++ b/test-suite/output/bug_11608.v @@ -0,0 +1,13 @@ +(* -*- mode: coq; coq-prog-args: ("-vos") -*- *) + +Set Default Proof Using "Type". + +Section foo. + Context (A:Type). + Definition x : option A. + (* this can get printed with -vos since without "Proof." there's no Proof + using, even with a default annotation. *) + idtac "creating x without [Proof.]". + exact None. + Qed. +End foo. diff --git a/test-suite/success/Notations2.v b/test-suite/success/Notations2.v index f166a53256..382c252727 100644 --- a/test-suite/success/Notations2.v +++ b/test-suite/success/Notations2.v @@ -194,3 +194,11 @@ Notation q := @p. Check fun A n => q (A * A) (n * n). (* check that argument scopes are propagated *) End InheritanceArgumentScopes. + +Module InheritanceMaximalImplicitPureNotation. + +Definition id {A B:Type} (a:B) := a. +Notation "#" := (@id nat). +Check # = (fun a:nat => a). (* # should inherit its maximal implicit argument *) + +End InheritanceMaximalImplicitPureNotation. diff --git a/theories/Floats/FloatLemmas.v b/theories/Floats/FloatLemmas.v index 81cb7120e0..5db501742f 100644 --- a/theories/Floats/FloatLemmas.v +++ b/theories/Floats/FloatLemmas.v @@ -24,7 +24,7 @@ Theorem ldexp_spec : forall f e, Prim2SF (ldexp f e) = SFldexp prec emax (Prim2S destruct (Prim2SF f); auto. unfold SFldexp. unfold binary_round. - assert (Hmod_elim : forall e, ([| of_Z (Z.max (Z.min e (emax - emin)) (emin - emax - 1) + shift)|]%int63 - shift = Z.max (Z.min e (emax - emin)) (emin - emax - 1))%Z). + assert (Hmod_elim : forall e, (φ (of_Z (Z.max (Z.min e (emax - emin)) (emin - emax - 1) + shift))%int63 - shift = Z.max (Z.min e (emax - emin)) (emin - emax - 1))%Z). { intro e1. rewrite of_Z_spec, shift_value. diff --git a/theories/Floats/FloatOps.v b/theories/Floats/FloatOps.v index f0d3bcced9..e74cb09c27 100644 --- a/theories/Floats/FloatOps.v +++ b/theories/Floats/FloatOps.v @@ -10,7 +10,7 @@ Definition shift := 2101%Z. (** [= 2*emax + prec] *) Definition frexp f := let (m, se) := frshiftexp f in - (m, ([| se |] - shift)%Z%int63). + (m, (φ se - shift)%Z%int63). Definition ldexp f e := let e' := Z.max (Z.min e (emax - emin)) (emin - emax - 1) in @@ -28,7 +28,7 @@ Definition Prim2SF f := else let (r, exp) := frexp f in let e := (exp - prec)%Z in - let (shr, e') := shr_fexp prec emax [| normfr_mantissa r |]%int63 e loc_Exact in + let (shr, e') := shr_fexp prec emax (φ (normfr_mantissa r))%int63 e loc_Exact in match shr_m shr with | Zpos p => S754_finite (get_sign f) p e' | Zneg _ | Z0 => S754_zero false (* must never occur *) diff --git a/theories/Init/Logic.v b/theories/Init/Logic.v index 9698737d33..aa376b780a 100644 --- a/theories/Init/Logic.v +++ b/theories/Init/Logic.v @@ -352,10 +352,6 @@ Inductive eq (A:Type) (x:A) : A -> Prop := where "x = y :> A" := (@eq A x y) : type_scope. -Notation "x = y" := (x = y :>_) : type_scope. -Notation "x <> y :> T" := (~ x = y :>T) : type_scope. -Notation "x <> y" := (x <> y :>_) : type_scope. - Arguments eq {A} x _. Arguments eq_refl {A x} , [A] x. @@ -363,6 +359,10 @@ Arguments eq_ind [A] x P _ y _. Arguments eq_rec [A] x P _ y _. Arguments eq_rect [A] x P _ y _. +Notation "x = y" := (eq x y) : type_scope. +Notation "x <> y :> T" := (~ x = y :>T) : type_scope. +Notation "x <> y" := (~ (x = y)) : type_scope. + Hint Resolve I conj or_introl or_intror : core. Hint Resolve eq_refl: core. Hint Resolve ex_intro ex_intro2: core. diff --git a/theories/Numbers/Cyclic/Int63/Cyclic63.v b/theories/Numbers/Cyclic/Int63/Cyclic63.v index 74c91ac226..4125f6abb7 100644 --- a/theories/Numbers/Cyclic/Int63/Cyclic63.v +++ b/theories/Numbers/Cyclic/Int63/Cyclic63.v @@ -109,7 +109,7 @@ Instance int_ops : ZnZ.Ops int := Local Open Scope Z_scope. -Lemma is_zero_spec_aux : forall x : int, is_zero x = true -> [|x|] = 0%Z. +Lemma is_zero_spec_aux : forall x : int, is_zero x = true -> φ x = 0%Z. Proof. intros x;rewrite is_zero_spec;intros H;rewrite H;trivial. Qed. @@ -120,8 +120,8 @@ Lemma positive_to_int_spec : Z_of_N (fst (positive_to_int p)) * wB + to_Z (snd (positive_to_int p)). Proof. assert (H: (wB <= wB) -> forall p : positive, - Zpos p = Z_of_N (fst (positive_to_int p)) * wB + [|snd (positive_to_int p)|] /\ - [|snd (positive_to_int p)|] < wB). + Zpos p = Z_of_N (fst (positive_to_int p)) * wB + φ (snd (positive_to_int p)) /\ + φ (snd (positive_to_int p)) < wB). 2: intros p; case (H (Z.le_refl wB) p); auto. unfold positive_to_int, wB at 1 3 4. elim size. @@ -136,7 +136,7 @@ Proof. generalize (IH F1 p1); case positive_to_int_rec; simpl. intros n1 i (H1,H2). rewrite Zpos_xI, H1. - replace [|i << 1 + 1|] with ([|i|] * 2 + 1). + replace (φ (i << 1 + 1)) with (φ i * 2 + 1). split; auto with zarith; ring. rewrite add_spec, lsl_spec, Zplus_mod_idemp_l, to_Z_1, Z.pow_1_r, Zmod_small; auto. case (to_Z_bounded i); split; auto with zarith. @@ -144,7 +144,7 @@ Proof. generalize (IH F1 p1); case positive_to_int_rec; simpl. intros n1 i (H1,H2). rewrite Zpos_xO, H1. - replace [|i << 1|] with ([|i|] * 2). + replace (φ (i << 1)) with (φ i * 2). split; auto with zarith; ring. rewrite lsl_spec, to_Z_1, Z.pow_1_r, Zmod_small; auto. case (to_Z_bounded i); split; auto with zarith. @@ -152,7 +152,7 @@ Proof. Qed. Lemma mulc_WW_spec : - forall x y,[|| x *c y ||] = [|x|] * [|y|]. + forall x y, Φ ( x *c y ) = φ x * φ y. Proof. intros x y;unfold mulc_WW. generalize (mulc_spec x y);destruct (mulc x y);simpl;intros Heq;rewrite Heq. @@ -164,18 +164,18 @@ Qed. Lemma squarec_spec : forall x, - [||x *c x||] = [|x|] * [|x|]. + Φ(x *c x) = φ x * φ x. Proof (fun x => mulc_WW_spec x x). -Lemma diveucl_spec_aux : forall a b, 0 < [|b|] -> +Lemma diveucl_spec_aux : forall a b, 0 < φ b -> let (q,r) := diveucl a b in - [|a|] = [|q|] * [|b|] + [|r|] /\ - 0 <= [|r|] < [|b|]. + φ a = φ q * φ b + φ r /\ + 0 <= φ r < φ b. Proof. intros a b H;assert (W:= diveucl_spec a b). - assert ([|b|]>0) by (auto with zarith). - generalize (Z_div_mod [|a|] [|b|] H0). - destruct (diveucl a b);destruct (Z.div_eucl [|a|] [|b|]). + assert (φ b>0) by (auto with zarith). + generalize (Z_div_mod φ a φ b H0). + destruct (diveucl a b);destruct (Z.div_eucl φ a φ b). inversion W;rewrite Zmult_comm;trivial. Qed. @@ -252,10 +252,10 @@ Proof. case lebP; intros hle. 2: { symmetry; apply Zmod_small. - assert (2 ^ [|Int63.digits|] < 2 ^ [|p|]); [ apply Zpower_lt_monotone; auto with zarith | ]. - change wB with (2 ^ [|Int63.digits|]) in *; auto with zarith. } - rewrite <- (shift_unshift_mod_3 [|Int63.digits|] [|p|] [|w|]) by auto with zarith. - replace ([|Int63.digits|] - [|p|]) with [|Int63.digits - p|] by (rewrite sub_spec, Zmod_small; auto with zarith). + assert (2 ^ φ Int63.digits < 2 ^ φ p); [ apply Zpower_lt_monotone; auto with zarith | ]. + change wB with (2 ^ φ Int63.digits) in *; auto with zarith. } + rewrite <- (shift_unshift_mod_3 φ Int63.digits φ p φ w) by auto with zarith. + replace (φ Int63.digits - φ p) with (φ (Int63.digits - p)) by (rewrite sub_spec, Zmod_small; auto with zarith). rewrite lsr_spec, lsl_spec; reflexivity. Qed. diff --git a/theories/Numbers/Cyclic/Int63/Int63.v b/theories/Numbers/Cyclic/Int63/Int63.v index febf4fa1be..d490c28578 100644 --- a/theories/Numbers/Cyclic/Int63/Int63.v +++ b/theories/Numbers/Cyclic/Int63/Int63.v @@ -194,6 +194,8 @@ Fixpoint to_Z_rec (n:nat) (i:int) := Definition to_Z := to_Z_rec size. +Notation "'φ' x" := (to_Z x) (at level 0) : int63_scope. + Fixpoint of_pos_rec (n:nat) (p:positive) := match n, p with | O, _ => 0 @@ -211,10 +213,11 @@ Definition of_Z z := | Zneg p => - (of_pos p) end. -Notation "[| x |]" := (to_Z x) (at level 0, x at level 99) : int63_scope. - Definition wB := (2 ^ (Z.of_nat size))%Z. +Notation "'Φ' x" := + (zn2z_to_Z wB to_Z x) (at level 0) : int63_scope. + Lemma to_Z_rec_bounded size : forall x, (0 <= to_Z_rec size x < 2 ^ Z.of_nat size)%Z. Proof. elim size. simpl; auto with zarith. @@ -225,7 +228,7 @@ Proof. rewrite Zdouble_plus_one_mult; auto with zarith. Qed. -Corollary to_Z_bounded : forall x, (0 <= [| x |] < wB)%Z. +Corollary to_Z_bounded : forall x, (0 <= φ x < wB)%Z. Proof. apply to_Z_rec_bounded. Qed. (* =================================================== *) @@ -290,29 +293,24 @@ Proof. exact (fun x => let 'eq_refl := x in idProp). Qed. Lemma wB_pos : 0 < wB. Proof. reflexivity. Qed. -Lemma to_Z_0 : [|0|] = 0. +Lemma to_Z_0 : φ 0 = 0. Proof. reflexivity. Qed. -Lemma to_Z_1 : [|1|] = 1. +Lemma to_Z_1 : φ 1 = 1. Proof. reflexivity. Qed. (* Notations *) Local Open Scope Z_scope. -Notation "[+| c |]" := +Local Notation "[+| c |]" := (interp_carry 1 wB to_Z c) (at level 0, c at level 99) : int63_scope. -Notation "[-| c |]" := +Local Notation "[-| c |]" := (interp_carry (-1) wB to_Z c) (at level 0, c at level 99) : int63_scope. -Notation "[|| x ||]" := - (zn2z_to_Z wB to_Z x) (at level 0, x at level 99) : int63_scope. - (* Bijection : int63 <-> Bvector size *) -Axiom of_to_Z : forall x, of_Z [| x |] = x. - -Notation "'φ' x" := [| x |] (at level 0) : int63_scope. +Axiom of_to_Z : forall x, of_Z φ x = x. Lemma can_inj {rT aT} {f: aT -> rT} {g: rT -> aT} (K: forall a, g (f a) = a) {a a'} (e: f a = f a') : a = a'. Proof. generalize (K a) (K a'). congruence. Qed. @@ -322,9 +320,9 @@ Proof. exact (λ e, can_inj of_to_Z e). Qed. (** Specification of logical operations *) Local Open Scope Z_scope. -Axiom lsl_spec : forall x p, [| x << p |] = [| x |] * 2 ^ [| p |] mod wB. +Axiom lsl_spec : forall x p, φ (x << p) = φ x * 2 ^ φ p mod wB. -Axiom lsr_spec : forall x p, [|x >> p|] = [|x|] / 2 ^ [|p|]. +Axiom lsr_spec : forall x p, φ (x >> p) = φ x / 2 ^ φ p. Axiom land_spec: forall x y i , bit (x land y) i = bit x i && bit y i. @@ -339,26 +337,26 @@ Axiom lxor_spec: forall x y i, bit (x lxor y) i = xorb (bit x i) (bit y i). (* Remarque : les axiomes seraient plus simple si on utilise of_Z a la place : exemple : add_spec : forall x y, of_Z (x + y) = of_Z x + of_Z y. *) -Axiom add_spec : forall x y, [|x + y|] = ([|x|] + [|y|]) mod wB. +Axiom add_spec : forall x y, φ (x + y) = (φ x + φ y) mod wB. -Axiom sub_spec : forall x y, [|x - y|] = ([|x|] - [|y|]) mod wB. +Axiom sub_spec : forall x y, φ (x - y) = (φ x - φ y) mod wB. -Axiom mul_spec : forall x y, [| x * y |] = [|x|] * [|y|] mod wB. +Axiom mul_spec : forall x y, φ (x * y) = φ x * φ y mod wB. -Axiom mulc_spec : forall x y, [|x|] * [|y|] = [|fst (mulc x y)|] * wB + [|snd (mulc x y)|]. +Axiom mulc_spec : forall x y, φ x * φ y = φ (fst (mulc x y)) * wB + φ (snd (mulc x y)). -Axiom div_spec : forall x y, [|x / y|] = [|x|] / [|y|]. +Axiom div_spec : forall x y, φ (x / y) = φ x / φ y. -Axiom mod_spec : forall x y, [|x \% y|] = [|x|] mod [|y|]. +Axiom mod_spec : forall x y, φ (x \% y) = φ x mod φ y. (* Comparisons *) Axiom eqb_correct : forall i j, (i == j)%int63 = true -> i = j. Axiom eqb_refl : forall x, (x == x)%int63 = true. -Axiom ltb_spec : forall x y, (x < y)%int63 = true <-> [|x|] < [|y|]. +Axiom ltb_spec : forall x y, (x < y)%int63 = true <-> φ x < φ y. -Axiom leb_spec : forall x y, (x <= y)%int63 = true <-> [|x|] <= [|y|]. +Axiom leb_spec : forall x y, (x <= y)%int63 = true <-> φ x <= φ y. (** Exotic operations *) @@ -370,11 +368,11 @@ Primitive tail0 := #int63_tail0. Axiom compare_def_spec : forall x y, compare x y = compare_def x y. -Axiom head0_spec : forall x, 0 < [|x|] -> - wB/ 2 <= 2 ^ ([|head0 x|]) * [|x|] < wB. +Axiom head0_spec : forall x, 0 < φ x -> + wB/ 2 <= 2 ^ (φ (head0 x)) * φ x < wB. -Axiom tail0_spec : forall x, 0 < [|x|] -> - (exists y, 0 <= y /\ [|x|] = (2 * y + 1) * (2 ^ [|tail0 x|]))%Z. +Axiom tail0_spec : forall x, 0 < φ x -> + (exists y, 0 <= y /\ φ x = (2 * y + 1) * (2 ^ φ (tail0 x)))%Z. Axiom addc_def_spec : forall x y, (x +c y)%int63 = addc_def x y. @@ -388,8 +386,8 @@ Axiom diveucl_def_spec : forall x y, diveucl x y = diveucl_def x y. Axiom diveucl_21_spec : forall a1 a2 b, let (q,r) := diveucl_21 a1 a2 b in - let (q',r') := Z.div_eucl ([|a1|] * wB + [|a2|]) [|b|] in - [|a1|] < [|b|] -> [|q|] = q' /\ [|r|] = r'. + let (q',r') := Z.div_eucl (φ a1 * wB + φ a2) φ b in + φ a1 < φ b -> φ q = q' /\ φ r = r'. Axiom addmuldiv_def_spec : forall p x y, addmuldiv p x y = addmuldiv_def p x y. @@ -550,16 +548,16 @@ Qed. (** Comparison *) -Lemma eqbP x y : reflect ([| x |] = [| y |]) (x == y). +Lemma eqbP x y : reflect (φ x = φ y ) (x == y). Proof. apply iff_reflect; rewrite eqb_spec; split; [ apply to_Z_inj | apply f_equal ]. Qed. -Lemma ltbP x y : reflect ([| x |] < [| y |])%Z (x < y). +Lemma ltbP x y : reflect (φ x < φ y )%Z (x < y). Proof. apply iff_reflect; symmetry; apply ltb_spec. Qed. -Lemma lebP x y : reflect ([| x |] <= [| y |])%Z (x ≤ y). +Lemma lebP x y : reflect (φ x <= φ y )%Z (x ≤ y). Proof. apply iff_reflect; symmetry; apply leb_spec. Qed. -Lemma compare_spec x y : compare x y = ([|x|] ?= [|y|])%Z. +Lemma compare_spec x y : compare x y = (φ x ?= φ y)%Z. Proof. rewrite compare_def_spec; unfold compare_def. case ltbP; [ auto using Z.compare_lt_iff | intros hge ]. @@ -572,72 +570,72 @@ Proof. apply eqb_spec. Qed. Lemma diveucl_spec x y : let (q,r) := diveucl x y in - ([| q |], [| r |]) = Z.div_eucl [| x |] [| y |]. + (φ q , φ r ) = Z.div_eucl φ x φ y . Proof. rewrite diveucl_def_spec; unfold diveucl_def; rewrite div_spec, mod_spec; unfold Z.div, Zmod. - destruct (Z.div_eucl [| x |] [| y |]); trivial. + destruct (Z.div_eucl φ x φ y ); trivial. Qed. Local Open Scope Z_scope. (** Addition *) -Lemma addc_spec x y : [+| x +c y |] = [| x |] + [| y |]. +Lemma addc_spec x y : [+| x +c y |] = φ x + φ y . Proof. rewrite addc_def_spec; unfold addc_def, interp_carry. pose proof (to_Z_bounded x); pose proof (to_Z_bounded y). case ltbP; rewrite add_spec. - case (Z_lt_ge_dec ([| x |] + [| y |]) wB). + case (Z_lt_ge_dec (φ x + φ y ) wB). intros k; rewrite Zmod_small; lia. - intros hge; rewrite <- (Zmod_unique _ _ 1 ([| x |] + [| y |] - wB)); lia. - case (Z_lt_ge_dec ([| x |] + [| y |]) wB). + intros hge; rewrite <- (Zmod_unique _ _ 1 (φ x + φ y - wB)); lia. + case (Z_lt_ge_dec (φ x + φ y ) wB). intros k; rewrite Zmod_small; lia. - intros hge; rewrite <- (Zmod_unique _ _ 1 ([| x |] + [| y |] - wB)); lia. + intros hge; rewrite <- (Zmod_unique _ _ 1 (φ x + φ y - wB)); lia. Qed. -Lemma succ_spec x : [| succ x |] = ([| x |] + 1) mod wB. +Lemma succ_spec x : φ (succ x) = (φ x + 1) mod wB. Proof. apply add_spec. Qed. -Lemma succc_spec x : [+| succc x |] = [| x |] + 1. +Lemma succc_spec x : [+| succc x |] = φ x + 1. Proof. apply addc_spec. Qed. -Lemma addcarry_spec x y : [| addcarry x y |] = ([| x |] + [| y |] + 1) mod wB. +Lemma addcarry_spec x y : φ (addcarry x y) = (φ x + φ y + 1) mod wB. Proof. unfold addcarry; rewrite -> !add_spec, Zplus_mod_idemp_l; trivial. Qed. -Lemma addcarryc_spec x y : [+| addcarryc x y |] = [| x |] + [| y |] + 1. +Lemma addcarryc_spec x y : [+| addcarryc x y |] = φ x + φ y + 1. Proof. rewrite addcarryc_def_spec; unfold addcarryc_def, interp_carry. pose proof (to_Z_bounded x); pose proof (to_Z_bounded y). case lebP; rewrite addcarry_spec. - case (Z_lt_ge_dec ([| x |] + [| y |] + 1) wB). + case (Z_lt_ge_dec (φ x + φ y + 1) wB). intros hlt; rewrite Zmod_small; lia. - intros hge; rewrite <- (Zmod_unique _ _ 1 ([| x |] + [| y |] + 1 - wB)); lia. - case (Z_lt_ge_dec ([| x |] + [| y |] + 1) wB). + intros hge; rewrite <- (Zmod_unique _ _ 1 (φ x + φ y + 1 - wB)); lia. + case (Z_lt_ge_dec (φ x + φ y + 1) wB). intros hlt; rewrite Zmod_small; lia. - intros hge; rewrite <- (Zmod_unique _ _ 1 ([| x |] + [| y |] + 1 - wB)); lia. + intros hge; rewrite <- (Zmod_unique _ _ 1 (φ x + φ y + 1 - wB)); lia. Qed. (** Subtraction *) -Lemma subc_spec x y : [-| x -c y |] = [| x |] - [| y |]. +Lemma subc_spec x y : [-| x -c y |] = φ x - φ y . Proof. rewrite subc_def_spec; unfold subc_def; unfold interp_carry. pose proof (to_Z_bounded x); pose proof (to_Z_bounded y). case lebP. intros hle; rewrite sub_spec, Z.mod_small; lia. - intros hgt; rewrite sub_spec, <- (Zmod_unique _ wB (-1) ([| x |] - [| y |] + wB)); lia. + intros hgt; rewrite sub_spec, <- (Zmod_unique _ wB (-1) (φ x - φ y + wB)); lia. Qed. -Lemma pred_spec x : [| pred x |] = ([| x |] - 1) mod wB. +Lemma pred_spec x : φ (pred x) = (φ x - 1) mod wB. Proof. apply sub_spec. Qed. -Lemma predc_spec x : [-| predc x |] = [| x |] - 1. +Lemma predc_spec x : [-| predc x |] = φ x - 1. Proof. apply subc_spec. Qed. -Lemma oppc_spec x : [-| oppc x |] = - [| x |]. +Lemma oppc_spec x : [-| oppc x |] = - φ x . Proof. unfold oppc; rewrite -> subc_spec, to_Z_0; trivial. Qed. -Lemma opp_spec x : [|- x |] = - [| x |] mod wB. +Lemma opp_spec x : φ (- x) = - φ x mod wB. Proof. unfold opp; rewrite -> sub_spec, to_Z_0; trivial. Qed. -Lemma oppcarry_spec x : [| oppcarry x |] = wB - [| x |] - 1. +Lemma oppcarry_spec x : φ (oppcarry x) = wB - φ x - 1. Proof. unfold oppcarry; rewrite sub_spec. rewrite <- Zminus_plus_distr, Zplus_comm, Zminus_plus_distr. @@ -645,20 +643,20 @@ Proof. generalize (to_Z_bounded x); auto with zarith. Qed. -Lemma subcarry_spec x y : [| subcarry x y |] = ([| x |] - [| y |] - 1) mod wB. +Lemma subcarry_spec x y : φ (subcarry x y) = (φ x - φ y - 1) mod wB. Proof. unfold subcarry; rewrite !sub_spec, Zminus_mod_idemp_l; trivial. Qed. -Lemma subcarryc_spec x y : [-| subcarryc x y |] = [| x |] - [| y |] - 1. +Lemma subcarryc_spec x y : [-| subcarryc x y |] = φ x - φ y - 1. Proof. rewrite subcarryc_def_spec; unfold subcarryc_def, interp_carry; fold (subcarry x y). pose proof (to_Z_bounded x); pose proof (to_Z_bounded y). case ltbP; rewrite subcarry_spec. intros hlt; rewrite Zmod_small; lia. - intros hge; rewrite <- (Zmod_unique _ _ (-1) ([| x |] - [| y |] - 1 + wB)); lia. + intros hge; rewrite <- (Zmod_unique _ _ (-1) (φ x - φ y - 1 + wB)); lia. Qed. (** GCD *) -Lemma to_Z_gcd : forall i j, [| gcd i j |] = Zgcdn (2 * size) [| j |] [| i |]. +Lemma to_Z_gcd : forall i j, φ (gcd i j) = Zgcdn (2 * size) (φ j) (φ i). Proof. unfold gcd. elim (2*size)%nat. reflexivity. @@ -668,17 +666,17 @@ Proof. intros ->; rewrite Z.abs_eq; lia. intros hne; rewrite ih; clear ih. rewrite <- mod_spec. - revert hj hne; case [| j |]; intros; lia. + revert hj hne; case φ j ; intros; lia. Qed. -Lemma gcd_spec a b : Zis_gcd [| a |] [| b |] [| gcd a b |]. +Lemma gcd_spec a b : Zis_gcd (φ a) (φ b) (φ (gcd a b)). Proof. rewrite to_Z_gcd. apply Zis_gcd_sym. apply Zgcdn_is_gcd. unfold Zgcd_bound. generalize (to_Z_bounded b). - destruct [|b|]. + destruct φ b. unfold size; auto with zarith. intros (_,H). cut (Psize p <= size)%nat; [ lia | rewrite <- Zpower2_Psize; auto]. @@ -686,10 +684,10 @@ Proof. Qed. (** Head0, Tail0 *) -Lemma head00_spec x : [| x |] = 0 -> [| head0 x |] = [| digits |]. +Lemma head00_spec x : φ x = 0 -> φ (head0 x) = φ digits . Proof. now intros h; rewrite (to_Z_inj _ 0 h). Qed. -Lemma tail00_spec x : [| x |] = 0 -> [|tail0 x|] = [|digits|]. +Lemma tail00_spec x : φ x = 0 -> φ (tail0 x) = φ digits. Proof. now intros h; rewrite (to_Z_inj _ 0 h). Qed. Infix "≡" := (eqm wB) (at level 80) : int63_scope. @@ -744,20 +742,20 @@ Proof. Qed. Lemma add_le_r m n: - if (n <= m + n)%int63 then ([|m|] + [|n|] < wB)%Z else (wB <= [|m|] + [|n|])%Z. + if (n <= m + n)%int63 then (φ m + φ n < wB)%Z else (wB <= φ m + φ n)%Z. Proof. case (to_Z_bounded m); intros H1m H2m. case (to_Z_bounded n); intros H1n H2n. - case (Zle_or_lt wB ([|m|] + [|n|])); intros H. - assert (H1: ([| m + n |] = [|m|] + [|n|] - wB)%Z). + case (Zle_or_lt wB (φ m + φ n)); intros H. + assert (H1: (φ (m + n) = φ m + φ n - wB)%Z). rewrite add_spec. - replace (([|m|] + [|n|]) mod wB)%Z with (((([|m|] + [|n|]) - wB) + wB) mod wB)%Z. + replace ((φ m + φ n) mod wB)%Z with ((((φ m + φ n) - wB) + wB) mod wB)%Z. rewrite -> Zplus_mod, Z_mod_same_full, Zplus_0_r, !Zmod_small; auto with zarith. rewrite !Zmod_small; auto with zarith. apply f_equal2 with (f := Zmod); auto with zarith. case_eq (n <= m + n)%int63; auto. rewrite leb_spec, H1; auto with zarith. - assert (H1: ([| m + n |] = [|m|] + [|n|])%Z). + assert (H1: (φ (m + n) = φ m + φ n)%Z). rewrite add_spec, Zmod_small; auto with zarith. replace (n <= m + n)%int63 with true; auto. apply sym_equal; rewrite leb_spec, H1; auto with zarith. @@ -844,40 +842,40 @@ Proof. rewrite -> leb_spec in H. apply Zdiv_small; split; [ auto | ]. apply (Z.lt_le_trans _ _ _ H2x). - unfold wB; change (Z_of_nat size) with [|digits|]. + unfold wB; change (Z_of_nat size) with φ digits. apply Zpower_le_monotone; auto with zarith. Qed. (* BIT *) -Lemma bit_0_spec i: [|bit i 0|] = [|i|] mod 2. +Lemma bit_0_spec i: φ (bit i 0) = φ i mod 2. Proof. unfold bit, is_zero. rewrite lsr_0_r. - assert (Hbi: ([|i|] mod 2 < 2)%Z). + assert (Hbi: (φ i mod 2 < 2)%Z). apply Z_mod_lt; auto with zarith. case (to_Z_bounded i); intros H1i H2i. - case (Zmod_le_first [|i|] 2); auto with zarith; intros H3i H4i. - assert (H2b: (0 < 2 ^ [|digits - 1|])%Z). + case (Zmod_le_first (φ i) 2); auto with zarith; intros H3i H4i. + assert (H2b: (0 < 2 ^ φ (digits - 1))%Z). apply Zpower_gt_0; auto with zarith. case (to_Z_bounded (digits -1)); auto with zarith. - assert (H: [|i << (digits -1)|] = ([|i|] mod 2 * 2^ [|digits -1|])%Z). + assert (H: φ (i << (digits -1)) = (φ i mod 2 * 2^ φ (digits -1))%Z). rewrite lsl_spec. - rewrite -> (Z_div_mod_eq [|i|] 2) at 1; auto with zarith. + rewrite -> (Z_div_mod_eq φ i 2) at 1; auto with zarith. rewrite -> Zmult_plus_distr_l, <-Zplus_mod_idemp_l. rewrite -> (Zmult_comm 2), <-Zmult_assoc. - replace (2 * 2 ^ [|digits - 1|])%Z with wB; auto. + replace (2 * 2 ^ φ (digits - 1))%Z with wB; auto. rewrite Z_mod_mult, Zplus_0_l; apply Zmod_small. split; auto with zarith. - replace wB with (2 * 2 ^ [|digits -1|])%Z; auto. + replace wB with (2 * 2 ^ φ (digits -1))%Z; auto. apply Zmult_lt_compat_r; auto with zarith. - case (Zle_lt_or_eq 0 ([|i|] mod 2)); auto with zarith; intros Hi. + case (Zle_lt_or_eq 0 (φ i mod 2)); auto with zarith; intros Hi. 2: generalize H; rewrite <-Hi, Zmult_0_l. - 2: replace 0%Z with [|0|]; auto. + 2: replace 0%Z with φ 0; auto. 2: now case eqbP. - generalize H; replace ([|i|] mod 2) with 1%Z; auto with zarith. + generalize H; replace (φ i mod 2) with 1%Z; auto with zarith. rewrite Zmult_1_l. intros H1. - assert (H2: [|i << (digits - 1)|] <> [|0|]). - replace [|0|] with 0%Z; auto with zarith. + assert (H2: φ (i << (digits - 1)) <> φ 0). + replace φ 0 with 0%Z; auto with zarith. now case eqbP. Qed. @@ -885,7 +883,7 @@ Lemma bit_split i : ( i = (i >> 1 ) << 1 + bit i 0)%int63. Proof. apply to_Z_inj. rewrite -> add_spec, lsl_spec, lsr_spec, bit_0_spec, Zplus_mod_idemp_l. - replace (2 ^ [|1|]) with 2%Z; auto with zarith. + replace (2 ^ φ 1) with 2%Z; auto with zarith. rewrite -> Zmult_comm, <-Z_div_mod_eq; auto with zarith. rewrite Zmod_small; auto; case (to_Z_bounded i); auto. Qed. @@ -911,11 +909,11 @@ Qed. Local Hint Resolve Z.lt_gt Z.div_pos : zarith. -Lemma to_Z_split x : [|x|] = [|(x >> 1)|] * 2 + [|bit x 0|]. +Lemma to_Z_split x : φ x = φ (x >> 1) * 2 + φ (bit x 0). Proof. case (to_Z_bounded x); intros H1x H2x. case (to_Z_bounded (bit x 0)); intros H1b H2b. - assert (F1: 0 <= [|x >> 1|] < wB/2). + assert (F1: 0 <= φ (x >> 1) < wB/2). rewrite -> lsr_spec, to_Z_1, Z.pow_1_r. split; auto with zarith. apply Zdiv_lt_upper_bound; auto with zarith. rewrite -> (bit_split x) at 1. @@ -927,7 +925,7 @@ Proof. rewrite -> lsl_spec, to_Z_1, Z.pow_1_r, Zmod_small; auto with zarith. 2: change wB with ((wB/2)*2); auto with zarith. change wB with (((wB/2 - 1) * 2 + 1) + 1). - assert ([|bit x 0|] <= 1); auto with zarith. + assert (φ (bit x 0) <= 1); auto with zarith. case bit; discriminate. Qed. @@ -944,11 +942,11 @@ Proof. intros H1; assert (H2: n = max_int). 2: generalize H; rewrite H2; discriminate. case (to_Z_bounded n); intros H1n H2n. - case (Zle_lt_or_eq [|n|] (wB - 1)); auto with zarith; + case (Zle_lt_or_eq φ n (wB - 1)); auto with zarith; intros H2; apply to_Z_inj; auto. generalize (add_le_r 1 n); rewrite H1. - change [|max_int|] with (wB - 1)%Z. - replace [|1|] with 1%Z; auto with zarith. + change φ max_int with (wB - 1)%Z. + replace φ 1 with 1%Z; auto with zarith. Qed. Lemma bit_ext i j : (forall n, bit i n = bit j n) -> i = j. @@ -964,7 +962,7 @@ Proof. 1, 3: apply to_Z_bounded. 1, 2: rewrite lsr_spec; auto using Z_lt_div2. intros b. - case (Zle_or_lt [|digits|] [|b|]). + case (Zle_or_lt φ digits φ b). rewrite <- leb_spec; intros; rewrite !bit_M; auto. rewrite <- ltb_spec; intros; rewrite !bit_half; auto. Qed. @@ -975,58 +973,58 @@ Proof. assert (F1: 1 >= 0) by discriminate. case_eq (digits <= j)%int63; intros H. rewrite orb_true_r, bit_M; auto. - set (d := [|digits|]). - case (Zle_or_lt d [|j|]); intros H1. + set (d := φ digits). + case (Zle_or_lt d (φ j)); intros H1. case (leb_spec digits j); rewrite H; auto with zarith. intros _ HH; generalize (HH H1); discriminate. clear H. generalize (ltb_spec j i); case ltb; intros H2; unfold bit; simpl. - assert (F2: ([|j|] < [|i|])%Z) by (case H2; auto); clear H2. + assert (F2: (φ j < φ i)%Z) by (case H2; auto); clear H2. replace (is_zero (((x << i) >> j) << (digits - 1))) with true; auto. case (to_Z_bounded j); intros H1j H2j. apply sym_equal; rewrite is_zero_spec; apply to_Z_inj. rewrite lsl_spec, lsr_spec, lsl_spec. replace wB with (2^d); auto. - pattern d at 1; replace d with ((d - ([|j|] + 1)) + ([|j|] + 1))%Z by ring. + pattern d at 1; replace d with ((d - (φ j + 1)) + (φ j + 1))%Z by ring. rewrite Zpower_exp; auto with zarith. - replace [|i|] with (([|i|] - ([|j|] + 1)) + ([|j|] + 1))%Z by ring. + replace φ i with ((φ i - (φ j + 1)) + (φ j + 1))%Z by ring. rewrite -> Zpower_exp, Zmult_assoc; auto with zarith. rewrite Zmult_mod_distr_r. rewrite -> Zplus_comm, Zpower_exp, !Zmult_assoc; auto with zarith. rewrite -> Z_div_mult_full; auto with zarith. rewrite <-Zmult_assoc, <-Zpower_exp; auto with zarith. - replace (1 + [|digits - 1|])%Z with d; auto with zarith. + replace (1 + φ digits - 1)%Z with d; auto with zarith. rewrite Z_mod_mult; auto. - case H2; intros _ H3; case (Zle_or_lt [|i|] [|j|]); intros F2. + case H2; intros _ H3; case (Zle_or_lt φ i φ j); intros F2. 2: generalize (H3 F2); discriminate. clear H2 H3. apply f_equal with (f := negb). apply f_equal with (f := is_zero). apply to_Z_inj. rewrite -> !lsl_spec, !lsr_spec, !lsl_spec. - pattern wB at 2 3; replace wB with (2^(1+ [|digits - 1|])); auto. + pattern wB at 2 3; replace wB with (2^(1+ φ (digits - 1))); auto. rewrite -> Zpower_exp, Z.pow_1_r; auto with zarith. rewrite !Zmult_mod_distr_r. apply f_equal2 with (f := Zmult); auto. replace wB with (2^ d); auto with zarith. - replace d with ((d - [|i|]) + [|i|])%Z by ring. + replace d with ((d - φ i) + φ i)%Z by ring. case (to_Z_bounded i); intros H1i H2i. rewrite Zpower_exp; auto with zarith. rewrite Zmult_mod_distr_r. case (to_Z_bounded j); intros H1j H2j. - replace [|j - i|] with ([|j|] - [|i|])%Z. + replace φ (j - i) with (φ j - φ i)%Z. 2: rewrite sub_spec, Zmod_small; auto with zarith. - set (d1 := (d - [|i|])%Z). - set (d2 := ([|j|] - [|i|])%Z). - pattern [|j|] at 1; - replace [|j|] with (d2 + [|i|])%Z. + set (d1 := (d - φ i)%Z). + set (d2 := (φ j - φ i)%Z). + pattern φ j at 1; + replace φ j with (d2 + φ i)%Z. 2: unfold d2; ring. rewrite -> Zpower_exp; auto with zarith. rewrite -> Zdiv_mult_cancel_r. - 2: generalize (Zpower2_lt_lin [| i |] H1i); auto with zarith. - rewrite -> (Z_div_mod_eq [|x|] (2^d1)) at 2; auto with zarith. + 2: generalize (Zpower2_lt_lin φ i H1i); auto with zarith. + rewrite -> (Z_div_mod_eq φ x (2^d1)) at 2; auto with zarith. pattern d1 at 2; - replace d1 with (d2 + (1+ (d - [|j|] - 1)))%Z + replace d1 with (d2 + (1+ (d - φ j - 1)))%Z by (unfold d1, d2; ring). rewrite Zpower_exp; auto with zarith. rewrite <-Zmult_assoc, Zmult_comm. @@ -1058,13 +1056,13 @@ Proof. intros Hx Hy. rewrite leb_spec. rewrite -> (to_Z_split y) at 1; rewrite (to_Z_split (x lor y)). - assert ([|y>>1|] <= [|(x lor y) >> 1|]). + assert (φ (y>>1) <= φ ((x lor y) >> 1)). rewrite -> lor_lsr, <-leb_spec; apply IH. rewrite -> lsr_spec, to_Z_1, Z.pow_1_r; split; auto with zarith. apply Zdiv_lt_upper_bound; auto with zarith. rewrite -> lsr_spec, to_Z_1, Z.pow_1_r; split; auto with zarith. apply Zdiv_lt_upper_bound; auto with zarith. - assert ([|bit y 0|] <= [|bit (x lor y) 0|]); auto with zarith. + assert (φ (bit y 0) <= φ (bit (x lor y) 0)); auto with zarith. rewrite lor_spec; do 2 case bit; try discriminate. Qed. @@ -1118,8 +1116,8 @@ Proof. assert (F: (bit x 0 + bit y 0)%int63 = (bit x 0 || bit y 0)). assert (F1: (2 | wB)) by (apply Zpower_divide; apply refl_equal). assert (F2: 0 < wB) by (apply refl_equal). - assert (F3: [|bit x 0 + bit y 0|] mod 2 = [|bit x 0 || bit y 0|] mod 2). - apply trans_equal with (([|(x>>1 + y>>1) << 1|] + [|bit x 0 + bit y 0|]) mod 2). + assert (F3: φ (bit x 0 + bit y 0) mod 2 = φ (bit x 0 || bit y 0) mod 2). + apply trans_equal with ((φ ((x>>1 + y>>1) << 1) + φ (bit x 0 + bit y 0)) mod 2). rewrite lsl_spec, Zplus_mod, <-Zmod_div_mod; auto with zarith. rewrite Z.pow_1_r, Z_mod_mult, Zplus_0_l, Zmod_mod; auto with zarith. rewrite (Zmod_div_mod 2 wB), <-add_spec, Heq; auto with zarith. @@ -1136,12 +1134,12 @@ Proof. case_eq (digits <= m)%int63. intros Hlm; rewrite bit_M; auto; discriminate. rewrite <- not_true_iff_false, leb_spec; intros Hlm. - case (Zle_lt_or_eq 0 [|m|]); auto; intros Hm. + case (Zle_lt_or_eq 0 φ m); auto; intros Hm. replace m with ((m -1) + 1)%int63. rewrite <-(bit_half x), <-(bit_half y); auto with zarith. apply HH. rewrite <-lor_lsr. - assert (0 <= [|bit (x lor y) 0|] <= 1) by (case bit; split; discriminate). + assert (0 <= φ (bit (x lor y) 0) <= 1) by (case bit; split; discriminate). rewrite F in Heq; generalize (add_cancel_r _ _ _ Heq). intros Heq1; apply to_Z_inj. generalize (f_equal to_Z Heq1); rewrite lsl_spec, to_Z_1, Z.pow_1_r, Zmod_small. @@ -1149,13 +1147,13 @@ Proof. case (to_Z_bounded (x lor y)); intros H1xy H2xy. rewrite lsr_spec, to_Z_1, Z.pow_1_r; auto with zarith. change wB with ((wB/2)*2); split; auto with zarith. - assert ([|x lor y|] / 2 < wB / 2); auto with zarith. + assert (φ (x lor y) / 2 < wB / 2); auto with zarith. apply Zdiv_lt_upper_bound; auto with zarith. split. case (to_Z_bounded (x >> 1 + y >> 1)); auto with zarith. rewrite add_spec. - apply Z.le_lt_trans with (([|x >> 1|] + [|y >> 1|]) * 2); auto with zarith. - case (Zmod_le_first ([|x >> 1|] + [|y >> 1|]) wB); auto with zarith. + apply Z.le_lt_trans with ((φ (x >> 1) + φ (y >> 1)) * 2); auto with zarith. + case (Zmod_le_first (φ (x >> 1) + φ (y >> 1)) wB); auto with zarith. case (to_Z_bounded (x >> 1)); case (to_Z_bounded (y >> 1)); auto with zarith. generalize Hb; rewrite (to_Z_split x) at 1; rewrite (to_Z_split y) at 1. case (to_Z_bounded (bit x 0)); case (to_Z_bounded (bit y 0)); auto with zarith. @@ -1168,8 +1166,8 @@ Proof. Qed. Lemma addmuldiv_spec x y p : - [| p |] <= [| digits |] -> - [| addmuldiv p x y |] = ([| x |] * (2 ^ [| p |]) + [| y |] / (2 ^ ([| digits |] - [| p |]))) mod wB. + φ p <= φ digits -> + φ (addmuldiv p x y) = (φ x * (2 ^ φ p) + φ y / (2 ^ (φ digits - φ p))) mod wB. Proof. intros H. assert (Fp := to_Z_bounded p); assert (Fd := to_Z_bounded digits). @@ -1203,7 +1201,7 @@ Proof. rewrite andb_false_r; auto. Qed. -Lemma is_even_spec x : if is_even x then [|x|] mod 2 = 0 else [|x|] mod 2 = 1. +Lemma is_even_spec x : if is_even x then φ x mod 2 = 0 else φ x mod 2 = 1. Proof. rewrite is_even_bit. generalize (bit_0_spec x); case bit; simpl; auto. @@ -1283,39 +1281,39 @@ Proof. Qed. Lemma sqrt_step_correct rec i j: - 0 < [|i|] -> 0 < [|j|] -> [|i|] < ([|j|] + 1) ^ 2 -> - 2 * [|j|] < wB -> + 0 < φ i -> 0 < φ j -> φ i < (φ j + 1) ^ 2 -> + 2 * φ j < wB -> (forall j1 : int, - 0 < [|j1|] < [|j|] -> [|i|] < ([|j1|] + 1) ^ 2 -> - [|rec i j1|] ^ 2 <= [|i|] < ([|rec i j1|] + 1) ^ 2) -> - [|sqrt_step rec i j|] ^ 2 <= [|i|] < ([|sqrt_step rec i j|] + 1) ^ 2. + 0 < φ j1 < φ j -> φ i < (φ j1 + 1) ^ 2 -> + φ (rec i j1) ^ 2 <= φ i < (φ (rec i j1) + 1) ^ 2) -> + φ (sqrt_step rec i j) ^ 2 <= φ i < (φ (sqrt_step rec i j) + 1) ^ 2. Proof. - assert (Hp2: 0 < [|2|]) by exact (refl_equal Lt). + assert (Hp2: 0 < φ 2) by exact (refl_equal Lt). intros Hi Hj Hij H31 Hrec. unfold sqrt_step. case ltbP; rewrite div_spec. - intros hlt. - assert ([| j + i / j|] = [|j|] + [|i|]/[|j|]) as hj. + assert (φ (j + i / j) = φ j + φ i/φ j) as hj. rewrite add_spec, Zmod_small;rewrite div_spec; auto with zarith. apply Hrec; rewrite lsr_spec, hj, to_Z_1; change (2 ^ 1) with 2. + split; [ | apply sqrt_test_false;auto with zarith]. - replace ([|j|] + [|i|]/[|j|]) with (1 * 2 + (([|j|] - 2) + [|i|] / [|j|])) by ring. + replace (φ j + φ i/φ j) with (1 * 2 + ((φ j - 2) + φ i / φ j)) by ring. rewrite Z_div_plus_full_l; auto with zarith. - assert (0 <= [|i|]/ [|j|]) by (apply Z_div_pos; auto with zarith). - assert (0 <= ([|j|] - 2 + [|i|] / [|j|]) / 2) ; auto with zarith. + assert (0 <= φ i/ φ j) by (apply Z_div_pos; auto with zarith). + assert (0 <= (φ j - 2 + φ i / φ j) / 2) ; auto with zarith. apply Z.div_pos; [ | lia ]. - case (Zle_lt_or_eq 1 [|j|]); auto with zarith; intros Hj1. + case (Zle_lt_or_eq 1 φ j); auto with zarith; intros Hj1. rewrite <- Hj1, Zdiv_1_r; lia. + apply sqrt_main;auto with zarith. - split;[apply sqrt_test_true | ];auto with zarith. Qed. -Lemma iter_sqrt_correct n rec i j: 0 < [|i|] -> 0 < [|j|] -> - [|i|] < ([|j|] + 1) ^ 2 -> 2 * [|j|] < wB -> - (forall j1, 0 < [|j1|] -> 2^(Z_of_nat n) + [|j1|] <= [|j|] -> - [|i|] < ([|j1|] + 1) ^ 2 -> 2 * [|j1|] < wB -> - [|rec i j1|] ^ 2 <= [|i|] < ([|rec i j1|] + 1) ^ 2) -> - [|iter_sqrt n rec i j|] ^ 2 <= [|i|] < ([|iter_sqrt n rec i j|] + 1) ^ 2. +Lemma iter_sqrt_correct n rec i j: 0 < φ i -> 0 < φ j -> + φ i < (φ j + 1) ^ 2 -> 2 * φ j < wB -> + (forall j1, 0 < φ j1 -> 2^(Z_of_nat n) + φ j1 <= φ j -> + φ i < (φ j1 + 1) ^ 2 -> 2 * φ j1 < wB -> + φ (rec i j1) ^ 2 <= φ i < (φ (rec i j1) + 1) ^ 2) -> + φ (iter_sqrt n rec i j) ^ 2 <= φ i < (φ (iter_sqrt n rec i j) + 1) ^ 2. Proof. revert rec i j; elim n; unfold iter_sqrt; fold iter_sqrt; clear n. intros rec i j Hi Hj Hij H31 Hrec; apply sqrt_step_correct; auto with zarith. @@ -1328,7 +1326,7 @@ Proof. intros j3 Hj3 Hpj3. apply HHrec; auto. rewrite -> inj_S, Z.pow_succ_r. - apply Z.le_trans with (2 ^Z_of_nat n + [|j2|]); auto with zarith. + apply Z.le_trans with (2 ^Z_of_nat n + φ j2); auto with zarith. apply Zle_0_nat. Qed. @@ -1351,7 +1349,7 @@ Proof. Qed. Lemma sqrt_spec : forall x, - [|sqrt x|] ^ 2 <= [|x|] < ([|sqrt x|] + 1) ^ 2. + φ (sqrt x) ^ 2 <= φ x < (φ (sqrt x) + 1) ^ 2. Proof. intros i; unfold sqrt. rewrite compare_spec. case Z.compare_spec; rewrite to_Z_1; @@ -1359,16 +1357,16 @@ Proof. lia. apply iter_sqrt_correct; auto with zarith; rewrite lsr_spec, to_Z_1; change (2^1) with 2; auto with zarith. - replace [|i|] with (1 * 2 + ([|i|] - 2))%Z; try ring. - assert (0 <= ([|i|] - 2)/2)%Z by (apply Z_div_pos; auto with zarith). + replace φ i with (1 * 2 + (φ i - 2))%Z; try ring. + assert (0 <= (φ i - 2)/2)%Z by (apply Z_div_pos; auto with zarith). rewrite Z_div_plus_full_l; auto with zarith. apply sqrt_init; auto. - assert (W:= Z_mult_div_ge [|i|] 2);assert (W':= to_Z_bounded i);auto with zarith. + assert (W:= Z_mult_div_ge φ i 2);assert (W':= to_Z_bounded i);auto with zarith. intros j2 H1 H2; contradict H2; apply Zlt_not_le. fold wB;assert (W:=to_Z_bounded i). - apply Z.le_lt_trans with ([|i|]); auto with zarith. - assert (0 <= [|i|]/2)%Z by (apply Z_div_pos; auto with zarith). - apply Z.le_trans with (2 * ([|i|]/2)); auto with zarith. + apply Z.le_lt_trans with (φ i); auto with zarith. + assert (0 <= φ i/2)%Z by (apply Z_div_pos; auto with zarith). + apply Z.le_trans with (2 * (φ i/2)); auto with zarith. apply Z_mult_div_ge; auto with zarith. case (to_Z_bounded i); repeat rewrite Z.pow_2_r; auto with zarith. Qed. @@ -1393,66 +1391,66 @@ Proof. Qed. Lemma sqrt2_lower_bound ih il j: - [|| WW ih il||] < ([|j|] + 1) ^ 2 -> [|ih|] <= [|j|]. + Φ (WW ih il) < (φ j + 1) ^ 2 -> φ ih <= φ j. Proof. intros H1. case (to_Z_bounded j); intros Hbj _. case (to_Z_bounded il); intros Hbil _. case (to_Z_bounded ih); intros Hbih Hbih1. - assert (([|ih|] < [|j|] + 1)%Z); auto with zarith. + assert ((φ ih < φ j + 1)%Z); auto with zarith. apply Zlt_square_simpl; auto with zarith. simpl zn2z_to_Z in H1. repeat rewrite <-Z.pow_2_r. refine (Z.le_lt_trans _ _ _ _ H1). - apply Z.le_trans with ([|ih|] * wB)%Z;try rewrite Z.pow_2_r; auto with zarith. + apply Z.le_trans with (φ ih * wB)%Z;try rewrite Z.pow_2_r; auto with zarith. Qed. Lemma diveucl_21_spec_aux : forall a1 a2 b, - wB/2 <= [|b|] -> - [|a1|] < [|b|] -> + wB/2 <= φ b -> + φ a1 < φ b -> let (q,r) := diveucl_21 a1 a2 b in - [|a1|] *wB+ [|a2|] = [|q|] * [|b|] + [|r|] /\ - 0 <= [|r|] < [|b|]. + φ a1 *wB+ φ a2 = φ q * φ b + φ r /\ + 0 <= φ r < φ b. Proof. intros a1 a2 b H1 H2;assert (W:= diveucl_21_spec a1 a2 b). assert (W1:= to_Z_bounded a1). assert (W2:= to_Z_bounded a2). assert (Wb:= to_Z_bounded b). - assert ([|b|]>0) by (auto with zarith). - generalize (Z_div_mod ([|a1|]*wB+[|a2|]) [|b|] H). + assert (φ b>0) by (auto with zarith). + generalize (Z_div_mod (φ a1*wB+φ a2) φ b H). revert W. - destruct (diveucl_21 a1 a2 b); destruct (Z.div_eucl ([|a1|]*wB+[|a2|]) [|b|]). + destruct (diveucl_21 a1 a2 b); destruct (Z.div_eucl (φ a1*wB+φ a2) φ b). intros (H', H''); auto; rewrite H', H''; clear H' H''. intros (H', H''); split; [ |exact H'']. now rewrite H', Zmult_comm. Qed. -Lemma div2_phi ih il j: (2^62 <= [|j|] -> [|ih|] < [|j|] -> - [|fst (diveucl_21 ih il j)|] = [|| WW ih il||] /[|j|])%Z. +Lemma div2_phi ih il j: (2^62 <= φ j -> φ ih < φ j -> + φ (fst (diveucl_21 ih il j)) = Φ (WW ih il) / φ j)%Z. Proof. intros Hj Hj1. generalize (diveucl_21_spec_aux ih il j Hj Hj1). case diveucl_21; intros q r (Hq, Hr). - apply Zdiv_unique with [|r|]; auto with zarith. + apply Zdiv_unique with φ r; auto with zarith. simpl @fst; apply eq_trans with (1 := Hq); ring. Qed. Lemma sqrt2_step_correct rec ih il j: - 2 ^ (Z_of_nat (size - 2)) <= [|ih|] -> - 0 < [|j|] -> [|| WW ih il||] < ([|j|] + 1) ^ 2 -> - (forall j1, 0 < [|j1|] < [|j|] -> [|| WW ih il||] < ([|j1|] + 1) ^ 2 -> - [|rec ih il j1|] ^ 2 <= [||WW ih il||] < ([|rec ih il j1|] + 1) ^ 2) -> - [|sqrt2_step rec ih il j|] ^ 2 <= [||WW ih il ||] - < ([|sqrt2_step rec ih il j|] + 1) ^ 2. -Proof. - assert (Hp2: (0 < [|2|])%Z) by exact (refl_equal Lt). + 2 ^ (Z_of_nat (size - 2)) <= φ ih -> + 0 < φ j -> Φ (WW ih il) < (φ j + 1) ^ 2 -> + (forall j1, 0 < φ j1 < φ j -> Φ (WW ih il) < (φ j1 + 1) ^ 2 -> + φ (rec ih il j1) ^ 2 <= Φ (WW ih il) < (φ (rec ih il j1) + 1) ^ 2) -> + φ (sqrt2_step rec ih il j) ^ 2 <= Φ (WW ih il) + < (φ (sqrt2_step rec ih il j) + 1) ^ 2. +Proof. + assert (Hp2: (0 < φ 2)%Z) by exact (refl_equal Lt). intros Hih Hj Hij Hrec; rewrite sqrt2_step_def. - assert (H1: ([|ih|] <= [|j|])%Z) by (apply sqrt2_lower_bound with il; auto). + assert (H1: (φ ih <= φ j)%Z) by (apply sqrt2_lower_bound with il; auto). case (to_Z_bounded ih); intros Hih1 _. case (to_Z_bounded il); intros Hil1 _. case (to_Z_bounded j); intros _ Hj1. - assert (Hp3: (0 < [||WW ih il||])). - {simpl zn2z_to_Z;apply Z.lt_le_trans with ([|ih|] * wB)%Z; auto with zarith. + assert (Hp3: (0 < Φ (WW ih il))). + {simpl zn2z_to_Z;apply Z.lt_le_trans with (φ ih * wB)%Z; auto with zarith. apply Zmult_lt_0_compat; auto with zarith. refine (Z.lt_le_trans _ _ _ _ Hih); auto with zarith. } cbv zeta. @@ -1461,10 +1459,10 @@ Proof. 2: rewrite <-not_true_iff_false, ltb_spec in Heq. 2: split; auto. 2: apply sqrt_test_true; auto with zarith. - 2: unfold zn2z_to_Z; replace [|ih|] with [|j|]; auto with zarith. - 2: assert (0 <= [|il|]/[|j|]) by (apply Z_div_pos; auto with zarith). + 2: unfold zn2z_to_Z; replace φ ih with φ j; auto with zarith. + 2: assert (0 <= φ il/φ j) by (apply Z_div_pos; auto with zarith). 2: rewrite Zmult_comm, Z_div_plus_full_l; unfold base; auto with zarith. - case (Zle_or_lt (2^(Z_of_nat size -1)) [|j|]); intros Hjj. + case (Zle_or_lt (2^(Z_of_nat size -1)) φ j); intros Hjj. case_eq (fst (diveucl_21 ih il j) < j)%int63;intros Heq0. 2: rewrite <-not_true_iff_false, ltb_spec, (div2_phi _ _ _ Hjj Heq) in Heq0. 2: split; auto; apply sqrt_test_true; auto with zarith. @@ -1472,50 +1470,50 @@ Proof. match goal with |- context[rec _ _ ?X] => set (u := X) end. - assert (H: [|u|] = ([|j|] + ([||WW ih il||])/([|j|]))/2). + assert (H: φ u = (φ j + (Φ (WW ih il))/(φ j))/2). { unfold u; generalize (addc_spec j (fst (diveucl_21 ih il j))); case addc;unfold interp_carry;rewrite (div2_phi _ _ _ Hjj Heq);simpl zn2z_to_Z. { intros i H;rewrite lsr_spec, H;trivial. } intros i H;rewrite <- H. case (to_Z_bounded i); intros H1i H2i. rewrite -> add_spec, Zmod_small, lsr_spec. - { change (1 * wB) with ([|(1 << (digits -1))|] * 2)%Z. + { change (1 * wB) with (φ (1 << (digits -1)) * 2)%Z. rewrite Z_div_plus_full_l; auto with zarith. } change wB with (2 * (wB/2))%Z; auto. - replace [|(1 << (digits - 1))|] with (wB/2); auto. + replace φ (1 << (digits - 1)) with (wB/2); auto. rewrite lsr_spec; auto. - replace (2^[|1|]) with 2%Z; auto. + replace (2^φ 1) with 2%Z; auto. split; auto with zarith. - assert ([|i|]/2 < wB/2); auto with zarith. + assert (φ i/2 < wB/2); auto with zarith. apply Zdiv_lt_upper_bound; auto with zarith. } apply Hrec; rewrite H; clear u H. - assert (Hf1: 0 <= [||WW ih il||]/ [|j|]) by (apply Z_div_pos; auto with zarith). - case (Zle_lt_or_eq 1 ([|j|])); auto with zarith; intros Hf2. + assert (Hf1: 0 <= Φ (WW ih il) / φ j) by (apply Z_div_pos; auto with zarith). + case (Zle_lt_or_eq 1 (φ j)); auto with zarith; intros Hf2. 2: contradict Heq0; apply Zle_not_lt; rewrite <- Hf2, Zdiv_1_r; auto with zarith. split. - replace ([|j|] + [||WW ih il||]/ [|j|])%Z with - (1 * 2 + (([|j|] - 2) + [||WW ih il||] / [|j|])) by lia. + replace (φ j + Φ (WW ih il) / φ j)%Z with + (1 * 2 + ((φ j - 2) + Φ (WW ih il) / φ j)) by lia. rewrite Z_div_plus_full_l; auto with zarith. - assert (0 <= ([|j|] - 2 + [||WW ih il||] / [|j|]) / 2) ; auto with zarith. + assert (0 <= (φ j - 2 + Φ (WW ih il) / φ j) / 2) ; auto with zarith. apply sqrt_test_false; auto with zarith. apply sqrt_main; auto with zarith. contradict Hij; apply Zle_not_lt. - assert ((1 + [|j|]) <= 2 ^ (Z_of_nat size - 1)); auto with zarith. + assert ((1 + φ j) <= 2 ^ (Z_of_nat size - 1)); auto with zarith. apply Z.le_trans with ((2 ^ (Z_of_nat size - 1)) ^2); auto with zarith. - assert (0 <= 1 + [|j|]); auto with zarith. + assert (0 <= 1 + φ j); auto with zarith. apply Zmult_le_compat; auto with zarith. change ((2 ^ (Z_of_nat size - 1))^2) with (2 ^ (Z_of_nat size - 2) * wB). - apply Z.le_trans with ([|ih|] * wB); auto with zarith. + apply Z.le_trans with (φ ih * wB); auto with zarith. unfold zn2z_to_Z, wB; auto with zarith. Qed. Lemma iter2_sqrt_correct n rec ih il j: - 2^(Z_of_nat (size - 2)) <= [|ih|] -> 0 < [|j|] -> [||WW ih il||] < ([|j|] + 1) ^ 2 -> - (forall j1, 0 < [|j1|] -> 2^(Z_of_nat n) + [|j1|] <= [|j|] -> - [||WW ih il||] < ([|j1|] + 1) ^ 2 -> - [|rec ih il j1|] ^ 2 <= [||WW ih il||] < ([|rec ih il j1|] + 1) ^ 2) -> - [|iter2_sqrt n rec ih il j|] ^ 2 <= [||WW ih il||] - < ([|iter2_sqrt n rec ih il j|] + 1) ^ 2. + 2^(Z_of_nat (size - 2)) <= φ ih -> 0 < φ j -> Φ (WW ih il) < (φ j + 1) ^ 2 -> + (forall j1, 0 < φ j1 -> 2^(Z_of_nat n) + φ j1 <= φ j -> + Φ (WW ih il) < (φ j1 + 1) ^ 2 -> + φ (rec ih il j1) ^ 2 <= Φ (WW ih il) < (φ (rec ih il j1) + 1) ^ 2) -> + φ (iter2_sqrt n rec ih il j) ^ 2 <= Φ (WW ih il) + < (φ (iter2_sqrt n rec ih il j) + 1) ^ 2. Proof. revert rec ih il j; elim n; unfold iter2_sqrt; fold iter2_sqrt; clear n. intros rec ih il j Hi Hj Hij Hrec; apply sqrt2_step_correct; auto with zarith. @@ -1528,22 +1526,22 @@ Proof. intros j3 Hj3 Hpj3. apply HHrec; auto. rewrite -> inj_S, Z.pow_succ_r. - apply Z.le_trans with (2 ^Z_of_nat n + [|j2|])%Z; auto with zarith. + apply Z.le_trans with (2 ^Z_of_nat n + φ j2)%Z; auto with zarith. apply Zle_0_nat. Qed. Lemma sqrt2_spec : forall x y, - wB/ 4 <= [|x|] -> + wB/ 4 <= φ x -> let (s,r) := sqrt2 x y in - [||WW x y||] = [|s|] ^ 2 + [+|r|] /\ - [+|r|] <= 2 * [|s|]. + Φ (WW x y) = φ s ^ 2 + [+|r|] /\ + [+|r|] <= 2 * φ s. Proof. intros ih il Hih; unfold sqrt2. - change [||WW ih il||] with ([||WW ih il||]). + change Φ (WW ih il) with (Φ(WW ih il)). assert (Hbin: forall s, s * s + 2* s + 1 = (s + 1) ^ 2) by (intros s; ring). assert (Hb: 0 <= wB) by (red; intros HH; discriminate). - assert (Hi2: [||WW ih il ||] < ([|max_int|] + 1) ^ 2). + assert (Hi2: Φ(WW ih il ) < (φ max_int + 1) ^ 2). apply Z.le_lt_trans with ((wB - 1) * wB + (wB - 1)); auto with zarith. 2: apply refl_equal. case (to_Z_bounded ih); case (to_Z_bounded il); intros H1 H2 H3 H4. @@ -1553,7 +1551,7 @@ Lemma sqrt2_spec : forall x y, intros j1 _ HH; contradict HH. apply Zlt_not_le. case (to_Z_bounded j1); auto with zarith. - change (2 ^ Z_of_nat size) with ([|max_int|]+1)%Z; auto with zarith. + change (2 ^ Z_of_nat size) with (φ max_int+1)%Z; auto with zarith. set (s := iter2_sqrt size (fun _ _ j : int=> j) ih il max_int). intros Hs1 Hs2. generalize (mulc_spec s s); case mulc. @@ -1565,104 +1563,104 @@ Lemma sqrt2_spec : forall x y, rewrite ltb_spec; intros Heq. unfold interp_carry; rewrite Zmult_1_l. rewrite -> Z.pow_2_r, Hihl1, Hil2. - case (Zle_lt_or_eq ([|ih1|] + 1) ([|ih|])); auto with zarith. + case (Zle_lt_or_eq (φ ih1 + 1) (φ ih)); auto with zarith. intros H2; contradict Hs2; apply Zle_not_lt. - replace (([|s|] + 1) ^ 2) with ([||WW ih1 il1||] + 2 * [|s|] + 1). + replace ((φ s + 1) ^ 2) with (Φ(WW ih1 il1) + 2 * φ s + 1). unfold zn2z_to_Z. case (to_Z_bounded il); intros Hpil _. - assert (Hl1l: [|il1|] <= [|il|]). + assert (Hl1l: φ il1 <= φ il). case (to_Z_bounded il2); rewrite Hil2; auto with zarith. - enough ([|ih1|] * wB + 2 * [|s|] + 1 <= [|ih|] * wB) by lia. + enough (φ ih1 * wB + 2 * φ s + 1 <= φ ih * wB) by lia. case (to_Z_bounded s); intros _ Hps. case (to_Z_bounded ih1); intros Hpih1 _. - apply Z.le_trans with (([|ih1|] + 2) * wB). lia. + apply Z.le_trans with ((φ ih1 + 2) * wB). lia. auto with zarith. unfold zn2z_to_Z; rewrite <-Hihl1, Hbin; auto. intros H2; split. unfold zn2z_to_Z; rewrite <- H2; ring. - replace (wB + ([|il|] - [|il1|])) with ([||WW ih il||] - ([|s|] * [|s|])). + replace (wB + (φ il - φ il1)) with (Φ(WW ih il) - (φ s * φ s)). rewrite <-Hbin in Hs2; auto with zarith. rewrite Hihl1; unfold zn2z_to_Z; rewrite <- H2; ring. unfold interp_carry. - case (Zle_lt_or_eq [|ih|] [|ih1|]); auto with zarith; intros H. + case (Zle_lt_or_eq φ ih φ ih1); auto with zarith; intros H. contradict Hs1. apply Zlt_not_le; rewrite Z.pow_2_r, Hihl1. unfold zn2z_to_Z. case (to_Z_bounded il); intros _ H2. - apply Z.lt_le_trans with (([|ih|] + 1) * wB + 0). + apply Z.lt_le_trans with ((φ ih + 1) * wB + 0). rewrite Zmult_plus_distr_l, Zplus_0_r; auto with zarith. case (to_Z_bounded il1); intros H3 _. apply Zplus_le_compat; auto with zarith. split. rewrite Z.pow_2_r, Hihl1. unfold zn2z_to_Z; ring[Hil2 H]. - replace [|il2|] with ([||WW ih il||] - [||WW ih1 il1||]). + replace φ il2 with (Φ(WW ih il) - Φ(WW ih1 il1)). unfold zn2z_to_Z at 2; rewrite <-Hihl1. rewrite <-Hbin in Hs2; auto with zarith. unfold zn2z_to_Z; rewrite H, Hil2; ring. unfold interp_carry in Hil2 |- *. - assert (Hsih: [|ih - 1|] = [|ih|] - 1). - rewrite sub_spec, Zmod_small; auto; replace [|1|] with 1; auto. + assert (Hsih: φ (ih - 1) = φ ih - 1). + rewrite sub_spec, Zmod_small; auto; replace φ 1 with 1; auto. case (to_Z_bounded ih); intros H1 H2. split; auto with zarith. apply Z.le_trans with (wB/4 - 1); auto with zarith. case_eq (ih1 < ih - 1)%int63; [idtac | rewrite <- not_true_iff_false]; rewrite ltb_spec, Hsih; intros Heq. rewrite Z.pow_2_r, Hihl1. - case (Zle_lt_or_eq ([|ih1|] + 2) [|ih|]); auto with zarith. + case (Zle_lt_or_eq (φ ih1 + 2) φ ih); auto with zarith. intros H2; contradict Hs2; apply Zle_not_lt. - replace (([|s|] + 1) ^ 2) with ([||WW ih1 il1||] + 2 * [|s|] + 1). + replace ((φ s + 1) ^ 2) with (Φ(WW ih1 il1) + 2 * φ s + 1). unfold zn2z_to_Z. - assert ([|ih1|] * wB + 2 * [|s|] + 1 <= [|ih|] * wB + ([|il|] - [|il1|])); + assert (φ ih1 * wB + 2 * φ s + 1 <= φ ih * wB + (φ il - φ il1)); auto with zarith. rewrite <-Hil2. case (to_Z_bounded il2); intros Hpil2 _. - apply Z.le_trans with ([|ih|] * wB + - wB); auto with zarith. + apply Z.le_trans with (φ ih * wB + - wB); auto with zarith. case (to_Z_bounded s); intros _ Hps. - assert (2 * [|s|] + 1 <= 2 * wB); auto with zarith. - apply Z.le_trans with ([|ih1|] * wB + 2 * wB); auto with zarith. - assert (Hi: ([|ih1|] + 3) * wB <= [|ih|] * wB) by auto with zarith. + assert (2 * φ s + 1 <= 2 * wB); auto with zarith. + apply Z.le_trans with (φ ih1 * wB + 2 * wB); auto with zarith. + assert (Hi: (φ ih1 + 3) * wB <= φ ih * wB) by auto with zarith. lia. unfold zn2z_to_Z; rewrite <-Hihl1, Hbin; auto. intros H2; unfold zn2z_to_Z; rewrite <-H2. split. - replace [|il|] with (([|il|] - [|il1|]) + [|il1|]); try ring. + replace φ il with ((φ il - φ il1) + φ il1); try ring. rewrite <-Hil2; ring. - replace (1 * wB + [|il2|]) with ([||WW ih il||] - [||WW ih1 il1||]). + replace (1 * wB + φ il2) with (Φ(WW ih il) - Φ(WW ih1 il1)). unfold zn2z_to_Z at 2; rewrite <-Hihl1. rewrite <-Hbin in Hs2; auto with zarith. unfold zn2z_to_Z; rewrite <-H2. - replace [|il|] with (([|il|] - [|il1|]) + [|il1|]); try ring. + replace φ il with ((φ il - φ il1) + φ il1); try ring. rewrite <-Hil2; ring. - case (Zle_lt_or_eq ([|ih|] - 1) ([|ih1|])); auto with zarith; intros H1. - assert (He: [|ih|] = [|ih1|]). + case (Zle_lt_or_eq (φ ih - 1) (φ ih1)); auto with zarith; intros H1. + assert (He: φ ih = φ ih1). apply Zle_antisym; auto with zarith. - case (Zle_or_lt [|ih1|] [|ih|]); auto; intros H2. + case (Zle_or_lt φ ih1 φ ih); auto; intros H2. contradict Hs1; apply Zlt_not_le; rewrite Z.pow_2_r, Hihl1. unfold zn2z_to_Z. case (to_Z_bounded il); intros _ Hpil1. - apply Z.lt_le_trans with (([|ih|] + 1) * wB). + apply Z.lt_le_trans with ((φ ih + 1) * wB). rewrite Zmult_plus_distr_l, Zmult_1_l; auto with zarith. case (to_Z_bounded il1); intros Hpil2 _. - apply Z.le_trans with (([|ih1|]) * wB); auto with zarith. + apply Z.le_trans with ((φ ih1) * wB); auto with zarith. contradict Hs1; apply Zlt_not_le; rewrite Z.pow_2_r, Hihl1. unfold zn2z_to_Z; rewrite He. - assert ([|il|] - [|il1|] < 0); auto with zarith. + assert (φ il - φ il1 < 0); auto with zarith. rewrite <-Hil2. case (to_Z_bounded il2); auto with zarith. split. rewrite Z.pow_2_r, Hihl1. unfold zn2z_to_Z; rewrite <-H1. - apply trans_equal with ([|ih|] * wB + [|il1|] + ([|il|] - [|il1|])). + apply trans_equal with (φ ih * wB + φ il1 + (φ il - φ il1)). ring. rewrite <-Hil2; ring. - replace [|il2|] with ([||WW ih il||] - [||WW ih1 il1||]). + replace φ il2 with (Φ(WW ih il) - Φ(WW ih1 il1)). unfold zn2z_to_Z at 2; rewrite <- Hihl1. rewrite <-Hbin in Hs2; auto with zarith. unfold zn2z_to_Z. rewrite <-H1. ring_simplify. - apply trans_equal with (wB + ([|il|] - [|il1|])). + apply trans_equal with (wB + (φ il - φ il1)). ring. rewrite <-Hil2; ring. Qed. @@ -1738,7 +1736,7 @@ Proof. symmetry; apply Z.mod_small. split. lia. exact h. Qed. -Lemma of_Z_spec n : [| of_Z n |] = n mod wB. +Lemma of_Z_spec n : φ (of_Z n) = n mod wB. Proof. destruct n. reflexivity. { now simpl; unfold of_pos; rewrite of_pos_rec_spec by lia. } 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/toplevel/coqargs.ml b/toplevel/coqargs.ml index 2b79bff1b2..949a13974c 100644 --- a/toplevel/coqargs.ml +++ b/toplevel/coqargs.ml @@ -55,6 +55,8 @@ type coqargs_config = { color : color; enable_VM : bool; native_compiler : native_compiler; + native_output_dir : CUnix.physical_path; + native_include_dirs : CUnix.physical_path list; stm_flags : Stm.AsyncOpts.stm_opt; debug : bool; diffs_set : bool; @@ -121,6 +123,8 @@ let default_config = { color = `AUTO; enable_VM = true; native_compiler = default_native; + native_output_dir = ".coq-native"; + native_include_dirs = []; stm_flags = Stm.AsyncOpts.default_opts; debug = false; diffs_set = false; @@ -261,8 +265,10 @@ let get_cache opt = function let get_native_name s = (* We ignore even critical errors because this mode has to be super silent *) try - String.concat "/" [Filename.dirname s; - Nativelib.output_dir; Library.native_name_from_filename s] + Filename.(List.fold_left concat (dirname s) + [ !Nativelib.output_dir + ; Library.native_name_from_filename s + ]) with _ -> "" let get_compat_file = function @@ -485,6 +491,14 @@ let parse_args ~help ~init arglist : t * string list = let opt = to_opt_key opt in { oval with config = { oval.config with set_options = (opt, OptionUnset) :: oval.config.set_options }} + |"-native-output-dir" -> + let native_output_dir = next () in + { oval with config = { oval.config with native_output_dir } } + + |"-nI" -> + let include_dir = next () in + { oval with config = {oval.config with native_include_dirs = include_dir :: oval.config.native_include_dirs } } + (* Options with zero arg *) |"-async-queries-always-delegate" |"-async-proofs-always-delegate" diff --git a/toplevel/coqargs.mli b/toplevel/coqargs.mli index f38381a086..aba6811f43 100644 --- a/toplevel/coqargs.mli +++ b/toplevel/coqargs.mli @@ -31,6 +31,8 @@ type coqargs_config = { color : color; enable_VM : bool; native_compiler : native_compiler; + native_output_dir : CUnix.physical_path; + native_include_dirs : CUnix.physical_path list; stm_flags : Stm.AsyncOpts.stm_opt; debug : bool; diffs_set : bool; diff --git a/toplevel/coqtop.ml b/toplevel/coqtop.ml index 46dd693155..1ea48ee766 100644 --- a/toplevel/coqtop.ml +++ b/toplevel/coqtop.ml @@ -239,6 +239,10 @@ let init_execution opts custom_init = set_options opts.config.set_options; + (* Native output dir *) + Nativelib.output_dir := opts.config.native_output_dir; + Nativelib.include_dirs := opts.config.native_include_dirs; + (* Allow the user to load an arbitrary state here *) inputstate opts.pre; diff --git a/toplevel/usage.ml b/toplevel/usage.ml index ba3deeb2f6..c7e1d607f4 100644 --- a/toplevel/usage.ml +++ b/toplevel/usage.ml @@ -94,6 +94,8 @@ let print_usage_common co command = \n for full Gc stats dump)\ \n -bytecode-compiler (yes|no) enable the vm_compute reduction machine\ \n -native-compiler (yes|no|ondemand) enable the native_compute reduction machine\ +\n -native-output-dir <directory> set the output directory for native objects\ +\n -nI dir OCaml include directories for the native compiler (default if not set) \ \n -h, -help, --help print this list of options\ \n" diff --git a/user-contrib/Ltac2/g_ltac2.mlg b/user-contrib/Ltac2/g_ltac2.mlg index 1c66fee9b8..e95ac3b02b 100644 --- a/user-contrib/Ltac2/g_ltac2.mlg +++ b/user-contrib/Ltac2/g_ltac2.mlg @@ -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/attributes.ml b/vernac/attributes.ml index 194308b77f..7213ba4829 100644 --- a/vernac/attributes.ml +++ b/vernac/attributes.ml @@ -163,23 +163,7 @@ let program = let locality = bool_attribute ~name:"Locality" ~on:"local" ~off:"global" -let warn_unqualified_univ_attr = - CWarnings.create ~name:"unqualified-univ-attr" ~category:"deprecated" - (fun key -> Pp.(str "Attribute " ++ str key ++ - str " should be qualified as \"universes("++str key++str")\".")) - let ukey = "universes" -let universe_transform ~warn_unqualified : unit attribute = - fun atts -> - let atts = List.map (fun (key,_ as att) -> - match key with - | "polymorphic" | "monomorphic" - | "template" | "notemplate" -> - if warn_unqualified then warn_unqualified_univ_attr key; - ukey, VernacFlagList [att] - | _ -> att) atts - in - atts, () let universe_polymorphism_option_name = ["Universe"; "Polymorphism"] let is_universe_polymorphism = @@ -198,16 +182,10 @@ let polymorphic_base = | Some b -> return b | None -> return (is_universe_polymorphism()) -let polymorphic_nowarn = - universe_transform ~warn_unqualified:false >> - qualify_attribute ukey polymorphic_base - let template = - universe_transform ~warn_unqualified:true >> qualify_attribute ukey (bool_attribute ~name:"Template" ~on:"template" ~off:"notemplate") let polymorphic = - universe_transform ~warn_unqualified:true >> qualify_attribute ukey polymorphic_base let deprecation_parser : Deprecation.t key_parser = fun orig args -> diff --git a/vernac/attributes.mli b/vernac/attributes.mli index 0074db66d3..7ecb7e4fb0 100644 --- a/vernac/attributes.mli +++ b/vernac/attributes.mli @@ -114,10 +114,6 @@ val make_attribute : (vernac_flags -> vernac_flags * 'a) -> 'a attribute val vernac_polymorphic_flag : vernac_flag val vernac_monomorphic_flag : vernac_flag -(** For the stm, do not use! *) - -val polymorphic_nowarn : bool attribute - -(** For internal use, avoid warning if not qualified as eg [universes(polymorphic)]. *) +(** For internal use. *) val universe_polymorphism_option_name : string list val is_universe_polymorphism : unit -> bool 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/metasyntax.ml b/vernac/metasyntax.ml index afff0347f5..3937f887ad 100644 --- a/vernac/metasyntax.ml +++ b/vernac/metasyntax.ml @@ -294,15 +294,15 @@ let precedence_of_position_and_level from_level = function | RightA, Right -> LevelLe n | LeftA, Left -> LevelLe n | LeftA, Right -> LevelLt n - | NonA, _ -> LevelLt n) - | NumLevel n, _ -> LevelLe n - | NextLevel, _ -> LevelLt from_level - | DefaultLevel, _ -> LevelSome + | NonA, _ -> LevelLt n), Some b + | NumLevel n, _ -> LevelLe n, None + | NextLevel, _ -> LevelLt from_level, None + | DefaultLevel, _ -> LevelSome, None (** Computing precedences of subentries for parsing *) let precedence_of_entry_type (from_custom,from_level) = function | ETConstr (custom,_,x) when notation_entry_eq custom from_custom -> - precedence_of_position_and_level from_level x + fst (precedence_of_position_and_level from_level x) | ETConstr (custom,_,(NumLevel n,_)) -> LevelLe n | ETConstr (custom,_,(NextLevel,_)) -> user_err (strbrk "\"next level\" is only for sub-expressions in the same entry as where the notation is (" ++ @@ -323,9 +323,9 @@ let unparsing_precedence_of_entry_type from_level = function (* Precedence of printing for a custom entry is managed using explicit insertion of entry coercions at the time of building a [constr_expr] *) - LevelSome - | ETPattern (_,n) -> (* in constr *) LevelLe (match n with Some n -> n | None -> 0) - | _ -> LevelSome (* should not matter *) + LevelSome, None + | ETPattern (_,n) -> (* in constr *) LevelLe (match n with Some n -> n | None -> 0), None + | _ -> LevelSome, None (* should not matter *) (* Some breaking examples *) (* "x = y" : "x /1 = y" (breaks before any symbol) *) @@ -392,10 +392,10 @@ let check_open_binder isopen sl m = let unparsing_metavar i from typs = let x = List.nth typs (i-1) in - let prec = unparsing_precedence_of_entry_type from x in + let prec,side = unparsing_precedence_of_entry_type from x in match x with | ETConstr _ | ETGlobal | ETBigint -> - UnpMetaVar prec + UnpMetaVar (prec,side) | ETPattern _ -> UnpBinderMetaVar prec | ETIdent -> @@ -446,14 +446,14 @@ let make_hunks etyps symbols from_level = | SProdList (m,sl) :: prods -> let i = index_id m vars in let typ = List.nth typs (i-1) in - let prec = unparsing_precedence_of_entry_type from_level typ in + let prec,side = unparsing_precedence_of_entry_type from_level typ in let sl' = (* If no separator: add a break *) if List.is_empty sl then add_break 1 [] (* We add NonTerminal for simulation but remove it afterwards *) else make true sl in let hunk = match typ with - | ETConstr _ -> UnpListMetaVar (prec,List.map snd sl') + | ETConstr _ -> UnpListMetaVar (prec,List.map snd sl',side) | ETBinder isopen -> check_open_binder isopen sl m; UnpBinderListMetaVar (isopen,List.map snd sl') @@ -589,13 +589,13 @@ let hunks_of_format (from_level,(vars,typs)) symfmt = | SProdList (m,sl) :: symbs, fmt when has_ldots fmt -> let i = index_id m vars in let typ = List.nth typs (i-1) in - let prec = unparsing_precedence_of_entry_type from_level typ in + let prec,side = unparsing_precedence_of_entry_type from_level typ in let loc_slfmt,rfmt = read_recursive_format sl fmt in let sl, slfmt = aux (sl,loc_slfmt) in if not (List.is_empty sl) then error_format ?loc:(find_prod_list_loc loc_slfmt fmt) (); let symbs, l = aux (symbs,rfmt) in let hunk = match typ with - | ETConstr _ -> UnpListMetaVar (prec,slfmt) + | ETConstr _ -> UnpListMetaVar (prec,slfmt,side) | ETBinder isopen -> check_open_binder isopen sl m; UnpBinderListMetaVar (isopen,slfmt) 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/vernacentries.ml b/vernac/vernacentries.ml index 63fc587f71..2eb1aa39b0 100644 --- a/vernac/vernacentries.ml +++ b/vernac/vernacentries.ml @@ -1282,6 +1282,13 @@ let () = let () = declare_bool_option { optdepr = false; + optkey = ["Printing";"Parentheses"]; + optread = (fun () -> !Constrextern.print_parentheses); + optwrite = (fun b -> Constrextern.print_parentheses := b) } + +let () = + declare_bool_option + { optdepr = false; optkey = ["Printing";"Existential";"Instances"]; optread = (fun () -> !Detyping.print_evar_arguments); optwrite = (:=) Detyping.print_evar_arguments } 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 |