From c938a665ca9c164671f3bf063a313bd883c25d4e Mon Sep 17 00:00:00 2001
From: Paul Cadman <git@paulcadman.dev>
Date: Fri, 22 Mar 2024 16:54:32 +0000
Subject: [PATCH] Parse nockma functionsPlaceholder atom

---
 src/Juvix/Compiler/Nockma/Pretty/Base.hs               | 10 +++++-----
 .../Compiler/Nockma/Translation/FromSource/Base.hs     |  4 ++++
 src/Juvix/Extra/Strings.hs                             |  3 +++
 3 files changed, 12 insertions(+), 5 deletions(-)

diff --git a/src/Juvix/Compiler/Nockma/Pretty/Base.hs b/src/Juvix/Compiler/Nockma/Pretty/Base.hs
index 9384b7269b..0eb8915156 100644
--- a/src/Juvix/Compiler/Nockma/Pretty/Base.hs
+++ b/src/Juvix/Compiler/Nockma/Pretty/Base.hs
@@ -37,12 +37,12 @@ instance (PrettyCode a, NockNatural a) => PrettyCode (Atom a) where
           AtomHintOp -> nockOp atm >>= ppCode
           AtomHintPath -> nockPath atm >>= ppCode
           AtomHintBool
-            | nockmaEq atm nockTrue -> return (annotate (AnnKind KNameInductive) "true")
-            | nockmaEq atm nockFalse -> return (annotate (AnnKind KNameAxiom) "false")
+            | nockmaEq atm nockTrue -> return (annotate (AnnKind KNameInductive) Str.true_)
+            | nockmaEq atm nockFalse -> return (annotate (AnnKind KNameAxiom) Str.false_)
             | otherwise -> fail
-          AtomHintNil -> return (annotate (AnnKind KNameConstructor) "nil")
-          AtomHintVoid -> return (annotate (AnnKind KNameAxiom) "void")
-          AtomHintFunctionsPlaceholder -> return (annotate (AnnKind KNameAxiom) "functions_placeholder")
+          AtomHintNil -> return (annotate (AnnKind KNameConstructor) Str.nil)
+          AtomHintVoid -> return (annotate (AnnKind KNameAxiom) Str.void)
+          AtomHintFunctionsPlaceholder -> return (annotate (AnnKind KNameAxiom) Str.functionsPlaceholder)
 
 instance PrettyCode Interval where
   ppCode = return . pretty
diff --git a/src/Juvix/Compiler/Nockma/Translation/FromSource/Base.hs b/src/Juvix/Compiler/Nockma/Translation/FromSource/Base.hs
index fa6a3788fb..4ba2118d74 100644
--- a/src/Juvix/Compiler/Nockma/Translation/FromSource/Base.hs
+++ b/src/Juvix/Compiler/Nockma/Translation/FromSource/Base.hs
@@ -136,6 +136,9 @@ atomNil = symbol Str.nil $> nockNil
 atomVoid :: Parser (Atom Natural)
 atomVoid = symbol Str.void $> nockVoid
 
+atomFunctionsPlaceholder :: Parser (Atom Natural)
+atomFunctionsPlaceholder = symbol Str.functionsPlaceholder $> nockNil
+
 patom :: Parser (Atom Natural)
 patom = do
   mtag <- optional pTag
@@ -145,6 +148,7 @@ patom = do
     <|> atomBool
     <|> atomNil
     <|> atomVoid
+    <|> atomFunctionsPlaceholder
 
 iden :: Parser Text
 iden = lexeme (takeWhile1P (Just "<iden>") (isAscii .&&. not . isWhiteSpace))
diff --git a/src/Juvix/Extra/Strings.hs b/src/Juvix/Extra/Strings.hs
index 8096c611c9..c0fc49bf27 100644
--- a/src/Juvix/Extra/Strings.hs
+++ b/src/Juvix/Extra/Strings.hs
@@ -985,3 +985,6 @@ package = "package"
 
 version :: (IsString s) => s
 version = "version"
+
+functionsPlaceholder :: (IsString s) => s
+functionsPlaceholder = "functions_placeholder"