···11+opam-version: "2.0"
22+maintainer: "Enrico Tassi <enrico.tassi@inria.fr>"
33+authors: [ "Claudio Sacerdoti Coen" "Enrico Tassi" ]
44+license: "LGPL-2.1-or-later"
55+homepage: "https://github.com/LPCIC/elpi"
66+doc: "https://LPCIC.github.io/elpi/"
77+dev-repo: "git+https://github.com/LPCIC/elpi.git"
88+bug-reports: "https://github.com/LPCIC/elpi/issues"
99+1010+build: [
1111+ ["dune" "subst"] {dev}
1212+ ["dune" "build" "-p" name "-j" jobs]
1313+ [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"}
1414+]
1515+1616+depends: [
1717+ "ocaml" {>= "4.08.0" }
1818+ "stdlib-shims"
1919+ "ppxlib" {>= "0.12.0" }
2020+ "menhir" {>= "20211230" }
2121+ "re" {>= "1.7.2"}
2222+ "ppx_deriving" {>= "4.3"}
2323+ "ANSITerminal" {with-test}
2424+ "cmdliner" {with-test}
2525+ "dune" {>= "2.8.0"}
2626+ "conf-time" {with-test}
2727+ "atdgen" {>= "2.10.0"}
2828+ "atdts" {>= "2.10.0"}
2929+ "odoc" {with-doc}
3030+]
3131+synopsis: "ELPI - Embeddable λProlog Interpreter"
3232+description: """
3333+ELPI implements a variant of λProlog enriched with Constraint Handling Rules,
3434+a programming language well suited to manipulate syntax trees with binders.
3535+3636+ELPI is designed to be embedded into larger applications written in OCaml as
3737+an extension language. It comes with an API to drive the interpreter and
3838+with an FFI for defining built-in predicates and data types, as well as
3939+quotations and similar goodies that are handy to adapt the language to the host
4040+application.
4141+4242+This package provides both a command line interpreter (elpi) and a library to
4343+be linked in other applications (eg by passing -package elpi to ocamlfind).
4444+4545+The ELPI programming language has the following features:
4646+4747+- Native support for variable binding and substitution, via an Higher Order
4848+ Abstract Syntax (HOAS) embedding of the object language. The programmer
4949+ does not need to care about technical devices to handle bound variables,
5050+ like De Bruijn indices.
5151+5252+- Native support for hypothetical context. When moving under a binder one can
5353+ attach to the bound variable extra information that is collected when the
5454+ variable gets out of scope. For example when writing a type-checker the
5555+ programmer needs not to care about managing the typing context.
5656+5757+- Native support for higher order unification variables, again via HOAS.
5858+ Unification variables of the meta-language (λProlog) can be reused to
5959+ represent the unification variables of the object language. The programmer
6060+ does not need to care about the unification-variable assignment map and
6161+ cannot assign to a unification variable a term containing variables out of
6262+ scope, or build a circular assignment.
6363+6464+- Native support for syntactic constraints and their meta-level handling rules.
6565+ The generative semantics of Prolog can be disabled by turning a goal into a
6666+ syntactic constraint (suspended goal). A syntactic constraint is resumed as
6767+ soon as relevant variables gets assigned. Syntactic constraints can be
6868+ manipulated by constraint handling rules (CHR).
6969+7070+- Native support for backtracking. To ease implementation of search.
7171+7272+- The constraint store is extensible. The host application can declare
7373+ non-syntactic constraints and use custom constraint solvers to check their
7474+ consistency.
7575+7676+- Clauses are graftable. The user is free to extend an existing program by
7777+ inserting/removing clauses, both at runtime (using implication) and at
7878+ "compilation" time by accumulating files.
7979+8080+ELPI is free software released under the terms of LGPL 2.1 or above."""
8181+url {
8282+ src:
8383+ "https://github.com/LPCIC/elpi/releases/download/v1.19.0/elpi-1.19.0.tbz"
8484+ checksum: [
8585+ "sha256=beb2c77e071d559952e438f47301d4fc0eae94bb692ccc86338398e595c37334"
8686+ "sha512=b8c9c5f57251e70ffa30508dbd7c50017dddff92a6711805149933f40f2b59db4f5335e8db717fb80917384d210d889d289d3881b328275011159aab2c61fb25"
8787+ ]
8888+}
8989+x-commit-hash: "ed314e2940e7b49d04e8c363862e32a33d34bb30"