From d843ee76140c2cafd0a805d688920b8247e438a6 Mon Sep 17 00:00:00 2001
From: eutro <git@eutro.dev>
Date: Fri, 17 Oct 2025 22:25:08 +0100
Subject: [PATCH] Add initial redex implementation of Qi

---
 Makefile           |  13 ++--
 qi-redex/info.rkt  |  11 ++++
 qi-redex/redex.rkt | 146 +++++++++++++++++++++++++++++++++++++++++++++
 3 files changed, 165 insertions(+), 5 deletions(-)
 create mode 100644 qi-redex/info.rkt
 create mode 100644 qi-redex/redex.rkt

diff --git a/Makefile b/Makefile
index 581c01a2..82690778 100644
--- a/Makefile
+++ b/Makefile
@@ -62,13 +62,13 @@ help:
 # Primarily for use by CI.
 # Installs dependencies as well as linking this as a package.
 install:
-	raco pkg install --deps search-auto --link $(PWD)/$(PACKAGE-NAME)-{lib,test,doc,probe} $(PWD)/$(PACKAGE-NAME)
+	raco pkg install --deps search-auto --link $(PWD)/$(PACKAGE-NAME)-{lib,test,doc,probe,redex} $(PWD)/$(PACKAGE-NAME)
 
 install-sdk:
 	raco pkg install --deps search-auto --link $(PWD)/$(PACKAGE-NAME)-sdk
 
 remove:
-	raco pkg remove $(PACKAGE-NAME)-{lib,test,doc,probe} $(PACKAGE-NAME)
+	raco pkg remove $(PACKAGE-NAME)-{lib,test,doc,probe,redex} $(PACKAGE-NAME)
 
 remove-sdk:
 	raco pkg remove $(PACKAGE-NAME)-sdk
@@ -91,7 +91,7 @@ build-docs:
 # Primarily for day-to-day dev.
 # Build libraries from source, build docs (if any), and check dependencies.
 build-all:
-	raco setup $(DEPS-FLAGS) --pkgs $(PACKAGE-NAME)-{lib,test,doc,probe} $(PACKAGE-NAME)
+	raco setup $(DEPS-FLAGS) --pkgs $(PACKAGE-NAME)-{lib,test,doc,probe,redex} $(PACKAGE-NAME)
 
 # Primarily for CI, for building backup docs that could be used in case
 # the main docs at docs.racket-lang.org become unavailable.
@@ -105,7 +105,7 @@ build-sdk:
 # (define clean '("compiled" "doc" "doc/<collect>")) to clean
 # generated docs, too.
 clean:
-	raco setup --fast-clean --pkgs $(PACKAGE-NAME)-{lib,test,doc,probe}
+	raco setup --fast-clean --pkgs $(PACKAGE-NAME)-{lib,test,doc,probe,redex}
 
 clean-sdk:
 	raco setup --fast-clean --pkgs $(PACKAGE-NAME)-sdk
@@ -116,7 +116,7 @@ clean-sdk:
 check-deps:
 	raco setup --no-docs $(DEPS-FLAGS) $(PACKAGE-NAME)
 
-test-all: test test-probe
+test-all: test test-probe test-redex
 
 # Suitable for both day-to-day dev and CI
 # Note: we don't test qi-doc since there aren't any tests there atm
@@ -158,6 +158,9 @@ test-compiler:
 test-probe:
 	raco test -exp $(PACKAGE-NAME)-probe
 
+test-redex:
+	raco test -exp $(PACKAGE-NAME)-redex
+
 test-with-errortrace:
 	racket -l errortrace -l racket -e '(require (submod "$(PACKAGE-NAME)-test/tests/qi.rkt" test))'
 
