package coq-of-ocaml
Install
Dune Dependency
Authors
Maintainers
Sources
sha256=1c6d414ae8e4babfd79f82cb667cdaaf11b4c3b76dc83de4c23f6ee8ec6affff
sha512=4b017b5892ef0c665a5ff5da292ec5cbdd1a103dfb7193553b78d25693787acd359a30028c335b300883d555786d3787258fe7a57d63cd53b94edc6b40e8ffbe
CHANGELOG.md.html
2.5.2 (January 25, 2022)
Various small improvements.
2.5.1 (June 24, 2021)
Improvement of the GADTs support.
2.5.0 (March 30, 2021)
Beginning of support of GADTs without axioms, thanks to a pull-request of @pedrotst https://github.com/clarus/coq-of-ocaml/pull/166.
Upgrade OCaml to the version 4.12, thanks to @lthms.
2.4.1 (March 15, 2021)
Add basic translation of
try ... with
with extensible types (cannot run in Coq but may be extracted to OCaml).Add basic support for matching on extensible types.
Add the attribute
@coq_type_annotation
to generate the type annotation of an expression.Show nicer error messages for errors in the configuration file.
Remove existential types from the modules (except for the first-class modules).
Upgrade OCaml to the version 4.10.
Upgrade Dune to the version 2.8.
2.4.0 (January 11, 2021)
Install the Coq proofs in
CoqOfOCaml
rather thanOCaml
for clarity.Simpler header at the top of the generated files.
Try to import documentation comments from OCaml.
Do not ignore sequences of instructions anymore.
Add support for top-level definitions as
init_module
functions.Add the attribute
@coq_mutual_as_notation
to translate a mutually recursive function as a notation.Add the configuration option
renaming_type_constructor
to rename some type constructors.Add the configuration option
operator_infix
to have notations for the infix operators.Add the configuration option
constant_warning
to disable warnings when converting constants.Add the configuration option
first_class_module_signature_blacklist
to ignore some signatures in the search of a signature name.
2.3.0 (November 3, 2020)
Add support for the OCaml's monadic notation.
Add support for records with polymorphic fields.
Add the attribute
@coq_cast
to force an unsafe cast of a sub-expression.Rename the attribute
@coq_axiom
as@coq_axiom_with_reason
.Add the attribute
@coq_precise_signature
to help to distinguish between ambiguous signatures.Remove the generation of
Import
in Coq and expand the names regardless of theopen
commands, in order to be compatible with local opens.Add support for anonymous sub-signatures.
Generate functors using a type class of the current arguments.
Add the configuration option
merge_returns
.Add the configuration option
merge_types
.Add the configuration options
monadic_lets
(renaming ofmonadic_bind
),monadic_let_returns
,monadic_rets
andmonadic_ret_lets
.Add a
@coq_plain_module
attribute to force a module to be compiled as a plain module.Add the configuration option
renaming_rules
.Add support for generative functors (using functors with a
unit
parameter).Add a mandatory string parameter to the
@coq_axiom
attribute in order to give a reason for the axiom.
2.2.1 (June 19, 2020)
Use a more standard Dune build command by keeping in the source the parser generated by Menhir.
2.2.0 (June 17, 2020)
Ignore unreachable expressions in match cases.
Add configuration to black list errors containing a certain message.
Add configuration to disable exit with error code on some files.
Exit with a non-null code in case of error.
Add configuration for the requires from long ident.
Add configuration to find the type of a polymorphic variant.
Add configuration to blacklist some errors.
Add configuration to blacklist some first-class module paths.
Add configuration to rename some variants.
Add configuration to rename some constructors.
Add configuration for module barriers in record aliases.
Add configuration to escape some value names.
Add configuration to add head suffix in the generated file.
Add configuration to add monadic operators.
Add configuration to specify dependencies required as mli files.
Add configuration to list the required files in a file, together with an import or not.
Add configuration to disable guard or positivity checking.
Add handling of a configuration file.
Add the
@coq_phantom
attribute to force an abstract type declaration to be phantom.
2.1.0 (March 20, 2020)
Add automatic re-ordering of type synonyms in mutual types to generate valid definitions.
Add minimal handling of class types as records.
Ignore type parameters with constraints (like being a sub-type of some variants).
Add a
@coq_struct "param"
attribute to specify the decreasing parameter name of fixpoints.Add a tactic
rewrite_cast_exists_eval_eq
to simplify the use of thecast_exists
axiom in proofs.Name the arguments of the signatures.
Rename
obj_magic
ascast
.Set the primitive projection flag.
Add support for the
with
operator on constructor records.Add an attribute
@coq_match_gadt_with_result
for GADT matches with casts for the results.Do not generate casts for the return values of the match branches with
@coq_match_gadt
.Remove the rarely used
match exception when false
construct for default return value in matches.Add arity annotations for the existentials.
Eliminate phantom types and propagate this erasing.
Inline the application operators
@@
and|>
.Put first-class modules in
Set
, using existentials in impredicative sets.Add a
@coq_match_with_default
to generate a default branch for incomplete matches.Add a
@coq_force_gadt
attribute to force a type to be defined as a GADT (without type parameters).Add basic handling of module alias and typeof in
.mli
files.Add more type annotations on values to better support polymorphic values.
Add better support for include of signatures in
.mli
files.Add support of
open
in.mli
files.Upgrade to Coq 8.11.
Add support for functors inside signatures.
Add a special treatment with no axioms for the matching of algebraic types with existentials which are not GADTs (with the same type parameters for all the constructors).
Add an annotation mechanism for implicits for Coq.
Generate the JSON output in a default file.
Optimize the execution time to find the name of a signature.
Name the type of the records of constructors.
Add an annotation mechanism to generate axioms for the
match
of GADTs.Use
record.(field)
to access record fields.Add an axiom for
assert
.Add basic support for includes of module types with sub-modules.
Add
with
notation for records.Ignore patterns with extensible types.
Replace the generation of
Export
byInclude
(fix).Add support of
include
in first-class module values.Add support of functor definitions.
Add an annotation mechanism
[@axiom]
to ignore the content of some definitions.Use list notation for list values.
Add support for
when
clauses inmatch
.Disable recursivity checks in Coq.
Change the include of signature to preserve the first-class sub-modules.
Define a default value for the extensible types.
Add support for constructors using records as parameters.
Add polymorphic record fields for modules with polymorphic elements.
Compute the shape of a module by only looking at the top-level of definitions.
Add support of functor application.
Use
let
to represent intermediate results in the definition of a first-class module value.Define modules with a named signature as dependent records.
Add changelog file.
Add support for
include
of modules represented as a record.Fix bug on ambiguous detection of first-class module signatures.
Ignore top-level
let () = ...
and the left-hand side of expression sequences... ; ...
.Capitalize generated file names.
Add the notation
record.[field]
to access to records with existential types.Use tuples with primitive projections for the tuples of existential types in first-class modules (notation
[x, y, z]
for the values,[X * Y * Z]
for the types).Only use the value names to infer a module type name to handle destructive type substitutions (
:=
operator).Add support for functor declarations.
Handle
include
in signatures of.mli
files.Wrap records into modules to prevent name collisions with projections.
Add support for polymorphic abstract types in modules.
Put more generated errors as comments to allow partial compilation.
Add support for module declarations with an anonymous signature in
.mli
files (by unfolding the signature).Add support for module type definitions in
.mli
files.Generate inductive type definitions for type definitions as polymorphic variants.
Convert inlined polymorphic variant types to sum types with annotations in comments.
Have a mechanism to lift some value names independently of type names to prevent name collisions.
Use
Set
instead ofType
(may require to use the-impredicative-set
flag to compile generated files).Reduce the number of parenthesis in generated types using the precedence of the type operators.
2.0.0 (December 15, 2019)
First public release financed by Nomadic Labs.