| Age | Commit message (Collapse) | Author |
|---|
|
|
|
|
|
These tactics now work correctly with multisuccess tactics by wrapping
the tactic argument in `once`.
Fixes #10965
|
|
This helps extraction by not building sigT which can lower to Prop by
template polymorphism.
Bug #10757 can probably still be triggered by using module functors to
hide that we're using Prop from Program Fixpoint but that's probably
unfixable without fixing extraction vs template polymorphism in
general.
In passing we notice that Program doesn't know how to telescope SProp
arguments, we would need a bunch of variants of sigma types to deal
with it (or use Box?) so let's figure it out some other time.
We also reuse the universe instance to avoid generating a bunch of
short-lived universes in the universe polymorphic case.
|
|
Reviewed-by: Zimmi48
Reviewed-by: herbelin
|
|
|
|
Co-authored-by: Konstantinos Kallas <konstantinos.kallas@hotmail.com>
|
|
This could be Prop (for compat with usual Coq), Set (for HoTT),
or actually an arbitrary "i".
Take lower bound of universes into account in pretyping/engine
Reinstate proper elaboration of SProp <= l constraints:
replacing is_small with equality with lbound is _not_ semantics preserving!
lbound = Set
Elaborate template polymorphic inductives with lower bound Prop
This will make more constraints explicit
Check univ constraints with Prop as lower bound for template inductives
Restrict template polymorphic universes to those not bounded from below
Fixes #9294
fix suggested by Matthieu
Try second fix suggested by Matthieu
Take care of modifying elaboration for record declarations as well.
Rebase and export functions for debug
Remove exported functions used while debugging
Add a new typing flag "check_template" and option "-no-template-checl"
This parameterizes the new criterion on template polymorphic inductives
to allow bypassing it (necessary for backward compatibility).
Update checker to the new typing flags structure
Switch on the new template_check flag to allow old unsafe behavior in
indTyping.
This is the only change of code really impacting the kernel, together
with the commit implementing unbounded from below and parameterization
by the lower bound on universes.
Add deprecated option `Unset Template Check` allowing to make proof
scripts work with both 8.9 and 8.10 for a while
Fix `Template Check` option name and test it
Add `Unset Template Check` to Coq89.v
Cooking of inductives and template-check tests
Cleanup test-suite file for template check / universes(template) flags
cookind tests
Move test of `Unset Template Check` to the failure/ dir, but comment it
for now
Template test-suite test explanation
Overlays for PR 9918
Overlay for paramcoq
Add overlay for fiat_parsers (-no-template-check)
Add overlay for fiat_crypto_legacy
Update fiat-crypto legacy overlay
Now it points at the version that I plan on merging; I am hoping that doing this will guard against mistakes by adding an extra check that the target tested by Coq's CI on this branch works with the change I made.
Remove overlay that should no longer be necessary
The setting in the compat file should handle it
Remove now-merged fiat-crypto-legacy overlay
Update `Print Assumptions` to reflect the typing flag for template checking
Fix About and Print Assumptions for template poly, giving info on which
variables are actually polymorphic
Fix pretty printing to print global universe levels properly
Fix printing of template polymorphic universes
Fix pretty printing for template polymorphism on no universe
Fix interaction of template check and universes(template) flag
Fix indTyping to really check if there is any point in polymorphism: the
conclusion sort should be parameterized over at least one local universe
Indtyping fixes for template polymorphic Props
Allow explicit template polymorphism again
Adapt to new indTyping interface
Handle the case of template-polymorphic on no universes
correctly (morally Type0m univ represented as Prop).
Fix check of meaningfullness of template polymorphism in the kernel.
It is now done w.r.t the min_univ, the minimal universe inferred for the
inductive/record type, independently of the user-written annotation
which must only be larger than min_univ. This preserves compatibility
with UniMath and template-polymorphism as it has been implemented up-to
now.
Comment on identity non-template-polymorphism
Remove incorrect universes(template) attributes from ssr
simpl_fun can be meaningfully template-poly, as well as
pred_key (although the use is debatable: it could just
as well be in Prop).
Move `fun_of_simpl` coercion declaration out of section to respect
uniform inheritance
Remove incorrect uses of #[universes(template)] from the stdlib
Extraction of micromega changes due to moving an ind decl out of a section
Remove incorrect uses of #[universes(template)] from plugins
Fix test-suite files, removing incorrect #[universes(template)] attributes
Remove incorrect #[universes(template)] attributes in test-suite
Fix test-suite
Remove overlays as they have been merged upstream.
|
|
|
|
sometimes, to use "intros [= ...]" rather than things like "intros H;
injection H as [= ...]".
Co-Authored-By: Théo Zimmermann <theo.zimmermann@univ-paris-diderot.fr>
|
|
|
|
Reviewed-by: Zimmi48
Reviewed-by: ejgallego
Ack-by: gares
Ack-by: herbelin
Ack-by: ppedrot
Ack-by: proux01
|
|
Reviewed-by: Zimmi48
Reviewed-by: ejgallego
Reviewed-by: jfehrle
Ack-by: maximedenes
Reviewed-by: ppedrot
|
|
This removes various compatibility notations.
Closes #8374
This commit was mostly created by running `./dev/tools/update-compat.py
--release`. There's a bit of manual spacing adjustment around all of the
removed compatibility notations, and some test-suite updates were done
manually.
The update to CHANGES.md was manual.
|
|
Rather than integers '[0-9]+', numeral constant can now be parsed
according to the regexp '[0-9]+ ([.][0-9]+)? ([eE][+-]?[0-9]+)?'.
This can be used in one of the two following ways:
- using the function `Notation.register_rawnumeral_interpreter` in an OCaml plugin
- using `Numeral Notation` with the type `decimal` added to `Decimal.v`
See examples of each use case in the next two commits.
|
|
Previously, they were hard-wired in the ML code.
|
|
|
|
Reviewed-by: Zimmi48
Reviewed-by: herbelin
Reviewed-by: ppedrot
|
|
Fixes #9453
|
|
|
|
ie default goal selector !
How to do this:
- change the default value of default goal selector in goal_select.ml
- eval the emacs code in this commit message
- compile Coq and in each erroring file repeatedly run
[C-c f] (my/maybe-fix-buller-error) then [C-c C-b] (proof-process-buffer)
until there are no errors (NB the first [C-c f] has no effect).
You need to watch for 2 cases:
- overly deep proofs where the bullets need to go beyond the list in
my/bullet-stack (6 layers is enough the vast majority of the time
though). The system will give you an error and you need to finish
the lemma manually.
- weird indentation when a bullet starts in the middle of a line and
doesn't end in that line. Just reindent as you like then go to the
next error and continue.
~~~emacs-lisp
(defconst my/bullet-stack (list "-" "+" "*" "--" "++" "**")
"Which bullets should be used, in order.")
(defvar-local my/bullet-count nil
"The value in the car indicates how many goals remain in the
bullet at (length-1), and so on recursively. nil means we
haven't started bulleting the current proof.")
(defvar-local my/last-seen-qed nil)
(defun my/get-maybe-bullet-error ()
"Extract the number of focused goals from the ! selector error message."
(when-let* ((rbuf (get-buffer "*response*"))
(str (with-current-buffer "*response*" (buffer-string)))
(_ (string-match
(rx "Error: Expected a single focused goal but " (group (+ digit)))
str))
(ngoals (string-to-number (match-string 1 str))))
ngoals))
(defun my/bullet-fix-indent ()
"Auto indent until the next Qed/Defined, and update my/last-seen-qed."
;; (insert (format "(* %s -> %s *)\n" my/prev-count my/bullet-count))
(when-let ((qed (save-excursion (search-forward-regexp (rx (or "Defined." "Qed.")) nil t))))
(set-marker my/last-seen-qed qed)
(indent-region (- (point) 1) qed)))
(defun my/nth-bullet (n)
"Get nth bullet, erroring if n >= length my/bullet-stack"
(or (nth n my/bullet-stack)
(error "Too many bullets.")))
(defun my/maybe-fix-bullet-error (&optional arg)
"Main function for porting a file to strict focusing.
Repeatedly process your file in proof general until you get a
focusing error, then run this function. Once there are no more
errors you're done.
Indentation commonly looks bad in the middle of fixing a proof,
but will be fixed unless you start a bullet in the middle of a
line and don't finish it in that line. ie in 'tac1. - tac2.\n
tac3.' tac3 will get indented to align with tac2, but if tac2
finished the bullet the next action will reindent.
This is a stateful process. The state is automatically reset when
you get to the next proof, but if you get an error or take manual
action which breaks the algorithm's expectation you can call with
prefix argument to reset."
(interactive "P")
(unless my/last-seen-qed
(setq my/last-seen-qed (set-marker (make-marker) 0)))
(when (or arg (> (point) my/last-seen-qed))
(setq my/bullet-count nil)
(set-marker my/last-seen-qed 0))
(when-let ((ngoals (my/get-maybe-bullet-error)))
(setq my/prev-count (format "%s %s" ngoals my/bullet-count))
(if (= ngoals 0)
(progn
(while (and my/bullet-count (= (car my/bullet-count) 0))
(pop my/bullet-count))
(insert (concat (my/nth-bullet (- (length my/bullet-count) 1)) " "))
(setq my/bullet-count (cons (- (car my/bullet-count) 1) (cdr my/bullet-count)))
(my/bullet-fix-indent))
(setq my/bullet-count (cons (- ngoals 1) my/bullet-count))
(insert (concat (my/nth-bullet (- (length my/bullet-count) 1)) " "))
(my/bullet-fix-indent))))
(bind-key "C-c f" #'my/maybe-fix-bullet-error coq-mode-map)
~~~
|
|
|
|
We encode the conversion to bits with little-endian right-associative
tuples to ensure that the head of the tuple (the `fst` element) is the
least significant bit. We still enforce that the ordering of bits
matches the order of the `bool`s in the `ascii` inductive type.
|
|
We could move another ~ 1s from Init.Byte to Strings.Byte by moving
`of_bits_to_bits` and `to_bits_of_bits`, but I figured it's probably not
worth it.
After | File Name | Before || Change | % Change
----------------------------------------------------------------------------------
1m16.75s | Total | 1m21.45s || -0m04.70s | -5.77%
----------------------------------------------------------------------------------
0m08.95s | Strings/Byte | 0m12.41s || -0m03.46s | -27.88%
0m07.24s | Byte | 0m08.76s || -0m01.51s | -17.35%
0m06.37s | plugins/setoid_ring/Ring_polynom | 0m06.24s || +0m00.12s | +2.08%
0m03.14s | Numbers/Integer/Abstract/ZBits | 0m03.20s || -0m00.06s | -1.87%
0m02.44s | ZArith/BinInt | 0m02.44s || +0m00.00s | +0.00%
0m02.24s | Numbers/Natural/Abstract/NBits | 0m02.20s || +0m00.04s | +1.81%
0m01.97s | Lists/List | 0m01.93s || +0m00.04s | +2.07%
0m01.85s | Numbers/NatInt/NZLog | 0m01.82s || +0m00.03s | +1.64%
0m01.78s | PArith/BinPos | 0m01.78s || +0m00.00s | +0.00%
0m01.74s | plugins/setoid_ring/InitialRing | 0m01.63s || +0m00.11s | +6.74%
0m01.73s | Strings/Ascii | 0m01.58s || +0m00.14s | +9.49%
0m01.39s | NArith/BinNat | 0m01.34s || +0m00.04s | +3.73%
0m01.32s | Numbers/NatInt/NZPow | 0m01.24s || +0m00.08s | +6.45%
0m01.22s | Numbers/NatInt/NZSqrt | 0m01.15s || +0m00.07s | +6.08%
0m01.11s | Arith/PeanoNat | 0m01.16s || -0m00.04s | -4.31%
0m01.10s | Numbers/Integer/Abstract/ZDivTrunc | 0m01.11s || -0m00.01s | -0.90%
0m01.02s | Specif | 0m01.04s || -0m00.02s | -1.92%
0m00.96s | Numbers/NatInt/NZMulOrder | 0m00.84s || +0m00.12s | +14.28%
0m00.95s | Numbers/Integer/Abstract/ZDivFloor | 0m00.97s || -0m00.02s | -2.06%
0m00.85s | plugins/setoid_ring/Ring_theory | 0m00.86s || -0m00.01s | -1.16%
0m00.82s | Structures/GenericMinMax | 0m00.85s || -0m00.03s | -3.52%
0m00.72s | Numbers/Integer/Abstract/ZLcm | 0m00.82s || -0m00.09s | -12.19%
0m00.69s | Numbers/NatInt/NZParity | 0m00.69s || +0m00.00s | +0.00%
0m00.68s | Numbers/NatInt/NZDiv | 0m00.71s || -0m00.02s | -4.22%
0m00.68s | Strings/String | 0m00.65s || +0m00.03s | +4.61%
0m00.64s | Numbers/Integer/Abstract/ZSgnAbs | 0m00.64s || +0m00.00s | +0.00%
0m00.64s | ZArith/Zeven | 0m00.48s || +0m00.16s | +33.33%
0m00.63s | ZArith/Zorder | 0m00.61s || +0m00.02s | +3.27%
0m00.57s | Numbers/Integer/Abstract/ZMulOrder | 0m00.67s || -0m00.10s | -14.92%
0m00.56s | Classes/Morphisms | 0m00.58s || -0m00.01s | -3.44%
0m00.55s | Numbers/NatInt/NZOrder | 0m00.51s || +0m00.04s | +7.84%
0m00.48s | ZArith/BinIntDef | 0m00.48s || +0m00.00s | +0.00%
0m00.46s | Classes/CMorphisms | 0m00.48s || -0m00.01s | -4.16%
0m00.46s | Numbers/Integer/Abstract/ZGcd | 0m00.46s || +0m00.00s | +0.00%
0m00.46s | Numbers/Natural/Abstract/NSub | 0m00.48s || -0m00.01s | -4.16%
0m00.45s | Logic | 0m00.44s || +0m00.01s | +2.27%
0m00.45s | Numbers/Natural/Abstract/NGcd | 0m00.48s || -0m00.02s | -6.24%
0m00.42s | Numbers/Natural/Abstract/NLcm | 0m00.40s || +0m00.01s | +4.99%
0m00.42s | Structures/OrdersFacts | 0m00.48s || -0m00.06s | -12.50%
0m00.41s | ZArith/Zbool | 0m00.38s || +0m00.02s | +7.89%
0m00.38s | Numbers/Integer/Abstract/ZPow | 0m00.34s || +0m00.03s | +11.76%
0m00.36s | Bool/Bool | 0m00.36s || +0m00.00s | +0.00%
0m00.36s | Numbers/NatInt/NZGcd | 0m00.35s || +0m00.01s | +2.85%
0m00.36s | ZArith/ZArith_dec | 0m00.38s || -0m00.02s | -5.26%
0m00.34s | Numbers/Integer/Abstract/ZAdd | 0m00.33s || +0m00.01s | +3.03%
0m00.34s | PArith/Pnat | 0m00.31s || +0m00.03s | +9.67%
0m00.32s | Numbers/Natural/Abstract/NOrder | 0m00.32s || +0m00.00s | +0.00%
0m00.32s | PArith/BinPosDef | 0m00.31s || +0m00.01s | +3.22%
0m00.32s | ZArith/Zcompare | 0m00.28s || +0m00.03s | +14.28%
0m00.30s | Classes/RelationClasses | 0m00.29s || +0m00.01s | +3.44%
0m00.30s | NArith/Nnat | 0m00.30s || +0m00.00s | +0.00%
0m00.29s | Numbers/Natural/Abstract/NAxioms | 0m00.26s || +0m00.02s | +11.53%
0m00.28s | Numbers/Integer/Abstract/ZAddOrder | 0m00.28s || +0m00.00s | +0.00%
0m00.28s | Structures/Orders | 0m00.30s || -0m00.01s | -6.66%
0m00.27s | Numbers/Integer/Abstract/ZAxioms | 0m00.23s || +0m00.04s | +17.39%
0m00.27s | Numbers/NatInt/NZAxioms | 0m00.26s || +0m00.01s | +3.84%
0m00.26s | Numbers/Integer/Abstract/ZMaxMin | 0m00.25s || +0m00.01s | +4.00%
0m00.26s | Numbers/NatInt/NZAdd | 0m00.28s || -0m00.02s | -7.14%
0m00.26s | Numbers/Natural/Abstract/NMaxMin | 0m00.24s || +0m00.02s | +8.33%
0m00.26s | Numbers/Natural/Abstract/NParity | 0m00.31s || -0m00.04s | -16.12%
0m00.26s | plugins/setoid_ring/ArithRing | 0m00.22s || +0m00.04s | +18.18%
0m00.26s | plugins/setoid_ring/Ring_tac | 0m00.24s || +0m00.02s | +8.33%
0m00.25s | Logic/Decidable | 0m00.26s || -0m00.01s | -3.84%
0m00.25s | Structures/OrdersTac | 0m00.25s || +0m00.00s | +0.00%
0m00.24s | Classes/Equivalence | 0m00.25s || -0m00.01s | -4.00%
0m00.24s | Datatypes | 0m00.27s || -0m00.03s | -11.11%
0m00.24s | Numbers/NatInt/NZMul | 0m00.25s || -0m00.01s | -4.00%
0m00.24s | plugins/setoid_ring/Ring | 0m00.20s || +0m00.03s | +19.99%
0m00.23s | Numbers/NatInt/NZAddOrder | 0m00.33s || -0m00.10s | -30.30%
0m00.23s | Numbers/Natural/Abstract/NAdd | 0m00.17s || +0m00.06s | +35.29%
0m00.22s | Arith/Compare_dec | 0m00.22s || +0m00.00s | +0.00%
0m00.22s | Classes/CRelationClasses | 0m00.25s || -0m00.03s | -12.00%
0m00.22s | Logic/EqdepFacts | 0m00.19s || +0m00.03s | +15.78%
0m00.22s | NArith/BinNatDef | 0m00.25s || -0m00.03s | -12.00%
0m00.22s | plugins/setoid_ring/Ring_base | 0m00.23s || -0m00.01s | -4.34%
0m00.21s | Arith/Arith | 0m00.19s || +0m00.01s | +10.52%
0m00.21s | Numbers/Natural/Abstract/NDiv | 0m00.19s || +0m00.01s | +10.52%
0m00.20s | Numbers/Integer/Abstract/ZProperties | 0m00.23s || -0m00.03s | -13.04%
0m00.20s | Relations/Relation_Operators | 0m00.17s || +0m00.03s | +17.64%
0m00.19s | Arith/Between | 0m00.22s || -0m00.03s | -13.63%
0m00.18s | Arith/Wf_nat | 0m00.24s || -0m00.06s | -25.00%
0m00.17s | Arith/Plus | 0m00.16s || +0m00.01s | +6.25%
0m00.17s | Nat | 0m00.18s || -0m00.00s | -5.55%
0m00.17s | Numbers/Natural/Abstract/NProperties | 0m00.22s || -0m00.04s | -22.72%
0m00.17s | Relations/Relation_Definitions | 0m00.08s || +0m00.09s | +112.50%
0m00.16s | Numbers/Integer/Abstract/ZLt | 0m00.16s || +0m00.00s | +0.00%
0m00.16s | Numbers/Natural/Abstract/NBase | 0m00.19s || -0m00.03s | -15.78%
0m00.16s | Numbers/Natural/Abstract/NPow | 0m00.15s || +0m00.01s | +6.66%
0m00.15s | Classes/Morphisms_Prop | 0m00.18s || -0m00.03s | -16.66%
0m00.14s | Arith/Mult | 0m00.12s || +0m00.02s | +16.66%
0m00.14s | Arith/Peano_dec | 0m00.16s || -0m00.01s | -12.49%
0m00.14s | Numbers/NatInt/NZBase | 0m00.13s || +0m00.01s | +7.69%
0m00.14s | Numbers/Natural/Abstract/NMulOrder | 0m00.13s || +0m00.01s | +7.69%
0m00.14s | Relations/Operators_Properties | 0m00.13s || +0m00.01s | +7.69%
0m00.14s | plugins/setoid_ring/BinList | 0m00.16s || -0m00.01s | -12.49%
0m00.13s | Arith/EqNat | 0m00.18s || -0m00.04s | -27.77%
0m00.13s | Structures/Equalities | 0m00.17s || -0m00.04s | -23.52%
0m00.12s | Arith/Lt | 0m00.11s || +0m00.00s | +9.09%
0m00.12s | Arith/Minus | 0m00.13s || -0m00.01s | -7.69%
0m00.12s | Decimal | 0m00.16s || -0m00.04s | -25.00%
0m00.12s | Numbers/Integer/Abstract/ZBase | 0m00.09s || +0m00.03s | +33.33%
0m00.12s | Numbers/Integer/Abstract/ZMul | 0m00.12s || +0m00.00s | +0.00%
0m00.12s | Numbers/Integer/Abstract/ZParity | 0m00.11s || +0m00.00s | +9.09%
0m00.12s | Numbers/Natural/Abstract/NAddOrder | 0m00.12s || +0m00.00s | +0.00%
0m00.11s | Arith/Factorial | 0m00.11s || +0m00.00s | +0.00%
0m00.11s | Lists/ListTactics | 0m00.13s || -0m00.02s | -15.38%
0m00.11s | Logic/Eqdep_dec | 0m00.12s || -0m00.00s | -8.33%
0m00.11s | Numbers/Natural/Abstract/NLog | 0m00.10s || +0m00.00s | +9.99%
0m00.11s | Peano | 0m00.10s || +0m00.00s | +9.99%
0m00.11s | Program/Basics | 0m00.07s || +0m00.03s | +57.14%
0m00.10s | Arith/Gt | 0m00.13s || -0m00.03s | -23.07%
0m00.10s | Bool/Sumbool | 0m00.10s || +0m00.00s | +0.00%
0m00.10s | Numbers/Natural/Abstract/NSqrt | 0m00.12s || -0m00.01s | -16.66%
0m00.10s | Wf | 0m00.11s || -0m00.00s | -9.09%
0m00.09s | Arith/Arith_base | 0m00.09s || +0m00.00s | +0.00%
0m00.09s | Logic_Type | 0m00.08s || +0m00.00s | +12.49%
0m00.08s | Arith/Le | 0m00.11s || -0m00.03s | -27.27%
0m00.08s | Numbers/BinNums | 0m00.06s || +0m00.02s | +33.33%
0m00.08s | Numbers/NatInt/NZBits | 0m00.12s || -0m00.03s | -33.33%
0m00.08s | Numbers/NatInt/NZProperties | 0m00.09s || -0m00.00s | -11.11%
0m00.08s | Program/Tactics | 0m00.08s || +0m00.00s | +0.00%
0m00.07s | Tactics | 0m00.10s || -0m00.03s | -30.00%
0m00.06s | Classes/SetoidTactics | 0m00.06s || +0m00.00s | +0.00%
0m00.06s | Numbers/NumPrelude | 0m00.06s || +0m00.00s | +0.00%
0m00.05s | Classes/Init | 0m00.04s || +0m00.01s | +25.00%
0m00.05s | Prelude | 0m00.09s || -0m00.03s | -44.44%
0m00.05s | Setoids/Setoid | 0m00.08s || -0m00.03s | -37.50%
0m00.04s | Relations/Relations | 0m00.04s || +0m00.00s | +0.00%
0m00.04s | Tauto | 0m00.09s || -0m00.05s | -55.55%
0m00.02s | Notations | 0m00.04s || -0m00.02s | -50.00%
|
|
Users can now register string notations for custom inductives.
Much of the code and documentation was copied from numeral notations.
I chose to use a 256-constructor inductive for primitive string syntax
because (a) it is easy to convert between character codes and
constructors, and (b) it is more efficient than the existing `ascii`
type.
Some choices about proofs of the new `byte` type were made based on
efficiency. For example, https://github.com/coq/coq/issues/8517 means
that we cannot simply use `Scheme Equality` for this type, and I have
taken some care to ensure that the proofs of decidable equality and
conversion are fast. (Unfortunately, the `Init/Byte.v` file is the
slowest one in the prelude (it takes a couple of seconds to build), and
I'm not sure where the slowness is.)
In String.v, some uses of `0` as a `nat` were replaced by `O`, because
the file initially refused to check interactively otherwise (it
complained that `0` could not be interpreted in `string_scope` before
loading `Coq.Strings.String`).
There is unfortunately a decent amount of code duplication between
numeral notations and string notations.
I have not put too much thought into chosing names; most names have been
chosen to be similar to numeral notations, though I chose the name
`byte` from
https://github.com/coq/coq/issues/8483#issuecomment-421671785.
Unfortunately, this feature does not support declaring string syntax for
`list ascii`, unless that type is wrapped in a record or other inductive
type. This is not a fundamental limitation; it should be relatively
easy for someone who knows the API of the reduction machinery in Coq to
extend both this and numeral notations to support any type whose hnf
starts with an inductive type. (The reason for needing an inductive
type to bottom out at is that this is how the plugin determines what
constructors are the entry points for printing the given notation.
However, see also https://github.com/coq/coq/issues/8964 for
complications that are more likely to arise if inductive type families
are supported.)
N.B. I generated the long lists of constructors for the `byte` type with
short python scripts.
Closes #8853
|
|
Previously, hints added without a specified database where implicitly
put in the "core" database, which was discouraged by the user manual
(because of the lack of modularity of this approach).
|
|
We refactor the `Coqlib` API to locate objects over a namespace
`module.object.property`.
This introduces the vernacular command `Register g as n` to expose the
Coq constant `g` under the name `n` (through the `register_ref`
function). The constant can then be dynamically located using the
`lib_ref` function.
Co-authored-by: Emilio Jesús Gallego Arias <e+git@x80.org>
Co-authored-by: Maxime Dénès <mail@maximedenes.fr>
Co-authored-by: Vincent Laporte <Vincent.Laporte@fondation-inria.fr>
|
|
All changes done with
```
git grep --name-only 'compat "8.6"' | xargs sed -i s'/compat "8.6"/compat "8.7"/g'
```
As per https://github.com/coq/coq/pull/8374#issuecomment-426202818 and
https://github.com/coq/coq/issues/8383#issuecomment-426200497
|
|
|
|
|
|
|
|
Removing in passing two Local which are no-ops in practice.
|
|
This avoid a clash with int_scope in ssreflect's ssrint.v
|
|
This parsing/printing method for nat should be just as fast as
the previous dedicated code. Moreover, we could now parse large
literals as nat numbers, by leaving them in a half-abstract form
such as (Nat.of_uint 123456). This form is convertible to the
closed (S (S (S ...))) form, so it shouldn't be a big deal for
compatibility, except for if some Ltac stuff relies on (S ...) to be
present after parsing. Of course, forcing the computation of
a (Nat.of_uint ....) may take a while or raise a Stack Overflow.
|
|
This way, we could fully bypass bigint.ml.
The previous mechanism of parsing/printing Z is kept for now.
Currently, the conversion functions accepted by Numeral Notation foo
may have the following types.
for parsing:
int -> foo
int -> option foo
uint -> foo
uint -> option foo
Z -> foo
Z -> option foo
for printing:
foo -> int
foo -> option int
foo -> uint
foo -> option uint
foo -> Z
foo -> option Z
Notes:
- The Declare ML Module is directly done in Prelude
- When doing a Numeral Notation, having the Z datatype around
isn't mandatory anymore (but the error messages suggest that
it can still be used).
- An option (abstract after ...) allows to keep large numbers in
an abstract form such as (Nat.of_uint 123456) instead of reducing
to (S (S (S ...))) and ending immediately with Stack Overflow.
- After checking with Matthieu, there is now a explicit check
and an error message in case of polymorphic inductive types
|
|
|
|
|
|
This gives user control on the transparent state of a hint db. Can
override defaults more easily (report by J. H. Jourdan).
For "core", declare that variables can be unfolded, but no constants
(ensures compatibility with previous auto which allowed conv on closed
terms)
Document Hint Variables
|
|
|
|
|
|
|
|
|
|
This was decided during the Fall WG (2017).
The aliases that are kept as deprecated are the ones where the difference
is only a prefix becoming a qualified module name.
The intention is to turn the warning for deprecated notations on.
We change the compat version to 8.6 to allow the removal of VOld and V8_5.
|
|
|
|
|
|
|
|
|
|
|
|
|
|
Concretely, we bypass the following limitation: The notation
"{ ' pat | P }" broke the parsing of expressions of the form
"{ forall x, P } + { Q }". Indeed the latter works thanks to a
tolerance of Camlp5 in parsing "forall x, P" at level 200 while the
rule asks to actually parse the interior of "{ ... }" at level 99 (the
reason for 99 is to be below the rule for "M : T" which is at level
100, so that "{ x : A | P }" does not see "x : A" as a cast). Adding
an extra "'"; pat = pattern in parallel to c = constr LEVEL "99" broke
the tolerance for constr at level 200.
We fix this by adding an ad hoc rule for "{ binder_constr }" in the
native grammar (g_constr.ml4).
Actually, this is inconsistent with having a rule for "{ constr at level 99 }"
in Notations.v. We should have both rules in Notations.v or both rules
hard-wired in the native grammar. But I still don't know what is the best
decision to take, so leaving as it at the current time.
Advantages of hard-wiring both rules in g_constr.ml4: a bit simpler in
metasyntax.ml (no need to ensure that the rule exist). Disadvantages:
if one wants a different initial state without the business needing
the "{ }" for sumbool, sumor, sig, sigT, one still have the rules
there.
Advantages of having them in Notations.v: more modular, we can change
the initial state. Disadvantages: one would need a new kind of
modifier, something like "x at level 99 || binder_constr", with all
the difficulty to find a nice, intuitive, name for "binder_constr",
and the difficulty of understanding if there is a generality to this
"||" disjunction operator, and whether it should be documented or not.
|
