Add support for Strings in the Anoma backend

src/Juvix/Compiler/Core/Transformation/Check/Anoma.hs

@@ -10,4 +10,4 @@ checkAnoma md = do
   checkMainExists md
   checkNoAxioms md
   mapAllNodesM checkNoIO md
-  mapAllNodesM (checkBuiltins' (builtinsString ++ builtinsCairo) [PrimString, PrimField]) md
+  mapAllNodesM (checkBuiltins' ([OpStrToInt, OpShow] ++ builtinsCairo) [PrimField]) md

src/Juvix/Compiler/Nockma/Encoding/ByteString.hs

@@ -6,15 +6,43 @@ import Juvix.Compiler.Nockma.Language
 import Juvix.Prelude.Base
 
 atomToByteString :: (NockNatural a, Member (Error (ErrNockNatural a)) r) => Atom a -> Sem r ByteString
-atomToByteString am = do
-  n <- nockNatural am
-  return (cloneToByteString . integerToVectorBits . toInteger $ n)
+atomToByteString = fmap naturalToByteString . nockNatural
 
 byteStringToAtom :: (NockNatural a, Member (Error (ErrNockNatural a)) r) => ByteString -> Sem r (Atom a)
-byteStringToAtom bs = do
-  a <- fromNatural . fromInteger . vectorBitsToInteger . cloneFromByteString $ bs
-  return
-    Atom
-      { _atomInfo = emptyAtomInfo,
-        _atom = a
-      }
+byteStringToAtom = fmap mkEmptyAtom . fromNatural . byteStringToNatural
+
+byteStringToNatural :: ByteString -> Natural
+byteStringToNatural = bitsToNatural . cloneFromByteString
+
+naturalToByteString :: Natural -> ByteString
+naturalToByteString = cloneToByteString . naturalToBits
+
+textToNatural :: Text -> Natural
+textToNatural = byteStringToNatural . encodeUtf8
+
+bitsToNatural :: Vector Bit -> Natural
+bitsToNatural = fromInteger . vectorBitsToInteger
+
+naturalToBits :: Natural -> Vector Bit
+naturalToBits = integerToVectorBits . toInteger
+
+atomToText :: (NockNatural a, Member (Error (ErrNockNatural a)) r) => Atom a -> Sem r Text
+atomToText = fmap decodeUtf8Lenient . atomToByteString
+
+-- | Construct an atom formed by concatenating the bits of two atoms, where each atom represents a sequence of bytes
+atomConcatenateBytes :: forall a r. (NockNatural a, Member (Error (ErrNockNatural a)) r) => Atom a -> Atom a -> Sem r (Atom a)
+atomConcatenateBytes l r = do
+  -- cloneToByteString ensures that the bytestring is zero-padded up to the byte boundary
+  lBs <- cloneToByteString <$> atomToBits l
+  rBs <- cloneToByteString <$> atomToBits r
+  byteStringToAtom (lBs <> rBs)
+  where
+    atomToBits :: Atom a -> Sem r (Vector Bit)
+    atomToBits = fmap naturalToBits . nockNatural
+
+mkEmptyAtom :: a -> Atom a
+mkEmptyAtom x =
+  Atom
+    { _atomInfo = emptyAtomInfo,
+      _atom = x
+    }

src/Juvix/Compiler/Nockma/Evaluator.hs

@@ -247,7 +247,13 @@ evalProfile inistack initerm =
             StdlibVerify -> case args' of
               TCell (TermAtom signedMessage) (TermAtom pubKey) -> goVerify signedMessage pubKey
               _ -> error "expected a term of the form [signedMessage (atom) public_key (atom)]"
+            StdlibCatBytes -> case args' of
+              TCell (TermAtom arg1) (TermAtom arg2) -> goCat arg1 arg2
+              _ -> error "expected a term with two atoms"
           where
+            goCat :: Atom a -> Atom a -> Sem r (Term a)
+            goCat arg1 arg2 = TermAtom . setAtomHint AtomHintString <$> atomConcatenateBytes arg1 arg2
+
             goVerifyDetached :: Atom a -> Atom a -> Atom a -> Sem r (Term a)
             goVerifyDetached sigT messageT pubKeyT = do
               sig <- Signature <$> atomToByteString sigT

src/Juvix/Compiler/Nockma/Language.hs

@@ -122,6 +122,7 @@ data AtomHint
   | AtomHintNil
   | AtomHintVoid
   | AtomHintFunctionsPlaceholder
+  | AtomHintString
   deriving stock (Show, Eq, Lift, Generic)
 
 instance Hashable AtomHint
@@ -346,6 +347,9 @@ atomHintInfo h =
     { _atomInfoHint = Just h
     }
 
+setAtomHint :: AtomHint -> Atom a -> Atom a
+setAtomHint h = set (atomInfo . atomInfoHint) (Just h)
+
 class IsNock nock where
   toNock :: nock -> Term Natural
 

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

@@ -5,6 +5,7 @@ module Juvix.Compiler.Nockma.Pretty.Base
   )
 where
 
+import Juvix.Compiler.Nockma.Encoding.ByteString (atomToText)
 import Juvix.Compiler.Nockma.Language
 import Juvix.Compiler.Nockma.Pretty.Options
 import Juvix.Data.CodeAnn
@@ -23,7 +24,7 @@ class PrettyCode c where
 runPrettyCode :: (PrettyCode c) => Options -> c -> Doc Ann
 runPrettyCode opts = run . runReader opts . ppCode
 
-instance (PrettyCode a, NockNatural a) => PrettyCode (Atom a) where
+instance forall a. (PrettyCode a, NockNatural a) => PrettyCode (Atom a) where
   ppCode atm = do
     t <- runFail $ do
       failWhenM (asks (^. optIgnoreTags))
@@ -43,6 +44,10 @@ instance (PrettyCode a, NockNatural a) => PrettyCode (Atom a) where
           AtomHintNil -> return (annotate (AnnKind KNameConstructor) Str.nil)
           AtomHintVoid -> return (annotate (AnnKind KNameAxiom) Str.void)
           AtomHintFunctionsPlaceholder -> return (annotate (AnnKind KNameAxiom) Str.functionsPlaceholder)
+          AtomHintString -> atomToText atm >>= ppCode
+
+instance PrettyCode Text where
+  ppCode = return . dquotes . pretty
 
 instance PrettyCode Interval where
   ppCode = return . pretty

src/Juvix/Compiler/Nockma/StdlibFunction.hs

@@ -25,3 +25,10 @@ stdlibPath = \case
   StdlibVerifyDetached -> [nock| [9 22 0 1] |]
   StdlibSign -> [nock| [9 10 0 1] |]
   StdlibVerify -> [nock| [9 4 0 1] |]
+  -- Obtained from the urbit dojo using:
+  --
+  -- =>  anoma  !=(~(cat block 3))
+  --
+  -- The `3` here is because we want to treat each atom as sequences of 2^3
+  -- bits, i.e bytes.
+  StdlibCatBytes -> [nock| [8 [9 10 0 7] 9 4 10 [6 7 [0 3] 1 3] 0 2] |]

src/Juvix/Compiler/Nockma/StdlibFunction/Base.hs

@@ -19,6 +19,7 @@ instance Pretty StdlibFunction where
     StdlibVerifyDetached -> "verify-detached"
     StdlibSign -> "sign"
     StdlibVerify -> "verify"
+    StdlibCatBytes -> "cat"
 
 data StdlibFunction
   = StdlibDec
@@ -35,6 +36,7 @@ data StdlibFunction
   | StdlibVerifyDetached
   | StdlibSign
   | StdlibVerify
+  | StdlibCatBytes
   deriving stock (Show, Lift, Eq, Bounded, Enum, Generic)
 
 instance Hashable StdlibFunction

src/Juvix/Compiler/Nockma/Translation/FromSource/Base.hs

@@ -3,6 +3,7 @@ module Juvix.Compiler.Nockma.Translation.FromSource.Base where
 import Data.HashMap.Internal.Strict qualified as HashMap
 import Data.List.NonEmpty qualified as NonEmpty
 import Data.Text qualified as Text
+import Juvix.Compiler.Nockma.Encoding.ByteString (textToNatural)
 import Juvix.Compiler.Nockma.Language
 import Juvix.Extra.Paths
 import Juvix.Extra.Strings qualified as Str
@@ -63,6 +64,9 @@ lsbracket = void (lexeme "[")
 rsbracket :: Parser ()
 rsbracket = void (lexeme "]")
 
+stringLiteral :: Parser Text
+stringLiteral = lexeme (pack <$> (char '"' >> manyTill L.charLiteral (char '"')))
+
 dottedNatural :: Parser Natural
 dottedNatural = lexeme $ do
   firstDigit <- digit
@@ -139,6 +143,17 @@ atomVoid = symbol Str.void $> nockVoid
 atomFunctionsPlaceholder :: Parser (Atom Natural)
 atomFunctionsPlaceholder = symbol Str.functionsPlaceholder $> nockNil
 
+atomStringLiteral :: Parser (Atom Natural)
+atomStringLiteral = do
+  WithLoc loc s <- withLoc stringLiteral
+  let info =
+        AtomInfo
+          { _atomInfoTag = Nothing,
+            _atomInfoLoc = Irrelevant (Just loc),
+            _atomInfoHint = Just AtomHintString
+          }
+  return (Atom (textToNatural s) info)
+
 patom :: Parser (Atom Natural)
 patom = do
   mtag <- optional pTag
@@ -149,6 +164,7 @@ patom = do
     <|> atomNil
     <|> atomVoid
     <|> atomFunctionsPlaceholder
+    <|> try atomStringLiteral
 
 iden :: Parser Text
 iden = lexeme (takeWhile1P (Just "<iden>") (isAscii .&&. not . isWhiteSpace))

src/Juvix/Compiler/Nockma/Translation/FromTree.hs

@@ -33,6 +33,7 @@ module Juvix.Compiler.Nockma.Translation.FromTree
   )
 where
 
