Give a proper type to literal Strings

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

@@ -620,7 +620,7 @@ goApplication a = do
 
 goLiteral :: Symbol -> LiteralLoc -> Node
 goLiteral intToNat l = case l ^. withLocParam of
-  Internal.LitString s -> mkLambda' (mkLitConst (ConstString s))
+  Internal.LitString s -> mkLitConst (ConstString s)
   Internal.LitInteger i -> mkApp' (mkIdent' intToNat) (mkLitConst (ConstInteger i))
   where
     mkLitConst :: ConstantValue -> Node

src/Juvix/Compiler/Internal/Translation/FromInternal/Analysis/ArityChecking/Checker.hs

@@ -107,7 +107,7 @@ guessArity ::
 guessArity = \case
   ExpressionHole {} -> return ArityUnknown
   ExpressionFunction {} -> return ArityUnit
-  ExpressionLiteral l -> return (arityLiteral l)
+  ExpressionLiteral {} -> return arityLiteral
   ExpressionApplication a -> appHelper a
   ExpressionIden i -> idenHelper i
   ExpressionUniverse {} -> return arityUniverse
@@ -141,16 +141,8 @@ guessArity = \case
         arif :: Sem r Arity
         arif = guessArity f
 
-arityLiteral :: LiteralLoc -> Arity
-arityLiteral (WithLoc _ l) = case l of
-  LitInteger {} -> ArityUnit
-  -- The arity of all strings is assumed to be: {} -> 1
-  LitString {} ->
-    ArityFunction
-      FunctionArity
-        { _functionArityLeft = ParamImplicit,
-          _functionArityRight = ArityUnit
-        }
+arityLiteral :: Arity
+arityLiteral = ArityUnit
 
 arityUniverse :: Arity
 arityUniverse = ArityUnit
@@ -411,7 +403,7 @@ checkExpression hintArity expr = case expr of
       args' :: [(IsImplicit, Expression)] <- case fun of
         ExpressionHole {} -> mapM (secondM (checkExpression ArityUnknown)) args
         ExpressionIden i -> idenArity i >>= helper (getLoc i)
-        ExpressionLiteral l -> helper (getLoc l) (arityLiteral l)
+        ExpressionLiteral l -> helper (getLoc l) arityLiteral
         ExpressionUniverse l -> helper (getLoc l) arityUniverse
         ExpressionSimpleLambda {} -> simplelambda
         ExpressionFunction f ->

src/Juvix/Compiler/Internal/Translation/FromInternal/Analysis/TypeChecking/Checker.hs

@@ -479,39 +479,13 @@ literalType lit@(WithLoc i l) = case l of
         { _typedExpression = ExpressionLiteral lit,
           _typedType = ExpressionIden (IdenInductive nat)
         }
-  LitString {} -> literalMagicType lit
-
--- | Returns {A : Expression} → A
-literalMagicType :: Members '[NameIdGen] r => LiteralLoc -> Sem r TypedExpression
-literalMagicType l = do
-  uid <- freshNameId
-  let strA :: Text
-      strA = "A"
-      typeVar =
-        Name
-          { _nameText = strA,
-            _nameId = uid,
-            _namePretty = strA,
-            _nameKind = KNameLocal,
-            _nameLoc = getLoc l
-          }
-      param =
-        FunctionParameter
-          { _paramName = Just typeVar,
-            _paramImplicit = Implicit,
-            _paramType = smallUniverseE (getLoc l)
-          }
-      type_ =
-        ExpressionFunction
-          Function
-            { _functionLeft = param,
-              _functionRight = ExpressionIden (IdenVar typeVar)
-            }
-  return
-    TypedExpression
-      { _typedType = type_,
-        _typedExpression = ExpressionLiteral l
-      }
+  LitString {} -> do
+    str <- getBuiltinName i BuiltinString
+    return
+      TypedExpression
+        { _typedExpression = ExpressionLiteral lit,
+          _typedType = ExpressionIden (IdenAxiom str)
+        }
 
 inferExpression' ::
   forall r.

tests/positive/FullExamples/MonoSimpleFungibleToken.juvix

@@ -107,7 +107,7 @@ compile + {
 -- Strings
 --------------------------------------------------------------------------------
 
-axiom String : Type;
+builtin string axiom String : Type;
 compile String {
   ghc ↦ "[Char]";
 };

tests/positive/FullExamples/SimpleFungibleTokenImplicit.juvix

@@ -126,7 +126,7 @@ compile + {
 -- Strings
 --------------------------------------------------------------------------------
 
-axiom String : Type;
+builtin string axiom String : Type;
 compile String {
   ghc ↦ "[Char]";
 };

tests/positive/Internal/LiteralString.juvix

@@ -1,10 +1,12 @@
 module LiteralString;
+  builtin string axiom String : Type;
+
   type A :=
     a : A;
 
   type B :=
     b : B;
 
-  f : A;
+  f : String;
   f := "a";
 end;

tests/positive/MiniC/HelloWorld/Input.juvix

@@ -1,6 +1,6 @@
 module Input;
 
-axiom String : Type;
+builtin string axiom String : Type;
 
 compile String {
   c ↦ "char*";

tests/positive/MiniC/HigherOrder/Input.juvix

@@ -4,7 +4,7 @@ module Input;
 -- Strings
 --------------------------------------------------------------------------------
 
-axiom String : Type;
+builtin string axiom String : Type;
 
 compile String {
   c ↦ "char*";

tests/positive/MiniC/Lib/Data/String.juvix

@@ -1,6 +1,6 @@
 module Data.String;
 
-axiom String : Type;
+builtin string axiom String : Type;
 
 compile String {
   ghc ↦ "[Char]";

tests/positive/MiniC/MultiModules/Data/String.juvix

@@ -1,6 +1,6 @@
 module Data.String;
 
-axiom String : Type;
+builtin string axiom String : Type;
 
 compile String {
   ghc ↦ "[Char]";

tests/positive/MiniC/MutuallyRecursive/Data/String.juvix

@@ -1,6 +1,6 @@
 module Data.String;
 
-axiom String : Type;
+builtin string axiom String : Type;
 
 compile String {
   ghc ↦ "[Char]";

tests/positive/MiniC/Nat/Input.juvix

@@ -12,7 +12,7 @@ type Bool :=
 -- Strings
 --------------------------------------------------------------------------------
 
-axiom String : Type;
+builtin string axiom String : Type;
 
 compile String {
   ghc ↦ "[Char]";

tests/positive/MiniC/Polymorphism/Input.juvix

@@ -12,7 +12,7 @@ type Bool :=
 -- Strings
 --------------------------------------------------------------------------------
 
-axiom String : Type;
+builtin string axiom String : Type;
 
 compile String {
   ghc ↦ "[Char]";

tests/positive/MiniC/PolymorphismHoles/Input.juvix

@@ -12,7 +12,7 @@ type Bool :=
 -- Strings
 --------------------------------------------------------------------------------
 
-axiom String : Type;
+builtin string axiom String : Type;
 
 compile String {
   ghc ↦ "[Char]";

tests/positive/MiniC/SimpleFungibleTokenImplicit/Input.juvix

@@ -163,7 +163,7 @@ compile + {
 -- Strings
 --------------------------------------------------------------------------------
 
-axiom String : Type;
+builtin string axiom String : Type;
 compile String {
   c ↦ "char*";
 };