| Age | Commit message (Collapse) | Author |
|---|
|
|
|
csdp.cache -> .csdp.cache
lia.cache -> .lia.cache
nlia.cache -> .nia.cache
|
|
we use a hashtable to reduce the complexity of creating
a duplicate-free list.
|
|
the function in_ideal of ideal.ml supposes the list of polynomials
does not contain zero and is duplicate free.
I force this invariant in the call of in_ideal in nsatz.ml4
the function clean_pol returns the reduced list plus a list of
booleans that indicates which polynomials have been deleted
the function expand_pol translates back the certificate of
the reduced to list to the complete list thanks to the list
of booleans.
The fix is quadratic with respect to the input list which should
be ok for reasonable usage of nsatz.
If there is some performance issue we could improve the in_pol
function.
|
|
changing
set (x := val)
into
let x := fresh "x" in
set (x := val)
|
|
Because refreshing Prop is not semantics-preserving,
the new universe is >= Set, so cannot be minimized to Prop
afterwards.
|
|
This fixes the end of bug #4069, provoked by a use
of unshelve refine which introduces a cast.
|
|
In congruence, refresh universes including the Set/Prop ones so that
congruence works with cumulativity, not restricting itself to the
inferred types of terms that are manipulated but allowing them to be
used at more general types. This fixes bug #4609.
|
|
|
|
|
|
|
|
- In Program, a check_evars_are_solved was introduced
too early. Program does it's checking of evars by itself.
- In Function, the universe environments were not threaded
correctly.
|
|
Use the compatibility match construction to extract the compatibility
constant associated to a primitive projection.
|
|
Anomaly: Uncaught exception Unix.Unix_error(Unix.EACCES, "open", "lia.cache").
Please report.
|
|
|
|
The Haskell extraction code would allow line-wrapping of the Haskell
type definition, which would lead to unparseable Haskell code when the
linebreak occured just before the type name. In particular, with a term
name of 46 characters or more, the following Coq code:
Definition xxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxx := tt.
Extraction Language Haskell.
Extraction xxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxx.
would produce:
xxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxx ::
Unit
xxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxx =
Tt
which failed to compile with GHC (according to Haskell's indentation
rules, the "Unit" line must be indented to be treated as a continuation
of the previous line).
This patch always forces the type onto a separate line, and ensures that
it is always indented by 2 spaces (just like the body of each definition).
|
|
Note that extracting terms containing primitive projections is still
utterly broken, so don't use them.
|
|
|
|
The extraction of [Z] into Ocaml's [Big_int] passed arguments in the
wrong order to [Big.compare_case] for [Pos.compare_cont]. It seems
unlikely this ever worked before.
|
|
printer in the congruence tactic.
Debugging messages were always built even when not in the verbose mode
of congruence.
|
|
Fixes compilation of Coq with OCaml 4.03 beta 1.
|
|
|
|
|
|
The Map interface of upcoming OCaml 4.03 includes a new union operator. In
order to make our homemade implementation of Maps compatible with OCaml
versions from 3.12 to 4.03, we define our own signatures for Maps.
|
|
|
|
The previous behavior was to include the interface of such a functor,
possibly leading to the creation of unexpected axioms, see bug report #3746.
In the case of non-functor module with restricted signature, we could
simply refer to the original objects (strengthening), but for a functor,
the inner objects have no existence yet. As said in the new error message,
a simple workaround is hence to first instantiate the functor, then include
the local instance:
Module LocalInstance := Funct(Args).
Include LocalInstance.
By the way, the mod_type_alg field is now filled more systematically,
cf new comments in declarations.mli. This way, we could use it to know
whether a module had been given a restricted signature (via ":"). Earlier,
some mod_type_alg were None in situations not handled by the extraction
(MEapply of module type).
Some code refactoring on the fly.
|
|
On an application (f args) where the head is magic, we first remove Obj.magic
on arguments before continuing with simplifications (that may push magic down
inside the arguments).
For instance, starting with ((Obj.magic f) (Obj.magic (g h))), we now end
with ((Obj.magic f) (g h)) instead of ((Obj.magic f) ((Obj.magic g) h))) as
before.
|
|
Unfortunately, my first attempt at replacing (Obj.magic (fun x -> u) v)
by ((fun x -> Obj.magic u) v) was badly typed, as seen in FingerTree:
the argument v should also be magic now, otherwise it might not have
the same type as x.
This optimization is now correctly done, and to mitigate the potential inflation
of Obj.magic, I've added a few simplification rules to avoid redundant magics,
push them down inside terms, favor the form (Obj.magic f x y z), etc.
|
|
During an extraction, a few tables are maintained to cache
intermediate results. Due to modules, the kernel_name index
for these caching tables aren't enough. For instance, in
bug #3923, a constant is first transparent (from inside the
module) then opaque (when seen from the signature). The previous
protections were actually obsolete (tests via visible_con), we
now checks that the constant_body is still the same.
|
|
vars by _)
|
|
This is done via a unique pass which seems roughly linear in practice,
even on big developments like CompCert. There's a List.nth in an env at
each MLrel, that could be made logarithmic if necessary via Okasaki's
skew list for instance.
Another approach would be to keep names (as a form of documentation), but
prefix them by _ to please OCaml's warnings. For now, let's be radical and
use the _ pattern.
|
|
This fix only handles MLapp(MLmagic(MLlam...),...). Someday, we'll have
to properly investigate the interaction between all the other optimizations
and MLmagic. But well, at least this precise bug is fixed now.
|
|
In front of "let rec f x y = ... in f n m", if n is now an implicit argument,
then the argument x of the inner fixpoint f is also considered as implicit.
This optimization is rather ad-hoc, since we only handle MLapp(MLfix()) for
now, and the implicit argument should be reused verbatim as argument.
Note that it might happen that x cannot be implicit in f. But in this
case we would have add an error message about n still occurring somewhere...
At least this small heuristic was easy to add, and was sufficient to solve
the part 2 of bug #4243.
|
|
|
|
|
|
Some explicit '\n' in Pp.str were interacting badly with Format boxes
in Compcert, leading to right-flushed "sig..end" blocks in some .mli
|
|
|
|
Instead of the original hacks (embedding implicits in string msg in MLexn !)
we now use a proper construction MLdummy (Kimplicit (r,i)) to replace the use
of the i-th argument of constant or constructor r when this argument has been
declared as implicit.
A new option Set/Unset Extraction SafeImplicits controls what happens
when some implicits still occur after an extraction : fail in safe mode,
or otherwise produce some code nonetheless. This code is probably buggish
if the implicits are actually used to do anything relevant (match, function
call, etc), but it might also be fine if the implicits are just passed along.
And anyway, this unsafe mode could help figure what's going on.
Note: the MLdummy now expected a kill_reason, just as Tdummy.
These kill_reason are now Ktype, Kprop (formerly Kother) and Kimplicit.
Some minor refactoring on the fly.
|
|
|
|
The ind_equiv field wasn't correctly set, due to some kernel names
glitches (canonical vs. user). The fix is to take into account the
delta_resolver while traversing module structures.
|
|
|
|
|
|
constr, and the associated signature, not needed anymore.
Update CHANGES, no evar_map is produced by pattern_of_constr anymore.
|
|
pattern-matching on function calls.
|
|
for reporting it.
A "cut" was not appropriately chained on the second goal but on both
goals, with the chaining on the first goal introducing noise.
|
|
Keep user-side information on the names used in instances of universe
polymorphic references and use them for printing.
|
|
Side effects are now an opaque data type, called private_constant, you can
only obtain from safe_typing. When add_constant is called on a
definition_entry that contains private constants, they are either
- inlined in the main proof term but not re-checked
- declared globally without re-checking them
As a safety measure, the opaque data type contains a pointer to the
revstruct (an internal field of safe_env that changes every time a new
constant is added), and such pointer is compared with the current value
store in safe_env when the private_constant is inlined. Only when the
comparison is successful the private_constant is not re-checked. Otherwise
else it is. In short, we accept into the kernel private constant only
when they arrive in the very same order and on top of the very same env
they arrived when we fist checked them.
Note: private_constants produced by workers never pass the safety
measure (the revstruct pointer is an Ephemeron). Sending back the
entire revstruct is possible but: 1. we lack a way to quickly compare
two revstructs, 2. it can be large.
|
|
|
|
Since the functions of this plugin exit by raising exceptions, globing
was never restarted. This prevented coqdoc from generating a proper
output whenever some feature of this plugin was used. There does not seem
to be any parsing of dynamic expressions, so pausing globing does not make
much sense in the first place.
|
|
|
