| Age | Commit message (Collapse) | Author |
|---|
|
|
|
|
|
Previously real constants were parsed by an unproved OCaml code. The
parser and printer are now implemented in Coq, which will enable a
proof and hopefully make it easier to maintain / make evolve.
Previously reals were all parsed as an integer, an integer multiplied
by a power of ten or an integer divided by a power of ten. This means
1.02 and 102e-2 were both parsed as 102 / 100 and could not be tell
apart when printing. So the printer had to choose between two
representations : without exponent or without decimal dot. The choice
was made heuristically toward a most compact representation.
Now, decimal dot is parsed as a rational and exponents are parsed as a
product or division by a power of ten. For instance, 1.02 is parsed as
Q2R (102 # 100) whereas 102e-2 is parsed as IZR 102 / IZR (Z.pow_pos
10 2).
1.02 and 102e-2 remain equal (proved by reflexivity) but 1.02e1 = Q2R
(102 # 100) * 10 and 10.2 = Q2R (102 # 10) no longer are.
|
|
|
|
|
|
Previously rationals were all parsed as a pair numerator, denominator.
This means 1.02 and 102e-2 were both parsed as 102 # 100 and could not
be tell apart when printing. So the printer had to choose between two
representations : without exponent or without decimal dot. The choice
was made heuristically toward a most compact representation.
Now, decimal dot is still parsed as a power of ten denominator but
exponents are parsed as a product or division by Z.pow_pos. For
instance, 1.02 is parsed as 102 # 100 whereas 102e-2 is parsed as
(102 # 1) / (Z.pow_pos 10 2 # 1).
1.02 and 102e-2 remain equal (proved by reflexivity) but 1.02e1
= (102 # 100) * (10 # 1) = 1020 # 100 and 10.2 = 102 # 10 no longer are.
A nice side effect is that exponents can no longer blow up during
parsing. Previously 1e1_000_000 literally produced a numerator with a
million digits, now it just yields (1 # 1) * (Z.pow_pos 10 1_000_000 # 1).
|
|
Just to get a cleaner log, this will be proved again in a few commits.
|
|
|
|
|
|
This enables numeral notations for non inductive types by
pre/postprocessing them to a given proxy inductive type.
For instance, this should enable the use of numeral notations for R.
|
|
This will enable to define numeral notation on non inductive by using
an inductive type as proxy and those translations to translate to/from
the actual type to the inductive type.
|
|
|
|
This is a generated file since #13147
|
|
|
|
|
|
|
|
Reviewed-by: gares
Reviewed-by: herbelin
Ack-by: ppedrot
|
|
grammars more consistent
Reviewed-by: Zimmi48
Reviewed-by: herbelin
Ack-by: SkySkimmer
|
|
Reviewed-by: gares
|
|
|
|
typ_param -> ltac2_typevar,
tac2expr -> ltac2_expr
|
|
|
|
|
|
|
|
Reviewed-by: SkySkimmer
Ack-by: gares
Ack-by: ejgallego
|
|
Reviewed-by: ejgallego
Reviewed-by: gares
Reviewed-by: ppedrot
|
|
Reviewed-by: vbgl
|
|
pattern-matching clause with unused named variable
Reviewed-by: jfehrle
Reviewed-by: vbgl
Ack-by: gares
|
|
|
|
Using it feels nicer this way, with GADT details hidden inside comtactic
|
|
Reviewed-by: Zimmi48
Reviewed-by: Blaisorblade
|
|
functions
Reviewed-by: SkySkimmer
|
|
|
|
Reviewed-by: herbelin
|
|
Reviewed-by: Zimmi48
Ack-by: mattam82
Ack-by: pi8027
Ack-by: herbelin
Ack-by: gares
Ack-by: fajb
Ack-by: proux01
|
|
|
|
Reviewed-by: Zimmi48
Reviewed-by: jfehrle
|
|
The cast keywords are <: and <<:, not :>/:>>
:>> stopped being a keyword in #13106
|
|
Reviewed-by: Zimmi48
|
|
We move quite a few obligation functions from a `let rec ... and`
block, as they are not mutually recursive.
By the way, we perform some refactoring on `solve_by_tac`, which is
quite messy still, but now the code flow could actually accommodate
passing a declaration entry instead of low-level objects.
[It seems that we will need to introduce a special obligation entry
for that purpose, but thankfully it will be internal. We are actually
pretty close on being able to remove `build_by_tactic`, which we
should do ASAP due to its current semantics breaking abstraction
barriers]
|
|
Git wants an identity and none is setup on the CI.
|
|
Fixup #13050.
|
|
Reviewed-by: Zimmi48
|
|
Always generate prodn* files if edits succeed
|
|
Reviewed-by: jfehrle
|
|
|
|
Reviewed-by: ppedrot
|
|
Reviewed-by: vbgl
|
|
This allows native_compute to work and is the same fix that was
applied to the nixpkgs repo in NixOS/nixpkgs#101058.
|
|
lambda
Reviewed-by: ppedrot
|
