Add assert function to Haskell.Control.Exception

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 : _

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

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
 #-}

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 #-}

test/golden/AllTests.hs

@@ -88,4 +88,5 @@ import ProjectionLike
 import FunCon
 import Issue308
 import Issue324
+import Assert
 

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)
+