forked from carp-lang/Carp
-
Notifications
You must be signed in to change notification settings - Fork 0
/
Validate.hs
134 lines (126 loc) · 5.92 KB
/
Validate.hs
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132
133
134
module Validate where
import Control.Monad (foldM)
import Data.List (nubBy, (\\))
import qualified Env as E
import Obj
import qualified Reify as R
import qualified TypeCandidate as TC
import TypeError
import TypePredicates
import Types
--------------------------------------------------------------------------------
-- Public
-- | Determine whether a given type candidate is a valid type.
validateType :: TC.TypeCandidate -> Either TypeError ()
validateType candidate =
do
checkDuplicateMembers candidate
checkMembers candidate
checkKindConsistency candidate
--------------------------------------------------------------------------------
-- Private
-- | Checks whether any field names in the type are used more than once.
checkDuplicateMembers :: TC.TypeCandidate -> Either TypeError ()
checkDuplicateMembers candidate =
let allFields = fmap TC.fieldName (TC.getFields candidate)
uniqueFields = nubBy (==) allFields
duplicates = allFields \\ uniqueFields
in if null duplicates
then Right ()
else Left (DuplicatedMembers (map R.symbol duplicates))
-- | Returns an error if one of the types fields can't be used as a member type.
checkMembers :: TC.TypeCandidate -> Either TypeError ()
checkMembers candidate =
let tenv = TC.getTypeEnv candidate
env = TC.getValueEnv candidate
tys = concat (map TC.fieldTypes (TC.getFields candidate))
in mapM_ (canBeUsedAsMemberType (TC.getName candidate) (TC.getRestriction candidate) tenv env (TC.getVariables candidate)) tys
-- | Returns an error if the type variables in the body of the type and variables in the head of the type are of incompatible kinds.
checkKindConsistency :: TC.TypeCandidate -> Either TypeError ()
checkKindConsistency candidate =
let allFieldTypes = concat (map TC.fieldTypes (TC.getFields candidate))
allGenerics = filter isTypeGeneric $ allFieldTypes
in case areKindsConsistent allGenerics of
Left var -> Left (InconsistentKinds var (map R.reify allFieldTypes))
_ -> pure ()
-- | Can this type be used as a member for a deftype?
canBeUsedAsMemberType :: String -> TC.TypeVarRestriction -> TypeEnv -> Env -> [Ty] -> Ty -> Either TypeError ()
canBeUsedAsMemberType tname typeVarRestriction typeEnv globalEnv typeVariables ty =
case ty of
UnitTy -> pure ()
IntTy -> pure ()
FloatTy -> pure ()
DoubleTy -> pure ()
ByteTy -> pure ()
LongTy -> pure ()
BoolTy -> pure ()
StringTy -> pure ()
PatternTy -> pure ()
CharTy -> pure ()
FuncTy {} -> pure ()
PointerTy UnitTy -> pure ()
PointerTy inner ->
canBeUsedAsMemberType tname typeVarRestriction typeEnv globalEnv typeVariables inner
-- Struct variables may appear as complete applications or individual
-- components in the head of a definition; that is the forms:
-- ((Foo (f a b)) [x (f a b)])
-- ((Foo f a b) [x f y a z b])
-- are both valid, but restrict their types differently. In the former,
-- `f` may only appear in complete applications over `a` and `b`, in
-- other words, `f` is closed over `a` and `b`. In the latter, f may
-- flexibly be used as a type variable of nullary kind, or as a type
-- variable of unary kind `(Foo f a b) [x (f a) y (f b)])` so long as
-- the kinds of each occasion of `f` are consistent.
--
-- Likewise, the types denoted by:
-- ((Foo (f a) b) ...)
-- and
-- ((Foo (f a) (f b)) ...)
-- differ.
-- Attempt the first, more restrictive formulation first.
struct@(StructTy name tyVars) ->
checkVar struct <> checkStruct name tyVars
v@(VarTy _) -> checkVar v
_ -> Left (InvalidMemberType ty (R.reify ty))
where
checkStruct :: Ty -> [Ty] -> Either TypeError ()
checkStruct (ConcreteNameTy (SymPath [] "Array")) [innerType] =
canBeUsedAsMemberType tname typeVarRestriction typeEnv globalEnv typeVariables innerType
checkStruct (ConcreteNameTy path@(SymPath _ name)) vars =
case E.getTypeBinder typeEnv name <> E.findTypeBinder globalEnv path of
Right (Binder _ (XObj (Lst (XObj (ExternalType _) _ _ : _)) _ _)) ->
pure ()
Right (Binder _ (XObj (Lst (XObj (Deftype t) _ _ : _)) _ _)) ->
checkInhabitants t >> foldM (\_ typ -> canBeUsedAsMemberType tname typeVarRestriction typeEnv globalEnv typeVariables typ) () vars
Right (Binder _ (XObj (Lst (XObj (DefSumtype t) _ _ : _)) _ _)) ->
checkInhabitants t >> foldM (\_ typ -> canBeUsedAsMemberType tname typeVarRestriction typeEnv globalEnv typeVariables typ) () vars
_ -> Left (NotAmongRegisteredTypes ty (R.reify ty))
where
checkInhabitants :: Ty -> Either TypeError ()
checkInhabitants (StructTy _ vs) =
if length vs == length vars
then pure ()
else Left (UninhabitedConstructor ty (R.reify ty) (length vs) (length vars))
checkInhabitants _ = Left (InvalidMemberType ty (R.reify ty))
checkStruct v@(VarTy _) vars =
canBeUsedAsMemberType tname typeVarRestriction typeEnv globalEnv typeVariables v
>> foldM (\_ typ -> canBeUsedAsMemberType tname typeVarRestriction typeEnv globalEnv typeVariables typ) () vars
checkStruct _ _ = error "checkstruct"
checkVar :: Ty -> Either TypeError ()
checkVar variable =
case typeVarRestriction of
TC.AllowAny -> pure ()
TC.OnlyNamesInScope ->
if any (isCaptured variable) typeVariables
then pure ()
else Left (InvalidMemberType ty (R.reify ty))
where
-- If a variable `a` appears in a higher-order polymorphic form, such as `(f a)`
-- `a` may be used as a member, sans `f`, but `f` may not appear
-- without `a`.
isCaptured :: Ty -> Ty -> Bool
isCaptured v@(VarTy _) t@(VarTy _) = t == v
isCaptured sa@(StructTy (VarTy _) _) sb@(StructTy (VarTy _) _) = sa == sb
isCaptured v@(VarTy _) (StructTy _ vars) = v `elem` vars
-- Not a variable.
isCaptured _ _ = True