Ebfer
=====

<!--
Copyright (c) 2025-2026 Chris Pressey, Cat's Eye Technologies.
This file is distributed under a 2-clause BSD license.  See LICENSES/ dir.
SPDX-License-Identifier: LicenseRef-BSD-2-Clause-X-Ebfer
-->

This document describes Ebfer, a simple pure functional programming
language which has a simple proof language embedded within it.

When examples are given in this document, they are actually runnable
test cases written in [Falderal][] format.  Each indented code block
(generally preceded by a description) represents a test.  All the lines of
the code block up until the `===>` line give the input to be tested; the
text after `===>` gives the expected output.  `???>` gives an expected
error message, which is permitted to be a partial (substring) match.

The proof language that is embedded in Ebfer is called Lome and it is
defined prescriptively in [its own repository](https://codeberg.org/catseye/Lome).

This description of Ebfer will for the most part refer to that
description when necessary, rather than repeating it here.

Modules
-------

An Ebfer module consists of a number of function definitions.

Alongside these function definitions may appear all the components of a
Lome development: proof transformer rules, proofs, and theorems.

In addition, these developments are extended in their scope, so that they
may refer to, and thus prove properties of, the Ebfer functions in the
same module.

Functions
---------

    -> Tests for functionality "Parse Ebfer Module"

    -> Functionality "Parse Ebfer Module" is implemented by
    -> shell command
    -> "python3 bin/ebfer --no-check --no-eval %(test-body-file) && echo 'ok'"

An Ebfer function looks a lot like a Lome rule, but is introduced with
the keyword `fun`.

    fun perim(W, L) => add(mul(W, 2), mul(L, 2))
    ===> ok

Syntax is of course checked when parsing functions.

    fun perim(W, L) => ()
    ???> Expected identifier

Evaluation
----------

    -> Tests for functionality "Evaluate Ebfer Module"

    -> Functionality "Evaluate Ebfer Module" is implemented by
    -> shell command
    -> "python3 bin/ebfer --no-check %(test-body-file)"

When an Ebfer module is evaluated, the function `main` in that module
is evaluated.

    fun main() => add(mul(5,2), mul(6,2))
    ===> 22

When `main` is evaluated it is not given any arguments.

    fun main(X) => add(X, X)
    ???> 

There should be a unique `main` function in the module, in order for it to
be evaluated.

    fun perim(W, L) => add(mul(W, 2), mul(L, 2))
    ???> No unique main function

    fun perim(W, L) => add(mul(W, 2), mul(L, 2))
    fun main() => perim(6,5)
    fun main() => perim(6,7)
    ???> No unique main function

Functions (including `main`, of course) can call other functions in the module.

    fun perim(W, L) => add(mul(W, 2), mul(L, 2))
    fun main() => perim(6,5)
    ===> 22

Evaluating an atom (a term without subterms) in a context where that atom is
bound to a value (such as when the atom is a formal parameter of the called
function being evaluates), evaluates to the value that the atom is bound to.

    fun blain(X) => X
    fun main() => blain(23)
    ===> 23

In a context where the atom is not bound, however, it evaluates to the atom.

    fun blain(Y) => X
    fun main() => blain(23)
    ===> X

Proof-checking
--------------

    -> Tests for functionality "Check Ebfer Module"

    -> Functionality "Check Ebfer Module" is implemented by
    -> shell command
    -> "python3 bin/ebfer --no-eval %(test-body-file)"

An Ebfer module may contain a Lome development, independent
of any Ebfer code.

    rule mul_id_right(mul(X, 1)) => X
    proof
        mul(a, 1)
        *mul_id_right(mul(a, 1))
        a
    qed
    ===> 1/1 proofs verified.

But the real advantage of embedding Lome in Ebfer, is that
Lome proofs about Ebfer functions can be written.

For every function in the program, one or more rules are
made available.  A rule named after the function, suffixed with
`_expand`, can be applied, to expand the function to its definition.

    fun double(X) => mul(2, X)
    rule mul_nihil_right(mul(X, 0)) => 0
    theorem
        double(0) => 0
    proof
        *double_expand(double(0))
        mul(2, 0)
        *mul_nihil_right(mul(2, 0))
        0
    qed
    ===> 1/1 proofs verified.

Providing a concrete value as in the above example results in
a theorem that looks a lot like a unit test.  The advantage over
unit tests is that we don't need to write these proofs on
concrete values.

    fun mulzero(X) => mul(X, 0)
    rule mul_nihil_right(mul(X, 0)) => 0
    theorem
        mulzero(X) => 0
    proof
        *mulzero_expand(mulzero(X))
        mul(X, 0)
        *mul_nihil_right(mul(X, 0))
        0
    qed
    ===> 1/1 proofs verified.

In addition to `_expand`, a rule named after the function, suffixed
with `_contract`, is available to make the reverse transformation.

    fun perim(W, L) => add(mul(W, 2), mul(L, 2))
    rule mul_comm(mul(A, B)) => mul(B, A)
    rule add_comm(add(A, B)) => add(B, A)
    theorem
        perim_comm(perim(W, L)) => perim(L, W)
    proof
        *perim_expand(perim(W, L))
        add(mul(W, 2), mul(L, 2))
        *add_comm(add(mul(W, 2), mul(L, 2)))
        add(mul(L, 2), mul(W, 2))
        *perim_contract(add(mul(L, 2), mul(W, 2)))
        perim(L, W)
    qed
    ===> 1/1 proofs verified.