| Age | Commit message (Collapse) | Author |
|---|
|
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16662 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16659 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
1. sorts.ml: A small file utility for sorts;
2. constr.ml: Really low-level terms, essentially kind_of_constr, smart
constructor and basic operators;
3. vars.ml: Everything related to term variables, that is, occurences
and substitution;
4. context.ml: Rel/Named context and all that;
5. term.ml: derived utility operations on terms; also includes constr.ml
up to some renaming, and acts as a compatibility layer, to be deprecated.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16462 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16351 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
- constr_substituted and lazy_constr are now in a dedicated kernel/lazyconstr.ml
- the functions that were in declarations.ml (mostly substitution utilities
and hashcons) are now in kernel/declareops.ml
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16250 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
Ok, this is merely a matter of taste, but up to now the usage
in Coq is rather to use capital letters instead of _ in the
names of inner modules.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16221 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16165 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@16072 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16071 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16007 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16006 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15992 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
the new Int module. Only the most obvious were removed, so there
are a lot more in the wild.
This may sound heavyweight, but it has two advantages:
1. Monomorphization is explicit, hence we do not miss particular
optimizations of equality when doing it carelessly with the generic
equality.
2. When we have removed all the generic equalities on integers, we
will be able to write something like "let (=) = ()" to retrieve all
its other uses (mostly faulty) spread throughout the code, statically.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15957 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15835 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15804 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
List module. That way, an "open Util" in the header permits using
any function of CList in the List namespace (and in particular, this
permits optimized reimplementations of the List functions, as, for
example, tail-rec implementations.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15801 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
|
|
Same for check_leq instead of check_geq
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15081 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
|
|
If two distinct parameters of the inductive type contributes to
polymorphism, they must have distinct names, othewise an aliasing
problem of the form "fun x x => max(x,x)" happens.
Also insisted that a parameter contributes to universe polymorphism
only if the corresponding occurrence of Type is not hidden behind a
definition.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14511 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14315 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
No need to tell the world about the fact that constraints are
implemented via caml's Set. Other modules just need to know about
the empty and union functions (and addition functions "enforce_geq"
and "enforce_eq" that were already there).
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13725 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
The lambda_implicit series of functions are used only in Indtypes, so
we move them there. In the checker, they are already there...
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13615 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
In particular, the unused lib/tlm.ml and lib/gset.ml are removed
In addition, to simplify code, Libobject.record_object returning only the
('a->obj) function, which is enough almost all the time.
Use Libobject.record_object_full if you really need also the (obj->'a).
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13460 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13323 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
types were seen as real constructor arguments...
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13290 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
In "(match ... with |... -> fun x -> t end) u", "x" has now the subterm
property of "u" in the analysis of "t".
Commutative cuts aren't compatible with typing so we need to ensure that
term of "x"'s type and term of "u"'s have the same subterm_spec.
Consequently,declaration.MRec argument has changed to the inductive name
instead of only the number of the inductive in the mutual_inductive
family.
In subterm_specif and check_rec_call, arguments are stored in a stack.
At each lambda, one element is popped to add in renv a smarter
subterm_spec for the variable. subterm_spec of constructor's argument
was added this way, the job is now done more often.
Some eta contracted match branches are now accepted but enforcing
eta-expansion of branches might be anyway a recommended invariant.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13012 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12974 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
|
|
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12616 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
|
|
very useful in practice but as soon as let-in's were not forbidden in
the internal data structure, better to do it. Moreover, this gets
closer to the view were inductive definitions are uniformly built from
"contexts". (checker not changed!)
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12273 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
- Added dependency of mltop.ml4 into config/Makefile (see bug #2023).
- Fixed bug #1963 (dependent inversion building a universe-ill-formed
conversion problem).
- Incidentally, moved "Large non-propositional inductive ..." error
message to standard himsg.ml error displayer.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11774 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
splay_prod_n, lam_it -> it_mkLambda, splay_lambda -> splay_lam). Added
shortcuts for "fst (decompose_prod t)" and co.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11727 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11349 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
contraintes bornant par le haut le type de l'inductif (ce qui peut
arriver quand l'inductif est argument d'une constante) étaient
oubliées : on pouvait se retrouver avec des inductifs dont le type des
constructeurs, une fois instancié par des paramètres) n'était plus
typable (seul leur réduit, après expansion des constantes, était
typable). [kernel, test-suite]
+ Affichage des inductifs (via Print) en prenant la forme utilisateur des
constructeurs.
+ Correction warning dans compilation gallina.ml.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11266 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
opportunity to extend the class of singleton types to (possibly mutual)
recursive types with single constructors of which all arguments are in
Prop. This covers Acc. Acc_rect can consequently be defined in the
direct way.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11249 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
majuscule - si pas un ident ou un terme - et se terminent par un point).
Restent quelques utilisations de "error" qui sont liées à des usages internes,
ne faudrait-il pas utiliser des exceptions plus spécifiques à la place ?
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11230 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
univers, suite à discussion avec Bruno : on franchit le cap et on
ajoute le sous-typage Prop <= Set. On n'a donc plus besoin d'utiliser
l'image de Prop dans la hiérarchie en dehors de la zone de calcul de
la sorte la plus basse d'un inductif polymorphe (au passage, nous
avons décidé de renommer Type -1 en Type 0-, pour bien indiquer qu'il
se trouve au même niveau que Type 0).
Coq se retrouve donc avec la hiérarchie Prop <= Set <= Type i et avec
une copie de Prop (Type 0-) et une copie de Set (Type 0) dans la
hiérarchie Type. En théorie, on pourrait donc supprimer "Prop Null" et
"Prop Pos" de l'implémentation et ne travailler qu'avec "Type".
L'ajout de Prop <= Set vaut à la fois dans le cas Set prédicatif et
dans le cas Set imprédicatif (Prop et Set étant en bas de la
hiérarchie, il n'y a pas d'incohérence connue). Dans le modéle
ensembliste, Prop et Type 0- sont interprétés par exemple comme
{{},{o}}, où "o" est un objet particulier interprétant les preuves, et
il n'y a pas de Set imprédicatif. Dans un modèle de réalisabilité,
Set imprédicatif est interprétable et Prop peut au choix s'interpréter
comme Set ou comme booléen (cf la thèse de Miquel). Le sous-typage du
côté ensembliste s'obtient en mettant au moins l'ensemble {{},{o}}
dans l'interprétation de Set (ce qu'on fait de la même manière que
Prop <= Type 1, avec conversion typée), et du côté réalisabilité en
mettant l'ensemble {Typ(vide),Typ(unit)} dans l'interprétation de Set
("Typ" étant la coercion faisant d'un ensemble un terme), ce qui est
fait dans la section 6.2.4 de la thèse d'Alexandre Miquel (modèle du
CC implicite sans types inductifs).
Il reste un problème pratique. Lorsqu'on donne
Inductive unit:Type := tt:unit.
Coq dit que unit est dans Prop. C'est correct parce qu'il n'y a pas de
contraintes d'univers mais un peu déroutant même si la coercion
"unit : Set" reste valide. Une suggestion est de ne rendre polymorphe
que les inductifs dont on ne donne pas la sorte explicitement, comme dans
Inductive unit := tt:unit.
mais alors, comment indiquer l'absence de sorte explicite si le type a
des paramètres réels (comme "vect") ??
PS: modification de sort_cmp dans checker/inductive.ml faite.
--This line, and those below, will be ignored--
M kernel/univ.ml
M kernel/univ.mli
M kernel/inductive.ml
M kernel/reduction.ml
M kernel/indtypes.ml
M checker/inductive.ml
M checker/reduction.ml
M pretyping/reductionops.ml
M pretyping/termops.ml
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10920 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
(i.e. "Inductive unit := tt." conduisait à "t:Prop" alors que le
principe de la hiérarchie d'univers est d'être cumulative -- et que
Set en soit le niveau 0).
Une solution aurait été de poser Prop <= Set mais on adopte une autre
solution. Pour éviter le côté contre-intuitif d'avoir unit dans Type
et Prop <= Set, on garde la représentation de Prop au sein de la
hiérarchie prédicative sous la forme "Type (max ([],[])" (le niveau
sans aucune contrainte inférieure, appelons Type -1) et on adapte les
fonctions de sous-typage et de typage pour qu'elle prenne en compte la
règle Type -1 <= Prop (cf reduction.ml, reductionops.ml, et effets
incidents dans Termops.refresh_universes et Univ.super).
Petite uniformisation des noms d'univers et de sortes au passage
(univ.ml, univ.mli, term.ml, term.mli et les autres fichiers).
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10859 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
conclusion) and improved error message when the conclusion of the type
of a constructor is invalid.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10425 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10296 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9831 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
l'élimination vers Set était autorisée: comme souligné par Benjamin,
c'est incompatible avec EM + AC (report rev 9633 8.1)
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9634 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
uniformes dans le cas de types mutuellement inductifs)
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9445 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
|
