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 :: DataConstructorName
-> TypeConstructorMapping
-> Maybe (TypeConstructorDef, DataConstructorDef)
findDataConstructor DataConstructorName
dName = ((TypeConstructorDef, [DataConstructorDef])
 -> Maybe (TypeConstructorDef, DataConstructorDef)
 -> Maybe (TypeConstructorDef, DataConstructorDef))
-> Maybe (TypeConstructorDef, DataConstructorDef)
-> TypeConstructorMapping
-> Maybe (TypeConstructorDef, DataConstructorDef)
forall (t :: * -> *) a b.
Foldable t =>
(a -> b -> b) -> b -> t a -> b
foldr (TypeConstructorDef, [DataConstructorDef])
-> Maybe (TypeConstructorDef, DataConstructorDef)
-> Maybe (TypeConstructorDef, DataConstructorDef)
forall a.
(a, [DataConstructorDef])
-> Maybe (a, DataConstructorDef) -> Maybe (a, DataConstructorDef)
tConsFolder Maybe (TypeConstructorDef, DataConstructorDef)
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 Maybe (a, DataConstructorDef) -> Bool
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 -> (a, DataConstructorDef) -> Maybe (a, DataConstructorDef)
forall a. a -> Maybe a
Just (a
tCons, DataConstructorDef
dCons)
                                  Maybe DataConstructorDef
Nothing -> Maybe (a, DataConstructorDef)
forall a. Maybe a
Nothing
    findDCons :: [DataConstructorDef] -> Maybe DataConstructorDef
findDCons [DataConstructorDef]
dConsList = case (DataConstructorDef -> Bool)
-> [DataConstructorDef] -> [DataConstructorDef]
forall a. (a -> Bool) -> [a] -> [a]
filter (\DataConstructorDef
dCons -> DataConstructorDef -> DataConstructorName
DCD.name DataConstructorDef
dCons DataConstructorName -> DataConstructorName -> Bool
forall a. Eq a => a -> a -> Bool
== DataConstructorName
dName) [DataConstructorDef]
dConsList of
      [] -> Maybe DataConstructorDef
forall a. Maybe a
Nothing
      [DataConstructorDef
dCons] -> DataConstructorDef -> Maybe DataConstructorDef
forall a. a -> Maybe a
Just DataConstructorDef
dCons
      [DataConstructorDef]
_ -> [Char] -> Maybe 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
  AtomType -> Either RelationalError AtomType
forall (f :: * -> *) a. Applicative f => a -> f a
pure AtomType
aType

atomTypeForDataConstructorDefArg (DataConstructorDefTypeVarNameArg DataConstructorName
_) AtomType
aType TypeConstructorMapping
_ = AtomType -> Either RelationalError AtomType
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
-> DataConstructorName
-> [AtomType]
-> Either RelationalError AtomType
atomTypeForDataConstructor TypeConstructorMapping
tConss DataConstructorName
dConsName [AtomType]
atomArgTypes =
  --lookup the data constructor
  case DataConstructorName
-> TypeConstructorMapping
-> Maybe (TypeConstructorDef, DataConstructorDef)
findDataConstructor DataConstructorName
dConsName TypeConstructorMapping
tConss of
    Maybe (TypeConstructorDef, DataConstructorDef)
Nothing -> RelationalError -> Either RelationalError AtomType
forall a b. a -> Either a b
Left (DataConstructorName -> RelationalError
NoSuchDataConstructorError DataConstructorName
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 = [(DataConstructorName, AtomType)] -> TypeVarMap
forall k a. Ord k => [(k, a)] -> Map k a
M.fromList ((DataConstructorName -> (DataConstructorName, AtomType))
-> [DataConstructorName] -> [(DataConstructorName, AtomType)]
forall a b. (a -> b) -> [a] -> [b]
map (\DataConstructorName
v -> (DataConstructorName
v, DataConstructorName -> AtomType
TypeVariableType DataConstructorName
v)) (TypeConstructorDef -> [DataConstructorName]
TCD.typeVars TypeConstructorDef
tCons))
          allVars :: TypeVarMap
allVars = TypeVarMap -> TypeVarMap -> TypeVarMap
forall k a. Ord k => Map k a -> Map k a -> Map k a
M.union TypeVarMap
dConsVars TypeVarMap
tConsVars
          unresolvedType :: AtomType
unresolvedType = DataConstructorName -> TypeVarMap -> AtomType
ConstructedAtomType (TypeConstructorDef -> DataConstructorName
TCD.name TypeConstructorDef
tCons) TypeVarMap
allVars
      --validateAtomType unresolvedType tConss -- do not validate here because the type may not be fully resolved at this point
      AtomType -> Either RelationalError AtomType
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 DataConstructorName
_ [DataConstructorDefArg]
defArgs) [AtomType]
aTypeArgs TypeConstructorMapping
tConss = do
  let defCount :: Int
defCount = [DataConstructorDefArg] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length [DataConstructorDefArg]
defArgs
      argCount :: Int
argCount = [AtomType] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length [AtomType]
aTypeArgs
  if Int
defCount Int -> Int -> Bool
forall a. Eq a => a -> a -> Bool
/= Int
argCount then
    RelationalError -> Either RelationalError TypeVarMap
forall a b. a -> Either a b
Left (Int -> Int -> RelationalError
ConstructedAtomArgumentCountMismatchError Int
defCount Int
argCount)
    else do
    [TypeVarMap]
maps <- ((DataConstructorDefArg, AtomType)
 -> Either RelationalError TypeVarMap)
-> [(DataConstructorDefArg, AtomType)]
-> Either RelationalError [TypeVarMap]
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) ([DataConstructorDefArg]
-> [AtomType] -> [(DataConstructorDefArg, AtomType)]
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 -> RelationalError -> Either RelationalError TypeVarMap
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 DataConstructorName
_) -> RelationalError -> Either RelationalError TypeVarMap
forall a b. a -> Either a b
Left (DataConstructorName -> TypeVarMap -> TypeVarMap -> RelationalError
DataConstructorTypeVarsMismatch (DataConstructorDef -> DataConstructorName
DCD.name DataConstructorDef
dCons) TypeVarMap
accMap TypeVarMap
valMap)
              Left RelationalError
err -> RelationalError -> Either RelationalError TypeVarMap
forall a b. a -> Either a b
Left RelationalError
err
              Right TypeVarMap
ok -> TypeVarMap -> Either RelationalError TypeVarMap
forall (f :: * -> *) a. Applicative f => a -> f a
pure TypeVarMap
ok
    case (TypeVarMap
 -> Either RelationalError TypeVarMap
 -> Either RelationalError TypeVarMap)
