| Commit message (Collapse) | Author | Age |
... | |
|
|
|
| |
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).
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
| |
File format:
The .vo file format changed:
- after the magic number there are 3 segments. A segment is made of 3
components: bynary int, an ocaml value, a digest. The binary int
is the position of the digest, so that one can skip the value without
unmarshalling it
- the first segment is the library, as before
- the second segment is the STM task list
- the third segment is the opaque table, as before
A .vo file has a complete opaque table (all proof terms are there).
A .vi file follows the same format of a .vo file, but some entries
in the opaque table are missing. A proof task is stocked instead.
Utilities:
coqc: option -quick generates a .vi insted of a .vo
coq_makefile: target quick to generate all .vi
coqdep: generate deps for .vi files too
votour: can browse .vi files too, the first question is which segment
should be read
coqchk: rejects .vi files
|
|
|
|
|
|
| |
But for vm, the kernel should be functional now
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16961 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
| |
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
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
| |
- No more modinfo sub-record in the safe_environment record,
this was a syntactic pain.
senv.modinfo.modpath --> senv.modpath
senv.modinfo.variant --> senv.modvariant
senv.modinfo.resolver --> senv.modresolver
senv.modinfo.resolver_of_param --> senv.paramresolver
senv.modinfo.label : removed (can be inferred from modpath)
- No more systematic chaining of safe_environment ('old' field).
Instead, earlier safe_environment is stored in the modvariant field
when necessary (STRUCT and SIG case).
- Improved sharing between end_module and end_modtype
- More qualified names instead of open, better comments, ...
- Some user errors are now checked earlier elsewhere (see for
instance vernac_end_segment), so we can turn these errors into
asserts. The user error about higher-order include is now algebraic.
- Highlight the idea of a state monad in Safe_typing :
type 'a safe_transformer = safe_environment -> 'a * safe_environment
More systematic code in Global, thanks to 'globalize' function.
- Declaremods : less informations stored in openmod_info
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16708 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
|
|
|
|
|
|
|
| |
It can be:
`Yes Full data, in a state that can be marshalled
`No Full data, good for Undo only
`Shallow Partial data, marshallable, good for slave processes
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16682 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
|
|
| |
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16679 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
| |
The process_transaction function adds a new edge to the Dag without
executing the transaction (when possible).
The observe id function runs the transactions necessary to reach to the
state id. Transaction being on a merged branch are not executed but
stored into a future.
The finish function calls observe on the tip of the current branch.
Imperative modifications to the environment made by some tactics are
now explicitly declared by the tactic and modeled as let-in/beta-redexes
at the root of the proof term. An example is the abstract tactic.
This is the work described in the Coq Workshop 2012 paper.
Coq is compile with thread support from now on.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16674 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
|
|
|
|
|
|
|
|
| |
the VM
too. Almost only a new grammar entry since the inlining machinery was already
implemented.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16623 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
| |
- Most of the time, the table registered via Summary.declare_summary
is just a single reference. A new function Summary.ref now allows
to both declare this ref and register it to summary in one shot.
- Clarifications concerning the role of [init_function].
For statically registered tables that don't need a special initializer,
just do nothing there (see the new Summary.nop function).
Beware: now that Summary exports a function named "ref", any code that
do an "open Summary" will probably fail to compile.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16441 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
|
|
|
|
|
|
| |
- get_module_substobjs (resp. modtype) without useless mp_from arg
- no need for the whole Safe_typing.pack_module
- ...
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16407 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
|
|
|
|
|
|
|
| |
* Remove the mind_of_delta and constant_of_delta functions,
prefer instead the {mind,constant}_of_delta_kn functions.
* Attempt to make subst_ind and subst_con0 more self-contained
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16247 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
|
|
|
|
|
|
|
|
|
|
|
| |
native OCaml code.
Warning: the "retroknowledge" mechanism has not been ported to the native
compiler, because integers and persistent arrays will ultimately be defined as
primitive constructions. Until then, computation on numbers may be faster using
the VM, since it takes advantage of machine integers.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16136 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
|
|
| |
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16097 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
|
|
| |
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15844 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
|
|
|
|
| |
Util module.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15802 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
|
|
|
|
|
|
|
|
| |
compiler warnings).
I was afraid that such a brutal refactoring breaks some obscure
invariant about linking order and side-effects but the standard
library still compiles.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15800 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
|
|
| |
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15715 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
|
|
|
|
| |
grammar.cma
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15384 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
|
|
|
|
|
|
|
|
|
|
|
|
| |
We now accept the following code: Definition E := 0. Module E. End E.
Techically, we simply allow the same label to occur at most twice in
a structure_body, which is a (label * structure_field_body) list).
These two label occurences should not be at the same level of fields
(e.g. a SFBmodule and a SFBmind are ok, but not two SFBmodule's or
a SFBmodule and a SFBmodtype). Gain : a minimal amount of code change.
Drawback : no more simple List.assoc or equivalent should be performed
on a structure_body ...
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15088 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
|
|
|
|
|
|
|
|
|
| |
Util only depends on Ocaml stdlib and Utf8 tables.
Generic pretty printing and loc functions are in Pp.
Generic errors are in Errors.
+ Training white-spaces, useless open, prlist copies random erasure.
Too many "open Errors" on the contrary.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15020 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
|
|
|
|
|
|
|
|
| |
Most of the time, a constant name is built from:
- a kernel_name for its user part
- a delta_resolver applied to this kernel_name for its canonical part
With this patch we avoid building unnecessary constants for immediately
amending them (cf in particular the awkward code removed in safe_typing).
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14545 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
|
|
|
|
|
|
|
|
| |
Maybe could we keep only the kernel check, but message would
certainly need to be reformulated then.
For instance, the message was previously different for an attempt to
redefine a name whether this name was in the same section or not.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14528 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
|
|
| |
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13323 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
|
|
|
|
|
|
|
|
|
| |
- Many of them were broken, some of them after Pierre B's rework
of mli for ocamldoc, but not only (many bad annotation, many files
with no svn property about Id, etc)
- Useless for those of us that work with git-svn (and a fortiori
in a forthcoming git-only setting)
- Even in svn, they seem to be of little interest
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12972 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
|
|
|
|
|
|
| |
For F(X:T), the application !F M works as F M, except that if module type T
contains some "Inline" annotations, they are not taken in account when substituting
X with M in F. See forthcoming commits for examples of use for this feature.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12678 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
| |
If you have some Module Type F (X:Sig), and you are in a Module Type
containing everything required to satisfy Sig (typically thanks to
some earlier Include), then you can say Include Self Type F, and voila,
objects of F are now added in your context, instantiated by local objects.
Same behavior (hopefully) for modules and functors when using Include Self F.
This experimental new command allows to easily produce static signatures
out of functorial ones:
Module Type F_static. Include Sig. Include Self F. End F_static.
... is similar to ...
Module Type F_static. Declare Module X:Sig. Include F X. End F_static.
... but without the pollution of this artificial inner module X.
This allow to split things in many othogonal components, and then mix them.
It is a lightweight way to tackle the "diamond problem" of modular
developpements without things like "overlapping" Include's (planned, but
not yet there). See next commit for an example of use.
Thanks to Elie for the debugging of my first ugly prototype...
NB: According to Yann R.G., this is related with Scala's Traits.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12528 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
| |
1- Management of the name-space in a modular development / sharing of non-logical objects.
2- Performance of atomic module operations (adding a module to the environment, subtyping ...).
1-
There are 3 module constructions which derive equalities on fields from a module to another:
Let P be a module path and foo a field of P
Module M := P.
Module M.
Include P.
...
End M.
Declare Module K : S with Module M := P.
In this 3 cases we don't want to be bothered by the duplication of names.
Of course, M.foo delta reduce to P.foo but many non-logical features of coq
do not work modulo conversion (they use eq_constr or constr_pat object).
To engender a transparent name-space (ie using P.foo or M.foo is the same thing)
we quotient the name-space by the equivalence relation on names induced by the
3 constructions above.
To implement this, the types constant and mutual_inductive are now couples of
kernel_names. The first projection correspond to the name used by the user and the second
projection to the canonical name, for example the internal name of M.foo is
(M.foo,P.foo).
So:
*************************************************************************************
* Use the eq_(con,mind,constructor,gr,egr...) function and not = on names values *
*************************************************************************************
Map and Set indexed on names are ordered on user name for the kernel side
and on canonical name outside. Thus we have sharing of notation, hints... for free
(also for a posteriori declaration of them, ex: a notation on M.foo will be
avaible on P.foo). If you want to use this, use the appropriate compare function
defined in name.ml or libnames.ml.
2-
No more time explosion (i hoppe) when using modules i have re-implemented atomic
module operations so that they are all linear in the size of the module. We also
have no more unique identifier (internal module names) for modules, it is now based
on a section_path like mechanism => we have less substitutions to perform at require,
module closing and subtyping but we pre-compute more information hence if we instanciate
several functors then we have bigger vo.
Last thing, the checker will not work well on vo(s) that contains one of the 3 constructions
above, i will work on it soon...
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12406 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
|
|
| |
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12337 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
|
|
|
|
|
|
|
|
| |
only used to allow a module to be ended before the summaries were
restored what can be solved by moving upwards the place where the
summaries are restored).
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12275 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
|
|
| |
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10664 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
| |
kernel:
-declaration.ml
unification des representations pour les modules et modules types.
(type struct_expr_body)
-mod_typing.ml
le typage des modules est separe de l'evaluation des modules
-modops.ml
nouvelle fonction qui pour toutes expressions de structure calcule
sa forme evaluee.(eval_struct)
-safe_typing.ml
ajout du support du nouvel operateur Include.(add_include).
library:
-declaremods.ml
nouveaux objets Include et Module-alias et gestion de la resolution de noms pour
les alias via la nametab.
parsing:
-g_vernac.ml4:
nouvelles regles pour le support des Includes et pour l'application des signatures
fonctorielles.
extraction:
Adaptation a la nouvelle representation des modules et support de l'operateur with.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10497 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
|
|
|
|
|
|
|
| |
details).
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9821 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
|
|
|
|
|
|
|
|
| |
(suppression au passage d'un cast dans constant_entry_of_com - ce
n'est pas normal qu'on force le type s'il n'est pas déjà présent mais
en même temps il semble que ce cast serve pour rafraîchir les univers
algébriques...)
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9310 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
|
|
|
|
|
|
|
|
|
| |
foncteurs sont données un par un ce qui permet de faire les
load_objects correspondants au bon moment (càd juste après l'ajout des
déclarations logiques et avant l'ajout du paramètre suivant). Ceci
clôt le bug #1118 et corrige des erreurs de localisation introduite
par le commit précédent.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8723 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
| |
à la déclaration des paramètres de foncteurs (problème de
synchronisation révélé par bug #1118, apparu suite à l'appel de
lookup_mind par load_struct, suite au passage à un discharge local)
Les objets non logiques sont maintenant chargés après car ils peuvent
dépendre d'objets logiques. Et comme les objets non logiques
(p.ex. l'import récursif de modules dans la nametab) sont nécessaires
au typage de l'éventuelle contrainte de module, on reporte la gestion
de la contrainte au moment du end_module (on aurait peut-être pu faire
plus fin et extraire dans do_module la partie purement module, mais
après tout le report de la contrainte de type dans le end_module ne
semble pas génante).
À la date d'aujourd'hui, le bug #1118 reste toutefois ouvert avec les
définitions de module non interactives.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8721 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
|
|
|
|
|
|
| |
Ajout de cast indiquant au kernel la strategie a suivre
Resolution du bug sur les coinductifs
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@7639 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
|
|
| |
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@7602 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
|
|
|
|
|
|
|
| |
to accept a mind_specif (a couple mutual_inductive_body * one_inductive_body)
instead of looking it up in the environment. A version of the same functions
with the old type is put in Inductiveops (outside the kernel).
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6589 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
|
|
| |
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6305 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
|
|
| |
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5920 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
|
|
| |
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4727 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
|
|
| |
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4534 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
|
|
|
|
| |
noms uniques
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3405 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
|
|
| |
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2957 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
|
|
|
|
|
| |
meilleure discrimination dans les tactiques d'inversion
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2491 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
|
|
| |
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2211 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
|
|
| |
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2178 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
|
|
|
|
|
|
|
|
| |
- reduction du noyau (variables existentielles, fonctions auxiliaires
pour inventer des noms, etc. deplacees hors de kernel/)
- changement de noms de constructeurs des constr (suppression de "Is" et
"Mut")
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2158 85f007b7-540e-0410-9357-904b9bb8a0f7
|