+import Juvix.Compiler.Nockma.Encoding
 import Juvix.Compiler.Nockma.Language.Path
 import Juvix.Compiler.Nockma.Pretty
 import Juvix.Compiler.Nockma.Stdlib
@@ -384,11 +385,19 @@ compile = \case
         | i < 0 -> error "negative integer"
         | otherwise -> nockIntegralLiteral i
       Tree.ConstBool i -> nockBoolLiteral i
-      Tree.ConstString {} -> stringsErr
+      Tree.ConstString t -> OpQuote # goConstString t
       Tree.ConstUnit -> OpQuote # constUnit
       Tree.ConstVoid -> OpQuote # constVoid
       Tree.ConstField {} -> fieldErr
 
+    goConstString :: Text -> Term Natural
+    goConstString t =
+      TermAtom
+        Atom
+          { _atomInfo = atomHintInfo AtomHintString,
+            _atom = textToNatural t
+          }
+
     goSave :: Tree.NodeSave -> Sem r (Term Natural)
     goSave Tree.NodeSave {..} = do
       arg <- compile _nodeSaveArg
@@ -440,8 +449,8 @@ compile = \case
 
     goPrimUnop :: Tree.UnaryOp -> Term Natural -> Term Natural
     goPrimUnop op arg = case op of
