Adapt Anoma builtins to new Anoma Node API (#2861)

src/Juvix/Compiler/Builtins/Anoma.hs

@@ -71,18 +71,19 @@ registerAnomaSign f = do
     (error "anomaSign must be of type {A : Type} -> A -> Nat -> Nat")
   registerBuiltin BuiltinAnomaSign (f ^. axiomName)
 
-registerAnomaVerify :: (Members '[Builtins, NameIdGen] r) => AxiomDef -> Sem r ()
-registerAnomaVerify f = do
+registerAnomaVerifyWithMessage :: (Members '[Builtins, NameIdGen] r) => AxiomDef -> Sem r ()
+registerAnomaVerifyWithMessage f = do
   let ftype = f ^. axiomType
       u = ExpressionUniverse smallUniverseNoLoc
       l = getLoc f
   dataT <- freshVar l "dataT"
   nat <- getBuiltinName (getLoc f) BuiltinNat
+  maybe_ <- getBuiltinName (getLoc f) BuiltinMaybe
   let freeVars = HashSet.fromList [dataT]
   unless
-    ((ftype ==% (u <>--> nat --> nat --> dataT)) freeVars)
-    (error "anomaVerify must be of type {A : Type} -> Nat -> Nat -> A")
-  registerBuiltin BuiltinAnomaVerify (f ^. axiomName)
+    ((ftype ==% (u <>--> nat --> nat --> maybe_ @@ dataT)) freeVars)
+    (error "anomaVerify must be of type {A : Type} -> Nat -> Nat -> Maybe A")
+  registerBuiltin BuiltinAnomaVerifyWithMessage (f ^. axiomName)
 
 registerAnomaSignDetached :: (Members '[Builtins, NameIdGen] r) => AxiomDef -> Sem r ()
 registerAnomaSignDetached f = do

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

@@ -209,7 +209,7 @@ data BuiltinAxiom
   | BuiltinAnomaVerifyDetached
   | BuiltinAnomaSign
   | BuiltinAnomaSignDetached
-  | BuiltinAnomaVerify
+  | BuiltinAnomaVerifyWithMessage
   | BuiltinPoseidon
   | BuiltinEcOp
   | BuiltinRandomEcPoint
@@ -246,7 +246,7 @@ instance HasNameKind BuiltinAxiom where
     BuiltinAnomaVerifyDetached -> KNameFunction
     BuiltinAnomaSign -> KNameFunction
     BuiltinAnomaSignDetached -> KNameFunction
-    BuiltinAnomaVerify -> KNameFunction
+    BuiltinAnomaVerifyWithMessage -> KNameFunction
     BuiltinPoseidon -> KNameFunction
     BuiltinEcOp -> KNameFunction
     BuiltinRandomEcPoint -> KNameFunction
@@ -291,7 +291,7 @@ instance Pretty BuiltinAxiom where
     BuiltinAnomaVerifyDetached -> Str.anomaVerifyDetached
     BuiltinAnomaSignDetached -> Str.anomaSignDetached
     BuiltinAnomaSign -> Str.anomaSign
-    BuiltinAnomaVerify -> Str.anomaVerify
+    BuiltinAnomaVerifyWithMessage -> Str.anomaVerifyWithMessage
     BuiltinPoseidon -> Str.cairoPoseidon
     BuiltinEcOp -> Str.cairoEcOp
     BuiltinRandomEcPoint -> Str.cairoRandomEcPoint

src/Juvix/Compiler/Core/Data/InfoTableBuilder.hs

@@ -277,6 +277,17 @@ declareNatBuiltins = do
       (tagSuc, "suc", \x -> mkPi' x x, Just BuiltinNatSuc)
     ]
 
+declareMaybeBuiltins :: (Member InfoTableBuilder r) => Sem r ()
+declareMaybeBuiltins = do
+  tagNothing <- freshTag
+  tagJust <- freshTag
+  declareInductiveBuiltins
+    "Maybe"
+    (Just (BuiltinTypeInductive BuiltinMaybe))
+    [ (tagNothing, "nothing", id, Just BuiltinMaybeNothing),
+      (tagJust, "just", mkPi' mkDynamic', Just BuiltinMaybeJust)
+    ]
+
 reserveLiteralIntToNatSymbol :: (Member InfoTableBuilder r) => Sem r ()
 reserveLiteralIntToNatSymbol = do
   sym <- freshSymbol

src/Juvix/Compiler/Core/Evaluator.hs

@@ -64,23 +64,31 @@ instance Show EvalError where
 instance Exception.Exception EvalError
 
 evalInfoTable :: Handle -> InfoTable -> Node
-evalInfoTable herr info = eval herr idenCtxt [] mainNode
+evalInfoTable herr tab = eval herr tab [] mainNode
   where
-    idenCtxt = info ^. identContext
-    mainSym = fromJust (info ^. infoMain)
-    mainNode = fromJust (HashMap.lookup mainSym idenCtxt)
+    mainSym = fromJust (tab ^. infoMain)
+    mainNode = fromJust (HashMap.lookup mainSym (tab ^. identContext))
 
 -- | `eval ctx env n` evaluates a node `n` whose all free variables point into
 -- `env`. All nodes in `ctx` must be closed. All nodes in `env` must be values.
 -- Invariant for values v: eval ctx env v = v
-eval :: Handle -> IdentContext -> Env -> Node -> Node
+eval :: Handle -> InfoTable -> Env -> Node -> Node
 eval herr ctx env = geval defaultEvalOptions herr ctx env
 
-geval :: EvalOptions -> Handle -> IdentContext -> Env -> Node -> Node
-geval opts herr ctx env0 = eval' env0
+geval :: EvalOptions -> Handle -> InfoTable -> Env -> Node -> Node
+geval opts herr tab env0 = eval' env0
   where
+    ctx :: IdentContext
+    ctx = tab ^. identContext
+
+    evalError' :: Text -> Maybe Node -> a
+    evalError' msg = Exception.throw . EvalError msg
+
     evalError :: Text -> Node -> a
-    evalError msg node = Exception.throw (EvalError msg (Just node))
+    evalError msg node = evalError' msg (Just node)
+
+    evalErrorMsg' :: Text -> a
+    evalErrorMsg' msg = evalError' msg Nothing
 
     eval' :: Env -> Node -> Node
     eval' !env !n = case n of
@@ -201,7 +209,7 @@ geval opts herr ctx env0 = eval' env0
       OpAnomaVerifyDetached -> anomaVerifyDetachedOp
       OpAnomaSign -> anomaSignOp
       OpAnomaSignDetached -> anomaSignDetachedOp
-      OpAnomaVerify -> anomaVerifyOp
+      OpAnomaVerifyWithMessage -> anomaVerifyWithMessageOp
       OpPoseidonHash -> poseidonHashOp
       OpEc -> ecOp
       OpRandomEcPoint -> randomEcPointOp
@@ -406,18 +414,18 @@ geval opts herr ctx env0 = eval' env0
                       Nothing -> err "anomaSignDetachedOp: second argument not an integer"
         {-# INLINE anomaSignDetachedOp #-}
 
-        anomaVerifyOp :: [Node] -> Node
-        anomaVerifyOp = checkApply $ \arg1 arg2 ->
+        anomaVerifyWithMessageOp :: [Node] -> Node
+        anomaVerifyWithMessageOp = checkApply $ \arg1 arg2 ->
           let !v1 = eval' env arg1
               !v2 = eval' env arg2
            in if
                   | opts ^. evalOptionsNormalize || opts ^. evalOptionsNoFailure ->
-                      mkBuiltinApp' OpAnomaVerify [v1, v2]
+                      mkBuiltinApp' OpAnomaVerifyWithMessage [v1, v2]
                   | otherwise ->
                       case (integerFromNode v1, integerFromNode v2) of
                         (Just i1, Just i2) -> verify i1 i2
-                        _ -> err "anomaVerifyOp: both arguments are not integers"
-        {-# INLINE anomaVerifyOp #-}
+                        _ -> err "anomaVerifyWithMessageOp: both arguments are not integers"
+        {-# INLINE anomaVerifyWithMessageOp #-}
 
         poseidonHashOp :: [Node] -> Node
         poseidonHashOp = unary $ \arg ->
@@ -482,8 +490,8 @@ geval opts herr ctx env0 = eval' env0
           let !signedMessage = decodeByteString signedMessageInt
               !publicKey = publicKeyFromInteger publicKeyInt
            in if
-                  | E.verify publicKey signedMessage -> deserializeNode (E.removeSignature signedMessage)
-                  | otherwise -> err "signature verification failed"
+                  | E.verify publicKey signedMessage -> nodeMaybeJust (deserializeNode (E.removeSignature signedMessage))
+                  | otherwise -> nodeMaybeNothing
         {-# INLINE verify #-}
 
         signDetached :: Node -> Integer -> Node
@@ -530,6 +538,26 @@ geval opts herr ctx env0 = eval' env0
           | otherwise = TagFalse
     {-# INLINE nodeFromBool #-}
 
+    mkBuiltinConstructor :: BuiltinConstructor -> [Node] -> Maybe Node
+    mkBuiltinConstructor ctor args =
+      (\tag -> mkConstr' tag args)
+        . (^. constructorTag)
+        <$> lookupTabBuiltinConstructor tab ctor
+
+    nodeMaybeNothing :: Node
+    nodeMaybeNothing =
+      fromMaybe
+        (evalErrorMsg' "builtin Maybe is not available")
+        (mkBuiltinConstructor BuiltinMaybeNothing [])
+    {-# INLINE nodeMaybeNothing #-}
+
+    nodeMaybeJust :: Node -> Node
+    nodeMaybeJust n =
+      fromMaybe
+        (evalErrorMsg' "builtin Maybe is not available")
+        (mkBuiltinConstructor BuiltinMaybeJust [n])
+    {-# INLINE nodeMaybeJust #-}
+
     integerFromNode :: Node -> Maybe Integer
     integerFromNode = \case
       NCst (Constant _ (ConstInteger int)) -> Just int
@@ -613,15 +641,15 @@ geval opts herr ctx env0 = eval' env0
           mkCase i sym b (map (substEnvInBranch env) bs) (fmap (substEnv env) def)
 
 -- Evaluate `node` and interpret the builtin IO actions.
-hEvalIO' :: EvalOptions -> Handle -> Handle -> Handle -> IdentContext -> Env -> Node -> IO Node
-hEvalIO' opts herr hin hout ctx env node =
-  let node' = geval opts herr ctx env node
+hEvalIO' :: EvalOptions -> Handle -> Handle -> Handle -> InfoTable -> Env -> Node -> IO Node
+hEvalIO' opts herr hin hout tab env node =
+  let node' = geval opts herr tab env node
    in case node' of
         NCtr (Constr _ (BuiltinTag TagReturn) [x]) ->
           return x
         NCtr (Constr _ (BuiltinTag TagBind) [x, f]) -> do
-          x' <- hEvalIO' opts herr hin hout ctx env x
-          hEvalIO' opts herr hin hout ctx env (mkApp Info.empty f x')
+          x' <- hEvalIO' opts herr hin hout tab env x
+          hEvalIO' opts herr hin hout tab env (mkApp Info.empty f x')
         NCtr (Constr _ (BuiltinTag TagWrite) [NCst (Constant _ (ConstString s))]) -> do
           hPutStr hout s
           return unitNode
@@ -636,12 +664,6 @@ hEvalIO' opts herr hin hout ctx env node =
   where
     unitNode = mkConstr (Info.singleton (NoDisplayInfo ())) (BuiltinTag TagTrue) []
 
-hEvalIO :: Handle -> Handle -> Handle -> IdentContext -> Env -> Node -> IO Node
-hEvalIO = hEvalIO' defaultEvalOptions
-
-evalIO :: IdentContext -> Env -> Node -> IO Node
-evalIO = hEvalIO stderr stdin stdout
-
 doEval ::
   forall r.
   (MonadIO (Sem r)) =>
@@ -652,8 +674,8 @@ doEval ::
   Node ->
   Sem r (Either CoreError Node)
 doEval mfsize noIO loc tab node
-  | noIO = catchEvalError loc (eval stderr (tab ^. identContext) [] node)
-  | otherwise = liftIO (catchEvalErrorIO loc (hEvalIO' opts stderr stdin stdout (tab ^. identContext) [] node))
+  | noIO = catchEvalError loc (eval stderr tab [] node)
+  | otherwise = liftIO (catchEvalErrorIO loc (hEvalIO' opts stderr stdin stdout tab [] node))
   where
     opts =
       maybe

src/Juvix/Compiler/Core/Extra/Utils.hs

@@ -429,7 +429,7 @@ builtinOpArgTypes = \case
   OpAnomaVerifyDetached -> [mkDynamic', mkDynamic', mkDynamic']
   OpAnomaSign -> [mkDynamic', mkDynamic']
   OpAnomaSignDetached -> [mkDynamic', mkDynamic']
-  OpAnomaVerify -> [mkDynamic', mkDynamic']
+  OpAnomaVerifyWithMessage -> [mkDynamic', mkDynamic']
   OpPoseidonHash -> [mkDynamic']
   OpEc -> [mkDynamic', mkTypeField', mkDynamic']
   OpRandomEcPoint -> []

src/Juvix/Compiler/Core/Keywords.hs

@@ -12,8 +12,8 @@ import Juvix.Data.Keyword.All
     kwAnomaEncode,
     kwAnomaSign,
     kwAnomaSignDetached,
-    kwAnomaVerify,
     kwAnomaVerifyDetached,
+    kwAnomaVerifyWithMessage,
     kwAny,
     kwAssign,
     kwBind,

src/Juvix/Compiler/Core/Language/Builtins.hs

@@ -32,7 +32,7 @@ data BuiltinOp
   | OpAnomaVerifyDetached
   | OpAnomaSign
   | OpAnomaSignDetached
-  | OpAnomaVerify
+  | OpAnomaVerifyWithMessage
   | OpPoseidonHash
   | OpEc
   | OpRandomEcPoint
@@ -86,7 +86,7 @@ builtinOpArgsNum = \case
   OpAnomaVerifyDetached -> 3
   OpAnomaSign -> 2
   OpAnomaSignDetached -> 2
-  OpAnomaVerify -> 2
+  OpAnomaVerifyWithMessage -> 2
   OpPoseidonHash -> 1
   OpEc -> 3
   OpRandomEcPoint -> 0
@@ -129,7 +129,7 @@ builtinIsFoldable = \case
   OpAnomaVerifyDetached -> False
   OpAnomaSign -> False
   OpAnomaSignDetached -> False
-  OpAnomaVerify -> False
+  OpAnomaVerifyWithMessage -> False
   OpPoseidonHash -> False
   OpEc -> False
   OpRandomEcPoint -> False
@@ -153,6 +153,6 @@ builtinsAnoma =
     OpAnomaDecode,
     OpAnomaVerifyDetached,
     OpAnomaSign,
-    OpAnomaVerify,
+    OpAnomaVerifyWithMessage,
     OpAnomaSignDetached
   ]

src/Juvix/Compiler/Core/Normalizer.hs

@@ -29,7 +29,7 @@ normalize fsize md = run . evalInfoTableBuilder md . runReader normEnv . normali
           _normEnvLevel = 0,
           _normEnvEvalEnv = []
         }
-    identCtx = computeCombinedIdentContext md
+    tab = computeCombinedInfoTable md
 
     normalize' :: Node -> Norm Node
     normalize' node0 = do
@@ -39,7 +39,7 @@ normalize fsize md = run . evalInfoTableBuilder md . runReader normEnv . normali
     neval :: Node -> Norm Node
     neval node = do
       env <- asks (^. normEnvEvalEnv)
-      return $ geval opts stdout identCtx env node
+      return $ geval opts stdout tab env node
       where
         opts =
           defaultEvalOptions

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

@@ -58,7 +58,7 @@ instance PrettyCode BuiltinOp where
     OpAnomaVerifyDetached -> return primAnomaVerifyDetached
     OpAnomaSign -> return primAnomaSign
     OpAnomaSignDetached -> return primAnomaSignDetached
-    OpAnomaVerify -> return primAnomaVerify
+    OpAnomaVerifyWithMessage -> return primAnomaVerifyWithMessage
     OpPoseidonHash -> return primPoseidonHash
     OpEc -> return primEc
     OpRandomEcPoint -> return primRandomEcPoint
@@ -819,8 +819,8 @@ primAnomaSign = primitive Str.anomaSign
 primAnomaSignDetached :: Doc Ann
 primAnomaSignDetached = primitive Str.anomaSignDetached
 
-primAnomaVerify :: Doc Ann
-primAnomaVerify = primitive Str.anomaVerify
+primAnomaVerifyWithMessage :: Doc Ann
+primAnomaVerifyWithMessage = primitive Str.anomaVerifyWithMessage
 
 primPoseidonHash :: Doc Ann
 primPoseidonHash = primitive Str.cairoPoseidon

src/Juvix/Compiler/Core/Transformation/ComputeTypeInfo.hs

@@ -72,7 +72,7 @@ computeNodeTypeInfo md = umapL go
           OpAnomaVerifyDetached -> Info.getNodeType node
           OpAnomaSign -> Info.getNodeType node
           OpAnomaSignDetached -> Info.getNodeType node
-          OpAnomaVerify -> Info.getNodeType node
+          OpAnomaVerifyWithMessage -> Info.getNodeType node
           OpPoseidonHash -> case _builtinAppArgs of
             [arg] -> Info.getNodeType arg
             _ -> error "incorrect poseidon builtin application"

src/Juvix/Compiler/Core/Transformation/Optimize/ConstantFolding.hs

@@ -53,7 +53,7 @@ convertNode opts nonRecSyms tab md = umap go
       _ -> isType' node
 
     doEval' :: Node -> Node
-    doEval' = removeClosures . geval eopts stderr (tab ^. identContext) []
+    doEval' = removeClosures . geval eopts stderr tab []
       where
         eopts =
           defaultEvalOptions

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

@@ -591,7 +591,7 @@ goAxiomInductive a = whenJust (a ^. Internal.axiomBuiltin) builtinInductive
       Internal.BuiltinAnomaVerifyDetached -> return ()
       Internal.BuiltinAnomaSign -> return ()
       Internal.BuiltinAnomaSignDetached -> return ()
-      Internal.BuiltinAnomaVerify -> return ()
+      Internal.BuiltinAnomaVerifyWithMessage -> return ()
       Internal.BuiltinPoseidon -> return ()
       Internal.BuiltinEcOp -> return ()
       Internal.BuiltinRandomEcPoint -> return ()
@@ -767,7 +767,7 @@ goAxiomDef a = maybe goAxiomNotBuiltin builtinBody (a ^. Internal.axiomBuiltin)
                   )
               )
           )
-      Internal.BuiltinAnomaVerify -> do
+      Internal.BuiltinAnomaVerifyWithMessage -> do
         natType <- getNatType
         registerAxiomDef
           ( mkLambda'
@@ -776,7 +776,7 @@ goAxiomDef a = maybe goAxiomNotBuiltin builtinBody (a ^. Internal.axiomBuiltin)
                   natType
                   ( mkLambda'
                       natType
-                      (mkBuiltinApp' OpAnomaVerify [mkVar' 1, mkVar' 0])
+                      (mkBuiltinApp' OpAnomaVerifyWithMessage [mkVar' 1, mkVar' 0])
                   )
               )
           )
@@ -1189,7 +1189,7 @@ goApplication a = do
         Just Internal.BuiltinAnomaVerifyDetached -> app
         Just Internal.BuiltinAnomaSign -> app
         Just Internal.BuiltinAnomaSignDetached -> app
-        Just Internal.BuiltinAnomaVerify -> app
+        Just Internal.BuiltinAnomaVerifyWithMessage -> app
         Just Internal.BuiltinPoseidon -> app
         Just Internal.BuiltinEcOp -> app
         Just Internal.BuiltinRandomEcPoint -> app

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

@@ -78,6 +78,7 @@ parseToplevel = do
   lift declareIOBuiltins
   lift declareBoolBuiltins
   lift declareNatBuiltins
+  lift declareMaybeBuiltins
   space
   P.endBy statement (kw delimSemicolon)
   r <- optional expression
@@ -576,7 +577,7 @@ builtinAppExpr varsNum vars = do
       <|> (kw kwAnomaEncode $> OpAnomaEncode)
       <|> (kw kwAnomaDecode $> OpAnomaDecode)
       <|> (kw kwAnomaSign $> OpAnomaSign)
-      <|> (kw kwAnomaVerify $> OpAnomaVerify)
+      <|> (kw kwAnomaVerifyWithMessage $> OpAnomaVerifyWithMessage)
       <|> (kw kwAnomaSignDetached $> OpAnomaSignDetached)
       <|> (kw kwAnomaVerifyDetached $> OpAnomaVerifyDetached)
   args <- P.many (atom varsNum vars)

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

@@ -103,7 +103,7 @@ fromCore fsize tab =
         BuiltinAnomaVerifyDetached -> False
         BuiltinAnomaSign -> False
         BuiltinAnomaSignDetached -> False
-        BuiltinAnomaVerify -> False
+        BuiltinAnomaVerifyWithMessage -> False
         BuiltinPoseidon -> False
         BuiltinEcOp -> False
         BuiltinRandomEcPoint -> False