-> Either RelationalError TypeVarMap
-> [TypeVarMap]
-> Either RelationalError TypeVarMap
forall (t :: * -> *) a b.
Foldable t =>
(a -> b -> b) -> b -> t a -> b
foldr TypeVarMap
-> Either RelationalError TypeVarMap
-> Either RelationalError TypeVarMap
typeVarMapFolder (TypeVarMap -> Either RelationalError TypeVarMap
forall a b. b -> Either a b
Right TypeVarMap
forall k a. Map k a
M.empty) [TypeVarMap]
maps of
      Left RelationalError
err -> RelationalError -> Either RelationalError TypeVarMap
forall a b. a -> Either a b
Left RelationalError
err
      Right TypeVarMap
typeVarMaps -> TypeVarMap -> Either RelationalError TypeVarMap
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 DataConstructorName
pVarName) AtomType
aType TypeConstructorMapping
_ = TypeVarMap -> Either RelationalError TypeVarMap
forall a b. b -> Either a b
Right (DataConstructorName -> AtomType -> TypeVarMap
forall k a. k -> a -> Map k a
M.singleton DataConstructorName
pVarName AtomType
aType)

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

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

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

resolveTypeConstructorTypeVars (RelationAtomTypeConstructor [AttributeExprBase ()]
attrExprs) AtomType
typ TypeConstructorMapping
tConsMap = 
  case AtomType
typ of
    RelationAtomType Attributes
attrs -> 
      --resolve any typevars in the attrExprs 
      [TypeVarMap] -> TypeVarMap
forall (f :: * -> *) k a.
(Foldable f, Ord k) =>
f (Map k a) -> Map k a
M.unions ([TypeVarMap] -> TypeVarMap)
-> Either RelationalError [TypeVarMap]
-> Either RelationalError TypeVarMap
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> ((AtomType, AttributeExprBase ())
 -> Either RelationalError TypeVarMap)
-> [(AtomType, AttributeExprBase ())]
-> Either RelationalError [TypeVarMap]
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
mapM (\(AtomType
expectedAtomType, AttributeExprBase ()
attrExpr) -> AttributeExprBase ()
-> AtomType
-> TypeConstructorMapping
-> Either RelationalError TypeVarMap
forall a.
AttributeExprBase a
-> AtomType
-> TypeConstructorMapping
-> Either RelationalError TypeVarMap
resolveAttributeExprTypeVars AttributeExprBase ()
attrExpr AtomType
expectedAtomType TypeConstructorMapping
tConsMap) ([AtomType]
-> [AttributeExprBase ()] -> [(AtomType, AttributeExprBase ())]
forall a b. [a] -> [b] -> [(a, b)]
zip (Attributes -> [AtomType]
A.atomTypesList Attributes
attrs) [AttributeExprBase ()]
attrExprs)
    AtomType
otherType -> RelationalError -> Either RelationalError TypeVarMap
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 :: AttributeExprBase a
-> AtomType
-> TypeConstructorMapping
-> Either RelationalError TypeVarMap
resolveAttributeExprTypeVars (NakedAttributeExpr Attribute
attr) AtomType
aType TypeConstructorMapping
_ = TypeVarMap -> Either RelationalError TypeVarMap
forall (f :: * -> *) a. Applicative f => a -> f a
pure (TypeVarMap -> Either RelationalError TypeVarMap)
-> TypeVarMap -> Either RelationalError TypeVarMap
forall a b. (a -> b) -> a -> b
$ AtomType -> AtomType -> TypeVarMap
resolveTypeVariable (Attribute -> AtomType
A.atomType Attribute
attr) AtomType
aType
resolveAttributeExprTypeVars (AttributeAndTypeNameExpr DataConstructorName
_ 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 :: [DataConstructorName]
duplicateDConsNames = [DataConstructorName] -> [DataConstructorName]
forall a. Eq a => [a] -> [a]
dupes ([DataConstructorName] -> [DataConstructorName]
forall a. Ord a => [a] -> [a]
L.sort ((DataConstructorDef -> DataConstructorName)
-> [DataConstructorDef] -> [DataConstructorName]
forall a b. (a -> b) -> [a] -> [b]
map DataConstructorDef -> DataConstructorName
DCD.name [DataConstructorDef]
dConsList))
  Bool -> Either RelationalError () -> Either RelationalError ()
forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
unless ([DataConstructorName] -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null [DataConstructorName]
duplicateDConsNames) (RelationalError -> Either RelationalError ()
forall a b. a -> Either a b
Left ([RelationalError] -> RelationalError
someErrors ((DataConstructorName -> RelationalError)
-> [DataConstructorName] -> [RelationalError]
forall a b. (a -> b) -> [a] -> [b]
map DataConstructorName -> RelationalError
DataConstructorNameInUseError [DataConstructorName]
duplicateDConsNames)))
  let leftSideVars :: Set DataConstructorName
leftSideVars = [DataConstructorName] -> Set DataConstructorName
forall a. Ord a => [a] -> Set a
S.fromList (TypeConstructorDef -> [DataConstructorName]
TCD.typeVars TypeConstructorDef
tConsDef)
      rightSideVars :: Set DataConstructorName
rightSideVars = [Set DataConstructorName] -> Set DataConstructorName
forall (f :: * -> *) a. (Foldable f, Ord a) => f (Set a) -> Set a
S.unions ((DataConstructorDef -> Set DataConstructorName)
-> [DataConstructorDef] -> [Set DataConstructorName]
forall a b. (a -> b) -> [a] -> [b]
map DataConstructorDef -> Set DataConstructorName
DCD.typeVars [DataConstructorDef]
dConsList)
      varsDiff :: Set DataConstructorName
varsDiff = Set DataConstructorName
-> Set DataConstructorName -> Set DataConstructorName
forall a. Ord a => Set a -> Set a -> Set a
S.difference Set DataConstructorName
leftSideVars Set DataConstructorName
rightSideVars
  Bool -> Either RelationalError () -> Either RelationalError ()
forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
when (Set DataConstructorName -> Int
forall a. Set a -> Int
S.size Set DataConstructorName
varsDiff Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
> Int
0) (RelationalError -> Either RelationalError ()
forall a b. a -> Either a b
Left ([RelationalError] -> RelationalError
someErrors ((DataConstructorName -> RelationalError)
-> [DataConstructorName] -> [RelationalError]
forall a b. (a -> b) -> [a] -> [b]
map DataConstructorName -> RelationalError
DataConstructorUsesUndeclaredTypeVariable (Set DataConstructorName -> [DataConstructorName]
forall a. Set a -> [a]
S.toList Set DataConstructorName
varsDiff))))
  (DataConstructorDef -> Either RelationalError ())
-> [DataConstructorDef] -> Either RelationalError ()
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 DataConstructorName
dConsName [DataConstructorDefArg]
dConsDefArgs) TypeConstructorDef
tConsDef TypeConstructorMapping
tConsMap = 
  case DataConstructorName