-      Tree.OpShow -> stringsErr
-      Tree.OpStrToInt -> stringsErr
+      Tree.OpShow -> stringsErr "show"
+      Tree.OpStrToInt -> stringsErr "strToInt"
       Tree.OpArgsNum ->
         let getF f = getClosureField f arg
          in sub (getF ClosureTotalArgsNum) (getF ClosureArgsNum)
@@ -500,7 +509,7 @@ compile = \case
           Tree.OpIntLt -> return (callStdlib StdlibLt args)
           Tree.OpIntLe -> return (callStdlib StdlibLe args)
           Tree.OpEq -> testEq _nodeBinopArg1 _nodeBinopArg2
-          Tree.OpStrConcat -> stringsErr
+          Tree.OpStrConcat -> return (callStdlib StdlibCatBytes args)
           Tree.OpFieldAdd -> fieldErr
           Tree.OpFieldSub -> fieldErr
           Tree.OpFieldMul -> fieldErr
@@ -718,8 +727,8 @@ goConstructor mr t args = case t of
 unsupported :: Text -> a
 unsupported thing = error ("The Nockma backend does not support " <> thing)
 
-stringsErr :: a
-stringsErr = unsupported "strings"
+stringsErr :: Text -> a
+stringsErr t = unsupported ("strings: " <> t)
 
 fieldErr :: a
 fieldErr = unsupported "the field type"

test/Anoma/Compilation/Positive.hs

@@ -576,5 +576,12 @@ allTests =
             $(mkRelFile "test078.juvix")
             [OpQuote # toSignAndVerify]
             $ checkOutput
-              [toSignAndVerify]
+              [toSignAndVerify],
+      let inputStr :: Term Natural = [nock| "Juvix!" |]
+       in mkAnomaCallTest
+            "Test079: Strings"
+            $(mkRelDir ".")
+            $(mkRelFile "test079.juvix")
+            [OpQuote # inputStr]
+            $ checkOutput [[nock| "Juvix! ✨ héllo world ✨" |]]
     ]

test/Nockma/Eval/Positive.hs

@@ -268,7 +268,8 @@ juvixCallingConventionTests =
                res :: Term Natural = foldTerms (toNock <$> r)
                lenR :: Term Natural = nockIntegralLiteral (length r)
                tupR = OpQuote # foldTerms (toNock <$> r)
-            in compilerTest "appendToTuple (left empty, right-nonempty)" (appendToTuple (OpQuote # nockNilTagged "test-appendtotuple") (nockNatLiteral 0) tupR lenR) (eqNock res)
+            in compilerTest "appendToTuple (left empty, right-nonempty)" (appendToTuple (OpQuote # nockNilTagged "test-appendtotuple") (nockNatLiteral 0) tupR lenR) (eqNock res),
+           compilerTest "stdlib cat" (callStdlib StdlibCatBytes [nockNatLiteral 2, nockNatLiteral 1]) (eqNock [nock| 258 |])
          ]
 
 unitTests :: [Test]

tests/Anoma/Compilation/negative/String.juvix

@@ -2,4 +2,4 @@ module String;
 
 import Stdlib.Prelude open;
 
-main : String := "boom";
+main : String := intToString 1;

tests/Anoma/Compilation/positive/test079.juvix

@@ -0,0 +1,6 @@
+module test079;
+
+import Stdlib.Prelude open;
+
+main (s : String) : String :=
+  s ++str " " ++str "✨ héllo" ++str " " ++str "world ✨";