reword README

README.md

@@ -1,13 +1,17 @@
 [![Build Status](https://travis-ci.org/LPCIC/elpi.svg?branch=master)](https://travis-ci.org/LPCIC/elpi)
-# ELPI
+# ELPI - Embeddable λProlog Interpreter
 
-ELPI implements a variant of λProlog enriched with Constraint Handling Rules.
+ELPI implements a variant of λProlog enriched with Constraint Handling Rules,
+a programming language well suited to manipulate syntax trees with binders.
 
 ELPI is a research project aimed at providing a programming platform
 for the so called *elaborator* component of an interactive theorem prover.
-ELPI stands for Embeddable Lambda Prolog Interpreter, and indeed it is
-designed to be easily embedded into larger softwares 
-as Coq or Matita.
+
+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.
 
 ELPI is free software released under LGPL vesion 2.1 or above.
 
@@ -82,32 +86,31 @@ to customize its behavior.
 ## What problem does ELPI (try to) solve and how?
 
 The programming language has the following features
-- Native support for variable binding and substitution, via 
-  HOAS embedding of the object language.  The programmer needs
-  not to care about *De Bruijn indexes*.
-- 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 variable binding and substitution, via an Higher Order
+  Abstract Syntax (HOAS) embedding of the object language. The programmer needs
+  not to care about De Bruijn indexes.
+- 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. 
+  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 constraint (suspended goal). A constraint is resumed as soon as
-  relevant variables gets assigned. Suspended constraints can be manipulated
-  by constraint handling rules (CHR). Moreover external constraint solvers
-  can be integrated to support non syntactic constraints.
-  The programmer can declare any set of *constraints that is automatically
-  checked for satisfiability* whenever such set gets updates.
-- Clauses are graftable. The user is free to *extend an existing program* by
+  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
-  "parse time" by accumulating files.
-- Native support for backtracking. To ease implementation of *search*.
+  "compilation" time by accumulating files.
 
 Most of these feature come with λProlog.  Constraints and propagation rules are novel in ELPI.