From 7cae101843a077eb4dcb8f8a294e2215cbaf0dff Mon Sep 17 00:00:00 2001
From: Jesper Cockx <jesper@sikanda.be>
Date: Mon, 6 Jan 2025 17:43:15 +0100
Subject: [PATCH] Add `assert` function to `Haskell.Control.Exception`

---
 lib/Haskell/Control/Exception.agda | 11 +++++++++++
 src/Agda2Hs/Compile/Name.hs        |  1 +
 test/AllTests.agda                 |  2 ++
 test/Assert.agda                   | 10 ++++++++++
 test/golden/AllTests.hs            |  1 +
 test/golden/Assert.hs              |  8 ++++++++
 6 files changed, 33 insertions(+)
 create mode 100644 lib/Haskell/Control/Exception.agda
 create mode 100644 test/Assert.agda
 create mode 100644 test/golden/Assert.hs

diff --git a/lib/Haskell/Control/Exception.agda b/lib/Haskell/Control/Exception.agda
new file mode 100644
index 00000000..5c4323ae
--- /dev/null
+++ b/lib/Haskell/Control/Exception.agda
@@ -0,0 +1,11 @@
+module Haskell.Control.Exception where
+
+open import Haskell.Prim
+
+open import Haskell.Extra.Dec
+open import Haskell.Extra.Refinement
+
+assert : (@0 b : Set ℓ) → {{Dec b}} → (@0 {{b}} → a) → a
+assert _ {{True  ⟨ p ⟩}} x = x {{p}}
+assert _ {{False ⟨ _ ⟩}} x = oops
+  where postulate oops : _
diff --git a/src/Agda2Hs/Compile/Name.hs b/src/Agda2Hs/Compile/Name.hs
index 8cd55e1d..bb2ad92b 100644
--- a/src/Agda2Hs/Compile/Name.hs
+++ b/src/Agda2Hs/Compile/Name.hs
@@ -67,6 +67,7 @@ defaultSpecialRules :: SpecialRules
 defaultSpecialRules = Map.fromList
   [ "Agda.Builtin.Nat.Nat"          `to` "Natural"      `importing` Just "Numeric.Natural"
   , "Haskell.Control.Monad.guard"   `to` "guard"        `importing` Just "Control.Monad"
+  , "Haskell.Control.Exception.assert" `to` "assert"    `importing` Just "Control.Exception"
   , "Haskell.Prelude.coerce"        `to` "unsafeCoerce" `importing` Just "Unsafe.Coerce"
   , "Agda.Builtin.Int.Int"          `to` "Integer"      `importing` Nothing
   , "Agda.Builtin.Word.Word64"      `to` "Word"         `importing` Nothing
diff --git a/test/AllTests.agda b/test/AllTests.agda
index 84a701d2..53c2f9b7 100644
--- a/test/AllTests.agda
+++ b/test/AllTests.agda
@@ -93,6 +93,7 @@ import ProjectionLike
 import FunCon
 import Issue308
 import Issue324
+import Assert
 
 {-# FOREIGN AGDA2HS
 import Issue14
@@ -183,4 +184,5 @@ import ProjectionLike
 import FunCon
 import Issue308
 import Issue324
+import Assert
 #-}
diff --git a/test/Assert.agda b/test/Assert.agda
new file mode 100644
index 00000000..e3145162
--- /dev/null
+++ b/test/Assert.agda
@@ -0,0 +1,10 @@
+
+open import Haskell.Prelude
+open import Haskell.Control.Exception
+open import Haskell.Law.Ord
+open import Haskell.Extra.Dec
+
+subtractChecked : Nat → Nat → Nat
+subtractChecked x y = assert (IsFalse (x < y)) (x - y)
+
+{-# COMPILE AGDA2HS subtractChecked #-}
diff --git a/test/golden/AllTests.hs b/test/golden/AllTests.hs
index bb75ed92..1c79aa3e 100644
--- a/test/golden/AllTests.hs
+++ b/test/golden/AllTests.hs
@@ -88,4 +88,5 @@ import ProjectionLike
 import FunCon
 import Issue308
 import Issue324
+import Assert
 
diff --git a/test/golden/Assert.hs b/test/golden/Assert.hs
new file mode 100644
index 00000000..71aa14af
--- /dev/null
+++ b/test/golden/Assert.hs
@@ -0,0 +1,8 @@
+module Assert where
+
+import Control.Exception (assert)
+import Numeric.Natural (Natural)
+
+subtractChecked :: Natural -> Natural -> Natural
+subtractChecked x y = assert (not (x < y)) (x - y)
+