Parse nockma functionsPlaceholder atom

anoma · Mar 22, 2024 · c938a66 · c938a66
1 parent a693f45
commit c938a66
Show file tree

Hide file tree

Showing 3 changed files with 12 additions and 5 deletions.
diff --git 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
@@ -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
@@ -985,3 +985,6 @@ package = "package"
 
 version :: (IsString s) => s
 version = "version"
+
+functionsPlaceholder :: (IsString s) => s
+functionsPlaceholder = "functions_placeholder"