module ProjectM36.AtomType where
import ProjectM36.Base
import qualified ProjectM36.TypeConstructorDef as TCD
import qualified ProjectM36.TypeConstructor as TC
import qualified ProjectM36.DataConstructorDef as DCD
import ProjectM36.MiscUtils
import ProjectM36.Error
import ProjectM36.DataTypes.Primitive
import ProjectM36.AttributeExpr as AE
import qualified ProjectM36.Attribute as A
import qualified Data.Vector as V
import qualified Data.Set as S
import qualified Data.List as L
import Data.Maybe (isJust)
import Data.Either (rights, lefts)
import Control.Monad (foldM, unless, when)
import qualified Data.Map as M
import qualified Data.Text as T

findDataConstructor :: DataConstructorName -> TypeConstructorMapping -> Maybe (TypeConstructorDef, DataConstructorDef)
findDataConstructor :: AttributeName
-> TypeConstructorMapping
-> Maybe (TypeConstructorDef, DataConstructorDef)
findDataConstructor AttributeName
dName = forall (t :: * -> *) a b.
Foldable t =>
(a -> b -> b) -> b -> t a -> b
foldr forall {a}.
(a, [DataConstructorDef])
-> Maybe (a, DataConstructorDef) -> Maybe (a, DataConstructorDef)
tConsFolder forall a. Maybe a
Nothing
  where
    tConsFolder :: (a, [DataConstructorDef])
-> Maybe (a, DataConstructorDef) -> Maybe (a, DataConstructorDef)
tConsFolder (a
tCons, [DataConstructorDef]
dConsList) Maybe (a, DataConstructorDef)
accum = if forall a. Maybe a -> Bool
isJust Maybe (a, DataConstructorDef)
accum then
                                Maybe (a, DataConstructorDef)
accum
                              else
                                case [DataConstructorDef] -> Maybe DataConstructorDef
findDCons [DataConstructorDef]
dConsList of
                                  Just DataConstructorDef
dCons -> forall a. a -> Maybe a
Just (a
tCons, DataConstructorDef
dCons)
                                  Maybe DataConstructorDef
Nothing -> forall a. Maybe a
Nothing
    findDCons :: [DataConstructorDef] -> Maybe DataConstructorDef
findDCons [DataConstructorDef]
dConsList = case forall a. (a -> Bool) -> [a] -> [a]
filter (\DataConstructorDef
dCons -> DataConstructorDef -> AttributeName
DCD.name DataConstructorDef
dCons forall a. Eq a => a -> a -> Bool
== AttributeName
dName) [DataConstructorDef]
dConsList of
      [] -> forall a. Maybe a
Nothing
      [DataConstructorDef
dCons] -> forall a. a -> Maybe a
Just DataConstructorDef
dCons
      [DataConstructorDef]
_ -> forall a. HasCallStack => [Char] -> a
error [Char]
"More than one data constructor with the same name found"
  
{-
-- | Scan the atom types and return the resultant ConstructedAtomType or error.
-- Used in typeFromAtomExpr to validate argument types.
atomTypeForDataConstructorName :: DataConstructorName -> [AtomType] -> TypeConstructorMapping -> Either RelationalError AtomType
-- search for the data constructor and resolve the types' names
atomTypeForDataConstructorName dConsName atomTypesIn tConsList =
  case findDataConstructor dConsName tConsList of
    Nothing -> Left (NoSuchDataConstructorError dConsName)
    Just (tCons, dCons) -> do
      dConsVars <- resolveDataConstructorTypeVars dCons atomTypesIn tConsList      
      let tConsVars = M.fromList (map TypeVariableType (TCD.typeVars tCons))
          allVars = M.union dConsVars tConsVars
      ConstructedAtomType (TCD.name tCons) <$> allVars
-}
        
atomTypeForDataConstructorDefArg :: DataConstructorDefArg -> AtomType -> TypeConstructorMapping ->  Either RelationalError AtomType
atomTypeForDataConstructorDefArg :: DataConstructorDefArg
-> AtomType
-> TypeConstructorMapping
-> Either RelationalError AtomType
atomTypeForDataConstructorDefArg (DataConstructorDefTypeConstructorArg TypeConstructor
tCons) AtomType
aType TypeConstructorMapping
tConss = do
  AtomType
-> TypeConstructor
-> TypeConstructorMapping
-> Either RelationalError ()
isValidAtomTypeForTypeConstructor AtomType
aType TypeConstructor
tCons TypeConstructorMapping
tConss
  forall (f :: * -> *) a. Applicative f => a -> f a
pure AtomType
aType

atomTypeForDataConstructorDefArg (DataConstructorDefTypeVarNameArg AttributeName
_) AtomType
aType TypeConstructorMapping
_ = forall a b. b -> Either a b
Right AtomType
aType --any type is OK
        
-- | Used to determine if the atom arguments can be used with the data constructor.  
-- | This is the entry point for type-checking from RelationalExpression.hs
atomTypeForDataConstructor :: TypeConstructorMapping -> DataConstructorName -> [AtomType] -> Either RelationalError AtomType
atomTypeForDataConstructor :: TypeConstructorMapping
-> AttributeName -> [AtomType] -> Either RelationalError AtomType
atomTypeForDataConstructor TypeConstructorMapping
tConss AttributeName
dConsName [AtomType]
atomArgTypes =
  --lookup the data constructor
  case AttributeName
-> TypeConstructorMapping
-> Maybe (TypeConstructorDef, DataConstructorDef)
findDataConstructor AttributeName
dConsName TypeConstructorMapping
tConss of
    Maybe (TypeConstructorDef, DataConstructorDef)
Nothing -> forall a b. a -> Either a b
Left (AttributeName -> RelationalError
NoSuchDataConstructorError AttributeName
dConsName)
    Just (TypeConstructorDef
tCons, DataConstructorDef
dCons) -> do
      --validate that the type constructor arguments are fulfilled in the data constructor
      TypeVarMap
dConsVars <- DataConstructorDef
-> [AtomType]
-> TypeConstructorMapping
-> Either RelationalError TypeVarMap
resolveDataConstructorTypeVars DataConstructorDef
dCons [AtomType]
atomArgTypes TypeConstructorMapping
tConss
      let tConsVars :: TypeVarMap
tConsVars = forall k a. Ord k => [(k, a)] -> Map k a
M.fromList (forall a b. (a -> b) -> [a] -> [b]
map (\AttributeName
v -> (AttributeName
v, AttributeName -> AtomType
TypeVariableType AttributeName
v)) (TypeConstructorDef -> [AttributeName]
TCD.typeVars TypeConstructorDef
tCons))
          allVars :: TypeVarMap
allVars = forall k a. Ord k => Map k a -> Map k a -> Map k a
M.union TypeVarMap
dConsVars TypeVarMap
tConsVars
          unresolvedType :: AtomType
unresolvedType = AttributeName -> TypeVarMap -> AtomType
ConstructedAtomType (TypeConstructorDef -> AttributeName
TCD.name TypeConstructorDef
tCons) TypeVarMap
allVars
      --validateAtomType unresolvedType tConss -- do not validate here because the type may not be fully resolved at this point
      forall (f :: * -> *) a. Applicative f => a -> f a
pure AtomType
unresolvedType
      
-- | Walks the data and type constructors to extract the type variable map.
resolveDataConstructorTypeVars :: DataConstructorDef -> [AtomType] -> TypeConstructorMapping -> Either RelationalError TypeVarMap
resolveDataConstructorTypeVars :: DataConstructorDef
-> [AtomType]
-> TypeConstructorMapping
-> Either RelationalError TypeVarMap
resolveDataConstructorTypeVars dCons :: DataConstructorDef
dCons@(DataConstructorDef AttributeName
_ [DataConstructorDefArg]
defArgs) [AtomType]
aTypeArgs TypeConstructorMapping
tConss = do
  let defCount :: Int
defCount = forall (t :: * -> *) a. Foldable t => t a -> Int
length [DataConstructorDefArg]
defArgs
      argCount :: Int
argCount = forall (t :: * -> *) a. Foldable t => t a -> Int
length [AtomType]
aTypeArgs
  if Int
defCount forall a. Eq a => a -> a -> Bool
/= Int
argCount then
    forall a b. a -> Either a b
Left (Int -> Int -> RelationalError
ConstructedAtomArgumentCountMismatchError Int
defCount Int
argCount)
    else do
    [TypeVarMap]
maps <- forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
mapM (\(DataConstructorDefArg
dCons',AtomType
aTypeArg) -> DataConstructorDefArg
-> AtomType
-> TypeConstructorMapping
-> Either RelationalError TypeVarMap
resolveDataConstructorArgTypeVars DataConstructorDefArg
dCons' AtomType
aTypeArg TypeConstructorMapping
tConss) (forall a b. [a] -> [b] -> [(a, b)]
zip (DataConstructorDef -> [DataConstructorDefArg]
DCD.fields DataConstructorDef
dCons) [AtomType]
aTypeArgs)
  --if any two maps have the same key and different values, this indicates a type arg mismatch
    let typeVarMapFolder :: TypeVarMap
-> Either RelationalError TypeVarMap
-> Either RelationalError TypeVarMap
typeVarMapFolder TypeVarMap
valMap Either RelationalError TypeVarMap
acc = case Either RelationalError TypeVarMap
acc of
          Left RelationalError
