Claimr — a constraint logic programming language

Claimr is a constraint logic programming language implemented in Rust, inspired by Prolog III and similar constraint logic programming systems. It combines logical reasoning with constraint solving, allowing for expressive, declarative programs.

The project was originally called Claim; it was renamed to Claimr because claim is already taken on crates.io. Source files use the .claimr extension.

Features

• Prolog-like syntax for facts and rules
• Constraint solving integrated into the logic programming paradigm
• First-class constraints usable in facts, rules, and queries
• Exact arithmetic — numbers are arbitrary-precision rationals, never floats; 18.5 means exactly 37/2, and + - * / are term constructors usable anywhere a term goes (as in Prolog III)
• Implication syntax ({ … } => head.) as syntactic sugar
• Quoted atoms ('situation:frame-in-spec') — any content as an atom; identity is content, quoting is spelling, print-back quotes exactly when needed
• Lists as a constraint domain — Prolog III tuples <a, b, c>, the cons pattern <H> . T, the length |L| as a number in the constraint store, and concatenation X . Y as a constraint that runs in both directions (docs/design/2026-11-09-lists-as-a-constraint-domain.md)
• Strings as character lists ("abc" is <a, b, c>), atom_chars/2 as a delayed constraint, and the type relations number/1, atom/1, list/1 (docs/reference/builtins.md)
• Control in bodies — disjunction A ; B, if-then-else C -> T ; E and negation \+ G, decided only on a ground condition so an answer is never a guess (docs/design/2026-11-09-negation-disjunction-and-if-then-else.md)
• Aggregation — the list comprehension <T | Body>, counts as its length |<T | Body>|, and the exact sum relation sum(L, S) (docs/design/2026-11-09-aggregation-list-comprehensions-and-sum.md)
• A REPL (claimr, claimr -i file) with Prolog-style answer stepping
• Machine-readable output (claimr --json): one JSON document per query, structured diagnostics — a pinned contract for programmatic consumers (docs/reference/json-output.md)
• Explanations (claimr --explain, :explain in the REPL): each answer with its proof tree — the clauses, by position and text, and the constraint instances that derived it (docs/design/2026-11-09-explanations-of-answers.md)
• Tabling (:- table ancestor/2.): declared predicates memoise their ground answers, so transitive closures terminate on cyclic data in either direction of recursion and give each answer once (docs/design/2026-11-10-tabling-for-recursive-rules.md)
• A step limit (claimr --steps N, :steps N): a budget of resolution steps for the whole query, reached as a runtime error that names the goal — an untabled recursion over cyclic data is reported, never a hang (docs/design/2026-11-11-step-limit-for-queries.md)
• Parser generated with rustemo, an LR parser generator for Rust — the grammar file is the single source of truth for the syntax, and syntax errors carry line/column positions
• Highlight tokens (highlight::line_tokens): error-tolerant, line-based lexing in claimr's own vocabulary, for editors and UIs

Current status: the parser (src/parser/), the evaluator (src/eval/: SLD resolution over rational trees with first-argument indexing and tabling, =/!= on terms, lists, strings, control constructs, comprehensions, answers in solved form projected onto the query, explanations), the linear constraint solver (src/solver/: exact rational simplex, attribute terms such as age(X), list lengths, delayed non-linear products), and the REPL are implemented. Open: non-linear and finite-domain constraints, explanations of failure. The changelog lists what each release added.

Grammar

The authoritative grammar is src/parser/claimr.rustemo; docs/reference/grammar.md is an EBNF view of it. The top-level shape:

program        ::= { clause }
clause         ::= fact | rule | constraint_fact | constraint_rule | implication | query | directive

fact           ::= atom "."
rule           ::= atom ":-" body "."
constraint_fact ::= "{" constraint_expr "}" "."
constraint_rule ::= atom ":-" body_with_constraints "."
query          ::= "?-" (body_with_constraints | "{" constraint_expr "}") "."
implication    ::= "{" constraint_expr "}" "=>" atom "."
directive      ::= ":-" identifier indicator { "," indicator } "."   (* `:- table ancestor/2.` *)
indicator      ::= name "/" number

body           ::= alt [ ";" body ]              (* `;` right-assoc, `->` then `,` tighter *)
alt            ::= conj [ "->" conj ]
conj           ::= goal { "," goal }
goal           ::= atom | "{" constraint_expr "}" | "\+" goal | "(" body ")"

