| Age | Commit message (Collapse) | Author |
|---|
|
devient Flags.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10348 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
extraction is given the name of a .v Module.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10245 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
Initial Idea: getting rid of nasty renaming issues in modules, in
particular bugs #820 (part d) #1340 #1526 #1654
Final effect: lots of changes, simplifications, cleanups, unrelated
fixes and ehancements, and also probably some regressions (time will
tell).
A few details:
* no more experimental "Toplevel" language.
* no more functors Make in Ocaml/Haskell/Scheme. The spirit of these
functors and Mlpp_params was already not followed much, and this
framework was more a nuisance that anything else.
* instead, some records language_descr regrouping the specific
features of the different output languages.
* Common now comes before Ocaml/Haskell/Scheme, these ones are now
independant from each others. print_structure_to_file is now
in Extract_env.
* A nice detail: no more duplications of warnings concerning axioms.
* In modular extraction, the clashes due to the opened modules
are now computed once and for all thanks to record_contents_fstlev,
instead of re-asking Coq each time about these opened modules and
using Extraction.constant_kind
* some utilities about modules_path added and/or moved from Modutil
to Table.
* using a .v file as a module, e.g. in a functor application should
now works in modular extraction.
Now concerning renaming issues themselves:
* printing is done twice, the first time toward /dev/null, in order
to encounter the naming issues unsolvable by a simple qualification.
On the second run, we create artificial modules Coq__123 for
allowing qualification of these hidden objects.
* names are now fully separated into their syntaxic categories:
terms/types/constructors/modules
* Only one last unsupported situation (but at least detected and
signaled by an error): an object M.t from an external file-module
M.v can't be printed when a local module M is in the way.
This situation is really unlikely (in Coq you must use _long_
file-module name, e.g. Init.Datatypes.nat). It could be solved
by inserting "module Coq_123 = M" at the beginning of the file,
but then the signature of Coq_123 (that is, the one of M) should
be written explicitely in the .mli, which is _really_ not nice.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10232 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
If a library is Require'd from inside an "opaque" Module (e.g. a module with
an interface given by a ":"), then the required library is not loaded anymore
after closing this module. We add an error in this situation, asking the user
to manually do a Require before performing the Extraction.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10208 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10206 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
It even seems to work from inside a functor. Fix old bug #472.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10204 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
It is critical to avoid duplicated calls to extract_ind (see e.g.
example in #1709). But the same kernel_name can lead to different
inductive bodies, due to module substitutions. So we used to
factorize only "visible" kn, that were not subject to change under
substitution. As shown by P. Cregut in #1709, this is not enough.
New approach is now to store also Coq inductive data (mib). If the
recorded mib matches the current one, we trust the recorded result,
otherwise we start a fresh computation of extract_ind.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10194 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
|
|
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9205 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
1. when applying a functor F(X) := B to a module M, the obtained module
is no longer B{X.t := M.t for all t}, but B{X.t := b where b is the
body of t in M}. In principle it is now easy to fine tune the behaviour
to choose whether b or M.t must be used. This change implies modifications
both inside and outside the kernel.
2. for each object in the library it is now necessary to define the behaviour
w.r.t. the substitution {X.t := b}. Notice that in many many cases the
pre-existing behaviour w.r.t. the substitution {X.t := M.t} was broken
(in the sense that it used to break several invariants). This commit
fixes the behaviours for most of the objects, excluded
a) coercions: a future commit should allow any term to be declared
as a coercion; moreover the invariant that just a coercion path
exists between two classes will be broken by the instantiation.
b) global references when used as arguments of a few tactics/commands
In all the other cases the behaviour implemented is the one that looks
to me as the one expected by the user (if possible):
[ terminology: not expanded (X.t := M.t) vs expanded (X.t := b) ]
a) argument scopes: not expanded
b) SYNTAXCONSTANT: expanded
c) implicit arguments: not expanded
d) coercions: expansion to be done (for now not expanded)
e) concrete syntax tree for patterns: expanded
f) concrete syntax tree for raw terms: expanded
g) evaluable references (used by unfold, delta expansion, etc.): not
expanded
h) auto's hints: expanded when possible (i.e. when the expansion of the
head of the pattern is rigid)
i) realizers (for program extraction): nothing is done since the actual
code does not look for the realizer of definitions with a body;
however this solution is fragile.
l) syntax and notation: expanded
m) structures and canonical structures: an invariant says that no
parameter can happear in them ==> the substitution always yelds the
original term
n) stuff related to V7 syntax: since this part of the code is doomed
to disappear, I have made no effort to fix a reasonable semantics;
not expanded is the default one applied
o) RefArgTypes: to be understood. For now a warning is issued whether
expanded != not expanded, and the not expanded solution is chosen.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6555 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6441 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
MOVITATION: in a forthcoming commit the application of a substitution to a
constant will return a constr and not a constant. The application of a
substitution to a kernel_name will return a kernel_name. Thus "constant"
should be use as a kernel name for references that can be delta-expanded.
KNOWN PROBLEMS: the only problem faced is in pretyping/recordops.ml (the code
that implements "Canonical Structure"s). The ADT is violated once in this
ocaml module. My feeling is that the implementation of "Canonical Structure"s
should be rewritten to avoid this situation.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6303 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5920 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
mind_record
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5836 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5567 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5545 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4851 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4849 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4847 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4534 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3967 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
------------------
- (Recursive) Extraction Module devient (Recursive) Extraction Library
(pour cause d'ambiguite avec les nouveaux modules Coq).
- un nouveau Extraction Module qui extrait dans le toplevel tout module Coq
- tout fixpoint est de nouveau inlinable (Yves).
- fix bug du calcul d'env minimal des modules en extraction monolithique.
- un nouveau fichier Modutil regroupant manques de Modops & functions
specifiques aux modules MiniML
- plus d'aliases a trainer (mais des substitutions des le depart)
- ET SURTOUT: un nommage correct (ou du moins moins pire) dans les modtypes
et les functors.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3934 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3788 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3688 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3645 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3569 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3388 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3380 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3336 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3287 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3284 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2957 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2887 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
* extraction.ml + modulaire (cf extract_type) et + proche theorie (cf feu extract_app)
* table.ml filtre les Extract Constant vers types ou terms
* extract_env.ml refuse maintenant les Extraction constr.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2886 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2771 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
commandes vernaculaires (cf dev/changements.txt pour plus de précisions)
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2734 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2522 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
test_extraction.v
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2514 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
- Changement de syntaxe (Extraction Language Toplevel/Ocaml/Haskell)
- Retour des inductifs singletons et vides dans extraction.ml
(extraction.ml -> actions sur le type, mlutil.ml -> conserve le type)
- maintenant par defaut Recursive Extraction === Extraction "file"
- kill_prop global est fait dans extraction.ml selon typage (a suivre...)
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2508 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2309 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2291 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2189 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
|
|
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2145 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
ETC etc etc
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2141 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2138 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
options d'extraction en synchrone
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2137 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2135 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
options
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2133 85f007b7-540e-0410-9357-904b9bb8a0f7
|