-> TypeConstructorMapping
-> Maybe (TypeConstructorDef, DataConstructorDef)
findDataConstructor DataConstructorName
dConsName TypeConstructorMapping
tConsMap of
    Just (TypeConstructorDef, DataConstructorDef)
_ -> RelationalError -> Either RelationalError ()
forall a b. a -> Either a b
Left (DataConstructorName -> RelationalError
DataConstructorNameInUseError DataConstructorName
dConsName)
    Maybe (TypeConstructorDef, DataConstructorDef)
Nothing ->
      (DataConstructorDefArg -> Either RelationalError ())
-> [DataConstructorDefArg] -> Either RelationalError ()
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 DataConstructorName
_ AtomType
_)) TypeConstructorDef
_ TypeConstructorMapping
_ = () -> Either RelationalError ()
forall a b. b -> Either a b
Right ()
validateDataConstructorDefArg (DataConstructorDefTypeConstructorArg (TypeVariable DataConstructorName
_)) TypeConstructorDef
_ TypeConstructorMapping
_ = () -> Either RelationalError ()
forall a b. b -> Either a b
Right ()
validateDataConstructorDefArg (DataConstructorDefTypeConstructorArg TypeConstructor
tCons) TypeConstructorDef
tConsDef TypeConstructorMapping
tConsMap = case DataConstructorName
-> TypeConstructorMapping
-> Maybe (TypeConstructorDef, [DataConstructorDef])
findTypeConstructor (TypeConstructor -> DataConstructorName
TC.name TypeConstructor
tCons) TypeConstructorMapping
tConsMap of
  Maybe (TypeConstructorDef, [DataConstructorDef])
Nothing ->
    Bool -> Either RelationalError () -> Either RelationalError ()
forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
when (TypeConstructor -> DataConstructorName
TC.name TypeConstructor
tCons DataConstructorName -> DataConstructorName -> Bool
forall a. Eq a => a -> a -> Bool
/= TypeConstructorDef -> DataConstructorName
TCD.name TypeConstructorDef
tConsDef) (RelationalError -> Either RelationalError ()
forall a b. a -> Either a b
Left (DataConstructorName -> RelationalError
NoSuchTypeConstructorName (TypeConstructor -> DataConstructorName
TC.name TypeConstructor
tCons))) --allows for recursively-defined types
  Just (ADTypeConstructorDef DataConstructorName
_ [DataConstructorName]
tConsArgs, [DataConstructorDef]
_) -> do --validate that the argument count matches- type matching can occur later
    let existingCount :: Int
existingCount = [DataConstructorName] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length [DataConstructorName]
tConsArgs
        newCount :: Int
newCount = [TypeConstructor] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length (TypeConstructor -> [TypeConstructor]
TC.arguments TypeConstructor
tCons) 
    Bool -> Either RelationalError () -> Either RelationalError ()
forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
when (Int
newCount Int -> Int -> Bool
forall a. Eq a => a -> a -> Bool
/= Int
existingCount) (RelationalError -> Either RelationalError ()
forall a b. a -> Either a b
Left (Int -> Int -> RelationalError
ConstructedAtomArgumentCountMismatchError Int
existingCount Int
newCount))
  Just (PrimitiveTypeConstructorDef DataConstructorName
_ AtomType
_, [DataConstructorDef]
_) -> () -> Either RelationalError ()
forall (f :: * -> *) a. Applicative f => a -> f a
pure ()  
validateDataConstructorDefArg (DataConstructorDefTypeVarNameArg DataConstructorName
_) TypeConstructorDef
_ TypeConstructorMapping
_ = () -> Either RelationalError ()
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 DataConstructorName
_ AtomType
aType) TypeConstructorMapping
_ TypeVarMap
_ = AtomType -> Either RelationalError AtomType
forall a b. b -> Either a b
Right AtomType
aType
atomTypeForTypeConstructorValidate Bool
validate (TypeVariable DataConstructorName
tvname) TypeConstructorMapping
_ TypeVarMap
tvMap = case DataConstructorName -> TypeVarMap -> Maybe AtomType
forall k a. Ord k => k -> Map k a -> Maybe a
M.lookup DataConstructorName
tvname TypeVarMap
tvMap of
  Maybe AtomType
Nothing -> if Bool
validate then
                RelationalError -> Either RelationalError AtomType
forall a b. a -> Either a b
Left (DataConstructorName -> RelationalError
TypeConstructorTypeVarMissing DataConstructorName
tvname)
             else
               AtomType -> Either RelationalError AtomType
forall (f :: * -> *) a. Applicative f => a -> f a
pure (DataConstructorName -> AtomType
TypeVariableType DataConstructorName
tvname)
  Just AtomType
typ -> AtomType -> Either RelationalError AtomType
forall a b. b -> Either a b
Right AtomType
typ
atomTypeForTypeConstructorValidate Bool
_ (RelationAtomTypeConstructor [AttributeExprBase ()]
attrExprs) TypeConstructorMapping
tConsMap TypeVarMap
tvMap = do
  [AtomType]
resolvedAtomTypes <- (AttributeExprBase () -> Either RelationalError AtomType)
-> [AttributeExprBase ()] -> Either RelationalError [AtomType]
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
mapM (\AttributeExprBase ()
expr -> AttributeExprBase ()
-> TypeConstructorMapping
-> TypeVarMap
-> Either RelationalError AtomType
forall a.
AttributeExprBase a
-> TypeConstructorMapping
-> TypeVarMap
-> Either RelationalError AtomType
atomTypeForAttributeExpr AttributeExprBase ()
expr TypeConstructorMapping
tConsMap TypeVarMap
tvMap) [AttributeExprBase ()]
attrExprs
  let attrs :: [Attribute]
attrs = (DataConstructorName -> AtomType -> Attribute)
-> [DataConstructorName] -> [AtomType] -> [Attribute]
forall a b c. (a -> b -> c) -> [a] -> [b] -> [c]
zipWith DataConstructorName -> AtomType -> Attribute
Attribute ((AttributeExprBase () -> DataConstructorName)
-> [AttributeExprBase ()] -> [DataConstructorName]
forall a b. (a -> b) -> [a] -> [b]
map AttributeExprBase () -> DataConstructorName
forall a. AttributeExprBase a -> DataConstructorName
AE.attributeName [AttributeExprBase ()]
attrExprs) [AtomType]
resolvedAtomTypes
  AtomType -> Either RelationalError AtomType
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 DataConstructorName
-> TypeConstructorMapping
-> Maybe (TypeConstructorDef, [DataConstructorDef])
findTypeConstructor (TypeConstructor -> DataConstructorName
TC.name TypeConstructor
tCons) TypeConstructorMapping
tConss of
  Maybe (TypeConstructorDef, [DataConstructorDef])
