[new release] elpi (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 `pred`icates 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.

Author: gares

packages/elpi/elpi.3.0.0/opam

@@ -0,0 +1,90 @@
+opam-version: "2.0"
+maintainer: "Enrico Tassi <[email protected]>"
+authors: [ "Claudio Sacerdoti Coen" "Enrico Tassi" ]
+license: "LGPL-2.1-or-later"
+homepage: "https://github.com/LPCIC/elpi"
+doc: "https://LPCIC.github.io/elpi/"
+dev-repo: "git+https://github.com/LPCIC/elpi.git"
+bug-reports: "https://github.com/LPCIC/elpi/issues"
+
+build: [
+  ["dune" "subst"] {dev}
+  ["dune" "build" "-p" name "-j" jobs]
+  [make "tests" "DUNE_OPTS=-p %{name}%" "SKIP=performance_HO" "SKIP+=performance_FO" "SKIP+=elpi_api_performance"] {with-test & os != "macos" & os-distribution != "alpine" & os-distribution != "freebsd"}
+]
+x-maintenance-intent: ["(latest)"]
+depends: [
+  "ocaml" {>= "4.13.0" }
+  "stdlib-shims"
+  "ppxlib" {>= "0.12.0" & < "0.36.0"}
+  "menhir" {>= "20211230" }
+  "re" {>= "1.7.2"}
+  "ppx_deriving" {>= "4.3"}
+  "ANSITerminal" {with-test}
+  "cmdliner" {with-test}
+  "fileutils" {with-test}
+  "dune" {>= "2.8.0"}
+  "conf-time" {with-test}
+  "atdgen" {>= "2.10.0"}
+  "atdts" {>= "2.10.0"}
+  "odoc" {with-doc}
+]
+synopsis: "ELPI - Embeddable λProlog Interpreter"
+description: """
+ELPI implements a variant of λProlog enriched with Constraint Handling Rules,
+a programming language well suited to manipulate syntax trees with binders.
+
+ELPI is designed to be embedded into larger applications written in OCaml as
+an extension language. It comes with an API to drive the interpreter and 
+with an FFI for defining built-in predicates and data types, as well as
+quotations and similar goodies that are handy to adapt the language to the host
+application.
+
+This package provides both a command line interpreter (elpi) and a library to
+be linked in other applications (eg by passing -package elpi to ocamlfind).
+
+The ELPI programming language has the following features:
+
+- Native support for variable binding and substitution, via an Higher Order
+  Abstract Syntax (HOAS) embedding of the object language. The programmer
+  does not need to care about technical devices to handle bound variables,
+  like De Bruijn indices.
+
+- Native support for hypothetical context. When moving under a binder one can
+  attach to the bound variable extra information that is collected when the
+  variable gets out of scope. For example when writing a type-checker the
+  programmer needs not to care about managing the typing context.
+
+- Native support for higher order unification variables, again via HOAS.
+  Unification variables of the meta-language (λProlog) can be reused to
+  represent the unification variables of the object language. The programmer
+  does not need to care about the unification-variable assignment map and
+  cannot assign to a unification variable a term containing variables out of
+  scope, or build a circular assignment.
+
+- Native support for syntactic constraints and their meta-level handling rules.
+  The generative semantics of Prolog can be disabled by turning a goal into a
+  syntactic constraint (suspended goal). A syntactic constraint is resumed as
+  soon as relevant variables gets assigned. Syntactic constraints can be
+  manipulated by constraint handling rules (CHR).
+
+- Native support for backtracking. To ease implementation of search.
+
+- The constraint store is extensible.  The host application can declare
+  non-syntactic constraints and use custom constraint solvers to check their
+  consistency.
+
+- Clauses are graftable. The user is free to extend an existing program by
+  inserting/removing clauses, both at runtime (using implication) and at
+  "compilation" time by accumulating files.
+
+ELPI is free software released under the terms of LGPL 2.1 or above."""
+url {
+  src:
+    "https://github.com/LPCIC/elpi/releases/download/v3.0.0/elpi-3.0.0.tbz"
+  checksum: [
+    "sha256=424e5a4631f5935a1436093b614917210b00259d16700912488ba4cd148115d1"
+    "sha512=fa54ce05101fafe905c6db2e5fa7ad79d714ec3b580add4ff711bad37fc9545a58795f69056d62f6c18d8c87d424acc1992ab7fb667652e980d182d4ed80ba16"
+  ]
+}
+x-commit-hash: "a7090745b0c582139e91645dbaa1f17e06013f04"