| Age | Commit message (Collapse) | Author |
|---|
|
During an extraction, a few tables are maintained to cache
intermediate results. Due to modules, the kernel_name index
for these caching tables aren't enough. For instance, in
bug #3923, a constant is first transparent (from inside the
module) then opaque (when seen from the signature). The previous
protections were actually obsolete (tests via visible_con), we
now checks that the constant_body is still the same.
|
|
vars by _)
|
|
This is done via a unique pass which seems roughly linear in practice,
even on big developments like CompCert. There's a List.nth in an env at
each MLrel, that could be made logarithmic if necessary via Okasaki's
skew list for instance.
Another approach would be to keep names (as a form of documentation), but
prefix them by _ to please OCaml's warnings. For now, let's be radical and
use the _ pattern.
|
|
This fix only handles MLapp(MLmagic(MLlam...),...). Someday, we'll have
to properly investigate the interaction between all the other optimizations
and MLmagic. But well, at least this precise bug is fixed now.
|
|
In front of "let rec f x y = ... in f n m", if n is now an implicit argument,
then the argument x of the inner fixpoint f is also considered as implicit.
This optimization is rather ad-hoc, since we only handle MLapp(MLfix()) for
now, and the implicit argument should be reused verbatim as argument.
Note that it might happen that x cannot be implicit in f. But in this
case we would have add an error message about n still occurring somewhere...
At least this small heuristic was easy to add, and was sufficient to solve
the part 2 of bug #4243.
|
|
|
|
|
|
Some explicit '\n' in Pp.str were interacting badly with Format boxes
in Compcert, leading to right-flushed "sig..end" blocks in some .mli
|
|
|
|
Instead of the original hacks (embedding implicits in string msg in MLexn !)
we now use a proper construction MLdummy (Kimplicit (r,i)) to replace the use
of the i-th argument of constant or constructor r when this argument has been
declared as implicit.
A new option Set/Unset Extraction SafeImplicits controls what happens
when some implicits still occur after an extraction : fail in safe mode,
or otherwise produce some code nonetheless. This code is probably buggish
if the implicits are actually used to do anything relevant (match, function
call, etc), but it might also be fine if the implicits are just passed along.
And anyway, this unsafe mode could help figure what's going on.
Note: the MLdummy now expected a kill_reason, just as Tdummy.
These kill_reason are now Ktype, Kprop (formerly Kother) and Kimplicit.
Some minor refactoring on the fly.
|
|
|
|
The ind_equiv field wasn't correctly set, due to some kernel names
glitches (canonical vs. user). The fix is to take into account the
delta_resolver while traversing module structures.
|
|
|
|
|
|
|
|
|
|
The previous extraction of [Z.div] for Haskell did not properly handle
divide-by-zero. Fix it by introducing an explicit [if] statement in the
generated Haskell code.
Also, introduce a similar extraction rule for [Z.modulo], with the same
check for modulo-by-zero.
|
|
The previous extraction of [Nat.div] for Haskell did not properly handle
divide-by-zero. Fix it by introducing an explicit [if] statement in the
generated Haskell code.
Also, introduce a similar extraction rule for [Nat.modulo], with the same
check for modulo-by-zero.
|
|
Use expand projection to come back to the projection-as-constant encoding, dealing with parameters correctly.
|
|
This mirrors the existing extraction libraries for OCaml.
One wart: the extraction for [string] requires that the Haskell code
imports Data.Bits and Data.Char. Coq has no way to add extra import
statements to the extracted code. So we have to rely on the user to
somehow import these libraries (e.g., using the -pgmF ghc option).
See also https://coq.inria.fr/bugs/show_bug.cgi?id=4189
Message to github robot: this commit closes #65
|
|
|
|
|
|
This is important to disambiguate identical names from different modules.
|
|
This patch allows Coq terms to be extracted into the widely used JSON
format. This is useful in at least two cases:
- One might want to manipulate Coq values outside of Coq, but without
being forced to use one of the three existing extraction languages
(OCaml, Haskell, or Scheme), and without having to compile Coq's
extracted result. This is especially useful when a Coq evaluation
produces some data structure that needs to be moved out of Coq.
Having to invoke an OCaml/Haskell/Scheme compiler just to get a
data structure out of Coq is somewhat awkward.
- One might want to experiment with extracting Coq code into other
languages (Go, Javascript, etc), without having to write the whole
extraction logic in OCaml and recompile Coq's extraction plugin
each time. This makes it easy to quickly prototype extraction
in any language, without having to build Coq from source.
Extraction to JSON is implemented by adding the JSON "pseudo-language"
to the extraction facility. Thus, one can extract the JSON encoding
of a single term using:
Extraction Language JSON.
Extraction qualid.
and extract an entire Coq library "ident" into "ident.json" using:
Extraction Language JSON.
Extraction Library ident.
Nota (Pierre Letouzey) : this is an updated version of the original
PullRequest, updated to match recent changes in trunk
|
|
|
|
The extraction machinery has specialized support for extracting [ascii]
characters into native characters in the target language, as opposed
to using an explicit constructor from 8 boolean bits. This works by
hard-coding the name of the character type in the target language.
Unfortunately, the hard-coded type for Haskell was "Char", not the
fully-qualified "Prelude.Char". As a result, it was impossible to
extract characters into Haskell without getting type errors about "Char".
This patch changes this hard-coded name to "Prelude.Char".
|
|
|
|
|
|
Commit 84c2433a introduced the Any type alias as the Haskell extracted
version of MiniML's Tunknown. However, the code to define the Any
type alias was generated conditional on usf.magic. As it turns out,
sometimes Tunknown appears even if usf.magic is false (i.e., even if
MLmagic does not appear anywhere in the AST). This produced Haskell
code that would not compile; e.g.:
% coqtop
Coq < Extraction Language Haskell.
Coq < Extraction Library Datatypes.
The file Datatypes.hs has been created by extraction.
% ghc Datatypes.hs
[1 of 1] Compiling Datatypes ( Datatypes.hs, Datatypes.o )
Datatypes.hs:261:17: Not in scope: type constructor or class `Any'
Datatypes.hs:261:24: Not in scope: type constructor or class `Any'
The fix is straightforward: produce the code that defines the Any type
alias if usf.tunknown is true.
|
|
|
|
|
|
(Fix for bugs #3470 and #3694)
|
|
typecheck with definitions and thread it accordingly when typechecking
module expressions.
|
|
Since name clashes are discovered by side effects, the order of traversal of
module structs cannot be changed.
|
|
The control flow of extraction is hard to read due to exceptions. When meeting
an inlined constant extracted to custom code, they could desynchronize some
tables in charge of detecting name clashes, leading to an anomaly.
|
|
|
|
|
|
After this commit, module_type_body is a particular case of module_type.
For a [module_type_body], the implementation field [mod_expr] is
supposed to be always [Abstract]. This is verified by coqchk, even
if this isn't so crucial, since [mod_expr] is never read in the case
of a module type.
Concretely, this amounts to the following rewrite on field names
for module_type_body:
- typ_expr --> mod_type
- typ_expr_alg --> mod_type_alg
- typ_* --> mod_*
and adding two new fields to mtb:
- mod_expr (always containing Abstract)
- mod_retroknowledge (always containing [])
This refactoring should be completely transparent for the user.
Pros: code sharing, for instance subst_modtype = subst_module.
Cons: a runtime invariant (mod_expr = Abstract) which isn't
enforced by typing. I tried a polymorphic typing of mod_expr,
to share field names while not having mtb = mb, but the OCaml
typechecker isn't clever enough with polymorphic mutual fixpoints,
and reject code sharing (e.g. between subst_modtype and subst_module).
In the future (with ocaml>=4), some GADT could maybe help here,
but for now the current solution seems good enough.
|
|
In the case of an inner module without explicit signature,
(and not used later in a functor application), we now extract
only the needed items (used later or asked by the user),
instead of blindly extracting all fields as earlier.
|
|
Since type variables are local to the definition, we simply rename
them in case of unicode chars. We also get rid of any ' to avoid
Ocaml illegal 'a' type var (clash with char litteral).
|
|
|
|
- Common.get_native_char instead of just a pp function of this char
- Enrich the record projection table
|
|
|
|
|
|
When Coq's Haskell extraction needs to use unsafeCoerce, it passes
the -fglasgow-exts option to GHC, but recent versions of GHC warn
against this:
xx.hs:1:16: Warning:
-fglasgow-exts is deprecated: Use individual extensions instead
This patch does as the warning suggests, replacing -fglasgow-exts
with the specific option that the extraction needs (-XMagicHash).
|
|
When Haskell extraction requires magic type coersion, Coq produces
the following code:
unsafeCoerce :: a -> b
#ifdef __GLASGOW_HASKELL__
import qualified GHC.Base
unsafeCoerce = GHC.Base.unsafeCoerce#
#else
-- HUGS
import qualified IOExts
unsafeCoerce = IOExts.unsafeCoerce
#endif
GHC version 7.6.3 does not allow imports after a type declaration,
and produces this error:
xx.hs:20:1: parse error on input `import'
(referring to the first import statement above). This patch moves
the unsafeCoerce type declaration to just after the import statement,
fixing this compile error.
|
|
|
|
Before this patch opaque tables were only growing, making them unusable
in interactive mode (leak on Undo).
With this patch the opaque tables are functional and part of the env.
I.e. a constant_body can point to the proof term in 2 ways:
1) directly (before the constant is discharged)
2) indirectly, via an int, that is mapped by the opaque table to
the proof term.
This is now consistent in batch/interactive mode
This is step 0 to make an interactive coqtop able to dump a .vo/.vi
|
|
for the record binder of classes. This name is no longer generated
in the kernel but part of the declaration. Also cleanup the interface
to recognize primitive records based on an option type instead of a
dynamic check of the length of an array.
|
|
so as to reproduce correctly the reduction behavior of existing
projections, i.e. delta + iota. Make [projection] an abstract datatype
in Names.ml, most of the patch is about using that abstraction.
Fix unification.ml which tried canonical projections too early in
presence of primitive projections.
|
