| Commit message (Collapse) | Author | Age |
|---|
| ... | |
| | |
|
| |
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
| |
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.
|
| |
|
|
| |
Involves changing the [mind_finite] field in the kernel from a bool to the trivalued type [Decl_kinds.recursivity_kind]. This is why so many files are (unfortunately) affected. It would not be very surprising if some bug was introduced.
|
| |
|
|
|
|
|
|
|
|
|
| |
Now kernel/indtypes builds the corresponding terms (has to be trusted)
while translate_constant just binds a constant name to the
already entered projection body, avoiding the dubious "check"
of user given terms. "case" Pattern-matching on primitive records is
now disallowed, and the default scheme is implemented using
projections and eta (all elimination tactics now use projections
as well). Elaborate "let (x, y) := p in t" using let bindings
for the projections of p too.
|
| |
|
|
|
|
|
|
|
|
|
| |
It's possible that I should have removed more "allows", as many
instances of "foo allows to bar" could have been replaced by "foo bars"
(e.g., "[Qed] allows to check and save a complete proof term" could be
"[Qed] checks and saves a complete proof term"), but not always (e.g.,
"the optional argument allows to ignore universe polymorphism" should
not be "the optional argument ignores universe polymorphism" but "the
optional argument allows the caller to instruct Coq to ignore universe
polymorphism" or something similar).
|
| | |
|
| |
|
|
|
|
|
|
|
|
|
| |
I'm not quite sure why, but I'm pretty sure it's not. Rather, in
"allowing for foo" and "allowing to foo", "foo" modifies the sense in
which someting is allowed, rather than it being "foo" that's allowed.
"Allowing fooing" generally works, though it can sound a bit awkward.
"Allowing one to foo" (or "Allowing {him,her,it,Coq} to foo") is always
acceptable, in-as-much as it's ok to use "one".
I haven't touched the older instances of it in the CHANGES file.
|
| |
|
|
|
|
|
|
|
|
|
|
| |
- realargs: refers either to the indices of an inductive, or to the proper args
of a constructor
- params: refers to parameters (which are common to inductive and constructors)
- allargs = params + realargs
- realdecls: refers to the defining context of indices or proper args
of a constructor (it includes letins)
- paramdecls: refers to the defining context of params (it includes letins)
- alldecls = paramdecls + realdecls
|
| |
|
|
|
|
|
| |
These options no longer have any impact on the way proofs are loaded. In
other words, loading is always lazy, whatever the options. Keeping them
just so that coqc dies when the user prints some opaque symbol does not
seem worth it.
|
| |
|
|
| |
problem with hashconsing at the same time. This fixes bug# 3302.
|
Pierre Letouzey
Guillaume Melquiond
Maxime Dénès
Nickolai Zeldovich
Matthieu Sozeau
Pierre-Marie Pédrot
Matthieu Sozeau
Enrico Tassi
Arnaud Spiwack
Jason Gross
Hugo Herbelin