| Age | Commit message (Collapse) | Author |
|---|
|
Extraction under modules is highly experimental, and just work a bit.
Don't expect too much of it. With this commit, I simply avoid a few
"assert false" to occur when we are under modules. But things are
still quite wrong, for instance with:
Definition foo.
Module M.
Definition bar := foo.
Recursive Extraction bar.
Extraction of bar is ok, but foo isn't displayed, since extraction
can't get it: Lib.contents_after doesn't mention it, it is probably
in some frozen summary.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13281 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
#2241)
Here, the constants "without body" we don't want to autoinline are
constants made opaque by the rigid signature of their module.
As mentionned by X.L. inlining them might lead to untypable code.
The current solution is safe, but not ideal: we could want to inline
such constants at least inside their own module, and we could also
want to inline constants that are not globally visible (functors...).
NB: AutoInline is anyway not activated by default anymore
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13273 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
In addition to the "| _ -> cst" situation, now we can also
reconstruct a "| e -> f e" final branch. For instance,
this has a tremenduous effect on Compcert/backend/Selection.v.
NB: The "fun" factorisation is almost more general than the "cst"
situation, but not always. Think of A=>A|B=>A, 1st branch will be
recognized as (fun x->x), not (fun x->A). We also add a fine
detection of inductive types with phantom type variables, for which
this optimisation is type-unsafe.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13267 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
The auto-inlining has always been cumbersome. We only keep the
inlining of recursors (foo_rect for inductive foo), and a short
list of specific constants declared in mlutil.ml. In particular
we inline andb and orb to keep their lazy behavior.
The previous behavior is available via Set Extraction AutoInline
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13266 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13261 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
And similarly for Haskell: we do not force capitalized/uncapitalized
filenames anymore, but we rather follow the name of the .v file (with
new extensions of course). Ok, this is an incompatible change, but
it is really convenient, some people where actually already doing
some hacks to have this behavior (cf. Compcert).
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13260 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
We use the mod_type_alg and typ_expr_alg field when they aren't
empty. As a consequences, many signatures are now simple
abbreviations, or "with" constructions, leading to .mli that are
_way_ shorter this way. Various fixups concerning the "with
Definition" syntax. In extract_seb_spec, we propagate both the alg
and non-alg versions of the structure, for handlying nicely the
"with" situation, and expanding situations not possible in ocaml.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13249 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
- MPbound can be part of visible_mps (when printing the type of
a module parameter, or when printing body of a With), hence
the locality test base_mp mp = base_mp (top_visible_mp ())
isn't accurate.
- new organisation, pp_ocaml_gen is splitted in many sub-functions,
attempt to be clearer
- the shortcut (if List.length ls = 1 then ...) isn't safe,
we might detect name conflict even in this case.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13248 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
- Add module parameters in the structure of visible_layer,
in order for module params to be part of name clash detection,
avoiding this way a source of potentially wrong code.
- In case of clash, module params are alpha-renamed to something
unique (Foo__XXX where XXX is the number contained in the mbid).
This solves some situations that were unsupported by extraction.
for instance the "Module F (X:T). Module X:=X. ... End F."
- We now check in Coq identifiers the presence of the
extraction-reserved string __. If it is found, we issue a warning
(which might become an error someday).
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13240 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
- For Haskell, modules abbreviations and applied functors are expanded.
The only remaining sitation that isn't supported is extracting functors
and applying them after extraction.
- Add a module extraction for Scheme with the same capabilities as for
Haskell (with no Extraction Library, though).
- Nicer extracted module types (use of the mb.mod_type_alg if present)
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13236 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13235 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
Module types are ignored, functors and module ident raise an error
When dealing with simple modules, even nested, the structure
hierarchy is removed, and names are arranged in the following way:
- For the monolithic extraction, we simply use next_ident_away
on short names, as we do when the same name appears in two .v.
- For modular extraction, A.B.t become A__B__t or _A__B__t
depending whether t is a type, a constructor or a constant.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13210 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13208 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13192 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
#2158,#2179)
Any unicode character above 128 is replaced by __Uxxxx_ where xxxx is
the hexa code for the unicode index of this character. For instance
<alpha> is turned into __U03b1_. I know, this is ugly. Better
solutions are welcome, but I'm afraid we can't do much better as long
as ocaml and haskell don't accept unicode letters in idents. At
least, this way we're pretty sure this translating won't create name
conflit, as long as extraction users avoid __ in their names,
something that they should already do btw (see for instance
extraction of coinductive types in ocaml). Yes, I should add a test
and a warning/error in case of use of __ someday.
NB: this commit belongs proudly to the quick'n'dirty category
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13173 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13158 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
- we use a wrapper file big.ml to have short names about big_int
and specialized functions for extraction
- new files : ExtrOcamlZInt for Z==>int and N==>int,
ExtrOcamlZBigInt for Z==>big_int and N==>big_int
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13137 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13109 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13093 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13089 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
When Requiring ExtrOcamlString :
* ascii is mapped to Ocaml's char, the ugly translation of constructor
and pattern-match should hopefully be seen very rarely (never ?).
We add a hack in ocaml.ml for recognizing constant chars.
* string is mapped to (list char). Extracting to Ocaml's string could be
done, but would be really nasty (lots of non-trivial Extract Constant to
add). For now, (list char) seems a good compromise.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13078 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13074 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
- ExtrOcamlBasic: mapping of basic types to ocaml's ones
- ExtrOcamlIntConv: conversion between int and coq's numerical types
- ExtrOcamlBigIntConv: same with big_int (no overflow)
- ExtrOcamlNatInt: realizes nat by int (unsafe)
more to come: Haskell, handling of stings, more stuff in ExtrOcamlNatInt,
etc etc...
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13050 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
For instance:
Extract Inductive nat => int [ "0" "succ" ]
"(fun fO fS n => if n=0 then fO () else fS (n-1))".
See Extraction.v for more details and caveat.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13025 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12983 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
The command : Extraction Implicit foo [1 3].
will tell the extraction to consider fst and third arg of foo as implicit,
and remove them, unless a final occur-check after extraction shows they
are still there. Here, foo can be a inductive constructor or a global
constant.
This allow typicaly to extract vectors into usual list :-)
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12982 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
|
|
- When using an infix constructor such as (::), whitespaces are
to be given by the user, for instance
Extract Inductive list => list [ "[]" "( :: )" ].
- Remove ugly whitespaces when using the ""-for-Pair trick:
Extract Inductive prod => "(*)" [ "" ].
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12944 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12943 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
- we saturate the normalize function : as long as
(kill_dummy + simpl) isn't a nop, we do it again.
- generalize_case allowed on all types of theories/Init/*.v
instead of only bool,sumbool,sumor. NB: this optim cannot
be performed on any type, it might produce untyped code.
- common_branch allowed on match with one branch: in this
situation it indicates whether the match can be removed or not.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12942 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12940 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12939 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
* An inductive constructor Dummy instead of a constant dummy_name
* The Tmp constructor indicates that the corresponding MLlam or
MLletin is extraction-specific and can be reduced if possible
* When inlining a glob (for instance a recursor), we tag some
lambdas as reducible. In (nat_rect Fo Fs n), the head lams of
Fo and Fs are treated this way, in order for the recursive call
inside nat_rect to be correctly pushed as deeper as possible.
* This way, we can stop allowing by default linear beta/let
reduction even under binders (can be activated back via
Set Extraction Flag).
* Btw, fix the strange definition of non_stricts for (x y).
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12938 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
eta-expansions
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12936 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12485 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@12338 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12337 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
only used to allow a module to be ended before the summaries were
restored what can be solved by moving upwards the place where the
summaries are restored).
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12275 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12266 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
(uniformisation of function names, classification). One of the most
visible change is the renaming of section_path into full_path (the
use of name section was obsolete due to the module system, but I
don't know if the new name is the best chosen one - especially it
remains some "sp" here and there).
- Simplification of the interface of classify_object (first argument dropped).
- Simplification of the code for vernac keyword "End".
- Other small cleaning or dead code removal.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12265 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
- add coqtop option "-compat X.Y" so as to provide compatibility with
previous versions of Coq (of course, this requires to take care of
providing flags for controlling changes of behaviors!),
- add support for option names made of an arbitrary length of words
(instead of one, two or three words only),
- add options for recovering 8.2 behavior for discriminate, tauto,
evar unification ("Set Tactic Evars Pattern Unification", "Set
Discriminate Introduction", "Set Intuition Iff Unfolding").
Update of .gitignore
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12258 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
* generalize the use of .mllib to build all cma, not only in plugins/
* the .mllib in plugins/ now mention Bruno's new _mod.ml files
* lots of .cmo enumerations in Makefile.common are removed, since
they are now in .mllib
* the list of .cmo/.cmi can be retreive via a shell script line,
see for instance rule install-library
* Tolink.core_objs and Tolink.ide now contains ocaml _modules_, not
_files_
* a -I option to coqdep_boot allows to control piority of includes
(some files with the same names in kernel and checker ...)
This is quite a lot of changes, you know who to blame / report to
if something breaks.
... and last but not least I've started playing with ocamlbuild.
The myocamlbuild.ml is far from complete now, but it already allows
to build coqtop.{opt,byte} here. See comments at the top of
myocamlbuild.ml, and don't hesitate to contribute, either for completing
or simplifying it !
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12002 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
user contribs
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11996 85f007b7-540e-0410-9357-904b9bb8a0f7
|
