Changes

Since OOPSLA release

Usability

* Command line flags are allowed in test metadata.
* Syntax highlighter and file icon for VS Code in `bluejay-language/`.
* Solver timeout is reported by concolic evaluator.
* Parallelism is available to check type statements in parallel instead of in series.
* Interpreter for all three languages (Bluejay, Desugared, Embedded).
* Some simple error messages for type mismatch and abort reasons.
* Delete DBMC, Sato, and Jil-analysis.
* Translation specification is in docs.
* Upgraded to OCaml 5.2.0.

Language

* `singletype` and `list` are type functions and are values themselves.
* Parametrized recursive types with `Mu t a b c. tau`, where `t` is a type function with parameters `a`, `b`, and `c`.
* Sugar for refined function parameters, e.g. `let f (x : int | x == 0) ...`.
* Dependent parameters have `dependent` or `dep` (which is strictly shorthand) keyword preceding them, and no more `letd`.
* Deterministic functions.
* It is a parse error to have patterns after a catchall pattern.
* `val t1 = t2` sugar for `val t1 : singletype t2`.
* `type`, `top`, `bottom`, `singletype`.
* No more type casing.
* Bluejay programs are statement lists.
* Modules and module types.
* Refinement types can optionally name the candidate to then use a nonfunction as the predicate.
* Refinement types use normal curly braces.
* Record types use normal curly braces. The empty record type is written `{:}`.
* `unit` is the type with member `()`.
* `List` renamed to `list`, and `Mu` renamed to `mu`.
* `let%bind x = e1 in e2` is sugar for `bind e1 (fun x -> e2)`.
* Bluejay has `|>` for pipelining.
* `_` allowed as lvalue.
* Use `&&` and `||` for logical binary operations.
* Use `and` instead of `with` for mutually recursive functions.
* No parentheses needed on typed let-expressions.
* Variant declarations use `of` instead of double backtick.
* Single pipe `|` between variant declarations, and pipe is optional before first constructor declaration.
* Embedded target no longer in ANF.

Performance

* Check physical equality of values before checking intensional value equality
* Solver is never loaded.
* Remove unnecessary case in singleton variant generation, so path tree is smaller.
* Logical product of all expressions when solving, and check one expression only.
* Make trivial substitutions before solving to simplify expressions.
* Split variant constructors by recursiveness.
* N-ary branches.
* Skip many solves where possible.
* Simplify expressions.
* Simpler translations.

Implementation

* Use `Cmdliner` for command line arguments.
* Type splaying is allowed, and we stub recursive types to get incompleteness but decidability.
* Assertions for `wrap` in translation to ensure it is optional.
* Match logic is in value.
* Faster state/result/reader monad for concolic evaluator.
* Polyvariadic fixpoint combinator for mutual recursion.
* Lazy environments are used in the interpreter for recursion instead of ref cells.
* Generated functions and polymorphic values have a nonce so that they work with deterministic functions.
* No more path tree: it is indirectly built by sharing expressions amongst targets.
* GADTs almost everywhere to get int/bool typing.
* Concolic values are in the environment, and expressions have no special handling.
* Build expressions as trees before porting to Z3.
* Typed Z3 interface.
* List types are desugared to recursive variants.
* Intersection types are desugared to match types, then embedded normally.
* Full rewrite of translation--it closely mirrors the spec.

Bug fixes

* Modules and records cannot double as each other.
* Division and modulus in Z3 are consistent with OCaml.
* Recursive functions can reference self in their types and are wrapped properly.
* Keywords are valid function arguments--they no longer need to be in parentheses.
* Record types can have labels of same name as that label's type.