constraint_expr ::= constraint_term { "," constraint_term }
constraint_term ::= expr relop expr
relop           ::= "=" | "!=" | "<" | ">" | "<=" | ">="

expr           ::= expr ("+" | "-") expr | expr ("*" | "/") expr | "-" expr
                 | "(" expr ")" | name | number | atom | variable
                 | tuple | expr "." expr | "|" expr "|" | string
tuple          ::= "<" [ args ] ">" | "<" expr "|" body ">"   (* a list comprehension *)

name           ::= identifier | quoted_atom

Arithmetic operators are term constructors, usable anywhere a term goes (Prolog III style); % starts a comment that runs to the end of the line. Quoted atoms ('situation:frame-in-spec', backslash escapes) admit any content as an atom — identity is content, quoting is spelling. Lists are Prolog III tuples: <> is the empty list, <a, b, c> a list, and <a, b> . T the chain a, b then T (the cons pattern in a head: member(X, <X> . T).); answers print lists the same way. |L| is the length of L, a number in the constraint store: { |L| >= 2 } is an ordinary linear constraint, and a length that becomes determined makes its list a tuple of fresh variables ({ |L| = 3 } answers L = <_1, _2, _3>). X . Y is the concatenation of two lists: with a known left operand it is the chain, with an open one a constraint that completes as soon as |X| is known, so last(L, X) :- { L = F . <X> }. and the two-clause reverse run in both directions. A string "abc" is the list of its characters <a, b, c>, not a type of its own; atom_chars(A, L) bridges an atom and its characters as a delayed constraint, and number/1, atom/1, list/1 are type relations with Prolog III's semantics — the only built-in predicates (docs/reference/builtins.md). :- table ancestor/2. declares a tabled predicate: its calls are answered from a table of its ground answers, computed once over the program, so ancestor(X, Z) :- ancestor(X, Y), parent(Y, Z). terminates on a cyclic parent graph and answers each ancestor once (examples/tabling.claimr).

Examples

See examples/socrates.claimr for a complete program; the integration tests parse every file under examples/.

% Facts and rules
human(socrates).
mortal(X) :- human(X).

% Constraints — exact rational arithmetic, usable in terms and constraints
{ age(socrates) > 70 }.
eligible(X) :- { age(X) >= 18 }.
average(X, Y, (X + Y) / 2).
{ X + Y = 10, 2*X - Y >= 1/3 }.

% Implication sugar
{ age(X) >= 18 } => eligible(X).

% Queries
?- mortal(socrates).
?- eligible(alice), { age(alice) >= 18 }.

Installation

Prerequisites

• Rust 1.85 or newer (edition 2024) — install via rustup

Building from source

git clone https://github.com/a1v0lut10n/claimr.git
cd claimr
cargo build --release
cargo test

Usage

# Run a program: each `?-` query is answered in order
cargo run -- examples/family.claimr

# Or, after `cargo install --path .`
claimr path/to/program.claimr
claimr --limit 5 program.claimr    # cap answers per query (unlimited by default)
claimr --steps 100000 program.claimr  # stop a query that takes more than N resolution steps with an error (unlimited by default)
claimr --json program.claimr       # one JSON document per query (docs/reference/json-output.md)
claimr --explain program.claimr    # each answer with its proof tree: the clauses and constraints that derived it
claimr --parse program.claimr      # dump the parsed clauses instead of running
claimr                             # the interactive loop
claimr -i program.claimr           # run the program, then continue interactively

Interactively, you type claimr syntax exactly as in a file — ?- goals. is answered, any other clause (a fact, a rule, a { … }. constraint) is added to the session — and answers are stepped Prolog-style: ; for the next one, Enter to stop.

$ claimr
claimr> human(socrates).
claimr> human(plato).
claimr> mortal(X) :- human(X).
claimr> ?- mortal(W).
W = socrates ;
W = plato.
claimr> eligible(X) :- { age(X) >= 18 }.
claimr> ?- eligible(bob).
age(bob) >= 18.
claimr> :load examples/family.claimr
...
claimr> :quit

A pipe on stdin drives the same loop: printf '?- p(X).\n;\n' | claimr.

