| Commit message (Collapse) | Author | Age |
|
|
|
|
|
|
|
|
|
|
| |
This leads to code closer to the original input of the user,
and moreover some more dummy __ may be removed this way.
To avoid unfolding by mistake user's variables, we change
the name of these generated let-in into "program_branch_NN" instead
of "branch_NN"
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13964 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
|
|
|
|
|
|
|
|
|
| |
Due to wrong pattern order in Mlutil.mgu, simple situations like
?n == ?n were considered unsolvable as soon as one side was aliased
(i.e. inside an instantiated type meta).
Moreover, use general equality as last resort, instead of forgetting
cases like Taxiom == Taxiom.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13963 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
| |
The recent experiment with -dont-load-proofs in the stdlib showed that
this options isn't fully safe: some axioms were generated (Include ?
functor application ? This is still to be fully understood).
Instead, I've implemented an idea of Yann: only load opaque proofs when
we need them. This is almost as fast as -dont-load-proofs (on the stdlib,
we're now 15% faster than before instead of 20% faster with -dont-load-proofs),
but fully compatible with Coq standard behavior.
Technically, the const_body field of Declarations.constant_body now regroup
const_body + const_opaque + const_inline in a ternary type. It is now either:
- Undef : an axiom or parameter, with an inline info
- Def : a transparent definition, with a constr_substituted
- OpaqueDef : an opaque definition, with a lazy constr_substitued
Accessing the lazy constr of an OpaqueDef might trigger the read on disk of
the final section of a .vo, where opaque proofs are located.
Some functions (body_of_constant, is_opaque, constant_has_body) emulate
the behavior of the old fields. The rest of Coq (including the checker)
has been adapted accordingly, either via direct access to the new const_body
or via these new functions. Many places look nicer now (ok, subjective notion).
There are now three options: -lazy-load-proofs (default), -force-load-proofs
(earlier semantics), -dont-load-proofs. Note that -outputstate now implies
-force-load-proofs (otherwise the marshaling fails on some delayed lazy).
On the way, I fixed what looked like a bug : a module type
(T with Definition x := c) was accepted even when x in T was opaque.
I also tried to clarify Subtyping.check_constant.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13952 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
|
|
|
|
|
| |
If the user customized the inductive, he should know what he is
doing... This (hopefully) fixes bug #2482.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13944 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
|
|
| |
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13891 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
|
|
| |
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13890 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
|
|
|
|
|
| |
This happens for instance when the main component of the fixpoint
block has been provided via Extract Constant
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13889 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
| |
This is a mix of "Recursive Extraction" and "Extraction Library":
- like "Extraction Library", the extracted code is splitted in
separated files, one per coq source file.
- unlike "Extraction Library", but similarly to "Recursive Extraction",
not everything gets extracted, but only dependencies of some
initially-given elements
We prepare for a more clever dependency selection inside sub-modules.
For the moment all needed sub-modules are still fully extracted (other we
would need to fix signatures accordingly).
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13888 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
| |
For Haskell, we still try to provide readable indentation,
but we now avoid relying on this indentation for correctness.
Instead, we use layout-independant syntax with { } when
necessary (after "case of" and "let"). It is much safer this
way, even if the syntax gets a bit more cumbersome.
For people allergic to {;}, they can most of the time do a
tr -d "{;}" without changing the meaning of the program.
Be careful nonetheless: since "case of" is now delimited,
some parenthesis that used to be mandatory are now removed.
Note also that the initial "module ... where" is still without
{ }: even when Format goes crazy it doesn't tamper with column 0.
Other modifications:
- Using "Set Printing Width" now affects uniformly the extraction
pretty-printers. You can set a greater value than the default 78
before extracting a program that you know to be "really deep".
- In ocaml (and also a bit in Haskell), we now try to avoid abusing
of 2-char-right-indentation. For instance | is now aligned with
the "m" of match. This way, max_indent will be reached less frequently.
- As soon as a pretty-print box contains an explicit newline,
we set its virtual size to a big number, in order to prevent this
box to be part of some horizontal arrangement.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13870 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
|
|
| |
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13861 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
|
|
| |
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13859 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
| |
As said in CHANGES:
<<
The inlining done during application of functors can now be controlled
more precisely. In addition to the "!F G" syntax preventing any inlining,
we can now use a priority level to select parameters to inline :
"<30>F G" means "only inline in F the parameters whose levels are <= 30".
The level of a parameter can be fixed by "Parameter Inline(30) foo".
When levels aren't given, the default value is 100. One can also use
the flag "Set Inline Level ..." to set a level.
>>
Nota : the syntax "Parameter Inline(30) foo" is equivalent to
"Set Inline Level 30. Parameter Inline foo.",
and "Include <30>F G" is equivalent to "Set Inline Level 30. Include F G."
For instance, in ZBinary, eq is @Logic.eq and should rather be inlined,
while in BigZ, eq is (fun x y => [x]=[y]) and should rather not be inlined.
We could achieve this behavior by setting a level such as 30 to the
parameter eq, and then tweaking the current level when applying functors.
This idea of levels might be too restrictive, we'll see, but at least
the implementation of this change was quite simple. There might be
situation where parameters cannot be linearly ordered according to their
"inlinablility". For these cases, we would need to mention names to inline
or not at a functor application, and this is a bit more tricky
(and might be a pain to use if there are many names).
No documentation for the moment, since this feature is experimental
and might still evolve.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13807 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
|
|
| |
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13770 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
|
|
|
|
|
|
| |
We now keep some type information in the "info" field of constructors
and cases, and compact a match with some default branches (or remove
this match completely) only if this transformation is type-preserving.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13732 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
|
|
|
|
| |
in addition, a makefile entry pluginsopt for compiling only the .cmxs
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13509 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
|
|
| |
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13461 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
|
|
|
|
|
|
|
|
| |
In particular, the unused lib/tlm.ml and lib/gset.ml are removed
In addition, to simplify code, Libobject.record_object returning only the
('a->obj) function, which is enough almost all the time.
Use Libobject.record_object_full if you really need also the (obj->'a).
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13460 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
| |
'_a types
If there's no lambdas at the top of a constant body
and its type is functional
and this type contains type variable
and we're extracting to Ocaml
then we perform one eta-expansion to please the ML type-checker
This might slow down things, if some computations are shared
thanks to the partial application. But it seems quite unlikely to
encounter both situations (clever partial application and
non-generalizable variable) at the same time. Compcert is ok,
for instance.
As a consequence, no need for manual eta-expansion in AVL code
(and by the way MSetAVL.element wasn't a problem, it is monomorphic)
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13441 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
| |
Cf. coqdev for the details of the bug report.
- Protect some Hashtbl.find and other risky functions in order to avoid
as much as possible to end with an irritating Anomaly : Not_found.
- Re-enable in pp_ocaml_extern the case of a module-file used as
a module (e.g. module A' := A for A.v) when doing modular extraction.
- Rework the code that decides to "open" or not modules initially:
opening A when A contains a submodule B hides the file B even when
B isn't opened itself, we avoid that now.
- Fix some tables (sets or maps) used by extraction for which it is
critical to consider constants/inductives/global_reference _not_
modulo the equivalence of Elie, but rather via Pervasives.compare.
Still to do : avoid appearance of '_a in extracted code.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13424 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
|
|
| |
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13417 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
|
|
|
|
| |
See http://caml.inria.fr/mantis/view.php?id=4940
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13413 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
|
|
| |
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13323 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
| |
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
|