assert builtin

src/Juvix/Compiler/Builtins/Assert.hs

@@ -0,0 +1,16 @@
+module Juvix.Compiler.Builtins.Assert where
+
+import Juvix.Compiler.Internal.Builtins
+import Juvix.Compiler.Internal.Extra
+import Juvix.Prelude
+
+checkAssert :: (Members '[Reader BuiltinsTable, Error ScoperError, NameIdGen] r) => FunctionDef -> Sem r ()
+checkAssert f = do
+  let ftype = f ^. funDefType
+      u = ExpressionUniverse smallUniverseNoLoc
+      l = getLoc f
+  bool_ <- getBuiltinNameScoper (getLoc f) BuiltinBool
+  valueT <- freshVar l "valueT"
+  let freeVars = hashSet [valueT]
+  unless ((ftype ==% (u <>--> bool_ --> valueT --> valueT)) freeVars) $
+    builtinsErrorText (getLoc f) "assert must be of type {Value : Type} -> Bool -> Value -> Value"

src/Juvix/Compiler/Concrete/Data/Builtins.hs

@@ -125,7 +125,8 @@ instance Serialize BuiltinConstructor
 instance NFData BuiltinConstructor
 
 data BuiltinFunction
-  = BuiltinNatPlus
+  = BuiltinAssert
+  | BuiltinNatPlus
   | BuiltinNatSub
   | BuiltinNatMul
   | BuiltinNatUDiv
@@ -163,6 +164,7 @@ instance NFData BuiltinFunction
 
 instance Pretty BuiltinFunction where
   pretty = \case
+    BuiltinAssert -> Str.assert
     BuiltinNatPlus -> Str.natPlus
     BuiltinNatSub -> Str.natSub
     BuiltinNatMul -> Str.natMul
@@ -368,6 +370,7 @@ isNatBuiltin = \case
   BuiltinNatLt -> True
   BuiltinNatEq -> True
   --
+  BuiltinAssert -> False
   BuiltinBoolIf -> False
   BuiltinBoolOr -> False
   BuiltinBoolAnd -> False
@@ -403,6 +406,7 @@ isIntBuiltin = \case
   BuiltinIntLe -> True
   BuiltinIntLt -> True
   --
+  BuiltinAssert -> False
   BuiltinNatPlus -> False
   BuiltinNatSub -> False
   BuiltinNatMul -> False
@@ -425,6 +429,7 @@ isCastBuiltin = \case
   BuiltinFromNat -> True
   BuiltinFromInt -> True
   --
+  BuiltinAssert -> False
   BuiltinIntEq -> False
   BuiltinIntPlus -> False
   BuiltinIntSubNat -> False
@@ -463,6 +468,7 @@ isIgnoredBuiltin f
         .&&. (not . isIntBuiltin)
         .&&. (not . isCastBuiltin)
         .&&. (/= BuiltinMonadBind)
+        .&&. (/= BuiltinAssert)
         $ f
 
     explicit :: Bool
@@ -495,6 +501,8 @@ isIgnoredBuiltin f
       BuiltinNatEq -> False
       -- Monad
       BuiltinMonadBind -> False
+      -- Assert
+      BuiltinAssert -> False
       -- Ignored
       BuiltinBoolIf -> True
       BuiltinBoolOr -> True

src/Juvix/Compiler/Core/Translation/Stripped/FromCore.hs

@@ -54,6 +54,7 @@ fromCore fsize tab =
       BuiltinIntLt -> False
       BuiltinSeq -> False
       BuiltinMonadBind -> True -- TODO revise
+      BuiltinAssert -> True
       BuiltinFromNat -> True
       BuiltinFromInt -> True
 

src/Juvix/Compiler/Internal/Translation/FromConcrete.hs

@@ -14,6 +14,7 @@ import Data.HashSet qualified as HashSet
 import Data.IntMap.Strict qualified as IntMap
 import Data.List.NonEmpty qualified as NonEmpty
 import Juvix.Compiler.Builtins
+import Juvix.Compiler.Builtins.Assert
 import Juvix.Compiler.Builtins.Pair
 import Juvix.Compiler.Concrete.Data.ScopedName qualified as S
 import Juvix.Compiler.Concrete.Extra qualified as Concrete
@@ -537,6 +538,7 @@ checkBuiltinFunction ::
   BuiltinFunction ->
   Sem r ()
 checkBuiltinFunction d f = localBuiltins $ case f of
+  BuiltinAssert -> checkAssert d
   BuiltinNatPlus -> checkNatPlus d
   BuiltinNatSub -> checkNatSub d
   BuiltinNatMul -> checkNatMul d

src/Juvix/Extra/Strings.hs

@@ -260,6 +260,9 @@ ioSequence = "IO-sequence"
 ioReadline :: (IsString s) => s
 ioReadline = "IO-readline"
 
+assert :: (IsString s) => s
+assert = "assert"
+
 natPrint :: (IsString s) => s
 natPrint = "nat-print"