| Age | Commit message (Collapse) | Author |
|---|
|
|
|
|
|
|
|
letting make validate progress.
|
|
|
|
After this commit, module_type_body is a particular case of module_type.
For a [module_type_body], the implementation field [mod_expr] is
supposed to be always [Abstract]. This is verified by coqchk, even
if this isn't so crucial, since [mod_expr] is never read in the case
of a module type.
Concretely, this amounts to the following rewrite on field names
for module_type_body:
- typ_expr --> mod_type
- typ_expr_alg --> mod_type_alg
- typ_* --> mod_*
and adding two new fields to mtb:
- mod_expr (always containing Abstract)
- mod_retroknowledge (always containing [])
This refactoring should be completely transparent for the user.
Pros: code sharing, for instance subst_modtype = subst_module.
Cons: a runtime invariant (mod_expr = Abstract) which isn't
enforced by typing. I tried a polymorphic typing of mod_expr,
to share field names while not having mtb = mb, but the OCaml
typechecker isn't clever enough with polymorphic mutual fixpoints,
and reject code sharing (e.g. between subst_modtype and subst_module).
In the future (with ocaml>=4), some GADT could maybe help here,
but for now the current solution seems good enough.
|
|
|
|
|
|
|
|
|
|
|
|
constraints only.
|
|
|
|
|
|
did not notice that kernel/values.ml had to be made consistent with
kernel/cic.mli).
|
|
Some wrong generic equalities and hashes were removed too.
|
|
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).
|
|
|
|
|
|
discrepancy introduced in commit d3eac3d5fc8e5af499eb8750ca08ead8562dac6f
|
|
A future always carries a fix_exn with it: a function that enriches
an exception with the state in which the error occurs and also a safe
state close to it where one could backtrack.
A future can be in two states: Ongoing or Finished.
The latter state is obtained by Future.join and after that the future
can be safely marshalled.
An Ongoing future can be marshalled, but its value is lost. This makes
it possible to send the environment to a slave process without
pre-processing it to drop all unfinished proofs (they are dropped
automatically in some sense).
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16892 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
removing an unneeded indirection.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16781 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
TODO: register the desired dynamic types.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16733 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
Since digests are strings (of size 16), we just dump them
now in vo files (cf. Digest.output) instead of using Marshal
on them : this is cleaner and saves a few bytes.
Increased VOMAGIC to clearly identify this change in the format.
Please rerun ./configure after this commit.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16722 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
The earlier type [struct_expr_body] was far too broad,
leading to code with unclear invariants, many "assert false", etc etc.
Its replacement [module_alg_expr] has only three constructors:
* MEident
* MEapply : note the module_path as 2nd arg, no more constraints here
* MEwith : no more constant_body inside, constr is just fine
But no more SEBfunctor or SEBstruct constructor here (see below).
This way, this datatype corresponds to algebraic expressions,
i.e. anything that can appear in non-interactive modules.
In fact, it even coincides now with [Entries.module_struct_entry].
- Functor constructors are now necessarily on top of other
structures thanks to a generic [functorize] datatype.
- Structures are now separated from algebraic expressions by design :
the [mod_type] and [typ_expr] fields now only contain structures
(or functorized structures), while [mod_type_alg] and [typ_expr_alg]
are restricted to algebraic expressions only.
- Only the implementation field [mod_expr] could be either algebraic
or structural. We handle this via a specialized datatype
[module_implementation] with four constructors:
* Abstract : no implementation (cf. for instance Declare Module)
* Algebraic(_) : for non-interactive modules, e.g. Module M := N.
* Struct(_) : for interactive module, e.g. Module M : T. ... End M.
* FullStruct : for interactive module with no type restriction.
The [FullStruct] is a particular case of [Struct] where the implementation
need not be stored at all, since it is exactly equal to its expanded
type present in [mod_type]. This is less fragile than hoping as earlier
that pointer equality between [mod_type] and [mod_expr] will be
preserved...
- We clearly emphasize that only [mod_type] and [typ_expr] are
relevant for the kernel, while [mod_type_alg] and [typ_expr_alg]
are there only for a nicer extraction and shorter module printing.
[mod_expr] is also not accessed by the kernel, but it is important
for Print Assumptions later.
- A few implicit invariants remain, for instance "no MEwith in mod_expr",
see the final comment in Declarations
- Heavy refactoring of module-related files : modops, mod_typing,
safe_typing, declaremods, extraction/extract_env.ml ...
- Coqchk has been adapted accordingly. The code concerning MEwith
in Mod_checking is now gone, since we cannot have any in mod_expr.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16712 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16706 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
still not working, it complains about the universe constraint
set...
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16691 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16690 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
When refering to a module / module type, or when doing an include,
we do not duplicate and substitution original libobjects immediatly.
Instead, we store the module path, plus a substitution. The libobjects
are retrieved later from this module path and substituted, typically
during a Require. This allows to vastly decrease vo size (up to 50%
on some files in the stdlib). More work is done during load (some
substitutions), but the extra time overhead appears to be negligible.
Beware: all subst_function operations should now be
environment-insensitive, since they may be arbitrarily delayed.
Apparently only subst_arguments_scope had to be adapted.
A few more remarks:
- Increased code factorisation between modules and modtypes
- Many errors and anomaly are now assert
- One hack : brutal access of inner parts of module types
(cf handle_missing_substobjs)
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16630 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16405 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16404 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16402 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16400 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16399 85f007b7-540e-0410-9357-904b9bb8a0f7
|