Nothing -> RelationalError -> Either RelationalError AtomType
forall a b. a -> Either a b
Left (DataConstructorName -> RelationalError
NoSuchTypeConstructorError (TypeConstructor -> DataConstructorName
TC.name TypeConstructor
tCons))
  Just (PrimitiveTypeConstructorDef DataConstructorName
_ AtomType
aType, [DataConstructorDef]
_) -> AtomType -> Either RelationalError AtomType
forall a b. b -> Either a b
Right AtomType
aType
  Just (TypeConstructorDef
tConsDef, [DataConstructorDef]
_) -> do
          [AtomType]
tConsArgTypes <- (TypeConstructor -> Either RelationalError AtomType)
-> [TypeConstructor] -> Either RelationalError [AtomType]
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 :: [DataConstructorName]
pVarNames = TypeConstructorDef -> [DataConstructorName]
TCD.typeVars TypeConstructorDef
tConsDef
              tConsArgs :: TypeVarMap
tConsArgs = [(DataConstructorName, AtomType)] -> TypeVarMap
forall k a. Ord k => [(k, a)] -> Map k a
M.fromList ([DataConstructorName]
-> [AtomType] -> [(DataConstructorName, AtomType)]
forall a b. [a] -> [b] -> [(a, b)]
zip [DataConstructorName]
pVarNames [AtomType]
tConsArgTypes)
          AtomType -> Either RelationalError AtomType
forall a b. b -> Either a b
Right (DataConstructorName -> TypeVarMap -> AtomType
ConstructedAtomType (TypeConstructor -> DataConstructorName
TC.name TypeConstructor
tCons) TypeVarMap
tConsArgs)      

      
atomTypeForAttributeExpr :: AttributeExprBase a -> TypeConstructorMapping -> TypeVarMap -> Either RelationalError AtomType      
atomTypeForAttributeExpr :: AttributeExprBase a
-> TypeConstructorMapping
-> TypeVarMap
-> Either RelationalError AtomType
atomTypeForAttributeExpr (NakedAttributeExpr Attribute
attr) TypeConstructorMapping
_ TypeVarMap
_ = AtomType -> Either RelationalError AtomType
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Attribute -> AtomType
A.atomType Attribute
attr)
atomTypeForAttributeExpr (AttributeAndTypeNameExpr DataConstructorName
_ 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 DataConstructorName
_ AtomType
expectedAType) TypeConstructorMapping
_ =
  Bool -> Either RelationalError () -> Either RelationalError ()
forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
when (AtomType
expectedAType AtomType -> AtomType -> Bool
forall a. Eq a => a -> a -> Bool
/= AtomType
aType) (Either RelationalError () -> Either RelationalError ())
-> Either RelationalError () -> Either RelationalError ()
forall a b. (a -> b) -> a -> b
$ RelationalError -> Either RelationalError ()
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 DataConstructorName
tConsName TypeVarMap
_) (ADTypeConstructor DataConstructorName
expectedTConsName [TypeConstructor]
_) TypeConstructorMapping
_ =  Bool -> Either RelationalError () -> Either RelationalError ()
forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
when (DataConstructorName
tConsName DataConstructorName -> DataConstructorName -> Bool
forall a. Eq a => a -> a -> Bool
/= DataConstructorName
expectedTConsName) (Either RelationalError () -> Either RelationalError ())
-> Either RelationalError () -> Either RelationalError ()
forall a b. (a -> b) -> a -> b
$ RelationalError -> Either RelationalError ()
forall a b. a -> Either a b
Left (DataConstructorName -> DataConstructorName -> RelationalError
TypeConstructorNameMismatch DataConstructorName
expectedTConsName DataConstructorName
tConsName)

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

findTypeConstructor :: TypeConstructorName -> TypeConstructorMapping -> Maybe (TypeConstructorDef, [DataConstructorDef])
findTypeConstructor :: DataConstructorName
-> TypeConstructorMapping
-> Maybe (TypeConstructorDef, [DataConstructorDef])
findTypeConstructor DataConstructorName
name = ((TypeConstructorDef, [DataConstructorDef])
 -> Maybe (TypeConstructorDef, [DataConstructorDef])
 -> Maybe (TypeConstructorDef, [DataConstructorDef]))
-> Maybe (TypeConstructorDef, [DataConstructorDef])
-> TypeConstructorMapping
-> Maybe (TypeConstructorDef, [DataConstructorDef])
forall (t :: * -> *) a b.
Foldable t =>
(a -> b -> b) -> b -> t a -> b
foldr (TypeConstructorDef, [DataConstructorDef])
-> Maybe (TypeConstructorDef, [DataConstructorDef])
-> Maybe (TypeConstructorDef, [DataConstructorDef])
forall b.
(TypeConstructorDef, b)
-> Maybe (TypeConstructorDef, b) -> Maybe (TypeConstructorDef, b)
tConsFolder Maybe (TypeConstructorDef, [DataConstructorDef])
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 -> DataConstructorName
TCD.name TypeConstructorDef
tCons DataConstructorName -> DataConstructorName -> Bool
forall a. Eq a => a -> a -> Bool
== DataConstructorName
name then
                                     (TypeConstructorDef, b) -> Maybe (TypeConstructorDef, b)
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 -> DataConstructorName
A.attributeName Attribute
attrA DataConstructorName -> DataConstructorName -> Bool
forall a. Eq a => a -> a -> Bool
/= Attribute -> DataConstructorName
A.attributeName Attribute
attrB then
    RelationalError -> Either RelationalError Attribute
forall a b. a -> Either a b
Left (RelationalError -> Either RelationalError Attribute)
-> RelationalError -> Either RelationalError Attribute
forall a b. (a -> b) -> a -> b
$ Set DataConstructorName -> RelationalError
AttributeNamesMismatchError ([DataConstructorName] -> Set DataConstructorName
forall a. Ord a => [a] -> Set a
S.fromList ((Attribute -> DataConstructorName)
-> [Attribute] -> [DataConstructorName]
forall a b. (a -> b) -> [a] -> [b]
map Attribute -> DataConstructorName
A.attributeName [Attribute
attrA, Attribute
attrB]))
  else
    DataConstructorName -> AtomType -> Attribute
