Elpi — Embeddable λProlog Interpreter

Elpi is an embeddable implementation of λProlog extended with Constraint Handling Rules (CHR). It is a logic programming language well suited to manipulate abstract syntax trees with binders and unification variables, the kind of data the elaborator of an interactive theorem prover works with. Elpi is designed to be embedded into larger applications written in OCaml as an extension language, and it comes with an API to drive the interpreter and a foreign function interface (FFI) to add built-in predicates and data types.

This manual describes Elpi’s syntax, its execution model (including CHR), every language feature, the standard library and built-in predicates, the debugging and tracing tools, and the OCaml API used to embed and extend the interpreter. It assumes familiarity with λProlog; the reference for standard λProlog is Programming with Higher-Order Logic, by Miller and Nadathur.

Overview

• Introduction
  • Why Elpi
  • Relation to standard λProlog and to Teyjus
  • How to read this manual
• Getting started
  • Installing Elpi
  • Running a program
  • Editor support

Syntax

• Lexical conventions
  • Comments
  • Identifiers
  • Literals
  • Operators
  • Keywords
  • The reference tokenizer
• Terms
  • Application
  • λ-abstraction
  • Operators
  • Lists
  • Type ascription
  • Naming a subterm with as
  • Braces
• Type declarations
  • Data types
  • Data constructors
  • Type abbreviations
  • Predicate signatures
  • Signature attributes
  • A worked set of declarations
• Inference rules and queries
  • Rules
  • Goals
  • Committing a hypothetical rule
  • Naming a subterm of the head
  • Attributes
  • Queries
• Constraint handling rules
  • The constraint block
  • Rules
  • Sequent patterns
  • Generating a constraint
• File structure and attributes
  • Accumulating files
  • Namespaces
  • Shortening names
  • A library’s public surface
  • Macros
  • A multi-file program
• Rule attributes
  • Grafting
  • Conditional compilation
  • Suppressing the type checker

Semantics

• Elpi = λProlog + CHR
• Logic Programming
  • Elpi vs Prolog
  • Elpi vs λProlog
• Constraints
  • Controlling instantiation
  • Matching, not unifying
  • Suspending and resuming
  • Incompatible constraints
• The constraint store
  • Frozen variables
  • Triggers and clustering
  • Application of CHR rules
  • Symmetric CHR rules
  • Cliques fix what a rule can see
  • A global variable built on CHR
• Formal semantics
  • Abstract syntax
  • Runtime objects
  • The semantics

Language features

• Unification and variables
  • Unification variable inspection
  • The pattern fragment
  • The occur check
  • The wildcard _
• Binders and HOAS
  • Moving under a binder
  • sigma for per-call locals
  • Inspecting the context
  • Restricting a variable’s scope
• Control and cut
  • Cut and disjunction
  • not, if and if2
  • halt and stop
  • Taming backtracking
• Spilling
  • Spilling into a binder
  • Spilling out of a term-level lambda
  • Spilling a conjunction
• Types and type checking
  • Polymorphic predicates
  • Overloading
  • Undeclared constants
• Determinacy checking
  • What a functional signature promises
  • What the checker requires
  • Wrongly called predicates
  • A function that extends the program
  • Signatures as a subtyping relation
  • Functional status of outputs
• Argument indexing
  • The default and :index
  • Which index to use
  • Discrimination trees and hashes
• Pitfalls
  • Misleading precedence of =>
  • Treacherous one-rule anonymous predicates
  • Scope error as a silent failure
  • =!=> and functional predicates
  • Unification variables are not imperative variables

Examples

• Simply-typed λ-calculus
• Hindley-Milner type inference

Libraries

• Built-in predicates
  • Logic, control and inspection
  • Arithmetic
  • Standard data types
  • Regular expressions and randomness
  • Input, output and the file system
  • Typed finite maps
  • Garbage collector and runtime
• The standard library
  • Naming conventions
  • List and option combinators
  • Associative structures

Debugging & tooling

• Debugging and tracing
  • The tracing facility
  • The spy predicate
  • Debugging the parser
  • Conditional debug rules

Embedding and extending

• Embedding and extending Elpi
  • Embedding
  • Extending: a builtin written in OCaml
  • Extending: a quotation
  • Also worth knowing

Reference

• Compatibility with Teyjus, Prolog and legacy Elpi
  • Lexical differences
  • Semantic differences
  • Superseded Elpi keywords
  • Older signature forms
  • The occur check
  • Modules
• Bibliography

API

• elpi