Types.hs

-----------------------------------------------------------------------------
-- |
-- Module    : Data.SBV.Compilers.C.Types
-- Copyright : (c) Levent Erkok
-- License   : BSD3
-- Maintainer: erkokl@gmail.com
-- Stability : experimental
--
-- Shared C type and helper names for structurally lowered SBV kinds.
-----------------------------------------------------------------------------

{-# OPTIONS_GHC -Wall -Werror #-}

module Data.SBV.Compilers.C.Types
  ( tupleCType
  , adtCType
  , definedFunctionCName
  , arrayKindTag
  , arrayOutputCTypeName
  , arrayStoredCloneName
  , arrayStoredReleaseName
  , tupleFieldName
  , tupleOwnedInitName
  , tupleOwnedSetName
  , tupleOwnedCloneName
  , tupleOwnedReleaseName
  , adtOwnedInitName
  , adtOwnedSetName
  , adtOwnedCloneName
  , adtOwnedReleaseName
  , adtEqualName
  , listCloneName
  , listReleaseName
  , listHelperName
  , setCloneName
  , setReleaseName
  , setHelperName
  , textCloneName
  , textReleaseName
  , textCompareName
  , elementCType
  , constElementCType
  , kindTag
  , isConcreteADT
  , isConcreteADTReference
  ) where

import Data.Char                   (isAlphaNum, isAscii, ord)
import Numeric                     (showHex)

import Data.SBV.Compilers.C.FP         (arbitraryFPCType)
import Data.SBV.Core.Data

-- | Return the helper name that initializes caller-owned storage for a tuple
-- with recursively managed fields.
tupleOwnedInitName :: Kind -> String
tupleOwnedInitName kind = "sbv_tuple_owned_init_" ++ kindTag kind

-- | Return the helper name that assigns into initialized owned tuple storage.
tupleOwnedSetName :: Kind -> String
tupleOwnedSetName kind = "sbv_tuple_owned_set_" ++ kindTag kind

-- | Return the public helper name that deep-copies a managed-field tuple.
tupleOwnedCloneName :: Kind -> String
tupleOwnedCloneName kind = "sbv_tuple_owned_clone_" ++ kindTag kind

-- | Return the public helper name that releases an owned managed-field tuple.
tupleOwnedReleaseName :: Kind -> String
tupleOwnedReleaseName kind = "sbv_tuple_owned_release_" ++ kindTag kind

-- | Return the helper name that initializes caller-owned storage for one ADT
-- constructor.
adtOwnedInitName :: Kind -> String
adtOwnedInitName kind = "sbv_adt_owned_init_" ++ adtCType kind

-- | Return the helper name that assigns into initialized owned ADT storage.
adtOwnedSetName :: Kind -> String
adtOwnedSetName kind = "sbv_adt_owned_set_" ++ adtCType kind

-- | Return the public helper name that deep-copies an owned ADT.
adtOwnedCloneName :: Kind -> String
adtOwnedCloneName kind = "sbv_adt_owned_clone_" ++ adtCType kind

-- | Return the public helper name that releases an owned ADT.
adtOwnedReleaseName :: Kind -> String
adtOwnedReleaseName kind = "sbv_adt_owned_release_" ++ adtCType kind

-- | Return the generated structural-equality helper for a recursive ADT.
adtEqualName :: Bool -> Kind -> String
adtEqualName strong kind = "sbv_adt_" ++ (if strong then "object_" else "")
                        ++ "equal_" ++ adtCType kind

-- | Return the generated clone-helper name for a list kind.
listCloneName :: Kind -> String
listCloneName (KList elementKind) = "sbv_list_clone_" ++ kindTag elementKind
listCloneName kind                = error $ "SBV->C: Expected a list kind, received " ++ show kind

-- | Return the generated release-helper name for a list kind.
listReleaseName :: Kind -> String
listReleaseName (KList elementKind) = "sbv_list_release_" ++ kindTag elementKind
listReleaseName kind                = error $ "SBV->C: Expected a list kind, received " ++ show kind

-- | Return one specialized list-operation helper name.
listHelperName :: Kind -> String -> String
listHelperName (KList elementKind) suffix = "sbv_list_" ++ kindTag elementKind ++ "_" ++ suffix
listHelperName kind                _      = error $ "SBV->C: Expected a list kind, received " ++ show kind

-- | Return the generated clone-helper name for a set kind.
setCloneName :: Kind -> String
setCloneName (KSet elementKind) = "sbv_set_clone_" ++ kindTag elementKind
setCloneName kind               = error $ "SBV->C: Expected a set kind, received " ++ show kind

-- | Return the generated release-helper name for a set kind.
setReleaseName :: Kind -> String
setReleaseName (KSet elementKind) = "sbv_set_release_" ++ kindTag elementKind
setReleaseName kind               = error $ "SBV->C: Expected a set kind, received " ++ show kind

-- | Return one specialized set-operation helper name.
setHelperName :: Kind -> String -> String
setHelperName (KSet elementKind) suffix = "sbv_set_" ++ kindTag elementKind ++ "_" ++ suffix
setHelperName kind               _      = error $ "SBV->C: Expected a set kind, received " ++ show kind

-- | Name of the public helper that copies a string into owned storage.
textCloneName :: String
textCloneName = "sbv_string_clone"

-- | Name of the public helper that releases owned string storage.
textReleaseName :: String
textReleaseName = "sbv_string_release"

-- | Name of the lexicographic string-comparison runtime helper.
textCompareName :: String
textCompareName = "sbv_text_compare"

-- | A resolved user ADT, excluding built-in rounding modes and opaque sorts.
isConcreteADT :: Kind -> Bool
isConcreteADT kind = isADT kind && not (isRoundingMode kind) && not (isUninterpreted kind)

-- | A user ADT or a retained application awaiting ADT-reference resolution.
-- Keep this distinct from 'isConcreteADT' for dependency and ownership walks.
isConcreteADTReference :: Kind -> Bool
isConcreteADTReference KApp{} = True
isConcreteADTReference kind   = isConcreteADT kind

-- | Return the public C structure type used for a tuple kind.
tupleCType :: Kind -> String
tupleCType kind@KTuple{} = "SBVTuple_" ++ kindTag kind
tupleCType kind          = error $ "SBV->C: Expected a tuple kind, received " ++ show kind

-- | Return the public C structure type used for a concrete ADT kind or an
-- unresolved application of a registered ADT.
adtCType :: Kind -> String
adtCType kind@(KADT typeName parameters _)
  | isADT kind && not (isRoundingMode kind) && not (isUninterpreted kind)
  = appliedType typeName (map snd parameters)
  | True
  = error $ "SBV->C: Expected a concrete ADT kind, received " ++ show kind
adtCType (KApp typeName arguments) = appliedType typeName arguments
adtCType kind = error $ "SBV->C: Expected an ADT kind, received " ++ show kind

-- | Return the private C identifier used for an SBV-defined function. Encoding
-- the complete SMT identifier keeps quoted and firstified names collision-free.
definedFunctionCName :: String -> String
definedFunctionCName functionName = "sbv_function_" ++ encodeIdentifier functionName

-- | Render the common C type spelling shared by a concrete ADT and an
-- unresolved application of that same registered ADT.
appliedType :: String -> [Kind] -> String
appliedType typeName arguments = "SBVADT_" ++ encodeIdentifier typeName ++ concatMap parameterTag arguments
 where parameterTag parameterKind = "_" ++ show (length tag) ++ "_" ++ tag
        where tag = kindTag parameterKind

-- | Return the public member name used for a one-based tuple field index.
tupleFieldName :: Int -> String
tupleFieldName index
  | index >= 1 = "field" ++ show index
  | True       = error $ "SBV->C: Tuple fields are one-based, received " ++ show index

-- | Return the public C type used for a structurally lowered field or element.
elementCType :: Kind -> String
elementCType KBool               = "SBool"
elementCType (KBounded False 1)  = "SBool"
elementCType (KBounded False w)  = "SWord" ++ show w
elementCType (KBounded True  w)  = "SInt" ++ show w
elementCType KUnbounded          = "SInteger"
elementCType KReal               = "SReal"
elementCType KRational           = "SRational"
elementCType KFloat              = "SFloat"
elementCType KDouble             = "SDouble"
elementCType KChar               = "SChar"
elementCType KString             = "SString"
elementCType kind@KFP{}          = arbitraryFPCType kind
elementCType kind@KTuple{}       = tupleCType kind
elementCType kind@KADT{}
  | isRoundingMode kind          = "RoundingMode"
  | True                         = adtCType kind
elementCType kind@KApp{}         = adtCType kind
elementCType (KList elementKind) = "SBVList_" ++ kindTag elementKind
elementCType (KSet elementKind)  = "SBVSet_" ++ kindTag elementKind
elementCType kind@KArray{}       = arrayOutputCTypeName kind ++ " *"
elementCType kind                = error $ "SBV->C: Unsupported structural kind: " ++ show kind

-- | Qualify a stored value itself. Array values are spelled as pointers, so
-- their const qualifier belongs after the pointer, not on its pointee.
constElementCType :: Kind -> String
constElementCType kind
  | isArray kind = elementCType kind ++ " const"
  | True         = "const " ++ elementCType kind

-- | Return the suffix used by a generated structural C type. Structural
-- components are length-framed and identifiers are escaped injectively.
-- Consumers must preserve case, including in preprocessor guards and tags.
-- Booleans and unsigned one-bit vectors intentionally share a representation,
-- as do a concrete ADT and its corresponding resolved application.
kindTag :: Kind -> String
kindTag KBool               = "u1"
kindTag (KBounded False w)  = "u" ++ show w
kindTag (KBounded True  w)  = "s" ++ show w
kindTag KUnbounded          = "integer"
kindTag KReal               = "real"
kindTag KRational           = "rational"
kindTag KFloat              = "float"
kindTag KDouble             = "double"
kindTag KChar               = "char"
kindTag KString             = "string"
kindTag (KFP eb sb)         = "fp_e" ++ show eb ++ "_s" ++ show sb
kindTag (KTuple fields)     = "t" ++ show (length fields) ++ concatMap (('_' :) . taggedKind . kindTag) fields
kindTag kind@KADT{}
  | isRoundingMode kind     = "rounding_mode"
  | True                    = "adt_" ++ encodeIdentifier (adtCType kind)
kindTag kind@KApp{}         = "adt_" ++ encodeIdentifier (adtCType kind)
kindTag (KList elementKind) = "list_" ++ taggedKind (kindTag elementKind)
kindTag (KSet elementKind)  = "set_"  ++ taggedKind (kindTag elementKind)
kindTag kind@KArray{}       = "array_" ++ taggedKind (arrayKindTag kind)
kindTag kind                = error $ "SBV->C: Unsupported structural kind: " ++ show kind

-- | Return the key/value suffix shared by generated names for an array kind.
-- Frame both components by length, just as for tuple fields and ADT arguments,
-- so nested tags need not be parsed to find the key/value boundary.
--
-- >>> arrayKindTag (KArray (KBounded False 8) (KBounded False 32))
-- "2_u8_3_u32"
arrayKindTag :: Kind -> String
arrayKindTag (KArray keyKind valueKind) = taggedKind (kindTag keyKind) ++ "_" ++ taggedKind (kindTag valueKind)
arrayKindTag kind                       = error $ "SBV->C: Expected an array kind, received " ++ show kind

-- | Return the public owned-output descriptor name for an array kind.
arrayOutputCTypeName :: Kind -> String
arrayOutputCTypeName kind@KArray{} = "SBVArrayOutput_" ++ arrayKindTag kind
arrayOutputCTypeName kind          = error $ "SBV->C: Expected an array kind, received " ++ show kind

-- | Return the helper name that clones an array descriptor stored by pointer
-- inside another generated value.
arrayStoredCloneName :: Kind -> String
arrayStoredCloneName kind@KArray{} = "sbv_array_stored_clone_" ++ arrayKindTag kind
arrayStoredCloneName kind          = error $ "SBV->C: Expected an array kind, received " ++ show kind

-- | Return the helper name that releases an array descriptor stored by pointer
-- inside another generated value.
arrayStoredReleaseName :: Kind -> String
arrayStoredReleaseName kind@KArray{} = "sbv_array_stored_release_" ++ arrayKindTag kind
arrayStoredReleaseName kind          = error $ "SBV->C: Expected an array kind, received " ++ show kind

-- | Prefix a generated kind tag with its length so adjacent tags cannot
-- collide.
taggedKind :: String -> String
taggedKind value = show (length value) ++ "_" ++ value

-- | Encode an arbitrary Haskell type name as a valid C identifier component.
encodeIdentifier :: String -> String
encodeIdentifier = concatMap encode
 where encode character
         | isAscii character && isAlphaNum character = [character]
         | True                                      = "_x" ++ showHex (ord character) "" ++ "_"