Add termTypePrec to TermLiteral to allow for TermLiteral SNat

changelog/2022-09-14T12_17_00+02_00_add_termTypePrec

@@ -0,0 +1,14 @@
+Internal change: Added `showsTypePrec` to `TermLiteral` to make `TermLiteral SNat` work as expected. Deriving an instance is now a bit simpler. Instances which previously had to be defined as:
+
+```haskell
+instance TermLiteral Bool where
+  termToData = $(deriveTermToData ''Bool)
+```
+
+can now be defined using:
+
+```haskell
+deriveTermLiteral ''Bool
+```
+
+Internal add: Added `TermLiteral` instance for `Either`.

clash-lib/clash-lib.cabal

@@ -368,13 +368,15 @@ test-suite unittests
       tasty         >= 1.2      && < 1.5,
       tasty-hunit,
       tasty-quickcheck,
+      tasty-th,
       template-haskell,
       text,
       transformers,
       unordered-containers
 
   Other-Modules: Clash.Tests.Core.FreeVars
                  Clash.Tests.Core.Subst
+                 Clash.Tests.Core.TermLiteral
                  Clash.Tests.Driver.Manifest
                  Clash.Tests.Netlist.Id
                  Clash.Tests.Util.Interpolate

clash-lib/src/Clash/Core/TermLiteral.hs

