From 4b9e9445182455c9c0a44785d73cefc34d374226 Mon Sep 17 00:00:00 2001 From: Lucas Kramer Date: Thu, 1 Aug 2024 11:54:32 -0700 Subject: [PATCH] Implement type-level string append function --- src/Libraries/Base1/Prelude.bs | 4 ++- src/comp/CType.hs | 6 +++- src/comp/ISyntax.hs | 5 ++- src/comp/PreIds.hs | 3 +- src/comp/PreStrings.hs | 1 + src/comp/Pred.hs | 4 ++- src/comp/{NumType.hs => TypeOps.hs} | 14 +++++++-- testsuite/bsc.typechecker/string/TApp.bs | 31 +++++++++++++++++++ testsuite/bsc.typechecker/string/string.exp | 1 + .../string/sysTApp.out.expected | 3 ++ 10 files changed, 64 insertions(+), 8 deletions(-) rename src/comp/{NumType.hs => TypeOps.hs} (70%) create mode 100644 testsuite/bsc.typechecker/string/TApp.bs create mode 100644 testsuite/bsc.typechecker/string/sysTApp.out.expected diff --git a/src/Libraries/Base1/Prelude.bs b/src/Libraries/Base1/Prelude.bs index 5c379d024..7bf80b829 100644 --- a/src/Libraries/Base1/Prelude.bs +++ b/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 diff --git a/src/comp/CType.hs b/src/comp/CType.hs index 21609e355..eed9551a4 100644 --- a/src/comp/CType.hs +++ b/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 diff --git a/src/comp/ISyntax.hs b/src/comp/ISyntax.hs index c8af1ea6b..756680dc9 100644 --- a/src/comp/ISyntax.hs +++ b/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)) $ diff --git a/src/comp/PreIds.hs b/src/comp/PreIds.hs index 192621e27..500c59a66 100644 --- a/src/comp/PreIds.hs +++ b/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 diff --git a/src/comp/PreStrings.hs b/src/comp/PreStrings.hs index cc06010b6..0d9623724 100644 --- a/src/comp/PreStrings.hs +++ b/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" diff --git a/src/comp/Pred.hs b/src/comp/Pred.hs index f91093565..1456592a4 100644 --- a/src/comp/Pred.hs +++ b/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 ----------------------------------------------------------------------------- diff --git a/src/comp/NumType.hs b/src/comp/TypeOps.hs similarity index 70% rename from src/comp/NumType.hs rename to src/comp/TypeOps.hs index 6446a55df..24b82b6ab 100644 --- a/src/comp/NumType.hs +++ b/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] diff --git a/testsuite/bsc.typechecker/string/TApp.bs b/testsuite/bsc.typechecker/string/TApp.bs new file mode 100644 index 000000000..aac199b89 --- /dev/null +++ b/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 diff --git a/testsuite/bsc.typechecker/string/string.exp b/testsuite/bsc.typechecker/string/string.exp index b3b6581f1..7acab4bb4 100644 --- a/testsuite/bsc.typechecker/string/string.exp +++ b/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 diff --git a/testsuite/bsc.typechecker/string/sysTApp.out.expected b/testsuite/bsc.typechecker/string/sysTApp.out.expected new file mode 100644 index 000000000..3246f2a70 --- /dev/null +++ b/testsuite/bsc.typechecker/string/sysTApp.out.expected @@ -0,0 +1,3 @@ +aaabbb +aaa_bbb_ccc +