From ebbf0fc10c9914cbcec2004684d15a9e4f8bb339 Mon Sep 17 00:00:00 2001 From: giles Date: Thu, 7 May 2026 13:36:39 +0000 Subject: [PATCH] =?UTF-8?q?haskell:=20Phase=2013=20=E2=80=94=20Ord=20defau?= =?UTF-8?q?lt=20verification=20(myMax/myMin)=20(+5=20tests,=2010/10)?= MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit Co-Authored-By: Claude Sonnet 4.6 --- lib/haskell/tests/class-defaults.sx | 29 +++++++++++++++++++++++++++++ plans/haskell-completeness.md | 7 ++++++- 2 files changed, 35 insertions(+), 1 deletion(-) diff --git a/lib/haskell/tests/class-defaults.sx b/lib/haskell/tests/class-defaults.sx index c3710957..db3372c1 100644 --- a/lib/haskell/tests/class-defaults.sx +++ b/lib/haskell/tests/class-defaults.sx @@ -35,4 +35,33 @@ "class Hi a where\n greet :: a -> String\n greet x = \"default\"\ninstance Hi Bool where\nmain = greet True")) "default") +(define + hk-myord-source + "class MyOrd a where\n myCmp :: a -> a -> Bool\n myMax :: a -> a -> a\n myMin :: a -> a -> a\n myMax a b = if myCmp a b then a else b\n myMin a b = if myCmp a b then b else a\ninstance MyOrd Int where\n myCmp x y = x >= y\n") + +(hk-test + "Ord default: myMax 3 5 = 5" + (hk-deep-force (hk-run (str hk-myord-source "main = myMax 3 5\n"))) + 5) + +(hk-test + "Ord default: myMax 8 2 = 8" + (hk-deep-force (hk-run (str hk-myord-source "main = myMax 8 2\n"))) + 8) + +(hk-test + "Ord default: myMin 3 5 = 3" + (hk-deep-force (hk-run (str hk-myord-source "main = myMin 3 5\n"))) + 3) + +(hk-test + "Ord default: myMin 8 2 = 2" + (hk-deep-force (hk-run (str hk-myord-source "main = myMin 8 2\n"))) + 2) + +(hk-test + "Ord default: myMax of equals returns first" + (hk-deep-force (hk-run (str hk-myord-source "main = myMax 4 4\n"))) + 4) + {:fails hk-test-fails :pass hk-test-pass :fail hk-test-fail} diff --git a/plans/haskell-completeness.md b/plans/haskell-completeness.md index 461c4926..7adc9d90 100644 --- a/plans/haskell-completeness.md +++ b/plans/haskell-completeness.md @@ -232,7 +232,7 @@ No OCaml changes are needed. The view type is fully representable as an SX dict. explicit `/=` in every Eq instance. _Verified using a `MyEq`/`myNeq` class + instance test (operator-style `(/=)` is a parser concern; the default mechanism itself is verified)._ -- [ ] `Ord` defaults: `max a b = if a >= b then a else b`, `min a b = if a <= +- [x] `Ord` defaults: `max a b = if a >= b then a else b`, `min a b = if a <= b then a else b`. Verify. - [ ] `Num` defaults: `negate x = 0 - x`, `abs x = if x < 0 then negate x else x`, `signum x = if x > 0 then 1 else if x < 0 then -1 else 0`. Verify. @@ -309,6 +309,11 @@ No OCaml changes are needed. The view type is fully representable as an SX dict. _Newest first._ +**2026-05-07** — Phase 13 Ord-style default verification: +- Added 5 tests to `class-defaults.sx` for myMax/myMin defined as defaults + in terms of `myCmp` (≥). Verified myMax/myMin on (3,5), (8,2), (4,4). + Suite is now 10/10. + **2026-05-07** — Phase 13 Eq-style default verification: - New `tests/class-defaults.sx` (5 tests) seeds the class-defaults test file. Covers a 2-arg default method (`myNeq x y = not (myEq x y)`) where the