Ligare

Everything is a term. Everything is a constraint.
File extension: .lig

Official Website

中文版

Ligare is an experimental programming language and compiler written in Rust. It explores a minimal core where values, types, propositions, proofs, functions, data declarations, and macros are all represented as terms constrained by other terms.

This repository contains the compiler, the C backend, the standard library, the formatter, the Markdown documentation generator, and the ligls language server. The compiler is usable for experiments, but the language and package formats are still evolving and should not be treated as a stable release.

The current implementation includes:

• A lexer, parser, type checker, evaluator, formatter, documentation generator, and C backend for .lig source files.
• A package mode driven by ligare.toml, with Cargo-style new/init, build/run/check, update, test, clean, fmt, and doc commands.
• Refinement constraints, proof blocks, structs, enums, pattern matching, modules, generics, compile-time quotation/splicing, and code generation to C.
• A standard library under libs/std, plus the ligls language-server crate under crates/ligls.

The C backend is currently the only registered backend. Some sections below describe design direction as well as implemented syntax; experimental or planned behavior is called out where relevant.

Installation

Build from the repository

The repository pins its Rust toolchain in rust-toolchain.toml:

git clone https://github.com/ligare-lang/ligare.git
cd ligare
cargo build --release
cargo build -p ligls --release

The solver uses a system-installed Z3 by default (for example, libz3-dev on Debian/Ubuntu, z3 from Homebrew on macOS, or the z3 Chocolatey package on Windows). For a self-contained release binary, enable the static-z3 feature (this builds Z3 from source and requires CMake):

cargo build --release --features static-z3
cargo build -p ligls --release --features ligare/static-z3

Debug builds made from this checkout discover libs/std automatically. When using the release binaries from another directory, point the compiler and language server at an absolute standard-library path:

export LIGARE_STD_PATH="$PWD/libs/std"
target/release/ligare --version
test -x target/release/ligls

The C backend also needs a C99-compatible compiler. Set CC when cc is not the desired compiler.

Repository documentation

• README_zh.md is the Chinese version of this overview.
• docs/kernel-judgments.md documents the kernel trust boundary and proof replay rules.
• The documentation site contains guided lessons and CLI/reference pages.

Quick Start

Requirements

• Rust toolchain. The repository includes rust-toolchain.toml, so rustup will select the pinned toolchain automatically.
• A C compiler available as cc when using native output with -o or package builds.

Build and Test

cargo build
cargo test

Run a Source File

cargo run -- tests/fixtures/test.lig
cargo run -- tests/fixtures/test.lig --eval "1 + 2"

cargo run builds the compiler in debug mode. After installing a binary, replace cargo run -- with ligare (or the path to the binary).

Emit C source

cargo run -- --emit-source tests/fixtures/test.lig

Create and build a package

cargo run -- new /tmp/ligare-hello
cargo run -- check --manifest-path /tmp/ligare-hello/ligare.toml
cargo run -- build --manifest-path /tmp/ligare-hello/ligare.toml
cargo run -- run --manifest-path /tmp/ligare-hello/ligare.toml

For the checked-in example package:

cargo run -- build --manifest-path examples/test/ligare.toml
./examples/test/target/debug/test

check validates a package without emitting backend output. clean removes the selected package's target directory:

cargo run -- check --manifest-path examples/test/ligare.toml
cargo run -- clean --manifest-path examples/test/ligare.toml

Format Source

cargo run -- fmt .
cargo run -- fmt --check .

Generate Markdown Docs

cargo run -- doc .
cargo run -- doc . -o docs/api.md

Use the language server

ligls speaks LSP over standard input and output. Build it with cargo build -p ligls --release, then configure your editor to launch target/release/ligls for .lig files. The server uses the same parser, module loader, standard-library discovery, and diagnostics as the compiler.

Standard Library

The standard library is the std package in libs/std. Its public modules include:

