Make Maybe a builtin inductive type (#2860)

This is required as the return type of the builtin
`anomaVerifyWithMessage` axiom.

Part of:
* https://github.com/anoma/juvix/issues/2850

include/package-base/Juvix/Builtin/V1/Maybe.juvix

@@ -2,6 +2,7 @@ module Juvix.Builtin.V1.Maybe;
 
 --- Represents an optional value that may or may not be present. Provides a way
 --- to handle null or missing values in a type-safe manner.
+builtin maybe
 type Maybe A :=
   | nothing
   | just A;

src/Juvix/Compiler/Builtins.hs

@@ -5,6 +5,7 @@ module Juvix.Compiler.Builtins
     module Juvix.Compiler.Builtins.Int,
     module Juvix.Compiler.Builtins.Bool,
     module Juvix.Compiler.Builtins.List,
+    module Juvix.Compiler.Builtins.Maybe,
     module Juvix.Compiler.Builtins.String,
     module Juvix.Compiler.Builtins.Field,
     module Juvix.Compiler.Builtins.Debug,
@@ -24,5 +25,6 @@ import Juvix.Compiler.Builtins.Field
 import Juvix.Compiler.Builtins.IO
 import Juvix.Compiler.Builtins.Int
 import Juvix.Compiler.Builtins.List
+import Juvix.Compiler.Builtins.Maybe
 import Juvix.Compiler.Builtins.Nat
 import Juvix.Compiler.Builtins.String

src/Juvix/Compiler/Builtins/Maybe.hs

@@ -0,0 +1,37 @@
+module Juvix.Compiler.Builtins.Maybe where
+
+import Juvix.Compiler.Builtins.Effect
+import Juvix.Compiler.Internal.Extra
+import Juvix.Compiler.Internal.Pretty
+import Juvix.Prelude
+
+registerMaybeDef :: (Member Builtins r) => InductiveDef -> Sem r ()
+registerMaybeDef d = do
+  unless (isSmallUniverse' (d ^. inductiveType)) (error "Maybe should be in the small universe")
+  registerBuiltin BuiltinMaybe (d ^. inductiveName)
+  case d ^. inductiveConstructors of
+    [c1, c2] -> registerNothing param c1 >> registerJust param c2
+    _ -> error "Maybe should have exactly two constructors"
+  where
+    param :: VarName
+    param = case d ^. inductiveParameters of
+      [v] -> v ^. inductiveParamName
+      _ -> error "Maybe should have exactly one type parameter"
+
+registerNothing :: (Member Builtins r) => VarName -> ConstructorDef -> Sem r ()
+registerNothing a d@ConstructorDef {..} = do
+  let nothing = _inductiveConstructorName
+      ty = _inductiveConstructorType
+  maybe_ <- getBuiltinName (getLoc d) BuiltinMaybe
+  let nothingty = maybe_ @@ a
+  unless (ty === nothingty) (error $ "nothing has the wrong type " <> ppTrace ty <> " | " <> ppTrace nothingty)
+  registerBuiltin BuiltinMaybeNothing nothing
+
+registerJust :: (Member Builtins r) => VarName -> ConstructorDef -> Sem r ()
+registerJust a d@ConstructorDef {..} = do
+  let just_ = _inductiveConstructorName
+      ty = _inductiveConstructorType
+  maybe_ <- getBuiltinName (getLoc d) BuiltinMaybe
+  let justty = a --> maybe_ @@ a
+  unless (ty === justty) (error "just has the wrong type")
+  registerBuiltin BuiltinMaybeJust just_

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

@@ -47,6 +47,7 @@ builtinConstructors = \case
   BuiltinBool -> [BuiltinBoolTrue, BuiltinBoolFalse]
   BuiltinInt -> [BuiltinIntOfNat, BuiltinIntNegSuc]
   BuiltinList -> [BuiltinListNil, BuiltinListCons]
+  BuiltinMaybe -> [BuiltinMaybeNothing, BuiltinMaybeJust]
   BuiltinPoseidonState -> [BuiltinMkPoseidonState]
   BuiltinEcPoint -> [BuiltinMkEcPoint]
 
@@ -55,6 +56,7 @@ data BuiltinInductive
   | BuiltinBool
   | BuiltinInt
   | BuiltinList
+  | BuiltinMaybe
   | BuiltinPoseidonState
   | BuiltinEcPoint
   deriving stock (Show, Eq, Ord, Enum, Bounded, Generic, Data)
@@ -71,6 +73,7 @@ instance Pretty BuiltinInductive where
     BuiltinBool -> Str.bool_
     BuiltinInt -> Str.int_
     BuiltinList -> Str.list
+    BuiltinMaybe -> Str.maybe_
     BuiltinPoseidonState -> Str.cairoPoseidonState
     BuiltinEcPoint -> Str.cairoEcPoint
 
@@ -84,6 +87,8 @@ instance Pretty BuiltinConstructor where
     BuiltinIntNegSuc -> Str.negSuc
     BuiltinListNil -> Str.nil
     BuiltinListCons -> Str.cons
+    BuiltinMaybeNothing -> Str.nothing
+    BuiltinMaybeJust -> Str.just
     BuiltinMkPoseidonState -> Str.cairoMkPoseidonState
     BuiltinMkEcPoint -> Str.cairoMkEcPoint
 
@@ -96,6 +101,8 @@ data BuiltinConstructor
   | BuiltinIntNegSuc
   | BuiltinListNil
   | BuiltinListCons
+  | BuiltinMaybeNothing
+  | BuiltinMaybeJust
   | BuiltinMkPoseidonState
   | BuiltinMkEcPoint
   deriving stock (Show, Eq, Ord, Generic, Data)

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

@@ -209,6 +209,8 @@ goConstructor sym ctor = do
       Just Internal.BuiltinIntNegSuc -> freshTag
       Just Internal.BuiltinListNil -> freshTag
       Just Internal.BuiltinListCons -> freshTag
+      Just Internal.BuiltinMaybeNothing -> freshTag
+      Just Internal.BuiltinMaybeJust -> freshTag
       Just Internal.BuiltinMkPoseidonState -> freshTag
       Just Internal.BuiltinMkEcPoint -> freshTag
       Nothing -> freshTag

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

@@ -62,6 +62,8 @@ fromCore fsize tab =
       BuiltinListCons -> True
       BuiltinMkPoseidonState -> True
       BuiltinMkEcPoint -> True
+      BuiltinMaybeNothing -> True
+      BuiltinMaybeJust -> True
       BuiltinNatZero -> False
       BuiltinNatSuc -> False
       BuiltinBoolTrue -> False
@@ -107,6 +109,7 @@ fromCore fsize tab =
         BuiltinRandomEcPoint -> False
       BuiltinTypeInductive i -> case i of
         BuiltinList -> True
+        BuiltinMaybe -> True
         BuiltinPoseidonState -> True
         BuiltinEcPoint -> True
         BuiltinNat -> False

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

@@ -194,6 +194,7 @@ checkBuiltinInductiveStartNode i = whenJust (i ^. inductiveBuiltin) go
         modify (set builderStateInt (Just (i ^. inductiveName)))
         addInductiveStartNode
       BuiltinList -> return ()
+      BuiltinMaybe -> return ()
       BuiltinPoseidonState -> return ()
       BuiltinEcPoint -> return ()
 

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

@@ -503,6 +503,7 @@ registerBuiltinInductive d = \case
   BuiltinBool -> registerBoolDef d
   BuiltinInt -> registerIntDef d
   BuiltinList -> registerListDef d
+  BuiltinMaybe -> registerMaybeDef d
   BuiltinPoseidonState -> registerPoseidonStateDef d
   BuiltinEcPoint -> registerEcPointDef d
 

src/Juvix/Extra/Strings.hs

@@ -194,6 +194,9 @@ bool_ = "bool"
 list :: (IsString s) => s
 list = "list"
 
+maybe_ :: (IsString s) => s
+maybe_ = "maybe"
+
 int_ :: (IsString s) => s
 int_ = "int"
 
@@ -989,6 +992,12 @@ nil = "nil"
 cons :: (IsString s) => s
 cons = "cons"
 
+nothing :: (IsString s) => s
+nothing = "nothing"
+
+just :: (IsString s) => s
+just = "just"
+
 unary :: (IsString s) => s
 unary = "unary"
 

test/Compilation/Positive.hs

@@ -450,5 +450,10 @@ tests =
         "Test075: Multiway If"
         $(mkRelDir ".")
         $(mkRelFile "test075.juvix")
-        $(mkRelFile "out/test075.out")
+        $(mkRelFile "out/test075.out"),
+      posTestEval
+        "Test076: Builtin Maybe"
+        $(mkRelDir ".")
+        $(mkRelFile "test076.juvix")
+        $(mkRelFile "out/test076.out")
     ]

tests/Compilation/positive/out/test076.out

@@ -0,0 +1 @@
+6

tests/Compilation/positive/test076.juvix

@@ -0,0 +1,15 @@
+-- builtin maybe
+module test076;
+
+import Juvix.Builtin.V1.Nat open;
+
+builtin maybe
+type Maybe A :=
+  | nothing
+  | just A;
+
+fromMaybe {A} (default : A) : Maybe A -> A
+  | nothing := default
+  | (just a) := a;
+
+main : Nat := fromMaybe 0 (just 1) + fromMaybe 5 nothing;