err -> forall a b. a -> Either a b
Left RelationalError
err
          Right TypeVarMap
accMap -> do
            case TypeVarMap -> TypeVarMap -> Either RelationalError TypeVarMap
resolveAtomTypesInTypeVarMap TypeVarMap
valMap TypeVarMap
accMap of
              Left (TypeConstructorTypeVarMissing AttributeName
_) -> forall a b. a -> Either a b
Left (AttributeName -> TypeVarMap -> TypeVarMap -> RelationalError
DataConstructorTypeVarsMismatch (DataConstructorDef -> AttributeName
DCD.name DataConstructorDef
dCons) TypeVarMap
accMap TypeVarMap
valMap)
              Left RelationalError
err -> forall a b. a -> Either a b
Left RelationalError
err
              Right TypeVarMap
ok -> forall (f :: * -> *) a. Applicative f => a -> f a
pure TypeVarMap
ok
    case forall (t :: * -> *) a b.
Foldable t =>
(a -> b -> b) -> b -> t a -> b
foldr TypeVarMap
-> Either RelationalError TypeVarMap
-> Either RelationalError TypeVarMap
typeVarMapFolder (forall a b. b -> Either a b
Right forall k a. Map k a
M.empty) [TypeVarMap]
maps of
      Left RelationalError
err -> forall a b. a -> Either a b
Left RelationalError
err
      Right TypeVarMap
typeVarMaps -> forall (f :: * -> *) a. Applicative f => a -> f a
pure TypeVarMap
typeVarMaps
  --if the data constructor cannot complete a type constructor variables (ex. "Nothing" could be Maybe Int or Maybe Text, etc.), then fill that space with TypeVar which is resolved when the relation is constructed- the relation must contain all resolved atom types.


-- | Attempt to match the data constructor argument to a type constructor type variable.
resolveDataConstructorArgTypeVars :: DataConstructorDefArg -> AtomType -> TypeConstructorMapping -> Either RelationalError TypeVarMap
resolveDataConstructorArgTypeVars :: DataConstructorDefArg
-> AtomType
-> TypeConstructorMapping
-> Either RelationalError TypeVarMap
resolveDataConstructorArgTypeVars (DataConstructorDefTypeConstructorArg TypeConstructor
tCons) AtomType
aType TypeConstructorMapping
tConss = TypeConstructor
-> AtomType
-> TypeConstructorMapping
-> Either RelationalError TypeVarMap
resolveTypeConstructorTypeVars TypeConstructor
tCons AtomType
aType TypeConstructorMapping
tConss
  
resolveDataConstructorArgTypeVars (DataConstructorDefTypeVarNameArg AttributeName
pVarName) AtomType
aType TypeConstructorMapping
_ = forall a b. b -> Either a b
Right (forall k a. k -> a -> Map k a
M.singleton AttributeName
pVarName AtomType
aType)

resolveTypeConstructorTypeVars :: TypeConstructor -> AtomType -> TypeConstructorMapping -> Either RelationalError TypeVarMap
resolveTypeConstructorTypeVars :: TypeConstructor
-> AtomType
-> TypeConstructorMapping
-> Either RelationalError TypeVarMap
resolveTypeConstructorTypeVars (PrimitiveTypeConstructor AttributeName
_ AtomType
pType) AtomType
aType TypeConstructorMapping
_ = 
  if AtomType
aType forall a. Eq a => a -> a -> Bool
/= AtomType
pType then
    forall a b. a -> Either a b
Left (AtomType -> AtomType -> RelationalError
AtomTypeMismatchError AtomType
pType AtomType
aType)
  else
    forall a b. b -> Either a b
Right forall k a. Map k a
M.empty