std::io                  IO monad and basic input/output
std::async                poll-driven Future computations
std::fmt                 Display-based formatting
std::string              string helpers
std::data::{bool,nat,order,product}
std::mem::{list,vec}     collections and length-indexed vectors
std::collections         HashMap and HashSet
std::hash                 hashing interfaces for hash-based collections
std::fs                   filesystem operations
std::path                 filesystem path values and helpers
std::option              optional values
std::result              success/error values
std::primitive           compiler-provided primitive declarations
std::meta                attributes and compile-time support

For example, a package can import the standard I/O helpers with:

use std::io::print_line

pub def main : IO () :=
  do
    print_line 42

The checkout's debug build searches libs/std by default. An installed or relocated binary needs LIGARE_STD_PATH set to an absolute path; the variable may contain the platform's path-separated list of standard-library roots.

CLI Reference

Usage: ligare [OPTIONS] [FILE]... [COMMAND]

Command or option	Description
ligare <files>	Process one or more .lig files and run top-level checks/evaluations.
--version	Print the Ligare version; -V is also accepted.
--eval <EXPR>	Evaluate an expression after processing the input files.
--emit-source	Emit backend source instead of evaluating or compiling it.
--backend <NAME>	Select a registered backend; c is currently the only backend.
-o, --output <PATH>	Compile generated C into a native executable at PATH.
--release	Build in release mode with -O3 by default and write package artifacts to target/release.
-O, --opt-level <LEVEL>	Override native optimization with 0, 1, 2, 3, s, or z.
new [OPTIONS] PATH	Create a new package directory with ligare.toml and a src entry file; --lib, --bin, --name, and --vcs customize the generated package.
init [OPTIONS] [PATH]	Initialize the current or target directory as a package, preserving existing files; --lib, --bin, --name, and --vcs customize it.
build [PATH]	Build the package found at PATH or the current directory. Build options may follow the subcommand.
run [PATH] [-- ARGS...]	Build and run a binary package, forwarding arguments after --.
check [PATH]	Check a package without emitting backend source or a native executable.
update [NAME] [VERSION]	Refresh ligare.lock, optionally pinning one dependency.
test [PATH]	Run package files whose names end in _test.lig; --manifest-path selects a manifest explicitly.
clean [PATH]	Remove the selected package's target directory.
fmt [--check] [PATH]	Format .lig files, or check whether formatting is needed.
doc [--private] [-o PATH] [PATH]	Generate Markdown documentation from .lig files.

Package commands accept either a project directory or --manifest-path PATH/to/ligare.toml. build, run, and direct source compilation accept --emit-source, --backend, -o, --release, and -O; release and optimization options require native compilation. Use ligare help <COMMAND> for the full command-specific help.

Development package builds default to -O0 with debug information and write artifacts to target/debug. Release builds default to -O3 and define NDEBUG. An explicit --opt-level overrides the profile default; for example, ligare build --release -Os produces a size-optimized release artifact.

Package Manifest

Package builds use ligare.toml:

[package]
name = "test"
version = "0.1.0"
type = "binary"

[dependencies]

Supported package types are binary and lib. Binary packages default to src/main.lig; library packages default to src/lib.lig. If entry is omitted, Ligare infers the package type from the available default entry. Dependencies may point to Git repositories or local paths:

[dependencies]
mathlib = { path = "../mathlib" }
remote_lib = { git = "https://example.com/remote_lib.git", version = "v0.1.0" }

build and run write a ligare.lock file after dependency resolution.

Repository Layout

crates/ligare_ast core term syntax, arena allocation, and desugaring
crates/ligare_front/src/{lexer,parser}.rs  lexer and parser
crates/ligare_kernel core evaluation, constraint checking, inference, and erasure
crates/ligare_prover proof search and elaboration
crates/ligare_solver SMT solving and proof replay
src/compiler/     file/module pipeline, project loading, monomorphization
crates/ligare_backend backend contract and backend-independent planning
crates/ligare_backend_c/src/{c,ir}.rs C code generation and C IR
src/package/      manifest, lockfile, and dependency resolution
libs/std/          standard library package
libs/mathlib/      example math library package
crates/ligare_fmt formatter crate
crates/ligare_doc markdown documentation generator crate
crates/ligls/     experimental language server crate
tests/            integration and regression tests
tests/fixtures/   sample .lig programs used by tests
examples/test/    example Ligare package
docs/             grammar, kernel, and implementation notes