Attribute (Attribute -> DataConstructorName
A.attributeName Attribute
attrA) (AtomType -> Attribute)
-> Either RelationalError AtomType
-> Either RelationalError Attribute
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 DataConstructorName
tConsName TypeVarMap
resolvedTypeVarMap) (ConstructedAtomType DataConstructorName
_ TypeVarMap
unresolvedTypeVarMap) =
  DataConstructorName -> TypeVarMap -> AtomType
ConstructedAtomType DataConstructorName
tConsName (TypeVarMap -> AtomType)
-> Either RelationalError TypeVarMap
-> Either RelationalError AtomType
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 AtomType -> AtomType -> Bool
forall a. Eq a => a -> a -> Bool
== AtomType
unresolvedType then
                                                    AtomType -> Either RelationalError AtomType
forall a b. b -> Either a b
Right AtomType
typeFromRelation
                                                  else
                                                    RelationalError -> Either RelationalError AtomType
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 :: DataConstructorName
-> AtomType
-> Either RelationalError (DataConstructorName, AtomType)
resolveTypePair DataConstructorName
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 DataConstructorName -> TypeVarMap -> Maybe AtomType
forall k a. Ord k => k -> Map k a -> Maybe a
M.lookup DataConstructorName
resKey TypeVarMap
unresolvedTypeMap of
          Just AtomType
unresType -> case AtomType
unresType of
            --do we need to recurse for RelationAtomType?
            subType :: AtomType
subType@(ConstructedAtomType DataConstructorName
_ TypeVarMap
_) -> do
              AtomType
resSubType <- AtomType -> AtomType -> Either RelationalError AtomType
resolveAtomType AtomType
resType AtomType
subType
              (DataConstructorName, AtomType)
-> Either RelationalError (DataConstructorName, AtomType)
forall (f :: * -> *) a. Applicative f => a -> f a
pure (DataConstructorName
resKey, AtomType
resSubType)
            TypeVariableType DataConstructorName
_ -> (DataConstructorName, AtomType)
-> Either RelationalError (DataConstructorName, AtomType)
forall (f :: * -> *) a. Applicative f => a -> f a
pure (DataConstructorName
resKey, AtomType
resType)
            AtomType
typ -> if AtomType
typ AtomType -> AtomType -> Bool
forall a. Eq a => a -> a -> Bool
== AtomType
resType then
                     (DataConstructorName, AtomType)
-> Either RelationalError (DataConstructorName, AtomType)
forall (f :: * -> *) a. Applicative f => a -> f a
pure (DataConstructorName
resKey, AtomType
resType)
                   else
                     RelationalError
-> Either RelationalError (DataConstructorName, AtomType)
forall a b. a -> Either a b
Left (RelationalError
 -> Either RelationalError (DataConstructorName, AtomType))
-> RelationalError
-> Either RelationalError (DataConstructorName, AtomType)
forall a b. (a -> b) -> a -> b
$ AtomType -> AtomType -> RelationalError
AtomTypeMismatchError AtomType
typ AtomType
resType
          Maybe AtomType
Nothing ->
            (DataConstructorName, AtomType)
-> Either RelationalError (DataConstructorName, AtomType)
forall (f :: * -> *) a. Applicative f => a -> f a
pure (DataConstructorName
resKey, AtomType
resType) --swipe the missing type var from the expected map
  [(DataConstructorName, AtomType)]
tVarList <- ((DataConstructorName, AtomType)
 -> Either RelationalError (DataConstructorName, AtomType))
-> [(DataConstructorName, AtomType)]
-> Either RelationalError [(DataConstructorName, AtomType)]
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
mapM ((DataConstructorName
 -> AtomType
 -> Either RelationalError (DataConstructorName, AtomType))
-> (DataConstructorName, AtomType)
-> Either RelationalError (DataConstructorName, AtomType)
forall a b c. (a -> b -> c) -> (a, b) -> c
uncurry DataConstructorName
-> AtomType
-> Either RelationalError (DataConstructorName, AtomType)
resolveTypePair) (TypeVarMap -> [(DataConstructorName, AtomType)]
forall k a. Map k a -> [(k, a)]
M.toList TypeVarMap
resolvedTypeMap)
  TypeVarMap -> Either RelationalError TypeVarMap
forall (f :: * -> *) a. Applicative f => a -> f a
pure ([(DataConstructorName, AtomType)] -> TypeVarMap
forall k a. Ord k => [(k, a)] -> Map k a
M.fromList [(DataConstructorName, 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 DataConstructorName
_ TypeVarMap
tvMap) atomIn :: Atom
atomIn@(ConstructedAtom DataConstructorName
dConsName AtomType
_ [Atom]
args) TypeConstructorMapping
tConss = do
  AtomType
newType <- AtomType -> AtomType -> Either RelationalError AtomType
resolveAtomType AtomType
typeFromRelation (Atom -> AtomType
atomTypeForAtom Atom
atomIn)
  case DataConstructorName
-> TypeConstructorMapping
-> Maybe (TypeConstructorDef, DataConstructorDef)
findDataConstructor DataConstructorName
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
      Atom -> Either RelationalError Atom
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 <- ((Atom, AtomType) -> Either RelationalError Atom)
-> [(Atom, AtomType)] -> Either RelationalError [Atom]
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) ([Atom] -> [AtomType] -> [(Atom, AtomType)]
forall a b. [a] -> [b] -> [(a, b)]
zip [Atom]
args [AtomType]
atomArgTypes)
      Atom -> Either RelationalError Atom
forall (f :: * -> *) a. Applicative f => a -> f a
pure (DataConstructorName -> AtomType -> [Atom] -> Atom
ConstructedAtom DataConstructorName
dConsName AtomType
newType [Atom]
newArgs)
resolveTypeInAtom (RelationAtomType Attributes
attrs) (RelationAtom (Relation Attributes
_ RelationTupleSet
tupSet)) TypeConstructorMapping
tConss = do
  let newTups :: Either RelationalError [RelationTuple]
newTups = (RelationTuple -> Either RelationalError RelationTuple)
-> [RelationTuple] -> Either RelationalError [RelationTuple]
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 (Relation -> Atom)
-> ([RelationTuple] -> Relation) -> [RelationTuple] -> Atom
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Attributes -> RelationTupleSet -> Relation
Relation Attributes
attrs (RelationTupleSet -> Relation)
-> ([RelationTuple] -> RelationTupleSet)
-> [RelationTuple]
-> Relation
forall b c a. (b -> c) -> (a -> b) -> a -> c
. [RelationTuple] -> RelationTupleSet
RelationTupleSet ([RelationTuple] -> Atom)
-> Either RelationalError [RelationTuple]
-> Either RelationalError Atom
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Either RelationalError [RelationTuple]
newTups
resolveTypeInAtom AtomType
_ Atom
atom TypeConstructorMapping
_ = Atom -> Either RelationalError Atom
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 <- ((Atom, AtomType) -> Either RelationalError Atom)
-> [(Atom, AtomType)] -> Either RelationalError [Atom]
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) ([Atom] -> [AtomType] -> [(Atom, AtomType)]
forall a b. [a] -> [b] -> [(a, b)]
zip (Vector Atom -> [Atom]
forall a. Vector a -> [a]
V.toList Vector Atom
tupAtoms) ([AtomType] -> [(Atom, AtomType)])
-> [AtomType] -> [(Atom, AtomType)]
forall a b. (a -> b) -> a -> b
$ Attributes -> [AtomType]
A.atomTypesList Attributes
resolvedAttrs)
  RelationTuple -> Either RelationalError RelationTuple
