| Age | Commit message (Collapse) | Author |
|---|
|
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16921 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16806 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16727 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16542 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16510 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
- Most of the time, the table registered via Summary.declare_summary
is just a single reference. A new function Summary.ref now allows
to both declare this ref and register it to summary in one shot.
- Clarifications concerning the role of [init_function].
For statically registered tables that don't need a special initializer,
just do nothing there (see the new Summary.nop function).
Beware: now that Summary exports a function named "ref", any code that
do an "open Summary" will probably fail to compile.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16441 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16315 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16282 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16248 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
Ok, this is merely a matter of taste, but up to now the usage
in Coq is rather to use capital letters instead of _ in the
names of inner modules.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16221 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
Gmap uses Pervasives.compare which may interact badly with
structures like pairs of kernel names
For the moment, we consider elements in classes and coercions only
according to their user kernel name: this provides maximal compatibility.
But it could be interesting to try using comparision according to
canonical kernel names...
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16218 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16211 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16165 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16097 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16072 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16071 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15968 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15805 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
List module. That way, an "open Util" in the header permits using
any function of CList in the List namespace (and in particular, this
permits optimized reimplementations of the List functions, as, for
example, tail-rec implementations.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15801 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
especially about unused definitions, unused opens and unused rec
flags.
The following patch uses information gathered using these warnings to
clean Coq source tree. In this patch, I focused on warnings whose fix
are very unlikely to introduce bugs.
(a) "unused rec flags". They cannot change the semantics of the program
but only allow the inliner to do a better job.
(b) "unused type definitions". I only removed type definitions that were
given to functors that do not require them. Some type definitions were
used as documentation to obtain better error messages, but were not
ascribed to any definition. I superficially mentioned them in one
arbitrary chosen definition to remove the warning. This is unaesthetic
but I did not find a better way.
(c) "unused for loop index". The following idiom of imperative
programming is used at several places: "for i = 1 to n do
that_side_effect () done". I replaced "i" with "_i" to remove the
warning... but, there is a combinator named "Util.repeat" that
would only cost us a function call while improving readibility.
Should'nt we use it?
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15797 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
Scheme comments are output on a single line because Ocaml's Format
module which serves as a backend to Pp has an integer, rather than a string
as identation value, so we cannot make it so that each new line in the
comment starts with ";; ".
I've tried something with Pp.ifb but it was hackish at best and had somewhat
strange results.
Known bug: as Pp.std_ppcmds is non-persistent, the comment is actually printed
only once per Extraction command, even if it outputs several files.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15763 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
Extracted code need not preserve typing relations (e:t) from the source code.
This may be a problem as the extracted code may not implement the intented
interface. This option disables the optimisations which would prevent an
extracted term's type to be its extracted source term's type.
At this point the only such optimization is (I think) removing some dummy
λ-abstractions in constant definitions.
Extraction Implicit is still honored in this mode, and it's mostly necessary
to produce reasonable types. So in the conservative type mode, which
abstractions can be removed and which can'tt is entirely under the user's
control.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15762 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15715 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
Patch by Adam Chilipala.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15679 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15412 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15400 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
grammar.cma
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15384 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
Util only depends on Ocaml stdlib and Utf8 tables.
Generic pretty printing and loc functions are in Pp.
Generic errors are in Errors.
+ Training white-spaces, useless open, prlist copies random erasure.
Too many "open Errors" on the contrary.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15020 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
The MLcase has notably changed:
- No more case_info in it, but only a type annotation
- No more "one branch for one constructor", but rather a sequence
of patterns. Earlier "full" pattern correspond to pattern Pusual.
Patterns Pwild and Prel allow to encode optimized matchs without
hacks as earlier. Other pattern situations aren't used (yet)
by extraction, but only by P.N Tollitte's code.
A MLtuple constructor has been introduced. It isn't used by
the extraction for the moment, but only but P.N. Tollitte's code.
Many pretty-print functions in ocaml.ml and other have been reorganized
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14734 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
are declared as such, but I suspect Coq to contain some more.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14724 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
These annotations are purely optional, but could be quite helpful
when trying to understand the code, and in particular trying to
trace which which data-structure may end in the libobject part
of a vo. By the way, we performed some code simplifications :
- in Library, a part of the REQUIRE objects was unused.
- in Declaremods, we removed some checks that were marked as
useless, this allows to slightly simplify the stored objects.
To investigate someday : in recordops, the RECMETHODS is storing
some evar_maps. This is ok for the moment, but might not be in
the future (cf previous commit on auto hints). This RECMETHODS
was not detected by my earlier tests : not used in the stdlib ?
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14627 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
For Ocaml, we now use the extraction-reserved substring "__" :
The name foo__i will be pick for i-th field of record foo if it is anonymous.
For Haskell, still no printing of records as native records,
hence nothing to do.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14420 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
A informative inductive type with one constructor C and one informative arg to C
is normally extracted as an identity, with C removed, see for example
the "sig" type. When this new option is set, these singleton types
are left untouch, providing extracted code which is closer to the initial
Coq development.
Feature requested by Wouter Swiestra.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14260 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
A particular case in sort-polymorphism of inductive types allows
an informative type (such as prod) to have instances in Prop:
(I,I) : True * True : Prop
This is due to the fact that prod is a singleton type: indeed (I,I)
has no informative content. But this invalidates an important invariant
for the correctness of the extraction: inductive constructors stop
having always the same sort as their inductive type. Consider for instance:
Definition f (X:Type)(x:X*X)(g:X->nat) := g (fst x).
Definition test := f _ (I,I) (fun _ => 0).
Then the inductive element (I,I) is extracted as a logical part __,
but during a strict evaluation (i.e. in Ocaml, not Haskell), this __
will be given to fst, and hence to a match, leading to a nasty result
(potentially segfault). Haskell is not affected, since fst is never
evaluated.
This patch adds a check for this situation during any Ocaml extraction,
leading for the moment to a fatal error. Some functions in inductive.ml
and retyping.ml now have an extra optional argument ?(polyprop=true)
that should stay untouched in regular Coq usage, while type-checking
done during extraction will disable this prop-polymorphism.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14256 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
"Print Module M" prints now by default both a signature
(fields with their types) and a body (fields with their types
and transparent bodies).
"Print Module Type M" could be used both when M is a module
or a module Type, it will only display th signature of M.
The earlier minimalist behavior (printing only the field names)
could be reactivated by option "Set Short Module Printing".
For the moment, the content of internal sub-modules and sub-modtypes
are not displayed.
Note: this commit is an experiment, many sitations are still
unsupported. When such situations are encountered, Print Module
will fall back on the earlier minimalist behavior. This might
occur in particular in presence of "with" annotations, or in the
conjonction of a non-global module (i.e. functor or module type)
and internal sub-modules.
Side effects of this commit:
- a better compare function for global_reference, with no
allocations at each comparison
- Nametab.the_globrevtab is now searched according to user part only
of a kernel_name
- The printing of an inductive block is now in Printer, and rely less
on the Nametab. Instead, we use identifiers in mind_typename and
mind_consnames. Note that Print M.indu will not display anymore
the pseudo-code "Inductive M.indu ..." but rather "Inductive indu..."
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14117 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14094 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
I thought this situation wasn't possible, hence the Option.get.
But it's apparently legal to use Declare Module anywhere, even
outside a Module Type. No idea on how to handle that at extraction
for the moment, hence a proper "unsupported" error message.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14013 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
In signatures, opaque terms are always seen as parameters.
In implementations, a flag Set/Unset Extraction AccessOpaque
allows to customize things:
- Set : opacity is ignored (this is the old behavior)
- Unset : opaque terms are extracted as axioms (default now)
Some warnings are anyway emitted when extraction encounters
informative opaque terms.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13999 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
|
|
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13891 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
|
|
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
|
|
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@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
|
|
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
|