1. Core Philosophy

Ligare is a minimalist programming language. It recognizes only one kind of entity — the Term.
There is no separate "type" syntax, no "type vs. value" dichotomy, and no "program vs. proof" dichotomy.
Everything is a term, and every relationship is a constraint.

2. Terms and Constraints

2.1 Terms

A term is the only existence in the language. Variables, literals, functions, data types, propositions, proofs, macros... all are terms.

2.2 Constraints

Relationships between terms are established through constraints.
a : T means that term a is constrained by term T (i.e., a has type T).
The constraint relationship replaces the "type ascription" found in traditional languages, but constraints themselves are also terms and can be constrained by other terms.

Example

3 : int       -- 3 is constrained by int
int : prop    -- int is constrained by data

2.3 Levels

All terms have a level. Constraint relationships enforce level ordering to prevent Russell-paradox-style self-referential structures.
(Specific level rules will be defined in detail in the formalization section.)

2.4 Naming Conventions

• Constraints / Types: PascalCase (e.g., Nat, Point, LinkedList)
• Functions / Theorems: snake_case (e.g., div, is_sorted, add_node)

3. Meta-Constraints

The language has two universes.

Universe	Meaning	Exists at runtime?
data	The computable data universe; all terms ultimately retained belong here	Yes
prop	The proposition universe, describing logical conditions	No (erased)

theorem is a top-level command for declaring and checking a named inhabitant of a proposition; it is not a constraint or universe. There is no proof P wrapper: by Curry-Howard, a proof of P is simply a term checked directly against P. Proposition terms are erased after checking. sort n classifies every expression at level n, regardless of whether it belongs to data or prop; it is a level classifier, not a third universe.

The indexed forms data n and prop n select the runtime-data and proposition universe at level n; plain data and prop remain available as the base forms. Universe checking assigns a level variable to every term and solves constraints of the form u + k <= v in a Coq-style graph; a positive cycle reports an inconsistent universe.

4. Refinement Constraints (Where Clauses)

Users can define new constraints by refining an existing constraint with a predicate. This is Ligare's way of defining "subtypes."

Syntax

def nat := int where (x => x >= 0)

Interpretation
nat is a new constraint. Any term constrained by nat must:

1. Be constrained by int (which itself is constrained by data);
2. Satisfy the predicate x >= 0.

Usage

def x : nat := 10
#check x : nat       -- passes
#check x : int       -- also passes (nat is a subtype of int)
#check -5 : nat      -- fails: -5 is not >= 0

The compiler automatically demands this proof where needed, or derives it from context.

Multiple refinements can coexist in the same program:

def pos   := int where (x => x > 0)
def even  := int where (x => x % 2 = 0)
def ten   := int where (x => x = 10)

Refinements can also be used inline in function parameters:

def sdiv (a : int) (b : int where (x => x /= 0)) : int := a / b

5. Functions

Functions are defined with def (or func), using curried parameter lists. They can constrain their own parameters via where clauses, forming pre-condition contracts.

Syntax example

def div (a : int) (b : int where (x => x /= 0)) : int := a / b

Proof obligations

• The caller must provide a proof that b /= 0 (or the compiler derives it automatically).
• The function body operates under the guarantee that the parameter constraints hold.

All terms in prop are erased after passing compile-time checks, with zero runtime overhead.

Function with no return type annotation

def id (x : int) := x

Recursive function

def fib (n : int) : int :=
  if n < 2 then n else fib (n - 1) + fib (n - 2)

Recursive definitions must carry termination evidence. The compiler first checks structural recursion; when it cannot prove termination, provide a termination proof, use #[terminating] (an explicitly trusted axiom), or declare the return type as !. ! is an uninhabited runtime type that can be eliminated into any runtime type, but it cannot enter logical propositions.

6. if Expressions and Theorem Introduction

The condition of an if is treated as a proposition. When entering a branch, the branch context automatically introduces a corresponding theorem.

Example

