git.iko.soy/project-m36
on d64cdeb help sign in
project-m36/src/lib/ProjectM36/AtomType.hs
310 lines 19 kB history raw
1module ProjectM36.AtomType where
2import ProjectM36.Base
3import qualified ProjectM36.TypeConstructorDef as TCD
4import qualified ProjectM36.TypeConstructor as TC
5import qualified ProjectM36.DataConstructorDef as DCD
6import ProjectM36.MiscUtils
7import ProjectM36.Error
8import ProjectM36.DataTypes.Primitive
9import qualified ProjectM36.Attribute as A
10import qualified Data.Vector as V
11import qualified Data.Set as S
12import qualified Data.List as L
13import Data.Maybe (isJust)
14import Data.Either (rights, lefts)
15import Control.Monad.Writer
16import qualified Data.Map as M
17import qualified Data.Text as T
19findDataConstructor :: DataConstructorName -> TypeConstructorMapping -> Maybe (TypeConstructorDef, DataConstructorDef)
20findDataConstructor dName = foldr tConsFolder Nothing
21 where
22 tConsFolder (tCons, dConsList) accum = if isJust accum then
23 accum
24 else
25 case findDCons dConsList of
26 Just dCons -> Just (tCons, dCons)
27 Nothing -> Nothing
28 findDCons dConsList = case filter (\dCons -> DCD.name dCons == dName) dConsList of
29 [] -> Nothing
30 [dCons] -> Just dCons
31 _ -> error "More than one data constructor with the same name found"
33-- | Scan the atom types and return the resultant ConstructedAtomType or error.
34-- Used in typeFromAtomExpr to validate argument types.
35atomTypeForDataConstructorName :: DataConstructorName -> [AtomType] -> TypeConstructorMapping -> Either RelationalError AtomType
36-- search for the data constructor and resolve the types' names
37atomTypeForDataConstructorName dConsName atomTypesIn tConsList =
38 case findDataConstructor dConsName tConsList of
39 Nothing -> Left (NoSuchDataConstructorError dConsName)
40 Just (tCons, dCons) -> do
41 typeVars <- resolveDataConstructorTypeVars dCons atomTypesIn tConsList
42 pure (ConstructedAtomType (TCD.name tCons) typeVars)
44atomTypeForDataConstructorDefArg :: DataConstructorDefArg -> AtomType -> TypeConstructorMapping -> Either RelationalError AtomType
45atomTypeForDataConstructorDefArg (DataConstructorDefTypeConstructorArg tCons) aType tConss =
46 case isValidAtomTypeForTypeConstructor aType tCons tConss of
47 Just err -> Left err
48 Nothing -> Right aType
50atomTypeForDataConstructorDefArg (DataConstructorDefTypeVarNameArg _) aType _ = Right aType --any type is OK
52--reconcile the atom-in types with the type constructors
53isValidAtomTypeForTypeConstructor :: AtomType -> TypeConstructor -> TypeConstructorMapping -> Maybe RelationalError
54isValidAtomTypeForTypeConstructor aType (PrimitiveTypeConstructor _ expectedAType) _ = if expectedAType /= aType then Just (AtomTypeMismatchError expectedAType aType) else Nothing
56--lookup constructor name and check if the incoming atom types are valid
57isValidAtomTypeForTypeConstructor (ConstructedAtomType tConsName _) (ADTypeConstructor expectedTConsName _) _ = if tConsName /= expectedTConsName then Just (TypeConstructorNameMismatch expectedTConsName tConsName) else Nothing
59isValidAtomTypeForTypeConstructor aType tCons _ = Just (AtomTypeTypeConstructorReconciliationError aType (TC.name tCons))
61-- | Used to determine if the atom arguments can be used with the data constructor.
62-- | This is the entry point for type-checking from RelationalExpression.hs.
63atomTypeForDataConstructor :: TypeConstructorMapping -> DataConstructorName -> [AtomType] -> Either RelationalError AtomType
64atomTypeForDataConstructor tConss dConsName atomArgTypes =
65 --lookup the data constructor
66 case findDataConstructor dConsName tConss of
67 Nothing -> Left (NoSuchDataConstructorError dConsName)
68 Just (tCons, dCons) -> do
69 --validate that the type constructor arguments are fulfilled in the data constructor
70 typeVars <- resolveDataConstructorTypeVars dCons atomArgTypes tConss
71 pure (ConstructedAtomType (TCD.name tCons) typeVars)
73-- | Walks the data and type constructors to extract the type variable map.
74resolveDataConstructorTypeVars :: DataConstructorDef -> [AtomType] -> TypeConstructorMapping -> Either RelationalError TypeVarMap
75resolveDataConstructorTypeVars dCons@(DataConstructorDef _ defArgs) aTypeArgs tConss = do
76 let defCount = length defArgs
77 argCount = length aTypeArgs
78 if defCount /= argCount then
79 Left (ConstructedAtomArgumentCountMismatchError defCount argCount)
80 else do
81 maps <- mapM (\(dCons',aTypeArg) -> resolveDataConstructorArgTypeVars dCons' aTypeArg tConss) (zip (DCD.fields dCons) aTypeArgs)
82 --if any two maps have the same key and different values, this indicates a type arg mismatch
83 let typeVarMapFolder valMap acc = case acc of
84 Left err -> Left err
85 Right accMap -> if accMap `M.isSubmapOf` valMap then
86 Right (M.union accMap valMap)
87 else
88 Left (DataConstructorTypeVarsMismatch (DCD.name dCons) accMap valMap)
89 case foldr typeVarMapFolder (Right M.empty) maps of
90 Left err -> Left err
91 Right typeVarMaps -> pure typeVarMaps
92 --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.
95-- | Attempt to match the data constructor argument to a type constructor type variable.
96resolveDataConstructorArgTypeVars :: DataConstructorDefArg -> AtomType -> TypeConstructorMapping -> Either RelationalError TypeVarMap
97resolveDataConstructorArgTypeVars (DataConstructorDefTypeConstructorArg tCons) aType tConss = resolveTypeConstructorTypeVars tCons aType tConss
99resolveDataConstructorArgTypeVars (DataConstructorDefTypeVarNameArg pVarName) aType _ = Right (M.singleton pVarName aType)
101resolveTypeConstructorTypeVars :: TypeConstructor -> AtomType -> TypeConstructorMapping -> Either RelationalError TypeVarMap
102resolveTypeConstructorTypeVars (PrimitiveTypeConstructor _ pType) aType _ =
103 if aType /= pType then
104 Left (AtomTypeMismatchError pType aType)
105 else
106 Right M.empty
108resolveTypeConstructorTypeVars (ADTypeConstructor tConsName _) (ConstructedAtomType tConsName' pVarMap') tConss =
109 if tConsName /= tConsName' then
110 Left (TypeConstructorNameMismatch tConsName tConsName')
111 else
112 case findTypeConstructor tConsName tConss of
113 Nothing -> Left (NoSuchTypeConstructorName tConsName)
114 Just (tConsDef, _) -> let expectedPVarNames = S.fromList (TCD.typeVars tConsDef) in
115 if M.keysSet pVarMap' `S.isSubsetOf` expectedPVarNames then
116 Right pVarMap'
117 else
118 Left (TypeConstructorTypeVarsMismatch expectedPVarNames (M.keysSet pVarMap'))
119resolveTypeConstructorTypeVars (TypeVariable tvName) typ _ = Right (M.singleton tvName typ)
120resolveTypeConstructorTypeVars (ADTypeConstructor tConsName _) typ _ = Left (TypeConstructorAtomTypeMismatch tConsName typ)
122-- check that type vars on the right also appear on the left
123-- check that the data constructor names are unique
124validateTypeConstructorDef :: TypeConstructorDef -> [DataConstructorDef] -> [RelationalError]
125validateTypeConstructorDef tConsDef dConsList = execWriter $ do
126 let duplicateDConsNames = dupes (L.sort (map DCD.name dConsList))
127 mapM_ tell [map DataConstructorNameInUseError duplicateDConsNames]
128 let leftSideVars = S.fromList (TCD.typeVars tConsDef)
129 rightSideVars = S.unions (map DCD.typeVars dConsList)
130 varsDiff = S.difference leftSideVars rightSideVars
131 mapM_ tell [map DataConstructorUsesUndeclaredTypeVariable (S.toList varsDiff)]
132 pure ()
135-- | Create an atom type iff all type variables are provided.
136-- Either Int Text -> ConstructedAtomType "Either" {Int , Text}
137atomTypeForTypeConstructor :: TypeConstructor -> TypeConstructorMapping -> TypeVarMap -> Either RelationalError AtomType
138atomTypeForTypeConstructor (PrimitiveTypeConstructor _ aType) _ _ = Right aType
139atomTypeForTypeConstructor (TypeVariable tvname) _ tvMap = case M.lookup tvname tvMap of
140 Nothing -> Right (TypeVariableType tvname)
141 Just typ -> Right typ
142atomTypeForTypeConstructor tCons tConss tvMap = case findTypeConstructor (TC.name tCons) tConss of
143 Nothing -> Left (NoSuchTypeConstructorError (TC.name tCons))
144 Just (tConsDef, _) -> do
145 tConsArgTypes <- mapM (\tConsArg -> atomTypeForTypeConstructor tConsArg tConss tvMap) (TC.arguments tCons)
146 let pVarNames = TCD.typeVars tConsDef
147 tConsArgs = M.fromList (zip pVarNames tConsArgTypes)
148 Right (ConstructedAtomType (TC.name tCons) tConsArgs)
150findTypeConstructor :: TypeConstructorName -> TypeConstructorMapping -> Maybe (TypeConstructorDef, [DataConstructorDef])
151findTypeConstructor name = foldr tConsFolder Nothing
152 where
153 tConsFolder (tCons, dConsList) accum = if TCD.name tCons == name then
154 Just (tCons, dConsList)
155 else
156 accum
158resolveAtomType :: AtomType -> AtomType -> Either RelationalError AtomType
159resolveAtomType (ConstructedAtomType tConsName resolvedTypeVarMap) (ConstructedAtomType _ unresolvedTypeVarMap) = do
160 tVarMap <- resolveAtomTypesInTypeVarMap resolvedTypeVarMap unresolvedTypeVarMap
161 pure (ConstructedAtomType tConsName tVarMap)
162resolveAtomType typeFromRelation unresolvedType = if typeFromRelation == unresolvedType then
163 Right typeFromRelation
164 else
165 Left (AtomTypeMismatchError typeFromRelation unresolvedType)
167-- this could be optimized to reduce new tuple creation- if anyatomtype does not appear, just return the original typevarmap
168resolveAtomTypesInTypeVarMap :: TypeVarMap -> TypeVarMap -> Either RelationalError TypeVarMap
169resolveAtomTypesInTypeVarMap resolvedTypeMap unresolvedTypeMap = do
170 {-
171 let resKeySet = traceShowId $ M.keysSet resolvedTypeMap
172 unresKeySet = traceShowId $ M.keysSet unresolvedTypeMap
173 when (resKeySet /= unresKeySet) (Left $ TypeConstructorTypeVarsMismatch resKeySet unresKeySet)
176 let lookupOrDef key tMap = case M.lookup key tMap of
177 Nothing -> Left (TypeConstructorTypeVarMissing key)
178 Just val -> Right val
179 -}
180 let resolveTypePair resKey resType =
181 -- if the key is missing in the unresolved type map, then fill it in with the value from the resolved map
182 case M.lookup resKey unresolvedTypeMap of
183 Just unresType -> case unresType of
184 --do we need to recurse for RelationAtomType?
185 subType@(ConstructedAtomType _ _) -> do
186 resSubType <- resolveAtomType resType subType
187 pure (resKey, resSubType)
188 otherType -> pure (resKey, otherType)
189 Nothing ->
190 pure (resKey, resType) --swipe the missing type var from the expected map
191 tVarList <- mapM (uncurry resolveTypePair) (M.toList resolvedTypeMap)
192 pure (M.fromList tVarList)
194-- | See notes at `resolveTypesInTuple`. The typeFromRelation must not include any wildcards.
195resolveTypeInAtom :: AtomType -> Atom -> Either RelationalError Atom
196resolveTypeInAtom typeFromRelation atomIn@(ConstructedAtom dConsName _ args) = do
197 newType <- resolveAtomType typeFromRelation (atomTypeForAtom atomIn)
198 pure (ConstructedAtom dConsName newType args)
199resolveTypeInAtom _ atom = Right atom
201-- | 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.
202-- 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.
203resolveTypesInTuple :: Attributes -> RelationTuple -> Either RelationalError RelationTuple
204resolveTypesInTuple resolvedAttrs (RelationTuple _ tupAtoms) = do
205 newAtoms <- mapM (\(atom, resolvedType) -> resolveTypeInAtom resolvedType atom) (zip (V.toList tupAtoms) $ map A.atomType (V.toList resolvedAttrs))
206 Right (RelationTuple resolvedAttrs (V.fromList newAtoms))
208-- | Validate that the type is provided with complete type variables for type constructors.
209validateAtomType :: AtomType -> TypeConstructorMapping -> Either RelationalError ()
210validateAtomType typ@(ConstructedAtomType tConsName tVarMap) tConss =
211 case findTypeConstructor tConsName tConss of
212 Nothing -> Left (TypeConstructorAtomTypeMismatch tConsName typ)
213 Just (tConsDef, _) -> case tConsDef of
214 ADTypeConstructorDef _ tVarNames -> let expectedTyVarNames = S.fromList tVarNames
215 actualTyVarNames = M.keysSet tVarMap
216 diff = S.difference expectedTyVarNames actualTyVarNames in
217 if not (S.null diff) then
218 Left $ TypeConstructorTypeVarsMismatch expectedTyVarNames actualTyVarNames
219 else
220 Right ()
221 _ -> Right ()
222validateAtomType _ _ = Right ()
224validateTuple :: RelationTuple -> TypeConstructorMapping -> Either RelationalError ()
225validateTuple (RelationTuple _ atoms) tConss = mapM_ (\a -> validateAtomType (atomTypeForAtom a) tConss) atoms
227-- | Determine if two types are equal or compatible (including special handling for TypeVar x).
228atomTypeVerify :: AtomType -> AtomType -> Either RelationalError AtomType
229atomTypeVerify (TypeVariableType _) x = Right x
230atomTypeVerify x (TypeVariableType _) = Right x
231atomTypeVerify x@(ConstructedAtomType tConsNameA tVarMapA) (ConstructedAtomType tConsNameB tVarMapB)
232 | tConsNameA /= tConsNameB = Left (TypeConstructorNameMismatch tConsNameA tConsNameB)
233 | not (typeVarMapsVerify tVarMapA tVarMapB) = Left (TypeConstructorTypeVarsTypesMismatch tConsNameA tVarMapA tVarMapB)
234 | otherwise = Right x
236atomTypeVerify x@(RelationAtomType attrs1) y@(RelationAtomType attrs2) = do
237 mapM_ (\(attr1,attr2) -> let name1 = A.attributeName attr1
238 name2 = A.attributeName attr2 in
239 if notElem "_" [name1, name2] && name1 /= name2 then
240 Left $ AtomTypeMismatchError x y
241 else
242 atomTypeVerify (A.atomType attr1) (A.atomType attr2)) $ V.toList (V.zip attrs1 attrs2)
243 return x
244atomTypeVerify (IntervalAtomType typA) (IntervalAtomType typB) = atomTypeVerify typA typB
245atomTypeVerify x y = if x == y then
246 Right x
247 else
248 Left $ AtomTypeMismatchError x y
250-- | Determine if two typeVars are logically compatible.
251typeVarMapsVerify :: TypeVarMap -> TypeVarMap -> Bool
252typeVarMapsVerify a b = M.keysSet a == M.keysSet b && (length . rights) (map (\((_,v1),(_,v2)) -> atomTypeVerify v1 v2) (zip (M.toAscList a) (M.toAscList b))) == M.size a
254prettyAtomType :: AtomType -> T.Text
255prettyAtomType (RelationAtomType attrs) = "relation {" `T.append` T.intercalate "," (map prettyAttribute (V.toList attrs)) `T.append` "}"
256prettyAtomType (ConstructedAtomType tConsName typeVarMap) = tConsName `T.append` T.concat (map showTypeVars (M.toList typeVarMap))
257 where
258 showTypeVars (tyVarName, aType) = " (" `T.append` tyVarName `T.append` "::" `T.append` prettyAtomType aType `T.append` ")"
259-- 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?)
260prettyAtomType (TypeVariableType x) = "?TypeVariableType " <> x <> "?"
261prettyAtomType (IntervalAtomType tv) = "Interval (" <> prettyAtomType tv <> ")"
262prettyAtomType aType = T.take (T.length fullName - T.length "AtomType") fullName
263 where fullName = (T.pack . show) aType
265prettyAttribute :: Attribute -> T.Text
266prettyAttribute attr = A.attributeName attr `T.append` "::" `T.append` prettyAtomType (A.atomType attr)
268resolveTypeVariables :: [AtomType] -> [AtomType] -> Either RelationalError TypeVarMap
269resolveTypeVariables expectedArgTypes actualArgTypes = do
270 let tvmaps = zipWith resolveTypeVariable expectedArgTypes actualArgTypes
271 --if there are any new keys which don't have equal values then we have a conflict!
272 foldM (\acc tvmap -> do
273 let inter = M.intersectionWithKey (\tvName vala valb ->
274 if vala /= valb then
275 Left (AtomFunctionTypeVariableMismatch tvName vala valb)
276 else
277 Right vala) acc tvmap
278 errs = lefts (M.elems inter)
279 case errs of
280 [] -> pure (M.unions tvmaps)
281 errs' -> Left (someErrors errs')) M.empty tvmaps
283resolveTypeVariable :: AtomType -> AtomType -> TypeVarMap
284resolveTypeVariable (TypeVariableType tv) typ = M.singleton tv typ
285resolveTypeVariable (IntervalAtomType ityp) typ = resolveTypeVariable ityp typ
286resolveTypeVariable (ConstructedAtomType _ _) (ConstructedAtomType _ actualTvMap) = actualTvMap
287resolveTypeVariable _ _ = M.empty
289resolveFunctionReturnValue :: AtomFunctionName -> TypeVarMap -> AtomType -> Either RelationalError AtomType
290resolveFunctionReturnValue funcName tvMap (ConstructedAtomType tCons retMap) = do
291 let diff = M.difference retMap tvMap
292 if M.null diff then
293 pure (ConstructedAtomType tCons (M.intersection tvMap retMap))
294 else
295 Left (AtomFunctionTypeVariableResolutionError funcName (fst (head (M.toList diff))))
296resolveFunctionReturnValue funcName tvMap (IntervalAtomType tv) = IntervalAtomType <$> resolveFunctionReturnValue funcName tvMap tv
297resolveFunctionReturnValue funcName tvMap (TypeVariableType tvName) = case M.lookup tvName tvMap of
298 Nothing -> Left (AtomFunctionTypeVariableResolutionError funcName tvName)
299 Just typ -> pure typ
300resolveFunctionReturnValue _ _ typ = pure typ
302-- convert a typevarmap and data constructor definition into a list of atomtypes which represent the arguments-- no type variables are allowed to remain
303resolvedAtomTypesForDataConstructorDefArgs :: TypeConstructorMapping -> TypeVarMap -> DataConstructorDef -> Either RelationalError [AtomType]
304resolvedAtomTypesForDataConstructorDefArgs tConsMap tvMap (DataConstructorDef _ args) = mapM (resolvedAtomTypeForDataConstructorDefArg tConsMap tvMap) args
306resolvedAtomTypeForDataConstructorDefArg :: TypeConstructorMapping -> TypeVarMap -> DataConstructorDefArg -> Either RelationalError AtomType
307resolvedAtomTypeForDataConstructorDefArg tConsMap tvMap (DataConstructorDefTypeConstructorArg typCons) = atomTypeForTypeConstructor typCons tConsMap tvMap
308resolvedAtomTypeForDataConstructorDefArg _ tvMap (DataConstructorDefTypeVarNameArg tvName) = case M.lookup tvName tvMap of
309 Nothing -> Left (DataConstructorUsesUndeclaredTypeVariable tvName)
310 Just typ -> Right typ