forall a b. b -> Either a b
Right (Attributes -> Vector Atom -> RelationTuple
RelationTuple Attributes
resolvedAttrs ([Atom] -> Vector Atom
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 DataConstructorName
tConsName TypeVarMap
tVarMap) TypeConstructorMapping
tConss =
  case DataConstructorName
-> TypeConstructorMapping
-> Maybe (TypeConstructorDef, [DataConstructorDef])
findTypeConstructor DataConstructorName
tConsName TypeConstructorMapping
tConss of 
    Maybe (TypeConstructorDef, [DataConstructorDef])
Nothing -> RelationalError -> Either RelationalError ()
forall a b. a -> Either a b
Left (DataConstructorName -> RelationalError
NoSuchTypeConstructorError DataConstructorName
tConsName)
    Just (TypeConstructorDef
tConsDef, [DataConstructorDef]
_) -> case TypeConstructorDef
tConsDef of
      ADTypeConstructorDef DataConstructorName
_ [DataConstructorName]
tVarNames -> let expectedTyVarNames :: Set DataConstructorName
expectedTyVarNames = [DataConstructorName] -> Set DataConstructorName
forall a. Ord a => [a] -> Set a
S.fromList [DataConstructorName]
tVarNames
                                              actualTyVarNames :: Set DataConstructorName
actualTyVarNames = TypeVarMap -> Set DataConstructorName
forall k a. Map k a -> Set k
M.keysSet TypeVarMap
tVarMap
                                              diff :: Set DataConstructorName
diff = Set DataConstructorName
-> Set DataConstructorName -> Set DataConstructorName
forall a. Ord a => Set a -> Set a -> Set a
S.difference Set DataConstructorName
expectedTyVarNames Set DataConstructorName
actualTyVarNames in
                                          if Bool -> Bool
not (Set DataConstructorName -> Bool
forall a. Set a -> Bool
S.null Set DataConstructorName
diff) then
                                            RelationalError -> Either RelationalError ()
forall a b. a -> Either a b
Left (RelationalError -> Either RelationalError ())
-> RelationalError -> Either RelationalError ()
forall a b. (a -> b) -> a -> b
$ Set DataConstructorName
-> Set DataConstructorName -> RelationalError
TypeConstructorTypeVarsMismatch Set DataConstructorName
expectedTyVarNames Set DataConstructorName
actualTyVarNames
                                          else
                                            TypeVarMap -> TypeConstructorMapping -> Either RelationalError ()
validateTypeVarMap TypeVarMap
tVarMap TypeConstructorMapping
tConss
      TypeConstructorDef
_ -> () -> Either RelationalError ()
forall a b. b -> Either a b
Right ()
validateAtomType (RelationAtomType Attributes
attrs) TypeConstructorMapping
tConss =
  (Attribute -> Either RelationalError ())
-> Vector Attribute -> Either RelationalError ()
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 DataConstructorName
x) TypeConstructorMapping
_ = RelationalError -> Either RelationalError ()
forall a b. a -> Either a b
Left (DataConstructorName -> RelationalError
TypeConstructorTypeVarMissing DataConstructorName
x)  
validateAtomType AtomType
_ TypeConstructorMapping
_ = () -> Either RelationalError ()
forall (f :: * -> *) a. Applicative f => a -> f a
pure ()

validateAttributes :: TypeConstructorMapping -> Attributes -> Either RelationalError ()
validateAttributes :: TypeConstructorMapping -> Attributes -> Either RelationalError ()
validateAttributes TypeConstructorMapping
tConss Attributes
attrs =
  Bool -> Either RelationalError () -> Either RelationalError ()
forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
unless ([RelationalError] -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null [RelationalError]
errs) (Either RelationalError () -> Either RelationalError ())
-> Either RelationalError () -> Either RelationalError ()
forall a b. (a -> b) -> a -> b
$ RelationalError -> Either RelationalError ()
forall a b. a -> Either a b
Left ([RelationalError] -> RelationalError
someErrors [RelationalError]
errs)
  where
    errs :: [RelationalError]
errs = [Either RelationalError ()] -> [RelationalError]
forall a b. [Either a b] -> [a]
lefts ([Either RelationalError ()] -> [RelationalError])
-> [Either RelationalError ()] -> [RelationalError]
forall a b. (a -> b) -> a -> b
$ (AtomType -> Either RelationalError ())
-> [AtomType] -> [Either RelationalError ()]
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 = (AtomType -> Either RelationalError ())
-> [AtomType] -> Either RelationalError ()
forall (t :: * -> *) (m :: * -> *) a b.
(Foldable t, Monad m) =>
(a -> m b) -> t a -> m ()
mapM_ (AtomType -> TypeConstructorMapping -> Either RelationalError ()
`validateAtomType` TypeConstructorMapping
tConss) ([AtomType] -> Either RelationalError ())
-> [AtomType] -> Either RelationalError ()
forall a b. (a -> b) -> a -> b
$ TypeVarMap -> [AtomType]
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 = (Atom -> Either RelationalError ())
-> Vector Atom -> Either RelationalError ()
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 = (RelationTuple -> Either RelationalError ())
-> [RelationTuple] -> Either RelationalError ()
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 DataConstructorName
_ AtomType
dConsType [Atom]
atomArgs) TypeConstructorMapping
tConss = do
  AtomType -> TypeConstructorMapping -> Either RelationalError ()
validateAtomType AtomType
dConsType TypeConstructorMapping
tConss
  (Atom -> Either RelationalError ())
