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