diff options
62 files changed, 819 insertions, 1459 deletions
diff --git a/azure-pipelines.yml b/azure-pipelines.yml index 1648638555..862c54900f 100644 --- a/azure-pipelines.yml +++ b/azure-pipelines.yml @@ -58,7 +58,7 @@ jobs: displayName: 'Install system dependencies' env: HOMEBREW_NO_AUTO_UPDATE: "1" - HBCORE_DATE: "2019-06-18" + HBCORE_DATE: "2019-06-16" HBCORE_REF: "944a5b7d83e4b81c749d93831b514607bdd2b6a1" - script: | diff --git a/dev/ci/ci-basic-overlay.sh b/dev/ci/ci-basic-overlay.sh index dadb2bb8f1..ad22c394d8 100755 --- a/dev/ci/ci-basic-overlay.sh +++ b/dev/ci/ci-basic-overlay.sh @@ -181,9 +181,9 @@ ######################################################################## # SF ######################################################################## -: "${sf_lf_CI_TARURL:=https://www.cis.upenn.edu/~bcpierce/sf/lf-current/lf.tgz}" -: "${sf_plf_CI_TARURL:=https://www.cis.upenn.edu/~bcpierce/sf/plf-current/plf.tgz}" -: "${sf_vfa_CI_TARURL:=https://www.cis.upenn.edu/~bcpierce/sf/vfa-current/vfa.tgz}" +: "${sf_lf_CI_TARURL:=https://softwarefoundations.cis.upenn.edu/lf-current/lf.tgz}" +: "${sf_plf_CI_TARURL:=https://softwarefoundations.cis.upenn.edu/plf-current/plf.tgz}" +: "${sf_vfa_CI_TARURL:=https://softwarefoundations.cis.upenn.edu/vfa-current/vfa.tgz}" ######################################################################## # TLC diff --git a/doc/changelog/08-tools/10430-extraction-int63.rst b/doc/changelog/08-tools/10430-extraction-int63.rst new file mode 100644 index 0000000000..68ae4591a4 --- /dev/null +++ b/doc/changelog/08-tools/10430-extraction-int63.rst @@ -0,0 +1,5 @@ +- Fix extraction to OCaml of primitive machine integers; + see :ref:`primitive-integers` + (`#10430 <https://github.com/coq/coq/pull/10430>`_, + fixes `#10361 <https://github.com/coq/coq/issues/10361>`_, + by Vincent Laporte). diff --git a/doc/changelog/10-standard-library/09811-remove-zlogarithm.rst b/doc/changelog/10-standard-library/09811-remove-zlogarithm.rst new file mode 100644 index 0000000000..ab625b9e03 --- /dev/null +++ b/doc/changelog/10-standard-library/09811-remove-zlogarithm.rst @@ -0,0 +1,4 @@ +- Removes deprecated modules `Coq.ZArith.Zlogarithm` + and `Coq.ZArith.Zsqrt_compat` + (#9881 <https://github.com/coq/coq/pull/9811> + by Vincent Laporte). diff --git a/doc/sphinx/changes.rst b/doc/sphinx/changes.rst index fd84868a1f..6ac55e7bf4 100644 --- a/doc/sphinx/changes.rst +++ b/doc/sphinx/changes.rst @@ -102,10 +102,10 @@ reference manual. Here are the most important user-visible changes: extensionality lemma: - interactive mode: :n:`under @term`, associated terminator: :tacn:`over` - - one-liner mode: `under @term do [@tactic | ...]` + - one-liner mode: :n:`under @term do [@tactic | ...]` It can take occurrence switches, contextual patterns, and intro patterns: - :g:`under {2}[in RHS]eq_big => [i|i ?] do ...` + :g:`under {2}[in RHS]eq_big => [i|i ?]` (`#9651 <https://github.com/coq/coq/pull/9651>`_, by Erik Martin-Dorel and Enrico Tassi). diff --git a/doc/sphinx/language/coq-library.rst b/doc/sphinx/language/coq-library.rst index d1b95e6203..ac75240cfb 100644 --- a/doc/sphinx/language/coq-library.rst +++ b/doc/sphinx/language/coq-library.rst @@ -7,22 +7,20 @@ The |Coq| library single: Theories -The |Coq| library is structured into two parts: +The |Coq| library has two parts: - * **The initial library**: it contains elementary logical notions and - data-types. It constitutes the basic state of the system directly - available when running |Coq|; + * **The basic library**: definitions and theorems for + the most commonly used elementary logical notions and + data types. |Coq| normally loads these files automatically when it starts. - * **The standard library**: general-purpose libraries containing various - developments of |Coq| axiomatizations about sets, lists, sorting, - arithmetic, etc. This library comes with the system and its modules - are directly accessible through the ``Require`` command (see - Section :ref:`compiled-files`); + * **The standard library**: general-purpose libraries with + definitions and theorems for sets, lists, sorting, + arithmetic, etc. To use these files, users must load them explicitly + with the ``Require`` command (see :ref:`compiled-files`) -In addition, user-provided libraries or developments are provided by -|Coq| users' community. These libraries and developments are available -for download at http://coq.inria.fr (see -Section :ref:`userscontributions`). +There are also many libraries provided by |Coq| users' community. +These libraries and developments are available +for download at http://coq.inria.fr (see :ref:`userscontributions`). This chapter briefly reviews the |Coq| libraries whose contents can also be browsed at http://coq.inria.fr/stdlib. @@ -514,8 +512,8 @@ realizability interpretation. forall (A B:Prop) (P:Type), (A -> B -> P) -> A /\ B -> P. -Basic Arithmetics -~~~~~~~~~~~~~~~~~ +Basic Arithmetic +~~~~~~~~~~~~~~~~ The basic library includes a few elementary properties of natural numbers, together with the definitions of predecessor, addition and @@ -804,8 +802,8 @@ Notation Interpretation =============== =================== -Notations for integer arithmetics -~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ +Notations for integer arithmetic +~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ .. index:: single: Arithmetical notations @@ -822,7 +820,7 @@ Notations for integer arithmetics The following table describes the syntax of expressions -for integer arithmetics. It is provided by requiring and opening the module ``ZArith`` and opening scope ``Z_scope``. +for integer arithmetic. It is provided by requiring and opening the module ``ZArith`` and opening scope ``Z_scope``. It specifies how notations are interpreted and, when not already reserved, the precedence and associativity. @@ -866,7 +864,7 @@ Notations for real numbers This is provided by requiring and opening the module ``Reals`` and opening scope ``R_scope``. This set of notations is very similar to -the notation for integer arithmetics. The inverse function was added. +the notation for integer arithmetic. The inverse function was added. =============== =================== Notation Interpretation diff --git a/doc/sphinx/language/gallina-extensions.rst b/doc/sphinx/language/gallina-extensions.rst index c93984661e..acf68e9fd2 100644 --- a/doc/sphinx/language/gallina-extensions.rst +++ b/doc/sphinx/language/gallina-extensions.rst @@ -2443,12 +2443,19 @@ The reduction machines (:tacn:`vm_compute`, :tacn:`native_compute`) implement dedicated, efficient, rules to reduce the applications of these primitive operations. -These primitives, when extracted to OCaml (see :ref:`extraction`), are mapped to -types and functions of a :g:`Uint63` module. Said module is not produced by +The extraction of these primitives can be customized similarly to the extraction +of regular axioms (see :ref:`extraction`). Nonetheless, the :g:`ExtrOCamlInt63` +module can be used when extracting to OCaml: it maps the Coq primitives to types +and functions of a :g:`Uint63` module. Said OCaml module is not produced by extraction. Instead, it has to be provided by the user (if they want to compile or execute the extracted code). For instance, an implementation of this module can be taken from the kernel of Coq. +Literal values (at type :g:`Int63.int`) are extracted to literal OCaml values +wrapped into the :g:`Uint63.of_int` (resp. :g:`Uint63.of_int64`) constructor on +64-bit (resp. 32-bit) platforms. Currently, this cannot be customized (see the +function :g:`Uint63.compile` from the kernel). + Bidirectionality hints ---------------------- diff --git a/doc/sphinx/language/gallina-specification-language.rst b/doc/sphinx/language/gallina-specification-language.rst index 38f6714f46..91dfa34494 100644 --- a/doc/sphinx/language/gallina-specification-language.rst +++ b/doc/sphinx/language/gallina-specification-language.rst @@ -44,78 +44,91 @@ Lexical conventions =================== Blanks - Space, newline and horizontal tabulation are considered as blanks. + Space, newline and horizontal tab are considered blanks. Blanks are ignored but they separate tokens. Comments - Comments in Coq are enclosed between ``(*`` and ``*)``, and can be nested. - They can contain any character. However, :token:`string` literals must be + Comments are enclosed between ``(*`` and ``*)``. They can be nested. + They can contain any character. However, embedded :token:`string` literals must be correctly closed. Comments are treated as blanks. -Identifiers and access identifiers +Identifiers and field identifiers Identifiers, written :token:`ident`, are sequences of letters, digits, ``_`` and - ``'``, that do not start with a digit or ``'``. That is, they are - recognized by the following lexical class: + ``'``, that do not start with a digit or ``'``. That is, they are + recognized by the following grammar (except that the string ``_`` is reserved; + it is not a valid identifier): .. productionlist:: coq - first_letter : a..z ∣ A..Z ∣ _ ∣ unicode-letter - subsequent_letter : a..z ∣ A..Z ∣ 0..9 ∣ _ ∣ ' ∣ unicode-letter ∣ unicode-id-part ident : `first_letter`[`subsequent_letter`…`subsequent_letter`] - access_ident : .`ident` + field : .`ident` + first_letter : a..z ∣ A..Z ∣ _ ∣ `unicode_letter` + subsequent_letter : `first_letter` ∣ 0..9 ∣ ' ∣ `unicode_id_part` All characters are meaningful. In particular, identifiers are case-sensitive. - The entry ``unicode-letter`` non-exhaustively includes Latin, + :production:`unicode_letter` non-exhaustively includes Latin, Greek, Gothic, Cyrillic, Arabic, Hebrew, Georgian, Hangul, Hiragana and Katakana characters, CJK ideographs, mathematical letter-like - symbols, hyphens, non-breaking space, … The entry ``unicode-id-part`` + symbols and non-breaking space. :production:`unicode_id_part` non-exhaustively includes symbols for prime letters and subscripts. - Access identifiers, written :token:`access_ident`, are identifiers prefixed by - `.` (dot) without blank. They are used in the syntax of qualified - identifiers. + Field identifiers, written :token:`field`, are identifiers prefixed by + `.` (dot) with no blank between the dot and the identifier. They are used in + the syntax of qualified identifiers. Numerals - Numerals are sequences of digits with a potential fractional part - and exponent. Integers are numerals without fractional nor exponent - part and optionally preceded by a minus sign. Underscores ``_`` can - be used as comments in numerals. + Numerals are sequences of digits with an optional fractional part + and exponent, optionally preceded by a minus sign. :token:`int` is an integer; + a numeral without fractional or exponent parts. :token:`num` is a non-negative + integer. Underscores embedded in the digits are ignored, for example + ``1_000_000`` is the same as ``1000000``. .. productionlist:: coq - digit : 0..9 + numeral : `num`[. `num`][`exp`[`sign`]`num`] + int : [-]`num` num : `digit`…`digit` - integer : [-]`num` - dot : . + digit : 0..9 exp : e | E sign : + | - - numeral : `num`[`dot` `num`][`exp`[`sign`]`num`] Strings - Strings are delimited by ``"`` (double quote), and enclose a sequence of - any characters different from ``"`` or the sequence ``""`` to denote the - double quote character. In grammars, the entry for quoted strings is - :production:`string`. + Strings begin and end with ``"`` (double quote). Use ``""`` to represent + a double quote character within a string. In the grammar, strings are + identified with :production:`string`. Keywords - The following identifiers are reserved keywords, and cannot be - employed otherwise:: - - _ as at cofix else end exists exists2 fix for - forall fun if IF in let match mod return - SProp Prop Set Type then using where with - -Special tokens - The following sequences of characters are special tokens:: - - ! % & && ( () ) * + ++ , - -> . .( .. - / /\ : :: :< := :> ; < <- <-> <: <= <> = - => =_D > >-> >= ? ?= @ [ \/ ] ^ { | |- - || } ~ #[ - - Lexical ambiguities are resolved according to the “longest match” - rule: when a sequence of non alphanumerical characters can be - decomposed into several different ways, then the first token is the - longest possible one (among all tokens defined at this moment), and so - on. + The following character sequences are reserved keywords that cannot be + used as identifiers:: + + _ Axiom CoFixpoint Definition Fixpoint Hypothesis IF Parameter Prop + SProp Set Theorem Type Variable as at by cofix discriminated else + end exists exists2 fix for forall fun if in lazymatch let match + multimatch return then using where with + + Note that plugins may define additional keywords when they are loaded. + +Other tokens + The set of + tokens defined at any given time can vary because the :cmd:`Notation` + command can define new tokens. A :cmd:`Require` command may load more notation definitions, + while the end of a :cmd:`Section` may remove notations. Some notations + are defined in the basic library (see :ref:`thecoqlibrary`) and are normallly + loaded automatically at startup time. + + Here are the character sequences that Coq directly defines as tokens + without using :cmd:`Notation` (omitting 25 specialized tokens that begin with + ``#int63_``):: + + ! #[ % & ' ( () (bfs) (dfs) ) * ** + , - -> + . .( .. ... / : ::= := :> :>> ; < <+ <- <: + <<: <= = => > >-> >= ? @ @{ [ [= ] _ _eqn + `( `{ { {| | |- || } + + When multiple tokens match the beginning of a sequence of characters, + the longest matching token is used. + Occasionally you may need to insert spaces to separate tokens. For example, + if ``~`` and ``~~`` are both defined as tokens, the inputs ``~ ~`` and + ``~~`` generate different tokens, whereas if `~~` is not defined, then the + two inputs are equivalent. .. _term: @@ -164,7 +177,7 @@ is described in Chapter :ref:`syntaxextensionsandinterpretationscopes`. : ( `name` [: `term`] := `term` ) : ' `pattern` name : `ident` | _ - qualid : `ident` | `qualid` `access_ident` + qualid : `ident` | `qualid` `field` sort : SProp | Prop | Set | Type fix_bodies : `fix_body` : `fix_body` with `fix_body` with … with `fix_body` for `ident` diff --git a/doc/sphinx/practical-tools/coqide.rst b/doc/sphinx/practical-tools/coqide.rst index efb5df720a..7d6171285e 100644 --- a/doc/sphinx/practical-tools/coqide.rst +++ b/doc/sphinx/practical-tools/coqide.rst @@ -88,8 +88,6 @@ There are other buttons on the |CoqIDE| toolbar: a button to save the running buffer; a button to close the current buffer (an "X"); buttons to switch among buffers (left and right arrows); an "information" button; and a "gears" button. -The "information" button is described in Section :ref:`try-tactics-automatically`. - The "gears" button submits proof terms to the |Coq| kernel for type checking. When |Coq| uses asynchronous processing (see Chapter :ref:`asynchronousandparallelproofprocessing`), proofs may have been completed without kernel-checking of generated proof terms. @@ -100,27 +98,6 @@ processed color, though their preceding proofs have the processed color. Notice that for all these buttons, except for the "gears" button, their operations are also available in the menu, where their keyboard shortcuts are given. -.. _try-tactics-automatically: - -Trying tactics automatically ------------------------------- - -The menu Try Tactics provides some features for automatically trying -to solve the current goal using simple tactics. If such a tactic -succeeds in solving the goal, then its text is automatically inserted -into the script. There is finally a combination of these tactics, -called the *proof wizard* which will try each of them in turn. This -wizard is also available as a tool button (the "information" button). The set of -tactics tried by the wizard is customizable in the preferences. - -These tactics are general ones, in particular they do not refer to -particular hypotheses. You may also try specific tactics related to -the goal or one of the hypotheses, by clicking with the right mouse -button on the goal or the considered hypothesis. This is the -“contextual menu on goals” feature, that may be disabled in the -preferences if undesirable. - - Proof folding ------------------ @@ -202,13 +179,6 @@ compilation, printing, web browsing. In the browser command, you may use `%s` to denote the URL to open, for example: `firefox -remote "OpenURL(%s)"`. -The `Tactics Wizard` section allows defining the set of tactics that -should be tried, in sequence, to solve the current goal. - -The last section is for miscellaneous boolean settings, such as the -“contextual menu on goals” feature presented in the section -:ref:`Try tactics automatically <try-tactics-automatically>`. - Notice that these settings are saved in the file `.coqiderc` of your home directory. diff --git a/doc/sphinx/proof-engine/ltac.rst b/doc/sphinx/proof-engine/ltac.rst index 46f9826e41..362c3da6cb 100644 --- a/doc/sphinx/proof-engine/ltac.rst +++ b/doc/sphinx/proof-engine/ltac.rst @@ -31,10 +31,10 @@ Syntax The syntax of the tactic language is given below. See Chapter :ref:`gallinaspecificationlanguage` for a description of the BNF metasyntax used in these grammar rules. Various already defined entries will be used in this -chapter: entries :token:`natural`, :token:`integer`, :token:`ident`, +chapter: entries :token:`num`, :token:`int`, :token:`ident` :token:`qualid`, :token:`term`, :token:`cpattern` and :token:`tactic` -represent respectively the natural and integer numbers, the authorized -identificators and qualified names, Coq terms and patterns and all the atomic +represent respectively natural and integer numbers, +identifiers, qualified names, Coq terms, patterns and the atomic tactics described in Chapter :ref:`tactics`. The syntax of :production:`cpattern` is @@ -141,10 +141,10 @@ mode but it can also be used in toplevel definitions as shown below. : `atom` atom : `qualid` : () - : `integer` + : `int` : ( `ltac_expr` ) component : `string` | `qualid` - message_token : `string` | `ident` | `integer` + message_token : `string` | `ident` | `int` tacarg : `qualid` : () : ltac : `atom` @@ -159,11 +159,11 @@ mode but it can also be used in toplevel definitions as shown below. match_rule : `cpattern` => `ltac_expr` : context [`ident`] [ `cpattern` ] => `ltac_expr` : _ => `ltac_expr` - test : `integer` = `integer` - : `integer` (< | <= | > | >=) `integer` + test : `int` = `int` + : `int` (< | <= | > | >=) `int` selector : [`ident`] - : `integer` - : (`integer` | `integer` - `integer`), ..., (`integer` | `integer` - `integer`) + : `int` + : (`int` | `int` - `int`), ..., (`int` | `int` - `int`) toplevel_selector : `selector` : all : par diff --git a/doc/sphinx/proof-engine/ltac2.rst b/doc/sphinx/proof-engine/ltac2.rst index 3036648b08..ceaa2775bf 100644 --- a/doc/sphinx/proof-engine/ltac2.rst +++ b/doc/sphinx/proof-engine/ltac2.rst @@ -179,7 +179,7 @@ constructions from ML. : let `ltac2_var` := `ltac2_term` in `ltac2_term` : let rec `ltac2_var` := `ltac2_term` in `ltac2_term` : match `ltac2_term` with `ltac2_branch` ... `ltac2_branch` end - : `integer` + : `int` : `string` : `ltac2_term` ; `ltac2_term` : [| `ltac2_term` ; ... ; `ltac2_term` |] @@ -670,7 +670,7 @@ A scope is a name given to a grammar entry used to produce some Ltac2 expression at parsing time. Scopes are described using a form of S-expression. .. prodn:: - ltac2_scope ::= {| @string | @integer | @lident ({+, @ltac2_scope}) } + ltac2_scope ::= {| @string | @int | @lident ({+, @ltac2_scope}) } A few scopes contain antiquotation features. For sake of uniformity, all antiquotations are introduced by the syntax :n:`$@lident`. @@ -719,7 +719,7 @@ The following scopes are built-in. + parses a Ltac2 expression at the next level and return it as is. -- :n:`tactic(n = @integer)`: +- :n:`tactic(n = @int)`: + parses a Ltac2 expression at the provided level :n:`n` and return it as is. @@ -760,7 +760,7 @@ Notations The Ltac2 parser can be extended by syntactic notations. -.. cmd:: Ltac2 Notation {+ {| @lident (@ltac2_scope) | @string } } {? : @integer} := @ltac2_term +.. cmd:: Ltac2 Notation {+ {| @lident (@ltac2_scope) | @string } } {? : @int} := @ltac2_term :name: Ltac2 Notation A Ltac2 notation adds a parsing rule to the Ltac2 grammar, which is expanded diff --git a/doc/sphinx/proof-engine/ssreflect-proof-language.rst b/doc/sphinx/proof-engine/ssreflect-proof-language.rst index 1b9e3ce0f3..ed980bd4de 100644 --- a/doc/sphinx/proof-engine/ssreflect-proof-language.rst +++ b/doc/sphinx/proof-engine/ssreflect-proof-language.rst @@ -3761,10 +3761,10 @@ involves the following steps: 5. If so :tacn:`under` protects these n goals against an accidental instantiation of the evar. - These protected goals are displayed using the ``Under[ … ]`` - notation (e.g. ``Under[ m - m ]`` in the running example). + These protected goals are displayed using the ``'Under[ … ]`` + notation (e.g. ``'Under[ m - m ]`` in the running example). -6. The expression inside the ``Under[ … ]`` notation can be +6. The expression inside the ``'Under[ … ]`` notation can be proved equivalent to the desired expression by using a regular :tacn:`rewrite` tactic. @@ -3782,7 +3782,7 @@ The over tactic Two equivalent facilities (a terminator and a lemma) are provided to close intermediate subgoals generated by :tacn:`under` (i.e. goals -displayed as ``Under[ … ]``): +displayed as ``'Under[ … ]``): .. tacn:: over :name: over @@ -3792,7 +3792,7 @@ displayed as ``Under[ … ]``): .. tacv:: by rewrite over - This is a variant of :tacn:`over` in order to close ``Under[ … ]`` + This is a variant of :tacn:`over` in order to close ``'Under[ … ]`` goals, relying on the ``over`` rewrite rule. .. _under_one_liner: diff --git a/doc/sphinx/proof-engine/vernacular-commands.rst b/doc/sphinx/proof-engine/vernacular-commands.rst index 5f3e82938d..774732825a 100644 --- a/doc/sphinx/proof-engine/vernacular-commands.rst +++ b/doc/sphinx/proof-engine/vernacular-commands.rst @@ -870,26 +870,6 @@ interactively, they cannot be part of a vernacular file loaded via have to undo some extra commands and end on a state :n:`@num′ ≤ @num` if necessary. - .. cmdv:: Backtrack @num @num @num - :name: Backtrack - - .. deprecated:: 8.4 - - :cmd:`Backtrack` is a *deprecated* form of - :cmd:`BackTo` which allows explicitly manipulating the proof environment. The - three numbers represent the following: - - + *first number* : State label to reach, as for :cmd:`BackTo`. - + *second number* : *Proof state number* to unbury once aborts have been done. - |Coq| will compute the number of :cmd:`Undo` to perform (see Chapter :ref:`proofhandling`). - + *third number* : Number of :cmd:`Abort` to perform, i.e. the number of currently - opened nested proofs that must be canceled (see Chapter :ref:`proofhandling`). - - .. exn:: Invalid backtrack. - - The destination state label is unknown. - - .. _quitting-and-debugging: Quitting and debugging diff --git a/doc/stdlib/hidden-files b/doc/stdlib/hidden-files index b25104ddb9..46175e37ed 100644 --- a/doc/stdlib/hidden-files +++ b/doc/stdlib/hidden-files @@ -12,6 +12,7 @@ plugins/extraction/ExtrHaskellZInteger.v plugins/extraction/ExtrHaskellZNum.v plugins/extraction/ExtrOcamlBasic.v plugins/extraction/ExtrOcamlBigIntConv.v +plugins/extraction/ExtrOCamlInt63.v plugins/extraction/ExtrOcamlIntConv.v plugins/extraction/ExtrOcamlNatBigInt.v plugins/extraction/ExtrOcamlNatInt.v diff --git a/doc/stdlib/index-list.html.template b/doc/stdlib/index-list.html.template index a561de1d0c..8b5ede7036 100644 --- a/doc/stdlib/index-list.html.template +++ b/doc/stdlib/index-list.html.template @@ -181,14 +181,12 @@ through the <tt>Require Import</tt> command.</p> theories/ZArith/Zhints.v (theories/ZArith/ZArith_base.v) theories/ZArith/Zcomplements.v - theories/ZArith/Zsqrt_compat.v theories/ZArith/Zpow_def.v theories/ZArith/Zpow_alt.v theories/ZArith/Zpower.v theories/ZArith/Zdiv.v theories/ZArith/Zquot.v theories/ZArith/Zeuclid.v - theories/ZArith/Zlogarithm.v (theories/ZArith/ZArith.v) theories/ZArith/Zgcd_alt.v theories/ZArith/Zwf.v diff --git a/doc/tools/docgram/doc_grammar.ml b/doc/tools/docgram/doc_grammar.ml index 9f0a1942f9..eb86bab37e 100644 --- a/doc/tools/docgram/doc_grammar.ml +++ b/doc/tools/docgram/doc_grammar.ml @@ -1020,6 +1020,37 @@ let apply_edit_file g edits = in List.rev (List.concat (List.map traverse prod)) + (* get the special tokens in the grammar *) +let print_special_tokens g = + let rec traverse set = function + | Sterm s -> + let c = s.[0] in + if (c >= 'a' && c <= 'z') || (c >= 'A' && c <= 'Z') then set + else StringSet.add s set + | Snterm s -> set + | Slist1 sym + | Slist0 sym + | Sopt sym + -> traverse set sym + | Slist1sep (sym, sep) + | Slist0sep (sym, sep) + -> traverse (traverse set sym) sep + | Sparen sym_list -> traverse_prod set sym_list + | Sprod sym_list_list -> traverse_prods set sym_list_list + | Sedit _ + | Sedit2 _ -> set + and traverse_prod set prod = List.fold_left traverse set prod + and traverse_prods set prods = List.fold_left traverse_prod set prods + in + let spec_toks = List.fold_left (fun set b -> + let nt, prods = b in + traverse_prods set prods) + StringSet.empty (NTMap.bindings !g.map) + in + Printf.printf "Special tokens:"; + StringSet.iter (fun t -> Printf.printf " %s" t) spec_toks; + Printf.printf "\n\n" + (* get the transitive closure of a non-terminal excluding "stops" symbols. Preserve ordering to the extent possible *) (* todo: at the moment, the code doesn't use the ordering; consider switching to using @@ -1099,8 +1130,9 @@ let print_chunks g out fmt () = (*seen := StringSet.diff !seen (StringSet.of_list ssr_tops);*) (*print_chunk out g seen fmt "vernac_toplevel" ["vernac_toplevel"] [];*) -let start_symbols = ["vernac_toplevel"; "tactic_mode"] -let tokens = [ "BULLET"; "FIELD"; "IDENT"; "NUMERAL"; "STRING" ] (* don't report as undefined *) +let start_symbols = ["vernac_toplevel"] +(* don't report tokens as undefined *) +let tokens = [ "bullet"; "field"; "ident"; "int"; "num"; "numeral"; "string" ] let report_bad_nts g file = let rec get_nts refd defd bindings = @@ -1468,6 +1500,8 @@ let process_grammar args = print_in_order out g `MLG !g.order StringSet.empty; close_out out; finish_with_file (dir "fullGrammar") args.verify; + if args.verbose then + print_special_tokens g; if not args.fullGrammar then begin (* do shared edits *) diff --git a/ide/MacOS/default_accel_map b/ide/MacOS/default_accel_map index 54a592a04d..6bcf3b438f 100644 --- a/ide/MacOS/default_accel_map +++ b/ide/MacOS/default_accel_map @@ -7,7 +7,6 @@ ; (gtk_accel_path "<Actions>/Templates/Template Program Lemma" "") (gtk_accel_path "<Actions>/Templates/Lemma" "<Shift><Primary>l") ; (gtk_accel_path "<Actions>/Templates/Template Fact" "") -(gtk_accel_path "<Actions>/Tactics/auto" "<Primary><Control>a") ; (gtk_accel_path "<Actions>/Tactics/Tactic fold" "") ; (gtk_accel_path "<Actions>/Help/About Coq" "") ; (gtk_accel_path "<Actions>/Templates/Template Add Ring A Aplus Amult Aone Azero Ainv Aeq T [ c1 ... cn ]. " "") @@ -19,7 +18,6 @@ ; (gtk_accel_path "<Actions>/Tactics/Tactic inversion" "") ; (gtk_accel_path "<Actions>/Templates/Template Write State" "") ; (gtk_accel_path "<Actions>/Export/Export to" "") -(gtk_accel_path "<Actions>/Tactics/auto with *" "<Primary><Control>asterisk") ; (gtk_accel_path "<Actions>/Tactics/Tactic inversion--clear" "") ; (gtk_accel_path "<Actions>/Templates/Template Implicit Arguments" "") ; (gtk_accel_path "<Actions>/Edit/Copy" "<Primary>c") @@ -50,7 +48,6 @@ ; (gtk_accel_path "<Actions>/Tactics/Tactic fail" "") ; (gtk_accel_path "<Actions>/Tactics/Tactic left" "") (gtk_accel_path "<Actions>/Edit/Undo" "<Primary>u") -(gtk_accel_path "<Actions>/Tactics/eauto with *" "<Primary><Control>ampersand") ; (gtk_accel_path "<Actions>/Templates/Template Infix" "") ; (gtk_accel_path "<Actions>/Tactics/Tactic functional induction" "") ; (gtk_accel_path "<Actions>/Tactics/Tactic clear" "") @@ -149,7 +146,6 @@ (gtk_accel_path "<Actions>/Templates/Theorem" "<Shift><Primary>t") ; (gtk_accel_path "<Actions>/Templates/Template Derive Dependent Inversion--clear" "") ; (gtk_accel_path "<Actions>/Tactics/Tactic unfold" "") -; (gtk_accel_path "<Actions>/Tactics/Try Tactics" "") ; (gtk_accel_path "<Actions>/Tactics/Tactic red in" "") ; (gtk_accel_path "<Actions>/Tactics/Tactic rewrite <- -- in" "") ; (gtk_accel_path "<Actions>/Templates/Template Hint Extern" "") @@ -187,7 +183,6 @@ ; (gtk_accel_path "<Actions>/Tactics/Tactic intro -- after" "") ; (gtk_accel_path "<Actions>/Tactics/Tactic fold -- in" "") ; (gtk_accel_path "<Actions>/Templates/Template Program Definition" "") -(gtk_accel_path "<Actions>/Tactics/Wizard" "<Primary><Control>dollar") ; (gtk_accel_path "<Actions>/Templates/Template Hint Resolve" "") ; (gtk_accel_path "<Actions>/Templates/Template Set Extraction Optimize" "") ; (gtk_accel_path "<Actions>/File/Revert all buffers" "") @@ -228,7 +223,6 @@ ; (gtk_accel_path "<Actions>/Export/Html" "") ; (gtk_accel_path "<Actions>/Templates/Template Extraction Inline" "") ; (gtk_accel_path "<Actions>/Tactics/Tactic absurd" "") -(gtk_accel_path "<Actions>/Tactics/intuition" "<Primary><Control>i") ; (gtk_accel_path "<Actions>/Tactics/Tactic simple induction" "") ; (gtk_accel_path "<Actions>/Queries/Queries" "") ; (gtk_accel_path "<Actions>/Tactics/Tactic rewrite -- in" "") @@ -289,7 +283,6 @@ ; (gtk_accel_path "<Actions>/Templates/Template Add Field" "") ; (gtk_accel_path "<Actions>/Templates/Template Require Export" "") ; (gtk_accel_path "<Actions>/Tactics/Tactic rewrite <-" "") -(gtk_accel_path "<Actions>/Tactics/omega" "<Primary><Control>o") ; (gtk_accel_path "<Actions>/Tactics/Tactic split" "") ; (gtk_accel_path "<Actions>/File/Quit" "<Primary>q") (gtk_accel_path "<Actions>/View/Display existential variable instances" "<Shift><Control>e") @@ -328,7 +321,6 @@ ; (gtk_accel_path "<Actions>/Edit/Edit" "") ; (gtk_accel_path "<Actions>/Tactics/Tactic firstorder" "") ; (gtk_accel_path "<Actions>/Templates/Template C" "") -(gtk_accel_path "<Actions>/Tactics/simpl" "<Primary><Control>s") ; (gtk_accel_path "<Actions>/Tactics/Tactic replace -- with" "") ; (gtk_accel_path "<Actions>/Templates/Template A" "") ; (gtk_accel_path "<Actions>/Templates/Template Remove Printing Record" "") @@ -360,13 +352,11 @@ ; (gtk_accel_path "<Actions>/File/File" "") ; (gtk_accel_path "<Actions>/Tactics/Tactic setoid--replace" "") ; (gtk_accel_path "<Actions>/Tactics/Tactic generalize dependent" "") -(gtk_accel_path "<Actions>/Tactics/trivial" "<Primary><Control>v") ; (gtk_accel_path "<Actions>/Tactics/Tactic fix -- with" "") ; (gtk_accel_path "<Actions>/Tactics/Tactic pose --:=--)" "") ; (gtk_accel_path "<Actions>/Tactics/Tactic auto with" "") ; (gtk_accel_path "<Actions>/Templates/Template Add Printing Record" "") ; (gtk_accel_path "<Actions>/Tactics/Tactic inversion -- in" "") -(gtk_accel_path "<Actions>/Tactics/eauto" "<Primary><Control>e") ; (gtk_accel_path "<Actions>/File/Open" "<Primary>o") ; (gtk_accel_path "<Actions>/Tactics/Tactic elim -- using" "") ; (gtk_accel_path "<Actions>/Templates/Template Hint" "") diff --git a/ide/coqOps.ml b/ide/coqOps.ml index 566654218d..d52f038f1f 100644 --- a/ide/coqOps.ml +++ b/ide/coqOps.ml @@ -137,7 +137,6 @@ class type ops = object method go_to_insert : unit task method go_to_mark : GText.mark -> unit task - method tactic_wizard : string list -> unit task method process_next_phrase : unit task method process_until_end_or_error : unit task method handle_reset_initial : unit task @@ -806,48 +805,6 @@ object(self) else Coq.seq (self#backtrack_to_iter ~move_insert:false point) (Coq.lift (fun () -> Sentence.tag_on_insert buffer))) - method tactic_wizard l = - let insert_phrase phrase tag = - let stop = self#get_start_of_input in - let phrase' = if stop#starts_line then phrase else "\n"^phrase in - buffer#insert ~iter:stop phrase'; - Sentence.tag_on_insert buffer; - let start = self#get_start_of_input in - buffer#move_mark ~where:stop (`NAME "start_of_input"); - buffer#apply_tag tag ~start ~stop; - if self#get_insert#compare stop <= 0 then - buffer#place_cursor ~where:stop; - let sentence = - mk_sentence - ~start:(`MARK (buffer#create_mark start)) - ~stop:(`MARK (buffer#create_mark stop)) - [] in - Doc.push document sentence; - messages#default_route#clear; - self#show_goals - in - let display_error (loc, s) = - messages#default_route#add (Ideutils.validate s) in - let try_phrase phrase stop more = - let action = log "Sending to coq now" in - let route_id = 0 in - let query = Coq.query (route_id,(phrase,Stateid.dummy)) in - let next = function - | Fail (_, l, str) -> (* FIXME: check *) - display_error (l, str); - messages#default_route#add (Pp.str ("Unsuccessfully tried: "^phrase)); - more - | Good () -> stop Tags.Script.processed - in - Coq.bind (Coq.seq action query) next - in - let rec loop l = match l with - | [] -> Coq.return () - | p :: l' -> - try_phrase ("progress "^p^".") (insert_phrase (p^".")) (loop l') - in - loop l - method handle_reset_initial = let action () = (* clear the stack *) diff --git a/ide/coqOps.mli b/ide/coqOps.mli index 83ad8c15dc..1e8d87bb15 100644 --- a/ide/coqOps.mli +++ b/ide/coqOps.mli @@ -15,7 +15,6 @@ class type ops = object method go_to_insert : unit task method go_to_mark : GText.mark -> unit task - method tactic_wizard : string list -> unit task method process_next_phrase : unit task method process_until_end_or_error : unit task method handle_reset_initial : unit task diff --git a/ide/coqide.ml b/ide/coqide.ml index 8d95dcee27..2c9f116cc3 100644 --- a/ide/coqide.ml +++ b/ide/coqide.ml @@ -603,9 +603,6 @@ module Nav = struct let join_document _ = send_to_coq (fun sn -> sn.coqops#join_document) end -let tactic_wizard_callback l _ = - send_to_coq (fun sn -> sn.coqops#tactic_wizard l) - let printopts_callback opts v = let b = v#get_active in let () = List.iter (fun o -> Coq.PrintOpt.set o b) opts in @@ -1106,25 +1103,8 @@ let build_ui () = ("Force", "_Force", `EXECUTE, Nav.join_document, "Fully check the document", "f"); ] end; - let tacitem s sc = - item s ~label:("_"^s) - ~accel:(modifier_for_tactics#get^sc) - ~callback:(tactic_wizard_callback [s]) - in menu tactics_menu [ - item "Try Tactics" ~label:"_Try Tactics"; - item "Wizard" ~label:"<Proof Wizard>" ~stock:`DIALOG_INFO - ~tooltip:"Proof Wizard" ~accel:(modifier_for_tactics#get^"dollar") - ~callback:(tactic_wizard_callback automatic_tactics#get); - tacitem "auto" "a"; - tacitem "auto with *" "asterisk"; - tacitem "eauto" "e"; - tacitem "eauto with *" "ampersand"; - tacitem "intuition" "i"; - tacitem "omega" "o"; - tacitem "simpl" "s"; - tacitem "tauto" "p"; - tacitem "trivial" "v"; + item "Tactics" ~label:"_Tactics"; ]; alpha_items tactics_menu "Tactic" Coq_commands.tactics; diff --git a/ide/coqide_ui.ml b/ide/coqide_ui.ml index d4a339f4f5..452808490d 100644 --- a/ide/coqide_ui.ml +++ b/ide/coqide_ui.ml @@ -100,18 +100,7 @@ let init () = \n <menuitem action='Previous' />\ \n <menuitem action='Next' />\ \n </menu>\ -\n <menu action='Try Tactics'>\ -\n <menuitem action='auto' />\ -\n <menuitem action='auto with *' />\ -\n <menuitem action='eauto' />\ -\n <menuitem action='eauto with *' />\ -\n <menuitem action='intuition' />\ -\n <menuitem action='omega' />\ -\n <menuitem action='simpl' />\ -\n <menuitem action='tauto' />\ -\n <menuitem action='trivial' />\ -\n <menuitem action='Wizard' />\ -\n <separator />\ +\n <menu action='Tactics'>\ \n %s\ \n </menu>\ \n <menu action='Templates'>\ @@ -173,7 +162,6 @@ let init () = \n <toolitem action='Interrupt' />\ \n <toolitem action='Previous' />\ \n <toolitem action='Next' />\ -\n <toolitem action='Wizard' />\ \n</toolbar>\ \n</ui>" (if Coq_config.gtk_platform <> `QUARTZ then "<menuitem action='Quit' />" else "") diff --git a/ide/preferences.ml b/ide/preferences.ml index ea0495bb19..bf9fe8922a 100644 --- a/ide/preferences.ml +++ b/ide/preferences.ml @@ -938,16 +938,6 @@ let configure ?(apply=(fun () -> ())) parent = else cmd_browse#get]) cmd_browse#get in -(* - let automatic_tactics = - strings - ~f:automatic_tactics#set - ~add:(fun () -> ["<edit me>"]) - "Wizard tactics to try in order" - automatic_tactics#get - - in -*) let contextual_menus_on_goal = pbool "Contextual menus on goal" contextual_menus_on_goal in @@ -1008,10 +998,6 @@ let configure ?(apply=(fun () -> ())) parent = Section("Externals", None, [cmd_coqtop;cmd_coqc;cmd_make;cmd_coqmakefile; cmd_coqdoc; cmd_print;cmd_editor;cmd_browse]); -(* - Section("Tactics Wizard", None, - [automatic_tactics]); -*) Section("Shortcuts", Some `PREFERENCES, [modifiers_valid; modifier_for_tactics; modifier_for_templates; modifier_for_display; modifier_for_navigation; diff --git a/kernel/byterun/coq_uint63_native.h b/kernel/byterun/coq_uint63_native.h index 1fdafc9d8f..9fbd3f83d8 100644 --- a/kernel/byterun/coq_uint63_native.h +++ b/kernel/byterun/coq_uint63_native.h @@ -111,51 +111,26 @@ value uint63_mulc(value x, value y, value* h) { #define le128(xh,xl,yh,yl) (uint63_lt(xh,yh) || (uint63_eq(xh,yh) && uint63_leq(xl,yl))) #define maxuint63 ((uint64_t)0x7FFFFFFFFFFFFFFF) -/* precondition: y <> 0 */ -/* outputs r and sets ql to q % 2^63 s.t. x = q * y + r, r < y */ +/* precondition: xh < y */ +/* outputs r and sets ql to q s.t. x = q * y + r, r < y */ static value uint63_div21_aux(value xh, value xl, value y, value* ql) { - xh = uint63_of_value(xh); - xl = uint63_of_value(xl); + uint64_t nh = uint63_of_value(xh); + uint64_t nl = uint63_of_value(xl); y = uint63_of_value(y); - uint64_t maskh = 0; - uint64_t maskl = 1; - uint64_t dh = 0; - uint64_t dl = y; - int cmp = 1; - /* int n = 0 */ - /* loop invariant: mask = 2^n, d = mask * y, (2 * d <= x -> cmp), n >= 0, d < 2^(2*63) */ - while (!(dh >> (63 - 1)) && cmp) { - dh = (dh << 1) | (dl >> (63 - 1)); - dl = (dl << 1) & maxuint63; - maskh = (maskh << 1) | (maskl >> (63 - 1)); - maskl = (maskl << 1) & maxuint63; - /* ++n */ - cmp = lt128(dh,dl,xh,xl); + uint64_t q = 0; + for (int i = 0; i < 63; ++i) { + // invariants: 0 <= nh < y, nl = (xl*2^i) % 2^64, + // (q*y + nh) * 2^(63-i) + (xl % 2^(63-i)) = (xh%y) * 2^63 + xl + nl <<= 1; + nh = (nh << 1) | (nl >> 63); + q <<= 1; + if (nh >= y) { q |= 1; nh -= y; } } - uint64_t remh = xh; - uint64_t reml = xl; - /* uint64_t quotienth = 0; */ - uint64_t quotientl = 0; - /* loop invariant: x = quotient * y + rem, y * 2^(n+1) > r, - mask = floor(2^n), d = mask * y, n >= -1 */ - while (maskh | maskl) { - if (le128(dh,dl,remh,reml)) { /* if rem >= d, add one bit and subtract d */ - /* quotienth = quotienth | maskh */ - quotientl = quotientl | maskl; - remh = (uint63_lt(reml,dl)) ? (remh - dh - 1) : (remh - dh); - reml = reml - dl; - } - maskl = (maskl >> 1) | ((maskh << (63 - 1)) & maxuint63); - maskh = maskh >> 1; - dl = (dl >> 1) | ((dh << (63 - 1)) & maxuint63); - dh = dh >> 1; - /* decr n */ - } - *ql = Val_int(quotientl); - return Val_int(reml); + *ql = Val_int(q); + return Val_int(nh); } value uint63_div21(value xh, value xl, value y, value* ql) { - if (uint63_of_value(y) == 0) { + if (uint63_leq(y, xh)) { *ql = Val_int(0); return Val_int(0); } else { diff --git a/kernel/cClosure.ml b/kernel/cClosure.ml index 1cc3dc3975..3fd613e905 100644 --- a/kernel/cClosure.ml +++ b/kernel/cClosure.ml @@ -1075,7 +1075,7 @@ module FNativeEntries = let mkInt env i = check_int env; - { mark = mark Norm KnownR; term = FInt i } + { mark = mark Cstr KnownR; term = FInt i } let mkBool env b = check_bool env; diff --git a/kernel/uint63.mli b/kernel/uint63.mli index 93632da110..5542716af2 100644 --- a/kernel/uint63.mli +++ b/kernel/uint63.mli @@ -37,6 +37,8 @@ val mul : t -> t -> t val div : t -> t -> t val rem : t -> t -> t +val diveucl : t -> t -> t * t + (* Specific arithmetic operations *) val mulc : t -> t -> t * t val addmuldiv : t -> t -> t -> t @@ -57,3 +59,13 @@ val head0 : t -> t val tail0 : t -> t val is_uint63 : Obj.t -> bool + +(* Arithmetic with explicit carries *) + +(* Analog of Numbers.Abstract.Cyclic.carry *) +type 'a carry = C0 of 'a | C1 of 'a + +val addc : t -> t -> t carry +val addcarryc : t -> t -> t carry +val subc : t -> t -> t carry +val subcarryc : t -> t -> t carry diff --git a/kernel/uint63_amd64_63.ml b/kernel/uint63_amd64_63.ml index 20b2f58496..5c4028e1c8 100644 --- a/kernel/uint63_amd64_63.ml +++ b/kernel/uint63_amd64_63.ml @@ -82,6 +82,8 @@ let div (x : int) (y : int) = let rem (x : int) (y : int) = if y = 0 then 0 else Int64.to_int (Int64.rem (to_uint64 x) (to_uint64 y)) +let diveucl x y = (div x y, rem x y) + let addmuldiv p x y = l_or (l_sl x p) (l_sr y (uint_size - p)) @@ -94,55 +96,32 @@ let le (x : int) (y : int) = (x lxor 0x4000000000000000) <= (y lxor 0x4000000000000000) [@@ocaml.inline always] -(* A few helper functions on 128 bits *) -let lt128 xh xl yh yl = - lt xh yh || (xh = yh && lt xl yl) - -let le128 xh xl yh yl = - lt xh yh || (xh = yh && le xl yl) - (* division of two numbers by one *) -(* precondition: y <> 0 *) -(* outputs: q % 2^63, r s.t. x = q * y + r, r < y *) +(* precondition: xh < y *) +(* outputs: q, r s.t. x = q * y + r, r < y *) let div21 xh xl y = - let maskh = ref 0 in - let maskl = ref 1 in - let dh = ref 0 in - let dl = ref y in - let cmp = ref true in - (* n = ref 0 *) - (* loop invariant: mask = 2^n, d = mask * y, (2 * d <= x -> cmp), n >= 0 *) - while !dh >= 0 && !cmp do (* dh >= 0 tests that dh highest bit is zero *) - (* We don't use addmuldiv below to avoid checks on 1 *) - dh := (!dh lsl 1) lor (!dl lsr (uint_size - 1)); - dl := !dl lsl 1; - maskh := (!maskh lsl 1) lor (!maskl lsr (uint_size - 1)); - maskl := !maskl lsl 1; - (* incr n *) - cmp := lt128 !dh !dl xh xl; - done; (* mask = 2^n, d = 2^n * y, 2 * d > x *) - let remh = ref xh in - let reml = ref xl in - (* quotienth = ref 0 *) - let quotientl = ref 0 in - (* loop invariant: x = quotient * y + rem, y * 2^(n+1) > r, - mask = floor(2^n), d = mask * y, n >= -1 *) - while !maskh lor !maskl <> 0 do - if le128 !dh !dl !remh !reml then begin (* if rem >= d, add one bit and subtract d *) - (* quotienth := !quotienth lor !maskh *) - quotientl := !quotientl lor !maskl; - remh := if lt !reml !dl then !remh - !dh - 1 else !remh - !dh; - reml := !reml - !dl; - end; - maskl := (!maskl lsr 1) lor (!maskh lsl (uint_size - 1)); - maskh := !maskh lsr 1; - dl := (!dl lsr 1) lor (!dh lsl (uint_size - 1)); - dh := !dh lsr 1; - (* decr n *) + (* nh might temporarily grow as large as 2*y - 1 in the loop body, + so we store it as a 64-bit unsigned integer *) + let nh = ref xh in + let nl = ref xl in + let q = ref 0 in + for _i = 0 to 62 do + (* invariants: 0 <= nh < y, nl = (xl*2^i) % 2^63, + (q*y + nh) * 2^(63-i) + (xl % 2^(63-i)) = (xh%y) * 2^63 + xl *) + nh := Int64.logor (Int64.shift_left !nh 1) (Int64.of_int (!nl lsr 62)); + nl := !nl lsl 1; + q := !q lsl 1; + (* TODO: use "Int64.unsigned_compare !nh y >= 0", + once OCaml 4.08 becomes the minimal required version *) + if Int64.compare !nh 0L < 0 || Int64.compare !nh y >= 0 then + begin q := !q lor 1; nh := Int64.sub !nh y; end done; - !quotientl, !reml + !q, Int64.to_int !nh -let div21 xh xl y = if y = 0 then 0, 0 else div21 xh xl y +let div21 xh xl y = + let xh = to_uint64 xh in + let y = to_uint64 y in + if Int64.compare y xh <= 0 then 0, 0 else div21 xh xl y (* exact multiplication *) (* TODO: check that none of these additions could be a logical or *) @@ -225,3 +204,24 @@ let tail0 x = let is_uint63 t = Obj.is_int t [@@ocaml.inline always] + +(* Arithmetic with explicit carries *) + +(* Analog of Numbers.Abstract.Cyclic.carry *) +type 'a carry = C0 of 'a | C1 of 'a + +let addc x y = + let r = x + y in + if lt r x then C1 r else C0 r + +let addcarryc x y = + let r = x + y + 1 in + if le r x then C1 r else C0 r + +let subc x y = + let r = x - y in + if le y x then C0 r else C1 r + +let subcarryc x y = + let r = x - y - 1 in + if lt y x then C0 r else C1 r diff --git a/kernel/uint63_i386_31.ml b/kernel/uint63_i386_31.ml index c3279779e1..b8eccd19fb 100644 --- a/kernel/uint63_i386_31.ml +++ b/kernel/uint63_i386_31.ml @@ -83,58 +83,33 @@ let div x y = let rem x y = if y = 0L then 0L else Int64.rem x y +let diveucl x y = (div x y, rem x y) + let addmuldiv p x y = l_or (l_sl x p) (l_sr y Int64.(sub (of_int uint_size) p)) -(* A few helper functions on 128 bits *) -let lt128 xh xl yh yl = - lt xh yh || (xh = yh && lt xl yl) - -let le128 xh xl yh yl = - lt xh yh || (xh = yh && le xl yl) - (* division of two numbers by one *) -(* precondition: y <> 0 *) -(* outputs: q % 2^63, r s.t. x = q * y + r, r < y *) +(* precondition: xh < y *) +(* outputs: q, r s.t. x = q * y + r, r < y *) let div21 xh xl y = - let maskh = ref zero in - let maskl = ref one in - let dh = ref zero in - let dl = ref y in - let cmp = ref true in - (* n = ref 0 *) - (* loop invariant: mask = 2^n, d = mask * y, (2 * d <= x -> cmp), n >= 0 *) - while Int64.equal (l_sr !dh (of_int (uint_size - 1))) zero && !cmp do - (* We don't use addmuldiv below to avoid checks on 1 *) - dh := l_or (l_sl !dh one) (l_sr !dl (of_int (uint_size - 1))); - dl := l_sl !dl one; - maskh := l_or (l_sl !maskh one) (l_sr !maskl (of_int (uint_size - 1))); - maskl := l_sl !maskl one; - (* incr n *) - cmp := lt128 !dh !dl xh xl; - done; (* mask = 2^n, d = 2^n * d, 2 * d > x *) - let remh = ref xh in - let reml = ref xl in - (* quotienth = ref 0 *) - let quotientl = ref zero in - (* loop invariant: x = quotient * y + rem, y * 2^(n+1) > r, - mask = floor(2^n), d = mask * y, n >= -1 *) - while not (Int64.equal (l_or !maskh !maskl) zero) do - if le128 !dh !dl !remh !reml then begin (* if rem >= d, add one bit and subtract d *) - (* quotienth := !quotienth lor !maskh *) - quotientl := l_or !quotientl !maskl; - remh := if lt !reml !dl then sub (sub !remh !dh) one else sub !remh !dh; - reml := sub !reml !dl - end; - maskl := l_or (l_sr !maskl one) (l_sl !maskh (of_int (uint_size - 1))); - maskh := l_sr !maskh one; - dl := l_or (l_sr !dl one) (l_sl !dh (of_int (uint_size - 1))); - dh := l_sr !dh one - (* decr n *) + let nh = ref xh in + let nl = ref xl in + let q = ref 0L in + for _i = 0 to 62 do + (* invariants: 0 <= nh < y, nl = (xl*2^i) % 2^64, + (q*y + nh) * 2^(63-i) + (xl % 2^(63-i)) = (xh%y) * 2^63 + xl *) + nl := Int64.shift_left !nl 1; + nh := Int64.logor (Int64.shift_left !nh 1) (Int64.shift_right_logical !nl 63); + q := Int64.shift_left !q 1; + (* TODO: use "Int64.unsigned_compare !nh y >= 0", + once OCaml 4.08 becomes the minimal required version *) + if Int64.compare !nh 0L < 0 || Int64.compare !nh y >= 0 then + begin q := Int64.logor !q 1L; nh := Int64.sub !nh y; end done; - !quotientl, !reml + !q, !nh -let div21 xh xl y = if Int64.equal y zero then zero, zero else div21 xh xl y +let div21 xh xl y = + if Int64.compare y xh <= 0 then zero, zero else div21 xh xl y (* exact multiplication *) let mulc x y = @@ -191,6 +166,27 @@ let is_uint63 t = Obj.is_block t && Int.equal (Obj.tag t) Obj.custom_tag && le (Obj.magic t) maxuint63 +(* Arithmetic with explicit carries *) + +(* Analog of Numbers.Abstract.Cyclic.carry *) +type 'a carry = C0 of 'a | C1 of 'a + +let addc x y = + let r = add x y in + if lt r x then C1 r else C0 r + +let addcarryc x y = + let r = addcarry x y in + if le r x then C1 r else C0 r + +let subc x y = + let r = sub x y in + if le y x then C0 r else C1 r + +let subcarryc x y = + let r = subcarry x y in + if lt y x then C0 r else C1 r + (* Register all exported functions so that they can be called from C code *) let () = diff --git a/plugins/extraction/ExtrOCamlInt63.v b/plugins/extraction/ExtrOCamlInt63.v new file mode 100644 index 0000000000..a2ee602313 --- /dev/null +++ b/plugins/extraction/ExtrOCamlInt63.v @@ -0,0 +1,56 @@ +(************************************************************************) +(* * The Coq Proof Assistant / The Coq Development Team *) +(* v * INRIA, CNRS and contributors - Copyright 1999-2019 *) +(* <O___,, * (see CREDITS file for the list of authors) *) +(* \VV/ **************************************************************) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(* * (see LICENSE file for the text of the license) *) +(************************************************************************) + +(** Extraction to OCaml of native 63-bit machine integers. *) + +From Coq Require Int63 Extraction. + +(** Basic data types used by some primitive operators. *) + +Extract Inductive bool => bool [ true false ]. +Extract Inductive prod => "( * )" [ "" ]. +Extract Inductive comparison => int [ "0" "(-1)" "1" ]. +Extract Inductive DoubleType.carry => "Uint63.carry" [ "Uint63.C0" "Uint63.C1" ]. + +(** Primitive types and operators. *) +Extract Constant Int63.int => "Uint63.t". +Extraction Inline Int63.int. +(* Otherwise, the name conflicts with the primitive OCaml type [int] *) + +Extract Constant Int63.lsl => "Uint63.l_sl". +Extract Constant Int63.lsr => "Uint63.l_sr". +Extract Constant Int63.land => "Uint63.l_and". +Extract Constant Int63.lor => "Uint63.l_or". +Extract Constant Int63.lxor => "Uint63.l_xor". + +Extract Constant Int63.add => "Uint63.add". +Extract Constant Int63.sub => "Uint63.sub". +Extract Constant Int63.mul => "Uint63.mul". +Extract Constant Int63.mulc => "Uint63.mulc". +Extract Constant Int63.div => "Uint63.div". +Extract Constant Int63.mod => "Uint63.rem". + +Extract Constant Int63.eqb => "Uint63.equal". +Extract Constant Int63.ltb => "Uint63.lt". +Extract Constant Int63.leb => "Uint63.le". + +Extract Constant Int63.addc => "Uint63.addc". +Extract Constant Int63.addcarryc => "Uint63.addcarryc". +Extract Constant Int63.subc => "Uint63.subc". +Extract Constant Int63.subcarryc => "Uint63.subcarryc". + +Extract Constant Int63.diveucl => "Uint63.diveucl". +Extract Constant Int63.diveucl_21 => "Uint63.div21". +Extract Constant Int63.addmuldiv => "Uint63.addmuldiv". + +Extract Constant Int63.compare => "Uint63.compare". + +Extract Constant Int63.head0 => "Uint63.head0". +Extract Constant Int63.tail0 => "Uint63.tail0". diff --git a/plugins/funind/g_indfun.mlg b/plugins/funind/g_indfun.mlg index 5f859b3e4b..1b75d3d966 100644 --- a/plugins/funind/g_indfun.mlg +++ b/plugins/funind/g_indfun.mlg @@ -148,9 +148,7 @@ END module Vernac = Pvernac.Vernac_ module Tactic = Pltac -type function_rec_definition_loc_argtype = (Vernacexpr.fixpoint_expr * Vernacexpr.decl_notation list) Loc.located - -let (wit_function_rec_definition_loc : function_rec_definition_loc_argtype Genarg.uniform_genarg_type) = +let (wit_function_rec_definition_loc : Vernacexpr.fixpoint_expr Loc.located Genarg.uniform_genarg_type) = Genarg.create_arg "function_rec_definition_loc" let function_rec_definition_loc = @@ -175,10 +173,10 @@ let () = let is_proof_termination_interactively_checked recsl = List.exists (function - | _,((_,( Some { CAst.v = CMeasureRec _ } - | Some { CAst.v = CWfRec _}),_,_,_),_) -> true - | _,((_,Some { CAst.v = CStructRec _ },_,_,_),_) - | _,((_,None,_,_,_),_) -> false) recsl + | _,( Vernacexpr.{ rec_order = Some { CAst.v = CMeasureRec _ } } + | Vernacexpr.{ rec_order = Some { CAst.v = CWfRec _} }) -> true + | _, Vernacexpr.{ rec_order = Some { CAst.v = CStructRec _ } } + | _, Vernacexpr.{ rec_order = None } -> false) recsl let classify_as_Fixpoint recsl = Vernac_classifier.classify_vernac diff --git a/plugins/funind/indfun.ml b/plugins/funind/indfun.ml index 6e19ef4804..1987677d7d 100644 --- a/plugins/funind/indfun.ml +++ b/plugins/funind/indfun.ml @@ -1,3 +1,13 @@ +(************************************************************************) +(* * The Coq Proof Assistant / The Coq Development Team *) +(* v * INRIA, CNRS and contributors - Copyright 1999-2019 *) +(* <O___,, * (see CREDITS file for the list of authors) *) +(* \VV/ **************************************************************) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(* * (see LICENSE file for the text of the license) *) +(************************************************************************) + open CErrors open Sorts open Util @@ -157,17 +167,16 @@ let interp_casted_constr_with_implicits env sigma impls c = and not as a constr *) -let build_newrecursive - lnameargsardef = +let build_newrecursive lnameargsardef = let env0 = Global.env() in let sigma = Evd.from_env env0 in let (rec_sign,rec_impls) = List.fold_left - (fun (env,impls) (({CAst.v=recname},_),bl,arityc,_) -> - let arityc = Constrexpr_ops.mkCProdN bl arityc in + (fun (env,impls) { Vernacexpr.fname={CAst.v=recname}; binders; rtype } -> + let arityc = Constrexpr_ops.mkCProdN binders rtype in let arity,ctx = Constrintern.interp_type env0 sigma arityc in let evd = Evd.from_env env0 in - let evd, (_, (_, impls')) = Constrintern.interp_context_evars ~program_mode:false env evd bl in + let evd, (_, (_, impls')) = Constrintern.interp_context_evars ~program_mode:false env evd binders in let impl = Constrintern.compute_internalization_data env0 evd Constrintern.Recursive arity impls' in let open Context.Named.Declaration in let r = Sorts.Relevant in (* TODO relevance *) @@ -175,26 +184,18 @@ let build_newrecursive (env0,Constrintern.empty_internalization_env) lnameargsardef in let recdef = (* Declare local notations *) - let f (_,bl,_,def) = - let def = abstract_glob_constr def bl in - interp_casted_constr_with_implicits - rec_sign sigma rec_impls def + let f { Vernacexpr.binders; body_def } = + match body_def with + | Some body_def -> + let def = abstract_glob_constr body_def binders in + interp_casted_constr_with_implicits + rec_sign sigma rec_impls def + | None -> user_err ~hdr:"Function" (str "Body of Function must be given") in States.with_state_protection (List.map f) lnameargsardef in recdef,rec_impls -let build_newrecursive l = - let l' = List.map - (fun ((fixna,_,bll,ar,body_opt),lnot) -> - match body_opt with - | Some body -> - (fixna,bll,ar,body) - | None -> user_err ~hdr:"Function" (str "Body of Function must be given") - ) l - in - build_newrecursive l' - let error msg = user_err Pp.(str msg) (* Checks whether or not the mutual bloc is recursive *) @@ -237,8 +238,8 @@ let rec local_binders_length = function | Constrexpr.CLocalAssum (idl,_,_)::bl -> List.length idl + local_binders_length bl | Constrexpr.CLocalPattern _::bl -> assert false -let prepare_body ((name,_,args,types,_),_) rt = - let n = local_binders_length args in +let prepare_body { Vernacexpr.binders; rtype } rt = + let n = local_binders_length binders in (* Pp.msgnl (str "nb lambda to chop : " ++ str (string_of_int n) ++ fnl () ++Printer.pr_glob_constr rt); *) let fun_args,rt' = chop_rlambda_n n rt in (fun_args,rt') @@ -336,13 +337,13 @@ let error_error names e = | _ -> raise e let generate_principle (evd:Evd.evar_map ref) pconstants on_error - is_general do_built (fix_rec_l:(Vernacexpr.fixpoint_expr * Vernacexpr.decl_notation list) list) recdefs interactive_proof + is_general do_built (fix_rec_l : Vernacexpr.fixpoint_expr list) recdefs interactive_proof (continue_proof : int -> Names.Constant.t array -> EConstr.constr array -> int -> Tacmach.tactic) : unit = - let names = List.map (function (({CAst.v=name},_),_,_,_,_),_ -> name) fix_rec_l in + let names = List.map (function { Vernacexpr.fname = {CAst.v=name} } -> name) fix_rec_l in let fun_bodies = List.map2 prepare_body fix_rec_l recdefs in let funs_args = List.map fst fun_bodies in - let funs_types = List.map (function ((_,_,_,types,_),_) -> types) fix_rec_l in + let funs_types = List.map (function { Vernacexpr.rtype } -> rtype) fix_rec_l in try (* We then register the Inductive graphs of the functions *) Glob_term_to_relation.build_inductive !evd pconstants funs_args funs_types recdefs; @@ -359,7 +360,7 @@ let generate_principle (evd:Evd.evar_map ref) pconstants on_error locate_ind f_R_mut) in - let fname_kn (((fname,_),_,_,_,_),_) = + let fname_kn { Vernacexpr.fname } = let f_ref = qualid_of_ident ?loc:fname.CAst.loc fname.CAst.v in locate_with_msg (pr_qualid f_ref++str ": Not an inductive type!") @@ -398,23 +399,25 @@ let generate_principle (evd:Evd.evar_map ref) pconstants on_error with e when CErrors.noncritical e -> on_error names e -let register_struct is_rec (fixpoint_exprl:(Vernacexpr.fixpoint_expr * Vernacexpr.decl_notation list) list) = +let register_struct is_rec (fixpoint_exprl: Vernacexpr.fixpoint_expr list) = match fixpoint_exprl with - | [(({CAst.v=fname},pl),_,bl,ret_type,body),_] when not is_rec -> - let body = match body with | Some body -> body | None -> user_err ~hdr:"Function" (str "Body of Function must be given") in + | [ { Vernacexpr.fname; univs; binders; rtype; body_def } ] when not is_rec -> + let body = match body_def with + | Some body -> body + | None -> user_err ~hdr:"Function" (str "Body of Function must be given") in ComDefinition.do_definition ~program_mode:false - ~name:fname + ~name:fname.CAst.v ~poly:false ~scope:(DeclareDef.Global Declare.ImportDefaultBehavior) - ~kind:Decls.Definition pl - bl None body (Some ret_type); + ~kind:Decls.Definition univs + binders None body (Some rtype); let evd,rev_pconstants = List.fold_left - (fun (evd,l) ((({CAst.v=fname},_),_,_,_,_),_) -> + (fun (evd,l) { Vernacexpr.fname } -> let evd,c = Evd.fresh_global - (Global.env ()) evd (Constrintern.locate_reference (Libnames.qualid_of_ident fname)) in + (Global.env ()) evd (Constrintern.locate_reference (Libnames.qualid_of_ident fname.CAst.v)) in let (cst, u) = destConst evd c in let u = EInstance.kind evd u in evd,((cst, u) :: l) @@ -427,10 +430,10 @@ let register_struct is_rec (fixpoint_exprl:(Vernacexpr.fixpoint_expr * Vernacexp ComFixpoint.do_fixpoint ~scope:(DeclareDef.Global Declare.ImportDefaultBehavior) ~poly:false fixpoint_exprl; let evd,rev_pconstants = List.fold_left - (fun (evd,l) ((({CAst.v=fname},_),_,_,_,_),_) -> + (fun (evd,l) { Vernacexpr.fname } -> let evd,c = Evd.fresh_global - (Global.env ()) evd (Constrintern.locate_reference (Libnames.qualid_of_ident fname)) in + (Global.env ()) evd (Constrintern.locate_reference (Libnames.qualid_of_ident fname.CAst.v)) in let (cst, u) = destConst evd c in let u = EInstance.kind evd u in evd,((cst, u) :: l) @@ -464,7 +467,7 @@ let register_wf interactive_proof ?(is_mes=false) fname rec_impls wf_rel_expr wf let unbounded_eq = let f_app_args = CAst.make @@ Constrexpr.CAppExpl( - (None,qualid_of_ident fname,None) , + (None,qualid_of_ident fname.CAst.v,None) , (List.map (function | {CAst.v=Anonymous} -> assert false @@ -485,13 +488,13 @@ let register_wf interactive_proof ?(is_mes=false) fname rec_impls wf_rel_expr wf (generate_correction_proof_wf f_ref tcc_lemma_ref is_mes functional_ref eq_ref rec_arg_num rec_arg_type nb_args relation ); - derive_inversion [fname] + derive_inversion [fname.CAst.v] with e when CErrors.noncritical e -> (* No proof done *) () in Recdef.recursive_definition ~interactive_proof - ~is_mes fname rec_impls + ~is_mes fname.CAst.v rec_impls type_of_f wf_rel_expr rec_arg_num @@ -607,88 +610,93 @@ and rebuild_nal aux bk bl' nal typ = let rebuild_bl aux bl typ = rebuild_bl aux bl typ -let recompute_binder_list (fixpoint_exprl : (Vernacexpr.fixpoint_expr * Vernacexpr.decl_notation list) list) = - let fixl,ntns = ComFixpoint.extract_fixpoint_components ~structonly:false fixpoint_exprl in - let ((_,_,_,typel),_,ctx,_) = ComFixpoint.interp_fixpoint ~cofix:false fixl ntns in +let recompute_binder_list fixpoint_exprl = + let fixl = + List.map (fun fix -> Vernacexpr.{ + fix + with rec_order = ComFixpoint.adjust_rec_order ~structonly:false fix.binders fix.rec_order }) fixpoint_exprl in + let ((_,_,_,typel),_,ctx,_) = ComFixpoint.interp_fixpoint ~cofix:false fixl in let constr_expr_typel = with_full_print (List.map (fun c -> Constrextern.extern_constr false (Global.env ()) (Evd.from_ctx ctx) (EConstr.of_constr c))) typel in let fixpoint_exprl_with_new_bl = - List.map2 (fun ((lna,rec_order_opt,bl,ret_typ,opt_body),notation_list) fix_typ -> - - let new_bl',new_ret_type = rebuild_bl [] bl fix_typ in - (((lna,rec_order_opt,new_bl',new_ret_type,opt_body),notation_list):(Vernacexpr.fixpoint_expr * Vernacexpr.decl_notation list)) - ) - fixpoint_exprl constr_expr_typel + List.map2 (fun ({ Vernacexpr.binders } as fp) fix_typ -> + let binders, rtype = rebuild_bl [] binders fix_typ in + { fp with Vernacexpr.binders; rtype } + ) fixpoint_exprl constr_expr_typel in fixpoint_exprl_with_new_bl let do_generate_principle_aux pconstants on_error register_built interactive_proof - (fixpoint_exprl:(Vernacexpr.fixpoint_expr * Vernacexpr.decl_notation list) list) : Lemmas.t option = - List.iter (fun (_,l) -> if not (List.is_empty l) then error "Function does not support notations for now") fixpoint_exprl; + (fixpoint_exprl : Vernacexpr.fixpoint_expr list) : Lemmas.t option = + List.iter (fun { Vernacexpr.notations } -> + if not (List.is_empty notations) + then error "Function does not support notations for now") fixpoint_exprl; let lemma, _is_struct = match fixpoint_exprl with - | [((_,Some {CAst.v = Constrexpr.CWfRec (wf_x,wf_rel)},_,_,_),_) as fixpoint_expr] -> - let (((({CAst.v=name},pl),_,args,types,body)),_) as fixpoint_expr = - match recompute_binder_list [fixpoint_expr] with - | [e] -> e - | _ -> assert false - in - let fixpoint_exprl = [fixpoint_expr] in - let body = match body with | Some body -> body | None -> user_err ~hdr:"Function" (str "Body of Function must be given") in - let recdefs,rec_impls = build_newrecursive fixpoint_exprl in - let using_lemmas = [] in - let pre_hook pconstants = - generate_principle - (ref (Evd.from_env (Global.env ()))) - pconstants - on_error - true - register_built - fixpoint_exprl - recdefs - true - in - if register_built - then register_wf interactive_proof name rec_impls wf_rel wf_x.CAst.v using_lemmas args types body pre_hook, false - else None, false - |[((_,Some {CAst.v = Constrexpr.CMeasureRec(wf_x,wf_mes,wf_rel_opt)},_,_,_),_) as fixpoint_expr] -> - let (((({CAst.v=name},_),_,args,types,body)),_) as fixpoint_expr = - match recompute_binder_list [fixpoint_expr] with - | [e] -> e - | _ -> assert false - in - let fixpoint_exprl = [fixpoint_expr] in - let recdefs,rec_impls = build_newrecursive fixpoint_exprl in - let using_lemmas = [] in - let body = match body with | Some body -> body | None -> user_err ~hdr:"Function" (str "Body of Function must be given") in - let pre_hook pconstants = - generate_principle - (ref (Evd.from_env (Global.env ()))) - pconstants - on_error - true - register_built - fixpoint_exprl - recdefs - true - in - if register_built - then register_mes interactive_proof name rec_impls wf_mes wf_rel_opt (map_option (fun x -> x.CAst.v) wf_x) using_lemmas args types body pre_hook, true - else None, true + | [{ Vernacexpr.rec_order = Some {CAst.v = Constrexpr.CWfRec (wf_x,wf_rel)} } as fixpoint_expr] -> + let { Vernacexpr.fname; univs; binders; rtype; body_def } as fixpoint_expr = + match recompute_binder_list [fixpoint_expr] with + | [e] -> e + | _ -> assert false + in + let fixpoint_exprl = [fixpoint_expr] in + let body = match body_def with + | Some body -> body + | None -> user_err ~hdr:"Function" (str "Body of Function must be given") in + let recdefs,rec_impls = build_newrecursive fixpoint_exprl in + let using_lemmas = [] in + let pre_hook pconstants = + generate_principle + (ref (Evd.from_env (Global.env ()))) + pconstants + on_error + true + register_built + fixpoint_exprl + recdefs + true + in + if register_built + then register_wf interactive_proof fname rec_impls wf_rel wf_x.CAst.v using_lemmas binders rtype body pre_hook, false + else None, false + |[{ Vernacexpr.rec_order=Some {CAst.v = Constrexpr.CMeasureRec(wf_x,wf_mes,wf_rel_opt)} } as fixpoint_expr] -> + let { Vernacexpr.fname; univs; binders; rtype; body_def} as fixpoint_expr = + match recompute_binder_list [fixpoint_expr] with + | [e] -> e + | _ -> assert false + in + let fixpoint_exprl = [fixpoint_expr] in + let recdefs,rec_impls = build_newrecursive fixpoint_exprl in + let using_lemmas = [] in + let body = match body_def with + | Some body -> body + | None -> user_err ~hdr:"Function" (str "Body of Function must be given") in + let pre_hook pconstants = + generate_principle + (ref (Evd.from_env (Global.env ()))) + pconstants + on_error + true + register_built + fixpoint_exprl + recdefs + true + in + if register_built + then register_mes interactive_proof fname rec_impls wf_mes wf_rel_opt (map_option (fun x -> x.CAst.v) wf_x) using_lemmas binders rtype body pre_hook, true + else None, true | _ -> - List.iter (function ((_na,ord,_args,_body,_type),_not) -> - match ord with - | Some { CAst.v = (Constrexpr.CMeasureRec _ | Constrexpr.CWfRec _) } -> - error - ("Cannot use mutual definition with well-founded recursion or measure") - | _ -> () + List.iter (function { Vernacexpr.rec_order } -> + match rec_order with + | Some { CAst.v = (Constrexpr.CMeasureRec _ | Constrexpr.CWfRec _) } -> + error + ("Cannot use mutual definition with well-founded recursion or measure") + | _ -> () ) fixpoint_exprl; let fixpoint_exprl = recompute_binder_list fixpoint_exprl in - let fix_names = - List.map (function ((({CAst.v=name},_),_,_,_,_),_) -> name) fixpoint_exprl - in + let fix_names = List.map (function { Vernacexpr.fname } -> fname.CAst.v) fixpoint_exprl in (* ok all the expressions are structural *) let recdefs,rec_impls = build_newrecursive fixpoint_exprl in let is_rec = List.exists (is_rec fix_names) recdefs in @@ -845,59 +853,59 @@ let make_graph (f_ref : GlobRef.t) = | None -> error "Cannot build a graph over an axiom!" | Some (body, _, _) -> let env = Global.env () in - let extern_body,extern_type = - with_full_print (fun () -> - (Constrextern.extern_constr false env sigma (EConstr.of_constr body), - Constrextern.extern_type false env sigma - (EConstr.of_constr (*FIXME*) c_body.const_type) - ) + let extern_body,extern_type = + with_full_print (fun () -> + (Constrextern.extern_constr false env sigma (EConstr.of_constr body), + Constrextern.extern_type false env sigma + (EConstr.of_constr (*FIXME*) c_body.const_type) ) - () - in - let (nal_tas,b,t) = get_args extern_body extern_type in - let expr_list = - match b.CAst.v with - | Constrexpr.CFix(l_id,fixexprl) -> - let l = - List.map - (fun (id,recexp,bl,t,b) -> - let { CAst.loc; v=rec_id } = match Option.get recexp with - | { CAst.v = CStructRec id } -> id - | { CAst.v = CWfRec (id,_) } -> id - | { CAst.v = CMeasureRec (oid,_,_) } -> Option.get oid - in - let new_args = - List.flatten - (List.map - (function - | Constrexpr.CLocalDef (na,_,_)-> [] - | Constrexpr.CLocalAssum (nal,_,_) -> - List.map - (fun {CAst.loc;v=n} -> CAst.make ?loc @@ - CRef(Libnames.qualid_of_ident ?loc @@ Nameops.Name.get_id n,None)) - nal - | Constrexpr.CLocalPattern _ -> assert false - ) - nal_tas - ) - in - let b' = add_args id.CAst.v new_args b in - ((((id,None), ( Some (CAst.make (CStructRec (CAst.make rec_id)))),nal_tas@bl,t,Some b'),[]):(Vernacexpr.fixpoint_expr * Vernacexpr.decl_notation list)) - ) - fixexprl + ) () + in + let (nal_tas,b,t) = get_args extern_body extern_type in + let expr_list = + match b.CAst.v with + | Constrexpr.CFix(l_id,fixexprl) -> + let l = + List.map + (fun (id,recexp,bl,t,b) -> + let { CAst.loc; v=rec_id } = match Option.get recexp with + | { CAst.v = CStructRec id } -> id + | { CAst.v = CWfRec (id,_) } -> id + | { CAst.v = CMeasureRec (oid,_,_) } -> Option.get oid + in + let new_args = + List.flatten + (List.map + (function + | Constrexpr.CLocalDef (na,_,_)-> [] + | Constrexpr.CLocalAssum (nal,_,_) -> + List.map + (fun {CAst.loc;v=n} -> CAst.make ?loc @@ + CRef(Libnames.qualid_of_ident ?loc @@ Nameops.Name.get_id n,None)) + nal + | Constrexpr.CLocalPattern _ -> assert false + ) + nal_tas + ) in - l - | _ -> - let id = Label.to_id (Constant.label c) in - [((CAst.make id,None),None,nal_tas,t,Some b),[]] - in - let mp = Constant.modpath c in - let pstate = do_generate_principle_aux [c,Univ.Instance.empty] error_error false false expr_list in - assert (Option.is_empty pstate); - (* We register the infos *) - List.iter - (fun ((({CAst.v=id},_),_,_,_,_),_) -> add_Function false (Constant.make2 mp (Label.of_id id))) - expr_list) + let b' = add_args id.CAst.v new_args b in + { Vernacexpr.fname=id; univs=None + ; rec_order = Some (CAst.make (CStructRec (CAst.make rec_id))) + ; binders = nal_tas@bl; rtype=t; body_def=Some b'; notations = []} + ) fixexprl in + l + | _ -> + let fname = CAst.make (Label.to_id (Constant.label c)) in + [{ Vernacexpr.fname; univs=None; rec_order = None; binders=nal_tas; rtype=t; body_def=Some b; notations=[]}] + in + let mp = Constant.modpath c in + let pstate = do_generate_principle_aux [c,Univ.Instance.empty] error_error false false expr_list in + assert (Option.is_empty pstate); + (* We register the infos *) + List.iter + (fun { Vernacexpr.fname= {CAst.v=id} } -> + add_Function false (Constant.make2 mp (Label.of_id id))) + expr_list) (* *************** statically typed entrypoints ************************* *) diff --git a/plugins/funind/indfun.mli b/plugins/funind/indfun.mli index 3bc52272ac..bfc9686ae5 100644 --- a/plugins/funind/indfun.mli +++ b/plugins/funind/indfun.mli @@ -5,12 +5,9 @@ val warn_cannot_define_graph : ?loc:Loc.t -> Pp.t * Pp.t -> unit val warn_cannot_define_principle : ?loc:Loc.t -> Pp.t * Pp.t -> unit -val do_generate_principle : - (Vernacexpr.fixpoint_expr * Vernacexpr.decl_notation list) list -> unit +val do_generate_principle : Vernacexpr.fixpoint_expr list -> unit -val do_generate_principle_interactive : - (Vernacexpr.fixpoint_expr * Vernacexpr.decl_notation list) list -> - Lemmas.t +val do_generate_principle_interactive : Vernacexpr.fixpoint_expr list -> Lemmas.t val functional_induction : bool -> diff --git a/pretyping/unification.ml b/pretyping/unification.ml index 00831b5962..a9eb43e573 100644 --- a/pretyping/unification.ml +++ b/pretyping/unification.ml @@ -839,8 +839,9 @@ let rec unify_0_with_initial_metas (sigma,ms,es as subst : subst0) conv_at_top e unify_app_pattern true curenvnb pb opt substn cM f1 l1 cN f2 l2 | _ -> raise ex) - | Case (_,p1,c1,cl1), Case (_,p2,c2,cl2) -> - (try + | Case (ci1,p1,c1,cl1), Case (ci2,p2,c2,cl2) -> + (try + if not (eq_ind ci1.ci_ind ci2.ci_ind) then error_cannot_unify curenv sigma (cM,cN); let opt' = {opt with at_top = true; with_types = false} in Array.fold_left2 (unirec_rec curenvnb CONV {opt with at_top = true}) (unirec_rec curenvnb CONV opt' diff --git a/stm/stm.ml b/stm/stm.ml index d5e6e6fd8b..69dbebbc57 100644 --- a/stm/stm.ml +++ b/stm/stm.ml @@ -1073,7 +1073,7 @@ let stm_vernac_interp ?route id st { verbose; expr } : Vernacstate.t = *) let is_filtered_command = function | VernacResetName _ | VernacResetInitial | VernacBack _ - | VernacBackTo _ | VernacRestart | VernacUndo _ | VernacUndoTo _ + | VernacRestart | VernacUndo _ | VernacUndoTo _ | VernacAbortAll | VernacAbort _ -> true | _ -> false in @@ -1216,8 +1216,6 @@ end = struct (* {{{ *) match Vcs_.branches vcs with [_] -> `Stop id | _ -> `Cont ()) () id in oid - | VernacBackTo id -> - Stateid.of_int id | _ -> anomaly Pp.(str "incorrect VtMeta classification") with | Not_found -> diff --git a/stm/vernac_classifier.ml b/stm/vernac_classifier.ml index aaba36287a..5af576dad2 100644 --- a/stm/vernac_classifier.ml +++ b/stm/vernac_classifier.ml @@ -106,8 +106,8 @@ let classify_vernac e = else GuaranteesOpacity in let ids, open_proof = - List.fold_left (fun (l,b) ((({v=id},_),_,_,_,p),_) -> - id::l, b || p = None) ([],false) l in + List.fold_left (fun (l,b) {Vernacexpr.fname={CAst.v=id}; body_def} -> + id::l, b || body_def = None) ([],false) l in if open_proof then VtStartProof (guarantee,ids) else VtSideff (ids, VtLater) @@ -118,8 +118,8 @@ let classify_vernac e = else GuaranteesOpacity in let ids, open_proof = - List.fold_left (fun (l,b) ((({v=id},_),_,_,p),_) -> - id::l, b || p = None) ([],false) l in + List.fold_left (fun (l,b) { Vernacexpr.fname={CAst.v=id}; body_def } -> + id::l, b || body_def = None) ([],false) l in if open_proof then VtStartProof (guarantee,ids) else VtSideff (ids, VtLater) @@ -193,7 +193,7 @@ let classify_vernac e = | VernacBack _ | VernacAbortAll | VernacUndoTo _ | VernacUndo _ | VernacResetName _ | VernacResetInitial - | VernacBackTo _ | VernacRestart -> VtMeta + | VernacRestart -> VtMeta (* What are these? *) | VernacRestoreState _ | VernacWriteState _ -> VtSideff ([], VtNow) diff --git a/test-suite/arithmetic/diveucl_21.v b/test-suite/arithmetic/diveucl_21.v index b888c97be3..b12dba429c 100644 --- a/test-suite/arithmetic/diveucl_21.v +++ b/test-suite/arithmetic/diveucl_21.v @@ -10,11 +10,11 @@ Check (eq_refl (4611686018427387904,1) <<: diveucl_21 1 1 2 = (46116860184273879 Definition compute1 := Eval compute in diveucl_21 1 1 2. Check (eq_refl compute1 : (4611686018427387904,1) = (4611686018427387904,1)). -Check (eq_refl : diveucl_21 3 1 2 = (4611686018427387904, 1)). -Check (eq_refl (4611686018427387904, 1) <: diveucl_21 3 1 2 = (4611686018427387904, 1)). -Check (eq_refl (4611686018427387904, 1) <<: diveucl_21 3 1 2 = (4611686018427387904, 1)). +Check (eq_refl : diveucl_21 3 1 2 = (0, 0)). +Check (eq_refl (0, 0) <: diveucl_21 3 1 2 = (0, 0)). +Check (eq_refl (0, 0) <<: diveucl_21 3 1 2 = (0, 0)). Definition compute2 := Eval compute in diveucl_21 3 1 2. -Check (eq_refl compute2 : (4611686018427387904, 1) = (4611686018427387904, 1)). +Check (eq_refl compute2 : (0, 0) = (0, 0)). Check (eq_refl : diveucl_21 1 1 0 = (0,0)). Check (eq_refl (0,0) <: diveucl_21 1 1 0 = (0,0)). @@ -23,3 +23,7 @@ Check (eq_refl (0,0) <<: diveucl_21 1 1 0 = (0,0)). Check (eq_refl : diveucl_21 9223372036854775807 0 1 = (0,0)). Check (eq_refl (0,0) <: diveucl_21 9223372036854775807 0 1 = (0,0)). Check (eq_refl (0,0) <<: diveucl_21 9223372036854775807 0 1 = (0,0)). + +Check (eq_refl : diveucl_21 9305446873517 1793572051078448654 4930380657631323783 = (17407905077428, 3068214991893055266)). +Check (eq_refl (17407905077428, 3068214991893055266) <: diveucl_21 9305446873517 1793572051078448654 4930380657631323783 = (17407905077428, 3068214991893055266)). +Check (eq_refl (17407905077428, 3068214991893055266) <<: diveucl_21 9305446873517 1793572051078448654 4930380657631323783 = (17407905077428, 3068214991893055266)). diff --git a/test-suite/bugs/closed/bug_10533.v b/test-suite/bugs/closed/bug_10533.v new file mode 100644 index 0000000000..e72957bdee --- /dev/null +++ b/test-suite/bugs/closed/bug_10533.v @@ -0,0 +1,8 @@ + +Require Import Eqdep Setoid. +Goal forall (t : unit) (pf : tt = t), + if (match pf with eq_refl => false end) then True else False. +Proof. + intros. + try setoid_rewrite <-Eqdep.Eq_rect_eq.eq_rect_eq. +Abort. diff --git a/test-suite/bugs/closed/bug_10560.v b/test-suite/bugs/closed/bug_10560.v new file mode 100644 index 0000000000..a9a0949d9a --- /dev/null +++ b/test-suite/bugs/closed/bug_10560.v @@ -0,0 +1,9 @@ +From Coq Require Import Int63. +Open Scope int63_scope. + +Lemma foo : + let n := opp 0 in add n 0 = n. +Proof. +cbv. +apply eq_refl. +Qed. diff --git a/theories/Numbers/Cyclic/Int63/Int63.v b/theories/Numbers/Cyclic/Int63/Int63.v index 9bb16b97e2..9e9481341f 100644 --- a/theories/Numbers/Cyclic/Int63/Int63.v +++ b/theories/Numbers/Cyclic/Int63/Int63.v @@ -388,7 +388,7 @@ 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 - [|q|] = Z.modulo q' wB /\ [|r|] = r'. + [|a1|] < [|b|] -> [|q|] = q' /\ [|r|] = r'. Axiom addmuldiv_def_spec : forall p x y, addmuldiv p x y = addmuldiv_def p x y. @@ -812,14 +812,6 @@ Proof. eapply Z.lt_le_trans; [ | apply Zpower2_le_lin ]; auto with zarith. Qed. -Lemma lsr_add_distr x y n: (x + y) << n = ((x << n) + (y << n))%int63. -Proof. - apply to_Z_inj. - rewrite -> add_spec, !lsl_spec, add_spec. - rewrite -> Zmult_mod_idemp_l, <-Zplus_mod. - apply f_equal2 with (f := Zmod); auto with zarith. -Qed. - (* LSL *) Lemma lsl0 i: 0 << i = 0%int63. Proof. @@ -1119,7 +1111,7 @@ Proof. generalize (add_le_r x y); rewrite Heq, lor_le; intro Hb. generalize Heq; rewrite (bit_split x) at 1; rewrite (bit_split y )at 1; clear Heq. rewrite (fun y => add_comm y (bit x 0)), <-!add_assoc, add_comm, - <-!add_assoc, (add_comm (bit y 0)), add_assoc, <-lsr_add_distr. + <-!add_assoc, (add_comm (bit y 0)), add_assoc, <-lsl_add_distr. rewrite (bit_split (x lor y)), lor_spec. intros Heq. assert (F: (bit x 0 + bit y 0)%int63 = (bit x 0 || bit y 0)). @@ -1429,26 +1421,9 @@ Proof. 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|]). - intros (H', H''); rewrite H', H''; clear H' H''. + intros (H', H''); auto; rewrite H', H''; clear H' H''. intros (H', H''); split; [ |exact H'']. - rewrite H', Zmult_comm, Z.mod_small; [reflexivity| ]. - split. - { revert H'; case z; [now simpl..|intros p H']. - exfalso; apply (Z.lt_irrefl 0), (Z.le_lt_trans _ ([|a1|] * wB + [|a2|])). - { now apply Z.add_nonneg_nonneg; [apply Z.mul_nonneg_nonneg| ]. } - rewrite H'; apply (Zplus_lt_reg_r _ _ (- z0)); ring_simplify. - apply (Z.le_lt_trans _ (- [|b|])); [ |now auto with zarith]. - rewrite Z.opp_eq_mul_m1; apply Zmult_le_compat_l; [ |now apply Wb]. - rewrite <-!Pos2Z.opp_pos, <-Z.opp_le_mono. - now change 1 with (Z.succ 0); apply Zlt_le_succ. } - rewrite <-Z.nle_gt; intro Hz; revert H2; apply Zle_not_lt. - rewrite (Z.div_unique_pos (wB * [|a1|] + [|a2|]) wB [|a1|] [|a2|]); - [ |now simpl..]. - rewrite Z.mul_comm, H'. - rewrite (Z.div_unique_pos (wB * [|b|] + z0) wB [|b|] z0) at 1; - [ |split; [ |apply (Z.lt_trans _ [|b|])]; now simpl|reflexivity]. - apply Z_div_le; [now simpl| ]; rewrite Z.mul_comm; apply Zplus_le_compat_r. - now apply Zmult_le_compat_l. + now rewrite H', Zmult_comm. Qed. Lemma div2_phi ih il j: (2^62 <= [|j|] -> [|ih|] < [|j|] -> diff --git a/theories/Numbers/Cyclic/ZModulo/ZModulo.v b/theories/Numbers/Cyclic/ZModulo/ZModulo.v index 28565b2fe3..2785e89c5d 100644 --- a/theories/Numbers/Cyclic/ZModulo/ZModulo.v +++ b/theories/Numbers/Cyclic/ZModulo/ZModulo.v @@ -648,40 +648,15 @@ Section ZModulo. apply two_power_pos_correct. Qed. - Definition head0 x := match [|x|] with + Definition head0 x := + match [| x |] with | Z0 => zdigits - | Zpos p => zdigits - log_inf p - 1 - | _ => 0 - end. + | Zneg _ => 0 + | (Zpos _) as p => zdigits - Z.log2 p - 1 + end. Lemma spec_head00: forall x, [|x|] = 0 -> [|head0 x|] = Zpos digits. - Proof. - unfold head0; intros. - rewrite H; simpl. - apply spec_zdigits. - Qed. - - Lemma log_inf_bounded : forall x p, Zpos x < 2^p -> log_inf x < p. - Proof. - induction x; simpl; intros. - - assert (0 < p) by (destruct p; compute; auto with zarith; discriminate). - cut (log_inf x < p - 1); [omega| ]. - apply IHx. - change (Zpos x~1) with (2*(Zpos x)+1) in H. - replace p with (Z.succ (p-1)) in H; auto with zarith. - rewrite Z.pow_succ_r in H; auto with zarith. - - assert (0 < p) by (destruct p; compute; auto with zarith; discriminate). - cut (log_inf x < p - 1); [omega| ]. - apply IHx. - change (Zpos x~0) with (2*(Zpos x)) in H. - replace p with (Z.succ (p-1)) in H; auto with zarith. - rewrite Z.pow_succ_r in H; auto with zarith. - - simpl; intros; destruct p; compute; auto with zarith. - Qed. - + Proof. unfold head0; intros x ->; apply spec_zdigits. Qed. Lemma spec_head0 : forall x, 0 < [|x|] -> wB/ 2 <= 2 ^ ([|head0 x|]) * [|x|] < wB. @@ -689,36 +664,35 @@ Section ZModulo. intros; unfold head0. generalize (spec_to_Z x). destruct [|x|]; try discriminate. + pose proof (Z.log2_nonneg (Zpos p)). + destruct (Z.log2_spec (Zpos p)); auto. intros. - destruct (log_inf_correct p). - rewrite 2 two_p_power2 in H2; auto with zarith. - assert (0 <= zdigits - log_inf p - 1 < wB). + assert (0 <= zdigits - Z.log2 (Zpos p) - 1 < wB) as Hrange. split. - cut (log_inf p < zdigits); try omega. + cut (Z.log2 (Zpos p) < zdigits). omega. unfold zdigits. unfold wB, base in *. - apply log_inf_bounded; auto with zarith. + apply Z.log2_lt_pow2; intuition. apply Z.lt_trans with zdigits. omega. unfold zdigits, wB, base; apply Zpower2_lt_lin; auto with zarith. - unfold to_Z; rewrite (Zmod_small _ _ H3). - destruct H2. + unfold to_Z; rewrite (Zmod_small _ _ Hrange). split. - apply Z.le_trans with (2^(zdigits - log_inf p - 1)*(2^log_inf p)). + apply Z.le_trans with (2^(zdigits - Z.log2 (Zpos p) - 1)*(2^Z.log2 (Zpos p))). apply Zdiv_le_upper_bound; auto with zarith. rewrite <- Zpower_exp; auto with zarith. rewrite Z.mul_comm; rewrite <- Z.pow_succ_r; auto with zarith. - replace (Z.succ (zdigits - log_inf p -1 +log_inf p)) with zdigits + replace (Z.succ (zdigits - Z.log2 (Zpos p) -1 + Z.log2 (Zpos p))) with zdigits by ring. unfold wB, base, zdigits; auto with zarith. apply Z.mul_le_mono_nonneg; auto with zarith. apply Z.lt_le_trans - with (2^(zdigits - log_inf p - 1)*(2^(Z.succ (log_inf p)))). + with (2^(zdigits - Z.log2 (Zpos p) - 1)*(2^(Z.succ (Z.log2 (Zpos p))))). apply Z.mul_lt_mono_pos_l; auto with zarith. rewrite <- Zpower_exp; auto with zarith. - replace (zdigits - log_inf p -1 +Z.succ (log_inf p)) with zdigits + replace (zdigits - Z.log2 (Zpos p) -1 +Z.succ (Z.log2 (Zpos p))) with zdigits by ring. unfold wB, base, zdigits; auto with zarith. Qed. diff --git a/theories/Reals/Rtrigo_calc.v b/theories/Reals/Rtrigo_calc.v index 5ed60b0a0f..2428fc495d 100644 --- a/theories/Reals/Rtrigo_calc.v +++ b/theories/Reals/Rtrigo_calc.v @@ -178,7 +178,7 @@ Proof. change (cos (PI / 4) <> 0); rewrite cos_PI4; apply R1_sqrt2_neq_0. Qed. -Lemma cos3PI4 : cos (3 * (PI / 4)) = -1 / sqrt 2. +Lemma cos_3PI4 : cos (3 * (PI / 4)) = -1 / sqrt 2. Proof. replace (3 * (PI / 4)) with (PI / 2 - - (PI / 4)) by field. rewrite cos_shift; rewrite sin_neg; rewrite sin_PI4. @@ -186,12 +186,16 @@ Proof. ring. Qed. -Lemma sin3PI4 : sin (3 * (PI / 4)) = 1 / sqrt 2. +#[deprecated(since="8.10",note="Use cos_3PI4 instead.")] Notation cos3PI4 := cos_3PI4. + +Lemma sin_3PI4 : sin (3 * (PI / 4)) = 1 / sqrt 2. Proof. replace (3 * (PI / 4)) with (PI / 2 - - (PI / 4)) by field. now rewrite sin_shift, cos_neg, cos_PI4. Qed. +#[deprecated(since="8.10",note="Use sin_3PI4 instead.")] Notation sin3PI4 := sin_3PI4. + Lemma cos_PI6 : cos (PI / 6) = sqrt 3 / 2. Proof with trivial. apply Rsqr_inj... diff --git a/theories/ZArith/ZArith.v b/theories/ZArith/ZArith.v index c2c97fca4f..b0744caa7b 100644 --- a/theories/ZArith/ZArith.v +++ b/theories/ZArith/ZArith.v @@ -21,6 +21,5 @@ Require Export Zpow_def. Require Export Zcomplements. Require Export Zpower. Require Export Zdiv. -Require Export Zlogarithm. Export ZArithRing. diff --git a/theories/ZArith/Zlogarithm.v b/theories/ZArith/Zlogarithm.v deleted file mode 100644 index edbd3a18fe..0000000000 --- a/theories/ZArith/Zlogarithm.v +++ /dev/null @@ -1,273 +0,0 @@ -(************************************************************************) -(* * The Coq Proof Assistant / The Coq Development Team *) -(* v * INRIA, CNRS and contributors - Copyright 1999-2019 *) -(* <O___,, * (see CREDITS file for the list of authors) *) -(* \VV/ **************************************************************) -(* // * This file is distributed under the terms of the *) -(* * GNU Lesser General Public License Version 2.1 *) -(* * (see LICENSE file for the text of the license) *) -(************************************************************************) - -(**********************************************************************) - -(** The integer logarithms with base 2. *) - -(** THIS FILE IS DEPRECATED. - Please rather use [Z.log2] (or [Z.log2_up]), which - are defined in [BinIntDef], and whose properties can - be found in [BinInt.Z]. *) - -(* There are three logarithms defined here, - depending on the rounding of the real 2-based logarithm: - - [Log_inf]: [y = (Log_inf x) iff 2^y <= x < 2^(y+1)] - i.e. [Log_inf x] is the biggest integer that is smaller than [Log x] - - [Log_sup]: [y = (Log_sup x) iff 2^(y-1) < x <= 2^y] - i.e. [Log_inf x] is the smallest integer that is bigger than [Log x] - - [Log_nearest]: [y= (Log_nearest x) iff 2^(y-1/2) < x <= 2^(y+1/2)] - i.e. [Log_nearest x] is the integer nearest from [Log x] *) - -Require Import ZArith_base Omega Zcomplements Zpower. -Local Open Scope Z_scope. - -Section Log_pos. (* Log of positive integers *) - - (** First we build [log_inf] and [log_sup] *) - - Fixpoint log_inf (p:positive) : Z := - match p with - | xH => 0 (* 1 *) - | xO q => Z.succ (log_inf q) (* 2n *) - | xI q => Z.succ (log_inf q) (* 2n+1 *) - end. - - Fixpoint log_sup (p:positive) : Z := - match p with - | xH => 0 (* 1 *) - | xO n => Z.succ (log_sup n) (* 2n *) - | xI n => Z.succ (Z.succ (log_inf n)) (* 2n+1 *) - end. - - Hint Unfold log_inf log_sup : core. - - Lemma Psize_log_inf : forall p, Zpos (Pos.size p) = Z.succ (log_inf p). - Proof. - induction p; simpl; now rewrite ?Pos2Z.inj_succ, ?IHp. - Qed. - - Lemma Zlog2_log_inf : forall p, Z.log2 (Zpos p) = log_inf p. - Proof. - unfold Z.log2. destruct p; simpl; trivial; apply Psize_log_inf. - Qed. - - Lemma Zlog2_up_log_sup : forall p, Z.log2_up (Zpos p) = log_sup p. - Proof. - induction p; simpl log_sup. - - change (Zpos p~1) with (2*(Zpos p)+1). - rewrite Z.log2_up_succ_double, Zlog2_log_inf; try easy. - unfold Z.succ. now rewrite !(Z.add_comm _ 1), Z.add_assoc. - - change (Zpos p~0) with (2*Zpos p). - now rewrite Z.log2_up_double, IHp. - - reflexivity. - Qed. - - (** Then we give the specifications of [log_inf] and [log_sup] - and prove their validity *) - - Hint Resolve Z.le_trans: zarith. - - Theorem log_inf_correct : - forall x:positive, - 0 <= log_inf x /\ two_p (log_inf x) <= Zpos x < two_p (Z.succ (log_inf x)). - Proof. - simple induction x; intros; simpl; - [ elim H; intros Hp HR; clear H; split; - [ auto with zarith - | rewrite two_p_S with (x := Z.succ (log_inf p)) by (apply Z.le_le_succ_r; trivial); - rewrite two_p_S by trivial; - rewrite two_p_S in HR by trivial; rewrite (BinInt.Pos2Z.inj_xI p); - omega ] - | elim H; intros Hp HR; clear H; split; - [ auto with zarith - | rewrite two_p_S with (x := Z.succ (log_inf p)) by (apply Z.le_le_succ_r; trivial); - rewrite two_p_S by trivial; - rewrite two_p_S in HR by trivial; rewrite (BinInt.Pos2Z.inj_xO p); - omega ] - | unfold two_power_pos; unfold shift_pos; simpl; - omega ]. - Qed. - - Definition log_inf_correct1 (p:positive) := proj1 (log_inf_correct p). - Definition log_inf_correct2 (p:positive) := proj2 (log_inf_correct p). - - Opaque log_inf_correct1 log_inf_correct2. - - Hint Resolve log_inf_correct1 log_inf_correct2: zarith. - - Lemma log_sup_correct1 : forall p:positive, 0 <= log_sup p. - Proof. - simple induction p; intros; simpl; auto with zarith. - Qed. - - (** For every [p], either [p] is a power of two and [(log_inf p)=(log_sup p)] - either [(log_sup p)=(log_inf p)+1] *) - - Theorem log_sup_log_inf : - forall p:positive, - IF Zpos p = two_p (log_inf p) then Zpos p = two_p (log_sup p) - else log_sup p = Z.succ (log_inf p). - Proof. - simple induction p; intros; - [ elim H; right; simpl; - rewrite (two_p_S (log_inf p0) (log_inf_correct1 p0)); - rewrite BinInt.Pos2Z.inj_xI; unfold Z.succ; omega - | elim H; clear H; intro Hif; - [ left; simpl; - rewrite (two_p_S (log_inf p0) (log_inf_correct1 p0)); - rewrite (two_p_S (log_sup p0) (log_sup_correct1 p0)); - rewrite <- (proj1 Hif); rewrite <- (proj2 Hif); - auto - | right; simpl; - rewrite (two_p_S (log_inf p0) (log_inf_correct1 p0)); - rewrite BinInt.Pos2Z.inj_xO; unfold Z.succ; - omega ] - | left; auto ]. - Qed. - - Theorem log_sup_correct2 : - forall x:positive, two_p (Z.pred (log_sup x)) < Zpos x <= two_p (log_sup x). - Proof. - intro. - elim (log_sup_log_inf x). - (* x is a power of two and [log_sup = log_inf] *) - intros [E1 E2]; rewrite E2. - split; [ apply two_p_pred; apply log_sup_correct1 | apply Z.le_refl ]. - intros [E1 E2]; rewrite E2. - rewrite (Z.pred_succ (log_inf x)). - generalize (log_inf_correct2 x); omega. - Qed. - - Lemma log_inf_le_log_sup : forall p:positive, log_inf p <= log_sup p. - Proof. - simple induction p; simpl; intros; omega. - Qed. - - Lemma log_sup_le_Slog_inf : forall p:positive, log_sup p <= Z.succ (log_inf p). - Proof. - simple induction p; simpl; intros; omega. - Qed. - - (** Now it's possible to specify and build the [Log] rounded to the nearest *) - - Fixpoint log_near (x:positive) : Z := - match x with - | xH => 0 - | xO xH => 1 - | xI xH => 2 - | xO y => Z.succ (log_near y) - | xI y => Z.succ (log_near y) - end. - - Theorem log_near_correct1 : forall p:positive, 0 <= log_near p. - Proof. - simple induction p; simpl; intros; - [ elim p0; auto with zarith - | elim p0; auto with zarith - | trivial with zarith ]. - intros; apply Z.le_le_succ_r. - generalize H0; now elim p1. - intros; apply Z.le_le_succ_r. - generalize H0; now elim p1. - Qed. - - Theorem log_near_correct2 : - forall p:positive, log_near p = log_inf p \/ log_near p = log_sup p. - Proof. - simple induction p. - intros p0 [Einf| Esup]. - simpl. rewrite Einf. - case p0; [ left | left | right ]; reflexivity. - simpl; rewrite Esup. - elim (log_sup_log_inf p0). - generalize (log_inf_le_log_sup p0). - generalize (log_sup_le_Slog_inf p0). - case p0; auto with zarith. - intros; omega. - case p0; intros; auto with zarith. - intros p0 [Einf| Esup]. - simpl. - repeat rewrite Einf. - case p0; intros; auto with zarith. - simpl. - repeat rewrite Esup. - case p0; intros; auto with zarith. - auto. - Qed. - -End Log_pos. - -Section divers. - - (** Number of significative digits. *) - - Definition N_digits (x:Z) := - match x with - | Zpos p => log_inf p - | Zneg p => log_inf p - | Z0 => 0 - end. - - Lemma ZERO_le_N_digits : forall x:Z, 0 <= N_digits x. - Proof. - simple induction x; simpl; - [ apply Z.le_refl | exact log_inf_correct1 | exact log_inf_correct1 ]. - Qed. - - Lemma log_inf_shift_nat : forall n:nat, log_inf (shift_nat n 1) = Z.of_nat n. - Proof. - simple induction n; intros; - [ try trivial | rewrite Nat2Z.inj_succ; rewrite <- H; reflexivity ]. - Qed. - - Lemma log_sup_shift_nat : forall n:nat, log_sup (shift_nat n 1) = Z.of_nat n. - Proof. - simple induction n; intros; - [ try trivial | rewrite Nat2Z.inj_succ; rewrite <- H; reflexivity ]. - Qed. - - (** [Is_power p] means that p is a power of two *) - Fixpoint Is_power (p:positive) : Prop := - match p with - | xH => True - | xO q => Is_power q - | xI q => False - end. - - Lemma Is_power_correct : - forall p:positive, Is_power p <-> (exists y : nat, p = shift_nat y 1). - Proof. - split; - [ elim p; - [ simpl; tauto - | simpl; intros; generalize (H H0); intro H1; elim H1; - intros y0 Hy0; exists (S y0); rewrite Hy0; reflexivity - | intro; exists 0%nat; reflexivity ] - | intros; elim H; intros; rewrite H0; elim x; intros; simpl; trivial ]. - Qed. - - Lemma Is_power_or : forall p:positive, Is_power p \/ ~ Is_power p. - Proof. - simple induction p; - [ intros; right; simpl; tauto - | intros; elim H; - [ intros; left; simpl; exact H0 - | intros; right; simpl; exact H0 ] - | left; simpl; trivial ]. - Qed. - -End divers. - - - - - - diff --git a/theories/ZArith/Zsqrt_compat.v b/theories/ZArith/Zsqrt_compat.v deleted file mode 100644 index 6873c737a7..0000000000 --- a/theories/ZArith/Zsqrt_compat.v +++ /dev/null @@ -1,234 +0,0 @@ -(************************************************************************) -(* * The Coq Proof Assistant / The Coq Development Team *) -(* v * INRIA, CNRS and contributors - Copyright 1999-2019 *) -(* <O___,, * (see CREDITS file for the list of authors) *) -(* \VV/ **************************************************************) -(* // * This file is distributed under the terms of the *) -(* * GNU Lesser General Public License Version 2.1 *) -(* * (see LICENSE file for the text of the license) *) -(************************************************************************) - -Require Import ZArithRing. -Require Import Omega. -Require Export ZArith_base. -Local Open Scope Z_scope. - -(** THIS FILE IS DEPRECATED - - Instead of the various [Zsqrt] defined here, please use rather - [Z.sqrt] (or [Z.sqrtrem]). The latter are pure functions without - proof parts, and more results are available about them. - Some equivalence proofs between the old and the new versions - can be found below. Importing ZArith will provides by default - the new versions. - -*) - -(**********************************************************************) -(** Definition and properties of square root on Z *) - -(** The following tactic replaces all instances of (POS (xI ...)) by - `2*(POS ...)+1`, but only when ... is not made only with xO, XI, or xH. *) -Ltac compute_POS := - match goal with - | |- context [(Zpos (xI ?X1))] => - match constr:(X1) with - | context [1%positive] => fail 1 - | _ => rewrite (Pos2Z.inj_xI X1) - end - | |- context [(Zpos (xO ?X1))] => - match constr:(X1) with - | context [1%positive] => fail 1 - | _ => rewrite (Pos2Z.inj_xO X1) - end - end. - -Inductive sqrt_data (n:Z) : Set := - c_sqrt : forall s r:Z, n = s * s + r -> 0 <= r <= 2 * s -> sqrt_data n. - -Definition sqrtrempos : forall p:positive, sqrt_data (Zpos p). - refine - (fix sqrtrempos (p:positive) : sqrt_data (Zpos p) := - match p return sqrt_data (Zpos p) with - | xH => c_sqrt 1 1 0 _ _ - | xO xH => c_sqrt 2 1 1 _ _ - | xI xH => c_sqrt 3 1 2 _ _ - | xO (xO p') => - match sqrtrempos p' with - | c_sqrt _ s' r' Heq Hint => - match Z_le_gt_dec (4 * s' + 1) (4 * r') with - | left Hle => - c_sqrt (Zpos (xO (xO p'))) (2 * s' + 1) - (4 * r' - (4 * s' + 1)) _ _ - | right Hgt => c_sqrt (Zpos (xO (xO p'))) (2 * s') (4 * r') _ _ - end - end - | xO (xI p') => - match sqrtrempos p' with - | c_sqrt _ s' r' Heq Hint => - match Z_le_gt_dec (4 * s' + 1) (4 * r' + 2) with - | left Hle => - c_sqrt (Zpos (xO (xI p'))) (2 * s' + 1) - (4 * r' + 2 - (4 * s' + 1)) _ _ - | right Hgt => - c_sqrt (Zpos (xO (xI p'))) (2 * s') (4 * r' + 2) _ _ - end - end - | xI (xO p') => - match sqrtrempos p' with - | c_sqrt _ s' r' Heq Hint => - match Z_le_gt_dec (4 * s' + 1) (4 * r' + 1) with - | left Hle => - c_sqrt (Zpos (xI (xO p'))) (2 * s' + 1) - (4 * r' + 1 - (4 * s' + 1)) _ _ - | right Hgt => - c_sqrt (Zpos (xI (xO p'))) (2 * s') (4 * r' + 1) _ _ - end - end - | xI (xI p') => - match sqrtrempos p' with - | c_sqrt _ s' r' Heq Hint => - match Z_le_gt_dec (4 * s' + 1) (4 * r' + 3) with - | left Hle => - c_sqrt (Zpos (xI (xI p'))) (2 * s' + 1) - (4 * r' + 3 - (4 * s' + 1)) _ _ - | right Hgt => - c_sqrt (Zpos (xI (xI p'))) (2 * s') (4 * r' + 3) _ _ - end - end - end); clear sqrtrempos; repeat compute_POS; - try (try rewrite Heq; ring); try omega. -Defined. - -(** Define with integer input, but with a strong (readable) specification. *) -Definition Zsqrt : - forall x:Z, - 0 <= x -> - {s : Z & {r : Z | x = s * s + r /\ s * s <= x < (s + 1) * (s + 1)}}. - refine - (fun x => - match - x - return - 0 <= x -> - {s : Z & {r : Z | x = s * s + r /\ s * s <= x < (s + 1) * (s + 1)}} - with - | Zpos p => - fun h => - match sqrtrempos p with - | c_sqrt _ s r Heq Hint => - existT - (fun s:Z => - {r : Z | - Zpos p = s * s + r /\ s * s <= Zpos p < (s + 1) * (s + 1)}) - s - (exist - (fun r:Z => - Zpos p = s * s + r /\ - s * s <= Zpos p < (s + 1) * (s + 1)) r _) - end - | Zneg p => - fun h => - False_rec - {s : Z & - {r : Z | - Zneg p = s * s + r /\ s * s <= Zneg p < (s + 1) * (s + 1)}} - (h (eq_refl Datatypes.Gt)) - | Z0 => - fun h => - existT - (fun s:Z => - {r : Z | 0 = s * s + r /\ s * s <= 0 < (s + 1) * (s + 1)}) 0 - (exist - (fun r:Z => 0 = 0 * 0 + r /\ 0 * 0 <= 0 < (0 + 1) * (0 + 1)) 0 - _) - end); try omega. - split; [ omega | rewrite Heq; ring_simplify (s*s) ((s + 1) * (s + 1)); omega ]. -Defined. - -(** Define a function of type Z->Z that computes the integer square root, - but only for positive numbers, and 0 for others. *) -Definition Zsqrt_plain (x:Z) : Z := - match x with - | Zpos p => - match Zsqrt (Zpos p) (Pos2Z.is_nonneg p) with - | existT _ s _ => s - end - | Zneg p => 0 - | Z0 => 0 - end. - -(** A basic theorem about Zsqrt_plain *) - -Theorem Zsqrt_interval : - forall n:Z, - 0 <= n -> - Zsqrt_plain n * Zsqrt_plain n <= n < - (Zsqrt_plain n + 1) * (Zsqrt_plain n + 1). -Proof. - intros [|p|p] Hp. - - now compute. - - unfold Zsqrt_plain. - now destruct Zsqrt as (s & r & Heq & Hint). - - now elim Hp. -Qed. - -(** Positivity *) - -Theorem Zsqrt_plain_is_pos: forall n, 0 <= n -> 0 <= Zsqrt_plain n. -Proof. - intros n m; case (Zsqrt_interval n); auto with zarith. - intros H1 H2; case (Z.le_gt_cases 0 (Zsqrt_plain n)); auto. - intros H3; contradict H2; auto; apply Z.le_ngt. - apply Z.le_trans with ( 2 := H1 ). - replace ((Zsqrt_plain n + 1) * (Zsqrt_plain n + 1)) - with (Zsqrt_plain n * Zsqrt_plain n + (2 * Zsqrt_plain n + 1)); - auto with zarith. - ring. -Qed. - -(** Direct correctness on squares. *) - -Theorem Zsqrt_square_id: forall a, 0 <= a -> Zsqrt_plain (a * a) = a. -Proof. - intros a H. - generalize (Zsqrt_plain_is_pos (a * a)); auto with zarith; intros Haa. - case (Zsqrt_interval (a * a)); auto with zarith. - intros H1 H2. - case (Z.le_gt_cases a (Zsqrt_plain (a * a))); intros H3. - - Z.le_elim H3; auto. - contradict H1; auto; apply Z.lt_nge; auto with zarith. - apply Z.le_lt_trans with (a * Zsqrt_plain (a * a)); auto with zarith. - apply Z.mul_lt_mono_pos_r; auto with zarith. - - contradict H2; auto; apply Z.le_ngt; auto with zarith. - apply Z.mul_le_mono_nonneg; auto with zarith. -Qed. - -(** [Zsqrt_plain] is increasing *) - -Theorem Zsqrt_le: - forall p q, 0 <= p <= q -> Zsqrt_plain p <= Zsqrt_plain q. -Proof. - intros p q [H1 H2]. - Z.le_elim H2; [ | subst q; auto with zarith]. - case (Z.le_gt_cases (Zsqrt_plain p) (Zsqrt_plain q)); auto; intros H3. - assert (Hp: (0 <= Zsqrt_plain q)). - { apply Zsqrt_plain_is_pos; auto with zarith. } - absurd (q <= p); auto with zarith. - apply Z.le_trans with ((Zsqrt_plain q + 1) * (Zsqrt_plain q + 1)). - case (Zsqrt_interval q); auto with zarith. - apply Z.le_trans with (Zsqrt_plain p * Zsqrt_plain p); auto with zarith. - apply Z.mul_le_mono_nonneg; auto with zarith. - case (Zsqrt_interval p); auto with zarith. -Qed. - - -(** Equivalence between Zsqrt_plain and [Z.sqrt] *) - -Lemma Zsqrt_equiv : forall n, Zsqrt_plain n = Z.sqrt n. -Proof. - intros. destruct (Z_le_gt_dec 0 n). - symmetry. apply Z.sqrt_unique; trivial. - now apply Zsqrt_interval. - now destruct n. -Qed. diff --git a/toplevel/coqloop.ml b/toplevel/coqloop.ml index e49b1c0c07..2673995a86 100644 --- a/toplevel/coqloop.ml +++ b/toplevel/coqloop.ml @@ -383,7 +383,7 @@ let rec vernac_loop ~state = try let input = top_buffer.tokens in match read_sentence ~state input with - | Some (VernacBacktrack(bid,_,_)) -> + | Some (VernacBackTo bid) -> let bid = Stateid.of_int bid in let doc, res = Stm.edit_at ~doc:state.doc bid in assert (res = `NewTip); diff --git a/toplevel/g_toplevel.mlg b/toplevel/g_toplevel.mlg index fed337ab03..1a1537113e 100644 --- a/toplevel/g_toplevel.mlg +++ b/toplevel/g_toplevel.mlg @@ -17,7 +17,7 @@ open Vernacexpr (* Vernaculars specific to the toplevel *) type vernac_toplevel = - | VernacBacktrack of int * int * int + | VernacBackTo of int | VernacDrop | VernacQuit | VernacControl of vernac_control @@ -54,8 +54,8 @@ GRAMMAR EXTEND Gram vernac_toplevel: FIRST [ [ IDENT "Drop"; "." -> { Some VernacDrop } | IDENT "Quit"; "." -> { Some VernacQuit } - | IDENT "Backtrack"; n = natural ; m = natural ; p = natural; "." -> - { Some (VernacBacktrack (n,m,p)) } + | IDENT "BackTo"; n = natural; "." -> + { Some (VernacBackTo n) } (* show a goal for the specified proof state *) | test_show_goal; IDENT "Show"; IDENT "Goal"; gid = natural; IDENT "at"; sid = natural; "." -> { Some (VernacShowGoal {gid; sid}) } diff --git a/vernac/comFixpoint.ml b/vernac/comFixpoint.ml index 3f13d772ab..74c9bc2886 100644 --- a/vernac/comFixpoint.ml +++ b/vernac/comFixpoint.ml @@ -107,26 +107,20 @@ let check_mutuality env evd isfix fixl = warn_non_full_mutual (x,xge,y,yge,isfix,rest) | _ -> () -type structured_fixpoint_expr = { - fix_name : Id.t; - fix_univs : universe_decl_expr option; - fix_annot : lident option; - fix_binders : local_binder_expr list; - fix_body : constr_expr option; - fix_type : constr_expr -} - let interp_fix_context ~program_mode ~cofix env sigma fix = - let before, after = if not cofix then split_at_annot fix.fix_binders fix.fix_annot else [], fix.fix_binders in + let before, after = + if not cofix + then split_at_annot fix.Vernacexpr.binders fix.Vernacexpr.rec_order + else [], fix.Vernacexpr.binders in let sigma, (impl_env, ((env', ctx), imps)) = interp_context_evars ~program_mode env sigma before in let sigma, (impl_env', ((env'', ctx'), imps')) = interp_context_evars ~program_mode ~impl_env ~shift:(Context.Rel.nhyps ctx) env' sigma after in - let annot = Option.map (fun _ -> List.length (assums_of_rel_context ctx)) fix.fix_annot in + let annot = Option.map (fun _ -> List.length (assums_of_rel_context ctx)) fix.Vernacexpr.rec_order in sigma, ((env'', ctx' @ ctx), (impl_env',imps @ imps'), annot) let interp_fix_ccl ~program_mode sigma impls (env,_) fix = - let sigma, (c, impl) = interp_type_evars_impls ~program_mode ~impls env sigma fix.fix_type in + let sigma, (c, impl) = interp_type_evars_impls ~program_mode ~impls env sigma fix.Vernacexpr.rtype in let r = Retyping.relevance_of_type env sigma c in sigma, (c, r, impl) @@ -135,7 +129,7 @@ let interp_fix_body ~program_mode env_rec sigma impls (_,ctx) fix ccl = Option.cata (fun body -> let env = push_rel_context ctx env_rec in let sigma, body = interp_casted_constr_evars ~program_mode env sigma ~impls body ccl in - sigma, Some (it_mkLambda_or_LetIn body ctx)) (sigma, None) fix.fix_body + sigma, Some (it_mkLambda_or_LetIn body ctx)) (sigma, None) fix.Vernacexpr.body_def let build_fix_type (_,ctx) ccl = EConstr.it_mkProd_or_LetIn ccl ctx @@ -167,16 +161,16 @@ type recursive_preentry = let fix_proto sigma = Evarutil.new_global sigma (Coqlib.lib_ref "program.tactic.fix_proto") -let interp_recursive ~program_mode ~cofix fixl notations = +let interp_recursive ~program_mode ~cofix (fixl : 'a Vernacexpr.fix_expr_gen list) = let open Context.Named.Declaration in let open EConstr in let env = Global.env() in - let fixnames = List.map (fun fix -> fix.fix_name) fixl in + let fixnames = List.map (fun fix -> fix.Vernacexpr.fname.CAst.v) fixl in (* Interp arities allowing for unresolved types *) let all_universes = List.fold_right (fun sfe acc -> - match sfe.fix_univs , acc with + match sfe.Vernacexpr.univs , acc with | None , acc -> acc | x , None -> x | Some ls , Some us -> @@ -222,6 +216,7 @@ let interp_recursive ~program_mode ~cofix fixl notations = (* Interp bodies with rollback because temp use of notations/implicit *) let sigma, fixdefs = Metasyntax.with_syntax_protection (fun () -> + let notations = List.map_append (fun { Vernacexpr.notations } -> notations) fixl in List.iter (Metasyntax.set_notation_for_interpretation env_rec impls) notations; List.fold_left4_map (fun sigma fixctximpenv -> interp_fix_body ~program_mode env_rec sigma (Id.Map.fold Id.Map.add fixctximpenv impls)) @@ -248,8 +243,8 @@ let ground_fixpoint env evd (fixnames,fixrs,fixdefs,fixtypes) = let fixtypes = List.map EConstr.(to_constr evd) fixtypes in Evd.evar_universe_context evd, (fixnames,fixrs,fixdefs,fixtypes) -let interp_fixpoint ~cofix l ntns = - let (env,_,pl,evd),fix,info = interp_recursive ~program_mode:false ~cofix l ntns in +let interp_fixpoint ~cofix l = + let (env,_,pl,evd),fix,info = interp_recursive ~program_mode:false ~cofix l in check_recursive true env evd fix; let uctx,fix = ground_fixpoint env evd fix in (fix,pl,uctx,info) @@ -316,38 +311,29 @@ let extract_decreasing_argument ~structonly = function { CAst.v = v } -> match v | _ -> user_err Pp.(str "Well-founded induction requires Program Fixpoint or Function.") -let extract_fixpoint_components ~structonly l = - let fixl, ntnl = List.split l in - let fixl = List.map (fun (({CAst.v=id},pl),ann,bl,typ,def) -> - (* This is a special case: if there's only one binder, we pick it as the - recursive argument if none is provided. *) - let ann = Option.map (fun ann -> match bl, ann with - | [CLocalAssum([{ CAst.v = Name x }],_,_)], { CAst.v = CMeasureRec(None, mes, rel); CAst.loc } -> - CAst.make ?loc @@ CMeasureRec(Some (CAst.make x), mes, rel) - | [CLocalDef({ CAst.v = Name x },_,_)], { CAst.v = CMeasureRec(None, mes, rel); CAst.loc } -> - CAst.make ?loc @@ CMeasureRec(Some (CAst.make x), mes, rel) - | _, x -> x) ann - in - let ann = Option.map (extract_decreasing_argument ~structonly) ann in - {fix_name = id; fix_annot = ann; fix_univs = pl; - fix_binders = bl; fix_body = def; fix_type = typ}) fixl in - fixl, List.flatten ntnl - -let extract_cofixpoint_components l = - let fixl, ntnl = List.split l in - List.map (fun (({CAst.v=id},pl),bl,typ,def) -> - {fix_name = id; fix_annot = None; fix_univs = pl; - fix_binders = bl; fix_body = def; fix_type = typ}) fixl, - List.flatten ntnl +(* This is a special case: if there's only one binder, we pick it as + the recursive argument if none is provided. *) +let adjust_rec_order ~structonly binders rec_order = + let rec_order = Option.map (fun rec_order -> match binders, rec_order with + | [CLocalAssum([{ CAst.v = Name x }],_,_)], { CAst.v = CMeasureRec(None, mes, rel); CAst.loc } -> + CAst.make ?loc @@ CMeasureRec(Some (CAst.make x), mes, rel) + | [CLocalDef({ CAst.v = Name x },_,_)], { CAst.v = CMeasureRec(None, mes, rel); CAst.loc } -> + CAst.make ?loc @@ CMeasureRec(Some (CAst.make x), mes, rel) + | _, x -> x) rec_order + in + Option.map (extract_decreasing_argument ~structonly) rec_order let check_safe () = let open Declarations in let flags = Environ.typing_flags (Global.env ()) in flags.check_universes && flags.check_guarded -let do_fixpoint_common l = - let fixl, ntns = extract_fixpoint_components ~structonly:true l in - let (_, _, _, info as fix) = interp_fixpoint ~cofix:false fixl ntns in +let do_fixpoint_common (fixl : Vernacexpr.fixpoint_expr list) = + let fixl = List.map (fun fix -> + Vernacexpr.{ fix + with rec_order = adjust_rec_order ~structonly:true fix.binders fix.rec_order }) fixl in + let ntns = List.map_append (fun { Vernacexpr.notations } -> notations ) fixl in + let (_, _, _, info as fix) = interp_fixpoint ~cofix:false fixl in fixl, ntns, fix, List.map compute_possible_guardness_evidences info let do_fixpoint_interactive ~scope ~poly l : Lemmas.t = @@ -361,17 +347,18 @@ let do_fixpoint ~scope ~poly l = declare_fixpoint_generic ~indexes:possible_indexes ~scope ~poly fix ntns; if not (check_safe ()) then Feedback.feedback Feedback.AddedAxiom else () -let do_cofixpoint_common l = - let fixl,ntns = extract_cofixpoint_components l in - ntns, interp_fixpoint ~cofix:true fixl ntns +let do_cofixpoint_common (fixl : Vernacexpr.cofixpoint_expr list) = + let fixl = List.map (fun fix -> {fix with Vernacexpr.rec_order = None}) fixl in + let ntns = List.map_append (fun { Vernacexpr.notations } -> notations ) fixl in + interp_fixpoint ~cofix:true fixl, ntns let do_cofixpoint_interactive ~scope ~poly l = - let ntns, cofix = do_cofixpoint_common l in + let cofix, ntns = do_cofixpoint_common l in let lemma = declare_fixpoint_interactive_generic ~scope ~poly cofix ntns in if not (check_safe ()) then Feedback.feedback Feedback.AddedAxiom else (); lemma let do_cofixpoint ~scope ~poly l = - let ntns, cofix = do_cofixpoint_common l in + let cofix, ntns = do_cofixpoint_common l in declare_fixpoint_generic ~scope ~poly cofix ntns; if not (check_safe ()) then Feedback.feedback Feedback.AddedAxiom else () diff --git a/vernac/comFixpoint.mli b/vernac/comFixpoint.mli index 982d316605..4f8e9018de 100644 --- a/vernac/comFixpoint.mli +++ b/vernac/comFixpoint.mli @@ -10,7 +10,6 @@ open Names open Constr -open Constrexpr open Vernacexpr (** {6 Fixpoints and cofixpoints} *) @@ -18,39 +17,35 @@ open Vernacexpr (** Entry points for the vernacular commands Fixpoint and CoFixpoint *) val do_fixpoint_interactive : - scope:DeclareDef.locality -> poly:bool -> (fixpoint_expr * decl_notation list) list -> Lemmas.t + scope:DeclareDef.locality -> poly:bool -> fixpoint_expr list -> Lemmas.t val do_fixpoint : - scope:DeclareDef.locality -> poly:bool -> (fixpoint_expr * decl_notation list) list -> unit + scope:DeclareDef.locality -> poly:bool -> fixpoint_expr list -> unit val do_cofixpoint_interactive : - scope:DeclareDef.locality -> poly:bool -> (cofixpoint_expr * decl_notation list) list -> Lemmas.t + scope:DeclareDef.locality -> poly:bool -> cofixpoint_expr list -> Lemmas.t val do_cofixpoint : - scope:DeclareDef.locality -> poly:bool -> (cofixpoint_expr * decl_notation list) list -> unit + scope:DeclareDef.locality -> poly:bool -> cofixpoint_expr list -> unit (************************************************************************) (** Internal API *) (************************************************************************) -type structured_fixpoint_expr = { - fix_name : Id.t; - fix_univs : Constrexpr.universe_decl_expr option; - fix_annot : lident option; - fix_binders : local_binder_expr list; - fix_body : constr_expr option; - fix_type : constr_expr -} - (** Typing global fixpoints and cofixpoint_expr *) +val adjust_rec_order + : structonly:bool + -> Constrexpr.local_binder_expr list + -> Constrexpr.recursion_order_expr option + -> lident option + (** Exported for Program *) val interp_recursive : (* Misc arguments *) program_mode:bool -> cofix:bool -> (* Notations of the fixpoint / should that be folded in the previous argument? *) - structured_fixpoint_expr list -> decl_notation list -> - + lident option fix_expr_gen list -> (* env / signature / univs / evar_map *) (Environ.env * EConstr.named_context * UState.universe_decl * Evd.evar_map) * (* names / defs / types *) @@ -60,25 +55,13 @@ val interp_recursive : (** Exported for Funind *) -(** Extracting the semantical components out of the raw syntax of - (co)fixpoints declarations *) - -val extract_fixpoint_components : structonly:bool -> - (fixpoint_expr * decl_notation list) list -> - structured_fixpoint_expr list * decl_notation list +type recursive_preentry = Id.t list * Sorts.relevance list * constr option list * types list -val extract_cofixpoint_components : - (cofixpoint_expr * decl_notation list) list -> - structured_fixpoint_expr list * decl_notation list - -type recursive_preentry = - Id.t list * Sorts.relevance list * constr option list * types list - -val interp_fixpoint : - cofix:bool -> - structured_fixpoint_expr list -> decl_notation list -> - recursive_preentry * UState.universe_decl * UState.t * - (EConstr.rel_context * Impargs.manual_implicits * int option) list +val interp_fixpoint + : cofix:bool + -> lident option fix_expr_gen list + -> recursive_preentry * UState.universe_decl * UState.t * + (EConstr.rel_context * Impargs.manual_implicits * int option) list (** Very private function, do not use *) val compute_possible_guardness_evidences : diff --git a/vernac/comInductive.ml b/vernac/comInductive.ml index 65db4401d9..664010c917 100644 --- a/vernac/comInductive.ml +++ b/vernac/comInductive.ml @@ -80,9 +80,6 @@ type structured_one_inductive_expr = { ind_lc : (Id.t * constr_expr) list } -type structured_inductive_expr = - local_binder_expr list * structured_one_inductive_expr list - let minductive_message = function | [] -> user_err Pp.(str "No inductive definition.") | [x] -> (Id.print x ++ str " is defined") @@ -468,9 +465,6 @@ let interp_mutual_inductive_gen env0 ~template udecl (uparamsl,paramsl,indl) not InferCumulativity.infer_inductive env_ar mind_ent else mind_ent), Evd.universe_binders sigma, impls -let interp_mutual_inductive ~template udecl (paramsl,indl) notations ~cumulative ~poly ~private_ind finite = - interp_mutual_inductive_gen (Global.env()) ~template udecl ([],paramsl,indl) notations ~cumulative ~poly ~private_ind finite - (* Very syntactical equality *) let eq_local_binders bl1 bl2 = List.equal local_binder_eq bl1 bl2 diff --git a/vernac/comInductive.mli b/vernac/comInductive.mli index 97f930c0a1..285be8cd51 100644 --- a/vernac/comInductive.mli +++ b/vernac/comInductive.mli @@ -10,7 +10,6 @@ open Names open Entries -open Libnames open Vernacexpr open Constrexpr @@ -33,12 +32,20 @@ val do_mutual_inductive -> Declarations.recursivity_kind -> unit +(** User-interface API *) + +(** Prepare a "match" template for a given inductive type. + For each branch of the match, we list the constructor name + followed by enough pattern variables. + [Not_found] is raised if the given string isn't the qualid of + a known inductive type. *) + +val make_cases : Names.inductive -> string list list + (************************************************************************) -(** Internal API *) +(** Internal API, exported for Record *) (************************************************************************) -(** Exported for Record and Funind *) - (** Registering a mutual inductive definition together with its associated schemes *) @@ -55,41 +62,3 @@ val should_auto_template : Id.t -> bool -> bool (** [should_auto_template x b] is [true] when [b] is [true] and we automatically use template polymorphism. [x] is the name of the inductive under consideration. *) - -(** Exported for Funind *) - -(** Extracting the semantical components out of the raw syntax of mutual - inductive declarations *) - -type structured_one_inductive_expr = { - ind_name : Id.t; - ind_arity : constr_expr; - ind_lc : (Id.t * constr_expr) list -} - -type structured_inductive_expr = - local_binder_expr list * structured_one_inductive_expr list - -val extract_mutual_inductive_declaration_components : - (one_inductive_expr * decl_notation list) list -> - structured_inductive_expr * (*coercions:*) qualid list * decl_notation list - -(** Typing mutual inductive definitions *) -val interp_mutual_inductive - : template:bool option - -> universe_decl_expr option - -> structured_inductive_expr - -> decl_notation list - -> cumulative:bool - -> poly:bool - -> private_ind:bool - -> Declarations.recursivity_kind - -> mutual_inductive_entry * UnivNames.universe_binders * one_inductive_impls list - -(** Prepare a "match" template for a given inductive type. - For each branch of the match, we list the constructor name - followed by enough pattern variables. - [Not_found] is raised if the given string isn't the qualid of - a known inductive type. *) - -val make_cases : Names.inductive -> string list list diff --git a/vernac/comProgramFixpoint.ml b/vernac/comProgramFixpoint.ml index 0fd65ad9b4..c6e68effd7 100644 --- a/vernac/comProgramFixpoint.ml +++ b/vernac/comProgramFixpoint.ml @@ -244,10 +244,10 @@ let collect_evars_of_term evd c ty = Evar.Set.fold (fun ev acc -> Evd.add acc ev (Evd.find_undefined evd ev)) evars (Evd.from_ctx (Evd.evar_universe_context evd)) -let do_program_recursive ~scope ~poly fixkind fixl ntns = +let do_program_recursive ~scope ~poly fixkind fixl = let cofix = fixkind = DeclareObl.IsCoFixpoint in let (env, rec_sign, pl, evd), fix, info = - interp_recursive ~cofix ~program_mode:true fixl ntns + interp_recursive ~cofix ~program_mode:true fixl in (* Program-specific code *) (* Get the interesting evars, those that were not instantiated *) @@ -289,16 +289,19 @@ let do_program_recursive ~scope ~poly fixkind fixl ntns = | DeclareObl.IsFixpoint _ -> Decls.Fixpoint | DeclareObl.IsCoFixpoint -> Decls.CoFixpoint in + let ntns = List.map_append (fun { Vernacexpr.notations } -> notations ) fixl in Obligations.add_mutual_definitions defs ~poly ~scope ~kind ~univdecl:pl ctx ntns fixkind let do_program_fixpoint ~scope ~poly l = - let g = List.map (fun ((_,wf,_,_,_),_) -> wf) l in + let g = List.map (fun { Vernacexpr.rec_order } -> rec_order) l in match g, l with - | [Some { CAst.v = CWfRec (n,r) }], [((({CAst.v=id},pl),_,bl,typ,def),ntn)] -> + | [Some { CAst.v = CWfRec (n,r) }], + [ Vernacexpr.{fname={CAst.v=id}; univs; binders; rtype; body_def; notations} ] -> let recarg = mkIdentC n.CAst.v in - build_wellfounded (id, pl, bl, typ, out_def def) poly r recarg ntn + build_wellfounded (id, univs, binders, rtype, out_def body_def) poly r recarg notations - | [Some { CAst.v = CMeasureRec (n, m, r) }], [((({CAst.v=id},pl),_,bl,typ,def),ntn)] -> + | [Some { CAst.v = CMeasureRec (n, m, r) }], + [Vernacexpr.{fname={CAst.v=id}; univs; binders; rtype; body_def; notations }] -> (* We resolve here a clash between the syntax of Program Fixpoint and the one of funind *) let r = match n, r with | Some id, None -> @@ -308,25 +311,20 @@ let do_program_fixpoint ~scope ~poly l = user_err Pp.(str"Measure takes only two arguments in Program Fixpoint.") | _, _ -> r in - build_wellfounded (id, pl, bl, typ, out_def def) poly - (Option.default (CAst.make @@ CRef (lt_ref,None)) r) m ntn + build_wellfounded (id, univs, binders, rtype, out_def body_def) poly + (Option.default (CAst.make @@ CRef (lt_ref,None)) r) m notations | _, _ when List.for_all (fun ro -> match ro with None | Some { CAst.v = CStructRec _} -> true | _ -> false) g -> - let fixl,ntns = extract_fixpoint_components ~structonly:true l in - let fixkind = DeclareObl.IsFixpoint (List.map (fun d -> d.fix_annot) fixl) in - do_program_recursive ~scope ~poly fixkind fixl ntns + let annots = List.map (fun fix -> + Vernacexpr.(ComFixpoint.adjust_rec_order ~structonly:true fix.binders fix.rec_order)) l in + let fixkind = DeclareObl.IsFixpoint annots in + let l = List.map2 (fun fix rec_order -> { fix with Vernacexpr.rec_order }) l annots in + do_program_recursive ~scope ~poly fixkind l | _, _ -> user_err ~hdr:"do_program_fixpoint" (str "Well-founded fixpoints not allowed in mutually recursive blocks") -let extract_cofixpoint_components l = - let fixl, ntnl = List.split l in - List.map (fun (({CAst.v=id},pl),bl,typ,def) -> - {fix_name = id; fix_annot = None; fix_univs = pl; - fix_binders = bl; fix_body = def; fix_type = typ}) fixl, - List.flatten ntnl - let check_safe () = let open Declarations in let flags = Environ.typing_flags (Global.env ()) in @@ -336,7 +334,7 @@ let do_fixpoint ~scope ~poly l = do_program_fixpoint ~scope ~poly l; if not (check_safe ()) then Feedback.feedback Feedback.AddedAxiom else () -let do_cofixpoint ~scope ~poly l = - let fixl,ntns = extract_cofixpoint_components l in - do_program_recursive ~scope ~poly DeclareObl.IsCoFixpoint fixl ntns; +let do_cofixpoint ~scope ~poly fixl = + let fixl = List.map (fun fix -> { fix with Vernacexpr.rec_order = None }) fixl in + do_program_recursive ~scope ~poly DeclareObl.IsCoFixpoint fixl; if not (check_safe ()) then Feedback.feedback Feedback.AddedAxiom else () diff --git a/vernac/comProgramFixpoint.mli b/vernac/comProgramFixpoint.mli index f25abb95c3..a851e4dff5 100644 --- a/vernac/comProgramFixpoint.mli +++ b/vernac/comProgramFixpoint.mli @@ -1,11 +1,21 @@ +(************************************************************************) +(* * The Coq Proof Assistant / The Coq Development Team *) +(* v * INRIA, CNRS and contributors - Copyright 1999-2019 *) +(* <O___,, * (see CREDITS file for the list of authors) *) +(* \VV/ **************************************************************) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(* * (see LICENSE file for the text of the license) *) +(************************************************************************) + open Vernacexpr (** Special Fixpoint handling when command is activated. *) val do_fixpoint : (* When [false], assume guarded. *) - scope:DeclareDef.locality -> poly:bool -> (fixpoint_expr * decl_notation list) list -> unit + scope:DeclareDef.locality -> poly:bool -> fixpoint_expr list -> unit val do_cofixpoint : (* When [false], assume guarded. *) - scope:DeclareDef.locality -> poly:bool -> (cofixpoint_expr * decl_notation list) list -> unit + scope:DeclareDef.locality -> poly:bool -> cofixpoint_expr list -> unit diff --git a/vernac/declareObl.ml b/vernac/declareObl.ml index 0c45ff11d7..c5cbb095ca 100644 --- a/vernac/declareObl.ml +++ b/vernac/declareObl.ml @@ -29,9 +29,6 @@ type obligation = type obligations = obligation array * int -type notations = - (lstring * Constrexpr.constr_expr * Notation_term.scope_name option) list - type fixpoint_kind = | IsFixpoint of lident option list | IsCoFixpoint @@ -46,7 +43,7 @@ type program_info = ; prg_deps : Id.t list ; prg_fixkind : fixpoint_kind option ; prg_implicits : Impargs.manual_implicits - ; prg_notations : notations + ; prg_notations : Vernacexpr.decl_notation list ; prg_poly : bool ; prg_scope : DeclareDef.locality ; prg_kind : Decls.definition_object_kind diff --git a/vernac/declareObl.mli b/vernac/declareObl.mli index a8dd5040cb..2a8fa734b3 100644 --- a/vernac/declareObl.mli +++ b/vernac/declareObl.mli @@ -24,9 +24,6 @@ type obligation = type obligations = obligation array * int -type notations = - (lstring * Constrexpr.constr_expr * Notation_term.scope_name option) list - type fixpoint_kind = | IsFixpoint of lident option list | IsCoFixpoint @@ -41,7 +38,7 @@ type program_info = ; prg_deps : Id.t list ; prg_fixkind : fixpoint_kind option ; prg_implicits : Impargs.manual_implicits - ; prg_notations : notations + ; prg_notations : Vernacexpr.decl_notation list ; prg_poly : bool ; prg_scope : DeclareDef.locality ; prg_kind : Decls.definition_object_kind diff --git a/vernac/g_vernac.mlg b/vernac/g_vernac.mlg index 2b475f1ef9..ad5d98669d 100644 --- a/vernac/g_vernac.mlg +++ b/vernac/g_vernac.mlg @@ -402,16 +402,19 @@ GRAMMAR EXTEND Gram ; (* (co)-fixpoints *) rec_definition: - [ [ id = ident_decl; + [ [ id_decl = ident_decl; bl = binders_fixannot; - ty = type_cstr; - def = OPT [":="; def = lconstr -> { def } ]; ntn = decl_notation -> - { let bl, annot = bl in ((id,annot,bl,ty,def),ntn) } ] ] + rtype = type_cstr; + body_def = OPT [":="; def = lconstr -> { def } ]; notations = decl_notation -> + { let binders, rec_order = bl in + {fname = fst id_decl; univs = snd id_decl; rec_order; binders; rtype; body_def; notations} + } ] ] ; corec_definition: - [ [ id = ident_decl; bl = binders; ty = type_cstr; - def = OPT [":="; def = lconstr -> { def }]; ntn = decl_notation -> - { ((id,bl,ty,def),ntn) } ] ] + [ [ id_decl = ident_decl; binders = binders; rtype = type_cstr; + body_def = OPT [":="; def = lconstr -> { def }]; notations = decl_notation -> + { {fname = fst id_decl; univs = snd id_decl; rec_order = (); binders; rtype; body_def; notations} + } ]] ; type_cstr: [ [ ":"; c=lconstr -> { c } @@ -1138,7 +1141,6 @@ GRAMMAR EXTEND Gram | IDENT "Reset"; id = identref -> { VernacResetName id } | IDENT "Back" -> { VernacBack 1 } | IDENT "Back"; n = natural -> { VernacBack n } - | IDENT "BackTo"; n = natural -> { VernacBackTo n } (* Tactic Debugger *) | IDENT "Debug"; IDENT "On" -> diff --git a/vernac/lemmas.ml b/vernac/lemmas.ml index ecea9ae4c9..6a754a0cde 100644 --- a/vernac/lemmas.ml +++ b/vernac/lemmas.ml @@ -113,46 +113,6 @@ let by tac pf = (* Creating a lemma-like constant *) (************************************************************************) -(* Support for mutually proved theorems *) - -let retrieve_first_recthm uctx = function - | GlobRef.VarRef id -> - NamedDecl.get_value (Global.lookup_named id), - Decls.variable_opacity id - | GlobRef.ConstRef cst -> - let cb = Global.lookup_constant cst in - (* we get the right order somehow but surely it could be enforced in a better way *) - let uctx = UState.context uctx in - let inst = Univ.UContext.instance uctx in - let map (c, _, _) = Vars.subst_instance_constr inst c in - (Option.map map (Global.body_of_constant_body Library.indirect_accessor cb), is_opaque cb) - | _ -> assert false - -let adjust_guardness_conditions const = function - | [] -> const (* Not a recursive statement *) - | possible_indexes -> - (* Try all combinations... not optimal *) - let env = Global.env() in - let open Proof_global in - { const with proof_entry_body = - Future.chain const.proof_entry_body - (fun ((body, ctx), eff) -> - match Constr.kind body with - | Fix ((nv,0),(_,_,fixdefs as fixdecls)) -> -(* let possible_indexes = - List.map2 (fun i c -> match i with Some i -> i | None -> - List.interval 0 (List.length ((lam_assum c)))) - lemma_guard (Array.to_list fixdefs) in -*) - let env = Safe_typing.push_private_constants env eff.Evd.seff_private in - let indexes = - search_guard env - possible_indexes fixdecls in - (mkFix ((indexes,0),fixdecls), ctx), eff - | _ -> (body, ctx), eff) } - -let default_thm_id = Id.of_string "Unnamed_thm" - let check_name_freshness locality {CAst.loc;v=id} : unit = (* We check existence here: it's a bit late at Qed time *) if Nametab.exists_cci (Lib.make_path id) || is_section_variable id || @@ -160,52 +120,6 @@ let check_name_freshness locality {CAst.loc;v=id} : unit = then user_err ?loc (Id.print id ++ str " already exists.") -let save_remaining_recthms env sigma ~poly ~scope norm univs body opaq i { Recthm.name; typ; impargs } = - let t_i = norm typ in - let kind = Decls.(IsAssumption Conjectural) in - match body with - | None -> - let open DeclareDef in - (match scope with - | Discharge -> - let impl = false in (* copy values from Vernacentries *) - let univs = match univs with - | Polymorphic_entry (_, univs) -> - (* What is going on here? *) - Univ.ContextSet.of_context univs - | Monomorphic_entry univs -> univs - in - let c = Declare.SectionLocalAssum {typ=t_i; univs; poly; impl} in - let () = Declare.declare_variable ~name ~kind c in - (GlobRef.VarRef name,impargs) - | Global local -> - let kind = Decls.(IsAssumption Conjectural) in - let decl = Declare.ParameterEntry (None,(t_i,univs),None) in - let kn = Declare.declare_constant ~name ~local ~kind decl in - (GlobRef.ConstRef kn,impargs)) - | Some body -> - let body = norm body in - let rec body_i t = match Constr.kind t with - | Fix ((nv,0),decls) -> mkFix ((nv,i),decls) - | CoFix (0,decls) -> mkCoFix (i,decls) - | LetIn(na,t1,ty,t2) -> mkLetIn (na,t1,ty, body_i t2) - | Lambda(na,ty,t) -> mkLambda(na,ty,body_i t) - | App (t, args) -> mkApp (body_i t, args) - | _ -> - anomaly Pp.(str "Not a proof by induction: " ++ Printer.pr_constr_env env sigma body ++ str ".") in - let body_i = body_i body in - let open DeclareDef in - match scope with - | Discharge -> - let const = Declare.definition_entry ~types:t_i ~opaque:opaq ~univs body_i in - let c = Declare.SectionLocalDef const in - let () = Declare.declare_variable ~name ~kind c in - (GlobRef.VarRef name,impargs) - | Global local -> - let const = Declare.definition_entry ~types:t_i ~univs ~opaque:opaq body_i in - let kn = Declare.declare_constant ~name ~local ~kind (Declare.DefinitionEntry const) in - (GlobRef.ConstRef kn,impargs) - let initialize_named_context_for_proof () = let sign = Global.named_context () in List.fold_right @@ -315,9 +229,73 @@ let start_lemma_com ~program_mode ~poly ~scope ~kind ?inference_hook ?hook thms start_lemma_with_initialization ?hook ~poly ~scope ~kind evd ~udecl recguard thms snl (************************************************************************) -(* Commom constant saving path *) +(* Commom constant saving path, for both Qed and Admitted *) (************************************************************************) +(* Helper for process_recthms *) +let retrieve_first_recthm uctx = function + | GlobRef.VarRef id -> + NamedDecl.get_value (Global.lookup_named id), + Decls.variable_opacity id + | GlobRef.ConstRef cst -> + let cb = Global.lookup_constant cst in + (* we get the right order somehow but surely it could be enforced in a better way *) + let uctx = UState.context uctx in + let inst = Univ.UContext.instance uctx in + let map (c, _, _) = Vars.subst_instance_constr inst c in + (Option.map map (Global.body_of_constant_body Library.indirect_accessor cb), is_opaque cb) + | _ -> assert false + +(* Helper for process_recthms *) +let save_remaining_recthms env sigma ~poly ~scope ~udecl uctx body opaq i { Recthm.name; typ; impargs } = + let norm c = EConstr.to_constr (Evd.from_ctx uctx) c in + let body = Option.map EConstr.of_constr body in + let univs = UState.check_univ_decl ~poly uctx udecl in + let t_i = norm typ in + let kind = Decls.(IsAssumption Conjectural) in + match body with + | None -> + let open DeclareDef in + (match scope with + | Discharge -> + let impl = false in (* copy values from Vernacentries *) + let univs = match univs with + | Polymorphic_entry (_, univs) -> + (* What is going on here? *) + Univ.ContextSet.of_context univs + | Monomorphic_entry univs -> univs + in + let c = Declare.SectionLocalAssum {typ=t_i; univs; poly; impl} in + let () = Declare.declare_variable ~name ~kind c in + GlobRef.VarRef name, impargs + | Global local -> + let kind = Decls.(IsAssumption Conjectural) in + let decl = Declare.ParameterEntry (None,(t_i,univs),None) in + let kn = Declare.declare_constant ~name ~local ~kind decl in + GlobRef.ConstRef kn, impargs) + | Some body -> + let body = norm body in + let rec body_i t = match Constr.kind t with + | Fix ((nv,0),decls) -> mkFix ((nv,i),decls) + | CoFix (0,decls) -> mkCoFix (i,decls) + | LetIn(na,t1,ty,t2) -> mkLetIn (na,t1,ty, body_i t2) + | Lambda(na,ty,t) -> mkLambda(na,ty,body_i t) + | App (t, args) -> mkApp (body_i t, args) + | _ -> + anomaly Pp.(str "Not a proof by induction: " ++ Printer.pr_constr_env env sigma body ++ str ".") in + let body_i = body_i body in + let open DeclareDef in + match scope with + | Discharge -> + let const = Declare.definition_entry ~types:t_i ~opaque:opaq ~univs body_i in + let c = Declare.SectionLocalDef const in + let () = Declare.declare_variable ~name ~kind c in + GlobRef.VarRef name, impargs + | Global local -> + let const = Declare.definition_entry ~types:t_i ~univs ~opaque:opaq body_i in + let kn = Declare.declare_constant ~name ~local ~kind (Declare.DefinitionEntry const) in + GlobRef.ConstRef kn, impargs + (* This declares implicits and calls the hooks for all the theorems, including the main one *) let process_recthms ?fix_exn ?hook env sigma uctx ~udecl ~poly ~scope dref imps other_thms = @@ -325,10 +303,7 @@ let process_recthms ?fix_exn ?hook env sigma uctx ~udecl ~poly ~scope dref imps if List.is_empty other_thms then [] else (* there are several theorems defined mutually *) let body,opaq = retrieve_first_recthm uctx dref in - let norm c = EConstr.to_constr (Evd.from_ctx uctx) c in - let body = Option.map EConstr.of_constr body in - let uctx = UState.check_univ_decl ~poly uctx udecl in - List.map_i (save_remaining_recthms env sigma ~poly ~scope norm uctx body opaq) 1 other_thms in + List.map_i (save_remaining_recthms env sigma ~poly ~scope ~udecl uctx body opaq) 1 other_thms in let thms_data = (dref,imps)::other_thms_data in List.iter (fun (dref,imps) -> maybe_declare_manual_implicits false dref imps; @@ -395,10 +370,33 @@ let save_lemma_admitted ~(lemma : t) : unit = (* Saving a lemma-like constant *) (************************************************************************) +let default_thm_id = Id.of_string "Unnamed_thm" + let check_anonymity id save_ident = if not (String.equal (atompart_of_id id) (Id.to_string (default_thm_id))) then user_err Pp.(str "This command can only be used for unnamed theorem.") +(* Support for mutually proved theorems *) + +(* Helper for finish_proved *) +let adjust_guardness_conditions const = function + | [] -> const (* Not a recursive statement *) + | possible_indexes -> + (* Try all combinations... not optimal *) + let env = Global.env() in + let open Proof_global in + { const with + proof_entry_body = + Future.chain const.proof_entry_body + (fun ((body, ctx), eff) -> + match Constr.kind body with + | Fix ((nv,0),(_,_,fixdefs as fixdecls)) -> + let env = Safe_typing.push_private_constants env eff.Evd.seff_private in + let indexes = search_guard env possible_indexes fixdecls in + (mkFix ((indexes,0),fixdecls), ctx), eff + | _ -> (body, ctx), eff) + } + let finish_proved env sigma idopt po info = let open Proof_global in let { Info.hook; compute_guard; impargs; other_thms; scope; kind } = info in diff --git a/vernac/obligations.mli b/vernac/obligations.mli index f97bc784c3..2a0d0aba97 100644 --- a/vernac/obligations.mli +++ b/vernac/obligations.mli @@ -18,27 +18,33 @@ val check_evars : env -> evar_map -> unit val evar_dependencies : evar_map -> Evar.t -> Evar.Set.t val sort_dependencies : (Evar.t * evar_info * Evar.Set.t) list -> (Evar.t * evar_info * Evar.Set.t) list -(* env, id, evars, number of function prototypes to try to clear from - evars contexts, object and type *) -val eterm_obligations : env -> Id.t -> evar_map -> int -> - ?status:Evar_kinds.obligation_definition_status -> EConstr.constr -> EConstr.types -> - (Id.t * types * Evar_kinds.t Loc.located * - (bool * Evar_kinds.obligation_definition_status) * Int.Set.t * - unit Proofview.tactic option) array - (* Existential key, obl. name, type as product, - location of the original evar, associated tactic, - status and dependencies as indexes into the array *) - * ((Evar.t * Id.t) list * ((Id.t -> EConstr.constr) -> EConstr.constr -> constr)) * - constr * types - (* Translations from existential identifiers to obligation identifiers - and for terms with existentials to closed terms, given a - translation from obligation identifiers to constrs, new term, new type *) - +(* ident, type, location, (opaque or transparent, expand or define), dependencies, tactic to solve it *) type obligation_info = (Id.t * types * Evar_kinds.t Loc.located * - (bool * Evar_kinds.obligation_definition_status) * Int.Set.t * unit Proofview.tactic option) array - (* ident, type, location, (opaque or transparent, expand or define), - dependencies, tactic to solve it *) + (bool * Evar_kinds.obligation_definition_status) * Int.Set.t * unit Proofview.tactic option) array + +(* env, id, evars, number of function prototypes to try to clear from + evars contexts, object and type *) +val eterm_obligations + : env + -> Id.t + -> evar_map + -> int + -> ?status:Evar_kinds.obligation_definition_status + -> EConstr.constr + -> EConstr.types + -> obligation_info * + + (* Existential key, obl. name, type as product, location of the + original evar, associated tactic, status and dependencies as + indexes into the array *) + ((Evar.t * Id.t) list * ((Id.t -> EConstr.constr) -> EConstr.constr -> constr)) * + + (* Translations from existential identifiers to obligation + identifiers and for terms with existentials to closed terms, + given a translation from obligation identifiers to constrs, + new term, new type *) + constr * types val default_tactic : unit Proofview.tactic ref @@ -69,7 +75,7 @@ val add_mutual_definitions -> ?kind:Decls.definition_object_kind -> ?reduce:(constr -> constr) -> ?hook:DeclareDef.Hook.t -> ?opaque:bool - -> DeclareObl.notations + -> Vernacexpr.decl_notation list -> DeclareObl.fixpoint_kind -> unit val obligation diff --git a/vernac/ppvernac.ml b/vernac/ppvernac.ml index e676fe94db..0eb0b1b6f6 100644 --- a/vernac/ppvernac.ml +++ b/vernac/ppvernac.ml @@ -419,15 +419,15 @@ let string_of_theorem_kind = let open Decls in function | l -> spc() ++ hov 1 (str"(" ++ prlist_with_sep sep_v2 pr_syntax_modifier l ++ str")") - let pr_rec_definition ((iddecl,ro,bl,type_,def),ntn) = + let pr_rec_definition { fname; univs; rec_order; binders; rtype; body_def; notations } = let env = Global.env () in let sigma = Evd.from_env env in let pr_pure_lconstr c = Flags.without_option Flags.beautify pr_lconstr c in - let annot = pr_guard_annot (pr_lconstr_expr env sigma) bl ro in - pr_ident_decl iddecl ++ pr_binders_arg bl ++ annot - ++ pr_type_option (fun c -> spc() ++ pr_lconstr_expr env sigma c) type_ - ++ pr_opt (fun def -> str":=" ++ brk(1,2) ++ pr_pure_lconstr env sigma def) def - ++ prlist (pr_decl_notation @@ pr_constr env sigma) ntn + let annot = pr_guard_annot (pr_lconstr_expr env sigma) binders rec_order in + pr_ident_decl (fname,univs) ++ pr_binders_arg binders ++ annot + ++ pr_type_option (fun c -> spc() ++ pr_lconstr_expr env sigma c) rtype + ++ pr_opt (fun def -> str":=" ++ brk(1,2) ++ pr_pure_lconstr env sigma def) body_def + ++ prlist (pr_decl_notation @@ pr_constr env sigma) notations let pr_statement head (idpl,(bl,c)) = let env = Global.env () in @@ -669,8 +669,6 @@ let string_of_definition_object_kind = let open Decls in function return ( if Int.equal i 1 then keyword "Back" else keyword "Back" ++ pr_intarg i ) - | VernacBackTo i -> - return (keyword "BackTo" ++ pr_intarg i) (* State management *) | VernacWriteState s -> @@ -858,11 +856,11 @@ let string_of_definition_object_kind = let open Decls in function | DoDischarge -> keyword "Let" ++ spc () | NoDischarge -> str "" in - let pr_onecorec ((iddecl,bl,c,def),ntn) = - pr_ident_decl iddecl ++ spc() ++ pr_binders env sigma bl ++ spc() ++ str":" ++ - spc() ++ pr_lconstr_expr env sigma c ++ - pr_opt (fun def -> str":=" ++ brk(1,2) ++ pr_lconstr env sigma def) def ++ - prlist (pr_decl_notation @@ pr_constr env sigma) ntn + let pr_onecorec {fname; univs; binders; rtype; body_def; notations } = + pr_ident_decl (fname,univs) ++ spc() ++ pr_binders env sigma binders ++ spc() ++ str":" ++ + spc() ++ pr_lconstr_expr env sigma rtype ++ + pr_opt (fun def -> str":=" ++ brk(1,2) ++ pr_lconstr env sigma def) body_def ++ + prlist (pr_decl_notation @@ pr_constr env sigma) notations in return ( hov 0 (local ++ keyword "CoFixpoint" ++ spc() ++ diff --git a/vernac/ppvernac.mli b/vernac/ppvernac.mli index d4d49a09a3..9ade5afb87 100644 --- a/vernac/ppvernac.mli +++ b/vernac/ppvernac.mli @@ -14,7 +14,7 @@ val pr_set_entry_type : ('a -> Pp.t) -> 'a Extend.constr_entry_key_gen -> Pp.t (** Prints a fixpoint body *) -val pr_rec_definition : (Vernacexpr.fixpoint_expr * Vernacexpr.decl_notation list) -> Pp.t +val pr_rec_definition : Vernacexpr.fixpoint_expr -> Pp.t (** Prints a vernac expression without dot *) val pr_vernac_expr : Vernacexpr.vernac_expr -> Pp.t diff --git a/vernac/pvernac.mli b/vernac/pvernac.mli index c9eb979a90..3bd252ecef 100644 --- a/vernac/pvernac.mli +++ b/vernac/pvernac.mli @@ -23,7 +23,7 @@ module Vernac_ : val command : vernac_expr Entry.t val syntax : vernac_expr Entry.t val vernac_control : vernac_control Entry.t - val rec_definition : (fixpoint_expr * decl_notation list) Entry.t + val rec_definition : fixpoint_expr Entry.t val noedit_mode : vernac_expr Entry.t val command_entry : vernac_expr Entry.t val main_entry : vernac_control option Entry.t diff --git a/vernac/vernacentries.ml b/vernac/vernacentries.ml index 46ddf214ab..9af8d8b67c 100644 --- a/vernac/vernacentries.ml +++ b/vernac/vernacentries.ml @@ -772,7 +772,7 @@ let vernac_inductive ~atts cum lo finite indl = let vernac_fixpoint_common ~atts discharge l = if Dumpglob.dump () then - List.iter (fun (((lid,_), _, _, _, _), _) -> Dumpglob.dump_definition lid false "def") l; + List.iter (fun { fname } -> Dumpglob.dump_definition fname false "def") l; enforce_locality_exp atts.DefAttributes.locality discharge let vernac_fixpoint_interactive ~atts discharge l = @@ -793,7 +793,7 @@ let vernac_fixpoint ~atts discharge l = let vernac_cofixpoint_common ~atts discharge l = if Dumpglob.dump () then - List.iter (fun (((lid,_), _, _, _), _) -> Dumpglob.dump_definition lid false "def") l; + List.iter (fun { fname } -> Dumpglob.dump_definition fname false "def") l; enforce_locality_exp atts.DefAttributes.locality discharge let vernac_cofixpoint_interactive ~atts discharge l = @@ -2298,7 +2298,6 @@ let rec translate_vernac ~atts v = let open Vernacextend in match v with | VernacResetName _ | VernacResetInitial | VernacBack _ - | VernacBackTo _ | VernacAbort _ -> anomaly (str "type_vernac") (* Syntax *) @@ -2358,7 +2357,7 @@ let rec translate_vernac ~atts v = let open Vernacextend in match v with | VernacInductive (cum, priv, finite, l) -> VtDefault(fun () -> vernac_inductive ~atts cum priv finite l) | VernacFixpoint (discharge, l) -> - let opens = List.exists (fun ((_,_,_,_,p),_) -> Option.is_empty p) l in + let opens = List.exists (fun { body_def } -> Option.is_empty body_def) l in if opens then VtOpenProof (fun () -> with_def_attributes ~atts vernac_fixpoint_interactive discharge l) @@ -2366,7 +2365,7 @@ let rec translate_vernac ~atts v = let open Vernacextend in match v with VtDefault (fun () -> with_def_attributes ~atts vernac_fixpoint discharge l) | VernacCoFixpoint (discharge, l) -> - let opens = List.exists (fun ((_,_,_,p),_) -> Option.is_empty p) l in + let opens = List.exists (fun { body_def } -> Option.is_empty body_def) l in if opens then VtOpenProof(fun () -> with_def_attributes ~atts vernac_cofixpoint_interactive discharge l) else @@ -2630,7 +2629,6 @@ and interp_expr ?proof ~atts ~st c = | VernacResetName _ -> anomaly (str "VernacResetName not handled by Stm.") | VernacResetInitial -> anomaly (str "VernacResetInitial not handled by Stm.") | VernacBack _ -> anomaly (str "VernacBack not handled by Stm.") - | VernacBackTo _ -> anomaly (str "VernacBackTo not handled by Stm.") (* This one is possible to handle here *) | VernacAbort id -> CErrors.user_err (str "Abort cannot be used through the Load command") diff --git a/vernac/vernacexpr.ml b/vernac/vernacexpr.ml index ee1f839b8d..0968632c2d 100644 --- a/vernac/vernacexpr.ml +++ b/vernac/vernacexpr.ml @@ -128,18 +128,26 @@ type definition_expr = | DefineBody of local_binder_expr list * Genredexpr.raw_red_expr option * constr_expr * constr_expr option -type fixpoint_expr = - ident_decl * recursion_order_expr option * local_binder_expr list * constr_expr * constr_expr option +type decl_notation = lstring * constr_expr * scope_name option + +type 'a fix_expr_gen = + { fname : lident + ; univs : universe_decl_expr option + ; rec_order : 'a + ; binders : local_binder_expr list + ; rtype : constr_expr + ; body_def : constr_expr option + ; notations : decl_notation list + } -type cofixpoint_expr = - ident_decl * local_binder_expr list * constr_expr * constr_expr option +type fixpoint_expr = recursion_order_expr option fix_expr_gen +type cofixpoint_expr = unit fix_expr_gen type local_decl_expr = | AssumExpr of lname * constr_expr | DefExpr of lname * constr_expr * constr_expr option type inductive_kind = Inductive_kw | CoInductive | Variant | Record | Structure | Class of bool (* true = definitional, false = inductive *) -type decl_notation = lstring * constr_expr * scope_name option type simple_binder = lident list * constr_expr type class_binder = lident * constr_expr list type 'a with_coercion = coercion_flag * 'a @@ -283,8 +291,8 @@ type nonrec vernac_expr = | VernacAssumption of (discharge * Decls.assumption_object_kind) * Declaremods.inline * (ident_decl list * constr_expr) with_coercion list | VernacInductive of vernac_cumulative option * bool (* private *) * inductive_flag * (inductive_expr * decl_notation list) list - | VernacFixpoint of discharge * (fixpoint_expr * decl_notation list) list - | VernacCoFixpoint of discharge * (cofixpoint_expr * decl_notation list) list + | VernacFixpoint of discharge * fixpoint_expr list + | VernacCoFixpoint of discharge * cofixpoint_expr list | VernacScheme of (lident option * scheme) list | VernacCombinedScheme of lident * lident list | VernacUniverse of lident list @@ -351,7 +359,6 @@ type nonrec vernac_expr = | VernacResetName of lident | VernacResetInitial | VernacBack of int - | VernacBackTo of int (* Commands *) | VernacCreateHintDb of string * bool diff --git a/vernac/vernacprop.ml b/vernac/vernacprop.ml index 1dd8164ebc..747998c6cc 100644 --- a/vernac/vernacprop.ml +++ b/vernac/vernacprop.ml @@ -32,7 +32,6 @@ let rec has_Fail v = v |> CAst.with_val (function let is_navigation_vernac_expr = function | VernacResetInitial | VernacResetName _ - | VernacBackTo _ | VernacBack _ -> true | _ -> false |