diff --git a/qi-redex/info.rkt b/qi-redex/info.rkt
new file mode 100644
index 00000000..a94c1b35
--- /dev/null
+++ b/qi-redex/info.rkt
@@ -0,0 +1,11 @@
+#lang info
+
+(define version "5.0")
+(define collection "qi")
+(define deps '("base"
+               "redex-lib"))
+(define build-deps '())
+(define clean '("compiled" "private/compiled"))
+(define compile-omit-paths '("tests"))
+(define test-include-paths '("tests"))
+(define pkg-authors '(countvajhula))
diff --git a/qi-redex/redex.rkt b/qi-redex/redex.rkt
new file mode 100644
index 00000000..945e8d06
--- /dev/null
+++ b/qi-redex/redex.rkt
@@ -0,0 +1,146 @@
+#lang racket/base
+
+(require redex/reduction-semantics)
+
+(provide Qi floe-reduce)
+
+(define-language Qi
+  ;; Variables
+  (x ::= variable-not-otherwise-mentioned)
+  (n ::= number)
+  ;; Lambda calculus / Racket expressions
+  (e ::= (λ (x ...) e) (e e ...) x n (values e ...))
+  ;; Lambda calculus contexts
+  (E ::= hole (v ... E e ...) (values v ... E e ...))
+  ;; Normalised terms / Racket values
+  (v ::= (λ (x ...) e) n)
+  ;; Flow expressions
+  (f ::=
+     (~> f ...)
+     (-< f ...)
+     (== f ...)
+     (gen e ...)
+     (esc e)
+     (>< f))
+  ;; Flow values (normalised flows)
+  (fv ::= (gen v ...))
+  ;; Flow contexts
+  (F ::= hole
+     (~> fv ... F f ...)
+     (-< fv ... F f ...)
+     (== fv ... F f ...)
+     (gen v ... E e ...)
+     (esc E)
+     (>< F))
+
+  #:binding-forms
+  (λ (x ...) e #:refers-to (shadow x ...)))
+
+(define-metafunction Qi
+  β-reduce : (λ (x ..._1) e) e ..._1 -> e
+  [(β-reduce (λ (x ...) e) e_x ...) (substitute e [x e_x] ...)])
+
+;; Floe reductions
+(define floe-reduce
+  (reduction-relation
+   Qi
+   ;; Threading
+   (--> (in-hole F (~> (gen v ...) (esc v_1) f ...))
+        (in-hole F (~> (gen (v_1 v ...)) f ...))
+        thread-step)
+   (--> (in-hole F (~> (gen v ...)))
+        (in-hole F (gen v ...))
+        thread-red)
+   ;; Tee
+   (--> (in-hole F (~> (gen v ...) (-< f ...)))
+        (in-hole F (-< (~> (gen v ...) f) ...))
+        tee-step)
+   (--> (in-hole F (-< (gen v ...) ...))
+        (in-hole F (gen v ... ...))
+        tee-red)
+   ;; Relay
+   (--> (in-hole F (~> (gen v ...) (== f ...)))
+        (in-hole F (-< (~> (gen v) f) ...))
+        relay-red)
+   ;; Amp
+   (--> (in-hole F (~> (gen v ...) (>< f)))
+        (in-hole F (-< (~> (gen v) f) ...))
+        amp-red)
+   ;; Gen
+   (--> (in-hole F (gen v_1 ... (values v_2 ...) e ...))
+        (in-hole F (gen v_1 ... v_2 ... e ...))
+        gen-values)
+   (--> (in-hole F (~> (gen v_1 ...) (gen v_2 ...)))
+        (in-hole F (gen v_2 ...))
+        gen-red)
+
+   ;; Lambda calculus reductions
+   (--> (in-hole F ((λ (x ...) e) v ...))
+        (in-hole F (mf-apply β-reduce (λ (x ...) e) v ...))
+        beta-red)))
+
+(module+ test
+  (test-->
+   floe-reduce
+   (term (~> (gen 0)))
+   (term (gen 0)))
+
+  (test-->
+   floe-reduce
+   (term (~> (~> (gen 0))))
+   (term (~> (gen 0))))
+
+  (test-match Qi f (term (esc (λ (x) x))))
+  (test-match Qi fv (term (gen 1)))
+
+  (test-->
+   floe-reduce
+   (term (~> (gen 1) (esc (λ (x) x))))
+   (term (~> (gen ((λ (x) x) 1)))))
+
+  (test-->
+   floe-reduce
+   (term (gen ((λ (x) x) 1)))
+   (term (gen 1)))
+
+  (test-->>
+   floe-reduce
+   (term (~> (gen 1) (esc (λ (x) x))))
+   (term (gen 1)))
+
+  (test-->
+   floe-reduce
+   (term (gen (values 1 2 3)))
+   (term (gen 1 2 3)))
+
+  (test-->>
+   floe-reduce
+   (term (~> (gen 1 2)
+             (-< (esc (λ (x y) y))
+                 (esc (λ (x y) x)))))
+   (term (gen 2 1)))
+
+  (test-->>
+   floe-reduce
+   (term (~> (gen 1 2)
+             (-< (esc (λ (x y) (values x y)))
+                 (esc (λ (x y) (values y x))))))
+   (term (gen 1 2 2 1)))
+
+  (test-->>
+   floe-reduce
+   (term (~> (gen 1 2)
+             (== (esc (λ (x) (values 0 x)))
+                 (esc (λ (x) (values x 3))))))
+   (term (gen 0 1 2 3)))
+
+  (test-->>
+   floe-reduce
+   (term (~> (gen 1 2)
+             (>< (esc (λ (x) (values x 0))))))
+   (term (gen 1 0 2 0)))
+
+  (test-->
+   floe-reduce
+   (term (~> (gen 1 2 3) (gen 4)))
+   (term (gen 4))))