diff --git a/.gitattributes b/.gitattributes new file mode 100644 index 0000000..83ea39a --- /dev/null +++ b/.gitattributes @@ -0,0 +1,3 @@ +# Golden outputs are compared byte for byte, so text stays LF on every platform +* text=auto eol=lf +*.theos binary diff --git a/.github/workflows/ci.yml b/.github/workflows/ci.yml index 02837ac..3cebaec 100644 --- a/.github/workflows/ci.yml +++ b/.github/workflows/ci.yml @@ -11,14 +11,18 @@ jobs: fail-fast: false matrix: compiler: - - { cc: gcc, cxx: g++ } - - { cc: clang, cxx: clang++ } + - { cc: gcc, cxx: g++, flags: "" } + # libstdc++ 13 hides std::expected from Clang 18, so Clang builds against libc++ + - { cc: clang, cxx: clang++, flags: "-stdlib=libc++" } name: linux-${{ matrix.compiler.cc }} runs-on: ubuntu-24.04 steps: - uses: actions/checkout@v4 + - name: Install libc++ + if: matrix.compiler.cc == 'clang' + run: sudo apt-get update && sudo apt-get install -y libc++-18-dev libc++abi-18-dev - name: Configure - run: cmake -B build -G Ninja -DCMAKE_BUILD_TYPE=Release -DCMAKE_CXX_COMPILER=${{ matrix.compiler.cxx }} + run: cmake -B build -G Ninja -DCMAKE_BUILD_TYPE=Release -DCMAKE_CXX_COMPILER=${{ matrix.compiler.cxx }} "-DCMAKE_CXX_FLAGS=${{ matrix.compiler.flags }}" - name: Build run: cmake --build build - name: Test diff --git a/CMakeLists.txt b/CMakeLists.txt index 71b051b..eeba1db 100644 --- a/CMakeLists.txt +++ b/CMakeLists.txt @@ -17,10 +17,15 @@ if(MINGW) endif() add_library(theos_core STATIC + src/core/ast.cpp + src/core/canon.cpp + src/core/diagnostic.cpp + src/core/driver.cpp + src/core/exporter.cpp + src/core/expr.cpp + src/core/lexer.cpp src/core/parser.cpp src/core/validator.cpp - src/core/exporter.cpp - src/core/format.cpp ) target_include_directories(theos_core PUBLIC include) target_link_libraries(theos_core PRIVATE theos_warnings) diff --git a/README.md b/README.md index dcff11e..31e252f 100644 --- a/README.md +++ b/README.md @@ -1,6 +1,6 @@ # Theos Engine (`theosc`) -A high-performance C++20 engine and CLI toolchain designed to parse, logically validate, and serialize formal theological and philosophical arguments. +A C++23 engine and CLI for writing, checking and visualizing formal theological and philosophical arguments. --- @@ -12,49 +12,62 @@ Theos bridges this gap. It provides a deterministic pipeline to turn human-reada --- -## Architecture & Pipeline - -The system operates on an end-to-end compilation pipeline: +## Pipeline ``` -[ .theo Source ] - │ - ▼ - Parser (AST) - │ - ▼ - Validator (DFS Cycle & Integrity Check) - ├───► Exporter (Mermaid.js / Diagrams) - └───► Binary Serializer ───► [ .theos Binary Format ] - +.theo source ─► Lexer ─► Parser ─► AST ─► Validator ─► Mermaid exporter ``` -1. **Parser:** Ingests human-readable `.theo` DSL files into a typed abstract syntax tree (AST) representing nodes (premises, deductions, conclusions) and foundational axioms. -2. **Validator:** Executes graph-level checks, including cycle detection and referential integrity verification, ensuring that circular dependencies or dangling references are caught before export. -3. **Serializer (`.theos`):** Packs validated graphs into a custom binary layout optimized for fast zero-overhead loading. +Each claim in a `.theo` file carries natural-language text and a formula: ---- +```theo +argument "Modus Ponens Demo" -## The `.theos` Binary Format +axiom Obs = source("Field notes", "p. 4") -To ensure memory efficiency and lightning-fast loading, the `.theos` format utilizes a structured layout separated into fixed-size tables and a memory-pooled string heap: +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 +} +``` -* **Header (`TheosHeader`):** 32-byte fixed header featuring magic bytes (`0x5448454F` / `"THEO"`), version metadata, element counts, and exact byte offsets for tables. -* **Axiom Table:** Packed records linking philosophical/scriptural citations, chapter indices, and verse ranges. -* **Node Table:** Typed graph nodes containing unique identifiers, classification tags, text payloads, and dynamic support/dependency vectors. -* **String Heap:** A contiguous null-terminated character pool referenced via zero-copy byte offsets, eliminating internal pointer bloat. +The full language is specified in [docs/spec/language.md](docs/spec/language.md). --- ## CLI Usage ```sh -theosc export examples/aquinas_first_way.theo --format mermaid -o diagram.md -theosc export examples/aquinas_first_way.theo --format binary -o aquinas.theos -theosc inspect aquinas.theos +theosc check examples/aquinas_first_way.theo +theosc export examples/resurrection.theo --format mermaid -o resurrection.mmd ``` -Diagnostics go to stderr; exit code 0 = success, 1 = invalid input, 2 = usage error. +Diagnostics go to stderr as `file:line:col: error: message` with the source line underneath; +exit code 0 = success, 1 = invalid input, 2 = usage error. + +--- + +## Project Structure + +```text +theos-engine/ +├── include/theos/ # Public headers +├── src/core/ # Core library (lexer, parser, validator, exporter) +├── src/cli/ # theosc command-line tool +├── docs/spec/ # Language specification +├── examples/ # Sample .theo arguments +└── tests/ # Catch2 unit tests and golden files +``` --- diff --git a/ROADMAP.md b/ROADMAP.md index f199d2e..0d0e62e 100644 --- a/ROADMAP.md +++ b/ROADMAP.md @@ -259,3 +259,4 @@ Answers to the original open questions (2026-10-24) and decisions made while bui | Phase | Status | |-------|--------| | 0 Foundation | done | +| 1 Language v2 | done — formulas are fully parsed already (needed to find where they end); the v1 binary format was removed here rather than in M2.2 because it was tied to the old AST; syntax errors stop at the first error, static-rule errors are all reported; Clang builds use libc++ because libstdc++ 13 hides `std::expected` from Clang 18 | diff --git a/docs/spec/language.md b/docs/spec/language.md new file mode 100644 index 0000000..2b468af --- /dev/null +++ b/docs/spec/language.md @@ -0,0 +1,239 @@ +# The `.theo` Language — Specification v2 + +A `.theo` file states one argument, or a library of reusable axioms and +definitions. Every claim carries **natural-language text** for readers and a +**formula** for the checker. + +```theo +argument "Modus Ponens Demo" by "Anonymous" + +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 +} +``` + +--- + +## 1. Lexical structure + +Source is UTF-8. Whitespace separates tokens and is otherwise insignificant. + +| Token | Form | +|-------|------| +| Line comment | `//` to end of line | +| Block comment | `/*` … `*/` (no nesting) | +| Identifier | `[A-Za-z_][A-Za-z0-9_]*`, excluding keywords | +| Number | `[0-9]+` | +| String | `"` … `"`, escapes `\"` `\\` `\n`; may not contain a raw newline | +| Punctuation | `{ } [ ] ( ) , . : = :=` and `-` (only in proof ranges) | + +Operators, each with an ASCII and a Unicode spelling: + +| Meaning | ASCII | Unicode | +|---------|-------|---------| +| negation | `~` | `¬` | +| conjunction | `&` | `∧` | +| disjunction | `\|` | `∨` | +| implication | `->` | `→` | +| biconditional | `<->` | `↔` | +| necessity | `[]` | `□` | +| possibility | `<>` | `◇` | +| universal | `forall` | `∀` | +| existential | `exists` | `∃` | +| abstraction | `\` or `lambda` | `λ` | +| falsum | `bot` | `⊥` | +| identity / non-identity | `=` / `!=` | `=` / `≠` | + +`[]` is a necessity operator only when `[` and `]` are adjacent; otherwise they +are list brackets. + +**Keywords:** `argument by import axiom scripture source principle define +premise deduction conclusion from grounded_by text formula proof box objection +reply against to forall exists lambda bot ind prop`. + +--- + +## 2. Grammar (EBNF) + +```ebnf +document = [ header ] , { item } ; +header = "argument" , STRING , [ "by" , STRING ] ; +item = import | axiom | definition | node | objection | reply ; + +import = "import" , STRING ; + +axiom = "axiom" , IDENT , "=" , axiom_body ; +axiom_body = "scripture" , "(" , IDENT , "," , STRING , ")" + | "source" , "(" , STRING , "," , STRING , ")" + | "principle" , "(" , STRING , ")" ; + +definition = "define" , IDENT , [ "(" , binder , { "," , binder } , ")" ] , ":=" , formula ; +binder = IDENT , [ ":" , sort ] ; +sort = "ind" | "prop" ; + +node = node_kind , IDENT , { clause } , "{" , { field } , "}" ; +node_kind = "premise" | "deduction" | "conclusion" ; +clause = "from" , id_list | "grounded_by" , id_list | "by" , IDENT ; +id_list = "[" , IDENT , { "," , IDENT } , "]" ; +field = "text" , ":" , STRING + | "formula" , ":" , formula + | proof ; + +objection = "objection" , IDENT , "against" , IDENT , "{" , { field } , "}" ; +reply = "reply" , IDENT , "to" , IDENT , "{" , { field } , "}" ; + +proof = "proof" , "{" , { proof_item } , "}" ; +proof_item = line | subproof ; +line = NUMBER , "." , formula , IDENT , [ ref , { "," , ref } ] ; +ref = NUMBER , [ "-" , NUMBER ] | IDENT ; +subproof = [ "box" ] , "{" , [ "[" , IDENT , "]" ] , { proof_item } , "}" ; + +formula = iff ; +iff = imp , [ ( "<->" | "↔" ) , imp ] ; +imp = or , [ ( "->" | "→" ) , imp ] ; (* right-associative *) +or = and , { ( "|" | "∨" ) , and } ; +and = unary , { ( "&" | "∧" ) , unary } ; +unary = ( "~" | "¬" | "[]" | "□" | "<>" | "◇" ) , unary + | quantifier , binder , { binder } , "." , formula (* body extends maximally right *) + | atom ; +quantifier = "forall" | "∀" | "exists" | "∃" ; +atom = "(" , formula , ")" + | "bot" | "⊥" + | IDENT , "(" , term , { "," , term } , ")" (* predicate application *) + | IDENT , ( "=" | "!=" | "≠" ) , IDENT (* identity *) + | IDENT ; (* propositional letter *) +term = IDENT | lambda | "(" , lambda , ")" ; +lambda = ( "\" | "lambda" | "λ" ) , binder , "." , formula ; +``` + +A formula ends at the first token that cannot continue it, so fields need no +terminator: in `formula: P -> Q` followed by `text: "..."`, the keyword `text` +ends the formula. + +--- + +## 3. Items + +### Header +`argument "Title" by "Author"` names the argument. A file with a header is an +**argument file** and must contain at least one premise and one conclusion. A +file without a header is a **library file** (axioms, definitions, reusable +premises). + +### Imports +`import "path"` makes every item of another file visible. The path has no +extension; `.theo` is appended. It is resolved first relative to the importing +file, then against each library search directory (`-L dir` on the command line, +then the `library/` directory of the installation). Imported names share the +importing file's namespace: a name defined twice is an error. + +### Axioms +Axioms are the evidence premises rest on. + +| Form | Meaning | +|------|---------| +| `scripture(canon, "Book C:V-W")` | Scripture reference in a named canon | +| `source("Work", "locator")` | Philosophical or historical source | +| `principle("statement")` | Self-evident first principle | + +Canons: `protestant` (66 books), `catholic` (73), `orthodox` (Catholic plus +1 Esdras, Prayer of Manasseh, 3–4 Maccabees; Psalms has 151), `quran`. +Reference forms: `"Book C"`, `"Book C:V"`, `"Book C:V-W"`, `"Book C:V-C2:W"`; +for the Quran the book is omitted (`"2:255"`). Book names are matched ignoring +case and spaces (`1 Corinthians` = `1corinthians`); chapter numbers are checked +against the canon, and for the Quran verse numbers are checked too. + +### Definitions +`define G(x) := forall F:prop. (Positive(F) -> F(x))` introduces an +abbreviation. Binders default to sort `ind`. Definitions may refer to earlier +definitions only (no recursion). + +### Nodes +| Kind | Clauses | Meaning | +|------|---------|---------| +| `premise` | `grounded_by [axioms]` (optional) | Accepted claim; ungrounded premises get a warning | +| `deduction` | `from [nodes]` required | Intermediate step inferred from other nodes | +| `conclusion` | `from [nodes]` required | Final claim | + +Every node needs `text` and `formula`. An inferred node is justified in exactly +one way: + +| Justification | Meaning | +|---------------|---------| +| *(none)* | The checker decides whether the `from` formulas entail the formula (decidable fragments only: propositional, propositional S5) | +| `by rule` | A single proof rule applied to the `from` formulas in order | +| `by z3` | Entailment confirmed by the Z3 solver | +| `proof { … }` | A natural-deduction proof (§4) | + +### Objections and replies +`objection O1 against P2 { text: "..." }` attacks a node; `reply R1 to O1 { ... }` +attacks an objection or another reply. `text` is required, `formula` optional. + +--- + +## 4. Proofs + +Fitch-style natural deduction. Each line has a number, a formula and a +justification (rule name plus references). + +```theo +proof { + 1. A -> B premise P1 + 2. B -> C premise P2 + { + 3. A assume + 4. B imp_e 1, 3 + 5. C imp_e 2, 4 + } + 6. A -> C imp_i 3-5 +} +``` + +- `premise X` cites a node listed in `from`. +- A line may cite earlier lines in the same or an enclosing block, and closed + subproofs (`n-m` = first and last line) directly inside the same or an + enclosing block. +- `{ ... }` opens a subproof whose first line, if justified by `assume`, is its + assumption. `{ [a] ... }` introduces a fresh name `a` (for `forall_i` and + `exists_e`). `box { ... }` opens a strict (modal) subproof. +- Line numbers must be unique and increasing. +- The last line of the top-level proof must be the node's formula. + +The rule set and its checking are specified in [proofs.md](proofs.md). + +--- + +## 5. Static rules + +Errors: +- Duplicate name among axioms, definitions, nodes, objections and replies. +- `from` naming anything but a node; `grounded_by` naming anything but an axiom; + `against` naming anything but a node; `to` naming anything but an objection or reply. +- `premise` with `from`, `by` or `proof`; `deduction`/`conclusion` without `from`. +- Both `by` and `proof` on one node. +- Missing `text` or `formula` on a node; missing `text` on an objection or reply; + a field given twice. +- A cycle through `from` edges. +- An argument file without a premise or without a conclusion. +- Unknown canon or book, chapter or verse out of range. + +Warnings: +- A premise with no `grounded_by`. +- A node that no conclusion depends on. + +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. diff --git a/examples/aquinas_first_way.theo b/examples/aquinas_first_way.theo index 378b24c..b375bcf 100644 --- a/examples/aquinas_first_way.theo +++ b/examples/aquinas_first_way.theo @@ -1,33 +1,43 @@ -// ========================================== -// Title: The First Way (Cosmological Argument) -// Author: Thomas Aquinas (Formalized) -// ========================================== +// The First Way (argument from motion), Summa Theologiae I, q.2, a.3. +// The regress premise is stated explicitly so the inference is deductively valid. -title: "The First Way: Argument from Motion" -author: "Thomas Aquinas" +argument "The First Way: Argument from Motion" by "Thomas Aquinas" -// Philosophical and Scriptural Axioms -axiom UnmovedMoverAx = scripture(Psalm, 102, 25, 27) -axiom SustainingWordAx = scripture(Hebrews, 1, 3, 3) +axiom ST = source("Thomas Aquinas, Summa Theologiae", "I, q.2, a.3") +axiom Ps102 = scripture(protestant, "Psalms 102:25-27") +axiom Heb1 = scripture(protestant, "Hebrews 1:3") -premise P1 { - text: "Certain things in the world are in motion or undergoing change, and potentiality is brought to actuality only by something already actual." - supports: [] +premise P1 grounded_by [ST] { + text: "Some things in the world are in motion." + formula: exists x. Moved(x) } -premise P2 { - text: "Whatever is moved must be moved by another; an infinite regress of actual movers is metaphysically impossible." - supports: [P1] +premise P2 grounded_by [ST] { + text: "Whatever is moved is moved by something other than itself." + formula: forall x. Moved(x) -> exists y. (Moves(y, x) & y != x) } -deduction D1 { - text: "Therefore, it is necessary to arrive at a first mover, put in motion by no other, which all men understand to be God." - supports: [P1, P2] - depends_on: [P1, P2] +premise P3 grounded_by [ST] { + text: "An infinite regress of movers is impossible." + formula: ~Regress } -conclusion C1 { - text: "An Unmoved Mover (God) necessarily exists as the ultimate source of all change and actuality in the universe." - supports: [D1] - depends_on: [D1] -} \ No newline at end of file +premise P4 grounded_by [ST] { + text: "If something is moved, every moved thing has another mover, and every mover is itself moved, then there is an infinite regress of movers." + formula: (exists x. Moved(x)) & (forall x. Moved(x) -> exists y. (Moves(y, x) & y != x)) & (forall x. forall y. Moved(x) & Moves(y, x) -> Moved(y)) -> Regress +} + +premise P5 grounded_by [ST, Ps102, Heb1] { + text: "A first mover, itself unmoved, is what everyone understands to be God." + formula: forall y. (~Moved(y) & exists x. Moves(y, x)) -> God(y) +} + +deduction D1 from [P1, P2, P3, P4] { + text: "Therefore there is a first mover, moved by no other." + formula: exists y. (~Moved(y) & exists x. Moves(y, x)) +} + +conclusion C1 from [D1, P5] { + text: "Therefore God exists." + formula: exists y. God(y) +} diff --git a/examples/resurrection.theo b/examples/resurrection.theo index 53508a9..8b5174e 100644 --- a/examples/resurrection.theo +++ b/examples/resurrection.theo @@ -1,22 +1,42 @@ -meta { - title: "Historical Case for the Resurrection" - author: "Portfolio Developer" - version: 1.0 +// A minimal-facts argument for the resurrection. The inference to the best +// explanation is made an explicit premise (P4), which is where debate belongs. + +argument "Historical Case for the Resurrection" by "Theos Examples" + +axiom Cor15 = scripture(protestant, "1 Corinthians 15:3-8") +axiom Mk16 = scripture(protestant, "Mark 16:1-8") +axiom Lk24 = scripture(protestant, "Luke 24:36-43") +axiom IBE = principle("The hypothesis that best explains the established facts is probably true.") + +premise P1 grounded_by [Cor15] { + text: "Jesus died by crucifixion and was buried." + formula: Died } -axiom A1 = scripture(1Corinthians, 15, 3, 8) -axiom A2 = scripture(Luke, 24, 36, 43) +premise P2 grounded_by [Mk16] { + text: "The tomb was found empty shortly after." + formula: EmptyTomb +} -premise P1 { - text: "Jesus died by Roman crucifixion and was buried in a known tomb." +premise P3 grounded_by [Cor15, Lk24] { + text: "Individuals and groups experienced appearances of Jesus alive." + formula: Appearances } -premise P2 { - text: "Multiple independent sources report the tomb was found empty shortly after." - supports: [A1] +premise P4 grounded_by [IBE] { + text: "If Jesus died, the tomb was empty and he appeared alive, the best explanation is that God raised him." + formula: Died & EmptyTomb & Appearances -> Raised } -conclusion C1 { - text: "God raised Jesus from the dead as the best historical explanation of the data." - depends_on: [P1, P2] -} \ No newline at end of file +conclusion C1 from [P1, P2, P3, P4] { + text: "God raised Jesus from the dead." + formula: Raised +} + +objection O1 against P4 { + text: "Grief hallucinations explain the appearances without a resurrection." +} + +reply R1 to O1 { + text: "Hallucinations are private; they do not explain group appearances or the empty tomb." +} diff --git a/include/theos/ast.hpp b/include/theos/ast.hpp index 42b1a68..9125c55 100644 --- a/include/theos/ast.hpp +++ b/include/theos/ast.hpp @@ -1,34 +1,144 @@ #pragma once +#include "theos/diagnostic.hpp" +#include "theos/expr.hpp" +#include +#include #include +#include #include -#include namespace Theos::AST { +// A name written in source, kept with its position for diagnostics +struct Ref { + std::string name; + Span span; +}; + +// ---- Proofs ---- + +struct ProofRef { + enum class Kind : uint8_t { Line, Range, Name }; + Kind kind = Kind::Line; + uint32_t first = 0; // Line, Range + uint32_t last = 0; // Range + std::string name; // Name + Span span; +}; + +struct ProofLine { + uint32_t number = 0; + ExprPtr formula; + Ref rule; + std::vector refs; + Span span; +}; + +struct ProofItem; + +struct Subproof { + bool strict = false; // box { ... } + std::optional fresh; // { [a] ... } + std::vector items; + Span span; +}; + +struct ProofItem : std::variant { + using variant::variant; +}; + +struct Proof { + std::vector items; + Span span; +}; + +// ---- Items ---- + +enum class Canon : uint8_t { Protestant, Catholic, Orthodox, Quran }; + +struct ScriptureRef { + Canon canon = Canon::Protestant; + uint16_t book = 0; // 1-based index into the canon's book list; 0 for the Quran + uint16_t chapter = 0; // chapter (surah) + uint16_t verse = 0; // 0 = whole chapter + uint16_t end_chapter = 0; + uint16_t end_verse = 0; +}; + +enum class AxiomKind : uint8_t { Scripture, Source, Principle }; + struct Axiom { + std::string id; + AxiomKind kind = AxiomKind::Principle; + std::string canon; // Scripture: canon name as written + std::string citation; // Scripture: reference text; Source: work; Principle: statement + std::string locator; // Source: locator within the work + ScriptureRef scripture; // Scripture: resolved by the validator + Span span; +}; + +struct Binder { std::string name; - std::string book_name; - uint8_t book_id; - uint16_t chapter; - uint8_t start_verse; - uint8_t end_verse; + Sort sort = Sort::Ind; + Span span; }; +struct Definition { + std::string id; + std::vector params; + ExprPtr body; + Span span; +}; + +enum class NodeKind : uint8_t { Premise, Deduction, Conclusion }; + struct Node { + NodeKind kind = NodeKind::Premise; std::string id; + std::vector from; + std::vector grounded_by; + std::optional rule; // by std::string text; - std::string type; // "premise", "deduction", "conclusion" - std::vector supports; - std::vector depends_on; + ExprPtr formula; + std::optional proof; + bool imported = false; // defined in an imported file + Span span; }; -struct TheologicalGraph { - std::string title; +enum class DialecticKind : uint8_t { Objection, Reply }; + +// Objections attack nodes; replies attack objections or other replies +struct Dialectic { + DialecticKind kind = DialecticKind::Objection; + std::string id; + Ref target; + std::string text; + ExprPtr formula; // optional + Span span; +}; + +struct Import { + std::string path; + Span span; +}; + +struct Document { + std::string file; + std::optional title; // set for argument files std::string author; - double version = 1.0; + std::vector imports; std::vector axioms; + std::vector definitions; std::vector nodes; + std::vector dialectics; }; -} // namespace Theos::AST \ No newline at end of file +std::string_view to_string(NodeKind kind); +std::string_view to_string(AxiomKind kind); +std::string_view to_string(DialecticKind kind); + +// Stable, human-readable dump used by golden tests +std::string dump(const Document& doc); + +} // namespace Theos::AST diff --git a/include/theos/canon.hpp b/include/theos/canon.hpp new file mode 100644 index 0000000..cf56290 --- /dev/null +++ b/include/theos/canon.hpp @@ -0,0 +1,25 @@ +#pragma once + +#include "theos/ast.hpp" +#include +#include +#include +#include + +namespace Theos::Scripture { + +std::optional from_name(std::string_view name); +std::string_view name(AST::Canon canon); + +// Number of books in a canon (0 for the Quran, which is addressed by surah) +uint16_t book_count(AST::Canon canon); +std::string_view book_name(AST::Canon canon, uint16_t book); + +// Parses "Book C", "Book C:V", "Book C:V-W", "Book C:V-C2:W" (Quran: "C:V..." without a book). +// The error string explains what is wrong with the reference. +std::expected resolve(AST::Canon canon, std::string_view reference); + +// Canonical citation text, e.g. "Psalms 102:25-27" +std::string format(const AST::ScriptureRef& ref); + +} // namespace Theos::Scripture diff --git a/include/theos/diagnostic.hpp b/include/theos/diagnostic.hpp new file mode 100644 index 0000000..6f81987 --- /dev/null +++ b/include/theos/diagnostic.hpp @@ -0,0 +1,34 @@ +#pragma once + +#include +#include +#include +#include + +namespace Theos { + +// Position of a token in its source file. Columns count code points, so carets line up under UTF-8 text. +struct Span { + uint32_t line = 0; + uint32_t col = 0; + uint32_t offset = 0; // byte offset into the source + uint32_t length = 0; // byte length +}; + +enum class Severity { Error, Warning }; + +struct Diagnostic { + Severity severity = Severity::Error; + std::string file; + Span span; + std::string message; +}; + +using Diagnostics = std::vector; + +bool has_errors(const Diagnostics& diags); + +// "file:line:col: error: message" followed by the source line and a caret underline +std::string render(const Diagnostic& diag, std::string_view source); + +} // namespace Theos diff --git a/include/theos/driver.hpp b/include/theos/driver.hpp new file mode 100644 index 0000000..8d21332 --- /dev/null +++ b/include/theos/driver.hpp @@ -0,0 +1,30 @@ +#pragma once + +#include "theos/ast.hpp" +#include +#include +#include + +namespace Theos::Driver { + +struct Source { + std::string path; + std::string text; +}; + +// Outcome of running the pipeline on one file. `doc` is set once parsing succeeded. +struct Result { + std::optional doc; + Diagnostics diagnostics; + std::vector sources; // every file read, for rendering diagnostics + + bool ok() const { return doc && !has_errors(diagnostics); } +}; + +Result check_source(std::string text, const std::string& path); +Result check_file(const std::string& path); + +// All diagnostics with source excerpts, in the order produced +std::string render_diagnostics(const Result& result); + +} // namespace Theos::Driver diff --git a/include/theos/exporter.hpp b/include/theos/exporter.hpp index 8813d2d..8f8dbc7 100644 --- a/include/theos/exporter.hpp +++ b/include/theos/exporter.hpp @@ -4,6 +4,8 @@ #include namespace Theos::Exporter { - // Generates a Mermaid flowchart string from an AST graph - std::string to_mermaid(const AST::TheologicalGraph& graph); -} \ No newline at end of file + +// Mermaid flowchart source (without Markdown fences) +std::string to_mermaid(const AST::Document& doc); + +} // namespace Theos::Exporter diff --git a/include/theos/expr.hpp b/include/theos/expr.hpp new file mode 100644 index 0000000..1b5a933 --- /dev/null +++ b/include/theos/expr.hpp @@ -0,0 +1,54 @@ +#pragma once + +#include "theos/diagnostic.hpp" +#include +#include +#include + +namespace Theos { + +// Sort of a bound variable: individuals, or properties of individuals (ind -> bool) +enum class Sort : uint8_t { Ind, Prop }; + +enum class ExprKind : uint8_t { + // terms + Symbol, // name + Lambda, // \name:sort. args[0] + // formulas + Atom, // name(args...) — args are terms; zero args = propositional letter + Eq, // args[0] = args[1] + Bottom, + Not, Box, Dia, // args[0] + And, Or, Implies, Iff, // args[0], args[1] + Forall, Exists, // name:sort. args[0] +}; + +struct Expr; +using ExprPtr = std::shared_ptr; + +// Immutable formula/term node, shared between formulas once built +struct Expr { + ExprKind kind; + std::string name; + Sort sort = Sort::Ind; + std::vector args; + Span span; +}; + +ExprPtr make_symbol(std::string name, Span span = {}); +ExprPtr make_atom(std::string head, std::vector args, Span span = {}); +ExprPtr make_eq(ExprPtr lhs, ExprPtr rhs, Span span = {}); +ExprPtr make_bottom(Span span = {}); +ExprPtr make_unary(ExprKind kind, ExprPtr operand, Span span = {}); +ExprPtr make_binary(ExprKind kind, ExprPtr lhs, ExprPtr rhs, Span span = {}); +ExprPtr make_binder(ExprKind kind, std::string var, Sort sort, ExprPtr body, Span span = {}); + +bool is_binder(ExprKind kind); +bool is_binary(ExprKind kind); + +enum class Notation { Ascii, Unicode }; + +// Canonical printing: re-parsing the output yields a structurally identical formula +std::string print(const Expr& expr, Notation notation = Notation::Ascii); + +} // namespace Theos diff --git a/include/theos/format.hpp b/include/theos/format.hpp deleted file mode 100644 index 1c81c41..0000000 --- a/include/theos/format.hpp +++ /dev/null @@ -1,61 +0,0 @@ -#pragma once - -#include -#include -#include -#include -#include "theos/ast.hpp" - -namespace Theos { - -constexpr uint32_t THEOS_MAGIC = 0x5448454F; // "THEO" -constexpr uint16_t THEOS_VERSION = 0x0100; // v1.0 - -#pragma pack(push, 1) - -struct TheosHeader { - uint32_t magic; - uint16_t version; - uint16_t node_count; - uint16_t axiom_count; - uint32_t axiom_table_offset; - uint32_t node_table_offset; - uint32_t string_heap_offset; - uint8_t reserved[12]; -}; - -struct TheosAxiomRecord { - uint32_t name_string_offset; // Offset into string heap for axiom name (e.g. "Ax1") - uint32_t scripture_packed; // Bit-packed book, chapter, verses -}; - -struct TheosNodeRecord { - uint32_t id_string_offset; // Offset into string heap for node ID (e.g. "P1") - uint32_t type_string_offset; // Offset into string heap for node type ("premise", etc.) - uint32_t text_string_offset; // Offset into string heap for node text description - uint16_t supports_count; // Number of items in supports list - uint16_t depends_count; // Number of items in depends_on list - // Followed dynamically in file by: - // uint32_t supports_offsets[supports_count]; - // uint32_t depends_offsets[depends_count]; -}; - -#pragma pack(pop) - -// Utility for bit-packing scripture references into a single uint32_t -inline uint32_t pack_scripture(uint8_t book, uint16_t chapter, uint8_t start_verse, uint8_t end_verse) { - return (static_cast(book) << 24) | - (static_cast(chapter & 0x1FF) << 15) | - (static_cast(start_verse) << 7) | - (static_cast(end_verse & 0x7F)); -} - -inline void unpack_scripture(uint32_t packed, uint8_t& book, uint16_t& chapter, uint8_t& start_verse, uint8_t& end_verse) { - book = static_cast(packed >> 24); - chapter = static_cast((packed >> 15) & 0x1FF); - start_verse = static_cast((packed >> 7) & 0xFF); - end_verse = static_cast(packed & 0x7F); -} -void write_binary_file(const std::string& filepath, const AST::TheologicalGraph& graph); -AST::TheologicalGraph read_binary_file(const std::string& filepath); -} // namespace Theos \ No newline at end of file diff --git a/include/theos/lexer.hpp b/include/theos/lexer.hpp new file mode 100644 index 0000000..3284948 --- /dev/null +++ b/include/theos/lexer.hpp @@ -0,0 +1,31 @@ +#pragma once + +#include "theos/diagnostic.hpp" +#include +#include +#include +#include + +namespace Theos { + +enum class Tok { + Ident, Keyword, Number, String, + LBrace, RBrace, LBracket, RBracket, LParen, RParen, + Comma, Dot, Colon, Equals, Define, Minus, + Not, And, Or, Implies, Iff, Box, Diamond, Lambda, Bottom, NotEquals, + Forall, Exists, + End, +}; + +struct Token { + Tok kind; + std::string text; // identifier/keyword spelling, number digits, or decoded string contents + Span span; +}; + +std::string_view describe(Tok kind); + +// Tokenizes a whole file; the last token is always Tok::End +std::expected, Diagnostic> lex(std::string_view source, const std::string& file); + +} // namespace Theos diff --git a/include/theos/parser.hpp b/include/theos/parser.hpp index 4df9f5f..5fc73e8 100644 --- a/include/theos/parser.hpp +++ b/include/theos/parser.hpp @@ -1,14 +1,16 @@ #pragma once #include "theos/ast.hpp" +#include #include +#include namespace Theos::Parser { -// Parses a .theo source file path into an AST TheologicalGraph -AST::TheologicalGraph parse_file(const std::string& filepath); +// Parses one .theo source. Syntax errors stop at the first error. +std::expected parse(std::string_view source, const std::string& file); -// Parses a raw std::string containing .theo DSL source code -AST::TheologicalGraph parse_string(const std::string& source); +// Parses a standalone formula (used by tests and tools) +std::expected parse_formula(std::string_view source); -} // namespace Theos::Parser \ No newline at end of file +} // namespace Theos::Parser diff --git a/include/theos/validator.hpp b/include/theos/validator.hpp index fbfb4ef..43ccbdb 100644 --- a/include/theos/validator.hpp +++ b/include/theos/validator.hpp @@ -1,17 +1,10 @@ #pragma once #include "theos/ast.hpp" -#include -#include namespace Theos::Validator { -struct ValidationResult { - bool is_valid = true; - std::vector errors; - std::vector warnings; -}; +// Checks the static rules of the language spec (§5) and resolves scripture references in place. +Diagnostics validate(AST::Document& doc); -ValidationResult validate(const AST::TheologicalGraph& graph); - -} // namespace Theos::Validator \ No newline at end of file +} // namespace Theos::Validator diff --git a/src/cli/main.cpp b/src/cli/main.cpp index 615c93d..8357c58 100644 --- a/src/cli/main.cpp +++ b/src/cli/main.cpp @@ -1,94 +1,82 @@ -#include +#include "theos/driver.hpp" +#include "theos/exporter.hpp" #include +#include #include -#include "theos/ast.hpp" -#include "theos/parser.hpp" -#include "theos/exporter.hpp" -#include "theos/format.hpp" -#include "theos/validator.hpp" +#include namespace { constexpr int EXIT_INVALID = 1; constexpr int EXIT_USAGE = 2; -void print_help() { - std::cerr << "theosc - the Theos argument compiler\n\n" - << "Usage:\n" - << " theosc export --format [-o output_file]\n" - << " theosc inspect \n"; -} - -int inspect(const std::string& input_file) { - auto graph = Theos::read_binary_file(input_file); - std::cout << "Nodes: " << graph.nodes.size() << ", Axioms: " << graph.axioms.size() << "\n"; - for (const auto& node : graph.nodes) { - std::cout << " [" << node.type << "] " << node.id << ": " << node.text << "\n"; - } - return 0; -} +constexpr const char* usage = + "theosc - the Theos argument compiler\n" + "\n" + "Usage:\n" + " theosc check \n" + " theosc export --format mermaid [-o ]\n"; -int export_file(int argc, char* argv[]) { - std::string input_file; +struct Args { + std::string command; + std::string input; std::string format; - std::string output_file; + std::string output; +}; +std::optional parse_args(int argc, char* argv[]) { + if (argc < 3) return std::nullopt; + Args a; + a.command = argv[1]; for (int i = 2; i < argc; ++i) { - std::string arg = argv[i]; - if (arg == "--format" && i + 1 < argc) { - format = argv[++i]; - } else if (arg == "-o" && i + 1 < argc) { - output_file = argv[++i]; - } else if (input_file.empty()) { - input_file = arg; - } else { - std::cerr << "error: unexpected argument '" << arg << "'\n"; - return EXIT_USAGE; - } - } - if (input_file.empty() || (format != "mermaid" && format != "binary")) { - print_help(); - return EXIT_USAGE; + const std::string arg = argv[i]; + if (arg == "--format" && i + 1 < argc) a.format = argv[++i]; + else if (arg == "-o" && i + 1 < argc) a.output = argv[++i]; + else if (a.input.empty() && !arg.starts_with("-")) a.input = arg; + else return std::nullopt; } + if (a.input.empty()) return std::nullopt; + return a; +} - auto graph = Theos::Parser::parse_file(input_file); - auto validation = Theos::Validator::validate(graph); - if (!validation.is_valid) { - for (const auto& err : validation.errors) { - std::cerr << input_file << ": error: " << err << "\n"; - } - return EXIT_INVALID; +void write_output(const std::string& path, const std::string& content) { + if (path.empty()) { + std::cout << content; + return; } + std::ofstream out(path, std::ios::binary); + if (!out) throw std::runtime_error("cannot write '" + path + "'"); + out << content; +} - if (format == "mermaid") { - const std::string mermaid = Theos::Exporter::to_mermaid(graph); - if (output_file.empty()) { - std::cout << mermaid; - return 0; - } - std::ofstream out(output_file); - if (!out) throw std::runtime_error("cannot write " + output_file); - out << mermaid; +int run(const Args& args) { + if (args.command != "check" && args.command != "export") return EXIT_USAGE; + if (args.command == "export" && args.format != "mermaid") return EXIT_USAGE; + + auto result = Theos::Driver::check_file(args.input); + std::cerr << Theos::Driver::render_diagnostics(result); + if (!result.ok()) return EXIT_INVALID; + + if (args.command == "check") { + std::cerr << args.input << ": ok\n"; return 0; } - - Theos::write_binary_file(output_file.empty() ? "output.theos" : output_file, graph); + write_output(args.output, Theos::Exporter::to_mermaid(*result.doc)); return 0; } } // namespace int main(int argc, char* argv[]) { - if (argc < 3) { - print_help(); + auto args = parse_args(argc, argv); + if (!args) { + std::cerr << usage; return EXIT_USAGE; } try { - const std::string command = argv[1]; - if (command == "inspect") return inspect(argv[2]); - if (command == "export") return export_file(argc, argv); - print_help(); - return EXIT_USAGE; + const int code = run(*args); + if (code == EXIT_USAGE) std::cerr << usage; + return code; } catch (const std::exception& e) { std::cerr << "error: " << e.what() << "\n"; return EXIT_INVALID; diff --git a/src/core/ast.cpp b/src/core/ast.cpp new file mode 100644 index 0000000..0cbae4f --- /dev/null +++ b/src/core/ast.cpp @@ -0,0 +1,112 @@ +#include "theos/ast.hpp" + +namespace Theos::AST { + +std::string_view to_string(NodeKind kind) { + switch (kind) { + case NodeKind::Premise: return "premise"; + case NodeKind::Deduction: return "deduction"; + case NodeKind::Conclusion: return "conclusion"; + } + return ""; +} + +std::string_view to_string(AxiomKind kind) { + switch (kind) { + case AxiomKind::Scripture: return "scripture"; + case AxiomKind::Source: return "source"; + case AxiomKind::Principle: return "principle"; + } + return ""; +} + +std::string_view to_string(DialecticKind kind) { + return kind == DialecticKind::Objection ? "objection" : "reply"; +} + +namespace { + +std::string quote(const std::string& s) { + std::string out = "\""; + for (char c : s) { + if (c == '"' || c == '\\') out += '\\'; + if (c == '\n') { + out += "\\n"; + continue; + } + out += c; + } + return out + "\""; +} + +std::string refs(const std::vector& list) { + std::string out = "["; + for (size_t i = 0; i < list.size(); ++i) out += (i ? ", " : "") + list[i].name; + return out + "]"; +} + +void dump_items(const std::vector& items, const std::string& indent, std::string& out) { + for (const auto& item : items) { + if (const auto* line = std::get_if(&item)) { + out += indent + std::to_string(line->number) + ". " + print(*line->formula) + " " + line->rule.name; + for (size_t i = 0; i < line->refs.size(); ++i) { + const auto& r = line->refs[i]; + out += i ? ", " : " "; + if (r.kind == ProofRef::Kind::Name) out += r.name; + else if (r.kind == ProofRef::Kind::Line) out += std::to_string(r.first); + else out += std::to_string(r.first) + "-" + std::to_string(r.last); + } + out += "\n"; + } else { + const auto& sub = std::get(item); + out += indent + (sub.strict ? "box {" : "{") + (sub.fresh ? " [" + sub.fresh->name + "]" : "") + "\n"; + dump_items(sub.items, indent + " ", out); + out += indent + "}\n"; + } + } +} + +} // namespace + +std::string dump(const Document& doc) { + std::string out; + if (doc.title) out += "argument " + quote(*doc.title) + (doc.author.empty() ? "" : " by " + quote(doc.author)) + "\n"; + for (const auto& imp : doc.imports) out += "import " + quote(imp.path) + "\n"; + for (const auto& ax : doc.axioms) { + out += "axiom " + ax.id + " " + std::string(to_string(ax.kind)); + if (ax.kind == AxiomKind::Scripture) out += " " + ax.canon; + out += " " + quote(ax.citation); + if (ax.kind == AxiomKind::Source) out += " " + quote(ax.locator); + out += "\n"; + } + for (const auto& def : doc.definitions) { + out += "define " + def.id; + if (!def.params.empty()) { + out += "("; + for (size_t i = 0; i < def.params.size(); ++i) { + out += (i ? ", " : "") + def.params[i].name + (def.params[i].sort == Sort::Prop ? ":prop" : ""); + } + out += ")"; + } + out += " := " + print(*def.body) + "\n"; + } + for (const auto& n : doc.nodes) { + out += std::string(to_string(n.kind)) + " " + n.id; + if (!n.from.empty()) out += " from " + refs(n.from); + if (!n.grounded_by.empty()) out += " grounded_by " + refs(n.grounded_by); + if (n.rule) out += " by " + n.rule->name; + out += "\n text: " + quote(n.text) + "\n formula: " + print(*n.formula) + "\n"; + if (n.proof) { + out += " proof\n"; + dump_items(n.proof->items, " ", out); + } + } + for (const auto& d : doc.dialectics) { + out += std::string(to_string(d.kind)) + " " + d.id + (d.kind == DialecticKind::Objection ? " against " : " to ") + + d.target.name + "\n text: " + quote(d.text) + "\n"; + if (d.formula) out += " formula: " + print(*d.formula) + "\n"; + } + return out; +} + +} // namespace Theos::AST diff --git a/src/core/canon.cpp b/src/core/canon.cpp new file mode 100644 index 0000000..4e75daf --- /dev/null +++ b/src/core/canon.cpp @@ -0,0 +1,262 @@ +#include "theos/canon.hpp" +#include +#include +#include +#include + +namespace Theos::Scripture { + +namespace { + +struct Book { + std::string_view name; + uint16_t chapters; +}; + +// Books shared by every Christian canon, in Protestant order, with Protestant chapter counts +constexpr std::array old_testament = {{ + {"Genesis", 50}, {"Exodus", 40}, {"Leviticus", 27}, {"Numbers", 36}, {"Deuteronomy", 34}, + {"Joshua", 24}, {"Judges", 21}, {"Ruth", 4}, {"1 Samuel", 31}, {"2 Samuel", 24}, + {"1 Kings", 22}, {"2 Kings", 25}, {"1 Chronicles", 29}, {"2 Chronicles", 36}, {"Ezra", 10}, + {"Nehemiah", 13}, {"Esther", 10}, {"Job", 42}, {"Psalms", 150}, {"Proverbs", 31}, + {"Ecclesiastes", 12}, {"Song of Solomon", 8}, {"Isaiah", 66}, {"Jeremiah", 52}, {"Lamentations", 5}, + {"Ezekiel", 48}, {"Daniel", 12}, {"Hosea", 14}, {"Joel", 3}, {"Amos", 9}, + {"Obadiah", 1}, {"Jonah", 4}, {"Micah", 7}, {"Nahum", 3}, {"Habakkuk", 3}, + {"Zephaniah", 3}, {"Haggai", 2}, {"Zechariah", 14}, {"Malachi", 4}, +}}; + +constexpr std::array new_testament = {{ + {"Matthew", 28}, {"Mark", 16}, {"Luke", 24}, {"John", 21}, {"Acts", 28}, + {"Romans", 16}, {"1 Corinthians", 16}, {"2 Corinthians", 13}, {"Galatians", 6}, {"Ephesians", 6}, + {"Philippians", 4}, {"Colossians", 4}, {"1 Thessalonians", 5}, {"2 Thessalonians", 3}, {"1 Timothy", 6}, + {"2 Timothy", 4}, {"Titus", 3}, {"Philemon", 1}, {"Hebrews", 13}, {"James", 5}, + {"1 Peter", 5}, {"2 Peter", 3}, {"1 John", 5}, {"2 John", 1}, {"3 John", 1}, + {"Jude", 1}, {"Revelation", 22}, +}}; + +// Ayah counts per surah (6,236 in total) +constexpr std::array quran_ayahs = { + 7, 286, 200, 176, 120, 165, 206, 75, 129, 109, 123, 111, 43, 52, 99, 128, 111, 110, 98, 135, + 112, 78, 118, 64, 77, 227, 93, 88, 69, 60, 34, 30, 73, 54, 45, 83, 182, 88, 75, 85, + 54, 53, 89, 59, 37, 35, 38, 29, 18, 45, 60, 49, 62, 55, 78, 96, 29, 22, 24, 13, + 14, 11, 11, 18, 12, 12, 30, 52, 52, 44, 28, 28, 20, 56, 40, 31, 50, 40, 46, 42, + 29, 19, 36, 25, 22, 17, 19, 26, 30, 20, 15, 21, 11, 8, 8, 19, 5, 8, 8, 11, + 11, 8, 3, 9, 5, 4, 7, 3, 6, 3, 5, 4, 5, 6, +}; + +std::vector build_protestant() { + std::vector books(old_testament.begin(), old_testament.end()); + books.insert(books.end(), new_testament.begin(), new_testament.end()); + return books; +} + +// Catholic: deuterocanon inserted in Vulgate order; Esther with the Greek additions (16), Daniel 14, +// Joel 4 and Malachi 4 per the common Catholic chapter divisions +std::vector build_catholic() { + std::vector books; + for (const auto& b : old_testament) { + if (b.name == "Esther") { + books.push_back({"Tobit", 14}); + books.push_back({"Judith", 16}); + books.push_back({"Esther", 16}); + books.push_back({"1 Maccabees", 16}); + books.push_back({"2 Maccabees", 15}); + } else if (b.name == "Song of Solomon") { + books.push_back(b); + books.push_back({"Wisdom", 19}); + books.push_back({"Sirach", 51}); + } else if (b.name == "Lamentations") { + books.push_back(b); + books.push_back({"Baruch", 6}); + } else if (b.name == "Daniel") { + books.push_back({"Daniel", 14}); + } else if (b.name == "Joel") { + books.push_back({"Joel", 4}); + } else { + books.push_back(b); + } + } + books.insert(books.end(), new_testament.begin(), new_testament.end()); + return books; +} + +// Orthodox: Catholic canon plus 1 Esdras, Prayer of Manasseh, 3 and 4 Maccabees, and Psalm 151 +std::vector build_orthodox() { + std::vector books; + for (const auto& b : build_catholic()) { + if (b.name == "Psalms") { + books.push_back({"Psalms", 151}); + continue; + } + books.push_back(b); + if (b.name == "2 Chronicles") { + books.push_back({"Prayer of Manasseh", 1}); + books.push_back({"1 Esdras", 9}); + } else if (b.name == "2 Maccabees") { + books.push_back({"3 Maccabees", 7}); + books.push_back({"4 Maccabees", 18}); + } + } + return books; +} + +const std::vector& books(AST::Canon canon) { + static const std::vector protestant = build_protestant(); + static const std::vector catholic = build_catholic(); + static const std::vector orthodox = build_orthodox(); + static const std::vector none; + switch (canon) { + case AST::Canon::Protestant: return protestant; + case AST::Canon::Catholic: return catholic; + case AST::Canon::Orthodox: return orthodox; + case AST::Canon::Quran: return none; + } + return none; +} + +// Lowercase, spaces removed: "1 Corinthians" -> "1corinthians" +std::string normalize(std::string_view s) { + std::string out; + for (char c : s) { + if (c == ' ') continue; + out += (c >= 'A' && c <= 'Z') ? static_cast(c - 'A' + 'a') : c; + } + return out; +} + +constexpr std::array, 8> aliases = {{ + {"psalm", "psalms"}, {"songofsongs", "songofsolomon"}, {"canticles", "songofsolomon"}, + {"qoheleth", "ecclesiastes"}, {"ecclesiasticus", "sirach"}, {"wisdomofsolomon", "wisdom"}, + {"revelations", "revelation"}, {"apocalypse", "revelation"}, +}}; + +std::optional find_book(AST::Canon canon, std::string_view name) { + std::string key = normalize(name); + for (const auto& [alias, target] : aliases) { + if (key == alias) key = target; + } + const auto& list = books(canon); + for (size_t i = 0; i < list.size(); ++i) { + if (normalize(list[i].name) == key) return static_cast(i + 1); + } + return std::nullopt; +} + +std::optional to_number(std::string_view s) { + uint16_t value = 0; + auto [ptr, ec] = std::from_chars(s.data(), s.data() + s.size(), value); + if (ec != std::errc{} || ptr != s.data() + s.size() || s.empty()) return std::nullopt; + return value; +} + +// Parses "C", "C:V", "C:V-W", "C:V-C2:W" into ref (chapter/verse fields only) +bool parse_location(std::string_view text, AST::ScriptureRef& ref) { + const size_t dash = text.find('-'); + const std::string_view start = text.substr(0, dash); + const size_t colon = start.find(':'); + auto chapter = to_number(start.substr(0, colon)); + if (!chapter) return false; + ref.chapter = ref.end_chapter = *chapter; + if (colon != std::string_view::npos) { + auto verse = to_number(start.substr(colon + 1)); + if (!verse) return false; + ref.verse = ref.end_verse = *verse; + } + if (dash == std::string_view::npos) return true; + if (ref.verse == 0) return false; + const std::string_view end = text.substr(dash + 1); + const size_t end_colon = end.find(':'); + if (end_colon == std::string_view::npos) { + auto verse = to_number(end); + if (!verse) return false; + ref.end_verse = *verse; + return true; + } + auto end_chapter = to_number(end.substr(0, end_colon)); + auto end_verse = to_number(end.substr(end_colon + 1)); + if (!end_chapter || !end_verse) return false; + ref.end_chapter = *end_chapter; + ref.end_verse = *end_verse; + return true; +} + +} // namespace + +std::optional from_name(std::string_view n) { + if (n == "protestant") return AST::Canon::Protestant; + if (n == "catholic") return AST::Canon::Catholic; + if (n == "orthodox") return AST::Canon::Orthodox; + if (n == "quran") return AST::Canon::Quran; + return std::nullopt; +} + +std::string_view name(AST::Canon canon) { + switch (canon) { + case AST::Canon::Protestant: return "protestant"; + case AST::Canon::Catholic: return "catholic"; + case AST::Canon::Orthodox: return "orthodox"; + case AST::Canon::Quran: return "quran"; + } + return ""; +} + +uint16_t book_count(AST::Canon canon) { return static_cast(books(canon).size()); } + +std::string_view book_name(AST::Canon canon, uint16_t book) { + const auto& list = books(canon); + return book >= 1 && book <= list.size() ? list[book - 1].name : std::string_view{}; +} + +std::expected resolve(AST::Canon canon, std::string_view reference) { + AST::ScriptureRef ref; + ref.canon = canon; + const std::string text(reference); + const auto bad_form = [&] { + return std::unexpected("malformed reference '" + text + "'; expected " + + (canon == AST::Canon::Quran ? "'S:V' or 'S:V-W'" : "'Book C', 'Book C:V' or 'Book C:V-W'")); + }; + + std::string_view location = reference; + uint16_t max_chapter = 0; + if (canon == AST::Canon::Quran) { + max_chapter = static_cast(quran_ayahs.size()); + } else { + const size_t space = reference.rfind(' '); + if (space == std::string_view::npos) return bad_form(); + const std::string_view book_text = reference.substr(0, space); + auto book = find_book(canon, book_text); + if (!book) return std::unexpected("unknown book '" + std::string(book_text) + "' in the " + std::string(name(canon)) + " canon"); + ref.book = *book; + max_chapter = books(canon)[*book - 1].chapters; + location = reference.substr(space + 1); + } + + if (!parse_location(location, ref)) return bad_form(); + + const std::string where = canon == AST::Canon::Quran ? "the Quran" : std::string(book_name(canon, ref.book)); + const std::string unit = canon == AST::Canon::Quran ? "surah" : "chapter"; + if (ref.chapter < 1 || ref.chapter > max_chapter || ref.end_chapter < ref.chapter || ref.end_chapter > max_chapter) { + return std::unexpected(unit + " out of range in '" + text + "': " + where + " has " + std::to_string(max_chapter) + " " + unit + "s"); + } + if (ref.verse != 0 && (ref.end_verse < 1 || (ref.end_chapter == ref.chapter && ref.end_verse < ref.verse))) { + return std::unexpected("verse range is empty or reversed in '" + text + "'"); + } + if (canon == AST::Canon::Quran) { + if (ref.verse > quran_ayahs[ref.chapter - 1] || ref.end_verse > quran_ayahs[ref.end_chapter - 1]) { + return std::unexpected("verse out of range in '" + text + "'"); + } + } + return ref; +} + +std::string format(const AST::ScriptureRef& ref) { + std::string out = ref.canon == AST::Canon::Quran ? "" : std::string(book_name(ref.canon, ref.book)) + " "; + out += std::to_string(ref.chapter); + if (ref.verse == 0) return out; + out += ":" + std::to_string(ref.verse); + if (ref.end_chapter != ref.chapter) return out + "-" + std::to_string(ref.end_chapter) + ":" + std::to_string(ref.end_verse); + if (ref.end_verse != ref.verse) out += "-" + std::to_string(ref.end_verse); + return out; +} + +} // namespace Theos::Scripture diff --git a/src/core/diagnostic.cpp b/src/core/diagnostic.cpp new file mode 100644 index 0000000..b500e11 --- /dev/null +++ b/src/core/diagnostic.cpp @@ -0,0 +1,36 @@ +#include "theos/diagnostic.hpp" +#include + +namespace Theos { + +bool has_errors(const Diagnostics& diags) { + return std::ranges::any_of(diags, [](const Diagnostic& d) { return d.severity == Severity::Error; }); +} + +namespace { +bool is_continuation(char c) { return (static_cast(c) & 0xC0) == 0x80; } + +size_t code_points(std::string_view s) { + return static_cast(std::ranges::count_if(s, [](char c) { return !is_continuation(c); })); +} +} // namespace + +std::string render(const Diagnostic& diag, std::string_view source) { + std::string out = diag.file + ":" + std::to_string(diag.span.line) + ":" + std::to_string(diag.span.col) + ": " + + (diag.severity == Severity::Error ? "error: " : "warning: ") + diag.message + "\n"; + if (diag.span.line == 0 || diag.span.offset > source.size()) return out; + + const size_t line_start = source.rfind('\n', diag.span.offset == 0 ? 0 : diag.span.offset - 1); + const size_t begin = (line_start == std::string_view::npos || diag.span.offset == 0) ? 0 : line_start + 1; + size_t end = std::min(source.find('\n', diag.span.offset), source.size()); + if (end > begin && source[end - 1] == '\r') --end; // CRLF sources (Windows checkouts) + const std::string_view line = source.substr(begin, end - begin); + + const size_t underline_bytes = std::min(std::max(diag.span.length, 1), end - diag.span.offset); + const size_t underline = std::max(code_points(source.substr(diag.span.offset, underline_bytes)), 1); + out += " " + std::string(line) + "\n"; + out += " " + std::string(diag.span.col - 1, ' ') + "^" + std::string(underline - 1, '~') + "\n"; + return out; +} + +} // namespace Theos diff --git a/src/core/driver.cpp b/src/core/driver.cpp new file mode 100644 index 0000000..75e037c --- /dev/null +++ b/src/core/driver.cpp @@ -0,0 +1,44 @@ +#include "theos/driver.hpp" +#include "theos/parser.hpp" +#include "theos/validator.hpp" +#include +#include +#include + +namespace Theos::Driver { + +Result check_source(std::string text, const std::string& path) { + Result result; + result.sources.push_back({path, std::move(text)}); + auto parsed = Parser::parse(result.sources.back().text, path); + if (!parsed) { + result.diagnostics.push_back(parsed.error()); + return result; + } + result.doc = std::move(*parsed); + auto diags = Validator::validate(*result.doc); + result.diagnostics.insert(result.diagnostics.end(), diags.begin(), diags.end()); + return result; +} + +Result check_file(const std::string& path) { + std::ifstream in(path, std::ios::binary); + if (!in) throw std::runtime_error("cannot open '" + path + "'"); + std::ostringstream buffer; + buffer << in.rdbuf(); + return check_source(buffer.str(), path); +} + +std::string render_diagnostics(const Result& result) { + std::string out; + for (const auto& d : result.diagnostics) { + std::string_view text; + for (const auto& s : result.sources) { + if (s.path == d.file) text = s.text; + } + out += render(d, text); + } + return out; +} + +} // namespace Theos::Driver diff --git a/src/core/exporter.cpp b/src/core/exporter.cpp index e5c928b..0ad0625 100644 --- a/src/core/exporter.cpp +++ b/src/core/exporter.cpp @@ -1,62 +1,69 @@ #include "theos/exporter.hpp" -#include +#include "theos/canon.hpp" #include namespace Theos::Exporter { namespace { -// Mermaid labels are double-quoted; entity codes keep quotes and brackets from ending them -std::string escape_label(const std::string& text) { + +// Mermaid labels are double-quoted HTML; entity codes keep quotes and brackets from ending them +std::string escape(const std::string& text) { std::string out; for (char c : text) { switch (c) { case '"': out += "#quot;"; break; case '<': out += "#lt;"; break; case '>': out += "#gt;"; break; + case '\n': out += "
"; break; default: out += c; } } return out; } + +std::string axiom_label(const AST::Axiom& ax) { + switch (ax.kind) { + case AST::AxiomKind::Scripture: return ax.scripture.chapter ? Scripture::format(ax.scripture) : ax.citation; + case AST::AxiomKind::Source: return ax.citation + ", " + ax.locator; + case AST::AxiomKind::Principle: return ax.citation; + } + return ""; +} + } // namespace -std::string to_mermaid(const AST::TheologicalGraph& graph) { +std::string to_mermaid(const AST::Document& doc) { std::ostringstream ss; - ss << "```mermaid\ngraph TD;\n"; - - // Style definitions for visual hierarchy + ss << "flowchart TD\n"; + ss << " classDef axiom fill:#f3e5f5,stroke:#6a1b9a;\n"; ss << " classDef premise fill:#e1f5fe,stroke:#01579b,stroke-width:2px;\n"; - ss << " classDef deduction fill:#fff9c4,stroke:#fbc02d,stroke-width:2px;\n"; - ss << " classDef conclusion fill:#e8f5e9,stroke:#2e7d32,stroke-width:3px;\n\n"; - - // Render nodes with escaped text and styling classes - for (const auto& node : graph.nodes) { - // Format: NodeID["Node Text"] - ss << " " << node.id << "[\"" << node.id << ": " << escape_label(node.text) << "\"];\n"; - - // Apply class based on type - if (node.type == "premise") { - ss << " class " << node.id << " premise;\n"; - } else if (node.type == "deduction") { - ss << " class " << node.id << " deduction;\n"; - } else if (node.type == "conclusion") { - ss << " class " << node.id << " conclusion;\n"; - } - } - - ss << "\n %% Dependencies and Support Edges\n"; - for (const auto& node : graph.nodes) { - // Combine supports and depends_on edges, each parent once - std::set parents(node.supports.begin(), node.supports.end()); - parents.insert(node.depends_on.begin(), node.depends_on.end()); + ss << " classDef deduction fill:#fff9c4,stroke:#f9a825,stroke-width:2px;\n"; + ss << " classDef conclusion fill:#e8f5e9,stroke:#2e7d32,stroke-width:3px;\n"; + ss << " classDef objection fill:#ffebee,stroke:#c62828;\n"; + ss << " classDef reply fill:#fff3e0,stroke:#ef6c00;\n"; + ss << " classDef imported stroke-dasharray:4 3;\n"; - for (const auto& parent : parents) { - ss << " " << parent << " --> " << node.id << ";\n"; - } + for (const auto& ax : doc.axioms) { + ss << " " << ax.id << "([\"" << ax.id << ": " << escape(axiom_label(ax)) << "\"]):::axiom\n"; + } + for (const auto& n : doc.nodes) { + ss << " " << n.id << "[\"" << n.id << ": " << escape(n.text) << "
" + << escape(print(*n.formula, Notation::Unicode)) << "\"]:::" << AST::to_string(n.kind) << "\n"; + if (n.imported) ss << " class " << n.id << " imported\n"; + } + for (const auto& d : doc.dialectics) { + ss << " " << d.id << "{{\"" << d.id << ": " << escape(d.text) << "\"}}:::" << AST::to_string(d.kind) << "\n"; } - ss << "```\n"; + for (const auto& n : doc.nodes) { + for (const auto& g : n.grounded_by) ss << " " << g.name << " -.-> " << n.id << "\n"; + for (const auto& f : n.from) ss << " " << f.name << " --> " << n.id << "\n"; + } + for (const auto& d : doc.dialectics) { + ss << " " << d.id << " -. " << (d.kind == AST::DialecticKind::Objection ? "objects" : "replies") << " .-> " + << d.target.name << "\n"; + } return ss.str(); } -} // namespace Theos::Exporter \ No newline at end of file +} // namespace Theos::Exporter diff --git a/src/core/expr.cpp b/src/core/expr.cpp new file mode 100644 index 0000000..2ea16ca --- /dev/null +++ b/src/core/expr.cpp @@ -0,0 +1,152 @@ +#include "theos/expr.hpp" + +namespace Theos { + +ExprPtr make_symbol(std::string name, Span span) { + return std::make_shared(Expr{ExprKind::Symbol, std::move(name), Sort::Ind, {}, span}); +} + +ExprPtr make_atom(std::string head, std::vector args, Span span) { + return std::make_shared(Expr{ExprKind::Atom, std::move(head), Sort::Ind, std::move(args), span}); +} + +ExprPtr make_eq(ExprPtr lhs, ExprPtr rhs, Span span) { + return std::make_shared(Expr{ExprKind::Eq, "", Sort::Ind, {std::move(lhs), std::move(rhs)}, span}); +} + +ExprPtr make_bottom(Span span) { + return std::make_shared(Expr{ExprKind::Bottom, "", Sort::Ind, {}, span}); +} + +ExprPtr make_unary(ExprKind kind, ExprPtr operand, Span span) { + return std::make_shared(Expr{kind, "", Sort::Ind, {std::move(operand)}, span}); +} + +ExprPtr make_binary(ExprKind kind, ExprPtr lhs, ExprPtr rhs, Span span) { + return std::make_shared(Expr{kind, "", Sort::Ind, {std::move(lhs), std::move(rhs)}, span}); +} + +ExprPtr make_binder(ExprKind kind, std::string var, Sort sort, ExprPtr body, Span span) { + return std::make_shared(Expr{kind, std::move(var), sort, {std::move(body)}, span}); +} + +bool is_binder(ExprKind kind) { + return kind == ExprKind::Forall || kind == ExprKind::Exists || kind == ExprKind::Lambda; +} + +bool is_binary(ExprKind kind) { + return kind == ExprKind::And || kind == ExprKind::Or || kind == ExprKind::Implies || kind == ExprKind::Iff; +} + +namespace { + +struct Spelling { + const char* not_; + const char* and_; + const char* or_; + const char* implies; + const char* iff; + const char* box; + const char* dia; + const char* forall; + const char* exists; + const char* lambda; + const char* bottom; + const char* neq; +}; + +constexpr Spelling ascii{"~", " & ", " | ", " -> ", " <-> ", "[]", "<>", "forall ", "exists ", "\\", "bot", " != "}; +constexpr Spelling unicode{"¬", " ∧ ", " ∨ ", " → ", " ↔ ", "□", "◇", "∀", "∃", "λ", "⊥", " ≠ "}; + +int precedence(ExprKind kind) { + switch (kind) { + case ExprKind::Iff: return 1; + case ExprKind::Implies: return 2; + case ExprKind::Or: return 3; + case ExprKind::And: return 4; + default: return 5; + } +} + +class Printer { +public: + explicit Printer(const Spelling& s) : s_(s) {} + + std::string formula(const Expr& e) const { + switch (e.kind) { + case ExprKind::Symbol: return e.name; + case ExprKind::Lambda: return s_.lambda + binder(e) + ". " + formula(*e.args[0]); + case ExprKind::Atom: return atom(e); + case ExprKind::Eq: return e.args[0]->name + " = " + e.args[1]->name; + case ExprKind::Bottom: return s_.bottom; + case ExprKind::Not: + case ExprKind::Box: + case ExprKind::Dia: { + if (e.kind == ExprKind::Not && e.args[0]->kind == ExprKind::Eq) { + return e.args[0]->args[0]->name + s_.neq + e.args[0]->args[1]->name; + } + const char* op = e.kind == ExprKind::Not ? s_.not_ : e.kind == ExprKind::Box ? s_.box : s_.dia; + return op + operand(*e.args[0]); + } + case ExprKind::And: + case ExprKind::Or: + case ExprKind::Implies: + case ExprKind::Iff: return binary(e); + case ExprKind::Forall: + case ExprKind::Exists: + return (e.kind == ExprKind::Forall ? s_.forall : s_.exists) + binder(e) + ". " + formula(*e.args[0]); + } + return ""; + } + +private: + std::string binder(const Expr& e) const { return e.sort == Sort::Prop ? e.name + ":prop" : e.name; } + + std::string atom(const Expr& e) const { + if (e.args.empty()) return e.name; + std::string out = e.name + "("; + for (size_t i = 0; i < e.args.size(); ++i) { + if (i) out += ", "; + out += formula(*e.args[i]); + } + return out + ")"; + } + + // Operand of a unary operator: binary formulas need parentheses, binders extend right and do not + std::string operand(const Expr& e) const { + return is_binary(e.kind) ? "(" + formula(e) + ")" : formula(e); + } + + std::string side(const Expr& child, ExprKind parent, bool left) const { + if (is_binder(child.kind)) return "(" + formula(child) + ")"; + if (!is_binary(child.kind)) return formula(child); + const int pc = precedence(child.kind); + const int pp = precedence(parent); + bool parens = pc < pp; + if (pc == pp) { + // & and | associate left, -> associates right, <-> does not associate + if (parent == ExprKind::Implies) parens = left; + else if (parent == ExprKind::Iff) parens = true; + else parens = !left; + } + return parens ? "(" + formula(child) + ")" : formula(child); + } + + std::string binary(const Expr& e) const { + const char* op = e.kind == ExprKind::And ? s_.and_ + : e.kind == ExprKind::Or ? s_.or_ + : e.kind == ExprKind::Implies ? s_.implies + : s_.iff; + return side(*e.args[0], e.kind, true) + op + side(*e.args[1], e.kind, false); + } + + const Spelling& s_; +}; + +} // namespace + +std::string print(const Expr& expr, Notation notation) { + return Printer(notation == Notation::Ascii ? ascii : unicode).formula(expr); +} + +} // namespace Theos diff --git a/src/core/format.cpp b/src/core/format.cpp deleted file mode 100644 index 59f0b4a..0000000 --- a/src/core/format.cpp +++ /dev/null @@ -1,206 +0,0 @@ -#include "theos/format.hpp" -#include "theos/ast.hpp" -#include -#include -#include -#include -#include -#include - -namespace Theos { - -// --- BINARY WRITER --- -void write_binary_file(const std::string& filepath, const AST::TheologicalGraph& graph) { - std::ofstream out(filepath, std::ios::binary); - if (!out) { - throw std::runtime_error("Failed to open binary file for writing: " + filepath); - } - - // Build String Heap (index 0 is reserved null terminator) - std::vector string_heap; - string_heap.push_back('\0'); - - auto add_to_heap = [&](const std::string& s) -> uint32_t { - if (s.empty()) return 0; - uint32_t offset = static_cast(string_heap.size()); - for (char c : s) { - string_heap.push_back(c); - } - string_heap.push_back('\0'); - return offset; - }; - - // Pre-calculate offsets - TheosHeader header{}; - header.magic = THEOS_MAGIC; - header.version = 1; - header.axiom_count = static_cast(graph.axioms.size()); - header.node_count = static_cast(graph.nodes.size()); - - header.axiom_table_offset = sizeof(TheosHeader); - header.node_table_offset = header.axiom_table_offset + header.axiom_count * (sizeof(uint32_t) * 2 + sizeof(uint16_t) + sizeof(uint8_t) * 2); - - // We will compute string heap offset after serializing tables if needed, - // or place it right after the node table. Let's build node records to calculate size. - - // Serialize Axioms into a temp buffer - std::vector axiom_table_data; - for (const auto& ax : graph.axioms) { - uint32_t name_off = add_to_heap(ax.name); - uint32_t book_off = add_to_heap(ax.book_name); - uint16_t chapter = ax.chapter; - uint8_t start_v = ax.start_verse; - uint8_t end_v = ax.end_verse; - - auto append_bytes = [&](const void* data, size_t size) { - const char* p = reinterpret_cast(data); - axiom_table_data.insert(axiom_table_data.end(), p, p + size); - }; - - append_bytes(&name_off, sizeof(name_off)); - append_bytes(&book_off, sizeof(book_off)); - append_bytes(&chapter, sizeof(chapter)); - append_bytes(&start_v, sizeof(start_v)); - append_bytes(&end_v, sizeof(end_v)); - } - - // Serialize Nodes into a temp buffer - std::vector node_table_data; - for (const auto& node : graph.nodes) { - uint32_t id_off = add_to_heap(node.id); - uint32_t type_off = add_to_heap(node.type); - uint32_t text_off = add_to_heap(node.text); - - auto append_bytes = [&](const void* data, size_t size) { - const char* p = reinterpret_cast(data); - node_table_data.insert(node_table_data.end(), p, p + size); - }; - - append_bytes(&id_off, sizeof(id_off)); - append_bytes(&type_off, sizeof(type_off)); - append_bytes(&text_off, sizeof(text_off)); - - // Supports list - uint16_t sup_count = static_cast(node.supports.size()); - append_bytes(&sup_count, sizeof(sup_count)); - for (const auto& sup : node.supports) { - uint32_t sup_off = add_to_heap(sup); - append_bytes(&sup_off, sizeof(sup_off)); - } - - // Depends on list - uint16_t dep_count = static_cast(node.depends_on.size()); - append_bytes(&dep_count, sizeof(dep_count)); - for (const auto& dep : node.depends_on) { - uint32_t dep_off = add_to_heap(dep); - append_bytes(&dep_off, sizeof(dep_off)); - } - } - - // Finalize header offsets explicitly - header.axiom_table_offset = sizeof(TheosHeader); - header.node_table_offset = header.axiom_table_offset + static_cast(axiom_table_data.size()); - header.string_heap_offset = header.node_table_offset + static_cast(node_table_data.size()); - - // Write everything out - out.write(reinterpret_cast(&header), sizeof(header)); - if (!axiom_table_data.empty()) { - out.write(axiom_table_data.data(), axiom_table_data.size()); - } - if (!node_table_data.empty()) { - out.write(node_table_data.data(), node_table_data.size()); - } - if (!string_heap.empty()) { - out.write(string_heap.data(), string_heap.size()); - } -} - -// --- BINARY READER --- -namespace { - -// Bounds-checked sequential reader over the file buffer -class Cursor { -public: - Cursor(const std::vector& buf, size_t pos) : buf_(buf), pos_(pos) { - if (pos > buf.size()) throw std::runtime_error("Invalid binary file: table offset past end of file."); - } - - template - T read() { - if (buf_.size() - pos_ < sizeof(T)) throw std::runtime_error("Invalid binary file: unexpected end of data."); - T value; - std::memcpy(&value, buf_.data() + pos_, sizeof(T)); - pos_ += sizeof(T); - return value; - } - -private: - const std::vector& buf_; - size_t pos_; -}; - -} // namespace - -AST::TheologicalGraph read_binary_file(const std::string& filepath) { - std::ifstream in(filepath, std::ios::binary); - if (!in) { - throw std::runtime_error("Failed to open binary file for reading: " + filepath); - } - const std::vector buffer{std::istreambuf_iterator(in), {}}; - - if (buffer.size() < sizeof(TheosHeader)) { - throw std::runtime_error("Invalid binary file: File too small."); - } - TheosHeader header; - std::memcpy(&header, buffer.data(), sizeof(header)); - if (header.magic != THEOS_MAGIC) { - throw std::runtime_error("Invalid binary file: Bad magic number."); - } - if (header.string_heap_offset >= buffer.size()) { - throw std::runtime_error("Invalid binary file: string heap offset past end of file."); - } - - auto get_string_from_heap = [&](uint32_t offset) -> std::string { - if (offset == 0) return ""; - const size_t start = size_t{header.string_heap_offset} + offset; - if (start >= buffer.size()) throw std::runtime_error("Invalid binary file: string offset past end of file."); - const auto end = std::find(buffer.begin() + static_cast(start), buffer.end(), '\0'); - if (end == buffer.end()) throw std::runtime_error("Invalid binary file: unterminated string."); - return std::string(buffer.begin() + static_cast(start), end); - }; - - AST::TheologicalGraph graph; - - Cursor axioms(buffer, header.axiom_table_offset); - for (uint16_t i = 0; i < header.axiom_count; ++i) { - AST::Axiom ax; - ax.name = get_string_from_heap(axioms.read()); - ax.book_name = get_string_from_heap(axioms.read()); - ax.book_id = 0; - ax.chapter = axioms.read(); - ax.start_verse = axioms.read(); - ax.end_verse = axioms.read(); - graph.axioms.push_back(ax); - } - - Cursor nodes(buffer, header.node_table_offset); - for (uint16_t i = 0; i < header.node_count; ++i) { - AST::Node node; - node.id = get_string_from_heap(nodes.read()); - node.type = get_string_from_heap(nodes.read()); - node.text = get_string_from_heap(nodes.read()); - const auto supports_count = nodes.read(); - for (uint16_t s = 0; s < supports_count; ++s) { - node.supports.push_back(get_string_from_heap(nodes.read())); - } - const auto depends_count = nodes.read(); - for (uint16_t d = 0; d < depends_count; ++d) { - node.depends_on.push_back(get_string_from_heap(nodes.read())); - } - graph.nodes.push_back(node); - } - - return graph; -} - -} // namespace Theos \ No newline at end of file diff --git a/src/core/lexer.cpp b/src/core/lexer.cpp new file mode 100644 index 0000000..40b0187 --- /dev/null +++ b/src/core/lexer.cpp @@ -0,0 +1,220 @@ +#include "theos/lexer.hpp" +#include +#include +#include + +namespace Theos { + +namespace { + +constexpr std::array keywords = { + "argument", "by", "import", "axiom", "scripture", "source", "principle", "define", + "premise", "deduction", "conclusion", "from", "grounded_by", "text", "formula", + "proof", "box", "objection", "reply", "against", "to", "ind", "prop", +}; + +// Multi-character and Unicode operators, longest first so "<->" wins over "<>" +constexpr std::array, 19> operators = {{ + {"<->", Tok::Iff}, {"↔", Tok::Iff}, {"->", Tok::Implies}, {"→", Tok::Implies}, + {"<>", Tok::Diamond}, {"◇", Tok::Diamond}, {"□", Tok::Box}, {":=", Tok::Define}, + {"!=", Tok::NotEquals}, {"≠", Tok::NotEquals}, {"¬", Tok::Not}, {"∧", Tok::And}, + {"∨", Tok::Or}, {"λ", Tok::Lambda}, {"⊥", Tok::Bottom}, {"∀", Tok::Forall}, + {"∃", Tok::Exists}, {"~", Tok::Not}, {"&", Tok::And}, +}}; + +constexpr std::array, 13> single = {{ + {'{', Tok::LBrace}, {'}', Tok::RBrace}, {'[', Tok::LBracket}, {']', Tok::RBracket}, + {'(', Tok::LParen}, {')', Tok::RParen}, {',', Tok::Comma}, {'.', Tok::Dot}, + {':', Tok::Colon}, {'=', Tok::Equals}, {'-', Tok::Minus}, {'|', Tok::Or}, + {'\\', Tok::Lambda}, +}}; + +bool is_ident_start(char c) { return (c >= 'a' && c <= 'z') || (c >= 'A' && c <= 'Z') || c == '_'; } +bool is_digit(char c) { return c >= '0' && c <= '9'; } + +class Lexer { +public: + Lexer(std::string_view src, const std::string& file) : src_(src), file_(file) {} + + std::expected, Diagnostic> run() { + std::vector tokens; + while (true) { + if (auto err = skip_trivia()) return std::unexpected(*err); + const Span start = here(); + if (pos_ >= src_.size()) { + tokens.push_back({Tok::End, "", start}); + return tokens; + } + auto tok = next(start); + if (!tok) return std::unexpected(tok.error()); + tokens.push_back(std::move(*tok)); + } + } + +private: + Span here() const { return Span{line_, col_, static_cast(pos_), 0}; } + + void advance(size_t bytes) { + for (size_t i = 0; i < bytes && pos_ < src_.size(); ++i, ++pos_) { + const char c = src_[pos_]; + if (c == '\n') { + ++line_; + col_ = 1; + } else if ((static_cast(c) & 0xC0) != 0x80) { + ++col_; + } + } + } + + Diagnostic error(Span span, std::string message) const { + return Diagnostic{Severity::Error, file_, span, std::move(message)}; + } + + Token finish(Tok kind, Span start, std::string text) const { + start.length = static_cast(pos_ - start.offset); + return Token{kind, std::move(text), start}; + } + + std::optional skip_trivia() { + while (pos_ < src_.size()) { + const char c = src_[pos_]; + if (c == ' ' || c == '\t' || c == '\r' || c == '\n') { + advance(1); + } else if (src_.substr(pos_, 2) == "//") { + while (pos_ < src_.size() && src_[pos_] != '\n') advance(1); + } else if (src_.substr(pos_, 2) == "/*") { + Span start = here(); + start.length = 2; + const size_t close = src_.find("*/", pos_ + 2); + if (close == std::string_view::npos) return error(start, "unterminated block comment"); + advance(close + 2 - pos_); + } else { + break; + } + } + return std::nullopt; + } + + std::expected next(Span start) { + const char c = src_[pos_]; + + if (is_ident_start(c)) { + size_t end = pos_; + while (end < src_.size() && (is_ident_start(src_[end]) || is_digit(src_[end]))) ++end; + std::string word(src_.substr(pos_, end - pos_)); + advance(end - pos_); + if (word == "forall") return finish(Tok::Forall, start, word); + if (word == "exists") return finish(Tok::Exists, start, word); + if (word == "lambda") return finish(Tok::Lambda, start, word); + if (word == "bot") return finish(Tok::Bottom, start, word); + for (const char* kw : keywords) { + if (word == kw) return finish(Tok::Keyword, start, word); + } + return finish(Tok::Ident, start, word); + } + + if (is_digit(c)) { + size_t end = pos_; + while (end < src_.size() && is_digit(src_[end])) ++end; + std::string digits(src_.substr(pos_, end - pos_)); + advance(end - pos_); + return finish(Tok::Number, start, digits); + } + + if (c == '"') return string_literal(start); + + for (const auto& [spelling, kind] : operators) { + if (src_.substr(pos_, spelling.size()) == spelling) { + advance(spelling.size()); + return finish(kind, start, std::string(spelling)); + } + } + for (const auto& [ch, kind] : single) { + if (c == ch) { + advance(1); + return finish(kind, start, std::string(1, ch)); + } + } + + start.length = 1; + return std::unexpected(error(start, std::string("unexpected character '") + c + "'")); + } + + std::expected string_literal(Span start) { + advance(1); + std::string value; + while (true) { + if (pos_ >= src_.size() || src_[pos_] == '\n') { + start.length = 1; + return std::unexpected(error(start, "unterminated string")); + } + const char c = src_[pos_]; + if (c == '"') { + advance(1); + return finish(Tok::String, start, value); + } + if (c == '\\') { + const char e = pos_ + 1 < src_.size() ? src_[pos_ + 1] : '\0'; + if (e != '"' && e != '\\' && e != 'n') { + Span at = here(); + at.length = 2; + return std::unexpected(error(at, "unknown escape sequence")); + } + value += e == 'n' ? '\n' : e; + advance(2); + continue; + } + value += c; + advance(1); + } + } + + std::string_view src_; + const std::string& file_; + size_t pos_ = 0; + uint32_t line_ = 1; + uint32_t col_ = 1; +}; + +} // namespace + +std::string_view describe(Tok kind) { + switch (kind) { + case Tok::Ident: return "identifier"; + case Tok::Keyword: return "keyword"; + case Tok::Number: return "number"; + case Tok::String: return "string"; + case Tok::LBrace: return "'{'"; + case Tok::RBrace: return "'}'"; + case Tok::LBracket: return "'['"; + case Tok::RBracket: return "']'"; + case Tok::LParen: return "'('"; + case Tok::RParen: return "')'"; + case Tok::Comma: return "','"; + case Tok::Dot: return "'.'"; + case Tok::Colon: return "':'"; + case Tok::Equals: return "'='"; + case Tok::Define: return "':='"; + case Tok::Minus: return "'-'"; + case Tok::Not: return "'~'"; + case Tok::And: return "'&'"; + case Tok::Or: return "'|'"; + case Tok::Implies: return "'->'"; + case Tok::Iff: return "'<->'"; + case Tok::Box: return "'[]'"; + case Tok::Diamond: return "'<>'"; + case Tok::Lambda: return "lambda"; + case Tok::Bottom: return "'bot'"; + case Tok::NotEquals: return "'!='"; + case Tok::Forall: return "'forall'"; + case Tok::Exists: return "'exists'"; + case Tok::End: return "end of file"; + } + return "token"; +} + +std::expected, Diagnostic> lex(std::string_view source, const std::string& file) { + return Lexer(source, file).run(); +} + +} // namespace Theos diff --git a/src/core/parser.cpp b/src/core/parser.cpp index fb399bb..a9e94f6 100644 --- a/src/core/parser.cpp +++ b/src/core/parser.cpp @@ -1,166 +1,501 @@ #include "theos/parser.hpp" -#include "theos/format.hpp" -#include -#include -#include -#include -#include +#include "theos/lexer.hpp" +#include +#include namespace Theos::Parser { namespace { -// Helper to trim whitespace -std::string trim(const std::string& str) { - size_t first = str.find_first_not_of(" \t\r\n"); - if (first == std::string::npos) return ""; - size_t last = str.find_last_not_of(" \t\r\n"); - return str.substr(first, (last - first + 1)); -} - -// Map common book names to IDs (1-66) -uint8_t resolve_book_id(const std::string& book_name) { - if (book_name == "Matthew") return 40; - if (book_name == "Luke") return 42; - if (book_name == "John") return 43; - if (book_name == "Romans") return 45; - if (book_name == "1Corinthians") return 46; - if (book_name == "Galatians") return 48; - // Default fallback / place-holder mapping - return 1; -} +// Thrown internally to unwind to parse(); never escapes this file +struct SyntaxError { + Diagnostic diag; +}; -// Parses comma-separated array strings like "[P1, P2]" into std::vector -std::vector parse_string_list(const std::string& list_str) { - std::vector items; - size_t start = list_str.find('['); - size_t end = list_str.find(']'); - if (start == std::string::npos || end == std::string::npos) return items; +class Parser { +public: + Parser(std::vector tokens, std::string file) : toks_(std::move(tokens)), file_(std::move(file)) {} - std::string content = list_str.substr(start + 1, end - start - 1); - std::stringstream ss(content); - std::string item; - while (std::getline(ss, item, ',')) { - std::string cleaned = trim(item); - if (!cleaned.empty()) { - items.push_back(cleaned); + AST::Document document() { + AST::Document doc; + doc.file = file_; + if (accept_keyword("argument")) { + doc.title = expect(Tok::String, "argument title").text; + if (accept_keyword("by")) doc.author = expect(Tok::String, "author name").text; } + while (!at(Tok::End)) item(doc); + return doc; } - return items; -} -} // anonymous namespace + ExprPtr standalone_formula() { + auto f = formula(); + expect(Tok::End, "end of formula"); + return f; + } -AST::TheologicalGraph parse_string(const std::string& source) { - AST::TheologicalGraph graph; - std::stringstream stream(source); - std::string line; +private: + // ---- token helpers ---- - bool in_node_block = false; - AST::Node current_node; + const Token& peek(size_t ahead = 0) const { return toks_[std::min(pos_ + ahead, toks_.size() - 1)]; } + bool at(Tok kind) const { return peek().kind == kind; } + bool at_keyword(std::string_view kw) const { return at(Tok::Keyword) && peek().text == kw; } + const Token& advance() { return toks_[pos_ < toks_.size() - 1 ? pos_++ : pos_]; } - while (std::getline(stream, line)) { - std::string trimmed = trim(line); - if (trimmed.empty() || trimmed.rfind("//", 0) == 0) continue; // Skip empty & comments + [[noreturn]] void fail(const Span& span, std::string message) const { + throw SyntaxError{Diagnostic{Severity::Error, file_, span, std::move(message)}}; + } - // Parse Metadata: title: "..." - if (trimmed.rfind("title:", 0) == 0) { - size_t q1 = trimmed.find('"'); - size_t q2 = trimmed.rfind('"'); - if (q1 != std::string::npos && q2 != std::string::npos && q2 > q1) { - graph.title = trimmed.substr(q1 + 1, q2 - q1 - 1); + [[noreturn]] void fail_expected(std::string_view what) const { + const Token& t = peek(); + std::string found = t.kind == Tok::End ? "end of file" : "'" + t.text + "'"; + fail(t.span, "expected " + std::string(what) + ", found " + found); + } + + const Token& expect(Tok kind, std::string_view what) { + if (!at(kind)) fail_expected(what); + return advance(); + } + + void expect_keyword(std::string_view kw) { + if (!at_keyword(kw)) fail_expected("'" + std::string(kw) + "'"); + advance(); + } + + bool accept(Tok kind) { + if (!at(kind)) return false; + advance(); + return true; + } + + bool accept_keyword(std::string_view kw) { + if (!at_keyword(kw)) return false; + advance(); + return true; + } + + AST::Ref ident(std::string_view what) { + const Token& t = expect(Tok::Ident, what); + return AST::Ref{t.text, t.span}; + } + + uint32_t number(const Token& t) const { + uint32_t value = 0; + auto [ptr, ec] = std::from_chars(t.text.data(), t.text.data() + t.text.size(), value); + if (ec != std::errc{}) fail(t.span, "number out of range"); + return value; + } + + static Span join(Span a, const Span& b) { + a.length = b.offset + b.length - a.offset; + return a; + } + + Span prev_span() const { return toks_[pos_ == 0 ? 0 : pos_ - 1].span; } + + // ---- items ---- + + void item(AST::Document& doc) { + const Token& t = peek(); + if (t.kind != Tok::Keyword) fail_expected("an item (import, axiom, define, premise, deduction, conclusion, objection or reply)"); + if (t.text == "import") return import(doc); + if (t.text == "axiom") return axiom(doc); + if (t.text == "define") return definition(doc); + if (t.text == "premise" || t.text == "deduction" || t.text == "conclusion") return node(doc); + if (t.text == "objection" || t.text == "reply") return dialectic(doc); + if (t.text == "argument") fail(t.span, "the 'argument' header must come first and appear once"); + fail_expected("an item (import, axiom, define, premise, deduction, conclusion, objection or reply)"); + } + + void import(AST::Document& doc) { + const Span start = advance().span; + const Token& path = expect(Tok::String, "import path"); + doc.imports.push_back(AST::Import{path.text, join(start, path.span)}); + } + + void axiom(AST::Document& doc) { + const Span start = advance().span; + AST::Axiom ax; + auto id = ident("axiom name"); + ax.id = id.name; + expect(Tok::Equals, "'='"); + if (accept_keyword("scripture")) { + ax.kind = AST::AxiomKind::Scripture; + expect(Tok::LParen, "'('"); + ax.canon = ident("canon name (protestant, catholic, orthodox, quran)").name; + expect(Tok::Comma, "','"); + ax.citation = expect(Tok::String, "scripture reference").text; + expect(Tok::RParen, "')'"); + } else if (accept_keyword("source")) { + ax.kind = AST::AxiomKind::Source; + expect(Tok::LParen, "'('"); + ax.citation = expect(Tok::String, "work title").text; + expect(Tok::Comma, "','"); + ax.locator = expect(Tok::String, "locator").text; + expect(Tok::RParen, "')'"); + } else if (accept_keyword("principle")) { + ax.kind = AST::AxiomKind::Principle; + expect(Tok::LParen, "'('"); + ax.citation = expect(Tok::String, "principle statement").text; + expect(Tok::RParen, "')'"); + } else { + fail_expected("'scripture', 'source' or 'principle'"); + } + ax.span = join(start, prev_span()); + doc.axioms.push_back(std::move(ax)); + } + + void definition(AST::Document& doc) { + const Span start = advance().span; + AST::Definition def; + def.id = ident("definition name").name; + if (accept(Tok::LParen)) { + do { + def.params.push_back(binder()); + } while (accept(Tok::Comma)); + expect(Tok::RParen, "')'"); + } + expect(Tok::Define, "':='"); + def.body = formula(); + def.span = join(start, prev_span()); + doc.definitions.push_back(std::move(def)); + } + + std::vector id_list() { + std::vector ids; + expect(Tok::LBracket, "'['"); + do { + ids.push_back(ident("name")); + } while (accept(Tok::Comma)); + expect(Tok::RBracket, "']'"); + return ids; + } + + void node(AST::Document& doc) { + const Token& kw = advance(); + AST::Node n; + n.kind = kw.text == "premise" ? AST::NodeKind::Premise + : kw.text == "deduction" ? AST::NodeKind::Deduction + : AST::NodeKind::Conclusion; + n.id = ident("node name").name; + + bool seen_from = false, seen_grounds = false; + while (!at(Tok::LBrace)) { + const Token& clause = peek(); + if (accept_keyword("from")) { + if (seen_from) fail(clause.span, "'from' given twice"); + seen_from = true; + n.from = id_list(); + } else if (accept_keyword("grounded_by")) { + if (seen_grounds) fail(clause.span, "'grounded_by' given twice"); + seen_grounds = true; + n.grounded_by = id_list(); + } else if (accept_keyword("by")) { + if (n.rule) fail(clause.span, "'by' given twice"); + n.rule = rule_name(); + } else { + fail_expected("'from', 'grounded_by', 'by' or '{'"); } - continue; } - // Parse Metadata: author: "..." - if (trimmed.rfind("author:", 0) == 0) { - size_t q1 = trimmed.find('"'); - size_t q2 = trimmed.rfind('"'); - if (q1 != std::string::npos && q2 != std::string::npos && q2 > q1) { - graph.author = trimmed.substr(q1 + 1, q2 - q1 - 1); + Fields f = fields(true); + n.text = std::move(f.text); + n.formula = std::move(f.formula); + n.proof = std::move(f.proof); + n.span = join(kw.span, prev_span()); + if (!f.has_text) fail(n.span, "node '" + n.id + "' is missing 'text'"); + if (!n.formula) fail(n.span, "node '" + n.id + "' is missing 'formula'"); + doc.nodes.push_back(std::move(n)); + } + + void dialectic(AST::Document& doc) { + const Token& kw = advance(); + AST::Dialectic d; + d.kind = kw.text == "objection" ? AST::DialecticKind::Objection : AST::DialecticKind::Reply; + d.id = ident(kw.text + " name").name; + expect_keyword(d.kind == AST::DialecticKind::Objection ? "against" : "to"); + d.target = ident("target name"); + Fields f = fields(false); + d.text = std::move(f.text); + d.formula = std::move(f.formula); + d.span = join(kw.span, prev_span()); + if (!f.has_text) fail(d.span, kw.text + " '" + d.id + "' is missing 'text'"); + doc.dialectics.push_back(std::move(d)); + } + + struct Fields { + bool has_text = false; + std::string text; + ExprPtr formula; + std::optional proof; + }; + + Fields fields(bool allow_proof) { + Fields f; + expect(Tok::LBrace, "'{'"); + while (!accept(Tok::RBrace)) { + const Token& t = peek(); + if (accept_keyword("text")) { + if (f.has_text) fail(t.span, "'text' given twice"); + expect(Tok::Colon, "':'"); + f.text = expect(Tok::String, "text string").text; + f.has_text = true; + } else if (accept_keyword("formula")) { + if (f.formula) fail(t.span, "'formula' given twice"); + expect(Tok::Colon, "':'"); + f.formula = formula(); + } else if (allow_proof && at_keyword("proof")) { + if (f.proof) fail(t.span, "'proof' given twice"); + f.proof = proof(); + } else { + fail_expected(allow_proof ? "'text', 'formula', 'proof' or '}'" : "'text', 'formula' or '}'"); } - continue; - } - - // Parse Axioms: axiom Name = scripture(Book, Ch, Start, End) - if (trimmed.rfind("axiom", 0) == 0) { - size_t eq_pos = trimmed.find('='); - if (eq_pos != std::string::npos) { - std::string header = trim(trimmed.substr(5, eq_pos - 5)); - AST::Axiom ax; - ax.name = header; - - size_t p_start = trimmed.find('(', eq_pos); - size_t p_end = trimmed.rfind(')'); - if (p_start != std::string::npos && p_end != std::string::npos) { - std::string args_str = trimmed.substr(p_start + 1, p_end - p_start - 1); - std::stringstream ss(args_str); - std::string book, ch, start_v, end_v; - if (std::getline(ss, book, ',') && - std::getline(ss, ch, ',') && - std::getline(ss, start_v, ',') && - std::getline(ss, end_v, ',')) { - - ax.book_name = trim(book); - ax.book_id = resolve_book_id(ax.book_name); - ax.chapter = static_cast(std::stoi(trim(ch))); - ax.start_verse = static_cast(std::stoi(trim(start_v))); - ax.end_verse = static_cast(std::stoi(trim(end_v))); - graph.axioms.push_back(ax); - } - } + } + return f; + } + + // Rule names are identifiers, plus the keyword 'premise' + AST::Ref rule_name() { + if (at(Tok::Ident) || at_keyword("premise")) { + const Token& t = advance(); + return AST::Ref{t.text, t.span}; + } + fail_expected("rule name"); + } + + // ---- proofs ---- + + AST::Proof proof() { + AST::Proof p; + p.span = advance().span; + expect(Tok::LBrace, "'{'"); + while (!accept(Tok::RBrace)) p.items.push_back(proof_item()); + p.span = join(p.span, prev_span()); + return p; + } + + AST::ProofItem proof_item() { + if (at(Tok::Number)) return proof_line(); + if (at(Tok::LBrace) || at_keyword("box")) return subproof(); + fail_expected("proof line number, '{', 'box' or '}'"); + } + + AST::ProofItem subproof() { + AST::Subproof sub; + sub.span = peek().span; + sub.strict = accept_keyword("box"); + expect(Tok::LBrace, "'{'"); + if (accept(Tok::LBracket)) { + sub.fresh = ident("fresh name"); + expect(Tok::RBracket, "']'"); + } + while (!accept(Tok::RBrace)) sub.items.push_back(proof_item()); + sub.span = join(sub.span, prev_span()); + return sub; + } + + AST::ProofItem proof_line() { + AST::ProofLine line; + const Token& num = advance(); + line.number = number(num); + expect(Tok::Dot, "'.' after line number"); + line.formula = formula(); + line.rule = rule_name(); + // A number followed by '.' starts the next line rather than being a reference + if ((at(Tok::Number) || at(Tok::Ident)) && peek(1).kind != Tok::Dot) { + line.refs.push_back(proof_ref()); + while (accept(Tok::Comma)) line.refs.push_back(proof_ref()); + } + line.span = join(num.span, prev_span()); + return line; + } + + AST::ProofRef proof_ref() { + AST::ProofRef ref; + ref.span = peek().span; + if (at(Tok::Ident)) { + ref.kind = AST::ProofRef::Kind::Name; + ref.name = advance().text; + return ref; + } + ref.first = number(expect(Tok::Number, "line number or name")); + if (accept(Tok::Minus)) { + ref.kind = AST::ProofRef::Kind::Range; + ref.last = number(expect(Tok::Number, "range end")); + ref.span = join(ref.span, prev_span()); + } + return ref; + } + + // ---- formulas ---- + + ExprPtr formula() { return iff(); } + + ExprPtr iff() { + auto lhs = implies(); + if (at(Tok::Iff)) { + advance(); + auto rhs = implies(); + return make_binary(ExprKind::Iff, lhs, rhs, join(lhs->span, rhs->span)); + } + return lhs; + } + + ExprPtr implies() { + auto lhs = disjunction(); + if (at(Tok::Implies)) { + advance(); + auto rhs = implies(); + return make_binary(ExprKind::Implies, lhs, rhs, join(lhs->span, rhs->span)); + } + return lhs; + } + + ExprPtr disjunction() { + auto lhs = conjunction(); + while (at(Tok::Or)) { + advance(); + auto rhs = conjunction(); + lhs = make_binary(ExprKind::Or, lhs, rhs, join(lhs->span, rhs->span)); + } + return lhs; + } + + ExprPtr conjunction() { + auto lhs = unary(); + while (at(Tok::And)) { + advance(); + auto rhs = unary(); + lhs = make_binary(ExprKind::And, lhs, rhs, join(lhs->span, rhs->span)); + } + return lhs; + } + + // "[]" is necessity only when the brackets touch + bool at_box() const { + if (at(Tok::Box)) return true; + return at(Tok::LBracket) && peek(1).kind == Tok::RBracket && + peek(1).span.offset == peek().span.offset + 1; + } + + ExprPtr unary() { + const Span start = peek().span; + if (accept(Tok::Not)) { + auto e = unary(); + return make_unary(ExprKind::Not, e, join(start, e->span)); + } + if (at_box()) { + if (!accept(Tok::Box)) { + advance(); + advance(); } - continue; - } - - // Parse Node Header: premise P1 { or deduction D1 { or conclusion C1 { - if (!in_node_block && (trimmed.rfind("premise", 0) == 0 || trimmed.rfind("deduction", 0) == 0 || trimmed.rfind("conclusion", 0) == 0)) { - size_t space_pos = trimmed.find(' '); - size_t brace_pos = trimmed.find('{'); - if (space_pos != std::string::npos && brace_pos != std::string::npos) { - current_node = AST::Node{}; - current_node.type = trim(trimmed.substr(0, space_pos)); - current_node.id = trim(trimmed.substr(space_pos + 1, brace_pos - space_pos - 1)); - in_node_block = true; + auto e = unary(); + return make_unary(ExprKind::Box, e, join(start, e->span)); + } + if (accept(Tok::Diamond)) { + auto e = unary(); + return make_unary(ExprKind::Dia, e, join(start, e->span)); + } + if (at(Tok::Forall) || at(Tok::Exists)) { + const ExprKind kind = advance().kind == Tok::Forall ? ExprKind::Forall : ExprKind::Exists; + std::vector binders; + do { + binders.push_back(binder()); + } while (at(Tok::Ident)); + expect(Tok::Dot, "'.' after quantified variables"); + auto body = formula(); + for (auto it = binders.rbegin(); it != binders.rend(); ++it) { + body = make_binder(kind, it->name, it->sort, body, join(start, body->span)); } - continue; + return body; } + return atom(); + } - // Inside a Node Block ({ ... }) - if (in_node_block) { - if (trimmed == "}") { - graph.nodes.push_back(current_node); - in_node_block = false; - continue; - } + AST::Binder binder() { + auto name = ident("variable name"); + AST::Binder b{name.name, Sort::Ind, name.span}; + if (accept(Tok::Colon)) { + if (accept_keyword("prop")) b.sort = Sort::Prop; + else if (!accept_keyword("ind")) fail_expected("sort 'ind' or 'prop'"); + } + return b; + } - if (trimmed.rfind("text:", 0) == 0) { - size_t q1 = trimmed.find('"'); - size_t q2 = trimmed.rfind('"'); - if (q1 != std::string::npos && q2 != std::string::npos && q2 > q1) { - current_node.text = trimmed.substr(q1 + 1, q2 - q1 - 1); - } - } else if (trimmed.rfind("supports:", 0) == 0) { - current_node.supports = parse_string_list(trimmed); - } else if (trimmed.rfind("depends_on:", 0) == 0) { - current_node.depends_on = parse_string_list(trimmed); + ExprPtr atom() { + const Token& t = peek(); + if (accept(Tok::LParen)) { + auto inner = formula(); + expect(Tok::RParen, "')'"); + return inner; + } + if (accept(Tok::Bottom)) return make_bottom(t.span); + if (at(Tok::Ident)) { + const Token& name = advance(); + if (accept(Tok::LParen)) { + std::vector args; + do { + args.push_back(term()); + } while (accept(Tok::Comma)); + expect(Tok::RParen, "')'"); + return make_atom(name.text, std::move(args), join(name.span, prev_span())); + } + if (at(Tok::Equals) || at(Tok::NotEquals)) { + const bool negated = advance().kind == Tok::NotEquals; + const Token& rhs = expect(Tok::Ident, "identifier after '='"); + const Span span = join(name.span, rhs.span); + auto eq = make_eq(make_symbol(name.text, name.span), make_symbol(rhs.text, rhs.span), span); + return negated ? make_unary(ExprKind::Not, eq, span) : eq; } + return make_atom(name.text, {}, name.span); } + fail_expected("formula"); } - return graph; -} + ExprPtr term() { + if (at(Tok::LParen) && peek(1).kind == Tok::Lambda) { + advance(); + auto l = lambda(); + expect(Tok::RParen, "')'"); + return l; + } + if (at(Tok::Lambda)) return lambda(); + const Token& name = expect(Tok::Ident, "term (name or lambda)"); + return make_symbol(name.text, name.span); + } -AST::TheologicalGraph parse_file(const std::string& filepath) { - std::ifstream file(filepath); - if (!file.is_open()) { - throw std::runtime_error("Could not open .theo file: " + filepath); + ExprPtr lambda() { + const Span start = advance().span; + auto b = binder(); + expect(Tok::Dot, "'.' after lambda variable"); + auto body = formula(); + return make_binder(ExprKind::Lambda, b.name, b.sort, body, join(start, body->span)); } - std::stringstream buffer; - buffer << file.rdbuf(); - return parse_string(buffer.str()); + std::vector toks_; + std::string file_; + size_t pos_ = 0; +}; + +} // namespace + +std::expected parse(std::string_view source, const std::string& file) { + auto tokens = lex(source, file); + if (!tokens) return std::unexpected(tokens.error()); + try { + return Parser(std::move(*tokens), file).document(); + } catch (const SyntaxError& e) { + return std::unexpected(e.diag); + } +} + +std::expected parse_formula(std::string_view source) { + auto tokens = lex(source, ""); + if (!tokens) return std::unexpected(tokens.error()); + try { + return Parser(std::move(*tokens), "").standalone_formula(); + } catch (const SyntaxError& e) { + return std::unexpected(e.diag); + } } -} // namespace Theos::Parser \ No newline at end of file +} // namespace Theos::Parser diff --git a/src/core/validator.cpp b/src/core/validator.cpp index f6a81cc..6fe532e 100644 --- a/src/core/validator.cpp +++ b/src/core/validator.cpp @@ -1,89 +1,189 @@ #include "theos/validator.hpp" -#include -#include +#include "theos/canon.hpp" #include +#include +#include +#include namespace Theos::Validator { -ValidationResult validate(const AST::TheologicalGraph& graph) { - ValidationResult result; - std::unordered_set node_ids; - bool has_premise = false; - bool has_conclusion = false; - - // 1. Collect all node IDs and check basic types - for (const auto& node : graph.nodes) { - if (node_ids.count(node.id)) { - result.is_valid = false; - result.errors.push_back("Duplicate node ID found: " + node.id); - } - node_ids.insert(node.id); +namespace { - if (node.type == "premise") has_premise = true; - if (node.type == "conclusion") has_conclusion = true; +enum class ItemKind { Axiom, Definition, Node, Objection, Reply }; + +std::string_view describe(ItemKind kind) { + switch (kind) { + case ItemKind::Axiom: return "an axiom"; + case ItemKind::Definition: return "a definition"; + case ItemKind::Node: return "a node"; + case ItemKind::Objection: return "an objection"; + case ItemKind::Reply: return "a reply"; } + return ""; +} + +class Checker { +public: + explicit Checker(AST::Document& doc) : doc_(doc) {} - if (!has_premise) { - result.is_valid = false; - result.errors.push_back("Graph validation error: Missing at least one premise."); + Diagnostics run() { + collect_names(); + check_axioms(); + check_nodes(); + check_dialectics(); + check_cycles(); + check_relevance(); + if (doc_.title) check_argument_shape(); + return std::move(diags_); } - if (!has_conclusion) { - result.is_valid = false; - result.errors.push_back("Graph validation error: Missing at least one conclusion."); + +private: + void error(const Span& span, std::string message) { + diags_.push_back({Severity::Error, doc_.file, span, std::move(message)}); } - // 2. Check for dangling references in supports and depends_on - for (const auto& node : graph.nodes) { - for (const auto& sup : node.supports) { - if (!node_ids.count(sup)) { - result.is_valid = false; - result.errors.push_back("Node '" + node.id + "' supports non-existent node '" + sup + "'."); - } + void warning(const Span& span, std::string message) { + diags_.push_back({Severity::Warning, doc_.file, span, std::move(message)}); + } + + void declare(const std::string& id, ItemKind kind, const Span& span) { + if (!names_.emplace(id, kind).second) error(span, "'" + id + "' is already defined"); + } + + void collect_names() { + for (const auto& ax : doc_.axioms) declare(ax.id, ItemKind::Axiom, ax.span); + for (const auto& def : doc_.definitions) declare(def.id, ItemKind::Definition, def.span); + for (const auto& n : doc_.nodes) declare(n.id, ItemKind::Node, n.span); + for (const auto& d : doc_.dialectics) { + declare(d.id, d.kind == AST::DialecticKind::Objection ? ItemKind::Objection : ItemKind::Reply, d.span); } - for (const auto& dep : node.depends_on) { - if (!node_ids.count(dep)) { - result.is_valid = false; - result.errors.push_back("Node '" + node.id + "' depends on non-existent node '" + dep + "'."); + } + + // Reports a reference that is undefined or names the wrong kind of item + bool expect_kind(const AST::Ref& ref, std::initializer_list allowed, std::string_view role) { + auto it = names_.find(ref.name); + if (it == names_.end()) { + error(ref.span, "'" + ref.name + "' is not defined"); + return false; + } + for (ItemKind k : allowed) { + if (it->second == k) return true; + } + error(ref.span, std::string(role) + " '" + ref.name + "', which is " + std::string(describe(it->second))); + return false; + } + + void check_axioms() { + for (auto& ax : doc_.axioms) { + if (ax.kind != AST::AxiomKind::Scripture) continue; + auto canon = Scripture::from_name(ax.canon); + if (!canon) { + error(ax.span, "unknown canon '" + ax.canon + "' (expected protestant, catholic, orthodox or quran)"); + continue; + } + auto ref = Scripture::resolve(*canon, ax.citation); + if (!ref) { + error(ax.span, ref.error()); + continue; } + ax.scripture = *ref; } } - // 3. Cycle detection using DFS coloring (White = 0, Gray = 1, Black = 2) - std::unordered_map visited; - for (const auto& node : graph.nodes) { - visited[node.id] = 0; + void check_nodes() { + for (const auto& n : doc_.nodes) { + const bool premise = n.kind == AST::NodeKind::Premise; + if (premise) { + if (!n.from.empty()) error(n.span, "premise '" + n.id + "' cannot have 'from'; use a deduction"); + if (n.rule) error(n.rule->span, "premise '" + n.id + "' cannot have 'by'"); + if (n.proof) error(n.proof->span, "premise '" + n.id + "' cannot have a proof"); + if (n.grounded_by.empty() && !n.imported) warning(n.span, "premise '" + n.id + "' is not grounded by any axiom"); + } else if (n.from.empty()) { + error(n.span, std::string(AST::to_string(n.kind)) + " '" + n.id + "' needs 'from'"); + } + if (n.rule && n.proof) error(n.proof->span, "node '" + n.id + "' has both 'by' and a proof; use one"); + for (const auto& r : n.from) expect_kind(r, {ItemKind::Node}, "'from' names"); + for (const auto& r : n.grounded_by) expect_kind(r, {ItemKind::Axiom}, "'grounded_by' names"); + } } - auto has_cycle = [&](auto& self, const std::string& curr_id, const std::unordered_map>& adj) -> bool { - visited[curr_id] = 1; // Mark as visiting (gray) - auto it = adj.find(curr_id); - if (it != adj.end()) { - for (const auto& neighbor : it->second) { - if (visited[neighbor] == 1) return true; // Cycle detected - if (visited[neighbor] == 0 && self(self, neighbor, adj)) return true; + void check_dialectics() { + for (const auto& d : doc_.dialectics) { + if (d.kind == AST::DialecticKind::Objection) { + expect_kind(d.target, {ItemKind::Node}, "objection targets"); + } else { + expect_kind(d.target, {ItemKind::Objection, ItemKind::Reply}, "reply targets"); } } - visited[curr_id] = 2; // Mark as visited (black) - return false; - }; + } + + void check_cycles() { + std::unordered_map by_id; + for (const auto& n : doc_.nodes) by_id.emplace(n.id, &n); - // Build adjacency list for dependencies - std::unordered_map> adj; - for (const auto& node : graph.nodes) { - adj[node.id] = node.depends_on; + enum class Mark { White, Gray, Black }; + std::unordered_map mark; + std::function visit = [&](const AST::Node& n) { + mark[n.id] = Mark::Gray; + for (const auto& r : n.from) { + auto it = by_id.find(r.name); + if (it == by_id.end()) continue; + if (mark[r.name] == Mark::Gray) { + error(r.span, "circular reasoning: '" + n.id + "' depends on '" + r.name + "', which depends back on '" + n.id + "'"); + return true; + } + if (mark[r.name] == Mark::White && visit(*it->second)) return true; + } + mark[n.id] = Mark::Black; + return false; + }; + for (const auto& n : doc_.nodes) { + if (mark[n.id] == Mark::White && visit(n)) return; + } } - for (const auto& node : graph.nodes) { - if (visited[node.id] == 0) { - if (has_cycle(has_cycle, node.id, adj)) { - result.is_valid = false; - result.errors.push_back("Logical cycle detected involving node '" + node.id + "'. Circular reasoning is invalid."); - break; + // Every non-conclusion node should feed some conclusion + void check_relevance() { + std::unordered_map by_id; + for (const auto& n : doc_.nodes) by_id.emplace(n.id, &n); + std::unordered_set used; + std::function mark = [&](const AST::Node& n) { + for (const auto& r : n.from) { + auto it = by_id.find(r.name); + if (it != by_id.end() && used.insert(r.name).second) mark(*it->second); + } + }; + for (const auto& n : doc_.nodes) { + if (n.kind == AST::NodeKind::Conclusion) mark(n); + } + if (!doc_.title) return; // library files offer premises for others to use + for (const auto& n : doc_.nodes) { + if (n.kind != AST::NodeKind::Conclusion && !n.imported && !used.contains(n.id)) { + warning(n.span, std::string(AST::to_string(n.kind)) + " '" + n.id + "' is not used by any conclusion"); } } } - return result; -} + void check_argument_shape() { + bool premise = false, conclusion = false; + for (const auto& n : doc_.nodes) { + if (n.imported) continue; + premise |= n.kind == AST::NodeKind::Premise; + conclusion |= n.kind == AST::NodeKind::Conclusion; + } + if (!conclusion) error({}, "argument '" + *doc_.title + "' has no conclusion"); + if (!premise && !std::ranges::any_of(doc_.nodes, [](const AST::Node& n) { return n.imported; })) { + error({}, "argument '" + *doc_.title + "' has no premise"); + } + } + + AST::Document& doc_; + Diagnostics diags_; + std::unordered_map names_; +}; + +} // namespace + +Diagnostics validate(AST::Document& doc) { return Checker(doc).run(); } -} // namespace Theos::Validator \ No newline at end of file +} // namespace Theos::Validator diff --git a/tests/CMakeLists.txt b/tests/CMakeLists.txt index bf8256a..c16d3d8 100644 --- a/tests/CMakeLists.txt +++ b/tests/CMakeLists.txt @@ -6,10 +6,12 @@ FetchContent_Declare(Catch2 FetchContent_MakeAvailable(Catch2) add_executable(theos_tests - test_validator.cpp - test_parser.cpp + test_canon.cpp test_exporter.cpp - test_format.cpp + test_golden.cpp + test_lexer.cpp + test_parser.cpp + test_validator.cpp ) target_link_libraries(theos_tests PRIVATE theos_core theos_warnings Catch2::Catch2WithMain) target_compile_definitions(theos_tests PRIVATE THEOS_SOURCE_DIR="${PROJECT_SOURCE_DIR}") diff --git a/tests/golden/parser/bad_formula.out b/tests/golden/parser/bad_formula.out new file mode 100644 index 0000000..756d4e9 --- /dev/null +++ b/tests/golden/parser/bad_formula.out @@ -0,0 +1,3 @@ +bad_formula.theo:3:18: error: expected formula, found '&' + formula: A & & B + ^ diff --git a/tests/golden/parser/bad_formula.theo b/tests/golden/parser/bad_formula.theo new file mode 100644 index 0000000..db1bf0c --- /dev/null +++ b/tests/golden/parser/bad_formula.theo @@ -0,0 +1,4 @@ +premise P1 { + text: "a" + formula: A & & B +} diff --git a/tests/golden/parser/full_document.out b/tests/golden/parser/full_document.out new file mode 100644 index 0000000..db10ac8 --- /dev/null +++ b/tests/golden/parser/full_document.out @@ -0,0 +1,32 @@ +--- +argument "Golden" by "Tests" +import "lib/shared" +axiom S scripture catholic "Wisdom 13:1-9" +axiom W source "Aristotle, Physics" "VIII.5" +axiom N principle "Nothing comes from nothing." +define Contingent(x) := <>~Exists(x) +define G(x) := forall F:prop. Positive(F) -> F(x) +premise P1 grounded_by [S, W] + text: "Some things are contingent." + formula: exists x. Contingent(x) +premise P2 grounded_by [N] + text: "Contingent things need a cause." + formula: forall x. Contingent(x) -> (exists y. Causes(y, x) & x != y) +conclusion C1 from [P1, P2] + text: "Something causes something." + formula: exists x. exists y. Causes(y, x) + proof + 1. exists x. Contingent(x) premise P1 + { [a] + 2. Contingent(a) assume + 3. Contingent(a) -> (exists y. Causes(y, a) & a != y) forall_e P2 + } + box { + 4. []A reit 1 + } + 5. exists x. exists y. Causes(y, x) exists_e 1, 2-4 +objection O1 against P2 + text: "Causation might be an illusion." +reply R1 to O1 + text: "Then so is the objection's motivation." + formula: ~Illusion diff --git a/tests/golden/parser/full_document.theo b/tests/golden/parser/full_document.theo new file mode 100644 index 0000000..e705514 --- /dev/null +++ b/tests/golden/parser/full_document.theo @@ -0,0 +1,39 @@ +argument "Golden" by "Tests" + +import "lib/shared" + +axiom S = scripture(catholic, "Wisdom 13:1-9") +axiom W = source("Aristotle, Physics", "VIII.5") +axiom N = principle("Nothing comes from nothing.") + +define Contingent(x) := <>~Exists(x) +define G(x) := forall F:prop. Positive(F) -> F(x) + +premise P1 grounded_by [S, W] { + text: "Some things are contingent." + formula: ∃x. Contingent(x) +} + +premise P2 grounded_by [N] { + text: "Contingent things need a cause." + formula: forall x. Contingent(x) -> exists y. (Causes(y, x) & x != y) +} + +conclusion C1 from [P1, P2] { + text: "Something causes something." + formula: exists x y. Causes(y, x) + proof { + 1. exists x. Contingent(x) premise P1 + { [a] + 2. Contingent(a) assume + 3. Contingent(a) -> exists y. (Causes(y, a) & a != y) forall_e P2 + } + box { + 4. []A reit 1 + } + 5. exists x y. Causes(y, x) exists_e 1, 2-4 + } +} + +objection O1 against P2 { text: "Causation might be an illusion." } +reply R1 to O1 { text: "Then so is the objection's motivation." formula: ~Illusion } diff --git a/tests/golden/parser/missing_brace.out b/tests/golden/parser/missing_brace.out new file mode 100644 index 0000000..22e7880 --- /dev/null +++ b/tests/golden/parser/missing_brace.out @@ -0,0 +1,3 @@ +missing_brace.theo:4:1: error: expected 'text', 'formula', 'proof' or '}', found end of file + + ^ diff --git a/tests/golden/parser/missing_brace.theo b/tests/golden/parser/missing_brace.theo new file mode 100644 index 0000000..b923a86 --- /dev/null +++ b/tests/golden/parser/missing_brace.theo @@ -0,0 +1,3 @@ +premise P1 { + text: "a" + formula: A diff --git a/tests/golden/parser/static_errors.out b/tests/golden/parser/static_errors.out new file mode 100644 index 0000000..878748a --- /dev/null +++ b/tests/golden/parser/static_errors.out @@ -0,0 +1,33 @@ +static_errors.theo:3:1: error: unknown book 'Hezekiah' in the protestant canon + axiom S = scripture(protestant, "Hezekiah 1:1") + ^~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ +static_errors.theo:8:21: error: 'Missing' is not defined + conclusion C1 from [Missing] { text: "c" formula: D } + ^~~~~~~ +static_errors.theo:7:20: error: circular reasoning: 'D2' depends on 'D1', which depends back on 'D2' + deduction D2 from [D1] { text: "d" formula: C } + ^~ +static_errors.theo:5:1: warning: premise 'P1' is not used by any conclusion + premise P1 grounded_by [S] { text: "p" formula: A } + ^~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ +static_errors.theo:6:1: warning: deduction 'D1' is not used by any conclusion + deduction D1 from [P1, D2] { text: "d" formula: B } + ^~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ +static_errors.theo:7:1: warning: deduction 'D2' is not used by any conclusion + deduction D2 from [D1] { text: "d" formula: C } + ^~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ +--- +argument "Broken" +axiom S scripture protestant "Hezekiah 1:1" +premise P1 grounded_by [S] + text: "p" + formula: A +deduction D1 from [P1, D2] + text: "d" + formula: B +deduction D2 from [D1] + text: "d" + formula: C +conclusion C1 from [Missing] + text: "c" + formula: D diff --git a/tests/golden/parser/static_errors.theo b/tests/golden/parser/static_errors.theo new file mode 100644 index 0000000..5c30f8f --- /dev/null +++ b/tests/golden/parser/static_errors.theo @@ -0,0 +1,8 @@ +argument "Broken" + +axiom S = scripture(protestant, "Hezekiah 1:1") + +premise P1 grounded_by [S] { text: "p" formula: A } +deduction D1 from [P1, D2] { text: "d" formula: B } +deduction D2 from [D1] { text: "d" formula: C } +conclusion C1 from [Missing] { text: "c" formula: D } diff --git a/tests/golden/parser/unknown_item.out b/tests/golden/parser/unknown_item.out new file mode 100644 index 0000000..c7ff518 --- /dev/null +++ b/tests/golden/parser/unknown_item.out @@ -0,0 +1,3 @@ +unknown_item.theo:1:1: error: expected an item (import, axiom, define, premise, deduction, conclusion, objection or reply), found 'premiss' + premiss P1 { text: "typo" formula: A } + ^~~~~~~ diff --git a/tests/golden/parser/unknown_item.theo b/tests/golden/parser/unknown_item.theo new file mode 100644 index 0000000..a7d613b --- /dev/null +++ b/tests/golden/parser/unknown_item.theo @@ -0,0 +1 @@ +premiss P1 { text: "typo" formula: A } diff --git a/tests/golden/parser/unterminated_string.out b/tests/golden/parser/unterminated_string.out new file mode 100644 index 0000000..a39736e --- /dev/null +++ b/tests/golden/parser/unterminated_string.out @@ -0,0 +1,3 @@ +unterminated_string.theo:2:11: error: unterminated string + text: "never closed + ^ diff --git a/tests/golden/parser/unterminated_string.theo b/tests/golden/parser/unterminated_string.theo new file mode 100644 index 0000000..9a4cfb8 --- /dev/null +++ b/tests/golden/parser/unterminated_string.theo @@ -0,0 +1,3 @@ +premise P1 { + text: "never closed +} diff --git a/tests/test_canon.cpp b/tests/test_canon.cpp new file mode 100644 index 0000000..720db0d --- /dev/null +++ b/tests/test_canon.cpp @@ -0,0 +1,55 @@ +#include +#include "theos/canon.hpp" + +using namespace Theos; +using AST::Canon; + +TEST_CASE("Canon sizes", "[canon]") { + REQUIRE(Scripture::book_count(Canon::Protestant) == 66); + REQUIRE(Scripture::book_count(Canon::Catholic) == 73); + REQUIRE(Scripture::book_count(Canon::Orthodox) == 77); +} + +TEST_CASE("Resolves references per canon", "[canon]") { + auto ps = Scripture::resolve(Canon::Protestant, "Psalms 102:25-27"); + REQUIRE(ps); + REQUIRE(Scripture::book_name(Canon::Protestant, ps->book) == "Psalms"); + REQUIRE(ps->book == 19); + REQUIRE(ps->verse == 25); + REQUIRE(ps->end_verse == 27); + + auto cat = Scripture::resolve(Canon::Catholic, "Psalm 102:25"); + REQUIRE(cat); + REQUIRE(Scripture::book_name(Canon::Catholic, cat->book) == "Psalms"); + REQUIRE(cat->book == 23); // after Tobit, Judith, 1-2 Maccabees + + REQUIRE(Scripture::resolve(Canon::Protestant, "1 corinthians 15:3-8")); + REQUIRE(Scripture::resolve(Canon::Protestant, "1Corinthians 15")); + REQUIRE(Scripture::resolve(Canon::Orthodox, "Psalms 151:1")); + REQUIRE(Scripture::resolve(Canon::Catholic, "Wisdom 13:1-9")); +} + +TEST_CASE("Rejects unknown books and out-of-range chapters", "[canon]") { + REQUIRE(Scripture::resolve(Canon::Protestant, "Wisdom 13:1").error() == "unknown book 'Wisdom' in the protestant canon"); + REQUIRE_FALSE(Scripture::resolve(Canon::Protestant, "Psalms 151:1")); + REQUIRE_FALSE(Scripture::resolve(Canon::Protestant, "Jude 2:1")); + REQUIRE_FALSE(Scripture::resolve(Canon::Protestant, "John 3:16-10")); + REQUIRE_FALSE(Scripture::resolve(Canon::Protestant, "John")); + REQUIRE_FALSE(Scripture::resolve(Canon::Protestant, "John x:1")); +} + +TEST_CASE("Quran surah and ayah bounds", "[canon]") { + auto kursi = Scripture::resolve(Canon::Quran, "2:255"); + REQUIRE(kursi); + REQUIRE(kursi->chapter == 2); + REQUIRE(Scripture::format(*kursi) == "2:255"); + REQUIRE_FALSE(Scripture::resolve(Canon::Quran, "1:8")); + REQUIRE_FALSE(Scripture::resolve(Canon::Quran, "115:1")); + REQUIRE(Scripture::resolve(Canon::Quran, "112:1-4")); +} + +TEST_CASE("Formats canonical citations", "[canon]") { + REQUIRE(Scripture::format(*Scripture::resolve(Canon::Protestant, "song of songs 2:1")) == "Song of Solomon 2:1"); + REQUIRE(Scripture::format(*Scripture::resolve(Canon::Protestant, "John 1:1-2:3")) == "John 1:1-2:3"); + REQUIRE(Scripture::format(*Scripture::resolve(Canon::Protestant, "Jude 1")) == "Jude 1"); +} diff --git a/tests/test_exporter.cpp b/tests/test_exporter.cpp index c382afd..f94677b 100644 --- a/tests/test_exporter.cpp +++ b/tests/test_exporter.cpp @@ -1,21 +1,24 @@ #include +#include "theos/driver.hpp" #include "theos/exporter.hpp" using namespace Theos; -TEST_CASE("Mermaid escapes quotes in node text", "[exporter]") { - AST::TheologicalGraph g; - g.nodes = {AST::Node{"P1", "He said \"so\"", "premise", {}, {}}}; - auto out = Exporter::to_mermaid(g); +TEST_CASE("Mermaid shows axioms, nodes, edges and objections", "[exporter]") { + auto r = Driver::check_source(R"( +axiom S = scripture(protestant, "John 1:1") +premise P1 grounded_by [S] { text: "He said \"so\"" formula: A -> B } +premise P2 grounded_by [S] { text: "a" formula: A } +conclusion C1 from [P1, P2] { text: "b" formula: B } +objection O1 against P1 { text: "no" } +)", "m.theo"); + REQUIRE(r.ok()); + auto out = Exporter::to_mermaid(*r.doc); + REQUIRE(out.starts_with("flowchart TD\n")); + REQUIRE(out.find(R"(S(["S: John 1:1"]):::axiom)") != std::string::npos); REQUIRE(out.find("He said #quot;so#quot;") != std::string::npos); -} - -TEST_CASE("Mermaid emits each edge once", "[exporter]") { - AST::TheologicalGraph g; - g.nodes = {AST::Node{"P1", "p", "premise", {}, {}}, - AST::Node{"C1", "c", "conclusion", {"P1"}, {"P1"}}}; - auto out = Exporter::to_mermaid(g); - auto first = out.find("P1 --> C1"); - REQUIRE(first != std::string::npos); - REQUIRE(out.find("P1 --> C1", first + 1) == std::string::npos); + REQUIRE(out.find("A → B") != std::string::npos); + REQUIRE(out.find("S -.-> P1") != std::string::npos); + REQUIRE(out.find("P1 --> C1") != std::string::npos); + REQUIRE(out.find("O1 -. objects .-> P1") != std::string::npos); } diff --git a/tests/test_format.cpp b/tests/test_format.cpp deleted file mode 100644 index 5701d6c..0000000 --- a/tests/test_format.cpp +++ /dev/null @@ -1,64 +0,0 @@ -#include -#include "theos/format.hpp" -#include "theos/parser.hpp" -#include -#include - -using namespace Theos; -namespace fs = std::filesystem; - -namespace { -fs::path tmp(const std::string& name) { return fs::temp_directory_path() / name; } - -std::vector read_all(const fs::path& p) { - std::ifstream in(p, std::ios::binary); - return {std::istreambuf_iterator(in), {}}; -} - -void write_all(const fs::path& p, const std::vector& bytes) { - std::ofstream out(p, std::ios::binary); - out.write(bytes.data(), static_cast(bytes.size())); -} - -fs::path compiled_aquinas() { - auto g = Parser::parse_file(THEOS_SOURCE_DIR "/examples/aquinas_first_way.theo"); - auto p = tmp("theos_aquinas.theos"); - write_binary_file(p.string(), g); - return p; -} -} // namespace - -TEST_CASE("Binary round trip preserves nodes", "[format]") { - auto g = read_binary_file(compiled_aquinas().string()); - REQUIRE(g.nodes.size() == 4); - REQUIRE(g.nodes[3].id == "C1"); - REQUIRE(g.nodes[3].depends_on == std::vector{"D1"}); - REQUIRE(g.axioms.size() == 2); -} - -TEST_CASE("Truncated binary throws", "[format]") { - auto bytes = read_all(compiled_aquinas()); - for (size_t len : {size_t{0}, size_t{10}, size_t{40}, bytes.size() - 1}) { - auto p = tmp("theos_truncated.theos"); - write_all(p, std::vector(bytes.begin(), bytes.begin() + static_cast(len))); - REQUIRE_THROWS_AS(read_binary_file(p.string()), std::runtime_error); - } -} - -TEST_CASE("Bad magic throws", "[format]") { - auto bytes = read_all(compiled_aquinas()); - bytes[0] = 'X'; - auto p = tmp("theos_badmagic.theos"); - write_all(p, bytes); - REQUIRE_THROWS_AS(read_binary_file(p.string()), std::runtime_error); -} - -TEST_CASE("Out-of-range offsets throw", "[format]") { - auto bytes = read_all(compiled_aquinas()); - // node_table_offset lives at byte 14 of the header - uint32_t huge = 0xFFFFFF00u; - std::memcpy(bytes.data() + 14, &huge, sizeof(huge)); - auto p = tmp("theos_badoffset.theos"); - write_all(p, bytes); - REQUIRE_THROWS_AS(read_binary_file(p.string()), std::runtime_error); -} diff --git a/tests/test_golden.cpp b/tests/test_golden.cpp new file mode 100644 index 0000000..5b2939c --- /dev/null +++ b/tests/test_golden.cpp @@ -0,0 +1,48 @@ +// Golden tests: each tests/golden//*.theo is checked and its diagnostics plus AST dump are +// compared with the neighbouring .out file. Set THEOS_UPDATE_GOLDEN=1 to rewrite the .out files. +#include +#include "theos/driver.hpp" +#include +#include +#include +#include + +using namespace Theos; +namespace fs = std::filesystem; + +namespace { +std::string read(const fs::path& p) { + std::ifstream in(p, std::ios::binary); + std::ostringstream ss; + ss << in.rdbuf(); + return ss.str(); +} + +std::string actual_output(const fs::path& file) { + // Paths are printed relative to the suite so .out files do not depend on the checkout location + auto r = Driver::check_source(read(file), file.filename().string()); + std::string out = Driver::render_diagnostics(r); + if (r.doc) out += "---\n" + AST::dump(*r.doc); + return out; +} +} // namespace + +TEST_CASE("Golden files", "[golden]") { + const bool update = std::getenv("THEOS_UPDATE_GOLDEN") != nullptr; + const fs::path root = fs::path(THEOS_SOURCE_DIR) / "tests" / "golden"; + size_t count = 0; + for (const auto& entry : fs::recursive_directory_iterator(root)) { + if (entry.path().extension() != ".theo") continue; + ++count; + const fs::path expected_path = fs::path(entry.path()).replace_extension(".out"); + const std::string actual = actual_output(entry.path()); + if (update) { + std::ofstream(expected_path, std::ios::binary) << actual; + continue; + } + INFO("golden file: " << entry.path().string()); + REQUIRE(fs::exists(expected_path)); + REQUIRE(actual == read(expected_path)); + } + REQUIRE(count > 0); +} diff --git a/tests/test_lexer.cpp b/tests/test_lexer.cpp new file mode 100644 index 0000000..80147dd --- /dev/null +++ b/tests/test_lexer.cpp @@ -0,0 +1,72 @@ +#include +#include "theos/lexer.hpp" + +using namespace Theos; + +namespace { +std::vector kinds(std::string_view src) { + auto toks = lex(src, "t.theo"); + REQUIRE(toks.has_value()); + std::vector out; + for (const auto& t : *toks) out.push_back(t.kind); + return out; +} +} // namespace + +TEST_CASE("Lexes keywords, identifiers, numbers and strings", "[lexer]") { + auto toks = lex("premise P1 { text: \"a \\\"b\\\"\" } 42", "t.theo"); + REQUIRE(toks); + REQUIRE((*toks)[0].kind == Tok::Keyword); + REQUIRE((*toks)[1].kind == Tok::Ident); + REQUIRE((*toks)[1].text == "P1"); + REQUIRE((*toks)[5].kind == Tok::String); + REQUIRE((*toks)[5].text == "a \"b\""); + REQUIRE((*toks)[7].kind == Tok::Number); + REQUIRE(toks->back().kind == Tok::End); +} + +TEST_CASE("ASCII and Unicode operators lex to the same tokens", "[lexer]") { + REQUIRE(kinds("~ & | -> <-> <> := != \\ bot forall exists") == + std::vector{Tok::Not, Tok::And, Tok::Or, Tok::Implies, Tok::Iff, Tok::Diamond, Tok::Define, + Tok::NotEquals, Tok::Lambda, Tok::Bottom, Tok::Forall, Tok::Exists, Tok::End}); + REQUIRE(kinds("¬ ∧ ∨ → ↔ ◇ □ ≠ λ ⊥ ∀ ∃") == + std::vector{Tok::Not, Tok::And, Tok::Or, Tok::Implies, Tok::Iff, Tok::Diamond, Tok::Box, + Tok::NotEquals, Tok::Lambda, Tok::Bottom, Tok::Forall, Tok::Exists, Tok::End}); +} + +TEST_CASE("Comments are skipped", "[lexer]") { + REQUIRE(kinds("a // line\n /* block\n */ b") == std::vector{Tok::Ident, Tok::Ident, Tok::End}); +} + +TEST_CASE("Columns count code points", "[lexer]") { + auto toks = lex("¬¬ P", "t.theo"); + REQUIRE(toks); + REQUIRE((*toks)[2].span.col == 4); +} + +TEST_CASE("Unterminated string reports its start", "[lexer]") { + auto toks = lex("text: \"abc\n", "t.theo"); + REQUIRE_FALSE(toks); + REQUIRE(toks.error().span.line == 1); + REQUIRE(toks.error().span.col == 7); + REQUIRE(toks.error().message == "unterminated string"); +} + +TEST_CASE("Unexpected character is reported with position", "[lexer]") { + auto toks = lex("a\n $", "t.theo"); + REQUIRE_FALSE(toks); + REQUIRE(toks.error().span.line == 2); + REQUIRE(toks.error().span.col == 3); +} + +TEST_CASE("Unterminated block comment is an error", "[lexer]") { + REQUIRE_FALSE(lex("/* never closed", "t.theo")); +} + +TEST_CASE("Diagnostics on CRLF sources do not echo carriage returns", "[diagnostic]") { + const std::string src = "premise P1 {\r\n text: \"a\r\n}\r\n"; + auto toks = lex(src, "crlf.theo"); + REQUIRE_FALSE(toks); + const std::string out = render(toks.error(), src); + REQUIRE(out.find('\r') == std::string::npos); +} diff --git a/tests/test_parser.cpp b/tests/test_parser.cpp index 2807bd4..f3aa403 100644 --- a/tests/test_parser.cpp +++ b/tests/test_parser.cpp @@ -1,33 +1,116 @@ #include #include "theos/parser.hpp" -#include "theos/validator.hpp" using namespace Theos; -TEST_CASE("Parses metadata, axioms and nodes", "[parser]") { - auto g = Parser::parse_string(R"( -title: "T" -author: "A" -axiom Ax1 = scripture(John, 1, 1, 3) -premise P1 { +namespace { +std::string reprint(std::string_view src) { + auto f = Parser::parse_formula(src); + REQUIRE(f.has_value()); + return print(**f); +} +} // namespace + +TEST_CASE("Formula precedence", "[parser]") { + REQUIRE(reprint("A & B | C -> D <-> E") == "A & B | C -> D <-> E"); + REQUIRE(reprint("A -> B -> C") == "A -> B -> C"); + REQUIRE(reprint("(A -> B) -> C") == "(A -> B) -> C"); + REQUIRE(reprint("A & (B & C)") == "A & (B & C)"); + REQUIRE(reprint("(A & B) & C") == "A & B & C"); + REQUIRE(reprint("~A & B") == "~A & B"); + REQUIRE(reprint("~(A & B)") == "~(A & B)"); +} + +TEST_CASE("Quantifier bodies extend right", "[parser]") { + REQUIRE(reprint("forall x. P(x) -> Q(x)") == "forall x. P(x) -> Q(x)"); + REQUIRE(reprint("(forall x. P(x)) -> Q") == "(forall x. P(x)) -> Q"); + REQUIRE(reprint("forall x y. R(x, y)") == "forall x. forall y. R(x, y)"); +} + +TEST_CASE("Unicode notation parses like ASCII", "[parser]") { + REQUIRE(reprint("∀x. □P(x) → ◇∃y. x ≠ y") == "forall x. []P(x) -> <>exists y. x != y"); + auto f = Parser::parse_formula("forall x. []P(x) -> <>exists y. x != y"); + REQUIRE(print(**f, Notation::Unicode) == "∀x. □P(x) → ◇∃y. x ≠ y"); +} + +TEST_CASE("Higher-order syntax", "[parser]") { + REQUIRE(reprint("forall F:prop. Positive(F) -> F(x)") == "forall F:prop. Positive(F) -> F(x)"); + REQUIRE(reprint("Positive(\\x. ~F(x))") == "Positive(\\x. ~F(x))"); + REQUIRE(reprint("Positive(λx. ¬F(x), G)") == "Positive(\\x. ~F(x), G)"); +} + +TEST_CASE("Box needs adjacent brackets", "[parser]") { + REQUIRE(reprint("[]A") == "[]A"); + REQUIRE_FALSE(Parser::parse_formula("[ ]A")); +} + +TEST_CASE("Formula syntax errors point at the token", "[parser]") { + auto f = Parser::parse_formula("A & -> B"); + REQUIRE_FALSE(f); + REQUIRE(f.error().span.col == 5); + REQUIRE(f.error().message == "expected formula, found '->'"); +} + +TEST_CASE("Parses a document with every item kind", "[parser]") { + auto doc = Parser::parse(R"( +argument "Demo" by "Me" +import "std/principles" +axiom S = scripture(protestant, "John 1:1-3") +axiom W = source("Work", "1.2") +axiom N = principle("Nothing comes from nothing.") +define Big(x) := Large(x) & Heavy(x) +premise P1 grounded_by [S, W] { text: "p" + formula: A -> B +} +premise P2 { formula: A text: "q" } +conclusion C1 from [P1, P2] by imp_e { + text: "c" + formula: B } -conclusion C1 { +objection O1 against P1 { text: "o" } +reply R1 to O1 { text: "r" formula: A } +)", "demo.theo"); + REQUIRE(doc.has_value()); + REQUIRE(doc->title == "Demo"); + REQUIRE(doc->imports.size() == 1); + REQUIRE(doc->axioms.size() == 3); + REQUIRE(doc->axioms[0].kind == AST::AxiomKind::Scripture); + REQUIRE(doc->definitions[0].params.size() == 1); + REQUIRE(doc->nodes.size() == 3); + REQUIRE(doc->nodes[2].rule->name == "imp_e"); + REQUIRE(doc->dialectics.size() == 2); + REQUIRE(doc->dialectics[1].formula); +} + +TEST_CASE("Parses proofs with subproofs, fresh names and boxes", "[parser]") { + auto doc = Parser::parse(R"( +conclusion C1 from [P1] { text: "c" - depends_on: [P1] -} -)"); - REQUIRE(g.title == "T"); - REQUIRE(g.author == "A"); - REQUIRE(g.axioms.size() == 1); - REQUIRE(g.axioms[0].book_id == 43); - REQUIRE(g.axioms[0].chapter == 1); - REQUIRE(g.nodes.size() == 2); - REQUIRE(g.nodes[1].depends_on == std::vector{"P1"}); -} - -TEST_CASE("Aquinas example parses and validates", "[parser]") { - auto g = Parser::parse_file(THEOS_SOURCE_DIR "/examples/aquinas_first_way.theo"); - REQUIRE(g.nodes.size() == 4); - REQUIRE(Validator::validate(g).is_valid); + formula: A -> A + proof { + { 1. A assume + 2. A reit 1 } + 3. A -> A imp_i 1-2 + { [a] 4. P(a) premise P1 } + box { 5. B premise P1 } + } +} +)", "p.theo"); + REQUIRE(doc.has_value()); + const auto& items = doc->nodes[0].proof->items; + REQUIRE(items.size() == 4); + const auto& sub = std::get(items[0]); + REQUIRE(sub.items.size() == 2); + const auto& line3 = std::get(items[1]); + REQUIRE(line3.refs[0].kind == AST::ProofRef::Kind::Range); + REQUIRE(line3.refs[0].last == 2); + REQUIRE(std::get(items[2]).fresh->name == "a"); + REQUIRE(std::get(items[3]).strict); +} + +TEST_CASE("Missing formula is a syntax error", "[parser]") { + auto doc = Parser::parse("premise P1 { text: \"x\" }", "m.theo"); + REQUIRE_FALSE(doc); + REQUIRE(doc.error().message == "node 'P1' is missing 'formula'"); } diff --git a/tests/test_validator.cpp b/tests/test_validator.cpp index 861fb3a..e7667e1 100644 --- a/tests/test_validator.cpp +++ b/tests/test_validator.cpp @@ -1,57 +1,108 @@ #include -#include "theos/validator.hpp" +#include +#include "theos/driver.hpp" using namespace Theos; namespace { -AST::Node node(std::string id, std::string type, std::vector deps) { - return AST::Node{std::move(id), "text", std::move(type), {}, std::move(deps)}; +Diagnostics diagnose(std::string src) { + auto r = Driver::check_source(std::move(src), "v.theo"); + REQUIRE(r.doc.has_value()); + return r.diagnostics; } -bool has_error_containing(const Validator::ValidationResult& r, const std::string& needle) { - for (const auto& e : r.errors) { - if (e.find(needle) != std::string::npos) return true; +bool has(const Diagnostics& diags, Severity sev, const std::string& needle) { + for (const auto& d : diags) { + if (d.severity == sev && d.message.find(needle) != std::string::npos) return true; } return false; } + +constexpr const char* valid = R"( +argument "A" +axiom S = principle("s") +premise P1 grounded_by [S] { text: "p" formula: A } +premise P2 grounded_by [S] { text: "q" formula: A -> B } +conclusion C1 from [P1, P2] { text: "c" formula: B } +)"; } // namespace -TEST_CASE("Valid DAG passes", "[validator]") { - AST::TheologicalGraph g; - g.nodes = {node("P1", "premise", {}), node("D1", "deduction", {"P1"}), node("C1", "conclusion", {"D1"})}; - auto r = Validator::validate(g); - REQUIRE(r.is_valid); - REQUIRE(r.errors.empty()); +TEST_CASE("Valid argument has no diagnostics", "[validator]") { + REQUIRE(diagnose(valid).empty()); +} + +TEST_CASE("Duplicate names", "[validator]") { + auto d = diagnose(R"( +axiom X = principle("s") +premise X { text: "p" formula: A } +)"); + REQUIRE(has(d, Severity::Error, "'X' is already defined")); +} + +TEST_CASE("References must name the right kind of item", "[validator]") { + auto d = diagnose(R"( +axiom S = principle("s") +premise P1 grounded_by [P1] { text: "p" formula: A } +deduction D1 from [S, Nope] { text: "d" formula: A } +objection O1 against S { text: "o" } +reply R1 to P1 { text: "r" } +)"); + REQUIRE(has(d, Severity::Error, "'grounded_by' names 'P1', which is a node")); + REQUIRE(has(d, Severity::Error, "'from' names 'S', which is an axiom")); + REQUIRE(has(d, Severity::Error, "'Nope' is not defined")); + REQUIRE(has(d, Severity::Error, "objection targets 'S', which is an axiom")); + REQUIRE(has(d, Severity::Error, "reply targets 'P1', which is a node")); } -TEST_CASE("Cycle is rejected", "[validator]") { - AST::TheologicalGraph g; - g.nodes = {node("A", "premise", {"C"}), node("B", "deduction", {"A"}), node("C", "conclusion", {"B"})}; - auto r = Validator::validate(g); - REQUIRE_FALSE(r.is_valid); - REQUIRE(has_error_containing(r, "cycle")); +TEST_CASE("Node kind rules", "[validator]") { + auto d = diagnose(R"( +premise P0 { text: "p" formula: A } +premise P1 from [P0] by imp_e { text: "p" formula: A } +deduction D1 { text: "d" formula: A } +conclusion C1 from [P0] by imp_e { text: "c" formula: A proof { 1. A premise P0 } } +)"); + REQUIRE(has(d, Severity::Error, "premise 'P1' cannot have 'from'")); + REQUIRE(has(d, Severity::Error, "premise 'P1' cannot have 'by'")); + REQUIRE(has(d, Severity::Error, "deduction 'D1' needs 'from'")); + REQUIRE(has(d, Severity::Error, "has both 'by' and a proof")); + REQUIRE(has(d, Severity::Warning, "premise 'P0' is not grounded")); } -TEST_CASE("Dangling reference is rejected", "[validator]") { - AST::TheologicalGraph g; - g.nodes = {node("P1", "premise", {}), node("C1", "conclusion", {"X9"})}; - auto r = Validator::validate(g); - REQUIRE_FALSE(r.is_valid); - REQUIRE(has_error_containing(r, "non-existent node 'X9'")); +TEST_CASE("Cycles are circular reasoning", "[validator]") { + auto d = diagnose(R"( +premise P { text: "p" formula: A } +deduction A1 from [P, B1] { text: "a" formula: A } +deduction B1 from [A1] { text: "b" formula: A } +)"); + REQUIRE(has(d, Severity::Error, "circular reasoning")); } -TEST_CASE("Duplicate ID is rejected", "[validator]") { - AST::TheologicalGraph g; - g.nodes = {node("P1", "premise", {}), node("P1", "premise", {}), node("C1", "conclusion", {"P1"})}; - auto r = Validator::validate(g); - REQUIRE_FALSE(r.is_valid); - REQUIRE(has_error_containing(r, "Duplicate node ID")); +TEST_CASE("Argument files need premises and conclusions", "[validator]") { + auto d = diagnose("argument \"Empty\"\n"); + REQUIRE(has(d, Severity::Error, "has no conclusion")); + REQUIRE(has(d, Severity::Error, "has no premise")); } -TEST_CASE("Missing premise and conclusion are rejected", "[validator]") { - AST::TheologicalGraph g; - g.nodes = {node("D1", "deduction", {})}; - auto r = Validator::validate(g); - REQUIRE(has_error_containing(r, "premise")); - REQUIRE(has_error_containing(r, "conclusion")); +TEST_CASE("Unused nodes are warned about in argument files", "[validator]") { + auto d = diagnose(std::string(valid) + "premise P9 grounded_by [S] { text: \"x\" formula: X }\n"); + REQUIRE(has(d, Severity::Warning, "premise 'P9' is not used by any conclusion")); +} + +TEST_CASE("Scripture references are checked and resolved", "[validator]") { + auto r = Driver::check_source(R"( +axiom A = scripture(protestant, "Psalms 102:25") +axiom B = scripture(protestant, "Psalms 200:1") +axiom C = scripture(lutheran, "John 1:1") +)", "s.theo"); + REQUIRE(r.doc->axioms[0].scripture.book == 19); + REQUIRE(has(r.diagnostics, Severity::Error, "chapter out of range in 'Psalms 200:1': Psalms has 150 chapters")); + 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()); + } }