make Eq builtin

src/Juvix/Compiler/Builtins.hs

@@ -1,6 +1,7 @@
 module Juvix.Compiler.Builtins
   ( module Juvix.Compiler.Builtins.Nat,
     module Juvix.Compiler.Builtins.IO,
+    module Juvix.Compiler.Builtins.Eq,
     module Juvix.Compiler.Builtins.Int,
     module Juvix.Compiler.Builtins.Bool,
     module Juvix.Compiler.Builtins.List,
@@ -24,6 +25,7 @@ import Juvix.Compiler.Builtins.ByteArray
 import Juvix.Compiler.Builtins.Cairo
 import Juvix.Compiler.Builtins.Control
 import Juvix.Compiler.Builtins.Debug
+import Juvix.Compiler.Builtins.Eq
 import Juvix.Compiler.Builtins.Field
 import Juvix.Compiler.Builtins.IO
 import Juvix.Compiler.Builtins.Int

src/Juvix/Compiler/Builtins/Eq.hs

@@ -0,0 +1,10 @@
+module Juvix.Compiler.Builtins.Eq where
+
+import Juvix.Compiler.Internal.Extra
+import Juvix.Prelude
+
+checkEqDef :: InductiveDef -> Sem r ()
+checkEqDef _ = return ()
+
+checkIsEq :: FunctionDef -> Sem r ()
+checkIsEq _ = return ()

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

@@ -59,6 +59,7 @@ builtinConstructors = \case
   BuiltinEcPoint -> [BuiltinMkEcPoint]
   BuiltinAnomaResource -> [BuiltinMkAnomaResource]
   BuiltinAnomaAction -> [BuiltinMkAnomaAction]
+  BuiltinEq -> [BuiltinMkEq]
 
 data BuiltinInductive
   = BuiltinNat
@@ -67,6 +68,7 @@ data BuiltinInductive
   | BuiltinList
   | BuiltinMaybe
   | BuiltinPair
+  | BuiltinEq
   | BuiltinPoseidonState
   | BuiltinEcPoint
   | BuiltinAnomaResource
@@ -87,6 +89,7 @@ instance Pretty BuiltinInductive where
     BuiltinList -> Str.list
     BuiltinMaybe -> Str.maybe_
     BuiltinPair -> Str.pair
+    BuiltinEq -> Str.eq
     BuiltinPoseidonState -> Str.cairoPoseidonState
     BuiltinEcPoint -> Str.cairoEcPoint
     BuiltinAnomaResource -> Str.anomaResource
@@ -109,6 +112,7 @@ instance Pretty BuiltinConstructor where
     BuiltinMkEcPoint -> Str.cairoMkEcPoint
     BuiltinMkAnomaResource -> Str.anomaMkResource
     BuiltinMkAnomaAction -> Str.anomaMkAction
+    BuiltinMkEq -> Str.mkEq
 
 data BuiltinConstructor
   = BuiltinNatZero
@@ -119,6 +123,7 @@ data BuiltinConstructor
   | BuiltinIntNegSuc
   | BuiltinListNil
   | BuiltinListCons
+  | BuiltinMkEq
   | BuiltinMaybeNothing
   | BuiltinMaybeJust
   | BuiltinPairConstr
@@ -161,6 +166,7 @@ data BuiltinFunction
   | BuiltinIntLe
   | BuiltinIntLt
   | BuiltinFromNat
+  | BuiltinIsEq
   | BuiltinFromInt
   | BuiltinSeq
   | BuiltinMonadBind
@@ -202,6 +208,7 @@ instance Pretty BuiltinFunction where
     BuiltinFromNat -> Str.fromNat
     BuiltinFromInt -> Str.fromInt
     BuiltinSeq -> Str.builtinSeq
+    BuiltinIsEq -> Str.isEqual
     BuiltinMonadBind -> Str.builtinMonadBind
 
 data BuiltinAxiom
@@ -434,6 +441,7 @@ isNatBuiltin = \case
   BuiltinNatLt -> True
   BuiltinNatEq -> True
   --
+  BuiltinIsEq -> False
   BuiltinAssert -> False
   BuiltinBoolIf -> False
   BuiltinBoolOr -> False
@@ -486,13 +494,15 @@ isIntBuiltin = \case
   BuiltinFromNat -> False
   BuiltinFromInt -> False
   BuiltinSeq -> False
+  BuiltinIsEq -> False
   BuiltinMonadBind -> False
 
 isCastBuiltin :: BuiltinFunction -> Bool
 isCastBuiltin = \case
   BuiltinFromNat -> True
   BuiltinFromInt -> True
   --
+  BuiltinIsEq -> False
   BuiltinAssert -> False
   BuiltinIntEq -> False
   BuiltinIntPlus -> False
@@ -532,6 +542,7 @@ isIgnoredBuiltin f
         .&&. (not . isIntBuiltin)
         .&&. (not . isCastBuiltin)
         .&&. (/= BuiltinMonadBind)
+        .&&. (/= BuiltinIsEq)
         $ f
 
     explicit :: Bool
@@ -562,6 +573,8 @@ isIgnoredBuiltin f
       BuiltinNatLe -> False
       BuiltinNatLt -> False
       BuiltinNatEq -> False
+      -- Eq
+      BuiltinIsEq -> False
       -- Monad
       BuiltinMonadBind -> False
       -- Ignored

src/Juvix/Compiler/Core/Pretty/Base.hs

@@ -647,16 +647,17 @@ instance PrettyCode InfoTable where
           shouldPrintInductive :: Maybe BuiltinType -> Bool
           shouldPrintInductive = \case
             Just (BuiltinTypeInductive i) -> case i of
-              BuiltinList -> False
-              BuiltinMaybe -> False
               BuiltinPair -> True
               BuiltinPoseidonState -> True
               BuiltinEcPoint -> True
+              BuiltinAnomaResource -> True
+              BuiltinAnomaAction -> True
+              BuiltinList -> False
+              BuiltinEq -> False
+              BuiltinMaybe -> False
               BuiltinNat -> False
               BuiltinInt -> False
               BuiltinBool -> False
-              BuiltinAnomaResource -> True
-              BuiltinAnomaAction -> True
             Just _ -> False
             Nothing -> True
 

src/Juvix/Compiler/Core/Translation/FromInternal.hs

@@ -217,6 +217,7 @@ goConstructor sym ctor = do
     ctorTag = \case
       Just Internal.BuiltinBoolTrue -> return (BuiltinTag TagTrue)
       Just Internal.BuiltinBoolFalse -> return (BuiltinTag TagFalse)
+      Just Internal.BuiltinMkEq -> freshTag
       Just Internal.BuiltinNatZero -> freshTag
       Just Internal.BuiltinNatSuc -> freshTag
       Just Internal.BuiltinIntOfNat -> freshTag

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

@@ -54,6 +54,7 @@ fromCore fsize tab =
       BuiltinIntLe -> False
       BuiltinIntLt -> False
       BuiltinSeq -> False
+      BuiltinIsEq -> False
       BuiltinMonadBind -> True -- TODO revise
       BuiltinFromNat -> True
       BuiltinFromInt -> True
@@ -62,19 +63,20 @@ fromCore fsize tab =
     shouldKeepConstructor = \case
       BuiltinListNil -> True
       BuiltinListCons -> True
+      BuiltinMkEq -> True
       BuiltinMkPoseidonState -> True
       BuiltinMkEcPoint -> True
       BuiltinMaybeNothing -> True
       BuiltinMaybeJust -> True
       BuiltinPairConstr -> True
+      BuiltinMkAnomaResource -> True
+      BuiltinMkAnomaAction -> True
       BuiltinNatZero -> False
       BuiltinNatSuc -> False
       BuiltinBoolTrue -> False
       BuiltinBoolFalse -> False
       BuiltinIntOfNat -> False
       BuiltinIntNegSuc -> False
-      BuiltinMkAnomaResource -> True
-      BuiltinMkAnomaAction -> True
 
     shouldKeepType :: BuiltinType -> Bool
     shouldKeepType = \case
@@ -141,6 +143,7 @@ fromCore fsize tab =
         BuiltinByteArrayLength -> False
       BuiltinTypeInductive i -> case i of
         BuiltinList -> True
+        BuiltinEq -> True
         BuiltinMaybe -> True
         BuiltinPair -> True
         BuiltinPoseidonState -> True

src/Juvix/Compiler/Internal/Extra/DependencyBuilder.hs

@@ -178,7 +178,7 @@ goInductive p i = do
     mapM_ goInductiveParameter (i ^. inductiveParameters)
     goExpression (i ^. inductiveType)
 
--- BuiltinBool and BuiltinNat are required by the Internal to Core translation
+-- | BuiltinBool and BuiltinNat are required by the Internal to Core translation
 -- when translating literal integers to Nats.
 checkBuiltinInductiveStartNode :: forall r. (Members '[State StartNodes, State BuilderState] r) => InductiveDef -> Sem r ()
 checkBuiltinInductiveStartNode i = whenJust (i ^. inductiveBuiltin) go
@@ -199,6 +199,7 @@ checkBuiltinInductiveStartNode i = whenJust (i ^. inductiveBuiltin) go
       BuiltinEcPoint -> return ()
       BuiltinAnomaResource -> return ()
       BuiltinAnomaAction -> return ()
+      BuiltinEq -> return ()
 
     addInductiveStartNode :: Sem r ()
     addInductiveStartNode = addStartNode (i ^. inductiveName)

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

@@ -519,6 +519,7 @@ checkBuiltinInductive ::
   Sem r ()
 checkBuiltinInductive d b = localBuiltins $ case b of
   BuiltinNat -> checkNatDef d
+  BuiltinEq -> checkEqDef d
   BuiltinBool -> checkBoolDef d
   BuiltinInt -> checkIntDef d
   BuiltinList -> checkListDef d
@@ -541,6 +542,7 @@ checkBuiltinFunction ::
   Sem r ()
 checkBuiltinFunction d f = localBuiltins $ case f of
   BuiltinAssert -> checkAssert d
+  BuiltinIsEq -> checkIsEq d
   BuiltinNatPlus -> checkNatPlus d
   BuiltinNatSub -> checkNatSub d
   BuiltinNatMul -> checkNatMul d

src/Juvix/Extra/Strings.hs

@@ -539,6 +539,9 @@ seqq_ = ">>>"
 sseq_ :: (IsString s) => s
 sseq_ = "seq"
 
+isEqual :: (IsString s) => s
+isEqual = "isEqual"
+
 eq :: (IsString s) => s
 eq = "eq"
 
@@ -1145,6 +1148,9 @@ anomaMkResource = "mkResource"
 anomaMkAction :: (IsString s) => s
 anomaMkAction = "mkAction"
 
+mkEq :: (IsString s) => s
+mkEq = "mkEq"
+
 rustFn :: (IsString s) => s
 rustFn = "fn"