Minor release, optimization round 2

This is a minor release, with some optimizations and minor bug fixes.

Minor release, optimization

This is a very minor release with "low-hanging-fruit" optimization and updated documentation.

Minor release improving coverage and the FFT example

This is a very minor release with improved coverage and with the complete Fast Fourier Transform example, originally from https://github.com/ucsd-progsys/dsolve/blob/master/tests/POPL2008/fft.ml

Minor release facilitating inference in presence of assertions

This is a very minor release, with better inference in presence of positive assertions assert num and assert type, updated tests and documentation.

Great coverage

This release greatly improves coverage / completeness, i.e. the intended types are inferred for more programs. All algorithms got significant improvements, and even the type system definition needed an update.

Changes:

• Syntax sugar for if / eif - then - else and function definitions.
• Constant coefficients syntax for expressions.
• Built-in syntax for run-time failures.
• Many command-line options to control inference.
• Multiple bug fixes and algorithms improvements.
• The flagship AVL trees example now without assertions.
• Many new tests in the examples directory.

Attached is an executable for Linux 3.11 x86_64 (aka. amd64), and a manual, which can also be found in the doc directory.

Rejecting dead code

I attach an executable compiled under AMD64 (aka. x86_64) and Linux 3.11. The manual can also be found in the doc directory.

Changes:

• One or two minor bug fixes; implementation cleanup including the conceptual level (specification).
• Option to reject all programs with dead code.
• Syntax for external with default FFI name.

Min and max relations in the numerical sort

I attach an executable compiled under AMD64 (aka. x86_64) and Linux 3.11. The manual can also be found in the doc directory.

Changes:

• Several bug fixes.
• So-called "opti" relations: k=min(m,n) and k=max(m,n) in the num sort, with general form in concrete syntax min|max(m-k,n-k), resp. min|max(k-m,k-n).
• So-called "subopti" relations k<=max(m,n) and min(m,n)<=k in the num sort, with general form in concrete syntax min||max(m-k,n-k), resp. min||max(k-m,k-n).
• Less confusing syntax: datatype and datacons keywords, existential types.
• Pattern-matching guards when e1 <= e2, where e1 and e2 are expressions of type Num.
• Positive assert clauses, assert num e1 <= e2; ... and assert type e1 = e2; ....
• Flagship example: AVL trees with imbalance of 2 (based on the implementation from OCaml standard library).

OCaml exporting; documentation and bug fixes

I attach an executable compiled under AMD64 (aka. x86_64) and Linux 3.11. The manual can also be found in the doc directory.

Changes:

• Better manual.
• Num, Int, Bool and String as built-in types, exported to their OCaml counterparts. String literals.
• Regular comments (*...*), ignored during lexing, and documentation comments (**...*) preserved in interface and exported code files.
• New syntax for value declarations:
• external let _name_ : _type_scheme_ = "OCaml definition" for providing the definition of the value to use in exported code -- added benefit is that it will be typechecked by OCaml by the call to invargent;
• external _name_ : _type_scheme_ = "_C_name_" for exporting as external, or by convention external _name_ : _type_scheme_ = "_name_" when we are not interested in running the exported code.
• Option -richer_answers to deal with some rare tricky to infer programs.
• Export datatypes without value constructors as types with one constructor (postfix phantom) to avoid problems with injectivity checking.
• Option -keep_assert_false to preserve assert false branches in exported code.
• Multiple bug fixes.

First release.

First release of InvarGenT.
Attached is an executable for Linux 3.11 x86_64 (aka. amd64), and a manual, which can also be found in the doc directory.