v1.9.0

CHANGES:

• Typing:

  • typeabbrev declarations are now taken into account and unfolded
    by the compiler. The type checker refolds abbreviations
    when printing error messages with the following caveat: when two type
    abbreviations can be refolded the last declared one wins.

• Compiler:

  • @macro are no more accepted in types, since typeabbrev provides the
    same functionality.
  • fix clash between builtin names and type names
  • accumulate is idempotent: accumulating the same file a second time
    has no effect.

• FFI:

  • built in predicate are allowed to not assign (not produce a value) for
    output and input-output arguments.
  • input-output arguments are forced to be Conversion.t of type 'a ioarg,
    and recommended to wrap any nested type not able to represent variables
    in ioarg. Eg int option should be int ioarg option ioarg. In this
    way one can safely call these builtins with non-ground terms, such as
    some _, for example to assert the result is not none but without
    providing a ground term such as some 3.
  • MLData declarations for OpaqueData are no more named using a macro
    but rather using a type abbreviation. This can break user code. The fix
    is to substitutie @myopaquetype with myopaquetype everywhere.

• Stdlib:

  • diagnostic data type to be used as an ioarg for builtins that can fail
    with a relevant error message. On the ML side one can used Elpi.Builtin.mkOK
    and Elpi.Builtin.mkERROR "msg" to build its values.
  • std.assert-ok!, std.forall-ok, std.do-ok!, std.lift-ok and
    std.while-ok-do! commodity predicates.
  • All operators for calc (infix _ is _) now come with a type declaration.