refactor: rename vql++/vqlpp to VQL-UT across typeql-experimental

Canonical naming is now VQL-UT (Ultimate Type-Safe). Renames all .vqlpp
files to .vqlut, updates all documentation references from VQL++/vqlpp
to VQL-UT/vqlut. The old names are dead.

Co-Authored-By: Claude Opus 4.6 (1M context) <noreply@anthropic.com>

Author: hyperpolymath

typeql-experimental/.machine_readable/6a2/STATE.a2ml

@@ -28,7 +28,7 @@
     (component "rescript-parser"
       (status "written")
       (description "Extended AST (TQLAst.res) and parser (TQLParser.res) for 6 new
-                    VQL++ clauses. Follows VeriSimDB combinator patterns. Not yet
+                    VQL-UT clauses. Follows VeriSimDB combinator patterns. Not yet
                     build-tested (requires rescript-legacy toolchain).")
       (completion 70))
     (component "grammar-spec"
@@ -44,7 +44,7 @@
       (completion 100))
     (component "examples"
       (status "complete")
-      (description "7 annotated .vqlpp example files covering all 6 extensions
+      (description "7 annotated .vqlut example files covering all 6 extensions
                     individually plus a combined maximal query.")
       (completion 100))
     (component "idris2-tests"
@@ -69,7 +69,7 @@
       (description "ReScript parser written with combinator pattern from VeriSimDB")
       (completion 70))
     (milestone "parser-build-tested"
-      (description "ReScript parser compiles and accepts all 7 example .vqlpp files")
+      (description "ReScript parser compiles and accepts all 7 example .vqlut files")
       (completion 0))
     (milestone "integration"
       (description "Idris2 proofs validated against ReScript-parsed ASTs")
@@ -103,5 +103,5 @@
 
   (critical-next-actions
     (action "Build-test ReScript parser with rescript-legacy toolchain")
-    (action "Test all 7 example .vqlpp files parse correctly")
+    (action "Test all 7 example .vqlut files parse correctly")
     (action "Wire Idris2 proof results to ReScript-parsed ASTs (integration phase)")))

typeql-experimental/0-AI-MANIFEST.a2ml

@@ -20,7 +20,7 @@ An experimental exploration of six advanced type-theoretic extensions to VQL:
 - **Idris2 kernel**: 9/9 modules type-check clean (`idris2 --typecheck`)
 - **Zig FFI bridge**: 5/5 tests pass (`zig build test`, Zig 0.15.2)
 - **ReScript parser**: Written, not yet build-tested
-- **Examples**: 7 annotated .vqlpp files
+- **Examples**: 7 annotated .vqlut files
 - **Banned patterns**: Zero `believe_me`, `assert_total`, `assert_smaller`
 - **Overall completion**: ~85%
 
@@ -71,9 +71,9 @@ Idris2 Type Kernel                    ReScript Parser
 | ProofCarrying.idr  |                    syntax
 | Quantitative.idr   |                        |
 | Checker.idr        |               +------------------+
-| Proofs.idr         |               | .vqlpp files     |
+| Proofs.idr         |               | .vqlut files     |
 +--------------------+               +------------------+
-  proves properties                  VQL++ query language
+  proves properties                  VQL-UT query language
          |
          v
 +--------------------+

typeql-experimental/DESIGN-2026-03-01-typeql-experimental.adoc

@@ -130,7 +130,7 @@ from exact-1 to at-most-n.
 * **Phase 2**: Idris2 Kernel (9 modules) — Core, Linear, Session, Effects,
   Modal, ProofCarrying, Quantitative, Checker, Proofs
 * **Phase 3**: ReScript Parser (2 files) — TQLAst.res, TQLParser.res
-* **Phase 4**: Examples & Tests (11 files) — 7 .vqlpp examples, 3 Idris2 test
+* **Phase 4**: Examples & Tests (11 files) — 7 .vqlut examples, 3 Idris2 test
   modules, 1 ReScript test module
 * **Phase 5**: FFI Skeleton (3 files) — build.zig, build.zig.zon, bridge.zig
 * **Phase 6**: Documentation (1 file) — examples.adoc
@@ -193,5 +193,5 @@ from exact-1 to at-most-n.
 1. `idris2 --typecheck typeql-experimental.ipkg` — all modules compile with `%default total`
 2. `cd ffi/zig && zig build test` — all 5 FFI tests pass
 3. `grep -rn 'believe_me\|assert_total\|assert_smaller' src/abi/` — returns nothing
-4. (Future) ReScript parser compiles and accepts all 7 example `.vqlpp` files
+4. (Future) ReScript parser compiles and accepts all 7 example `.vqlut` files
 5. (Future) Idris2 proofs validated against ReScript-parsed ASTs

typeql-experimental/README.adoc

@@ -17,7 +17,7 @@ The six extensions are:
 
 [cols="1,2,2"]
 |===
-|Extension |VQL++ Syntax |Idris2 Mechanism
+|Extension |VQL-UT Syntax |Idris2 Mechanism
 
 |Linear Types
 |`CONSUME AFTER N USE`
@@ -66,7 +66,7 @@ The six extensions are:
 |Complete
 |Delta EBNF extending VQL v3.0
 
-|Examples (7 .vqlpp files)
+|Examples (7 .vqlut files)
 |Complete
 |All 6 extensions + combined maximal query
 

typeql-experimental/WHITEPAPER.md

@@ -408,8 +408,8 @@ existing keywords.
 
 ### 6.2 File Extension
 
-TypeQL-Experimental queries use the `.vqlpp` extension (VQL Plus Plus),
-distinguishing them from standard `.vql` files.
+TypeQL-Experimental queries use the `.vqlut` extension (VQL Ultimate Type-Safe),
+distinguishing them from standard `.vql` files. (Previously `.vqlpp` — renamed to align with VQL-UT canonical naming.)
 
 ---
 

typeql-experimental/docs/examples.adoc

@@ -1,13 +1,13 @@
 // SPDX-License-Identifier: PMPL-1.0-or-later
-= VQL-dt++ Annotated Examples
+= VQL-UT Annotated Examples
 Jonathan D.A. Jewell <j.d.a.jewell@open.ac.uk>
 :date: 2026-03-01
 :toc: macro
 
 == Overview
 
-This document provides comprehensive, annotated examples of each VQL-dt++
-extension and their combinations. Each example shows the VQL++ surface syntax,
+This document provides comprehensive, annotated examples of each VQL-UT
+extension and their combinations. Each example shows the VQL-UT surface syntax,
 the Idris2 type-level encoding, and the property being enforced.
 
 == 1. Linear Types: CONSUME AFTER N USE