Claude/wokelang ebnf grammar qoe vv#3
Merged
Conversation
Complete implementation of WokeLang with: Lexer (src/lexer/): - Token definitions for all keywords, operators, literals - Uses logos for fast tokenization - Handles comments, strings with escapes, numbers Parser (src/parser/): - Recursive descent parser - Full expression parsing with correct precedence - All statement types: remember, when/otherwise, repeat, attempt safely - Pattern matching with decide based on - Emote tags, consent blocks, gratitude declarations AST (src/ast/): - Complete type definitions for all language constructs - Spanned nodes for error reporting Interpreter (src/interpreter/): - Tree-walking interpreter - Scoped environments for variables - Built-in functions: print, len, toString, toInt - Consent system with interactive prompts - Pattern matching evaluation - All operators (arithmetic, comparison, logical) CLI (src/main.rs): - woke <file.woke> - run program - woke --tokenize <file> - show tokens - woke --parse <file> - show AST Examples: - examples/hello.woke - feature showcase - examples/demo.woke - runnable demo
REPL (src/repl.rs): - Interactive command-line interface with rustyline - Commands: :help, :quit, :clear, :reset, :load, :ast - Expression evaluation with automatic result printing - Start with `woke` or `woke --repl` WASM Compilation (src/codegen/): - Compile WokeLang to WebAssembly binary format - Uses wasm-encoder for proper WASM generation - Supports functions, expressions, loops, conditionals - Pattern matching compilation - CLI: `woke -c input.woke` outputs input.wasm Zig FFI (src/ffi/, zig/, include/): - C-compatible API for embedding WokeLang - Interpreter lifecycle: woke_interpreter_new/free - Code execution: woke_exec, woke_eval - Value operations: type checking, conversion, creation - Static library (libwokelang.a) and shared library (.so) - C header (include/wokelang.h) - Zig bindings (zig/wokelang.zig) with idiomatic wrapper - Example Zig program and build.zig Other: - examples/math.woke - math functions for WASM demo - Cargo.toml updated for cdylib/staticlib targets
hyperpolymath
added a commit
that referenced
this pull request
Jun 18, 2026
## What
Statements were **declared** (`Stmt`/`stmt`) in both provers but had
**no typing rules** — so `progress`/`preservation` never saw them. This
adds a context-threading **statement typing judgment** and its core
metatheory, in **both** Lean (`WokeLang.lean`) and Coq (`WokeLang.v`),
at parity. It directly retires the AUDIT.md row *"Statements: declared,
no typing/exec."*
## Judgment (mutually inductive with the block form)
- `StmtWellTyped Γ s Γ'` — a single statement threads the type context
- `StmtsWellTyped Γ ss Γ'` — a block threads the context left-to-right
All nine forms: `varDecl` (extends the context), `assign` (requires a
prior declaration at the assigned type), `return`, `if`, `loop`,
`attempt`, `consent`, `expr`, `complain`. Compound statements are
**block-scoped** (they return the incoming context). This is the
statement-level analogue of the expression `has_type`/`HasType`.
## Metatheorems (all proved)
- `ctxDomSub_{refl,trans,extend}` — the context-domain preorder + the
extension fact
- `stmt_wellTyped_mono` / `stmts_wellTyped_mono` — **context
monotonicity**: a well-typed statement/block never undeclares a variable
- `stmts_wellTyped_append` — **sequencing composes**: typing one block
then another from the resulting context types their concatenation
- `stmts_wellTyped_example` — inhabitation smoke (`let x = 0; x`)
## Verification
- **Lean 4.30.0:** `lean WokeLang.lean` → exit 0, no warnings,
`sorry`-free.
- **Coq 8.18.0:** `coqc WokeLang.v` → exit 0; `Print Assumptions` on all
four statement lemmas reports **"Closed under the global context"** —
i.e. axiom-free (they don't even touch the classical-reals axioms the
float fragment needs).
- Purely **additive** (new §5b in each file); existing theorems
untouched.
## Method note
The single-statement metatheorems are non-recursive (blocks are scoped),
which breaks the mutual dependency; the block versions then go by
ordinary **induction on the list**, sidestepping a mutual-induction
scheme in both provers.
## Scope / next step (honest)
This is the **static** story (typing + structural metatheory). The
**dynamic** story — a statement execution relation + a store-typing
*preservation* theorem — is the natural follow-up. Its prerequisite is
generalising the expression `preservation`/`type_safety` to **open**
terms (non-empty context + a store-typing agreement), since
statement-embedded expressions reference declared variables and the
current expression proofs assume the empty context. This is recorded in
AUDIT.md ("Recommended next proof steps" #3).
🤖 Generated with [Claude Code](https://claude.com/claude-code)
https://claude.ai/code/session_013wg3Mtq2QFhYi4XVw1Z6z7
---
_Generated by [Claude
Code](https://claude.ai/code/session_013wg3Mtq2QFhYi4XVw1Z6z7)_
---------
Co-authored-by: Claude <noreply@anthropic.com>
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
2 participants
Add this suggestion to a batch that can be applied as a single commit.This suggestion is invalid because no changes were made to the code.Suggestions cannot be applied while the pull request is closed.Suggestions cannot be applied while viewing a subset of changes.Only one suggestion per line can be applied in a batch.Add this suggestion to a batch that can be applied as a single commit.Applying suggestions on deleted lines is not supported.You must change the existing code in this line in order to create a valid suggestion.Outdated suggestions cannot be applied.This suggestion has been applied or marked resolved.Suggestions cannot be applied from pending reviews.Suggestions cannot be applied on multi-line comments.Suggestions cannot be applied while the pull request is queued to merge.Suggestion cannot be applied right now. Please check back later.
No description provided.