add integer and string literals

assets/source-ayu-light.css

@@ -1,30 +1,34 @@
 /* Color palette based on https://github.com/ayu-theme/ayu-colors */
 body {
-	  background-color: #f8f9fa;
+    background-color: #f8f9fa;
 }
 
 .ju-inductive {
-	  color: #86b300;
+    color: #86b300;
 }
 
 .ju-constructor {
-	  color: #a37acc;
+    color: #a37acc;
 }
 
 .ju-function {
-	  color: #f2ae49;
+    color: #f2ae49;
 }
 
 .ju-axiom {
-	  color: #f07171;
+    color: #f07171;
+}
+
+.ju-string {
+    color: #f07171;
 }
 
 .ju-keyword {
-	  color: #399ee6;
+    color: #399ee6;
 }
 
 .ju-delimiter {
-	  color: #787b80;
+    color: #787b80;
 }
 
 .ju-var {
@@ -36,9 +40,9 @@ body {
 }
 
 a:hover, a.hover-highlight {
-	  background-color: #dadbdc ;
+    background-color: #dadbdc ;
 }
 
 a:link, a:visited {
-	  text-decoration: none;
+    text-decoration: none;
 }

assets/source-nord.css

@@ -1,30 +1,34 @@
 /* Color palette based on https://www.nordtheme.com/ */
 body {
-	  background-color: #2e3440;
+    background-color: #2e3440;
 }
 
 .ju-inductive {
-	  color: #a3be8c;
+    color: #a3be8c;
 }
 
 .ju-constructor {
-	  color: #b48ead;
+    color: #b48ead;
 }
 
 .ju-function {
-	  color: #ebcb8b;
+    color: #ebcb8b;
 }
 
 .ju-axiom {
-	  color: #bf616a;
+    color: #bf616a;
+}
+
+.ju-string {
+    color: #bf616a;
 }
 
 .ju-keyword {
-	  color: #81a1c1;
+    color: #81a1c1;
 }
 
 .ju-delimiter {
-	  color: #5e81ac;
+    color: #5e81ac;
 }
 
 .ju-var {
@@ -36,9 +40,9 @@ body {
 }
 
 a:link, a:visited {
-	text-decoration: none;
+  text-decoration: none;
 }
 
 a:hover, a.hover-highlight {
-	background-color: #4c566a;
+  background-color: #4c566a;
 }

src/MiniJuvix/Syntax/Abstract/Pretty/Ann.hs

@@ -9,6 +9,8 @@ data Ann =
   AnnKind S.NameKind
   | AnnKeyword
   | AnnImportant
+  | AnnLiteralString
+  | AnnLiteralInteger
 
 fromScopedAnn :: S.Ann -> Maybe Ann
 fromScopedAnn s = case s of
@@ -16,6 +18,7 @@ fromScopedAnn s = case s of
   S.AnnKeyword -> Nothing
   S.AnnDelimiter -> Nothing
   S.AnnUnkindedSym -> Nothing
-  S.AnnNumber -> Nothing
   S.AnnDef {} -> Nothing
   S.AnnRef {} -> Nothing
+  S.AnnLiteralString -> Just AnnLiteralInteger
+  S.AnnLiteralInteger -> Just AnnLiteralString

src/MiniJuvix/Syntax/Abstract/Pretty/Ansi.hs

@@ -37,3 +37,5 @@ stylize a = case a of
     KNameTopModule -> mempty
   AnnKeyword -> colorDull Blue
   AnnImportant -> bold
+  AnnLiteralString -> colorDull Red
+  AnnLiteralInteger -> colorDull Cyan

src/MiniJuvix/Syntax/Concrete/Language.hs

@@ -463,6 +463,7 @@ data Expression
   | ExpressionMatch (Match 'Scoped)
   | ExpressionLetBlock (LetBlock 'Scoped)
   | ExpressionUniverse Universe
+  | ExpressionLiteral Literal
   | ExpressionFunction (Function 'Scoped)
   deriving stock (Show, Eq, Ord)
 
@@ -474,15 +475,21 @@ instance HasAtomicity Expression where
     ExpressionInfixApplication a -> Aggregate (getFixity a)
     ExpressionPostfixApplication a -> Aggregate (getFixity a)
     ExpressionLambda {} -> Atom
+    ExpressionLiteral {} -> Atom
     ExpressionMatch {} -> Atom
     ExpressionLetBlock {} -> Atom
     ExpressionUniverse {} -> Atom
     ExpressionFunction {} -> Aggregate funFixity
 
 --------------------------------------------------------------------------------
--- Expression section
+-- Expression atom
 --------------------------------------------------------------------------------
 
+data Literal =
+  LitString Text
+  | LitInteger Integer
+  deriving stock (Show, Eq, Ord)
+
 -- | Expressions without application
 data ExpressionAtom (s :: Stage)
   = AtomIdentifier (NameType s)
@@ -492,6 +499,7 @@ data ExpressionAtom (s :: Stage)
   | AtomFunction (Function s)
   | AtomFunArrow
   | AtomMatch (Match s)
+  | AtomLiteral Literal
   | AtomParens (ExpressionType s)
 
 deriving stock instance

src/MiniJuvix/Syntax/Concrete/Lexer.hs

@@ -9,6 +9,7 @@ import MiniJuvix.Prelude
 import qualified Text.Megaparsec.Char.Lexer as L
 import MiniJuvix.Syntax.Concrete.Loc
 import qualified MiniJuvix.Internal.Strings as Str
+import qualified Data.Text as Text
 
 --------------------------------------------------------------------------------
 
@@ -38,6 +39,17 @@ identifierL = lexeme bareIdentifier
 fromPos :: P.Pos -> Pos
 fromPos = Pos . fromIntegral . P.unPos
 
+integer :: MonadParsec e Text m => m Integer
+integer = do
+  minus <- optional (char '-')
+  nat <- lexeme L.decimal
+  case minus of
+    Nothing -> return nat
+    _ -> return (- nat)
+
+string :: MonadParsec e Text m => m Text
+string = pack <$> (char '"' >> manyTill L.charLiteral (char '"'))
+
 mkLoc :: SourcePos -> Loc
 mkLoc SourcePos {..} = Loc {..}
   where
@@ -61,15 +73,22 @@ interval ma = do
   return (res, mkInterval start end)
 
 -- | Same as @identifier@ but does not consume space after it.
+-- TODO: revise.
 bareIdentifier :: MonadParsec e Text m => m (Text, Interval)
 bareIdentifier = interval $ do
   notFollowedBy (choice allKeywords)
-  P.takeWhile1P Nothing validChar
+  h <- P.satisfy validFirstChar
+  t <- P.takeWhileP Nothing validChar
+  return (Text.cons h t)
   where
     validChar :: Char -> Bool
     validChar c =
+      isAlphaNum c || validFirstChar c
+    validFirstChar :: Char -> Bool
+    validFirstChar c =
+      c /= '-' &&
       or
-        [ isAlphaNum c,
+        [ isLetter c,
           cat == MathSymbol,
           cat == CurrencySymbol,
           cat == ModifierLetter,

src/MiniJuvix/Syntax/Concrete/Parser.hs

@@ -123,7 +123,8 @@ import_ = do
 expressionAtom :: MonadParsec e Text m => m (ExpressionAtom 'Parsed)
 expressionAtom =
   do
-    AtomIdentifier <$> name
+     AtomLiteral <$> literal
+    <|> AtomIdentifier <$> name
     <|> (AtomUniverse <$> universe)
     <|> (AtomLambda <$> lambda)
     <|> (AtomFunction <$> function)
@@ -135,6 +136,15 @@ expressionAtom =
 expressionAtoms :: MonadParsec e Text m => m (ExpressionAtoms 'Parsed)
 expressionAtoms = ExpressionAtoms <$> P.some expressionAtom
 
+--------------------------------------------------------------------------------
+-- Literals
+--------------------------------------------------------------------------------
+
+literal :: MonadParsec e Text m => m Literal
+literal =
+      LitInteger <$> integer
+  <|> LitString <$> string
+
 --------------------------------------------------------------------------------
 -- Match expression
 --------------------------------------------------------------------------------

src/MiniJuvix/Syntax/Concrete/Scoped/Pretty/Ann.hs

@@ -7,7 +7,8 @@ data Ann
   = AnnKind S.NameKind
   | AnnKeyword
   | AnnDelimiter
+  | AnnLiteralString
+  | AnnLiteralInteger
   | AnnUnkindedSym
-  | AnnNumber
   | AnnDef TopModulePath S.NameId
   | AnnRef TopModulePath S.NameId

src/MiniJuvix/Syntax/Concrete/Scoped/Pretty/Ansi.hs

@@ -36,5 +36,6 @@ stylize a = case a of
   AnnKeyword -> colorDull Blue
   AnnDef {} -> mempty
   AnnRef {} -> mempty
-  AnnNumber -> mempty
+  AnnLiteralString -> colorDull Red
+  AnnLiteralInteger -> colorDull Cyan
   AnnUnkindedSym -> mempty

src/MiniJuvix/Syntax/Concrete/Scoped/Pretty/Base.hs

@@ -142,6 +142,9 @@ kwParenL = delimiter "("
 kwParenR :: Doc Ann
 kwParenR = delimiter ")"
 
+kwDQuote :: Doc Ann
+kwDQuote = pretty ("\"" :: Text)
+
 kwDot :: Doc Ann
 kwDot = delimiter "."
 
@@ -161,6 +164,9 @@ braces = enclose kwBraceL kwBraceR
 parens :: Doc Ann -> Doc Ann
 parens = enclose kwParenL kwParenR
 
+doubleQuotes :: Doc Ann -> Doc Ann
+doubleQuotes = enclose kwDQuote kwDQuote
+
 ppModulePathType :: forall t s r. (SingI t, SingI s, Members '[Reader Options] r) =>
   ModulePathType s t -> Sem r (Doc Ann)
 ppModulePathType x = case sing :: SStage s of
@@ -305,7 +311,7 @@ instance (SingI s, SingI t) => PrettyCode (Module s t) where
           SModuleTop -> Just kwSemicolon
 
 instance PrettyCode Precedence where
-  ppCode p = return $ annotate AnnNumber $ case p of
+  ppCode p = return $ case p of
     PrecMinusOmega -> pretty ("-ω" :: Text)
     PrecNat n -> pretty n
     PrecOmega -> pretty ("ω" :: Text)
@@ -599,6 +605,11 @@ instance PrettyCode Application where
     r' <- ppRightExpression appFixity r
     return $ l' <+> r'
 
+instance PrettyCode Literal where
+  ppCode l = case l of
+    LitInteger n -> return $ annotate AnnLiteralInteger (pretty n)
+    LitString s -> return $ annotate AnnLiteralString (doubleQuotes (pretty s))
+
 instance PrettyCode Expression where
   ppCode e = case e of
     ExpressionIdentifier n -> ppCode n
@@ -610,6 +621,7 @@ instance PrettyCode Expression where
     ExpressionMatch m -> ppCode m
     ExpressionLetBlock lb -> ppCode lb
     ExpressionUniverse u -> ppCode u
+    ExpressionLiteral l -> ppCode l
     ExpressionFunction f -> ppCode f
 
 instance PrettyCode Pattern where
@@ -673,6 +685,7 @@ instance SingI s => PrettyCode (ExpressionAtom s) where
     AtomLetBlock lb -> ppCode lb
     AtomUniverse uni -> ppCode uni
     AtomFunction fun -> ppCode fun
+    AtomLiteral lit -> ppCode lit
     AtomFunArrow -> return kwArrowR
     AtomMatch m -> ppCode m
     AtomParens e -> parens <$> ppExpression e

src/MiniJuvix/Syntax/Concrete/Scoped/Pretty/Html.hs

@@ -104,7 +104,8 @@ fromText = fromString . unpack
 putTag :: Ann -> Html -> Html
 putTag ann x = case ann of
    AnnKind k -> tagKind k x
-   AnnNumber -> Html.span ! Attr.class_ "ju-number" $ x
+   AnnLiteralInteger -> Html.span ! Attr.class_ "ju-number" $ x
+   AnnLiteralString -> Html.span ! Attr.class_ "ju-string" $ x
    AnnKeyword -> Html.span ! Attr.class_ "ju-keyword" $ x
    AnnUnkindedSym -> Html.span ! Attr.class_ "ju-var" $ x
    AnnDelimiter -> Html.span ! Attr.class_ "ju-delimiter" $ x

src/MiniJuvix/Syntax/Concrete/Scoped/Scoper.hs

@@ -918,6 +918,7 @@ checkExpressionAtom e = case e of
   AtomFunction fun -> AtomFunction <$> checkFunction fun
   AtomParens par -> AtomParens <$> checkParens par
   AtomFunArrow -> return AtomFunArrow
+  AtomLiteral l -> return (AtomLiteral l)
   AtomMatch match -> AtomMatch <$> checkMatch match
 
 checkParens :: Members '[Error ScopeError, State Scope, State ScoperState, Reader LocalVars] r =>
@@ -1090,7 +1091,7 @@ mkExpressionParser table = embed @Parse pExpression
     pExpression :: Parse Expression
     pExpression = P.makeExprParser (runM parseTerm) table
 
-parseTerm :: forall r. Members '[Embed Parse] r => Sem r Expression
+parseTerm :: Members '[Embed Parse] r => Sem r Expression
 parseTerm =
   embed @Parse $
     parseUniverse
@@ -1098,9 +1099,18 @@ parseTerm =
       <|> parseParens
       <|> parseFunction
       <|> parseLambda
+      <|> parseLiteral
       <|> parseMatch
       <|> parseLetBlock
   where
+    parseLiteral :: Parse Expression
+    parseLiteral = ExpressionLiteral <$> P.token lit mempty
+       where
+        lit :: ExpressionAtom 'Scoped -> Maybe Literal
+        lit s = case s of
+          AtomLiteral l -> Just l
+          _ -> Nothing
+
     parseLambda :: Parse Expression
     parseLambda = ExpressionLambda <$> P.token lambda mempty
       where

src/MiniJuvix/Syntax/MiniHaskell/Language.hs

@@ -63,8 +63,8 @@ data Expression
   | ExpressionApplication Application
 
 data Application = Application {
-  _appFunction :: FunctionName,
-  _appArguments :: [Expression]
+  _appLeft :: Expression,
+  _appRight :: Expression
   }
 
 data Function = Function {

test/Scope/Positive.hs

@@ -68,4 +68,6 @@ tests = [
      "StdlibList" "Data/List.mjuvix"
   , PosTest "Operators (+)"
      "." "Operators.mjuvix"
+  , PosTest "Literals"
+     "." "Literals.mjuvix"
  ]

tests/positive/Literals.mjuvix

@@ -0,0 +1,12 @@
+module Literals;
+  axiom Int : Type;
+  axiom String : Type;
+  a : Int;
+  a := 12313;
+
+  b : Int;
+  b := -008;
+
+  c : String;
+  c := "hellooooo";
+end;