From f679860cc78918803367de42629ebab7457df398 Mon Sep 17 00:00:00 2001
From: Shriram Krishnamurthi <75030+shriram@users.noreply.github.com>
Date: Tue, 15 Jul 2025 20:22:41 -0400
Subject: [PATCH 1/2] added type refinements

---
 examples/refinement.html.pm | 11 ++++++++++
 examples/refinement.js      | 41 +++++++++++++++++++++++++++++++++++++
 index.html.pm               |  1 +
 3 files changed, 53 insertions(+)
 create mode 100644 examples/refinement.html.pm
 create mode 100644 examples/refinement.js

diff --git a/examples/refinement.html.pm b/examples/refinement.html.pm
new file mode 100644
index 0000000..8c32ab7
--- /dev/null
+++ b/examples/refinement.html.pm
@@ -0,0 +1,11 @@
+#lang pollen
+
+◊p{
+   As students learn to work with invariants, it is helpful and
+   instructive to express them directly in the source program. Pyret
+   supports ◊em{refinments} to enable this. Currently, refinements in
+   Pyret are checked dynamically, so that students don't have to go
+   through the hurdles of convincing a proof-assistant that the
+   program is compliant, and they can get concrete examples of
+   failures.
+   }
diff --git a/examples/refinement.js b/examples/refinement.js
new file mode 100644
index 0000000..5f361d0
--- /dev/null
+++ b/examples/refinement.js
@@ -0,0 +1,41 @@
+const example = `use context starter2024
+
+fun is-sorted-ascending(l :: List<Number>) -> Boolean:
+  cases (List) l:
+    | empty => true
+    | link(f, r) =>
+      cases (List) r:
+        | empty => true
+        | link(fr, rr) =>
+          if f <= fr:
+            is-sorted-ascending(r)
+          else:
+            false
+          end
+      end
+  end
+end
+
+fun insert(n :: Number,
+    l :: List%(is-sorted-ascending))
+  -> List%(is-sorted-ascending):
+  cases (List) l:
+    | empty => [list: n]
+    | link(f, r) =>
+      if n < f: link(n, l)
+      else:     link(f, insert(n, r))
+      end
+  end
+end
+
+check:
+  insert(1, [list: 2, 3, 4]) is [list: 1, 2, 3, 4]
+  insert(1, [list: 3, 2, 4]) raises "predicate"
+end
+`;
+
+export const refinement = {
+  definitionsAtLastRun: example,
+  editorContents: example,
+  replContents: ""
+};
diff --git a/index.html.pm b/index.html.pm
index 701a555..4b209c2 100644
--- a/index.html.pm
+++ b/index.html.pm
@@ -14,6 +14,7 @@
 		    ("tables" . "Tables")
 		    ("data" . "Data Structures")
 		    ("lambdas" . "Lambdas")
+		    ("refinement" . "Type Refinements")
 		    ("oop" . "Object-Oriented Programming")
 		    ("forloops" . "Loops")
 		    ("mutation" . "Mutation and State")

From c6c82de2eb6a502181ea8fb7baceaa73626c6e85 Mon Sep 17 00:00:00 2001
From: Shriram Krishnamurthi <75030+shriram@users.noreply.github.com>
Date: Wed, 16 Jul 2025 07:22:04 -0400
Subject: [PATCH 2/2] added exhortation to try it for themselves

---
 examples/refinement.js | 3 +++
 1 file changed, 3 insertions(+)

diff --git a/examples/refinement.js b/examples/refinement.js
index 5f361d0..57d384b 100644
--- a/examples/refinement.js
+++ b/examples/refinement.js
@@ -32,6 +32,9 @@ check:
   insert(1, [list: 2, 3, 4]) is [list: 1, 2, 3, 4]
   insert(1, [list: 3, 2, 4]) raises "predicate"
 end
+
+# Uncomment and run the next line to see the error message!
+# insert(1, [list: 3, 2, 4])
 `;
 
 export const refinement = {