diff --git a/packages/elpi/elpi.1.20.0/opam b/packages/elpi/elpi.1.20.0/opam new file mode 100644 index 00000000000..5c1aa12ae0f --- /dev/null +++ b/packages/elpi/elpi.1.20.0/opam @@ -0,0 +1,90 @@ +opam-version: "2.0" +maintainer: "Enrico Tassi " +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"} +] + +depends: [ + "ocaml" {>= "4.08.0" } + "stdlib-shims" + "ppxlib" {>= "0.12.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/v1.20.0/elpi-1.20.0.tbz" + checksum: [ + "sha256=95cb590084203a0e5df8b7c82ed5ac05572c7a6577cd36587c97c3942c47b5c0" + "sha512=95c0160d237a5786daff5f4748b9c9c41dc1192fe235c6d60b79febfec56c3673815eb2d7983ea595e54927369a4d60a8a2a6008f7053bc7d7bb1871628f1697" + ] +} +x-commit-hash: "eb195c67dad82f4cdf3eaaeff47b71e541f8ee0b"