resolveTypeConstructorTypeVars (ADTypeConstructor AttributeName
tConsName [TypeConstructor]
_) (ConstructedAtomType AttributeName
tConsName' TypeVarMap
pVarMap') TypeConstructorMapping
tConss = 
  if AttributeName
tConsName forall a. Eq a => a -> a -> Bool
/= AttributeName
tConsName' then
    forall a b. a -> Either a b
Left (AttributeName -> AttributeName -> RelationalError
TypeConstructorNameMismatch AttributeName
tConsName AttributeName
tConsName')
  else
    case AttributeName
-> TypeConstructorMapping
-> Maybe (TypeConstructorDef, [DataConstructorDef])
findTypeConstructor AttributeName
tConsName TypeConstructorMapping
tConss of
      Maybe (TypeConstructorDef, [DataConstructorDef])
Nothing -> forall a b. a -> Either a b
Left (AttributeName -> RelationalError
NoSuchTypeConstructorName AttributeName
tConsName)
      Just (TypeConstructorDef
tConsDef, [DataConstructorDef]
_) -> let expectedPVarNames :: Set AttributeName
expectedPVarNames = forall a. Ord a => [a] -> Set a
S.fromList (TypeConstructorDef -> [AttributeName]
TCD.typeVars TypeConstructorDef
tConsDef) in
        if forall k a. Map k a -> Set k
M.keysSet TypeVarMap
pVarMap' forall a. Ord a => Set a -> Set a -> Bool
`S.isSubsetOf` Set AttributeName
expectedPVarNames then
          forall a b. b -> Either a b
Right TypeVarMap
pVarMap' 
        else
          forall a b. a -> Either a b
Left (Set AttributeName -> Set AttributeName -> RelationalError
TypeConstructorTypeVarsMismatch Set AttributeName
expectedPVarNames (forall k a. Map k a -> Set k
M.keysSet TypeVarMap
pVarMap'))
resolveTypeConstructorTypeVars (TypeVariable AttributeName
tvName) AtomType
typ TypeConstructorMapping
_ = case AtomType
typ of
  TypeVariableType AttributeName
nam -> forall a b. a -> Either a b
Left (AttributeName -> RelationalError
TypeConstructorTypeVarMissing AttributeName
nam)
  AtomType
_ -> forall a b. b -> Either a b
Right (forall k a. k -> a -> Map k a
M.singleton AttributeName
tvName AtomType
typ)
resolveTypeConstructorTypeVars (ADTypeConstructor AttributeName
tConsName []) AtomType
typ TypeConstructorMapping
tConss = case AttributeName
-> TypeConstructorMapping
-> Maybe (TypeConstructorDef, [DataConstructorDef])
findTypeConstructor AttributeName
tConsName TypeConstructorMapping
tConss of
  Just (PrimitiveTypeConstructorDef AttributeName
_ AtomType
_, [DataConstructorDef]
_) -> forall a b. b -> Either a b
Right forall k a. Map k a
M.empty
  Maybe (TypeConstructorDef, [DataConstructorDef])
_ -> forall a b. a -> Either a b
Left (AttributeName -> AtomType -> RelationalError
TypeConstructorAtomTypeMismatch AttributeName
tConsName AtomType
typ)

resolveTypeConstructorTypeVars (ADTypeConstructor AttributeName
tConsName [TypeConstructor]
_) AtomType
typ TypeConstructorMapping
_ = forall a b. a -> Either a b
Left (AttributeName -> AtomType -> RelationalError
TypeConstructorAtomTypeMismatch AttributeName
tConsName AtomType
typ)

resolveTypeConstructorTypeVars (RelationAtomTypeConstructor [AttributeExprBase ()]
attrExprs) AtomType
typ TypeConstructorMapping
tConsMap = 
  case AtomType
typ of
    RelationAtomType Attributes
attrs -> 
      --resolve any typevars in the attrExprs 
      forall (f :: * -> *) k a.
(Foldable f, Ord k) =>
f (Map k a) -> Map k a
M.unions forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
mapM (\(AtomType
expectedAtomType, AttributeExprBase ()
attrExpr) -> forall a.
AttributeExprBase a
-> AtomType
-> TypeConstructorMapping
-> Either RelationalError TypeVarMap
resolveAttributeExprTypeVars AttributeExprBase ()
attrExpr AtomType
expectedAtomType TypeConstructorMapping
tConsMap) (forall a b. [a] -> [b] -> [(a, b)]
zip (Attributes -> [AtomType]
A.atomTypesList Attributes
attrs) [AttributeExprBase ()]
attrExprs)
    AtomType
otherType -> forall a b. a -> Either a b
Left (AtomType -> AtomType -> RelationalError
AtomTypeMismatchError AtomType
typ AtomType
otherType)
      
--used when recursing down sub-relation type definition
resolveAttributeExprTypeVars :: AttributeExprBase a -> AtomType -> TypeConstructorMapping -> Either RelationalError TypeVarMap
resolveAttributeExprTypeVars :: forall a.
AttributeExprBase a
-> AtomType
-> TypeConstructorMapping
-> Either RelationalError TypeVarMap
resolveAttributeExprTypeVars (NakedAttributeExpr Attribute
attr) AtomType
aType TypeConstructorMapping
_ = forall (f :: * -> *) a. Applicative f => a -> f a
pure forall a b. (a -> b) -> a -> b
$ AtomType -> AtomType -> TypeVarMap
resolveTypeVariable (Attribute -> AtomType
A.atomType Attribute
attr) AtomType
aType
resolveAttributeExprTypeVars (AttributeAndTypeNameExpr AttributeName
_ TypeConstructor
tCons a
_) AtomType
aType TypeConstructorMapping
tConsMap = TypeConstructor
-> AtomType
-> TypeConstructorMapping
-> Either RelationalError TypeVarMap
resolveTypeConstructorTypeVars TypeConstructor
tCons AtomType
aType TypeConstructorMapping
tConsMap
    
-- check that type vars on the right also appear on the left
-- check that the data constructor names are unique      
validateTypeConstructorDef :: TypeConstructorDef -> [DataConstructorDef] -> TypeConstructorMapping -> Either RelationalError ()
validateTypeConstructorDef :: TypeConstructorDef
-> [DataConstructorDef]
-> TypeConstructorMapping
-> Either RelationalError ()
validateTypeConstructorDef TypeConstructorDef
tConsDef [DataConstructorDef]
dConsList TypeConstructorMapping
tConsMap = do
  let duplicateDConsNames :: [AttributeName]
duplicateDConsNames = forall a. Eq a => [a] -> [a]
dupes (forall a. Ord a => [a] -> [a]
L.sort (forall a b. (a -> b) -> [a] -> [b]
map DataConstructorDef -> AttributeName
DCD.name [DataConstructorDef]
dConsList))
  forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
unless (forall (t :: * -> *) a. Foldable t => t a -> Bool
null [AttributeName]
duplicateDConsNames) (forall a b. a -> Either a b
Left ([RelationalError] -> RelationalError
someErrors (forall a b. (a -> b) -> [a] -> [b]
map AttributeName -> RelationalError
DataConstructorNameInUseError [AttributeName]
duplicateDConsNames)))
  let leftSideVars :: Set AttributeName
leftSideVars = forall a. Ord a => [a] -> Set a
S.fromList (TypeConstructorDef -> [AttributeName]
TCD.typeVars TypeConstructorDef
tConsDef)
      rightSideVars :: Set AttributeName
rightSideVars = forall (f :: * -> *) a. (Foldable f, Ord a) => f (Set a) -> Set a
S.unions (forall a b. (a -> b) -> [a] -> [b]
map DataConstructorDef -> Set AttributeName
DCD.typeVars [DataConstructorDef]
dConsList)
      varsDiff :: Set AttributeName
varsDiff = forall a. Ord a => Set a -> Set a -> Set a
S.difference Set AttributeName
leftSideVars Set AttributeName
rightSideVars
  forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
when (forall a. Set a -> Int
S.size Set AttributeName
varsDiff forall a. Ord a => a -> a -> Bool
> Int
0) (forall a b. a -> Either a b
Left ([RelationalError] -> RelationalError
someErrors (forall a b. (a -> b) -> [a] -> [b]
map AttributeName -> RelationalError
DataConstructorUsesUndeclaredTypeVariable (forall a. Set a -> [a]
S.toList Set AttributeName
varsDiff))))
  forall (t :: * -> *) (m :: * -> *) a b.
(Foldable t, Monad m) =>
(a -> m b) -> t a -> m ()
mapM_ (\DataConstructorDef
dConsDef -> DataConstructorDef
-> TypeConstructorDef
-> TypeConstructorMapping
-> Either RelationalError ()
validateDataConstructorDef DataConstructorDef
dConsDef TypeConstructorDef
tConsDef TypeConstructorMapping
tConsMap) [DataConstructorDef]
dConsList

--check that the data constructor names are not in use (recursively)
validateDataConstructorDef :: DataConstructorDef -> TypeConstructorDef -> TypeConstructorMapping -> Either RelationalError ()
validateDataConstructorDef :: DataConstructorDef
-> TypeConstructorDef
-> TypeConstructorMapping
-> Either RelationalError ()
validateDataConstructorDef (DataConstructorDef AttributeName
dConsName [DataConstructorDefArg]
dConsDefArgs) TypeConstructorDef
tConsDef TypeConstructorMapping
tConsMap = 
  case AttributeName
-> TypeConstructorMapping
-> Maybe (TypeConstructorDef, DataConstructorDef)
findDataConstructor AttributeName
dConsName TypeConstructorMapping
tConsMap of
    Just (TypeConstructorDef, DataConstructorDef)
_ -> forall a b. a -> Either a b
Left (AttributeName -> RelationalError
DataConstructorNameInUseError AttributeName
dConsName)
    Maybe (TypeConstructorDef, DataConstructorDef)
Nothing ->
      forall (t :: * -> *) (m :: * -> *) a b.
(Foldable t, Monad m) =>
(a -> m b) -> t a -> m ()
mapM_ (\DataConstructorDefArg
arg -> DataConstructorDefArg
-> TypeConstructorDef
-> TypeConstructorMapping
-> Either RelationalError ()
validateDataConstructorDefArg DataConstructorDefArg
arg TypeConstructorDef
tConsDef TypeConstructorMapping
tConsMap) [DataConstructorDefArg]
dConsDefArgs


validateDataConstructorDefArg :: DataConstructorDefArg -> TypeConstructorDef -> TypeConstructorMapping -> Either RelationalError ()
validateDataConstructorDefArg :: DataConstructorDefArg
-> TypeConstructorDef
-> TypeConstructorMapping
-> Either RelationalError ()
validateDataConstructorDefArg (DataConstructorDefTypeConstructorArg (PrimitiveTypeConstructor AttributeName
_ AtomType
_)) TypeConstructorDef
_ TypeConstructorMapping
_ = forall a b. b -> Either a b
Right ()
validateDataConstructorDefArg (DataConstructorDefTypeConstructorArg (TypeVariable AttributeName
_)) TypeConstructorDef
_ TypeConstructorMapping
_ = forall a b. b -> Either a b
Right ()
validateDataConstructorDefArg (DataConstructorDefTypeConstructorArg TypeConstructor
tCons) TypeConstructorDef
tConsDef TypeConstructorMapping
tConsMap = case AttributeName
-> TypeConstructorMapping
-> Maybe (TypeConstructorDef, [DataConstructorDef])
findTypeConstructor (TypeConstructor -> AttributeName
TC.name TypeConstructor
tCons) TypeConstructorMapping
tConsMap of
  Maybe (TypeConstructorDef, [DataConstructorDef])
Nothing ->
    forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
when (TypeConstructor -> AttributeName
TC.name TypeConstructor
tCons forall a. Eq a => a -> a -> Bool
/= TypeConstructorDef -> AttributeName
TCD.name TypeConstructorDef
tConsDef) (forall a b. a -> Either a b
Left (AttributeName -> RelationalError
NoSuchTypeConstructorName (TypeConstructor -> AttributeName
TC.name TypeConstructor
tCons))) --allows for recursively-defined types
  Just (ADTypeConstructorDef AttributeName
_ [AttributeName]
tConsArgs, [DataConstructorDef]
_) -> do --validate that the argument count matches- type matching can occur later
    let existingCount :: Int
existingCount = forall (t :: * -> *) a. Foldable t => t a -> Int
length [AttributeName]
tConsArgs
        newCount :: Int
newCount = forall (t :: * -> *) a. Foldable t => t a -> Int
length (TypeConstructor -> [TypeConstructor]
TC.arguments TypeConstructor
tCons) 
    forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
when (Int
newCount forall a. Eq a => a -> a -> Bool
/= Int
existingCount) (forall a b. a -> Either a b
Left (Int -> Int -> RelationalError
ConstructedAtomArgumentCountMismatchError Int
existingCount Int
newCount))
  Just (PrimitiveTypeConstructorDef AttributeName
_ AtomType
_, [DataConstructorDef]
_) -> forall (f :: * -> *) a. Applicative f => a -> f a
pure ()  
validateDataConstructorDefArg (DataConstructorDefTypeVarNameArg AttributeName
_) TypeConstructorDef
_ TypeConstructorMapping
_ = forall a b. b -> Either a b
Right ()

atomTypeForTypeConstructor :: TypeConstructor -> TypeConstructorMapping -> TypeVarMap -> Either RelationalError AtomType
atomTypeForTypeConstructor :: TypeConstructor
-> TypeConstructorMapping
-> TypeVarMap
-> Either RelationalError AtomType
atomTypeForTypeConstructor = Bool
-> TypeConstructor
-> TypeConstructorMapping
-> TypeVarMap
-> Either RelationalError AtomType
atomTypeForTypeConstructorValidate Bool
False

-- | Create an atom type iff all type variables are provided.
-- Either Int Text -> ConstructedAtomType "Either" {Int , Text}
atomTypeForTypeConstructorValidate :: Bool -> TypeConstructor -> TypeConstructorMapping -> TypeVarMap -> Either RelationalError AtomType
atomTypeForTypeConstructorValidate :: Bool
-> TypeConstructor
-> TypeConstructorMapping
-> TypeVarMap
-> Either RelationalError AtomType
atomTypeForTypeConstructorValidate Bool
_ (PrimitiveTypeConstructor AttributeName
_ AtomType
aType) TypeConstructorMapping
_ TypeVarMap
_ = forall a b. b -> Either a b
Right AtomType
aType
atomTypeForTypeConstructorValidate Bool
validate (TypeVariable AttributeName
tvname) TypeConstructorMapping
_ TypeVarMap
tvMap = case forall k a. Ord k => k -> Map k a -> Maybe a
M.lookup AttributeName
tvname TypeVarMap
tvMap of
  Maybe AtomType
Nothing -> if Bool
validate then
                forall a b. a -> Either a b
Left (AttributeName -> RelationalError
TypeConstructorTypeVarMissing AttributeName
tvname)
             else
               forall (f :: * -> *) a. Applicative f => a -> f a
pure (AttributeName -> AtomType
TypeVariableType AttributeName
tvname)
  Just AtomType
typ -> forall a b. b -> Either a b
Right AtomType
typ
atomTypeForTypeConstructorValidate Bool
_ (RelationAtomTypeConstructor [AttributeExprBase ()]
attrExprs) TypeConstructorMapping
tConsMap TypeVarMap
tvMap = do
  [AtomType]
resolvedAtomTypes <- forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
mapM (\AttributeExprBase ()
expr -> forall a.
AttributeExprBase a
-> TypeConstructorMapping
-> TypeVarMap
-> Either RelationalError AtomType
atomTypeForAttributeExpr AttributeExprBase ()
expr TypeConstructorMapping
tConsMap TypeVarMap
tvMap) [AttributeExprBase ()]
attrExprs
  let attrs :: [Attribute]
attrs = forall a b c. (a -> b -> c) -> [a] -> [b] -> [c]
zipWith AttributeName -> AtomType -> Attribute
Attribute (forall a b. (a -> b) -> [a] -> [b]
map forall a. AttributeExprBase a -> AttributeName
AE.attributeName [AttributeExprBase ()]
attrExprs) [AtomType]
resolvedAtomTypes
  forall (f :: * -> *) a. Applicative f => a -> f a
pure (Attributes -> AtomType
RelationAtomType ([Attribute] -> Attributes
A.attributesFromList [Attribute]
attrs))
atomTypeForTypeConstructorValidate Bool
val TypeConstructor
tCons TypeConstructorMapping
tConss TypeVarMap
tvMap = case AttributeName
-> TypeConstructorMapping
-> Maybe (TypeConstructorDef, [DataConstructorDef])
findTypeConstructor (TypeConstructor -> AttributeName
TC.name TypeConstructor
tCons) TypeConstructorMapping
tConss of
  Maybe (TypeConstructorDef, [DataConstructorDef])
Nothing -> forall a b. a -> Either a b
Left (AttributeName -> RelationalError
NoSuchTypeConstructorError (TypeConstructor -> AttributeName
TC.name TypeConstructor
tCons))
  Just (PrimitiveTypeConstructorDef AttributeName
_ AtomType
aType, [DataConstructorDef]
_) -> forall a b. b -> Either a b
Right AtomType
aType
  Just (TypeConstructorDef
tConsDef, [DataConstructorDef]
_) -> do
          [AtomType]
tConsArgTypes <- forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
mapM (\TypeConstructor
tConsArg -> Bool
-> TypeConstructor
-> TypeConstructorMapping
-> TypeVarMap
-> Either RelationalError AtomType
atomTypeForTypeConstructorValidate Bool
val TypeConstructor
tConsArg TypeConstructorMapping
tConss TypeVarMap
tvMap) (TypeConstructor -> [TypeConstructor]
TC.arguments TypeConstructor
tCons)    
          let pVarNames :: [AttributeName]
pVarNames = TypeConstructorDef -> [AttributeName]
TCD.typeVars TypeConstructorDef
tConsDef
              tConsArgs :: TypeVarMap
tConsArgs = forall k a. Ord k => [(k, a)] -> Map k a
M.fromList (forall a b. [a] -> [b] -> [(a, b)]
zip [AttributeName]
pVarNames [AtomType]
tConsArgTypes)
          forall a b. b -> Either a b
Right (AttributeName -> TypeVarMap -> AtomType
ConstructedAtomType (TypeConstructor -> AttributeName
TC.name TypeConstructor
tCons) TypeVarMap
tConsArgs)      

      
atomTypeForAttributeExpr :: AttributeExprBase a -> TypeConstructorMapping -> TypeVarMap -> Either RelationalError AtomType      
atomTypeForAttributeExpr :: forall a.
AttributeExprBase a
-> TypeConstructorMapping
-> TypeVarMap
-> Either RelationalError AtomType
atomTypeForAttributeExpr (NakedAttributeExpr Attribute
attr) TypeConstructorMapping
_ TypeVarMap
_ = forall (f :: * -> *) a. Applicative f => a -> f a
pure (Attribute -> AtomType
A.atomType Attribute
attr)
atomTypeForAttributeExpr (AttributeAndTypeNameExpr AttributeName
_ TypeConstructor
tCons a
_) TypeConstructorMapping
tConsMap TypeVarMap
tvMap = Bool
-> TypeConstructor
-> TypeConstructorMapping
-> TypeVarMap
-> Either RelationalError AtomType
atomTypeForTypeConstructorValidate Bool
True TypeConstructor
tCons TypeConstructorMapping
tConsMap TypeVarMap
tvMap

--reconcile the atom-in types with the type constructors
isValidAtomTypeForTypeConstructor :: AtomType -> TypeConstructor -> TypeConstructorMapping -> Either RelationalError ()
isValidAtomTypeForTypeConstructor :: AtomType
-> TypeConstructor
-> TypeConstructorMapping
-> Either RelationalError ()
isValidAtomTypeForTypeConstructor AtomType
aType (PrimitiveTypeConstructor AttributeName
_ AtomType
expectedAType) TypeConstructorMapping
_ =
  forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
when (AtomType
expectedAType forall a. Eq a => a -> a -> Bool
/= AtomType
aType) forall a b. (a -> b) -> a -> b
$ forall a b. a -> Either a b
Left (AtomType -> AtomType -> RelationalError
AtomTypeMismatchError AtomType
expectedAType AtomType
aType)

--lookup constructor name and check if the incoming atom types are valid
isValidAtomTypeForTypeConstructor (ConstructedAtomType AttributeName
tConsName TypeVarMap
_) (ADTypeConstructor AttributeName
expectedTConsName [TypeConstructor]
_) TypeConstructorMapping
_ =  forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
when (AttributeName
tConsName forall a. Eq a => a -> a -> Bool
/= AttributeName
expectedTConsName) forall a b. (a -> b) -> a -> b
$ forall a b. a -> Either a b
Left (AttributeName -> AttributeName -> RelationalError
TypeConstructorNameMismatch AttributeName
expectedTConsName AttributeName
tConsName)

isValidAtomTypeForTypeConstructor (RelationAtomType Attributes
attrs) (RelationAtomTypeConstructor [AttributeExprBase ()]
attrExprs) TypeConstructorMapping
tConsMap = do
  [AtomType]
evaldAtomTypes <- forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
mapM (\AttributeExprBase ()
expr -> forall a.
AttributeExprBase a
-> TypeConstructorMapping
-> TypeVarMap
-> Either RelationalError AtomType
atomTypeForAttributeExpr AttributeExprBase ()
expr TypeConstructorMapping
tConsMap forall k a. Map k a
M.empty) [AttributeExprBase ()]
attrExprs
  forall (t :: * -> *) (m :: * -> *) a b.
(Foldable t, Monad m) =>
(a -> m b) -> t a -> m ()
mapM_ (forall a b c. (a -> b -> c) -> (a, b) -> c
uncurry AtomType -> AtomType -> Either RelationalError AtomType
resolveAtomType) (forall a b. [a] -> [b] -> [(a, b)]
zip (Attributes -> [AtomType]
A.atomTypesList Attributes
attrs) [AtomType]
evaldAtomTypes)
isValidAtomTypeForTypeConstructor AtomType
aType TypeConstructor
tCons TypeConstructorMapping
_ = forall a b. a -> Either a b
Left (AtomType -> AttributeName -> RelationalError
AtomTypeTypeConstructorReconciliationError AtomType
aType (TypeConstructor -> AttributeName
TC.name TypeConstructor
tCons))

findTypeConstructor :: TypeConstructorName -> TypeConstructorMapping -> Maybe (TypeConstructorDef, [DataConstructorDef])
findTypeConstructor :: AttributeName
-> TypeConstructorMapping
-> Maybe (TypeConstructorDef, [DataConstructorDef])
findTypeConstructor AttributeName
name = forall (t :: * -> *) a b.
Foldable t =>
(a -> b -> b) -> b -> t a -> b
foldr forall {b}.
(TypeConstructorDef, b)
-> Maybe (TypeConstructorDef, b) -> Maybe (TypeConstructorDef, b)
tConsFolder forall a. Maybe a
Nothing
  where
    tConsFolder :: (TypeConstructorDef, b)
-> Maybe (TypeConstructorDef, b) -> Maybe (TypeConstructorDef, b)
tConsFolder (TypeConstructorDef
tCons, b
dConsList) Maybe (TypeConstructorDef, b)
accum = if TypeConstructorDef -> AttributeName
TCD.name TypeConstructorDef
tCons forall a. Eq a => a -> a -> Bool
== AttributeName
name then
                                     forall a. a -> Maybe a
Just (TypeConstructorDef
tCons, b
dConsList)
                                   else
                                     Maybe (TypeConstructorDef, b)
accum

resolveAttributes :: Attribute -> Attribute -> Either RelationalError Attribute
resolveAttributes :: Attribute -> Attribute -> Either RelationalError Attribute
resolveAttributes Attribute
attrA Attribute
attrB =
  if Attribute -> AttributeName
A.attributeName Attribute
attrA forall a. Eq a => a -> a -> Bool
/= Attribute -> AttributeName
A.attributeName Attribute
attrB then
    forall a b. a -> Either a b
Left forall a b. (a -> b) -> a -> b
$ Set AttributeName -> RelationalError
AttributeNamesMismatchError (forall a. Ord a => [a] -> Set a
S.fromList (forall a b. (a -> b) -> [a] -> [b]
map Attribute -> AttributeName
A.attributeName [Attribute
attrA, Attribute
attrB]))
  else
    AttributeName -> AtomType -> Attribute
Attribute (Attribute -> AttributeName
A.attributeName Attribute
attrA) forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> AtomType -> AtomType -> Either RelationalError AtomType
resolveAtomType (Attribute -> AtomType
A.atomType Attribute
attrA) (Attribute -> AtomType
A.atomType Attribute
attrB)
    
--given two atom types, try to resolve type variables                                     
resolveAtomType :: AtomType -> AtomType -> Either RelationalError AtomType  
resolveAtomType :: AtomType -> AtomType -> Either RelationalError AtomType
resolveAtomType (ConstructedAtomType AttributeName
tConsName TypeVarMap
resolvedTypeVarMap) (ConstructedAtomType AttributeName
_ TypeVarMap
unresolvedTypeVarMap) = do
  AttributeName -> TypeVarMap -> AtomType
ConstructedAtomType AttributeName
tConsName forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> TypeVarMap -> TypeVarMap -> Either RelationalError TypeVarMap
resolveAtomTypesInTypeVarMap TypeVarMap
resolvedTypeVarMap TypeVarMap
unresolvedTypeVarMap 
resolveAtomType AtomType
typeFromRelation AtomType
unresolvedType = if AtomType
typeFromRelation forall a. Eq a => a -> a -> Bool
== AtomType
unresolvedType then
                                                    forall a b. b -> Either a b
Right AtomType
typeFromRelation
                                                  else
                                                    forall a b. a -> Either a b
Left (AtomType -> AtomType -> RelationalError
AtomTypeMismatchError AtomType
typeFromRelation AtomType
unresolvedType)
                                                    
{-
--walk an `AtomType` and apply the type variables in the map
resolveAtomTypeVars :: TypeVarMap -> AtomType -> AtomType   
resolveAtomTypeVars tvMap typ@(TypeVariableType nam) = fromMaybe typ (M.lookup nam tvMap)
resolveAtomTypeVars tvMap (RelationAtomType relAttrs) = 
-}                                                    
-- this could be optimized to reduce new tuple creation
resolveAtomTypesInTypeVarMap :: TypeVarMap -> TypeVarMap -> Either RelationalError TypeVarMap
resolveAtomTypesInTypeVarMap :: TypeVarMap -> TypeVarMap -> Either RelationalError TypeVarMap
resolveAtomTypesInTypeVarMap TypeVarMap
resolvedTypeMap TypeVarMap
unresolvedTypeMap = do
  {-
  let resKeySet = traceShowId $ M.keysSet resolvedTypeMap
      unresKeySet = traceShowId $ M.keysSet unresolvedTypeMap
  when (resKeySet /= unresKeySet) (Left $ TypeConstructorTypeVarsMismatch resKeySet unresKeySet)
  

  let lookupOrDef key tMap = case M.lookup key tMap of
        Nothing -> Left (TypeConstructorTypeVarMissing key)
        Just val -> Right val
  -}
  let resolveTypePair :: AttributeName
-> AtomType -> Either RelationalError (AttributeName, AtomType)
resolveTypePair AttributeName
resKey AtomType
resType =
        -- if the key is missing in the unresolved type map, then fill it in with the value from the resolved map
        case forall k a. Ord k => k -> Map k a -> Maybe a
M.lookup AttributeName
resKey TypeVarMap
unresolvedTypeMap of
          Just AtomType
unresType -> case AtomType
unresType of
            --do we need to recurse for RelationAtomType?
            subType :: AtomType
subType@(ConstructedAtomType AttributeName
_ TypeVarMap
_) -> do
              AtomType
resSubType <- AtomType -> AtomType -> Either RelationalError AtomType
resolveAtomType AtomType
resType AtomType
subType
              forall (f :: * -> *) a. Applicative f => a -> f a
pure (AttributeName
resKey, AtomType
resSubType)
            TypeVariableType AttributeName
_ -> forall (f :: * -> *) a. Applicative f => a -> f a
pure (AttributeName
resKey, AtomType
resType)
            -- in the data type F (Maybe Integer) (Maybe Integer), if the first Maybe Integer is "Nothing", then we want to prefer the concrete "unresolved type"- improvement: create different Haskell types for unresolved and concrete types using Void phantom type for TypeVariableType for concrete type
            AtomType
typ -> if AtomType -> Bool
isResolvedType AtomType
typ then
                       forall (f :: * -> *) a. Applicative f => a -> f a
pure (AttributeName
resKey, AtomType
typ)
                   else if AtomType -> Bool
isResolvedType AtomType
resType Bool -> Bool -> Bool
&& AtomType
typ forall a. Eq a => a -> a -> Bool
== AtomType
resType then
                       forall (f :: * -> *) a. Applicative f => a -> f a
pure (AttributeName
resKey, AtomType
resType)
                   else
                       forall a b. a -> Either a b
Left forall a b. (a -> b) -> a -> b
$ AtomType -> AtomType -> RelationalError
AtomTypeMismatchError AtomType
typ AtomType
resType
          Maybe AtomType
Nothing ->
            forall (f :: * -> *) a. Applicative f => a -> f a
pure (AttributeName
resKey, AtomType
resType) --swipe the missing type var from the expected map
  [(AttributeName, AtomType)]
tVarList <- forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
mapM (forall a b c. (a -> b -> c) -> (a, b) -> c
uncurry AttributeName
-> AtomType -> Either RelationalError (AttributeName, AtomType)
resolveTypePair) (forall k a. Map k a -> [(k, a)]
M.toList TypeVarMap
resolvedTypeMap)
  forall (f :: * -> *) a. Applicative f => a -> f a
pure (forall k a. Ord k => [(k, a)] -> Map k a
M.fromList [(AttributeName, AtomType)]
tVarList)
  
-- | See notes at `resolveTypesInTuple`. The typeFromRelation must not include any wildcards.
resolveTypeInAtom :: AtomType -> Atom -> TypeConstructorMapping -> Either RelationalError Atom
resolveTypeInAtom :: AtomType
-> Atom -> TypeConstructorMapping -> Either RelationalError Atom
resolveTypeInAtom typeFromRelation :: AtomType
typeFromRelation@(ConstructedAtomType AttributeName
_ TypeVarMap
tvMap) atomIn :: Atom
atomIn@(ConstructedAtom AttributeName
dConsName AtomType
_ [Atom]
args) TypeConstructorMapping
tConss = do
  AtomType
newType <- AtomType -> AtomType -> Either RelationalError AtomType
resolveAtomType AtomType
typeFromRelation (Atom -> AtomType
atomTypeForAtom Atom
atomIn)
  case AttributeName
-> TypeConstructorMapping
-> Maybe (TypeConstructorDef, DataConstructorDef)
findDataConstructor AttributeName
dConsName TypeConstructorMapping
tConss of
    Maybe (TypeConstructorDef, DataConstructorDef)
Nothing -> -- the atom may have been constructed using a constructor function without a public data constructor, no further resolution is possible
      forall (f :: * -> *) a. Applicative f => a -> f a
pure Atom
atomIn
    Just (TypeConstructorDef
_, DataConstructorDef
dConsDef) -> do
      [AtomType]
atomArgTypes <- TypeConstructorMapping
-> TypeVarMap
-> DataConstructorDef
-> Either RelationalError [AtomType]
resolvedAtomTypesForDataConstructorDefArgs TypeConstructorMapping
tConss TypeVarMap
tvMap DataConstructorDef
dConsDef
      [Atom]
newArgs <- forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
mapM (\(Atom
atom, AtomType
atomTyp) -> AtomType
-> Atom -> TypeConstructorMapping -> Either RelationalError Atom
resolveTypeInAtom AtomType
atomTyp Atom
atom TypeConstructorMapping
tConss) (forall a b. [a] -> [b] -> [(a, b)]
zip [Atom]
args [AtomType]
atomArgTypes)
      forall (f :: * -> *) a. Applicative f => a -> f a
pure (AttributeName -> AtomType -> [Atom] -> Atom
ConstructedAtom AttributeName
dConsName AtomType
newType [Atom]
newArgs)
resolveTypeInAtom (RelationAtomType Attributes
attrs) (RelationAtom (Relation Attributes
_ RelationTupleSet
tupSet)) TypeConstructorMapping
tConss = do
  let newTups :: Either RelationalError [RelationTuple]
newTups = forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
mapM (Attributes
-> TypeConstructorMapping
-> RelationTuple
-> Either RelationalError RelationTuple
resolveTypesInTuple Attributes
attrs TypeConstructorMapping
tConss) (RelationTupleSet -> [RelationTuple]
asList RelationTupleSet
tupSet)
  Relation -> Atom
RelationAtom forall b c a. (b -> c) -> (a -> b) -> a -> c
. Attributes -> RelationTupleSet -> Relation
Relation Attributes
attrs forall b c a. (b -> c) -> (a -> b) -> a -> c
. [RelationTuple] -> RelationTupleSet
RelationTupleSet forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Either RelationalError [RelationTuple]
newTups
resolveTypeInAtom AtomType
_ Atom
atom TypeConstructorMapping
_ = forall a b. b -> Either a b
Right Atom
atom
  
-- | When creating a tuple, the data constructor may not complete the type constructor arguments, so the wildcard "TypeVar x" fills in the type constructor's argument. The tuple type must be resolved before it can be part of a relation, however.
-- Example: "Nothing" does not specify the the argument in "Maybe a", so allow delayed resolution in the tuple before it is added to the relation. Note that this resolution could cause a type error. Hardly a Hindley-Milner system.
resolveTypesInTuple :: Attributes -> TypeConstructorMapping -> RelationTuple -> Either RelationalError RelationTuple
resolveTypesInTuple :: Attributes
-> TypeConstructorMapping
-> RelationTuple
-> Either RelationalError RelationTuple
resolveTypesInTuple Attributes
resolvedAttrs TypeConstructorMapping
tConss (RelationTuple Attributes
_ Vector Atom
tupAtoms) = do
  [Atom]
newAtoms <- forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
mapM (\(Atom
atom, AtomType
resolvedType) -> AtomType
-> Atom -> TypeConstructorMapping -> Either RelationalError Atom
resolveTypeInAtom AtomType
resolvedType Atom
atom TypeConstructorMapping
tConss) (forall a b. [a] -> [b] -> [(a, b)]
zip (forall a. Vector a -> [a]
V.toList Vector Atom
tupAtoms) forall a b. (a -> b) -> a -> b
$ Attributes -> [AtomType]
A.atomTypesList Attributes
resolvedAttrs)
  forall a b. b -> Either a b
Right (Attributes -> Vector Atom -> RelationTuple
RelationTuple Attributes
resolvedAttrs (forall a. [a] -> Vector a
V.fromList [Atom]
newAtoms))
                           
-- | Validate that the type is provided with complete type variables for type constructors.
validateAtomType :: AtomType -> TypeConstructorMapping -> Either RelationalError ()
validateAtomType :: AtomType -> TypeConstructorMapping -> Either RelationalError ()
validateAtomType (ConstructedAtomType AttributeName
tConsName TypeVarMap
tVarMap) TypeConstructorMapping
tConss =
  case AttributeName
-> TypeConstructorMapping
-> Maybe (TypeConstructorDef, [DataConstructorDef])
findTypeConstructor AttributeName
tConsName TypeConstructorMapping
tConss of 
    Maybe (TypeConstructorDef, [DataConstructorDef])
Nothing -> forall a b. a -> Either a b
Left (AttributeName -> RelationalError
NoSuchTypeConstructorError AttributeName
tConsName)
    Just (TypeConstructorDef
tConsDef, [DataConstructorDef]
_) -> case TypeConstructorDef
tConsDef of
      ADTypeConstructorDef AttributeName
_ [AttributeName]
tVarNames -> let expectedTyVarNames :: Set AttributeName
expectedTyVarNames = forall a. Ord a => [a] -> Set a
S.fromList [AttributeName]
tVarNames
                                              actualTyVarNames :: Set AttributeName
actualTyVarNames = forall k a. Map k a -> Set k
M.keysSet TypeVarMap
tVarMap
                                              diff :: Set AttributeName
diff = forall a. Ord a => Set a -> Set a -> Set a
S.difference Set AttributeName
expectedTyVarNames Set AttributeName
actualTyVarNames in
                                          if Bool -> Bool
not (forall a. Set a -> Bool
S.null Set AttributeName
diff) then
                                            forall a b. a -> Either a b
Left forall a b. (a -> b) -> a -> b
$ Set AttributeName -> Set AttributeName -> RelationalError
TypeConstructorTypeVarsMismatch Set AttributeName
expectedTyVarNames Set AttributeName
actualTyVarNames
                                          else
                                            TypeVarMap -> TypeConstructorMapping -> Either RelationalError ()
validateTypeVarMap TypeVarMap
tVarMap TypeConstructorMapping
tConss
      TypeConstructorDef
_ -> forall a b. b -> Either a b
Right ()
validateAtomType (RelationAtomType Attributes
attrs) TypeConstructorMapping
tConss =
  forall (t :: * -> *) (m :: * -> *) a b.
(Foldable t, Monad m) =>
(a -> m b) -> t a -> m ()
mapM_ (\Attribute
attr ->
         AtomType -> TypeConstructorMapping -> Either RelationalError ()
validateAtomType (Attribute -> AtomType
A.atomType Attribute
attr) TypeConstructorMapping
tConss) (Attributes -> Vector Attribute
attributesVec Attributes
attrs)
validateAtomType (TypeVariableType AttributeName
x) TypeConstructorMapping
_ = forall a b. a -> Either a b
Left (AttributeName -> RelationalError
TypeConstructorTypeVarMissing AttributeName
x)  
validateAtomType AtomType
_ TypeConstructorMapping
_ = forall (f :: * -> *) a. Applicative f => a -> f a
pure ()

validateAttributes :: TypeConstructorMapping -> Attributes -> Either RelationalError ()
validateAttributes :: TypeConstructorMapping -> Attributes -> Either RelationalError ()
validateAttributes TypeConstructorMapping
tConss Attributes
attrs =
  forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
unless (forall (t :: * -> *) a. Foldable t => t a -> Bool
null [RelationalError]
errs) forall a b. (a -> b) -> a -> b
$ forall a b. a -> Either a b
Left ([RelationalError] -> RelationalError
someErrors [RelationalError]
errs)
  where
    errs :: [RelationalError]
errs = forall a b. [Either a b] -> [a]
lefts forall a b. (a -> b) -> a -> b
$ forall a b. (a -> b) -> [a] -> [b]
map (AtomType -> TypeConstructorMapping -> Either RelationalError ()
`validateAtomType` TypeConstructorMapping
tConss) (Attributes -> [AtomType]
A.atomTypesList Attributes
attrs)

--ensure that all type vars are fully resolved
validateTypeVarMap :: TypeVarMap -> TypeConstructorMapping -> Either RelationalError ()
validateTypeVarMap :: TypeVarMap -> TypeConstructorMapping -> Either RelationalError ()
validateTypeVarMap TypeVarMap
tvMap TypeConstructorMapping
tConss = forall (t :: * -> *) (m :: * -> *) a b.
(Foldable t, Monad m) =>
(a -> m b) -> t a -> m ()
mapM_ (AtomType -> TypeConstructorMapping -> Either RelationalError ()
`validateAtomType` TypeConstructorMapping
tConss) forall a b. (a -> b) -> a -> b
$ forall k a. Map k a -> [a]
M.elems TypeVarMap
tvMap

validateTuple :: RelationTuple -> TypeConstructorMapping -> Either RelationalError ()
validateTuple :: RelationTuple
-> TypeConstructorMapping -> Either RelationalError ()
validateTuple (RelationTuple Attributes
_ Vector Atom
atoms) TypeConstructorMapping
tConss = forall (t :: * -> *) (m :: * -> *) a b.
(Foldable t, Monad m) =>
(a -> m b) -> t a -> m ()
mapM_ (Atom -> TypeConstructorMapping -> Either RelationalError ()
`validateAtom` TypeConstructorMapping
tConss) Vector Atom
atoms

--ensure that all types are fully resolved
validateAtom :: Atom -> TypeConstructorMapping -> Either RelationalError ()
validateAtom :: Atom -> TypeConstructorMapping -> Either RelationalError ()
validateAtom (RelationAtom (Relation Attributes
_ RelationTupleSet
tupSet)) TypeConstructorMapping
tConss = forall (t :: * -> *) (m :: * -> *) a b.
(Foldable t, Monad m) =>
(a -> m b) -> t a -> m ()
mapM_ (RelationTuple
-> TypeConstructorMapping -> Either RelationalError ()
`validateTuple` TypeConstructorMapping
tConss) (RelationTupleSet -> [RelationTuple]
asList RelationTupleSet
tupSet)
validateAtom (ConstructedAtom AttributeName
_ AtomType
dConsType [Atom]
atomArgs) TypeConstructorMapping
tConss = do
  AtomType -> TypeConstructorMapping -> Either RelationalError ()
validateAtomType AtomType
dConsType TypeConstructorMapping
tConss
  forall (t :: * -> *) (m :: * -> *) a b.
(Foldable t, Monad m) =>
(a -> m b) -> t a -> m ()
mapM_ (Atom -> TypeConstructorMapping -> Either RelationalError ()
`validateAtom` TypeConstructorMapping
tConss) [Atom]
atomArgs
validateAtom Atom
_ TypeConstructorMapping
_ = forall (f :: * -> *) a. Applicative f => a -> f a
pure ()
  

-- | Determine if two types are equal or compatible (including special handling for TypeVar x).
atomTypeVerify :: AtomType -> AtomType -> Either RelationalError AtomType
atomTypeVerify :: AtomType -> AtomType -> Either RelationalError AtomType
atomTypeVerify (TypeVariableType AttributeName
_) AtomType
x = forall a b. b -> Either a b
Right AtomType
x
atomTypeVerify AtomType
x (TypeVariableType AttributeName
_) = forall a b. b -> Either a b
Right AtomType
x
atomTypeVerify x :: AtomType
x@(ConstructedAtomType AttributeName
tConsNameA TypeVarMap
tVarMapA) (ConstructedAtomType AttributeName
tConsNameB TypeVarMap
tVarMapB) 
  | AttributeName
tConsNameA forall a. Eq a => a -> a -> Bool
/= AttributeName
tConsNameB = forall a b. a -> Either a b
Left (AttributeName -> AttributeName -> RelationalError
TypeConstructorNameMismatch AttributeName
tConsNameA AttributeName
tConsNameB)
  | Bool -> Bool
not (TypeVarMap -> TypeVarMap -> Bool
typeVarMapsVerify TypeVarMap
tVarMapA TypeVarMap
tVarMapB) = forall a b. a -> Either a b
Left (AttributeName -> TypeVarMap -> TypeVarMap -> RelationalError
TypeConstructorTypeVarsTypesMismatch AttributeName
tConsNameA TypeVarMap
tVarMapA TypeVarMap
tVarMapB)
  | Bool
otherwise = forall a b. b -> Either a b
Right AtomType
x

atomTypeVerify x :: AtomType
x@(RelationAtomType Attributes
attrs1) y :: AtomType
y@(RelationAtomType Attributes
attrs2) = do
  forall (t :: * -> *) (m :: * -> *) a b.
(Foldable t, Monad m) =>
(a -> m b) -> t a -> m ()
mapM_ (\(Attribute
attr1,Attribute
attr2) -> let name1 :: AttributeName
name1 = Attribute -> AttributeName
A.attributeName Attribute
attr1
                               name2 :: AttributeName
name2 = Attribute -> AttributeName
A.attributeName Attribute
attr2 in
                               if forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
notElem AttributeName
"_" [AttributeName
name1, AttributeName
name2] Bool -> Bool -> Bool
&& AttributeName
name1 forall a. Eq a => a -> a -> Bool
/= AttributeName
name2 then 
                                 forall a b. a -> Either a b
Left forall a b. (a -> b) -> a -> b
$ AtomType -> AtomType -> RelationalError
AtomTypeMismatchError AtomType
x AtomType
y
                               else
                                 AtomType -> AtomType -> Either RelationalError AtomType
atomTypeVerify (Attribute -> AtomType
A.atomType Attribute
attr1) (Attribute -> AtomType
A.atomType Attribute
attr2)) forall a b. (a -> b) -> a -> b
$ forall a. Vector a -> [a]
V.toList (forall a b. Vector a -> Vector b -> Vector (a, b)
V.zip (Attributes -> Vector Attribute
attributesVec Attributes
attrs1) (Attributes -> Vector Attribute
attributesVec Attributes
attrs2))
  forall (m :: * -> *) a. Monad m => a -> m a
return AtomType
x
atomTypeVerify (SubrelationFoldAtomType AtomType
typ1) (SubrelationFoldAtomType AtomType
typ2) = do
  AtomType
resTyp <- AtomType -> AtomType -> Either RelationalError AtomType
atomTypeVerify AtomType
typ1 AtomType
typ2
  forall (f :: * -> *) a. Applicative f => a -> f a
pure (AtomType -> AtomType
SubrelationFoldAtomType AtomType
resTyp)
atomTypeVerify AtomType
x AtomType
y = if AtomType
x forall a. Eq a => a -> a -> Bool
== AtomType
y then
                       forall a b. b -> Either a b
Right AtomType
x
                     else
                       forall a b. a -> Either a b
Left forall a b. (a -> b) -> a -> b
$ AtomType -> AtomType -> RelationalError
AtomTypeMismatchError AtomType
x AtomType
y

-- | Determine if two typeVars are logically compatible.
typeVarMapsVerify :: TypeVarMap -> TypeVarMap -> Bool
typeVarMapsVerify :: TypeVarMap -> TypeVarMap -> Bool
typeVarMapsVerify TypeVarMap
a TypeVarMap
b = forall k a. Map k a -> Set k
M.keysSet TypeVarMap
a forall a. Eq a => a -> a -> Bool
== forall k a. Map k a -> Set k
M.keysSet TypeVarMap
b Bool -> Bool -> Bool
&& (forall (t :: * -> *) a. Foldable t => t a -> Int
length forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a b. [Either a b] -> [b]
rights) [Either RelationalError AtomType]
zipped forall a. Eq a => a -> a -> Bool
== forall k a. Map k a -> Int
M.size TypeVarMap
a
  where
    zipped :: [Either RelationalError AtomType]
zipped = forall a b c. (a -> b -> c) -> [a] -> [b] -> [c]
zipWith
      (forall a b c. ((a, b) -> c) -> a -> b -> c
curry (\ ((AttributeName
_, AtomType
v1), (AttributeName
_, AtomType
v2)) -> AtomType -> AtomType -> Either RelationalError AtomType
atomTypeVerify AtomType
v1 AtomType
v2))
      (forall k a. Map k a -> [(k, a)]
M.toAscList TypeVarMap
a)
      (forall k a. Map k a -> [(k, a)]
M.toAscList TypeVarMap
b)

prettyAtomType :: AtomType -> T.Text
prettyAtomType :: AtomType -> AttributeName
prettyAtomType (RelationAtomType Attributes
attrs) = AttributeName
"relation {" AttributeName -> AttributeName -> AttributeName
`T.append` AttributeName -> [AttributeName] -> AttributeName
T.intercalate AttributeName
"," (forall a b. (a -> b) -> [a] -> [b]
map Attribute -> AttributeName
prettyAttribute (forall a. Vector a -> [a]
V.toList (Attributes -> Vector Attribute
attributesVec Attributes
attrs))) AttributeName -> AttributeName -> AttributeName
`T.append` AttributeName
"}"
prettyAtomType (ConstructedAtomType AttributeName
tConsName TypeVarMap
typeVarMap) = AttributeName
tConsName AttributeName -> AttributeName -> AttributeName
`T.append` [AttributeName] -> AttributeName
T.concat (forall a b. (a -> b) -> [a] -> [b]
map (AttributeName, AtomType) -> AttributeName
showTypeVars (forall k a. Map k a -> [(k, a)]
M.toList TypeVarMap
typeVarMap))
  where
    showTypeVars :: (AttributeName, AtomType) -> AttributeName
showTypeVars (AttributeName
_, TypeVariableType AttributeName
x) = AttributeName
" " forall a. Semigroup a => a -> a -> a
<> AttributeName
x
    showTypeVars (AttributeName
tyVarName, AtomType
aType) = AttributeName
" (" AttributeName -> AttributeName -> AttributeName
`T.append` AttributeName
tyVarName AttributeName -> AttributeName -> AttributeName
`T.append` AttributeName
"::" AttributeName -> AttributeName -> AttributeName
`T.append` AtomType -> AttributeName
prettyAtomType AtomType
aType AttributeName -> AttributeName -> AttributeName
`T.append` AttributeName
")"
-- it would be nice to have the original ordering, but we don't have access to the type constructor here- maybe the typevarmap should be also positional (ordered map?)
prettyAtomType (TypeVariableType AttributeName
x) = AttributeName
x
prettyAtomType AtomType
aType = Int -> AttributeName -> AttributeName
T.take (AttributeName -> Int
T.length AttributeName
fullName forall a. Num a => a -> a -> a
- AttributeName -> Int
T.length AttributeName
"AtomType") AttributeName
fullName
  where fullName :: AttributeName
fullName = ([Char] -> AttributeName
T.pack forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a. Show a => a -> [Char]
show) AtomType
aType

prettyAttribute :: Attribute -> T.Text
prettyAttribute :: Attribute -> AttributeName
prettyAttribute (Attribute AttributeName
_ (TypeVariableType AttributeName
x)) = AttributeName
x
prettyAttribute Attribute
attr = Attribute -> AttributeName
A.attributeName Attribute
attr AttributeName -> AttributeName -> AttributeName
`T.append` AttributeName
"::" AttributeName -> AttributeName -> AttributeName
`T.append` AtomType -> AttributeName
prettyAtomType (Attribute -> AtomType
A.atomType Attribute
attr)

resolveTypeVariables :: [AtomType] -> [AtomType] -> Either RelationalError TypeVarMap  
resolveTypeVariables :: [AtomType] -> [AtomType] -> Either RelationalError TypeVarMap
resolveTypeVariables [AtomType]
expectedArgTypes [AtomType]
actualArgTypes = do
  let tvmaps :: [TypeVarMap]
tvmaps = forall a b c. (a -> b -> c) -> [a] -> [b] -> [c]
zipWith AtomType -> AtomType -> TypeVarMap
resolveTypeVariable [AtomType]
expectedArgTypes [AtomType]
actualArgTypes
  --if there are any new keys which don't have equal values then we have a conflict!
  forall (t :: * -> *) (m :: * -> *) b a.
(Foldable t, Monad m) =>
(b -> a -> m b) -> b -> t a -> m b
foldM (\TypeVarMap
acc TypeVarMap
tvmap -> do
            let inter :: Map AttributeName (Either RelationalError AtomType)
inter = forall k a b c.
Ord k =>
(k -> a -> b -> c) -> Map k a -> Map k b -> Map k c
M.intersectionWithKey (\AttributeName
tvName AtomType
vala AtomType
valb -> 
                                                if AtomType
vala forall a. Eq a => a -> a -> Bool
/= AtomType
valb then
                                                  forall a b. a -> Either a b
Left (AttributeName -> AtomType -> AtomType -> RelationalError
AtomFunctionTypeVariableMismatch AttributeName
tvName AtomType
vala AtomType
valb)
                                                else
                                                  forall a b. b -> Either a b
Right AtomType
vala) TypeVarMap
acc TypeVarMap
tvmap
                errs :: [RelationalError]
errs = forall a b. [Either a b] -> [a]
lefts (forall k a. Map k a -> [a]
M.elems Map AttributeName (Either RelationalError AtomType)
inter)
            case [RelationalError]
errs of
              [] -> forall (f :: * -> *) a. Applicative f => a -> f a
pure (forall (f :: * -> *) k a.
(Foldable f, Ord k) =>
f (Map k a) -> Map k a
M.unions [TypeVarMap]
tvmaps)
              [RelationalError]
errs' -> forall a b. a -> Either a b
Left ([RelationalError] -> RelationalError
someErrors [RelationalError]
errs')) forall k a. Map k a
M.empty [TypeVarMap]
tvmaps
  
resolveTypeVariable :: AtomType -> AtomType -> TypeVarMap
resolveTypeVariable :: AtomType -> AtomType -> TypeVarMap
resolveTypeVariable (TypeVariableType AttributeName
tv) AtomType
typ = forall k a. k -> a -> Map k a
M.singleton AttributeName
tv AtomType
typ
resolveTypeVariable (ConstructedAtomType AttributeName
_ TypeVarMap
_) (ConstructedAtomType AttributeName
_ TypeVarMap
actualTvMap) = TypeVarMap
actualTvMap
resolveTypeVariable AtomType
_ AtomType
_ = forall k a. Map k a
M.empty

resolveFunctionReturnValue :: FunctionName -> TypeVarMap -> AtomType -> Either RelationalError AtomType
resolveFunctionReturnValue :: AttributeName
-> TypeVarMap -> AtomType -> Either RelationalError AtomType
resolveFunctionReturnValue AttributeName
funcName' TypeVarMap
tvMap ctype :: AtomType
ctype@(ConstructedAtomType AttributeName
tCons TypeVarMap
retMap) =
  if AtomType -> Bool
isResolvedType AtomType
ctype then
    forall (f :: * -> *) a. Applicative f => a -> f a
pure AtomType
ctype
    else do
    let diff :: TypeVarMap
diff = forall k a b. Ord k => Map k a -> Map k b -> Map k a
M.difference TypeVarMap
retMap TypeVarMap
tvMap
    case forall k a. Map k a -> [(k, a)]
M.toList TypeVarMap
diff of
      [] -> forall (f :: * -> *) a. Applicative f => a -> f a
pure (AttributeName -> TypeVarMap -> AtomType
ConstructedAtomType AttributeName
tCons (forall k a b. Ord k => Map k a -> Map k b -> Map k a
M.intersection TypeVarMap
tvMap TypeVarMap
retMap))
      (AttributeName, AtomType)
x : [(AttributeName, AtomType)]
_ -> forall a b. a -> Either a b
Left (AttributeName -> AttributeName -> RelationalError
AtomFunctionTypeVariableResolutionError AttributeName
funcName' (forall a b. (a, b) -> a
fst (AttributeName, AtomType)
x))
resolveFunctionReturnValue AttributeName
funcName' TypeVarMap
tvMap (TypeVariableType AttributeName
tvName) = case forall k a. Ord k => k -> Map k a -> Maybe a
M.lookup AttributeName
tvName TypeVarMap
tvMap of
  Maybe AtomType
Nothing -> forall a b. a -> Either a b
Left (AttributeName -> AttributeName -> RelationalError
AtomFunctionTypeVariableResolutionError AttributeName
funcName' AttributeName
tvName)
  Just AtomType
typ -> forall (f :: * -> *) a. Applicative f => a -> f a
pure AtomType
typ
resolveFunctionReturnValue AttributeName
_ TypeVarMap
_ AtomType
typ = forall (f :: * -> *) a. Applicative f => a -> f a
pure AtomType
typ

-- convert a typevarmap and data constructor definition into a list of atomtypes which represent the arguments-- no type variables are allowed to remain
resolvedAtomTypesForDataConstructorDefArgs :: TypeConstructorMapping -> TypeVarMap -> DataConstructorDef -> Either RelationalError [AtomType] 
resolvedAtomTypesForDataConstructorDefArgs :: TypeConstructorMapping
-> TypeVarMap
-> DataConstructorDef
-> Either RelationalError [AtomType]
resolvedAtomTypesForDataConstructorDefArgs TypeConstructorMapping
tConsMap TypeVarMap
tvMap (DataConstructorDef AttributeName
_ [DataConstructorDefArg]
args) = forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
mapM (TypeConstructorMapping
-> TypeVarMap
-> DataConstructorDefArg
-> Either RelationalError AtomType
resolvedAtomTypeForDataConstructorDefArg TypeConstructorMapping
tConsMap TypeVarMap
tvMap) [DataConstructorDefArg]
args

resolvedAtomTypeForDataConstructorDefArg :: TypeConstructorMapping -> TypeVarMap -> DataConstructorDefArg -> Either RelationalError AtomType
resolvedAtomTypeForDataConstructorDefArg :: TypeConstructorMapping
-> TypeVarMap
-> DataConstructorDefArg
-> Either RelationalError AtomType
resolvedAtomTypeForDataConstructorDefArg TypeConstructorMapping
tConsMap TypeVarMap
tvMap (DataConstructorDefTypeConstructorArg TypeConstructor
typCons) = TypeConstructor
-> TypeConstructorMapping
-> TypeVarMap
-> Either RelationalError AtomType
atomTypeForTypeConstructor TypeConstructor
typCons TypeConstructorMapping
tConsMap TypeVarMap
tvMap
resolvedAtomTypeForDataConstructorDefArg TypeConstructorMapping
_ TypeVarMap
tvMap (DataConstructorDefTypeVarNameArg AttributeName
tvName) = case forall k a. Ord k => k -> Map k a -> Maybe a
M.lookup AttributeName
tvName TypeVarMap
tvMap of
  Maybe AtomType
Nothing -> forall a b. a -> Either a b
Left (AttributeName -> RelationalError
DataConstructorUsesUndeclaredTypeVariable AttributeName
tvName)
  Just AtomType
typ -> forall a b. b -> Either a b
Right AtomType
typ

isResolvedType :: AtomType -> Bool
isResolvedType :: AtomType -> Bool
isResolvedType AtomType
typ =
  case AtomType
typ of
    AtomType
IntAtomType -> Bool
True
    AtomType
IntegerAtomType -> Bool
True
    AtomType
ScientificAtomType -> Bool
True
    AtomType
DoubleAtomType -> Bool
True
    AtomType
TextAtomType -> Bool
True
    AtomType
DayAtomType -> Bool
True
    AtomType
DateTimeAtomType -> Bool
True
    AtomType
ByteStringAtomType -> Bool
True
    AtomType
BoolAtomType -> Bool
True
    AtomType
UUIDAtomType -> Bool
True
    AtomType
RelationalExprAtomType -> Bool
True
    RelationAtomType Attributes
attrs -> Attributes -> Bool
isResolvedAttributes Attributes
attrs
    ConstructedAtomType AttributeName
_ TypeVarMap
tvMap -> forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
all AtomType -> Bool
isResolvedType (forall k a. Map k a -> [a]
M.elems TypeVarMap
tvMap)
    SubrelationFoldAtomType AtomType
typ' -> AtomType -> Bool
isResolvedType AtomType
typ'
    TypeVariableType AttributeName
_ -> Bool
False

isResolvedAttributes :: Attributes -> Bool
isResolvedAttributes :: Attributes -> Bool
isResolvedAttributes Attributes
attrs = forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
all Attribute -> Bool
isResolvedAttribute (forall a. Vector a -> [a]
V.toList (Attributes -> Vector Attribute
attributesVec Attributes
attrs))

isResolvedAttribute :: Attribute -> Bool
isResolvedAttribute :: Attribute -> Bool
isResolvedAttribute = AtomType -> Bool
isResolvedType forall b c a. (b -> c) -> (a -> b) -> a -> c
. Attribute -> AtomType
A.atomType

anyRelationAtomType :: AtomType
anyRelationAtomType :: AtomType
anyRelationAtomType = Attributes -> AtomType
RelationAtomType ([Attribute] -> Attributes
A.attributesFromList [AttributeName -> AtomType -> Attribute
Attribute AttributeName
"_" (AttributeName -> AtomType
TypeVariableType AttributeName
"a")])