Implement type-level string append function

src/Libraries/Base1/Prelude.bs

@@ -7,7 +7,7 @@ package Prelude(
         PrimParam(..), PrimPort(..),
         Bit, Rules, Module, Integer, Real, String, Char, SizeOf, Id__,
         PrimAction, ActionValue, Action, ActionValue_, ActionWorld, AVStruct,
-        TAdd, TSub, TMul, TDiv, TLog, TExp, TMax, TMin,
+        TAdd, TSub, TMul, TDiv, TLog, TExp, TMax, TMin, TApp,
         Nat(..),
         IsModule(..), addModuleRules, addRules,
 
@@ -2772,6 +2772,8 @@ primitive type TExp :: # -> #
 primitive type TMax :: # -> # -> #
 primitive type TMin :: # -> # -> #
 
+primitive type TApp :: $ -> $ -> $
+
 ------------------
 
 --- Bit operations

src/comp/CType.hs

@@ -71,7 +71,7 @@ import PreIds(idArrow, idPrimPair, idPrimUnit, idBit, idString,
 import Util(itos)
 import ErrorUtil
 import Pragma(IfcPragma)
-import NumType
+import TypeOps
 import PVPrint(PVPrint(..))
 import FStringCompat
 
@@ -507,6 +507,10 @@ normTAp (TCon (TyCon op _ _)) (TCon (TyNum x xpos))
         | isJust (res) = cTNum (fromJust res) (getPosition op)
   where res = opNumT op [x]
 
+normTAp (TAp (TCon (TyCon op _ _)) (TCon (TyStr x xpos))) (TCon (TyStr y ypos))
+        | isJust (res) = cTStr (fromJust res) (getPosition op)
+  where res = opStrT op [x, y]
+
 normTAp f a = TAp f a
 
 getTypeKind :: Type -> Maybe Kind

src/comp/ISyntax.hs

@@ -96,7 +96,7 @@ import IdPrint
 import PreIds(idSizeOf, idId, idBind, idReturn, idPack, idUnpack, idMonad, idLiftModule, idBit, idFromInteger)
 import Backend
 import Prim(PrimOp(..))
-import NumType
+import TypeOps
 import ConTagInfo
 import VModInfo(VModInfo, vArgs, vName, VName(..), {- VeriPortProp(..), -}
                 VArgInfo(..), VFieldInfo(..), isParam, VWireInfo)
@@ -425,6 +425,9 @@ normITAp (ITAp (ITCon op _ _) (ITNum x)) (ITNum y) | isJust (res) =
 normITAp (ITCon op _ _) (ITNum x) | isJust (res) =
     mkNumConT (fromJust res)
   where res = opNumT op [x]
+normITAp (ITAp (ITCon op _ _) (ITStr x)) (ITStr y) | isJust (res) =
+    ITStr (fromJust res)
+  where res = opStrT op [x, y]
 
 normITAp f@(ITCon op _ _) a | op == idSizeOf && notVar a =
         -- trace ("normITAp: " ++ ppReadable (ITAp f a)) $

src/comp/PreIds.hs

@@ -81,7 +81,7 @@ idPrimSnd = prelude_id_no fsPrimSnd
 idPrimPair = prelude_id_no fsPrimPair
 idFalse = prelude_id_no fsFalse
 idTrue = prelude_id_no fsTrue
-idSizeOf, idTAdd, idTSub, idTMul, idTDiv, idTLog, idTExp, idTMax, idTMin :: Id
+idSizeOf, idTAdd, idTSub, idTMul, idTDiv, idTLog, idTExp, idTMax, idTMin, idTApp :: Id
 idSizeOf = prelude_id_no fsSizeOf
 idTAdd = prelude_id_no fsTAdd
 idTSub = prelude_id_no fsTSub
@@ -91,6 +91,7 @@ idTLog = prelude_id_no fsTLog
 idTExp = prelude_id_no fsTExp
 idTMax = prelude_id_no fsTMax
 idTMin = prelude_id_no fsTMin
+idTApp = prelude_id_no fsTApp
 idAction, idPrimAction, idToPrimAction, idFromPrimAction :: Id
 idAction = prelude_id_no fsAction
 idPrimAction = prelude_id_no fsPrimAction

src/comp/PreStrings.hs

@@ -279,6 +279,7 @@ fsTLog             = mkFString "TLog"
 fsTExp             = mkFString "TExp"
 fsTMax             = mkFString "TMax"
 fsTMin             = mkFString "TMin"
+fsTApp             = mkFString "TApp"
 fsStaticAssert     = mkFString "staticAssert"
 fsDynamicAssert    = mkFString "dynamicAssert"
 fsContinuousAssert = mkFString "continuousAssert"

src/comp/Pred.hs

@@ -20,7 +20,7 @@ import Position
 import Id
 import IdPrint
 import Type
-import NumType
+import TypeOps
 import PFPrint
 import CSyntax(CExpr)
 import CType
@@ -267,6 +267,8 @@ apTFun :: Type -> Id -> [Type] -> Type
 apTFun _ i [TCon (TyNum x px), TCon (TyNum y py)] | Just n <- opNumT i [x, y] = TCon (TyNum n p')
   where p' = bestPosition px py
 apTFun _ i [TCon (TyNum x px)] | Just n <- opNumT i [x] = TCon (TyNum n px)
+apTFun _ i [TCon (TyStr x px), TCon (TyStr y py)] | Just s <- opStrT i [x, y] = TCon (TyStr s p')
+  where p' = bestPosition px py
 apTFun t _ as = foldl TAp t as
 
 -----------------------------------------------------------------------------

src/comp/NumType.hs → src/comp/TypeOps.hs

@@ -1,9 +1,10 @@
-module NumType(opNumT, numOpNames) where
--- common routines for handling numeric types
+module TypeOps(opNumT, numOpNames, opStrT, strOpNames) where
+-- common routines for handling numeric and string types
 
 import Id
-import PreIds(idTAdd, idTSub, idTMul, idTDiv, idTLog, idTExp, idTMax, idTMin)
+import PreIds(idTAdd, idTSub, idTMul, idTDiv, idTLog, idTExp, idTMax, idTMin, idTApp)
 import Util(divC, log2)
+import FStringCompat(FString, concatFString)
 
 -- do a numeric type operation on a list of arguments
 -- note that we have to validate that the result is going to
@@ -21,3 +22,10 @@ opNumT _ _      = Nothing
 
 numOpNames :: [Id]
 numOpNames = [idTAdd, idTSub, idTMul, idTDiv, idTExp, idTLog, idTMax, idTMin]
+
+opStrT :: Id -> [FString] -> Maybe FString
+opStrT i xs | i == idTApp = Just $ concatFString xs
+opStrT _ _ = Nothing
+
+strOpNames :: [Id]
+strOpNames = [idTApp]

testsuite/bsc.typechecker/string/TApp.bs

@@ -0,0 +1,31 @@
+package TApp where
+
+data (WrapStr :: $ -> *) s = WrapStr
+
+printWrapStr :: WrapStr s -> Action
+printWrapStr _ = $display (stringOf s)
+
+a :: WrapStr (TApp "aaa" "bbb")
+a = WrapStr
+
+class FlatWrapStr a s | a -> s where {}
+
+instance (FlatWrapStr a s2) => FlatWrapStr (WrapStr s1, a) (TApp s1 (TApp "_" s2)) where {}
+instance FlatWrapStr (WrapStr s) s where {}
+instance FlatWrapStr () "" where {}
+
+b :: (FlatWrapStr (WrapStr "aaa", WrapStr "bbb", WrapStr "ccc") s) => WrapStr s
+b = WrapStr
+
+c :: (FlatWrapStr () s) => WrapStr s
+c = WrapStr
+
+sysTApp :: Module Empty
+sysTApp = module
+
+  rules
+    when True ==> do
+      printWrapStr a
+      printWrapStr b
+      printWrapStr c
+      $finish

testsuite/bsc.typechecker/string/string.exp

@@ -15,3 +15,4 @@ test_c_veri StringOf
 test_c_veri_bsv StringOfBSV
 
 test_c_veri TypeClassString
+test_c_veri TApp

testsuite/bsc.typechecker/string/sysTApp.out.expected

@@ -0,0 +1,3 @@
+aaabbb
+aaa_bbb_ccc
+