Strings support

granule-compiler.cabal

@@ -30,9 +30,11 @@ library
       Language.Granule.Codegen.MarkGlobals
   other-modules:
       Language.Granule.Codegen.Builtins.Builtins
+      Language.Granule.Codegen.Builtins.Char
       Language.Granule.Codegen.Builtins.Extras
       Language.Granule.Codegen.Builtins.FloatArray
       Language.Granule.Codegen.Builtins.Shared
+      Language.Granule.Codegen.Builtins.String
       Language.Granule.Codegen.Emit.EmitableDef
       Language.Granule.Codegen.Emit.EmitBuiltins
       Language.Granule.Codegen.Emit.EmitterState

src/Language/Granule/Codegen/Builtins/Builtins.hs

@@ -1,13 +1,19 @@
 module Language.Granule.Codegen.Builtins.Builtins where
 
+import Language.Granule.Codegen.Builtins.Char
 import Language.Granule.Codegen.Builtins.Extras
 import Language.Granule.Codegen.Builtins.FloatArray
 import Language.Granule.Codegen.Builtins.Shared
+import Language.Granule.Codegen.Builtins.String
 import Language.Granule.Syntax.Identifiers (Id, mkId)
 
 builtins :: [Builtin]
 builtins =
   [ charToIntDef,
+    charFromIntDef,
+    stringAppendDef,
+    stringConsDef,
+    stringSnocDef,
     divDef,
     newFloatArrayIDef,
     readFloatArrayIDef,

src/Language/Granule/Codegen/Builtins/Char.hs

@@ -0,0 +1,17 @@
+{-# OPTIONS_GHC -Wno-incomplete-patterns #-}
+
+module Language.Granule.Codegen.Builtins.Char where
+
+import LLVM.AST.Type (i32, i8)
+import LLVM.IRBuilder.Instruction (trunc, zext)
+import Language.Granule.Codegen.Builtins.Shared
+
+charToIntDef, charFromIntDef :: Builtin
+charToIntDef =
+  Builtin "charToInt" [tyChar] tyInt impl
+  where
+    impl [x] = zext x i32
+charFromIntDef =
+  Builtin "charFromInt" [tyInt] tyChar impl
+  where
+    impl [x] = trunc x i8

src/Language/Granule/Codegen/Builtins/Extras.hs

@@ -2,21 +2,11 @@
 
 module Language.Granule.Codegen.Builtins.Extras where
 
-import LLVM.AST.Type as IR
 import LLVM.IRBuilder.Instruction
 import Language.Granule.Codegen.Builtins.Shared
 import Language.Granule.Syntax.Identifiers
 import Language.Granule.Syntax.Type as Gr
 
--- charToInt :: Char -> Int
-charToIntDef :: Builtin
-charToIntDef =
-    Builtin "charToInt" args ret impl
-    where
-        args = [TyCon (Id "Char" "Char")]
-        ret = TyCon (Id "Int" "Int")
-        impl [x] = zext x i32
-
 -- div :: Int -> Int -> Int
 divDef :: Builtin
 divDef =

src/Language/Granule/Codegen/Builtins/Shared.hs

@@ -99,6 +99,9 @@ tyChar = TyCon (Id "Char" "Char")
 tyUnit :: Gr.Type
 tyUnit = TyCon (Id "()" "()")
 
+tyString :: Gr.Type
+tyString = TyCon (Id "String" "String")
+
 tyPair :: (Gr.Type, Gr.Type) -> Gr.Type
 tyPair (l, r) = TyApp (TyApp (TyCon (Id "," ",")) l) r
 

src/Language/Granule/Codegen/Builtins/String.hs

@@ -0,0 +1,64 @@
+{-# OPTIONS_GHC -Wno-incomplete-patterns #-}
+
+module Language.Granule.Codegen.Builtins.String where
+
+import LLVM.AST
+import LLVM.AST.Type as IR
+import LLVM.IRBuilder.Constant as C
+import LLVM.IRBuilder.Instruction
+import LLVM.IRBuilder.Module (MonadModuleBuilder)
+import LLVM.IRBuilder.Monad (MonadIRBuilder)
+import Language.Granule.Codegen.Builtins.Shared
+
+stringAppendDef, stringConsDef, stringSnocDef :: Builtin
+stringAppendDef =
+  Builtin "stringAppend" [tyString, tyString] tyString impl
+  where
+    impl [strPtrA, strPtrB] = do
+      (lenA, dataPtrA) <- readString strPtrA
+      (lenB, dataPtrB) <- readString strPtrB
+
+      len <- add lenA lenB
+      dataPtr <- allocate len i8
+
+      -- copy x into new arr
+      _ <- copy dataPtr dataPtrA lenA
+
+      -- offset pointer to end of string A
+      nextPos <- gep dataPtr [lenA]
+
+      -- copy y into new arr from offset
+      _ <- copy nextPos dataPtrB lenB
+
+      makeArrayStruct i8 len dataPtr
+stringConsDef =
+  Builtin "stringCons" [tyChar, tyString] tyString impl
+  where
+    impl [char, strPtr] = do
+      (len, dataPtr) <- readString strPtr
+      newLen <- add len (int32 1)
+      newDataPtr <- allocate newLen i8
+      writeData newDataPtr (int32 0) char
+      firstPos <- gep newDataPtr [int32 1]
+      _ <- copy firstPos dataPtr len
+      makeArrayStruct i8 newLen newDataPtr
+stringSnocDef =
+  Builtin "stringSnoc" [tyString, tyChar] tyString impl
+  where
+    impl [strPtr, char] = do
+      (len, dataPtr) <- readString strPtr
+      newLen <- add len (int32 1)
+      newDataPtr <- allocate newLen i8
+      _ <- copy newDataPtr dataPtr len
+      writeData newDataPtr len char
+      makeArrayStruct i8 newLen newDataPtr
+
+stringStruct :: IR.Type
+stringStruct = StructureType False [i32, ptr i8]
+
+-- read length and data ptr from string
+readString :: (MonadIRBuilder m, MonadModuleBuilder m) => Operand -> m (Operand, Operand)
+readString strPtr = do
+  len <- readStruct strPtr 0
+  dataPtr <- readStruct strPtr 1
+  return (len, dataPtr)

src/Language/Granule/Codegen/Emit/LLVMHelpers.hs

@@ -13,6 +13,9 @@ import Data.Char (ord)
 import LLVM.AST.Constant (Constant)
 import qualified LLVM.AST.Constant as C
 import qualified LLVM.AST.Linkage as L
+import LLVM.IRBuilder
+import Language.Granule.Codegen.Emit.Primitives (malloc)
+import Control.Monad (forM_)
 
 -- | Define and emit a (non-variadic) internal function definition
 privateFunction
@@ -62,6 +65,28 @@ stringConstant :: String -> Constant
 stringConstant str =
     C.Vector (map charConstant str)
 
+allocateString :: MonadModuleBuilder m => MonadIRBuilder m => String -> m Operand
+allocateString str = do
+  -- [len, char*]
+  let structTy = StructureType False [i32, ptr i8]
+  strPtr <- call (ConstantOperand malloc) [(ConstantOperand $ sizeOf structTy, [])]
+  strPtr' <- bitcast strPtr (ptr structTy)
+  lenField <- gep strPtr' [int32 0, int32 0]
+  dataField <- gep strPtr' [int32 0, int32 1]
+
+  -- store the length
+  let len = int32 $ fromIntegral $ length str
+  store lenField 0 len
+
+  -- store the chars
+  dataPtr <- call (ConstantOperand malloc) [(len, [])]
+  forM_ (zip [0..] str) $ \(i, ch) -> do
+      dataPtr' <- gep dataPtr [int32 $ fromIntegral i]
+      store dataPtr' 0 (int8 $ fromIntegral $ ord ch)
+  store dataField 0 dataPtr
+
+  return strPtr
+
 intConstant :: Int -> Constant
 intConstant n =
     C.Int {

src/Language/Granule/Codegen/Emit/LowerExpression.hs

@@ -12,7 +12,7 @@ import Language.Granule.Codegen.Emit.LowerClosure (emitClosureMarker)
 import Language.Granule.Codegen.Emit.EmitterState
 import Language.Granule.Codegen.Emit.Names
 import Language.Granule.Codegen.Emit.Primitives (trap)
-import Language.Granule.Codegen.Emit.LLVMHelpers (stringConstant, charConstant)
+import Language.Granule.Codegen.Emit.LLVMHelpers (charConstant, allocateString)
 
 import Language.Granule.Syntax.Expr
 import Language.Granule.Syntax.Annotated (annotation)
@@ -136,8 +136,9 @@ emitValue _ (NumIntF n) = return $ IC.int32 (toInteger n)
 emitValue _ (NumFloatF n) = return $ IC.double n
 emitValue _ (CharLiteralF ch) =
     return $ IR.ConstantOperand (charConstant ch)
-emitValue _ (StringLiteralF str) =
-    return $ IR.ConstantOperand (stringConstant $ unpack str)
+-- allocate strings as we do with float arrays
+-- TODO: better handling for constants/literals
+emitValue _ (StringLiteralF str) = allocateString (unpack str)
 emitValue _ (ExtF a (Left (GlobalVar ty ident))) = do
     let ref = IR.ConstantOperand $ C.GlobalReference (ptr (llvmType ty)) (definitionNameFromId ident)
     load ref 4

src/Language/Granule/Codegen/Emit/LowerType.hs

@@ -51,6 +51,7 @@ llvmType (TyCon (MkId "()")) =
 llvmType (TyCon (MkId "Int")) = i32
 llvmType (TyCon (MkId "Float")) = double
 llvmType (TyCon (MkId "Char")) = i8
+llvmType (TyCon (MkId "String")) = ptr $ StructureType False [i32, ptr i8]
 llvmType (TyCon (MkId "Handle")) = i8
 llvmType (TyCon (MkId "Bool")) = i1
 llvmType (Box coeffect ty) = llvmType ty

src/Language/Granule/Codegen/Emit/MainOut.hs

@@ -34,7 +34,8 @@ loadMainValue mainTy = load mainRef 4
 emitMainOut :: (MonadModuleBuilder m) => GrType -> m Operand
 emitMainOut ty =
     function "internal_mainOut" [(llvmType ty, mkPName "x")] void $ \[x] -> do
-        _ <- emitPrint ty [x]
+        _ <- emitPrint ty x
+        _ <- printFmt "\n" []
         retVoid
 
 mainOut :: GrType -> Constant
@@ -43,26 +44,38 @@ mainOut ty = GlobalReference functionType name
         name = mkName "internal_mainOut"
         functionType = ptr (FunctionType void [llvmType ty] False)
 
-emitPrint :: (MonadModuleBuilder m, MonadIRBuilder m) => GrType -> [Operand] -> m Operand
-emitPrint ty vals = do
-    let str = fmtStrForTy ty ++ "\n"
-    let strLen = length str + 1 -- newline 2 chars
-    fmt <- globalStringPtr str (mkName "internal_mainOut.fmtStr")
-    let fmtPtr = IR.ConstantOperand $ C.GetElementPtr True
-                    (GlobalReference (ptr (ArrayType (fromIntegral strLen) i8)) "internal_mainOut.fmtStr")
-                    [C.Int 32 0, C.Int 32 0]
-    let args = (fmtPtr, []) : map (\v -> (v, [])) vals
-    _ <- call (IR.ConstantOperand printf) args
-    return fmtPtr
+emitPrint :: (MonadModuleBuilder m, MonadIRBuilder m) => GrType -> Operand -> m Operand
+emitPrint ty val = case ty of
+    (TyCon (Id "Int" _)) -> printFmt "%d" [val]
+    (TyCon (Id "Float" _)) -> printFmt "%.6f" [val]
+    (TyCon (Id "Char" _)) -> printFmt "'%c'" [val]
+    (TyCon (Id "()" _)) -> printFmt "()" []
+    (TyApp (TyCon (Id "FloatArray" _)) _) -> printFmt "<array>" []
+    (TyApp (TyApp (TyCon (Id "," _)) leftTy) rightTy) -> do
+        left <- extractValue val [0]
+        right <- extractValue val [1]
+        _ <- printFmt "(" []
+        _ <- emitPrint leftTy left
+        _ <- printFmt ", " []
+        _ <- emitPrint rightTy right
+        printFmt ")" []
+    (TyCon (Id "String" _)) -> do
+        lenPtr <- gep val [int32 0, int32 0]
+        len <- load lenPtr 4
+        elemsPtr <- gep val [int32 0, int32 1]
+        elems <- load elemsPtr 8
+        printFmt "\"%.*s\"" [len, elems]
+    _ -> error "Unsupported"
 
-fmtStrForTy :: GrType -> String
-fmtStrForTy x =
-    case x of
-        (TyCon (Id "Int" _)) -> "%d"
-        (TyCon (Id "Float" _)) -> "%.6f"
-        (TyApp (TyApp (TyCon (Id "," _)) leftTy) rightTy) ->
-            "(" ++ fmtStrForTy leftTy ++ ", " ++ fmtStrForTy rightTy ++ ")"
-        (TyApp (TyCon (Id "FloatArray" _)) _) -> "<array>"
-        (TyCon (Id "()" _)) -> "()"
-        (TyExists _ _ (Borrow _ ty)) -> "*" ++ fmtStrForTy ty
-        _ -> error ("Unsupported Main type: " ++ show x)
+printFmt :: (MonadModuleBuilder m, MonadIRBuilder m) => String -> [Operand] -> m Operand
+printFmt fmt args = do
+    let name = mkName $ "fmt." ++ fmt
+    fmtPtr <- mkFmtPtr fmt name (length fmt + 1)
+    call (IR.ConstantOperand printf) ((fmtPtr, []) : map (\a -> (a, [])) args)
+
+mkFmtPtr :: (MonadModuleBuilder m, MonadIRBuilder m) => String -> IR.Name -> Int -> m Operand
+mkFmtPtr str name len = do
+    _ <- globalStringPtr str name
+    return $ IR.ConstantOperand $ C.GetElementPtr True
+              (GlobalReference (ptr (ArrayType (fromIntegral len) i8)) name)
+              [C.Int 32 0, C.Int 32 0]

tests/golden/positive/string.golden

@@ -0,0 +1 @@
+"hello world"

tests/golden/positive/string.gr

@@ -0,0 +1,6 @@
+hello : String
+hello = stringSnoc "hell" (charFromInt 111)
+
+
+main : String
+main = stringAppend hello (stringCons ' ' "world")