if x > 0 then
  -- a theorem: x > 0 is automatically available here
  -- it can be used to satisfy proof obligations of other constraints
  div 10 x  -- x /= 0 can be automatically derived from x > 0
else
  -- a theorem: not (x > 0) is automatically available here

After compilation, if is still compiled into a simple conditional jump; all proof parts are erased.

7. Proofs and Tactics (Lean 4-style by blocks)

Ligare supports interactive proof construction via by blocks with tactics, inspired by Lean 4.

left = right is propositional equality and may be used as a proof goal or hypothesis. left == right is a runtime comparison whose result has type bool; it is not accepted by equality-rewriting tactics.

Simple proof with exact

#check 5 by
  exact auto : nat

Multi-tactic proof with intro

#check 0 by
  intro
  exact 0 : int -> int

Standalone proof term (no subject)

#check (by
  intro
  exact 0) : int -> int

Available tactics:

• exact <term> — provide a term that satisfies the goal directly
• intro [name ...] — introduce one or more Pi-type hypotheses
• apply <term> — apply a function to reduce the goal
• have <name> := <term> — introduce a lemma
• rw [<evidence>, ...] — use terms that directly inhabit equality propositions
• simp [<evidence>, ...] / simpa — add equality lemmas and finish with the kernel's normalizer
• constructor — split conjunction goals or construct structs
• left / right — choose a branch of a disjunction
• cases <term> — generate Boolean or enum branches
• induction <enum-term> — generate exhaustive structural enum branches
• assumption — close the goal with a matching local hypothesis
• rfl — close a propositional equality goal by reflexivity
• solve — bounded proof search over introductions, local implications, logical connectives, assumptions, and kernel automation
• trivial, decide, norm_num, omega, and linarith — request kernel-checked automatic proof search for the current proposition
• contradiction — eliminate an impossible hypothesis
• change <constraint> / show <constraint> — continue with a definitionally equal goal

The arithmetic tactics are names for the same fail-closed, replayable kernel decision procedure; they do not grant the tactic elaborator any proof authority. For example:

theorem identity : int -> int := by solve

theorem ordered : (a : int) -> a >= a := by omega

theorem symmetric (a b : int) (h : a = b) : b = a := by
  simp [h]

Custom tactics run when the prover reaches them, so they observe the current goal after earlier tactics have changed it. Their first parameter is always TacticContext, which exposes both the current target and local declarations:

#[tactic]
def first_assumption (ctx : TacticContext) : Expr :=
  match ctx with
  | Goal target locals => match locals with
    | NoLocals => Int 0
    | MoreLocals local tail => match local with
      | Local name constraint => Name name

theorem identity : int -> int := by
  intro value
  first_assumption

TacticContext contains target : Expr and a newest-first TacticLocals list. A generated proof expression is desugared in that local scope and then checked by the kernel.

For tactics that transform proof state instead of immediately closing the goal, return TacticScript. Scripts can introduce locals, apply terms, add lemmas, provide exact proofs, and call core or registered tactics:

#[tactic]
def split (ctx : TacticContext) : TacticScript :=
  TacticCall "constructor" NoTacticArgs TacticDone

def Pair : prop := struct
  left : int
  right : bool

def pair : Pair := by
  split
  exact 7
  exact true

The script constructors are TacticExact, TacticApply, TacticIntro, TacticHave, and TacticCall; each carries its following script and ends in TacticDone. An empty string passed to TacticIntro requests an anonymous binder. Call arguments use NoTacticArgs/MoreTacticArgs.

auto is bound to the concrete current proposition and checked by the proof checker; bare auto or membership in prop is not universal evidence. Logical decisions use Proved / Refuted / Unknown: Unknown cannot prove a negation and cannot make an implication antecedent vacuously false. Integer arithmetic proofs construct and replay a linear certificate for every Boolean branch; non-linear multiplication, /, and % conservatively return Unknown.

See docs/kernel-judgments.md for the trust-boundary rules. #[terminating] is an argument-free, explicitly trusted termination axiom.

8. Expressions and Let Bindings

Lambda expressions

fun x => x + 1
fun x y => x + y
fun (x : int) => x + 1
fun a (b : int) => a + b

