3.0.0

CHANGES:

Requires Menhir 20211230 and OCaml 4.13 or above.

• Language:

  • A functional predicate is a predicate that does not leave choice points
    for any of its calls. A functional predicate can have preconditions, eg
    map is functional if the higher order argument also is. Functional
    predicates (with preconditions) can be miscalled, in that case they behave
    as relations.
  • The matching operator used for input arguments is now also available as a
    builtin predicate named pattern_match.

• API:

  • New Utils.ground_check and Utils.cmp_term (already available as builtins)
  • Change Constants.declare_global_symbol takes an optional variant argument.

• Parser:

  • The fprop keyword is akin to prop but signals the predicate is functional
  • The :functional attribute flags predicates as functional (equivalent to func ...).
  • Dedicated syntax for functional signatures:
    func name(comma_sep(types_of_inputs)* [-> comma_sep(types_of_outputs*)].
    Example: The signature of map is func map list A, (func A -> B) -> list B
  • New [external] symbol name : type [= "variant"] is a synonim of type and can be
    used to ascribe a type to a symbol. External symbols must be matched by
    a declaration in OCaml, and when the symbol is overloaded the variant
    label is used for the matching (additionally to the name).

• Compiler:

  • The type checker is in charge of resolving all symbols, overloaded or not,
    to a Symbol.t datatype that gathers the Loc.t where it is defined
    (and it can be defined at multiple places, e.g. OCaml + Elpi, or twice
    in Elpi). This data can be used to implement jump-to-def and the like in
    modern UIs.
  • The determinacy_checker statically analyzes whether a predicate labeled
    as functional adheres to its signature.
  • The elaboration of {spilling} has been moved to a dedicated file.
  • CHR rules are typechecked (finally)
  • Macros are typechecked. This paves the way to make them live in name
    spaces and possibly globally available, but it is not implemented yet.

• Runtime:

  • Builtin predicates now have a dedicated node when they are part of the
    Elpi language, i.e. Cut, And, Impl, RImpl, Pi, Sigma, Eq, Match, Findall,
    Delay.
  • Symbols part of the Elpi language (other than the builtins) also have
    a dedicated status, i.e. As, Uv, ECons, ENil although As and Uv do not
    have a dedicated node in the AST, while ENil and ECons do have it.