-> [Atom] -> Either RelationalError ()
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
_ = () -> Either RelationalError ()
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 DataConstructorName
_) AtomType
x = AtomType -> Either RelationalError AtomType
forall a b. b -> Either a b
Right AtomType
x
atomTypeVerify AtomType
x (TypeVariableType DataConstructorName
_) = AtomType -> Either RelationalError AtomType
forall a b. b -> Either a b
Right AtomType
x
atomTypeVerify x :: AtomType
x@(ConstructedAtomType DataConstructorName
tConsNameA TypeVarMap
tVarMapA) (ConstructedAtomType DataConstructorName
tConsNameB TypeVarMap
tVarMapB) 
  | DataConstructorName
tConsNameA DataConstructorName -> DataConstructorName -> Bool
forall a. Eq a => a -> a -> Bool
/= DataConstructorName
tConsNameB = RelationalError -> Either RelationalError AtomType
forall a b. a -> Either a b
Left (DataConstructorName -> DataConstructorName -> RelationalError
TypeConstructorNameMismatch DataConstructorName
tConsNameA DataConstructorName
tConsNameB)
  | Bool -> Bool
not (TypeVarMap -> TypeVarMap -> Bool
typeVarMapsVerify TypeVarMap
tVarMapA TypeVarMap
tVarMapB) = RelationalError -> Either RelationalError AtomType
forall a b. a -> Either a b
Left (DataConstructorName -> TypeVarMap -> TypeVarMap -> RelationalError
TypeConstructorTypeVarsTypesMismatch DataConstructorName
tConsNameA TypeVarMap
tVarMapA TypeVarMap
tVarMapB)
  | Bool
otherwise = AtomType -> Either RelationalError AtomType
forall a b. b -> Either a b
Right AtomType
x

atomTypeVerify x :: AtomType
x@(RelationAtomType Attributes
attrs1) y :: AtomType
y@(RelationAtomType Attributes
attrs2) = do
  ((Attribute, Attribute) -> Either RelationalError AtomType)
-> [(Attribute, Attribute)] -> Either RelationalError ()
forall (t :: * -> *) (m :: * -> *) a b.
(Foldable t, Monad m) =>
(a -> m b) -> t a -> m ()
mapM_ (\(Attribute
attr1,Attribute
attr2) -> let name1 :: DataConstructorName
name1 = Attribute -> DataConstructorName
A.attributeName Attribute
attr1
                               name2 :: DataConstructorName
name2 = Attribute -> DataConstructorName
A.attributeName Attribute
attr2 in
                               if DataConstructorName -> [DataConstructorName] -> Bool
forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
notElem DataConstructorName
"_" [DataConstructorName
name1, DataConstructorName
name2] Bool -> Bool -> Bool
&& DataConstructorName
name1 DataConstructorName -> DataConstructorName -> Bool
forall a. Eq a => a -> a -> Bool
/= DataConstructorName
name2 then 
                                 RelationalError -> Either RelationalError AtomType
forall a b. a -> Either a b
Left (RelationalError -> Either RelationalError AtomType)
-> RelationalError -> Either RelationalError AtomType
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)) ([(Attribute, Attribute)] -> Either RelationalError ())
-> [(Attribute, Attribute)] -> Either RelationalError ()
forall a b. (a -> b) -> a -> b
$ Vector (Attribute, Attribute) -> [(Attribute, Attribute)]
forall a. Vector a -> [a]
V.toList (Vector Attribute
-> Vector Attribute -> Vector (Attribute, Attribute)
forall a b. Vector a -> Vector b -> Vector (a, b)
V.zip (Attributes -> Vector Attribute
attributesVec Attributes
attrs1) (Attributes -> Vector Attribute
attributesVec Attributes
attrs2))
  AtomType -> Either RelationalError AtomType
forall (m :: * -> *) a. Monad m => a -> m a
return AtomType
x
atomTypeVerify AtomType
x AtomType
y = if AtomType
x AtomType -> AtomType -> Bool
forall a. Eq a => a -> a -> Bool
== AtomType
y then
                       AtomType -> Either RelationalError AtomType
forall a b. b -> Either a b
Right AtomType
x
                     else
                       RelationalError -> Either RelationalError AtomType
forall a b. a -> Either a b
Left (RelationalError -> Either RelationalError AtomType)
-> RelationalError -> Either RelationalError AtomType
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 = TypeVarMap -> Set DataConstructorName
forall k a. Map k a -> Set k
M.keysSet TypeVarMap
a Set DataConstructorName -> Set DataConstructorName -> Bool
forall a. Eq a => a -> a -> Bool
== TypeVarMap -> Set DataConstructorName
forall k a. Map k a -> Set k
M.keysSet TypeVarMap
b Bool -> Bool -> Bool
&& ([AtomType] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length ([AtomType] -> Int)
-> ([Either RelationalError AtomType] -> [AtomType])
-> [Either RelationalError AtomType]
-> Int
forall b c a. (b -> c) -> (a -> b) -> a -> c
. [Either RelationalError AtomType] -> [AtomType]
forall a b. [Either a b] -> [b]
rights) [Either RelationalError AtomType]
zipped Int -> Int -> Bool
forall a. Eq a => a -> a -> Bool
== TypeVarMap -> Int
forall k a. Map k a -> Int
M.size TypeVarMap
a
  where
    zipped :: [Either RelationalError AtomType]
zipped = ((DataConstructorName, AtomType)
 -> (DataConstructorName, AtomType)
 -> Either RelationalError AtomType)
-> [(DataConstructorName, AtomType)]
-> [(DataConstructorName, AtomType)]
-> [Either RelationalError AtomType]
forall a b c. (a -> b -> c) -> [a] -> [b] -> [c]
zipWith
      ((((DataConstructorName, AtomType), (DataConstructorName, AtomType))
 -> Either RelationalError AtomType)
-> (DataConstructorName, AtomType)
-> (DataConstructorName, AtomType)
-> Either RelationalError AtomType
forall a b c. ((a, b) -> c) -> a -> b -> c
curry (\ ((DataConstructorName
_, AtomType
v1), (DataConstructorName
_, AtomType
v2)) -> AtomType -> AtomType -> Either RelationalError AtomType
atomTypeVerify AtomType
v1 AtomType
v2))
      (TypeVarMap -> [(DataConstructorName, AtomType)]
forall k a. Map k a -> [(k, a)]
M.toAscList TypeVarMap
a)
      (TypeVarMap -> [(DataConstructorName, AtomType)]
forall k a. Map k a -> [(k, a)]
M.toAscList TypeVarMap
b)

