| Age | Commit message (Collapse) | Author |
|---|
|
user contribs
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11996 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11977 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11949 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11889 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
Quelques modifications autour (géographiquement) de Util.list_split_at
Util.list_split_at devient Util.list_split_when (dénomination inventée
arbitrairement par moi-même, mais qui ne devrait pas déranger grand
monde vu qu'il semble n'y avoir que deux occurences de cette fonction).
Pour laisser la place à la fonction suivante :
Introduction de Util.list_split_at: qui sépare la liste à une position
donnée (alors que la nouvellement nommé list_split_when sépare à la
première occurence "vrai" d'un prédicat).
Ajout de quelques commentaires dans util.ml (pas le mli) sur ces deux
fonctions.
Suppression de Impargs.list_split_at (appel à Util).
Suppression de Subtac_pretyping.list_split_at (qui était du code mort de
toute façon).
Suppression Util.list_split_by qui n'est utilisé nulle part et est une
réimplémentation de List.partition (qui est probablement meilleure, en
particulier tail-recursive)
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11851 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11848 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
#2025)
For instance, when we need to extract Init.Wf and Program.Wf,
the first one gives wf.ml and the second wf0.ml.
This name resolution mechanism is merged with the handling of the
extraction filename blacklist. Hence, after Extraction Blacklist Foo,
the coq file Foo.v will now be extracted as foo0.ml (instead of
coq_Foo.ml as previously).
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11843 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@11695 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11690 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11688 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
revival of option -translate as a -beautify option.
PS: compilation checked against 11610.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11618 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
(diff says it's a big commit, whereas diff -w says it's an empty one ;-)
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11547 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
Ocaml :
- Fix the Coq__1 that was appearing in a .mli for some functor app
in the corresponding .ml (virtual printing of the interface in the .ml +
a pp_modname delayed in MTfunsig)
- Cleanup in MTwith parts
- Better handling of subst for MTsig
- Correct push/pop_visible in pp_struct/pp_signature
Common :
- Merge most of pp_global and pp_module
- Clarify the use of tables : remove some of them, attach many others
to their corresponding function.
- The "visible" table now groups mps, their content, and some subst
(for the inside of MTsig)
- Cleanup of tables is done via a registration mecanism
- No more "initial" create_renamings, instead some fully on-the-fly
renaming (thanks to the "Pre" phase)
- opened libaries are computed between "Pre" and "Impl" phases
- for simplicity, static_clash aren't computed statically anymore (cost?)
Extract_env:
- A "Pre" phase not only for Ocaml
- Extraction Library is in fact also Recursive (for getting a right
mpfiles_content) ... but only last item is printed to a real file
instead of /dev/null
Modutil: No more struct_get_references_*
Util : fix the evaluation order of prlist_strict
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11538 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11485 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
(unrelated: a useless pattern variable becomes _ in Extract_env)
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11458 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11456 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
-The use of Modops.type_of_mb seems to be sometimes an overkill :
it expands the situation where mb.mod_type=SEBident...
we use a simplier my_type_of_mb instead
-No more "truetype" boolean argument to this function. Normally,
the use of my_type_of_mb should ensure that all seb we inspect
are "true" module types, see the invariant written before this
function.
-Remove the use of replicate_msid: it was commented out since
a few months, no problem appeared, and anyway the handling of
"With ..." has completely changed since Elie's work.
-And by the way, cleanup of whitespaces at the end of lines...
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11455 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11454 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
When doing monolithic extraction, the initial dependency graph
may turn to be too broad thanks to later optimisations. We now do
an extra dependency pass at the end, killing more useless code.
In addition, when doing an "Extract Constant t => ...", if t
isn't an axiom, we don't include the dependencies of the body of t.
This may break earlier extraction setups (with or without Extract
Constant), since they may take advantage of objects that were earlier
"wrongly" included in the extracted code. The fix is simple : just
add these missing objects to the extraction command-line.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11239 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
for debug / external output via coqtop.byte + Drop
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10895 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10805 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10794 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10665 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10664 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
* When no explicit module type is given in Coq, extraction proceeds
with more caution when recontructing a module type from the
module. For instance, a module ident isn't keep, since it's the name
of an implementation, not of a module type. Fix the bug
functor M -> M : funsig M -> M instead of funsig M -> typeof(M)
* Removed duplicated code with Modops
* The call to replicate_msid doesn't seem to be as crucial as before.
Let's try to remove it.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10620 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10596 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10592 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
|
|
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10460 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10455 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
devient Flags.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10348 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
lib/option.ml(i) . J'en profite pour rajouter des primitives de lifting
des fonctions (à un ou deux arguments tous ou partie de type option).
Il reste quelques opérations dans Util à propos desquelles je ne suis
pas trop sûr, ou simplement que j'ai oublié, mais qui attendront demain
car il est tard (comme some_in qui devrait devenir Option.make je
suppose) . Elles s'expriment souvent facilement en fonction des
autres, par exemple "option_compare x y" est égal à "Option.lift2 compare x y"
. Le option_cons devrait faire son chemin dans le module parce qu'il est
assez primitif et qu'il n'y a pas de fonction "cons" dans OCaml.
J'en ai profité aussi pour remplacer les trop nombreux "failwith" par
des erreurs locales au module, donc plus robustes.
J'ai trouvé aussi une fonction qui était définie deux fois, et une
définie dans un module particulier.
Mon seul bémol (mais facile à traiter) c'est la proximité entre le
nom de module Option et l'ancien Options. J'ai pas de meilleure idée de
nom à l'heure qu'il est, ni pour l'un, ni pour l'autre.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10346 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10329 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10266 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
|
|
A better eta-reduction allows to detect that List.map is indeed a fixpoint.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10244 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
Unlike prlist_xxxx and prvect, the function prlist is acting lazily,
which is bad for extraction (synchronization with tables). We add and
use a prlist_strict function.
Additionaly:
- cleanup of the preamble printing
- no need for 2-pass printing (/dev/null trick) when the language
isn't ocaml
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10233 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
|
|
If a constructor has two arguments and the corresponding string
given in a Extract Inductive is of the form "(foo)", then foo
is used as an infix constructor.
Idem for a inductive type name.
Examples:
Extract Inductive list => list [ "[]" "(::)" ].
Extract Inductive prod => "(*)" [ "(,)" ].
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10188 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
If a match has two or more identical branches (that moreover do not
depend on their pattern variables), we merge them in a last branch
whose pattern is _
If _all_ branches are identical, we just remove the match
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10186 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
Not maintained, probably broken, of no interest except (maybe) for
myself, bad interaction with tools that work recursively (coqdep).
===> I move it to a personal repository
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9986 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
details).
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9821 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
1) Disparition de test_extraction.v rebasculé dans test-suite/success/extraction.v
Au passage, remplacement de quelques Set en Type pour ne pas avoir besoin du
-impredicative-set. Et ajout de passes d'extraction en Haskell et Scheme.
Simplification du Makefile en conséquence (plus de barestate)
2) Au passage, reparation (et embellissement) de extract_env. Depuis
le passage de Claudio dans cette portion (il y a 2 ans ?),
faire Extraction S (ou tout autre constructeur) echouait. Idem pour
un nom d'inductif mutuel autre que le premier du paquet. Etonnant que
personne n'ait remarqué ca plus tot...
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9484 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9483 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9471 85f007b7-540e-0410-9357-904b9bb8a0f7
|
