From c5080834403d79b44078f00c4f3106cf0ea27197 Mon Sep 17 00:00:00 2001 From: Claude Date: Sat, 24 Oct 2026 20:32:01 +0000 Subject: [PATCH] Phase 5: sort checking and the argument library - Sort checker: every free name gets one type (individual, proposition, predicate over individuals/properties, property) across node formulas, proof lines, objections and definitions; runs before proof checking - Spec section on sorts; tests for inference and each class of clash - library/arguments/: Aquinas's First Way, the kalam cosmological argument (new, with two objections and replies) and the resurrection argument - examples/: modus ponens and a deliberately invalid argument showing the counterexample output - Gallery, playground, tests and README follow the new layout Co-Authored-By: Claude Opus 5.5 Claude-Session: https://claude.ai/code/session_019WEmxyo9CRKSbjbEdCuJTG --- CMakeLists.txt | 1 + README.md | 12 +- ROADMAP.md | 1 + docs/spec/language.md | 25 +++ examples/affirming_the_consequent.theo | 21 +++ examples/modus_ponens.theo | 20 +++ include/theos/types.hpp | 30 ++++ .../arguments}/aquinas_first_way.theo | 0 library/arguments/kalam.theo | 68 ++++++++ .../arguments}/resurrection.theo | 0 src/core/driver.cpp | 6 +- src/core/types.cpp | 158 ++++++++++++++++++ tests/CMakeLists.txt | 1 + tests/test_binary.cpp | 4 +- tests/test_proofs.cpp | 2 +- tests/test_types.cpp | 62 +++++++ tests/test_validator.cpp | 16 +- tests/web/wasm_smoke.cjs | 2 +- web/app.js | 6 +- web/build-site.sh | 5 +- 20 files changed, 421 insertions(+), 19 deletions(-) create mode 100644 examples/affirming_the_consequent.theo create mode 100644 examples/modus_ponens.theo create mode 100644 include/theos/types.hpp rename {examples => library/arguments}/aquinas_first_way.theo (100%) create mode 100644 library/arguments/kalam.theo rename {examples => library/arguments}/resurrection.theo (100%) create mode 100644 src/core/types.cpp create mode 100644 tests/test_types.cpp diff --git a/CMakeLists.txt b/CMakeLists.txt index 5ad8364..df242e8 100644 --- a/CMakeLists.txt +++ b/CMakeLists.txt @@ -38,6 +38,7 @@ add_library(theos_core STATIC src/core/proof_checker.cpp src/core/site.cpp src/core/truth_table.cpp + src/core/types.cpp src/core/validator.cpp ) target_include_directories(theos_core PUBLIC include) diff --git a/README.md b/README.md index b9c135d..27cdcb4 100644 --- a/README.md +++ b/README.md @@ -79,12 +79,13 @@ See [web/README.md](web/README.md) to build them locally. ## CLI Usage ```sh -theosc check examples/aquinas_first_way.theo -theosc export examples/resurrection.theo --format mermaid -o resurrection.mmd -theosc build examples/resurrection.theo -o resurrection.theos +theosc check library/arguments/aquinas_first_way.theo +theosc check examples/affirming_the_consequent.theo # rejected, with a counterexample +theosc export library/arguments/resurrection.theo --format mermaid -o resurrection.mmd +theosc build library/arguments/resurrection.theo -o resurrection.theos theosc inspect resurrection.theos # decoded argument theosc inspect resurrection.theos --chunks # chunk table and hex view -theosc site examples -o site/gallery # static gallery pages +theosc site library/arguments -o site/gallery # static gallery pages ``` Diagnostics go to stderr as `file:line:col: error: message` with the source line underneath; @@ -102,7 +103,8 @@ theos-engine/ ├── src/wasm/ # WebAssembly entry point for the playground ├── web/ # Playground, gallery styles, site assembly ├── docs/spec/ # Language, proof rules and binary format specifications -├── examples/ # Sample .theo arguments +├── examples/ # Small teaching examples +├── library/ # Formalized arguments (the gallery) ├── fuzz/ # libFuzzer targets and seed corpora └── tests/ # Catch2 unit tests and golden files ``` diff --git a/ROADMAP.md b/ROADMAP.md index a6f4ab3..699ef90 100644 --- a/ROADMAP.md +++ b/ROADMAP.md @@ -263,3 +263,4 @@ Answers to the original open questions (2026-10-24) and decisions made while bui | 2 Binary v2 | done — formulas, proofs and objections are serialized here (M3.4 folded in, since the AST already carries them); padding must be zero so every single-byte corruption is detected (verified by flipping every byte); nesting depth is capped in parser (256) and decoder (512) | | 3 Propositional logic | done — the natural-deduction checker already implements the full rule set (quantifiers, identity, S5, definitions, property variables) because the substitution machinery is shared and the Aquinas example needs first-order proofs to pass; formulas are immutable shared trees rather than hash-consed (structural sharing happens in the binary encoder); 39 exercises plus misuse tests; recursive definitions are rejected so expansion terminates | | 4 Web | done — Emscripten 3.1.74 build with wasm exceptions (embind `check` returning JSON); playground with live verdict, graph, glosses keyed to lines, shareable `#src=` links; `theosc site` gallery with Fitch-style proof rendering; Node and Playwright smoke tests; Pages deployment needs Pages enabled ("GitHub Actions" source) in repository settings | +| 5 First-order logic | done — sort checker (docs/spec/language.md §6) infers one type per free name across nodes, proofs, objections and definitions, and runs before proof checking; `library/arguments/` holds the gallery set (Aquinas, kalam, resurrection) and `examples/` holds teaching examples, including one invalid on purpose | diff --git a/docs/spec/language.md b/docs/spec/language.md index 2b468af..fd574a8 100644 --- a/docs/spec/language.md +++ b/docs/spec/language.md @@ -237,3 +237,28 @@ Warnings: Diagnostics are printed as `file:line:col: error: message`, followed by the source line and a caret under the offending token. Syntax errors stop parsing at the first error; static-rule errors are all reported. + +--- + +## 6. Sorts + +Every name that is not bound by a quantifier or λ has exactly one type across +the whole file (node formulas, proof lines, objections and definitions): + +| Type | How it arises | +|------|---------------| +| individual | used only as an argument, or in an identity | +| proposition | applied to no arguments: `Rain` | +| predicate | applied to arguments: `Moves(y, x)`; argument sorts are individual or property | +| property | a one-place predicate over individuals, which may also appear as an argument: `G(x)` and `Positive(G)` | + +Bound variables have the sort their binder declares (`ind` by default, +`prop` for properties). Errors: + +- a name used with different arities or argument sorts (`P(a)` and `P(a, b)`); +- an individual variable applied as a predicate, or a property variable applied to anything but one individual; +- a predicate of more than one place, or over properties, used as an argument; +- an identity between properties; +- a λ abstracting over anything but an individual. + +A defined name has the type given by its parameters. diff --git a/examples/affirming_the_consequent.theo b/examples/affirming_the_consequent.theo new file mode 100644 index 0000000..6b08b89 --- /dev/null +++ b/examples/affirming_the_consequent.theo @@ -0,0 +1,21 @@ +// Deliberately invalid: `theosc check` rejects it and shows a counterexample +// (Rain = false, Wet = true: the street can be wet without rain). + +argument "Affirming the Consequent" + +axiom Obs = source("Field notes", "p. 4") + +premise P1 grounded_by [Obs] { + text: "If it rains, the street is wet." + formula: Rain -> Wet +} + +premise P2 grounded_by [Obs] { + text: "The street is wet." + formula: Wet +} + +conclusion C1 from [P1, P2] { + text: "It rains." + formula: Rain +} diff --git a/examples/modus_ponens.theo b/examples/modus_ponens.theo new file mode 100644 index 0000000..9d22cb6 --- /dev/null +++ b/examples/modus_ponens.theo @@ -0,0 +1,20 @@ +// The smallest complete argument: two premises and a single rule. + +argument "Modus Ponens" + +axiom Obs = source("Field notes", "p. 4") + +premise P1 grounded_by [Obs] { + text: "If it rains, the street is wet." + formula: Rain -> Wet +} + +premise P2 grounded_by [Obs] { + text: "It rains." + formula: Rain +} + +conclusion C1 from [P1, P2] by imp_e { + text: "The street is wet." + formula: Wet +} diff --git a/include/theos/types.hpp b/include/theos/types.hpp new file mode 100644 index 0000000..cdd7dfc --- /dev/null +++ b/include/theos/types.hpp @@ -0,0 +1,30 @@ +#pragma once + +#include "theos/ast.hpp" +#include +#include +#include + +// Sort checking (docs/spec/language.md §6): every free symbol gets one consistent type +namespace Theos::Types { + +// A free symbol is an individual constant, or a predicate over individuals and properties. +// A property constant is a predicate with one individual argument. +struct Type { + bool predicate = false; + std::vector args; // predicate argument sorts +}; + +using Signature = std::map; + +std::string describe(const Type& t); + +struct Result { + Signature signature; + Diagnostics diagnostics; +}; + +// Checks every formula in the document: nodes, objections, definitions and proof lines +Result check(const AST::Document& doc); + +} // namespace Theos::Types diff --git a/examples/aquinas_first_way.theo b/library/arguments/aquinas_first_way.theo similarity index 100% rename from examples/aquinas_first_way.theo rename to library/arguments/aquinas_first_way.theo diff --git a/library/arguments/kalam.theo b/library/arguments/kalam.theo new file mode 100644 index 0000000..9a26b7b --- /dev/null +++ b/library/arguments/kalam.theo @@ -0,0 +1,68 @@ +// The kalam cosmological argument in its modern form. The step from "has a +// cause" to "has a transcendent cause" is made explicit as premise P3. + +argument "The Kalam Cosmological Argument" by "William Lane Craig, after al-Ghazali" + +axiom Ghazali = source("al-Ghazali, The Incoherence of the Philosophers", "First Discussion") +axiom Craig = source("William Lane Craig, The Kalam Cosmological Argument", "Part II") +axiom ExNihilo = principle("Nothing comes from nothing.") +axiom Gen1 = scripture(protestant, "Genesis 1:1") + +premise P1 grounded_by [ExNihilo] { + text: "Whatever begins to exist has a cause." + formula: forall x. Began(x) -> exists y. Causes(y, x) +} + +premise P2 grounded_by [Ghazali, Craig, Gen1] { + text: "The universe began to exist." + formula: Began(universe) +} + +deduction D1 from [P1, P2] { + text: "Therefore the universe has a cause." + formula: exists y. Causes(y, universe) + proof { + 1. forall x. Began(x) -> exists y. Causes(y, x) premise P1 + 2. Began(universe) premise P2 + 3. Began(universe) -> exists y. Causes(y, universe) forall_e 1 + 4. exists y. Causes(y, universe) imp_e 3, 2 + } +} + +premise P3 grounded_by [Craig] { + text: "A cause of all of space and time is itself beyond space and time." + formula: forall y. Causes(y, universe) -> Transcendent(y) +} + +conclusion C1 from [D1, P3] { + text: "Therefore the universe has a transcendent cause." + formula: exists y. (Causes(y, universe) & Transcendent(y)) + proof { + 1. exists y. Causes(y, universe) premise D1 + 2. forall y. Causes(y, universe) -> Transcendent(y) premise P3 + { [c] + 3. Causes(c, universe) assume + 4. Causes(c, universe) -> Transcendent(c) forall_e 2 + 5. Transcendent(c) imp_e 4, 3 + 6. Causes(c, universe) & Transcendent(c) and_i 3, 5 + 7. exists y. (Causes(y, universe) & Transcendent(y)) exists_i 6 + } + 8. exists y. (Causes(y, universe) & Transcendent(y)) exists_e 1, 3-7 + } +} + +objection O1 against P1 { + text: "Quantum events, such as radioactive decay, seem to begin without a cause." +} + +reply R1 to O1 { + text: "Quantum events arise within a vacuum governed by physical law, which is not nothing; P1 concerns coming into being from nothing." +} + +objection O2 against P2 { + text: "The universe might have an infinite past, so it never began." +} + +reply R2 to O2 { + text: "A series of past events formed by successive addition cannot be actually infinite, since an infinite cannot be traversed one step at a time." +} diff --git a/examples/resurrection.theo b/library/arguments/resurrection.theo similarity index 100% rename from examples/resurrection.theo rename to library/arguments/resurrection.theo diff --git a/src/core/driver.cpp b/src/core/driver.cpp index 25bdee2..c7c7993 100644 --- a/src/core/driver.cpp +++ b/src/core/driver.cpp @@ -1,5 +1,6 @@ #include "theos/driver.hpp" #include "theos/checker.hpp" +#include "theos/types.hpp" #include "theos/parser.hpp" #include "theos/validator.hpp" #include @@ -19,7 +20,10 @@ Result check_source(std::string text, const std::string& path) { result.doc = std::move(*parsed); auto diags = Validator::validate(*result.doc); result.diagnostics.insert(result.diagnostics.end(), diags.begin(), diags.end()); - if (has_errors(result.diagnostics)) return result; // logic checking assumes a well-formed document + if (has_errors(result.diagnostics)) return result; // later stages assume a well-formed document + auto types = Types::check(*result.doc).diagnostics; + result.diagnostics.insert(result.diagnostics.end(), types.begin(), types.end()); + if (has_errors(result.diagnostics)) return result; // logic checking assumes well-sorted formulas auto logic = Checker::check(*result.doc); result.diagnostics.insert(result.diagnostics.end(), logic.begin(), logic.end()); return result; diff --git a/src/core/types.cpp b/src/core/types.cpp new file mode 100644 index 0000000..f6474f9 --- /dev/null +++ b/src/core/types.cpp @@ -0,0 +1,158 @@ +#include "theos/types.hpp" +#include + +namespace Theos::Types { + +std::string describe(const Type& t) { + if (!t.predicate) return "an individual"; + if (t.args.empty()) return "a proposition"; + if (t.args.size() == 1 && t.args[0] == Sort::Ind) return "a property"; + std::string out = "a predicate of ("; + for (size_t i = 0; i < t.args.size(); ++i) out += std::string(i ? ", " : "") + (t.args[i] == Sort::Ind ? "individual" : "property"); + return out + ")"; +} + +namespace { + +bool same(const Type& a, const Type& b) { return a.predicate == b.predicate && a.args == b.args; } + +const Type property{true, {Sort::Ind}}; +const Type individual{false, {}}; + +class Checker { +public: + explicit Checker(const AST::Document& doc) : doc_(doc) {} + + Result run() { + // Definitions fix the type of the symbol they define + for (const auto& d : doc_.definitions) { + Type t{true, {}}; + for (const auto& p : d.params) t.args.push_back(p.sort); + declare(d.id, t, d.span); + } + // Heads first: a symbol applied anywhere is a predicate, which decides how bare uses are read + for (const auto* f : formulas()) collect_heads(*f, {}); + for (const auto& d : doc_.definitions) { + Env env; + for (const auto& p : d.params) env.push_back({p.name, p.sort}); + formula(*d.body, env); + } + for (const auto* f : formulas()) formula(*f, {}); + return {std::move(sig_), std::move(diags_)}; + } + +private: + using Env = std::vector>; + + std::vector formulas() const { + std::vector out; + for (const auto& n : doc_.nodes) { + out.push_back(n.formula.get()); + if (n.proof) proof_lines(n.proof->items, out); + } + for (const auto& d : doc_.dialectics) { + if (d.formula) out.push_back(d.formula.get()); + } + return out; + } + + static void proof_lines(const std::vector& items, std::vector& out) { + for (const auto& item : items) { + if (const auto* line = std::get_if(&item)) out.push_back(line->formula.get()); + else proof_lines(std::get(item).items, out); + } + } + + static std::optional lookup(const Env& env, const std::string& name) { + for (auto it = env.rbegin(); it != env.rend(); ++it) { + if (it->first == name) return it->second; + } + return std::nullopt; + } + + void error(const Span& span, std::string message) { + diags_.push_back({Severity::Error, doc_.file, span, std::move(message)}); + } + + void declare(const std::string& name, const Type& t, const Span& span) { + auto [it, inserted] = sig_.emplace(name, t); + if (!inserted && !same(it->second, t)) { + error(span, "'" + name + "' is used as " + describe(t) + " here but as " + describe(it->second) + " elsewhere"); + } + } + + void collect_heads(const Expr& e, Env env) { + if (e.kind == ExprKind::Atom && !lookup(env, e.name)) heads_.emplace(e.name, e.args.size()); + if (is_binder(e.kind)) env.push_back({e.name, e.sort}); + for (const auto& a : e.args) collect_heads(*a, env); + } + + // Sort of a term in argument position + Sort term(const Expr& t, const Env& env) { + if (t.kind == ExprKind::Lambda) { + if (t.sort != Sort::Ind) error(t.span, "a lambda must abstract over an individual variable"); + Env inner = env; + inner.push_back({t.name, t.sort}); + formula(*t.args[0], inner); + return Sort::Prop; + } + if (auto bound = lookup(env, t.name)) return *bound; + // A free name that is applied somewhere is a property; otherwise an individual + auto head = heads_.find(t.name); + auto def = sig_.find(t.name); + if ((def != sig_.end() && def->second.predicate) || head != heads_.end()) { + const Type expected = def != sig_.end() ? def->second : property; + if (!same(expected, property)) { + error(t.span, "'" + t.name + "' is " + describe(expected) + " and cannot be used as a term"); + return Sort::Prop; + } + declare(t.name, property, t.span); + return Sort::Prop; + } + declare(t.name, individual, t.span); + return Sort::Ind; + } + + void formula(const Expr& e, Env env) { + switch (e.kind) { + case ExprKind::Atom: { + std::vector args; + for (const auto& a : e.args) args.push_back(term(*a, env)); + if (auto bound = lookup(env, e.name)) { + if (*bound != Sort::Prop) error(e.span, "'" + e.name + "' is an individual variable and cannot be applied"); + else if (args != std::vector{Sort::Ind}) error(e.span, "property variable '" + e.name + "' takes one individual"); + return; + } + declare(e.name, Type{true, args}, e.span); + return; + } + case ExprKind::Eq: + for (const auto& a : e.args) { + if (term(*a, env) != Sort::Ind) error(a->span, "identity relates individuals; '" + a->name + "' is a property"); + } + return; + case ExprKind::Symbol: + case ExprKind::Lambda: + error(e.span, "expected a formula, found a term"); + return; + case ExprKind::Forall: + case ExprKind::Exists: + env.push_back({e.name, e.sort}); + formula(*e.args[0], env); + return; + default: + for (const auto& a : e.args) formula(*a, env); + } + } + + const AST::Document& doc_; + Signature sig_; + std::map heads_; + Diagnostics diags_; +}; + +} // namespace + +Result check(const AST::Document& doc) { return Checker(doc).run(); } + +} // namespace Theos::Types diff --git a/tests/CMakeLists.txt b/tests/CMakeLists.txt index 0fb4261..9fe38fe 100644 --- a/tests/CMakeLists.txt +++ b/tests/CMakeLists.txt @@ -13,6 +13,7 @@ add_executable(theos_tests test_lexer.cpp test_parser.cpp test_proofs.cpp + test_types.cpp test_validator.cpp ) target_link_libraries(theos_tests PRIVATE theos_core theos_warnings Catch2::Catch2WithMain) diff --git a/tests/test_binary.cpp b/tests/test_binary.cpp index 37faadf..04e8d09 100644 --- a/tests/test_binary.cpp +++ b/tests/test_binary.cpp @@ -22,7 +22,7 @@ AST::Document load(const fs::path& p) { std::vector valid_sources() { std::vector out; - for (const auto& e : fs::directory_iterator(fs::path(THEOS_SOURCE_DIR) / "examples")) { + for (const auto& e : fs::directory_iterator(fs::path(THEOS_SOURCE_DIR) / "library/arguments")) { if (e.path().extension() == ".theo") out.push_back(e.path()); } out.push_back(fs::path(THEOS_SOURCE_DIR) / "tests/golden/binary/tiny.theo"); @@ -119,7 +119,7 @@ TEST_CASE("Golden binaries are byte-for-byte stable", "[binary][golden]") { } TEST_CASE("Every single-byte corruption is detected", "[binary]") { - const auto bytes = Binary::encode(load(fs::path(THEOS_SOURCE_DIR) / "examples/resurrection.theo")); + const auto bytes = Binary::encode(load(fs::path(THEOS_SOURCE_DIR) / "library/arguments/resurrection.theo")); for (size_t i = 0; i < bytes.size(); ++i) { auto corrupt = bytes; corrupt[i] ^= std::byte{0x20}; diff --git a/tests/test_proofs.cpp b/tests/test_proofs.cpp index 9dd6a1e..9c5ff1c 100644 --- a/tests/test_proofs.cpp +++ b/tests/test_proofs.cpp @@ -459,7 +459,7 @@ TEST_CASE("Quantifier side conditions are enforced", "[proofs][errors]") { "is not an instance"); // an individual variable cannot take a lambda require_error(argument({"forall x. Q(x)"}, "Q(\\y. P(y))", "1. forall x. Q(x) premise P1\n2. Q(\\y. P(y)) forall_e 1"), - "cannot instantiate an individual variable with a lambda"); + "'Q' is used as a predicate of (property) here but as a property elsewhere"); // identity substitution must be faithful require_error(argument({"P(a)", "a = b"}, "P(c)", "1. P(a) premise P1\n2. a = b premise P2\n3. P(c) eq_e 2, 1"), "eq_e needs"); } diff --git a/tests/test_types.cpp b/tests/test_types.cpp new file mode 100644 index 0000000..eec0d9b --- /dev/null +++ b/tests/test_types.cpp @@ -0,0 +1,62 @@ +#include +#include "theos/driver.hpp" +#include "theos/parser.hpp" +#include "theos/types.hpp" + +using namespace Theos; + +namespace { +Types::Result types(const std::string& src) { + auto doc = Parser::parse(src, "t.theo"); + REQUIRE(doc.has_value()); + return Types::check(*doc); +} + +bool has(const Types::Result& r, const std::string& needle) { + for (const auto& d : r.diagnostics) { + if (d.message.find(needle) != std::string::npos) return true; + } + return false; +} + +std::string premise(const std::string& formula) { return "premise P { text: \"\" formula: " + formula + " }\n"; } +} // namespace + +TEST_CASE("Signatures are inferred", "[types]") { + auto r = types(premise("forall x. Moved(x) -> exists y. (Moves(y, x) & y != x)") + premise("Rain") + + "define G(x) := forall F:prop. Positive(F) -> F(x)\n" + premise("Positive(G) & G(g)")); + INFO(r.diagnostics.size()); + REQUIRE(r.diagnostics.empty()); + REQUIRE(Types::describe(r.signature.at("Moved")) == "a property"); + REQUIRE(Types::describe(r.signature.at("Moves")) == "a predicate of (individual, individual)"); + REQUIRE(Types::describe(r.signature.at("Rain")) == "a proposition"); + REQUIRE(Types::describe(r.signature.at("Positive")) == "a predicate of (property)"); + REQUIRE(Types::describe(r.signature.at("g")) == "an individual"); +} + +TEST_CASE("Arity and sort clashes are errors", "[types]") { + REQUIRE(has(types(premise("P(a)") + premise("P(a, b)")), "'P' is used as a predicate of (individual, individual) here but as a property elsewhere")); + REQUIRE(has(types(premise("Positive(G)") + premise("G(a)") + premise("Positive(a)")), "'Positive' is used as a property here but as a predicate of (property) elsewhere")); + REQUIRE(has(types(premise("forall x. x(a)")), "'x' is an individual variable and cannot be applied")); + REQUIRE(has(types(premise("forall F:prop. F(a, b)")), "property variable 'F' takes one individual")); + REQUIRE(has(types(premise("R(a, b)") + premise("Q(R)")), "'R' is a predicate of (individual, individual) and cannot be used as a term")); + REQUIRE(has(types(premise("G(a)") + premise("G = H") + premise("H(b)")), "identity relates individuals")); + REQUIRE(has(types(premise("Q(\\F:prop. F(a))")), "a lambda must abstract over an individual variable")); +} + +TEST_CASE("Proof lines are sort-checked too", "[types]") { + auto r = Driver::check_source(R"( +premise P1 { text: "" formula: forall x. Q(x) } +conclusion C from [P1] { text: "" formula: Q(a) + proof { + 1. forall x. Q(x) premise P1 + 2. Q(a, a) forall_e 1 + 3. Q(a) forall_e 1 + } +} +)", "t.theo"); + REQUIRE_FALSE(r.ok()); + bool found = false; + for (const auto& d : r.diagnostics) found |= d.message.find("'Q' is used as") != std::string::npos; + REQUIRE(found); +} diff --git a/tests/test_validator.cpp b/tests/test_validator.cpp index f2b2b7e..447b90f 100644 --- a/tests/test_validator.cpp +++ b/tests/test_validator.cpp @@ -1,6 +1,7 @@ #include #include #include "theos/driver.hpp" +#include using namespace Theos; @@ -99,11 +100,16 @@ axiom C = scripture(lutheran, "John 1:1") REQUIRE(has(r.diagnostics, Severity::Error, "unknown canon 'lutheran'")); } -TEST_CASE("Examples validate", "[validator][examples]") { - for (const char* name : {"aquinas_first_way", "resurrection"}) { - auto r = Driver::check_file(std::string(THEOS_SOURCE_DIR) + "/examples/" + name + ".theo"); - INFO(Driver::render_diagnostics(r)); - REQUIRE(r.ok()); +TEST_CASE("Library arguments and examples check", "[validator][examples]") { + namespace fs = std::filesystem; + for (const char* dir : {"library/arguments", "examples"}) { + for (const auto& e : fs::directory_iterator(fs::path(THEOS_SOURCE_DIR) / dir)) { + if (e.path().extension() != ".theo") continue; + auto r = Driver::check_file(e.path().string()); + INFO(e.path().string() << "\n" << Driver::render_diagnostics(r)); + // affirming_the_consequent.theo is invalid on purpose + REQUIRE(r.ok() == (e.path().stem() != "affirming_the_consequent")); + } } } diff --git a/tests/web/wasm_smoke.cjs b/tests/web/wasm_smoke.cjs index 14c8cef..8e976f7 100644 --- a/tests/web/wasm_smoke.cjs +++ b/tests/web/wasm_smoke.cjs @@ -8,7 +8,7 @@ const createTheos = require(path.join(__dirname, '../../web/dist/theos.js')); (async () => { const theos = await createTheos(); - const good = JSON.parse(theos.check(fs.readFileSync(path.join(__dirname, '../../examples/aquinas_first_way.theo'), 'utf8'))); + const good = JSON.parse(theos.check(fs.readFileSync(path.join(__dirname, '../../library/arguments/aquinas_first_way.theo'), 'utf8'))); assert.equal(good.ok, true, good.rendered); assert.ok(good.mermaid.startsWith('flowchart TD')); assert.equal(good.nodes.length, 7); diff --git a/web/app.js b/web/app.js index e6a0b0e..56a1be3 100644 --- a/web/app.js +++ b/web/app.js @@ -2,8 +2,10 @@ 'use strict'; const EXAMPLES = [ - ['The First Way (Aquinas)', 'examples/aquinas_first_way.theo'], - ['Resurrection (minimal facts)', 'examples/resurrection.theo'], + ['Affirming the consequent (invalid)', 'examples/affirming_the_consequent.theo'], + ['The First Way (Aquinas)', 'library/arguments/aquinas_first_way.theo'], + ['The kalam cosmological argument', 'library/arguments/kalam.theo'], + ['Resurrection (minimal facts)', 'library/arguments/resurrection.theo'], ]; const STARTER = `argument "Modus Ponens" diff --git a/web/build-site.sh b/web/build-site.sh index 6eb1833..cf1271c 100755 --- a/web/build-site.sh +++ b/web/build-site.sh @@ -7,9 +7,10 @@ OUT="$2" ROOT="$(cd "$(dirname "$0")/.." && pwd)" rm -rf "$OUT" -mkdir -p "$OUT/gallery" "$OUT/examples" +mkdir -p "$OUT/gallery" "$OUT/examples" "$OUT/library" cp "$ROOT/web/index.html" "$ROOT/web/app.js" "$ROOT/web/theos.css" "$ROOT/web/playground.css" "$OUT/" cp -r "$ROOT/web/dist" "$OUT/dist" cp "$ROOT"/examples/*.theo "$OUT/examples/" +cp -r "$ROOT/library/arguments" "$OUT/library/arguments" cp "$ROOT/web/theos.css" "$ROOT/web/gallery.css" "$OUT/gallery/" -"$THEOSC" site "$ROOT/examples" -o "$OUT/gallery" +"$THEOSC" site "$ROOT/library/arguments" -o "$OUT/gallery"