Answers are printed in solved form, one per line, true when nothing remains to say and false when a query has no answers. Constraints that remain open are part of the answer:

?- grandparent(tom, Who).
Who = ann
Who = pat
?- { X + Y = 10, X - Y = 2 }.
X = 6, Y = 4
?- average(3, 4, A).
A = 7/2
?- eligible(alice).
age(alice) >= 18
?- { X > 3 }, { X < 5 }, { X != 4 }.
X > 3, X < 5, X != 4
?- p(A).                     % p(X) :- { X = Y + Z, Y > 0, Z > 0 }.
A > 0
?- { X != Y }, same(X, f(Z)), same(Y, f(W)).
X = f(Z), Y = f(W), Z != W
?- omega(X).
X = f(X)

Answers are the store projected onto the query: internal variables are eliminated (Gaussian substitution and Fourier–Motzkin), redundant constraints dropped, and what remains is printed in solved form.

As a library:

use claimr::{parse_program, Program};

let clauses = parse_program("human(socrates).\nmortal(X) :- human(X).\n?- mortal(W).\n")?;
let program = Program::compile(&clauses)?;
for query in program.queries() {
    for answer in program.solve(query) {
        println!("{answer}"); // W = socrates
    }
}

Diagnostics are GCC-style file:line:column: message for syntax errors (structured JSON objects under --json); load errors (an unsatisfiable set of constraint facts) and runtime errors (a non-linear constraint still undetermined at answer time — Claimr never approximates) name the file and the query:

$ claimr broken.claimr
broken.claimr:1:21: Expected one of Neq, Le, Ge, Comma, RParen, RBrace, Eq, Lt, Gt.
$ claimr nonlinear.claimr
nonlinear.claimr: in `?- { Y = X * Z }.`: non-linear constraint `X * Z` is still undetermined; claimr does not approximate (evaluator stage 3 supports linear constraints only)

Project layout

claimr/
├── Cargo.toml
├── CHANGELOG.md         # what each release added
├── build.rs             # generates the parser from the grammar (rustemo)
├── src/
│   ├── lib.rs           # public API: parse_program, parse_clause, ParseError
│   ├── ast.rs           # AST types
│   ├── number.rs        # exact rational Number type (no floats)
│   ├── parser/
│   │   ├── claimr.rustemo       # THE grammar (authoritative)
│   │   ├── claimr_actions.rs    # semantic actions: productions -> ast
│   │   └── mod.rs               # includes the generated parser (OUT_DIR)
│   ├── eval/            # evaluator: store (heap, trail, dif, numeric glue), compile, SLD machine, tables, projection, answers
│   ├── solver/          # exact linear solver: delta-rationals, linear expressions, simplex
│   ├── highlight.rs     # error-tolerant line lexer for editors and UIs
│   ├── json_out.rs      # the --json output writer (pinned contract)
│   ├── repl.rs          # the interactive loop
│   └── main.rs          # `claimr` CLI: run a program (--json, --explain, --limit, --steps), --parse, or the REPL
├── examples/            # sample .claimr programs (parsed by the tests; *.answers = golden runs)
├── tests/               # integration tests
└── docs/                # documentation workflow (see docs/README.md)
    ├── reference/grammar.md
    ├── journal/  tasks/  design/  architecture/  inbox/
    └── incubation/  catalyst/

Development

cargo build                                # also regenerates the parser if the grammar changed
cargo test
cargo clippy --all-targets -- -D warnings

To change the language: edit src/parser/claimr.rustemo, then adjust src/parser/claimr_actions.rs (rustemo appends stubs for new productions and preserves your edits), add an example under examples/, and update the EBNF view in docs/reference/grammar.md.

Documentation, decision records, and the development journal follow the aivolution documentation workflow — see docs/README.md. Branches are named <type>/CLM-NNNN-short-name; docs/NEXT-TICKET holds the next free ticket number.

License

This project is licensed under the Apache License 2.0.

Copyright 2025-2026 Hans Van Wesenbeeck (hvw@aivolution.ch)

Contributing

Contributions are welcome — open a Pull Request:

1. Fork the repository
2. Create your feature branch (git checkout -b feature/CLM-NNNN-amazing-feature)
3. Commit your changes
4. Push to the branch and open a Pull Request