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.Writer
import qualified Data.Map as M
import qualified Data.Text as T

findDataConstructor :: DataConstructorName -> TypeConstructorMapping -> Maybe (TypeConstructorDef, DataConstructorDef)
findDataConstructor :: TypeVarName
-> TypeConstructorMapping
-> Maybe (TypeConstructorDef, DataConstructorDef)
findDataConstructor TypeVarName
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 -> TypeVarName
DCD.name DataConstructorDef
dCons forall a. Eq a => a -> a -> Bool
== TypeVarName
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 TypeVarName
_) 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
-> TypeVarName -> [AtomType] -> Either RelationalError AtomType
atomTypeForDataConstructor TypeConstructorMapping
tConss TypeVarName
dConsName [AtomType]
atomArgTypes =
  --lookup the data constructor
  case TypeVarName
-> TypeConstructorMapping
-> Maybe (TypeConstructorDef, DataConstructorDef)
findDataConstructor TypeVarName
dConsName TypeConstructorMapping
tConss of
    Maybe (TypeConstructorDef, DataConstructorDef)
Nothing -> forall a b. a -> Either a b
Left (TypeVarName -> RelationalError
NoSuchDataConstructorError TypeVarName
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 (\TypeVarName
v -> (TypeVarName
v, TypeVarName -> AtomType
TypeVariableType TypeVarName
v)) (TypeConstructorDef -> [TypeVarName]
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 = TypeVarName -> TypeVarMap -> AtomType
ConstructedAtomType (TypeConstructorDef -> TypeVarName
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 TypeVarName
_ [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 -> 
            case TypeVarMap -> TypeVarMap -> Either RelationalError TypeVarMap
resolveAtomTypesInTypeVarMap TypeVarMap
valMap TypeVarMap
accMap of
              Left (TypeConstructorTypeVarMissing TypeVarName
_) -> forall a b. a -> Either a b
Left (TypeVarName -> TypeVarMap -> TypeVarMap -> RelationalError
DataConstructorTypeVarsMismatch (DataConstructorDef -> TypeVarName
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 TypeVarName
pVarName) AtomType
aType TypeConstructorMapping
_ = forall a b. b -> Either a b
Right (forall k a. k -> a -> Map k a
M.singleton TypeVarName
pVarName AtomType
aType)

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

resolveTypeConstructorTypeVars (ADTypeConstructor TypeVarName
tConsName [TypeConstructor]
_) AtomType
typ TypeConstructorMapping
_ = forall a b. a -> Either a b
Left (TypeVarName -> AtomType -> RelationalError
TypeConstructorAtomTypeMismatch TypeVarName
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 TypeVarName
_ 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 :: [TypeVarName]
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 -> TypeVarName
DCD.name [DataConstructorDef]
dConsList))
  forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
unless (forall (t :: * -> *) a. Foldable t => t a -> Bool
null [TypeVarName]
duplicateDConsNames) (forall a b. a -> Either a b
Left ([RelationalError] -> RelationalError
someErrors (forall a b. (a -> b) -> [a] -> [b]
map TypeVarName -> RelationalError
DataConstructorNameInUseError [TypeVarName]
duplicateDConsNames)))
  let leftSideVars :: Set TypeVarName
leftSideVars = forall a. Ord a => [a] -> Set a
S.fromList (TypeConstructorDef -> [TypeVarName]
TCD.typeVars TypeConstructorDef
tConsDef)
      rightSideVars :: Set TypeVarName
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 TypeVarName
DCD.typeVars [DataConstructorDef]
dConsList)
      varsDiff :: Set TypeVarName
varsDiff = forall a. Ord a => Set a -> Set a -> Set a
S.difference Set TypeVarName
leftSideVars Set TypeVarName
rightSideVars
  forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
when (forall a. Set a -> Int
S.size Set TypeVarName
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 TypeVarName -> RelationalError
DataConstructorUsesUndeclaredTypeVariable (forall a. Set a -> [a]
S.toList Set TypeVarName
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 TypeVarName
dConsName [DataConstructorDefArg]
dConsDefArgs) TypeConstructorDef
tConsDef TypeConstructorMapping
tConsMap = 
  case TypeVarName
-> TypeConstructorMapping
-> Maybe (TypeConstructorDef, DataConstructorDef)
findDataConstructor TypeVarName
dConsName TypeConstructorMapping
tConsMap of
    Just (TypeConstructorDef, DataConstructorDef)
_ -> forall a b. a -> Either a b
Left (TypeVarName -> RelationalError
DataConstructorNameInUseError TypeVarName
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 TypeVarName
_ AtomType
_)) TypeConstructorDef
_ TypeConstructorMapping
_ = forall a b. b -> Either a b
Right ()
validateDataConstructorDefArg (DataConstructorDefTypeConstructorArg (TypeVariable TypeVarName
_)) TypeConstructorDef
_ TypeConstructorMapping
_ = forall a b. b -> Either a b
Right ()
validateDataConstructorDefArg (DataConstructorDefTypeConstructorArg TypeConstructor
tCons) TypeConstructorDef
tConsDef TypeConstructorMapping
tConsMap = case TypeVarName
-> TypeConstructorMapping
-> Maybe (TypeConstructorDef, [DataConstructorDef])
findTypeConstructor (TypeConstructor -> TypeVarName
TC.name TypeConstructor
tCons) TypeConstructorMapping
tConsMap of
  Maybe (TypeConstructorDef, [DataConstructorDef])
Nothing ->
    forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
when (TypeConstructor -> TypeVarName
TC.name TypeConstructor
tCons forall a. Eq a => a -> a -> Bool
/= TypeConstructorDef -> TypeVarName
TCD.name TypeConstructorDef
tConsDef) (forall a b. a -> Either a b
Left (TypeVarName -> RelationalError
NoSuchTypeConstructorName (TypeConstructor -> TypeVarName
TC.name TypeConstructor
tCons))) --allows for recursively-defined types
  Just (ADTypeConstructorDef TypeVarName
_ [TypeVarName]
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 [TypeVarName]
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 TypeVarName
_ AtomType
_, [DataConstructorDef]
_) -> forall (f :: * -> *) a. Applicative f => a -> f a
pure ()  
validateDataConstructorDefArg (DataConstructorDefTypeVarNameArg TypeVarName
_) 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 TypeVarName
_ AtomType
aType) TypeConstructorMapping
_ TypeVarMap
_ = forall a b. b -> Either a b
Right AtomType
aType
atomTypeForTypeConstructorValidate Bool
validate (TypeVariable TypeVarName
tvname) TypeConstructorMapping
_ TypeVarMap
tvMap = case forall k a. Ord k => k -> Map k a -> Maybe a
M.lookup TypeVarName
tvname TypeVarMap
tvMap of
  Maybe AtomType
Nothing -> if Bool
validate then
                forall a b. a -> Either a b
Left (TypeVarName -> RelationalError
TypeConstructorTypeVarMissing TypeVarName
tvname)
             else
               forall (f :: * -> *) a. Applicative f => a -> f a
pure (TypeVarName -> AtomType
TypeVariableType TypeVarName
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 TypeVarName -> AtomType -> Attribute
Attribute (forall a b. (a -> b) -> [a] -> [b]
map forall a. AttributeExprBase a -> TypeVarName
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 TypeVarName
-> TypeConstructorMapping
-> Maybe (TypeConstructorDef, [DataConstructorDef])
findTypeConstructor (TypeConstructor -> TypeVarName
TC.name TypeConstructor
tCons) TypeConstructorMapping
tConss of
  Maybe (TypeConstructorDef, [DataConstructorDef])
Nothing -> forall a b. a -> Either a b
Left (TypeVarName -> RelationalError
NoSuchTypeConstructorError (TypeConstructor -> TypeVarName
TC.name TypeConstructor
tCons))
  Just (PrimitiveTypeConstructorDef TypeVarName
_ 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 :: [TypeVarName]
pVarNames = TypeConstructorDef -> [TypeVarName]
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 [TypeVarName]
pVarNames [AtomType]
tConsArgTypes)
          forall a b. b -> Either a b
Right (TypeVarName -> TypeVarMap -> AtomType
ConstructedAtomType (TypeConstructor -> TypeVarName
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 TypeVarName
_ 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 TypeVarName
_ 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 TypeVarName
tConsName TypeVarMap
_) (ADTypeConstructor TypeVarName
expectedTConsName [TypeConstructor]
_) TypeConstructorMapping
_ =  forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
when (TypeVarName
tConsName forall a. Eq a => a -> a -> Bool
/= TypeVarName
expectedTConsName) forall a b. (a -> b) -> a -> b
$ forall a b. a -> Either a b
Left (TypeVarName -> TypeVarName -> RelationalError
TypeConstructorNameMismatch TypeVarName
expectedTConsName TypeVarName
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 -> TypeVarName -> RelationalError
AtomTypeTypeConstructorReconciliationError AtomType
aType (TypeConstructor -> TypeVarName
TC.name TypeConstructor
tCons))

findTypeConstructor :: TypeConstructorName -> TypeConstructorMapping -> Maybe (TypeConstructorDef, [DataConstructorDef])
findTypeConstructor :: TypeVarName
-> TypeConstructorMapping
-> Maybe (TypeConstructorDef, [DataConstructorDef])
findTypeConstructor TypeVarName
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 -> TypeVarName
TCD.name TypeConstructorDef
tCons forall a. Eq a => a -> a -> Bool
== TypeVarName
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 -> TypeVarName
A.attributeName Attribute
attrA forall a. Eq a => a -> a -> Bool
/= Attribute -> TypeVarName
A.attributeName Attribute
attrB then
    forall a b. a -> Either a b
Left forall a b. (a -> b) -> a -> b
$ Set TypeVarName -> RelationalError
AttributeNamesMismatchError (forall a. Ord a => [a] -> Set a
S.fromList (forall a b. (a -> b) -> [a] -> [b]
map Attribute -> TypeVarName
A.attributeName [Attribute
attrA, Attribute
attrB]))
  else
    TypeVarName -> AtomType -> Attribute
Attribute (Attribute -> TypeVarName
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 TypeVarName
tConsName TypeVarMap
resolvedTypeVarMap) (ConstructedAtomType TypeVarName
_ TypeVarMap
unresolvedTypeVarMap) =
  TypeVarName -> TypeVarMap -> AtomType
ConstructedAtomType TypeVarName
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 :: TypeVarName
-> AtomType -> Either RelationalError (TypeVarName, AtomType)
resolveTypePair TypeVarName
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 TypeVarName
resKey TypeVarMap
unresolvedTypeMap of
          Just AtomType
unresType -> case AtomType
unresType of
            --do we need to recurse for RelationAtomType?
            subType :: AtomType
subType@(ConstructedAtomType TypeVarName
_ TypeVarMap
_) -> do
              AtomType
resSubType <- AtomType -> AtomType -> Either RelationalError AtomType
resolveAtomType AtomType
resType AtomType
subType
              forall (f :: * -> *) a. Applicative f => a -> f a
pure (TypeVarName
resKey, AtomType
resSubType)
            TypeVariableType TypeVarName
_ -> forall (f :: * -> *) a. Applicative f => a -> f a
pure (TypeVarName
resKey, AtomType
resType)
            AtomType
typ -> if AtomType
typ forall a. Eq a => a -> a -> Bool
== AtomType
resType then
                     forall (f :: * -> *) a. Applicative f => a -> f a
pure (TypeVarName
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 (TypeVarName
resKey, AtomType
resType) --swipe the missing type var from the expected map
  [(TypeVarName, 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 TypeVarName
-> AtomType -> Either RelationalError (TypeVarName, 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 [(TypeVarName, 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 TypeVarName
_ TypeVarMap
tvMap) atomIn :: Atom
atomIn@(ConstructedAtom TypeVarName
dConsName AtomType
_ [Atom]
args) TypeConstructorMapping
tConss = do
  AtomType
newType <- AtomType -> AtomType -> Either RelationalError AtomType
resolveAtomType AtomType
typeFromRelation (Atom -> AtomType
atomTypeForAtom Atom
atomIn)
  case TypeVarName
-> TypeConstructorMapping
-> Maybe (TypeConstructorDef, DataConstructorDef)
findDataConstructor TypeVarName
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 (TypeVarName -> AtomType -> [Atom] -> Atom
ConstructedAtom TypeVarName
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 TypeVarName
tConsName TypeVarMap
tVarMap) TypeConstructorMapping
tConss =
  case TypeVarName
-> TypeConstructorMapping
-> Maybe (TypeConstructorDef, [DataConstructorDef])
findTypeConstructor TypeVarName
tConsName TypeConstructorMapping
tConss of 
    Maybe (TypeConstructorDef, [DataConstructorDef])
Nothing -> forall a b. a -> Either a b
Left (TypeVarName -> RelationalError
NoSuchTypeConstructorError TypeVarName
tConsName)
    Just (TypeConstructorDef
tConsDef, [DataConstructorDef]
_) -> case TypeConstructorDef
tConsDef of
      ADTypeConstructorDef TypeVarName
_ [TypeVarName]
tVarNames -> let expectedTyVarNames :: Set TypeVarName
expectedTyVarNames = forall a. Ord a => [a] -> Set a
S.fromList [TypeVarName]
tVarNames
                                              actualTyVarNames :: Set TypeVarName
actualTyVarNames = forall k a. Map k a -> Set k
M.keysSet TypeVarMap
tVarMap
                                              diff :: Set TypeVarName
diff = forall a. Ord a => Set a -> Set a -> Set a
S.difference Set TypeVarName
expectedTyVarNames Set TypeVarName
actualTyVarNames in
                                          if Bool -> Bool
not (forall a. Set a -> Bool
S.null Set TypeVarName
diff) then
                                            forall a b. a -> Either a b
Left forall a b. (a -> b) -> a -> b
$ Set TypeVarName -> Set TypeVarName -> RelationalError
TypeConstructorTypeVarsMismatch Set TypeVarName
expectedTyVarNames Set TypeVarName
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 TypeVarName
x) TypeConstructorMapping
_ = forall a b. a -> Either a b
Left (TypeVarName -> RelationalError
TypeConstructorTypeVarMissing TypeVarName
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 TypeVarName
_ 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 TypeVarName
_) AtomType
x = forall a b. b -> Either a b
Right AtomType
x
atomTypeVerify AtomType
x (TypeVariableType TypeVarName
_) = forall a b. b -> Either a b
Right AtomType
x
atomTypeVerify x :: AtomType
x@(ConstructedAtomType TypeVarName
tConsNameA TypeVarMap
tVarMapA) (ConstructedAtomType TypeVarName
tConsNameB TypeVarMap
tVarMapB) 
  | TypeVarName
tConsNameA forall a. Eq a => a -> a -> Bool
/= TypeVarName
tConsNameB = forall a b. a -> Either a b
Left (TypeVarName -> TypeVarName -> RelationalError
TypeConstructorNameMismatch TypeVarName
tConsNameA TypeVarName
tConsNameB)
  | Bool -> Bool
not (TypeVarMap -> TypeVarMap -> Bool
typeVarMapsVerify TypeVarMap
tVarMapA TypeVarMap
tVarMapB) = forall a b. a -> Either a b
Left (TypeVarName -> TypeVarMap -> TypeVarMap -> RelationalError
TypeConstructorTypeVarsTypesMismatch TypeVarName
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 :: TypeVarName
name1 = Attribute -> TypeVarName
A.attributeName Attribute
attr1
                               name2 :: TypeVarName
name2 = Attribute -> TypeVarName
A.attributeName Attribute
attr2 in
                               if forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
notElem TypeVarName
"_" [TypeVarName
name1, TypeVarName
name2] Bool -> Bool -> Bool
&& TypeVarName
name1 forall a. Eq a => a -> a -> Bool
/= TypeVarName
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 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 (\ ((TypeVarName
_, AtomType
v1), (TypeVarName
_, 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 -> TypeVarName
prettyAtomType (RelationAtomType Attributes
attrs) = TypeVarName
"relation {" TypeVarName -> TypeVarName -> TypeVarName
`T.append` TypeVarName -> [TypeVarName] -> TypeVarName
T.intercalate TypeVarName
"," (forall a b. (a -> b) -> [a] -> [b]
map Attribute -> TypeVarName
prettyAttribute (forall a. Vector a -> [a]
V.toList (Attributes -> Vector Attribute
attributesVec Attributes
attrs))) TypeVarName -> TypeVarName -> TypeVarName
`T.append` TypeVarName
"}"
prettyAtomType (ConstructedAtomType TypeVarName
tConsName TypeVarMap
typeVarMap) = TypeVarName
tConsName TypeVarName -> TypeVarName -> TypeVarName
`T.append` [TypeVarName] -> TypeVarName
T.concat (forall a b. (a -> b) -> [a] -> [b]
map (TypeVarName, AtomType) -> TypeVarName
showTypeVars (forall k a. Map k a -> [(k, a)]
M.toList TypeVarMap
typeVarMap))
  where
    showTypeVars :: (TypeVarName, AtomType) -> TypeVarName
showTypeVars (TypeVarName
_, TypeVariableType TypeVarName
x) = TypeVarName
" " forall a. Semigroup a => a -> a -> a
<> TypeVarName
x
    showTypeVars (TypeVarName
tyVarName, AtomType
aType) = TypeVarName
" (" TypeVarName -> TypeVarName -> TypeVarName
`T.append` TypeVarName
tyVarName TypeVarName -> TypeVarName -> TypeVarName
`T.append` TypeVarName
"::" TypeVarName -> TypeVarName -> TypeVarName
`T.append` AtomType -> TypeVarName
prettyAtomType AtomType
aType TypeVarName -> TypeVarName -> TypeVarName
`T.append` TypeVarName
")"
-- 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 TypeVarName
x) = TypeVarName
x
prettyAtomType AtomType
aType = Int -> TypeVarName -> TypeVarName
T.take (TypeVarName -> Int
T.length TypeVarName
fullName forall a. Num a => a -> a -> a
- TypeVarName -> Int
T.length TypeVarName
"AtomType") TypeVarName
fullName
  where fullName :: TypeVarName
fullName = ([Char] -> TypeVarName
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 -> TypeVarName
prettyAttribute (Attribute TypeVarName
_ (TypeVariableType TypeVarName
x)) = TypeVarName
x
prettyAttribute Attribute
attr = Attribute -> TypeVarName
A.attributeName Attribute
attr TypeVarName -> TypeVarName -> TypeVarName
`T.append` TypeVarName
"::" TypeVarName -> TypeVarName -> TypeVarName
`T.append` AtomType -> TypeVarName
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 TypeVarName (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 (\TypeVarName
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 (TypeVarName -> AtomType -> AtomType -> RelationalError
AtomFunctionTypeVariableMismatch TypeVarName
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 TypeVarName (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 TypeVarName
tv) AtomType
typ = forall k a. k -> a -> Map k a
M.singleton TypeVarName
tv AtomType
typ
resolveTypeVariable (ConstructedAtomType TypeVarName
_ TypeVarMap
_) (ConstructedAtomType TypeVarName
_ TypeVarMap
actualTvMap) = TypeVarMap
actualTvMap
resolveTypeVariable AtomType
_ AtomType
_ = forall k a. Map k a
M.empty

resolveFunctionReturnValue :: FunctionName -> TypeVarMap -> AtomType -> Either RelationalError AtomType
resolveFunctionReturnValue :: TypeVarName
-> TypeVarMap -> AtomType -> Either RelationalError AtomType
resolveFunctionReturnValue TypeVarName
funcName' TypeVarMap
tvMap ctype :: AtomType
ctype@(ConstructedAtomType TypeVarName
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
    if forall k a. Map k a -> Bool
M.null TypeVarMap
diff then
      forall (f :: * -> *) a. Applicative f => a -> f a
pure (TypeVarName -> TypeVarMap -> AtomType
ConstructedAtomType TypeVarName
tCons (forall k a b. Ord k => Map k a -> Map k b -> Map k a
M.intersection TypeVarMap
tvMap TypeVarMap
retMap))
      else
      forall a b. a -> Either a b
Left (TypeVarName -> TypeVarName -> RelationalError
AtomFunctionTypeVariableResolutionError TypeVarName
funcName' (forall a b. (a, b) -> a
fst (forall a. [a] -> a
head (forall k a. Map k a -> [(k, a)]
M.toList TypeVarMap
diff))))
resolveFunctionReturnValue TypeVarName
funcName' TypeVarMap
tvMap (TypeVariableType TypeVarName
tvName) = case forall k a. Ord k => k -> Map k a -> Maybe a
M.lookup TypeVarName
tvName TypeVarMap
tvMap of
  Maybe AtomType
Nothing -> forall a b. a -> Either a b
Left (TypeVarName -> TypeVarName -> RelationalError
AtomFunctionTypeVariableResolutionError TypeVarName
funcName' TypeVarName
tvName)
  Just AtomType
typ -> forall (f :: * -> *) a. Applicative f => a -> f a
pure AtomType
typ
resolveFunctionReturnValue TypeVarName
_ 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 TypeVarName
_ [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 TypeVarName
tvName) = case forall k a. Ord k => k -> Map k a -> Maybe a
M.lookup TypeVarName
tvName TypeVarMap
tvMap of
  Maybe AtomType
Nothing -> forall a b. a -> Either a b
Left (TypeVarName -> RelationalError
DataConstructorUsesUndeclaredTypeVariable TypeVarName
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 TypeVarName
_ 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)
    TypeVariableType TypeVarName
_ -> 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

--given two AtomTypes x,y