coq-of-ocaml

Compile a subset of OCaml to Coq
IN THIS PACKAGE
Empty package map
  • 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 than OCaml 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 the open 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 of monadic_bind), monadic_let_returns, monadic_rets and monadic_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 the cast_exists axiom in proofs.

  • Name the arguments of the signatures.

  • Rename obj_magic as cast.

  • 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 by Include (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 in match.

  • 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 of Type (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)