@@ -1,6 +1,7 @@
 {-|
 Copyright   :  (C) 2019, Myrtle Software Ltd,
                    2021, QBayLogic B.V.
+                   2022, Google Inc.
 License     :  BSD2 (see the file LICENSE)
 Maintainer  :  QBayLogic B.V. <devops@qbaylogic.com>
 
@@ -14,6 +15,8 @@ Tools to convert a 'Term' into its "real" representation
 
 module Clash.Core.TermLiteral
   ( TermLiteral
+  , showsTypePrec
+  , showType
   , termToData
   , termToDataError
   ) where
@@ -30,13 +33,19 @@ import           GHC.Stack
 import           Clash.Core.Term                 (Term(Literal), collectArgs)
 import           Clash.Core.Literal
 import           Clash.Core.Pretty               (showPpr)
+import           Clash.Promoted.Nat
+import           Clash.Promoted.Nat.Unsafe
 import qualified Clash.Util.Interpolate          as I
 import qualified Clash.Verification.Internal     as Cv
 
 import           Clash.Core.TermLiteral.TH
 
--- | Tools to deal with literals encoded as a "Term".
-class Typeable a => TermLiteral a where
+-- | Pretty print type @a@
+showType :: TermLiteral a => Proxy a -> String
+showType proxy = showsTypePrec 0 proxy ""
+
+-- | Tools to deal with literals encoded as a 'Term'.
+class TermLiteral a where
   -- | Convert 'Term' to the constant it represents. Will return an error if
   -- (one of the subterms) fail to translate.
   termToData
@@ -47,6 +56,23 @@ class Typeable a => TermLiteral a where
     -- ^ 'Left' indicates a failure, containing the (sub)term that failed to
     -- translate. 'Right' indicates a success.
 
+  -- | Pretty print the type of a term (for error messages). Its default implementation
+  -- uses 'Typeable' to print the type. Note that this method is there to allow
+  -- an instance for 'SNat' to exist (and other GADTs imposing
+  -- t'GHC.TypeNats.KnownNat'). Without it, GHC would ask for a @KnownNat@
+  -- constraint on the instance, which would defeat the purpose of it.
+  showsTypePrec ::
+    -- | The operator precedence of the enclosing context (a number from @0@ to
+    -- @11@). Function application has precedence @10@. Used to determine whether
+    -- the result should be wrapped in parentheses.
+    Int ->
+    -- | Proxy for a term whose type needs to be pretty printed
+    Proxy a ->
+    ShowS
+
+  default showsTypePrec :: Typeable a => Int -> Proxy a -> ShowS
+  showsTypePrec n _ = showsPrec n (typeRep (Proxy @a))
+
 instance TermLiteral Term where
   termToData = pure
 
@@ -80,34 +106,59 @@ instance TermLiteral Natural where
     Right (fromInteger n)
   termToData t = Left t
 
+-- | Unsafe warning: If you use this instance in a monomorphic context (e.g.,
+-- @TermLiteral (SNat 5)@), you need to make very sure that the term corresponds
+-- to the literal. If you don't, there will be a mismatch between type level
+-- variables and the proof carried in 'SNat's 'KnownNat'. Typical usage of this
+-- instance will therefore leave the /n/ polymorphic.
+--
+instance TermLiteral (SNat n) where
+  termToData (collectArgs -> (_, [_, Left (Literal (NaturalLiteral n))])) =
+    Right (unsafeSNat n)
+  termToData t = Left t
+
+  showsTypePrec n _
+    -- We don't know the literal /n/ at this point. However, we can't simply put
+    -- and /n/ here either, as it might collide with other type variables. To
+    -- prevent confusion, we put an underscore. This is obviously "wrong", but
+    -- good enough for error messages - the main purpose of this function.
+    = showParen (n > 10) $ showString "SNat _"
+
 instance (TermLiteral a, TermLiteral b) => TermLiteral (a, b) where
   termToData (collectArgs -> (_, lefts -> [a, b])) = do
     a' <- termToData a
     b' <- termToData b
     pure (a', b')
   termToData t = Left t
 
-instance TermLiteral a => TermLiteral (Maybe a) where
-  termToData = $(deriveTermToData ''Maybe)
-
-instance TermLiteral Bool where
-  termToData = $(deriveTermToData ''Bool)
-
-instance TermLiteral Cv.RenderAs where
-  termToData = $(deriveTermToData ''Cv.RenderAs)
-
-instance TermLiteral a => TermLiteral (Cv.Assertion' a) where
-  termToData = $(deriveTermToData ''Cv.Assertion')
-
-instance TermLiteral a => TermLiteral (Cv.Property' a) where
-  termToData = $(deriveTermToData ''Cv.Property')
+  showsTypePrec _ _ =
+    -- XXX: We pass in 11 here, but should really be passing in 0. We never want
+    --      any parentheses for fields in tuples. However, Typeable's show
+    --      implementation does put parentheses around tuple fields - so we
+    --      replicate that behavior here for ease of testing.
+      showChar '('
+    . showsTypePrec 11 (Proxy @a)
+    . showString ","
+    . showsTypePrec 11 (Proxy @b)
+    . showChar ')'
+
+deriveTermLiteral ''Bool
+deriveTermLiteral ''Maybe
+deriveTermLiteral ''Either
+deriveTermLiteral ''Cv.RenderAs
+deriveTermLiteral ''Cv.Assertion'
+deriveTermLiteral ''Cv.Property'
 
 -- | Same as 'termToData', but returns printable error message if it couldn't
 -- translate a term.
 termToDataError :: forall a. TermLiteral a => Term -> Either String a
 termToDataError term = bimap err id (termToData term)
  where
-  typ = show (typeRep (Proxy @a))
+  -- XXX: If we put this construct in the quasiquoted part, it yields a parse
+  --      error on some platforms. This is likely related to some older version
+  --      of dependencies. In the interested of time yours truly just moved it
+  --      outside of the quasiquoter.
+  shownType = showType (Proxy @a)
 
   err failedTerm = [I.i|
     Failed to translate term to literal. Term that failed to translate:
@@ -120,5 +171,5 @@ termToDataError term = bimap err id (termToData term)
 
     While trying to interpret something to type:
 
-      #{typ}
+      #{shownType}
   |]

clash-lib/src/Clash/Core/TermLiteral/TH.hs

@@ -1,15 +1,22 @@
-{-# LANGUAGE TemplateHaskellQuotes #-}
+{-# LANGUAGE CPP #-}
+{-# LANGUAGE LambdaCase #-}
+{-# LANGUAGE TemplateHaskell #-}
 
 module Clash.Core.TermLiteral.TH
-  (  deriveTermToData
+  ( deriveTermToData
+  , deriveshowsTypePrec
+  , deriveTermLiteral
      -- Stop exporting @dcName'@  once `ghcide` stops type-checking expanded
      -- TH splices
   ,  dcName'
   ) where
 
 import           Data.Either
 import qualified Data.Text                       as Text
+import           Data.List                       (intersperse)
+import           Data.Proxy
 import           Language.Haskell.TH.Syntax
+import           Language.Haskell.TH.Lib         hiding (match)
 
 import           Clash.Core.DataCon
 import           Clash.Core.Term                 (collectArgs, Term(Data))
@@ -21,11 +28,114 @@ import           Clash.Core.Name                 (nameOcc)
 -- module Clash.Core.Subst cannot be linked; it is only available as a boot module
 import Clash.Core.Subst ()
 
+#if __GLASGOW_HASKELL__ >= 900
+type CompatTyVarBndr = TyVarBndr ()
+#else
+type CompatTyVarBndr = TyVarBndr
+#endif
+
 dcName' :: DataCon -> String
 dcName' = Text.unpack . nameOcc . dcName
 
 termToDataName :: Name
-termToDataName = mkName "Clash.Core.TermLiteral.termToData"
+termToDataName =
+  -- Note that we can't use a fully qualified name here: GHC disallows fully
+  -- qualified names in instance function declarations.
+  mkName "termToData"
+
+showsTypePrecName :: Name
+showsTypePrecName =
+  -- Note that we can't use a fully qualified name here: GHC disallows fully
+  -- qualified names in instance function declarations.
+  mkName "showsTypePrec"
+
+termLiteralName :: Name
+termLiteralName = mkName "Clash.Core.TermLiteral.TermLiteral"
+
+-- | Extracts variable names from a 'TyVarBndr', errors if it is not a simply
+-- typed variable name.
+typeVarName :: CompatTyVarBndr -> Q Name
+typeVarName = \case
+#if __GLASGOW_HASKELL__ >= 900
+  PlainTV typVarName () -> pure typVarName
+  KindedTV typVarName () StarT -> pure typVarName
+#else
+  PlainTV typVarName -> pure typVarName
+  KindedTV typVarName StarT -> pure typVarName
+#endif
+  k@(KindedTV {}) -> fail $ "Not supported: KindedTV: " <> show k
+
+-- | Derive a t'Clash.Core.TermLiteral.TermLiteral' instance for given type
+deriveTermLiteral :: Name -> Q [Dec]
+deriveTermLiteral typName = do
+  TyConI (DataD _ _ typeVars _ _ _) <- reify typName
+  typeVarNames <- mapM typeVarName typeVars
+  showsTypePrec <- deriveshowsTypePrec typName typeVarNames
+  termToDataBody <- deriveTermToData typName
+  let
+    termToData = FunD termToDataName [Clause [] (NormalB termToDataBody) []]
+    innerInstanceType = foldl AppT (ConT typName) (map VarT typeVarNames)
+    instanceType = ConT termLiteralName `AppT` innerInstanceType
+    constraint typVarName = [t| $(conT termLiteralName) $(varT typVarName) |]
+  constraints <- mapM constraint typeVarNames
+  pure $ [InstanceD Nothing constraints instanceType [showsTypePrec, termToData]]
+
+-- | For 'Maybe', constructs:
+--
+-- > showsTypePrec n _
+-- >   = let
+-- >       showSpace = showChar ' '
+-- >       precCalls = [showsTypePrec 11 (Proxy @a)]
+-- >       interspersedPrecCalls = intersperse showSpace precCalls
+-- >       showType = foldl (.) (showString "Maybe") (showSpace : interspersedPrecCalls)
+-- >     in
+-- >       showParen (n > 10) showType
+--
+deriveshowsTypePrec :: Name -> [Name] -> Q Dec
+deriveshowsTypePrec typName typeVarNames = do
+  TyConI (DataD _ _ typeVars _ _ _) <- reify typName
+  showTypeBody <- mkShowTypeBody typeVars
+  pure (FunD showsTypePrecName [Clause [VarP nName, WildP] (NormalB showTypeBody) []])
+ where
+  showTypeName = [| showString $(litE (StringL (nameBase typName))) |]
+
+  -- Constructs:
+  --
+  -- > showsTypePrec 11 (Proxy @a)
+  --
+  -- where the 'a' is given as an argument. The surrounding operator precedence
+  -- is set to indicate "function" application. I.e., it instructs the call to
+  -- wrap the type string in parentheses.
+  --
+  mkTypePrecCall typVarName =
+    [| $(varE showsTypePrecName) 11 (Proxy @($(varT typVarName))) |]
+
+  -- Constructs:
+  --
+  -- > showString "Maybe" . showChar ' ' . showsTypePrec 11 (Proxy @a)
+  --
+  -- This is wrapped in an if-statement wrapping the result in parentheses if the
+  -- incoming prec is more than 10 (function application).
+  --
+  mkShowTypeBody :: [CompatTyVarBndr] -> Q Exp
+  mkShowTypeBody typeVars =
+    case typeVars of
+      [] ->
+        -- We seq on `n` here to prevent _unused variable_ warnings. This is a
+        -- bit of a hack (the real solution would be to selectively pattern
+        -- match).
+        [| $(varE nName) `seq` $(showTypeName) |]
+      _  -> [|
+        let
+          showSpace = showChar ' '
+          precCalls = $(listE (map mkTypePrecCall typeVarNames))
+          interspersedPrecCalls = intersperse showSpace precCalls
+          showType = foldl (.) $(showTypeName) (showSpace : interspersedPrecCalls)
+        in
+          showParen ($(varE nName) > 10) showType
+       |]
+
+  nName = mkName "n"
 
 deriveTermToData :: Name -> Q Exp
 deriveTermToData typName = do
@@ -95,4 +205,3 @@ deriveTermToData1 constrs =
   argsName = mkName "args"
   argNames = [mkName ("arg" ++ show n) | n <- [0..nArgs-1]]
   nameName = mkName "nm"
-