prettyAtomType :: AtomType -> T.Text
prettyAtomType :: AtomType -> DataConstructorName
prettyAtomType (RelationAtomType Attributes
attrs) = DataConstructorName
"relation {" DataConstructorName -> DataConstructorName -> DataConstructorName
`T.append` DataConstructorName -> [DataConstructorName] -> DataConstructorName
T.intercalate DataConstructorName
"," ((Attribute -> DataConstructorName)
-> [Attribute] -> [DataConstructorName]
forall a b. (a -> b) -> [a] -> [b]
map Attribute -> DataConstructorName
prettyAttribute (Vector Attribute -> [Attribute]
forall a. Vector a -> [a]
V.toList (Attributes -> Vector Attribute
attributesVec Attributes
attrs))) DataConstructorName -> DataConstructorName -> DataConstructorName
`T.append` DataConstructorName
"}"
prettyAtomType (ConstructedAtomType DataConstructorName
tConsName TypeVarMap
typeVarMap) = DataConstructorName
tConsName DataConstructorName -> DataConstructorName -> DataConstructorName
`T.append` [DataConstructorName] -> DataConstructorName
T.concat (((DataConstructorName, AtomType) -> DataConstructorName)
-> [(DataConstructorName, AtomType)] -> [DataConstructorName]
forall a b. (a -> b) -> [a] -> [b]
map (DataConstructorName, AtomType) -> DataConstructorName
showTypeVars (TypeVarMap -> [(DataConstructorName, AtomType)]
forall k a. Map k a -> [(k, a)]
M.toList TypeVarMap
typeVarMap))
  where
    showTypeVars :: (DataConstructorName, AtomType) -> DataConstructorName
showTypeVars (DataConstructorName
_, TypeVariableType DataConstructorName
x) = DataConstructorName
" " DataConstructorName -> DataConstructorName -> DataConstructorName
forall a. Semigroup a => a -> a -> a
<> DataConstructorName
x
    showTypeVars (DataConstructorName
tyVarName, AtomType
aType) = DataConstructorName
" (" DataConstructorName -> DataConstructorName -> DataConstructorName
`T.append` DataConstructorName
tyVarName DataConstructorName -> DataConstructorName -> DataConstructorName
`T.append` DataConstructorName
"::" DataConstructorName -> DataConstructorName -> DataConstructorName
`T.append` AtomType -> DataConstructorName
prettyAtomType AtomType
aType DataConstructorName -> DataConstructorName -> DataConstructorName
`T.append` DataConstructorName
")"
-- 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 DataConstructorName
x) = DataConstructorName
x
prettyAtomType AtomType
aType = Int -> DataConstructorName -> DataConstructorName
T.take (DataConstructorName -> Int
T.length DataConstructorName
fullName Int -> Int -> Int
forall a. Num a => a -> a -> a
- DataConstructorName -> Int
T.length DataConstructorName
"AtomType") DataConstructorName
fullName
  where fullName :: DataConstructorName
fullName = ([Char] -> DataConstructorName
T.pack ([Char] -> DataConstructorName)
-> (AtomType -> [Char]) -> AtomType -> DataConstructorName
forall b c a. (b -> c) -> (a -> b) -> a -> c
. AtomType -> [Char]
forall a. Show a => a -> [Char]
show) AtomType
aType

prettyAttribute :: Attribute -> T.Text
prettyAttribute :: Attribute -> DataConstructorName
prettyAttribute (Attribute DataConstructorName
_ (TypeVariableType DataConstructorName
x)) = DataConstructorName
x
prettyAttribute Attribute
attr = Attribute -> DataConstructorName
A.attributeName Attribute
attr DataConstructorName -> DataConstructorName -> DataConstructorName
`T.append` DataConstructorName
"::" DataConstructorName -> DataConstructorName -> DataConstructorName
`T.append` AtomType -> DataConstructorName
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 = (AtomType -> AtomType -> TypeVarMap)
-> [AtomType] -> [AtomType] -> [TypeVarMap]
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!
  (TypeVarMap -> TypeVarMap -> Either RelationalError TypeVarMap)
-> TypeVarMap -> [TypeVarMap] -> Either RelationalError TypeVarMap
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 DataConstructorName (Either RelationalError AtomType)
inter = (DataConstructorName
 -> AtomType -> AtomType -> Either RelationalError AtomType)
-> TypeVarMap
-> TypeVarMap
-> Map DataConstructorName (Either RelationalError AtomType)
forall k a b c.
Ord k =>
(k -> a -> b -> c) -> Map k a -> Map k b -> Map k c
M.intersectionWithKey (\DataConstructorName
tvName AtomType
vala AtomType
valb -> 
                                                if AtomType
vala AtomType -> AtomType -> Bool
forall a. Eq a => a -> a -> Bool
/= AtomType
valb then
                                                  RelationalError -> Either RelationalError AtomType
forall a b. a -> Either a b
Left (DataConstructorName -> AtomType -> AtomType -> RelationalError
AtomFunctionTypeVariableMismatch DataConstructorName
tvName AtomType
vala AtomType
valb)
                                                else
                                                  AtomType -> Either RelationalError AtomType
forall a b. b -> Either a b
Right AtomType
vala) TypeVarMap
acc TypeVarMap
tvmap
                errs :: [RelationalError]
errs = [Either RelationalError AtomType] -> [RelationalError]
forall a b. [Either a b] -> [a]
lefts (Map DataConstructorName (Either RelationalError AtomType)
-> [Either RelationalError AtomType]
forall k a. Map k a -> [a]
M.elems Map DataConstructorName (Either RelationalError AtomType)
inter)
            case [RelationalError]
errs of
              [] -> TypeVarMap -> Either RelationalError TypeVarMap
forall (f :: * -> *) a. Applicative f => a -> f a
pure ([TypeVarMap] -> TypeVarMap
forall (f :: * -> *) k a.
(Foldable f, Ord k) =>
f (Map k a) -> Map k a
M.unions [TypeVarMap]
tvmaps)
              [RelationalError]
errs' -> RelationalError -> Either RelationalError TypeVarMap
forall a b. a -> Either a b
Left ([RelationalError] -> RelationalError
someErrors [RelationalError]
errs')) TypeVarMap
forall k a. Map k a
M.empty [TypeVarMap]
tvmaps
  
resolveTypeVariable :: AtomType -> AtomType -> TypeVarMap
resolveTypeVariable :: AtomType -> AtomType -> TypeVarMap
resolveTypeVariable (TypeVariableType DataConstructorName
tv) AtomType
typ = DataConstructorName -> AtomType -> TypeVarMap
forall k a. k -> a -> Map k a
M.singleton DataConstructorName
tv AtomType
typ
resolveTypeVariable (ConstructedAtomType DataConstructorName
_ TypeVarMap
_) (ConstructedAtomType DataConstructorName
_ TypeVarMap
actualTvMap) = TypeVarMap
actualTvMap
resolveTypeVariable AtomType
_ AtomType
_ = TypeVarMap
forall k a. Map k a
M.empty

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

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

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

--given two AtomTypes x,y