| Age | Commit message (Collapse) | Author |
|---|
|
one_inductive_body so that when eta-expanding at "match" printing time
we know if a let is part of the expected signature or part of the
body.
This is an easy fix for bugs like #3293. Another fix could be to
enforce, as an invariant, or better syntactically, that
"match"/"Case"'s have the body of their branches expanded.
|
|
|
|
|
|
|
|
|
|
There were actually two problems, one of them being clearly unsound.
To make sure that this does not show up somewhere else in the code, it would
be better to resort to an abstraction keeping in sync the environment and the
De Bruijn index of the current cofixpoints, like guard_env does for fixpoints.
|
|
|
|
|
|
applications of I31 constructor as lazy.
|
|
|
|
This completes the port of the native compiler to retroknowledge.
However, some testing and optimizations are still to be done.
|
|
|
|
|
|
dependencies.
|
|
|
|
|
|
Inside a section, Let followed by a Proof. Qed. are handled as regular
definitions, hence they have universe constraints coming from the type
and from the body. Only the former set was returned to libstack, but
both sets were added to the global universe graph. Hence, at section
closing time, an incomplete set of universe constraints was added back
to the global graph (End Section replays the libstack) and hence saved
in the .vo file. coqchk was right in reporting missing constraints.
|
|
when defining cache hash tables in Closure. Why it was working in 3.12
is a mystery to me.
|
|
|
|
transparent status of variables and constants.
|
|
no particular purpose.
|
|
Universes that are computed in the vi2vo step are not part of the
outermost module stocked in the vo file. They are part of the
Library.seg_univ segment and are hence added to the safe env when
the vo file is loaded.
The seg_univ has been augmented. It is now:
- an array of universe constraints, one for each constant whose opaque
body was computed in the vi2vo phase. This is useful only to print
the constants (and its associated constraints).
- a union of all the constraints that come from proofs generated in the
vi2vo phase. This is morally the missing bits in the toplevel module
body stocked in the vo file, and is there to ease the loading of
a .vo file (obtained from a .vi file).
- a boolean, false if the file is incomplete (.vi) and true if it is
complete (.vo obtained via vi2vo).
|
|
Universe constraints coming from subtyping were not propagated
to the outermost module and hence not stocked in the .vo file.
Still, they were added to the interactive safe environment and
hence checked for satisfiability.
|
|
|
|
|
|
|
|
iter order, but it seems nobody was relying on it (contrarily to the string case).
|
|
|
|
|
|
|
|
|
|
|
|
The removed code isn't used locally and isn't exported in the signature
|
|
With ocaml 4.01, the 'unused open' warning also checks the mli :-)
Beware: some open are reported as useless when compiling with camlp5,
but are necessary for compatibility with camlp4. These open are now
marked with a comment.
|
|
did not respect the requirement that equality should preserve hash.
|
|
|
|
|
|
duplicates in kernel side effects. They were chosen according to an equality
that was quite irrelevant, and as expected this patch did not break the
test-suite.
|
|
|
|
|
|
|
|
|
|
optimization purposes. I replaced their use with the under-approximation
of pointer equality.
|
|
This meas that the list of future_constraints in safe_env is empty,
meaning that nothing was delayed.
|
|
Make this module deal only with opaque proofs.
Make discharging/substitution invariant more explicit via a third constructor.
|
|
When you resume the compilation of a .vi file, you want to
avoid collisions on fresh names.
|
|
|
|
To obtain a.vo one can now:
1) coqtop -quick -compile a
2) coqtop -vi2vo a.vi
To make that possible the .vo structure has been complicated. It is now
made of 5 segments.
| vo | vi | vi2vo | contents
--------------+------+-----+-------+------------------------------------
lib | Yes | Yes | Yes | libstack (modules, notations,...)
opauqe_univs | No | Yes | Yes | constraints coming from opaque proofs
discharge | No | Yes | No | data needed to close sections
tasks | No | Yes | No | STM tasks to produce proof terms
opaque_proofs | Yes | Yes | Yes | proof terms
--------------+------+-----+-------+------------------------------------
This means one can load only the strictly necessay parts. Usually one
does not load the tasks segment of a .vi nor the opaque_proof segment of
a .vo, unless one is turning a .vi into a .vo, in which case he load
all the segments.
Optional segments are marshalled as None. But for lib, all segments
are Array.t of:
| type
--------------+---------------------------------------------------------
lib | a list of Libobject.obj (n'importe quoi)
opauqe_univs | Univ.consraints Future.computation
discharge | what Cooking.cook_constr needs
tasks | Stm.tasks (a task is system_state * vernacexpr list)
opaque_proofs | Term.constr Future.computation
--------------+------+-----+-------+------------------------------------
Invariant: all Future.computation in a vo file (obtained by a vi2vo
compilation or not) have been terminated with Future.join (or
Future.sink). This means they are values (inside a box).
This invariant does not hold for vi files. E.g. opauqe_proofs can be
dangling Future.computation (i.e. NotHere exception). The vi2vo
compilation step will replace them by true values.
Rationale for opaque_univs: in the vi2vo transformation we want to reuse
the lib segment. Hence the missing pieces have to be put on the side,
not inside. Opaque proof terms are already in a separte segment.
Universe constraints are not, hence the new opauqe_univs segment. Such
segment, if present in a .vo file, is always loaded, and
Declare.open_constant will add to the environment the constraints stored
there. For regular constants this is not necessay since the constraints
are already in their enclosing module (and also in the constant_body).
With vi2vo the constraints coming from the proof are not in the
constant_body (hence not in the enclosing module) but there and are
added to the environment explicitly by Declare.open_constant.
Rationale for discharge: vi2vo produces a proof term in its original
context (in the middle of a section). Then it has to discharge the
object. This segment contains the data that is needed in order to do
so. It is morally the input that Lib.close_section passes to Cooking
(via the insane rewinding of libstack, GlobalRecipe, etc chain).
Checksums: the checksum of .vi and a .vo obtain from it is the same.
This means that if if b.vo has been compiled using a.vi, and then
a.vi is compiled into a.vo, Require Import b works (and recursively
loads a.vo).
|
|
subst1 case.
|
|
|
