Add support for assert function from 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 : _

lib/Haskell/Extra/Dec.agda

@@ -46,3 +46,20 @@ mapDec f g (False ⟨ h ⟩) = False ⟨ h ∘ g ⟩
 ifDec : Dec a → (@0 {{a}} → b) → (@0 {{a → ⊥}} → b) → b
 ifDec (b ⟨ p ⟩) x y = if b then (λ where {{refl}} → x {{p}}) else (λ where {{refl}} → y {{p}})
 {-# COMPILE AGDA2HS ifDec inline #-}
+
+instance
+  iDecIsTrue : {b : Bool} → Dec (IsTrue b)
+  iDecIsTrue {False} = False ⟨ (λ ()) ⟩
+  iDecIsTrue {True}  = True  ⟨ IsTrue.itsTrue ⟩
+  {-# COMPILE AGDA2HS iDecIsTrue transparent #-}
+
+  iDecIsFalse : {b : Bool} → Dec (IsFalse b)
+  iDecIsFalse {b} = mapDec isTrueNotIsFalse isFalseIsTrueNot (iDecIsTrue {not b})
+    where
+      @0 isTrueNotIsFalse : {b : Bool} → IsTrue (not b) → IsFalse b
+      isTrueNotIsFalse {False} IsTrue.itsTrue = IsFalse.itsFalse
+
+      @0 isFalseIsTrueNot : {b : Bool} → IsFalse b → IsTrue (not b)
+      isFalseIsTrueNot {False} IsFalse.itsFalse = IsTrue.itsTrue
+  {-# COMPILE AGDA2HS iDecIsFalse inline #-}
+

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/NonClassInstance.agda

@@ -3,13 +3,6 @@ open import Haskell.Prelude
 open import Haskell.Extra.Dec
 open import Haskell.Extra.Refinement
 
-instance
-  iDecIsTrue : {b : Bool} → Dec (IsTrue b)
-  iDecIsTrue {False} = False ⟨ (λ ()) ⟩
-  iDecIsTrue {True}  = True  ⟨ IsTrue.itsTrue ⟩
-
-{-# COMPILE AGDA2HS iDecIsTrue #-}
-
 foo : (b : Bool) → {{Dec (IsTrue b)}} → Bool
 foo _ {{b ⟨ _ ⟩}} = not b
 

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

test/golden/NonClassInstance.hs

@@ -1,12 +1,8 @@
 module NonClassInstance where
 
-iDecIsTrue :: Bool -> Bool
-iDecIsTrue False = False
-iDecIsTrue True = True
-
 foo :: Bool -> Bool -> Bool
 foo _ b = not b
 
 bar :: Bool -> Bool
-bar b = foo b (iDecIsTrue b)
+bar b = foo b b