Let expressions

let x := 5 in x + 3
let x : int := 5 in x
let x := 5 in let y := x + 1 in y * 2

Type annotation

(5 : int)
(5 : nat) by exact true

Function (Pi) types

int -> bool               -- non-dependent arrow
(x : int) -> x            -- dependent arrow

Proposition combinators

∧ P Q    -- conjunction: P ∧ Q
∨ P Q    -- disjunction: P ∨ Q
¬ P      -- negation: ¬P

9. Structs

A struct definition is a constraint — it lives in the prop universe and is erased after type checking. Struct values (constructed instances) live in data and are retained at runtime.

A struct has named fields. It is the product type (∧) of Ligare: all fields exist simultaneously. Since refinement types (where clauses) already handle invariants, structs focus solely on bundling named data.

Syntax

def Point : prop := struct
  x : int
  y : int

Construction

def p : Point := Point.mk 3 4
def q : Point := Point{x := 3, y := 4}
def r : Point := {x := 3, y := 4}

Field projection

#check Point.x p : int
def get_x (pt : Point) : int := Point.x pt

How it works

• Point.mk is an auto-generated constructor that takes field values in order.
• Point{...} initializes a struct by field name; {...} is also allowed when the expected struct type is known.
• Point.x is an auto-generated projector that extracts the named field from a struct value.
• The compiler automatically generates these from the struct definition.
• Field constraints are verified at construction time.

C representation

typedef struct Point {
    int64_t x;
    int64_t y;
} Point;

10. Enum Types

An enum definition is a constraint — it lives in the prop universe and is erased after type checking. Enum values (variant instances) live in data and are retained at runtime.

An enum has named variants, each with optional payload fields. It is the sum type (∨) of Ligare: exactly one variant holds at a time.

10.1 Definition

Enums use the enum keyword, symmetric with struct. Each variant is introduced by |:

-- Simple enumeration (no payload)
def Color : prop := enum
  | Red
  | Green
  | Blue

-- Polymorphic enum with payload
def Option (A : prop) : prop := enum
  | None
  | Some of (val : A)

-- Recursive enum — essential for compiler ASTs
def Expr : prop := enum
  | Lit  of (n : int)
  | Add  of (l : Expr) (r : Expr)
  | If   of (c : Expr) (t : Expr) (e : Expr)

-- Multi-field payload with named parameters
def Result (T : prop) (E : prop) : prop := enum
  | Ok  of (value : T)
  | Err of (error : E)

10.2 Construction

Variant names are constructor functions. They are automatically generated from the enum definition:

def c  : Color          := Color::Red
def x  : Option int     := Option::Some 5
def y  : Option int     := Option::None              -- type annotation needed for inference
def e  : Expr           := Expr::Add (Expr::Lit 1) (Expr::Lit 2)
def ok : Result int str := Result::Ok 42

For no-payload variants like None, the type parameter cannot be inferred from arguments alone — a type annotation (: Option int) provides the necessary constraint for the compiler to resolve A = int.

Variants with refinement-constrained payloads require proof obligations at construction time:

def PosOption : prop := enum
  | Nothing
  | Just of (val : int where (x => x > 0))

def j : PosOption := PosOption::Just 5       -- auto proof: 5 > 0
def k : PosOption := PosOption::Just (-3)    -- compile error: -3 > 0 is false

10.3 Pattern Matching (Elimination)

Enum values are eliminated via match expressions. Each branch covers one variant and binds its payload:

def unwrap_or (opt : Option int) (default : int) : int :=
  match opt with
  | Option::None     => default
  | Option::Some val => val

The final branch may use _ to cover every variant not matched earlier. A whole-branch wildcard does not bind any payloads:

def is_some (opt : Option int) : bool :=
  match opt with
  | Option::Some _ => true
  | _ => false

Theorem introduction — every match branch automatically introduces a theorem that the scrutinee is of that variant, exactly like if branches introduce the condition theorem:

match opt with
| Option::None =>
  -- theorem: opt = Option::None  (available in this branch)
