Self-contained unit tests using let + mocks. A module rebinds forward-declared primitives to mock values via run-on-entry, turning formal expressions into computable self-tests — only when loaded as the entry point.
"""
Demo: Entry Mocks
Scenario: Self-contained unit tests using let + mocks. A module rebinds
forward-declared primitives to mock values via run-on-entry, turning
formal expressions into computable self-tests — only when loaded as the
entry point.
"""
import logging
import os
import sys
from parseltongue import load_main
def pltg_print(_system, *args):
print(*[str(a).replace("\\n", "\n") for a in args])
return True
def print_facts(system):
for name, fact in system.facts.items():
print(f" {name} = {fact.wff}")
return True
def print_theorems(system):
for t in system.list_theorems():
print(f" {t}")
return True
def assert_true(system, label, value):
status = "PASS" if value is True else f"FAIL (got {value})"
print(f" [{status}] {label}")
return True
def mock_succ(_system, x):
return x + 1
EFFECTS = {
"print": pltg_print,
"print-facts": print_facts,
"print-theorems": print_theorems,
"assert-true": assert_true,
"mock-succ": mock_succ,
}
if __name__ == "__main__":
plog = logging.getLogger("parseltongue")
plog.setLevel(logging.WARNING)
handler = logging.StreamHandler(sys.stdout)
handler.setFormatter(logging.Formatter(" [%(levelname)s] %(message)s"))
plog.addHandler(handler)
os.chdir(os.path.dirname(__file__))
# Scenario 1: demo.pltg imports math — math's self-test is skipped
print("=" * 60)
print("Scenario 1: demo.pltg imports math")
print("=" * 60)
load_main("demo.pltg", EFFECTS)
# Scenario 2: math.pltg as entry point — self-test fires
print("\n" + "=" * 60)
print("Scenario 2: math.pltg as entry point (standalone)")
print("=" * 60)
os.chdir(os.path.join(os.path.dirname(__file__), "src"))
load_main("math.pltg", EFFECTS)
print("=" * 60)
; ==========================================================
; Entry Mocks Demo — run-on-entry as self-contained unit test
; ==========================================================
(print "============================================================")
(print "Entry Mocks Demo — run-on-entry self-test with let + mocks")
(print "============================================================")
(print "\n--- Importing math (which imports primitives + axioms) ---")
(print " math's run-on-entry self-test: SKIPPED (not main)")
(import (quote src.math))
(print "\n--- Facts loaded (no test fact — math is not main) ---")
(print-facts)
(print "\n--- Theorems loaded ---")
(print-theorems)
(print "\n============================================================")
(print "math.pltg's run-on-entry self-test did not fire.")
(print "Run math.pltg directly to see let rebind primitives.zero")
(print "(a forward-declared symbol with no body) to 0, making the")
(print "formal expression computable as a unit test.")
(print "============================================================")
; Axioms — imports primitives, defines Peano rules
(import (quote primitives))
(defterm zero primitives.zero :origin "import")
(defterm succ primitives.succ :origin "import")
(defterm equals primitives.equals :origin "import")
(defterm plus primitives.plus :origin "import")
(axiom add-identity (equals (plus ?n zero) ?n) :origin "Peano")
(axiom add-commutative (equals (plus ?a ?b) (plus ?b ?a)) :origin "Peano")
; math.pltg — Reusable module with a self-contained unit test.
;
; Imports primitives (forward-declared, no concrete values),
; defines axioms and derives a theorem — all purely formal.
;
; run-on-entry block rebinds the non-existent primitives
; to concrete mock values via let, turning the formal theorem
; into a computable self-test.
(import (quote primitives))
(import (quote axioms))
; Aliases
(defterm zero primitives.zero :origin "import")
(defterm succ primitives.succ :origin "import")
(defterm equals primitives.equals :origin "import")
(defterm plus primitives.plus :origin "import")
; Theorem: 3 + 0 = 3
(derive three-plus-zero axioms.add-identity
:bind ((?n (succ (succ (succ zero)))))
:using (axioms.add-identity succ zero))
; --- Self-test: only fires when math.pltg is the entry point ---
; primitives are forward-declared (no body). let rebinds them
; to concrete mocks, making the formal theorem computable.
(run-on-entry
(quote (assert-true "add-identity: 5 + 0 = 5"
(let ((primitives.zero 0)
(primitives.plus +)
(primitives.equals =))
(primitives.equals (primitives.plus 5 primitives.zero) 5))))
(quote (print " three-plus-zero evaluates to:"
(let ((primitives.zero 0)
(primitives.succ mock-succ)
(primitives.plus +)
(primitives.equals =))
three-plus-zero)))
(quote (assert-true "three-plus-zero: S(S(S(0))) + 0 = S(S(S(0)))"
(let ((primitives.zero 0)
(primitives.succ mock-succ)
(primitives.plus +)
(primitives.equals =))
three-plus-zero)))
(quote (print " three-plus-zero with replaced zero with 1 evaluates to:"
(let ((primitives.zero 1)
(primitives.succ mock-succ)
(primitives.plus +)
(primitives.equals =))
three-plus-zero))))
; Primitive symbols — forward declarations
(defterm zero :origin "primitive")
(defterm succ :origin "primitive")
(defterm equals :origin "primitive")
(defterm plus :origin "primitive")