| Commit message (Collapse) | Author | Age |
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
| |
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
|
|
|
|
| |
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9455 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
|
|
|
|
|
|
| |
famille
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9032 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
|
|
| |
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8931 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
|
|
|
|
|
|
|
|
|
|
|
|
| |
- qualification correcte des noms en Haskell
- on imprime les types de toutes les fonctions en Haskell
- en Ocaml, les appels recursifs d'une f : 'a truc doivent
se faire avec les _meme_ parametres de types 'a. Exemple illegal:
let rec f = function [] -> 0 | l -> f [l];;
On met maintenant des Obj.magic en conséquence.
En Haskell (avec typage fourni), ca passe.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8930 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
|
|
| |
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8921 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
|
|
| |
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8891 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
|
|
| |
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8886 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
|
|
|
|
|
|
|
|
|
| |
- prise en compte du niveau à la déclaration du type comme une fonction
des sortes des conclusions des paramètres uniformes
- suppression du retypage de chaque instance de type inductif (trop coûteux)
et donc abandon de l'idée de calculer une sorte minimale même dans
des cas comme Inductive t (b:bool) := c : (if b then Prop else Type) -> t.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8845 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
|
|
|
|
| |
'properties' de Subversion
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8758 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
|
|
| |
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8752 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
|
|
| |
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8724 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
|
|
| |
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@7751 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
|
|
|
|
| |
G_*new en G_*.ml + autres petites modifications liées à suppression du traducteur
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@7740 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
|
|
|
|
| |
(mcanismes de renommage des noms de constantes, de module, de ltac et de certaines variables lies de lemmes et de tactiques, mcanisme d'ajout d'arguments implicites, etc.)
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@7734 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
|
|
|
|
| |
tactiques
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@7681 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
|
|
|
|
| |
suppression des Sig
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@7653 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
|
|
|
|
|
|
|
|
| |
- une syntaxe unique bigloo / pas bigloo (match sans ?)
- un (load "macros_extr.scm") initial, et un mot sur ou le trouver
- gestion des realisations d'axiomes
- les ' dans les identifiateurs sont translates vers ~
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@7651 85f007b7-540e-0410-9357-904b9bb8a0f7
|