|
| 1 | +opam-version: "2.0" |
| 2 | +maintainer: "Enrico Tassi < [email protected]>" |
| 3 | +authors: [ "Claudio Sacerdoti Coen" "Enrico Tassi" ] |
| 4 | +license: "LGPL-2.1-or-later" |
| 5 | +homepage: "https://github.com/LPCIC/elpi" |
| 6 | +doc: "https://LPCIC.github.io/elpi/" |
| 7 | +dev-repo: "git+https://github.com/LPCIC/elpi.git" |
| 8 | +bug-reports: "https://github.com/LPCIC/elpi/issues" |
| 9 | + |
| 10 | +build: [ |
| 11 | + ["dune" "subst"] {dev} |
| 12 | + ["dune" "build" "-p" name "-j" jobs] |
| 13 | + [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"} |
| 14 | +] |
| 15 | + |
| 16 | +depends: [ |
| 17 | + "ocaml" {>= "4.08.0" } |
| 18 | + "stdlib-shims" |
| 19 | + "ppxlib" {>= "0.12.0" } |
| 20 | + "menhir" {>= "20211230" } |
| 21 | + "re" {>= "1.7.2"} |
| 22 | + "ppx_deriving" {>= "4.3"} |
| 23 | + "ANSITerminal" {with-test} |
| 24 | + "cmdliner" {with-test} |
| 25 | + "fileutils" {with-test} |
| 26 | + "dune" {>= "2.8.0"} |
| 27 | + "conf-time" {with-test} |
| 28 | + "atdgen" {>= "2.10.0"} |
| 29 | + "atdts" {>= "2.10.0"} |
| 30 | + "odoc" {with-doc} |
| 31 | +] |
| 32 | +synopsis: "ELPI - Embeddable λProlog Interpreter" |
| 33 | +description: """ |
| 34 | +ELPI implements a variant of λProlog enriched with Constraint Handling Rules, |
| 35 | +a programming language well suited to manipulate syntax trees with binders. |
| 36 | + |
| 37 | +ELPI is designed to be embedded into larger applications written in OCaml as |
| 38 | +an extension language. It comes with an API to drive the interpreter and |
| 39 | +with an FFI for defining built-in predicates and data types, as well as |
| 40 | +quotations and similar goodies that are handy to adapt the language to the host |
| 41 | +application. |
| 42 | + |
| 43 | +This package provides both a command line interpreter (elpi) and a library to |
| 44 | +be linked in other applications (eg by passing -package elpi to ocamlfind). |
| 45 | + |
| 46 | +The ELPI programming language has the following features: |
| 47 | + |
| 48 | +- Native support for variable binding and substitution, via an Higher Order |
| 49 | + Abstract Syntax (HOAS) embedding of the object language. The programmer |
| 50 | + does not need to care about technical devices to handle bound variables, |
| 51 | + like De Bruijn indices. |
| 52 | + |
| 53 | +- Native support for hypothetical context. When moving under a binder one can |
| 54 | + attach to the bound variable extra information that is collected when the |
| 55 | + variable gets out of scope. For example when writing a type-checker the |
| 56 | + programmer needs not to care about managing the typing context. |
| 57 | + |
| 58 | +- Native support for higher order unification variables, again via HOAS. |
| 59 | + Unification variables of the meta-language (λProlog) can be reused to |
| 60 | + represent the unification variables of the object language. The programmer |
| 61 | + does not need to care about the unification-variable assignment map and |
| 62 | + cannot assign to a unification variable a term containing variables out of |
| 63 | + scope, or build a circular assignment. |
| 64 | + |
| 65 | +- Native support for syntactic constraints and their meta-level handling rules. |
| 66 | + The generative semantics of Prolog can be disabled by turning a goal into a |
| 67 | + syntactic constraint (suspended goal). A syntactic constraint is resumed as |
| 68 | + soon as relevant variables gets assigned. Syntactic constraints can be |
| 69 | + manipulated by constraint handling rules (CHR). |
| 70 | + |
| 71 | +- Native support for backtracking. To ease implementation of search. |
| 72 | + |
| 73 | +- The constraint store is extensible. The host application can declare |
| 74 | + non-syntactic constraints and use custom constraint solvers to check their |
| 75 | + consistency. |
| 76 | + |
| 77 | +- Clauses are graftable. The user is free to extend an existing program by |
| 78 | + inserting/removing clauses, both at runtime (using implication) and at |
| 79 | + "compilation" time by accumulating files. |
| 80 | + |
| 81 | +ELPI is free software released under the terms of LGPL 2.1 or above.""" |
| 82 | +url { |
| 83 | + src: |
| 84 | + "https://github.com/LPCIC/elpi/releases/download/v1.19.5/elpi-1.19.5.tbz" |
| 85 | + checksum: [ |
| 86 | + "sha256=033f1e86d155a53bc1908fd5ee8bff007bc924866b5cd066a053bce154635715" |
| 87 | + "sha512=ddf0c7e1a3ed9b8d9be765e96c937f4b35ebefef0aeeef77bb05b1e4a5ed78c5cc34bc37a486ca6855ac5af8f038dbdbab361d0c210b5f8115cbf1c254136252" |
| 88 | + ] |
| 89 | +} |
| 90 | +x-commit-hash: "f27441e35eff9379b1c1839ee165ad533759e79d" |
0 commit comments