| 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
|
|
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
|
|
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
|
|
(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
|
|
-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
|
|
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@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
|
|
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
|
|
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
|
|
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
|
|
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
|
|
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
|
|
(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
|
|
This commit fixes the bug that prevented extraction of Lyon/CIRCUITS.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6328 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
the new module kernel/mod_subst.ml.
MOTIVATION: mod_subst is compiled after kernel/term.ml; thus it is now
possible to define substitutions that also delta-expand constants
(by associating the delta-expanded form to the constant name).
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6304 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
|
|
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4856 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@4847 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4843 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4530 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@3645 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3623 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3622 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3621 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@3494 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3432 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@3381 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@3199 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3029 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@2913 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
|