| Option::Some val =>
  -- theorem: opt = Option::Some val  (available in this branch)
  -- if val has a refinement constraint (e.g. val > 0),
  -- that theorem is also available here

This enables safe refinement propagation through match branches:

def safe_div (opt : PosOption) (x : int) : int :=
  match opt with
  | PosOption::Nothing  => 0
  | PosOption::Just val =>
    -- theorem: val > 0 (from PosOption's refinement)
    -- this satisfies div's proof obligation that the divisor is non-zero
    div x val

Exhaustiveness checking — the compiler verifies that every variant of the enum is covered. Missing a variant is a compile-time error.

Nested matches are naturally supported:

def eval (e : Expr) : int :=
  match e with
  | Expr::Lit n      => n
  | Expr::Add l r    => eval l + eval r
  | Expr::If c t e   => if eval c /= 0 then eval t else eval e

10.4 Erasure and Compilation

Enum definitions are prop — erased at compile time. Enum values and match expressions are data — retained at runtime.

The C backend compiles enums to tagged union structs and match to switch statements, achieving zero-overhead representation:

// Option_int (A = int)
typedef struct {
    int tag;          // 0 = None, 1 = Some
    union {
        struct { int64_t val; } Some;
    } data;
} Option_int;

// match opt with | None => 0 | Some val => val + 1
switch (opt.tag) {
case 0: return 0;
case 1: { int64_t val = opt.data.Some.val; return val + 1; }
}

10.5 Structs vs. Enums — Duality

	Struct (product)	Enum (sum)
Logical dual	∧ (all hold)	∨ (one holds)
Construction	Provide all fields	Choose one variant
Elimination	Field projection (.x)	Pattern matching (match)
C representation	Contiguous fields	Tag + union
Universe	definition: prop, value: data	definition: prop, value: data

11. Compile-Time Metaprogramming (experimental)

Ligare can quote source expressions as Expr values, evaluate metaprograms at compile time, and splice the resulting AST back into the program.

Implemented mechanism

-- Quote: converts a code fragment into manipulable AST data
quote { x + 1 }

-- Expression splice: the argument must evaluate to Expr
$(quote { 1 + 2 })

Safety guarantee Spliced expressions are checked against their surrounding constraint. Top-level splices must evaluate to Definitions; generated definitions and instances pass through the normal compiler checks. Functions marked with #[tactic] or #[attr] can extend proof scripts and attributes at compile time.

Metaprogram execution is erased and does not enter the generated runtime program.

12. Top-Level Commands

Ligare programs consist of a sequence of top-level commands:

Command	Description
def <name> <params>? : <type>? := <body>	Define a named term or function
#[instance] + def <name> : <type> := <body>	Register an implicit compile-time instance
#[no_small_int] + def ...	Disable the generated small-integer specialization for this function
theorem <name> <params>? : <type> := <body>	Define a named theorem with a required result type (type-checked, then available as a term)
#check <expr> : <type>	Type-check an expression against a constraint
#eval <expr>	Evaluate an expression and display the result

Implicit instances are declared with #[instance] on a normal definition:

#[instance]
def show_nat : Show nat := Show.mk render_nat

Example program

def nat := int where (x => x >= 0)
def x : nat := 10
theorem x_is_nat : nat := x by
  exact true

#check x : int
#eval x

13. Compilation and Erasure

The compilation process is divided into two major phases:

1. Constraint checking and proof verification
   Perform constraint checking on all terms and verify that all proposition obligations are satisfied.

2. Erasure and code generation
   Retain all terms constrained by data, and remove all terms constrained by prop. The final product is pure, zero-overhead executable code.

14. Summary

Ligare uses the single core concept of "terms constrained by terms" to unify:

• The type system (constraints as terms in prop)
• Propositions and proofs
• Design by contract (refinement types)
• Product types (structs) and sum types (enums) — both as constraints in prop
• Compile-time metaprogramming with checked quote, splice, tactics, and attributes

It pursues the extreme of static safety with zero runtime burden, while maintaining a minimal set of concepts.
This document describes the currently implemented syntax and planned features; formal definitions, operational semantics, and implementation details will be added progressively.